Theorem Proving in Lean

Re:Theorem Proving in Lean by gmfawcett on Tuesday May 29, 2018 @09:45AM (#17179074)

Just for the sake of comparison, the same proof in Coq might be written:

    Theorem and_commutative (P Q : Prop) : P ∧ Q → Q ∧ P.
    Proof.
      intros [HP HQ].
      split.
        - apply HQ.
        - apply HP. 
    Qed.

"intros [HP HQ]" separates the two conjuncts of the hypothesis into separate hypotheses (P, and Q); "split" breaks the goal (Q ∧ P) into two subgoals (Q, and P), and the two applications prove the two subgoals.

It could also be written:

    Theorem and_commutative_2 (P Q : Prop) : P ∧ Q → Q ∧ P.
    Proof. tauto. Qed.

...as the proof tactic "tauto" is capable of proving this (simple) theorem immediately.

[ Parent | on HN ]

Re:Theorem Proving in Lean by tom_mellior on Tuesday May 29, 2018 @10:10AM (#17179292)

There are tons of other ways of writing the same thing in Lean too, of course. Here is one:

    theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
    begin intros, simp * end

https://leanprover.github.io/live/3.4.1/#code=theorem%20and_...

[ Parent | on HN ]

Re:Theorem Proving in Lean by kevinzz on Tuesday May 29, 2018 @06:47PM (#17183448)

In Lean you could do

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := by cc

for a tactic proof and

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := λ ⟨h,j⟩,⟨j,h⟩

for a term proof (just write down the function).

[ Parent | on HN ]

Re:Theorem Proving in Lean by gmfawcett on Tuesday May 29, 2018 @11:04AM (#17179754)

Cool, thanks for this. I've yet to play with Lean, but it looks very interesting! (I'm hoping that my time invested in Coq will transfer reasonably well...)

[ Parent | on HN ]

Re:Theorem Proving in Lean by tom_mellior on Tuesday May 29, 2018 @03:32PM (#17182250)

You're welcome! I'm in a similar boat, coming to this tutorial from a Coq background (and some Isabelle/HOL). I'm pleasantly surprised how similar many things are. But I'm also a bit disappointed because I was under the impression that Lean was relying on automation via Z3 a lot more. Not quite done with the tutorial yet, so there might still be some material to this effect coming up, but I'm afraid not.

[ Parent | on HN ]