diff options
| -rw-r--r-- | pretyping/unification.ml | 161 | ||||
| -rw-r--r-- | tactics/tactics.ml | 39 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3698.v | 25 |
3 files changed, 117 insertions, 108 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 7544ba37a..64d837f0c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -416,8 +416,15 @@ let expand_key ts env sigma = function with RetypeError _ -> None) | None -> None -let subterm_restriction is_subterm flags = - not is_subterm && flags.restrict_conv_on_strict_subterms + +type unirec_flags = { + at_top: bool; + with_types: bool; + with_cs : bool; +} + +let subterm_restriction opt flags = + not opt.at_top && flags.restrict_conv_on_strict_subterms let key_of env b flags f = if subterm_restriction b flags then None else @@ -542,8 +549,18 @@ let eta_constructor_app env f l1 term = | _ -> assert false) | _ -> assert false +let debug_unification = ref (false) +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = + "Print states sent to w_unify unification"; + Goptions.optkey = ["Debug";"Tactic";"Unification"]; + Goptions.optread = (fun () -> !debug_unification); + Goptions.optwrite = (fun a -> debug_unification:=a); +} + let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = - let rec unirec_rec (curenv,nb as curenvnb) pb b wt ((sigma,metasubst,evarsubst) as substn) curm curn = + let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in let () = @@ -555,7 +572,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if Int.equal k1 k2 then substn else let stM,stN = extract_instance_status pb in let sigma = - if wt && flags.check_applied_meta_types then + if opt.with_types && flags.check_applied_meta_types then let tyM = Typing.meta_type sigma k1 in let tyN = Typing.meta_type sigma k2 in let l, r = if k2 < k1 then tyN, tyM else tyM, tyN in @@ -567,7 +584,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | Meta k, _ when not (dependent cM cN) (* helps early trying alternatives *) -> let sigma = - if wt && flags.check_applied_meta_types then + if opt.with_types && flags.check_applied_meta_types then (try let tyM = Typing.meta_type sigma k in let tyN = get_type_of curenv ~lax:true sigma cN in @@ -587,7 +604,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | _, Meta k when not (dependent cN cM) (* helps early trying alternatives *) -> let sigma = - if wt && flags.check_applied_meta_types then + if opt.with_types && flags.check_applied_meta_types then (try let tyM = get_type_of curenv ~lax:true sigma cM in let tyN = Typing.meta_type sigma k in @@ -629,20 +646,21 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb error_cannot_unify curenv sigma (m,n)) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) CONV true wt - (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2 + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} + (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 | Prod (na,t1,c1), Prod (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) pb true false - (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2 - | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b wt substn (subst1 a c) cN - | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b wt substn cM (subst1 a c) + unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} + (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 + | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN + | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (** Fast path for projections. *) | Proj (p1,c1), Proj (p2,c2) when eq_constant (Projection.constant p1) (Projection.constant p2) -> - (try unify_same_proj curenvnb cv_pb true wt substn c1 c2 + (try unify_same_proj curenvnb cv_pb {opt with at_top = true} + substn c1 c2 with ex when precatchable_exception ex -> - unify_not_same_head curenvnb pb b wt substn cM cN) + unify_not_same_head curenvnb pb opt substn cM cN) | Proj (p1,c1), _ when not (Projection.unfolded p1) -> let cM' = @@ -652,7 +670,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb to FO and eta in particular, fail gracefully in that case *) error_cannot_unify (fst curenvnb) sigma (cM,cN) in - unirec_rec curenvnb CONV true false substn cM' cN + unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn cM' cN | _, Proj (p2,c2) when not (Projection.unfolded p2) -> let cN' = @@ -662,43 +680,44 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb to FO and eta in particular, fail gracefully in that case *) error_cannot_unify (fst curenvnb) sigma (cM,cN) in - unirec_rec curenvnb CONV true false substn cM cN' + unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn cM cN' (* eta-expansion *) | Lambda (na,t1,c1), _ when flags.modulo_eta -> - unirec_rec (push (na,t1) curenvnb) CONV true wt substn + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn c1 (mkApp (lift 1 cN,[|mkRel 1|])) | _, Lambda (na,t2,c2) when flags.modulo_eta -> - unirec_rec (push (na,t2) curenvnb) CONV true wt substn + unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn (mkApp (lift 1 cM,[|mkRel 1|])) c2 (* For records *) | App (f1, l1), _ when flags.modulo_eta && is_eta_constructor_app curenv f1 l1 -> (try let l1', l2' = eta_constructor_app curenv f1 l1 cN in Array.fold_left2 - (unirec_rec curenvnb CONV true wt) substn l1' l2' + (unirec_rec curenvnb CONV {opt with at_top = true; with_cs = false}) substn l1' l2' with ex when precatchable_exception ex -> (match kind_of_term cN with - | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 - | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)) + | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 + | _ -> unify_not_same_head curenvnb pb opt substn cM cN)) | _, App (f2, l2) when flags.modulo_eta && is_eta_constructor_app curenv f2 l2 -> (try let l2', l1' = eta_constructor_app curenv f2 l2 cM in Array.fold_left2 - (unirec_rec curenvnb CONV true wt) substn l1' l2' + (unirec_rec curenvnb CONV {opt with at_top = true; with_cs = false}) substn l1' l2' with ex when precatchable_exception ex -> (match kind_of_term cM with - | App (f1,l1) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 - | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)) + | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 + | _ -> unify_not_same_head curenvnb pb opt substn cM cN)) | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> (try - Array.fold_left2 (unirec_rec curenvnb CONV true wt) - (unirec_rec curenvnb CONV true false - (unirec_rec curenvnb CONV true false substn p1 p2) c1 c2) + let opt' = {opt with at_top = true; with_types = false} in + Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true}) + (unirec_rec curenvnb CONV opt' + (unirec_rec curenvnb CONV opt' substn p1 p2) c1 c2) cl1 cl2 with ex when precatchable_exception ex -> - reduce curenvnb pb b wt substn cM cN) + reduce curenvnb pb opt substn cM cN) | App (f1,l1), _ when (isMeta f1 && use_metas_pattern_unification flags nb l1 @@ -708,8 +727,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb with | None -> (match kind_of_term cN with - | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 - | _ -> unify_not_same_head curenvnb pb b wt substn cM cN) + | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 + | _ -> unify_not_same_head curenvnb pb opt substn cM cN) | Some l -> solve_pattern_eqn_array curenvnb f1 l cN substn) @@ -721,18 +740,18 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb with | None -> (match kind_of_term cM with - | App (f1,l1) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 - | _ -> unify_not_same_head curenvnb pb b wt substn cM cN) + | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 + | _ -> unify_not_same_head curenvnb pb opt substn cM cN) | Some l -> solve_pattern_eqn_array curenvnb f2 l cM substn) | App (f1,l1), App (f2,l2) -> - unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 + unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> - unify_not_same_head curenvnb pb b wt substn cM cN + unify_not_same_head curenvnb pb opt substn cM cN - and unify_app (curenv, nb as curenvnb) pb b (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 = + and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 = try let expand_proj c l = match kind_of_term c with @@ -745,18 +764,20 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb in let f1, l1 = expand_proj f1 l1 in let f2, l2 = expand_proj f2 l2 in + let opta = {opt with at_top = true; with_types = false} in + let optf = {opt with at_top = true; with_types = true} in let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in - Array.fold_left2 (unirec_rec curenvnb CONV true false) - (unirec_rec curenvnb CONV true true substn f1 f2) l1 l2 + Array.fold_left2 (unirec_rec curenvnb CONV opta) + (unirec_rec curenvnb CONV optf substn f1 f2) l1 l2 with ex when precatchable_exception ex -> - try reduce curenvnb pb b false substn cM cN + try reduce curenvnb pb {opt with with_types = false} substn cM cN with ex when precatchable_exception ex -> - try canonical_projections curenvnb pb b cM cN substn + try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - expand curenvnb pb b false substn cM f1 l1 cN f2 l2 + expand curenvnb pb {opt with with_types = false} substn cM f1 l1 cN f2 l2 - and unify_same_proj (curenv, nb as curenvnb) cv_pb b wt substn c1 c2 = - let substn = unirec_rec curenvnb CONV b wt substn c1 c2 in + and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 = + let substn = unirec_rec curenvnb CONV opt substn c1 c2 in try (* Force unification of the types to fill in parameters *) let ty1 = get_type_of curenv ~lax:true sigma c1 in let ty2 = get_type_of curenv ~lax:true sigma c2 in @@ -768,33 +789,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb ty1 ty2 with RetypeError _ -> substn - and unify_not_same_head curenvnb pb b wt (sigma, metas, evars as substn) cM cN = - try canonical_projections curenvnb pb b cM cN substn + and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn) cM cN = + try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> let sigma', b = constr_cmp cv_pb sigma flags cM cN in if b then (sigma', metas, evars) else - try reduce curenvnb pb b wt substn cM cN + try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in let (f2,l2) = match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in - expand curenvnb pb b wt substn cM f1 l1 cN f2 l2 + expand curenvnb pb opt substn cM f1 l1 cN f2 l2 - and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN = - if use_full_betaiota flags && not (subterm_restriction b flags) then + and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN = + if use_full_betaiota flags && not (subterm_restriction opt flags) then let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in if not (Term.eq_constr cM cM') then - unirec_rec curenvnb pb b wt substn cM' cN + unirec_rec curenvnb pb opt substn cM' cN else let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in if not (Term.eq_constr cN cN') then - unirec_rec curenvnb pb b wt substn cM cN' + unirec_rec curenvnb pb opt substn cM cN' else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - and expand (curenv,_ as curenvnb) pb b wt (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 = + and expand (curenv,_ as curenvnb) pb opt (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 = let res = (* Try full conversion on meta-free terms. *) (* Back to 1995 (later on called trivial_unify in 2002), the @@ -808,7 +829,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (it is used by apply and rewrite); it might now be redundant with the support for delta-expansion (which is used essentially for apply)... *) - if subterm_restriction b flags then None else + if subterm_restriction opt flags then None else match flags.modulo_conv_on_closed_terms with | None -> None | Some convflags -> @@ -830,48 +851,48 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb match res with | Some substn -> substn | None -> - let cf1 = key_of curenv b flags f1 and cf2 = key_of curenv b flags f2 in + let cf1 = key_of curenv opt flags f1 and cf2 = key_of curenv opt flags f2 in match oracle_order curenv cf1 cf2 with | None -> error_cannot_unify curenv sigma (cM,cN) | Some true -> (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> - unirec_rec curenvnb pb b wt substn + unirec_rec curenvnb pb opt substn (whd_betaiotazeta sigma (mkApp(c,l1))) cN | None -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> - unirec_rec curenvnb pb b wt substn cM + unirec_rec curenvnb pb opt substn cM (whd_betaiotazeta sigma (mkApp(c,l2))) | None -> error_cannot_unify curenv sigma (cM,cN))) | Some false -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> - unirec_rec curenvnb pb b wt substn cM + unirec_rec curenvnb pb opt substn cM (whd_betaiotazeta sigma (mkApp(c,l2))) | None -> (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> - unirec_rec curenvnb pb b wt substn + unirec_rec curenvnb pb opt substn (whd_betaiotazeta sigma (mkApp(c,l1))) cN | None -> error_cannot_unify curenv sigma (cM,cN))) - and canonical_projections (curenv, _ as curenvnb) pb b cM cN (sigma,_,_ as substn) = + and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = if isApp cM then let f1l1 = whd_nored_state sigma (cM,Stack.empty) in if is_open_canonical_projection curenv sigma f1l1 then let f2l2 = whd_nored_state sigma (cN,Stack.empty) in - solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn + solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if + if not opt.with_cs || begin match flags.modulo_conv_on_closed_terms with | None -> true - | Some _ -> subterm_restriction b flags + | Some _ -> subterm_restriction opt flags end then error_cannot_unify (fst curenvnb) sigma (cM,cN) else @@ -880,11 +901,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let f2l2 = whd_nored_state sigma (cN, Stack.empty) in if is_open_canonical_projection curenv sigma f2l2 then let f1l1 = whd_nored_state sigma (cM, Stack.empty) in - solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn + solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - and solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 (sigma,ms,es) = + and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) = let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = try Evarconv.check_conv_record f1l1 f2l2 with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -901,24 +922,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (sigma,[],List.length bs - 1) bs in try + let opt' = {opt with with_types = false} in let (substn,_,_) = Reductionops.Stack.fold2 - (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u)) + (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) (evd,ms,es) us2 us in let (substn,_,_) = Reductionops.Stack.fold2 - (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u)) + (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) substn params1 params in - let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb b false) substn ts ts1 in + let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb opt') substn ts ts1 in let app = mkApp (c, Array.rev_of_list ks) in (* let substn = unirec_rec curenvnb pb b false substn t cN in *) - unirec_rec curenvnb pb b false substn c1 app + unirec_rec curenvnb pb opt' substn c1 app with Invalid_argument "Reductionops.Stack.fold2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) in + let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in let res = if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n - || subterm_restriction conv_at_top flags then None + || subterm_restriction opt flags then None else let sigma, b = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n @@ -933,7 +956,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb in match res with | Some sigma -> sigma, ms, es - | None -> unirec_rec (env,0) cv_pb conv_at_top false subst m n + | None -> unirec_rec (env,0) cv_pb opt subst m n let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e9fbf6d15..3d25e7607 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4134,45 +4134,6 @@ let admit_as_an_axiom = simplest_case (Coqlib.build_coq_proof_admitted ()) <*> Proofview.mark_as_unsafe -(* let current_sign = Global.named_context() *) -(* and global_sign = pf_hyps gl in *) -(* let poly = Flags.is_universe_polymorphism () in (\*FIXME*\) *) -(* let sign,secsign = *) -(* List.fold_right *) -(* (fun (id,_,_ as d) (s1,s2) -> *) -(* if mem_named_context id current_sign & *) -(* interpretable_as_section_decl (Context.lookup_named id current_sign) d *) -(* then (s1,add_named_decl d s2) *) -(* else (add_named_decl d s1,s2)) *) -(* global_sign (empty_named_context,empty_named_context) in *) -(* let name = add_suffix (get_current_proof_name ()) "_admitted" in *) -(* let na = next_global_ident_away name (pf_ids_of_hyps gl) in *) -(* let evd, nf = nf_evars_and_universes (project gl) in *) -(* let ctx = Evd.universe_context evd in *) -(* let newconcl = nf (pf_concl gl) in *) -(* let newsign = Context.map_named_context nf sign in *) -(* let concl = it_mkNamedProd_or_LetIn newconcl newsign in *) -(* if occur_existential concl then error"\"admit\" cannot handle existentials."; *) -(* let entry = *) -(* (Pfedit.get_used_variables(),poly,(concl,ctx),None) *) -(* in *) -(* let cd = Entries.ParameterEntry entry in *) -(* let decl = (cd, IsAssumption Logical) in *) -(* (\** ppedrot: seems legit to have admitted subproofs as local*\) *) -(* let con = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true na decl in *) -(* let evd, axiom = evd, (mkConstU (con, Univ.UContext.instance ctx)) in *) -(* (\* let evd, axiom = Evd.fresh_global (pf_env gl) (project gl) (ConstRef con) in *\) *) -(* let gl = tclTHEN (tclEVARS evd) *) -(* (tclTHEN (convert_concl_no_check newconcl DEFAULTcast) *) -(* (exact_check *) -(* (applist (axiom, *) -(* List.rev (Array.to_list (instance_from_named_context sign)))))) *) -(* gl *) -(* in *) -(* Pp.feedback Interface.AddedAxiom; *) -(* gl *) -(* >>>>>>> .merge_file_iUuzZK *) - let unify ?(state=full_transparent_state) x y = Proofview.Goal.nf_enter begin fun gl -> try diff --git a/test-suite/bugs/closed/3698.v b/test-suite/bugs/closed/3698.v new file mode 100644 index 000000000..3c53d243e --- /dev/null +++ b/test-suite/bugs/closed/3698.v @@ -0,0 +1,25 @@ +(* File reduced by coq-bug-finder from original input, then from 5479 lines to 4682 lines, then from 4214 lines to 86 lines, then from 60 lines to 25 lines *) +(* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *) +Set Primitive Projections. +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation pr1 := projT1. +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y. +Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. +Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }. +Global Existing Instance equiv_isequiv. +Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. +Axiom IsHSet : Type -> Type. +Local Open Scope equiv_scope. +Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. +Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). +Axiom issig_hSet: (sigT IsHSet) <~> hSet. +Definition isequiv_ap_setT X Y : IsEquiv (@ap _ _ setT X Y). +Proof. + assert (H'' : forall g : X = Y -> (issig_hSet^-1 X).1 = (issig_hSet^-1 Y).1, + g = g -> IsEquiv g) by admit. + Eval compute in (@projT1 Type IsHSet (@equiv_inv _ _ _ (equiv_isequiv _ _ issig_hSet) X)). + Fail apply H''. (* stack overflow *)
\ No newline at end of file |