4 ms·

That is also true, but its proof is different. Proofs have types; the "and.intro hq hp" part has type "q /\ p". If you change it to "and.intro hp hp", you can p

That is also true, but its proof is different. Proofs have types; the "and.intro hq hp" part has type "q /\ p". If you change it to "and.intro hp hp", you can prove "p /\ p". That is, the following works: theorem and_commutative (p q : Prop) : p ∧ q → p ∧ p := assume hpq : p ∧ q, have hp : p, from and.left hpq, have hq : q, from and.right hpq, show p ∧ p, from and.intro hp hp (and then you should rename it from "and_commutative" to something else, and you can remove the "hq" line)

gmfawcett 8y ago
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.
- tom_mellior 8y ago
  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_commutative%20(p%20q%20:%20Prop)%20:%20p%20%E2%88%A7%20q%20%E2%86%92%20q%20%E2%88%A7%20p%20:=%0Abegin%20intros,%20simp%20*%20end https://leanprover.github.io/live/3.4.1/#code=theorem%20and_...
  - gmfawcett 8y ago
    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...)
    - tom_mellior 8y ago
      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.
  - kevinzz 8y ago
    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).

gmfawcett 8y ago

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.

tom_mellior 8y ago
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_commutative%20(p%20q%20:%20Prop)%20:%20p%20%E2%88%A7%20q%20%E2%86%92%20q%20%E2%88%A7%20p%20:=%0Abegin%20intros,%20simp%20*%20end https://leanprover.github.io/live/3.4.1/#code=theorem%20and_...
- gmfawcett 8y ago
  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...)
  - tom_mellior 8y ago
    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.
- kevinzz 8y ago
  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).