From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- cparser/validator/Alphabet.v | 32 ++++++++++++++++---------------- cparser/validator/Interpreter_complete.v | 8 ++++---- 2 files changed, 20 insertions(+), 20 deletions(-) (limited to 'cparser/validator') diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index ca71bf59..a13f69b0 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -61,13 +61,13 @@ Qed. (** nat is comparable. **) Program Instance natComparable : Comparable nat := - { compare := nat_compare }. + { compare := Nat.compare }. Next Obligation. symmetry. -destruct (nat_compare x y) as [] eqn:?. -rewrite nat_compare_eq_iff in Heqc. +destruct (Nat.compare x y) as [] eqn:?. +rewrite Nat.compare_eq_iff in Heqc. destruct Heqc. -rewrite nat_compare_eq_iff. +rewrite Nat.compare_eq_iff. trivial. rewrite <- nat_compare_lt in *. rewrite <- nat_compare_gt in *. @@ -78,9 +78,9 @@ trivial. Qed. Next Obligation. destruct c. -rewrite nat_compare_eq_iff in *; destruct H; assumption. +rewrite Nat.compare_eq_iff in *; destruct H; assumption. rewrite <- nat_compare_lt in *. -apply (lt_trans _ _ _ H H0). +apply (Nat.lt_trans _ _ _ H H0). rewrite <- nat_compare_gt in *. apply (gt_trans _ _ _ H H0). Qed. @@ -149,7 +149,7 @@ destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..]; right; intro; destruct H; rewrite compare_refl in Heqc; discriminate. Defined. -Instance NComparableUsualEq : ComparableUsualEq natComparable := nat_compare_eq. +Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq. (** A pair of ComparableUsualEq is ComparableUsualEq **) Instance PairComparableUsualEq @@ -223,33 +223,33 @@ inversion Heqp. subst. clear Heqp. rewrite phi_incr in H. pose proof (phi_bounded i0). pose proof (phi_bounded (inj x)). -destruct (Z_lt_le_dec (Zsucc (phi i0)) (2 ^ Z_of_nat size)%Z). +destruct (Z_lt_le_dec (Z.succ (phi i0)) (2 ^ Z.of_nat size)%Z). rewrite Zmod_small in H by omega. apply Zlt_succ_le, Zle_lt_or_eq in H. destruct H; simpl; auto. left. rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity. -replace (Zsucc (phi i0)) with (2 ^ Z_of_nat size)%Z in H by omega. +replace (Z.succ (phi i0)) with (2 ^ Z.of_nat size)%Z in H by omega. rewrite Z_mod_same_full in H. exfalso; omega. rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. pose proof (phi_bounded inj_bound); pose proof (phi_bounded i). -rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega. +rewrite <- Z.abs_eq with (phi i), <- Z.abs_eq with (phi inj_bound) by omega. clear H H0 H1. -do 2 rewrite <- inj_Zabs_nat. +do 2 rewrite <- Zabs2Nat.id_abs. f_equal. revert l i Heqp. -assert (Zabs_nat (phi inj_bound) < Zabs_nat (2^31)). +assert (Z.abs_nat (phi inj_bound) < Z.abs_nat (2^31)). apply Zabs_nat_lt, phi_bounded. -induction (Zabs_nat (phi inj_bound)); intros. +induction (Z.abs_nat (phi inj_bound)); intros. inversion Heqp; reflexivity. inversion Heqp; clear H1 H2 Heqp. match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end. pose proof (phi_bounded i0). -erewrite <- IHn, <- Zabs_nat_Zsucc in H |- *; eauto; try omega. +erewrite <- IHn, <- Zabs2Nat.inj_succ in H |- *; eauto; try omega. rewrite phi_incr, Zmod_small; intuition; try omega. apply inj_lt in H. -pose proof Zle_le_succ. -do 2 rewrite inj_Zabs_nat, Zabs_eq in H; now eauto. +pose proof Z.le_le_succ_r. +do 2 rewrite Zabs2Nat.id_abs, Z.abs_eq in H; now eauto. Qed. (** Previous class instances for [option A] **) diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index ff88571b..f76731d5 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -304,7 +304,7 @@ reflexivity. destruct p. reflexivity. simpl; rewrite build_pt_dot_cost. -simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity. +simpl; rewrite <- plus_n_Sm, Nat.add_assoc; reflexivity. Qed. Lemma build_pt_dot_buffer: @@ -593,12 +593,12 @@ Lemma parse_fix_complete: Proof. fix 3. destruct n_steps; intros; simpl. -apply lt_0_Sn. +apply Nat.lt_0_succ. apply step_next_ptd in H. pose proof (next_ptd_cost ptd). destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition. rewrite H3 in H0; rewrite H0. -apply le_n_S, le_0_n. +apply le_n_S, Nat.le_0_l. destruct (next_ptd ptd); intuition; subst. eapply parse_fix_complete with (n_steps:=n_steps) in H1. rewrite H0. @@ -648,7 +648,7 @@ generalize (start_nt init). dependent destruction full_pt0. intros. rewrite build_pt_dot_cost; simpl. -rewrite H, plus_0_r; reflexivity. +rewrite H, Nat.add_0_r; reflexivity. Qed. Lemma init_ptd_buffer: -- cgit