This version contains documentation for the code of the packing tactic

warning have been removed
Examples for the use of type classes and canonical structures in
automatic proof have been moved to the end.

5 files changed, 168 insertions, 39 deletions

diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index a4095ae2e7..8b123eb7b0 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -1,7 +1,6 @@
 DECLARE PLUGIN "tuto3_plugin"
 
 open Ltac_plugin
-open Pp
 
 open Construction_game
 
@@ -24,15 +23,20 @@ VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
 | [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
 END
 
+TACTIC EXTEND collapse_hyps
+| [ "pack" "hypothesis" ident(i) ] ->
+  [ Tuto_tactic.pack_tactic i ]
+END
+
+(* More advanced examples, where automatic proof happens but
+   no tactic is being called explicitely.  The first one uses
+   type classes. *)
 VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
 | [ "Tuto3_3" int(n) ] -> [ example_classes n ]
 END
 
+(* The second one uses canonical structures. *)
 VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
 | [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
 END
 
-TACTIC EXTEND collapse_hyps
-| [ "hide" "hypothesis" ident(i) ] ->
-  [ Tuto_tactic.hide_tactic i ]
-END
\ No newline at end of file
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index a0ac967731..fbb6863f7e 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -2,15 +2,21 @@ open Proofview
 
 let constants = ref ([] : EConstr.t list)
 
+(* This is a pattern to collect terms from the Coq memory of valid terms
+  and proofs.  This pattern extends all the way to the definition of function
+ c_U *)
 let collect_constants () =
   if (!constants = []) then
     let open Coqlib in
     let open EConstr in
     let open Universes in
-    let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "hide" in
-    let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "hide_marker" in
+    let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in
+    let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in
+    let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
+    let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in
+    let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in
     constants := List.map (fun x -> of_constr (constr_of_global x))
-      [gr_H; gr_M];
+      [gr_H; gr_M; gr_R; gr_P; gr_U];
     !constants
   else
     !constants
@@ -18,35 +24,109 @@ let collect_constants () =
 let c_H () =
   match collect_constants () with
     it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of hide"
+  | _ -> failwith "could not obtain an internal representation of pack"
 
 let c_M () =
   match collect_constants () with
     _ :: it :: _ -> it
-  | _ -> failwith "could not obtain an internal representation of hide_marker"
+  | _ -> failwith "could not obtain an internal representation of pack_marker"
 
+let c_R () =
+  match collect_constants () with
+    _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of pair"
+
+let c_P () =
+  match collect_constants () with
+    _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of prod"
+
+let c_U () =
+  match collect_constants () with
+    _ :: _ :: _ :: _ :: it :: _ -> it
+  | _ -> failwith "could not obtain an internal representation of prod"
+
+(* The following tactic is meant to pack an hypothesis when no other
+   data is already packed.
+
+   The main difficulty in defining this tactic is to understand how to
+   construct the input expected by apply_in. *)
 let package i = Goal.enter begin fun gl ->
   Tactics.apply_in true false i
-   [None, (CAst.make (c_M (), Misctypes.NoBindings))] None
+   [(* this means that the applied theorem is not to be cleared. *)
+    None, (CAst.make (c_M (),
+           (* we don't specialize the theorem with extra values. *)
+           Misctypes.NoBindings))]
+     (* we don't destruct the result according to any intro_pattern *)
+    None
   end
-(*
-let package i = Goal.enter begin fun gl ->
-    let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+
+(* This function is meant to observe a type of shape (f a)
+   and return the value a.  *)
+
+(* Remark by Maxime: look for destApp combinator. *)
+let unpack_type evd term =
+  let report () =
+    CErrors.user_err (Pp.str "expecting a packed type") in
+  match EConstr.kind evd term with
+  | Constr.App (_, [| ty |]) -> ty
+  | _ -> report ()
+
+(* This function is meant to observe a type of shape
+   A -> pack B -> C and return A, B, C
+  but it is not used in the current version of our tactic.
+  It is kept as an example. *)
+let two_lambda_pattern evd term =
+  let report () =
+    CErrors.user_err (Pp.str "expecting two nested implications") in
+(* Note that pattern-matching is always done through the EConstr.kind function,
+   which only provides one-level deep patterns. *)
+  match EConstr.kind evd term with
+  (* Here we recognize the outer implication *)
+  | Constr.Prod (_, ty1, l1) ->
+      (* Here we recognize the inner implication *)
+      (match EConstr.kind evd l1 with
+      | Constr.Prod (n2, packed_ty2, deep_conclusion) ->
+        (* Here we recognized that the second type is an application *)
+        ty1, unpack_type evd packed_ty2, deep_conclusion
+      | _ -> report ())
+  | _ -> report ()
+
+(* In the environment of the goal, we can get the type of an assumption
+  directly by a lookup.  The other solution is to call a low-cost retyping
+  function like *)
+let get_type_of_hyp env id =
+  match EConstr.lookup_named id env with
+  | Context.Named.Declaration.LocalAssum (_, ty) -> ty
+  | _ -> CErrors.user_err (let open Pp in
+                             str (Names.Id.to_string id) ++
+                             str " is not a plain hypothesis")
+
+let repackage i h_hyps_id = Goal.enter begin fun gl ->
     let env = Goal.env gl in
     let store = Goal.extra gl in
-    let concl = Tacmach.New.pf_concl in
-    
-    let ty_i = ... in
-    let ev = Evarutil.new_evar in
-    mkApp (mkLambda(h_hyps_id, mkApp(c_h, [|ty_i|] , ev),
-           [| mkApp (c_hm, [| ty_ev; EConstr.mkVar i |]) |])
-end
- *)
-
-let repackage _ = failwith "todo"
-
-let hide_tactic i =
-  let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+    let evd = Tacmach.New.project gl in
+    let concl = Tacmach.New.pf_concl gl in
+    let (ty1 : EConstr.t) = get_type_of_hyp env i in
+    let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in
+    let ty2 = unpack_type evd packed_ty2 in
+    let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in
+    let open EConstr in
+    let new_packed_value =
+        mkApp (c_R (), [| ty1; ty2; mkVar i;
+          mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
+    Refine.refine ~typecheck:true begin fun evd ->
+      let evd, new_goal = Evarutil.new_evar env evd ~store
+          (mkProd (Names.Name.Anonymous,
+                     mkApp(c_H (), [| new_packed_type |]),
+                       Vars.lift 1 concl)) in
+        evd, mkApp (new_goal,
+                 [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
+      end
+    end
+
+let pack_tactic i =
+  let h_hyps_id = (Names.Id.of_string "packed_hyps") in
   Proofview.Goal.enter begin fun gl ->
     let hyps = Environ.named_context_val (Proofview.Goal.env gl) in
     if not (Termops.mem_named_context_val i hyps) then
@@ -54,9 +134,11 @@ let hide_tactic i =
           (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i))))
     else
       if Termops.mem_named_context_val h_hyps_id hyps then
-          tclTHEN (Tactics.revert [i; h_hyps_id]) (repackage ())
+          tclTHEN (repackage i h_hyps_id)
+            (tclTHEN (Tactics.clear [h_hyps_id; i])
+               (Tactics.introduction h_hyps_id))
       else
-        package i
+        tclTHEN (package i)
+          (tclTHEN (Tactics.rename_hyp [i, h_hyps_id])
+             (Tactics.move_hyp h_hyps_id Misctypes.MoveLast))
     end
-      
-      
diff --git a/tuto3/src/tuto_tactic.mli b/tuto3/src/tuto_tactic.mli
index 13f905ed8a..dbf6cf48e2 100644
--- a/tuto3/src/tuto_tactic.mli
+++ b/tuto3/src/tuto_tactic.mli
@@ -1 +1,3 @@
-val hide_tactic : Names.Id.t -> unit Proofview.tactic
+val two_lambda_pattern :
+    Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t
+val pack_tactic : Names.Id.t -> unit Proofview.tactic
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index 4de0a9a0f9..0b07fee4f2 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -1,5 +1,18 @@
 Require Import ArithRing.
 
+Inductive pack (A: Type) : Type :=
+  packer : A -> pack A.
+
+Arguments packer {A}.
+
+Definition uncover (A : Type) (packed : pack A) : A :=
+  match packed with packer v => v end.
+
+Notation "!!!" := (pack _) (at level 0, only printing).
+
+(* The following data is used as material for automatic proofs
+  based on type classes. *)
+
 Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
 
 Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
@@ -12,6 +25,18 @@ Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
 
 Definition tuto_div2 n (p : EvenNat n) := @half _ p.
 
+(* to be used in the following examples
+Compute (@half 8 _).
+
+Check (@half_prop 8 _).
+
+Check (@half_prop 7 _).
+
+and in command Tuto3_3 8. *)
+
+(* The following data is used as material for automatic proofs
+  based on canonical structures. *)
+
 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 :=
@@ -41,10 +66,3 @@ Check (C _ _ _ eq_refl : cmp 6 _).
 Check (C _ _ _ eq_refl : cmp 7 _).
 
 *)
-
-Inductive hide (A: Type) : Type :=
-  hide_marker : A -> hide A.
-
-Arguments hide_marker {A}.
-
-Notation "!!!" := (hide _) (at level 0, only printing).
\ No newline at end of file
diff --git a/tuto3/theories/test.v b/tuto3/theories/test.v
new file mode 100644
index 0000000000..43204ddf34
--- /dev/null
+++ b/tuto3/theories/test.v
@@ -0,0 +1,23 @@
+(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *)
+
+Require Import Tuto3.Loader.
+
+(* This should print Type. *)
+Tuto3_1.
+
+(* This should print a term that contains an existential variable. *)
+(* And then print the same term, where the variable has been correctly
+   instantiated. *)
+Tuto3_2.
+
+Lemma tutu x y (A : 0 < x) (B : 10 < y) : True.
+Proof.
+pack hypothesis A.
+(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis
+  should have appeared, with unreadable content. *)
+pack hypothesis B.
+(* Hypothesis B should have disappeared *)
+destruct packed_hyps as [unpacked_hyps].
+(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *)
+exact I.
+Qed.