lean - 在精益中证明 p 或 q 当且仅当 q 或 p

Question

尝试在精益文档中进行第3 章练习，但很难理解所有术语，因为我对编写证明的了解几乎为零。我想了解更多，但需要一些帮助。

我一直在尝试解决这个例子：

example : p ∨ q ↔ q ∨ p := sorry

不知道从哪里开始。是否有我缺少解释的答案键？

Answer 1

如果 TPIL 中的解释没有帮助，那么自然数游戏的命题世界可能会更好https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/。我已经给出了一个解决方案，但如果 TPIL 中的解释不是很有帮助，我不确定它是否会有帮助。

这是一个解决方案

example : p ∨ q ↔ q ∨ p := 
iff.intro
  (assume hpq : p ∨ q, or.elim hpq 
    (assume hp : p, or.inr hp)
    (assume hq : q, or.inl hq))
  (assume hqp : q ∨ p, or.elim hqp
    (assume hq : q, or.inr hq)
    (assume hp : p, or.inl hp))

iff.intro是你必须用来证明一个iff. 它要求两个论点，左蕴涵的证明和右蕴涵的证明。

为了证明一个蕴涵p -> q，你通常必须写出来assume hp : p,，然后q在给定假设的情况下证明p

如果你有 的证明p q，那么你可以用它or.elim来拆分成 case pis true 和 case qis true。这两个参数是p -> [your goal]和q -> [your goal]。

or.inl并且是通过证明左手边或右手边or.inr来证明陈述的工具。or