From Coq Require Export Program.Tactics.
Obligation Tactic := idtac.The default and global localities for this command
outside sections are currently equivalent to the
combination of the standard meaning of "global" (as
described in the reference manual), "export" and
re-exporting for every surrounding module. It will
change to just "global" (with the meaning used by the
"Set" command) in a future release.
To preserve the current meaning in a forward
compatible way, use the attribute "#[global,export]"
and repeat the command with just "#[export]" in any
surrounding modules. If you are fine with the change
of semantics, disable this warning.
[deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default]
From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From Coq Require Import Eqdep_dec.

Utility: General Definitions, Results and Tactics

Tactic Notation "spec" hyp(H) :=
  match type of H with ?a -> _ =>
  let H1 := fresh in (assert (H1 : a);
  [| generalize (H H1); clear H H1; intro H]) end.

Basic logic

Lemma Is_true_iff_eq_true : forall x : bool, x = true <-> x.∀ x : bool, x = true ↔ x
Proof.∀ x : bool, x = true ↔ x
  split.x: bool
x = true → x
x: bool
x → x = true
  -x: bool
x = true → x by apply Is_true_eq_left.
  -x: bool
x → x = true by apply Is_true_eq_true.
Qed.

Lemma and_proper_l (A B C : Prop) : (A -> (B <-> C)) -> (A /\ B) <-> (A /\ C).A, B, C: Prop
(A → B ↔ C) → A ∧ B ↔ A ∧ C
Proof.A, B, C: Prop
(A → B ↔ C) → A ∧ B ↔ A ∧ C by firstorder. Qed.

Lemma impl_proper (A B C : Prop) : (A -> (B <-> C)) -> (A -> B) <-> (A -> C).A, B, C: Prop
(A → B ↔ C) → (A → B) ↔ (A → C)
Proof.A, B, C: Prop
(A → B ↔ C) → (A → B) ↔ (A → C) by firstorder. Qed.

Decidable propositions

Lemma Decision_iff : forall {P Q}, (P <-> Q) -> Decision P -> Decision Q.∀ P Q : Prop, P ↔ Q → Decision P → Decision Q
Proof.∀ P Q : Prop, P ↔ Q → Decision P → Decision Q by firstorder. Qed.

#[export] Instance bool_decision {b : bool} : Decision b :=
  match b with
  | true => left I
  | false => right (fun H => H)
  end.

Notation decide_eq := (fun x y => decide (x = y)).

Lemmas about transitive closure

Lemma transitive_tc_idempotent `(Transitive A R) :
  forall a b, R a b <-> tc R a b.A: Type
R: relation A
H: Transitive R
∀ a b : A, R a b ↔ tc R a b
Proof.A: Type
R: relation A
H: Transitive R
∀ a b : A, R a b ↔ tc R a b
  split; [by constructor |].A: Type
R: relation A
H: Transitive R
a, b: A
tc R a b → R a b
  induction 1; [done |].A: Type
R: relation A
H: Transitive R
x, y, z: A
H0: R x y
H1: tc R y z
IHtc: R y z
R x z
  by etransitivity.
Qed.

If a relation R reflects a predicate P, then its transitive closure will also reflect it.

Lemma tc_reflect
  `(R : relation A)
  (P : A -> Prop)
  (Hreflects : forall dm m, R dm m -> P m -> P dm)
  : forall dm m, tc R dm m -> P m -> P dm.A: Type
R: relation A
P: A → Prop
Hreflects: ∀ dm m : A, R dm m → P m → P dm
∀ dm m : A, tc R dm m → P m → P dm
Proof.A: Type
R: relation A
P: A → Prop
Hreflects: ∀ dm m : A, R dm m → P m → P dm
∀ dm m : A, tc R dm m → P m → P dm by induction 1; firstorder. Qed.

Characterization of tc in terms of the last transitivity step.

Lemma tc_r_iff `(R : relation A) :
  forall x z, tc R x z <-> R x z \/ exists y, tc R x y /\ R y z.A: Type
R: relation A
∀ x z : A,
  tc R x z ↔ R x z ∨ (∃ y : A, tc R x y ∧ R y z)
Proof.A: Type
R: relation A
∀ x z : A,
  tc R x z ↔ R x z ∨ (∃ y : A, tc R x y ∧ R y z)
  split.A: Type
R: relation A
x, z: A
tc R x z → R x z ∨ (∃ y : A, tc R x y ∧ R y z)
A: Type
R: relation A
x, z: A
R x z ∨ (∃ y : A, tc R x y ∧ R y z) → tc R x z
  -A: Type
R: relation A
x, z: A
tc R x z → R x z ∨ (∃ y : A, tc R x y ∧ R y z) intros Htc; apply tc_nsteps in Htc as (n & Hn & Hsteps).A: Type
R: relation A
x, z: A
n: nat
Hn: 0 < n
Hsteps: nsteps R n x z
R x z ∨ (∃ y : A, tc R x y ∧ R y z)
    induction Hsteps; [lia |].A: Type
R: relation A
n: nat
Hn: 0 < S n
x, y, z: A
H: R x y
Hsteps: nsteps R n y z
IHHsteps: 0 < n
→ R y z ∨ (∃ y0 : A, tc R y y0 ∧ R y0 z)
R x z ∨ (∃ y : A, tc R x y ∧ R y z)
    destruct n; [by inversion Hsteps; subst; left |].A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
IHHsteps: 0 < S n
→ R y z ∨ (∃ y0 : A, tc R y y0 ∧ R y0 z)
R x z ∨ (∃ y : A, tc R x y ∧ R y z)
    spec IHHsteps; [lia |]; right; destruct IHHsteps as [Hyz | (y0 & Hyy0 & Hy0z)].A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
Hyz: R y z
∃ y : A, tc R x y ∧ R y z
A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
y0: A
Hyy0: tc R y y0
Hy0z: R y0 z
∃ y : A, tc R x y ∧ R y z
    +A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
Hyz: R y z
∃ y : A, tc R x y ∧ R y z by exists y; split; [constructor |].
    +A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
y0: A
Hyy0: tc R y y0
Hy0z: R y0 z
∃ y : A, tc R x y ∧ R y z exists y0; split; [| done].A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
y0: A
Hyy0: tc R y y0
Hy0z: R y0 z
tc R x y0
      apply tc_nsteps.A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
y0: A
Hyy0: tc R y y0
Hy0z: R y0 z
∃ n : nat, 0 < n ∧ nsteps R n x y0
      apply tc_nsteps in Hyy0 as (m & Hm & Hyy0).A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
y0: A
m: nat
Hm: 0 < m
Hyy0: nsteps R m y y0
Hy0z: R y0 z
∃ n : nat, 0 < n ∧ nsteps R n x y0
      exists (S m); split; [lia |].A: Type
R: relation A
n: nat
Hn: 0 < S (S n)
x, y, z: A
H: R x y
Hsteps: nsteps R (S n) y z
y0: A
m: nat
Hm: 0 < m
Hyy0: nsteps R m y y0
Hy0z: R y0 z
nsteps R (S m) x y0
      by econstructor.
  -A: Type
R: relation A
x, z: A
R x z ∨ (∃ y : A, tc R x y ∧ R y z) → tc R x z intros [Hxz | (y & Hxy & Hyz)]; [by constructor |].A: Type
R: relation A
x, z, y: A
Hxy: tc R x y
Hyz: R y z
tc R x z
    by eapply tc_r.
Qed.

Lemma tc_wf_projected
  `{R1 : relation A} `(R2 : relation B) `{!Transitive R2} (f : A -> B) :
  (forall x y, R1 x y -> R2 (f x) (f y)) ->
  well_founded R2 -> well_founded (tc R1).A: Type
R1: relation A
B: Type
R2: relation B
Transitive0: Transitive R2
f: A → B
(∀ x y : A, R1 x y → R2 (f x) (f y))
→ wf R2 → wf (tc R1)
Proof.A: Type
R1: relation A
B: Type
R2: relation B
Transitive0: Transitive R2
f: A → B
(∀ x y : A, R1 x y → R2 (f x) (f y))
→ wf R2 → wf (tc R1)
  intros Hpreserve.A: Type
R1: relation A
B: Type
R2: relation B
Transitive0: Transitive R2
f: A → B
Hpreserve: ∀ x y : A, R1 x y → R2 (f x) (f y)
wf R2 → wf (tc R1)
  apply wf_projected with f.A: Type
R1: relation A
B: Type
R2: relation B
Transitive0: Transitive R2
f: A → B
Hpreserve: ∀ x y : A, R1 x y → R2 (f x) (f y)
∀ x y : A, tc R1 x y → R2 (f x) (f y)
  induction 1; [by apply Hpreserve |].A: Type
R1: relation A
B: Type
R2: relation B
Transitive0: Transitive R2
f: A → B
Hpreserve: ∀ x y : A, R1 x y → R2 (f x) (f y)
x, y, z: A
H: R1 x y
H0: tc R1 y z
IHtc: R2 (f y) (f z)
R2 (f x) (f z)
  transitivity (f y); [| done].A: Type
R1: relation A
B: Type
R2: relation B
Transitive0: Transitive R2
f: A → B
Hpreserve: ∀ x y : A, R1 x y → R2 (f x) (f y)
x, y, z: A
H: R1 x y
H0: tc R1 y z
IHtc: R2 (f y) (f z)
R2 (f x) (f y)
  by apply Hpreserve.
Qed.

Lemma tc_reflect_irreflexive
  `(R : relation A) `{!Irreflexive (tc R)} : Irreflexive R.A: Type
R: relation A
Irreflexive0: Irreflexive (tc R)
Irreflexive R
Proof.A: Type
R: relation A
Irreflexive0: Irreflexive (tc R)
Irreflexive R
 intros ? ?.A: Type
R: relation A
Irreflexive0: Irreflexive (tc R)
x: A
H: R x x
False
 by eapply irreflexivity with (R := tc R); [| constructor].
Qed.

Lemma Proper_reflects_Irreflexive
  `(R1 : relation A) `(R2 : relation B) (f : A -> B)
  : Proper (R1 ==> R2) f -> Irreflexive R2 -> Irreflexive R1.A: Type
R1: relation A
B: Type
R2: relation B
f: A → B
Proper (R1 ==> R2) f → Irreflexive R2 → Irreflexive R1
Proof.A: Type
R1: relation A
B: Type
R2: relation B
f: A → B
Proper (R1 ==> R2) f → Irreflexive R2 → Irreflexive R1
  intros Hproper Hirreflexive x Hx.A: Type
R1: relation A
B: Type
R2: relation B
f: A → B
Hproper: Proper (R1 ==> R2) f
Hirreflexive: Irreflexive R2
x: A
Hx: R1 x x
False
  by apply Hirreflexive with (f x), Hproper.
Qed.

Lemma Proper_tc
  `(R1 : relation A) `(R2 : relation B) (f : A -> B) `{!Transitive R2}
  : Proper (R1 ==> R2) f -> Proper (tc R1 ==> R2) f.A: Type
R1: relation A
B: Type
R2: relation B
f: A → B
Transitive0: Transitive R2
Proper (R1 ==> R2) f → Proper (tc R1 ==> R2) f
Proof.A: Type
R1: relation A
B: Type
R2: relation B
f: A → B
Transitive0: Transitive R2
Proper (R1 ==> R2) f → Proper (tc R1 ==> R2) f
  intros Hproper x y Hxy; induction Hxy; [by apply Hproper |].A: Type
R1: relation A
B: Type
R2: relation B
f: A → B
Transitive0: Transitive R2
Hproper: Proper (R1 ==> R2) f
x, y, z: A
H: R1 x y
Hxy: tc R1 y z
IHHxy: R2 (f y) (f z)
R2 (f x) (f z)
  by etransitivity; [apply Hproper |].
Qed.

Equality of dependent pairs

Lemma exists_proj1_sig {A : Type} (P : A -> Prop) (a : A) :
  (exists xP : {x | P x}, proj1_sig xP = a) <-> P a.A: Type
P: A → Prop
a: A
(∃ xP : {x : A | P x}, `xP = a) ↔ P a
Proof.A: Type
P: A → Prop
a: A
(∃ xP : {x : A | P x}, `xP = a) ↔ P a
  split.A: Type
P: A → Prop
a: A
(∃ xP : {x : A | P x}, `xP = a) → P a
A: Type
P: A → Prop
a: A
P a → ∃ xP : {x : A | P x}, `xP = a
  -A: Type
P: A → Prop
a: A
(∃ xP : {x : A | P x}, `xP = a) → P a by intros [[x Hx] [= ->]].
  -A: Type
P: A → Prop
a: A
P a → ∃ xP : {x : A | P x}, `xP = a by intro Ha; exists (exist _ a Ha).
Qed.

Lemma dec_sig_to_exist {A} {P} {P_dec : forall x : A, Decision (P x)} (a : dsig P)
  : exists (a' : A) (e : P a'), a = dexist a' e.A: Type
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
a: dsig P
∃ (a' : A) (e : P a'), a = dexist a' e
Proof.A: Type
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
a: dsig P
∃ (a' : A) (e : P a'), a = dexist a' e
  by exists (proj1_sig a), (proj2_dsig a); apply dsig_eq.
Qed.

Ltac destruct_dec_sig a a' e H := pose proof (dec_sig_to_exist a) as (a' & e & H).

Lemma dec_sig_sigT_eq
  {A} (P : A -> Prop) {P_dec : forall x, Decision (P x)}
  (F : A -> Type)
  (a : A)
  (b1 b2 : F a)
  (e1 e2 : P a)
  (pa1 := dexist a e1)
  (pa2 := dexist a e2)
  (Heqb : b1 = b2)
  : @existT _ (fun pa : dsig P => F (proj1_sig pa)) pa1 b1
  = @existT _ (fun pa : dsig P => F (proj1_sig pa)) pa2 b2.A: Type
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
pa1:= dexist a e1: dsig P
pa2:= dexist a e2: dsig P
Heqb: b1 = b2
existT pa1 b1 = existT pa2 b2
Proof.A: Type
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
pa1:= dexist a e1: dsig P
pa2:= dexist a e2: dsig P
Heqb: b1 = b2
existT pa1 b1 = existT pa2 b2
  subst b2 pa1 pa2.A: Type
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1: F a
e1, e2: P a
existT (dexist a e1) b1 = existT (dexist a e2) b1
  unfold dexist.A: Type
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1: F a
e1, e2: P a
existT (a ↾ bool_decide_pack (P a) e1) b1 =
existT (a ↾ bool_decide_pack (P a) e2) b1
  replace (bool_decide_pack (P a) e1) with (bool_decide_pack (P a) e2); [done |].A: Type
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1: F a
e1, e2: P a
bool_decide_pack (P a) e2 = bool_decide_pack (P a) e1
  by apply proof_irrel.
Qed.

Lemma dec_sig_sigT_eq_rev
  `{EqDecision A} (P : A -> Prop) {P_dec : forall x, Decision (P x)}
  (F : A -> Type)
  (a : A)
  (b1 b2 : F a)
  (e1 e2 : P a)
  (pa1 := dexist a e1)
  (pa2 := dexist a e2)
  : @existT _ (fun pa : dsig P => F (proj1_sig pa)) pa1 b1
      = @existT _ (fun pa : dsig P => F (proj1_sig pa)) pa2 b2 ->
    b1 = b2.A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
pa1:= dexist a e1: dsig P
pa2:= dexist a e2: dsig P
existT pa1 b1 = existT pa2 b2 → b1 = b2
Proof.A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
pa1:= dexist a e1: dsig P
pa2:= dexist a e2: dsig P
existT pa1 b1 = existT pa2 b2 → b1 = b2
  subst pa1 pa2.A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
existT (dexist a e1) b1 = existT (dexist a e2) b2
→ b1 = b2
  unfold dexist.A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
existT (a ↾ bool_decide_pack (P a) e1) b1 =
existT (a ↾ bool_decide_pack (P a) e2) b2 → b1 = b2
  replace (bool_decide_pack (P a) e1) with (bool_decide_pack (P a) e2); [| by apply proof_irrel].A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
existT (a ↾ bool_decide_pack (P a) e2) b1 =
existT (a ↾ bool_decide_pack (P a) e2) b2 → b1 = b2
  apply inj_pair2_eq_dec.A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
∀ x y : dsig P, {x = y} + {x ≠ y}
  intros x y; destruct (decide (` x = ` y)).A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
x, y: dsig P
e: `x = `y
{x = y} + {x ≠ y}
A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
x, y: dsig P
n: `x ≠ `y
{x = y} + {x ≠ y}
  -A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
x, y: dsig P
e: `x = `y
{x = y} + {x ≠ y} by left; apply dsig_eq.
  -A: Type
EqDecision0: EqDecision A
P: A → Prop
P_dec: ∀ x : A, Decision (P x)
F: A → Type
a: A
b1, b2: F a
e1, e2: P a
x, y: dsig P
n: `x ≠ `y
{x = y} + {x ≠ y} by right; intros ->.
Qed.

(* https://coq.discourse.group/t/writing-equality-decision-that-reduces-dec-x-x-for-opaque-x/551/2 *)

Lemma eq_dec_refl :
  forall {A : Type} (eq_dec : forall x y : A, {x = y} + {x <> y}) (x : A),
    eq_dec x x = left eq_refl.∀ (A : Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}) 
  (x : A), eq_dec x x = left eq_refl
Proof.∀ (A : Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}) 
  (x : A), eq_dec x x = left eq_refl
  intros A eq_dec x.A: Type
eq_dec: ∀ x y : A, {x = y} + {x ≠ y}
x: A
eq_dec x x = left eq_refl
  destruct (eq_dec x x); [| done].A: Type
eq_dec: ∀ x y : A, {x = y} + {x ≠ y}
x: A
e: x = x
left e = left eq_refl
  by rewrite K_dec_type with (P := fun prf => prf = eq_refl).
Qed.

Minimal elements

A minimal element of a subset S (defined by a predicate P) of some preordered set is defined as an element of S that is not greater than any other element in S.

Definition minimal_among `(R : relation A) (P : A -> Prop) (m : A) : Prop :=
  P m /\ (forall m', P m' -> R m' m -> R m m').

Remark minimal_among_le_0 : minimal_among le (const True) 0.minimal_among le (const True) 0
Proof.minimal_among le (const True) 0
  by split; [| lia].
Qed.

Section sec_find_least_among.

Given a decidable property on naturals and a natural number on which the property holds, we can compute the least natural number on which it holds.

Context
  (P : nat -> Prop)
  `{forall n, Decision (P n)}
  (bound : nat)
  (Hbound : P bound).

#[local] Fixpoint find_least_among_helper (dif : nat) : nat :=
  match dif with
  | 0 => bound
  | S dif' =>
    if decide (P (bound - dif))
      then bound - dif
      else find_least_among_helper dif'
  end.

Definition find_least_among : nat := find_least_among_helper bound.

#[local] Lemma find_least_among_helper_bounded :
  forall n, bound - n <= find_least_among_helper n <= bound.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n : nat,
  bound - n <= find_least_among_helper n <= bound
Proof.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n : nat,
  bound - n <= find_least_among_helper n <= bound by induction n; cbn; [| case_decide]; lia. Qed.

#[local] Lemma find_least_among_helper_has_property :
  forall n, P (find_least_among_helper n).P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n : nat, P (find_least_among_helper n)
Proof.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n : nat, P (find_least_among_helper n) by induction n; cbn; [| case_decide]. Qed.

#[local] Lemma find_least_among_helper_minimal :
  forall n m,
    bound - n <= m <= bound -> m < find_least_among_helper n -> ~ P m.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n m : nat,
  bound - n <= m <= bound
  → m < find_least_among_helper n → ¬ P m
Proof.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n m : nat,
  bound - n <= m <= bound
  → m < find_least_among_helper n → ¬ P m
  induction n; cbn; [by lia |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
IHn: ∀ m : nat,
  bound - n <= m <= bound
  → m < find_least_among_helper n → ¬ P m
∀ m : nat,
  bound - S n <= m <= bound
  → m <
    (if decide (P (bound - S n))
     then bound - S n
     else find_least_among_helper n) → ¬ P m
  case_decide; [by lia |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
IHn: ∀ m : nat,
  bound - n <= m <= bound
  → m < find_least_among_helper n → ¬ P m
H0: ¬ P (bound - S n)
∀ m : nat,
  bound - S n <= m <= bound
  → m < find_least_among_helper n → ¬ P m
  intros.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
IHn: ∀ m : nat,
  bound - n <= m <= bound
  → m < find_least_among_helper n → ¬ P m
H0: ¬ P (bound - S n)
m: nat
H1: bound - S n <= m <= bound
H2: m < find_least_among_helper n
¬ P m
  destruct (decide (m = bound - S n)); [by subst |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
IHn: ∀ m : nat,
  bound - n <= m <= bound
  → m < find_least_among_helper n → ¬ P m
H0: ¬ P (bound - S n)
m: nat
H1: bound - S n <= m <= bound
H2: m < find_least_among_helper n
n0: m ≠ bound - S n
¬ P m
  by apply IHn; lia.
Qed.

#[local] Lemma find_least_among_helper_is_minimal :
  forall n,
    minimal_among le
      (fun m => bound - n <= m <= bound /\ P m)
      (find_least_among_helper n).P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n : nat,
  minimal_among le
    (λ m : nat, bound - n <= m <= bound ∧ P m)
    (find_least_among_helper n)
Proof.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
∀ n : nat,
  minimal_among le
    (λ m : nat, bound - n <= m <= bound ∧ P m)
    (find_least_among_helper n)
  split; [split |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
bound - n <= find_least_among_helper n <= bound
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
P (find_least_among_helper n)
P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
∀ m' : nat,
  bound - n <= m' <= bound ∧ P m'
  → m' ≤ find_least_among_helper n
    → find_least_among_helper n ≤ m'
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
bound - n <= find_least_among_helper n <= bound by apply find_least_among_helper_bounded.
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
P (find_least_among_helper n) by apply find_least_among_helper_has_property.
  -P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n: nat
∀ m' : nat,
  bound - n <= m' <= bound ∧ P m'
  → m' ≤ find_least_among_helper n
    → find_least_among_helper n ≤ m' intros ? [Hm' Hpm'] Hle.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n, m': nat
Hm': bound - n <= m' <= bound
Hpm': P m'
Hle: m' ≤ find_least_among_helper n
find_least_among_helper n ≤ m'
    destruct (decide (find_least_among_helper  n = m')); [by lia |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
n, m': nat
Hm': bound - n <= m' <= bound
Hpm': P m'
Hle: m' ≤ find_least_among_helper n
n0: find_least_among_helper n ≠ m'
find_least_among_helper n ≤ m'
    by exfalso; eapply find_least_among_helper_minimal with n m'; [| lia |].
Qed.

Lemma find_least_among_is_minimal
  : minimal_among le P find_least_among.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
minimal_among le P find_least_among
Proof.P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
minimal_among le P find_least_among
  destruct (find_least_among_helper_is_minimal bound) as [[[_ ?] ?] Hmin'].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
H0: find_least_among_helper bound ≤ bound
H1: P (find_least_among_helper bound)
Hmin': ∀ m' : nat,
  bound - bound <= m' <= bound ∧ P m'
  → m' ≤ find_least_among_helper bound
    → find_least_among_helper bound ≤ m'
minimal_among le P find_least_among
  split; [done |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
H0: find_least_among_helper bound ≤ bound
H1: P (find_least_among_helper bound)
Hmin': ∀ m' : nat,
  bound - bound <= m' <= bound ∧ P m'
  → m' ≤ find_least_among_helper bound
    → find_least_among_helper bound ≤ m'
∀ m' : nat,
  P m' → m' ≤ find_least_among → find_least_among ≤ m'
  intros; apply Hmin'; [| done].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
H0: find_least_among_helper bound ≤ bound
H1: P (find_least_among_helper bound)
Hmin': ∀ m' : nat,
  bound - bound <= m' <= bound ∧ P m'
  → m' ≤ find_least_among_helper bound
    → find_least_among_helper bound ≤ m'
m': nat
H2: P m'
H3: m' ≤ find_least_among
bound - bound <= m' <= bound ∧ P m'
  split; [| done].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
H0: find_least_among_helper bound ≤ bound
H1: P (find_least_among_helper bound)
Hmin': ∀ m' : nat,
  bound - bound <= m' <= bound ∧ P m'
  → m' ≤ find_least_among_helper bound
    → find_least_among_helper bound ≤ m'
m': nat
H2: P m'
H3: m' ≤ find_least_among
bound - bound <= m' <= bound
  split; [by lia |].P: nat → Prop
H: ∀ n : nat, Decision (P n)
bound: nat
Hbound: P bound
H0: find_least_among_helper bound ≤ bound
H1: P (find_least_among_helper bound)
Hmin': ∀ m' : nat,
  bound - bound <= m' <= bound ∧ P m'
  → m' ≤ find_least_among_helper bound
    → find_least_among_helper bound ≤ m'
m': nat
H2: P m'
H3: m' ≤ find_least_among
m' ≤ bound
  by etransitivity.
Qed.

End sec_find_least_among.

A more concise definition of minimality for strict orders.

Definition strict_minimal_among `(R : relation A) (P : A -> Prop) (m : A) : Prop :=
  P m /\ (forall m', P m' -> ~ R m' m).

Remark strict_minimal_among_lt_0 : minimal_among lt (const True) 0.minimal_among lt (const True) 0
Proof.minimal_among lt (const True) 0
  by split; [| lia].
Qed.

The minimality definitions are equivalent for Asymmetric relations.

Lemma asymmetric_minimal_among_iff
  `(R : relation A) `{!Asymmetric R} (P : A -> Prop)
  : forall m, minimal_among R P m <-> strict_minimal_among R P m.A: Type
R: relation A
Asymmetric0: Asymmetric R
P: A → Prop
∀ m : A,
  minimal_among R P m ↔ strict_minimal_among R P m
Proof.A: Type
R: relation A
Asymmetric0: Asymmetric R
P: A → Prop
∀ m : A,
  minimal_among R P m ↔ strict_minimal_among R P m
  unfold minimal_among, strict_minimal_among; specialize asymmetry.A: Type
R: relation A
Asymmetric0: Asymmetric R
P: A → Prop
(∀ x y : A, R x y → R y x → False)
→ ∀ m : A,
    P m ∧ (∀ m' : A, P m' → R m' m → R m m')
    ↔ P m ∧ (∀ m' : A, P m' → ¬ R m' m)
  by firstorder.
Qed.

The minimality definitions are equivalent for StrictOrders.

Lemma strict_minimal_among_iff
  `(R : relation A) `{!StrictOrder R} (P : A -> Prop)
  : forall m, minimal_among R P m <-> strict_minimal_among R P m.A: Type
R: relation A
StrictOrder0: StrictOrder R
P: A → Prop
∀ m : A,
  minimal_among R P m ↔ strict_minimal_among R P m
Proof.A: Type
R: relation A
StrictOrder0: StrictOrder R
P: A → Prop
∀ m : A,
  minimal_among R P m ↔ strict_minimal_among R P m
  by apply asymmetric_minimal_among_iff; typeclasses eauto.
Qed.

Dually, a maximal element is a minimal element w.r.t. the inverse relation.

Definition maximal_among `(R : relation A) := minimal_among (flip R).

Definition strict_maximal_among `(R : relation A) := strict_minimal_among (flip R).

Comparison operators

Reflexive comparison operators

Class CompareReflexive {A} (compare : A -> A -> comparison) : Prop :=
  compare_eq : forall x y, compare x y = Eq <-> x = y.

#[global] Hint Mode CompareReflexive ! - : typeclass_instances.

Lemma compare_eq_refl {A} `{CompareReflexive A} :
  forall x, compare x x = Eq.A: Type
compare: A → A → comparison
H: CompareReflexive compare
∀ x : A, compare x x = Eq
Proof.A: Type
compare: A → A → comparison
H: CompareReflexive compare
∀ x : A, compare x x = Eq by intros; apply H. Qed.

Transitive comparison operators

Class CompareTransitive {A} (compare : A -> A -> comparison) : Prop :=
  compare_transitive : forall x y z c, compare x y = c -> compare y z = c -> compare x z = c.

#[global] Hint Mode CompareTransitive ! - : typeclass_instances.

Comparison operators that correspond to a strict order

Class CompareStrictOrder {A} (compare : A -> A -> comparison) : Prop :=
{
  StrictOrder_Reflexive :> CompareReflexive compare;
  StrictOrder_Transitive :> CompareTransitive compare;
}.A coercion will be introduced instead of an instance
in future versions when using ':>' in 'Class'
declarations. Replace ':>' with '::' (or use
'#[global] Existing Instance field.' for compatibility
with Coq < 8.18). Beware that the default locality for
'::' is #[export], as opposed to #[global] for ':>'
currently. Add an explicit #[global] attribute to the
field if you need to keep the current behavior. For
example: "Class foo := { #[global] field :: bar }."
[future-coercion-class-field,deprecated-since-8.17,deprecated,default]

#[global] Hint Mode CompareStrictOrder ! - : typeclass_instances.

Strictly-ordered comparisons entail decidable equality.

#[export] Instance compare_eq_dec {A} `{CompareStrictOrder A} : EqDecision A.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
EqDecision A
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
EqDecision A
  intros x y; destruct (compare x y) eqn: Hxy.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Eq
Decision (x = y)
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Lt
Decision (x = y)
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Gt
Decision (x = y)
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Eq
Decision (x = y) by left; apply compare_eq.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Lt
Decision (x = y) by right; intros ->; rewrite compare_eq_refl in Hxy.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Gt
Decision (x = y) by right; intros ->; rewrite compare_eq_refl in Hxy.
Qed.

Asymmetric comparison operators

Class CompareAsymmetric {A} (compare : A -> A -> comparison) : Prop :=
  compare_asymmetric : forall x y, compare x y = CompOpp (compare y x).

#[global] Hint Mode CompareAsymmetric ! - : typeclass_instances.

Lemma compare_asymmetric' {A} `{CompareAsymmetric A} :
  forall x y, compare x y = Lt <-> compare y x = Gt.A: Type
compare: A → A → comparison
H: CompareAsymmetric compare
∀ x y : A, compare x y = Lt ↔ compare y x = Gt
Proof.A: Type
compare: A → A → comparison
H: CompareAsymmetric compare
∀ x y : A, compare x y = Lt ↔ compare y x = Gt
  intros x y.A: Type
compare: A → A → comparison
H: CompareAsymmetric compare
x, y: A
compare x y = Lt ↔ compare y x = Gt
  rewrite compare_asymmetric.A: Type
compare: A → A → comparison
H: CompareAsymmetric compare
x, y: A
CompOpp (compare y x) = Lt ↔ compare y x = Gt
  by destruct (compare y x); cbn; firstorder congruence.
Qed.

Strictly-ordered comparisons are asymmetric.

#[export] Instance compare_asymmetric_intro {A} `{CompareStrictOrder A} :
  CompareAsymmetric compare.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
CompareAsymmetric compare
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
CompareAsymmetric compare
  intros x y; destruct (compare y x) eqn: Hyx.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Eq
compare x y = CompOpp Eq
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Lt
compare x y = CompOpp Lt
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Gt
compare x y = CompOpp Gt
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Eq
compare x y = CompOpp Eq by rewrite compare_eq in *.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Lt
compare x y = CompOpp Lt destruct (compare x y) eqn: Hxy; cbn; [| | done].A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Lt
Hxy: compare x y = Eq
Eq = Gt
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Lt
Hxy: compare x y = Lt
Lt = Gt
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Lt
Hxy: compare x y = Eq
Eq = Gt by apply compare_eq in Hxy; subst; rewrite compare_eq_refl in Hyx.
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Lt
Hxy: compare x y = Lt
Lt = Gt assert (Hxx : compare x x = Lt) by (eapply compare_transitive; done).A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Lt
Hxy: compare x y = Lt
Hxx: compare x x = Lt
Lt = Gt
      by rewrite compare_eq_refl in Hxx.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Gt
compare x y = CompOpp Gt destruct (compare x y) eqn: Hxy; cbn; [| done |].A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Gt
Hxy: compare x y = Eq
Eq = Lt
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Gt
Hxy: compare x y = Gt
Gt = Lt
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Gt
Hxy: compare x y = Eq
Eq = Lt by apply compare_eq in Hxy; subst; rewrite compare_eq_refl in Hyx.
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Gt
Hxy: compare x y = Gt
Gt = Lt assert (Hxx : compare x x = Gt) by (eapply compare_transitive; done).A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hyx: compare y x = Gt
Hxy: compare x y = Gt
Hxx: compare x x = Gt
Gt = Lt
      by rewrite compare_eq_refl in Hxx.
Qed.

compare_lt is the relation that corresponds to compare.

Definition compare_lt {A} (compare : A -> A -> comparison) (x y : A) : Prop :=
  compare x y = Lt.

#[export] Instance compare_lt_dec [A : Type]
  (compare : A -> A -> comparison) {Hord : CompareStrictOrder compare}
  : RelDecision (compare_lt compare).A: Type
compare: A → A → comparison
Hord: CompareStrictOrder compare
RelDecision (compare_lt compare)
Proof.A: Type
compare: A → A → comparison
Hord: CompareStrictOrder compare
RelDecision (compare_lt compare)
  intros x y; unfold compare_lt.A: Type
compare: A → A → comparison
Hord: CompareStrictOrder compare
x, y: A
Decision (compare x y = Lt)
  by typeclasses eauto.
Qed.

Properties of compare_lt

Lemma compare_lt_irreflexive {A} `{CompareReflexive A} :
  Irreflexive (compare_lt compare).A: Type
compare: A → A → comparison
H: CompareReflexive compare
Irreflexive (compare_lt compare)
Proof.A: Type
compare: A → A → comparison
H: CompareReflexive compare
Irreflexive (compare_lt compare)
  by intros x; compute; rewrite compare_eq_refl.
Qed.

Lemma compare_lt_transitive {A} `{CompareTransitive A} :
  Transitive (compare_lt compare).A: Type
compare: A → A → comparison
H: CompareTransitive compare
Transitive (compare_lt compare)
Proof.A: Type
compare: A → A → comparison
H: CompareTransitive compare
Transitive (compare_lt compare)
  by intros x y z Hxy Hyz; eapply compare_transitive.
Qed.

Lemma compare_lt_strict_order {A} `{CompareStrictOrder A} :
  StrictOrder (compare_lt compare).A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
StrictOrder (compare_lt compare)
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
StrictOrder (compare_lt compare)
  split.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
Irreflexive (compare_lt compare)
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
Transitive (compare_lt compare)
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
Irreflexive (compare_lt compare) by apply compare_lt_irreflexive.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
Transitive (compare_lt compare) by apply compare_lt_transitive.
Qed.

Lemma compare_lt_asymmetric {A} `{CompareStrictOrder A} :
  Asymmetric (compare_lt compare).A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
Asymmetric (compare_lt compare)
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
Asymmetric (compare_lt compare)
  unfold compare_lt; intros x y Hxy Hyx.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Lt
Hyx: compare y x = Lt
False
  assert (Hxx : compare x x = Lt) by (eapply compare_transitive; eauto).A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
x, y: A
Hxy: compare x y = Lt
Hyx: compare y x = Lt
Hxx: compare x x = Lt
False
  by rewrite compare_eq_refl in Hxx.
Qed.

Strictly ordered types

Class StrictlyComparable (X : Type) : Type :=
{
  compare : X -> X -> comparison;
  compare_strictorder :> CompareStrictOrder compare;
}.A coercion will be introduced instead of an instance
in future versions when using ':>' in 'Class'
declarations. Replace ':>' with '::' (or use
'#[global] Existing Instance field.' for compatibility
with Coq < 8.18). Beware that the default locality for
'::' is #[export], as opposed to #[global] for ':>'
currently. Add an explicit #[global] attribute to the
field if you need to keep the current behavior. For
example: "Class foo := { #[global] field :: bar }."
[future-coercion-class-field,deprecated-since-8.17,deprecated,default]
#[global] Hint Mode StrictlyComparable ! : typeclass_instances.

Definition comparable `(R : relation A) : relation A :=
  fun x y => exists c, CompSpec (=) R x y c.

Lemma tc_CompSpec :
  forall A (Peq Plt : relation A) (a b : A) (c : comparison),
  CompSpec Peq Plt a b c -> CompSpec Peq (tc Plt) a b c.∀ (A : Type) (Peq Plt : relation A) (a b : A) (c : comparison),
  CompSpec Peq Plt a b c → CompSpec Peq (tc Plt) a b c
Proof.∀ (A : Type) (Peq Plt : relation A) (a b : A) (c : comparison),
  CompSpec Peq Plt a b c → CompSpec Peq (tc Plt) a b c by intros *; inversion 1; subst; repeat constructor. Qed.

Lemma tc_comparable :
  forall A (R : relation A) (a b : A),
    comparable R a b -> comparable (tc R) a b.∀ (A : Type) (R : relation A) (a b : A),
  comparable R a b → comparable (tc R) a b
Proof.∀ (A : Type) (R : relation A) (a b : A),
  comparable R a b → comparable (tc R) a b
  by intros *; inversion 1; subst; econstructor; apply tc_CompSpec.
Qed.

#[export] Instance comparable_symmetric {A : Type} (R : A -> A -> Prop) :
  Symmetric (comparable R).A: Type
R: A → A → Prop
Symmetric (comparable R)
Proof.A: Type
R: A → A → Prop
Symmetric (comparable R)
  intros a b; intros [c Hc]; subst; inversion Hc; subst.A: Type
R: A → A → Prop
b: A
Hc: CompSpec eq R b b Eq
comparable R b b
A: Type
R: A → A → Prop
a, b: A
Hc: CompSpec eq R a b Lt
H: R a b
comparable R b a
A: Type
R: A → A → Prop
a, b: A
Hc: CompSpec eq R a b Gt
H: R b a
comparable R b a
  -A: Type
R: A → A → Prop
b: A
Hc: CompSpec eq R b b Eq
comparable R b b by eexists.
  -A: Type
R: A → A → Prop
a, b: A
Hc: CompSpec eq R a b Lt
H: R a b
comparable R b a by exists Gt; constructor.
  -A: Type
R: A → A → Prop
a, b: A
Hc: CompSpec eq R a b Gt
H: R b a
comparable R b a by exists Lt; constructor.
Qed.

#[export] Instance comparable_reflexive {A : Type} (R : A -> A -> Prop) :
  Reflexive (comparable R).A: Type
R: A → A → Prop
Reflexive (comparable R)
Proof.A: Type
R: A → A → Prop
Reflexive (comparable R) by intro; exists Eq; constructor. Qed.

#[export] Instance comparable_dec
  `(R : relation A) `{EqDecision A} `{!RelDecision R} :
  RelDecision (comparable R).A: Type
R: relation A
EqDecision0: EqDecision A
RelDecision0: RelDecision R
RelDecision (comparable R)
Proof.A: Type
R: relation A
EqDecision0: EqDecision A
RelDecision0: RelDecision R
RelDecision (comparable R)
  intros a b.A: Type
R: relation A
EqDecision0: EqDecision A
RelDecision0: RelDecision R
a, b: A
Decision (comparable R a b)
  destruct (decide (a = b)); [by subst; left |].A: Type
R: relation A
EqDecision0: EqDecision A
RelDecision0: RelDecision R
a, b: A
n: a ≠ b
Decision (comparable R a b)
  destruct (decide (R a b)); [by left; exists Lt; constructor |].A: Type
R: relation A
EqDecision0: EqDecision A
RelDecision0: RelDecision R
a, b: A
n: a ≠ b
n0: ¬ R a b
Decision (comparable R a b)
  destruct (decide (R b a)); [by left; exists Gt; constructor |].A: Type
R: relation A
EqDecision0: EqDecision A
RelDecision0: RelDecision R
a, b: A
n: a ≠ b
n0: ¬ R a b
n1: ¬ R b a
Decision (comparable R a b)
  by right; intros [c Hc]; inversion Hc.
Qed.

Comparison for subtypes

Definition dsig_compare
  {X} `{StrictlyComparable X} (P : X -> Prop) {Pdec : forall x, Decision (P x)}
  (x y : dsig P) : comparison :=
    compare (`x) (`y).

Lemma dsig_compare_reflexive
  {X} `{StrictlyComparable X} (P : X -> Prop) {Pdec : forall x, Decision (P x)}
  : CompareReflexive (dsig_compare P).X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareReflexive (dsig_compare P)
Proof.X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareReflexive (dsig_compare P)
  by intros x y; unfold dsig_compare; rewrite dsig_eq, compare_eq.
Qed.

Lemma dsig_compare_transitive
  {X} `{StrictlyComparable X} (P : X -> Prop) {Pdec : forall x, Decision (P x)}
  : CompareTransitive (dsig_compare P).X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareTransitive (dsig_compare P)
Proof.X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareTransitive (dsig_compare P)
  by intros x y z; unfold dsig_compare; apply compare_transitive.
Qed.

Lemma CompareStrictOrder_dsig_compare
  {X} `{StrictlyComparable X} (P : X -> Prop) {Pdec : forall x, Decision (P x)}
  : CompareStrictOrder (dsig_compare P).X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareStrictOrder (dsig_compare P)
Proof.X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareStrictOrder (dsig_compare P)
  split.X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareReflexive (dsig_compare P)
X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareTransitive (dsig_compare P)
  -X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareReflexive (dsig_compare P) by apply dsig_compare_reflexive.
  -X: Type
H: StrictlyComparable X
P: X → Prop
Pdec: ∀ x : X, Decision (P x)
CompareTransitive (dsig_compare P) by apply dsig_compare_transitive.
Qed.

#[export] Instance StrictlyComparable_dsig
  {X} `{StrictlyComparable X} (P : X -> Prop) {Pdec : forall x, Decision (P x)}
  {Inh : Inhabited (dsig P)}
  : StrictlyComparable (dsig P) :=
{
  compare := dsig_compare P;
  compare_strictorder := CompareStrictOrder_dsig_compare P
}.

Comparison for options

Definition option_compare
  (X : Type) `{StrictlyComparable X}
  (ox oy : option X) : comparison :=
  match ox, oy with
  | None, None => Eq
  | None, _ => Lt
  | _, None => Gt
  | Some x, Some y => compare x y
  end.

Lemma option_compare_reflexive
  (X : Type) `{StrictlyComparable X}
  : CompareReflexive (option_compare X).X: Type
H: StrictlyComparable X
CompareReflexive (option_compare X)
Proof.X: Type
H: StrictlyComparable X
CompareReflexive (option_compare X)
  by intros [x |] [y |]; cbn; rewrite ?compare_eq; firstorder congruence.
Qed.

Lemma option_compare_transitive
  (X : Type) `{StrictlyComparable X}
  : CompareTransitive (option_compare X).X: Type
H: StrictlyComparable X
CompareTransitive (option_compare X)
Proof.X: Type
H: StrictlyComparable X
CompareTransitive (option_compare X)
  intros [x |] [y |] [z |] [| |]; simpl; intros Hxy Hyz; try done.X: Type
H: StrictlyComparable X
x, y, z: X
Hxy: compare x y = Eq
Hyz: compare y z = Eq
compare x z = Eq
X: Type
H: StrictlyComparable X
x, y, z: X
Hxy: compare x y = Lt
Hyz: compare y z = Lt
compare x z = Lt
X: Type
H: StrictlyComparable X
x, y, z: X
Hxy: compare x y = Gt
Hyz: compare y z = Gt
compare x z = Gt
  -X: Type
H: StrictlyComparable X
x, y, z: X
Hxy: compare x y = Eq
Hyz: compare y z = Eq
compare x z = Eq by apply (compare_transitive x y z).
  -X: Type
H: StrictlyComparable X
x, y, z: X
Hxy: compare x y = Lt
Hyz: compare y z = Lt
compare x z = Lt by apply (compare_transitive x y z).
  -X: Type
H: StrictlyComparable X
x, y, z: X
Hxy: compare x y = Gt
Hyz: compare y z = Gt
compare x z = Gt by apply (compare_transitive x y z).
Qed.

Lemma CompareStrictOrder_option_compare
  (X : Type) `{StrictlyComparable X}
  : CompareStrictOrder (option_compare X).X: Type
H: StrictlyComparable X
CompareStrictOrder (option_compare X)
Proof.X: Type
H: StrictlyComparable X
CompareStrictOrder (option_compare X)
  split.X: Type
H: StrictlyComparable X
CompareReflexive (option_compare X)
X: Type
H: StrictlyComparable X
CompareTransitive (option_compare X)
  -X: Type
H: StrictlyComparable X
CompareReflexive (option_compare X) by apply option_compare_reflexive.
  -X: Type
H: StrictlyComparable X
CompareTransitive (option_compare X) by apply option_compare_transitive.
Qed.

#[export] Instance StrictlyComparable_option
  (X : Type) `{StrictlyComparable X} : StrictlyComparable (option X) :=
{
  compare := option_compare X;
  compare_strictorder := CompareStrictOrder_option_compare _;
}.

Comparison for pairs and triples

Definition pair_compare
  (X Y : Type) `{StrictlyComparable X} `{StrictlyComparable Y}
  : (X * Y) -> (X * Y) -> comparison :=
  fun '(x1, y1) '(x2, y2) =>
  match compare x1 x2 with
  | Eq => compare y1 y2
  | c => c
  end.

Lemma pair_compare_reflexive
  (X Y : Type) `{StrictlyComparable X} `{StrictlyComparable Y}
  : CompareReflexive (pair_compare X Y).X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareReflexive (pair_compare X Y)
Proof.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareReflexive (pair_compare X Y)
  intros [x1 y1] [x2 y2]; split; cbn.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
match compare x1 x2 with
| Eq => compare y1 y2
| Lt => Lt
| Gt => Gt
end = Eq → (x1, y1) = (x2, y2)
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
(x1, y1) = (x2, y2)
→ match compare x1 x2 with
  | Eq => compare y1 y2
  | Lt => Lt
  | Gt => Gt
  end = Eq
  -X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
match compare x1 x2 with
| Eq => compare y1 y2
| Lt => Lt
| Gt => Gt
end = Eq → (x1, y1) = (x2, y2) destruct (compare x1 x2) eqn: Hx, (compare y1 y2) eqn: Hy; intros [=].X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
Hx: compare x1 x2 = Eq
Hy: compare y1 y2 = Eq
(x1, y1) = (x2, y2)
    by apply compare_eq in Hx, Hy; subst.
  -X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
(x1, y1) = (x2, y2)
→ match compare x1 x2 with
  | Eq => compare y1 y2
  | Lt => Lt
  | Gt => Gt
  end = Eq by intros [= -> ->]; cbn; rewrite !compare_eq_refl.
Qed.

Lemma pair_compare_lt
  {X Y : Type} `{StrictlyComparable X} `{StrictlyComparable Y} :
    forall (x1 x2 : X) (y1 y2 : Y) (c : comparison),
      pair_compare X Y (x1, y1) (x2, y2) = c ->
        compare x1 x2 = c \/ x1 = x2 /\ compare y1 y2 = c.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
∀ (x1 x2 : X) (y1 y2 : Y) (c : comparison),
  pair_compare X Y (x1, y1) (x2, y2) = c
  → compare x1 x2 = c ∨ x1 = x2 ∧ compare y1 y2 = c
Proof.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
∀ (x1 x2 : X) (y1 y2 : Y) (c : comparison),
  pair_compare X Y (x1, y1) (x2, y2) = c
  → compare x1 x2 = c ∨ x1 = x2 ∧ compare y1 y2 = c
  cbn; intros x1 x2 y1 y2 c Hcmp.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1, x2: X
y1, y2: Y
c: comparison
Hcmp: match compare x1 x2 with
| Eq => compare y1 y2
| Lt => Lt
| Gt => Gt
end = c
compare x1 x2 = c ∨ x1 = x2 ∧ compare y1 y2 = c
  rewrite <- compare_eq.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1, x2: X
y1, y2: Y
c: comparison
Hcmp: match compare x1 x2 with
| Eq => compare y1 y2
| Lt => Lt
| Gt => Gt
end = c
compare x1 x2 = c
∨ compare x1 x2 = Eq ∧ compare y1 y2 = c
  by destruct (compare x1 x2), (compare y1 y2); auto.
Qed.

Lemma pair_compare_transitive
  {X Y : Type} `{StrictlyComparable X} `{StrictlyComparable Y}
  : CompareTransitive (pair_compare X Y).X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareTransitive (pair_compare X Y)
Proof.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareTransitive (pair_compare X Y)
  intros [x1 y1] [x2 y2] [x3 y3] comp H12 H23.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H12: pair_compare X Y (x1, y1) (x2, y2) = comp
H23: pair_compare X Y (x2, y2) (x3, y3) = comp
pair_compare X Y (x1, y1) (x3, y3) = comp
  destruct comp eqn: H_comp.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Eq
H12: pair_compare X Y (x1, y1) (x2, y2) = Eq
H23: pair_compare X Y (x2, y2) (x3, y3) = Eq
pair_compare X Y (x1, y1) (x3, y3) = Eq
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H12: pair_compare X Y (x1, y1) (x2, y2) = Lt
H23: pair_compare X Y (x2, y2) (x3, y3) = Lt
pair_compare X Y (x1, y1) (x3, y3) = Lt
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H12: pair_compare X Y (x1, y1) (x2, y2) = Gt
H23: pair_compare X Y (x2, y2) (x3, y3) = Gt
pair_compare X Y (x1, y1) (x3, y3) = Gt
  -X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Eq
H12: pair_compare X Y (x1, y1) (x2, y2) = Eq
H23: pair_compare X Y (x2, y2) (x3, y3) = Eq
pair_compare X Y (x1, y1) (x3, y3) = Eq by apply pair_compare_reflexive; apply pair_compare_reflexive in H12, H23; congruence.
  -X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H12: pair_compare X Y (x1, y1) (x2, y2) = Lt
H23: pair_compare X Y (x2, y2) (x3, y3) = Lt
pair_compare X Y (x1, y1) (x3, y3) = Lt destruct (pair_compare_lt x1 x2 y1 y2 Lt H12) as [left | [-> right]],
             (pair_compare_lt x2 x3 y2 y3 Lt H23) as [left' | [-> right']]; cbn.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H12: pair_compare X Y (x1, y1) (x2, y2) = Lt
H23: pair_compare X Y (x2, y2) (x3, y3) = Lt
left: compare x1 x2 = Lt
left': compare x2 x3 = Lt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
left: compare x1 x3 = Lt
H23: pair_compare X Y (x3, y2) (x3, y3) = Lt
H12: pair_compare X Y (x1, y1) (x3, y2) = Lt
right': compare y2 y3 = Lt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H12: pair_compare X Y (x2, y1) (x2, y2) = Lt
H23: pair_compare X Y (x2, y2) (x3, y3) = Lt
right: compare y1 y2 = Lt
left': compare x2 x3 = Lt
match compare x2 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H23: pair_compare X Y (x3, y2) (x3, y3) = Lt
H12: pair_compare X Y (x3, y1) (x3, y2) = Lt
right: compare y1 y2 = Lt
right': compare y2 y3 = Lt
match compare x3 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H12: pair_compare X Y (x1, y1) (x2, y2) = Lt
H23: pair_compare X Y (x2, y2) (x3, y3) = Lt
left: compare x1 x2 = Lt
left': compare x2 x3 = Lt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt by replace (compare x1 x3) with Lt by (symmetry; eapply compare_transitive; done).
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
left: compare x1 x3 = Lt
H23: pair_compare X Y (x3, y2) (x3, y3) = Lt
H12: pair_compare X Y (x1, y1) (x3, y2) = Lt
right': compare y2 y3 = Lt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt by rewrite left.
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H12: pair_compare X Y (x2, y1) (x2, y2) = Lt
H23: pair_compare X Y (x2, y2) (x3, y3) = Lt
right: compare y1 y2 = Lt
left': compare x2 x3 = Lt
match compare x2 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt by rewrite left'.
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Lt
H23: pair_compare X Y (x3, y2) (x3, y3) = Lt
H12: pair_compare X Y (x3, y1) (x3, y2) = Lt
right: compare y1 y2 = Lt
right': compare y2 y3 = Lt
match compare x3 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Lt by rewrite compare_eq_refl; eapply compare_transitive.
  -X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H12: pair_compare X Y (x1, y1) (x2, y2) = Gt
H23: pair_compare X Y (x2, y2) (x3, y3) = Gt
pair_compare X Y (x1, y1) (x3, y3) = Gt destruct (pair_compare_lt x1 x2 y1 y2 Gt H12) as [left | [-> right]],
             (pair_compare_lt x2 x3 y2 y3 Gt H23) as [left' | [-> right']]; cbn.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H12: pair_compare X Y (x1, y1) (x2, y2) = Gt
H23: pair_compare X Y (x2, y2) (x3, y3) = Gt
left: compare x1 x2 = Gt
left': compare x2 x3 = Gt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
left: compare x1 x3 = Gt
H23: pair_compare X Y (x3, y2) (x3, y3) = Gt
H12: pair_compare X Y (x1, y1) (x3, y2) = Gt
right': compare y2 y3 = Gt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H12: pair_compare X Y (x2, y1) (x2, y2) = Gt
H23: pair_compare X Y (x2, y2) (x3, y3) = Gt
right: compare y1 y2 = Gt
left': compare x2 x3 = Gt
match compare x2 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H23: pair_compare X Y (x3, y2) (x3, y3) = Gt
H12: pair_compare X Y (x3, y1) (x3, y2) = Gt
right: compare y1 y2 = Gt
right': compare y2 y3 = Gt
match compare x3 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H12: pair_compare X Y (x1, y1) (x2, y2) = Gt
H23: pair_compare X Y (x2, y2) (x3, y3) = Gt
left: compare x1 x2 = Gt
left': compare x2 x3 = Gt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt by replace (compare x1 x3) with Gt by (symmetry; eapply compare_transitive; done).
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
x1: X
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
left: compare x1 x3 = Gt
H23: pair_compare X Y (x3, y2) (x3, y3) = Gt
H12: pair_compare X Y (x1, y1) (x3, y2) = Gt
right': compare y2 y3 = Gt
match compare x1 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt by rewrite left.
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1: Y
x2: X
y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H12: pair_compare X Y (x2, y1) (x2, y2) = Gt
H23: pair_compare X Y (x2, y2) (x3, y3) = Gt
right: compare y1 y2 = Gt
left': compare x2 x3 = Gt
match compare x2 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt by rewrite left'.
    +X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
y1, y2: Y
x3: X
y3: Y
comp: comparison
H_comp: comp = Gt
H23: pair_compare X Y (x3, y2) (x3, y3) = Gt
H12: pair_compare X Y (x3, y1) (x3, y2) = Gt
right: compare y1 y2 = Gt
right': compare y2 y3 = Gt
match compare x3 x3 with
| Eq => compare y1 y3
| Lt => Lt
| Gt => Gt
end = Gt by rewrite compare_eq_refl; eapply compare_transitive.
Qed.

Lemma CompareStrictOrder_pair_compare
  {X Y : Type} `{StrictlyComparable X} `{StrictlyComparable Y}
  : CompareStrictOrder (pair_compare X Y).X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareStrictOrder (pair_compare X Y)
Proof.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareStrictOrder (pair_compare X Y)
  split.X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareReflexive (pair_compare X Y)
X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareTransitive (pair_compare X Y)
  -X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareReflexive (pair_compare X Y) by apply pair_compare_reflexive.
  -X, Y: Type
H: StrictlyComparable X
H0: StrictlyComparable Y
CompareTransitive (pair_compare X Y) by apply pair_compare_transitive.
Qed.

#[export] Instance StrictlyComparable_pair
  (X Y : Type) `{StrictlyComparable X} `{StrictlyComparable Y} : StrictlyComparable (X * Y) :=
{
  compare := pair_compare X Y;
  compare_strictorder := CompareStrictOrder_pair_compare;
}.

#[export] Instance TripleStrictlyComparable
  (X Y Z : Type) `{StrictlyComparable X} `{StrictlyComparable Y} `{StrictlyComparable Z}
  : StrictlyComparable (X * Y * Z) :=
{
  compare := pair_compare (X * Y) Z;
  compare_strictorder := CompareStrictOrder_pair_compare;
}.

Comparison for lists

Fixpoint list_compare
  (A : Type) `{StrictlyComparable A}
  (l1 l2 : list A) : comparison :=
  match l1, l2 with
  | [], [] => Eq
  | [], _ => Lt
  | _, [] => Gt
  | h1 :: t1, h2 :: t2 =>
    match compare h1 h2 with
    | Eq => list_compare A t1 t2
    | cmp => cmp
    end
  end.

Lemma list_compare_reflexive
  {A : Type} `{StrictlyComparable A}
  : CompareReflexive (list_compare A).A: Type
H: StrictlyComparable A
CompareReflexive (list_compare A)
Proof.A: Type
H: StrictlyComparable A
CompareReflexive (list_compare A)
  intros l1; induction l1 as [| h1 t1]; intros [| h2 t2]; [done.. |].A: Type
H: StrictlyComparable A
h1: A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
list_compare A (h1 :: t1) (h2 :: t2) = Eq
↔ h1 :: t1 = h2 :: t2
  split; cbn.A: Type
H: StrictlyComparable A
h1: A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
match compare h1 h2 with
| Eq => list_compare A t1 t2
| Lt => Lt
| Gt => Gt
end = Eq → h1 :: t1 = h2 :: t2
A: Type
H: StrictlyComparable A
h1: A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
h1 :: t1 = h2 :: t2
→ match compare h1 h2 with
  | Eq => list_compare A t1 t2
  | Lt => Lt
  | Gt => Gt
  end = Eq
  -A: Type
H: StrictlyComparable A
h1: A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
match compare h1 h2 with
| Eq => list_compare A t1 t2
| Lt => Lt
| Gt => Gt
end = Eq → h1 :: t1 = h2 :: t2 intros Heq.A: Type
H: StrictlyComparable A
h1: A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
Heq: match compare h1 h2 with
| Eq => list_compare A t1 t2
| Lt => Lt
| Gt => Gt
end = Eq
h1 :: t1 = h2 :: t2
    destruct (compare h1 h2) eqn: Hcmp; [| done..].A: Type
H: StrictlyComparable A
h1: A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
Hcmp: compare h1 h2 = Eq
Heq: list_compare A t1 t2 = Eq
h1 :: t1 = h2 :: t2
    apply compare_eq in Hcmp as ->.A: Type
H: StrictlyComparable A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
Heq: list_compare A t1 t2 = Eq
h2 :: t1 = h2 :: t2
    by apply IHt1 in Heq as ->.
  -A: Type
H: StrictlyComparable A
h1: A
t1: list A
IHt1: ∀ y : list A, list_compare A t1 y = Eq ↔ t1 = y
h2: A
t2: list A
h1 :: t1 = h2 :: t2
→ match compare h1 h2 with
  | Eq => list_compare A t1 t2
  | Lt => Lt
  | Gt => Gt
  end = Eq inversion 1; subst.A: Type
H: StrictlyComparable A
t2: list A
h2: A
H0: h2 :: t2 = h2 :: t2
IHt1: ∀ y : list A, list_compare A t2 y = Eq ↔ t2 = y
match compare h2 h2 with
| Eq => list_compare A t2 t2
| Lt => Lt
| Gt => Gt
end = Eq
    by rewrite compare_eq_refl, IHt1.
Qed.

Lemma list_compare_transitive
  {A : Type} `{StrictlyComparable A}
  : CompareTransitive (list_compare A).A: Type
H: StrictlyComparable A
CompareTransitive (list_compare A)
Proof.A: Type
H: StrictlyComparable A
CompareTransitive (list_compare A)
  intros l1 l2 l3; revert l1 l3.A: Type
H: StrictlyComparable A
l2: list A
∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 l2 = c
  → list_compare A l2 l3 = c
    → list_compare A l1 l3 = c
  induction l2 as [| h2 t2]; cbn; [by destruct l1, l3; cbn; congruence |].A: Type
H: StrictlyComparable A
h2: A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 (h2 :: t2) = c
  → match l3 with
    | [] => Gt
    | h3 :: t3 =>
        match compare h2 h3 with
        | Eq => list_compare A t2 t3
        | Lt => Lt
        | Gt => Gt
        end
    end = c → list_compare A l1 l3 = c
  destruct l1 as [| h1 t1], l3 as [| h3 t3]; cbn; [by congruence.. |].A: Type
H: StrictlyComparable A
h2: A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
h1: A
t1: list A
h3: A
t3: list A
∀ c : comparison,
  match compare h1 h2 with
  | Eq => list_compare A t1 t2
  | Lt => Lt
  | Gt => Gt
  end = c
  → match compare h2 h3 with
    | Eq => list_compare A t2 t3
    | Lt => Lt
    | Gt => Gt
    end = c
    → match compare h1 h3 with
      | Eq => list_compare A t1 t3
      | Lt => Lt
      | Gt => Gt
      end = c
  intros c.A: Type
H: StrictlyComparable A
h2: A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
h1: A
t1: list A
h3: A
t3: list A
c: comparison
match compare h1 h2 with
| Eq => list_compare A t1 t2
| Lt => Lt
| Gt => Gt
end = c
→ match compare h2 h3 with
  | Eq => list_compare A t2 t3
  | Lt => Lt
  | Gt => Gt
  end = c
  → match compare h1 h3 with
    | Eq => list_compare A t1 t3
    | Lt => Lt
    | Gt => Gt
    end = c
  destruct (compare h1 h2) eqn: H12, (compare h2 h3) eqn: H23;
    rewrite ?compare_eq in H12; rewrite ?compare_eq in H23; subst;
    rewrite ?compare_eq_refl, ?H12, ?H23; only 2-4, 6-8: congruence.A: Type
H: StrictlyComparable A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
t1: list A
h3: A
t3: list A
c: comparison
list_compare A t1 t2 = c
→ list_compare A t2 t3 = c → list_compare A t1 t3 = c
A: Type
H: StrictlyComparable A
h2: A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
h1: A
t1: list A
h3: A
t3: list A
c: comparison
H12: compare h1 h2 = Lt
H23: compare h2 h3 = Lt
Lt = c
→ Lt = c
  → match compare h1 h3 with
    | Eq => list_compare A t1 t3
    | Lt => Lt
    | Gt => Gt
    end = c
A: Type
H: StrictlyComparable A
h2: A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
h1: A
t1: list A
h3: A
t3: list A
c: comparison
H12: compare h1 h2 = Gt
H23: compare h2 h3 = Gt
Gt = c
→ Gt = c
  → match compare h1 h3 with
    | Eq => list_compare A t1 t3
    | Lt => Lt
    | Gt => Gt
    end = c
  -A: Type
H: StrictlyComparable A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
t1: list A
h3: A
t3: list A
c: comparison
list_compare A t1 t2 = c
→ list_compare A t2 t3 = c → list_compare A t1 t3 = c by apply IHt2.
  -A: Type
H: StrictlyComparable A
h2: A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
h1: A
t1: list A
h3: A
t3: list A
c: comparison
H12: compare h1 h2 = Lt
H23: compare h2 h3 = Lt
Lt = c
→ Lt = c
  → match compare h1 h3 with
    | Eq => list_compare A t1 t3
    | Lt => Lt
    | Gt => Gt
    end = c by rewrite (StrictOrder_Transitive _ _ _ _ H12 H23).
  -A: Type
H: StrictlyComparable A
h2: A
t2: list A
IHt2: ∀ (l1 l3 : list A) (c : comparison),
  list_compare A l1 t2 = c
  → list_compare A t2 l3 = c
    → list_compare A l1 l3 = c
h1: A
t1: list A
h3: A
t3: list A
c: comparison
H12: compare h1 h2 = Gt
H23: compare h2 h3 = Gt
Gt = c
→ Gt = c
  → match compare h1 h3 with
    | Eq => list_compare A t1 t3
    | Lt => Lt
    | Gt => Gt
    end = c by rewrite (StrictOrder_Transitive _ _ _ _ H12 H23).
Qed.

#[export] Instance CompareStrictOrder_list_compare
  {A : Type} `{StrictlyComparable A}
  : CompareStrictOrder (list_compare A).A: Type
H: StrictlyComparable A
CompareStrictOrder (list_compare A)
Proof.A: Type
H: StrictlyComparable A
CompareStrictOrder (list_compare A)
  split.A: Type
H: StrictlyComparable A
CompareReflexive (list_compare A)
A: Type
H: StrictlyComparable A
CompareTransitive (list_compare A)
  -A: Type
H: StrictlyComparable A
CompareReflexive (list_compare A) by apply list_compare_reflexive.
  -A: Type
H: StrictlyComparable A
CompareTransitive (list_compare A) by apply list_compare_transitive.
Qed.

#[export] Instance StrictlyComparable_list
  {A : Type} `{StrictlyComparable A} : StrictlyComparable (list A) :=
{
  compare := list_compare A;
  compare_strictorder := CompareStrictOrder_list_compare;
}.

Liveness

Definition bounding (P : nat -> Prop)
  :=  {n1 : nat | forall (n2 : nat), n1 <= n2 -> ~ P n2}.

Definition liveness (P : nat -> Prop)
  := forall (n1 : nat), { n2 : nat | n1 <= n2 /\ P n2}.

Definition liveness_dec (P : nat -> Prop)
  := forall (n1 : nat), { n2 : nat | n1 <= n2 /\ P n2} + {~ exists n2 : nat, n1 <= n2 /\ P n2}.

Definition min_liveness (P : nat -> Prop)
  := forall (n1 : nat), { n2 : nat | n1 <= n2 /\ P n2
               /\ forall (n3 : nat), n2 <= n3 /\ P n3 -> n2 <= n3}.

Lemma not_bounding_impl_liveness
  (P : nat -> Prop)
  (Hdec : liveness_dec P)
  (Hnbound : ~ exists n1 : nat, forall (n2 : nat), n1 <= n2 -> ~ P n2)
  : liveness P.P: nat → Prop
Hdec: liveness_dec P
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
liveness P
Proof.P: nat → Prop
Hdec: liveness_dec P
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
liveness P
  intros n1.P: nat → Prop
Hdec: liveness_dec P
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
n1: nat
{n2 : nat | n1 ≤ n2 ∧ P n2}
  specialize (Hdec n1).P: nat → Prop
n1: nat
Hdec: {n2 : nat | n1 ≤ n2 ∧ P n2} +
{¬ (∃ n2 : nat, n1 ≤ n2 ∧ P n2)}
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
{n2 : nat | n1 ≤ n2 ∧ P n2}
  destruct Hdec as [Hex | Hnex]; [done |].P: nat → Prop
n1: nat
Hnex: ¬ (∃ n2 : nat, n1 ≤ n2 ∧ P n2)
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
{n2 : nat | n1 ≤ n2 ∧ P n2}
  contradiction Hnbound.P: nat → Prop
n1: nat
Hnex: ¬ (∃ n2 : nat, n1 ≤ n2 ∧ P n2)
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2
  exists n1.P: nat → Prop
n1: nat
Hnex: ¬ (∃ n2 : nat, n1 ≤ n2 ∧ P n2)
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
∀ n2 : nat, n1 ≤ n2 → ¬ P n2
  intros n2 Hleq HnP.P: nat → Prop
n1: nat
Hnex: ¬ (∃ n2 : nat, n1 ≤ n2 ∧ P n2)
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
n2: nat
Hleq: n1 ≤ n2
HnP: P n2
False
  apply Hnex.P: nat → Prop
n1: nat
Hnex: ¬ (∃ n2 : nat, n1 ≤ n2 ∧ P n2)
Hnbound: ¬ (∃ n1 : nat, ∀ n2 : nat, n1 ≤ n2 → ¬ P n2)
n2: nat
Hleq: n1 ≤ n2
HnP: P n2
∃ n2 : nat, n1 ≤ n2 ∧ P n2
  by exists n2.
Qed.

Misc

Extracts the left element from a sum, if possible.

Definition sum_project_left {A B : Type} (x : A + B) : option A :=
  match x with
  | inl a => Some a
  | inr _ => None
  end.

Extracts the right element from a sum, if possible.

Definition sum_project_right {A B : Type} (x : A + B) : option B :=
  match x with
  | inl _ => None
  | inr b => Some b
  end.

Program Definition not_lt_plus_dec {m n} (Hnlt : ~ n < m) : {k | k + m = n} :=
  exist _ (n - m) _.
Next Obligation.∀ m n : nat, ¬ n < m → (λ k : nat, k + m = n) (n - m)
Proof.∀ m n : nat, ¬ n < m → (λ k : nat, k + m = n) (n - m) by cbn; lia. Qed.

Definition update `{EqDecision A} `(f : A -> B) (a : A) (b : B) : A -> B :=
  fun a' : A => if decide (a = a') then b else f a'.

Lemma update_eq `{EqDecision A} `(f : A -> B) (a : A) (b : B) :
  update f a b a = b.A: Type
EqDecision0: EqDecision A
B: Type
f: A → B
a: A
b: B
update f a b a = b
Proof.A: Type
EqDecision0: EqDecision A
B: Type
f: A → B
a: A
b: B
update f a b a = b
  by unfold update; rewrite decide_True.
Qed.

Lemma update_neq `{EqDecision A} `(f : A -> B) (a : A) (b : B) (a' : A) :
  a <> a' -> update f a b a' = f a'.A: Type
EqDecision0: EqDecision A
B: Type
f: A → B
a: A
b: B
a': A
a ≠ a' → update f a b a' = f a'
Proof.A: Type
EqDecision0: EqDecision A
B: Type
f: A → B
a: A
b: B
a': A
a ≠ a' → update f a b a' = f a'
  by intros; unfold update; rewrite decide_False.
Qed.