From 1dd2a5ffce1a935d18372d298e0d85df96ef53bd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 4 Apr 2007 12:36:33 +0000 Subject: [PATCH] alpha equivalence test factorized and moved to CicUtil --- components/acic_procedural/acic2Procedural.ml | 31 ++- components/cic/cicUtil.ml | 240 ++++++++++++------ components/cic/cicUtil.mli | 1 + components/cic_acic/doubleTypeInference.ml | 73 +----- components/tactics/inversion.ml | 4 +- components/tactics/primitiveTactics.ml | 2 +- components/tactics/proofEngineReduction.ml | 71 ------ components/tactics/proofEngineReduction.mli | 2 - 8 files changed, 185 insertions(+), 239 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index 08727be1c..fb99090e9 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -35,7 +35,6 @@ module A = Cic2acic module Ut = CicUtil module E = CicEnvironment module PEH = ProofEngineHelpers -module PER = ProofEngineReduction module Pp = CicPp module Cl = ProceduralClassify @@ -155,6 +154,14 @@ try ty with e -> failwith (msg ^ ": " ^ Printexc.to_string e) +let get_entry st id = + let rec aux = function + | [] -> assert false + | Some (C.Name name, e) :: _ when name = id -> e + | _ :: tl -> aux tl + in + aux st.context + (* proof construction *******************************************************) let unused_premise = "UNUSED" @@ -174,14 +181,20 @@ let mk_exp_args hd tl classes = let convert st ?name v = match get_inner_types st v with - | None -> [] - | Some (st, et) -> - let cst, cet = cic st, cic et in - if PER.alpha_equivalence cst cet then [] else + | None -> [] + | Some (sty, ety) -> + let csty, cety = cic sty, cic ety in + if Ut.alpha_equivalence csty cety then [] else let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in match name with - | None -> [T.Change (st, et, None, e, "")] - | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")] + | None -> [T.Change (sty, ety, None, e, "")] + | Some id -> + begin match get_entry st id with + | C.Def _ -> [T.ClearBody (id, "")] + | C.Decl w -> + if Ut.alpha_equivalence csty w then [] + else [T.Change (sty, ety, Some (id, id), e, "")] + end let get_intro = function | C.Anonymous -> unused_premise @@ -193,7 +206,7 @@ let mk_intros st script = T.Intros (Some count, List.rev st.intros, "") :: script let mk_arg st = function - | C.ARel (_, _, _, name) as what -> [] (* convert st ~name what *) + | C.ARel (_, _, _, name) as what -> convert st ~name what | _ -> [] let mk_fwd_rewrite st dtext name tl direction = @@ -233,7 +246,7 @@ and proc_letin st what name v t = let qs = [[T.Id ""]; proc_proof (next st) v] in [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in - C.Decl (get_type "TC1" st v), rqv + C.Decl (cic ity), rqv | None -> C.Def (cic v, None), [T.LetIn (intro, v, dtext)] in diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml index 496452a87..d79c233df 100644 --- a/components/cic/cicUtil.ml +++ b/components/cic/cicUtil.ml @@ -25,7 +25,7 @@ (* $Id$ *) -open Printf +module C = Cic exception Meta_not_found of int exception Subst_not_found of int @@ -109,30 +109,30 @@ in let rec is_meta_closed = function - Cic.Rel _ -> true - | Cic.Meta _ -> false - | Cic.Sort _ -> true - | Cic.Implicit _ -> assert false - | Cic.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty - | Cic.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest - | Cic.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest - | Cic.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest - | Cic.Appl l -> + C.Rel _ -> true + | C.Meta _ -> false + | C.Sort _ -> true + | C.Implicit _ -> assert false + | C.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty + | C.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest + | C.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest + | C.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest + | C.Appl l -> not (List.exists (fun x -> not (is_meta_closed x)) l) - | Cic.Var (_,exp_named_subst) - | Cic.Const (_,exp_named_subst) - | Cic.MutInd (_,_,exp_named_subst) - | Cic.MutConstruct (_,_,_,exp_named_subst) -> + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) + | C.MutInd (_,_,exp_named_subst) + | C.MutConstruct (_,_,_,exp_named_subst) -> not (List.exists (fun (_,x) -> not (is_meta_closed x)) exp_named_subst) - | Cic.MutCase (_,_,out,te,pl) -> + | C.MutCase (_,_,out,te,pl) -> is_meta_closed out && is_meta_closed te && not (List.exists (fun x -> not (is_meta_closed x)) pl) - | Cic.Fix (_,fl) -> + | C.Fix (_,fl) -> not (List.exists (fun (_,_,ty,bo) -> not (is_meta_closed ty) || not (is_meta_closed bo)) fl) - | Cic.CoFix (_,fl) -> + | C.CoFix (_,fl) -> not (List.exists (fun (_,ty,bo) -> not (is_meta_closed ty) || not (is_meta_closed bo)) @@ -146,18 +146,18 @@ let term_of_uri uri = let s = UriManager.string_of_uri uri in try (if UriManager.uri_is_con uri then - Cic.Const (uri, []) + C.Const (uri, []) else if UriManager.uri_is_var uri then - Cic.Var (uri, []) + C.Var (uri, []) else if not (Str.string_match xpointer_RE s 0) then raise (UriManager.IllFormedUri s) else let (baseuri,xpointer) = (Str.matched_group 1 s, Str.matched_group 2 s) in let baseuri = UriManager.uri_of_string baseuri in (match Str.split slash_RE xpointer with - | [_; tyno] -> Cic.MutInd (baseuri, int_of_string tyno - 1, []) + | [_; tyno] -> C.MutInd (baseuri, int_of_string tyno - 1, []) | [_; tyno; consno] -> - Cic.MutConstruct + C.MutConstruct (baseuri, int_of_string tyno - 1, int_of_string consno, []) | _ -> raise Exit)) with @@ -166,14 +166,14 @@ let term_of_uri uri = | Not_found -> raise (UriManager.IllFormedUri s) let uri_of_term = function - | Cic.Const (uri, _) - | Cic.Var (uri, _) -> uri - | Cic.MutInd (baseuri, tyno, _) -> + | C.Const (uri, _) + | C.Var (uri, _) -> uri + | C.MutInd (baseuri, tyno, _) -> UriManager.uri_of_string - (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1)) - | Cic.MutConstruct (baseuri, tyno, consno, _) -> + (Printf.sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1)) + | C.MutConstruct (baseuri, tyno, consno, _) -> UriManager.uri_of_string - (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri) + (Printf.sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri) (tyno + 1) consno) | _ -> raise (Invalid_argument "uri_of_term") @@ -181,32 +181,32 @@ let uri_of_term = function (* let pack terms = List.fold_right - (fun term acc -> Cic.Prod (Cic.Anonymous, term, acc)) - terms (Cic.Sort (Cic.Type (CicUniv.fresh ()))) + (fun term acc -> C.Prod (C.Anonymous, term, acc)) + terms (C.Sort (C.Type (CicUniv.fresh ()))) let rec unpack = function - | Cic.Prod (Cic.Anonymous, term, Cic.Sort (Cic.Type _)) -> [term] - | Cic.Prod (Cic.Anonymous, term, tgt) -> term :: unpack tgt + | C.Prod (C.Anonymous, term, C.Sort (C.Type _)) -> [term] + | C.Prod (C.Anonymous, term, tgt) -> term :: unpack tgt | _ -> assert false *) let rec strip_prods n = function | t when n = 0 -> t - | Cic.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt + | C.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt | _ -> failwith "not enough prods" let params_of_obj = function - | Cic.Constant (_, _, _, params, _) - | Cic.Variable (_, _, _, params, _) - | Cic.CurrentProof (_, _, _, _, params, _) - | Cic.InductiveDefinition (_, params, _, _) -> + | C.Constant (_, _, _, params, _) + | C.Variable (_, _, _, params, _) + | C.CurrentProof (_, _, _, _, params, _) + | C.InductiveDefinition (_, params, _, _) -> params let attributes_of_obj = function - | Cic.Constant (_, _, _, _, attributes) - | Cic.Variable (_, _, _, _, attributes) - | Cic.CurrentProof (_, _, _, _, _, attributes) - | Cic.InductiveDefinition (_, _, _, attributes) -> + | C.Constant (_, _, _, _, attributes) + | C.Variable (_, _, _, _, attributes) + | C.CurrentProof (_, _, _, _, _, attributes) + | C.InductiveDefinition (_, _, _, attributes) -> attributes let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj) @@ -238,26 +238,26 @@ let projections_of_record obj uri = let rec mk_rels howmany from = match howmany with | 0 -> [] - | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) + | _ -> (C.Rel (howmany + from)) :: (mk_rels (howmany-1) from) let id_of_annterm = function - | Cic.ARel (id,_,_,_) - | Cic.AVar (id,_,_) - | Cic.AMeta (id,_,_) - | Cic.ASort (id,_) - | Cic.AImplicit (id,_) - | Cic.ACast (id,_,_) - | Cic.AProd (id,_,_,_) - | Cic.ALambda (id,_,_,_) - | Cic.ALetIn (id,_,_,_) - | Cic.AAppl (id,_) - | Cic.AConst (id,_,_) - | Cic.AMutInd (id,_,_,_) - | Cic.AMutConstruct (id,_,_,_,_) - | Cic.AMutCase (id,_,_,_,_,_) - | Cic.AFix (id,_,_) - | Cic.ACoFix (id,_,_) -> id + | C.ARel (id,_,_,_) + | C.AVar (id,_,_) + | C.AMeta (id,_,_) + | C.ASort (id,_) + | C.AImplicit (id,_) + | C.ACast (id,_,_) + | C.AProd (id,_,_,_) + | C.ALambda (id,_,_,_) + | C.ALetIn (id,_,_,_) + | C.AAppl (id,_) + | C.AConst (id,_,_) + | C.AMutInd (id,_,_,_) + | C.AMutConstruct (id,_,_,_,_) + | C.AMutCase (id,_,_,_,_,_) + | C.AFix (id,_,_) + | C.ACoFix (id,_,_) -> id let rec rehash_term = @@ -392,25 +392,25 @@ let rehash_obj = C.InductiveDefinition (tl', params', paramsno, attrs) let rec metas_of_term = function - | Cic.Meta (i, c) -> [i,c] - | Cic.Var (_, ens) - | Cic.Const (_, ens) - | Cic.MutInd (_, _, ens) - | Cic.MutConstruct (_, _, _, ens) -> + | C.Meta (i, c) -> [i,c] + | C.Var (_, ens) + | C.Const (_, ens) + | C.MutInd (_, _, ens) + | C.MutConstruct (_, _, _, ens) -> List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) - | Cic.Cast (s, t) - | Cic.Prod (_, s, t) - | Cic.Lambda (_, s, t) - | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) - | Cic.Appl l -> List.flatten (List.map metas_of_term l) - | Cic.MutCase (uri, i, s, t, l) -> + | C.Cast (s, t) + | C.Prod (_, s, t) + | C.Lambda (_, s, t) + | C.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) + | C.Appl l -> List.flatten (List.map metas_of_term l) + | C.MutCase (uri, i, s, t, l) -> (metas_of_term s) @ (metas_of_term t) @ (List.flatten (List.map metas_of_term l)) - | Cic.Fix (i, il) -> + | C.Fix (i, il) -> List.flatten (List.map (fun (s, i, t1, t2) -> (metas_of_term t1) @ (metas_of_term t2)) il) - | Cic.CoFix (i, il) -> + | C.CoFix (i, il) -> List.flatten (List.map (fun (s, t1, t2) -> (metas_of_term t1) @ (metas_of_term t2)) il) @@ -418,41 +418,41 @@ let rec metas_of_term = function ;; module MetaOT = struct - type t = int * Cic.term option list + type t = int * C.term option list let compare = Pervasives.compare end module S = Set.Make(MetaOT) let rec metas_of_term_set = function - | Cic.Meta (i, c) -> S.singleton (i,c) - | Cic.Var (_, ens) - | Cic.Const (_, ens) - | Cic.MutInd (_, _, ens) - | Cic.MutConstruct (_, _, _, ens) -> + | C.Meta (i, c) -> S.singleton (i,c) + | C.Var (_, ens) + | C.Const (_, ens) + | C.MutInd (_, _, ens) + | C.MutConstruct (_, _, _, ens) -> List.fold_left (fun s (_,t) -> S.union s (metas_of_term_set t)) S.empty ens - | Cic.Cast (s, t) - | Cic.Prod (_, s, t) - | Cic.Lambda (_, s, t) - | Cic.LetIn (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t) - | Cic.Appl l -> + | C.Cast (s, t) + | C.Prod (_, s, t) + | C.Lambda (_, s, t) + | C.LetIn (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t) + | C.Appl l -> List.fold_left (fun s t -> S.union s (metas_of_term_set t)) S.empty l - | Cic.MutCase (uri, i, s, t, l) -> + | C.MutCase (uri, i, s, t, l) -> S.union (S.union (metas_of_term_set s) (metas_of_term_set t)) (List.fold_left (fun s t -> S.union s (metas_of_term_set t)) S.empty l) - | Cic.Fix (_, il) -> + | C.Fix (_, il) -> (List.fold_left (fun s (_,_,t1,t2) -> S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2)))) S.empty il - | Cic.CoFix (i, il) -> + | C.CoFix (i, il) -> (List.fold_left (fun s (_,t1,t2) -> S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2)))) @@ -465,3 +465,75 @@ let metas_of_term_set t = S.elements s ;; +(* syntactic_equality up to the *) +(* distinction between fake dependent products *) +(* and non-dependent products, alfa-conversion *) +let alpha_equivalence = + let rec aux t t' = + if t = t' then true + else + match t,t' with + C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) -> + UriManager.eq uri1 uri2 && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.Cast (te,ty), C.Cast (te',ty') -> + aux te te' && aux ty ty' + | C.Prod (_,s,t), C.Prod (_,s',t') -> + aux s s' && aux t t' + | C.Lambda (_,s,t), C.Lambda (_,s',t') -> + aux s s' && aux t t' + | C.LetIn (_,s,t), C.LetIn(_,s',t') -> + aux s s' && aux t t' + | C.Appl l, C.Appl l' -> + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true l l' + with + Invalid_argument _ -> false) + | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) -> + UriManager.eq uri uri' && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) -> + UriManager.eq uri uri' && i = i' && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.MutConstruct (uri,i,j,exp_named_subst1), + C.MutConstruct (uri',i',j',exp_named_subst2) -> + UriManager.eq uri uri' && i = i' && j = j' && + aux_exp_named_subst exp_named_subst1 exp_named_subst2 + | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> + UriManager.eq sp sp' && i = i' && + aux outt outt' && aux t t' && + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true pl pl' + with + Invalid_argument _ -> false) + | C.Fix (i,fl), C.Fix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (_,i,ty,bo) (_,i',ty',bo') -> + b && i = i' && aux ty ty' && aux bo bo' + ) true fl fl' + with + Invalid_argument _ -> false) + | C.CoFix (i,fl), C.CoFix (i',fl') -> + i = i' && + (try + List.fold_left2 + (fun b (_,ty,bo) (_,ty',bo') -> + b && aux ty ty' && aux bo bo' + ) true fl fl' + with + Invalid_argument _ -> false) + | _,_ -> false (* we already know that t != t' *) + and aux_exp_named_subst exp_named_subst1 exp_named_subst2 = + try + List.fold_left2 + (fun b (uri1,t1) (uri2,t2) -> + b && UriManager.eq uri1 uri2 && aux t1 t2 + ) true exp_named_subst1 exp_named_subst2 + with + Invalid_argument _ -> false + in + aux diff --git a/components/cic/cicUtil.mli b/components/cic/cicUtil.mli index 9b1fecf0c..de8c02095 100644 --- a/components/cic/cicUtil.mli +++ b/components/cic/cicUtil.mli @@ -65,3 +65,4 @@ val mk_rels : int -> int -> Cic.term list val rehash_term: Cic.term -> Cic.term val rehash_obj: Cic.obj -> Cic.obj +val alpha_equivalence: Cic.term -> Cic.term -> bool diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml index 1ea800a6b..ca5848369 100644 --- a/components/cic_acic/doubleTypeInference.ml +++ b/components/cic_acic/doubleTypeInference.ml @@ -33,6 +33,8 @@ exception WrongUriToMutualInductiveDefinitions of string;; exception ListTooShort;; exception RelToHiddenHypothesis;; +(*CSC: must alfa-conversion be considered or not? *) + let xxx_type_of_aux' m c t = try Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph)) @@ -163,75 +165,6 @@ let rec beta_reduce = C.CoFix (i,fl') ;; -(* syntactic_equality up to the *) -(* distinction between fake dependent products *) -(* and non-dependent products, alfa-conversion *) -(*CSC: must alfa-conversion be considered or not? *) -let syntactic_equality t t' = - let module C = Cic in - let rec syntactic_equality t t' = - if t = t' then true - else - match t, t' with - C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.Cast (te,ty), C.Cast (te',ty') -> - syntactic_equality te te' && - syntactic_equality ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Appl l, C.Appl l' -> - List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' - | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') -> - UriManager.eq uri uri' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutConstruct (uri,i,j,exp_named_subst), - C.MutConstruct (uri',i',j',exp_named_subst') -> - UriManager.eq uri uri' && i = i' && j = j' && - syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' - | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> - UriManager.eq sp sp' && i = i' && - syntactic_equality outt outt' && - syntactic_equality t t' && - List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,i,ty,bo) (_,i',ty',bo') -> - b && i = i' && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,ty,bo) (_,ty',bo') -> - b && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | _, _ -> false (* we already know that t != t' *) - and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 = - List.fold_left2 - (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true - exp_named_subst1 exp_named_subst2 - in - try - syntactic_equality t t' - with - _ -> false -;; - let rec split l n = match (l,n) with (l,0) -> ([], l) @@ -621,7 +554,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = None -> (* No expected type *) {synthesized = synthesized' ; expected = None}, synthesized - | Some ty when syntactic_equality synthesized' ty -> + | Some ty when CicUtil.alpha_equivalence synthesized' ty -> (* The expected type is synthactically equal to *) (* the synthesized type. Let's forget it. *) {synthesized = synthesized' ; expected = None}, synthesized diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml index d80814fc3..5f8a9a37f 100644 --- a/components/tactics/inversion.ml +++ b/components/tactics/inversion.ml @@ -123,7 +123,7 @@ let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty (CicSubstitution.lift 1 termty) isSetType (CicSubstitution.lift 1 term)) | [] -> ProofEngineReduction.replace_lifting - ~equality:(ProofEngineReduction.alpha_equivalence) + ~equality:(CicUtil.alpha_equivalence) ~what: (if isSetType then (rightparameters_ @ [term] ) else (rightparameters_ ) ) @@ -151,7 +151,7 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_ | [] when isSetType -> Cic.Lambda ( (Cic.Name ("lambda" ^ (string_of_int nright))), (ProofEngineReduction.replace_lifting - ~equality:(ProofEngineReduction.alpha_equivalence) + ~equality:(CicUtil.alpha_equivalence) ~what: (rightparameters_ ) ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars) ~where:termty), (* type of H with replaced right parameters *) diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 07723ea9f..5310fea7e 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -701,7 +701,7 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam let n_lambdas = n_right_args + 1 in let lifted_ty = CicSubstitution.lift n_lambdas ty in let replace = ProofEngineReduction.replace_lifting - ~equality:(ProofEngineReduction.alpha_equivalence) + ~equality:(CicUtil.alpha_equivalence) in let captured_ty = let what = diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml index f72ec4679..b55b92b93 100644 --- a/components/tactics/proofEngineReduction.ml +++ b/components/tactics/proofEngineReduction.ml @@ -49,77 +49,6 @@ exception RelToHiddenHypothesis;; module C = Cic module S = CicSubstitution -let alpha_equivalence = - let rec aux t t' = - if t = t' then true - else - match t,t' with - C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) -> - UriManager.eq uri1 uri2 && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.Cast (te,ty), C.Cast (te',ty') -> - aux te te' && aux ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - aux s s' && aux t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - aux s s' && aux t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - aux s s' && aux t t' - | C.Appl l, C.Appl l' -> - (try - List.fold_left2 - (fun b t1 t2 -> b && aux t1 t2) true l l' - with - Invalid_argument _ -> false) - | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) -> - UriManager.eq uri uri' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) -> - UriManager.eq uri uri' && i = i' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutConstruct (uri,i,j,exp_named_subst1), - C.MutConstruct (uri',i',j',exp_named_subst2) -> - UriManager.eq uri uri' && i = i' && j = j' && - aux_exp_named_subst exp_named_subst1 exp_named_subst2 - | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') -> - UriManager.eq sp sp' && i = i' && - aux outt outt' && aux t t' && - (try - List.fold_left2 - (fun b t1 t2 -> b && aux t1 t2) true pl pl' - with - Invalid_argument _ -> false) - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - (try - List.fold_left2 - (fun b (_,i,ty,bo) (_,i',ty',bo') -> - b && i = i' && aux ty ty' && aux bo bo' - ) true fl fl' - with - Invalid_argument _ -> false) - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - (try - List.fold_left2 - (fun b (_,ty,bo) (_,ty',bo') -> - b && aux ty ty' && aux bo bo' - ) true fl fl' - with - Invalid_argument _ -> false) - | _,_ -> false (* we already know that t != t' *) - and aux_exp_named_subst exp_named_subst1 exp_named_subst2 = - try - List.fold_left2 - (fun b (uri1,t1) (uri2,t2) -> - b && UriManager.eq uri1 uri2 && aux t1 t2 - ) true exp_named_subst1 exp_named_subst2 - with - Invalid_argument _ -> false - in - aux -;; - exception WhatAndWithWhatDoNotHaveTheSameLength;; (* Replaces "textually" in "where" every term in "what" with the corresponding diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli index 78f4b7f4c..2d04d3959 100644 --- a/components/tactics/proofEngineReduction.mli +++ b/components/tactics/proofEngineReduction.mli @@ -34,8 +34,6 @@ exception WrongShape exception AlreadySimplified exception WhatAndWithWhatDoNotHaveTheSameLength;; -val alpha_equivalence: Cic.term -> Cic.term -> bool - (* Replaces "textually" in "where" every term in "what" with the corresponding term in "with_what". The terms in "what" ARE NOT lifted when binders are crossed. The terms in "with_what" ARE NOT lifted when binders are crossed. -- 2.39.2