“Algorithms are the computational content of proofs.” —Robert Harper
In Coq we have seen machanisms for
- Programming: using inductive data types and functions over them.
- Proving: using inductive propositions, implication, universal quantification.
Not separate, but related.
Types and propositions
between [:] as “has type” and [:] as “is a proof of” or “is evidence for” — is called the “Curry-Howard correspondence“.
propositions ~ types proofs ~ data values
E.g. the definition of ev and proof of (ev 4).
Gradually constructing a proof object — a term whose type is the proposition being proved!!
The tactics between [Proof] and [Qed] tell it how to build up a term of the required type.
Let’s see what happens with the help of [Show Proof command].
- A proof script is to fill the hole(?Goal).
- Tactic proofs are useful and convenient but not essential. We can use [Definition] rather than [Theorem] to give a global name directly to the evidence.
Proof of propositions including implications map to construct function(hypotheses as params and conclusion as results)
The equivalent proof/def of ex_plus4.
We terminate the [Definition] with a [.] rather than with [:=] followed by a term. This tells Coq to enter _proof scripting mode_ to build an object of type [nat -> nat]. And terminate the proof with [Defined] rather than [Qed].
End with [Defined] rather than [Qed] make the definition “transparent”. NEED BETTER UNDERSTANDING.
归纳定义足够用于表达我们目前为止遇到的大多数的联结词。事实上， 只有全称量化（以及作为特殊情况的蕴含式）是 Coq 内置的，所有其他的都是被归纳 定义的。
Here we know what conjunction [/] actually means.
This clarify why [destruct] and [intros] patterns can be used on a conjunctive hypothesis. Case analysis allow us to consider all possible ways in which [P /\ Q] was proved. Her just one (from the [conj] constructor).
Exercise: construct a proof object for the following proposition.
The inductive definition.
Construct the witness of such a Prop
[False] is an inductive type with no constructors. NO WAY TO BUILD AN EVIDENCE OR MAKE A DEFINITION!!
The Inductive definition is equivalent to Leibniz equality.
From inductive definition, the only way to construct a equal pair is applying the constructor [eq_refl] to a type [X] and value [x : X].
本博客所有文章除特别声明外，均采用 CC BY-SA 4.0 协议 ，转载请注明出处！