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.
    2023 - 2026