fix Nat deprecations

coq-community · Sep 16, 2022 · de00018 · de00018
1 parent 76f4ddd
commit de00018
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 14 deletions.
diff --git a/theories/complete.v b/theories/complete.v
@@ -230,7 +230,7 @@ simpl in |- *; intros S L a b V Eq H;
  elim (stateAssignContrad S L H a b V Eq); intros S' HS'.
 elim HS'; intros HS'1 HS'2; exists S'; auto with stalmarck.
 intros n' HR S L a b V Eq H.
-elim (le_or_lt (length (varTriplets L)) n'); intros Hn'.
+elim (Nat.le_gt_cases (length (varTriplets L)) n'); intros Hn'.
 apply (HR S L a b); auto with stalmarck.
 rewrite (nthTailProp3 n' (varTriplets L)); auto with stalmarck.
 elim (HR (addEq (myNth n' (varTriplets L) rZTrue, rZTrue) S) L a b); auto with stalmarck.

diff --git a/theories/ltState.v b/theories/ltState.v
@@ -72,9 +72,9 @@ Definition oneStateAll (S : State) (a b : rNat) :=
 
 Theorem lePlusComp : forall a b c d : nat, a <= b -> c <= d -> a + c <= b + d.
 intros a b c d H' H'0.
-apply le_trans with (m := a + d); auto with stalmarck.
-apply plus_le_compat_l; auto with stalmarck.
-apply plus_le_compat_r; auto with stalmarck.
+apply Nat.le_trans with (m := a + d); auto with stalmarck.
+apply Nat.add_le_mono_l; auto with stalmarck.
+apply Nat.add_le_mono_r; auto with stalmarck.
 Qed.
 Local Hint Resolve lePlusComp : stalmarck.
 (* Monotonicity *)
@@ -89,15 +89,15 @@ Local Hint Resolve oneStateAllLe : stalmarck.
 
 Theorem ltlePlusCompL :
  forall a b c d : nat, a < b -> c <= d -> a + c < b + d.
-intros a b c d H' H'0; apply lt_le_trans with (m := b + c); auto with stalmarck.
-apply plus_lt_compat_r; auto with stalmarck.
+intros a b c d H' H'0; apply Nat.lt_le_trans with (m := b + c); auto with stalmarck.
+apply Nat.add_lt_mono_r; auto with stalmarck.
 Qed.
 Local Hint Resolve ltlePlusCompL : stalmarck.
 
 Theorem ltlePlusCompR :
  forall a b c d : nat, a <= b -> c < d -> a + c < b + d.
-intros a b c d H' H'0; apply le_lt_trans with (m := b + c); auto with stalmarck.
-apply plus_lt_compat_l; auto with stalmarck.
+intros a b c d H' H'0; apply Nat.le_lt_trans with (m := b + c); auto with stalmarck.
+apply Nat.add_lt_mono_l; auto with stalmarck.
 Qed.
 Local Hint Resolve ltlePlusCompR : stalmarck.
 (* Strict monotony *)
@@ -217,7 +217,7 @@ Definition ltState (S1 S2 : State) := valState S1 < valState S2.
 Theorem ltStateTrans : transitive State ltState.
 red in |- *; unfold ltState in |- *; auto with stalmarck.
 intros S1 S2 S3 H' H'0.
-apply lt_trans with (m := valState S2); auto with stalmarck.
+apply Nat.lt_trans with (m := valState S2); auto with stalmarck.
 Qed.
 
 Theorem ltStateEqComp :
@@ -227,8 +227,8 @@ unfold eqState, ltState in |- *.
 intros S1 S2 S3 S4 H' H'0 H'1.
 Elimc H'0; intros H'0 H'2.
 Elimc H'; intros H' H'3.
-apply lt_le_trans with (m := valState S2); auto with stalmarck.
-apply le_lt_trans with (m := valState S1); auto with stalmarck.
+apply Nat.lt_le_trans with (m := valState S2); auto with stalmarck.
+apply Nat.le_lt_trans with (m := valState S1); auto with stalmarck.
 Qed.
 
 Theorem ltStateLt :

diff --git a/theories/rZ.v b/theories/rZ.v
@@ -124,7 +124,7 @@ Qed.
 Theorem rltTrans : transitive rNat rlt.
 red in |- *; unfold rlt in |- *; intros x y z H1 H2.
 apply nat_of_P_lt_Lt_compare_complement_morphism.
-apply lt_trans with (nat_of_P y); apply nat_of_P_lt_Lt_compare_morphism; auto with stalmarck.
+apply Nat.lt_trans with (nat_of_P y); apply nat_of_P_lt_Lt_compare_morphism; auto with stalmarck.
 Qed.
 
 Theorem rltNotRefl : forall a : rNat, ~ rlt a a.
@@ -137,7 +137,7 @@ Theorem rnextRlt : forall m : rNat, rlt m (rnext m).
 intros m; unfold rlt, rnext in |- *.
 apply nat_of_P_lt_Lt_compare_complement_morphism.
 rewrite Pplus_one_succ_r; rewrite nat_of_P_plus_morphism;
- unfold nat_of_P in |- *; simpl in |- *; rewrite plus_comm; 
+ unfold nat_of_P in |- *; simpl in |- *; rewrite Nat.add_comm; 
  simpl in |- *; auto with arith stalmarck.
 Qed.
 #[export] Hint Resolve rnextRlt : stalmarck.
@@ -180,7 +180,7 @@ Theorem rNextInv : forall n m : rNat, rlt n (rnext m) -> n = m \/ rlt n m.
 intros n m H'.
 generalize (nat_of_P_lt_Lt_compare_morphism _ _ H').
 rewrite rNextS.
-intros H'0; case (le_lt_or_eq _ _ (lt_n_Sm_le _ _ H'0)).
+intros H'0; case (proj1 (Nat.lt_eq_cases _ _) (proj1 (Nat.lt_succ_r _ _) H'0)).
 intros H'1; right; red in |- *;
  apply nat_of_P_lt_Lt_compare_complement_morphism; 
  auto with stalmarck.