New declarative tactic "we proceed by cases on t to prove t'".

Very unsatisfactory since it already introduces the hypothesis in advance,
actually ignoring the following "case S (n:nat)" declarative command.
I do not see any easy solution at all.

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 7a9b7b5ae05f7099244d3a7c70fa189fc5b85040..d6dfa53a65dc88e1a4b744e9ef0147539ee01f05 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -93,6 +93,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | We_need_to_prove of loc * 'term * 'ident option * 'term option
   | Bydone of loc * 'term option 
   | We_proceed_by_induction_on of loc * 'term * 'term
+  | We_proceed_by_cases_on of loc * 'term * 'term
   | Byinduction of loc * 'term * 'ident
   | Thesisbecomes of loc * 'term
   | Case of loc * string * (string * 'term) list 

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 0530697ada6b252b580405a4837ef7eca0e5eb68..d775a77dcdce83bcab4c8a018474bc7870a5bf17 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -166,6 +166,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
        (match term2 with  None -> " " | Some term2 -> term_pp term2)
   | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+  | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ 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

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 082eee5f95279cbb5265197849220bd3082e3311..a125d23be41c79f212c8e5b0999753ec6d101888 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -172,6 +172,8 @@ let tactic_of_ast status ast =
   | GrafiteAst.Bydone (_, t) ->
      Declarative.bydone ~dbd:(LibraryDb.instance())
       ~universe:status.GrafiteTypes.universe t
+  | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
+     Declarative.we_proceed_by_cases_on t t1
   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
      Declarative.we_proceed_by_induction_on t t1
   | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 42fbabacd600fa3acd796367d482da2f9f4750df..2d06942e309d0bc60901469ce4a9b5355ec5831c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -298,6 +298,10 @@ let disambiguate_tactic
                    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_cases_on (loc, term, term') ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+       let metasenv,cic' = disambiguate_term context metasenv term' in
+       metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
     | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
         let metasenv,cic = disambiguate_term context metasenv term in
        let metasenv,cic' = disambiguate_term context metasenv term' in

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index b2fb3616f6cc216866dd7a446b614e27ca7dd39c..054bff6215e1f64ec1b6d90813a3f7a316b88089 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -269,6 +269,8 @@ EXTEND
               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
     | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; 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 "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+        GrafiteAst.We_proceed_by_cases_on (loc, t, 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 ->

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 77276d92909866cfcba3c458c10f99eccc32f472..26276f97c072a75dba7c3fb967697cb4e347e4a9 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -225,6 +225,11 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
   ProofEngineTypes.mk_tactic aux
 ;;
 
+let we_proceed_by_cases_on t pat =
+ (*BUG here: pat unused *)
+ Tactics.cases_intros t
+;;
+
 let we_proceed_by_induction_on t pat =
  (*BUG here: pat unused *)
  Tactics.elim_intros ~depth:0 t

diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli
index fae5c7dcf3263c67ea821e05a7cb8367fde6cceb..4693085d2746d3dabcb859d5732e7b6178505dd7 100644 (file)
--- a/helm/software/components/tactics/declarative.mli
+++ b/helm/software/components/tactics/declarative.mli
@@ -37,6 +37,8 @@ val bydone : dbd:HMysql.dbd -> universe:Universe.universe -> Cic.term option ->
 val we_need_to_prove :
  Cic.term -> string option -> Cic.term option -> ProofEngineTypes.tactic
 
+val we_proceed_by_cases_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic
+
 val we_proceed_by_induction_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic
 
 val byinduction : Cic.term -> string -> ProofEngineTypes.tactic

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index c0702638f6d2780d9ca6f435a6fdf2693f5280fb..b0ec098e0b049cacb2696e9bc343820b8b40131e 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Dec 20 23:48:06 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Dec 21 00:41:09 CET 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :