-
Notifications
You must be signed in to change notification settings - Fork 98
/
Basic.lean
164 lines (119 loc) · 6.8 KB
/
Basic.lean
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
157
158
159
160
161
162
163
164
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Yury G. Kudryashov
-/
/-!
# Disjoint union of types
This file defines basic operations on the the sum type `α ⊕ β`.
`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
## Main declarations
* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
* `Sum.getLeft`: Retrieves the left content of a `x : α ⊕ β` that is known to come from the left.
* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` that is known to come from the right.
* `Sum.getLeft?`: Retrieves the left content of `x : α ⊕ β` as an option type or returns `none`
if it's coming from the right.
* `Sum.getRight?`: Retrieves the right content of `x : α ⊕ β` as an option type or returns `none`
if it's coming from the left.
* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
* `Sum.LiftRel`: The disjoint union of two relations.
* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
## Further material
See `Std.Data.Sum.Lemmas` for theorems about these definitions.
## Notes
The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
To this effect, we have `PSum`, which takes value in `Sort _` and carries a more complicated
universe signature in consequence. The `Prop` version is `Or`.
-/
namespace Sum
deriving instance DecidableEq for Sum
deriving instance BEq for Sum
section get
/-- Check if a sum is `inl`. -/
def isLeft : α ⊕ β → Bool
| inl _ => true
| inr _ => false
/-- Check if a sum is `inr`. -/
def isRight : α ⊕ β → Bool
| inl _ => false
| inr _ => true
/-- Retrieve the contents from a sum known to be `inl`.-/
def getLeft : (ab : α ⊕ β) → ab.isLeft → α
| inl a, _ => a
/-- Retrieve the contents from a sum known to be `inr`.-/
def getRight : (ab : α ⊕ β) → ab.isRight → β
| inr b, _ => b
@[simp] theorem isLeft_inl : (inl x : α ⊕ β).isLeft = true := rfl
@[simp] theorem isLeft_inr : (inr x : α ⊕ β).isLeft = false := rfl
@[simp] theorem isRight_inl : (inl x : α ⊕ β).isRight = false := rfl
@[simp] theorem isRight_inr : (inr x : α ⊕ β).isRight = true := rfl
@[simp] theorem getLeft_inl (h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x := rfl
@[simp] theorem getRight_inr (h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x := rfl
@[simp] theorem getLeft?_inl : (inl x : α ⊕ β).getLeft? = some x := rfl
@[simp] theorem getLeft?_inr : (inr x : α ⊕ β).getLeft? = none := rfl
@[simp] theorem getRight?_inl : (inl x : α ⊕ β).getRight? = none := rfl
@[simp] theorem getRight?_inr : (inr x : α ⊕ β).getRight? = some x := rfl
end get
/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
fun x => Sum.casesOn x f g
@[simp] theorem elim_inl (f : α → γ) (g : β → γ) (x : α) :
Sum.elim f g (inl x) = f x := rfl
@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
Sum.elim f g (inr x) = g x := rfl
/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
Sum.elim (inl ∘ f) (inr ∘ g)
@[simp] theorem map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl
@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
/-- Swap the factors of a sum type -/
def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl
@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl
@[simp] theorem swap_inr : swap (inr x : α ⊕ β) = inl x := rfl
section LiftRel
/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
`α ⊕ β` and `γ ⊕ δ`. -/
inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
/-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
| protected inl {a c} : r a c → LiftRel r s (inl a) (inl c)
/-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
| protected inr {b d} : s b d → LiftRel r s (inr b) (inr d)
@[simp] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
⟨fun h => by cases h; assumption, LiftRel.inl⟩
@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
@[simp] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
⟨fun h => by cases h; assumption, LiftRel.inr⟩
instance {r : α → γ → Prop} {s : β → δ → Prop}
[∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)
| inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
| inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
| inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
| inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr
end LiftRel
section Lex
/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
respective order on `α` or `β`. -/
inductive Lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
/-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
| protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
/-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
| protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
/-- `inl a` and `inr b` are always related via `Lex r s`. -/
| sep (a b) : Lex r s (inl a) (inr b)
attribute [simp] Lex.sep
@[simp] theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
⟨fun h => by cases h; assumption, Lex.inl⟩
@[simp] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
⟨fun h => by cases h; assumption, Lex.inr⟩
@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
| inl _, inl _ => decidable_of_iff' _ lex_inl_inl
| inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
| inr _, inl _ => Decidable.isFalse lex_inr_inl
| inr _, inr _ => decidable_of_iff' _ lex_inr_inr
end Lex