Update Rocq to 9.2.0

_RocqProject

@@ -1,7 +1,6 @@
 # [tag:flags]
 -arg "-set 'Default Goal Selector=!'"
--arg "-set 'Loose Hint Behavior=Strict'"
 -arg "-set 'Primitive Projections'"
 -arg "-set 'Printing Projections'"
--arg "-unset 'Printing Primitive Projection Parameters'"
+-arg "-w +default"
 -Q proofs_rocq main

proofs_rocq/category_theory/arrow.v

@@ -6,8 +6,6 @@
 (********************)
 (********************)
 
-Require Import Stdlib.Classes.Morphisms.
-Require Import Stdlib.Classes.Morphisms_Prop.
 Require Import main.category_theory.category.
 Require Import main.tactics.
 

proofs_rocq/category_theory/coproduct.v

@@ -6,7 +6,6 @@
 (************************)
 (************************)
 
-Require Import Stdlib.Classes.Morphisms.
 Require Import main.category_theory.arrow.
 Require Import main.category_theory.category.
 Require Import main.category_theory.initial.

proofs_rocq/category_theory/object.v

@@ -6,7 +6,6 @@
 (*********************)
 (*********************)
 
-Require Import Stdlib.Classes.Morphisms.
 Require Import main.category_theory.arrow.
 Require Import main.category_theory.category.
 Require Import main.tactics.

proofs_rocq/category_theory/terminal.v

@@ -6,7 +6,6 @@
 (******************************)
 (******************************)
 
-Require Import Stdlib.Classes.Morphisms.
 Require Import main.category_theory.category.
 Require Import main.category_theory.initial.
 Require Import main.category_theory.object.

proofs_rocq/icbics/icbics.v

@@ -23,6 +23,7 @@ Require Import Stdlib.Arith.Compare_dec.
 Require Import Stdlib.Lists.List.
 Require Import Stdlib.Sorting.Permutation.
 Require Import Stdlib.Sorting.Sorted.
+Require Import Stdlib.Vectors.FinFun.
 Require Import main.tactics.
 
 Import Stdlib.Arith.PeanoNat.Nat.
@@ -156,7 +157,6 @@ Proof.
   induction l; search; intros.
   - destruct j; search.
   - destruct i; destruct j; search.
-    apply IHl; search.
 Qed.
 
 #[local] Hint Resolve nth_firstn : main.
@@ -169,9 +169,6 @@ Proof.
   intros.
   outro i.
   induction l; intros; destruct i; search.
-  change (firstn (S i) (a :: l) ++ [nth (S i) (a :: l) d])
-    with (a :: firstn i l ++ [nth i l d]).
-  rewrite IHl; search.
 Qed.
 
 #[local] Hint Resolve cons_firstn_nth : main.
@@ -439,8 +436,6 @@ Proof.
   unfold for_loop.
   change (length l1) with n1.
   induction n1; search.
-  apply H0; search.
-  apply IHn1; search.
 Qed.
 
 (* Facts about `sort` *)

proofs_rocq/kleene/kleene_data.v

@@ -6,6 +6,8 @@
 (****************************************************************)
 (****************************************************************)
 
+Require Import main.tactics.
+
 Module Type KleeneData.
   (*
     Assumption: Let (`T`, `Leq`) be a partially ordered set, or poset. A poset

proofs_rocq/stlc/name.v

@@ -6,7 +6,6 @@
 (*******************************************)
 (*******************************************)
 
-Require Import Stdlib.Arith.Peano_dec.
 Require Import main.tactics.
 
 Module Type NameSig.

proofs_rocq/system_f/context.v

@@ -6,7 +6,6 @@
 (*****************************)
 (*****************************)
 
-Require Import Stdlib.Bool.Bool.
 Require Import Stdlib.Lists.List.
 Require Import main.system_f.free_var.
 Require Import main.system_f.local_closure.

proofs_rocq/system_f/local_closure.v

@@ -70,7 +70,6 @@ Theorem t_local_closure_monotonic :
   TLocallyClosed t i2.
 Proof.
   clean. outro i2 H. induction H0; search.
-  clean. apply tlc_for_all. apply IHTLocallyClosed. search.
 Qed.
 
 (* Don't add a resolve hint because `eapply` has a hard time guessing `i1`. *)
@@ -85,8 +84,6 @@ Proof.
   clean. outro ie2 it2 H H0.
   induction H1; search; constructor; search; clean.
   - apply t_local_closure_monotonic with (i1 := nt); search.
-  - apply IHELocallyClosed; search.
-  - apply IHELocallyClosed; search.
   - apply t_local_closure_monotonic with (i1 := nt); search.
 Qed.
 

proofs_rocq/system_f/name.v

@@ -6,7 +6,6 @@
 (*******************************************)
 (*******************************************)
 
-Require Import Stdlib.Arith.Peano_dec.
 Require Import Stdlib.Lists.List.
 Require Import main.tactics.
 

proofs_rocq/system_f/opening.v

@@ -231,10 +231,7 @@ Proof.
   induction H2; search; clean.
   specialize (IHTLocallyClosed t2 (S i)).
   feed IHTLocallyClosed.
-  - apply t_local_closure_monotonic with (i1 := i); search.
-  - apply tlc_for_all.
-    apply IHTLocallyClosed.
-    search.
+  apply t_local_closure_monotonic with (i1 := i); search.
 Qed.
 
 Hint Resolve locally_closed_open_for_all : main.
@@ -274,9 +271,7 @@ Proof.
     apply t_local_closure_monotonic with (i1 := nt); search.
   - specialize (IHELocallyClosed t0 (S it)).
     feed IHELocallyClosed.
-    + apply t_local_closure_monotonic with (i1 := it); search.
-    + apply IHELocallyClosed.
-      search.
+    apply t_local_closure_monotonic with (i1 := it); search.
   - apply locally_closed_open_for_all; search.
     constructor.
     apply t_local_closure_monotonic with (i1 := nt); search.

proofs_rocq/system_f/preservation.v

@@ -6,7 +6,6 @@
 (**************************************)
 (**************************************)
 
-Require Import Stdlib.Bool.Bool.
 Require Import Stdlib.Lists.List.
 Require Import main.system_f.context.
 Require Import main.system_f.free_var.

proofs_rocq/system_f/typing.v

@@ -6,7 +6,6 @@
 (**************************)
 (**************************)
 
-Require Import Stdlib.Bool.Bool.
 Require Import Stdlib.Lists.List.
 Require Import main.system_f.context.
 Require Import main.system_f.free_var.

proofs_rocq/tactics.v

@@ -8,9 +8,10 @@
 
 Require Import Stdlib.micromega.Lia.
 
-(* Ensure this hint database exists. *)
+(* Ensure these hint databases exist. *)
 
 Create HintDb main.
+Create Rewrite HintDb main.
 
 (*
   This tactic does a variety of simplifications on the goal and hypotheses.

proofs_rocq/tutorial/lesson3_logic.v

@@ -279,6 +279,13 @@ Inductive eq [A] (x : A) : A -> Prop :=
 Notation "x = y" := (eq x y) : type_scope.
 Notation "x <> y" := (~ (x = y)) : type_scope.
 
+(*
+  The `rewrite` tactic used below requires some machinery to work with our
+  new notion of equality. The following command generates it.
+*)
+
+Scheme Rewriting for eq.
+
 Definition one_plus_one_equals_two : 1 + 1 = 2 := eq_refl 2.
 
 Goal 1 + 1 = 2.
@@ -426,7 +433,8 @@ Definition divisible_by_4_implies_even x :
     | ex_intro y h2 =>
       ex_intro
         (2 * y)
-        match eq_sym (Nat.mul_assoc 2 2 y) in Logic.eq _ z return z = x with
+        match Logic.eq_sym (Nat.mul_assoc 2 2 y) in Logic.eq _ z return z = x
+        with
         | Logic.eq_refl _ => h2
         end
     end.

proofs_rocq/tutorial/lesson4_proof_techniques.v

@@ -6,7 +6,6 @@
 (******************************)
 (******************************)
 
-Require Import Stdlib.Arith.Arith. (* For facts in the `arith` hint database *)
 Require Import Stdlib.micromega.Lia. (* For the `lia` tactic *)
 
 (****************************)

toast.yml

@@ -88,12 +88,13 @@ tasks:
     command: |
       # Install Rocq via opam. The `rocq-prover` package is a virtual package
       # with unversioned dependencies on `rocq-core` and `rocq-stdlib`, so
-      # those two packages must be pinned explicitly.
+      # those two packages must be pinned explicitly. Note that `rocq-stdlib`
+      # is versioned independently of `rocq-core`.
       opam init --disable-sandboxing --yes
       eval "$(opam env)"
-      opam pin add --no-action rocq-core 9.0.0 --yes
-      opam pin add --no-action rocq-stdlib 9.0.0 --yes
-      opam pin add rocq-prover 9.0.0 --yes
+      opam pin add --no-action rocq-core 9.2.0 --yes
+      opam pin add --no-action rocq-stdlib 9.1.0 --yes
+      opam pin add --kind version rocq-prover meta.1 --yes
 
   install_tools:
     description: Install the tools needed to verify the Rocq proofs.
@@ -169,10 +170,9 @@ tasks:
         '^\s*Require (Import )?(Stdlib|main)\.' \
         "rocq compile \
           -set 'Default Goal Selector=!' \
-          -set 'Loose Hint Behavior=Strict' \
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
-          -unset 'Printing Primitive Projection Parameters' \
+          -w +default \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \
@@ -188,10 +188,9 @@ tasks:
         '^\s*Import ' \
         "rocq compile \
           -set 'Default Goal Selector=!' \
-          -set 'Loose Hint Behavior=Strict' \
           -set 'Primitive Projections' \
           -set 'Printing Projections' \
-          -unset 'Printing Primitive Projection Parameters' \
+          -w +default \
           -Q proofs_rocq main ?" \
         $(
           find . -type d \( \