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.