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

Question

我刚刚看了精益的文档，并尝试做3.7. Exercises，
还没有全部做完，但这是前四个练习（没有经典推理):

variables p q r : Prop

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := sorry
example : p ∨ q ↔ q ∨ p := sorry

-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry

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

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

如果您导入 Lean 的数学 library，那么策略 by tauto! 应该可以解决所有这些问题。此外，这些都是库定理，名称如 and_comm.

我认为没有任何来自第一原理的这些陈述的更短证明。缩短某些证明的唯一方法是删除 haves 和 shows 并降低它们的可读性。这是我对 or_assoc 的证明，它与你的基本相同，但没有 haves 和 shows。

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

Answer 2

只是另一个想法。对于我（也是 LEAN 的初学者）来说，如果我将它们分解成更小的部分，则更容易阅读校样。下面的代码片段是第二个交换性的证明属性用战术写成几步

--- 2) Prove p ∨ q ↔ q ∨ p
-- Easier if using these results first:
theorem LR2_11 : p → p ∨ q :=
begin
    intros hp,
    exact or.intro_left q hp
end
#check LR2_11 
theorem LR2_12 : p → q ∨ p :=
begin
    intros hp,
    exact or.intro_right q hp
end
#check LR2_12 
theorem LR2_2 : p ∨ q → q ∨ p :=
begin
    intros p_or_q, 
    exact or.elim p_or_q (LR2_12 p q) (LR2_11 q p)
end
theorem Comm2_2 : p ∨ q ↔ q ∨ p :=
begin
    exact iff.intro (LR2_2 p q) (LR2_2 q p)
end
#check Comm2_2

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

Some basic Propositional Logic Proofs in Lean

logic

proof

lean