From d669da59d27e2418e65a275dc5d405237db2b93a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Dec 2006 23:25:42 +0000 Subject: [PATCH] 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. --- helm/software/components/grafite/grafiteAst.ml | 1 + helm/software/components/grafite/grafiteAstPp.ml | 1 + helm/software/components/grafite_engine/grafiteEngine.ml | 2 ++ .../components/grafite_parser/grafiteDisambiguate.ml | 4 ++++ helm/software/components/grafite_parser/grafiteParser.ml | 2 ++ helm/software/components/tactics/declarative.ml | 5 +++++ helm/software/components/tactics/declarative.mli | 2 ++ helm/software/components/tactics/tactics.mli | 2 +- 8 files changed, 18 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 7a9b7b5ae..d6dfa53a6 100644 --- 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 0530697ad..d775a77dc 100644 --- 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 082eee5f9..a125d23be 100644 --- 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 42fbabacd..2d06942e3 100644 --- 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 b2fb3616f..054bff621 100644 --- 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 77276d929..26276f97c 100644 --- 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 fae5c7dcf..4693085d2 100644 --- 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 c0702638f..b0ec098e0 100644 --- 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 : -- 2.39.2