From 3e3eabe58aacb1cdf0c5814bd34c0db497c65ae3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Tue, 26 Sep 2017 16:50:45 +0200
Subject: [PATCH] Added Even.v.

---
 README.md  |  7 ++--
 coq/Even.v | 98 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 102 insertions(+), 3 deletions(-)
 create mode 100644 coq/Even.v

diff --git a/README.md b/README.md
index afd64aa..271a809 100644
--- a/README.md
+++ b/README.md
@@ -69,11 +69,12 @@ We also show the limits of dependently-typed functional programming.
   Syntax and operational semantics, on paper and on a machine
   ([slides 01a](slides/fpottier-01a.pdf))
   ([slides 01b](slides/fpottier-01b.pdf))
-  ([Coq demo](coq/DemoSyntaxReduction.v))
-  ([OCaml solution to Newton-Raphson exercise](ocaml/NewtonRaphson.ml)).
+  ([OCaml solution to Newton-Raphson exercise](ocaml/NewtonRaphson.ml))
+  ([Even.v](coq/Even.v)).
 * (29/09/2017)
   From a small-step semantics down to an efficient interpreter,
-  in several stages.
+  in several stages
+  ([Coq demo](coq/DemoSyntaxReduction.v)).
 * (06/10/2017) Compiling away first-class functions: closure conversion, defunctionalization.
 * (13/10/2017) Compiling away the call stack: the CPS transformation.
 * (20/10/2017) Equational reasoning and program optimizations.
diff --git a/coq/Even.v b/coq/Even.v
new file mode 100644
index 0000000..c68de79
--- /dev/null
+++ b/coq/Even.v
@@ -0,0 +1,98 @@
+(* 22/09/2017. Someone asked during the course whether [~ (even 1)] can be
+   proved, and if so, how. Here are several solutions, courtesy of
+   Pierre-Evariste Dagand. *)
+
+Inductive even: nat -> Prop :=
+| even_O:
+    even 0
+| even_SS:
+    forall n, even n -> even (S (S n)).
+
+(* 1. The shortest proof uses the tactic [inversion] to deconstruct the
+   hypothesis [even 1], that is, to perform case analysis. The tactic
+   automatically finds that this case is impossible, so the proof is
+   finished. *)
+
+Lemma even1_v1:
+  even 1 -> False.
+Proof.
+  inversion 1.
+  (* In case you wish the see the proof term: *)
+  (* Show Proof. *)
+Qed.
+
+(* For most practical purposes, the above proof *script* is good enough, and
+   is most concise. However, those who wish to understand what they are doing
+   may prefer to write a proof *term* by hand, in the Calculus of Inductive
+   Constructions, instead of letting [inversion] construct a (possibly
+   needlessly complicated) proof term. *)
+
+(* 2. Generalizing with equality. *)
+
+Lemma even1_v2':
+  forall n, even n -> n = 1 -> False.
+Proof.
+  exact (fun n t =>
+    match t with
+    | even_O =>
+      fun (q: 0 = 1) =>
+        match q with (* IMPOSSIBLE *) end
+    | even_SS n _ =>
+      fun (q : S (S n) = 1) =>
+        match q with (* IMPOSSIBLE *) end
+    end
+  ).
+Qed.
+
+Lemma even1_v2:
+  even 1 -> False.
+Proof.
+  eauto using even1_v2'.
+Qed.
+
+(* 3. Type-theoretically, through a large elimination. *)
+
+Lemma even1_v3':
+  forall n,
+  even n ->
+  match n with
+  | 0 => True
+  | 1 => False
+  | S (S _) => True
+  end.
+Proof.
+  exact (fun n t =>
+    match t with
+    | even_O => I
+    | even_SS _ _ => I
+    end
+  ).
+Qed.
+
+Lemma even1_v3:
+  even 1 -> False.
+Proof.
+  apply even1_v3'.
+Qed.
+
+(* 3'. Same technique, using a clever [match ... in ... return]. *)
+
+Lemma even1_v4':
+  even 1 -> False.
+Proof.
+  exact (fun t =>
+    match t in even n
+      return (
+        match n with
+        | 0 => True
+        | 1 => False
+        | S (S _) => True
+        end
+        (* BUG: we need the following (pointless) type annotation *)
+      : Prop)
+    with
+    | even_O => I
+    | even_SS _ _ => I
+    end
+  ).
+Qed.