The code and behaviour should be cleaned up a little bit.
| Byinduction of loc * 'term * 'ident
| Thesisbecomes of loc * 'term
| Case of loc * string * (string * 'term) list
- | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
+ | ExistsElim of loc * 'term option * 'ident * 'term * 'ident * 'lazy_term
| AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
| RewritingStep of
loc * (string option * 'term) option * 'term *
| 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
- | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ term_pp term0 ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ term_pp term1 ^ "(" ^ ident1 ^ ")"
+ | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ (match term0 with None -> "_" | Some term -> term_pp term) ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")"
| AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")"
| RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2) ^ (if cont then " done" else "")
| Case (_, id, args) ->
| GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
| GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
| GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
- Declarative.existselim t id1 t1 id2 t2
+ Declarative.existselim ~dbd:(LibraryDb.instance())
+ ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2
| GrafiteAst.Case (_,id,params) -> Declarative.case id params
| GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
| GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Thesisbecomes (loc, cic)
| GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
- 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
let metasenv,cic' = disambiguate_term context metasenv term1 in
- let metasenv,cic''= disambiguate_term context metasenv term2 in
+ let cic''= disambiguate_lazy_term term2 in
metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
| GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
let metasenv,cic = disambiguate_term context metasenv term in
| BYC_weproved (ty,id,t1) ->
GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
| BYC_letsuchthat (id1,t1,id2,t2) ->
- (match t with
+ (* (match t with
LNone floc ->
raise (HExtlib.Localized
(floc,CicNotationParser.Parse_error
"tactic_term expected here"))
- | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+ | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
| BYC_wehaveand (id1,t1,id2,t2) ->
(match t with
LNone floc ->
ProofEngineTypes.mk_tactic aux
;;
-let existselim t id1 t1 id2 t2 =
-(*BUG: t1 and t2 not used *)
-(*PARSING BUG: t2 is parsed in the current context, but it may
- have occurrences of id1 in it *)
- Tactics.elim_intros t
- ~mk_fresh_name_callback:
- (let i = ref 0 in
- fun _ _ _ ~typ ->
- incr i;
- if !i = 1 then Cic.Name id1 else Cic.Name id2)
+let existselim ~dbd ~universe t id1 t1 id2 t2 =
+ let aux (proof, goal) =
+ let (n,metasenv,bo,ty,attrs) = proof in
+ let metano,context,_ = CicUtil.lookup_meta goal metasenv in
+ let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
+ let proof' = (n,metasenv,bo,ty,attrs) in
+ ProofEngineTypes.apply_tactic (
+ Tacticals.thens
+ ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
+ ~continuations:
+ [ Tactics.elim_intros (Cic.Rel 1)
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
+ (match t with
+ None -> Tactics.auto ~dbd ~params:[] ~universe
+ | Some t -> Tactics.apply t)
+ ]) (proof', goal)
+ in
+ ProofEngineTypes.mk_tactic aux
+;;
-let andelim = existselim;;
+let andelim t id1 t1 id2 t2 =
+ Tactics.elim_intros t
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2)
let rewritingstep ~dbd ~universe lhs rhs just last_step =
let aux ((proof,goal) as status) =
val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic
val existselim :
- Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
+ dbd:HMysql.dbd -> universe:Universe.universe ->
+ Cic.term option -> string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic
val andelim :
Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic
-(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Feb 25 17:03:54 CET 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar 1 10:25:04 CET 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
projects / helm.git / commitdiff