From e32693f30563379989b75b53c3be088396b732da Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 23 Jun 2005 12:23:04 +0000
Subject: [PATCH] 1. Tactic generalize ported to patterns and activated in
 matita. 2. slightly improved syntax for patterns 3. new test for "hand
 implemented" inversion (that uses induction instead of    case analysis)

---
 helm/matita/matita.lang        |  1 +
 helm/matita/matitaEngine.ml    | 14 ++++++++------
 helm/matita/tests/inversion.ma | 22 ++++++++++++++++++++++
 helm/matita/tests/rewrite.ma   |  2 +-
 4 files changed, 32 insertions(+), 7 deletions(-)
 create mode 100644 helm/matita/tests/inversion.ma

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index baccdf714..d2015ee3e 100644
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -77,6 +77,7 @@
     <keyword>exists</keyword>
     <keyword>fold</keyword>
     <keyword>fourier</keyword>
+    <keyword>generalize</keyword>
     <keyword>goal</keyword>
     <keyword>injection</keyword>
     <keyword>intro</keyword>
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a9c85e7d8..7302e3bde 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -30,8 +30,12 @@ let tactic_of_ast = function
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
+(*
+  | TacticAst.Discriminate (_,id) -> Tactics.discriminate id
+*)
   | TacticAst.Exists _ -> Tactics.exists
   | TacticAst.Fourier _ -> Tactics.fourier
+  | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat
   | TacticAst.Goal (_, n) -> Tactics.set_goal n
   | TacticAst.Left _ -> Tactics.left
   | TacticAst.Right _ -> Tactics.right
@@ -58,7 +62,6 @@ let tactic_of_ast = function
   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
   | TacticAst.Change of 'term * 'term * 'ident option
   | TacticAst.Decompose of 'ident * 'ident list
-  | TacticAst.Discriminate of 'ident
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
   | TacticAst.Replace_pattern of 'term pattern * 'term
@@ -81,7 +84,6 @@ let tactic_of_ast = function
   | TacticAst.LApply (_, term, substs) ->
      let f (name, term) = Cic.Name name, term in
      Tactics.lapply ~substs:(List.map f substs) term
-  | _ -> assert false
 
 let eval_tactical status tac =
   let apply_tactic tactic =
@@ -408,6 +410,10 @@ let disambiguate_tactic status = function
       let status, cic1 = disambiguate_term status what in
       let status, cic2 = disambiguate_term status with_what in
       status, TacticAst.Change (loc, cic1, cic2, ident)
+  | TacticAst.Generalize (loc,term,pattern) ->
+      let status,term = disambiguate_term status term in
+      let pattern = disambiguate_pattern status.aliases pattern in
+      status, TacticAst.Generalize(loc,term,pattern)
 (*
   (* TODO Zack a lot more of tactics to be implemented here ... *)
   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
@@ -451,10 +457,6 @@ let disambiguate_tactic status = function
      let status, term = disambiguate_term status term in
      let status, substs = List.fold_left f (status, []) substs in 
      status, TacticAst.LApply (loc, term, substs)
-  
-  | x -> 
-      print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
-      assert false
 
 let rec disambiguate_tactical status = function 
   | TacticAst.Tactic (loc, tactic) -> 
diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
new file mode 100644
index 000000000..ccbc4d96b
--- /dev/null
+++ b/helm/matita/tests/inversion.ma
@@ -0,0 +1,22 @@
+inductive nat : Set \def
+   O : nat
+ | S : nat \to nat.
+ 
+inductive le (n:nat) : nat \to Prop \def
+   leO : le n n
+ | leS : \forall m. le n m \to le n (S m).
+
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+
+theorem test_inversion: \forall n. le n O \to n=O.
+ intros.
+ cut O=O.
+  (* goal 2: 0 = 0 *)
+  goal 7. reflexivity.
+  (* goal 1 *)
+  generalize Hcut.      (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
+  apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
+  intro. reflexivity.
+  simplify. intros.
+  (* manca discriminate H3 *)
+qed.
\ No newline at end of file
diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma
index 56ea93bf8..e597e66ef 100644
--- a/helm/matita/tests/rewrite.ma
+++ b/helm/matita/tests/rewrite.ma
@@ -6,6 +6,6 @@ theorem a:
   \forall a,b:nat.
   a = b \to b + a = a + a.
 intros.
-rewrite right H in (? ? % ?).
+rewrite right H in \vdash (? ? % ?).
 reflexivity.
 qed.
\ No newline at end of file
-- 
2.39.2