Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit eb024dc

Browse files
kim-emmergify[bot]
kim-em
authored and
mergify[bot]
committed
feat(order/lexicographic): lexicographic pre/partial/linear orders (#820)
* remove prod.(*)order instances * feat(order/lexicographic): lexicographic pre/partial/linear orders * add lex_decidable_linear_order * identical constructions for dependent pairs * cleaning up * Update lexicographic.lean forgotten `instance` * restore product instances, and add lex type synonym for lexicographic instances * proofs in progress * * define lt * prove lt_iff_le_not_le * refactoring
1 parent 29507a4 commit eb024dc

File tree

2 files changed

+238
-0
lines changed

2 files changed

+238
-0
lines changed

‎src/order/basic.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,6 +220,9 @@ instance prod.preorder (α : Type u) (β : Type v) [preorder α] [preorder β] :
220220
⟨le_trans hac hce, le_trans hbd hdf⟩,
221221
.. prod.has_le α β }
222222

223+
/-- The pointwise partial order on a product.
224+
(The lexicographic ordering is defined in order/lexicographic.lean, and the instances are
225+
available via the type synonym `lex α β = α × β`.) -/
223226
instance prod.partial_order (α : Type u) (β : Type v) [partial_order α] [partial_order β] :
224227
partial_order (α × β) :=
225228
{ le_antisymm := assume ⟨a, b⟩ ⟨c, d⟩ ⟨hac, hbd⟩ ⟨hca, hdb⟩,

‎src/order/lexicographic.lean

Lines changed: 235 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,235 @@
1+
/-
2+
Copyright (c) 2019 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Author: Scott Morrison
5+
6+
Lexicographic preorder / partial_order / linear_order / decidable_linear_order,
7+
for pairs and dependent pairs.
8+
-/
9+
import order.basic
10+
import tactic.interactive
11+
12+
universes u v
13+
14+
def lex (α : Type u) (β : Type v) := α × β
15+
16+
variables {α : Type u} {β : Type v}
17+
18+
/-- Dictionary / lexicographic ordering on pairs. -/
19+
instance lex_has_le [preorder α] [preorder β] : has_le (lex α β) :=
20+
{ le := λ a b, a.1 < b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) }
21+
22+
instance lex_has_lt [preorder α] [preorder β] : has_lt (lex α β) :=
23+
{ lt := λ a b, a.1 < b.1 ∨ (a.1 = b.1 ∧ a.2 < b.2) }
24+
25+
/-- Dictionary / lexicographic preorder for pairs. -/
26+
instance lex_preorder [preorder α] [preorder β] : preorder (lex α β) :=
27+
{ le_refl := λ a, or.inr ⟨rfl, le_refl _⟩,
28+
le_trans :=
29+
begin
30+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨a₃, b₃⟩ (a₁₂_lt | ⟨a₁₂_eq, b₁₂_le⟩) (a₂₃_lt | ⟨a₂₃_eq, b₂₃_le⟩),
31+
{ exact or.inl (lt_trans a₁₂_lt a₂₃_lt) },
32+
{ left, rwa ←a₂₃_eq },
33+
{ left, rwa a₁₂_eq },
34+
{ exact or.inr ⟨eq.trans a₁₂_eq a₂₃_eq, le_trans b₁₂_le b₂₃_le⟩, }
35+
end,
36+
lt_iff_le_not_le :=
37+
begin
38+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
39+
split,
40+
{ rintros (⟨a₁₂_lt⟩ | ⟨a₁₂_eq, b₁₂_lt⟩),
41+
{ exact ⟨
42+
or.inl a₁₂_lt,
43+
not_or_distrib.2 ⟨λ h, lt_irrefl _ (lt_trans h a₁₂_lt),
44+
λ h, begin cases h with h₁, dsimp at h₁, subst h₁, exact lt_irrefl _ a₁₂_lt end⟩ ⟩ },
45+
{ dsimp at a₁₂_eq,
46+
subst a₁₂_eq,
47+
exact ⟨or.inr ⟨rfl, le_of_lt b₁₂_lt⟩,
48+
not_or_distrib.2 ⟨lt_irrefl _, λ h, (lt_iff_le_not_le.1 b₁₂_lt).2 h.2⟩⟩ } },
49+
{ rintros ⟨a₁₂_lt | ⟨p, b₁₂_le⟩, b⟩,
50+
{ exact or.inl a₁₂_lt, },
51+
{ cases not_or_distrib.1 b with a₂₁_not_lt h,
52+
dsimp at p,
53+
subst p,
54+
exact or.inr ⟨rfl, lt_iff_le_not_le.2 ⟨b₁₂_le, by simpa using h⟩⟩ } }
55+
end,
56+
.. lex_has_le,
57+
.. lex_has_lt }
58+
59+
/-- Dictionary / lexicographic partial_order for pairs. -/
60+
instance lex_partial_order [partial_order α] [partial_order β] : partial_order (lex α β) :=
61+
{ le_antisymm :=
62+
begin
63+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (a₁₂_lt | ⟨a₁₂_eq, b₁₂_le⟩) (a₂₁_lt | ⟨a₂₁_eq, b₂₁_le⟩),
64+
{ exact false.elim (lt_irrefl a₁ (lt_trans a₁₂_lt a₂₁_lt)) },
65+
{ rw a₂₁_eq at a₁₂_lt, exact false.elim (lt_irrefl a₁ a₁₂_lt) },
66+
{ rw a₁₂_eq at a₂₁_lt, exact false.elim (lt_irrefl a₂ a₂₁_lt) },
67+
{ dsimp at a₁₂_eq, subst a₁₂_eq, have h := le_antisymm b₁₂_le b₂₁_le, dsimp at h, rw h }
68+
end
69+
.. lex_preorder }
70+
71+
/-- Dictionary / lexicographic linear_order for pairs. -/
72+
instance lex_linear_order [linear_order α] [linear_order β] : linear_order (lex α β) :=
73+
{ le_total :=
74+
begin
75+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
76+
rcases le_total a₁ a₂ with ha | ha;
77+
cases lt_or_eq_of_le ha with a_lt a_eq,
78+
-- Deal with the two goals with a₁ ≠ a₂
79+
{ left, left, exact a_lt },
80+
swap,
81+
{ right, left, exact a_lt },
82+
-- Now deal with the two goals with a₁ = a₂
83+
all_goals { subst a_eq,
84+
rcases le_total b₁ b₂ with hb | hb },
85+
{ left, right, exact ⟨rfl, hb⟩ },
86+
{ right, right, exact ⟨rfl, hb⟩ },
87+
{ left, right, exact ⟨rfl, hb⟩ },
88+
{ right, right, exact ⟨rfl, hb⟩ }
89+
end
90+
.. lex_partial_order }.
91+
92+
/-- Dictionary / lexicographic decidable_linear_order for pairs. -/
93+
instance lex_decidable_linear_order [decidable_linear_order α] [decidable_linear_order β] :
94+
decidable_linear_order (lex α β) :=
95+
{ decidable_le :=
96+
begin
97+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
98+
rcases decidable_linear_order.decidable_le α a₁ a₂ with a₂₁_lt | a₁₂_le,
99+
{ -- a₂ < a₁
100+
exact decidable.is_false (not_le.2 (or.inl (not_le.1 a₂₁_lt))) },
101+
{ -- a₁ ≤ a₂
102+
by_cases h : a₁ = a₂,
103+
{ subst h,
104+
rcases decidable_linear_order.decidable_le _ b₁ b₂ with b₂₁_lt | b₁₂_le,
105+
{ -- b₂ < b₁
106+
exact decidable.is_false (not_le.2 (or.inr ⟨rfl, not_le.1 b₂₁_lt⟩)) },
107+
{ -- b₁ ≤ b₂
108+
apply decidable.is_true,
109+
cases lt_or_eq_of_le a₁₂_le with a₁₂_lt a₁₂_eq,
110+
{ exact or.inl a₁₂_lt },
111+
{ exact or.inr ⟨a₁₂_eq, b₁₂_le⟩ } } },
112+
{ -- a₁ < a₂
113+
apply decidable.is_true,
114+
cases lt_or_eq_of_le a₁₂_le with a₁₂_lt a₁₂_eq,
115+
{ exact or.inl a₁₂_lt },
116+
{ exact or.inl (false.elim (h a₁₂_eq)) } }
117+
}
118+
end,
119+
.. lex_linear_order
120+
}
121+
122+
variables {Z : α → Type v}
123+
124+
/--
125+
Dictionary / lexicographic ordering on dependent pairs.
126+
127+
The 'pointwise' partial order `prod.has_le` doesn't make
128+
sense for dependent pairs, so it's safe to mark these as
129+
instances here.
130+
-/
131+
instance dlex_has_le [preorder α] [∀ a, preorder (Z a)] : has_le (Σ a, Z a) :=
132+
{ le := λ a b, a.1 < b.1 ∨ (∃ p : a.1 = b.1, a.2 ≤ (by convert b.2)) }
133+
instance dlex_has_lt [preorder α] [∀ a, preorder (Z a)] : has_lt (Σ a, Z a) :=
134+
{ lt := λ a b, a.1 < b.1 ∨ (∃ p : a.1 = b.1, a.2 < (by convert b.2)) }
135+
136+
/-- Dictionary / lexicographic preorder on dependent pairs. -/
137+
instance dlex_preorder [preorder α] [∀ a, preorder (Z a)] : preorder (Σ a, Z a) :=
138+
{ le_refl := λ a, or.inr ⟨rfl, le_refl _⟩,
139+
le_trans :=
140+
begin
141+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨a₃, b₃⟩ (a₁₂_lt | ⟨a₁₂_eq, b₁₂_le⟩) (a₂₃_lt | ⟨a₂₃_eq, b₂₃_le⟩),
142+
{ exact or.inl (lt_trans a₁₂_lt a₂₃_lt) },
143+
{ left, rwa ←a₂₃_eq },
144+
{ left, rwa a₁₂_eq },
145+
{ exact or.inr ⟨eq.trans a₁₂_eq a₂₃_eq, le_trans b₁₂_le (by convert b₂₃_le; simp) ⟩ }
146+
end,
147+
lt_iff_le_not_le :=
148+
begin
149+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
150+
split,
151+
{ rintros (⟨a₁₂_lt⟩ | ⟨a₁₂_eq, b₁₂_lt⟩),
152+
{ exact ⟨
153+
or.inl a₁₂_lt,
154+
not_or_distrib.2 ⟨λ h, lt_irrefl _ (lt_trans h a₁₂_lt),
155+
not_exists.2 (λ h w, by {
156+
dsimp at h,
157+
subst h,
158+
exact lt_irrefl _ a₁₂_lt })⟩ ⟩ },
159+
{ dsimp at a₁₂_eq,
160+
subst a₁₂_eq,
161+
exact ⟨or.inr ⟨rfl, le_of_lt b₁₂_lt⟩,
162+
not_or_distrib.2 ⟨lt_irrefl _, not_exists.2 (λ w h, (lt_iff_le_not_le.1 b₁₂_lt).2 h)⟩⟩,
163+
} },
164+
{ rintros ⟨a₁₂_lt | ⟨p, b₁₂_le⟩, b⟩,
165+
{ exact or.inl a₁₂_lt, },
166+
{ cases not_or_distrib.1 b with a₂₁_not_lt h,
167+
dsimp at p,
168+
subst p,
169+
exact or.inr ⟨rfl, lt_iff_le_not_le.2 ⟨b₁₂_le, by apply (not_exists.1 h) rfl ⟩⟩ } }
170+
end,
171+
.. dlex_has_le,
172+
.. dlex_has_lt }
173+
174+
/-- Dictionary / lexicographic partial_order for dependent pairs. -/
175+
instance dlex_partial_order [partial_order α] [∀ a, partial_order (Z a)] : partial_order (Σ a, Z a) :=
176+
{ le_antisymm :=
177+
begin
178+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (a₁₂_lt | ⟨a₁₂_eq, b₁₂_le⟩) (a₂₁_lt | ⟨a₂₁_eq, b₂₁_le⟩),
179+
{ exact false.elim (lt_irrefl a₁ (lt_trans a₁₂_lt a₂₁_lt)) },
180+
{ rw a₂₁_eq at a₁₂_lt, exact false.elim (lt_irrefl a₁ a₁₂_lt) },
181+
{ rw a₁₂_eq at a₂₁_lt, exact false.elim (lt_irrefl a₂ a₂₁_lt) },
182+
{ dsimp at a₁₂_eq, subst a₁₂_eq, have h := le_antisymm b₁₂_le b₂₁_le, dsimp at h, rw h, simp, }
183+
end
184+
.. dlex_preorder }
185+
186+
/-- Dictionary / lexicographic linear_order for pairs. -/
187+
instance dlex_linear_order [linear_order α] [∀ a, linear_order (Z a)] : linear_order (Σ a, Z a) :=
188+
{ le_total :=
189+
begin
190+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
191+
rcases le_total a₁ a₂ with ha | ha;
192+
cases lt_or_eq_of_le ha with a_lt a_eq,
193+
-- Deal with the two goals with a₁ ≠ a₂
194+
{ left, left, exact a_lt },
195+
swap,
196+
{ right, left, exact a_lt },
197+
-- Now deal with the two goals with a₁ = a₂
198+
all_goals { subst a_eq,
199+
rcases le_total b₁ b₂ with hb | hb },
200+
{ left, right, exact ⟨rfl, hb⟩ },
201+
{ right, right, exact ⟨rfl, hb⟩ },
202+
{ left, right, exact ⟨rfl, hb⟩ },
203+
{ right, right, exact ⟨rfl, hb⟩ }
204+
end
205+
.. dlex_partial_order }.
206+
207+
/-- Dictionary / lexicographic decidable_linear_order for dependent pairs. -/
208+
instance dlex_decidable_linear_order [decidable_linear_order α] [∀ a, decidable_linear_order (Z a)] :
209+
decidable_linear_order (Σ a, Z a) :=
210+
{ decidable_le :=
211+
begin
212+
rintros ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
213+
rcases decidable_linear_order.decidable_le α a₁ a₂ with a₂₁_lt | a₁₂_le,
214+
{ -- a₂ < a₁
215+
exact decidable.is_false (not_le.2 (or.inl (not_le.1 a₂₁_lt))) },
216+
{ -- a₁ ≤ a₂
217+
by_cases h : a₁ = a₂,
218+
{ subst h,
219+
rcases decidable_linear_order.decidable_le _ b₁ b₂ with b₂₁_lt | b₁₂_le,
220+
{ -- b₂ < b₁
221+
exact decidable.is_false (not_le.2 (or.inr ⟨rfl, not_le.1 b₂₁_lt⟩)) },
222+
{ -- b₁ ≤ b₂
223+
apply decidable.is_true,
224+
cases lt_or_eq_of_le a₁₂_le with a₁₂_lt a₁₂_eq,
225+
{ exact or.inl a₁₂_lt },
226+
{ exact or.inr ⟨a₁₂_eq, b₁₂_le⟩ } } },
227+
{ -- a₁ < a₂
228+
apply decidable.is_true,
229+
cases lt_or_eq_of_le a₁₂_le with a₁₂_lt a₁₂_eq,
230+
{ exact or.inl a₁₂_lt },
231+
{ exact or.inl (false.elim (h a₁₂_eq)) } }
232+
}
233+
end,
234+
.. dlex_linear_order
235+
}

0 commit comments

Comments
 (0)