Commit 831f06c7 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Bump Coq 8.12.

parent fc53d921
......@@ -29,15 +29,15 @@ variables:
- api
## Build jobs
build-coq.8.10.2:
build-coq.8.12.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.2"
OPAM_PINS: "coq version 8.12.0"
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.2 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
OPAM_PINS: "coq version 8.12.0 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
except:
only:
- triggers
......
......@@ -10,7 +10,7 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.9.1" & < "8.11~") | (= "dev") }
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-iris" { (= "dev.2020-10-14.0.dc793c10") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -775,7 +775,7 @@ Section Soundness.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (simpl ; eapply not_elem_of_dom, is_fresh).
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
by eapply adequate_tctranslation__adequate_result.
(* (2) safety: *)
- intros t2 σ2 e2 _ Hsteps He2.
......@@ -788,7 +788,7 @@ Section Soundness.
assert (loc_fresh_in_expr e2)
by by apply loc_not_in_set_is_fresh_in_expr.
assert (σ2 !! = None)
by by (simpl ; eapply not_elem_of_dom).
by by (simpl ; eapply (not_elem_of_dom (D:=gset loc))).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_tctranslation__safe.
(* (3) bounded time: *)
......@@ -796,7 +796,7 @@ Section Soundness.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply not_elem_of_dom, is_fresh).
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_tctranslation__bounded.
Qed.
......
......@@ -525,7 +525,7 @@ Proof.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Hloc := Build_TickCounter (fresh (dom (gset loc) σ2)) : TickCounter).
assert (σ2 !! = None)
by (simpl ; eapply not_elem_of_dom, is_fresh).
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
by eapply adequate_translation__nadequate_result.
(* (2) safety: *)
- intros n t2 σ2 e2 _ Hnsteps Inm He2.
......@@ -538,9 +538,10 @@ Proof.
assert (loc_fresh_in_expr e2)
by by apply loc_not_in_set_is_fresh_in_expr.
assert (σ2 !! = None)
by by (simpl ; eapply not_elem_of_dom).
by by (simpl ; eapply (not_elem_of_dom (D:=gset loc))).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_translation__nsafe.
Qed.
End Simulation.
......@@ -375,7 +375,7 @@ Section Soundness.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply not_elem_of_dom, is_fresh).
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_tctranslation__bounded.
Qed.
......
......@@ -172,7 +172,7 @@ Proof.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (simpl ; eapply not_elem_of_dom, is_fresh).
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
by eapply adequate_tctranslation__adequate_result.
(* (2) safety: *)
- intros t2 σ2 e2 _ Hsteps He2.
......@@ -185,7 +185,7 @@ Proof.
assert (loc_fresh_in_expr e2)
by by apply loc_not_in_set_is_fresh_in_expr.
assert (σ2 !! = None)
by by (simpl ; eapply not_elem_of_dom).
by by (simpl ; eapply (not_elem_of_dom (D:=gset loc))).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
by eapply safe_tctranslation__safe.
Qed.
......@@ -306,7 +306,7 @@ Proof.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply not_elem_of_dom, is_fresh).
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
eapply simulation_exec_alt in Hnsteps ; auto.
assert (0 m-n)%Z by by eapply spec_tctranslation__bounded.
lia.
......
......@@ -781,8 +781,8 @@ Lemma find_spec_inductive: forall d D R F K F' M V x,
«find #x»
{{{ M', RET #(R x); mapsto_M M' Mem D F' K V M' }}}.
Proof using.
intros d. induction_wf IH: Wf_nat.lt_wf d.
introv HI HM Dx HC. iIntros "#?" (Φ) "!# [HM TC] HΦ /=".
intros d. induction_wf IH: Wf_nat.lt_wf d. intros d.
introv IH HI HM Dx HC. iIntros "#?" (Φ) "!# [HM TC] HΦ /=".
iDestruct "TC" as "[TCd TC]". wp_tick_rec.
assert (HV := HM _ Dx). destruct (M !! x) as [c|] eqn:? =>//.
iDestruct (mapsto_M_acc_same with "HM") as (v Hv) "[Hx HM]"=>//. wp_tick_load.
......
......@@ -50,7 +50,7 @@ Proof using.
intro x.
rewrite Astep_eq.
rewrite fact.
omega.
lia.
Qed.
Lemma iter_A_1_eq:
......@@ -60,17 +60,17 @@ Lemma iter_A_1_eq:
Proof using.
Opaque plus. (* TEMPORARY ugly *)
induction i; simpl; intros.
omega.
lia.
rewrite A_1_eq. rewrite IHi.
(* Now for some pain... *)
assert (0 < 2^i). { eauto using power_positive. }
assert (0 < 1+x). { omega. }
assert (0 < 1+x). { lia. }
generalize dependent (2^i); intro n; intros.
generalize dependent (1+x); intro y; intros.
assert (0 < n * y). { eauto using mult_positive. }
rewrite <- mult_assoc.
rewrite <- Mult.mult_assoc.
generalize dependent (n * y); intros ny; intros.
omega. (* phew! *)
lia. (* phew! *)
Transparent plus.
Qed.
......@@ -94,7 +94,7 @@ Local Notation inflationary_ :=
Lemma inflationary_Abase:
inflationary_ Abase.
Proof using.
unfold inflationary, Abase. intros. omega.
unfold inflationary, Abase. intros. lia.
Qed.
Lemma preserves_inflationary_Astep:
......@@ -103,7 +103,7 @@ Proof using.
unfold preserves, within, inflationary, Astep. intros.
eapply iter_inflationary with (okA := everywhere);
unfold preserves, within;
eauto using le_trans.
eauto using Nat.le_trans.
Qed.
Lemma Ak_inflationary:
......@@ -124,7 +124,7 @@ Proof using.
(* Kind of reproving the same thing again... *)
eapply iter_inflationary with (okA := everywhere);
unfold preserves, within;
eauto using le_trans, Ak_inflationary.
eauto using Nat.le_trans, Ak_inflationary.
Qed.
(* -------------------------------------------------------------------------- *)
......@@ -138,7 +138,7 @@ Proof using.
unfold inflationary, pointwise, Astep. intros.
simpl. rewrite iter_iter_1.
eapply iter_inflationary with (okA := everywhere);
unfold preserves, within; eauto using le_trans.
unfold preserves, within; eauto using Nat.le_trans.
Qed.
(* -------------------------------------------------------------------------- *)
......@@ -156,7 +156,7 @@ Proof using.
must carry the information that [A k] is inflationary. This is done by
picking an appropriate [okA]. *)
eapply iter_monotonic_in_n_specialized with (okA := inflationary_);
unfold pointwise; eauto using le_trans, inflationary_Abase,
unfold pointwise; eauto using Nat.le_trans, inflationary_Abase,
preserves_inflationary_Astep, inflationary_Astep.
Qed.
......@@ -191,7 +191,7 @@ Qed.
Lemma monotonic_Abase:
monotonic le le Abase.
Proof using.
unfold monotonic, Abase. intros. omega.
unfold monotonic, Abase. intros. lia.
Qed.
Lemma preserves_monotonic_Astep:
......@@ -201,10 +201,10 @@ Lemma preserves_monotonic_Astep:
monotonic le le (Astep f).
Proof using.
intros. intros x1 x2 ?. unfold Astep.
eapply le_trans; [ | eapply iter_monotonic_in_x; eauto ].
eapply Nat.le_trans; [ | eapply iter_monotonic_in_x; eauto ].
eapply iter_monotonic_in_n with (okA := everywhere);
unfold preserves, within; eauto using le_trans.
omega.
unfold preserves, within; eauto using Nat.le_trans.
lia.
Qed.
Lemma Akx_monotonic_in_x:
......@@ -258,16 +258,16 @@ Proof using.
rewrite A_1_eq.
(* We are now comparing two applications of [iter]. It suffices to
exploit the fact that [iter n f x] is monotonic in [f] and [x]. *)
eapply le_trans; [ eapply iter_monotonic_in_f | eapply iter_monotonic_in_x ].
eapply Nat.le_trans; [ eapply iter_monotonic_in_f | eapply iter_monotonic_in_x ].
(* from [iter_monotonic_in_f] *)
eauto.
eauto using le_trans.
eauto using Nat.le_trans.
split.
eauto with monotonic.
unfold pointwise. intros. rewrite A_1_eq. omega.
unfold pointwise. intros. rewrite A_1_eq. lia.
(* from [iter_monotonic_in_x] *)
eauto with monotonic.
omega.
lia.
Qed.
(* A slightly more powerful version of the previous lemma. It is not a
......@@ -280,7 +280,7 @@ Lemma A_2_log2_lower_bound:
Proof using.
(* It is somewhat miraculous that this auxiliary assertion holds. *)
assert (forall b n, n <= 2 * iter (log2 n) (A 1) b + 1).
{ intros. eapply (log2_induction (fun k n => n <= 2 * iter k (A 1) b + 1)). omega. omega.
{ intros. eapply (log2_induction (fun k n => n <= 2 * iter k (A 1) b + 1)). lia. lia.
intros. simpl. rewrite A_1_eq. eauto with div2. }
intros. rewrite Astep_eq. simpl. rewrite A_1_eq. eauto.
(* An alternative proof would consist in using [A_2_eq] together
......@@ -297,16 +297,16 @@ Proof using.
rewrite Astep_eq.
(* We are now comparing two applications of [iter]. It suffices to
exploit the fact that [iter n f x] is monotonic in [f] and [x]. *)
eapply le_trans; [ eapply iter_monotonic_in_f | eapply iter_monotonic_in_x ].
eapply Nat.le_trans; [ eapply iter_monotonic_in_f | eapply iter_monotonic_in_x ].
(* from [iter_monotonic_in_f] *)
eauto.
eauto using le_trans.
eauto using Nat.le_trans.
split.
eauto with monotonic.
unfold pointwise. eauto using A_2_lower_bound.
(* from [iter_monotonic_in_x] *)
eauto with monotonic.
omega.
lia.
Qed.
(* -------------------------------------------------------------------------- *)
......@@ -341,15 +341,15 @@ Proof using.
intros x ? k _.
induction k; intros; simpl.
(* Base. *)
omega.
lia.
(* Step. *)
rewrite Astep_eq.
(* [1 + x] is at least 2, and [iter] is monotonic in [n]. *)
transitivity (iter 2 (A k) x).
2: eapply iter_monotonic_in_n_specialized with (okA := everywhere);
unfold preserves, within;
eauto using le_trans, Ak_inflationary
with omega.
eauto using Nat.le_trans, Ak_inflationary
with lia.
(* Unfold [iter], and exploit the induction hypothesis (which is
possible because [A k] is monotonic). *)
simpl.
......@@ -357,10 +357,10 @@ Proof using.
2: eauto with monotonic.
(* Now, [A k k] is at least [A 0 k]. *)
transitivity (A 0 k).
2: eauto with monotonic omega.
2: eauto with monotonic lia.
(* And [A 0 k] is precisely [1 + k]. *)
rewrite Abase_eq at 1.
omega.
lia.
Qed.
Lemma Akx_tends_to_infinity_along_k:
......@@ -390,10 +390,10 @@ Proof using.
[A 0]. The result follows by transitivity. *)
intros.
assert (x < A 0 x).
{ rewrite Abase_eq. omega. }
{ rewrite Abase_eq. lia. }
assert (A 0 x <= A k x).
{ eauto with monotonic omega. }
omega.
{ eauto with monotonic lia. }
lia.
Qed.
(* For every [n] other than zero, [iter n (A k)] is strictly inflationary. *)
......@@ -403,12 +403,12 @@ Lemma iter_Ak_strictly_inflationary:
n > 0 ->
x < iter n (A k) x.
Proof using.
intros. destruct n; [ omega | ]. simpl.
intros. destruct n; [ lia | ]. simpl.
assert (x < A k x).
{ eapply Ak_strictly_inflationary. }
assert (A k x <= A k (iter n (A k) x)).
{ eauto using iter_Ak_inflationary with monotonic. }
omega.
lia.
Qed.
(* -------------------------------------------------------------------------- *)
......@@ -433,8 +433,8 @@ Proof using.
assert (A k1 x < A (1 + k1) x).
{ eauto using Akx_strictly_monotonic_in_k_step. }
assert (A (1 + k1) x <= A k2 x).
{ eauto with monotonic omega. }
omega.
{ eauto with monotonic lia. }
lia.
Qed.
Hint Resolve Akx_strictly_monotonic_in_k : monotonic typeclass_instances.
......@@ -455,12 +455,12 @@ Proof using.
implies that iterating over and over takes us to infinity. *)
intros f x hinfl.
assert (bound: forall i, x + i <= iter i f x).
{ intro. eapply iter_indexed_invariant; [ | omega ]. intros j y ?.
generalize (hinfl y). omega. }
{ intro. eapply iter_indexed_invariant; [ | lia ]. intros j y ?.
generalize (hinfl y). lia. }
(* Manual proof. *)
eapply prove_tends_towards_infinity.
intro y. exists y. intros z ?.
generalize (bound z). omega.
generalize (bound z). lia.
Qed.
(* The orbit of [A k] out of [x] goes to infinity. *)
......@@ -481,11 +481,11 @@ Lemma iter_inflationary_monotonic:
monotonic le le (fun i => iter i f x).
Proof using.
intros f x hinfl i j ?.
replace j with ((j - i) + i) by omega.
replace j with ((j - i) + i) by lia.
rewrite iter_iter.
generalize (iter i f x). intro y.
eapply iter_inflationary with (okA := everywhere);
unfold preserves, within, inflationary; eauto using le_trans.
unfold preserves, within, inflationary; eauto using Nat.le_trans.
Qed.
(* [fun i => iter i (A k) x] is monotonic. *)
......@@ -498,4 +498,3 @@ Proof using.
eapply iter_inflationary_monotonic.
intro. eapply Ak_inflationary. tauto.
Qed.
......@@ -21,7 +21,7 @@ Proof.
introv [ m ? ]. exists m. eauto.
(* Closure by intersection and subset. *)
introv [ m1 ? ] [ m2 ? ] ?. exists (max m1 m2). intros.
max_case; eauto with omega.
max_case; eauto with lia.
Qed.
(* Every subset of the form [le m] is a member of this filter. *)
......
......@@ -53,10 +53,10 @@ Lemma beta_x_succ_x:
betaf (fun k => A k x) (x + 1) = 0.
Proof using.
intros.
cut (betaf (fun k => A k x) (x + 1) < 1). { omega. }
cut (betaf (fun k => A k x) (x + 1) < 1). { lia. }
eapply betaf_spec_direct_contrapositive; eauto with monotonic.
{ rewrite Abase_eq. omega. }
{ rewrite A_1_eq. omega. }
{ rewrite Abase_eq. lia. }
{ rewrite A_1_eq. lia. }
Qed.
(* -------------------------------------------------------------------------- *)
......@@ -77,7 +77,7 @@ Proof.
(* By definition of [alphaf]: *)
rewrite alphaf_spec by eauto with monotonic.
(* By definition of [A]: *)
rewrite (@plus_comm (alphaf (fun k : nat => A k r) n)).
rewrite (@Nat.add_comm (alphaf (fun k : nat => A k r) n)).
rewrite Astep_eq. simpl.
(* Because [r] is at least 1, this iteration is taken at least once.
Because [A _] is inflationary, we have the following fact. *)
......@@ -87,7 +87,7 @@ Proof.
).
{ simpl.
eapply iter_at_least_once with (okA := fun _ => True);
unfold preserves, within; eauto using le_trans, Ak_inflationary. }
unfold preserves, within; eauto using Nat.le_trans, Ak_inflationary. }
(* Thus, we simplify: *)
rewrite <- fact. clear fact.
(* Furthermore, we have [n <= A (alphaf (fun k : nat => A k r) n) r]. *)
......@@ -95,9 +95,9 @@ Proof.
(* Thus, we simplify: *)
rewrite <- fact. clear fact.
(* Because [n + 1] is [A 0 n], we can transform the goal to: *)
replace (n + 1) with (A 0 n) by (rewrite Abase_eq; omega).
replace (n + 1) with (A 0 n) by (rewrite Abase_eq; lia).
(* The goal follows from the fact that [A] is monotonic. *)
eapply Akx_monotonic_in_k. omega.
eapply Akx_monotonic_in_k. lia.
(* Phew! *)
Qed.
......@@ -154,4 +154,3 @@ Proof using.
[A 2] is an exponential. *)
eapply A_2_log2_lower_bound.
Qed.
......@@ -59,8 +59,8 @@ Proof using f_tends_to_infinity.
unfold lower_bound, inverse.
eexists x0.
intros x ?.
destruct (le_gt_dec x x0); [ assumption | ].
forwards: hx0 x. omega. omega.
destruct (Compare_dec.le_gt_dec x x0); [ assumption | ].
forwards: hx0 x. lia. lia.
Qed.
(* -------------------------------------------------------------------------- *)
......@@ -149,14 +149,14 @@ Proof using f_tends_to_infinity f_monotonic f_strictly_monotonic.
intros.
(* If this equality does not hold, then, by the previous lemma,
[alphaf (f x)] must be less than [x]. *)
destruct (eq_nat_dec (alphaf (f x)) x); [ assumption | false ].
destruct (Nat.eq_decidable (alphaf (f x)) x); [ assumption | false ].
assert (h1: alphaf (f x) < x).
{ forwards: alphaf_f x. omega. }
{ forwards: alphaf_f x. lia. }
(* By exploiting the fact that [f] is strictly monotonic and
the lemma [f_alphaf], we find [f x < f x]. Contradiction. *)
forwards h2: f_strictly_monotonic h1.
forwards h3: f_alphaf (f x).
omega.
lia.
Qed.
(* [alphaf] is monotonic. *)
......@@ -213,7 +213,7 @@ Lemma betaf_spec_direct_contrapositive_le:
betaf y <= x.
Proof using f_tends_to_infinity f_monotonic.
intros.
cut (betaf y < 1 + x). omega.
cut (betaf y < 1 + x). lia.
eauto using betaf_spec_direct_contrapositive.
Qed.
......@@ -269,15 +269,15 @@ Proof using f_tends_to_infinity f_strictly_monotonic f_monotonic.
intros.
(* If this equality does not hold, then, by the previous lemma,
[x] must be less than [betaf (f x)]. *)
destruct (eq_nat_dec x (betaf (f x))); [ assumption | false ].
destruct (Nat.eq_decidable x (betaf (f x))); [ assumption | false ].
assert (h1: x < betaf (f x)).
{ forwards: betaf_f x. omega. }
{ forwards: betaf_f x. lia. }
(* By exploiting the fact that [f] is strictly monotonic and
the lemma [f_betaf], we find [f x < f x]. Contradiction. *)
forwards h2: f_strictly_monotonic h1.
forwards h3: f_betaf (f x).
eauto with monotonic omega.
omega.
eauto with monotonic lia.
lia.
Qed.
(* [betaf] is monotonic. *)
......@@ -309,7 +309,7 @@ Proof using f_tends_to_infinity f_strictly_monotonic f_monotonic.
[f (betaf y)] is less than or equal to [f (alphaf y)]. *)
eapply monotonic_lt_lt_implies_inverse_monotonic_le_le; [ eapply f_strictly_monotonic | ].
(* The proof is now easy: [y] is between these numbers. *)
eauto 3 using le_trans, f_betaf, f_alphaf.
eauto 3 using Nat.le_trans, f_betaf, f_alphaf.
Qed.
(* In the above lemma, if [y] is of the form [f x], then we have equality
......@@ -324,8 +324,8 @@ Proof using f_tends_to_infinity f_strictly_monotonic f_monotonic.
forwards: alphaf_f x.
forwards: betaf_f x.
forwards: betaf_le_alphaf (f x).
{ eauto with monotonic omega. }
split; omega.
{ eauto with monotonic lia. }
split; lia.
Qed.
(* The converse of the above property holds. That is, we have equality
......@@ -343,7 +343,7 @@ Proof using f_tends_to_infinity f_monotonic.
forwards h4: f_betaf y. assumption.
rewrite h1 in h4. clear h1.
rewrite h2 in h3, h4. clear h2.
omega.
lia.
Qed.
(* [betaf y] and [alphaf y] differ by at most one. *)
......@@ -355,14 +355,14 @@ Proof using f_tends_to_infinity.
intros.
(* If the goal does not hold, then there exists [z] which is
greater than [betaf y] and less than [alphaf y]. *)
destruct (le_gt_dec (alphaf y) (1 + betaf y)); [ assumption | false ].
destruct (Compare_dec.le_gt_dec (alphaf y) (1 + betaf y)); [ assumption | false ].
assert (zz: exists z, betaf y < z < alphaf y).
{ exists (betaf y + 1). omega. }
{ exists (betaf y + 1). lia. }
destruct zz as [ z [ hz1 hz2 ]].
(* This [z] has the properties [y < f z] and [f z < y]. Contradiction. *)
forwards: betaf_spec_reciprocal_contrapositive. eexact hz1.
forwards: alphaf_spec_reciprocal_contrapositive. eexact hz2.
omega.
lia.
Qed.
(* Because [f] is monotonic, [y < z] implies [betaf y < alphaf z]. *)
......@@ -379,7 +379,7 @@ Proof using f_tends_to_infinity f_monotonic.
eapply monotonic_le_le_implies_inverse_monotonic_lt_lt.
eexact f_monotonic.
(* The proof is now easy: [y < z] are between these numbers. *)
eauto 4 using le_lt_trans, lt_le_trans, f_betaf, f_alphaf.
eauto 4 using Nat.le_lt_trans, Nat.lt_le_trans, f_betaf, f_alphaf.
Qed.
(* [betaf] tends to infinity. *)
......@@ -399,5 +399,3 @@ Qed.
End Inverse.
Hint Resolve alphaf_monotonic betaf_monotonic : monotonic typeclass_instances.
......@@ -2,9 +2,8 @@
such as the property of being monotonic. *)
Set Implicit Arguments.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.Morphisms Coq.micromega.Lia.
From TLC Require Import LibTactics.
Require Import Omega.
(* -------------------------------------------------------------------------- *)
......@@ -104,7 +103,7 @@ Qed.
specific instance of the ordering relation that appears in the
conclusion. Furthermore, picking a specific instance of the
ordering relation that appears in the premise can help apply
[omega] to the premise. *)
[lia] to the premise. *)
Hint Resolve (@use_monotonic nat le nat le) (@use_monotonic nat lt nat lt)
: monotonic typeclass_instances.
......@@ -148,13 +147,13 @@ Require Import Coq.Arith.Arith.
Ltac prove_le_le_by_contraposition :=
match goal with h: ?a <= ?b |- ?x <= ?y =>
(destruct (le_gt_dec x y); [ assumption | ]);
assert (b < a); [ clear h | omega ]