Coq学习——《Software-Foundation》Volume1.9-ProofObjects

ProofObjects: The Curry-Howard 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 “Curry-Howard 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
2
3
4
5
6
7
8
9
10
Theorem ev_4'' : ev 4.
Proof.
Show Proof. (* ?Goal *)
apply ev_SS.
Show Proof. (* (ev_SS 2 ?Goal) *)
apply ev_SS.
Show Proof. (* (ev_SS 2 (ev_SS 0 ?Goal)) *)
apply ev_0.
Show Proof. (* (ev_SS 2 (ev_SS 0 ev_0)) *)
Qed.
  • 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
2
3
4
5
6
7
8
9
10
11
12
13
14
Definition ev_4''' : ev 4 :=
ev_SS 2 (ev_SS 0 ev_0).

(** All these different ways of building the proof lead to exactly the
same evidence being saved in the global environment. *)

Print ev_4.
(* ===> ev_4 = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)
Print ev_4'.
(* ===> ev_4' = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)
Print ev_4''.
(* ===> ev_4'' = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)
Print ev_4'''.
(* ===> ev_4''' = ev_SS 2 (ev_SS 0 ev_0) : ev 4 *)

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
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Theorem ev_plus4 : forall n, ev n -> ev (4 + n).
Proof.
intros n H. simpl.
apply ev_SS.
apply ev_SS.
apply H.
Qed.

Definition ev_plus4' : forall n, ev n -> ev (4 + n) :=
fun (n : nat) => fun (H : ev n) =>
ev_SS (S (S n)) (ev_SS n H).

Definition ev_plus4'' (n : nat) (H : ev n)
: ev (4 + n) :=
ev_SS (S (S n)) (ev_SS n H).

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
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Definition add1 : nat -> nat.
intro n.
Show Proof.
apply S.
Show Proof.
apply n.
Show Proof.
(* Qed. *)
Defined. (* not Qed. *)

Print add1.
(* ==>
add1 = fun n : nat => S n
: nat -> nat
*)

Compute add1 2.
(* ==> 3 : nat *)

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
2
Inductive and (P Q : Prop) : Prop :=
| conj : P -> Q -> and P Q.

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
2
3
4
5
6
7
8
9
10
Definition conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R :=
fun (P Q R : Prop) =>
fun (H1 : P /\ Q) =>
fun (H2 : Q /\ R) =>
match H1 with
| conj P Q =>
match H2 with
| conj Q R => conj P R
end
end.

Disjunction

The inductive definition.

1
2
3
Inductive or (P Q : Prop) : Prop :=
| or_introl : P -> or P Q
| or_intror : Q -> or P Q.

Existential Quantification

Construct the witness of such a Prop

1
2
Inductive ex {A : Type} (P : A -> Prop) : Prop :=
| ex_intro : forall x : A, P x -> ex P.

[True] and [False]

Both simple

1
2
3
4
5
6
7
Inductive True : Prop :=
| I : True.

(** [False] is equally simple -- indeed, so simple it may look
syntactically wrong at first glance! *)

Inductive False : Prop := .

[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
2
Inductive eq {X:Type} : X -> X -> Prop :=
| eq_refl : forall x, eq x x.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
(** **** Exercise: 2 stars, standard (equality__leibniz_equality) 

The inductive definition of equality implies _Leibniz equality_:
what we mean when we say "[x] and [y] are equal" is that every
property on [P] that is true of [x] is also true of [y]. *)

Lemma equality__leibniz_equality : forall (X : Type) (x y: X),
x == y -> forall P:X->Prop, P x -> P y.
Proof.
intros X x y H.
induction H.
intros P HP.
apply HP.
Show Proof.
Qed.
(** [] *)

(** **** Exercise: 3 stars, standard, optional (leibniz_equality__equality)

Show that, in fact, the inductive definition of equality is
_equivalent_ to Leibniz equality. Hint: the proof is quite short;
about all you need to do is to invent a clever property [P] to
instantiate the antecedent.*)

Lemma leibniz_equality__equality : forall (X : Type) (x y: X),
(forall P:X->Prop, P x -> P y) -> x == y.
Proof.
intros X x y H.
Check (eq x x).
Check (eq x y).
Check (H (eq x)).
apply (H (eq x)).
apply eq_refl.
Qed.