标签: gallina

Theorem law_of_contradiction : forall (P Q : Prop),\n  P /\\ ~P -> Q.\nProof.\n  intros P Q P_and_not_P.\n  destruct P_and_not_P as [P_holds not_P].\n

我正在尝试真正理解这个intros关键字。假设我们想证明P /\\ ~P -> Q。好的，以某种方式intros P Q介绍P和Q。但是这是什么意思？它能识别出P要Q证明的事物吗？关于什么P_and_not_P？它是什么？为什么P和Q使用相同的名称，而is却P_and_not_P定义了一个名称？

更新：

看起来它是逐项匹配的：

Theorem modus_tollens: forall (P Q : Prop),\n  (P -> Q) -> ~Q -> ~P.\nProof.\nintro P.\nintro Q.\nintro P_implies_Q.\nintro not_q.\nintro not_p.\n

给出

P Q \xe2\x84\x99\nP_implies_Q P \xe2\x86\x92 …