PROSAGA码农传奇-精益-精益中的一些基本命题逻辑证明

我只是阅读了Lean的文档，然后尝试做3.7。练习， 并没有完成所有的人都还没有，但这里有前四次的练习（不含古典推理）：变量pqr：属性-∧和的可交换性 示例：p∧q↔q∧p：=对不起 示例：p∨q↔q∨p：=对不起-∧和as的关联性 例如：（p∧q）∧r↔p∧（q∧r）：=对不起 例子：（p∨q）∨r↔p∨（q∨r）：=对不起这是我为前四个练习所做的：
<pre><code>variables p q r : Prop

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := 
iff.intro
  (assume h : p ∧ q,
    show q ∧ p, from and.intro (and.right h) (and.left h))
  (assume h : q ∧ p,
    show p ∧ q, from and.intro (and.right h) (and.left h))

example : p ∨ q ↔ q ∨ p :=
iff.intro
  (assume h : p ∨ q,
  show q ∨ p, from 
  or.elim h
     (assume hp : p,
       show q ∨ p, from or.intro_right q hp)
     (assume hq : q,
       show q ∨ p, from or.intro_left p hq))
  (assume h : q ∨ p,
  show p ∨ q, from 
  or.elim h
     (assume hq : q,
       show p ∨ q, from or.intro_right p hq)
     (assume hp : p,
       show p ∨ q, from or.intro_left q hp))

-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := 
iff.intro
  (assume h: (p ∧ q) ∧ r,
    have hpq : p ∧ q, from and.elim_left h,
    have hqr : q ∧ r, from and.intro (and.right hpq) (and.right h),
    show p ∧ (q ∧ r), from and.intro (and.left hpq) (hqr))
  (assume h: p ∧ (q ∧ r),
    have hqr : q ∧ r, from and.elim_right h,
    have hpq : p ∧ q, from and.intro (and.left h) (and.left hqr),
    show (p ∧ q) ∧ r, from and.intro (hpq) (and.right hqr))

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
iff.intro
 (assume hpqr : (p ∨ q) ∨ r, 
 show p ∨ (q ∨ r), from or.elim hpqr
 (assume hpq : p ∨ q,
 show p ∨ (q ∨ r), from or.elim hpq
 (assume hp : p,
 show p ∨ (q ∨ r), from or.intro_left (q ∨ r) hp)
 (assume hq : q,
 have hqr : q ∨ r, from or.intro_left r hq,
 show p ∨ (q ∨ r), from or.intro_right p hqr))
 (assume hr : r,
 have hqr : q ∨ r, from or.intro_right q hr,
 show p ∨ (q ∨ r), from or.intro_right p hqr))
 (assume hpqr : p ∨ (q ∨ r),
 show (p ∨ q) ∨ r, from or.elim hpqr
 (assume hp : p,
 have hpq : (p ∨ q), from or.intro_left q hp,
 show (p ∨ q) ∨ r, from or.intro_left r hpq)
 (assume hqr : (q ∨ r),
 show (p ∨ q) ∨ r, from or.elim hqr
 (assume hq : q,
 have hpq : (p ∨ q), from or.intro_right p hq,
 show (p ∨ q) ∨ r, from or.intro_left r hpq)
 (assume hr : r,
 show (p ∨ q) ∨ r, from or.intro_right (p ∨ q) hr)))
</code></pre>我认为这是有效的，但是很长一段时间，这是我们能做到的最好吗，或者有更好的方法在精益中编写这些证明，任何建议都将不胜感激。