Add a with_eta checker flag, and trusted implementation in safeconversion

common/theories/config.v

@@ -16,29 +16,35 @@ 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 *)
 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'').

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 Σ)).

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
 

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
             )
+          }
         }
       }
     }.

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. *)