Adapted erasure to new array evaluation rules, except named wcbveval relation

Author: mattam82

common/theories/Environment.v

@@ -856,8 +856,8 @@ Module Environment (T : Term).
   Definition primitive_invariants (p : prim_tag) (cdecl : constant_body) :=
     match p with
     | primInt | primFloat =>
-     ∑ s, [/\ cdecl.(cst_type) = tSort s, cdecl.(cst_body) = None &
-             cdecl.(cst_universes) = Monomorphic_ctx]
+     [/\ cdecl.(cst_type) = tSort Universe.type0, cdecl.(cst_body) = None &
+          cdecl.(cst_universes) = Monomorphic_ctx]
     | primArray =>
       let s := Universe.make (Level.lvar 0) in
       [/\ cdecl.(cst_type) = tImpl (tSort s) (tSort s), cdecl.(cst_body) = None &

erasure-plugin/theories/ErasureCorrectness.v

@@ -262,7 +262,7 @@ Proof.
   intros Hf.
   fix aux 2.
   intros t fo; destruct fo.
-  eapply Hf => //. clear H. rename H0 into H.  
+  eapply Hf => //. clear H. rename H0 into H.
   move: args H.
   fix aux' 2.
   intros args []; constructor.
@@ -741,7 +741,7 @@ Proof.
   move: v; apply: firstorder_evalue_elim.
   intros.
   rewrite /flip (compile_evalue_box_mkApps) // ?app_nil_r.
-  pose proof (H' := H). 
+  pose proof (H' := H).
   eapply lookup_constructor_pars_args_nopars in H; tea. subst npars.
   rewrite skipn_0 in H1.
   constructor.
@@ -1559,7 +1559,7 @@ Section pipeline_cond.
     - cbn. intros wf ? ? ? ? ? ?. now eapply Normalisation.
   Qed.
 
-End pipeline_cond. 
+End pipeline_cond.
 
 Section pipeline_theorem.
 
@@ -1602,7 +1602,7 @@ Section pipeline_theorem.
 
   Lemma v_t_spec : v_t = (transform verified_erasure_pipeline (Σ, v) (precond2 _ _ _ _ expΣ expt typing _ _ Heval)).2.
   Proof.
-    unfold v_t. generalize fo_v. set (pre := precond2 _ _ _ _ _ _ _ _ _ _) in *. clearbody pre. 
+    unfold v_t. generalize fo_v. set (pre := precond2 _ _ _ _ _ _ _ _ _ _) in *. clearbody pre.
     intros hv.
     unfold verified_erasure_pipeline.
     rewrite -transform_compose_assoc.
@@ -1629,7 +1629,7 @@ Section pipeline_theorem.
     set (p := transform erase_transform _ _).
     pose proof (@erase_tranform_firstorder _ h v i u (List.map PCUICExpandLets.trans args) Normalisation').
     forward H0.
-    { cbn. rewrite -eqtr.  
+    { cbn. rewrite -eqtr.
       eapply (PCUICClassification.subject_reduction_eval (Σ := Σ)) in X; tea.
       eapply PCUICExpandLetsCorrectness.expand_lets_sound in X.
       now rewrite PCUICExpandLetsCorrectness.trans_mkApps /= in X. }
@@ -1664,24 +1664,24 @@ Section pipeline_theorem.
 
   Lemma verified_erasure_pipeline_lookup_env_in kn decl (efl := EInlineProjections.switch_no_params all_env_flags)  {has_rel : has_tRel} {has_box : has_tBox}  :
     EGlobalEnv.lookup_env Σ_v kn = Some (EAst.InductiveDecl decl) ->
-    exists decl', 
+    exists decl',
       PCUICAst.PCUICEnvironment.lookup_global (PCUICExpandLets.trans_global_decls
       (PCUICAst.PCUICEnvironment.declarations
          Σ.1)) kn = Some (PCUICAst.PCUICEnvironment.InductiveDecl decl')
-       /\ decl = ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl'). 
-  Proof. 
+       /\ decl = ERemoveParams.strip_inductive_decl (erase_mutual_inductive_body decl').
+  Proof.
     Opaque compose.
     unfold Σ_v, verified_erasure_pipeline.
-    repeat rewrite -transform_compose_assoc. 
-    destruct_compose; intro. cbn. 
+    repeat rewrite -transform_compose_assoc.
+    destruct_compose; intro. cbn.
     destruct_compose; intro. cbn.
-    set (erase_program _ _). 
+    set (erase_program _ _).
     unfold verified_lambdabox_pipeline.
-    repeat rewrite -transform_compose_assoc. 
-    repeat (destruct_compose; intro). 
+    repeat rewrite -transform_compose_assoc.
+    repeat (destruct_compose; intro).
     unfold transform at 1. cbn -[transform].
     rewrite EConstructorsAsBlocks.lookup_env_transform_blocks.
-    set (EConstructorsAsBlocks.transform_blocks_decl _). 
+    set (EConstructorsAsBlocks.transform_blocks_decl _).
     unfold transform at 1. cbn -[transform].
     unfold transform at 1. cbn -[transform].
     erewrite EInlineProjections.lookup_env_optimize.
@@ -1692,7 +1692,7 @@ Section pipeline_theorem.
       rewrite erase_global_deps_fast_spec.
       eapply erase_global_deps_wf_glob.
       intros ? He; now rewrite He. }
-    set (EInlineProjections.optimize_decl _). 
+    set (EInlineProjections.optimize_decl _).
     unfold transform at 1. cbn -[transform].
     unfold transform at 1. cbn -[transform].
     erewrite EOptimizePropDiscr.lookup_env_remove_match_on_box.
@@ -1710,25 +1710,25 @@ Section pipeline_theorem.
     unfold transform at 1. cbn -[transform].
     rewrite erase_global_deps_fast_spec.
     2: { cbn. intros ? He. rewrite He. eauto. }
-    intro. 
+    intro.
     set (EAstUtils.term_global_deps _).
     set (build_wf_env_from_env _ _).
-    epose proof 
+    epose proof
       (lookup_env_in_erase_global_deps optimized_abstract_env_impl w t0
       _ kn _ Hyp0).
     set (EGlobalEnv.lookup_env _ _).
     case_eq o. 2: { intros ?. inversion 1. }
     destruct g3; intro Ho; [inversion 1|].
-    cbn. inversion 1.  
+    cbn. inversion 1.
     specialize (H8 m). forward H8.
     epose proof (wf_fresh_globals _ HΣ). clear - H10.
     revert H10. cbn. set (Σ.1). induction 1; econstructor; eauto.
     cbn. clear -H. induction H; econstructor; eauto.
-    unfold o in Ho; rewrite Ho in H8.   
-    specialize (H8 eq_refl). 
+    unfold o in Ho; rewrite Ho in H8.
+    specialize (H8 eq_refl).
     destruct H8 as [decl' [? ?]]. exists decl'; split ; eauto.
     rewrite <- H10. now destruct decl, m.
-  Qed. 
+  Qed.
 
   Lemma verified_erasure_pipeline_firstorder_evalue_block :
     firstorder_evalue_block Σ_v v_t.
@@ -1740,9 +1740,9 @@ Section pipeline_theorem.
     destruct_compose.
     generalize fo_v. intros hv.
     cbn [transform pcuic_expand_lets_transform].
-    intros pre1. destruct_compose. intros pre2. 
-    destruct lambdabox_pres_fo as [fn [tr hfn]].  
-    destruct tr. destruct typing as [typing']. pose proof (Heval' := Heval). sq. rewrite transform_fo. 
+    intros pre1. destruct_compose. intros pre2.
+    destruct lambdabox_pres_fo as [fn [tr hfn]].
+    destruct tr. destruct typing as [typing']. pose proof (Heval' := Heval). sq. rewrite transform_fo.
     { intro. eapply preserves_fo. }
     assert (eqtr : PCUICExpandLets.trans v = v).
     { clear -hv.
@@ -1759,7 +1759,7 @@ Section pipeline_theorem.
     set (p := transform erase_transform _ _).
     pose proof (@erase_tranform_firstorder _ pre1 v i u (List.map PCUICExpandLets.trans args) Normalisation').
     forward H0.
-    { cbn. 
+    { cbn.
       eapply (PCUICClassification.subject_reduction_eval (Σ := Σ)) in Heval'; tea.
       eapply PCUICExpandLetsCorrectness.expand_lets_sound in Heval'.
       now rewrite PCUICExpandLetsCorrectness.trans_mkApps /= in Heval'. }
@@ -1777,29 +1777,29 @@ Section pipeline_theorem.
       eapply PCUICWcbvEval.eval_closed; tea. apply HΣ.
       unshelve apply (PCUICClosedTyp.subject_closed typing'). now rewrite eqtr. }
     specialize (H0 _ eq_refl).
-    rewrite /p.  
+    rewrite /p.
     rewrite erase_transform_fo //. { cbn. rewrite eqtr. exact H. }
     set (Σer := (transform erase_transform _ _).1).
     assert (firstorder_evalue Σer (compile_value_erase v [])).
     { apply H0. }
-    simpl. unfold fo_evalue_map. rewrite eqtr. exact H1. 
-  Qed.   
+    simpl. unfold fo_evalue_map. rewrite eqtr. exact H1.
+  Qed.
 
   Lemma verified_erasure_pipeline_extends (efl := EInlineProjections.switch_no_params all_env_flags)  {has_rel : has_tRel} {has_box : has_tBox} :
    EGlobalEnv.extends Σ_v Σ_t.
   Proof.
     unfold Σ_v, Σ_t. unfold verified_erasure_pipeline.
-    repeat (destruct_compose; intro). destruct typing as [typing'], Heval. 
+    repeat (destruct_compose; intro). destruct typing as [typing'], Heval.
     cbn [transform compose pcuic_expand_lets_transform] in *.
     unfold run, time.
     cbn [transform erase_transform] in *.
     set (erase_program _ _). set (erase_program _ _).
     eapply verified_lambdabox_pipeline_extends.
-    eapply extends_erase_pcuic_program; eauto. 
+    eapply extends_erase_pcuic_program; eauto.
       unshelve eapply (PCUICExpandLetsCorrectness.trans_wcbveval (cf := extraction_checker_flags) (Σ := (Σ.1, Σ.2))).
       { now eapply PCUICExpandLetsCorrectness.trans_wf. }
       { clear -HΣ typing'. now eapply PCUICClosedTyp.subject_closed in typing'. }
-      assumption. 
+      assumption.
       now eapply PCUICExpandLetsCorrectness.trans_axiom_free.
       pose proof (PCUICExpandLetsCorrectness.expand_lets_sound typing').
       rewrite PCUICExpandLetsCorrectness.trans_mkApps in X. eapply X.
@@ -1808,8 +1808,9 @@ Section pipeline_theorem.
         rewrite PCUICExpandLetsCorrectness.trans_lookup.
         destruct PCUICAst.PCUICEnvironment.lookup_env => //.
         destruct g => //=.
-        eapply PCUICExpandLetsCorrectness.trans_firstorder_mutind. eapply PCUICExpandLetsCorrectness.trans_firstorder_env. }
-  Qed. 
+        eapply PCUICExpandLetsCorrectness.trans_firstorder_mutind.
+        eapply PCUICExpandLetsCorrectness.trans_firstorder_env. }
+  Qed.
 
   Lemma verified_erasure_pipeline_theorem :
     ∥ eval (wfl := extraction_wcbv_flags) Σ_t t_t v_t ∥.
@@ -1820,7 +1821,7 @@ Section pipeline_theorem.
     destruct Hev as [v' [[H1] H2]].
     move: H2.
     rewrite v_t_spec.
-    set (pre := precond2 _ _ _ _ _ _ _ _ _ _) in *. clearbody pre. 
+    set (pre := precond2 _ _ _ _ _ _ _ _ _ _) in *. clearbody pre.
     subst v_t Σ_t t_t.
     revert H1.
     unfold verified_erasure_pipeline.
@@ -1874,7 +1875,7 @@ Section pipeline_theorem.
     eapply (ErasureFunctionProperties.firstorder_erases_deterministic optimized_abstract_env_impl wfe Σ.2) in b0. 3:tea.
     2:{ cbn. reflexivity. }
     2:{ eapply PCUICExpandLetsCorrectness.trans_wcbveval. eapply PCUICWcbvEval.eval_closed; tea. apply HΣ.
-        clear -typing'' HΣ. now eapply PCUICClosedTyp.subject_closed in typing''. 
+        clear -typing'' HΣ. now eapply PCUICClosedTyp.subject_closed in typing''.
         eapply PCUICWcbvEval.value_final. now eapply PCUICWcbvEval.eval_to_value in X0. }
     (* 2:{ clear -fo. cbn. now eapply (PCUICExpandLetsCorrectness.trans_firstorder_ind Σ). }
         eapply PCUICWcbvEval.value_final. now eapply PCUICWcbvEval.eval_to_value in X. } *)

erasure/theories/EArities.v

@@ -1051,3 +1051,70 @@ Proof.
     eapply PCUICElimination.unique_sorting_equality_propositional in Hprinc; eauto.
     rewrite Hprinc; eauto.
 Qed.
+
+(** Inhabitants of primitive types are not erasable: they must live in a relevant universe.
+
+  This currently relies on int and float being in Set, while arrays are universe polymorphic,
+  hence always relevant, and the primitive types are axioms, so not convertible to arities. *)
+
+Lemma prim_type_inv p prim_ty :
+  ∑ u args, prim_type p prim_ty = mkApps (tConst prim_ty u) args.
+Proof.
+  destruct p as [? []]; simp prim_type.
+  - eexists [], []. reflexivity.
+  - eexists [], []; reflexivity.
+  - eexists [_], [_]; reflexivity.
+Qed.
+
+Lemma primitive_invariants_axiom t decl : primitive_invariants t decl -> cst_body decl = None.
+Proof.
+  destruct t; cbn => //.
+  1-2:now intros [? []].
+  now intros [].
+Qed.
+
+Lemma nisErasable_tPrim Σ p :
+  wf_ext Σ ->
+  isErasable Σ [] (tPrim p) -> False.
+Proof.
+  intros wfΣ [T [Ht h]].
+  eapply inversion_Prim in Ht as [prim_ty [cdecl []]]; eauto.
+  pose proof (type_Prim _ _ _ _ _ a e d p0 p1). eapply validity in X.
+  destruct h.
+  - eapply invert_cumul_arity_r in w; tea.
+    destruct w as [ar [[H] r]].
+    destruct (prim_type_inv p prim_ty) as [u [args eq]].
+    rewrite eq in H.
+    eapply invert_red_axiom_app in H as [args' []]; tea.
+    2:now eapply primitive_invariants_axiom.
+    subst ar. now eapply isArity_mkApps in r as [].
+  - destruct s as [s [hs isp]].
+    eapply cumul_prop1' in hs; tea; eauto.
+    depelim p1; simp prim_type in hs.
+    * destruct p0 as [hd hb hu].
+      eapply inversion_Const in hs as [decl' [wf [decl'' [cu hs']]]]; eauto.
+      unshelve eapply declared_constant_to_gen in d, decl''. 3,6:eapply wfΣ.
+      eapply declared_constant_inj in d; tea. subst decl'.
+      rewrite hd in hs'. cbn in hs'.
+      eapply ws_cumul_pb_Sort_inv in hs'. red in hs'.
+      destruct s => //.
+    * destruct p0 as [hd hb hu].
+      eapply inversion_Const in hs as [decl' [wf [decl'' [cu hs']]]]; eauto.
+      unshelve eapply declared_constant_to_gen in d, decl''. 3,6:eapply wfΣ.
+      eapply declared_constant_inj in d; tea. subst decl'.
+      rewrite hd in hs'. cbn in hs'.
+      eapply ws_cumul_pb_Sort_inv in hs'. red in hs'.
+      destruct s => //.
+    * destruct p0 as [hd hb hu].
+      eapply inversion_App in hs as [na [A [B [hp [harg hres]]]]]; eauto.
+      eapply inversion_Const in hp as [decl' [wf [decl'' [cu hs']]]]; eauto.
+      unshelve eapply declared_constant_to_gen in d, decl''. 3,6:eapply wfΣ.
+      eapply declared_constant_inj in d; tea. subst decl'.
+      rewrite hd in hs'. cbn in hs'.
+      eapply ws_cumul_pb_Prod_Prod_inv in hs' as [].
+      eapply substitution_ws_cumul_pb_vass in w1; tea.
+      cbn in w1.
+      pose proof (ws_cumul_pb_trans _ _ _ w1 hres) as X0.
+      eapply ws_cumul_pb_Sort_inv in X0.
+      destruct s => //.
+Qed.

erasure/theories/EConstructorsAsBlocks.v

@@ -87,7 +87,7 @@ Section transform_blocks.
 
   End Def.
 
-  Hint Rewrite @map_InP_spec : transform_blocks.
+  Hint Rewrite @map_primIn_spec @map_InP_spec : transform_blocks.
 
   Arguments eqb : simpl never.
 
@@ -428,6 +428,8 @@ Section transform_blocks.
 
 End transform_blocks.
 
+Global Hint Rewrite @map_primIn_spec @map_InP_spec : transform_blocks.
+
 Definition transform_blocks_constant_decl Σ cb :=
   {| cst_body := option_map (transform_blocks Σ) cb.(cst_body) |}.
 
@@ -985,7 +987,7 @@ Proof.
     + unfold constructor_isprop_pars_decl.
       rewrite lookup_constructor_transform_blocks. cbn [fst].
       rewrite eqc //= H8 //.
-    + now rewrite map_InP_spec nth_error_map H3; eauto.
+    + now rewrite nth_error_map H3; eauto.
     + len.
     + rewrite H9. len.
     + rewrite wellformed_mkApps in i4 => //.
@@ -1014,8 +1016,7 @@ Proof.
       * eauto.
       * revert e1.  set (x := transform_blocks Σ f5).
         simp transform_blocks.
-      * rewrite map_InP_spec.
-        cbn in i8. unfold wf_fix in i8. rtoProp.
+      * cbn in i8. unfold wf_fix in i8. rtoProp.
         erewrite <- transform_blocks_cunfold_fix => //.
         all: eauto.
         eapply closed_fix_subst. solve_all. destruct x; cbn in H5 |- *. eauto.
@@ -1049,7 +1050,7 @@ Proof.
   - simp transform_blocks. rewrite -!transform_blocks_equation_1.
     rewrite transform_blocks_mkApps //=.
     simp transform_blocks. rewrite -!transform_blocks_equation_1.
-    rewrite !map_InP_spec. cbn [plus].
+    cbn [plus].
     intros.
     destruct H3 as [ev wf eta etad].
     destruct H6.
@@ -1062,7 +1063,7 @@ Proof.
     now rewrite transform_blocks_mkApps_eta_fn in e.
   - intros; repeat match goal with [H : MCProd.and5 _ _ _ _ _ |- _] => destruct H end.
     rewrite transform_blocks_mkApps //= in e0.
-    simp transform_blocks in e0. rewrite -!transform_blocks_equation_1 map_InP_spec in e0. simpl in e0.
+    simp transform_blocks in e0. rewrite -!transform_blocks_equation_1 in e0. simpl in e0.
     simp transform_blocks. rewrite -!transform_blocks_equation_1.
     move: i; rewrite /= wellformed_mkApps //. move/and3P => [] hasp wffn wfargs.
     move: i4; rewrite /= wellformed_mkApps //. move/andP => [] wfcof _.
@@ -1174,6 +1175,11 @@ Proof.
     unfold cstr_arity. cbn. rewrite H4; len.
     solve_all. clear -X0. eapply All2_All2_Set. solve_all.
     match goal with H : _ |- _ => apply H end.
+  - intros X; depelim X; simp transform_blocks; repeat constructor.
+    destruct a0.
+    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. 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

@@ -345,6 +345,8 @@ Proof.
     now constructor.
   - congruence.
   - depelim er. now constructor.
+  - depelim er; depelim X; constructor; eauto.
+    eapply All2_over_undep in a0. solve_all.
   - easy.
 Qed.