2008 - 02 - 11

(* This is the proof of an implication so it is a function. *)
Lemma n_le_SSn : forall m n, m <= n -> m <= S (S n). 
Proof.
exact (
  fun (m : nat) (n : nat) (H : m <= n) => le_S _ _ (le_S _ _ H)
).
Defined.
(* We use Defined instead of Qed so we can evaluate the proof later. Proofs
that are transparent like this one slow Coq down, since their bodies as well 
as their types need to be managed by the Coq engine. *)

(* We can write the same proof using the intro tactic. The intro tactic builds
the header of our function for us so that we need only write the body. *) 
Goal forall m n, m <= n -> m <= S (S n). 
Proof.
intros m n H.
Show Proof.
exact (le_S _ _ (le_S _ _ H)).
Qed.

(* Here we use modus ponens to prove 2 <= 4. *) 
Lemma two_le_four : 2 <= 4.
Proof.
exact (n_le_SSn _ _ (le_n _)).
Defined.
(* Note that we are using the Curry-Howard isomorphism in a new way. 
The proof is not a value, it is a function application. Its type is
the same as our earlier proofs that 2 <= 4 so it is just as good. *) 

(* When we evaluate the proof the normal form is the same as the 
proof we constructed last time. *)
Eval compute in two_le_four.

(* To prove the following, we must use recursion on n. *)
(* Working out the structure of the fixpoint is not too hard, but Coq will not
accept it unless we give it some further type annotations. 
We'll do this next time. *)
Lemma O_le_n : forall n, O <= n.
Proof.
exact (
  fix F (n : nat) =>
    match n with
    | O => le_n O
    | S n' => le_S O n' (F n')
    end
).