Coq学习——《SoftwareFoundation》Volume1.9ProofObjects
ProofObjects: The CurryHoward Correspondence
“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 “CurryHoward correspondence“.
propositions ~ types
proofs ~ data values
E.g. the definition of ev and proof of (ev 4).
Proof Scripts
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].
1 

 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.
1 

Quantifiers, Implications, Functions
Proof of propositions including implications map to construct function(hypotheses as params and conclusion as results)
The equivalent proof/def of ex_plus4.
1 

Programmig with Tactics
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].
1 

End with [Defined] rather than [Qed] make the definition “transparent”. NEED BETTER UNDERSTANDING.
Logical Connectives as Inductive Types
归纳定义足够用于表达我们目前为止遇到的大多数的联结词。事实上， 只有全称量化（以及作为特殊情况的蕴含式）是 Coq 内置的，所有其他的都是被归纳 定义的。
Here we know what conjunction [/] actually means.
1 

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.
1 

Disjunction
The inductive definition.
1 

Existential Quantification
Construct the witness of such a Prop
1 

[True] and [False]
Both simple
1 

[False] is an inductive type with no constructors. NO WAY TO BUILD AN EVIDENCE OR MAKE A DEFINITION!!
Equality
Inductive 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].
1 

1 

本博客所有文章除特别声明外，均采用 CC BYSA 4.0 协议 ，转载请注明出处！