From b635f87b5f17bc0d5b8329296a5bbdfbd0b87245 Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Fri, 14 Nov 2025 14:32:05 +0100 Subject: [PATCH] add a generic mechanism for rewriting with any equality satisfying J --- .../21098-tabareau-sortpoly-equality.sh | 1 + doc/corelib/index-list.html.template | 1 + plugins/ssr/ssrequality.ml | 46 +-- tactics/equality.ml | 315 ++++++++++++------ tactics/equality.mli | 7 +- tactics/tactics.ml | 32 +- tactics/tactics.mli | 8 +- test-suite/bugs/bug_14131.v | 5 +- test-suite/bugs/bug_17029.v | 2 + test-suite/bugs/bug_19203.v | 5 + test-suite/bugs/bug_19215.v | 5 + test-suite/bugs/bug_4216.v | 2 + test-suite/coqdoc/bug11353.html.out | 4 +- test-suite/coqdoc/bug11353.tex.out | 4 +- test-suite/coqdoc/links.html.out | 2 +- test-suite/coqdoc/links.tex.out | 2 +- test-suite/coqdoc/multiple_links.html.out | 2 +- test-suite/coqdoc/multiple_links.tex.out | 2 +- test-suite/coqdoc/typeclasses.html.out | 2 +- test-suite/coqdoc/typeclasses.tex.out | 2 +- test-suite/output/Arguments_renaming.out | 2 +- test-suite/output/Inductive.out | 2 +- test-suite/output/PrintInfos.out | 10 +- test-suite/output/SearchPattern.out | 3 + test-suite/output/bug_15020.out | 2 +- test-suite/success/Discriminate_HoTT.v | 7 + test-suite/success/Observational.v | 75 +++++ test-suite/success/RegisterScheme.v | 30 +- test-suite/success/eqtacticsnois.v | 2 + theories/Corelib/Init/Equality.v | 138 ++++++++ theories/Corelib/Init/Logic.v | 14 +- theories/Corelib/Init/Notations.v | 5 + theories/Corelib/Init/Prelude.v | 1 + theories/Corelib/Init/Tactics.v | 1 - theories/Corelib/extraction/ExtrOcamlBasic.v | 2 + 35 files changed, 540 insertions(+), 203 deletions(-) create mode 100644 dev/ci/user-overlays/21098-tabareau-sortpoly-equality.sh create mode 100644 test-suite/success/Observational.v create mode 100644 theories/Corelib/Init/Equality.v diff --git a/dev/ci/user-overlays/21098-tabareau-sortpoly-equality.sh b/dev/ci/user-overlays/21098-tabareau-sortpoly-equality.sh new file mode 100644 index 000000000000..ae84bd9eb600 --- /dev/null +++ b/dev/ci/user-overlays/21098-tabareau-sortpoly-equality.sh @@ -0,0 +1 @@ +overlay hott https://github.com/tabareau/HoTT sortpoly-equality 21098 diff --git a/doc/corelib/index-list.html.template b/doc/corelib/index-list.html.template index 987765ddbaec..edfdd0d8a3f0 100644 --- a/doc/corelib/index-list.html.template +++ b/doc/corelib/index-list.html.template @@ -15,6 +15,7 @@ through the Require Import command.

theories/Corelib/Init/Ltac.v theories/Corelib/Init/Notations.v + theories/Corelib/Init/Equality.v theories/Corelib/Init/Datatypes.v theories/Corelib/Init/Logic.v theories/Corelib/Init/Byte.v diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 080effd3dcaa..d4cc38261cd4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -161,7 +161,6 @@ let newssrcongrtac arg ist = (fun sigma' -> let x = List.find_map_exn (fun (n, x, _) -> if n = 0 then Some x else None) eq_args in let ty = fs sigma' x in - (* should we be using custom detyping flags? *) congrtac (arg, Detyping.detype Detyping.Now ~flags:(PrintingFlags.Detype.current()) env sigma ty) ist) (fun () -> try @@ -379,28 +378,13 @@ let id_map_redex _ sigma ~before:_ ~after = sigma, after ⊢ c : c_ty ⊢ c_ty ≡ EQN rdx_ty rdx new_rdx *) -let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty = + +let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty c_sort new_rdx dir (sigma, c) c_ty eq e_sort = let open Tacticals in Proofview.Goal.enter begin fun gl -> -(* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *) let env = Proofview.Goal.env gl in let beta = Reductionops.clos_norm_flags RedFlags.beta env sigma in let sigma, new_rdx = map_redex env sigma ~before:rdx ~after:new_rdx in - let sigma, elim = - let sort = Tacticals.elimination_sort_of_goal gl in - match Equality.eq_elimination_ref (dir = L2R) sort with - | Some r -> Evd.fresh_global env sigma r - | None -> - let ((kn, i) as ind, _) = Tacred.eval_to_quantified_ind env sigma c_ty in - let sort = Tacticals.elimination_sort_of_goal gl in - let sigma, elim = Evd.fresh_global env sigma (Elimschemes.lookup_eliminator env ind sort) in - if dir = R2L then sigma, elim else - let elim, _ = EConstr.destConst sigma elim in - let mp,l = KerName.repr (Constant.canonical elim) in - let l' = Nameops.add_suffix l "_r" in - let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in - Evd.fresh_global env sigma (ConstRef c1') - in (* The resulting goal *) let evty = beta (EConstr.Vars.subst1 new_rdx pred) in let typeclass_candidate = Typeclasses.is_maybe_class_type env sigma evty in @@ -412,9 +396,20 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ (* We check the proof is well typed. We assume that the type of [elim] is of the form [forall (A : Type) (x : A) (P : A -> Type@{s}), T] s.t. the only universes to unify are by checking the [A] and [P] arguments. *) - let sigma, p, pred = + let sigma, p, pred , elim = try let open EConstr in + let sigma, pred , elim = + let id = make_annot (Name pattern_id) ERelevance.relevant in + let penv = EConstr.push_rel (LocalAssum (id, rdx_ty)) env in + let pred = Vars.subst_var sigma pattern_id pred in + let sigma, predty , p_sort = + let sigma, predty = Typing.type_of penv sigma pred in + let p_sort = Retyping.get_sort_of penv sigma pred in + sigma, predty, p_sort in + let (sigma, elim), _ = Equality.lookup_eq_eliminator_with_error env sigma eq ~dep:false ~inccl:true ~l2r:(Some (dir = L2R)) ~c_sort ~e_sort ~p_sort in + sigma, { Environ.uj_val = mkLambda (id, rdx_ty, pred); uj_type = mkProd (id, rdx_ty, predty) } , elim + in let elimT = Retyping.get_type_of env sigma elim in let (idA, tA, elimT) = destProd sigma elimT in let (_, _, elimT) = destProd sigma elimT in @@ -424,15 +419,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ (* Do not fully retype pred, we already know that the domain is well-typed. The way this is written makes it easier to profile which part of typing is takes time. *) - let sigma, pred = - let id = make_annot (Name pattern_id) ERelevance.relevant in - let penv = EConstr.push_rel (LocalAssum (id, rdx_ty)) env in - let pred = Vars.subst_var sigma pattern_id pred in - let sigma, predty = Typing.type_of penv sigma pred in - sigma, { Environ.uj_val = mkLambda (id, rdx_ty, pred); uj_type = mkProd (id, rdx_ty, predty) } - in let sigma = Typing.check_actual_type env sigma pred tP in - sigma, p, pred.uj_val + sigma, p, pred.uj_val , elim with | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te))) | e when CErrors.noncritical e -> raise (PRtype_error None) @@ -495,7 +483,9 @@ let rwcltac ?under ?map_redex cl rdx dir (sigma, r) = match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when Ssrcommon.is_ind_ref env sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in - pirrel_rewrite ?under ?map_redex cl rdx a.(0) new_rdx dir (sigma, r) c_ty, Tacticals.tclIDTAC, sigma0 + let e_sort = Retyping.get_sort_of env sigma c_ty in + let c_sort = Retyping.get_sort_of env sigma a.(0) in + pirrel_rewrite ?under ?map_redex cl rdx a.(0) c_sort new_rdx dir (sigma, r) c_ty e e_sort, Tacticals.tclIDTAC, sigma0 | _ -> let cl' = EConstr.mkApp (EConstr.mkNamedLambda sigma (make_annot pattern_id ERelevance.relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in diff --git a/tactics/equality.ml b/tactics/equality.ml index d8b63c97d61a..53055fd5a897 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -13,7 +13,6 @@ open Pp open CErrors open Util open Names -open Nameops open Constr open Context open Termops @@ -207,6 +206,8 @@ let rewrite_keyed_unif_flags = { resolve_evars = false } +let rewrite_db = "rewrite_instances" + let tclNOTSAMEGOAL tac = let goal gl = Proofview.Goal.goal gl in Proofview.Goal.enter begin fun gl -> @@ -246,7 +247,7 @@ let elim_wrapper cls rwtac = Proofview.tclZERO ~info e end -let general_elim_clause with_evars frzevars tac cls c (ctx, eqn, args) l l2r elim = +let general_elim_clause with_evars frzevars tac cls c (ctx, eqn, args) l l2r elim indargs = (* Ad hoc asymmetric general_elim_clause *) let general_elim_clause0 rew = let rewrite_elim = @@ -261,7 +262,7 @@ let general_elim_clause with_evars frzevars tac cls c (ctx, eqn, args) l l2r eli let flags = make_flags frzevars sigma flags newevars in let metas = Clenv.clenv_meta_list rew in let submetas = (Clenv.clenv_arguments rew, metas) in - general_elim_clause with_evars flags cls (submetas, c, Clenv.clenv_type rew) elim + general_elim_clause with_evars flags cls (submetas, c, Clenv.clenv_type rew) elim indargs end in Proofview.Unsafe.tclEVARS (Clenv.clenv_evd rew) <*> @@ -311,29 +312,151 @@ let general_elim_clause with_evars frzevars tac cls c (ctx, eqn, args) l l2r eli let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hook.make () -(* Do we have a JMeq instance on twice the same domains ? *) +(* scheme_name returns the generic elimination principle to be used, dependending on dep(endency), in conclusion or not and left-to-right *) +let scheme_name dep lft2rgt inccl = + match dep, lft2rgt, inccl with + (* Non dependent case *) + | false, Some true, true -> rew_l2r_scheme_kind + | false, Some true, false -> rew_r2l_scheme_kind + | false, _, false -> rew_l2r_scheme_kind + | false, _, true -> rew_r2l_scheme_kind + (* Dependent case *) + | true, Some true, true -> rew_l2r_dep_scheme_kind + | true, Some true, false -> rew_l2r_forward_dep_scheme_kind + | true, _, true -> rew_r2l_dep_scheme_kind + | true, _, false -> rew_r2l_forward_dep_scheme_kind -let jmeq_same_dom env sigma (rels, eq, args) = - let env = push_rel_context rels env in - match args with - | [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2 - | _ -> false +let lib_ref_opt_pos name pos = + match Rocqlib.lib_ref_opt name with + | None -> None + | Some x -> Some (x , pos) -let eq_elimination_ref l2r sort = - let open UnivGen.QualityOrSet in - let name = - if l2r then - match sort with - | Qual (QConstant QProp) -> "core.eq.ind_r" - | Qual (QConstant QSProp) -> "core.eq.sind_r" - | Set | Qual (QConstant QType | QVar _) -> "core.eq.rect_r" - else - match sort with - | Qual (QConstant QProp) -> "core.eq.ind" - | Qual (QConstant QSProp) -> "core.eq.sind" - | Set | Qual (QConstant QType | QVar _) -> "core.eq.rect" - in - Rocqlib.lib_ref_opt name +(* eq_scheme_name returns the elimination principle to be used when dealing with eq, dependending on dep(endency), in conclusion or not and left-to-right *) +(* this could be handled by has_J_ref as well, but is more efficient has it bypasses the typeclass search *) +let eq_scheme_name dep lft2rgt inccl target is_set = let open Sorts.Quality in + match dep, lft2rgt, inccl, target , is_set with + (* Non dependent case *) + | false, Some true, true , QConstant QType , false -> lib_ref_opt_pos "core.eq.rect_r" (AtPosition 5) + | false, Some true, true , QConstant QType , true -> lib_ref_opt_pos "core.eq.rec_r" (AtPosition 5) + | false, Some true, true , QConstant QProp , _ -> lib_ref_opt_pos "core.eq.ind_r" (AtPosition 5) + | false, Some true, true , QConstant QSProp , _ -> lib_ref_opt_pos "core.eq.sind_r" (AtPosition 5) + | false, Some true, false , QConstant QType , false -> lib_ref_opt_pos "core.eq.rect" (AtPosition 5) + | false, Some true, false , QConstant QType , true -> lib_ref_opt_pos "core.eq.rec" (AtPosition 5) + | false, Some true, false , QConstant QProp , _ -> lib_ref_opt_pos "core.eq.ind" (AtPosition 5) + | false, Some true, false , QConstant QSProp , _ -> lib_ref_opt_pos "core.eq.sind" (AtPosition 5) + | false, _ , false , QConstant QType , false -> lib_ref_opt_pos "core.eq.rect_r" (AtPosition 5) + | false, _ , false , QConstant QType , true -> lib_ref_opt_pos "core.eq.rec_r" (AtPosition 5) + | false, _ , false , QConstant QProp , _ -> lib_ref_opt_pos "core.eq.ind_r" (AtPosition 5) + | false, _ , false , QConstant QSProp , _ -> lib_ref_opt_pos "core.eq.sind_r" (AtPosition 5) + | false, _ , true , QConstant QProp , _ -> lib_ref_opt_pos "core.eq.ind" (AtPosition 5) + | false, _ , true , QConstant QSProp , _ -> lib_ref_opt_pos "core.eq.sind" (AtPosition 5) + | false, _ , true , QConstant QType , false -> lib_ref_opt_pos "core.eq.rect" (AtPosition 5) + | false, _ , true , QConstant QType , true -> lib_ref_opt_pos "core.eq.rec" (AtPosition 5) + (* Dependent case *) + | true, Some true, true , QConstant QType , _ -> lib_ref_opt_pos "core.eq.rect_r_dep" (AtPosition 5) + | true, Some true, true , QConstant QProp , _ -> lib_ref_opt_pos "core.eq.ind_r_dep" (AtPosition 5) + | true, _ , true , QConstant QType , _ -> lib_ref_opt_pos "core.eq.rect_dep" (AtPosition 5) + | true, _ , true , QConstant QProp , _ -> lib_ref_opt_pos "core.eq.ind_dep" (AtPosition 5) + | _ , _, _ , _ , _ -> None + + +(* has_J_ref returns the name of the class to be used, dependending on dep(endency), in conclusion or not and left-to-right *) +(* The integer encodes the position of the equality argument in the elimination principle, starting from 0 *) +let has_J_ref dep lft2rgt inccl = + match dep, lft2rgt, inccl with + (* Non dependent case *) + | false, Some true, true -> Rocqlib.lib_ref "core.Has_Leibniz_r" , AtPosition 5 + | false, Some true, false -> Rocqlib.lib_ref "core.Has_Leibniz" , AtPosition 5 + | false, _, false -> Rocqlib.lib_ref "core.Has_Leibniz_r" , AtPosition 5 + | false, _, true -> Rocqlib.lib_ref "core.Has_Leibniz" , AtPosition 5 + (* Dependent case *) + | true, Some true, true -> Rocqlib.lib_ref "core.Has_J_r" , AtPosition 5 + | true, Some true, false -> Rocqlib.lib_ref "core.Has_J_r_forward" , AtPosition 4 + | true, _, true -> Rocqlib.lib_ref "core.Has_J" , AtPosition 5 + | true, _, false -> Rocqlib.lib_ref "core.Has_J_forward" , AtPosition 4 + +let level_init l sigma = + let rec aux l sigma = + match l with + | [] -> sigma , [] + | levels :: ls -> + let sigma , new_level = Evd.new_univ_level_variable UState.univ_flexible sigma in + let sigma , r = aux ls sigma in + sigma , new_level :: r + in aux l sigma + +let dbg = CDebug.create ~name:"equality" () + +let lookup_eq_eliminator env sigma eq ~dep ~inccl ~l2r ~e_sort ~c_sort ~p_sort = + let has_elim_ref , indarg = has_J_ref dep l2r inccl in + let has_refl_ref = Rocqlib.lib_ref "core.Has_refl" in + let c_quality = ESorts.quality sigma c_sort in + let e_quality = ESorts.quality sigma e_sort in + let p_quality = ESorts.quality sigma p_sort in + let qs = [ c_quality; e_quality; p_quality ] in + let c_level = Sorts.univ_of_sort (ESorts.kind sigma c_sort) in + let e_level = Sorts.univ_of_sort (ESorts.kind sigma e_sort) in + let p_level = Sorts.univ_of_sort (ESorts.kind sigma p_sort) in + let sigma , univs = level_init [ c_level; e_level; p_level ] sigma in + let names = EInstance.make @@ UVars.Instance.of_array (Array.of_list qs, Array.of_list univs) in + let eta_expand name typ f = + let body = EConstr.mkApp (Vars.lift 1 f , [| mkRel 1 |] ) in + EConstr.mkLambda (EConstr.nameR name, typ , body) in + (* This patch is to handle template poly equality with carrier in Prop, because of cumulatitivty of Prop into Type *) + let c_type = EConstr.mkSort (ESorts.make (Sorts.make c_quality (Univ.Universe.make (List.hd univs)))) in + let eq = eta_expand (Id.of_string "A") c_type eq in + let sigma , has_J_class = Evd.fresh_global ~names env sigma has_elim_ref in + if dep then + let has_refl_names = + EInstance.make @@ UVars.Instance.of_array (Array.of_list (List.firstn 2 qs), Array.of_list (List.firstn 2 univs)) in + let sigma , has_refl_class = Evd.fresh_global ~names:has_refl_names env sigma has_refl_ref in + let sigma , apprefl = Typing.checked_appvect env sigma has_refl_class [| eq |] in + let sigma , has_refl = Evarutil.new_evar ~typeclass_candidate:true env sigma apprefl in + let sigma , app = Typing.checked_appvect env sigma has_J_class [| eq; has_refl |] in + (sigma, (app, indarg)) + else + let sigma , app = Typing.checked_appvect env sigma has_J_class [| eq |] in + (sigma , (app, indarg)) + +let lookup_eq_eliminator_tc env sigma eq ~dep ~inccl ~l2r ~c_sort ~e_sort ~p_sort = + let sigma, (query,indarg) = lookup_eq_eliminator env sigma eq + ~dep ~inccl ~l2r ~c_sort ~e_sort ~p_sort in + let db = Hints.searchtable_map rewrite_db in + let (sigma , c) = Class_tactics.resolve_one_typeclass ~db env sigma query in + let hd , _ = EConstr.decompose_app sigma c in + let c_name , _ = Constr.destConst (EConstr.to_constr sigma hd) in + let c = Reductionops.whd_const c_name env sigma c in + (sigma , c), indarg + +let lookup_eq_eliminator_with_error env sigma eq ~dep ~inccl ~l2r ~c_sort ~e_sort ~p_sort = + let is_global_exists gr c = match Rocqlib.lib_ref_opt gr with + | Some gr -> isRefX env sigma gr c + | None -> false in + let is_eq = is_global_exists "core.eq.type" eq in + let eq_scheme = eq_scheme_name dep l2r inccl (ESorts.quality sigma p_sort) (ESorts.is_set sigma p_sort) in + if is_eq && not (Option.is_empty eq_scheme) then + begin + match eq_scheme with + | Some (r , indarg) -> + let elim = destConstRef r in + let (sigma, (c,u)) = Evd.fresh_constant_instance env sigma elim in + dbg (fun () -> Termops.Internal.print_constr_env env sigma (mkConstU (c,u))); + (sigma , mkConstU (c,u)), indarg + | None -> assert false (* Not possible *) + end + (* avoid to check instance for non homogenous equality types *) + else begin + try + lookup_eq_eliminator_tc env sigma eq ~dep ~inccl ~l2r ~c_sort ~e_sort ~p_sort + with Not_found -> user_err Pp.( + str "Eliminator not found for query for equality carrier: " ++ Sorts.raw_pr (ESorts.kind sigma e_sort) ++ + str " carrier quality: " ++ Sorts.raw_pr (ESorts.kind sigma c_sort) ++ + str " target quality: " ++ Sorts.raw_pr (ESorts.kind sigma p_sort)) + end + +let lookup_eq_eliminator_opt env sigma eq ~dep ~inccl l2r ~c_sort ~e_sort ~p_sort = + try Some (lookup_eq_eliminator_with_error env sigma eq ~dep ~inccl ~l2r ~e_sort ~c_sort ~p_sort) + with _ -> None type eq_scheme_kind = Minimality of UnivGen.QualityOrSet.t | Rewriting | Equality @@ -359,84 +482,45 @@ let find_scheme kind scheme_name ind = warn_missing_scheme (kind, Ind_tables.scheme_kind_name scheme_name, ind); force_find_scheme scheme_name ind -let find_elim lft2rgt dep cls ((_, hdcncl, _) as t) = +let find_elim lft2rgt dep inccl type_of_cls (ctx, hdcncl, args) = Proofview.Goal.enter_one begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let is_global_exists gr c = match Rocqlib.lib_ref_opt gr with - | Some gr -> isRefX env sigma gr c - | None -> false + let gen_elim () = + match EConstr.kind sigma hdcncl with + | Ind (ind,u) -> + find_scheme Rewriting (scheme_name dep lft2rgt inccl) ind >>= fun elim -> + Proofview.tclEVARMAP >>= fun sigma -> + let (sigma, gref) = Evd.fresh_global env sigma elim in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (gref, UnknownPosition) + | _ -> assert false in - let inccl = Option.is_empty cls in - let is_eq = is_global_exists "core.eq.type" hdcncl in - let is_jmeq = is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma t in - if (is_eq || is_jmeq) && not dep + if List.length args = 3 then - let sort = elimination_sort_of_clause cls gl in - let c = - match EConstr.kind sigma hdcncl with - | Ind (ind_sp,u) -> - begin match lft2rgt, cls with - | Some true, None - | Some false, Some _ -> - begin match if is_eq then eq_elimination_ref true sort else None with - | Some r -> r - | None -> - let c1 = destConstRef (Elimschemes.lookup_eliminator env ind_sp sort) in - let mp,l = KerName.repr (Constant.canonical c1) in - let l' = add_suffix l "_r" in - let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - if not (Environ.mem_constant c1' (Global.env ())) then - user_err - (str "Cannot find rewrite principle " ++ Id.print l' ++ str "."); - Names.GlobRef.ConstRef c1' - end - | _ -> - begin match if is_eq then eq_elimination_ref false sort else None with - | Some r -> r - | None -> Elimschemes.lookup_eliminator env ind_sp sort - end - end - | _ -> - (* cannot occur since we checked that we are in presence of - Logic.eq or Jmeq just before *) - assert false - in - Proofview.tclUNIT c + let env' = EConstr.push_rel_context ctx env in + let args = Array.of_list args in + let e_sort = Retyping.get_sort_of env' sigma (mkApp (hdcncl, args)) in + let c_sort = Retyping.get_sort_of env' sigma args.(0) in + let p_sort = Retyping.get_sort_of env sigma type_of_cls in + match lookup_eq_eliminator_opt env sigma hdcncl ~dep ~inccl lft2rgt ~c_sort ~e_sort ~p_sort with + | Some ((sigma, c),indarg) -> + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (c,indarg) + | None -> gen_elim () else - let scheme_name = match dep, lft2rgt, inccl with - (* Non dependent case *) - | false, Some true, true -> rew_l2r_scheme_kind - | false, Some true, false -> rew_r2l_scheme_kind - | false, _, false -> rew_l2r_scheme_kind - | false, _, true -> rew_r2l_scheme_kind - (* Dependent case *) - | true, Some true, true -> rew_l2r_dep_scheme_kind - | true, Some true, false -> rew_l2r_forward_dep_scheme_kind - | true, _, true -> rew_r2l_dep_scheme_kind - | true, _, false -> rew_r2l_forward_dep_scheme_kind - in - match EConstr.kind sigma hdcncl with - | Ind (ind,u) -> find_scheme Rewriting scheme_name ind - | _ -> assert false + gen_elim () end -let type_of_clause cls gl = match cls with - | None -> Proofview.Goal.concl gl - | Some id -> Tacmach.pf_get_hyp_typ id gl - let leibniz_rewrite_ebindings_clause cls lft2rgt tac c ((_, hdcncl, _) as t) l with_evars frzevars dep_proof_ok = Proofview.Goal.enter begin fun gl -> let evd = Proofview.Goal.sigma gl in - let type_of_cls = type_of_clause cls gl in + let type_of_cls = match cls with + | None -> Proofview.Goal.concl gl + | Some id -> Tacmach.pf_get_hyp_typ id gl in let dep = dep_proof_ok && dependent_no_evar evd c type_of_cls in - find_elim lft2rgt dep cls t >>= fun elim -> - Proofview.tclENV >>= fun env -> - Proofview.tclEVARMAP >>= fun sigma -> - let (sigma, elim) = Evd.fresh_global env sigma elim in - Proofview.Unsafe.tclEVARS sigma <*> - general_elim_clause with_evars frzevars tac cls c t l - (match lft2rgt with None -> false | Some b -> b) elim + let inccl = Option.is_empty cls in + find_elim lft2rgt dep inccl type_of_cls t >>= fun (elim, indarg) -> + general_elim_clause with_evars frzevars tac cls c t l + (match lft2rgt with None -> false | Some b -> b) elim indarg end let adjust_rewriting_direction args lft2rgt = @@ -788,7 +872,7 @@ let set_keep_equality = KeepEqualitiesTable.set let keep_head_inductive sigma c = (* Note that we do not weak-head normalize c before checking it is an - applied inductive, because [get_sort_quality_of] did not use to either. + applied inductive, because [get_sort_sort_of] did not use to either. As a matter of fact, if it reduces to an applied template inductive type but is not syntactically equal to it, it will fail to project. *) let _, hd = EConstr.decompose_prod sigma c in @@ -1010,6 +1094,7 @@ let rec build_discriminator env sigma true_0 false_0 pos c = function let subval = build_discriminator cnum_env sigma true_0 false_0 pos newc l in kont sigma subval false_0 + (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the path (see allowed_sorts in find_positions), the positions could @@ -1039,23 +1124,33 @@ let gen_absurdity id = where P=[e:t]discriminator absurd_term=False *) - -let ind_scheme_of_eq lbeq to_kind = +let _ind_scheme_of_eq lbeq to_kind = (* use ind rather than case by compatibility *) let kind = Elimschemes.elim_scheme ~dep:false ~to_kind in find_scheme (Minimality to_kind) kind (destIndRef lbeq.eq) >>= fun c -> Proofview.tclUNIT c -let discrimination_pf e (lbeq,s,(t,t1,t2)) discriminator p_quality = +let discrimination_pf e (eq,_,s,(t,t1,t2)) discriminator p_sort = build_rocq_I () >>= fun i -> - ind_scheme_of_eq lbeq (UnivGen.QualityOrSet.of_quality p_quality) >>= fun eq_elim -> - pf_constr_of_global eq_elim >>= fun eq_elim -> + Proofview.Goal.enter_one begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ((sigma, c),_) = lookup_eq_eliminator_with_error env sigma eq + ~dep:false ~inccl:true ~l2r:(Some false) + ~e_sort:s + ~c_sort:(Retyping.get_sort_of env sigma t) + ~p_sort in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c >>= fun eq_elim -> Proofview.tclEVARMAP >>= fun sigma -> - Proofview.tclUNIT - (applist (eq_elim, [t;t1;mkNamedLambda sigma (make_annot e ERelevance.relevant) t discriminator;i;t2])) + let term = + (applist (eq_elim, [t;t1;mkNamedLambda sigma (make_annot e ERelevance.relevant) t discriminator;i;t2])) + in + let sigma, _ = Typing.solve_evars env sigma term in + Proofview.Unsafe.tclEVARS sigma >>= fun _ -> Proofview.tclUNIT term + end type equality = { - eq_data : (rocq_eq_data * ESorts.t * (EConstr.t * EConstr.t * EConstr.t)); + eq_data : ( EConstr.constr * GlobRef.t * ESorts.t * (EConstr.t * EConstr.t * EConstr.t)); (* equality data + A : Type, t1 : A, t2 : A *) eq_term : EConstr.t; (* term [M : R A t1 t2] where [R] is the equality from above *) @@ -1065,11 +1160,11 @@ type equality = { let eq_baseid = Id.of_string "e" -let discr_positions env sigma { eq_data = (_, s, (t, _, _)) as eq_data; eq_term = v; eq_evar = evs } cpath dirn = +let discr_positions env sigma { eq_data = (_, _ , s, (t, _, _)) as eq_data; eq_term = v; eq_evar = evs } cpath dirn = build_rocq_True () >>= fun true_0 -> build_rocq_False () >>= fun false_0 -> let false_ty = Retyping.get_type_of env sigma false_0 in - let false_kind = ESorts.quality sigma (Retyping.get_sort_of env sigma false_0) in + let false_kind = Retyping.get_sort_of env sigma false_0 in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e ERelevance.relevant,t)) env in @@ -1089,7 +1184,7 @@ let discr_positions env sigma { eq_data = (_, s, (t, _, _)) as eq_data; eq_term [onLastHypId gen_absurdity; Tactics.exact_check pf <*> Proofview.Unsafe.tclNEWGOALS evs] let discrEq eq = - let { eq_data = (_, s, (_, t1, t2)) } = eq in + let { eq_data = (_, _ , s, (_, t1, t2)) } = eq in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1126,7 +1221,7 @@ let onEquality with_evars tac (c,lbindc) = let goals = List.map_filter filter eq_clause.EClause.cl_holes in let cl_args = Array.map_of_list (fun h -> h.EClause.hole_evar) eq_clause.EClause.cl_holes in let (eq,u,eq_args) = find_this_eq_data_decompose env sigma eq_clause.cl_concl in - let eq = { eq_data = (eq, s, eq_args); eq_term = mkApp (c, cl_args); eq_evar = goals } in + let eq = { eq_data = (EConstr.mkIndU (Globnames.destIndRef eq.eq, u), eq.congr, s, eq_args); eq_term = mkApp (c, cl_args); eq_evar = goals } in Proofview.Unsafe.tclEVARS sigma <*> tac eq end @@ -1273,7 +1368,6 @@ let inject_if_homogenous_dependent_pair ty = (* cut with the good equality and prove the requested goal *) tclTHENLIST [ - Proofview.Unsafe.tclEVARS sigma; intro; onLastHyp (fun hyp -> Tacticals.pf_constr_of_global Rocqlib.(lib_ref "core.eq.type") >>= fun ceq -> @@ -1299,7 +1393,7 @@ let simplify_args env sigma t = | _ -> t let inject_at_positions env sigma l2r eq posns tac = - let { eq_data = (eq, s, (t,t1,t2)); eq_term = v; eq_evar = evs } = eq in + let { eq_data = (eq, congr, s, (t,t1,t2)); eq_term = v; eq_evar = evs } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (make_annot e ERelevance.relevant,t)) env in let evdref = ref sigma in @@ -1308,7 +1402,7 @@ let inject_at_positions env sigma l2r eq posns tac = (* arbitrarily take t1' as the injector default value *) let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in let injfun = mkNamedLambda sigma (make_annot e ERelevance.relevant) t injbody in - let sigma,congr = Evd.fresh_global env sigma eq.congr in + let sigma,congr = Evd.fresh_global env sigma congr in (* pf : eq t t1 t2 -> eq resty (injfun t1) (injfun t2) *) let mk c = Retyping.get_judgment_of env sigma c in let args = Array.map mk [|t; resty; injfun; t1; t2|] in @@ -1340,9 +1434,10 @@ let () = CErrors.register_handler (function | NothingToInject -> Some (Pp.str "Nothing to inject.") | _ -> None) + let injEqThen keep_proofs tac l2r eql = Proofview.Goal.enter begin fun gl -> - let { eq_data = (eq, s, (t,t1,t2)) } = eql in + let { eq_data = (eq, _ , s, (t,t1,t2)) } = eql in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let goalsort = Retyping.get_sort_of env sigma (Proofview.Goal.concl gl) in @@ -1414,7 +1509,7 @@ let injConcl flags ?injection_in_context () = injClause flags ?injection_in_cont let injHyp flags ?injection_in_context clear_flag id = injClause flags ?injection_in_context None false (Some (clear_flag,ElimOnIdent CAst.(make id))) let decompEqThen keep_proofs ntac eq = - let { eq_data = (_, eqsort, (_,t1,t2)) } = eq in + let { eq_data = (_, _ , eqsort, (_,t1,t2)) } = eq in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1440,12 +1535,12 @@ let dEq ~keep_proofs with_evars = let dEqThen ~keep_proofs with_evars ntac where = dEqThen0 ~keep_proofs with_evars (fun _ _ n -> ntac n) where -let intro_decomp_eq tac (eq, _, data) (c, t) = +let intro_decomp_eq tac (eq, congr, _, data) (c, t) = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let s = Retyping.get_sort_of env sigma t in - let eq = { eq_data = (eq, s, data); eq_term = c; eq_evar = [] } in + let eq = { eq_data = (eq, congr , s, data); eq_term = c; eq_evar = [] } in decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq end diff --git a/tactics/equality.mli b/tactics/equality.mli index b73402afd65c..fa3d56eeb6ad 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -27,7 +27,12 @@ type conditions = | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *) -val eq_elimination_ref : orientation -> UnivGen.QualityOrSet.t -> GlobRef.t option +val lookup_eq_eliminator_with_error : Environ.env -> Evd.evar_map -> Evd.econstr -> + dep:orientation -> inccl:orientation -> l2r:orientation option -> + c_sort:ESorts.t -> + e_sort:ESorts.t -> + p_sort:ESorts.t -> + (Evd.evar_map * Evd.econstr) * equality_position_on_elim (* Equivalent to [general_rewrite l2r] *) val rewriteLR : constr -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 29cd9472507d..d161b86d6505 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1133,6 +1133,10 @@ type 'a core_destruction_arg = | ElimOnIdent of lident | ElimOnAnonHyp of int +type equality_position_on_elim = + | UnknownPosition + | AtPosition of int + type 'a destruction_arg = clear_flag * 'a core_destruction_arg @@ -1268,7 +1272,7 @@ let index_of_ind_arg sigma t = *) type eliminator = -| ElimConstant of EConstr.constr +| ElimConstant of EConstr.constr * equality_position_on_elim (* Constant generated by a scheme function *) | ElimClause of EConstr.constr with_bindings (* Arbitrary expression provided by the user *) @@ -1278,9 +1282,13 @@ let general_elim_clause0 with_evars flags (submetas, c, ty) elim = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let clause, bindings, index = match elim with - | ElimConstant elimc -> + | ElimConstant (elimc, i) -> let elimt = Retyping.get_type_of env sigma elimc in - let i = index_of_ind_arg sigma elimt in + let elimt = Reductionops.whd_all env sigma elimt in + let i = match i with + | AtPosition i -> i + | UnknownPosition -> index_of_ind_arg sigma elimt + in (elimc, elimt), NoBindings, Some i | ElimClause (elimc, lbindelimc) -> let elimt = Retyping.get_type_of env sigma elimc in @@ -1295,12 +1303,16 @@ let general_elim_clause0 with_evars flags (submetas, c, ty) elim = Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags end -let general_elim_clause_in0 with_evars flags id (submetas, c, ty) elimc = +let general_elim_clause_in0 with_evars flags id (submetas, c, ty) elimc indarg = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let elimt = Retyping.get_type_of env sigma elimc in - let i = index_of_ind_arg sigma elimt in + let elimt = Reductionops.whd_all env sigma elimt in + let i = match indarg with + | AtPosition i -> i + | UnknownPosition -> index_of_ind_arg sigma elimt + in let elimclause = mk_clenv_from env sigma (elimc, elimt) in let indmv = try nth_arg (Some i) (clenv_arguments elimclause) @@ -1344,10 +1356,10 @@ let general_elim with_evars clear_flag (c, lbindc) elim = (apply_clear_request clear_flag (use_clear_hyp_by_default ()) id) end -let general_elim_clause with_evars flags where arg elim = +let general_elim_clause with_evars flags where arg elim indarg = match where with - | None -> general_elim_clause0 with_evars flags arg (ElimConstant elim) - | Some id -> general_elim_clause_in0 with_evars flags id arg elim + | None -> general_elim_clause0 with_evars flags arg (ElimConstant (elim, indarg)) + | Some id -> general_elim_clause_in0 with_evars flags id arg elim indarg (* Case analysis tactics *) @@ -1422,7 +1434,7 @@ let default_elim with_evars clear_flag (c,_ as cx) = let sigma, elim = find_ind_eliminator env sigma ind (Retyping.get_sort_quality_of env sigma concl) in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (general_elim with_evars clear_flag cx (ElimConstant (mkConstU elim))) + (general_elim with_evars clear_flag cx (ElimConstant (mkConstU elim, UnknownPosition))) end) begin function (e, info) -> match e with | IsNonrec -> @@ -2120,7 +2132,7 @@ let intro_decomp_eq ?loc l thin tac id = | Some (eq,u,eq_args) -> !intro_decomp_eq_function (fun n -> tac ((CAst.make id)::thin) (Some n) l) - (eq,t,eq_args) (c, t) + (EConstr.mkIndU (Globnames.destIndRef eq.eq, u),eq.congr,t,eq_args) (c, t) | None -> let info = Exninfo.reify () in Tacticals.tclZEROMSG ~info (str "Not a primitive equality here.") diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 58ddadff8d2a..d56898a70b1b 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -176,6 +176,10 @@ type 'a core_destruction_arg = | ElimOnIdent of lident | ElimOnAnonHyp of int +type equality_position_on_elim = + | UnknownPosition + | AtPosition of int + type 'a destruction_arg = clear_flag * 'a core_destruction_arg @@ -455,7 +459,7 @@ val default_elim : evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val general_elim_clause : evars_flag -> unify_flags -> Id.t option -> - ((metavariable list * Unification.Meta.t) * EConstr.t * EConstr.types) -> EConstr.t -> unit Proofview.tactic + ((metavariable list * Unification.Meta.t) * EConstr.t * EConstr.types) -> EConstr.t -> equality_position_on_elim -> unit Proofview.tactic (** [general_case_analysis with_evars clear (t, bindings)] performs case analysis on [t]. If [t] is a variable which is not in the context, we attempt to perform introductions @@ -677,7 +681,7 @@ val subst_one : (bool -> Id.t -> Id.t * constr * bool -> unit Proofview.tactic) Hook.t val declare_intro_decomp_eq : - ((int -> unit Proofview.tactic) -> Rocqlib.rocq_eq_data * types * + ((int -> unit Proofview.tactic) -> EConstr.constr * GlobRef.t * types * (types * constr * constr) -> constr * types -> unit Proofview.tactic) -> unit diff --git a/test-suite/bugs/bug_14131.v b/test-suite/bugs/bug_14131.v index 611464458e9a..98121af703c4 100644 --- a/test-suite/bugs/bug_14131.v +++ b/test-suite/bugs/bug_14131.v @@ -8,10 +8,7 @@ Set Elimination Schemes. Register JMeq as core.JMeq.type. -Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), - P x -> forall y, JMeq x y -> P y. - -Register JMeq_ind as core.JMeq.ind. +Scheme Rewriting for JMeq. Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y, JMeq y x -> P y. diff --git a/test-suite/bugs/bug_17029.v b/test-suite/bugs/bug_17029.v index 0579313e1131..733bdf681da0 100644 --- a/test-suite/bugs/bug_17029.v +++ b/test-suite/bugs/bug_17029.v @@ -2,6 +2,8 @@ Require Import Setoid. Definition mydef (A B : Type) := True. +Scheme Rewriting for True. + Goal (forall A B : Type, mydef A B) -> Type. intros. Fail rewrite <- H. diff --git a/test-suite/bugs/bug_19203.v b/test-suite/bugs/bug_19203.v index 6ad69a42bf09..5a031402a949 100644 --- a/test-suite/bugs/bug_19203.v +++ b/test-suite/bugs/bug_19203.v @@ -17,6 +17,11 @@ Definition seq_elim@{q;u v|} := | srefl => f end. +Definition seq_Has_Leibniz_elim@{s; l l' l''} : Has_Leibniz@{s s s;l l' l''} (@seq) := + @seq_elim. + +Hint Resolve seq_Has_Leibniz_elim : rewrite_instances. + Register seq as core.eq.type. Register srefl as core.eq.refl. Register seq_elim as core.eq.rect. diff --git a/test-suite/bugs/bug_19215.v b/test-suite/bugs/bug_19215.v index 0d664c109f3e..39c558ef1a4b 100644 --- a/test-suite/bugs/bug_19215.v +++ b/test-suite/bugs/bug_19215.v @@ -102,6 +102,11 @@ Register Scheme eq_ind as ind_nodep for eq. End equality. + Definition eq_Has_Leibniz_elim@{s s'; l l' l''} : Has_Leibniz@{s s' s' ; l l' l''} (@eq@{s s' ; l l'}) := + fun A x P t y e => match e with eq_refl => t end. + + Hint Resolve eq_Has_Leibniz_elim : rewrite_instances. + Inductive comparison : Set := | Eq : comparison | Lt : comparison diff --git a/test-suite/bugs/bug_4216.v b/test-suite/bugs/bug_4216.v index a85e2881edd1..9c1050ee64e9 100644 --- a/test-suite/bugs/bug_4216.v +++ b/test-suite/bugs/bug_4216.v @@ -2,6 +2,8 @@ Generalizable Variables T A. Inductive path `(a: A): A -> Type := idpath: path a a. +Scheme Rewriting for path. + Class TMonad (T: Type -> Type) := { bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B; ret: forall {A: Type}, A -> T A; diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out index 5261998235b9..710d5d2833dd 100644 --- a/test-suite/coqdoc/bug11353.html.out +++ b/test-suite/coqdoc/bug11353.html.out @@ -21,8 +21,8 @@
Definition a := 0. #[ universes( template) ]
Inductive mysum (A B:Type) : Type :=
-  | myinl : A → mysum A B
-  | myinr : B → mysum A B.
+  | myinl : A → mysum A B
+  | myinr : B → mysum A B.

#[local]Definition b := 1.
diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out index 1a6eb36f3aca..47a95bcb03fa 100644 --- a/test-suite/coqdoc/bug11353.tex.out +++ b/test-suite/coqdoc/bug11353.tex.out @@ -24,9 +24,9 @@ \coqdocnoindent \coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdef{Coqdoc.bug11353.A:1}{A}{\coqdocbinder{A}} \coqdef{Coqdoc.bug11353.B:2}{B}{\coqdocbinder{B}}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol \coqdocindent{1.00em} -\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}\coqdoceol +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Notations}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}\coqdoceol \coqdocindent{1.00em} -\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}.\coqdoceol +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Notations}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}.\coqdoceol \coqdocemptyline \coqdocnoindent \#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 13e8b8c10b38..05bd88914357 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -68,7 +68,7 @@ Various checks for coqdoc Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).

-Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A
+Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A

where "x = y :> A" := (@eq A x y) : type_scope.
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 5a035db885b4..63d2b7c367d8 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -60,7 +60,7 @@ Various checks for coqdoc \coqdockw{Notation} \coqdef{Coqdoc.links.:::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Corelib.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdef{Coqdoc.links.A:3}{A}{\coqdocbinder{A}}:\coqdockw{Type}) (\coqdef{Coqdoc.links.x:4}{x}{\coqdocbinder{x}}:\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}\coqdoceol +\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdef{Coqdoc.links.A:3}{A}{\coqdocbinder{A}}:\coqdockw{Type}) (\coqdef{Coqdoc.links.x:4}{x}{\coqdocbinder{x}}:\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Notations}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}\coqdoceol \coqdocnoindent \coqdoceol \coqdocnoindent diff --git a/test-suite/coqdoc/multiple_links.html.out b/test-suite/coqdoc/multiple_links.html.out index 66a4dc1f9f3d..3f5df5f2e3ff 100644 --- a/test-suite/coqdoc/multiple_links.html.out +++ b/test-suite/coqdoc/multiple_links.html.out @@ -19,7 +19,7 @@

Library Coqdoc.multiple_links

-Inductive t := X | T : t → t.
+Inductive t := X | T : t → t.
Check X.
Check t.
Check t_ind.
diff --git a/test-suite/coqdoc/multiple_links.tex.out b/test-suite/coqdoc/multiple_links.tex.out index c4541f778afa..38242e649fd2 100644 --- a/test-suite/coqdoc/multiple_links.tex.out +++ b/test-suite/coqdoc/multiple_links.tex.out @@ -20,7 +20,7 @@ \begin{coqdoccode} \coqdocnoindent -\coqdockw{Inductive} \coqdef{Coqdoc.multiple links.t}{t}{\coqdocinductive{t}} := \coqdef{Coqdoc.multiple links.X}{X}{\coqdocconstructor{X}} \ensuremath{|} \coqdef{Coqdoc.multiple links.T}{T}{\coqdocconstructor{T}} : \coqref{Coqdoc.multiple links.t:1}{\coqdocinductive{t}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.multiple links.t:1}{\coqdocinductive{t}}.\coqdoceol +\coqdockw{Inductive} \coqdef{Coqdoc.multiple links.t}{t}{\coqdocinductive{t}} := \coqdef{Coqdoc.multiple links.X}{X}{\coqdocconstructor{X}} \ensuremath{|} \coqdef{Coqdoc.multiple links.T}{T}{\coqdocconstructor{T}} : \coqref{Coqdoc.multiple links.t:1}{\coqdocinductive{t}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Notations}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.multiple links.t:1}{\coqdocinductive{t}}.\coqdoceol \coqdocnoindent \coqdockw{Check} \coqref{Coqdoc.multiple links.X}{\coqdocconstructor{X}}.\coqdoceol \coqdocnoindent diff --git a/test-suite/coqdoc/typeclasses.html.out b/test-suite/coqdoc/typeclasses.html.out index 29a342468d89..23260cb349b4 100644 --- a/test-suite/coqdoc/typeclasses.html.out +++ b/test-suite/coqdoc/typeclasses.html.out @@ -19,7 +19,7 @@

Library Coqdoc.typeclasses

-Class EqDec T := { eqb : T → T → bool }.
+Class EqDec T := { eqb : T → T → bool }.

Section TC.
diff --git a/test-suite/coqdoc/typeclasses.tex.out b/test-suite/coqdoc/typeclasses.tex.out index f1c94d43aa9c..1a20ef4f3b8d 100644 --- a/test-suite/coqdoc/typeclasses.tex.out +++ b/test-suite/coqdoc/typeclasses.tex.out @@ -20,7 +20,7 @@ \begin{coqdoccode} \coqdocnoindent -\coqdockw{Class} \coqdef{Coqdoc.typeclasses.EqDec}{EqDec}{\coqdocrecord{EqDec}} \coqdef{Coqdoc.typeclasses.T:1}{T}{\coqdocbinder{T}} := \{ \coqdef{Coqdoc.typeclasses.eqb}{eqb}{\coqdocprojection{eqb}} : \coqref{Coqdoc.typeclasses.T:1}{\coqdocvariable{T}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.typeclasses.T:1}{\coqdocvariable{T}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqexternalref{bool}{http://coq.inria.fr/stdlib/Corelib.Init.Datatypes}{\coqdocinductive{bool}} \}.\coqdoceol +\coqdockw{Class} \coqdef{Coqdoc.typeclasses.EqDec}{EqDec}{\coqdocrecord{EqDec}} \coqdef{Coqdoc.typeclasses.T:1}{T}{\coqdocbinder{T}} := \{ \coqdef{Coqdoc.typeclasses.eqb}{eqb}{\coqdocprojection{eqb}} : \coqref{Coqdoc.typeclasses.T:1}{\coqdocvariable{T}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Notations}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.typeclasses.T:1}{\coqdocvariable{T}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Corelib.Init.Notations}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqexternalref{bool}{http://coq.inria.fr/stdlib/Corelib.Init.Datatypes}{\coqdocinductive{bool}} \}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Section} \coqdef{Coqdoc.typeclasses.TC}{TC}{\coqdocsection{TC}}.\coqdoceol diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index af123329ebf4..44d996320118 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -23,7 +23,7 @@ eq_refl is template universe polymorphic Arguments eq_refl {B}%_type_scope {y}, [_] _ (where some original arguments have been renamed) Expands to: Constructor Corelib.Init.Logic.eq_refl -Declared in library Corelib.Init.Logic, line 382, characters 4-11 +Declared in library Corelib.Init.Logic, line 380, characters 4-11 Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x. Arguments myEq B%_type_scope x _ diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 62d1e8d0089b..fac27879494a 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -40,7 +40,7 @@ or is not universe polymorphic or may only be eliminated to produce values whose type is SProp or Prop. Arguments or (A B)%_type_scope Expands to: Inductive Corelib.Init.Logic.or -Declared in library Corelib.Init.Logic, line 89, characters 10-12 +Declared in library Corelib.Init.Logic, line 87, characters 10-12 sunit : SProp sunit is not universe polymorphic diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index a472dfd39e04..aa8a989b7526 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -21,7 +21,7 @@ eq_refl : forall {A : Type} {x : A}, x = x eq_refl is template universe polymorphic Arguments eq_refl {A}%_type_scope {x}, [_] _ Expands to: Constructor Corelib.Init.Logic.eq_refl -Declared in library Corelib.Init.Logic, line 382, characters 4-11 +Declared in library Corelib.Init.Logic, line 380, characters 4-11 eq_refl : forall {A : Type} {x : A}, x = x When applied to no arguments: @@ -84,7 +84,7 @@ Arguments bar {x} Module Corelib.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Corelib.Init.Logic.sym_eq -Declared in library Corelib.Init.Logic, line 754, characters 0-45 +Declared in library Corelib.Init.Logic, line 764, characters 0-45 eq_sym : forall [A : Type] [x y : A], x = y -> y = x @@ -115,14 +115,14 @@ Alias.eq is template universe polymorphic Arguments Alias.eq {A}%_type_scope x _ Expands to: Inductive PrintInfos.Alias.eq (syntactically equal to Corelib.Init.Logic.eq) -Declared in library Corelib.Init.Logic, line 381, characters 10-12 +Declared in library Corelib.Init.Logic, line 379, characters 10-12 Alias.eq_refl : forall {A : Type} {x : A}, x = x Alias.eq_refl is template universe polymorphic Arguments Alias.eq_refl {A}%_type_scope {x}, [_] _ Expands to: Constructor PrintInfos.Alias.eq_refl (syntactically equal to Corelib.Init.Logic.eq_refl) -Declared in library Corelib.Init.Logic, line 382, characters 4-11 +Declared in library Corelib.Init.Logic, line 380, characters 4-11 Alias.eq_ind : forall [A : Type] (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y @@ -132,7 +132,7 @@ Arguments Alias.eq_ind [A]%_type_scope x P%_function_scope eq_refl y e Alias.eq_ind is transparent Expands to: Constant PrintInfos.Alias.eq_ind (syntactically equal to Corelib.Init.Logic.eq_ind) -Declared in library Corelib.Init.Logic, line 381, characters 0-115 +Declared in library Corelib.Init.Logic, line 379, characters 0-115 fst : forall A B : Type, prod A B -> A fst is not universe polymorphic diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index c4407cec2a00..4a06c5c6eb78 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -95,6 +95,9 @@ iff_refl: forall A : Prop, A <-> A le_n: forall n : nat, n <= n eq_refl: forall {A : Type} {x : A}, x = x Nat.divmod: nat -> nat -> nat -> nat -> nat * nat +refl: + forall {eq : forall A : Type@{β0 ; _}, A -> A -> Type@{β1 ; _}}, + Has_refl eq -> forall (A : Type@{β0 ; _}) (x : A), eq A x x (use "About" for full details on the implicit arguments of eq_refl) conj: forall [A B : Prop], A -> B -> A /\ B pair: forall {A B : Type}, A -> B -> A * B diff --git a/test-suite/output/bug_15020.out b/test-suite/output/bug_15020.out index 609550bd1989..4f0b6afc8cdf 100644 --- a/test-suite/output/bug_15020.out +++ b/test-suite/output/bug_15020.out @@ -7,4 +7,4 @@ Arguments eq_rect {A}%_type_scope {x} P%_function_scope eq_refl {y} e (where some original arguments have been renamed) eq_rect is transparent Expands to: Constant Corelib.Init.Logic.eq_rect -Declared in library Corelib.Init.Logic, line 381, characters 0-115 +Declared in library Corelib.Init.Logic, line 379, characters 0-115 diff --git a/test-suite/success/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v index c889caf78f23..a5eb564c3cea 100644 --- a/test-suite/success/Discriminate_HoTT.v +++ b/test-suite/success/Discriminate_HoTT.v @@ -9,6 +9,8 @@ Unset Elimination Schemes. Set Universe Polymorphism. +Require Import Equality. + Declare ML Module "rocq-runtime.plugins.ltac". Global Set Default Proof Mode "Classic". @@ -47,6 +49,11 @@ Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y Arguments ap {A B} f {x y} p. Register ap as core.identity.congr. +Definition paths_Has_Leibniz_elim@{l l' l''} : Has_Leibniz@{Type Type Type;l l' l''} (@paths) := + fun A x P t y e => match e with idpath => t end. + +Hint Resolve paths_Has_Leibniz_elim : rewrite_instances. + Variant Empty : Type :=. Register Empty as core.False.type. diff --git a/test-suite/success/Observational.v b/test-suite/success/Observational.v new file mode 100644 index 000000000000..dd4e5f789a56 --- /dev/null +++ b/test-suite/success/Observational.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* SProp := + obseq_refl : x ~ x + +where "x ~ y" := (@obseq _ x y) : type_scope. + +Arguments obseq {A} x _. +Arguments obseq_refl {A x} , [A] x. + +Instance obseq_Has_refl@{α;l} : Has_refl@{α SProp;l Set} (@obseq) := + fun A x => obseq_refl. + +Instance obseq_Has_J_elim_SProp@{α;l} : Has_J@{α SProp SProp;l Set Set} (@obseq) _ + := @obseq_sind. + +Hint Resolve obseq_Has_J_elim_SProp : rewrite_instances. + +Instance obseq_Has_Leibniz_elim_SProp@{α;l} : Has_Leibniz@{α SProp SProp;l Set Set} (@obseq) + := fun A x P t y e => @obseq_sind A x (fun x _ => P x) t y e. + +Hint Resolve obseq_Has_Leibniz_elim_SProp : rewrite_instances. + +Instance obseq_Has_Leibniz_r_elim_SProp@{α;l +} : Has_Leibniz_r@{α SProp SProp;l Set Set} (@obseq) + := fun A x P t y e => @obseq_sind A x (fun x _ => P x) t y (sym@{α SProp;l Set} e). + +Hint Resolve obseq_Has_Leibniz_r_elim_SProp : rewrite_instances. + +Parameter cast@{α;u u' | u A -> B. + +Notation "e # a" := (cast _ _ e a) (at level 55, only parsing). + +Instance obseq_Has_Leibniz_elim@{α β;l l' +} : Has_Leibniz@{α SProp β;l Set l'} (@obseq) := + { leibniz := fun A x P px y e => cast (P x) (P y) (ap P e) px}. + +Hint Resolve obseq_Has_Leibniz_elim : rewrite_instances. + +Instance obseq_Has_Leibniz_r_elim@{α β;l l' +} : Has_Leibniz_r@{α SProp β;l Set l'} (@obseq) := + { leibniz_r := fun A x P px y e => cast (P x) (P y) (ap P (sym e)) px}. + +Hint Resolve obseq_Has_Leibniz_r_elim : rewrite_instances. + +Definition obseq_apd@{sa sb; la lb lb' +} + {A : Type@{sa;la}} {a} (P : forall b : A, a ~ b -> Type@{sb ; lb}) + (b : A) (e : a ~ b) : @obseq _ (P a (refl A a)) (P b e) := + J_eliminator _ a (fun b e => @obseq _ (P a (refl _ _)) (P b e)) (refl _ _) b e. + +Instance obseq_Has_J_elim@{α β;l l' +} : Has_J@{α SProp β;l l l'} (@obseq) _ := + fun A a P t b e => cast (P a (refl _ _)) (P b e) (obseq_apd@{α β ;l l' _ _} P b e) t. + +Hint Resolve obseq_Has_J_elim : rewrite_instances. + +Lemma test {A:Type} (a b : A) (P : A -> Type) : a ~ b -> P a -> P b. +Proof. + intros e Pa. rewrite <- e. auto. +Defined. + +Lemma test2 {A:Type} (a b : A) (P : A -> Type) : a ~ b -> P a -> P b. +Proof. + intros e Pa. symmetry in e. rewrite e. auto. +Defined. diff --git a/test-suite/success/RegisterScheme.v b/test-suite/success/RegisterScheme.v index b4ee34b3fdd8..04636e1ac519 100644 --- a/test-suite/success/RegisterScheme.v +++ b/test-suite/success/RegisterScheme.v @@ -1,25 +1,3 @@ -(* use our own eq instead of the corelib one (which has rewriting schemes already declared) *) -Inductive eq (A:Type) (x:A) : A -> Prop := - eq_refl : x = x :>A - -where "x = y :> A" := (@eq A x y) : type_scope. - -Arguments eq {A} x _. -Arguments eq_refl {A x} , [A] x. - -Arguments eq_ind [A] x P _ y _ : rename. -Arguments eq_rec [A] x P _ y _ : rename. -Arguments eq_rect [A] x P _ y _ : rename. - -Notation "x = y" := (eq x y) : type_scope. -Notation "x <> y :> T" := (~ x = y :>T) : type_scope. -Notation "x <> y" := (~ (x = y)) : type_scope. - -Register eq as core.eq.type. -Register eq_refl as core.eq.refl. -Register eq_ind as core.eq.ind. -Register eq_rect as core.eq.rect. - Set Universe Polymorphism. Definition paths_rew_r_dep (A : Type) (x y : A) (P : forall y0 : A, y0 = y -> Type) @@ -64,11 +42,8 @@ Module Test1. Theorem upd_nop (a : A) (x : A) (e : a = x) (H: e = e) : eq_refl a = eq_refl. Proof. + (* The problem does not appear anymore *) (* neither TestLocal or TestExport registered the scheme *) - Fail subst. - Export TestLocal. - Fail subst. - Export TestExport. subst. exact H. Qed. @@ -81,8 +56,9 @@ Section GenMem. Theorem upd_nop (a : A) (x : A) (e : a = x) (H: e = e) : eq_refl a = eq_refl. Proof. + (* The problem does not appear anymore *) (* Export reverted by section end *) - Fail subst. + subst. Abort. End GenMem. diff --git a/test-suite/success/eqtacticsnois.v b/test-suite/success/eqtacticsnois.v index 7869532c67a4..2ffa4873b63c 100644 --- a/test-suite/success/eqtacticsnois.v +++ b/test-suite/success/eqtacticsnois.v @@ -8,6 +8,8 @@ Require Import Ltac. Register eq as core.eq.type. Register sym as core.eq.sym. +Scheme Rewriting for eq. + Goal forall A (x y:A) (_ : forall z, eq y z), eq x x. intros * H. replace x with y. - reflexivity. diff --git a/theories/Corelib/Init/Equality.v b/theories/Corelib/Init/Equality.v new file mode 100644 index 000000000000..a331edb2b0fd --- /dev/null +++ b/theories/Corelib/Init/Equality.v @@ -0,0 +1,138 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* A -> Type@{se;le}) +:= refl : forall A x, eq A x x. + +(* This class register a Martin-Löf like elimination principle *) + +Class Has_J@{sa se sp;la le lp} (eq : forall A : Type@{sa ; la}, A -> A -> Type@{se;le}) + (Has_refl : Has_refl eq) := + J_eliminator : forall (A : Type@{sa ; la}) (x : A) (P : forall y : A, eq A x y -> Type@{sp ; lp}), + P x (refl A x) -> forall y e, P y e. + +(* This class is for forward dependent rewriting *) + +Class Has_J_r@{sa se sp;la le lp} (eq : forall A : Type@{sa ; la}, A -> A -> Type@{se;le}) + (Has_refl : Has_refl eq) := + J_r_eliminator: forall (A : Type@{sa ; la}) (x : A) (P : forall y : A, eq A y x -> Type@{sp ; lp}), + P x (refl A x) -> forall y e, P y e. + +(* Those two classes are for dependent rewriting in an hypotesis *) + +Class Has_J_forward@{sa se sp;la le lp} (eq : forall A : Type@{sa ; la}, A -> A -> Type@{se;le}) + (Has_refl : Has_refl eq) := + J_forward : forall (A : Type@{sa ; la}) (x : A) (P : forall y : A, eq A x y -> Type@{sp ; lp}) y e, + P y e -> P x (refl A x). + +Class Has_J_r_forward@{sa se sp;la le lp} (eq : forall A : Type@{sa ; la}, A -> A -> Type@{se;le}) + (Has_refl : Has_refl eq) := + J_r_forward : forall (A : Type@{sa ; la}) (x : A) (P : forall y : A, eq A y x -> Type@{sp ; lp}) y e, + P y e -> P x (refl A x). + +(* Those two classes are for non-dependent rewriting *) + +Class Has_Leibniz@{sa se sp;la le lp} (eq : forall A : Type@{sa ; la}, A -> A -> Type@{se;le}) := + leibniz : forall (A : Type@{sa ; la}) (x : A) (P : A -> Type@{sp ; lp}), P x -> forall y, eq A x y -> P y. + +Class Has_Leibniz_r@{sa se sp;la le lp} (eq : forall A : Type@{sa ; la}, A -> A -> Type@{se;le}) := + leibniz_r : forall (A : Type@{sa ; la}) (x : A) (P : A -> Type@{sp ; lp}), P x -> forall y, eq A y x -> P y. + +Register Has_refl as core.Has_refl. +Typeclasses Opaque Has_refl. + +Register Has_J as core.Has_J. +Typeclasses Opaque Has_J. + +Register Has_J_r as core.Has_J_r. +Typeclasses Opaque Has_J_r. + +Register Has_J_forward as core.Has_J_forward. +Typeclasses Opaque Has_J_forward. + +Register Has_J_r_forward as core.Has_J_r_forward. +Typeclasses Opaque Has_J_r_forward. + +Register Has_Leibniz as core.Has_Leibniz. +Typeclasses Opaque Has_Leibniz. + +Register Has_Leibniz_r as core.Has_Leibniz_r. +Typeclasses Opaque Has_Leibniz_r. + +Definition J_no_dep@{s s' sp;l l' lp} {eq} {refl} (eqr : Has_J@{s s' sp;l l' lp} eq refl) : + forall (A : Type@{s ; l}) (x : A) (P : A -> Type@{sp ; lp}), P x -> forall y (e : eq A x y), P y := + fun A x P px y e => J_eliminator _ x (fun y _ => P y) px y e. + +Definition Has_J_Has_Leibniz@{s s' sp;l l' lp} {eq} {refl} (eqr : Has_J@{s s' sp;l l' lp} eq refl) : Has_Leibniz@{s s' sp;l l' lp} eq := + fun A x P px y e => J_no_dep eqr A x P px y e. + +Section ap. + Sort sa se sb se'. + Universe la le lb le'. + Context {eq : forall A : Type@{sa;la}, A -> A -> Type@{se;le} } + {eq' : forall A : Type@{sb; lb}, A -> A -> Type@{se';le'} } + {_refl: Has_refl@{sb se';lb le'} eq'} + {_leibniz: Has_Leibniz@{sa se se';la le le'} eq}. + + Definition ap [A : Type@{sa;la}] [B:Type@{sb;lb}] (f : A -> B) [x y : A] (e : eq _ x y) : eq' _ (f x) (f y) := + leibniz A x (fun y => eq' B (f x) (f y)) (refl _ _) y e. + +End ap. + +Register ap as core.ap. + +Section sym. + Sort sa se. + Universe la le. + Context {eq : forall A : Type@{sa;la}, A -> A -> Type@{se;le} } + {A : Type@{sa;la} } + {_refl: Has_refl@{sa se;la le} eq} + {_leibniz: Has_Leibniz@{sa se se;la le le} eq}. + + Definition sym {x y : A} (e : eq _ x y) : eq _ y x := + leibniz _ _ (fun y => eq A y _) (refl _ _) _ e. + +End sym. + +Definition Has_J_Has_J_forward@{sa se sp;la le lp} eq Has_refl + {has_J : Has_J@{sa se sp;la le lp} eq Has_refl} : + forall (A : Type@{sa ; la}) (x : A) (P : forall y : A, eq A x y -> Type@{sp ; lp}) y e, + P y e -> P x (refl A x) := + fun A x P y e => J_eliminator _ _ (fun y e => P y e -> P _ _) (fun x => x) _ _. + +Definition _Has_J_Has_J_forward@{sa se sp;la le lp} eq Has_refl + {has_J : Has_J@{sa se sp;la le lp} eq Has_refl} : Has_J_forward@{sa se sp;la le lp} eq Has_refl + := Has_J_Has_J_forward _ _. + +Hint Resolve _Has_J_Has_J_forward : rewrite_instances. + +Definition Has_J_r_Has_J_r_forward@{sa se sp;la le lp} eq Has_refl + {has_J : Has_J_r@{sa se sp;la le lp} eq Has_refl} : + forall (A : Type@{sa ; la}) (x : A) (P : forall y : A, eq A y x -> Type@{sp ; lp}) y e, + P y e -> P x (refl A x) := + fun A x P y e => J_r_eliminator _ _ (fun y e => P y e -> P _ _) (fun x => x) _ _. + +Definition _Has_J_r_Has_J_r_forward@{sa se sp;la le lp} eq Has_refl + {has_J : Has_J_r@{sa se sp;la le lp} eq Has_refl} : Has_J_r_forward@{sa se sp;la le lp} eq Has_refl + := Has_J_r_Has_J_r_forward _ _. + +Hint Resolve _Has_J_r_Has_J_r_forward : rewrite_instances. diff --git a/theories/Corelib/Init/Logic.v b/theories/Corelib/Init/Logic.v index 6d981c1feb6b..d89b2e54c8fb 100644 --- a/theories/Corelib/Init/Logic.v +++ b/theories/Corelib/Init/Logic.v @@ -13,8 +13,6 @@ Set Implicit Arguments. Require Export Notations. Require Import Ltac. -Notation "A -> B" := (forall (_ : A), B) : type_scope. - (** * Propositional connectives *) (** [True] is the always true proposition *) @@ -404,10 +402,17 @@ Hint Resolve ex_intro ex_intro2: core. Register eq as core.eq.type. Register eq_refl as core.eq.refl. Register eq_ind as core.eq.ind. +Register eq_sind as core.eq.sind. Register eq_rect as core.eq.rect. +Register eq_rec as core.eq.rec. Scheme Rewriting for eq. +Register eq_rew_dep as core.eq.rect_dep. +Register eq_rew_dep as core.eq.ind_dep. +Register eq_rew_r_dep as core.eq.rect_r_dep. +Register eq_rew_r_dep as core.eq.ind_r_dep. + Arguments eq_sym_involutive [A]%_type_scope [x y] e : rename. Section Logic_lemmas. @@ -463,6 +468,7 @@ Section Logic_lemmas. Defined. Register eq_ind_r as core.eq.ind_r. + Register eq_sind_r as core.eq.sind_r. Definition eq_rec_r : forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. @@ -473,6 +479,10 @@ Section Logic_lemmas. forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y. intros A x P H y H0; elim eq_sym with (1 := H0); assumption. Defined. + + Register eq_rect_r as core.eq.rect_r. + Register eq_rec_r as core.eq.rec_r. + End Logic_lemmas. Module EqNotations. diff --git a/theories/Corelib/Init/Notations.v b/theories/Corelib/Init/Notations.v index 3c59d5715e44..b97e86a166d5 100644 --- a/theories/Corelib/Init/Notations.v +++ b/theories/Corelib/Init/Notations.v @@ -137,3 +137,8 @@ Bind Scope type_scope with Sortclass. Open Scope core_scope. Open Scope function_scope. Open Scope type_scope. + + +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Create HintDb typeclass_instances discriminated. diff --git a/theories/Corelib/Init/Prelude.v b/theories/Corelib/Init/Prelude.v index a7106ac0f05d..f7041e993b61 100644 --- a/theories/Corelib/Init/Prelude.v +++ b/theories/Corelib/Init/Prelude.v @@ -9,6 +9,7 @@ (************************************************************************) Require Export Notations. +Require Export Equality. Require Export Logic. Require Export Datatypes. Require Export Specif. diff --git a/theories/Corelib/Init/Tactics.v b/theories/Corelib/Init/Tactics.v index ee8d0e2590bf..b6f8d48c5451 100644 --- a/theories/Corelib/Init/Tactics.v +++ b/theories/Corelib/Init/Tactics.v @@ -341,7 +341,6 @@ Tactic Notation "assert_fails" tactic3(tac) := Create HintDb rewrite discriminated. #[global] Hint Variables Opaque : rewrite. -Create HintDb typeclass_instances discriminated. (** A variant of [apply] using [refine], doing as much conversion as necessary. *) diff --git a/theories/Corelib/extraction/ExtrOcamlBasic.v b/theories/Corelib/extraction/ExtrOcamlBasic.v index 44dd2f627c6a..6aef76570ff9 100644 --- a/theories/Corelib/extraction/ExtrOcamlBasic.v +++ b/theories/Corelib/extraction/ExtrOcamlBasic.v @@ -35,3 +35,5 @@ Extract Inductive sumor => option [ Some None ]. Extract Inlined Constant andb => "(&&)". Extract Inlined Constant orb => "(||)". +(* for the dependent principle of equality*) +Extract Inlined Constant eq_rew_r_dep => "(fun _ _ t -> t)".