From 4e129f793e0a02343ae33d4f4bce6b4347e473ac Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 20 Mar 2026 17:21:57 +0100 Subject: [PATCH] Add a with_eta checker flag, and trusted implementation in safeconversion Eta-conversion is done the same way as in Rocq's conversion checker by expanding `G |- fun x : A => f ~= v` (with v weak-head irreducible) to `G, x : A |- f ~= v x` (if I did not make a mistake ;). A new `MetaRocq UnsafeCheck foo` command is available in the plugin, setting the checker_flag. This adds an axiom saying `with_eta = true -> False` as a shorcut to fill all the proofs. The default checker flags used for proofs everywhere have `with_eta = false` of course. --- common/theories/config.v | 28 +++++--- pcuic/theories/PCUICExpandLetsCorrectness.v | 3 +- .../src/g_metarocq_safechecker.mlg | 14 ++-- safechecker/theories/PCUICSafeConversion.v | 71 +++++++++++++++++-- test-suite/safechecker_test.v | 6 ++ 5 files changed, 103 insertions(+), 19 deletions(-) diff --git a/common/theories/config.v b/common/theories/config.v index 55ddc7889..fc2bf4498 100644 --- a/common/theories/config.v +++ b/common/theories/config.v @@ -16,7 +16,10 @@ Class checker_flags := { indices_matter : bool ; (* Lets in constructor types are allowed iff [true] *) - lets_in_constructor_types : bool + lets_in_constructor_types : bool ; + + (* Use the *unverified* eta rule in the checker *) + with_eta : bool; }. (** Should correspond to Rocq *) @@ -24,21 +27,24 @@ Local Instance default_checker_flags : checker_flags := {| check_univs := true ; prop_sub_type := true; indices_matter := false; - lets_in_constructor_types := true + lets_in_constructor_types := true; + with_eta := false; |}. Local Instance type_in_type : checker_flags := {| check_univs := false ; prop_sub_type := true; indices_matter := false; - lets_in_constructor_types := true + lets_in_constructor_types := true; + with_eta := false; |}. Local Instance extraction_checker_flags : checker_flags := {| check_univs := true ; prop_sub_type := false; indices_matter := false; - lets_in_constructor_types := false + lets_in_constructor_types := false; + with_eta := false; |}. (** [cf1 -> cf2] means that typing under [cf1] implies typing under [cf2] *) @@ -76,14 +82,16 @@ Definition laxest_checker_flags : checker_flags := {| check_univs := false ; prop_sub_type := true; indices_matter := false; - lets_in_constructor_types := true + lets_in_constructor_types := true; + with_eta := true; |}. Definition strictest_checker_flags : checker_flags := {| check_univs := true ; prop_sub_type := false; indices_matter := true; - lets_in_constructor_types := false + lets_in_constructor_types := false; + with_eta := false; |}. Lemma laxest_checker_flags_laxest : forall cf, impl cf laxest_checker_flags. @@ -107,14 +115,18 @@ Definition union_checker_flags (cf1 cf2 : checker_flags) : checker_flags := {| check_univs := andb cf2.(@check_univs) cf1.(@check_univs) ; prop_sub_type := orb cf1.(@prop_sub_type) cf2.(@prop_sub_type) ; indices_matter := andb cf2.(@indices_matter) cf1.(@indices_matter) - ; lets_in_constructor_types := orb cf1.(@lets_in_constructor_types) cf2.(@lets_in_constructor_types) |}. + ; lets_in_constructor_types := orb cf1.(@lets_in_constructor_types) cf2.(@lets_in_constructor_types) + ; with_eta := orb cf1.(@with_eta) cf2.(@with_eta) + |}. (** can check everything that both can check *) Definition inter_checker_flags (cf1 cf2 : checker_flags) : checker_flags := {| check_univs := orb cf2.(@check_univs) cf1.(@check_univs) ; prop_sub_type := andb cf1.(@prop_sub_type) cf2.(@prop_sub_type) ; indices_matter := orb cf2.(@indices_matter) cf1.(@indices_matter) - ; lets_in_constructor_types := andb cf1.(@lets_in_constructor_types) cf2.(@lets_in_constructor_types) |}. + ; lets_in_constructor_types := andb cf1.(@lets_in_constructor_types) cf2.(@lets_in_constructor_types) + ; with_eta := andb cf1.(@with_eta) cf2.(@with_eta) + |}. Lemma union_checker_flags_spec cf1 cf2 (cf' := union_checker_flags cf1 cf2) : impl cf1 cf' /\ impl cf2 cf' /\ (forall cf'', impl cf1 cf'' -> impl cf2 cf'' -> impl cf' cf''). diff --git a/pcuic/theories/PCUICExpandLetsCorrectness.v b/pcuic/theories/PCUICExpandLetsCorrectness.v index 5ea31f8dd..8ed66a4e1 100644 --- a/pcuic/theories/PCUICExpandLetsCorrectness.v +++ b/pcuic/theories/PCUICExpandLetsCorrectness.v @@ -1883,7 +1883,8 @@ Definition cf' cf := {| check_univs := cf.(@check_univs); prop_sub_type := cf.(@prop_sub_type); indices_matter := cf.(@indices_matter); - lets_in_constructor_types := false |}. + lets_in_constructor_types := false; + with_eta := cf.(with_eta) |}. Abbreviation wf_trans Σ := (@wf (cf' _) (trans_global_env Σ.1)). Abbreviation wf_ext_trans Σ := (@wf_ext (cf' _) (trans_global Σ)). diff --git a/safechecker-plugin/src/g_metarocq_safechecker.mlg b/safechecker-plugin/src/g_metarocq_safechecker.mlg index 76f0c995b..6bd18f96a 100644 --- a/safechecker-plugin/src/g_metarocq_safechecker.mlg +++ b/safechecker-plugin/src/g_metarocq_safechecker.mlg @@ -15,7 +15,7 @@ let pr_string l = (* We allow utf8 encoding *) str (caml_string_of_bytestring l) -let check ~opaque_access env evm poly (c, ustate) = +let check ~opaque_access env evm poly ~allow_eta (c, ustate) = debug (fun () -> str"Quoting"); let env = if poly then env else let (qs, us), (qcst, ucst) = Evd.sort_context_set evm in @@ -33,7 +33,7 @@ let check ~opaque_access env evm poly (c, ustate) = let check = time (str"Checking") (Extraction.infer_and_print_template_program_with_guard - Config0.default_checker_flags + Config0.{ default_checker_flags with with_eta = allow_eta } (* Config0.type_in_type *) prog) uctx @@ -44,11 +44,17 @@ let check ~opaque_access env evm poly (c, ustate) = } VERNAC COMMAND EXTEND MetaRocqSafeCheck CLASSIFIED AS QUERY STATE opaque_access -| #[ poly = polymorphic ] [ "MetaRocq" "SafeCheck" constr(c) ] -> { +| #[ poly = polymorphic ] [ "MetaRocq" "SafeCheck" constr(c) ] -> { let env = Global.env () in let evm = Evd.from_env env in let c = Constrintern.interp_constr env evm c in - check env evm poly c + check env evm poly ~allow_eta:false c + } +| #[ poly = polymorphic ] [ "MetaRocq" "UnsafeCheck" constr(c) ] -> { + let env = Global.env () in + let evm = Evd.from_env env in + let c = Constrintern.interp_constr env evm c in + check env evm poly ~allow_eta:true c } END diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v index 718b2d7dd..a648f8bcb 100644 --- a/safechecker/theories/PCUICSafeConversion.v +++ b/safechecker/theories/PCUICSafeConversion.v @@ -3372,8 +3372,6 @@ Equations (noeqns) isconv_array_values_aux all:eapply into_closed_red; tea; fvs. Qed. - - (* See https://github.com/coq/coq/blob/master/kernel/reduction.ml#L367 *) Opaque reduce_stack. Equations(noeqns) _isconv_prog (Γ : context) (leq : conv_pb) @@ -3608,8 +3606,7 @@ Equations (noeqns) isconv_array_values_aux } } ; - | prog_view_other t1 t2 h := - isconv_fallback leq t1 π1 t2 π2 aux + | prog_view_other t1 t2 h := isconv_fallback leq t1 π1 t2 π2 aux }. (* tApp *) @@ -5653,6 +5650,65 @@ Qed. auto. Qed. + Inductive is_eta_conv : term -> term -> Type := + | eta_left na A t x : is_eta_conv (tLambda na A t) x + | eta_right na A t x : is_eta_conv x (tLambda na A t) + | eta_none t1 t2 : ~~ isLambda t1 -> ~~ isLambda t2 -> is_eta_conv t1 t2. + + Equations eta_conv_view (t1 t2 : term) : is_eta_conv t1 t2 := + | tLambda na A t, x := eta_left na A t x ; + | x, tLambda na A t := eta_right na A t x ; + | t1, t2 := eta_none t1 t2 eq_refl eq_refl. + Axiom with_eta_cheat : with_eta = true -> forall {A}, A. + + Equations? isconv_eta (Γ : context) (leq : conv_pb) + (t1 : term) (π1 : stack) (h1 : wtp Γ t1 π1) + (t2 : term) (π2 : stack) (h2 : wtp Γ t2 π2) + (ir1 : isred_full Γ t1 π1) (ir2 : isred_full Γ t2 π2) + (hx : conv_stack_ctx Γ π1 π2) + (we : with_eta) + (ise : is_eta_conv t1 t2) + (aux : Aux Fallback Γ t1 π1 t2 π2 h2) + : ConversionResult (conv_term leq Γ t1 π1 t2 π2) := + isconv_eta Γ leq ?(tLambda na A t) π1 h1 t2 π2 h2 ir1 ir2 hx we (eta_left na A t t2) aux := + isconv_red leq t (Lambda_bd na A :: π1) (tApp (lift 1 0 t2) (tRel 0)) (Lambda_bd na A :: π2) aux; + isconv_eta Γ leq t1 π1 h1 ?(tLambda na A t) π2 h2 ir1 ir2 hx we (eta_right na A t t1) aux := + isconv_red leq (tApp (lift 1 0 t1) (tRel 0)) (Lambda_bd na A :: π1) t (Lambda_bd na A :: π2) aux; + isconv_eta Γ leq t1 π1 h1 t2 π2 h2 ir1 ir2 hx we (eta_none t1 t2 nlam1 nlam2) aux + := no ( + HeadMismatch + leq + (Γ ,,, stack_context π1) t1 + (Γ ,,, stack_context π2) t2 + ). + Proof. + all:clear aux. all: try specialize_Σ wfΣ. + - destruct h1 as (?&?); auto. + eapply isred_full_nobeta in ir1 => //. + now eapply with_eta_cheat. + - by apply with_eta_cheat. + - specialize (hx _ H). specialize_Σ H. + (* have h := abstract_env_ext_wf X H. as [[Σ' wfΣ]]. *) + eapply welltyped_zipc_zipp in h1 as hh1; eauto with pcuic. + + unfold zipp in hh1. + eapply isred_full_nobeta in ir1 => //. + eapply fst_decompose_stack_nil in ir1. + destruct (decompose_stack π1) as [l1 s1]. cbn in ir1. subst. + cbn in hh1. + now apply with_eta_cheat. + + now apply with_eta_cheat. + - now apply with_eta_cheat. (* Clearly false!*) + - now apply with_eta_cheat. (* Likely true !*) + - now apply with_eta_cheat. (* Likely true !*) + - now apply with_eta_cheat. (* Likely true !*) + - now apply with_eta_cheat. (* Likely true !*) + - now apply with_eta_cheat. (* Likely true !*) + - now apply with_eta_cheat. (* Likely true !*) + - now apply with_eta_cheat. (* Likely true !*) + Defined. + + Definition inspect_rev {A} (x : A) : {y : A | x = y} := exist x eq_refl. + (* TODO Factorise *) Equations(noeqns) _isconv_fallback (Γ : context) (leq : conv_pb) (t1 : term) (π1 : stack) (h1 : wtp Γ t1 π1) @@ -5681,13 +5737,16 @@ Qed. } ; | exist None nored2 with inspect (cmpb_term_napp leq #|(decompose_stack π1).1| t1 t2) := { | exist true eq1 := isconv_args leq t1 π1 t2 π2 aux; - | exist false noteq := - no ( + | exist false noteq with inspect_rev with_eta := { + | exist true we := isconv_eta Γ leq t1 π1 _ t2 π2 _ ir1 ir2 hx we (eta_conv_view t1 t2) aux ; + | exist false we := + no ( HeadMismatch leq (Γ ,,, stack_context π1) t1 (Γ ,,, stack_context π2) t2 ) + } } } }. diff --git a/test-suite/safechecker_test.v b/test-suite/safechecker_test.v index 22fe08270..0e67fea10 100644 --- a/test-suite/safechecker_test.v +++ b/test-suite/safechecker_test.v @@ -11,6 +11,12 @@ Environment is well-formed and Ind(Stdlib.Init.Datatypes.nat,0,[]) has type: Sor MetaRocq SafeCheck (3 + 1). +Axiom foo : nat -> nat. +Definition eta_rule : foo = fun x => foo x := eq_refl. + +Fail MetaRocq SafeCheck eta_rule. +MetaRocq UnsafeCheck eta_rule. + Definition bool_list := List.map negb (cons true (cons false nil)). (* was working a bit by accident *) (* MetaRocq SafeCheck bool_list. *)