From 52e8395bd1cf23f6bad6be55b406a526ecf3ac11 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Michele=20Galat=C3=A0?= Date: Thu, 12 Dec 2002 15:22:09 +0000 Subject: [PATCH] Added an almost working version of Generalize tactic. Added yet another version of replace, useful in Generalize. --- helm/gTopLevel/proofEngineReduction.ml | 84 +++++++++++++++++++++++++ helm/gTopLevel/proofEngineReduction.mli | 3 + helm/gTopLevel/variousTactics.ml | 80 +++-------------------- 3 files changed, 96 insertions(+), 71 deletions(-) diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 1b36e686e..710a48164 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -247,6 +247,90 @@ let replace_lifting ~equality ~what ~with_what ~where = substaux 1 what where ;; +(* replaces in a term a term with another one. *) +(* Lifting are performed as usual. *) +let replace_lifting_csc nnn ~equality ~what ~with_what ~where = + let rec substaux k = + let module C = Cic in + let module S = CicSubstitution in + function + t when (equality t what) -> S.lift (k-1) with_what + | C.Rel n as t -> + if n < k then C.Rel n else C.Rel (n + nnn) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) + | C.Prod (n,s,t) -> + C.Prod (n, substaux k s, substaux (k + 1) t) + | C.Lambda (n,s,t) -> + C.Lambda (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,t) -> + C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k) tl in + begin + match substaux k he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,substaux k t) exp_named_subst + in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,substaux k outt, substaux k t, + List.map (substaux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> + (name, i, substaux k ty, substaux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> + (name, substaux k ty, substaux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in +let res = + substaux 1 where +in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res +;; + (* Takes a well-typed term and fully reduces it. *) (*CSC: It does not perform reduction in a Case *) let reduce context = diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli index f185dd663..91bce1a39 100644 --- a/helm/gTopLevel/proofEngineReduction.mli +++ b/helm/gTopLevel/proofEngineReduction.mli @@ -40,5 +40,8 @@ val replace : val replace_lifting : equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term +val replace_lifting_csc : + int -> equality:(Cic.term -> Cic.term -> bool) -> + what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term val reduce : Cic.context -> Cic.term -> Cic.term val simpl : Cic.context -> Cic.term -> Cic.term diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index 9e8b18b7d..7d0748385 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -65,88 +65,30 @@ let assumption_tac ~status:(proof,goal)= (* ANCORA DA DEBUGGARE *) - -(* IN FASE DI IMPLEMENTAZIONE *) - 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 uno = (C.Appl [ - C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 2, []) ; - C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 1, [])]) in - let tuno = CicTypeChecker.type_of_aux' metasenv context uno in -prerr_endline ("#### uno: " ^ CicPp.ppterm uno); -prerr_endline ("#### tuno: " ^ CicPp.ppterm tuno); -*) -prerr_endline ("#### dummy: " ^ (CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv context term))); -prerr_endline ("#### with_what: " ^ CicPp.ppterm (C.Rel 1)); -prerr_endline ("#### term: " ^ CicPp.ppterm term); -prerr_endline ("#### ty: " ^ CicPp.ppterm ty); - - T.thens ~start:(P.cut_tac ~term:( C.Prod ( - (C.Name "dummy_for_gen"), - (CicTypeChecker.type_of_aux' metasenv context term), - (ProofEngineReduction.replace_lifting + (C.Name "dummy_for_gen")), + (CicTypeChecker.type_of_aux' metasenv context term)), + (ProofEngineReduction.replace_lifting_csc 1 ~equality:(==) - ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) ~what:term - ~where:ty)))) - ~continuations: - [T.id_tac ; (P.apply_tac ~term:(C.Appl [(C.Rel 1); term]))] (* in quest'ordine o viceversa? provare *) -(* [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)*) + ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) + ~where:ty) + ) + ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] ~status ;; -(* -let generalize_tac ~term ~status:((proof,goal) as status) = - let module C = Cic in - let module H = ProofEngineHelpers 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 add_decl_tac ~term ~status:(proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - let _ = CicTypeChecker.type_of_aux' metasenv context term in - let newmeta = H.new_meta ~proof in - let context_for_newmeta = (Some (C.Name "dummy_for_gen",C.Decl term))::context in - let irl = H.identity_relocation_list_for_metavariable context_for_newmeta in - let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (C.Name "dummy_for_gen" , term , C.Meta (newmeta,irl)) in - let (newproof, _) = H.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] - in - (newproof, [newmeta]) - - in - T.then_ - ~start:(add_decl_tac ~term:(CicTypeChecker.type_of_aux' metasenv context term)) - ~continuation:( -T.id_tac) (* T.thens - ~start:(P.cut_tac ~term:(ProofEngineReduction.replace - ~equality:(==) - ~with_what:(C.Rel 1) (* dummy_for_gen *) - ~what:term - ~where:ty)) - ~continuations: - [T.id_tac ; (P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)]))]) (* in quest'ordine o viceversa? provare *) -(* [(P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)])) ; T.id_tac]) in quest'ordine o viceversa? provare *) -*) ~status -;; -*) - +(* IN FASE DI IMPLEMENTAZIONE *) let decide_equality_tac = Tacticals.id_tac @@ -174,10 +116,6 @@ let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) = (*** DOMANDE *** -- come faccio clear di un ipotesi di cui non so il nome? -- differenza tra elim e induction ...e inversion? -- come passo a decompose la lista di termini? -- ma la rewrite funzionava? -- come implemento la generalize? +- field, omega... come ring? *) -- 2.39.2