Merge pull request #1089 from MetaCoq/force-lazy-evaluation

Add the `force (lazy t)` evaluation rule to LambdaBox

Author: mattam82

erasure-plugin/theories/ETransform.v

@@ -976,7 +976,7 @@ Program Definition coinductive_to_inductive_transformation (efl : EEnvFlags)
   {has_cstrblocks : cstr_as_blocks = true} :
   Transform.t _ _ EAst.term EAst.term _ _
     (eval_eprogram_env block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
-  {| name := "transforming co-inductive to inductive types";
+  {| name := "transforming co-inductive to lazy inductive types";
     transform p _ := ECoInductiveToInductive.trans_program p ;
     pre p := wf_eprogram_env efl p ;
     post p := wf_eprogram efl p ;

erasure/theories/EAstUtils.v

@@ -318,16 +318,25 @@ Definition is_box c :=
   | _ => false
   end.
 
+Definition isLazy c :=
+  match c with
+  | tLazy _ => true
+  | _ => false
+  end.
+
 Definition isFixApp t := isFix (head t).
 Definition isConstructApp t := isConstruct (head t).
 Definition isPrimApp t := isPrim (head t).
+Definition isLazyApp t := isLazy (head t).
 
 Lemma isFixApp_mkApps f l : isFixApp (mkApps f l) = isFixApp f.
 Proof. rewrite /isFixApp head_mkApps //. Qed.
 Lemma isConstructApp_mkApps f l : isConstructApp (mkApps f l) = isConstructApp f.
 Proof. rewrite /isConstructApp head_mkApps //. Qed.
 Lemma isPrimApp_mkApps f l : isPrimApp (mkApps f l) = isPrimApp f.
 Proof. rewrite /isPrimApp head_mkApps //. Qed.
+Lemma isLazyApp_mkApps f l : isLazyApp (mkApps f l) = isLazyApp f.
+Proof. rewrite /isLazyApp head_mkApps //. Qed.
 
 Lemma is_box_mkApps f a : is_box (mkApps f a) = is_box f.
 Proof.
@@ -347,6 +356,8 @@ Lemma nisBox_mkApps f args : ~~ isBox f -> ~~ isBox (mkApps f args).
 Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
 Lemma nisPrim_mkApps f args : ~~ isPrim f -> ~~ isPrim (mkApps f args).
 Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
+Lemma nisLazy_mkApps f args : ~~ isLazy f -> ~~ isLazy (mkApps f args).
+Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
 
 Definition string_of_def {A : Set} (f : A -> string) (def : def A) :=
   "(" ^ string_of_name (dname def) ^ "," ^ f (dbody def) ^ ","

erasure/theories/EConstructorsAsBlocks.v

@@ -649,6 +649,28 @@ Proof.
     eapply IHt1. cbn in Hwf'. rtoProp. intuition.
 Qed.
 
+Lemma transform_blocks_isLazyApp {efl : EEnvFlags} {Σ : GlobalContextMap.t} t :
+  has_cstr_params = false ->
+  wf_glob Σ -> wellformed Σ 0 t ->
+  isLazyApp (transform_blocks Σ t) = isLazyApp t.
+Proof.
+  intros haspars Hwf Hwf'.
+  induction t; try now cbn; eauto.
+  eapply transform_blocks_tApp; eauto.
+  destruct decompose_app.
+  destruct construct_viewc.
+  - rewrite GlobalContextMap.lookup_constructor_pars_args_spec.
+    destruct lookup_constructor_pars_args as [ [[]] | ]; eauto.
+    cbn. destruct chop. intros (? & ? & ?). subst.
+    rewrite -[tApp _ _](mkApps_app _ _ [t2]).
+    rewrite !isLazyApp_mkApps. cbn. reflexivity.
+  - change (tApp t1 t2) with (mkApps t1 [t2]).
+    change (tApp (transform_blocks Σ t1) (transform_blocks Σ t2)) with
+    (mkApps (transform_blocks Σ t1) [transform_blocks Σ t2]).
+    rewrite !isLazyApp_mkApps.
+    eapply IHt1. cbn in Hwf'. rtoProp. intuition.
+Qed.
+
 Lemma lookup_env_transform_blocks {Σ : GlobalContextMap.t} kn :
   lookup_env (transform_blocks_env Σ) kn =
   option_map (transform_blocks_decl Σ) (lookup_env Σ kn).
@@ -1125,17 +1147,20 @@ Proof.
       * rewrite GlobalContextMap.lookup_constructor_pars_args_spec;
           destruct lookup_constructor_pars_args as [ [[]] | ] eqn:hpa; eauto.
         cbn [plus]. destruct chop eqn:heqch.
-        intros [hl [ht ha]]. rewrite ht in H1. rewrite isConstructApp_mkApps isPrimApp_mkApps orb_true_r in H1 => //.
+        intros [hl [ht ha]]. rewrite ht in H1. rewrite isConstructApp_mkApps
+          isPrimApp_mkApps isLazyApp_mkApps orb_true_r in H1 => //.
       * eapply eval_app_cong; eauto.
         revert H1.
         destruct f'; try now cbn; tauto.
         intros H. cbn in H.
         rewrite transform_blocks_isConstructApp; eauto.
         rewrite transform_blocks_isPrimApp; eauto.
-        rewrite negb_or in H. move/andP: H => [] ncstr nprim.
+        rewrite transform_blocks_isLazyApp; eauto.
+        rewrite !negb_or in H. move/andP: H => [] /andP [] ncstr nprim nlazy.
         destruct (isConstructApp (tApp f'1 f'2)) eqn:heq'.
         -- cbn in ncstr. congruence.
-        -- eapply transform_blocks_tApp; eauto. clear -nprim.
+        -- eapply transform_blocks_tApp; eauto. clear -nprim nlazy.
+          move/negbTE: nlazy ->. move/negbTE: nprim -> => /=.
            destruct decompose_app.
            destruct construct_viewc; try now cbn; eauto.
            rewrite GlobalContextMap.lookup_constructor_pars_args_spec;
@@ -1186,6 +1211,11 @@ Proof.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. eapply All2_All2_Set. solve_all.
     now destruct b.
     now destruct a0.
+  - intros evl evt' [evt wft wflt etat etalt].
+    intros [evt'' wft' wfv etat' etav].
+    simp transform_blocks; rewrite -!transform_blocks_equation_1.
+    econstructor; eauto.
+    now simp transform_blocks in evt; rewrite -!transform_blocks_equation_1 in evt.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
     cbn -[lookup_constructor] in H |- *. destruct args => //.
     destruct lookup_constructor eqn:hl => //.

erasure/theories/EDeps.v

@@ -354,6 +354,7 @@ Proof.
   - depelim er; depelim X; constructor; eauto.
     eapply All2_over_undep in a0. solve_all.
   - easy.
+  - easy.
 Qed.
 
 #[global]

erasure/theories/EEtaExpandedFix.v

@@ -1056,7 +1056,7 @@ Lemma eval_etaexp {fl : WcbvFlags} {efl : EEnvFlags} {wcon : with_constructor_as
 Proof.
   intros etaΣ wfΣ.
   induction 1 as [ | ? ? ? ? ? ? ? ? IHs | | | | | ? ? ? ? ? ? ? ? ? ? ? IHs | ? ? ? ? ? ? ? ? ? ? ? IHs
-    | ? ? ? ? ? ? ? ? ? ? IHs | | | | | | | | | | | ] using eval_mkApps_rect; try now congruence.
+    | ? ? ? ? ? ? ? ? ? ? IHs | | | | | | | | | | | | ] using eval_mkApps_rect; try now congruence.
   all:try simp isEtaExp; rewrite -?isEtaExp_equation_1 => //.
   6:{
     move/isEtaExp_tApp'.
@@ -1375,6 +1375,7 @@ Proof.
   - solve_all.
     depelim X; solve_all. eapply All2_over_undep in a. subst a0 a';
       depelim H; constructor; solve_all. solve_all.
+  - simp_eta in IHeval1. eauto.
 Qed.
 
 Lemma isEtaExp_fixapp_mon {mfix idx n n'} : n <= n' -> isEtaExp_fixapp mfix idx n -> isEtaExp_fixapp mfix idx n'.
@@ -1961,6 +1962,8 @@ Proof.
   - intros hexp. simp_eta in hexp. depelim X; repeat constructor; eauto.
     eapply All2_over_undep in a. subst a0 a'. solve_all. depelim hexp; cbn in *. destruct p.
     eapply All2_All2_Set. solve_all. solve_all. depelim hexp. destruct p. solve_all.
+  - intros hexp. simp_eta in hexp. econstructor; eauto. apply IHeval2.
+    specialize (IHeval1 hexp). eapply eval_etaexp in IHeval1. now simp_eta in IHeval1. all:eauto.
   - intros hexp. now eapply eval_atom.
     Unshelve. all: eauto.
 Qed.

erasure/theories/EImplementBox.v

@@ -388,6 +388,15 @@ Proof.
   rewrite (isPrimApp_mkApps _ [_]). eauto.
 Qed.
 
+Lemma implement_box_isLazyApp {efl : EEnvFlags} {Σ : global_declarations} t :
+  isLazyApp (implement_box t) = isLazyApp t.
+Proof.
+  induction t; try now cbn; eauto.
+  simp implement_box.
+  rewrite (isLazyApp_mkApps _ [t2]).
+  rewrite (isLazyApp_mkApps _ [_]). eauto.
+Qed.
+
 Lemma lookup_env_implement_box {Σ : global_declarations} kn :
   lookup_env (implement_box_env Σ) kn =
   option_map (implement_box_decl) (lookup_env Σ kn).
@@ -670,6 +679,7 @@ Proof.
     intros H. cbn in H.
     rewrite implement_box_isConstructApp; eauto.
     rewrite implement_box_isPrimApp; eauto.
+    rewrite implement_box_isLazyApp; eauto.
   - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end.
     simp implement_box in *.
     eapply eval_construct_block; tea. eauto.
@@ -680,6 +690,9 @@ Proof.
   - intros wf H; depelim H; simp implement_box; repeat constructor.
     destruct a0. eapply All2_over_undep in a. eapply All2_All2_Set, All2_map.
     cbn -[implement_box]. solve_all. now destruct H. now destruct a0.
+  - intros evt evt' [] [].
+    simp implement_box. simp implement_box in e.
+    econstructor; eauto.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
     cbn -[lookup_constructor] in H |- *. destruct args => //.
 Qed.

erasure/theories/EInlineProjections.v

@@ -710,13 +710,14 @@ Proof.
     * destruct with_guarded_fix.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps
+          !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         rewrite !andb_true_r.
         rtoProp; intuition auto;  destruct v => /= //.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
   - intros; rtoProp; intuition eauto.
@@ -725,6 +726,8 @@ Proof.
     eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp.
     subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all.
     primProp; depelim H0; intuition eauto.
+  - intros wf; econstructor; eauto. eapply IHev2.
+    eapply eval_wellformed in ev1; tea => //.
   - destruct t => //.
     all:constructor; eauto.
     cbn [atom optimize] in i |- *.

erasure/theories/EOptimizePropDiscr.v

@@ -715,22 +715,24 @@ Proof.
     * destruct with_guarded_fix.
       + move: i.
         rewrite !negb_or.
-        rewrite remove_match_on_box_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         rewrite !andb_true_r.
         rtoProp; intuition auto.
         destruct v => /= //.
         destruct v => /= //.
         destruct v => /= //.
+        destruct v => /= //.
       + move: i.
         rewrite !negb_or.
-        rewrite remove_match_on_box_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
   - depelim X; repeat constructor.
     eapply All2_over_undep in a. eapply All2_All2_Set. eapply All2_Set_All2 in ev. subst a0 a'; cbn in *.
     rewrite /test_array_model /= in H. rtoProp; intuition auto; solve_all. eapply e.
     cbn in H. rewrite /test_array_model /= in H. now move/andP: H => [].
+  - intros. econstructor; eauto. eapply IHev2. eapply eval_closed in ev1; tea.
   - destruct t => //.
     all:constructor; eauto. cbn [atom remove_match_on_box] in i |- *.
     rewrite -lookup_constructor_remove_match_on_box //. destruct args => //.

erasure/theories/ERemoveParams.v

@@ -779,6 +779,14 @@ Proof.
   all:rewrite !isPrimApp_mkApps //.
 Qed.
 
+Lemma strip_isLazyApp Σ f :
+  isLazyApp f = isLazyApp (strip Σ f).
+Proof.
+  funelim (strip Σ f); cbn -[strip] => //.
+  all:rewrite map_InP_spec.
+  all:rewrite !isLazyApp_mkApps //.
+Qed.
+
 Lemma lookup_inductive_pars_is_prop_and_pars {Σ ind b pars} :
   inductive_isprop_and_pars Σ ind = Some (b, pars) ->
   lookup_inductive_pars Σ (inductive_mind ind) = Some pars.
@@ -1011,8 +1019,8 @@ Proof.
   - rewrite !strip_tApp //.
     eapply eval_app_cong; tea.
     move: H1. eapply contraNN.
-    rewrite -strip_isLambda -strip_isConstructApp -strip_isFixApp -strip_isBox -strip_isPrimApp //.
-    rewrite -strip_isFix //.
+    rewrite -strip_isLambda -strip_isConstructApp -strip_isFixApp -strip_isBox -strip_isPrimApp
+      -strip_isLazyApp // -strip_isFix //.
 
   - rewrite !strip_mkApps // /=.
     rewrite (lookup_constructor_lookup_inductive_pars H).
@@ -1030,6 +1038,8 @@ Proof.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. eapply All2_All2_Set. solve_all. now destruct b.
     now destruct a0.
 
+  - simp_strip. simp_strip in e0. econstructor; tea.
+
   - destruct t => //.
     all:constructor; eauto. simp strip.
     cbn [atom strip] in H |- *.

erasure/theories/EWcbvEval.v

@@ -38,6 +38,7 @@ Definition atom `{wfl : WcbvFlags} Σ t :=
   | tBox
   | tCoFix _ _
   | tLambda _ _
+  | tLazy _
   | tFix _ _ => true
   | tConstruct ind c [] => negb with_constructor_as_block && isSome (lookup_constructor Σ ind c)
   | _ => false
@@ -258,7 +259,7 @@ Section Wcbv.
   | eval_app_cong f f' a a' :
       eval f f' ->
       ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f' || isConstructApp f'
-        || isPrimApp f')  ->
+        || isPrimApp f' || isLazyApp f')  ->
       eval a a' ->
       eval (tApp f a) (tApp f' a')
 
@@ -272,13 +273,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_force t v v' :
+    eval t (tLazy v) ->
     eval v v' ->
-    eval (tForce t) v' *)
+    eval (tForce t) v'
 
-  (** Atoms are values (includes abstractions, cofixpoints and constructors) *)
+  (** Atoms are values (includes abstractions, cofixpoints, constructors and lazy) *)
   | eval_atom t : atom Σ t -> eval t t.
 
   Hint Constructors eval : core.
@@ -615,7 +615,7 @@ Section eval_rect.
                                                  isBox f'
                                                  ||
                                                  isConstructApp f'
-                                                 || isPrimApp f'))
+                                                 || isPrimApp f' || isLazyApp f'))
                                            (e0 : eval Σ a a'),
                                            P a a' e0
                                            → P (tApp f16 a)
@@ -626,14 +626,17 @@ Section eval_rect.
 
     (forall p p' (ev : eval_primitive (eval Σ) p p'),
       eval_primitive_ind _ P _ _ ev ->
-      P (tPrim p) (tPrim p') (eval_prim _ _ _ ev))
+      P (tPrim p) (tPrim p') (eval_prim _ _ _ ev)) ->
+    (forall t t' v (ev1 : eval Σ t (tLazy t')) (ev2 : eval Σ t' v),
+      P _ _ ev1 -> P _ _ ev2 ->
+      P (tForce t) v (eval_force _ t t' v ev1 ev2))
 
-      → (∀ (t : term) (i : atom Σ t),
+    → (∀ (t : term) (i : atom Σ t),
           P t t (eval_atom Σ t i))
       → ∀ (t t0 : term) (e : eval Σ t t0),
           P t t0 e.
   Proof using Type.
-    intros ?????????????????????? H.
+    intros ??????????????????????? H.
     revert t t0 H.
     fix aux 3.
     move aux at top.
@@ -785,6 +788,7 @@ Section Wcbv.
         + destruct with_guarded_fix.
           now cbn in i1. now cbn in i1.
         + constructor.
+        + now destruct with_guarded_fix; cbn in i1.
         + cbn in i. destruct with_guarded_fix; cbn in i; rtoProp; intuition auto.
       * destruct b0 as (ind & c & mdecl & idecl & cdecl & args & [H1 H2 H3 H4]).
         rewrite -[tApp _ _](mkApps_app _ (firstn n l) [a']).
@@ -1058,7 +1062,7 @@ Section Wcbv.
       rewrite !mkApps_app /=.
       eapply eval_app_cong; tea.
       eapply IHargs => //.
-      rewrite isFixApp_mkApps // /= isConstructApp_mkApps // !negb_or isPrimApp_mkApps.
+      rewrite isFixApp_mkApps // /= isConstructApp_mkApps // !negb_or isPrimApp_mkApps isLazyApp_mkApps.
       rtoProp; intuition auto.
       apply nisLambda_mkApps => //.
       destruct with_guarded_fix => //; eapply nisFix_mkApps => //.
@@ -1304,15 +1308,15 @@ Section Wcbv.
         cbn in i. rtoProp; intuition auto.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite guarded in i. rtoProp; intuition auto.
-        rewrite isFixApp_mkApps in H3 => //.
+        rewrite isFixApp_mkApps in H4 => //.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite guarded in i. rtoProp; intuition auto.
-        rewrite isFixApp_mkApps in H3 => //.
+        rewrite isFixApp_mkApps in H4 => //.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite unguarded in i. now cbn in i.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rtoProp; intuition auto.
-        now rewrite isConstructApp_mkApps in H1.
+        now rewrite isConstructApp_mkApps in H2.
       + specialize (IHev1 _ ev'1); noconf IHev1.
         specialize (IHev2 _ ev'2); noconf IHev2.
         now assert (i0 = i) as -> by now apply uip.
@@ -1329,6 +1333,7 @@ Section Wcbv.
       induction ev in a, ev0 |- *; depelim ev0; eauto.
       destruct a.
       f_equal; eauto. specialize (e0 _ e). now noconf e0.
+    - depelim ev'; go.
     - depelim ev'; try go.
       2: now assert (i0 = i) as -> by now apply uip.
       exfalso. invs i. rewrite e in H0. destruct args; cbn in H0; invs H0.