port to Rocq 9.0

Author: yforster

.github/workflows/build.yml

@@ -27,8 +27,8 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - run: opam repo add coq-released https://coq.inria.fr/opam/released
-      - run: opam install coq-equations.1.3+8.17 coq-stdpp.1.8.0 coq-metacoq-template.1.2+8.17 coq-library-undecidability.1.1+8.17
-      - run: cd theories && opam exec -- make models -j 2
+      - run: opam install rocq-equations.1.3.1+9.0 coq-stdpp
+      - run: cd theories && opam exec -- make 
 
 # name: Test compilation
 

README.md

@@ -11,9 +11,9 @@
   - Niklas Mück
   - Haoyi Zeng
 - Maintainer:
-  - Yannick Forster ([**@yforster**](https://github.com/yfrster))
+  - Yannick Forster ([**@yforster**](https://github.com/yforster))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.17
+- Compatible Coq versions: 9.0
 - Additional dependencies: 
   - the [`stdpp` library](https://gitlab.mpi-sws.org/iris/stdpp)
   - optionally, the [Coq Library of Undecidability Proofs](https://github.com/uds-psl/coq-library-undecidability)
@@ -48,7 +48,7 @@ This library contains results on synthetic computability theory.
 opam switch create coq-synthetic-computability --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda
 eval $(opam env)
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq.8.17.0 coq-equations.1.3+8.17 coq-metacoq-template.1.2+8.17 coq-stdpp.1.8.0
+opam install rocq-prover.9.0.0 rocq-equations rocq-metarocq-template coq-stdpp
 cd theories
 make
 make install
@@ -57,7 +57,7 @@ make install
 To build the part of the development relying on models of computation, in addition you have to 
 
 ```sh
-opam install coq-library-undecidability.1.1+8.17
+opam install coq-library-undecidability
 make models
 make install-models
 ```

theories/Axioms/halting.v

@@ -44,7 +44,7 @@ Proof.
   - exists (fun f x => negb (Nat.eqb (f x) 0)).
     intros f. unfold K_nat_nat, K_nat_bool.
     setoid_rewrite Bool.negb_true_iff.
-    now setoid_rewrite NPeano.Nat.eqb_neq.
+    now setoid_rewrite PeanoNat.Nat.eqb_neq.
 Qed.
 
 Lemma K_nat_equiv :

theories/Basic/CB.v

@@ -164,7 +164,7 @@ Section Def_F.
     forall x : X, index x < length (e (gen (map f (e (occ x))))).
   Proof.
     intros x.
-    eapply lt_le_trans.
+    eapply Nat.lt_le_trans.
     2: eapply gen_spec. 2:eapply NoDup_map; eauto.
     rewrite map_length.
     eapply nth_error_Some.
@@ -176,7 +176,7 @@ Section Def_F.
     nth_error (e (gen (map f (e (occ x))))) (index x) <> None.
   Proof.
     intros E. eapply nth_error_None in E. revert E.
-    eapply lt_not_le, index_length.
+    pose proof (index_length x). lia.
   Qed.
 
   Definition F_ (x : X) : Y :=

theories/Basic/CB_PHP.v

@@ -130,7 +130,7 @@ Section fixes.
     - destruct (in_dec eY x l2) as [Hi | Hni].
       2: firstorder.
       destruct (IHNoDup (remove eY x l2)) as (x0 & H1 & H2 & H3).
-      + eapply lt_le_trans. eapply remove_length_lt. 1: eauto. lia.
+      + eapply Nat.lt_le_trans. eapply remove_length_lt. 1: eauto. lia.
       + exists x0. firstorder. intros Hx0.
         eapply H3. eapply in_in_remove. 2: eauto.
         congruence.
@@ -276,8 +276,8 @@ Section fixes2.
       eapply build_corr_mono; eauto.
   Qed.
 
-  Definition f' x := proj1_sig (In1_compute _ _ (build_corrX x (S (IX x)) ltac:(abstract lia))).
-  Definition g' y := proj1_sig (In2_compute _ _ (build_corrY y (S (IY y)) ltac:(abstract lia))).
+  #[program] Definition f' x := proj1_sig (In1_compute _ _ (build_corrX x (S (IX x)) _)).
+  #[program] Definition g' y := proj1_sig (In2_compute _ _ (build_corrY y (S (IY y)) _)).
 
   Lemma f'_g' y :
     f' (g' y) = y.

theories/Basic/Myhill.v

@@ -99,17 +99,16 @@ Section fixes.
     (p x <-> p (γ C x)) /\ In (γ C x) (x :: map fst C) /\ ~ In2 (f (γ C x)) C.
   Proof.
     funelim (γ C x); try rename H0 into IH.
-    - intros Hx HC. rewrite <- Heqcall. eauto.
+    - intros Hx HC. eauto.
     - intros Hx HC.
       specialize (IH ) as (IH1 & IH2 & IH3).
       { intros ([] & E & [] % in_remove) % in_map_iff; cbn in E; subst.
         apply H1. f_equal. eapply HC; eauto. }
       { eapply correspondence_remove; eauto. }
       split. 2:split.
       + etransitivity. eapply f_red.
-        rewrite <- Heqcall. 
         rewrite <- IH1. symmetry. now eapply HC.
-      + rewrite <- Heqcall.  specialize IH2 as [EE | ([] & E & [] % in_remove) % in_map_iff]; eauto.
+      + specialize IH2 as [EE | ([] & E & [] % in_remove) % in_map_iff]; eauto.
         rewrite <- EE. right. eapply in_map_iff. eexists (_, _). eauto.
       + rewrite Heqcall in IH3, IH2, IH1 |- *.
         intros ([] & E & ?) % (in_map_iff). cbn in E. subst.
@@ -258,8 +257,8 @@ Section fixes2.
       eapply build_corr_mono; eauto.
   Qed.
 
-  Definition f' x := proj1_sig (In1_compute _ _ (build_corrX x (S (IX x)) ltac:(abstract lia))).
-  Definition g' y := proj1_sig (In2_compute _ _ (build_corrY y (S (IY y)) ltac:(abstract lia))).
+  Program Definition f' x := proj1_sig (In1_compute _ _ (build_corrX x (S (IX x)) _)).
+  Program Definition g' y := proj1_sig (In2_compute _ _ (build_corrY y (S (IY y)) _)).
 
   Lemma f'_red : reduces_m f' p q.
   Proof.

theories/CRM/baire_cantor.v

@@ -61,7 +61,7 @@ Lemma max_list_incl A B :
 Proof.
   induction A.
   - cbn. lia.
-  - cbn. intros H. eapply Max.max_lub.
+  - cbn. intros H. eapply Nat.max_lub.
     2: firstorder. eapply max_list_spec, H. firstorder.
 Qed.
 
@@ -89,7 +89,7 @@ Proof.
 
     specialize (H (map f_N (seq 0 n))).
     rewrite map_length seq_length in H.
-    specialize (H (le_refl _)).
+    specialize (H (Nat.le_refl _)).
     edestruct (listable_exists_dec (p := fun i => 0 < i <= n) ( q := fun i => ~ Exists (le i) (M (extend (take i (map f_N (seq 0 n)))) 0))).
     + exists (seq 1 n). clear. intros. rewrite in_seq. lia.
     + intros x. eapply not_dec. eapply Exists_dec. intros. eapply le_dec.
@@ -125,31 +125,31 @@ Proof.
     exists N. intros H.
     enough (N < N) by lia.
 
-    eapply lt_le_trans with (m := 1 + max_list (M (extend (map f (seq 0 N))) 0)).
+    eapply Nat.lt_le_trans with (m := 1 + max_list (M (extend (map f (seq 0 N))) 0)).
     + specialize (H N). setoid_rewrite List.Exists_exists in H.
       destruct H as [i Hi].
       * split. unfold N. cbn. lia. now rewrite map_length seq_length.
-      * eapply le_lt_trans. eapply Hi.
+      * eapply Nat.le_lt_trans. eapply Hi.
         enough (max_list [i] <=  max_list (M (extend (map f (seq 0 N))) 0)) as H0.
-        unfold max_list in H0 at 1. rewrite Max.max_0_r in H0. unfold id in H0 at 1. lia.
+        unfold max_list in H0 at 1. rewrite Nat.max_0_r in H0. unfold id in H0 at 1. lia.
         eapply max_list_incl. intros ? [-> | []].
         replace N with (length (map f (seq 0 N))) in Hi at 1.
         rewrite firstn_all in Hi. eapply Hi.
         now rewrite map_length seq_length.
     + unfold N. rewrite <- HL.
-      eapply plus_le_compat_l.
+      enough (max_list (M f 0) ≤ max_list (1 + length L :: L ++ M f 0)). lia.
       eapply max_list_incl, incl_tl, incl_appr, incl_refl.
       eapply map_ext_in.
       intros a Ha. unfold extend. 
       erewrite nth_indep.
       erewrite map_nth, seq_nth.
       * reflexivity.
       * enough (max_list [a] <=  max_list (1 + length L :: L ++ M f 0)) as H0.
-        unfold max_list in H0 at 1. rewrite Max.max_0_r in H0. unfold id in H0 at 1. lia.
+        unfold max_list in H0 at 1. rewrite Nat.max_0_r in H0. unfold id in H0 at 1. lia.
         eapply max_list_incl. intros ? [-> | []]. eapply in_cons, in_app_iff. eauto.
       * rewrite map_length seq_length.
         enough (max_list [a] <=  max_list (1 + length L :: L ++ M f 0)) as H0.
-        unfold max_list in H0 at 1. rewrite Max.max_0_r in H0. unfold id in H0 at 1. lia.
+        unfold max_list in H0 at 1. rewrite Nat.max_0_r in H0. unfold id in H0 at 1. lia.
         eapply max_list_incl. intros ? [-> | []]. eapply in_cons, in_app_iff. eauto.
         Unshelve. all:econstructor.
 Qed.
@@ -239,9 +239,15 @@ Proof.
   rewrite <- app_assoc in Heq.
   destruct (lt_eq_lt_dec (length l2') (length l1')) as [[Hlt|e] | Hgt].
   - eapply (f_equal (take (length l1'))) in Heq.
-    rewrite take_app take_ge in Heq.
-    rewrite app_length. cbn. lia.
-    subst. exfalso. eauto.
+    rewrite take_app in Heq.
+    rewrite take_app_ge in Heq. lia.
+    cbn in Heq.
+    exfalso. destruct (length l1' - length l2') eqn:E. lia.
+    cbn in *. subst. 
+    eapply nH2, tree_p. eapply (Kleene_T T_K). 2:exact H1.
+    rewrite Nat.sub_diag in Heq. cbn in Heq.
+    rewrite app_nil_r in Heq. rewrite <- Heq.
+    rewrite take_ge. lia. destruct n; cbn; eauto.
   - eapply app_inj_1 in Heq as [-> Heq]; eauto.
     destruct l3; cbn in *; congruence.
   - eapply (f_equal (take (length l2'))) in Heq.
@@ -251,6 +257,8 @@ Proof.
     exfalso. destruct (length l2' - length l1') eqn:E. lia.
     cbn in *. subst. 
     eapply nH1, tree_p. eapply (Kleene_T T_K). 2:exact H2.
+    rewrite Nat.sub_diag in Heq. cbn in Heq.
+    rewrite app_nil_r in Heq. rewrite firstn_all in Heq. subst.
     eexists. now rewrite <- app_assoc.
 Qed.
 
@@ -311,12 +319,12 @@ Proof.
     rewrite IHk. f_equal.
     destruct (drop k (F' f 0 k ++ ℓ (f k))) eqn:E1.
     + eapply (f_equal length) in E1.
-      rewrite drop_length in E1. cbn in E1.
+      rewrite skipn_length in E1. cbn in E1.
       pose proof (F'_length f 0 (S k)). cbn in H2. rewrite app_length in H2, E1.
       lia.
     + destruct (drop k (F' g 0 k ++ ℓ (g k))) eqn:E2.
       * eapply (f_equal length) in E2.
-        rewrite drop_length in E2. cbn in E2.
+        rewrite skipn_length in E2. cbn in E2.
         pose proof (F'_length g 0 (S k)). cbn in H2. rewrite app_length in H2, E2.
         lia.
       * cbn. rewrite !firstn_O. f_equal.
@@ -405,16 +413,16 @@ Proof.
         assert (k''' <= k''). {
           subst k''' k'' k.
           cbn. rewrite app_length. lia.
-        } 
+        }
         rewrite !take_take in Heq; eauto.
         rewrite firstn_app in Heq.
         rewrite !Nat.add_0_r in Heq.
         unfold k''' in Heq at 3.
-        rewrite take_app in Heq.
+        rewrite take_app_length in Heq.
         setoid_rewrite take_ge in Heq at 1. 2:eassumption.
         eapply leaf_prefix. eauto. eauto.
         eapply prefix_take_iff. rewrite <- Heq.
-        now rewrite take_app.
+        now rewrite take_app_length.
       * pose (k := (length (F' f 0 (S (S n))))).
         pose proof (F_inj_help H k) as Heq.
         pose proof (F'_eq_lt (o := 0) IH) as Hpref.
@@ -443,13 +451,13 @@ Proof.
         rewrite firstn_app in Heq.
         rewrite !Nat.add_0_r in Heq.
         unfold k''' in Heq at 3.
-        rewrite take_app in Heq.
+        rewrite take_app_length in Heq.
         setoid_rewrite take_ge in Heq at 1. 2:eassumption.
         symmetry.
         eapply leaf_prefix. eauto. eauto.
         eapply prefix_take_iff. rewrite <- Heq.
-        now rewrite take_app.
-Qed.      
+        now rewrite take_app_length.
+Qed.
 
 Lemma exists_leaf l2 :
   ~ T_K l2 -> exists l1, l1 `prefix_of` l2 /\ leaf l1.
@@ -767,7 +775,7 @@ Proof.
   - reflexivity.
   - cbn. rewrite app_length seq_app map_app.
     cbn. rewrite app_nth2. lia.
-    rewrite minus_diag. cbn. f_equal.
+    rewrite Nat.sub_diag. cbn. f_equal.
     rewrite <- IHl at 2.
     eapply map_ext_in.
     intros ? [_ ?] % in_seq. cbn in *.

theories/CRM/kleenetree.v

@@ -297,7 +297,7 @@ Proof.
     move => H n Hn x Hx.
     assert (Hg : D (length l1 + length l3) n = Some x). {
       eapply seval_mono. eassumption. lia. }
-    specialize (H n (lt_plus_trans _ _ (length l3) Hn) x Hg).
+    specialize (H n (Arith_base.lt_plus_trans_stt _ _ (length l3) Hn) x Hg).
     erewrite <- (lookup_app_l _ _ _ Hn). eassumption.
   - eapply decidable_iff. econstructor. move => a. generalize (length a) at 2 as k.
     induction a as [ | b a] using rev_rect; move => k; cbn.
@@ -308,11 +308,11 @@ Proof.
            ++ left. rewrite app_length. cbn. move => n Hn x' Hx'.
               destruct (nat_eq_dec n (length a)).
               ** subst. rewrite lookup_app_r. lia.
-                 rewrite minus_diag. cbn. congruence.
+                 rewrite Nat.sub_diag. cbn. congruence.
               ** rewrite lookup_app_l. lia.
                  eapply L. lia. eassumption.
            ++ right. rewrite app_length. cbn. move => / (fun H => H (length a)) H.
-              rewrite lookup_app_r ?minus_diag in H. lia. cbn in H.
+              rewrite lookup_app_r ?Nat.sub_diag in H. lia. cbn in H.
               eapply n.
               eapply Some_inj. symmetry. eapply H. lia. eauto.
         -- left. rewrite app_length. cbn. move => n Hn x' Hx'.
@@ -341,7 +341,7 @@ Proof.
       * cbn. destruct (nat_eq_dec n m).
         -- subst. rewrite Hx. destruct m. cbn. reflexivity.
            rewrite lookup_app_r. rewrite H_length. lia.
-           rewrite H_length minus_diag. reflexivity.
+           rewrite H_length Nat.sub_diag. reflexivity.
         -- rewrite lookup_app_l. rewrite H_length. lia.
            eapply IHm. lia.
     + rewrite H_length. lia.
@@ -434,7 +434,7 @@ Proof.
   - intros [k Hb].
     specialize (Hb (map (fun _ => true) (seq 0 k))).
     rewrite map_length seq_length in Hb.
-    specialize (Hb (le_refl _)).
+    specialize (Hb (Nat.le_refl _)).
     unfold tree_from in Hb. cbn in Hb.
     rewrite <- Is_true_iff in Hb.
     setoid_rewrite forallb_True in Hb.
@@ -544,8 +544,8 @@ Proof.
       exists (1 + Nat.max b1 b2). intros l Hl.
       destruct l; cbn in *; try lia.
       eapply le_S_n in Hl.
-      pose proof (Max.max_lub_l _ _ _ Hl).
-      pose proof (Max.max_lub_r _ _ _ Hl).
+      pose proof (Nat.max_lub_l _ _ _ Hl).
+      pose proof (Nat.max_lub_r _ _ _ Hl).
       destruct b; intros HT.
       * assert (T [true]). eapply tree_p. eapply T. 2:eauto. now eexists.
         eapply is_tree_subtree_at in H1.
@@ -701,7 +701,7 @@ Proof.
   intros Hl [w ->].
   rewrite <- firstn_all.
   rewrite <- (firstn_all u) at 1.
-  now rewrite Hl firstn_app Hl minus_diag firstn_O app_nil_r.
+  now rewrite Hl firstn_app Hl Nat.sub_diag firstn_O app_nil_r.
 Qed.
 
 Lemma take_prefix {X} n (l : list X) :
@@ -929,7 +929,7 @@ Proof.
       intros i Hi'. rewrite app_length in Hi'; cbn in *.
       assert (i = length u \/ i < length u) as [-> | Hi] by lia.
       + subst. rewrite app_nth2. lia.
-        intros. rewrite minus_diag. cbn. now eapply Hf.
+        intros. rewrite Nat.sub_diag. cbn. now eapply Hf.
       + intros. rewrite app_nth1. lia. now eapply IH.
   }
   exists g. intros n. cbn in *. eapply Hf. intros m.

theories/CRM/principles.v

@@ -358,7 +358,7 @@ Proof.
     + intros. eapply H. lia.
     + destruct (H (S n) (Nat.le_refl _)).
       * right. eauto.
-      * left. intros m [Hle |  ->] % le_lt_or_eq; eauto.
+      * left. intros m [Hle |  ->] % Nat.lt_eq_cases; eauto.
         eapply H1. lia.
     + right. exists m. split. lia. eassumption.
 Qed.
@@ -410,7 +410,7 @@ Proof.
     destruct (dec_bounded_quant (fun n => g n = true) n).
     + intros m ?; destruct (g m); firstorder congruence.
     + exfalso. enough (alpha' (2 * n) = true). rewrite H0 in H3. congruence.
-      rewrite mult_comm. unfold alpha'.
+      rewrite Nat.mul_comm. unfold alpha'.
       eapply andb_true_iff. split. eauto.
       eapply forallb_forall.
       intros b. rewrite in_map_iff. setoid_rewrite in_seq.
@@ -435,7 +435,7 @@ Proof.
     destruct (dec_bounded_quant (fun n => f n = true) (S n)).
     + intros m ?; destruct (f m); firstorder congruence.
     + exfalso. enough (H3 : alpha' (1 + 2 * n) = true). rewrite H0 in H3. congruence.
-      rewrite mult_comm. unfold alpha'.
+      rewrite Nat.mul_comm. unfold alpha'.
       eapply andb_true_iff. split. eauto.
       eapply forallb_forall.
       intros b. rewrite in_map_iff. setoid_rewrite in_seq.
@@ -854,10 +854,11 @@ Goal ADC -> ACC.
 Proof.
   intros C X R Htot.
   destruct (Htot 0) as [y0 Hy0].
-  unshelve specialize (C (∑ '(n, x), R n x) (fun '(exist _  (n, x) H) '(exist _ (m, y) H2) => m = S n)) as [f].
+  unshelve epose proof (C (∑ '(n, x), R n x) (fun '(exist _  (n, x) H) '(exist _ (m, y) H2) => m = S n)).
+  unshelve edestruct H as [f].
   - eexists (_, _). eauto.
-  - intros [(n, x) H]. destruct (Htot (S n)) as [y Hy]. now exists (exist _ (S n, y) Hy). 
-  - destruct H as [H0 H].
+  - intros [(n, x) H']. destruct (Htot (S n)) as [y Hy]. now exists (exist _ (S n, y) Hy). 
+  - clear H. destruct H0 as [H0 H].
     pose (N n := fst (proj1_sig (f n))).
     pose (s n := snd (proj1_sig (f n))).
     assert (HN : forall n, N (S n) = S (N n)). {