linearize case

erasure-plugin/theories/ETransform.v

@@ -567,7 +567,7 @@ Qed.
 From MetaCoq.Erasure Require Import EImplementBox.
 
 Program Definition implement_box_transformation {efl : EEnvFlags}
-  {has_app : has_tApp} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
+  {has_app : has_tApp} {has_letin : has_tLetIn} {has_cofix : has_tCoFix = false} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
   Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
   {| name := "transforming to constuctors as blocks";
     transform p _ := EImplementBox.implement_box_program p ;
@@ -577,7 +577,7 @@ Program Definition implement_box_transformation {efl : EEnvFlags}
 
 Next Obligation.
   intros. cbn in *. destruct p. split.
-  - eapply implement_box_env_wf_glob; eauto.
+  - eapply implement_box_env_wf_glob; eauto.   
   - now eapply transform_wellformed'.
 Qed.
 Next Obligation.
@@ -588,11 +588,12 @@ Next Obligation.
 Qed.
 
 #[global]
-Instance implement_box_extends (efl : EEnvFlags) {has_app : has_tApp} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
-   TransformExt.t (implement_box_transformation (has_app := has_app) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks)) extends_eprogram extends_eprogram.
+Instance implement_box_extends (efl : EEnvFlags) {has_app : has_tApp} {has_letin : has_tLetIn} {has_cofix : has_tCoFix = false} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
+   TransformExt.t (implement_box_transformation (has_app := has_app) (has_letin := has_letin) (has_cofix := has_cofix) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks)) extends_eprogram extends_eprogram.
 Proof.
   red. intros p p' pr pr' [ext eq]. rewrite /transform /= /implement_box_program /=.
   split => /=.
   eapply (implement_box_env_extends has_app ext). apply pr. apply pr'.
   now rewrite -eq.
 Qed.
+

erasure/theories/EImplementBox.v

@@ -40,8 +40,9 @@ Section implement_box.
     | tApp u v := tApp (implement_box u) (implement_box v)
     | tLetIn na b b' => EAst.tLetIn na (implement_box b) (implement_box b')
     | tCase ind c brs =>
-      let brs' := map_InP brs (fun x H => (x.1, implement_box x.2)) in
-      EAst.tCase (ind.1, 0) (implement_box c) brs'
+      let brs' := map_InP brs (fun x H => (x.1, lift 1 #|x.1| (implement_box x.2))) in
+      EAst.tLetIn (nNamed "discr") (implement_box c)
+      (EAst.tCase (ind.1, 0) (tRel 0) brs')
     | tProj p c => EAst.tProj {| proj_ind := p.(proj_ind); proj_npars := 0; proj_arg := p.(proj_arg) |} (implement_box c)
     | tFix mfix idx =>
       let mfix' := map_InP mfix (fun d H => {| dname := dname d; dbody := implement_box d.(dbody); rarg := d.(rarg) |}) in
@@ -93,44 +94,120 @@ Section implement_box.
     unfold test_def in *;
     simpl closed in *;
     try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
+    rtoProp. split. eauto.
+    solve_all.
+    replace (#|x.1| + S k) with (#|x.1| + k + 1) by lia.
+    eapply closedn_lift. eauto.
   Qed.
 
   Hint Rewrite @forallb_InP_spec : isEtaExp.
   Transparent isEtaExp_unfold_clause_1.
 
+  Lemma implement_box_lift a k b :
+    implement_box (lift a k b) = lift a k (implement_box b).
+  Proof.
+    revert k.
+    funelim (implement_box b); intros k; cbn; simp implement_box; try easy.
+    - destruct (Nat.leb_spec k i); reflexivity.
+    - f_equal. rewrite !map_map_compose. solve_all.
+      eapply In_All. eauto.
+    - cbn. f_equal. rewrite !map_map. solve_all.
+      eapply In_All. intros. eapply H; eauto.
+    - cbn. do 2 f_equal. 1: eauto.
+      rewrite !map_map. solve_all.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal.
+      replace (#|x.1| + S k) with (S (#|x.1| + k)) by lia.
+      erewrite H; eauto.
+      rewrite permute_lift. lia.
+      f_equal. lia.
+    - cbn. f_equal. rewrite !map_map. solve_all.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
+      f_equal. now rewrite map_length.
+    - cbn. f_equal. rewrite !map_map. solve_all.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
+      f_equal. now rewrite map_length.
+  Qed.
+
+  (* Lemma implement_box_subst a k b : *)
+  (*   implement_box (subst a k b) = subst (map implement_box a) k (implement_box b). *)
+  (* Proof using Type. *)
+  (*   revert k. *)
+  (*   funelim (implement_box b); intros k; cbn; simp implement_box; try easy. *)
+  (*   all: try now (cbn; f_equal; eauto). *)
+  (*   - destruct (Nat.leb_spec k i). *)
+  (*     + erewrite nth_error_map. *)
+  (*       destruct nth_error; cbn. *)
+  (*       * now rewrite implement_box_lift. *)
+  (*       * len. *)
+  (*     + reflexivity. *)
+  (*   - f_equal. rewrite !map_map_compose. solve_all. *)
+  (*     eapply In_All. eauto. *)
+  (*   - cbn. f_equal. rewrite !map_map. solve_all. *)
+  (*     eapply In_All. intros. eapply H; eauto. *)
+  (*   - cbn. do 2 f_equal. 1: eauto. *)
+  (*     rewrite !map_map. solve_all. *)
+  (*     eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. *)
+  (*     replace (#|x.1| + S k) with (S (#|x.1| + k)) by lia. *)
+  (*     rewrite commut_lift_subst. *)
+  (*     f_equal. *)
+  (*     eapply H; eauto. *)
+  (*   - cbn. f_equal. rewrite !map_map. solve_all. *)
+  (*     eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. *)
+  (*     f_equal. now rewrite map_length. *)
+  (*   - cbn. f_equal. rewrite !map_map. solve_all. *)
+  (*     eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto. *)
+  (*     f_equal. now rewrite map_length. *)
+  (* Qed. *)
+
   Lemma implement_box_csubst a k b :
+    closed a ->
     implement_box (ECSubst.csubst a k b) = ECSubst.csubst (implement_box a) k (implement_box b).
   Proof using Type.
-    revert a k.
-    funelim (implement_box b); intros a k; cbn; simp implement_box; try easy.
+    intros Ha.
+    revert k.
+    funelim (implement_box b); intros k; cbn; simp implement_box; try easy.
+    all: try now (cbn; f_equal; eauto).
     - destruct Nat.compare => //.
     - f_equal. rewrite !map_map_compose. solve_all.
       eapply In_All. eauto.
     - cbn. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto.
-    - cbn. rewrite H0. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. cbn. intros ? ?. f_equal. rewrite H; eauto.
+      eapply In_All. intros. eapply H; eauto.
+    - cbn. do 2 f_equal. 1: eauto.
+      rewrite !map_map. solve_all.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal.
+      setoid_rewrite -> closed_subst at 2.  
+      replace (#|x.1| + S k) with ((#|x.1| + k) + 1) by lia.
+      rewrite <- commut_lift_subst_rec. 2: lia.
+      rewrite <- closed_subst.
+      2, 3: eapply closed_implement_box; eauto.
+      f_equal.
+      eapply H; eauto.
     - cbn. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
       f_equal. now rewrite map_length.
     - cbn. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
       f_equal. now rewrite map_length.
   Qed.
 
   Lemma implement_box_substl s t :
+    All (fun x => closed x) s ->
     implement_box (substl s t) = substl (map implement_box s) (implement_box t).
   Proof using Type.
-    induction s in t |- *; simpl; auto.
-    rewrite IHs //. f_equal.
+    induction s in t |- *; simpl; auto; intros Hall.
+    inversion Hall.
+    rewrite IHs //.
     now rewrite implement_box_csubst.
   Qed.
 
   Lemma implement_box_iota_red pars args br :
+    All (fun x => closed x) args ->
     implement_box (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map implement_box args) (on_snd implement_box br).
   Proof using Type.
+    intros Hall.
     unfold EGlobalEnv.iota_red.
     rewrite implement_box_substl //.
+    solve_all. now eapply All_skipn.
     now rewrite map_rev map_skipn.
   Qed.
 
@@ -153,9 +230,11 @@ Section implement_box.
   Qed.
 
   Lemma implement_box_cunfold_fix mfix idx n f :
+    All (λ x : term, closed x) (fix_subst mfix) ->
     cunfold_fix mfix idx = Some (n, f) ->
     cunfold_fix (map (map_def implement_box) mfix) idx = Some (n, implement_box f).
   Proof using Type.
+    intros Hcl.
     unfold cunfold_fix.
     rewrite nth_error_map.
     destruct nth_error eqn:heq.
@@ -165,13 +244,15 @@ Section implement_box.
   Qed.
 
   Lemma implement_box_cunfold_cofix mfix idx n f :
+    All (λ x : term, closed x) (cofix_subst mfix) ->
     cunfold_cofix mfix idx = Some (n, f) ->
     cunfold_cofix (map (map_def implement_box) mfix) idx = Some (n, implement_box f).
   Proof using Type.
+    intros Hcl.
     unfold cunfold_cofix.
     rewrite nth_error_map.
     destruct nth_error eqn:heq.
-    intros [= <- <-] => /=. f_equal.
+    intros [= <- <-] => /=. f_equal. 
     rewrite implement_box_substl //. 2:congruence.
     f_equal. f_equal. apply implement_box_cofix_subst.
   Qed.
@@ -364,12 +445,12 @@ Definition switch_off_box (efl : EEnvFlags) :=
   {|  has_axioms := efl.(has_axioms) ; has_cstr_params := efl.(has_cstr_params) ; term_switches := disable_box_term_flags efl.(term_switches) ; cstr_as_blocks := efl.(cstr_as_blocks) |}.
 
 Lemma transform_wellformed' {efl : EEnvFlags} {Σ : list (kername × global_decl)} n t :
-  has_tApp ->
+  has_tApp -> has_tLetIn ->
   wf_glob Σ ->
   @wellformed efl Σ n t ->
   @wellformed (switch_off_box efl) (implement_box_env Σ) n (implement_box t).
 Proof.
-  intros hasa.
+  intros hasa hasl.
   revert n. funelim (implement_box t); simp_eta; cbn -[implement_box
     lookup_inductive lookup_constructor lookup_constructor_pars_args
     GlobalContextMap.lookup_constructor_pars_args isEtaExp]; intros m Hwf Hw; rtoProp; try split; eauto.
@@ -383,6 +464,8 @@ Proof.
     + solve_all.
     + destruct block_args; cbn in *; eauto.
   - rewrite lookup_inductive_implement_box. intuition auto. solve_all.
+    replace (#|x.1| + S m) with ((#|x.1| + m) + 1) by lia.
+    eapply wellformed_lift. eauto.
   - rewrite lookup_constructor_implement_box. intuition auto.
   - unfold wf_fix in *. rtoProp. solve_all. solve_all. now eapply isLambda_implement_box.
   - unfold wf_fix in *. rtoProp. solve_all.
@@ -393,7 +476,7 @@ Proof.
 Qed.
 
 Lemma transform_wellformed_decl' {efl : EEnvFlags} {Σ : global_declarations} d :
-  has_tApp ->
+  has_tApp -> has_tLetIn ->
   wf_glob Σ ->
   @wf_global_decl efl Σ d ->
   @wf_global_decl (switch_off_box efl) (implement_box_env Σ) (implement_box_decl d).
@@ -412,10 +495,10 @@ Proof.
 Qed.
 
 Lemma implement_box_env_wf_glob {efl : EEnvFlags} {Σ : global_declarations} :
-  has_tApp ->
+  has_tApp -> has_tLetIn ->
   wf_glob (efl := efl) Σ -> wf_glob (efl := switch_off_box efl) (implement_box_env Σ).
 Proof.
-  intros hasapp wfg.
+  intros hasapp haslet wfg.
   assert (extends_prefix Σ Σ). now exists [].
   revert H wfg. generalize Σ at 2 3.
   induction Σ; cbn; constructor; auto.
@@ -472,13 +555,14 @@ Lemma implement_box_eval {efl : EEnvFlags} (fl := block_wcbv_flags) :
   with_constructor_as_block = true ->
   has_cstr_params = false ->
   has_tApp ->
+  has_tCoFix = false ->
   forall (Σ : global_declarations), @wf_glob efl Σ ->
   forall t t',
   @wellformed efl Σ 0 t ->
   EWcbvEval.eval Σ t t' ->
   @EWcbvEval.eval block_wcbv_flags (implement_box_env Σ) (implement_box t) (implement_box t').
 Proof.
-  intros cstrbl prms hasapp Σ wfΣ.
+  intros cstrbl prms hasapp hascofix Σ wfΣ.
   eapply
   (EWcbvEvalCstrsAsBlocksInd.eval_preserve_mkApps_ind fl cstrbl (efl := efl) Σ _
     (wellformed Σ) (Qpres := Qpreserves_wellformed efl _ wfΣ)) => //.
@@ -508,40 +592,49 @@ Proof.
     pose proof (Hcon := H1).
     rewrite /constructor_isprop_pars_decl in H1.
     destruct lookup_constructor as [[[]] | ] eqn:eqc; cbn in H1; invs H1.
+    eapply eval_zeta => //.
+    1: eauto. rewrite H8.
+    cbn [csubst Nat.compare].
     eapply eval_iota_block => //.
-    + cbn [fst]. eapply e0.
+    + eapply value_final. eapply eval_to_value; eauto.
     + unfold constructor_isprop_pars_decl.
       rewrite lookup_constructor_implement_box. cbn [fst].
-      rewrite eqc //= H7 //.
-    + now rewrite map_InP_spec nth_error_map H2; eauto.
+      rewrite eqc //= H7 //. rewrite H8.
+      reflexivity.
+    + rewrite !map_InP_spec.
+      rewrite map_map.
+      rewrite nth_error_map H2; eauto.
+      reflexivity.
+    + rewrite map_InP_spec. len.
     + rewrite map_InP_spec. len.
-    + rewrite H8. rewrite map_InP_spec. len.
-    + rewrite map_InP_spec. rewrite -implement_box_iota_red. now rewrite H8.
+    + rewrite map_InP_spec.
+      cbn [csubst].
+      cbn [fst snd].
+      rewrite closed_subst.
+      { eapply wellformed_closed in i2.
+        cbn in i2 |- *. solve_all.
+        now eapply closed_implement_box.
+      }
+      rewrite Nat.add_0_r.
+      rewrite simpl_subst_k. reflexivity.
+      rewrite -implement_box_iota_red.
+      2: eauto.
+      eapply wellformed_closed in i2.
+      cbn in i2.
+      solve_all.
   - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end.
     simp implement_box in *.
     eapply eval_fix' => //; eauto. rewrite map_InP_spec.
-    now eapply implement_box_cunfold_fix.
+    eapply implement_box_cunfold_fix.
+    eapply forallb_All. eapply closed_fix_subst.
+    eapply wellformed_closed in i4.
+    now cbn in i4. eauto.
   - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end.
-    simp implement_box in *.
-    eapply eval_cofix_case.
-    2: now eapply implement_box_cunfold_cofix.
-    { rewrite implement_box_mkApps in e0.
-      simp implement_box in e0. rewrite map_InP_spec in e0.
-      cbn -[implement_box] in e0.
-      exact e0.
-    }
-    rewrite implement_box_mkApps in e.
-    simp implement_box in e.
+    rewrite wellformed_mkApps in i2. eauto.
+    cbn in i2. rtoProp. congruence.
   - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end.
-    simp implement_box in *.
-    eapply eval_cofix_proj.
-    2: now eapply implement_box_cunfold_cofix. { rewrite implement_box_mkApps in e0.
-      simp implement_box in e0. rewrite map_InP_spec in e0.
-      cbn -[implement_box] in e0.
-      exact e0.
-    }
-    rewrite implement_box_mkApps in e.
-    simp implement_box in e.
+    rewrite wellformed_mkApps in i2. eauto.
+    cbn in i2. rtoProp. congruence.
   - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end.
     simp implement_box in *.
     econstructor.

template-coq/theories/EtaExpand.v

@@ -102,8 +102,7 @@ Section Eta.
         in
         match nth_error def' i with
         | Some d => eta_fixpoint def' i d (map (eta_expand Γ) args)
-        | None => tVar ("Error: lookup of a fixpoint failed for "
-                          ++ string_of_term t)
+        | None => tVar ("Error: lookup of a fixpoint failed")
         end
       | tRel n =>
         match nth_error Γ n with
@@ -126,8 +125,7 @@ Section Eta.
                                         {| dname := dname d ; dtype := dtype d ; dbody := eta_expand (ctx ++  Γ) d.(dbody) ; rarg := rarg d |}) def) in
                       match nth_error def' i with
                       | Some d => eta_fixpoint def' i d []
-                      | None => tVar ("Error: lookup of a fixpoint failed for "
-                                       ++ string_of_term t)
+                      | None => tVar ("Error: lookup of a fixpoint failed ")
                       end
     | tCoFix def i => tCoFix (map (map_def id (eta_expand (repeat None (#|def|) ++ Γ))) def) i
     (* NOTE: we know that constructors and constants are not applied at this point,