Finish the proof of preservation of eta-expansion by dearging

erasure-plugin/src/g_metacoq_erasure.mlg

@@ -46,12 +46,18 @@ VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY
     let (c, _) = Constrintern.interp_constr env evm c in
     check ~bypass:true ~fast:false env evm c
   }
-| [ "MetaCoq" "Typed" "Erase" constr(c) ] -> {
+| [ "MetaCoq" "Bypass" "Typed" "Erase" constr(c) ] -> {
     let env = Global.env () in
     let evm = Evd.from_env env in
     let (c, _) = Constrintern.interp_constr env evm c in
     check ~bypass:true ~fast:false ~with_types:true env evm c
   }
+| [ "MetaCoq" "Typed" "Erase" constr(c) ] -> {
+    let env = Global.env () in
+    let evm = Evd.from_env env in
+    let (c, _) = Constrintern.interp_constr env evm c in
+    check ~bypass:false ~fast:false ~with_types:true env evm c
+  }
 | [ "MetaCoq" "Erase" constr(c) ] -> {
     let env = Global.env () in
     let evm = Evd.from_env env in

erasure-plugin/theories/ETransform.v

@@ -412,7 +412,7 @@ Proof.
    destruct p; cbn. clear.
   intros h; depind h.
   - destruct g; noconf H. constructor.
-  - destruct g0; noconf H0. destruct p as [[kn' b] d']. noconf H0.
+  - destruct g0; noconf H0. destruct p as [[kn' b] d'].
     constructor; eauto. now eapply fresh_global_trans.
 Qed.
 
@@ -535,7 +535,7 @@ Section Dearging.
     | None => (trans_env p.1.2, p.2)
     end.
 
-  Program Definition dearging_transform (efl := all_env_flags) {hastrel : has_tRel} {hastbox : has_tBox} :
+  Program Definition dearging_transform (efl := all_env_flags) :
     Transform.t _ _  EAst.term EAst.term _ _ (eval_typed_eprogram_masks opt_wcbv_flags) (eval_eprogram opt_wcbv_flags) :=
     {| name := "dearging";
       transform p _ := dearg p ;
@@ -561,7 +561,9 @@ Section Dearging.
       eapply wellformed_dearg; eauto.
       eapply wf.
     - rewrite /dearg_env -trans_env_debox. split; cbn.
-    todo "expanded".
+      eapply expanded_dearg_env; tea. apply exp.
+      eapply EEtaExpandedFix.isEtaExp_expanded, expanded_dearg; eauto.
+      apply EEtaExpandedFix.expanded_isEtaExp, exp.
   Qed.
 
   Next Obligation.
@@ -590,6 +592,8 @@ Section Dearging.
     * exists v. cbn. split => //.
   Qed.
 
+End Dearging.
+
 Definition extends_eprogram (p p' : eprogram) :=
   extends p.1 p'.1 /\ p.2 = p'.2.
 

erasure-plugin/theories/Erasure.v

@@ -227,7 +227,7 @@ Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl}
    remove_match_on_box_typed_transform (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
    (* Check if the preconditions for dearging are valid, otherwise dearging will be the identity *)
    dearging_checks_transform (hastrel := eq_refl) (hastbox := eq_refl) ▷
-   dearging_transform (hastrel := eq_refl) (hastbox := eq_refl) ▷
+   dearging_transform ▷
    rebuild_wf_env_transform true true ▷
    verified_lambdabox_typed_pipeline.
 

erasure/theories/EEtaExpandedFix.v

@@ -1980,4 +1980,64 @@ Proof.
     * intros [_ [_ [_ H]]]. move/andP: H => [] _. rewrite forallb_app.
       move=> /andP[] //=. now rewrite andb_true_r.
     * now move/and4P => [].
+Qed.
+
+Lemma isEtaExp_lift Σ Γ Γ' Γ'' t : isEtaExp Σ (Γ'' ++ Γ) t -> isEtaExp Σ (Γ'' ++ Γ' ++ Γ) (lift #|Γ'| #|Γ''| t).
+Proof using.
+  funelim (isEtaExp Σ _ t); cbn; simp_eta; try now easy; intros; solve_all.
+  all:cbn; simp_eta; toAll; bool; try rewrite -> forallb_InP_spec in *.
+  all:try solve [solve_all].
+
+  - destruct nth_error eqn:hnth => //=. move: hnth.
+    destruct (PCUICLiftSubst.nth_error_appP Γ'' Γ0 i) => h; noconf h; destruct (Nat.leb_spec #|Γ''| i); try lia; simp_eta.
+    * rewrite nth_error_app_lt //= e //=.
+    * rewrite nth_error_app_ge; try lia.
+      rewrite nth_error_app_ge; try lia.
+      replace (#|Γ'| + i - #|Γ''| - #|Γ'|) with (i - #|Γ''|) by lia.
+      now rewrite e.
+  - simp_eta. eapply (H Γ0 Γ' (0 :: Γ'')); trea.
+  - eapply (H0 Γ0 Γ' (0 :: Γ'')); trea.
+  - destruct block_args => //.
+  - solve_all.
+    specialize (a Γ0 Γ' (repeat 0 #|x.1| ++ Γ'') x.2).
+    rewrite -!app_assoc in a. len in a. now apply a.
+  - solve_all.
+    specialize (a Γ0 Γ' (repeat 0 #|mfix| ++ Γ'') (dbody x)).
+    rewrite -!app_assoc in a. len in a. now apply a.
+  - eapply InPrim_primProp in H.
+    solve_all. eapply primProp_map, primProp_impl; tea; cbn.
+    intros x [a exp].
+    specialize (a Γ0 Γ' Γ'' x).
+    now apply a.
+  - rewrite lift_mkApps /=.
+    rewrite isEtaExp_mkApps //=. bool.
+    + now len.
+    + solve_all.
+    + destruct block_args => //.
+  - rewrite lift_mkApps /=.
+    rewrite isEtaExp_mkApps //=. bool.
+    + len.
+      move: H1. rewrite /isEtaExp_fixapp nth_error_map.
+      destruct nth_error => //.
+    + solve_all. bool.
+      * destruct (dbody x) => //.
+      * set (rm := rev_map _ _).
+        specialize (a Γ0 Γ' (rm ++ Γ'') (dbody x)).
+        rewrite -!app_assoc in a. len in a.
+        rewrite /rm !rev_map_spec in H0 a *; len in a. len. eapply a; trea; rewrite map_map_compose //=.
+    + solve_all.
+  - rewrite lift_mkApps /=.
+    rewrite isEtaExp_mkApps //=; case: Nat.leb_spec => //= hn; bool; solve_all.
+    + move: H1.
+      destruct (PCUICLiftSubst.nth_error_appP Γ'' Γ0 n) => //= /Nat.leb_le hx.
+      * do 2 (rewrite nth_error_app_ge; [lia|]). lia.
+      * do 2 (rewrite nth_error_app_ge; [lia|]).
+      replace (#|Γ'| + n - #|Γ''| - #|Γ'|) with (n - #|Γ''|) by lia.
+      rewrite e //=. now apply Nat.leb_le.
+    + move: H1.
+      rewrite !nth_error_app_lt //=.
+  - rewrite lift_mkApps.
+    destruct (expanded_head_viewc u) => //.
+    bool.
+    eapply isEtaExp_mkApps_intro; eauto. solve_all.
 Qed.

erasure/theories/Typed/OptimizeCorrectness.v

@@ -2877,6 +2877,21 @@ Proof.
   now apply valid_cases_subst.
 Qed.
 
+Lemma isEtaExp_dearg_lambdas Σ Γ mask t :
+  isEtaExp Σ Γ t ->
+  isEtaExp Σ Γ (dearg_lambdas mask t).
+Proof.
+  intros valid.
+  induction t in Γ, mask, valid |- * using term_forall_list_ind; cbn in *; try easy.
+  - simp_eta in valid.
+    destruct mask as [|[] mask]; try easy.
+    + now simp_eta.
+    + cbn. unfold subst1. rewrite <- closed_subst; try easy.
+      eapply (isEtaExp_substl _ [0] _ [_]); easy.
+    + simp_eta. now eapply IHt.
+  - simp_eta. simp_eta in valid. rtoProp; intuition eauto.
+Qed.
+
 Lemma dearg_dearg_lambdas mask t :
   valid_dearg_mask mask t ->
   valid_cases t ->
@@ -3083,8 +3098,6 @@ Ltac facts :=
        assert (is_expanded v) by (unshelve eapply (eval_is_expanded_aux _ _ _ 0 _ H); trivial)
      end).
 
-Ltac bool := rtoProp; intuition eauto.
-
 Lemma count_zeros_le : forall mask, count_zeros mask <= #|mask|.
 Proof.
   induction mask;cbn;auto. destruct a;cbn; unfold count_zeros in *; lia.
@@ -3146,11 +3159,6 @@ Import EEtaExpandedFix.
 
 Hint Resolve dearg_elim : core.
 
-Lemma isEtaExp_lift Σ Γ Γ' t : isEtaExp Σ Γ t -> isEtaExp Σ (Γ' ++ Γ) (lift0 #|Γ'| t).
-Proof using.
-  todo "lift".
-Qed.
-
 Lemma isEtaExp_dearg_single Σ Γ t m l :
   isEtaExp Σ Γ t ->
   forallb (isEtaExp Σ Γ) l ->
@@ -3159,14 +3167,15 @@ Proof.
   induction m in Γ, l, t |- *; intros etat etal.
   - cbn. eapply isEtaExp_mkApps_intro; solve_all.
   - cbn. destruct a; destruct l; simp_eta; eauto. eapply IHm; eauto.
-    now eapply (isEtaExp_lift _ _ [_]).
+    now eapply (isEtaExp_lift _ _ [_] []).
     eapply IHm; eauto. now move/andP: etal.
     eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]).
-    now eapply (isEtaExp_lift _ _ [_]). constructor; eauto. simp_eta.
+    now eapply (isEtaExp_lift _ _ [_] []). constructor; eauto. simp_eta.
     eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]); eauto. constructor; eauto.
     all:now move/andP: etal.
 Qed.
 
+Unset Strict Universe Declaration.
 Section dearg.
   Context {wfl : WcbvFlags}.
   Context (n : nat).
@@ -3296,7 +3305,7 @@ Section dearg.
         clear IHev1 IHev2 IHev3.
         revert ev3 ev_len.
         cbn in *.
-        rewrite !closed_subst; [|now apply closedn_dearg_aux|easy].
+        rewrite !closed_subst; eauto. 2:now apply closedn_dearg_aux.
         intros.
         rewrite <- (dearg_subst [a']) by easy.
         unshelve eapply (IH _ _ _ _ _ ev3)...
@@ -3910,12 +3919,13 @@ Proof.
     intros n []; rewrite /trans_oib /dearg_oib //= /wf_inductive /wf_projections /=.
     rewrite /check_oib_masks /=.
     destruct ind_projs => //=; rewrite ?masked_nil //=.
-    move=> [] hl; apply eqb_eq in hl.
+    move=> [] /andP[] hcs /Nat.eqb_eq hps.
     destruct ind_ctors => //=. destruct ind_ctors => //=. len.
+    intros h % eqb_eq.
     destruct map eqn:hm; destruct p0 as [[pn pars] k] => //=.
-    intros h % eqb_eq. subst k.
+    cbn in h. subst k.
     rewrite masked_length. now (cbn; lia).
-    cbn. rewrite hl.
+    cbn. rewrite hps.
     apply/Nat.eqb_spec.
     pose proof (count_ones_zeros (get_branch_mask m0 n 0)). lia.
   - now destruct o; cbn.
@@ -3955,19 +3965,25 @@ Qed.
 Section EtaFix.
   Import EEtaExpandedFix.
   Lemma expanded_dearg_env (efl := all_env_flags) Σ :
-    (* valid_masks_env Σ -> *)
+    valid_masks_env Σ ->
     expanded_global_env (trans_env Σ) ->
     expanded_global_env (trans_env (dearg_env Σ)).
   Proof.
-    induction Σ; intros exp; depelim exp.
+    induction Σ; intros vm exp; depelim exp.
     - constructor.
-    - cbn. constructor; eauto. now apply IHΣ.
+    - cbn in *. constructor; eauto. move/andP: vm => [] va vΣ. now apply IHΣ.
       destruct a as [[kn ?] []]; cbn => //.
       + destruct c as [? []]; cbn => //.
         cbn in H.
+        move/andP: vm => [] /andP[] vdm vc vΣ.
+        eapply expanded_isEtaExp in H.
+        eapply isEtaExp_expanded.
+        eapply expanded_dearg; eauto.
+        now eapply valid_cases_dearg_lambdas.
+        now eapply isEtaExp_dearg_lambdas.
       + destruct o; cbn; constructor.
-
-
+  Qed.
+End EtaFix.
 
 Unset SsrRewrite.
 
@@ -4009,21 +4025,6 @@ Proof.
     f_equal; apply IH.
 Qed.
 
-Lemma filter_length {X} (f : X -> bool) (xs : list X) :
-  #|filter f xs| <= #|xs|.
-Proof.
-  induction xs; [easy|].
-  cbn.
-  destruct (f a); cbn; lia.
-Qed.
-
-Lemma map_repeat {X Y} (f : X -> Y) x n :
-  map f (repeat x n) = repeat (f x) n.
-Proof.
-  induction n; [easy|].
-  now cbn; rewrite IHn.
-Qed.
-
 Lemma nth_error_masked {X} m (xs : list X) n :
   nth n m false = false ->
   nth_error (masked m xs) (n - count_ones (firstn n m)) =

pcuic/theories/PCUICEtaExpand.v

@@ -233,6 +233,7 @@ Inductive expanded_global_declarations (univs : ContextSet.t) retro : forall (Σ
 | expanded_global_cons decl Σ : expanded_global_declarations univs retro Σ ->
   expanded_decl {| universes := univs; declarations := Σ; retroknowledge := retro |} decl.2 ->
   expanded_global_declarations univs retro (decl :: Σ).
+Derive Signature for expanded_global_declarations.
 
 Definition expanded_global_env (g : global_env) :=
   expanded_global_declarations g.(universes) g.(retroknowledge) g.(declarations).

utils/theories/MCList.v

@@ -1447,6 +1447,14 @@ Proof.
   induction n; cbn; congruence.
 Qed.
 
+Lemma filter_length {X} (f : X -> bool) (xs : list X) :
+  #|filter f xs| <= #|xs|.
+Proof.
+  induction xs; [easy|].
+  cbn.
+  destruct (f a); cbn; lia.
+Qed.
+
 Lemma map2_length :
   forall {A B C : Type} (f : A -> B -> C) (l : list A) (l' : list B), #| map2 f l l'| = min #|l| #|l'|.
 Proof.
@@ -1503,8 +1511,8 @@ Proof.
   { move => [->|[n H]]; [ exists 0 | exists (S n) ];
             rewrite ?skipn_0 ?skipn_S => //=. }
 Qed.
-  
+
 Lemma nth_error_firstn A n m (l:list A) x : nth_error (firstn n l) m = Some x -> nth_error l m = Some x.
 Proof.
   revert n l. induction m; intros n l H; destruct n, l; cbn in *; try solve [inversion H]; eauto.
-Qed. 
+Qed.

utils/theories/MCUtils.v

@@ -147,6 +147,7 @@ Ltac rtoProp :=
   | |- context [is_true (_ && _)] => rewrite andb_and
   end.
 
+Ltac bool := rtoProp; intuition eauto.
 
 Class Fuel := fuel : nat.