From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 23 Jun 2005 12:23:04 +0000 (+0000)
Subject: 1. Tactic generalize ported to patterns and activated in matita.
X-Git-Tag: INDEXING_NO_PROOFS~95
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e32693f30563379989b75b53c3be088396b732da;p=helm.git

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)
---

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