Merge pull request #432 from Blaisorblade/prepare-iris-coq-bump

Address deprecations in bump to Coq 8.16 (etc.)

Makefile

@@ -20,7 +20,7 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	@$(MAKE) -f Makefile.coq clean
-	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	find theories tests \( -name "*.d" -o -name "*.vo*" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
 	rm -f Makefile.coq
 .PHONY: clean
 

_CoqProject

@@ -36,6 +36,7 @@ theories/asubst_intf.v
 theories/asubst_base.v
 theories/proper.v
 theories/succ_notation.v
+theories/numbers.v
 theories/tactics.v
 
 theories/Dot/syn/syn.v

theories/Dot/examples/old_typing/old_subtyping_derived_rules.v

@@ -67,7 +67,7 @@ Qed.
 
 Lemma iSub_AddIJ' {Γ T} i j (Hle : i <= j) :
   Γ u⊢ₜ T, i <: T, j.
-Proof. rewrite (le_plus_minus i j Hle) Nat.add_comm. exact: iSub_AddIJ. Qed.
+Proof. rewrite -(Nat.sub_add i j Hle). exact: iSub_AddIJ. Qed.
 
 Lemma iSub_AddI Γ T i :
   Γ u⊢ₜ T, 0 <: T, i.
@@ -77,7 +77,7 @@ Lemma path_tp_delay {Γ p T i j} : i <= j →
   Γ u⊢ₚ p : T, i → Γ u⊢ₚ p : T, j.
 Proof.
   intros Hle Hp.
-  rewrite (le_plus_minus i j Hle); move: {j Hle} (j - i) => k.
+  rewrite -(Nat.sub_add i j Hle) (Nat.add_comm _ i). move: {j Hle} (j - i) => k.
   eapply iP_ISub, Hp.
   apply: iSub_AddIJ'; by [|lia].
 Qed.

theories/Dot/examples/sem/semtyp_lemmas/examples_lr.v

@@ -2,7 +2,7 @@
 Some are used in examples. *)
 From iris.proofmode Require Import proofmode.
 
-From D Require Import iris_prelude swap_later_impl.
+From D Require Import iris_prelude numbers swap_later_impl.
 From D.Dot Require Import rules path_repl.
 From D.Dot Require Export dot_semtypes dsub_lr sub_lr binding_lr.
 
@@ -26,7 +26,7 @@ Section Lemmas.
     Γ s⊨p p : oLaterN j T, i -∗
     Γ s⊨p p : T, i + j.
   Proof.
-    rewrite Nat.add_comm; elim: j i => [//|j IHj] i; rewrite plus_Snm_nSm.
+    rewrite Nat.add_comm; elim: j i => [//|j IHj] i; rewrite Nat_add_succ_r_l.
     by rewrite -(IHj i.+1) -sP_Later.
   Qed.
 

theories/Dot/examples/sem/storeless_typing_ex_utils.v

@@ -135,15 +135,6 @@ Lemma iT_ISub_nocoerce T1 T2 {Γ e} :
 Proof. intros. exact: (iT_ISub (i:=0)). Qed.
 #[global] Hint Resolve iT_ISub_nocoerce : core.
 
-Lemma path_tp_delay {Γ p T i j} (Hst : is_unstamped_ty' (length Γ) T) : i <= j →
-  Γ u⊢ₚ p : T, i → Γ u⊢ₚ p : T, j.
-Proof.
-  intros Hle Hp.
-  rewrite (le_plus_minus i j Hle); move: {j Hle} (j - i) => k.
-  eapply iP_ISub, Hp.
-  apply: iSub_AddIJ'; by [|lia].
-Qed.
-
 Lemma iT_Let Γ t u T U :
   Γ v⊢ₜ t : T →
   shift T :: Γ v⊢ₜ u : shift U →

theories/asubst_base.v

@@ -1,6 +1,6 @@
 (** * Substitution lemmas for languages implementing [ValuesSig]. *)
 From iris.program_logic Require Import language.
-From D Require Import prelude asubst_intf.
+From D Require Import prelude numbers asubst_intf.
 
 (** The module type [Sorts] is a "mixin module" that is included directly in
 each language implementing [ValuesSig],
@@ -88,7 +88,7 @@ Lemma eq_n_s_heads {n ρ1 ρ2} : eq_n_s ρ1 ρ2 n → n > 0 → shead ρ1 = shea
 Proof. rewrite /shead => /= HsEq. exact: HsEq. Qed.
 
 Lemma eq_cons v sb1 sb2 n : eq_n_s sb1 sb2 n → eq_n_s (v .: sb1) (v .: sb2) (S n).
-Proof. move => Heqs [//|x] /lt_S_n /Heqs //. Qed.
+Proof. move => Heqs [//|x] /Nat_succ_lt_mono_rev /Heqs //. Qed.
 
 Lemma up_sub_compose_base ρ v : up ρ >> v .: ids = v .: ρ.
 Proof. by rewrite -scons_up_swap /scomp subst_idX. Qed.
@@ -170,7 +170,7 @@ Section to_subst_idsσ_is_id.
 
   Lemma idsσ_eq_ids n : eq_n_s (∞ (idsσ n)) ids n.
   Proof.
-    elim: n => [|n IHn] [|i] // /lt_S_n Hle.
+    elim: n => [|n IHn] [|i] // /Nat_succ_lt_mono_rev Hle.
     rewrite /= to_subst_map_commute // IHn // id_subst //.
   Qed.
 End to_subst_idsσ_is_id.

theories/asubst_intf.v

@@ -6,7 +6,7 @@ well-known, our comments explain our usage.
 *)
 
 From iris.program_logic Require Import language.
-From D Require Import prelude.
+From D Require Import prelude numbers.
 
 (** ** [ValueSig] describes parameters that each D* language must implement.
 For our purposes here, a D* language is
@@ -184,7 +184,7 @@ Module Type SortsSig (Import V : ValuesSig).
     eq_n_s (∞ σ.|[ρ]) (∞ σ >> ρ) (length σ).
   Proof.
     elim: σ => /= [|v σ IHσ] i Hin; first lia; asimpl.
-    case: i Hin => [//|i] /lt_S_n Hin /=. exact: IHσ.
+    case: i Hin => [//|i] /= /Nat_succ_lt_mono_rev. exact: IHσ.
   Qed.
 
   (** [n]-closedness defines when some AST has at most [n] free variables (from [0] to [n - 1]). *)

theories/numbers.v

@@ -0,0 +1,7 @@
+From D Require Import prelude succ_notation.
+
+(* Nat.succ_lt_mono is awkward as a view. *)
+Lemma Nat_succ_lt_mono_rev {n m} : n.+1 < m.+1 ↔ n < m.
+Proof. by rewrite -Nat.succ_lt_mono. Qed.
+Lemma Nat_add_succ_r_l n m : n.+1 + m = n + m.+1.
+Proof. by rewrite Nat.add_comm Nat.add_succ_r -Nat.add_succ_l Nat.add_comm. Qed.