From: Michele Galatà Date: Fri, 24 Jan 2003 11:15:57 +0000 (+0000) Subject: Added Decompose tactic X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=646460657ac3945ba1c5ed6817fde4b5c806d175;p=helm.git Added Decompose tactic --- diff --git a/helm/gTopLevel/eliminationTactics.ml b/helm/gTopLevel/eliminationTactics.ml index d2ed74810..fc6906cbc 100644 --- a/helm/gTopLevel/eliminationTactics.ml +++ b/helm/gTopLevel/eliminationTactics.ml @@ -30,38 +30,20 @@ let induction_tac ~term ~status:((proof,goal) as status) = let module P = PrimitiveTactics in let module T = Tacticals in let module S = ProofEngineStructuralRules in - let module U = UriManager in + let module U = UriManager in let (_,metasenv,_,_) = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let termty = T.type_of_aux' metasenv context term in - let uri,exp_named_subst,typeno,args = - match termty with - C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) - | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args) - | _ -> raise (ProofEngineTypes.Fail "Induction: Not an Inductive Type to Eliminate") - in - let eliminator_uri = - let base = U.buri_of_uri uri in - let name = - match CicEnvironment.get_obj uri with - C.InductiveDefinition (tys,_,_) -> - let (name,_,_,_) = List.nth tys typeno in - name - | _ -> assert false - in - let ext = - match T.type_of_aux' metasenv context ty with - C.Sort C.Prop -> "_ind" - | C.Sort C.Set -> "_rec" - | C.Sort C.Type -> "_rect" - | _ -> assert false - in - U.uri_of_string (base ^ "/" ^ name ^ ext ^ ".con") - in - apply_tac ~term:(C.Const (eliminator_uri , exp_named_subst)) (* come mi devo comportare con gli args??? *) + let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *) + + T.then_ ~start:(T.repeat_tactic + ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *) + ~continuation:(P.intros)) + ~continuation:(P.elim_intros_simpl ~term) + ~status ;; *) + let elim_type_tac ~term ~status = let module C = Cic in let module P = PrimitiveTactics in @@ -80,111 +62,159 @@ let elim_type_tac ~term ~status = *) -(* PROVE DI DECOMPOSE +(* PROVE DI DECOMPOSE *) +(* guardare quali sono i tipi induttivi decomponibili presenti in +profondita' nel term; chiamare una funzione di call-back passando questa +lista e ritornando la lista di termini che l'utente vuole decomporre; +decomporre. *) -(* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *) -let decompose_tac ~what ~where ~status:((proof,goal) as status) = - let module C = Cic in - let module R = CicReduction in - let module P = PrimitiveTactics in - let module T = Tacticals in - let module S = ProofEngineStructuralRules in - let rec decomposing ty what = - match (what) with - [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *) - | hd::tl as what -> - match ty with - (C.Appl (hd::_)) -> hd - | _ -> decomposing ty tl - in +exception InteractiveUserUriChoiceNotRegistered - let (_,metasenv,_,_) = proof in - let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in - T.repeat_tactic - ~tactic:(T.then_ - ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what)) - ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *) - ) - ~status +let interactive_user_uri_choice = + (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) : + (selection_mode:[`SINGLE | `EXTENDED] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> string list -> string list) ref) +;; + +exception IllFormedUri of string + +let cic_textual_parser_uri_of_string uri' = + try + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then + CicTextualParser0.ConUri (UriManager.uri_of_string uri') + else + if String.sub uri' (String.length uri' - 4) 4 = ".var" then + CicTextualParser0.VarUri (UriManager.uri_of_string uri') + else + (try + (* Inductive Type *) + let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in + CicTextualParser0.IndTyUri (uri'',typeno) + with + _ -> + (* Constructor of an Inductive Type *) + let uri'',typeno,consno = + CicTextualLexer.indconuri_of_uri uri' + in + CicTextualParser0.IndConUri (uri'',typeno,consno) + ) + with + _ -> raise (IllFormedUri uri') +;; + +let constructor_uri_of_string uri = + match cic_textual_parser_uri_of_string uri with + CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) + | _ -> assert false +;; + +let call_back uris = +(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) + let module U = UriManager in + List.map + (constructor_uri_of_string) + (!interactive_user_uri_choice + ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false + ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" + (List.map + (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)) + uris) + ) ;; -let decompose_tac ~clist ~status:((proof,goal) as status) = +let decompose_tac ~term ~status:((proof,goal) as status) = let module C = Cic in let module R = CicReduction in let module P = PrimitiveTactics in let module T = Tacticals in let module S = ProofEngineStructuralRules in - let (_,metasenv,_,_) = proof in + let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - - let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *) - try - let (proof, goallist) = - T.then_ - ~start:(P.elim_simpl_intros_tac ~term) - ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *) - ~status + let old_context_len = List.length context in +(* let nr_of_hyp_still_to_elim = ref 1 in *) + let termty = CicTypeChecker.type_of_aux' metasenv context term in + + let rec make_list termty = +(* altamente inefficente? *) + let rec search_inductive_types urilist termty = + (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) + match termty with + (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> + (uri,typeno,exp_named_subst)::urilist + | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> + (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist) + | _ -> urilist + (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *) + in + let rec purge_duplicates urilist = + let rec aux triple urilist = + match urilist with + [] -> [] + | hd::tl -> + if (hd = triple) + then aux triple tl + else hd::(aux triple tl) in - let rec step proof goallist = - match goallist with - [] -> (proof, []) - | hd::tl -> - let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in - let (proof'', goallist'') = step proof' tl in - proof'', goallist'@goallist'' - in - step proof goallist - with - (Fail _) -> T.id_tac - - in - let rec decomposing ty clist = (* term -> (term list) -> bool *) - match (clist) with - [] -> false - | hd::tl as clist -> - match ty with - (C.Appl (hd::_)) -> true - | _ -> decomposing ty tl - + match urilist with + [] -> [] + | hd::tl -> hd::(purge_duplicates (aux hd tl)) + in + purge_duplicates (search_inductive_types [] termty) in - let term = decomposing (R.whd context ty) clist in - if (term == C.Implicit) - then (Fail "Decompose: nothing to decompose or no application") - else repeat_elim ~term ~status -;; -*) -let decompose_tac ~clist ~status = - let module C = Cic in - let module R = CicReduction in - let module P = PrimitiveTactics in - let module T = Tacticals in - let module S = ProofEngineStructuralRules in + let urilist = + (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *) + (* N.B.: due to a bug in call_back exp_named_subst are not significant (they all are []) *) + call_back (make_list termty) in + + let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) = +prerr_endline ("%%%%%%% nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)); + if nr_of_hyp_still_to_elim <> 0 then + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let old_context_len = List.length context in + let termty = CicTypeChecker.type_of_aux' metasenv context term' in +prerr_endline ("%%%%%%% elim_clear termty= " ^ CicPp.ppterm termty); + match termty with + C.MutInd (uri,typeno,exp_named_subst) + | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) + when (List.mem (uri,typeno,exp_named_subst) urilist) -> +prerr_endline ("%%%%%%% elim " ^ CicPp.ppterm termty); + T.then_ + ~start:(P.elim_intros_simpl_tac ~term:term') + ~continuation:( + (* clear the hyp that has just been eliminated *) + (fun ~status:((proof,goal) as status) -> + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + let new_context_len = List.length context in +prerr_endline ("%%%%%%% newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); + let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in + T.then_ + ~start:( + if (term'==term) (* this is the first application of elim: there's no need to clear the hyp *) + then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end + else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end) + ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim) + ~status + )) + ~status + | _ -> + let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in +prerr_endline ("%%%%%%% fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)); + elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status + else (* raise (ProofEngineTypes.Fail "Decomopse: finished decomposing"); *) T.id_tac ~status - let rec choose ty = - function - [] -> C.Implicit (* a cosa serve? *) - | hd::tl -> - match ty with - (C.Appl (hd::_)) -> hd - | _ -> choose ty tl - in - - let decompose_one_tac ~clist ~status:((proof,goal) as status) = - let (_,metasenv,_,_) = proof in - let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let term = choose (R.whd context ty) clist in - if (term == C.Implicit) - then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application") - else T.then_ - ~start:(P.elim_intros_simpl_tac ~term) - ~continuation:(S.clear ~hyp:(List.hd context)) -(* (S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)*) - ~status - in - T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status + in +(* T.repeat_tactic ~tactic: *) + (elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1) + ~status ;; + diff --git a/helm/gTopLevel/eliminationTactics.mli b/helm/gTopLevel/eliminationTactics.mli index 00ccedd64..a49c77158 100644 --- a/helm/gTopLevel/eliminationTactics.mli +++ b/helm/gTopLevel/eliminationTactics.mli @@ -25,4 +25,9 @@ val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic -val decompose_tac: clist:(Cic.term list) -> ProofEngineTypes.tactic +val interactive_user_uri_choice: ( selection_mode:[`SINGLE | `EXTENDED] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> string list -> string list) ref + +val decompose_tac: term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/equalityTactics.ml b/helm/gTopLevel/equalityTactics.ml index afa210119..79b5b1dbe 100644 --- a/helm/gTopLevel/equalityTactics.ml +++ b/helm/gTopLevel/equalityTactics.ml @@ -182,6 +182,8 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = ;; +(* All these tacs do is applying the right constructor/theorem *) + let reflexivity_tac = IntroductionTactics.constructor_tac ~n:1 ;; diff --git a/helm/gTopLevel/esempi/decompose.cic b/helm/gTopLevel/esempi/decompose.cic new file mode 100644 index 000000000..f03d410a3 --- /dev/null +++ b/helm/gTopLevel/esempi/decompose.cic @@ -0,0 +1,5 @@ +!A:Prop.!B:Prop.!C:Prop.(and (or A C) (and (or A B) (or B C))) -> True + +!A:Prop.!B:Prop.!C:Prop.(and (sumbool A C) (and (or A B) !D:Prop.(or B D))) -> True + +!A:Prop.!B:Prop.!C:Prop.(and (and A C) (and (and A B) (and B C))) -> True diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index ebe26c3e3..f590481ba 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -352,6 +352,9 @@ let raise NoChoice ;; +EliminationTactics.interactive_user_uri_choice := + (fun ~selection_mode -> interactive_user_uri_choice ~selection_mode:selection_mode);; + let interactive_interpretation_choice interpretations = let chosen = ref None in let window = @@ -2148,9 +2151,7 @@ let assumption = call_tactic ProofEngine.assumption;; let generalize = call_tactic_with_goal_input ProofEngine.generalize;; let absurd = call_tactic_with_input ProofEngine.absurd;; let contradiction = call_tactic ProofEngine.contradiction;; -(* Galla chiede: come dare alla tattica la lista di termini da decomporre? -let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;; -*) +let decompose = call_tactic_with_input ProofEngine.decompose;; let whd_in_scratch scratch_window = call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch @@ -3083,6 +3084,9 @@ object(self) let searchpatternb = GButton.button ~label:"SearchPattern_Apply" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in + let decomposeb = + GButton.button ~label:"Decompose" + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in ignore(exactb#connect#clicked exact) ; ignore(applyb#connect#clicked apply) ; @@ -3118,6 +3122,7 @@ object(self) ignore(introsb#connect#clicked intros) ; ignore(searchpatternb#connect#clicked searchPattern) ; ignore(proofw#connect#selection_changed (choose_selection proofw)) ; + ignore(decomposeb#connect#clicked decompose) ; )) end ;; diff --git a/helm/gTopLevel/introductionTactics.ml b/helm/gTopLevel/introductionTactics.ml index bd29f4f5a..bc28c4170 100644 --- a/helm/gTopLevel/introductionTactics.ml +++ b/helm/gTopLevel/introductionTactics.ml @@ -34,7 +34,7 @@ let constructor_tac ~n ~status:(proof, goal) = | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) -> PrimitiveTactics.apply_tac ~status:(proof, goal) ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) - | _ -> raise (ProofEngineTypes.Fail "Constructor failed") + | _ -> raise (ProofEngineTypes.Fail "Constructor: failed") ;; diff --git a/helm/gTopLevel/negationTactics.ml b/helm/gTopLevel/negationTactics.ml index d55f04556..2b87bb911 100644 --- a/helm/gTopLevel/negationTactics.ml +++ b/helm/gTopLevel/negationTactics.ml @@ -30,7 +30,7 @@ let absurd_tac ~term ~status:((proof,goal) as status) = let module P = PrimitiveTactics in let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) + if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *) then P.apply_tac ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") @@ -42,7 +42,8 @@ let contradiction_tac ~status = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in - T.then_ + try + T.then_ ~start: P.intros_tac ~continuation:( T.then_ @@ -50,6 +51,9 @@ let contradiction_tac ~status = ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )) ~continuation: VariousTactics.assumption_tac) ~status + with + (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption") + (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *) ;; (* Questa era in fourierR.ml diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 7d637551f..379007021 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -231,7 +231,7 @@ let generalize term = apply_tactic (VariousTactics.generalize_tac ~term) let absurd term = apply_tactic (NegationTactics.absurd_tac ~term) let contradiction () = apply_tactic NegationTactics.contradiction_tac -let decompose ~clist = apply_tactic (EliminationTactics.decompose_tac ~clist) +let decompose term = apply_tactic (EliminationTactics.decompose_tac ~term) (* let decide_equality () = apply_tactic VariousTactics.decide_equality_tac diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index ab1b0285e..0263fd1e7 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -81,7 +81,7 @@ val generalize : Cic.term -> unit val absurd : Cic.term -> unit val contradiction : unit -> unit -val decompose : clist:(Cic.term list) -> unit +val decompose : Cic.term -> unit (* val decide_equality : unit -> unit diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml index d48b6a02c..1319c13ca 100644 --- a/helm/gTopLevel/tacticals.ml +++ b/helm/gTopLevel/tacticals.ml @@ -103,7 +103,8 @@ let then_ ~start ~continuation ~status = (* Galla *) -(* si suppone che tutte le tattiche sollevano solamente Fail? *) +(* si suppone che tutte le tattiche sollevino solamente Fail? *) + (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *) @@ -201,6 +202,10 @@ let rec solve_tactics ~(tactics: (string * tactic) list) ~status = + + + + (** tattica di prova per debuggare i tatticali *) (* let thens' ~start ~continuations ~status = diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index 604307cd3..1df9128c1 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -24,7 +24,10 @@ *) -(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *) +(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio +chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una +funzione di callback che restituisce la (sola) hyp da applicare *) + let assumption_tac ~status:((proof,goal) as status) = let module C = Cic in let module R = CicReduction in @@ -67,13 +70,56 @@ let assumption_tac ~status:(proof,goal)= (* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda e li aggiunga nel context, poi si conta la lunghezza di questo nuovo -contesto e si lifta *) +contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *) + let generalize_tac ~term ~status:((proof,goal) as status) = let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +(* + let found = false in + let rec new_context context ty = + if ty == term then let found = true in context + else match ty with + C.Rel _ + | C.Var _ + | C.Meta _ (* ???? *) + | C.Sort s + | C.Implicit -> context + | C.Cast (val,typ) -> + let tmp_context = new_context context val in + tmp_context @ (new_context tmp_context typ) + | C.Prod (binder, source, target) -> + | C.Lambda (binder, source, target) -> + let tmp_context = new_context context source in + tmp_context @ (new_context tmp_context binder) + | C.LetIn (binder, term, target) -> + | C.Appl applist -> + let rec aux context = + match applist with + [] -> context + | hd::tl -> + let tmp_context = (new_context context hd) + in aux tmp_context tl + in aux context applist + | C.Const (uri, exp_named_subst) + | C.MutInd (uri, typeno, exp_named_subst) + | C.MutConstruct (uri, typeno, consno, exp_named_subst) -> + match exp_named_subst with + [] -> context + | (uri,t)::_ -> new_context context (type_of_aux' context t) + | _ -> assert false + | C.MutCase (uri, typeno, outtype, iterm, patterns) + | C.Fix (funno, funlist) + | C.CoFix (funno, funlist) -> + match funlist with + [] -> context (* caso possibile? *) + | (name, index, type, body)::_ -> + let tmp_context = ~ + in +*) T.thens ~start:(P.cut_tac ~term:( @@ -94,24 +140,67 @@ let generalize_tac ~term ~status:((proof,goal) as status) = (* IN FASE DI IMPLEMENTAZIONE *) let decide_equality_tac = +(* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza +e' vera o no e lo risolve *) Tacticals.id_tac ;; -(* -let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) = + +let compare_tac ~term ~status:((proof, goal) as status) = +(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *) +(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *) let module C = Cic in let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in - if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2)) - (* controllo che i due termini siano comparabili *) - then - T.thens - ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *) - ~continuations:[split_tac ; P.intros_tac ~name:"FOO"] - else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types") + let termty = (CicTypeChecker.type_of_aux' metasenv context term) in + match termty with + (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + + let term' = (* (t1=t2)\/~(t1=t2) *) + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; + term ; + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ; + t1 ; + C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] + ] + ] + in + T.thens + ~start:(P.cut_tac ~term:term') + ~continuations:[ + T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; + decide_equality_tac] + | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + let term' = (* (t1=t2) \/ ~(t1=t2) *) + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; + term ; + C.Appl [ + (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ; + t1 ; + C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] + ] + ] + in + T.thens + ~start:(P.cut_tac ~term:term') + ~continuations:[ + T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; + decide_equality_tac] + | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") +;; + + +let discriminate_tac ~term ~status:((proof, goal) as status) = + let module C = Cic in + let module U = UriManager in + let module P = PrimitiveTactics in + let module T = Tacticals in + T.id_tac ;; -*)