Proof Objects

Curry-Howard correspondence, proof objects, propositional extensionality, proof irrelevance

When Coq is following a proof script (sequence of tactics), it is gradually constructing a proof object.

You can also simply construct the required evidence by hand (by supplying a proof term).

Here is a proof that 4 is even using tactics:

Theorem ev_4'' : ev 4.
Proof.
  Show Proof.
  apply ev_SS.
  Show Proof.
  apply ev_SS.
  Show Proof.
  apply ev_0.
  Show Proof.
Qed.

Here is a proof that 4 is even by supplying evidence (a proof object).

Definition ev_4''' : ev 4 :=
  ev_SS 2 (ev_SS 0 ev_0).

Consider the following:

Theorem ev_plus4 : forall n, ev n → ev (4 + n).
Proof.
  intros n H. simpl.
  apply ev_SS.
  apply ev_SS.
  apply H.
Qed.

The corresponding proof object would be an expression whose type is the proposition forall n, ev n → ev (4 + n) itself:

Definition ev_plus4' : ∀ n, ev n → ev (4 + n) :=
  fun (n : nat) ⇒ fun (H : ev n) ⇒
    ev_SS (S (S n)) (ev_SS n H).

We realise that implication -> and quantification forall are the same thing - both introduce something that can be used in the body of the proof object.

-> is a degenerate use of forall where there is no need to give a name to the thing being introduced.

In general, P -> Q is just syntactic sugar for forall (_:P), Q-.

This notion is particularly important when constructing proof objects for propositions with quantifiers.

We can build proofs by supplying a proof object (i.e. a program). It turns out, we can also build program using tactics.

Definition add1 : nat → nat.
intro n.
Show Proof.
apply S.
Show Proof.
apply n. Defined.
Print add1.
(* ==>
    add1 = fun n : nat => S n
         : nat -> nat
*)
Compute add1 2.
(* ==> 3 : nat *)

Logical connectives can be inductively defined.

• Conjunction. To prove P /\ Q, prove both P and Q.

  Inductive and (P Q : Prop) : Prop :=
    | conj : P → Q → and P Q.
  

• Disjunction.

To prove P \/ Q, either prove P or prove Q.

Inductive or (P Q : Prop) : Prop :=
  | or_introl : P → or P Q
  | or_intror : Q → or P Q.

• Existential Quantification

  To prove exists x. P x, provide a witness x and a proof of P x.

  Inductive ex {A : Type} (P : A → Prop) : Prop :=
    | ex_intro : ∀ x : A, P x → ex P.
  

• True and False

  True has one constructor I and False has no constructor.

  Inductive True : Prop :=
    | I : True.
  
  Inductive False : Prop := .
  

Equality is defined as:

  Inductive eq {X:Type} : X → X → Prop :=
  | eq_refl : ∀ x, eq x x.

There is another notion of equivalence similar to functional extensionality:

Definition propositional_extensionality : Prop :=
  ∀ (P Q : Prop), (P ↔ Q) → P = Q.

Quoting,

Propositional extensionality asserts that if two propositions are equivalent – i.e., each implies the other – then they are in fact equal. The proof objects for the propositions might be syntactically different terms. But propositional extensionality overlooks that, just as functional extensionality overlooks the syntactic differences between functions.

2 stars, standard

2 stars, standard

2 stars, standard

2 stars, standard

2 stars, standard

1 star, standard

1 star, standard

2 stars, standard

2 stars, standard

2 stars, standard

3 stars, standard, optional

2 stars, standard

3 stars, standard

3 stars, standard

2 stars, standard

1 star, advanced

1 star, advanced

3 stars, advanced

Stuck at showing that pf1 and pf2 is equal to I.