Update dependencies (Coq 8.18) (#238)

.github/coq-concert.opam.locked

@@ -10,19 +10,19 @@ homepage: "https://github.com/AU-COBRA/ConCert"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
-  "coq" {= "8.17.0"}
-  "coq-bignums" {= "9.0.0+coq8.17"}
-  "coq-metacoq-common" {= "1.2+8.17"}
-  "coq-metacoq-erasure" {= "1.2+8.17"}
-  "coq-metacoq-pcuic" {= "1.2+8.17"}
-  "coq-metacoq-safechecker" {= "1.2+8.17"}
-  "coq-metacoq-template" {= "1.2+8.17"}
-  "coq-metacoq-template-pcuic" {= "1.2+8.17"}
-  "coq-metacoq-utils" {= "1.2+8.17"}
+  "coq" {= "8.18.0"}
+  "coq-bignums" {= "9.0.0+coq8.18"}
+  "coq-metacoq-common" {= "1.2.1+8.18"}
+  "coq-metacoq-erasure" {= "1.2.1+8.18"}
+  "coq-metacoq-pcuic" {= "1.2.1+8.18"}
+  "coq-metacoq-safechecker" {= "1.2.1+8.18"}
+  "coq-metacoq-template" {= "1.2.1+8.18"}
+  "coq-metacoq-template-pcuic" {= "1.2.1+8.18"}
+  "coq-metacoq-utils" {= "1.2.1+8.18"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
-  "coq-quickchick" {= "2.0.0"}
-  "coq-stdpp" {= "1.8.0"}
+  "coq-quickchick" {= "dev"}
+  "coq-stdpp" {= "1.9.0"}
 ]
 build: [
   [make]
@@ -37,10 +37,14 @@ dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"
 pin-depends: [
   [
     "coq-rust-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#f31a52ba2c1bddd42e9f9df8fca6c297ac359fae"
+    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#0053733e56008c917bf43d12e8bf0616d3b9a856"
   ]
   [
     "coq-elm-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#0c0a733486f915162a194ee646d5f11d2ffc5cc0"
+    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#903320120e3f36d7857161e5680fabeb6e743c6b"
+  ]
+  [
+    "coq-quickchick.dev"
+    "git+https://github.com/4ever2/QuickChick.git#bc61d58045feeb754264df9494965c280e266e1c"
   ]
 ]

coq-concert.opam

@@ -14,24 +14,25 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 
 depends: [
-  "coq" {>= "8.17" & < "8.18~"}
+  "coq" {>= "8.17" & < "8.19~"}
   "coq-bignums" {>= "8"}
-  "coq-quickchick" {= "2.0.0"}
-  "coq-metacoq-utils" {= "1.2+8.17"}
-  "coq-metacoq-common" {= "1.2+8.17"}
-  "coq-metacoq-template" {= "1.2+8.17"}
-  "coq-metacoq-template-pcuic" {= "1.2+8.17"}
-  "coq-metacoq-pcuic" {= "1.2+8.17"}
-  "coq-metacoq-safechecker" {= "1.2+8.17"}
-  "coq-metacoq-erasure" {= "1.2+8.17"}
+  "coq-quickchick" {= "dev"}
+  "coq-metacoq-utils" {>= "1.2" & < "1.3~"}
+  "coq-metacoq-common" {>= "1.2" & < "1.3~"}
+  "coq-metacoq-template" {>= "1.2" & < "1.3~"}
+  "coq-metacoq-template-pcuic" {>= "1.2" & < "1.3~"}
+  "coq-metacoq-pcuic" {>= "1.2" & < "1.3~"}
+  "coq-metacoq-safechecker" {>= "1.2" & < "1.3~"}
+  "coq-metacoq-erasure" {>= "1.2" & < "1.3~"}
   "coq-rust-extraction" {= "dev"}
   "coq-elm-extraction" {= "dev"}
-  "coq-stdpp" {>= "1.6.0" & <= "1.8.0"}
+  "coq-stdpp" {= "1.9.0"}
 ]
 
 pin-depends: [
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#f31a52ba2c1bddd42e9f9df8fca6c297ac359fae"]
-  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#0c0a733486f915162a194ee646d5f11d2ffc5cc0"]
+  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#0053733e56008c917bf43d12e8bf0616d3b9a856"]
+  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#903320120e3f36d7857161e5680fabeb6e743c6b"]
+  ["coq-quickchick.dev" "git+https://github.com/4ever2/QuickChick.git#bc61d58045feeb754264df9494965c280e266e1c"]
 ]
 
 build: [

embedding/theories/EnvSubst.v

@@ -110,7 +110,7 @@ Module NamelessSubst.
   Lemma lookup_i_of_val_env ρ n v :
     lookup_i ρ n = Some v -> lookup_i (exprs ρ) n = Some (of_val_i v).
   Proof.
-    revert dependent n.
+    generalize dependent n.
     induction ρ; intros n0 Hρ.
     + easy.
     + destruct a; simpl in *.
@@ -125,7 +125,7 @@ Module NamelessSubst.
     {v | lookup_i ρ n = Some v /\ (eRel n).[exprs ρ] = of_val_i v}.
   Proof.
     intros Hlt.
-    revert dependent n.
+    generalize dependent n.
     induction ρ; intros n1 Hlt.
     + easy.
     + destruct (Nat.eqb n1 0) eqn:Hn1.

embedding/theories/pcuic/PCUICCorrectness.v

@@ -45,10 +45,10 @@ Theorem expr_to_term_sound (n : nat) (ρ : env val) Σ1 Σ2
   iclosed_n 0 e2 = true ->
   Σ2 |- t⟦e2⟧Σ1 ⇓ t⟦of_val_i v⟧Σ1.
 Proof.
-  revert dependent v.
-  revert dependent ρ.
-  revert dependent e2.
-  revert dependent e1.
+  generalize dependent v.
+  generalize dependent ρ.
+  generalize dependent e2.
+  generalize dependent e1.
   induction n.
   - now intros.
   - intros e1 e2 ρ v Hsync Hgeok Hρ_ok He Henv Hc; destruct e1.
@@ -240,7 +240,7 @@ Proof.
           remember ((n0,_) :: (e2,_) :: ρ') as ρ''.
           eapply IHn with (ρ := ρ''); subst; eauto with hints.
           rewrite <- subst_env_compose_2;
-            (simpl; eauto using vars_to_apps_iclosed_n with hints).
+            (simpl; eauto using vars_to_apps_iclosed_n with hints; auto with bool hints).
           cbn.
           now repeat rewrite subst_env_i_ty_closed_0_eq by auto.
       * rename e0 into n0.
@@ -378,7 +378,7 @@ Proof.
                    extended_subst xs k = rev (reln [] k xs)).
         { intros xs k Hvass. rewrite reln_alt_eq. rewrite app_nil_r.
           rewrite rev_involutive.
-          revert dependent k.
+          generalize dependent k.
           induction xs; intros k; cbn; auto.
           inversion Hvass; subst; cbn.
           replace (k+1) with (1+k) by lia.

embedding/theories/pcuic/PCUICCorrectnessAux.v

@@ -310,7 +310,7 @@ Lemma type_eval_value Σ ρ ty ty_v n :
   ty_val ty_v.
 Proof.
   intros Hok He.
-  revert dependent ty_v. revert n.
+  generalize dependent ty_v. revert n.
   induction ty; intros.
   + simpl in *. inversion He; eauto with hints.
   + simpl in *.
@@ -545,7 +545,7 @@ Lemma subst_closed_map ts1 ts2 k :
   forallb (closedn k) ts2 ->
   map (subst ts1 k) ts2 = ts2.
 Proof.
-  intros H. revert dependent k. revert ts1.
+  intros H. generalize dependent k. revert ts1.
   induction ts2; intros; auto.
   simpl in *. propify. destruct_hyps.
   f_equal; eauto with hints.
@@ -583,7 +583,7 @@ Proof.
   intros Hgeok Hr. unfold resolve_inductive in *.
   destruct (lookup_global Σ ind) eqn:Hlg; tryfalse.
   destruct g; tryfalse. inversion Hr; subst; clear Hr.
-  revert dependent cs.
+  generalize dependent cs.
   induction Σ; intros; tryfalse.
   cbn in *. destruct a. cbn in *.
   destruct (e0 =? ind)%string; now propify.
@@ -623,7 +623,7 @@ Proof.
   intros Hlen Htys.
   apply forallb_Forall in Htys.
   apply Forall_map_inv in Htys.
-  revert dependent vs.
+  generalize dependent vs.
   induction tys; intros.
   - now destruct vs; tryfalse.
   - destruct vs; tryfalse; cbn in *.
@@ -967,7 +967,7 @@ Lemma map_subst_env_ty_closed n m ρ l0 :
   forallb (iclosed_ty n) l0 ->
   map (subst_env_i_ty (m + n) ρ) l0 = l0.
 Proof.
-  intros H. revert dependent n. revert m ρ. induction l0; intros m ρ n Hc; simpl; auto.
+  intros H. generalize dependent n. revert m ρ. induction l0; intros m ρ n Hc; simpl; auto.
   simpl in *. propify. destruct_hyps. f_equal; eauto with hints.
 Qed.
 
@@ -1212,7 +1212,7 @@ Lemma iclosed_ty_expr_env_ok :
   forall (n : nat) (ρ : env expr) e,
     iclosed_n n e -> ty_expr_env_ok ρ n e.
 Proof.
-  intros. revert dependent n. revert ρ.
+  intros. generalize dependent n. revert ρ.
   induction e using expr_elim_case; intros ?? Hc; eauto.
   + simpl in *. unfold is_true in *. propify.
     destruct_and_split; auto.
@@ -1401,7 +1401,7 @@ Lemma eval_ge_val_ok n ρ Σ e v :
   expr_eval_i Σ n ρ e = Ok v ->
   ge_val_ok Σ v.
 Proof.
-  revert dependent ρ. revert dependent v. revert dependent e.
+  generalize dependent ρ. generalize dependent v. generalize dependent e.
   induction n; intros e v ρ Hok He; tryfalse.
   destruct e; unfold expr_eval_i in *; simpl in *; inversion He; tryfalse.
   + destruct (lookup_i ρ n0) eqn:Hlook; simpl in *; inversion He; subst.
@@ -1631,7 +1631,7 @@ Lemma eval_val_ok n ρ Σ e v :
   expr_eval_i Σ n ρ e = Ok v ->
   val_ok Σ v.
 Proof.
-  revert dependent ρ. revert dependent v. revert dependent e.
+  generalize dependent ρ. generalize dependent v. generalize dependent e.
   induction n; intros e v ρ Hty_ok Hok Hc He; tryfalse.
   destruct e.
   + unfold expr_eval_i in *. simpl in *.
@@ -1841,9 +1841,9 @@ Lemma mkApps_atom_inv l1 l2 t1 t2 :
   l1 = l2 /\ t1 = t2.
 Proof.
   intros H1 H2 Hmk.
-  revert dependent t1.
-  revert dependent t2.
-  revert dependent l2.
+  generalize dependent t1.
+  generalize dependent t2.
+  generalize dependent l2.
   induction l1 using MCList.rev_ind; intros; destruct l2 using MCList.rev_ind.
   + inversion Hmk. easy.
   + simpl in *. subst. rewrite mkApps_unfold in *; tryfalse.
@@ -1867,7 +1867,7 @@ Lemma nth_error_map_exists {A B} (f : A -> B) (l : list A) n p:
   exists p0 : A, p = f p0.
 Proof.
   intros H.
-  revert dependent l.
+  generalize dependent l.
   induction n; simpl in *; intros l H; destruct l eqn:H1; inversion H; eauto.
 Qed.
 

embedding/theories/pcuic/PCUICFacts.v

@@ -104,7 +104,7 @@ Section Values.
     AllEnv P ρ -> lookup_i ρ n = Some e -> P e.
   Proof.
     intros Hfe Hl.
-    revert dependent n.
+    generalize dependent n.
     induction Hfe; intros n Hl.
     + inversion Hl.
     + simpl in *. destruct x; destruct (Nat.eqb n 0); inversion Hl; subst; eauto.
@@ -480,8 +480,8 @@ Section Values.
   Lemma lookup_ind_nth_error_False (ρ : env A) n m a key :
     lookup_with_ind_rec (1+n+m) ρ key = Some (n, a) -> False.
   Proof.
-    revert dependent m.
-    revert dependent n.
+    generalize dependent m.
+    generalize dependent n.
     induction ρ as [ |a0 ρ0]; intros n m H; tryfalse.
     simpl in *.
     destruct a0; destruct (s =? key).
@@ -494,15 +494,15 @@ Section Values.
     lookup_with_ind_rec (1+n) ρ key = Some (1+i, a) <->
     lookup_with_ind_rec n ρ key = Some (i, a).
   Proof.
-    split; revert dependent i; revert dependent n;
+    split; generalize dependent i; generalize dependent n;
     induction ρ; intros i1 n1 H; tryfalse; simpl in *;
       destruct a0; destruct ( s =? key); inversion H; eauto.
   Qed.
 
   Lemma lookup_ind_nth_error (ρ : env A) i a key :
     lookup_with_ind ρ key = Some (i,a) -> nth_error ρ i = Some (key,a).
   Proof.
-    revert dependent ρ.
+    generalize dependent ρ.
     induction i; simpl; intros ρ0 H.
     + destruct ρ0; tryfalse. unfold lookup_with_ind in H. simpl in *.
       destruct p as (nm,a0); destruct (nm =? key) eqn:Heq; try rewrite String.eqb_eq in *; subst.
@@ -563,7 +563,7 @@ Section Values.
     map fst l1 = map fst l2 ->
     find (p ∘ fst) l1 = None -> find (p ∘ fst) l2 = None.
   Proof.
-    revert dependent l2.
+    generalize dependent l2.
     induction l1 as [ | ab l1']; intros l2 Hmap Hfnd.
     + destruct l2; simpl in *; easy.
     + destruct l2; simpl in *; tryfalse.
@@ -592,7 +592,7 @@ Section Values.
     exists v2, find (p ∘ fst) l2 = Some v2
                /\ fst v1 = fst v1.
   Proof.
-    revert dependent l2.
+    generalize dependent l2.
     revert v1.
     induction l1 as [ | ab l1']; intros v1 l2 Hmap Hfnd.
     + destruct l2; simpl in *; easy.