Require Import HoTT.Classes.interfaces.canonical_names.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Generalizable Variables A R.

Local Set Universe Minimization ToSet.

Global Instance decide_eqb `{DecidablePaths A} : Eqb A
  := fun a b => if decide_rel paths a b then true else false.

Lemma decide_eqb_ok@{i} {A:Type@{i} } `{DecidablePaths A} :
  forall a b, iff@{Set i i} (eqb a b = true) (a = b).
A: Type
H: DecidablePaths A
forall a b : A, (a =? b) = true <-> a = b
Proof.
A: Type
H: DecidablePaths A
forall a b : A, (a =? b) = true <-> a = b
unfold eqb,decide_eqb.
A: Type
H: DecidablePaths A
forall a b : A,
(if decide_rel paths a b then true else false) = true <->
a = b
intros a b;destruct (decide_rel paths a b) as [E1|E1];split;intros E2;auto.
A: Type
H: DecidablePaths A
a, b: A
E1: a <> b
E2: false = true
a = b
A: Type
H: DecidablePaths A
a, b: A
E1: a <> b
E2: a = b
false = true
-
A: Type
H: DecidablePaths A
a, b: A
E1: a <> b
E2: false = true
a = b destruct (false_ne_true E2).
-
A: Type
H: DecidablePaths A
a, b: A
E1: a <> b
E2: a = b
false = true destruct (E1 E2).
Qed.

Lemma LT_EQ : LT <> EQ.
LT <> EQ
Proof.
LT <> EQ
intros E.
E: LT = EQ
Empty
change ((fun r => match r with LT => Unit | _ => Empty end) EQ).
E: LT = EQ
(fun r : comparison =>
 match r with
 | LT => Unit
 | _ => Empty
 end) EQ
rewrite <-E.
E: LT = EQ
Unit split.
Qed.

Lemma LT_GT : LT <> GT.
LT <> GT
Proof.
LT <> GT
intros E.
E: LT = GT
Empty
change ((fun r => match r with LT => Unit | _ => Empty end) GT).
E: LT = GT
(fun r : comparison =>
 match r with
 | LT => Unit
 | _ => Empty
 end) GT
rewrite <-E.
E: LT = GT
Unit split.
Qed.

Lemma EQ_LT : EQ <> LT.
EQ <> LT
Proof.
EQ <> LT
apply symmetric_neq, LT_EQ.
Qed.

Lemma EQ_GT : EQ <> GT.
EQ <> GT
Proof.
EQ <> GT
intros E.
E: EQ = GT
Empty
change ((fun r => match r with EQ => Unit | _ => Empty end) GT).
E: EQ = GT
(fun r : comparison =>
 match r with
 | EQ => Unit
 | _ => Empty
 end) GT
rewrite <-E.
E: EQ = GT
Unit split.
Qed.

Lemma GT_EQ : GT <> EQ.
GT <> EQ
Proof.
GT <> EQ
apply symmetric_neq, EQ_GT.
Qed.

Global Instance compare_eqb `{Compare A} : Eqb A | 2 := fun a b =>
  match a ?= b with
  | EQ => true
  | _ => false
  end.

Lemma compare_eqb_eq `{Compare A} : forall a b : A, a =? b = true -> a ?= b = EQ.
A: Type
H: Compare A
forall a b : A, (a =? b) = true -> (a ?= b) = EQ
Proof.
A: Type
H: Compare A
forall a b : A, (a =? b) = true -> (a ?= b) = EQ
unfold eqb,compare_eqb;simpl.
A: Type
H: Compare A
forall a b : A,
match a ?= b with
| EQ => true
| _ => false
end = true -> (a ?= b) = EQ
intros a b.
A: Type
H: Compare A
a, b: A
match a ?= b with
| EQ => true
| _ => false
end = true -> (a ?= b) = EQ destruct (a ?= b);trivial;intros E;destruct (false_ne_true E).
Qed.

Global Instance tricho_compare `{Trichotomy A R} : Compare A | 2
  := fun a b =>
  match trichotomy R a b with
  | inl _ => LT
  | inr (inl _) => EQ
  | inr (inr _) => GT
  end.

Lemma tricho_compare_eq `{Trichotomy A R}
  : forall a b : A, compare a b = EQ -> a = b.
A: Type
R: Relation A
H: Trichotomy R
forall a b : A, (a ?= b) = EQ -> a = b
Proof.
A: Type
R: Relation A
H: Trichotomy R
forall a b : A, (a ?= b) = EQ -> a = b
unfold compare,tricho_compare.
A: Type
R: Relation A
H: Trichotomy R
forall a b : A,
match trichotomy R a b with
| inl _ => LT
| inr (inl _) => EQ
| inr (inr _) => GT
end = EQ -> a = b
intros a b;destruct (trichotomy R a b) as [E|[E|E]];auto.
A: Type
R: Relation A
H: Trichotomy R
a, b: A
E: R a b
LT = EQ -> a = b
A: Type
R: Relation A
H: Trichotomy R
a, b: A
E: R b a
GT = EQ -> a = b
-
A: Type
R: Relation A
H: Trichotomy R
a, b: A
E: R a b
LT = EQ -> a = b intros E1;destruct (LT_EQ E1).
-
A: Type
R: Relation A
H: Trichotomy R
a, b: A
E: R b a
GT = EQ -> a = b intros E1;destruct (GT_EQ E1).
Qed.

Lemma tricho_compare_ok `{Trichotomy A R} `{Irreflexive A R}
  : forall a b : A, compare a b = EQ <-> a = b.
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
forall a b : A, (a ?= b) = EQ <-> a = b
Proof.
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
forall a b : A, (a ?= b) = EQ <-> a = b
unfold compare,tricho_compare.
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
forall a b : A,
match trichotomy R a b with
| inl _ => LT
| inr (inl _) => EQ
| inr (inr _) => GT
end = EQ <-> a = b
intros a b;destruct (trichotomy R a b) as [E1|[E1|E1]];split;auto.
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R a b
LT = EQ -> a = b
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R a b
a = b -> LT = EQ
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R b a
GT = EQ -> a = b
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R b a
a = b -> GT = EQ
-
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R a b
LT = EQ -> a = b intros E2;destruct (LT_EQ E2).
-
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R a b
a = b -> LT = EQ intros E2;rewrite E2 in E1.
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R b b
E2: a = b
LT = EQ destruct (irreflexivity R _ E1).
-
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R b a
GT = EQ -> a = b intros E2;destruct (GT_EQ E2).
-
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R b a
a = b -> GT = EQ intros E2;rewrite E2 in E1.
A: Type
R: Relation A
H: Trichotomy R
H0: Irreflexive R
a, b: A
E1: R b b
E2: a = b
GT = EQ destruct (irreflexivity R _ E1).
Qed.

Lemma total_abs_either `{Abs A} `{!TotalRelation le}
  : forall x : A, (0 <= x /\ abs x = x) |_| (x <= 0 /\ abs x = - x).
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
forall x : A,
((0 ≤ x) * (abs x = x) + (x ≤ 0) * (abs x = - x))%type
Proof.
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
forall x : A,
((0 ≤ x) * (abs x = x) + (x ≤ 0) * (abs x = - x))%type
intros x.
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
((0 ≤ x) * (abs x = x) + (x ≤ 0) * (abs x = - x))%type
destruct (total le 0 x) as [E|E].
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: 0 ≤ x
((0 ≤ x) * (abs x = x) + (x ≤ 0) * (abs x = - x))%type
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: x ≤ 0
((0 ≤ x) * (abs x = x) + (x ≤ 0) * (abs x = - x))%type
-
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: 0 ≤ x
((0 ≤ x) * (abs x = x) + (x ≤ 0) * (abs x = - x))%type left.
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: 0 ≤ x
((0 ≤ x) * (abs x = x))%type split;trivial.
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: 0 ≤ x
abs x = x apply ((abs_sig x).2);trivial.
-
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: x ≤ 0
((0 ≤ x) * (abs x = x) + (x ≤ 0) * (abs x = - x))%type right.
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: x ≤ 0
((x ≤ 0) * (abs x = - x))%type split;trivial.
A: Type
H: Le A
H0: Zero A
H1: Negate A
H2: Abs A
TotalRelation0: TotalRelation le
x: A
E: x ≤ 0
abs x = - x apply ((abs_sig x).2);trivial.
Qed.