Software Foundations: The Curry-Howard Correspondence

ProofObjects.v

Import Nat.

Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, even n -> even (S (S n)).

Theorem even_8 : even 8.
Proof. apply even_S, even_S, even_S, even_S, even_O. Qed.

Definition even_8' : even 8 :=
  even_S 6 (even_S 4 (even_S 2 (even_S 0 (even_O)))).

Theorem even_plus_4 : forall n,
  even n -> even (4 + n).
Proof. intros. apply even_S, even_S, H. Qed.

Definition even_plus_4' n : even n -> even (4 + n) :=
  fun H => even_S (2 + n) (even_S n H).

Definition succ : nat -> nat.
  intro n.
  apply S.
  apply n.
Defined.

Definition conj_fact : forall P Q R, P /\ Q -> Q /\ R -> P /\ R.
  intros P Q R [HP _] [_ HR].
  split. apply HP. apply HR.
Defined.

Definition or_comm : forall P Q, P \/ Q -> Q \/ P.
  intros P Q [HP | HQ].
  - right. apply HP.
  - left. apply HQ.
Defined.


Inductive eq' {A} : A -> A -> Prop :=
| refl : forall {a}, eq' a a.

Definition leibniz {A} (a a' : A) := forall (P : A -> Prop), P a -> P a'.

Lemma eq_leibniz : forall {A} (a a' : A),
  eq' a a' -> leibniz a a'.
Proof.
  unfold leibniz.
  intros A a a' eq P Pa.
  destruct eq.
  apply Pa.
Qed.

Lemma leibniz_eq : forall {A} (a a' : A),
  leibniz a a' -> eq' a a'.
Proof.
  unfold leibniz.
  intros A a a' eq.
  specialize (eq (eq' a) refl).
  assumption.
Qed.