精益中的几个基本命题逻辑证明

Question

我刚看了一下精益的文档，试着做3.7。练习，

还没有全部完成，但以下是前四项练习(没有经典推理)：

变量p q r:支柱 -∧和∨的交换性 例:p∧q↔q∧p p对不起 例:p∨q↔q∨p p对不起 -∧和∨的结合性 例：(p∧q)∧r↔p∧(q∧r) 例：(p∨q)∨r↔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

如果您导入精益的数学的图书馆，那么策略by tauto!应该解决所有这些问题。此外，这些都是具有像and_comm这样名字的库定理。

我认为从第一性原理看，这些陈述没有任何较短的证明。缩短一些证明的唯一方法是删除haves和shows并降低它们的可读性。这是我对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))

Answer 2

只是另一个想法。对我来说(也是一个瘦身的初学者)，如果我把校样分成几个小块，就更容易阅读了。下面的代码片段是在几个步骤中用策略编写的第二个交换性的证明。

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