前端之家

  1. 首页
  2. 问答

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

• 问答

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

  

变量p q r：属性

     

-∧和的可交换性
  例如：p∧q↔q∧p：=对不起
  例如：p∨q↔q∨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,from or.intro_right q hp)
     (assume hq : q,from or.intro_left p hq))
  (assume h : q ∨ p,show p ∨ q,from 
  or.elim h
     (assume hq : q,from or.intro_right p hq)
     (assume hp : p,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),from and.elim_right h,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,from or.elim hpq
          (assume hp : p,from or.intro_left (q ∨ r) hp)
          (assume hq : q,have hqr : q ∨ r,from or.intro_left r hq,from or.intro_right p hqr))
      (assume hr : r,from or.intro_right q hr,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,from or.intro_left r hpq)
    (assume hqr : (q ∨ r),from or.elim hqr
        (assume hq : q,from or.intro_right p hq,from or.intro_left r hpq)
        (assume hr : r,from or.intro_right (p ∨ q) hr)))

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

shangcangcun 回答：精益中的一些基本命题逻辑证明

如果导入精益数学的library，则策略if(user.isEmailVerified == false){ print('Email not verified') //in console screen setState((){ errorMessage='Email Not Verified'; }); // in android screen } 应该解决所有这些问题。另外，这些都是已经具有诸如by tauto!之类名称的库定理。

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

show
,

另一个想法。对于我（也是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
leanlogicproof
本文链接：https://www.f2er.com/2869158.html

大家都在问