checkpoint

3 files changed, 49 insertions, 5 deletions

diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 86731c48ac..4ca59ddd36 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -146,4 +146,26 @@ let example_classes n =
     EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), DEFAULTcast,
       EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
   let evd, final_type = Typing.type_of env evd proved_equality in
+  Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
+
+let example_canonical n =
+  let c_n = mk_nat n in
+  let n_half = mk_nat (n / 2) in
+  let c_N = c_N () in
+  let c_div = c_D () in
+  let c_even = c_E () in
+  let c_Q = c_Q () in
+  let c_R = c_R () in
+  let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, instance = Evarutil.new_evar env evd arg_type in
+  let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
+  let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+  let evd, the_type = Typing.type_of env evd c_half in
+  let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+  let proved_equality =
+    EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), DEFAULTcast,
+      EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
+  let evd, final_type = Typing.type_of env evd proved_equality in
   Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
\ No newline at end of file
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index 15e36bc6ec..c6ed5c66da 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -1,9 +1,31 @@
-Class EvenNat n := {half : nat; half_prop : 2 * half = n}.
+Require Import ArithRing.
 
-Instance EvenNat2 : EvenNat 2 := {half := 1; half_prop := eq_refl}.
+Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
 
-Instance EvenNat4 : EvenNat 4 := {half := 2; half_prop := eq_refl}.
+Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
 
-Definition tuto_div2 n (p : EvenNat n) := @half n p.
+Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n).
+Proof. intros H; ring [H]. Qed.
 
+Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
+ {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}.
+
+
+Definition tuto_div2 n (p : EvenNat n) := @half _ p.
+
+Record S_ev n := Build_S_ev {double_of : nat; s_h_prop : 2 * n = double_of}.
+
+Canonical Structure can_ev0 : S_ev 0 :=
+  Build_S_ev 0 0 (@eq_refl _ 0).
+
+Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n).
+Proof.
+intros s; exists (S (S (double_of _ s))).
+destruct s as [a P]. simpl. ring [P].
+Defined.
+
+Canonical Structure can_ev_rec.
+
+Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n :=
+  Build_S_ev n d Pd.
 
diff --git a/tuto3/theories/Loader.v b/tuto3/theories/Loader.v
index eb3182cdaa..952565dbea 100644
--- a/tuto3/theories/Loader.v
+++ b/tuto3/theories/Loader.v
@@ -1,3 +1,3 @@
-From Tuto3 Require Import Data.
+From Tuto3 Require Export Data.
 
 Declare ML Module "tuto3_plugin".
\ No newline at end of file