Skip to content

fix arith deprecations #40

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 15, 2023
Merged

fix arith deprecations #40

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 17 additions & 15 deletions theories/DKA_Construction.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ Module Algebraic.
rewrite mx_point_blocks11 by trivial.
setoid_rewrite mx_point_blocks01 at 2; trivial.
cbn.
rewrite 2minus_diag.
rewrite 2 Nat.sub_diag.
set (U := mx_point 1 n 0 i (1: regex)).
set (V := mx_point n 1 f 0 (1: regex)).
set (Y := mx_point n 1 s 0 (a: regex)).
Expand Down Expand Up @@ -522,9 +522,10 @@ Module Correctness.
Proof.
intros i j n A Hi Hj [Hd He]. split; auto.
intros s a t Hst. apply delta_add_var in Hst as [Hst|[-> [-> ->]]]; split; auto; simpl.
specialize (Hd _ _ _ Hst). destruct A. simpl. num_simpl. eapply lt_le_trans. apply Hd. apply Max.le_max_r.
specialize (Hd _ _ _ Hst). destruct A. simpl. num_simpl. eapply Nat.lt_le_trans.
apply Hd. apply Nat.le_max_r.
specialize (Hd _ _ _ Hst). intuition.
destruct A. simpl. num_simpl. apply Max.le_max_l.
destruct A. simpl. num_simpl. apply Nat.le_max_l.
destruct A. simpl. auto.
Qed.
#[local] Hint Resolve bounded_incr bounded_add_one bounded_add_var : core.
Expand Down Expand Up @@ -581,7 +582,7 @@ Module Correctness.
Qed.

Lemma leb_S: forall n, leb (S n) xH = false.
Proof. intros. case le_spec; intro H; trivial. num_simpl. elim (lt_n_O _ H). Qed.
Proof. intros. case le_spec; intro H; trivial. num_simpl. elim (Nat.nlt_0_r _ H). Qed.
Hint Rewrite leb_S : bool_simpl.

Lemma labelling_add_var : forall n A i j s t c,
Expand All @@ -602,7 +603,7 @@ Module Correctness.
Lemma psurj A: A = mk (size A) (epsilonmap A) (deltamap A) (max_label A).
Proof. destruct A. reflexivity. Qed.

Opaque Max.max.
Opaque Nat.max.
Lemma commute_add_var: forall n i f A,
bounded A -> belong i A -> belong f A ->
Algebraic.add_var (nat_of_state i) (nat_of_state f) n (preNFA_to_preMAUT A)
Expand All @@ -612,14 +613,14 @@ Module Correctness.
rewrite <- plus_assoc. apply plus_compat; trivial.
fold (add_var i f n (mk (size A) (epsilonmap A) (deltamap A) (max_label A))).
rewrite labelling_add_var.
rewrite (@labelling_crop (Max.max (Datatypes.S (nat_of_num n)) (max_label A))); auto with arith.
rewrite (@labelling_crop (Nat.max (Datatypes.S (nat_of_num n)) (max_label A))); auto with arith.
setoid_rewrite eqb_eq_nat_bool. setoid_rewrite id_nat.
unfold labelling. num_simpl.
nat_analyse; simpl; fold_regex; try semiring_reflexivity.
num_analyse; simpl; fold_regex; try semiring_reflexivity.
elim n0. clear. num_simpl. apply Max.le_max_l.
elim n0. clear. num_simpl. apply Nat.le_max_l.
Qed.
Transparent Max.max.
Transparent Nat.max.

Lemma not_true_eq_false: forall b, ~ b = true -> b = false.
Proof. intros [ ]; tauto. Qed.
Expand Down Expand Up @@ -927,7 +928,7 @@ Lemma build_max_label: forall a i e f A, i < max_label A -> i < max_label (build
Proof.
induction a; intros i e f A Hi; rewrite (psurj A); simpl; auto.
rewrite max_label_add_one. auto.
num_simpl. eauto 2 using Max.le_max_r with arith.
num_simpl. eauto 2 using Nat.le_max_r with arith.
Qed.

Lemma collect_max_label:
Expand All @@ -941,7 +942,7 @@ Proof.
eapply IHa2 in Hi as [Hi|Hi]. left. apply build_max_label, Hi. auto.
rewrite max_label_add_one. auto.
revert Hi. NumSetProps.set_iff. intuition.
subst. left. destruct A; simpl. num_simpl. eauto using Max.le_max_l with arith.
subst. left. destruct A; simpl. num_simpl. eauto using Nat.le_max_l with arith.
Qed.

Lemma max_label_collect:
Expand All @@ -958,7 +959,7 @@ Proof.
eapply IHa2 in Hi as [[j ? ?]|Hi]. left. exists j; auto using collect_incr_2. right. assumption.
eapply IHa in Hi as [Hi|Hi]; auto.
revert Hi. rewrite max_label_add_one, max_label_incr. auto.
revert Hi. rewrite max_label_add_var. num_simpl. apply Max.max_case; auto.
revert Hi. rewrite max_label_add_var. num_simpl. apply Nat.max_case; auto.
intro Hi. left. exists (nat_of_num p). auto with arith. num_simpl. auto with set.
Qed.

Expand All @@ -981,8 +982,9 @@ Proof.

clear. intros a b H. apply inf_leq. intros c Hc.
apply max_label_collect in Hc as [[d ? Hd]|?].
rewrite H in Hd. eapply collect_max_label in Hd as [Hd|?].
eapply le_lt_trans. eassumption. unfold statesetelt_of_nat in Hd. rewrite id_nat in Hd. eassumption.
NumSetProps.setdec.
simpl in *. compute in H0. lia_false.
rewrite H in Hd. eapply collect_max_label in Hd as [Hd|?].
eapply Nat.le_lt_trans. eassumption. unfold statesetelt_of_nat in Hd.
rewrite id_nat in Hd. eassumption.
NumSetProps.setdec.
simpl in *. compute in H0. lia_false.
Qed.
10 changes: 5 additions & 5 deletions theories/DKA_DFA_Equiv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -389,11 +389,11 @@ Section correctness.
constructor.
intros l Hl. apply Htar. rewrite <- add_lists_S. apply Htar''. assumption.
apply (ci_sameclass Htar'').
transitivity tar''. apply Htar''. apply Htar.
apply le_trans with (measure tar''). apply Htar. apply Htar''.
transitivity tar''. apply Htar''. apply Htar.
apply Nat.le_trans with (measure tar''). apply Htar. apply Htar''.
apply Htar.
apply Htar'', Hxy.
eapply le_lt_trans. apply Htar''. apply Hsize.
eapply Nat.le_lt_trans. apply Htar''. apply Hsize.

clear IHn. intro Hr.
destruct (IH _ Hr) as [IH1 IH2]; clear Hr IH.
Expand All @@ -405,8 +405,8 @@ Section correctness.
apply IH1. apply diag_ok; ti_auto.

transitivity (DS.union tarjan x y). apply DSUtils.le_union. apply IH1.
apply le_trans with (measure (DS.union tarjan x y)).
apply IH1. apply (measure_union_strict (size:=size)) in Hn; auto using lt_le_weak; num_lia.
apply Nat.le_trans with (measure (DS.union tarjan x y)).
apply IH1. apply (measure_union_strict (size:=size)) in Hn; auto using Nat.lt_le_incl; num_lia.
apply IH1. apply in_union.
Qed.

Expand Down
6 changes: 3 additions & 3 deletions theories/DKA_DFA_Language.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,12 +99,12 @@ Proof.
- compute. firstorder.
lia.
- intros j. simpl. unfold lang_union. rewrite IHn. clear IHn. intuition.
exists O; auto with arith. rewrite plus_comm. assumption.
exists O; auto with arith. rewrite Nat.add_comm. assumption.
destruct H0 as [k ? ?]. exists (Datatypes.S k); auto with arith. rewrite <- plus_n_Sm. assumption.
destruct H as [[|k] ? ?].
+ left. rewrite plus_comm in H0. assumption.
+ left. rewrite Nat.add_comm in H0. assumption.
+ right. exists k; auto with arith. rewrite <- plus_n_Sm in H0. assumption.
Qed.
Qed.

Lemma mx_leq_pointwise `{SL: SemiLattice}: forall n m A (M N: MX_ A n m),
M <== N <-> forall i j, i<n -> j<m -> !M i j <== !N i j.
Expand Down
10 changes: 4 additions & 6 deletions theories/DKA_Merge.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,26 +53,24 @@ Definition compare_DFAs T (equiv: DFA.t -> state -> state -> option T) A B :=

Lemma below_max_pi0: forall n m m', below n m -> below (pi0 n) (max (pi0 m) (pi1 m')).
Proof.
intros. rewrite lt_nat_spec, max_spec. eapply lt_le_trans. 2: apply Max.le_max_l.
intros. rewrite lt_nat_spec, max_spec. eapply Nat.lt_le_trans. 2: apply Nat.le_max_l.
rewrite <- lt_nat_spec. apply lt_pi0. assumption.
Qed.

Lemma below_max_pi1: forall n m m', below n m' -> below (pi1 n) (max (pi0 m) (pi1 m')).
Proof.
intros. rewrite lt_nat_spec, max_spec. eapply lt_le_trans. 2: apply Max.le_max_r.
intros. rewrite lt_nat_spec, max_spec. eapply Nat.lt_le_trans. 2: apply Nat.le_max_r.
rewrite <- lt_nat_spec. apply lt_pi1. assumption.
Qed.



Lemma merge_bounded: forall A B, bounded A -> bounded B -> bounded (merge_DFAs A B).
Proof.
intros A B HA HB. constructor.
intros a i. simpl. case_eq (pimatch i); intros p Hp.
apply below_max_pi0. apply (bounded_delta HA).
apply below_max_pi1. apply (bounded_delta HB).
rewrite lt_nat_spec. apply le_lt_trans with (nat_of_state (pi0 (delta A 0 0))).
apply le_O_n. rewrite <- lt_nat_spec. rapply below_max_pi0. apply (bounded_delta HA).
rewrite lt_nat_spec. apply Nat.le_lt_trans with (nat_of_state (pi0 (delta A 0 0))).
apply Nat.le_0_l. rewrite <- lt_nat_spec. rapply below_max_pi0. apply (bounded_delta HA).
unfold finaux, merge_DFAs.
apply NumSetProps.Props.fold_rec_nodep. apply NumSetProps.Props.fold_rec_nodep.
intro i. NumSetProps.setdec.
Expand Down
7 changes: 4 additions & 3 deletions theories/Model_MinPlus.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,14 +85,15 @@ Section protect.
Instance mp_ConverseSemiRing: ConverseIdemSemiRing mp_Graph.
Proof.
constructor; simpl; eauto with typeclass_instances.
destruct x; trivial. destruct y; trivial. destruct z; trivial. simpl. rewrite Plus.plus_assoc. reflexivity.
destruct x; trivial. destruct y; trivial. destruct z; trivial. simpl.
rewrite Nat.add_assoc. reflexivity.
destruct x; reflexivity.
destruct x; trivial. destruct y; trivial. simpl. rewrite plus_comm. reflexivity.
destruct x; trivial. destruct y; trivial. simpl. rewrite Nat.add_comm. reflexivity.
destruct y; reflexivity.
destruct x; trivial. destruct y; trivial. simpl. rewrite min_comm. reflexivity.
destruct y; reflexivity.
destruct x; trivial. destruct y; trivial; destruct z; trivial. simpl.
rewrite Min.plus_min_distr_r. reflexivity.
rewrite Nat.add_min_distr_r. reflexivity.
Qed.

Definition mp_IdemSemiRing: IdemSemiRing mp_Graph := Converse.CISR_ISR.
Expand Down
2 changes: 1 addition & 1 deletion theories/Monoid.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,7 @@ Section Props1.
intros until n.
rewrite <- (iter_once a) at 4.
rewrite <- iter_split.
rewrite plus_comm.
rewrite Nat.add_comm.
reflexivity.
Qed.

Expand Down
4 changes: 2 additions & 2 deletions theories/MxGraph.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,12 +85,12 @@ Ltac destruct_blocks :=
Ltac mx_intros i j Hi Hj :=
apply mx_equal'; intros i j Hi Hj;
match type of Hi with
| i < 0%nat => elim (lt_n_O _ Hi)
| i < 0%nat => elim (Nat.nlt_0_r _ Hi)
| i < 1%nat => destruct i; [clear Hi | elim (lt_n_1 Hi)]
| _ => idtac
end;
match type of Hj with
| j < 0%nat => elim (lt_n_O _ Hj)
| j < 0%nat => elim (Nat.nlt_0_r _ Hj)
| j < 1%nat => destruct j; [clear Hj | elim (lt_n_1 Hj)]
| _ => idtac
end.
Expand Down
16 changes: 8 additions & 8 deletions theories/MxSemiRing.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,35 +202,35 @@ Section Props2.
Proof.
simpl. intros. destruct_blocks.

rewrite (plus_comm m), sum_cut.
rewrite (Nat.add_comm m), sum_cut.
apply plus_compat.
apply sum_compat; intros.
destruct_blocks. reflexivity. lia_false.
rewrite (plus_comm m), sum_shift.
rewrite (Nat.add_comm m), sum_shift.
apply sum_compat; intros.
destruct_blocks. reflexivity.

rewrite (plus_comm m), sum_cut.
rewrite (Nat.add_comm m), sum_cut.
apply plus_compat.
apply sum_compat; intros.
destruct_blocks. reflexivity. lia_false.
rewrite (plus_comm m), sum_shift.
rewrite (Nat.add_comm m), sum_shift.
apply sum_compat; intros.
destruct_blocks. reflexivity.

rewrite (plus_comm m), sum_cut.
rewrite (Nat.add_comm m), sum_cut.
apply plus_compat.
apply sum_compat; intros.
destruct_blocks. reflexivity. lia_false.
rewrite (plus_comm m), sum_shift.
rewrite (Nat.add_comm m), sum_shift.
apply sum_compat; intros.
destruct_blocks. reflexivity.

rewrite (plus_comm m), sum_cut.
rewrite (Nat.add_comm m), sum_cut.
apply plus_compat.
apply sum_compat; intros.
destruct_blocks. reflexivity. lia_false.
rewrite (plus_comm m), sum_shift.
rewrite (Nat.add_comm m), sum_shift.
apply sum_compat; intros.
destruct_blocks. reflexivity.
Qed.
Expand Down
14 changes: 7 additions & 7 deletions theories/Numbers.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ Module Type NUM.

(* specification of operations and predicates, w.r.t. nat *)
Axiom S_nat_spec : forall n, nat_of_num (S n) = Datatypes.S (nat_of_num n).
Axiom max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
Axiom max_spec : forall n m, nat_of_num (max n m) = Nat.max (nat_of_num n) (nat_of_num m).
Axiom le_nat_spec : forall n m, n <= m <-> (nat_of_num n <= nat_of_num m)%nat.
Axiom lt_nat_spec : forall n m, n < m <-> (nat_of_num n < nat_of_num m)%nat.

Expand Down Expand Up @@ -136,12 +136,12 @@ Module NumUtils (N : NUM).
Proof.
constructor.
intros x; unfold Pos.le. rewrite le_nat_spec. auto with arith.
intros x y z Hxy Hyz. rewrite le_nat_spec in *. apply (le_trans _ (nat_of_num y)); auto.
intros x y z Hxy Hyz. rewrite le_nat_spec in *. apply (Nat.le_trans _ (nat_of_num y)); auto.
Qed.

#[global] Instance lt_transitive: Transitive lt.
Proof.
intros x y z Hxy Hyz. rewrite lt_nat_spec in *. apply (lt_trans _ (nat_of_num y)); auto.
intros x y z Hxy Hyz. rewrite lt_nat_spec in *. apply (Nat.lt_trans _ (nat_of_num y)); auto.
Qed.

Lemma num_peano_rec :
Expand Down Expand Up @@ -431,12 +431,12 @@ Module Positive <: NUM.
lia.
Qed.

Lemma max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
Lemma max_spec : forall n m, nat_of_num (max n m) = Nat.max (nat_of_num n) (nat_of_num m).
Proof.
intros n m. unfold max, Pos.max. fold (compare n m). destruct (compare_spec n m).
rewrite Max.max_r; trivial. apply lt_le_weak. rewrite <- lt_nat_spec. assumption.
subst. rewrite Max.max_r; trivial.
rewrite Max.max_l; trivial. apply lt_le_weak. rewrite <- lt_nat_spec. assumption.
rewrite Nat.max_r; trivial. apply Nat.lt_le_incl. rewrite <- lt_nat_spec. assumption.
subst. rewrite Nat.max_r; trivial.
rewrite Nat.max_l; trivial. apply Nat.lt_le_incl. rewrite <- lt_nat_spec. assumption.
Qed.


Expand Down
2 changes: 1 addition & 1 deletion theories/SemiLattice.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ Section FSumDef.
sum i (S k) f == sum i k f + f (i+k)%nat.
Proof.
revert i; induction k; intro i.
simpl. rewrite plus_0_r; apply plus_com.
simpl. rewrite Nat.add_0_r; apply plus_com.
change (sum i (S (S k)) f) with (f i + sum (S i) (S k) f).
rewrite IHk, plus_assoc. simpl. auto with compat.
Qed.
Expand Down
2 changes: 1 addition & 1 deletion theories/SemiRing.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -317,7 +317,7 @@ endtests*)
(plus (VLSet_to_X b) (dot (VLst_to_X a) y))
(VLSet_to_X (norm_aux' n b a y)))%nat.
Proof.
induction n; split; intros; try elim (lt_n_O _ H);
induction n; split; intros; try elim (Nat.nlt_0_r _ H);
destruct IHn as [IHnorm_aux IHnorm_aux'].

(* norm_aux *)
Expand Down