refactor(data/sum): use sections
This commit is contained in:
Leonardo de Moura
parent
15779c5d1e
commit
d56266c524
1 changed files with 56 additions and 51 deletions
|
|
@ -17,66 +17,71 @@ namespace sum
|
|||
infixr `+`:25 := sum -- conflicts with notation for addition
|
||||
end extra_notation
|
||||
|
||||
protected definition rec_on {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
|
||||
(H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
|
||||
rec H1 H2 s
|
||||
section
|
||||
variables {A B : Type}
|
||||
variables {a a₁ a₂ : A} {b b₁ b₂ : B}
|
||||
protected definition rec_on {C : (A ⊎ B) → Type} (s : A ⊎ B) (H₁ : ∀a : A, C (inl B a)) (H₂ : ∀b : B, C (inr A b)) : C s :=
|
||||
rec H₁ H₂ s
|
||||
|
||||
protected definition cases_on {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
|
||||
(H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
|
||||
rec H1 H2 s
|
||||
protected definition cases_on {P : (A ⊎ B) → Prop} (s : A ⊎ B) (H₁ : ∀a : A, P (inl B a)) (H₂ : ∀b : B, P (inr A b)) : P s :=
|
||||
rec H₁ H₂ s
|
||||
|
||||
-- Here is the trick for the theorems that follow:
|
||||
-- Fixing a1, "f s" is a recursive description of "inl B a1 = s".
|
||||
-- When s is (inl B a1), it reduces to a1 = a1.
|
||||
-- When s is (inl B a2), it reduces to a1 = a2.
|
||||
-- Fixing a₁, "f s" is a recursive description of "inl B a₁ = s".
|
||||
-- When s is (inl B a₁), it reduces to a₁ = a₁.
|
||||
-- When s is (inl B a₂), it reduces to a₁ = a₂.
|
||||
-- When s is (inr A b), it reduces to false.
|
||||
|
||||
theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
|
||||
let f := λs, rec_on s (λa, a1 = a) (λb, false) in
|
||||
have H1 : f (inl B a1), from rfl,
|
||||
have H2 : f (inl B a2), from H ▸ H1,
|
||||
H2
|
||||
theorem inl_inj : inl B a₁ = inl B a₂ → a₁ = a₂ :=
|
||||
assume H,
|
||||
let f := λs, rec_on s (λa, a₁ = a) (λb, false) in
|
||||
have H₁ : f (inl B a₁), from rfl,
|
||||
have H₂ : f (inl B a₂), from H ▸ H₁,
|
||||
H₂
|
||||
|
||||
theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
|
||||
theorem inl_neq_inr : inl B a ≠ inr A b :=
|
||||
assume H,
|
||||
let f := λs, rec_on s (λa', a = a') (λb, false) in
|
||||
have H1 : f (inl B a), from rfl,
|
||||
have H2 : f (inr A b), from H ▸ H1,
|
||||
H2
|
||||
have H₁ : f (inl B a), from rfl,
|
||||
have H₂ : f (inr A b), from H ▸ H₁,
|
||||
H₂
|
||||
|
||||
theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 :=
|
||||
let f := λs, rec_on s (λa, false) (λb, b1 = b) in
|
||||
have H1 : f (inr A b1), from rfl,
|
||||
have H2 : f (inr A b2), from H ▸ H1,
|
||||
H2
|
||||
theorem inr_inj : inr A b₁ = inr A b₂ → b₁ = b₂ :=
|
||||
assume H,
|
||||
let f := λs, rec_on s (λa, false) (λb, b₁ = b) in
|
||||
have H₁ : f (inr A b₁), from rfl,
|
||||
have H₂ : f (inr A b₂), from H ▸ H₁,
|
||||
H₂
|
||||
|
||||
protected definition is_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
|
||||
inhabited.mk (inl B (default A))
|
||||
protected definition is_inhabited_left [instance] : inhabited A → inhabited (A ⊎ B) :=
|
||||
assume H : inhabited A, inhabited.mk (inl B (default A))
|
||||
|
||||
protected definition is_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
|
||||
inhabited.mk (inr A (default B))
|
||||
protected definition is_inhabited_right [instance] : inhabited B → inhabited (A ⊎ B) :=
|
||||
assume H : inhabited B, inhabited.mk (inr A (default B))
|
||||
|
||||
protected definition has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :
|
||||
decidable_eq (A ⊎ B) :=
|
||||
take s1 s2 : A ⊎ B,
|
||||
rec_on s1
|
||||
(take a1, show decidable (inl B a1 = s2), from
|
||||
rec_on s2
|
||||
(take a2, show decidable (inl B a1 = inl B a2), from
|
||||
decidable.rec_on (H1 a1 a2)
|
||||
(assume Heq : a1 = a2, decidable.inl (Heq ▸ rfl))
|
||||
(assume Hne : a1 ≠ a2, decidable.inr (mt inl_inj Hne)))
|
||||
(take b2,
|
||||
have H3 : (inl B a1 = inr A b2) ↔ false,
|
||||
from iff.intro inl_neq_inr (assume H4, false_elim H4),
|
||||
show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3)))
|
||||
(take b1, show decidable (inr A b1 = s2), from
|
||||
rec_on s2
|
||||
(take a2,
|
||||
have H3 : (inr A b1 = inl B a2) ↔ false,
|
||||
from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4),
|
||||
show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3))
|
||||
(take b2, show decidable (inr A b1 = inr A b2), from
|
||||
decidable.rec_on (H2 b1 b2)
|
||||
(assume Heq : b1 = b2, decidable.inl (Heq ▸ rfl))
|
||||
(assume Hne : b1 ≠ b2, decidable.inr (mt inr_inj Hne))))
|
||||
protected definition has_eq_decidable [instance] : decidable_eq A → decidable_eq B → decidable_eq (A ⊎ B) :=
|
||||
assume (H₁ : decidable_eq A) (H₂ : decidable_eq B),
|
||||
take s₁ s₂ : A ⊎ B,
|
||||
rec_on s₁
|
||||
(take a₁, show decidable (inl B a₁ = s₂), from
|
||||
rec_on s₂
|
||||
(take a₂, show decidable (inl B a₁ = inl B a₂), from
|
||||
decidable.rec_on (H₁ a₁ a₂)
|
||||
(assume Heq : a₁ = a₂, decidable.inl (Heq ▸ rfl))
|
||||
(assume Hne : a₁ ≠ a₂, decidable.inr (mt inl_inj Hne)))
|
||||
(take b₂,
|
||||
have H₃ : (inl B a₁ = inr A b₂) ↔ false,
|
||||
from iff.intro inl_neq_inr (assume H₄, false_elim H₄),
|
||||
show decidable (inl B a₁ = inr A b₂), from decidable_iff_equiv _ (iff.symm H₃)))
|
||||
(take b₁, show decidable (inr A b₁ = s₂), from
|
||||
rec_on s₂
|
||||
(take a₂,
|
||||
have H₃ : (inr A b₁ = inl B a₂) ↔ false,
|
||||
from iff.intro (assume H₄, inl_neq_inr (H₄⁻¹)) (assume H₄, false_elim H₄),
|
||||
show decidable (inr A b₁ = inl B a₂), from decidable_iff_equiv _ (iff.symm H₃))
|
||||
(take b₂, show decidable (inr A b₁ = inr A b₂), from
|
||||
decidable.rec_on (H₂ b₁ b₂)
|
||||
(assume Heq : b₁ = b₂, decidable.inl (Heq ▸ rfl))
|
||||
(assume Hne : b₁ ≠ b₂, decidable.inr (mt inr_inj Hne))))
|
||||
end
|
||||
end sum
|
||||
|
|
|
|||
Loading…
Reference in a new issue