1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
From stdpp Require Import numbers.
From stdpp Require Import options.
Notation cast_trichotomy T :=
match T with
| inleft (left _) => inleft (left _)
| inleft (right _) => inleft (right _)
| inright _ => inright _
end.
Global Instance prod_lexico `{Lexico A, Lexico B} : Lexico (A * B) := λ p1 p2,
(**i 1.) *) lexico (p1.1) (p2.1) ∨
(**i 2.) *) p1.1 = p2.1 ∧ lexico (p1.2) (p2.2).
Global Instance bool_lexico : Lexico bool := λ b1 b2,
match b1, b2 with false, true => True | _, _ => False end.
Global Instance nat_lexico : Lexico nat := (<).
Global Instance N_lexico : Lexico N := (<)%N.
Global Instance Z_lexico : Lexico Z := (<)%Z.
Global Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
Global Instance list_lexico `{Lexico A} : Lexico (list A) :=
fix go l1 l2 :=
let _ : Lexico (list A) := @go in
match l1, l2 with
| [], _ :: _ => True
| x1 :: l1, x2 :: l2 => lexico (x1,l1) (x2,l2)
| _, _ => False
end.
Global Instance sig_lexico `{Lexico A} (P : A → Prop) `{∀ x, ProofIrrel (P x)} :
Lexico (sig P) := λ x1 x2, lexico (`x1) (`x2).
Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)}
(x : A) (y : B) : complement lexico y y → complement lexico (x,y) (x,y).
Proof. intros ? [?|[??]]; [|done]. by apply (irreflexivity lexico x). Qed.
Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)}
(x1 x2 x3 : A) (y1 y2 y3 : B) :
lexico (x1,y1) (x2,y2) → lexico (x2,y2) (x3,y3) →
(lexico y1 y2 → lexico y2 y3 → lexico y1 y3) → lexico (x1,y1) (x3,y3).
Proof.
intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
intros [|[??]] [?|[??]]; simplify_eq/=; auto.
by left; trans x2.
Qed.
Global Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
`{!StrictOrder (@lexico B _)} : StrictOrder (@lexico (A * B) _).
Proof.
split.
- intros [x y]. apply prod_lexico_irreflexive.
by apply (irreflexivity lexico y).
- intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply transitivity.
Qed.
Global Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
`{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
Proof.
red; refine (λ p1 p2,
match trichotomyT lexico (p1.1) (p2.1) with
| inleft (left _) => inleft (left _)
| inleft (right _) => cast_trichotomy (trichotomyT lexico (p1.2) (p2.2))
| inright _ => inright _
end); clear tA tB;
abstract (unfold lexico, prod_lexico; auto using injective_projections).
Defined.
Global Instance bool_lexico_po : StrictOrder (@lexico bool _).
Proof.
split.
- by intros [] ?.
- by intros [] [] [] ??.
Qed.
Global Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
Proof.
red; refine (λ b1 b2,
match b1, b2 with
| false, false => inleft (right _)
| false, true => inleft (left _)
| true, false => inright _
| true, true => inleft (right _)
end); abstract (unfold strict, lexico, bool_lexico; naive_solver).
Defined.
Global Instance nat_lexico_po : StrictOrder (@lexico nat _).
Proof. unfold lexico, nat_lexico. apply _. Qed.
Global Instance nat_lexico_trichotomy: TrichotomyT (@lexico nat _).
Proof.
red; refine (λ n1 n2,
match Nat.compare n1 n2 as c return Nat.compare n1 n2 = c → _ with
| Lt => λ H, inleft (left (nat_compare_Lt_lt _ _ H))
| Eq => λ H, inleft (right (nat_compare_eq _ _ H))
| Gt => λ H, inright (nat_compare_Gt_gt _ _ H)
end eq_refl).
Defined.
Global Instance N_lexico_po : StrictOrder (@lexico N _).
Proof. unfold lexico, N_lexico. apply _. Qed.
Global Instance N_lexico_trichotomy: TrichotomyT (@lexico N _).
Proof.
red; refine (λ n1 n2,
match N.compare n1 n2 as c return N.compare n1 n2 = c → _ with
| Lt => λ H, inleft (left (proj2 (N.compare_lt_iff _ _) H))
| Eq => λ H, inleft (right (N.compare_eq _ _ H))
| Gt => λ H, inright (proj1 (N.compare_gt_iff _ _) H)
end eq_refl).
Defined.
Global Instance Z_lexico_po : StrictOrder (@lexico Z _).
Proof. unfold lexico, Z_lexico. apply _. Qed.
Global Instance Z_lexico_trichotomy: TrichotomyT (@lexico Z _).
Proof.
red; refine (λ n1 n2,
match Z.compare n1 n2 as c return Z.compare n1 n2 = c → _ with
| Lt => λ H, inleft (left (proj2 (Z.compare_lt_iff _ _) H))
| Eq => λ H, inleft (right (Z.compare_eq _ _ H))
| Gt => λ H, inright (proj1 (Z.compare_gt_iff _ _) H)
end eq_refl).
Defined.
Global Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
StrictOrder (@lexico (list A) _).
Proof.
split.
- intros l. induction l; [by intros ? | by apply prod_lexico_irreflexive].
- intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
eapply prod_lexico_transitive; eauto.
Qed.
Global Instance list_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} :
TrichotomyT (@lexico (list A) _).
Proof.
refine (
fix go l1 l2 :=
let go' : TrichotomyT (@lexico (list A) _) := @go in
match l1, l2 with
| [], [] => inleft (right _)
| [], _ :: _ => inleft (left _)
| _ :: _, [] => inright _
| x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
end); clear tA go go';
abstract (repeat (done || constructor || congruence || by inv 1)).
Defined.
Global Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
Proof.
unfold lexico, sig_lexico. split.
- intros [x ?] ?. by apply (irreflexivity lexico x).
- intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
Qed.
Global Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
Proof.
red; refine (λ x1 x2, cast_trichotomy (trichotomyT lexico (`x1) (`x2)));
abstract (repeat (done || constructor || apply (sig_eq_pi P))).
Defined.
|
