Big change in universes:

  - change the representation of UnivExpr
  - change the representation of universes (sorted, non empty list w/o duplicate)
  - prove completness of the comparison algorithm

Author: SimonBoulier

.gitignore

@@ -357,6 +357,10 @@ pcuic/src/pCUICUtils.mli
 /erasure/src/pCUICSafeRetyping.mli
 /erasure/src/safeErasureFunction.ml
 /erasure/src/safeErasureFunction.mli
+erasure/src/mSetWeakList.ml
+erasure/src/mSetWeakList.mli
+erasure/src/utils.ml
+erasure/src/utils.mli
 
 template-coq/gen-src/cRelationClasses.mli.rej
 .DS_Store

checker/src/metacoq_checker_plugin.mlpack

@@ -1,9 +1,9 @@
-Compare_dec
-MSetList
 EqdepFacts
 Wf
 WGraph
 Monad_utils
+Utils
+MSetWeakList
 UGraph0
 EnvironmentTyping
 Typing0

checker/theories/Checker.v

@@ -546,7 +546,7 @@ Section Typecheck.
     | None => raise (NotEnoughFuel fuel)
     end.
 
-  Definition reduce_to_sort Γ (t : term) : typing_result universe :=
+  Definition reduce_to_sort Γ (t : term) : typing_result Universe.t :=
     match t with
     | tSort s => ret s
     | _ =>

checker/theories/Closed.v

@@ -26,7 +26,7 @@ Proof.
     rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length, ?Nat.add_assoc;
     simpl closed in *; solve_all;
     unfold compose, test_def, test_snd in *;
-      try solve [simpl lift; simpl closed; f_equal; auto; repeat (toProp; solve_all)]; try easy.
+      try solve [simpl lift; simpl closed; f_equal; auto; repeat (rtoProp; solve_all)]; try easy.
 
   - elim (Nat.leb_spec k' n0); intros. simpl.
     elim (Nat.ltb_spec); auto. apply Nat.ltb_lt in H. lia.
@@ -41,7 +41,7 @@ Proof.
   induction t in n, k, k' |- * using term_forall_list_ind; intros;
     simpl in *;
     rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length, ?Nat.add_assoc in *;
-    simpl closed in *; repeat (toProp; solve_all); try change_Sk;
+    simpl closed in *; repeat (rtoProp; solve_all); try change_Sk;
     unfold compose, test_def, on_snd, test_snd in *; simpl in *; eauto with all.
 
   - revert H0.
@@ -51,8 +51,8 @@ Proof.
   - specialize (IHt2 n (S k) (S k')). eauto with all.
   - specialize (IHt2 n (S k) (S k')). eauto with all.
   - specialize (IHt3 n (S k) (S k')). eauto with all.
-  - toProp. solve_all. specialize (H1 n (#|m| + k) (#|m| + k')). eauto with all.
-  - toProp. solve_all. specialize (H1 n (#|m| + k) (#|m| + k')). eauto with all.
+  - rtoProp. solve_all. specialize (H1 n (#|m| + k) (#|m| + k')). eauto with all.
+  - rtoProp. solve_all. specialize (H1 n (#|m| + k) (#|m| + k')). eauto with all.
 Qed.
 
 Lemma closedn_mkApps k f u:
@@ -85,7 +85,7 @@ Proof.
   induction t in k' |- * using term_forall_list_ind; intros;
     simpl in *;
     rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
-    simpl closed in *; try change_Sk; repeat (toProp; solve_all);
+    simpl closed in *; try change_Sk; repeat (rtoProp; solve_all);
     unfold compose, test_def, on_snd, test_snd in *; simpl in *; eauto with all.
 
   - elim (Nat.leb_spec k' n); intros. simpl.
@@ -105,10 +105,10 @@ Proof.
   - specialize (IHt3 (S k')).
     rewrite <- Nat.add_succ_comm in IHt3. eauto.
   - rewrite closedn_mkApps; solve_all.
-  - toProp; solve_all. rewrite -> !Nat.add_assoc in *.
+  - rtoProp; solve_all. rewrite -> !Nat.add_assoc in *.
     specialize (H0 (#|m| + k')). unfold is_true. rewrite <- H0. f_equal. lia.
     unfold is_true. rewrite <- H2. f_equal. lia.
-  - toProp; solve_all. rewrite -> !Nat.add_assoc in *.
+  - rtoProp; solve_all. rewrite -> !Nat.add_assoc in *.
     specialize (H0 (#|m| + k')). unfold is_true. rewrite <- H0. f_equal. lia.
     unfold is_true. rewrite <- H2. f_equal. lia.
 Qed.
@@ -249,6 +249,7 @@ Proof.
       now rewrite app_length // plus_n_Sm.
 Qed.
 
+
 Lemma typecheck_closed `{cf : checker_flags} :
   env_prop (fun Σ Γ t T =>
               closedn #|Γ| t && closedn #|Γ| T).
@@ -317,7 +318,7 @@ Proof.
       eauto using closed_upwards with arith.
 
   - intuition auto. solve_all. unfold test_snd. simpl in *.
-    toProp; eauto.
+    rtoProp; eauto.
     apply closedn_mkApps; auto.
     rewrite forallb_app. simpl. rewrite H1.
     rewrite forallb_skipn; auto.
@@ -342,26 +343,26 @@ Proof.
 
   - split. solve_all.
     destruct x; simpl in *.
-    unfold test_def. simpl. toProp.
+    unfold test_def. simpl. rtoProp.
     split.
     rewrite -> app_context_length in *. rewrite -> Nat.add_comm in *.
     eapply closedn_lift_inv in H2; eauto. lia.
     subst types.
     now rewrite app_context_length fix_context_length in H1.
-    eapply nth_error_all in H0; eauto. simpl in H0. intuition. toProp.
+    eapply nth_error_all in H0; eauto. simpl in H0. intuition. rtoProp.
     subst types. rewrite app_context_length in H1.
     rewrite Nat.add_comm in H1.
     now eapply closedn_lift_inv in H1.
 
   - split. solve_all. destruct x; simpl in *.
-    unfold test_def. simpl. toProp.
+    unfold test_def. simpl. rtoProp.
     split.
     rewrite -> app_context_length in *. rewrite -> Nat.add_comm in *.
     eapply closedn_lift_inv in H2; eauto. lia.
     subst types.
     now rewrite -> app_context_length, fix_context_length in H1.
     eapply (nth_error_all) in H; eauto. simpl in *.
-    intuition. toProp.
+    intuition. rtoProp.
     subst types. rewrite app_context_length in H1.
     rewrite Nat.add_comm in H1.
     now eapply closedn_lift_inv in H1.
@@ -435,7 +436,7 @@ Proof.
   eapply on_global_env_impl; cycle 1.
   apply (env_prop_sigma _ typecheck_closed _ X).
   red; intros. unfold lift_typing in *. destruct T; intuition auto with wf.
-  destruct X1 as [s0 Hs0]. simpl. toProp; intuition.
+  destruct X1 as [s0 Hs0]. simpl. rtoProp; intuition.
 Qed.
 
 Lemma closed_decl_upwards k d : closed_decl k d -> forall k', k <= k' -> closed_decl k' d.

checker/theories/Reflect.v

@@ -226,13 +226,13 @@ Proof.
   unfold eq_inductive, eqb; cbn. now rewrite eq_string_refl Nat.eqb_refl.
 Defined.
 
-Definition eq_def {A : Set} `{ReflectEq A} (d1 d2 : def A) : bool :=
+Definition eq_def {A} `{ReflectEq A} (d1 d2 : def A) : bool :=
   match d1, d2 with
   | mkdef n1 t1 b1 a1, mkdef n2 t2 b2 a2 =>
     eqb n1 n2 && eqb t1 t2 && eqb b1 b2 && eqb a1 a2
   end.
 
-#[program] Instance reflect_def : forall {A : Set} `{ReflectEq A}, ReflectEq (def A) := {
+#[program] Instance reflect_def : forall {A} `{ReflectEq A}, ReflectEq (def A) := {
   eqb := eq_def
 }.
 Next Obligation.
@@ -246,25 +246,6 @@ Next Obligation.
   cbn. constructor. subst. reflexivity.
 Defined.
 
-Fixpoint eq_non_empty_list {A : Set} (eqA : A -> A -> bool) (l l' : non_empty_list A) : bool :=
-  match l, l' with
-  | NEL.sing a, NEL.sing a' => eqA a a'
-  | NEL.cons a l, NEL.cons a' l' =>
-    eqA a a' && eq_non_empty_list eqA l l'
-  | _, _ => false
-  end.
-
-#[program] Instance reflect_non_empty_list :
-  forall {A : Set} `{ReflectEq A}, ReflectEq (non_empty_list A) :=
-  { eqb := eq_non_empty_list eqb }.
-Next Obligation.
-  induction x, y; cbn.
-  destruct (eqb_spec a a0); constructor; congruence.
-  constructor; congruence.
-  constructor; congruence.
-  destruct (eqb_spec a a0), (IHx y); constructor; congruence.
-Defined.
-
 Fixpoint eq_cast_kind (c c' : cast_kind) : bool :=
   match c, c' with
   | VmCast, VmCast
@@ -293,13 +274,16 @@ Local Ltac fcase c :=
   let e := fresh "e" in
   case c ; intro e ; [ subst ; try (left ; reflexivity) | finish ].
 
+Instance eq_dec_univ : EqDec Universe.t.
+Admitted.
+
 Local Ltac term_dec_tac term_dec :=
   repeat match goal with
          | t : term, u : term |- _ => fcase (term_dec t u)
-         | u : universe, u' : universe |- _ => fcase (eq_dec u u')
-         | x : universe_instance, y : universe_instance |- _ =>
+         | u : Universe.t, u' : Universe.t |- _ => fcase (eq_dec u u')
+         | x : Instance.t, y : Instance.t |- _ =>
            fcase (eq_dec x y)
-         | x : list Level.t, y : universe_instance |- _ =>
+         | x : list Level.t, y : Instance.t |- _ =>
            fcase (eq_dec x y)
          | n : nat, m : nat |- _ => fcase (Nat.eq_dec n m)
          | i : ident, i' : ident |- _ => fcase (string_dec i i')
@@ -315,18 +299,18 @@ Local Ltac term_dec_tac term_dec :=
 
 Derive NoConfusion NoConfusionHom for term.
 
-Derive EqDec for term.
-Next Obligation.
-  induction x using term_forall_list_rect ; intro t ;
+Instance EqDec_term : EqDec term.
+Proof.
+  intro x; induction x using term_forall_list_rect ; intro t ;
     destruct t ; try (right ; discriminate).
   all: term_dec_tac term_dec.
-  - induction H in args |- *.
+  - induction X in args |- *.
     + destruct args.
       * left. reflexivity.
       * right. discriminate.
     + destruct args.
       * right. discriminate.
-      * destruct (IHAll args) ; nodec.
+      * destruct (IHX args) ; nodec.
         destruct (p t) ; nodec.
         subst. left. inversion e. reflexivity.
   - destruct (IHx1 t1) ; nodec.
@@ -343,11 +327,11 @@ Next Obligation.
     destruct (IHx3 t3) ; nodec.
     subst. left. reflexivity.
   - destruct (IHx t) ; nodec.
-    subst. induction H in args |- *.
+    subst. induction X in args |- *.
     + destruct args. all: nodec.
       left. reflexivity.
     + destruct args. all: nodec.
-      destruct (IHAll args). all: nodec.
+      destruct (IHX args). all: nodec.
       destruct (p t0). all: nodec.
       subst. inversion e. subst.
       left. reflexivity.

checker/theories/Retyping.v

@@ -109,7 +109,7 @@ Section TypeOf.
       end
     end.
 
-  Definition sort_of (Γ : context) (t : term) : typing_result universe :=
+  Definition sort_of (Γ : context) (t : term) : typing_result Universe.t :=
     ty <- type_of Γ t;;
     type_of_as_sort type_of Γ ty.
 

checker/theories/Substitution.v

@@ -34,7 +34,7 @@ Inductive subs `{cf : checker_flags} Σ (Γ : context) : list term -> context ->
 (** Linking a context (with let-ins), an instance (reversed substitution)
     for its assumptions and a well-formed substitution for it. *)
 
-Inductive context_subst : context -> list term -> list term -> Set :=
+Inductive context_subst : context -> list term -> list term -> Type :=
 | context_subst_nil : context_subst [] [] []
 | context_subst_ass Γ args s na t a :
     context_subst Γ args s ->
@@ -920,7 +920,7 @@ Proof.
     f_equal.
     rewrite (lift_to_extended_list_k _ _ 1) map_map_compose.
     pose proof (to_extended_list_k_spec Γ k).
-    solve_all. destruct H3 as [n [-> Hn]].
+    solve_all. destruct H2 as [n [-> Hn]].
     rewrite /compose /lift (subst_app_decomp [a] s k); auto with wf.
     rewrite subst_rel_gt. simpl; lia.
     repeat (f_equal; simpl; try lia).
@@ -929,7 +929,7 @@ Proof.
     rewrite -IHcontext_subst // to_extended_list_k_cons /=.
     rewrite (lift_to_extended_list_k _ _ 1) map_map_compose.
     pose proof (to_extended_list_k_spec Γ k).
-    solve_all. destruct H3 as [n [-> Hn]].
+    solve_all. destruct H2 as [n [-> Hn]].
     rewrite /compose /lift (subst_app_decomp [subst0 s b] s k); auto with wf.
     rewrite subst_rel_gt. simpl; lia.
     repeat (f_equal; simpl; try lia).
@@ -943,7 +943,7 @@ Proof.
   induction 1. constructor.
   eapply All_app in wfargs as [wfargs wfa]. inv wfa. inv wfctx.
   constructor; intuition auto.
-  inv wfctx. red in H0. constructor; solve_all. apply wf_subst. solve_all. intuition auto with wf.
+  inv wfctx. red in H. constructor; solve_all. apply wf_subst. solve_all. intuition auto with wf.
 Qed.
 
 Lemma wf_make_context_subst ctx args s' :
@@ -1235,7 +1235,7 @@ Lemma red1_mkApps_l Σ Γ M1 N1 M2 :
 Proof.
   induction M2 in M1, N1 |- *. simpl; auto.
   intros. specialize (IHM2 (mkApp M1 a) (mkApp N1 a)).
-  inv H0.
+  inv X.
   forward IHM2. apply wf_mkApp; auto.
   forward IHM2. auto.
   rewrite <- !mkApps_mkApp; auto.
@@ -1247,17 +1247,17 @@ Lemma red1_mkApps_r Σ Γ M1 M2 N2 :
   Ast.wf M1 -> All Ast.wf M2 ->
   OnOne2 (red1 Σ Γ) M2 N2 -> red1 Σ Γ (mkApps M1 M2) (mkApps M1 N2).
 Proof.
-  intros. induction X in M1, H, H0 |- *.
-  inv H0.
+  intros. induction X0 in M1, H, X |- *.
+  inv X.
   destruct (isApp M1) eqn:Heq. destruct M1; try discriminate.
   simpl. constructor. apply OnOne2_app. constructor. auto.
   rewrite mkApps_tApp; try congruence.
   rewrite mkApps_tApp; try congruence.
   constructor. constructor. auto.
-  inv H0.
-  specialize (IHX (mkApp M1 hd)). forward IHX.
-  apply wf_mkApp; auto. forward IHX; auto.
-  now rewrite !mkApps_mkApp in IHX.
+  inv X.
+  specialize (IHX0 (mkApp M1 hd)). forward IHX0.
+  apply wf_mkApp; auto. forward IHX0; auto.
+  now rewrite !mkApps_mkApp in IHX0.
 Qed.
 
 Lemma wf_fix :
@@ -1402,11 +1402,11 @@ Proof.
     now apply All_map.
     assert(Ast.wf M1). now inv wfM.
     assert(All Ast.wf M2). eapply Forall_All. now inv wfM.
-    clear -X H1 H2 wfΓ Hs.
+    clear -X H0 X1 wfΓ Hs.
     induction X; constructor; auto.
     intuition.
-    eapply b; eauto. now inv H2.
-    apply IHX. now inv H2.
+    eapply b; eauto. now inv X1.
+    apply IHX. now inv X1.
 
   - forward IHred1. now inv wfM.
     constructor. specialize (IHred1 _ _ (Γ'' ,, vass na M1) eq_refl).
@@ -1592,13 +1592,13 @@ Proof.
     eapply All2_map.
     eapply All2_impl'. eassumption.
     eapply All_impl. eassumption.
-    cbn. apply All2_length in H3 as e. rewrite e.
+    cbn. apply All2_length in X0 as e. rewrite e.
     intros x [] y []; now split.
   - constructor.
     eapply All2_map.
     eapply All2_impl'. eassumption.
     eapply All_impl. eassumption.
-    cbn. apply All2_length in H3 as e. rewrite e.
+    cbn. apply All2_length in X0 as e. rewrite e.
     intros x [] y []; now split.
 Qed.
 
@@ -1638,7 +1638,7 @@ Lemma subst_eq_context `{checker_flags} φ l l' n k :
 Proof.
   induction l in l', n, k |- *; inversion 1. constructor.
   rewrite !subst_context_snoc. constructor.
-  apply All2_length in H5 as e. rewrite e.
+  apply All2_length in X1 as e. rewrite e.
   now apply subst_eq_decl.
   now apply IHl.
 Qed.