精益中的一些基本命题逻辑证明

Question

[我只是阅读了Lean的文档，并尝试完成3.7. Exercises，但还没有全部完成，但是这里是前四个练习（没有经典推理）：

变量p q r：属性

-∧和的可交换性例如：p q = q对不起例如：p∨q↔p =：=对不起

-∧和as的关联性例如：（p q）r r p p（q r）：=对不起例如：（p q）r r p p（q r）：=对不起

这是我在前四个练习中所做的：

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)))

我认为这是有效的，但是很长一段时间，这是我们能做到的最好吗，或者有更好的方法在精益中编写这些证明，任何建议都将不胜感激。

Answer 1

如果导入精益数学的library，则策略by tauto!应该解决所有这些问题。另外，这些都是已经存在的库定理，它们的名称类似于and_comm。

我不认为从第一性原则可以更简短地证明这些陈述。缩短某些证明的唯一方法是删除have和show，并使它们的可读性降低。这是我对or_assoc的证明，与您的证明基本相同，但没有have和show。

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
iff.intro 
  (λ h, or.elim h (λ hpq, or.elim hpq or.inl (λ hq, or.inr (or.inl hq))) (λ hr, or.inr (or.inr hr)))
  (λ h, or.elim h (λ hp, (or.inl (or.inl hp))) (λ hqr, or.elim hqr (λ hq, or.inl (or.inr hq)) or.inr))