New declarative commands (ast, pretty-printing and parsing only):

  [obtain term] = term by term
  by term we have term (id) and term (id)
  we proceed by induction on term to prove term
  the thesis becomes term
  by induciton hypothesis we know term
  case id [(id:term)]*

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 246df11c293144f981dec9ff84c51762c68a1f0d..65e35634f2b48172f21f1dfa5a526422ab7b04e9 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -87,11 +87,18 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Transitivity of loc * 'term
   (* Costruttori Aggiunti *)
   | Assume of loc * 'ident * 'term
-  | Suppose of loc * 'term *'ident
-  | By_term_we_proved of loc * 'term * 'term * 'ident
-  | We_need_to_prove of loc * 'term * 'ident
-  | Bydone of loc * 'term
-
+  | Suppose of loc * 'term *'ident * 'term option
+  | By_term_we_proved of loc *'term option * 'term * 'ident * 'term option
+  | We_need_to_prove of loc * 'term * 'ident * 'term option
+  | Bydone of loc * 'term option 
+  | We_proceed_by_induction_on of loc * 'term * 'term
+  | Byinduction of loc * 'term * 'ident
+  | Thesisbecomes of loc * 'term
+  | Case of loc * string * (string * 'term) list 
+  | Let1 of loc * 'ident * 'term * 'term
+  | Bywehave of loc * 'term option * 'term * 'ident * 'term * 'ident
+  | RewritingStep of loc * 'term option * 'term  * 'term option
+  
 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 
 type print_kind = [ `Env | `Coer ]
@@ -109,7 +116,7 @@ type 'term macro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 6
+let magic = 7
 
 type 'obj command =
   | Default of loc * string * UriManager.uri list

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 4a94152de956c5ea144f3af78e3ebd6d8392c37a..8f037f0320bac38bffa4502f8070a72253930552 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -154,8 +154,26 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
-  
-  let pp_search_kind = function
+  (* Tattiche Aggiunte *)
+  | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term 
+  | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "("  ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+  | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
+  | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ "(" ^ident^ ")" ^
+       (match term2 with  None -> " " | Some term2 -> term_pp term2)
+  | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+  | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
+  | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
+  | Thesisbecomes (_, term) -> "the thesis becomes" ^ term_pp term
+  | Let1 (_, ident, term, term1) -> "let" ^ ident ^ ":" ^ term_pp term ^ "such that" ^ term_pp term1
+  | Bywehave (_, term, term1, ident, term2, ident1) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we have" ^ term_pp term1 ^ "(" ^ ident ^ ")" ^ "and" ^       term_pp term2 ^ "(" ^ ident1 ^ ")" 
+  | RewritingStep (_, term, term1, term2 ) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2    )
+  | Case (_, id, args) ->
+     "case" ^ id ^
+       String.concat " "
+        (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^  ")")
+         args)
+
+ let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 6dff5468dc631abf05b87431898fe464e4c844dd..c96de18961f252a9f3689ff93937b14b77418f18 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -156,13 +156,21 @@ let tactic_of_ast ast =
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
   (* Implementazioni Aggiunte *)
   | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
-  | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id
-  | GrafiteAst.By_term_we_proved (_, t, ty, id) ->
-     Declarative.by_term_we_proved t ty id
-  | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id
-  | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
+  | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
+  | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
+     Declarative.by_term_we_proved t ty id t1
+  | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
+     Declarative.we_need_to_prove t id t2
+  | GrafiteAst.Bydone (_, t) -> Declarative.bydone t 
+  | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
+     Declarative.we_proceed_by_induction_on t t1
+  | GrafiteAst.Byinduction (_, t, id) -> Declarative.assume id t
+  | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
+  | GrafiteAst.Let1 (_, id, t, t1) -> Declarative.let1 id t t1
+  | GrafiteAst.Case (_,id,params) -> Declarative.case id params
+  | GrafiteAst.Bywehave(_,t,t1,id,t2,id1) -> Declarative.bywehave t t1 id t2 id1
+  | GrafiteAst.RewritingStep (_,termine,t1,t2) -> Declarative.prova termine t1 t2
 
-(* maybe we only need special cases for apply and goal *)
 let classify_tactic tactic = 
   match tactic with
   (* tactics that can't close the goal (return a goal we want to "select") *)

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 04521361ddbb27215c87964a11cb697b37ca5171..2e7f1224f795a99b46729613cb5ca816a78161cc 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2005, HELM Team.
+(*
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -255,19 +255,96 @@ let disambiguate_tactic
     | GrafiteAst.Assume (loc, id, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Assume (loc, id, cic)
-    | GrafiteAst.Suppose (loc, term, id) ->
-        let metasenv,cic = disambiguate_term context metasenv term in 
-       metasenv,GrafiteAst.Suppose (loc, cic, id)
+    | GrafiteAst.Suppose (loc, term, id, term') ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+       let metasenv,cic' =
+          match term' with
+             None -> metasenv,None
+           | Some t ->
+                 let metasenv,t = disambiguate_term context metasenv t in
+                 metasenv,Some t in
+       metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
     | GrafiteAst.Bydone (loc,term) ->
+        let metasenv,cic = 
+          match term with
+             None -> metasenv,None
+            |Some t ->
+                 let metasenv,t = disambiguate_term context metasenv t in
+                metasenv,Some t in
+                metasenv,GrafiteAst.Bydone (loc, cic)
+    | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
         let metasenv,cic = disambiguate_term context metasenv term in
-       metasenv,GrafiteAst.Bydone (loc, cic)
-    | GrafiteAst.We_need_to_prove (loc,term,id) ->
+       let metasenv,cic' = 
+           match term' with
+             None -> metasenv,None
+           | Some t ->
+                 let metasenv,t = disambiguate_term context metasenv t in
+                 metasenv,Some t in
+       metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
+    | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') ->
+        let metasenv,cic =
+          match term with 
+            None -> metasenv,None
+          | Some t ->
+                let metasenv,t = disambiguate_term context metasenv t in
+                metasenv,Some t in
+        let metasenv,cic' = disambiguate_term context metasenv term' in
+       let metasenv,cic'' = 
+           match term'' with
+             None -> metasenv,None
+          |  Some t ->  
+                   let metasenv,t = disambiguate_term context metasenv t in
+                    metasenv,Some t in
+       metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'')
+    | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
         let metasenv,cic = disambiguate_term context metasenv term in
-       metasenv,GrafiteAst.We_need_to_prove (loc,cic,id)
-    | GrafiteAst.By_term_we_proved (loc,term,term',id) ->
+       let metasenv,cic' = disambiguate_term context metasenv term' in
+       metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
+   | GrafiteAst.Byinduction (loc, term, id) ->
         let metasenv,cic = disambiguate_term context metasenv term in
-        let metasenv,cic' = disambiguate_term context metasenv term' in
-       metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id)
+       metasenv,GrafiteAst.Byinduction(loc, cic, id)
+   | GrafiteAst.Thesisbecomes (loc, term) ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.Thesisbecomes (loc, cic)
+   | GrafiteAst.Let1 (loc, id, term, term1) ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+       let metasenv,cic'= disambiguate_term context metasenv term1 in
+       metasenv,GrafiteAst.Let1(loc, id, cic, cic')
+   | GrafiteAst.Bywehave (loc, term, term1, id, term2, id1) ->
+        let metasenv,cic = 
+           match term with 
+            None -> metasenv,None
+          | Some t ->
+                let metasenv,t = disambiguate_term context metasenv t in
+                  metasenv,Some t in
+       let metasenv,cic'= disambiguate_term context metasenv term1 in
+       let metasenv,cic''= disambiguate_term context metasenv term2 in
+       metasenv,GrafiteAst.Bywehave(loc, cic, cic', id, cic'', id1)   
+   | GrafiteAst.Case (loc, id, params) ->
+        let metasenv,params' =
+        List.fold_right
+         (fun (id,term) (metasenv,params) ->
+            let metasenv,cic = disambiguate_term context metasenv term in
+            metasenv,(id,cic)::params
+         ) params (metasenv,[])
+       in
+       metasenv,GrafiteAst.Case(loc, id, params')   
+   | GrafiteAst.RewritingStep (loc, term1, term2, term3) ->
+        let metasenv,cic =
+        match term1 with
+           None -> metasenv,None
+         | Some t -> 
+            let metasenv,t = disambiguate_term context metasenv t in
+             metasenv,Some t in
+       let metasenv,cic'= disambiguate_term context metasenv term2 in
+        let metasenv,cic'' =
+        match term3 with
+           None -> metasenv,None
+         | Some t -> 
+            let metasenv,t = disambiguate_term context metasenv t in
+             metasenv,Some t in
+       metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'')   
+
 
 let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
   let uri =

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 13ee7297eacec364ab468ce5b29209b36371c7e3..5d6dac77108bbc9da550cf495a5193c08c613800 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -234,16 +234,40 @@ EXTEND
      (* Produzioni Aggiunte *)
     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
         GrafiteAst.Assume (loc, id, t)
-    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
-        GrafiteAst.Suppose (loc, t, id)
-    | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
-        GrafiteAst.By_term_we_proved (loc, t, ty, id)
-    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
-        GrafiteAst.We_need_to_prove (loc, t, id)
-    | IDENT "by" ; t = tactic_term ; IDENT "done" ->
-        GrafiteAst.Bydone (loc, t)
+    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']->
+        GrafiteAst.Suppose (loc, t, id, t1)
+    | IDENT "by" ; t = [t' = tactic_term -> Some t' | SYMBOL "_" -> None];
+      cont=by_continuation ->
+       (match cont with
+           None -> GrafiteAst.Bydone (loc, t) 
+        | Some (ty,id,t1) ->
+           GrafiteAst.By_term_we_proved(loc, t, ty, id, t1))
+    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+        GrafiteAst.We_need_to_prove (loc, t, id, t1)
+    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+        GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
+    | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.Byinduction(loc, t, id)
+    | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
+        GrafiteAst.Thesisbecomes(loc, t)
+    | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
+        SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
+        GrafiteAst.Case(loc,id,params)
+    | IDENT "let" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ; IDENT "such" ; IDENT "that" ; t1=tactic_term ->
+        GrafiteAst.Let1 (loc, id, t, t1)
+    | IDENT "by" ; t=[t'=tactic_term->Some t'|SYMBOL "_"-> None] ; IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id=IDENT ; RPAREN ; IDENT "and" ; t2=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ->
+       GrafiteAst.Bywehave (loc, t, t1, id, t2, id1)
+    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ->
+     GrafiteAst.RewritingStep(loc, Some termine, t1, t2)
+    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ->
+     GrafiteAst.RewritingStep(loc, None, t1, t2)
+  ]
+];
+  by_continuation: [
+    [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> Some (ty,id,t1)
+    | IDENT "done" -> None
     ]
-  ];
+];
   atomic_tactical:
     [ "sequence" LEFTA
       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index a1c8cab690d2bc8c8e5915e44d371653d969a1ec..1604d92d8029af62abb68fb4f79b0121bd97311a 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -24,16 +24,16 @@
  *)
 
 let assume id t =
- Tacticals.then_
-  ~start:
-    (Tactics.intros ~howmany:1
-      ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
-  ~continuation:
-    (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
-     (fun _ metasenv ugraph -> t,metasenv,ugraph))
+  Tacticals.then_
+     ~start:
+       (Tactics.intros ~howmany:1
+        ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
+     ~continuation:
+       (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+         (fun _ metasenv ugraph -> t,metasenv,ugraph))
 ;;
 
-let suppose t id =
+let suppose t id ty =
  Tacticals.then_
    ~start:
        (Tactics.intros ~howmany:1
@@ -43,20 +43,26 @@ let suppose t id =
              (fun _ metasenv ugraph -> t,metasenv,ugraph))
 ;;
 
-let by_term_we_proved t ty id =
- Tacticals.thens
- ~start:
-   (Tactics.cut ty
-     ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
- ~continuations:
-   [ Tacticals.id_tac ; Tactics.apply t ]
+let by_term_we_proved t ty id ty' =
+ match t with
+    None -> assert false
+  | Some t ->
+     Tacticals.thens
+     ~start:
+       (Tactics.cut ty
+         ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+     ~continuations:
+       [ Tacticals.id_tac ; Tactics.apply t ]
 ;;
 
 let bydone t =
-   (Tactics.apply ~term:t)
+   match t with
+    None -> assert false
+  | Some t ->
+    (Tactics.apply ~term:t)
 ;;
 
-let we_need_to_prove t id =
+let we_need_to_prove t id ty =
  let aux status =
   let proof,goals =
    ProofEngineTypes.apply_tactic
@@ -73,3 +79,17 @@ let we_need_to_prove t id =
  in
   ProofEngineTypes.mk_tactic aux
 ;;
+
+let prova _ = assert false
+;;
+let bywehave _ = assert false
+;;
+let case _ = assert false
+;;
+let thesisbecomes _ = assert false
+;;
+let byinduction _ = assert false
+;;
+let we_proceed_by_induction_on _ = assert false
+;;
+let let1 _ = assert false

diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli
index 2e9d506ca8fb5cc83d5b8a463566d2c177a0f725..ba2eaaea444e4b90d34e799427b532c90fe2ae19 100644 (file)
--- a/components/tactics/declarative.mli
+++ b/components/tactics/declarative.mli
@@ -24,7 +24,29 @@
  *)
 
 val assume : string -> Cic.term -> ProofEngineTypes.tactic
-val suppose : Cic.term -> string -> ProofEngineTypes.tactic
-val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic
-val bydone : Cic.term -> ProofEngineTypes.tactic
-val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic
+
+val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
+
+val by_term_we_proved : Cic.term option -> Cic.term -> string -> Cic.term option ->ProofEngineTypes.tactic
+
+val bydone : Cic.term option -> ProofEngineTypes.tactic
+
+val we_need_to_prove :
+ Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
+
+val we_proceed_by_induction_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic
+
+val byinduction : Cic.term -> string -> ProofEngineTypes.tactic
+
+val thesisbecomes : Cic.term -> ProofEngineTypes.tactic
+
+val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic
+
+val let1 : string -> Cic.term -> Cic.term -> ProofEngineTypes.tactic
+
+val bywehave :
+ Cic.term option -> Cic.term -> string -> Cic.term -> string ->
+  ProofEngineTypes.tactic
+
+val prova :
+ Cic.term option -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic

diff --git a/matita/matita.lang b/matita/matita.lang
index 4b88fa91dc6b2f5707b918abbf77acc75f95f5e3..0dbfa4c78187f4653b90736f7b13badd47c82de5 100644 (file)
--- a/matita/matita.lang
+++ b/matita/matita.lang
@@ -127,7 +127,33 @@
     <keyword>transitivity</keyword>
     <keyword>unfold</keyword>
     <keyword>whd</keyword>
-  </keyword-list>
+    (* Tattiche Aggiunte *)
+    <keyword>assume</keyword>
+    <keyword>suppose</keyword>
+    <keyword>by</keyword>
+    <keyword>we</keyword> 
+    <keyword>prove</keyword>
+    <keyword>proved</keyword>
+    <keyword>need</keyword>
+    <keyword>proceed</keyword>
+    <keyword>induction</keyword>
+    <keyword>inductive</keyword>
+    <keyword>case</keyword>
+    <keyword>base</keyword>
+    <keyword>let</keyword>
+    <keyword>such</keyword>
+    <keyword>that</keyword>
+    <keyword>by</keyword>
+    <keyword>have</keyword>
+    <keyword>and</keyword>
+    <keyword>the</keyword>
+    <keyword>thesis</keyword>
+    <keyword>becomes</keyword>
+    <keyword>hypothesis</keyword>
+    <keyword>know</keyword>
+    <keyword>case</keyword>             
+    <keyword>obtain</keyword>           
+</keyword-list>
 
   <keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
     <keyword>try</keyword>