This version contains an example of using canonical structures so

that type-checking actually triggers the automatic build of a proof.

5 files changed, 110 insertions, 8 deletions

diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 86731c48ac..9a3d046cf5 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -77,8 +77,11 @@ let collect_constants () =
     let gr_Q = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
     let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
     let gr_N = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
+    let gr_C = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
+    let gr_F = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
+    let gr_P = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
     constants := List.map (fun x -> of_constr (constr_of_global x))
-      [gr_S; gr_O; gr_E; gr_D; gr_Q; gr_R; gr_N];
+      [gr_S; gr_O; gr_E; gr_D; gr_Q; gr_R; gr_N; gr_C; gr_F; gr_P];
     !constants
   else
     !constants
@@ -118,6 +121,21 @@ let c_N () =
     _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
   | _ -> failwith "could not obtain an internal representation of nat"
 
+let c_C () =
+  match collect_constants () with
+    _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of cmp"
+
+let c_F () =
+  match collect_constants () with
+    _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of S_ev"
+
+let c_P () =
+  match collect_constants () with
+    _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of s_half_proof"
+
 let mk_nat n =
   let c_S = c_S () in
   let c_O = c_O () in
@@ -143,7 +161,50 @@ let example_classes n =
   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.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.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
+  Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
+
+(* This function, together with definitions in Data.v, shows how to
+  trigger automatic proofs at the time of typechecking.
+
+   n is a number for which we want to find the half (and a proof that
+   this half is indeed the half)
+*)
+let example_canonical n =
+(* Construct a natural representation of this integer. *)
+  let c_n = mk_nat n in
+(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
+  let c_N = c_N () in
+  let c_Q = c_Q () in
+  let c_F = c_F () in
+  let c_R = c_R () in
+  let c_C = c_C () in
+  let c_P = c_P () in
+(* the last argument of C *)
+  let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+(* Now we build two existential variables, for the value of the half and for
+   the "S_ev" structure that triggers the proof search. *)
+  let evd, ev1 = Evarutil.new_evar env evd c_N in
+(* This is the type for the second existential variable *)
+  let csev = EConstr.mkApp (c_F, [| ev1 |]) in
+  let evd, ev2 = Evarutil.new_evar env evd csev in
+(* Now we build the C structure. *)
+  let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in
+(* Type-checking this term will compute values for the existential variables *)
+  let evd, final_type = Typing.type_of env evd test_term in
+(* The computed type has two parameters, the second one is the proof. *)
+  let value = match EConstr.kind evd final_type with
+      | App(_, [| _; the_half |]) -> the_half
+      | _ -> failwith "expecting the whole type to be ""cmp _ the_half""" in
+  let _ = Feedback.msg_notice (Termops.print_constr_env env evd value) in
+(* I wish for a nicer way to get the value of ev2 in the evar_map *)
+  let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
+  let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in
+  let evd, the_statement = Typing.type_of env evd the_prf in
+  Feedback.msg_notice
+    (Termops.print_constr_env env evd the_prf ++ str " has type " ++
+     Termops.print_constr_env env evd the_statement)
\ No newline at end of file
diff --git a/tuto3/src/construction_game.mli b/tuto3/src/construction_game.mli
index a4172734fd..302aec1de9 100644
--- a/tuto3/src/construction_game.mli
+++ b/tuto3/src/construction_game.mli
@@ -1,2 +1,3 @@
 val example_sort_app_lambda : unit -> unit
 val example_classes : int -> unit
+val example_canonical : int -> unit
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index e0f60b34c8..963662895a 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -28,3 +28,7 @@ VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
 | [ "Tuto3_3" int(n) ] -> [ example_classes n ]
 END
 
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
+END
+
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index 15e36bc6ec..c288d5d452 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -1,9 +1,45 @@
-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; _ : 2 * n = double_of}.
+
+Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
+  match r with Build_S_ev _ _ h => h end.
+
+Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n :=
+  Build_S_ev n d Pd.
+
+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.
+
+Record cmp (n : nat) (k : nat) :=
+  C {h : S_ev k; _ : double_of k h = n}.
+
+(* To be used in, e.g.,
+
+Check (C _ _ _ eq_refl : cmp 6 _).
+
+Check (C _ _ _ eq_refl : cmp 7 _).
+
+*)
 
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