From e233e8d9748bdd02a4f6ac620084f56cb80483d1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Tue, 19 Mar 2024 10:45:33 +0100
Subject: [PATCH] Implement tLazy and tForce in EAst (#1058)

* Add tLazy and tForce constructors

With no evaluation semantics yet. Use them in ECoInductiveToInductive to allow efficient (unverified) implementation of cofixpoints in target languages.

* Install archive file for static linking
---
 erasure/theories/EAst.v                       |   4 +-
 erasure/theories/EAstUtils.v                  |   4 +
 erasure/theories/ECSubst.v                    |   2 +
 erasure/theories/ECoInductiveToInductive.v    | 142 +++++-------------
 erasure/theories/EConstructorsAsBlocks.v      |   4 +-
 erasure/theories/EDeps.v                      |   6 +
 erasure/theories/EEtaExpanded.v               |  22 ++-
 erasure/theories/EEtaExpandedFix.v            |   8 +-
 erasure/theories/EImplementBox.v              |   5 +-
 erasure/theories/EInduction.v                 |  20 ++-
 erasure/theories/EInlineProjections.v         |   3 +
 erasure/theories/ELiftSubst.v                 |  12 +-
 erasure/theories/EOptimizePropDiscr.v         |   2 +
 erasure/theories/EPretty.v                    |   2 +
 erasure/theories/EReflect.v                   |   2 +
 erasure/theories/ERemoveParams.v              |   6 +-
 erasure/theories/ESpineView.v                 |   8 +-
 erasure/theories/EWcbvEval.v                  |   6 +
 .../EWcbvEvalCstrsAsBlocksFixLambdaInd.v      |   6 +-
 erasure/theories/EWcbvEvalCstrsAsBlocksInd.v  |   6 +-
 erasure/theories/EWcbvEvalEtaInd.v            |  62 +++++---
 erasure/theories/EWcbvEvalNamed.v             |  62 +++++++-
 erasure/theories/EWellformed.v                |   4 +
 erasure/theories/ErasureFunctionProperties.v  |   2 +
 erasure/theories/Typed/Optimize.v             |  10 ++
 erasure/theories/Typed/OptimizeCorrectness.v  |  20 +++
 erasure/theories/Typed/TypeAnnotations.v      |   2 +
 template-coq/Makefile.plugin.local-late       |   1 +
 28 files changed, 279 insertions(+), 154 deletions(-)
 create mode 100644 template-coq/Makefile.plugin.local-late

diff --git a/erasure/theories/EAst.v b/erasure/theories/EAst.v
index cd1eec17f..7620ba662 100644
--- a/erasure/theories/EAst.v
+++ b/erasure/theories/EAst.v
@@ -40,7 +40,9 @@ Inductive term : Set :=
 | tProj (p : projection) (c : term)
 | tFix (mfix : mfixpoint term) (idx : nat)
 | tCoFix (mfix : mfixpoint term) (idx : nat)
-| tPrim (prim : prim_val term).
+| tPrim (prim : prim_val term)
+| tLazy (t : term)
+| tForce (t : term).
 
 Derive NoConfusion for term.
 
diff --git a/erasure/theories/EAstUtils.v b/erasure/theories/EAstUtils.v
index ec9068a60..de7c2655c 100644
--- a/erasure/theories/EAstUtils.v
+++ b/erasure/theories/EAstUtils.v
@@ -374,6 +374,8 @@ Fixpoint string_of_term (t : term) : string :=
   | tFix l n => "Fix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")"
   | tCoFix l n => "CoFix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")"
   | tPrim p => "Prim(" ^ EPrimitive.string_of_prim string_of_term p ^ ")"
+  | tLazy t => "Lazy(" ^ string_of_term t ^ ")"
+  | tForce t => "Force(" ^ string_of_term t ^ ")"
   end.
 
 (** Compute all the global environment dependencies of the term *)
@@ -409,5 +411,7 @@ Fixpoint term_global_deps (t : term) :=
     KernameSet.union (KernameSet.singleton (inductive_mind p.(proj_ind)))
       (term_global_deps c)
   | tPrim p => prim_global_deps term_global_deps p
+  | tLazy t => term_global_deps t
+  | tForce t => term_global_deps t
   | _ => KernameSet.empty
   end.
\ No newline at end of file
diff --git a/erasure/theories/ECSubst.v b/erasure/theories/ECSubst.v
index e05deb65d..3cc2d2881 100644
--- a/erasure/theories/ECSubst.v
+++ b/erasure/theories/ECSubst.v
@@ -38,6 +38,8 @@ Fixpoint csubst t k u :=
     tCoFix mfix' idx
   | tConstruct ind n args => tConstruct ind n (map (csubst t k) args)
   | tPrim p => tPrim (map_prim (csubst t k) p)
+  | tLazy u => tLazy (csubst t k u)
+  | tForce u => tForce (csubst t k u)
   | x => x
   end.
 
diff --git a/erasure/theories/ECoInductiveToInductive.v b/erasure/theories/ECoInductiveToInductive.v
index 5aff66bce..485284539 100644
--- a/erasure/theories/ECoInductiveToInductive.v
+++ b/erasure/theories/ECoInductiveToInductive.v
@@ -33,43 +33,9 @@ Axiom trust_cofix : forall {A}, A.
 #[global]
 Hint Constructors eval : core.
 
-Module Thunk.
-  Definition make (t : term) : term :=
-    tLambda (nNamed "thunk") (lift 1 0 t).
-
-  Definition force (t : term) :=
-    tApp t tBox.
-
-  Definition make_name (x : string) (n : nat) : string :=
-    (x ++ string_of_nat n)%bs.
-
-  (* Thunk an n-ary function:
-     [t] is supposed to be of type T0 -> ... -> Tn -> C here
-     and we want to produce an expansion:
-     λ x0 .. xn (), t x0 xn () *)
-  Equations make_n_aux (n : nat) (t : term) (acc : list term) : term :=
-  make_n_aux 0 t acc => tLambda
-    (nNamed "thunk")
-    (mkApps (lift0 1 t) (rev (tRel 0 :: map (lift0 1) acc)));
-  make_n_aux (S n) t acc =>
-    tLambda
-      (nNamed (make_name "x" (S n)))
-      (make_n_aux n (lift0 1 t) (tRel 0 :: map (lift0 1) acc)).
-
-  Definition make_n (n : nat) (t : term) := make_n_aux n t [].
-
-  (* Eval compute in make_n 2 (tRel 0). *)
-
-End Thunk.
-
 Section trans.
   Context (Σ : GlobalContextMap.t).
 
-  Definition trans_cofix (d : def term) :=
-    {| dname := d.(dname);
-       dbody := Thunk.make_n d.(rarg) d.(dbody);
-       rarg := d.(rarg) |}.
-
   Fixpoint trans (t : term) : term :=
     match t with
     | tRel i => tRel i
@@ -81,12 +47,12 @@ Section trans.
       let brs' := List.map (on_snd trans) brs in
       match GlobalContextMap.lookup_inductive_kind Σ (fst ind).(inductive_mind) with
       | Some CoFinite =>
-        tCase ind (Thunk.force (trans c)) brs'
+        tCase ind (tForce (trans c)) brs'
       | _ => tCase ind (trans c) brs'
       end
     | tProj p c =>
       match GlobalContextMap.lookup_inductive_kind Σ p.(proj_ind).(inductive_mind) with
-      | Some CoFinite => tProj p (Thunk.force (trans c))
+      | Some CoFinite => tProj p (tForce (trans c))
       | _ => tProj p (trans c)
       end
     | tFix mfix idx =>
@@ -94,20 +60,18 @@ Section trans.
       tFix mfix' idx
     | tCoFix mfix idx =>
       let mfix' := List.map (map_def trans) mfix in
-      let mfix' := List.map trans_cofix mfix' in
-      match nth_error mfix' idx with
-      | Some d => Thunk.make_n d.(rarg) (tFix mfix' idx)
-      | None => tCoFix mfix' idx
-      end
+      tFix mfix' idx
     | tBox => t
     | tVar _ => t
     | tConst _ => t
     | tConstruct ind i args =>
       match GlobalContextMap.lookup_inductive_kind Σ ind.(inductive_mind) with
-      | Some CoFinite => Thunk.make (tConstruct ind i (map trans args))
+      | Some CoFinite => tLazy (tConstruct ind i (map trans args))
       | _ => tConstruct ind i (map trans args)
       end
     | tPrim p => tPrim (map_prim trans p)
+    | tLazy t => tLazy (trans t)
+    | tForce t => tForce (trans t)
     end.
 
   (* cofix succ x := match x with Stream x xs => Stream (x + 1) (succ xs) ->
@@ -160,14 +124,9 @@ Section trans.
     unfold test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; solve_all.
-      rewrite -Nat.add_1_r. now eapply closedn_lift.
     - move/andP: H => [] clt clargs.
       destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all.
-    - solve_all. destruct nth_error eqn:hnth.
-      * apply trust_cofix.
-      * cbn. unfold trans_cofix. len. solve_all.
-        unfold test_def. cbn. apply trust_cofix.
     - primProp. solve_all_k 6.
   Qed.
 
@@ -219,25 +178,13 @@ Section trans.
     - destruct (k ?= n)%nat; auto.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //.
       1,3,4:f_equal; rewrite map_map_compose; solve_all.
-      unfold Thunk.make. f_equal. cbn.
-      rewrite !map_map_compose. f_equal; solve_all.
-      specialize (H k cl). rewrite H.
-      rewrite closed_subst. now apply closed_trans.
-      rewrite closed_subst. now apply closed_trans.
-      now rewrite commut_lift_subst_rec.
+      do 2 f_equal; solve_all.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //.
       all:f_equal; eauto; try (rewrite /on_snd map_map_compose; solve_all).
-      unfold Thunk.force. f_equal; eauto.
+      f_equal. eauto.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //.
       all:f_equal; eauto; try (rewrite /on_snd map_map_compose; solve_all).
-      unfold Thunk.force. f_equal; eauto.
-    - f_equal. solve_all.
-      rewrite !nth_error_map. destruct nth_error eqn:hnth => //=.
-      2:{ f_equal. rewrite map_map_compose. eapply map_ext_in => x hin.
-          rewrite /trans_cofix /map_def //=. f_equal. len.
-          rewrite /Thunk.make_n. apply trust_cofix.
-      }
-      apply trust_cofix.
+      f_equal; eauto.
   Qed.
 
   Lemma trans_substl s t :
@@ -284,11 +231,11 @@ Section trans.
     discriminate.
   Qed.
 
-  Lemma trans_cunfold_cofix mfix idx n f :
+  (* Lemma trans_cunfold_cofix mfix idx n f :
     forallb (closedn 0) (EGlobalEnv.cofix_subst mfix) ->
     cunfold_cofix mfix idx = Some (n, f) ->
     exists d, nth_error mfix idx = Some d /\
-      cunfold_fix (map trans_cofix mfix) idx = Some (n, substl (fix_subst (map trans_cofix mfix)) (Thunk.make_n (rarg d) (dbody d))).
+      cunfold_fix mfix idx = Some (n, substl (fix_subst mfix) (dbody d)).
   Proof using Type.
     intros hcofix.
     unfold cunfold_cofix, cunfold_fix.
@@ -296,7 +243,7 @@ Section trans.
     destruct nth_error.
     intros [= <- <-] => /=. f_equal. exists d. split => //.
     discriminate.
-  Qed.
+  Qed. *)
 
   Lemma trans_nth {n l d} :
     trans (nth n l d) = nth n (map trans l) (trans d).
@@ -450,7 +397,6 @@ Proof.
     unfold lookup_inductive in hl.
     destruct lookup_minductive => //.
     rewrite (IHt _ H2 _ H0 H1) //.
-  - apply trust_cofix.
 Qed.
 
 Lemma wellformed_trans_decl_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t :
@@ -611,11 +557,6 @@ Proof.
   exists mdecl, idecl; split => //.
 Qed.
 
-Lemma isLambda_make_n n t : isLambda (Thunk.make_n n t).
-Proof.
-  induction n; cbn => //.
-Qed.
-
 Lemma value_trans {efl : EEnvFlags} {fl : WcbvFlags} {hasc : cstr_as_blocks = true} {wcon : with_constructor_as_block = true} {Σ : GlobalContextMap.t} {c} :
   has_tApp -> wf_glob Σ ->
   wellformed Σ 0 c ->
@@ -628,11 +569,6 @@ Proof.
     all:try solve [intros; repeat constructor => //].
     destruct args => //.
     move=> /andP[] wc. now rewrite wcon in wc.
-    move=> _ /andP [] hascof /andP[] /Nat.ltb_lt /nth_error_Some hnth hm.
-    destruct nth_error => //.
-    pose proof (isLambda_make_n (rarg d) (tFix (map trans_cofix mfix) idx)).
-    destruct Thunk.make_n => //. apply trust_cofix.
-    (* do 3 constructor. *)
   - intros p pv IH wf. cbn. constructor. constructor 2.
     cbn in wf. move/andP: wf => [hasp tp].
     primProp. depelim tp; depelim pv; depelim IH; constructor; cbn in *; rtoProp; intuition auto; solve_all.
@@ -641,7 +577,8 @@ Proof.
     cbn -[GlobalContextMap.lookup_inductive_kind].
     destruct GlobalContextMap.lookup_inductive_kind as [[]|] eqn:hl' => //.
     1,3,4:eapply value_constructor; tea; [erewrite <-lookup_constructor_trans; tea|now len|solve_all].
-    now do 2 constructor.
+    apply trust_cofix.
+    (* now do 2 constructor. *)
   - intros f args vh harglen hargs ihargs.
     rewrite wellformed_mkApps // => /andP[] wff wfargs.
     rewrite trans_mkApps.
@@ -669,6 +606,7 @@ Ltac destruct_times :=
 From MetaCoq.Erasure Require Import EWcbvEvalCstrsAsBlocksInd.
 Lemma trans_correct {efl : EEnvFlags} {fl} {wcon : with_constructor_as_block = true}
   {wcb : cstr_as_blocks = true}
+  {wpc : with_prop_case = false} (* Avoid tLazy tBox values *)
   {Σ : GlobalContextMap.t} t v :
   has_tApp ->
   wf_glob Σ ->
@@ -712,7 +650,8 @@ Proof.
     1,3,4: eauto.
     + now rewrite -is_propositional_cstr_trans.
     + rewrite nth_error_map H2 //.
-    + eapply eval_beta. eapply e0; eauto.
+    + eapply trust_cofix.
+      (* eapply eval_beta. eapply e0; eauto.
       constructor; eauto.
       rewrite closed_subst // simpl_subst_k //.
       eapply EWcbvEval.eval_to_value in H.
@@ -724,27 +663,19 @@ Proof.
       instantiate (1 := map (trans Σ) args).
       eapply All2_All2_Set.
       eapply values_final. solve_all.
-      unshelve eapply value_trans; tea.
+      unshelve eapply value_trans; tea.*)
     + now len.
     + now len.
-    + exact e.
+    + apply trust_cofix.
 
-  - subst brs.
-    cbn -[lookup_constructor lookup_constructor_pars_args
-      GlobalContextMap.lookup_inductive_kind] in e0 |- *.
-    rewrite GlobalContextMap.lookup_inductive_kind_spec.
-    rewrite trans_substl ?map_repeat /= in e.
-    { now apply forallb_repeat. }
-    destruct lookup_inductive_kind as [[]|] eqn:hl => //.
-    1,3,4:eapply eval_iota_sing; [eauto|eauto|
-        now rewrite -is_propositional_trans|reflexivity|
-        rewrite /= ?trans_substl //; simpl; eauto].
-    eapply eval_iota_sing; eauto.
-    eapply eval_box; eauto.
-    rewrite -is_propositional_trans //.
-    reflexivity.
+  - now rewrite H in wpc.
 
   - apply trust_cofix.
+    (*rewrite trans_mkApps /= in e1.
+    cbn; eapply eval_fix => //; tea.
+    len. apply trust_cofix*)
+
+
   - apply trust_cofix.
   - apply trust_cofix.
   - apply trust_cofix.
@@ -910,13 +841,22 @@ Proof.
     destruct lookup_inductive_kind as [[]|] => /= //.
     2-3:constructor; eauto; solve_all.
     constructor; eauto; solve_all. cbn.
-    unfold Thunk.force.
-    eapply isEtaExp_expanded.
-    all:apply trust_cofix.
-  - apply trust_cofix.
-  - apply trust_cofix.
-  - apply trust_cofix.
-  - apply trust_cofix.
+    now constructor.
+    constructor; eauto; solve_all.
+  - cbn -[GlobalContextMap.lookup_inductive_kind].
+    rewrite GlobalContextMap.lookup_inductive_kind_spec.
+    destruct lookup_inductive_kind as [[]|] => /= //.
+    2-3:constructor; eauto; solve_all.
+    constructor; eauto; solve_all. cbn.
+    now constructor.
+    constructor; eauto; solve_all.
+  - cbn. econstructor; eauto. solve_all. now eapply isLambda_trans.
+  - cbn. econstructor; eauto; solve_all. apply trust_cofix.
+  - cbn -[GlobalContextMap.lookup_inductive_kind].
+    rewrite GlobalContextMap.lookup_inductive_kind_spec.
+    destruct lookup_inductive_kind as [[]|] => /= //.
+    1,3,4:eapply expanded_tConstruct_app; eauto; solve_all.
+    apply trust_cofix. (* Needs constructor_as_blocks = true invariant *)
 Qed.
     (*cbn.
     eapply isEtaExp_substl. eapply forallb_repeat => //.
diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
index a3073e9e3..b563e8a7a 100644
--- a/erasure/theories/EConstructorsAsBlocks.v
+++ b/erasure/theories/EConstructorsAsBlocks.v
@@ -62,7 +62,9 @@ Section transform_blocks.
     | tVar n => EAst.tVar n
     | tConst n => EAst.tConst n
     | tConstruct ind i block_args => EAst.tConstruct ind i []
-    | tPrim p => EAst.tPrim (map_primIn p (fun x H => transform_blocks x)) }.
+    | tPrim p => EAst.tPrim (map_primIn p (fun x H => transform_blocks x))
+    | tLazy t => EAst.tLazy (transform_blocks t)
+    | tForce t => EAst.tForce (transform_blocks t) }.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v
index 88a9d7716..b1180b5cc 100644
--- a/erasure/theories/EDeps.v
+++ b/erasure/theories/EDeps.v
@@ -86,6 +86,8 @@ Proof.
     now apply e.
   - depelim X; depelim er; constructor; cbn. solve_all.
     destruct p. solve_all.
+  - depelim er.
+  - depelim er.
 Qed.
 
 Lemma erases_deps_subst Σ Σ' s k t :
@@ -137,6 +139,8 @@ Proof.
     constructor; [|easy].
     now apply e.
   - depelim X; depelim er; constructor; cbn; intuition auto; solve_all.
+  - depelim er.
+  - depelim er.
 Qed.
 
 Lemma erases_deps_subst1 Σ Σ' t k u :
@@ -195,6 +199,8 @@ Proof.
     constructor; [|easy].
     now apply e.
   - depelim X; depelim er; constructor; cbn; intuition auto; solve_all.
+  - depelim er.
+  - depelim er.
 Qed.
 
 Lemma erases_deps_substl Σ Σ' s t :
diff --git a/erasure/theories/EEtaExpanded.v b/erasure/theories/EEtaExpanded.v
index 3bf7c7954..6599720d2 100644
--- a/erasure/theories/EEtaExpanded.v
+++ b/erasure/theories/EEtaExpanded.v
@@ -76,6 +76,8 @@ Section isEtaExp.
     | tVar _ => true
     | tConst _ => true
     | tPrim p => test_primIn p (fun x H => isEtaExp x)
+    | tLazy t => isEtaExp t
+    | tForce t => isEtaExp t
     | tConstruct ind i block_args => isEtaExp_app ind i 0 && is_nil block_args }.
   Proof.
     all:try lia.
@@ -474,6 +476,8 @@ Inductive expanded : term -> Prop :=
     Forall expanded args ->
     expanded (mkApps (tConstruct ind idx []) args)
 | expanded_tPrim p : primProp@{Set Set} expanded p -> expanded (tPrim p)
+| expanded_tLazy t : expanded t -> expanded (tLazy t)
+| expanded_tForce t : expanded t -> expanded (tForce t)
 | expanded_tBox : expanded tBox.
 
 End expanded.
@@ -513,19 +517,21 @@ forall (Σ : global_declarations) (P : term -> Prop),
  declared_constructor Σ (ind, idx) mind idecl cdecl ->
  #|args| >= cstr_arity mind cdecl -> Forall (expanded Σ) args -> Forall P args -> P (mkApps (tConstruct ind idx []) args)) ->
 (forall p, primProp (expanded Σ) p -> primProp P p -> P (tPrim p)) ->
+(forall t, expanded Σ t -> P t -> P (tLazy t)) ->
+(forall t, expanded Σ t -> P t -> P (tForce t)) ->
 (P tBox) ->
 forall t : term, expanded Σ t -> P t.
 Proof.
-  intros. revert t H13.
+  intros Σ P. intros hrel hvar hevar hlam hletin happ hconst hcase hproj hfix hcofix hcapp hprim hlazy hforce hbox.
   fix f 2.
   intros t Hexp. destruct Hexp; eauto.
-  - eapply H1; eauto. induction H13; econstructor; cbn in *; eauto.
-  - eapply H4; eauto. clear H14. induction H15; econstructor; cbn in *; eauto.
-  - eapply H6; eauto. induction H13; econstructor; cbn in *; eauto.
-  - eapply H8; eauto. induction H13; econstructor; cbn in *; intuition eauto.
-  - eapply H9; eauto. induction H13; econstructor; cbn in *; eauto.
-  - eapply H10; eauto. clear - H15 f. induction H15; econstructor; cbn in *; eauto.
-  - eapply H11; eauto.
+  - eapply hevar; eauto. induction H; econstructor; cbn in *; eauto.
+  - eapply happ; eauto. clear H0. induction H1; econstructor; cbn in *; eauto.
+  - eapply hcase; eauto. induction H; econstructor; cbn in *; eauto.
+  - eapply hfix; eauto. induction H; econstructor; cbn in *; intuition eauto.
+  - eapply hcofix; eauto. induction H; econstructor; cbn in *; eauto.
+  - eapply hcapp; eauto. clear - H1 f. induction H1; econstructor; cbn in *; eauto.
+  - eapply hprim; eauto.
     depelim X; constructor. destruct p; split; eauto.
     eapply (make_All_All f a0).
 Qed.
diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
index 46b839e2e..a094a3021 100644
--- a/erasure/theories/EEtaExpandedFix.v
+++ b/erasure/theories/EEtaExpandedFix.v
@@ -61,6 +61,8 @@ Inductive expanded (Γ : list nat): term -> Prop :=
     Forall (expanded Γ) args ->
     expanded Γ (mkApps (tConstruct ind idx []) args)
 | expanded_tPrim p : primProp@{Set Set} (expanded Γ) p -> expanded Γ (tPrim p)
+| expanded_tLazy t : expanded Γ t -> expanded Γ (tLazy t)
+| expanded_tForce t : expanded Γ t -> expanded Γ (tForce t)
 | expanded_tBox : expanded Γ tBox.
 
 End expanded.
@@ -139,10 +141,12 @@ Lemma expanded_ind :
         → Forall (P Γ) args
         → P Γ (mkApps (tConstruct ind idx []) args))
     → (∀ Γ p, primProp (expanded Σ Γ) p -> primProp (P Γ) p -> P Γ (tPrim p))
+    → (∀ Γ t, expanded Σ Γ t -> P Γ t -> P Γ (tLazy t))
+    → (∀ Γ t, expanded Σ Γ t -> P Γ t -> P Γ (tForce t))
     → (∀ Γ : list nat, P Γ tBox)
     → ∀ (Γ : list nat) (t : term), expanded Σ Γ t → P Γ t.
 Proof.
-  intros Σ P HRel_app HVar HEvar HLamdba HLetIn HmkApps HConst HCase HProj HFix HCoFix HConstruct HPrim HBox.
+  intros Σ P HRel_app HVar HEvar HLamdba HLetIn HmkApps HConst HCase HProj HFix HCoFix HConstruct HPrim HLazy HForce HBox.
   fix f 3.
   intros Γ t Hexp.  destruct Hexp; eauto.
   - eapply HRel_app; eauto. clear - f H0. induction H0; econstructor; eauto.
@@ -297,6 +301,8 @@ Section isEtaExp.
     | tVar _ => true
     | tConst _ => true
     | tPrim p => test_primIn p (fun x H => isEtaExp Γ x)
+    | tLazy t => isEtaExp Γ t
+    | tForce t => isEtaExp Γ t
     | tConstruct ind i block_args => isEtaExp_app ind i 0 && is_nil block_args }.
   Proof using Σ.
     all:try lia.
diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
index f6db6a82c..99deb0a5f 100644
--- a/erasure/theories/EImplementBox.v
+++ b/erasure/theories/EImplementBox.v
@@ -54,7 +54,9 @@ Section implement_box.
     | tVar n => EAst.tVar n
     | tConst n => EAst.tConst n
     | tConstruct ind i block_args => EAst.tConstruct ind i (map_InP block_args (fun d H => implement_box d))
-    | tPrim p => EAst.tPrim (map_primIn p (fun x H => implement_box x)).
+    | tPrim p => EAst.tPrim (map_primIn p (fun x H => implement_box x))
+    | tLazy t => EAst.tLazy (implement_box t)
+    | tForce t => EAst.tForce (implement_box t).
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
@@ -445,6 +447,7 @@ Definition disable_box_term_flags (et : ETermFlags) :=
     ; has_tFix := true
     ; has_tCoFix := has_tCoFix
     ; has_tPrim := has_tPrim
+    ; has_tLazy_Force := has_tLazy_Force
   |}.
 
 Definition switch_off_box (efl : EEnvFlags) :=
diff --git a/erasure/theories/EInduction.v b/erasure/theories/EInduction.v
index 306b6d25c..53d4d9bc0 100644
--- a/erasure/theories/EInduction.v
+++ b/erasure/theories/EInduction.v
@@ -35,6 +35,8 @@ Lemma term_forall_list_ind :
     (forall (m : mfixpoint term) (n : nat), All (fun x => P (dbody x)) m -> P (tFix m n)) ->
     (forall (m : mfixpoint term) (n : nat), All (fun x => P (dbody x)) m -> P (tCoFix m n)) ->
     (forall p, primProp P p -> P (tPrim p)) ->
+    (forall t, P t -> P (tLazy t)) ->
+    (forall t, P t -> P (tForce t)) ->
     forall t : term, P t.
 Proof.
   intros until t. revert t.
@@ -115,6 +117,8 @@ Fixpoint size (t : term) : nat :=
   | tCoFix mfix idx => S (list_size (fun x => size (dbody x)) mfix)
   | tConstruct _ _ ignore_args => S (list_size size ignore_args)
   | tPrim p => S (prim_size size p)
+  | tLazy t => S (size t)
+  | tForce t => S (size t)
   | _ => 1
   end.
 
@@ -239,7 +243,9 @@ Section MkApps_rec.
     (pproj : forall (s : projection) (t : term), P t -> P (tProj s t))
     (pfix : forall (m : mfixpoint term) (n : nat), All (fun x => P (dbody x)) m -> P (tFix m n))
     (pcofix : forall (m : mfixpoint term) (n : nat), All (fun x => P (dbody x)) m -> P (tCoFix m n))
-    (pprim : forall p, primProp P p -> P (tPrim p)).
+    (pprim : forall p, primProp P p -> P (tPrim p))
+    (plazy : forall t, P t -> P (tLazy t))
+    (pforce : forall t, P t -> P (tForce t)).
 
   Definition inspect {A} (x : A) : { y : A | x = y } := exist _ x eq_refl.
 
@@ -265,7 +271,9 @@ Section MkApps_rec.
     | tProj p c => pproj p c (rec c)
     | tFix mfix idx => pfix mfix idx (All_rec P dbody mfix (fun x H => rec x))
     | tCoFix mfix idx => pcofix mfix idx (All_rec P dbody mfix (fun x H => rec x))
-    | tPrim p => pprim p _.
+    | tPrim p => pprim p _
+    | tLazy t => plazy t (rec t)
+    | tForce t => pforce t (rec t).
   Proof.
     all:unfold MR; cbn; auto with arith. 4:lia.
     - clear -napp nonnil da rec.
@@ -303,7 +311,9 @@ Section MkApps_rec.
     (pproj : forall (s : projection) (t : term), P (tProj s t))
     (pfix : forall (m : mfixpoint term) (n : nat), P (tFix m n))
     (pcofix : forall (m : mfixpoint term) (n : nat), P (tCoFix m n))
-    (pprim : forall p, P (tPrim p)).
+    (pprim : forall p, P (tPrim p))
+    (plazy : forall t, P (tLazy t))
+    (pforce : forall t, P (tForce t)).
 
   Import EqNotations.
 
@@ -325,7 +335,9 @@ Section MkApps_rec.
     | tProj p c => pproj p c
     | tFix mfix idx => pfix mfix idx
     | tCoFix mfix idx => pcofix mfix idx
-    | tPrim p => pprim p.
+    | tPrim p => pprim p
+    | tLazy t => plazy t
+    | tForce t => pforce t.
 
   End MkApps_case.
 
diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v
index 1035e146a..a37b97ae7 100644
--- a/erasure/theories/EInlineProjections.v
+++ b/erasure/theories/EInlineProjections.v
@@ -49,6 +49,7 @@ Definition disable_projections_term_flags (et : ETermFlags) :=
     ; has_tFix := has_tFix
     ; has_tCoFix := has_tCoFix
     ; has_tPrim := has_tPrim
+    ; has_tLazy_Force := has_tLazy_Force
   |}.
 
 Definition disable_projections_env_flag (efl : EEnvFlags) :=
@@ -124,6 +125,8 @@ Section optimize.
     | tConst _ => t
     | tConstruct ind n args => tConstruct ind n (map optimize args)
     | tPrim p => tPrim (map_prim optimize p)
+    | tLazy t => tLazy (optimize t)
+    | tForce t => tForce (optimize t)
     end.
 
   Lemma optimize_mkApps f l : optimize (mkApps f l) = mkApps (optimize f) (map optimize l).
diff --git a/erasure/theories/ELiftSubst.v b/erasure/theories/ELiftSubst.v
index a03c221eb..40632fd9a 100644
--- a/erasure/theories/ELiftSubst.v
+++ b/erasure/theories/ELiftSubst.v
@@ -37,6 +37,8 @@ Fixpoint lift n k t : term :=
   | tConst _ => t
   | tConstruct ind i args => tConstruct ind i (map (lift n k) args)
   | tPrim p => tPrim (map_prim (lift n k) p)
+  | tLazy t => tLazy (lift n k t)
+  | tForce t => tForce (lift n k t)
   end.
 
 Notation lift0 n := (lift n 0).
@@ -72,7 +74,11 @@ Fixpoint subst s k u :=
     tCoFix mfix' idx
   | tConstruct ind i args => tConstruct ind i (map (subst s k) args)
   | tPrim p => tPrim (map_prim (subst s k) p)
-  | x => x
+  | tLazy t => tLazy (subst s k t)
+  | tForce t => tForce (subst s k t)
+  | tBox => tBox
+  | tVar n => tVar n
+  | tConst c => tConst c
   end.
 
 (** Substitutes [t1 ; .. ; tn] in u for [Rel 0; .. Rel (n-1)] *in parallel* *)
@@ -100,6 +106,8 @@ Fixpoint closedn k (t : term) : bool :=
     List.forallb (test_def (closedn k')) mfix
   | tConstruct ind i args => forallb (closedn k) args
   | tPrim p => test_prim (closedn k) p
+  | tLazy t => closedn k t
+  | tForce t => closedn k t
   | _ => true
   end.
 
@@ -634,6 +642,8 @@ Proof.
     intros. specialize (H (#|m| + k')).
     now rewrite !Nat.add_assoc !(Nat.add_comm k) in H |- *.
   - solve_all.
+  - solve_all.
+  - solve_all.
 Qed.
 
 Lemma closedn_subst s k t :
diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
index 673b9223e..211562f18 100644
--- a/erasure/theories/EOptimizePropDiscr.v
+++ b/erasure/theories/EOptimizePropDiscr.v
@@ -69,6 +69,8 @@ Section remove_match_on_box.
     | tConst _ => t
     | tConstruct ind i args => tConstruct ind i (map remove_match_on_box args)
     | tPrim p => tPrim (map_prim remove_match_on_box p)
+    | tLazy t => tLazy (remove_match_on_box t)
+    | tForce t => tForce (remove_match_on_box t)
     end.
 
   Lemma remove_match_on_box_mkApps f l : remove_match_on_box (mkApps f l) = mkApps (remove_match_on_box f) (map remove_match_on_box l).
diff --git a/erasure/theories/EPretty.v b/erasure/theories/EPretty.v
index 47324cd2d..97e6a2081 100644
--- a/erasure/theories/EPretty.v
+++ b/erasure/theories/EPretty.v
@@ -170,6 +170,8 @@ Module PrintTermTree.
       parens top ("let cofix " ^ print_defs print_term Γ l ^ nl ^
                                 " in " ^ List.nth_default (string_of_nat n) (map (string_of_name ∘ dname) l) n)
     | tPrim p => parens top (print_prim (print_term Γ false false) p)
+    | tLazy t => parens top ("lazy " ^ print_term Γ false false t)
+    | tForce t => parens top ("force " ^ print_term Γ false false t)
     end.
   End print_term.
 
diff --git a/erasure/theories/EReflect.v b/erasure/theories/EReflect.v
index 71284edc2..70bb89dc6 100644
--- a/erasure/theories/EReflect.v
+++ b/erasure/theories/EReflect.v
@@ -121,6 +121,8 @@ Proof.
       revert array_value; induction hv; intros []; eauto; nodec.
       destruct (p t); subst; nodec.
       destruct (IHhv l0); nodec. noconf e; eauto.
+  - destruct (IHx t); subst; nodec. now left.
+  - destruct (IHx t); subst; nodec. now left.
 Defined.
 
 #[global]
diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v
index f574e2893..c58d9e5d9 100644
--- a/erasure/theories/ERemoveParams.v
+++ b/erasure/theories/ERemoveParams.v
@@ -59,7 +59,9 @@ Section strip.
     | tVar n => EAst.tVar n
     | tConst n => EAst.tConst n
     | tConstruct ind i block_args => EAst.tConstruct ind i block_args
-    | tPrim p => EAst.tPrim (map_primIn p (fun x H => strip x)) }.
+    | tPrim p => EAst.tPrim (map_primIn p (fun x H => strip x))
+    | tLazy t => EAst.tLazy (strip t)
+    | tForce t => EAst.tForce (strip t) }.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
@@ -569,6 +571,8 @@ Module Fast.
     | app, tPrim (primFloat; primFloatModel f) => mkApps (tPrim (primFloat; primFloatModel f)) app
     | app, tPrim (primArray; primArrayModel a) =>
       mkApps (tPrim (primArray; primArrayModel {| array_default := strip [] a.(array_default); array_value := strip_args a.(array_value) |})) app
+    | app, tLazy t => mkApps (tLazy (strip [] t)) app
+    | app, tForce t => mkApps (tForce (strip [] t)) app
     | app, x => mkApps x app }
 
     where strip_args (t : list term) : list term :=
diff --git a/erasure/theories/ESpineView.v b/erasure/theories/ESpineView.v
index 6b5a58903..6278254eb 100644
--- a/erasure/theories/ESpineView.v
+++ b/erasure/theories/ESpineView.v
@@ -23,7 +23,9 @@ Inductive t : term -> Set :=
 | tProj p c : t (tProj p c)
 | tFix mfix idx : t (tFix mfix idx)
 | tCoFix mfix idx : t (tCoFix mfix idx)
-| tPrim p : t (tPrim p).
+| tPrim p : t (tPrim p)
+| tLazy p : t (tLazy p)
+| tForce p : t (tForce p).
 Derive Signature for t.
 
 Definition view : forall x : term, t x :=
@@ -39,7 +41,9 @@ Definition view : forall x : term, t x :=
     (fun p t => tProj p t)
     (fun mfix n => tFix mfix n)
     (fun mfix n => tCoFix mfix n)
-    (fun p => tPrim p).
+    (fun p => tPrim p)
+    tLazy
+    tForce.
 
 Lemma view_mkApps {f v} (vi : t (mkApps f v)) : ~~ isApp f -> v <> [] ->
   exists hf vn, vi = tApp f v hf vn.
diff --git a/erasure/theories/EWcbvEval.v b/erasure/theories/EWcbvEval.v
index d6ca6e787..7cd775a2a 100644
--- a/erasure/theories/EWcbvEval.v
+++ b/erasure/theories/EWcbvEval.v
@@ -272,6 +272,12 @@ Section Wcbv.
     eval_primitive eval p p' ->
     eval (tPrim p) (tPrim p')
 
+  (*
+  | eval_lazy : eval (tLazy t) (tLazy t)
+  | eval_force t v v' : eval t (tLazy v) ->
+    eval v v' ->
+    eval (tForce t) v' *)
+
   (** Atoms are values (includes abstractions, cofixpoints and constructors) *)
   | eval_atom t : atom Σ t -> eval t t.
 
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
index 86acd0804..dbc98f423 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
@@ -42,7 +42,9 @@ Section OnSubterm.
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
   | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
-  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p).
+  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p)
+  | on_lazy t : has_tLazy_Force -> Q n t -> on_subterms Q n (tLazy t)
+  | on_force t : has_tLazy_Force -> Q n t -> on_subterms Q n (tForce t).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -590,6 +592,8 @@ Proof.
     rtoProp; intuition auto.
     eapply on_cofix => //. move/andP: H0 => [] _ ha. solve_all.
     move/andP: H => [] hp ha. eapply on_prim => //. solve_all.
+    eapply on_lazy; rtoProp; intuition auto.
+    eapply on_force; rtoProp; intuition auto.
  - red. intros kn decl.
     move/(lookup_env_wellformed clΣ).
     unfold wf_global_decl. destruct cst_body => //.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
index 3949f4a54..36e726036 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
@@ -42,7 +42,9 @@ Section OnSubterm.
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
   | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
-  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p).
+  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p)
+  | on_lazy t : has_tLazy_Force -> Q n t -> on_subterms Q n (tLazy t)
+  | on_force t : has_tLazy_Force -> Q n t -> on_subterms Q n (tForce t).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -490,6 +492,8 @@ Proof.
     rtoProp; intuition auto.
     eapply on_cofix => //. move/andP: H0 => [] _ ha. solve_all.
     move/andP: H => [] hasp ht. eapply on_prim => //. solve_all.
+    eapply on_lazy; rtoProp; intuition auto.
+    eapply on_force; rtoProp; intuition auto.
   - red. intros kn decl.
     move/(lookup_env_wellformed clΣ).
     unfold wf_global_decl. destruct cst_body => //.
diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v
index 0f7f2cf38..6ed55b14a 100644
--- a/erasure/theories/EWcbvEvalEtaInd.v
+++ b/erasure/theories/EWcbvEvalEtaInd.v
@@ -42,7 +42,9 @@ Section OnSubterm.
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
   | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
-  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p).
+  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p)
+  | on_lazy t : has_tLazy_Force -> Q n t -> on_subterms Q n (tLazy t)
+  | on_force t : has_tLazy_Force -> Q n t -> on_subterms Q n (tForce t).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -322,6 +324,12 @@ Lemma eval_preserve_mkApps_ind :
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 
+  (* (forall t t', eval Σ t t' -> Q 0 t -> Q 0 t' -> P t t' ->
+    P' (tLazy t) (tLazy t')) ->
+
+  (forall t t', eval Σ t t' -> Q 0 t -> Q 0 t' -> P t t' ->
+    P' (tForce t) (tForce t')) -> *)
+
   (∀ t : term, atom Σ t → Q 0 t -> isEtaExp Σ t -> P' t t) ->
   ∀ (t t0 : term), Q 0 t -> isEtaExp Σ t -> eval Σ t t0 → P' t t0.
 Proof.
@@ -710,30 +718,6 @@ Proof.
  - intros ise. split => //. eapply Qatom; tea.
 Qed.
 
-Definition term_flags :=
-  {|
-    has_tBox := true;
-    has_tRel := true;
-    has_tVar := false;
-    has_tEvar := false;
-    has_tLambda := true;
-    has_tLetIn := true;
-    has_tApp := true;
-    has_tConst := true;
-    has_tConstruct := true;
-    has_tCase := true;
-    has_tProj := false;
-    has_tFix := true;
-    has_tCoFix := false;
-    has_tPrim := all_primitive_flags;
-  |}.
-
-Definition env_flags :=
-    {| has_axioms := false;
-       has_cstr_params := false;
-       term_switches := term_flags ;
-       cstr_as_blocks := false
-    |}.
 
 From MetaCoq.Erasure Require Import ELiftSubst.
 Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ :
@@ -757,6 +741,8 @@ Proof.
     eapply on_fix; eauto. move/andP: H0 => [] _ wf. solve_all.
     eapply on_cofix; eauto. move/andP: H0 => [] _ wf. solve_all.
     eapply on_prim; eauto. solve_all.
+    eapply on_lazy; eauto.
+    eapply on_force; eauto.
   - red. intros kn decl.
     move/(lookup_env_wellformed clΣ).
     unfold wf_global_decl. destruct cst_body => //.
@@ -780,6 +766,32 @@ Ltac destruct_nary_times :=
   | [ H : [× _, _, _, _ & _] |- _ ] => destruct H
   end.
 
+Definition term_flags :=
+  {|
+    has_tBox := true;
+    has_tRel := true;
+    has_tVar := false;
+    has_tEvar := false;
+    has_tLambda := true;
+    has_tLetIn := true;
+    has_tApp := true;
+    has_tConst := true;
+    has_tConstruct := true;
+    has_tCase := true;
+    has_tProj := false;
+    has_tFix := true;
+    has_tCoFix := false;
+    has_tPrim := all_primitive_flags;
+    has_tLazy_Force := false;
+  |}.
+
+Definition env_flags :=
+    {| has_axioms := false;
+        has_cstr_params := false;
+        term_switches := term_flags ;
+        cstr_as_blocks := false
+  |}.
+
 Lemma eval_etaexp {fl : WcbvFlags} (efl := env_flags) {Σ a a'} :
   with_constructor_as_block = false ->
   isEtaExp_env Σ ->
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index bb6a357b2..bf84c91f2 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -294,6 +294,13 @@ Inductive represents : list ident -> environment -> term -> term -> Set :=
 | represents_tPrim Γ E p p' :
   onPrims (represents Γ E) p p' ->
   Γ ;;; E ⊩ tPrim p ~ tPrim p'
+| represents_tLazy Γ E t t' :
+  Γ ;;; E ⊩ t ~ t' ->
+  Γ ;;; E ⊩ tLazy t ~ tLazy t'
+| represents_tForce Γ E t t' :
+  Γ ;;; E ⊩ t ~ t' ->
+  Γ ;;; E ⊩ tForce t ~ tForce t'
+
 with represents_value : value -> term -> Set :=
 | represents_value_tClos na E s t na' : [na] ;;; E ⊩ s ~ t -> represents_value (vClos na s E) (tLambda na' t)
 | represents_value_tConstruct vs ts ind c : All2_Set represents_value vs ts -> represents_value (vConstruct ind c vs) (tConstruct ind c ts)
@@ -371,6 +378,17 @@ Program Definition represents_ind :=
            (represents_tFix Γ E mfix mfix' idx nms Hbodies Hnodup a a0))
      (f9 : forall Γ E p p' (o : onPrims (represents Γ E) p p'), onPrims_dep _ (P Γ E) _ _ o ->
         P Γ E  (tPrim p) (tPrim p') (represents_tPrim Γ E p p' o))
+
+     (flazy : forall Γ E t t'
+      (he : Γ ;;; E ⊩ t ~ t'),
+      P Γ E t t' he ->
+      P Γ E _ _ (represents_tLazy Γ E t t' he))
+
+    (fforce : forall Γ E t t'
+      (he : Γ ;;; E ⊩ t ~ t'),
+      P Γ E t t' he ->
+      P Γ E _ _ (represents_tForce Γ E t t' he))
+
      (f10 :
        ∀ (na : ident)
          (E : environment)
@@ -419,7 +437,11 @@ Program Definition represents_ind :=
          f8 Γ E mfix mfix' idx nms Hbodies Hnodup a a0 _
      | represents_tPrim Γ E p p' r =>
          f9 Γ E p p' r (map_onPrims (F Γ E) r)
-     end
+     | represents_tLazy Γ E t t' e =>
+         flazy _ _ _ _ e (F Γ E _ _ e)
+     | represents_tForce Γ E t t' e =>
+         fforce _ _ _ _ e (F Γ E _ _ e)
+      end
    with F0 (v : value) (t : term) (r : represents_value v t) {struct r} :
      P0 v t r :=
           match r as r0 in (represents_value v0 t0) return (P0 v0 t0 r0) with
@@ -520,6 +542,16 @@ Program Definition represents_value_ind :=
     (f9 : forall Γ E p p' (o : onPrims (represents Γ E) p p'), onPrims_dep _ (P Γ E) _ _ o ->
         P Γ E  (tPrim p) (tPrim p') (represents_tPrim Γ E p p' o))
 
+    (flazy : forall Γ E t t'
+    (he : Γ ;;; E ⊩ t ~ t'),
+    P Γ E t t' he ->
+    P Γ E _ _ (represents_tLazy Γ E t t' he))
+
+  (fforce : forall Γ E t t'
+    (he : Γ ;;; E ⊩ t ~ t'),
+    P Γ E t t' he ->
+    P Γ E _ _ (represents_tForce Γ E t t' he))
+
      (f10 :
        ∀ (na : ident)
          (E : environment)
@@ -571,6 +603,10 @@ Program Definition represents_value_ind :=
          f8 Γ E mfix mfix' idx nms Hbodies Hnodup a a0 _
     | represents_tPrim Γ E p p' r =>
          f9 Γ E p p' r (map_onPrims (F Γ E) r)
+    | represents_tLazy Γ E t t' e =>
+         flazy _ _ _ _ e (F Γ E _ _ e)
+     | represents_tForce Γ E t t' e =>
+         fforce _ _ _ _ e (F Γ E _ _ e)
 
      end
    with F0 (v : value) (t : term) (r : represents_value v t) {struct r} :
@@ -672,8 +708,16 @@ Definition rep_ind :=
            (represents_tFix Γ E mfix mfix' idx nms Hbodies Hnodup a a0))
       (f9 : forall Γ E p p' (o : onPrims (represents Γ E) p p'), onPrims_dep _ (P Γ E) _ _ o ->
            P Γ E  (tPrim p) (tPrim p') (represents_tPrim Γ E p p' o))
-
-   (f10 :
+      (flazy : forall Γ E t t'
+        (he : Γ ;;; E ⊩ t ~ t'),
+        P Γ E t t' he ->
+        P Γ E _ _ (represents_tLazy Γ E t t' he))
+
+      (fforce : forall Γ E t t'
+        (he : Γ ;;; E ⊩ t ~ t'),
+        P Γ E t t' he ->
+        P Γ E _ _ (represents_tForce Γ E t t' he))
+      (f10 :
        ∀ (na : ident)
          (E : environment)
          (s t : term)
@@ -703,8 +747,8 @@ Definition rep_ind :=
       (f13 : forall p p' (o : onPrims represents_value p p'), onPrims_dep _ P0 _ _ o ->
            P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o))
            ,
-    (represents_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13,
-      represents_value_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13)).
+    (represents_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13,
+      represents_value_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13)).
 
 Local Notation "'⊩' v ~ s" := (represents_value v s) (at level 50).
 Local Hint Constructors represents : core.
@@ -893,6 +937,8 @@ Fixpoint annotate (s : list ident) (u : term) {struct u} : term :=
       let mfix' := map2 (fun d na => map_def_name _ (fun _ => nNamed na) (annotate (List.rev (gen_many_fresh s ((map dname mfix))) ++ s)) d) mfix nms in
       tFix mfix' idx
   | tPrim p => tPrim (map_prim (annotate s) p)
+  | tLazy t => tLazy (annotate s t)
+  | tForce t => tForce (annotate s t)
   | _ => u
   end.
 
@@ -918,6 +964,7 @@ Definition extraction_term_flags :=
   ; has_tFix := true
   ; has_tCoFix := false
   ; has_tPrim := all_primitive_flags
+  ; has_tLazy_Force := true
   |}.
 
 Definition extraction_env_flags :=
@@ -963,6 +1010,7 @@ Definition named_extraction_term_flags :=
   ; has_tFix := true
   ; has_tCoFix := false
   ; has_tPrim := all_primitive_flags
+  ; has_tLazy_Force := true
   |}.
 
 Definition named_extraction_env_flags :=
@@ -1101,7 +1149,7 @@ Lemma unfolds_bound :
   (forall Γ E s t, Γ ;;; E ⊩ s ~ t -> closedn #|Γ| t) ×
     (forall v s, ⊩ v ~ s -> closedn 0 s).
 Proof.
-  refine (rep_ind _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); intros; cbn; rtoProp; eauto.
+  refine (rep_ind _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); intros; cbn; rtoProp; eauto.
   - eapply Nat.ltb_lt, nth_error_Some. congruence.
   - eapply closed_upwards; eauto. lia.
   - solve_all. induction a; cbn in *; econstructor; firstorder.
@@ -1376,6 +1424,8 @@ Fixpoint sunny Γ (t : term) : bool :=
            forallb (test_def (sunny (names ++ Γ))) mfix
   | tConstruct _ _ args => forallb (sunny Γ) args
   | tPrim p => test_prim (sunny Γ) p
+  | tLazy t => sunny Γ t
+  | tForce t => sunny Γ t
   | _ => true
   end.
 
diff --git a/erasure/theories/EWellformed.v b/erasure/theories/EWellformed.v
index d50b7bbf5..25037ce0e 100644
--- a/erasure/theories/EWellformed.v
+++ b/erasure/theories/EWellformed.v
@@ -47,6 +47,7 @@ Class ETermFlags :=
   ; has_tFix : bool
   ; has_tCoFix : bool
   ; has_tPrim :: EPrimitiveFlags
+  ; has_tLazy_Force : bool
   }.
 
 Class EEnvFlags := {
@@ -80,6 +81,7 @@ Definition all_term_flags :=
     ; has_tFix := true
     ; has_tCoFix := true
     ; has_tPrim := all_primitive_flags
+    ; has_tLazy_Force := true
   |}.
 
 Definition all_env_flags :=
@@ -139,6 +141,8 @@ Section wf.
         && forallb (wellformed k) block_args else is_nil block_args
     | tVar _ => has_tVar
     | tPrim p => has_prim p && test_prim (wellformed k) p
+    | tLazy t => has_tLazy_Force && wellformed k t
+    | tForce t => has_tLazy_Force && wellformed k t
     end.
 
 End wf.
diff --git a/erasure/theories/ErasureFunctionProperties.v b/erasure/theories/ErasureFunctionProperties.v
index e40966fca..c6b674c45 100644
--- a/erasure/theories/ErasureFunctionProperties.v
+++ b/erasure/theories/ErasureFunctionProperties.v
@@ -1433,6 +1433,8 @@ Section wffix.
     | tVar _ => true
     | tBox => true
     | tPrim p => test_prim wf_fixpoints p
+    | tLazy t => wf_fixpoints t
+    | tForce t => wf_fixpoints t
     end.
 
 End wffix.
diff --git a/erasure/theories/Typed/Optimize.v b/erasure/theories/Typed/Optimize.v
index 966069827..ced7917f7 100644
--- a/erasure/theories/Typed/Optimize.v
+++ b/erasure/theories/Typed/Optimize.v
@@ -21,6 +21,8 @@ Definition map_subterms (f : term -> term) (t : term) : term :=
   | tFix def i => tFix (map (map_def f) def) i
   | tCoFix def i => tCoFix (map (map_def f) def) i
   | tPrim p => tPrim (map_prim f p)
+  | tLazy t => tLazy (f t)
+  | tForce t => tForce (f t)
   | t => t
   end.
 
@@ -313,6 +315,8 @@ Fixpoint is_dead (rel : nat) (t : term) : bool :=
   | tCoFix defs _ => forallb (is_dead (#|defs| + rel) ∘ EAst.dbody) defs
   | tConstruct _ _ args => forallb (is_dead rel) args
   | tPrim p => test_prim (is_dead rel) p
+  | tLazy t => is_dead rel t
+  | tForce t => is_dead rel t
   | _ => true
   end.
 
@@ -371,6 +375,8 @@ Fixpoint valid_cases (t : term) : bool :=
   | tCoFix defs _ => forallb (valid_cases ∘ EAst.dbody) defs
   | tConstruct _ _ (_ :: _) => false (* check whether constructors are not blocks*)
   | tPrim p => test_prim valid_cases p
+  | tLazy t => valid_cases t
+  | tForce t => valid_cases t
   | _ => true
   end.
 
@@ -429,6 +435,8 @@ Fixpoint is_expanded_aux (nargs : nat) (t : term) : bool :=
   | tFix defs _
   | tCoFix defs _ => forallb (is_expanded_aux 0 ∘ EAst.dbody) defs
   | tPrim p => test_prim (is_expanded_aux 0) p
+  | tLazy t => is_expanded_aux 0 t
+  | tForce t => is_expanded_aux 0 t
   end.
 
 (** Check if all applications are applied enough to be deboxed without eta expansion *)
@@ -666,6 +674,8 @@ Fixpoint analyze (state : analyze_state) (t : term) {struct t} : analyze_state :
     let state := fold_left (fun state d => analyze state (dbody d)) defs state in
     remove_vars state #|defs|
   | tPrim p => fold_prim analyze p state
+  | tLazy t => analyze state t
+  | tForce t => analyze state t
   end.
 
 Fixpoint decompose_TArr (bt : box_type) : list box_type × box_type :=
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index 03b7d4219..92bc3b69e 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -288,6 +288,8 @@ Proof.
     rewrite <- Nat.add_succ_r in *.
     now eapply IHX.
   - solve_all.
+  - solve_all.
+  - solve_all.
 Qed.
 
 Lemma is_dead_csubst k t u k' :
@@ -523,6 +525,8 @@ Proof.
     + rewrite <- !Nat.add_succ_r in *.
       now apply IHX.
   - f_equal; solve_all.
+  - f_equal; solve_all.
+  - f_equal; solve_all.
 Qed.
 
 Lemma masked_nil {X} mask :
@@ -872,6 +876,8 @@ Proof.
     f_equal.
     now rewrite p.
   - rewrite lift_mkApps. f_equal. simpl lift. f_equal. solve_all.
+  - rewrite lift_mkApps. f_equal. simpl lift. f_equal. solve_all.
+  - rewrite lift_mkApps. f_equal. simpl lift. f_equal. solve_all.
 Qed.
 
 Lemma lift_dearg n k t :
@@ -923,6 +929,8 @@ Proof.
     rewrite <- !Nat.add_succ_r.
     now apply IHX.
   - solve_all.
+  - solve_all.
+  - solve_all.
 Qed.
 
 Lemma is_dead_lift_all k k' n t :
@@ -1487,6 +1495,8 @@ Proof.
     split; [easy|].
     now apply IHX.
   - solve_all. rtoProp; intuition solve_all.
+  - solve_all. rtoProp; intuition solve_all.
+  - solve_all. rtoProp; intuition solve_all.
 Qed.
 
 Lemma valid_dearg_mask_dearg mask t :
@@ -1646,6 +1656,10 @@ Proof.
   - rewrite subst_mkApps, map_map; cbn; f_equal. f_equal.
     solve_all. eapply map_prim_eq_prop; tea; cbn; intuition eauto.
     specialize (a s k []). eauto.
+  - rewrite subst_mkApps, map_map; cbn; f_equal.
+    f_equal. specialize (IHt s k []); cbn in IHt. eauto.
+  - rewrite subst_mkApps, map_map; cbn; f_equal.
+    f_equal. specialize (IHt s k []); cbn in IHt. eauto.
 Qed.
 
 Lemma dearg_subst s k t :
@@ -1762,6 +1776,8 @@ Proof.
     rewrite <- !Nat.add_succ_r.
     now rewrite p, IHX.
   - solve_all_k 6.
+  - solve_all.
+  - solve_all.
 Qed.
 
 Lemma is_expanded_aux_subst s n t k :
@@ -1806,6 +1822,8 @@ Proof.
     rewrite <- !Nat.add_succ_r.
     now rewrite p, IHX.
   - solve_all_k 6.
+  - solve_all.
+  - solve_all.
 Qed.
 
 Lemma is_expanded_substl s n t :
@@ -2417,6 +2435,8 @@ Proof.
     rewrite <- !Nat.add_succ_r in *.
     now apply IHX.
   - rewrite closedn_mkApps; cbn; rtoProp; intuition solve_all. solve_all_k 6.
+  - rewrite closedn_mkApps; cbn; rtoProp; intuition solve_all.
+  - rewrite closedn_mkApps; cbn; rtoProp; intuition solve_all.
 Qed.
 
 Lemma Alli_map {A B P n} {f : A -> B} l :
diff --git a/erasure/theories/Typed/TypeAnnotations.v b/erasure/theories/Typed/TypeAnnotations.v
index 7984f8795..972518ce5 100644
--- a/erasure/theories/Typed/TypeAnnotations.v
+++ b/erasure/theories/Typed/TypeAnnotations.v
@@ -586,6 +586,8 @@ Proof.
     intros.
     exact (f _ All_nil _ X).
   - refine (annot_mkApps _ argsa). cbn. cbn in ta. exact ta.
+  - refine (annot_mkApps _ argsa). cbn. cbn in ta. exact ta.
+  - refine (annot_mkApps _ argsa). cbn. cbn in ta. exact ta.
 Defined.
 
 Definition annot_dearg im cm {t : term} (ta : annots box_type t) : annots box_type (dearg im cm t) :=
diff --git a/template-coq/Makefile.plugin.local-late b/template-coq/Makefile.plugin.local-late
new file mode 100644
index 000000000..eb053443d
--- /dev/null
+++ b/template-coq/Makefile.plugin.local-late
@@ -0,0 +1 @@
+FINDLIBFILESTOINSTALL += gen-src/metacoq_template_plugin.a
\ No newline at end of file