Ewellformed islambda (#735)

* Constructors as blocks improvement: they always have the right arity

* Include "isLambda" for fixpoint bodies in the ewellformed predicate.

* Derive an eliminator to reason on the evaluation relation when cstrs_as_blocks = true, preserving well-formedness

Author: mattam82

erasure/_CoqProject.in

@@ -34,4 +34,5 @@ theories/ERemoveParams.v
 theories/EInlineProjections.v
 theories/ETransform.v
 theories/EConstructorsAsBlocks.v
+theories/EWcbvEvalCstrsAsBlocksInd.v
 theories/Erasure.v

erasure/theories/EConstructorsAsBlocks.v

@@ -468,62 +468,37 @@ Definition env_flags_blocks :=
 
 Local Existing Instance env_flags.
 
-Lemma Qpreserves_wellformed Σ : wf_glob Σ -> Qpreserves (fun n x => wellformed Σ n x) Σ.
-Proof.
-  intros clΣ.
-  split.
-  - red. move=> n t.
-    destruct t; cbn; intuition auto; try solve [constructor; auto].
-    eapply on_letin; rtoProp; intuition auto.
-    eapply on_app; rtoProp; intuition auto.
-    eapply on_case; rtoProp; intuition auto. solve_all.
-    eapply on_fix. solve_all. move/andP: H => [] _ ha. solve_all.
-  - red. intros kn decl.
-    move/(lookup_env_wellformed clΣ).
-    unfold wf_global_decl. destruct cst_body => //.
-  - red. move=> hasapp n t args. rewrite wellformed_mkApps //. 
-    split; intros; rtoProp; intuition auto; solve_all.
-  - red. cbn => //.
-    (* move=> hascase n ci discr brs. simpl.
-    destruct lookup_inductive eqn:hl => /= //.
-    split; intros; rtoProp; intuition auto; solve_all. *)
-  - red. move=> hasproj n p discr. now cbn in hasproj.
-  - red. move=> t args clt cll.
-    eapply wellformed_substl. solve_all. now rewrite Nat.add_0_r.
-  - red. move=> n mfix idx. cbn. unfold wf_fix.
-    split; intros; rtoProp; intuition auto; solve_all. now apply Nat.ltb_lt.
-  - red. move=> n mfix idx. cbn.
-    split; intros; rtoProp; intuition auto; solve_all.
-Qed.
-
 Definition block_wcbv_flags := 
   {| with_prop_case := false ; with_guarded_fix := false ; with_constructor_as_block := true |}.
 
 Local Hint Resolve wellformed_closed : core.
 
-Lemma wellformed_lookup_inductive_pars Σ kn mdecl :
+Lemma wellformed_lookup_inductive_pars {efl : EEnvFlags} Σ kn mdecl :
+  has_cstr_params = false ->
   wf_glob Σ ->
   lookup_minductive Σ kn = Some mdecl -> mdecl.(ind_npars) = 0.
 Proof.
+  intros hasp.
   induction 1; cbn => //.
   case: eqb_spec => [|].
   - intros ->. destruct d => //. intros [= <-]. 
     cbn in H0. unfold wf_minductive in H0.
-    rtoProp. cbn in H0. now eapply eqb_eq in H0.
+    rtoProp. cbn in H0. rewrite hasp in H0; now eapply eqb_eq in H0.
   - intros _. eapply IHwf_glob.
 Qed.
 
-Lemma wellformed_lookup_constructor_pars {Σ kn c mdecl idecl cdecl} :
+Lemma wellformed_lookup_constructor_pars {efl : EEnvFlags} {Σ kn c mdecl idecl cdecl} :
+  has_cstr_params = false ->
   wf_glob Σ ->
   lookup_constructor Σ kn c = Some (mdecl, idecl, cdecl) -> mdecl.(ind_npars) = 0.
 Proof.
-  intros wf. cbn -[lookup_minductive].
+  intros hasp wf. cbn -[lookup_minductive].
   destruct lookup_minductive eqn:hl => //.
   do 2 destruct nth_error => //.
   eapply wellformed_lookup_inductive_pars in hl => //. congruence.
 Qed.
 
-Lemma lookup_constructor_pars_args_spec {Σ ind n mdecl idecl cdecl} :
+Lemma lookup_constructor_pars_args_spec {efl : EEnvFlags} {Σ ind n mdecl idecl cdecl} :
   wf_glob Σ ->
   lookup_constructor Σ ind n = Some (mdecl, idecl, cdecl) ->
   lookup_constructor_pars_args Σ ind n = Some (mdecl.(ind_npars), cdecl.(cstr_nargs)).
@@ -533,23 +508,25 @@ Proof.
   intros [= -> -> <-]. cbn. f_equal.
 Qed.
 
-Lemma wellformed_lookup_constructor_pars_args {Σ ind n block_args} :
+Lemma wellformed_lookup_constructor_pars_args {efl : EEnvFlags} {Σ ind n block_args} :
   wf_glob Σ ->
+  has_cstr_params = false ->
   wellformed Σ 0 (EAst.tConstruct ind n block_args) ->
   ∑ args, lookup_constructor_pars_args Σ ind n = Some (0, args).
 Proof.
-  intros wfΣ wf. cbn -[lookup_constructor] in wf.
+  intros wfΣ hasp wf. cbn -[lookup_constructor] in wf.
   destruct lookup_constructor as [[[mdecl idecl] cdecl]|] eqn:hl => //.
   exists cdecl.(cstr_nargs).
-  pose proof (wellformed_lookup_constructor_pars wfΣ hl).
+  pose proof (wellformed_lookup_constructor_pars hasp wfΣ hl).
   eapply lookup_constructor_pars_args_spec in hl => //. congruence.
+  destruct has_tConstruct => //.
 Qed.
 
-Lemma constructor_isprop_pars_decl_params {Σ ind c b pars cdecl} :
-  wf_glob Σ ->
+Lemma constructor_isprop_pars_decl_params {efl : EEnvFlags} {Σ ind c b pars cdecl} :
+  has_cstr_params = false -> wf_glob Σ ->
   constructor_isprop_pars_decl Σ ind c = Some (b, pars, cdecl) -> pars = 0.
 Proof.
-  intros hwf.
+  intros hasp hwf.
   rewrite /constructor_isprop_pars_decl /lookup_constructor /lookup_inductive.
   destruct lookup_minductive as [mdecl|] eqn:hl => /= //.
   do 2 destruct nth_error => //.
@@ -601,7 +578,7 @@ Proof.
   + eapply EEtaExpandedFix.decompose_app_tApp_split in da as [Ha Ht].
     cbn in wf.
     move: wf => /andP[]. rewrite Ha wellformed_mkApps // => /andP[] wfc wfl wft.
-    destruct (wellformed_lookup_constructor_pars_args wfΣ wfc).
+    destruct (wellformed_lookup_constructor_pars_args wfΣ eq_refl wfc).
     rewrite e. cbn.
     destruct chop eqn:eqch => //. 
     intros. apply H1. intuition auto.
@@ -674,14 +651,17 @@ Proof.
 Qed.
 
 Lemma lookup_constructor_transform_blocks Σ ind c :
-lookup_constructor (transform_blocks_env Σ) ind c =
-lookup_constructor Σ ind c.
+  lookup_constructor (transform_blocks_env Σ) ind c =
+  lookup_constructor Σ ind c.
 Proof.
   unfold lookup_constructor, lookup_inductive, lookup_minductive in *.
   rewrite lookup_env_transform_blocks.
   destruct lookup_env as [ [] | ]; cbn; congruence.
 Qed.
 
+Lemma isLambda_transform_blocks Σ c : isLambda c -> isLambda (transform_blocks Σ c).
+Proof. destruct c => //. Qed.
+
 Lemma transform_wellformed' Σ n t :
   wf_glob Σ -> 
   @wellformed env_flags Σ n t ->
@@ -692,9 +672,12 @@ Proof.
   all: rewrite ?map_InP_spec; toAll; eauto; try now solve_all.
   - destruct H1. unfold isEtaExp_app in H1. unfold lookup_constructor_pars_args in *.
     destruct (lookup_constructor Σ) as [[[]] | ]; try congruence; cbn - [transform_blocks].
-    2: eauto. split; auto.
+    2: eauto. split; auto. cbn in H1. eapply Nat.leb_le in H1.
+    apply/eqb_spec. lia.
   - destruct H4. solve_all.
-  - unfold wf_fix in *. rtoProp. solve_all. len. solve_all. len. destruct x.
+  - unfold wf_fix in *. rtoProp. solve_all. now eapply isLambda_transform_blocks.
+  - unfold wf_fix in *. rtoProp. solve_all.
+    len. solve_all. len. destruct x.
     cbn -[transform_blocks isEtaExp] in *. rtoProp. eauto.
   - rewrite !wellformed_mkApps in Hw |- * => //. rtoProp. intros.
     eapply isEtaExp_mkApps in H3. rewrite decompose_app_mkApps in H3; eauto.
@@ -708,16 +691,18 @@ Proof.
         rewrite ?lookup_constructor_transform_blocks; eauto.
       * destruct lookup_constructor as [ [[]] | ] eqn:E; cbn -[transform_blocks] in *; eauto.
         invs Heq. rewrite chop_firstn_skipn in Ec. invs Ec.
-        rewrite firstn_length. len. eapply Nat.leb_le in H2. eapply Nat.leb_le.
-        destruct lookup_env as [ [] | ] eqn:E'; try congruence.
-        eapply lookup_env_wellformed in E'; eauto.
-        cbn in E'. red in E'. unfold wf_minductive in E'.
-        rewrite andb_true_iff in E'.
-        cbn in E'. destruct E'.
-        eapply Nat.eqb_eq in H6.
-        destruct nth_error; invs E.
-        destruct nth_error; invs H9.
-        rewrite H6. lia.
+        rewrite firstn_length. len. eapply Nat.leb_le in H2.
+        apply/eqb_spec.
+        assert (ind_npars m0 = 0).
+        { destruct lookup_env as [ [] | ] eqn:E'; try congruence.
+          eapply lookup_env_wellformed in E'; eauto.
+          cbn in E'. red in E'. unfold wf_minductive in E'.
+          rewrite andb_true_iff in E'.
+          cbn in E'. destruct E'.
+          eapply Nat.eqb_eq in H6.
+          destruct nth_error; invs E.
+          now destruct nth_error; invs H9. }
+        lia.
       * rewrite chop_firstn_skipn in Ec. invs Ec.
         solve_all. eapply All_firstn. solve_all.
       * rewrite chop_firstn_skipn in Ec. invs Ec.
@@ -994,11 +979,18 @@ Proof.
     eapply All2_length in X0 as Hlen.
     cbn.
     rewrite !skipn_all Hlen skipn_all firstn_all. cbn.
-    eapply eval_mkApps_Construct_block; tea. eauto.
+    eapply eval_construct_block; tea. eauto.
     now rewrite lookup_constructor_transform_blocks.
-    constructor. cbn [atom]. now rewrite lookup_constructor_transform_blocks H.
-    len. unfold cstr_arity. lia.
-    solve_all. destruct H6; eauto.
-  - intros. econstructor. destruct t; try solve [cbn in H, H0 |- *; try congruence].
-    cbn -[lookup_constructor] in H |- *. destruct l => //. now rewrite lookup_constructor_transform_blocks H.
+    unfold cstr_arity. cbn. rewrite H4; len.
+    solve_all. clear -X0. eapply All2_All2_Set. solve_all.
+    apply H.
+  - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
+    cbn -[lookup_constructor] in H |- *. destruct l => //.
+    destruct lookup_constructor eqn:hl => //.
+    destruct p as [[mdecl idecl] cdecl].
+    eapply eval_construct_block => //.
+    now rewrite lookup_constructor_transform_blocks hl.
+    simp_eta in H1. cbn in H1. unfold isEtaExp_app in H1.
+    rewrite (lookup_constructor_pars_args_spec wfΣ hl) andb_true_r in H1.
+    apply Nat.leb_le in H1; cbn; unfold cstr_arity. lia.
 Qed.

erasure/theories/EDeps.v

@@ -281,7 +281,7 @@ Proof.
     + intuition auto.
       apply erases_deps_mkApps_inv in H4.
       now apply Forall_rev, Forall_skipn.
-    + eapply nth_error_forall in e1; [|now eauto].
+    + eapply nth_error_forall in e2; [|now eauto].
       assumption.
   - congruence.
   - depelim er.
@@ -333,7 +333,7 @@ Proof.
     intuition auto.
     apply erases_deps_mkApps_inv in H3 as (? & ?).
     apply IHev2.
-    now eapply nth_error_forall in e2.
+    now eapply nth_error_forall in e3.
   - congruence.
   - constructor.
   - depelim er.

erasure/theories/EEtaExpandedFix.v

@@ -1392,7 +1392,7 @@ Proof.
     destruct s.
     * destruct p; solve_discr. noconf H3.
       right. len.
-      move: e; unfold isEtaExp_fixapp.
+      move: e1; unfold isEtaExp_fixapp.
       unfold EGlobalEnv.cunfold_fix. destruct nth_error eqn:hnth => //.
       intros [=]. rewrite H3. rewrite -(All2_length a0). eapply Nat.ltb_lt; lia.
     * right. len. eapply isEtaExp_fixapp_mon; tea. lia.
@@ -1404,7 +1404,7 @@ Proof.
     destruct s.
     * destruct p; solve_discr. noconf H2.
       left. split. 
-      unfold isStuckFix'; rewrite e. len. eapply Nat.leb_le. lia.
+      unfold isStuckFix'; rewrite e1. len. eapply Nat.leb_le. lia.
       now rewrite -[tApp _ _](mkApps_app _ _ [av]).
     * right. len. eapply isEtaExp_fixapp_mon; tea. lia.
   + eapply mkApps_eq in H1 as [? []] => //; subst.
@@ -1571,7 +1571,7 @@ Proof.
   - pose proof (eval_trans' H H0_0). subst a'. econstructor; tea.
   - pose proof (eval_trans' H H0_0). subst av. eapply eval_fix; tea.
   - pose proof (eval_trans' H H0_0). subst av. eapply eval_fix_value; tea.
-  - eapply value_final in X. pose proof (eval_trans' X H0_). subst f.
+  - eapply value_final in X. pose proof (eval_trans' X H0_). subst f7.
     pose proof (eval_trans' H H0_0). subst av.
     eapply eval_fix'; tea.
   - eapply eval_construct; tea.
@@ -1854,7 +1854,7 @@ Proof.
       rewrite (remove_last_last l0 a hl).
       rewrite -[tApp _ _](mkApps_app _ _ [a']).
       eapply eval_mkApps_Construct; tea.  
-      { constructor. cbn [atom]; rewrite e0 //. }
+      { constructor. cbn [atom]; rewrite e e0 //. }
       { len. rewrite (All2_length hargs). lia. }
       eapply All2_app.
       eapply forallb_remove_last, forallb_All in etal.

erasure/theories/EInlineProjections.v

@@ -112,7 +112,11 @@ Section optimize.
 
   (* move to globalenv *)
 
-
+  Lemma isLambda_optimize t : isLambda t -> isLambda (optimize t).
+  Proof. destruct t => //. Qed.
+  Lemma isBox_optimize t : isBox t -> isBox (optimize t).
+  Proof. destruct t => //. Qed.
+  
   Lemma wf_optimize t k : 
     wf_glob Σ ->
     wellformed Σ k t -> wellformed Σ k (optimize t).
@@ -135,6 +139,7 @@ Section optimize.
       rewrite IHt //=; len. apply Nat.ltb_lt.
       lia.
     - len. rtoProp; solve_all. rewrite forallb_map; solve_all.
+      now eapply isLambda_optimize. solve_all.
     - len. rtoProp; solve_all. rewrite forallb_map; solve_all.
   Qed.
 
@@ -161,7 +166,7 @@ Section optimize.
       have arglen := wellformed_projection_args wfΣ hl.
       case: Nat.compare_spec. lia. lia.
       auto.
-    - f_equal. move/andP: wft => [hidx hb].
+    - f_equal. move/andP: wft => [hlam /andP[] hidx hb].
       solve_all. unfold map_def. f_equal.
       eapply a0. now rewrite -Nat.add_assoc.
     - f_equal. move/andP: wft => [hidx hb].
@@ -222,7 +227,7 @@ Section optimize.
     intros wfΣ hfix.
     unfold cunfold_fix.
     rewrite nth_error_map.
-    cbn in hfix. move/andP: hfix => [] hidx hfix. 
+    cbn in hfix. move/andP: hfix => [] hlam /andP[] hidx hfix. 
     destruct nth_error eqn:hnth => //.
     intros [= <- <-] => /=. f_equal.
     rewrite optimize_substl //. eapply wellformed_fix_subst => //.
@@ -512,23 +517,23 @@ Proof.
     eapply nth_error_forallb in wfbrs; tea.
     rewrite Nat.add_0_r in wfbrs.
     forward IHev2. eapply wellformed_iota_red; tea => //.
-    rewrite optimize_iota_red in IHev2 => //. now rewrite e3.
+    rewrite optimize_iota_red in IHev2 => //. now rewrite e4.
     econstructor; eauto.
     rewrite -is_propositional_cstr_optimize //. tea.
-    rewrite nth_error_map e1 //. len. len.
+    rewrite nth_error_map e2 //. len. len.
 
   - congruence.
 
   - move/andP => [] /andP[] hl wfd wfbrs.
     forward IHev2. eapply wellformed_substl; tea => //.
     rewrite forallb_repeat //. len.
-    rewrite e0 /= Nat.add_0_r in wfbrs. now move/andP: wfbrs.
+    rewrite e1 /= Nat.add_0_r in wfbrs. now move/andP: wfbrs.
     rewrite optimize_substl in IHev2 => //.
     rewrite forallb_repeat //. len.
-    rewrite e0 /= Nat.add_0_r in wfbrs. now move/andP: wfbrs.
+    rewrite e1 /= Nat.add_0_r in wfbrs. now move/andP: wfbrs.
     eapply eval_iota_sing => //; eauto.
     rewrite -is_propositional_optimize //.
-    rewrite e0 //. simpl.
+    rewrite e1 //. simpl.
     rewrite map_repeat in IHev2 => //.
 
   - move/andP => [] clf cla. rewrite optimize_mkApps in IHev1.
@@ -600,7 +605,7 @@ Proof.
     move/wf_mkApps: ev1 => [] wfc wfargs.
     destruct lookup_projection as [[[[mdecl idecl] cdecl'] pdecl]|] eqn:hl' => //.
     pose proof (lookup_projection_lookup_constructor hl').
-    rewrite (constructor_isprop_pars_decl_constructor H) in e0. noconf e0.
+    rewrite (constructor_isprop_pars_decl_constructor H) in e1. noconf e1.
     forward IHev1 by auto.
     forward IHev2. eapply nth_error_forallb in wfargs; tea.
     rewrite optimize_mkApps /= in IHev1.
@@ -617,11 +622,11 @@ Proof.
     rewrite nth_error_rev. len. rewrite skipn_length. lia. 
     rewrite List.rev_involutive. len. rewrite skipn_length.
     rewrite nth_error_skipn nth_error_map.
-    rewrite e1 -H1.
+    rewrite e2 -H1.
     assert((ind_npars mdecl + cstr_nargs cdecl - ind_npars mdecl) = cstr_nargs cdecl) by lia.
     rewrite H3.
-    eapply (f_equal (option_map (optimize Σ))) in e2.
-    cbn in e2. rewrite -e2. f_equal. f_equal. lia.
+    eapply (f_equal (option_map (optimize Σ))) in e3.
+    cbn in e3. rewrite -e3. f_equal. f_equal. lia.
 
   - congruence.
 
@@ -630,7 +635,7 @@ Proof.
     destruct lookup_projection as [[[[mdecl idecl] cdecl'] pdecl]|] eqn:hl' => //.
     pose proof (lookup_projection_lookup_constructor hl').
     simpl in H. 
-    move: e. rewrite /inductive_isprop_and_pars.
+    move: e0. rewrite /inductive_isprop_and_pars.
     rewrite (lookup_constructor_lookup_inductive H) /=.
     intros [= eq <-].
     eapply eval_iota_sing => //; eauto.
@@ -680,11 +685,6 @@ Qed.
 
 From MetaCoq.Erasure Require Import EEtaExpanded.
 
-Lemma isLambda_optimize Σ t : isLambda t -> isLambda (optimize Σ t).
-Proof. destruct t => //. Qed.
-Lemma isBox_optimize Σ t : isBox t -> isBox (optimize Σ t).
-Proof. destruct t => //. Qed.
-
 Lemma optimize_expanded {Σ : GlobalContextMap.t} t : expanded Σ t -> expanded Σ (optimize Σ t).
 Proof.
   induction 1 using expanded_ind.
@@ -829,7 +829,7 @@ Proof.
     rewrite hrel IHt //= andb_true_r.
     have hargs' := wellformed_projection_args wfΣ hl'.
     apply Nat.ltb_lt. len.
-  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now len.
+  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_optimize. now len.
     unfold test_def in *. len. eauto.
   - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now len.
     unfold test_def in *. len. eauto.