Partially restore the suppose tactic

Add a type for the suppose tactic in GrafiteAst

Add pretty printing code for the suppose tactic

Add a parsing rule for the suppose tactic in GrafiteParser

Add a call in to the suppose tactic in GrafiteEngine

Add code for the suppose tactic in Declarative

Add syntax highlight tag for the suppose tactic

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 8b911a60183c1ff0a7022160056e5696e8ee9dee..29dfe324b4426e25ade914f6aa5aac0be7f65677 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -76,7 +76,9 @@ type ntactic =
    | NRepeat of loc * ntactic
    | NBlock of loc * ntactic list
    (* Declarative langauge *)
+   (* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
    | Assume of loc * string * nterm (* loc, identifier, term *)
+   | Suppose of loc * nterm *string * nterm option
 
 type nmacro =
   | NCheck of loc * nterm

diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index d56e95de0cacafdcc8b4e785edc6b208c126516d..00789961ce5dd98ebe480ee453f88b2256583b68 100644 (file)
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -108,6 +108,8 @@ let rec pp_ntactic status ~map_unicode_to_tex =
      "(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
   | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
   | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term
+  | Suppose (_,term,ident,term1) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" ^ (match
+  term1 with None -> "" | Some t -> " that is equivalent to " ^ NotationPp.pp_term status t)
 ;;
 
 let pp_nmacro status = function

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index f76b8b02a802e80a406e1d9b8321c47b5e2b9087..be7154179812b0df00929c80a47541928f7c7819 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -482,6 +482,7 @@ let eval_ng_tac tac =
   |GrafiteAst.NRepeat (_,tac) ->
       NTactics.repeat_tac (f f (text, prefix_len, tac))
   |GrafiteAst.Assume (_,id,t) -> Declarative.assume id t
+  |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose t id t1
  in
   aux aux tac (* trick for non uniform recursion call *)
 ;;

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index c1b347071b799ce5ed9630f32ffc15672cd72b15..90abc0a89e435f26283041daf4737db03b9150f3 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -239,7 +239,9 @@ EXTEND
     | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
     | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
     | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
-    | IDENT "assume"; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+    | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that"; IDENT
+    "is"; IDENT "equivalent"; "to"; t' = tactic_term -> t'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)])
     ]
   ];
   auto_fixed_param: [

diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index 532ffbb3767b983780b5e42140677e72a2294c9d..ae07c18ee7361ffad9188ba0171a89fe61804146 100644 (file)
--- a/matita/components/ng_tactics/declarative.ml
+++ b/matita/components/ng_tactics/declarative.ml
@@ -28,3 +28,7 @@ open NTactics
 
 let assume name ty =
     exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit `JustOne)))
+
+let suppose t id t1 =
+    let t1 = match t1 with None -> t | Some t1 -> t1 in
+    exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit `JustOne)))

diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli
index f6f0ff953f8753d2c24f28c64c93550beedb7588..a7ec0e44d12260c8ba840e831e6e6991ef120c25 100644 (file)
--- a/matita/components/ng_tactics/declarative.mli
+++ b/matita/components/ng_tactics/declarative.mli
@@ -24,3 +24,4 @@
  *)
 
 val assume : string -> NotationPt.term -> 's NTacStatus.tactic
+val suppose : NotationPt.term -> string -> NotationPt.term option -> 's NTacStatus.tactic

diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index 8a47418b68009a5b5e09a11d7d7a9c4b8f66cc7e..6fa587de3b2c327167c432a92aec8566a7408229 100644 (file)
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -107,6 +107,11 @@
          <keyword>lapply</keyword>
          <keyword>destruct</keyword>
          <keyword>assume</keyword>
+         <keyword>suppose</keyword>
+         <keyword>that</keyword>
+         <keyword>is</keyword>
+         <keyword>equivalent</keyword>
+         <keyword>to</keyword>
 
           <!-- commands -->
           <keyword>alias</keyword>