Adapted all of PCUIC to primitive arrays (and in general term contain…

…ers in primitives)

pcuic/theories/Bidirectional/BDFromPCUIC.v

@@ -377,7 +377,15 @@ Proof.
 
   - intros p prim_ty cdecl wfΓ' hp hdecl pinv.
     eexists. split; [econstructor; tea|].
+    destruct X0. 1-2:constructor; eauto.
+    eapply conv_check in hty; tea.
+    eapply conv_check in hdef; tea.
+    constructor; eauto. solve_all.
+    now eapply conv_check in X0.
     eapply ws_cumul_pb_refl; fvs.
+    depelim X; cbn => //.
+    simp prim_type. cbn.
+    now eapply subject_is_open_term.
 
   - intros ? ? ? ? ? ? (?&?&?) ? (?&?&?) ?.
     eexists.

pcuic/theories/Bidirectional/BDStrengthening.v

@@ -1,5 +1,6 @@
 From Coq Require Import Bool List Arith Lia.
 From Coq Require String.
+From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils monad_utils.
 From MetaCoq.Common Require Import config.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICGlobalEnv
@@ -70,6 +71,7 @@ Proof.
     f_equal.
     1: auto.
     by rewrite map_length ebod shiftnP_shiftn.
+  - solve_all.
 Qed.
 
 Lemma Alli_impl_le {A P Q} {l : list A} {n} :
@@ -470,7 +472,8 @@ Section OnFreeVars.
       cbn in Hmfix.
       by move: Hmfix => /andP [].
 
-    - easy.
+    - intros. red. intros. destruct X1; cbn => //.
+      simp prim_type. cbn in *. solve_all.
     - easy.
 
     - intros ? ? ? ? ? ? _ HT Hred.
@@ -865,7 +868,11 @@ Proof using wfΣ.
     + by apply rename_wf_cofixpoint.
 
   - intros. red. intros P Δ f hf ht.
-    cbn. econstructor; tea.
+    cbn. rewrite rename_prim_type. econstructor; tea; rewrite ?prim_val_tag_map //.
+    destruct X1; cbn in *; constructor; cbn; eauto.
+    * eapply hty; tea; solve_all.
+    * eapply hdef; tea; solve_all.
+    * solve_all.
 
   - intros. red. intros P Δ f hf ht.
     econstructor ; eauto.
@@ -994,17 +1001,17 @@ Proof.
   move: (tyt) => /typing_wf_local wfΓ.
   move: (tyt) => /typing_infering [T' [inf cum]].
   unshelve epose proof (infering_on_free_vars _ _ _ _ _ _ _ _ inf); eauto.
-  pose proof (inf' := inf). apply infering_typing in inf; eauto. 
-  exists T'. split; eauto.  
+  pose proof (inf' := inf). apply infering_typing in inf; eauto.
+  exists T'. split; eauto.
   eapply ws_cumul_pb_forget_cumul; eauto.
   eapply bidirectional_renaming in inf'; eauto.  eapply infering_typing; eauto.
 Qed.
 
 Lemma strengthening `{cf: checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ Γ' Γ'' t T :
   Σ ;;; Γ ,,, Γ' ,,, lift_context #|Γ'| 0 Γ'' |- lift #|Γ'| #|Γ''| t : T ->
-  ∑ T', [× on_free_vars (strengthenP #|Γ''| #|Γ'| xpredT) T', 
+  ∑ T', [× on_free_vars (strengthenP #|Γ''| #|Γ'| xpredT) T',
         (Σ ;;; Γ ,,, Γ' ,,, lift_context #|Γ'| 0 Γ'' |- lift #|Γ'| #|Γ''|  t : T') ,
-        (Σ ;;; Γ ,,, Γ' ,,, lift_context #|Γ'| 0 Γ'' |- T' <= T) & 
+        (Σ ;;; Γ ,,, Γ' ,,, lift_context #|Γ'| 0 Γ'' |- T' <= T) &
         (Σ ;;;  Γ ,,, Γ'' |- t : unlift #|Γ'| #|Γ''| T')].
 Proof.
   intros Hty.
@@ -1037,9 +1044,9 @@ Proof.
   }
 
   eapply typing_renaming_cond_P in Hty as [T' [? ?]]; eauto.
-  exists T'. split; eauto. 
-  - erewrite <- (lift_unlift_term t); eauto. 
-  - split; eauto. eapply urenaming_strengthen. 
+  exists T'. split; eauto.
+  - erewrite <- (lift_unlift_term t); eauto.
+  - split; eauto. eapply urenaming_strengthen.
   - move: wfΓ'' => /wf_local_closed_context.
     rewrite on_free_vars_ctx_app => /andP [? ?].
     apply on_ctx_free_vars_strengthenP.
@@ -1056,31 +1063,31 @@ Qed.
 
 
 Lemma strengthening_type `{cf: checker_flags} {Σ : global_env_ext} {wfΣ : PCUICTyping.wf Σ} Γ Γ' Γ'' t s :
-  Σ ;;; Γ ,,, Γ' ,,, lift_context #|Γ'| 0 Γ'' |- lift #|Γ'| #|Γ''| t : tSort s -> 
+  Σ ;;; Γ ,,, Γ' ,,, lift_context #|Γ'| 0 Γ'' |- lift #|Γ'| #|Γ''| t : tSort s ->
   ∑ s', (Σ ;;; Γ ,,, Γ'' |- t : tSort s') * (compare_universe Cumul Σ s' s).
-Proof. 
+Proof.
   intros H; pose proof (H' := H); eapply strengthening in H. destruct H as [T' [? HT Hcumul HT']].
   pose proof (Hcumul' := Hcumul).
   pose proof (type_closed HT).
   eapply closedn_on_free_vars in H.
   pose proof (type_closed HT').
   eapply closedn_on_free_vars in H0.
   pose proof (wf_local_closed_context (typing_wf_local H')).
-  eapply into_ws_cumul_pb in Hcumul; eauto. 
+  eapply into_ws_cumul_pb in Hcumul; eauto.
   eapply PCUICConversion.ws_cumul_pb_Sort_r_inv in Hcumul as [s' [Hred Hcumul]].
-  eapply closed_red_red in Hred. pose proof (HT'':=HT'). eapply PCUICValidity.validity in HT' as [? ?]. 
+  eapply closed_red_red in Hred. pose proof (HT'':=HT'). eapply PCUICValidity.validity in HT' as [? ?].
   exists s'; split; eauto.
   assert (PCUICReduction.red Σ (Γ,,, Γ'') (unlift #|Γ'| #|Γ''| T') (tSort s')).
   { assert (tSort s' = unlift #|Γ'| #|Γ''| (tSort s')) by reflexivity. rewrite H2; clear H2.
     eapply red_rename. eauto. eapply (urenaming_strengthen _ _ _ _); eauto.
-    2-3: eauto. eapply typing_wf_local in HT''. 
+    2-3: eauto. eapply typing_wf_local in HT''.
     eapply wf_local_closed_context in HT''. revert HT''.
     rewrite on_free_vars_ctx_app => /andP [? ?].
     apply on_ctx_free_vars_strengthenP.
     all: eapply on_free_vars_ctx_on_ctx_free_vars_xpredT; eauto.
-  } 
+  }
   eapply type_Cumul; eauto. eapply PCUICSR.subject_reduction; eauto.
   assert (liftSort : unlift #|Γ'| #|Γ''| (tSort s') = tSort s') by reflexivity. rewrite <- liftSort; clear liftSort.
   eapply PCUICConversion.cumulAlgo_cumulSpec. eapply PCUICConversion.ws_cumul_pb_red_r_inv; eauto.
-  eapply ws_cumul_pb_refl; eauto. eapply PCUICInversion.typing_closed_ctx; eauto. 
+  eapply ws_cumul_pb_refl; eauto. eapply PCUICInversion.typing_closed_ctx; eauto.
 Qed.

pcuic/theories/Bidirectional/BDToPCUIC.v

@@ -416,7 +416,11 @@ Section BDToPCUICTyping.
         all: auto.
 
     - red; intros.
-      now econstructor.
+      econstructor; eauto.
+      depelim X1; constructor; eauto.
+      eapply hty; eauto. eexists. econstructor; eauto.
+      eapply hdef; eauto. eexists; eauto. eapply hty; eauto. eexists; econstructor; eauto.
+      solve_all. eapply X7; eauto. eexists. eapply hty; eauto. eexists; econstructor; eauto.
 
     - red ; intros.
       now eapply type_reduction.

pcuic/theories/Bidirectional/BDUnique.v

@@ -236,12 +236,12 @@ Proof using wfΣ.
       * fvs.
       * now eapply type_is_open_term, infering_typing.
 
-  - inversion X1; subst.
-    rewrite H in H2; noconf H2.
-    unshelve eapply declared_constant_to_gen in H0, H3; eauto.
-    have eq := (declared_constant_inj _ _ H0 H3); subst cdecl0.
-    exists (tConst prim_ty []).
-    split; eapply closed_red_refl; fvs.
+  - depelim X1; depelim X0.
+    * depelim X3. rewrite e in H; noconf H. eexists. split; eapply closed_red_refl; fvs.
+    * depelim X3. rewrite e in H; noconf H. eexists. split; eapply closed_red_refl; fvs.
+    * depelim X3. rewrite e in H; noconf H. eexists. split; eapply closed_red_refl; fvs.
+      all:simp prim_type; cbn. cbn in hty.
+      all:eapply type_is_open_term, checking_typing; tea; eexists; eapply checking_typing; tea; eexists; econstructor; tea.
 
   - inversion X3 ; subst.
     eapply X0 in X4 as [T'' []]; subst ; tea.

pcuic/theories/Conversion/PCUICInstConv.v

@@ -1914,7 +1914,7 @@ Proof using Type.
     generalize #|m|. intro k.
     eapply All2_map. simpl. solve_all.
   - simpl. constructor.
-    eapply onPrim_map_prop; tea. cbn; intuition eauto.
+    eapply onPrims_map_prop; tea. cbn; intuition eauto.
 Qed.
 
 Lemma inst_conv {Σ : global_env_ext} {wfΣ : wf Σ} {Γ Δ σ A B} :

pcuic/theories/Conversion/PCUICRenameConv.v

@@ -2,7 +2,7 @@
 From Coq Require Import Morphisms.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config.
-From MetaCoq.PCUIC Require Import PCUICAst PCUICOnOne PCUICAstUtils PCUICCases PCUICInduction
+From MetaCoq.PCUIC Require Import PCUICPrimitive PCUICAst PCUICOnOne PCUICAstUtils PCUICCases PCUICInduction
   PCUICLiftSubst PCUICUnivSubst PCUICCumulativity
   PCUICReduction PCUICGlobalEnv PCUICClosed PCUICEquality PCUICRenameDef PCUICWeakeningEnvConv
   PCUICSigmaCalculus PCUICClosed PCUICOnFreeVars PCUICGuardCondition
@@ -263,7 +263,7 @@ Proof using Type.
       * unfold map_def. intuition eauto.
       * eauto.
   - simpl. constructor.
-    eapply onPrim_map_prop; tea. cbn; intuition eauto.
+    eapply onPrims_map_prop; tea. cbn; intuition eauto.
 Qed.
 
 Lemma urenaming_impl :

pcuic/theories/PCUICAst.v

@@ -238,38 +238,6 @@ Definition isLambda t :=
 Lemma isLambda_inv t : isLambda t -> exists na ty bod, t = tLambda na ty bod.
 Proof. destruct t => //; eauto. Qed.
 
-Set Equations Transparent.
-
-Definition mapu_array_model {term term'} (fl : Level.t -> Level.t) (f : term -> term')
-  (ar : array_model term) : array_model term' :=
-  {| array_level := fl ar.(array_level);
-      array_value := map f ar.(array_value);
-      array_default := f ar.(array_default);
-      array_type := f ar.(array_type) |}.
-
-Equations mapu_prim {term term'} (f : Level.t -> Level.t) (g : term -> term')
-  (p : PCUICPrimitive.prim_val term) : PCUICPrimitive.prim_val term' :=
-| _, _, (primInt; primIntModel i) => (primInt; primIntModel i)
-| _, _, (primFloat; primFloatModel fl) => (primFloat; primFloatModel fl)
-| f, g, (primArray; primArrayModel ar) =>
-  (primArray; primArrayModel (mapu_array_model f g ar)).
-
-Notation map_array_model := (mapu_array_model id).
-Notation map_prim := (mapu_prim id).
-
-Equations test_prim (p : term -> bool) (p : prim_val) : bool :=
-| p, (primInt; _) => true
-| p, (primFloat; _) => true
-| p, (primArray; primArrayModel ar) =>
-  List.forallb p ar.(array_value) && p ar.(array_default) && p ar.(array_type).
-
-Equations test_primu (p : Level.t -> bool) (t : term -> bool) (p : prim_val) : bool :=
-| _, _, (primInt; _) => true
-| _, _, (primFloat; _) => true
-| p, pt, (primArray; primArrayModel ar) =>
-  p ar.(array_level) && forallb pt ar.(array_value) &&
-  pt ar.(array_default) && pt ar.(array_type).
-
 (** Basic operations on the AST: lifting, substitution and tests for variable occurrences. *)
 
 Fixpoint lift n k t : term :=
@@ -982,13 +950,6 @@ Proof.
   destruct p as [? []] => //.
 Qed.
 
-Definition tPrimProp {term} (P : term -> Type) (p : PCUICPrimitive.prim_val term) : Type :=
-  match p.π2 return Type with
-  | primIntModel f => unit
-  | primFloatModel f => unit
-  | primArrayModel a => P a.(array_type) × P a.(array_default) × All P a.(array_value)
-  end.
-
 Lemma mapu_array_model_proper {term term'} (l l' : Level.t -> Level.t) (f g : term -> term') a :
   l =1 l' -> f =1 g ->
   mapu_array_model l f a = mapu_array_model l' g a.
@@ -1027,7 +988,7 @@ Proof.
   destruct a => //=. rewrite /mapu_array_model /=. rewrite map_id //.
 Qed.
 
-Lemma test_prim_primProp {P p} : test_prim P p -> tPrimProp P p.
+Lemma test_prim_primProp {term} {P p} : @test_prim term P p -> tPrimProp P p.
 Proof.
   destruct p as [? []]; cbn => //.
   move/andP => [] /andP[]. intuition auto.
@@ -1095,7 +1056,7 @@ Proof.
   eapply All_forallb, All_map, All_impl; tea. intuition eauto. apply hg; intuition auto.
 Qed.
 
-Lemma test_prim_mapu {put l f p} :
+Lemma test_prim_mapu {term term'} {put : term' -> bool} {l} {f : term -> term'} {p} :
   test_prim put (mapu_prim l f p) = test_prim (fun x => put (f x)) p.
 Proof.
   destruct p as [? []]; cbn; eauto.