Done with template <-> PCUIC. Working on safe checker

.vscode/metacoq.code-workspace

@@ -11,31 +11,64 @@
 
 
 
-			"-R", "safechecker-plugin/theories", "MetaCoq.SafeCheckerPlugin",
+			"-R", "safechecker-plugin/theories,MetaCoq.SafeCheckerPlugin",
 
-			"-R", "utils/theories", "MetaCoq.Utils",
-			"-R", "common/theories", "MetaCoq.Common",
-			"-R", "template-pcuic/theories", "MetaCoq.TemplatePCUIC",
+			"-R", "utils/theories,MetaCoq.Utils",
+			"-R", "common/theories,MetaCoq.Common",
+			"-R", "template-pcuic/theories,MetaCoq.TemplatePCUIC",
 
-		"-I", "template-coq",
+		"-I template-coq",
     	//	"-bt", get backtraces from Coq on errors
-		"-I", "template-coq/build",
-		"-R", "template-coq/theories", "MetaCoq.Template",
-		"-R", "examples", "MetaCoq.Examples",
-		"-R", "checker/theories", "MetaCoq.Checker",
-		"-R", "pcuic/theories", "MetaCoq.PCUIC",
-		"-I", "safechecker/src",
-		"-R", "safechecker/theories", "MetaCoq.SafeChecker",
-		"-I", "erasure/src",
-		"-R", "erasure/theories", "MetaCoq.Erasure",
-		"-R", "erasure-plugin/theories", "MetaCoq.ErasurePlugin",
-		"-R", "translations", "MetaCoq.Translations",
-		"-R", "test-suite/plugin-demo/theories", "MetaCoq.ExtractedPluginDemo",
-		"-R", "test-suite", "MetaCoq.TestSuite"
+		"-I template-coq/build",
+		"-R", "template-coq/theories,MetaCoq.Template",
+		"-R", "examples,MetaCoq.Examples",
+		"-R", "checker/theories,MetaCoq.Checker",
+		"-R", "pcuic/theories,MetaCoq.PCUIC",
+		"-I safechecker/src",
+		"-R", "safechecker/theories,MetaCoq.SafeChecker",
+		"-I erasure/src",
+		"-R", "erasure/theories,MetaCoq.Erasure",
+		"-R", "erasure-plugin/theories,MetaCoq.ErasurePlugin",
+		"-R", "translations,MetaCoq.Translations",
+		"-R", "test-suite/plugin-demo/theories,MetaCoq.ExtractedPluginDemo",
+		"-R", "test-suite,MetaCoq.TestSuite"
 	    ],
 
 	 // When enabled, will trim trailing whitespace when saving a file.
 	"files.trimTrailingWhitespace": true,
-	"coqtop.binPath": "_opam/bin"
+	"coqtop.binPath": "_opam/bin",
+	"files.exclude": {
+		"**/*.vo": true,
+		"**/*.vok": true,
+		"**/*.vos": true,
+		"**/*.aux": true,
+		"**/*.glob": true,
+		"**/.git": true,
+		"**/.svn": true,
+		"**/.hg": true,
+		"**/CVS": true,
+		"**/.DS_Store": true,
+		"**/Thumbs.db": true
+	},
+	"coq-lsp.args": [
+	"-R", "safechecker-plugin/theories,MetaCoq.SafeCheckerPlugin",
+	"-R", "utils/theories,MetaCoq.Utils",
+		"-R", "common/theories,MetaCoq.Common",
+		"-R", "template-pcuic/theories,MetaCoq.TemplatePCUIC",
+
+	"-I", "template-coq",
+		//"-bt", // get backtraces from Coq on errors
+	//"-Itemplate-coq/build",
+	"-R", "template-coq/theories,MetaCoq.Template",
+	"-R", "examples,MetaCoq.Examples",
+	"-R", "pcuic/theories,MetaCoq.PCUIC",
+	"-R", "safechecker/theories,MetaCoq.SafeChecker",
+	"-R", "erasure/theories,MetaCoq.Erasure",
+	"-R", "erasure-plugin/theories,MetaCoq.ErasurePlugin",
+	"-R", "translations,MetaCoq.Translations",
+	"-R", "test-suite/plugin-demo/theories,MetaCoq.ExtractedPluginDemo",
+	"-R", "test-suite,MetaCoq.TestSuite"
+	],
+	"coq-lsp.path": "_opam/bin/coq-lsp"
     }
 }

pcuic/theories/Syntax/PCUICPosition.v

@@ -47,7 +47,10 @@ Inductive choice :=
 | prod_r
 | let_bd
 | let_ty
-| let_in.
+| let_in
+| array_def
+| array_ty
+| array_val (n : nat).
 
 Derive NoConfusion NoConfusionHom EqDec for choice.
 
@@ -115,6 +118,13 @@ Fixpoint validpos t (p : position) {struct p} :=
     | let_bd, tLetIn na b B t => validpos b p
     | let_ty, tLetIn na b B t => validpos B p
     | let_in, tLetIn na b B t => validpos t p
+    | array_def, tPrim (primArray; primArrayModel a) => validpos (array_default a) p
+    | array_ty, tPrim (primArray; primArrayModel a) => validpos (array_type a) p
+    | array_val n, tPrim (primArray; primArrayModel a) =>
+      match nth_error (array_value a) n with
+      | Some d => validpos d p
+      | None => false
+      end
     | _, _ => false
     end
   end.
@@ -253,6 +263,11 @@ Proof.
       * simpl in *. apply some_inj in e. subst.
         destruct y as [na' ty' bo' ra']. simpl in *. intuition eauto.
       * simpl in *. eapply IHa. all: eauto.
+    + depelim e. depelim o; eauto.
+    + depelim e; depelim o; eauto.
+    + depelim e. depelim o; eauto.
+      cbn in vp. destruct (nth_error (array_value a) n) eqn:e'; try discriminate.
+      cbn. eapply All2_nth_error_Some in a0 as [t' [-> ?]]; tea. eapply ih; tea.
 Qed.
 
 Lemma eq_term_valid_pos :
@@ -690,6 +705,34 @@ Proof.
         unshelve eapply Acc_cofix_mfix_bd with (1 := e1) (p := exist q _).
         -- simpl. rewrite e1 in e. assumption.
         -- eapply ihm.
+  - destruct q as [q e]. destruct q as [| c q].
+    + constructor. intros [p' e'] h.
+      unfold posR in h. cbn in h.
+      dependent destruction h.
+      destruct p as [? []];
+      destruct c. all: noconf e'.
+      * simpl in e'.
+        case_eq (nth_error m n0).
+        2:{ intro h. pose proof e' as hh. rewrite h in hh. discriminate. }
+        intros [na ty bo ra] e1.
+        eapply All_nth_error in X as ihm. 2: exact e1.
+        simpl in ihm.
+        unshelve eapply Acc_cofix_mfix_ty with (1 := e1) (p := exist p _).
+        -- simpl. rewrite e1 in e'. assumption.
+        -- eapply ihm.
+      * simpl in e'.
+        case_eq (nth_error m n0).
+        2:{ intro h. pose proof e' as hh. rewrite h in hh. discriminate. }
+        intros [na ty bo ra] e1.
+        eapply All_nth_error in X as ihm. 2: exact e1.
+        simpl in ihm.
+        unshelve eapply Acc_cofix_mfix_bd with (1 := e1) (p := exist p _).
+        -- simpl. rewrite e1 in e'. assumption.
+        -- eapply ihm.
+
+
+    destruct p as [? []]; cbn in X, e; intuition eauto; cbn in e.
+    + destruct x eqn:hp; try discriminate; cbn in e. constructor.
 Qed.
 
 Fixpoint atpos t (p : position) {struct p} : term :=
@@ -933,7 +976,11 @@ Variant stack_entry : Type :=
 | Lambda_bd (na : aname) (A : term)
 | LetIn_bd (na : aname) (B t : term)
 | LetIn_ty (na : aname) (b t : term)
-| LetIn_in (na : aname) (b B : term).
+| LetIn_in (na : aname) (b B : term)
+| PrimArray_ty (l : Level.t) (l : list term) (def : term)
+| PrimArray_def (l : Level.t) (l : list term) (ty : term)
+(* Hole in one of the values *)
+| PrimArray_val (l : Level.t) (bef : list term) (after : list term) (def : term) (ty : term).
 
 Definition stack := list stack_entry.
 
@@ -1029,6 +1076,9 @@ Definition fill_hole (t : term) (se : stack_entry) : term :=
   | LetIn_bd na B u => tLetIn na t B u
   | LetIn_ty na b u => tLetIn na b t u
   | LetIn_in na b B => tLetIn na b B t
+  | PrimArray_def l v ty => tPrim (primArray; primArrayModel {| array_level := l; array_value := v; array_default := t; array_type := ty |})
+  | PrimArray_ty l v def => tPrim (primArray; primArrayModel {| array_level := l; array_value := v; array_default := def; array_type := t |})
+  | PrimArray_val l bef after def ty => tPrim (primArray; primArrayModel {| array_level := l; array_value := bef ++ (t :: after); array_default := def; array_type := ty |})
   end.
 
 (* Not using fold_left here to get the right unfolding behavior *)
@@ -1307,6 +1357,9 @@ Definition closedn_stack_entry k se :=
   | LetIn_bd na B u => closedn k B && closedn (S k) u
   | LetIn_ty na b u => closedn k b && closedn (S k) u
   | LetIn_in na b B => closedn k b && closedn k B
+  | PrimArray_def l v ty => forallb (closedn k) v && closedn k ty
+  | PrimArray_ty l v def => forallb (closedn k) v && closedn k def
+  | PrimArray_val l bef after def ty => forallb (closedn k) bef && forallb (closedn k) after && closedn k def && closedn k ty
   end.
 
 Fixpoint closedn_stack k π :=

pcuic/theories/Syntax/PCUICReflect.v

@@ -115,7 +115,7 @@ Fixpoint eqb_term (u v : term) : bool :=
       eqb x.(rarg) y.(rarg) &&
       eqb x.(dname) y.(dname)) mfix mfix'
 
-  | tPrim p, tPrim p' => @eqb_prim_val _ eqb_term p p'
+  | tPrim p, tPrim p' => @eqb_prim_val _ eqb eqb_term p p'
   | _, _ => false
   end.
 

pcuic/theories/utils/PCUICPrimitive.v

@@ -78,15 +78,15 @@ Instance reflect_eq_spec_float : ReflectEq SpecFloat.spec_float := EqDec_Reflect
 
 Import ReflectEq.
 
-Definition eqb_array {term} {eqt : term -> term -> bool} (x y : array_model term) : bool :=
-   eqb x.(array_level) y.(array_level) &&
+Definition eqb_array {term} {equ : Level.t -> Level.t -> bool} {eqt : term -> term -> bool} (x y : array_model term) : bool :=
+   equ x.(array_level) y.(array_level) &&
    forallb2 eqt x.(array_value) y.(array_value) &&
    eqt x.(array_default) y.(array_default) &&
    eqt x.(array_type) y.(array_type).
 
 #[program,global]
 Instance reflect_eq_array {term} {req : ReflectEq term}: ReflectEq (array_model term) :=
-  { eqb := eqb_array (eqt := eqb) }.
+  { eqb := eqb_array (equ := eqb) (eqt := eqb) }.
 Next Obligation.
   intros term req [] []; cbn. unfold eqb_array. cbn.
   change (forallb2 eqb) with (eqb (A := list term)).
@@ -97,14 +97,14 @@ Next Obligation.
   all:constructor; congruence.
 Qed.
 
-Equations eqb_prim_model {term} {req : term -> term -> bool} {t : prim_tag} (x y : prim_model term t) : bool :=
+Equations eqb_prim_model {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} {t : prim_tag} (x y : prim_model term t) : bool :=
   | primIntModel x, primIntModel y := ReflectEq.eqb x y
   | primFloatModel x, primFloatModel y := ReflectEq.eqb x y
-  | primArrayModel x, primArrayModel y := eqb_array (eqt:=req) x y.
+  | primArrayModel x, primArrayModel y := eqb_array (equ := equ) (eqt:=req) x y.
 
 #[global, program]
 Instance prim_model_reflecteq {term} {req : ReflectEq term} {p : prim_tag} : ReflectEq (prim_model term p) :=
-  {| ReflectEq.eqb := eqb_prim_model (req := eqb) |}.
+  {| ReflectEq.eqb := eqb_prim_model (equ := eqb) (req := eqb) |}.
 Next Obligation.
   intros. depelim x; depelim y; simp eqb_prim_model.
   case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
@@ -116,15 +116,15 @@ Qed.
 #[global]
 Instance prim_model_eqdec {term} {req : ReflectEq term} : forall p : prim_tag, EqDec (prim_model term p) := _.
 
-Equations eqb_prim_val {term} {req : term -> term -> bool} (x y : prim_val term) : bool :=
-  | (primInt; i), (primInt; i') := eqb_prim_model (req := req) i i'
-  | (primFloat; f), (primFloat; f') := eqb_prim_model (req := req) f f'
-  | (primArray; a), (primArray; a') := eqb_prim_model (req := req) a a'
+Equations eqb_prim_val {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} (x y : prim_val term) : bool :=
+  | (primInt; i), (primInt; i') := eqb_prim_model (equ := equ) (req := req) i i'
+  | (primFloat; f), (primFloat; f') := eqb_prim_model (equ := equ) (req := req) f f'
+  | (primArray; a), (primArray; a') := eqb_prim_model (equ := equ) (req := req) a a'
   | x, y := false.
 
 #[global, program]
 Instance prim_val_reflect_eq {term} {req : ReflectEq term} : ReflectEq (prim_val term) :=
-  {| ReflectEq.eqb := eqb_prim_val (req := eqb) |}.
+  {| ReflectEq.eqb := eqb_prim_val (equ := eqb) (req := eqb) |}.
 Next Obligation.
   intros. funelim (eqb_prim_val x y); simp eqb_prim_val.
   change (eqb_prim_model i i') with (eqb i i').

safechecker/theories/PCUICEqualityDec.v

@@ -2,7 +2,7 @@
 From Coq Require Import ProofIrrelevance ssreflect ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config uGraph.
-From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics
+From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICPrimitive PCUICTactics
      PCUICReflect PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGlobalEnv
      PCUICCumulativity PCUICEquality PCUICWfUniverses
      PCUICInduction.
@@ -158,7 +158,8 @@ Fixpoint eqb_term_upto_univ_napp
       eqb_binder_annot x.(dname) y.(dname)
     ) mfix mfix'
 
-  | tPrim p, tPrim p' => eqb p p'
+  | tPrim p, tPrim p' => eqb_prim_val (equ := fun l l' => equ (Universe.make l) (Universe.make l'))
+    (req := eqb_term_upto_univ_napp equ equ gen_compare_global_instance 0) p p'
 
   | _, _ => false
   end.
@@ -396,6 +397,8 @@ Proof.
     eapply All_impl ; tea.
     move => ? [? ?].
     now apply /andP.
+  - destruct p as [? []]; cbn in *; rtoProp; intuition eauto.
+    solve_all.
 Qed.
 
 Definition reflect_eq_predicate {Σ equ lequ}
@@ -530,6 +533,8 @@ Proof.
   destruct gr; auto; now repeat rewrite hlookup.
 Qed.
 
+Transparent eqb_prim_val eqb_prim_model.
+
 Lemma reflect_eq_term_upto_univ Σ equ lequ
   (p : Universe.t -> bool) (q : nat -> term -> bool)
   (Re Rle : Universe.t -> Universe.t -> Prop)
@@ -754,7 +759,34 @@ Proof.
         constructor. constructor. constructor ; try easy.
         now inversion e3.
 
- - cbn - [eqb]. eqspecs. do 2 constructor.
+ - destruct p0 as [? []], prim as [? []];
+    cbn in X, ht, ht';
+    rewrite /eqb_prim_val /eqb_prim_model; cbn -[eqb]; try eqspecs;
+    try repeat constructor.
+    1-8:intros e; depelim e; try depelim o; intuition eauto.
+    unfold eqb_array. eqspecs; rewrite ?andb_true_r ?andb_false_r.
+    rtoProp; intuition auto. specialize (a1 equ Re 0 he _ H4 H0).
+    specialize (a2 equ Re 0 he _ H5 H1).
+    case: a1; rewrite ?andb_true_r ?andb_false_r; [intros eq|constructor; intros e; depelim e; depelim o]; eauto.
+    case: a2; rewrite ?andb_true_r ?andb_false_r; [intros eq'|constructor; intros e; depelim e; depelim o]; eauto.
+    equspec equ he; eauto; cbn.
+    2:constructor; intros e; depelim e; depelim o; eauto.
+    repeat toAll.
+    revert b0 H2.
+    destruct a as [l d ty v], a0 as [l' d' ty' v']; cbn in *.
+    intros a.
+    induction a in v' |- *; intros.
+    * depelim H2; cbn; constructor; eauto; try repeat constructor; cbn; eauto.
+      intros heq; depelim heq; cbn in *; depelim o; eauto. depelim a0.
+    * intuition auto. depelim H2; cbn; try constructor; eauto.
+      ++ intros heq; depelim heq; depelim o; eauto. depelim a2.
+      ++ specialize (IHa _ H2). case: IHa; intros htl.
+        +++ rewrite andb_true_r. specialize (b equ Re 0 he _ a0 i).
+            case: b; repeat constructor; eauto; depelim htl; depelim o; eauto.
+            intros heq; depelim heq; depelim o; cbn in *; eauto. eapply f. now depelim a3.
+        +++ rewrite andb_false_r; constructor.
+            intros heq; depelim heq; depelim o; cbn in *; eauto. eapply htl.
+            repeat constructor; eauto. cbn. now depelim a2.
 Qed.
 
  Lemma eqb_term_upto_univ_impl (equ lequ : _ -> _ -> bool)
@@ -944,6 +976,9 @@ Proof.
   - eapply forallb_All in wt; eapply All_mix in X; try apply wt; clear wt.
     eapply All_All2; eauto; simpl; intuition eauto;
     apply andb_and in a as [? ?]; eauto.
+  - destruct p as [? []]; cbn -[Universe.make] in X, wt; rtoProp; intuition eauto; constructor; eauto.
+    + eapply hRe. now move/wf_universe_reflect: H.
+    + solve_all. eapply All_All2; eauto; simpl; intuition eauto.
 Defined.
 
 Lemma eqb_term_upto_univ_refl Σ (eqb leqb : Universe.t -> Universe.t -> bool) (Re : Universe.t -> Universe.t -> Prop)