Adapt evaluation to primitive arrays (up-to PCUICProgress)

pcuic/theories/PCUICClassification.v

@@ -581,7 +581,7 @@ Proof.
   intros axfree.
   cut (Forall is_true []); [|constructor].
   generalize ([] : list bool).
-  induction t; intros axfree_args all_true; cbn; auto.
+  induction t using term_forall_list_ind; intros axfree_args all_true; cbn; auto.
   - destruct lookup_env eqn:find; auto.
     destruct g; auto.
     destruct c; auto.
@@ -615,6 +615,7 @@ Section classification.
       left ; eexists; split; eauto.
       now rewrite nth_error_nil.
     - eapply (whnf_cofixapp _ _ [] _ _ []).
+    - eapply whnf_prim.
     - destruct X => //.
       pose proof cl as cl'.
       rewrite closedn_mkApps in cl'. move/andP: cl' => [clfix _].
@@ -892,6 +893,7 @@ Section classification.
       cbn.
       destruct ?; auto.
       destruct ?; auto.
+    - cbn. constructor.
     - rewrite axiom_free_value_mkApps.
       rewrite app_nil_r.
       destruct X; try constructor.
@@ -916,7 +918,7 @@ Section classification.
   Proof.
     intros Hc He.
     revert ty Hc.
-    induction He; simpl; move=> ty Ht;
+    induction He using eval_rect_all; simpl; move=> ty Ht;
       try solve[econstructor; eauto].
 
     - eapply inversion_App in Ht as (? & ? & ? & ? & ? & ?); auto.
@@ -982,7 +984,7 @@ Section classification.
         eapply All2_refl; split; reflexivity.
         eapply red1_red. destruct p => /= //.
         eapply red_iota; tea.
-        rewrite e0 /cstr_arity eq_npars e2 //. }
+        rewrite e1 /cstr_arity eq_npars e3 //. }
       specialize (X X0).
       redt _; eauto.
 
@@ -1002,18 +1004,18 @@ Section classification.
       specialize (IHHe2 _ t0).
       epose proof (subject_reduction Σ [] _ _ _ wfΣ t IHHe1) as Ht2.
       epose proof (subject_reduction Σ [] _ _ _ wfΣ t0 IHHe2) as Ha2.
-      assert (red Σ [] (tApp f a) (tApp (mkApps fn argsv) av)).
+      assert (red Σ [] (tApp f4 a) (tApp (mkApps fn argsv) av)).
       { redt _.
         eapply red_app; eauto.
         rewrite -![tApp _ _](mkApps_app _ _ [_]).
         eapply red1_red.
-        rewrite -closed_unfold_fix_cunfold_eq in e.
+        rewrite -closed_unfold_fix_cunfold_eq in e1.
         { eapply subject_closed in Ht2; auto.
           rewrite closedn_mkApps in Ht2. now move/andP: Ht2 => [clf _]. }
         eapply red_fix; eauto.
         assert (Σ ;;; [] |- mkApps (tFix mfix idx) (argsv ++ [av]) : B {0 := av}).
         { rewrite mkApps_app /=. eapply type_App'; eauto. }
-        epose proof (fix_app_is_constructor X0 e); eauto.
+        epose proof (fix_app_is_constructor X0 e1); eauto.
         rewrite /is_constructor.
         destruct nth_error eqn:hnth => //.
         2:{ eapply nth_error_None in hnth. len in hnth. }
@@ -1077,6 +1079,12 @@ Section classification.
       specialize (IHHe1 _ Hf).
       specialize (IHHe2 _ Ha).
       now eapply red_app.
+
+    - eapply inversion_Prim in Ht as [prim_type [decl []]]; eauto.
+      depelim X. 1-2:reflexivity.
+      depelim p1. specialize (r _ hdef).
+      eapply red_primArray_congr; eauto.
+      eapply All2_undep in a. solve_all.
   Qed.
 
   Theorem subject_reduction_eval {t u T} :

pcuic/theories/PCUICProgress.v

@@ -535,7 +535,7 @@ Qed.
 Lemma value_mkApps_inv' Σ f args :
   negb (isApp f) ->
   value Σ (mkApps f args) ->
-  atom f × All (value Σ) args.
+  atomic_value (value Σ) f × All (value Σ) args.
 Proof.
   intros napp. move/value_mkApps_inv => [] => //.
   - intros [-> hf]. split => //.
@@ -596,7 +596,7 @@ Proof.
   destruct (value_mkApps_inv' _ _ _ napp vapp).
   eapply PCUICSpine.inversion_mkApps_direct in ht' as [A' [u [hfn [hhd hcum]]]]; tea.
   2:{ now eapply validity. }
-  destruct fn => //.
+  destruct fn => //; try depelim a; cbn in * => //.
   * eapply inversion_Sort in hfn as [? [? cu]]; tea.
     eapply typing_spine_strengthen in hcum. 3:tea. 2:{ eapply validity; econstructor; eauto. }
     now eapply typing_spine_sort, app_tip_nil in hcum.
@@ -606,7 +606,7 @@ Proof.
   * (* Lambda *) left. destruct args.
     - cbn. eexists. now eapply wcbv_red_beta.
     - eexists. rewrite mkApps_app. rewrite (mkApps_app _ [t] args). do 2 eapply wcbv_red1_mkApps_left.
-      cbn. eapply wcbv_red_beta. now depelim a.
+      cbn. eapply wcbv_red_beta. now depelim a0.
   * (* Inductive *)
     eapply inversion_Ind in hfn as [? [? [? [? [? cu]]]]]; tea.
     eapply typing_spine_strengthen in hcum. 3:tea. 2:{ eapply validity. econstructor; eauto. }
@@ -668,6 +668,23 @@ Proof.
   now do 2 rewrite !context_assumptions_subst_context ?context_assumptions_lift_context.
 Qed.
 
+#[global] Hint Constructors atomic_value : wcbv.
+
+Lemma All_or_disj {A} (P Q : A -> Type) l : All (fun x => P x + Q x)%type l ->
+  (∑ n v, All Q (firstn n l) × (nth_error l n = Some v × P v)) + All Q l.
+Proof.
+  induction 1.
+  - right; auto.
+  - destruct IHX.
+    * destruct s as [n [v [? []]]].
+      destruct p.
+      + left. exists 0, x; intuition auto.
+      + left. exists (S n), v; intuition cbn; auto.
+    * destruct p.
+      + left. exists 0, x; intuition auto.
+      + right; eauto.
+Qed.
+
 Lemma progress_env_prop `{cf : checker_flags}:
   env_prop (fun Σ Γ t T => axiom_free Σ -> Γ = [] -> Σ ;;; Γ |- t : T -> {t' & Σ ⊢ t ⇝ᵥ t'} + (value Σ t))
            (fun _ _ => True).
@@ -751,6 +768,22 @@ Proof with eauto with wcbv; try congruence.
       eapply inversion_CoFix in t as (? & ? & ? & ? & ? & ? & ?); eauto.
       eexists. eapply wcbv_red_cofix_proj. unfold cunfold_cofix. rewrite e0. reflexivity.
       eapply value_mkApps_inv in Hval as [[-> ]|[]]; eauto.
+  - intros Σ wfΣ Γ _ p c u mdecl idecl cdecl pdecl Hcon args Hargs -> hp.
+    depelim args... 1-2:right; constructor; constructor 2; constructor.
+    depelim Hcon.
+    destruct hdef; eauto.
+    + left. destruct s as [t' hred]. exists (tPrim (prim_array (set_array_default a t'))). now constructor.
+    + destruct a as []; cbn in *.
+      clear hty.
+      solve_all. clear -hvalue0 Hargs v.
+      set (a := {| array_level := _ |}).
+      assert (All (fun x : term => ((∑ t' : term, Σ ⊢ x ⇝ᵥ t') + value Σ x))%type array_value).
+      { solve_all. } clear hvalue0 Hargs.
+      eapply All_or_disj in X as [].
+      * destruct s as [n [v' [? []]]]. destruct s as [t' ht'].
+        left. exists (tPrim (prim_array (set_array_value a (firstn n array_value ++ t' :: skipn (S n) array_value)))).
+        econstructor; eauto.
+      * right. constructor. constructor 2. constructor; eauto.
 Qed.
 
 Lemma progress `{cf : checker_flags}: