Help with Homework

Stream: new members

[Jeremy Teitelbaum]

Hi, I'm trying to do the homework problem:

example : (p \to q \to r) \iff (p \and q \to r) := sorry,

from the Theorem Proving in Lean book. I can do this using tactics, but I'm trying to use native lean syntax.
I can prove one direction (I think):

example : (p → q → r) → (p ∧ q → r) :=
  (assume hpqr : p → q → r,
    assume hpaq : p ∧ q,
      show r, from hpqr hpaq.left hpaq.right)

but I can't seem to figure out how to do the other direction. FWIW I used the "apply" tactic in my solution to the version from Kevin's course, but I can't seem to translate that into lean.

I also can't figure out why my first block of code doesn't get translated into proper unicode symbols but my second one does.....

[Eric Wieser]

Regarding unicode translation, sometimes the plugin doesn't turn on in new files until you switch to another file and back

[Eric Wieser]

The definition you need in the other direction is docs#and.elim

[Eric Wieser]

But maybe that's cheating; in which case, you need to use and.rec (which has no documentation as its native)

[Mario Carneiro]

I think the book uses and.left and and.right

[Mario Carneiro]

except, I guess that's the direction that was done already. For the other direction you need and.intro

[Stuart Presnell]

In this case you can translate your tactic proof into a proof term. A natural tactic proof you might arrive at by "following your nose" is:

example : (p ∧ q → r) → (p → q → r) :=
begin
  intros h hp hq,
  apply h,
  exact ⟨hp, hq⟩,
end

(where the last line is suggested by library_search).

Then you can combine the last two lines, since the final line is just providing the argument for the h on the penultimate line:

example : (p ∧ q → r) → (p → q → r) :=
begin
  intros h hp hq,
  apply h ⟨hp, hq⟩,
end

Now, since apply finishes the job, we could replace it with exact.

Finally, since all we're doing now is taking some inputs and returning an expression built out of those inputs, we can rewrite this as a lambda expression:

example : (p ∧ q → r) → (p → q → r) :=
λ h hp hq, h ⟨hp, hq⟩

[Jeremy Teitelbaum]

Thanks a lot, I recast your solution into the assume/show format I was following and came up with this.

example : (p ∧ q → r) → (p → q → r) :=
  assume hpqr : p ∧ q → r,
    assume hp : p,
      assume hq : q,
        show  r, from hpqr ⟨ hp, hq ⟩