Coq | Rye Land

Coq

字数: 0

‌
‌
‌
‌
‌
‌
‌
‌
‌
‌
‌
‌
‌
‌
‌

Basic Definitions

Math	Coq	Meaning
		Whenever all of (hypothesis) are true then so is (goal).
		Apply a predicate to some arguments

notion image

Proof tactics

Implication

Introduction: The tactic intro takes a goal of the form P → Q and makes P a hypothesis, and makes Q the new goal.

根据括号分隔，每一次消耗一个 -> 前面的命题（前提）
The tactic intros will perform a series of intro commands.

最后一个箭头后的内容自动变为 goal

Elimination: If you have some hypothesis H of the form P→Q then the tactic apply H implements implie s elimination, transforming a goal Q into the goal P.

用于将一个命题应用到当前目标上，然后尝试生成一个或多个子目标。

例题

Conjunction

(AND)

Introduction: Given a goal of the form P ∧ Q, the tactic split replaces it with two new sub-goals, P and Q

Elimination: To use a hypothesis H of the form P ∧ Q, just type elim H - followed by intros, this will have the effect of creating two new assumptions, P and Q

例题

Disjunction

(OR)

Introduction: Replaces a goal consisting of a disjunction P V Q with just P or Q

use left if you have a proof of P
use right if you have a proof of Q

Elimination: To use a hypothesis H of the form P V Q, just type elim H - this will have the effect of creating two sub sub-proofs (after introsintros), one where P is a hypothesis, and one where Q is a hypothesis.

例题

Negation

The tactic red will reduce a goal of the form P to its more primitive form P→False.

If, for some , you have hypothesis stating both and , then the tactic contradiction tells Coq that the goal (whatever it is) is proved.

If you feel that a contradiction is implied by your hypothesis, you can make the proof a bit easier by using the tactic absurd P to replaces the current goal with two new sub-goals, and

例题

构造性逻辑 (Constructive Logic) 是Coq 默认使用的演绎推理逻辑

它假设每个命题不是真就是假，即使可以单独证明其中任何一个。

其核心规则是排中律 (Law of the Excluded Middle, LEM)，即不认为或对于所有的命题都是真的。

经典逻辑 (Classical Logic) 接受排中律，即或对于所有的命题都是真的

在 Coq 中要通常需要引入特定的库，从而在证明中使用 elim(classic P)

Forall

Introduction: If you have a goal of the form forall x: D, P you just need to do intro to introduce a new variable x: D into the context.

Note that Coq will rename th e variable if there’s an x there already.

Elimination: If you have a hypothesis H of the form forall x D, P, then pick some current variable of type D , say V and just use elim (H V).

Exist

Introduction: If you have a goal of the form exists x: D, (P x) you just need to identify some current variable v of type D, and then use exists v . Coq will then ask you to prove the sub-goal (P v)

Elimination: If you have a hypothesis H of the form exists x: D, P, then just use elim H - if you then do some intros you’ll see that you’ve now got a new variable of type D, and an assertion that P holds for it.