michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/init/datatypes): change implicit arguments of sum.inl and sum.inr

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 18:07:13 -08:00
parent 69191ef9b7
commit 9eea32b076
5 changed files with 53 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
library/data/sum.lean
View file

@ -21,43 +21,43 @@ namespace sum
variables {A B : Type}
variables {a a₁ a₂ : A} {b b₁ b₂ : B}
theorem inl_neq_inr : inl B a ≠ inr A b :=
theorem inl_neq_inr : inl a ≠ inr b :=
assume H, no_confusion H
theorem inl_inj : inl B a₁ = inl B a₂ → a₁ = a₂ :=
theorem inl_inj : intro_left B a₁ = intro_left B a₂ → a₁ = a₂ :=
assume H, no_confusion H (λe, e)
theorem inr_inj : inr A b₁ = inr A b₂ → b₁ = b₂ :=
theorem inr_inj : intro_right A b₁ = intro_right A b₂ → b₁ = b₂ :=
assume H, no_confusion H (λe, e)
protected definition is_inhabited_left [instance] : inhabited A → inhabited (A + B) :=
assume H : inhabited A, inhabited.mk (inl B (default A))
assume H : inhabited A, inhabited.mk (inl (default A))
protected definition is_inhabited_right [instance] : inhabited B → inhabited (A + B) :=
assume H : inhabited B, inhabited.mk (inr A (default B))
assume H : inhabited B, inhabited.mk (inr (default B))
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
(take a₁, show decidable (inl a₁ = s₂), from
rec_on s₂
(take a₂, show decidable (inl B a₁ = inl B a₂), from
(take a₂, show decidable (inl a₁ = inl 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,
have H₃ : (inl a₁ = inr b₂) ↔ false,
from iff.intro inl_neq_inr (assume H₄, !false.rec H₄),
show decidable (inl B a₁ = inr A b₂), from decidable_of_decidable_of_iff _ (iff.symm H₃)))
(take b₁, show decidable (inr A b₁ = s₂), from
show decidable (inl a₁ = inr b₂), from decidable_of_decidable_of_iff _ (iff.symm H₃)))
(take b₁, show decidable (inr b₁ = s₂), from
rec_on s₂
(take a₂,
have H₃ : (inr A b₁ = inl B a₂) ↔ false,
have H₃ : (inr b₁ = inl a₂) ↔ false,
from iff.intro (assume H₄, inl_neq_inr (H₄⁻¹)) (assume H₄, !false.rec H₄),
show decidable (inr A b₁ = inl B a₂), from decidable_of_decidable_of_iff _ (iff.symm H₃))
(take b₂, show decidable (inr A b₁ = inr A b₂), from
show decidable (inr b₁ = inl a₂), from decidable_of_decidable_of_iff _ (iff.symm H₃))
(take b₂, show decidable (inr b₁ = inr 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))))

20
library/init/datatypes.lean
View file

@ -46,12 +46,24 @@ definition and.elim_right {a b : Prop} (H : and a b) : b :=
and.rec (λa b, b) H
inductive sum (A B : Type) : Type :=
inl : A → sum A B,
inr : B → sum A B
inl {} : A → sum A B,
inr {} : B → sum A B
definition sum.intro_left [reducible] {A : Type} (B : Type) (a : A) : sum A B :=
sum.inl a
definition sum.intro_right [reducible] (A : Type) {B : Type} (b : B) : sum A B :=
sum.inr b
inductive or (a b : Prop) : Prop :=
intro_left : a → or a b,
intro_right : b → or a b
inl {} : a → or a b,
inr {} : b → or a b
definition or.intro_left {a : Prop} (b : Prop) (Ha : a) : or a b :=
or.inl Ha
definition or.intro_right (a : Prop) {b : Prop} (Hb : b) : or a b :=
or.inr Hb
-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).

6
library/init/logic.lean
View file

@ -166,12 +166,6 @@ notation a `\/` b := or a b
notation a ∨ b := or a b
namespace or
definition inl (Ha : a) : a ∨ b :=
intro_left b Ha
definition inr (Hb : b) : a ∨ b :=
intro_right a Hb
theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
rec H₂ H₃ H₁
end or

12
tests/lean/run/forest2.lean
View file

@ -29,23 +29,23 @@ namespace solution2
variables {A B : Type}
inductive same_kind : sum A B → sum A B → Prop :=
isl : Π (a₁ a₂ : A), same_kind (sum.inl B a₁) (sum.inl B a₂),
isr : Π (b₁ b₂ : B), same_kind (sum.inr A b₁) (sum.inr A b₂)
isl : Π (a₁ a₂ : A), same_kind (sum.inl a₁) (sum.inl a₂),
isr : Π (b₁ b₂ : B), same_kind (sum.inr b₁) (sum.inr b₂)
definition to_left (s : sum A B) (a : A) : same_kind s (sum.inl B a) → A :=
definition to_left (s : sum A B) (a : A) : same_kind s (sum.inl a) → A :=
sum.cases_on s
(λ a₁ H, a₁)
(λ b₁ H, false.rec _ (by cases H))
definition to_right (s : sum A B) (b : B) : same_kind s (sum.inr A b) → B :=
definition to_right (s : sum A B) (b : B) : same_kind s (sum.inr b) → B :=
sum.cases_on s
(λ a₁ H, false.rec _ (by cases H))
(λ b₁ H, b₁)
theorem to_left_inl (a₁ a₂ : A) (H : same_kind (sum.inl B a₁) (sum.inl B a₂)) : to_left (sum.inl B a₁) a₂ H = a₁ :=
theorem to_left_inl (a₁ a₂ : A) (H : same_kind (sum.intro_left B a₁) (sum.inl a₂)) : to_left (sum.inl a₁) a₂ H = a₁ :=
rfl
theorem to_right_inr (b₁ b₂ : B) (H : same_kind (sum.inr A b₁) (sum.inr A b₂)) : to_right (sum.inr A b₁) b₂ H = b₁ :=
theorem to_right_inr (b₁ b₂ : B) (H : same_kind (sum.intro_right A b₁) (sum.inr b₂)) : to_right (sum.inr b₁) b₂ H = b₁ :=
rfl
end solution2

36
tests/lean/run/forest_height.lean
View file

@ -35,17 +35,17 @@ inv_image.wf tree_forest_height lt.wf
infix [local] `≺`:50 := tree_forest.subterm
definition tree_forest.height_lt.node {A : Type} (a : A) (f : forest A) : sum.inr _ f ≺ sum.inl _ (tree.node a f) :=
definition tree_forest.height_lt.node {A : Type} (a : A) (f : forest A) : sum.inr f ≺ sum.inl (tree.node a f) :=
have aux : forest.height f < tree.height (tree.node a f), from
lt.base (forest.height f),
aux
definition tree_forest.height_lt.cons₁ {A : Type} (t : tree A) (f : forest A) : sum.inl _ t ≺ sum.inr _ (forest.cons t f) :=
definition tree_forest.height_lt.cons₁ {A : Type} (t : tree A) (f : forest A) : sum.inl t ≺ sum.inr (forest.cons t f) :=
have aux : tree.height t < forest.height (forest.cons t f), from
lt_succ_of_le (max.left _ _),
aux
definition tree_forest.height_lt.cons₂ {A : Type} (t : tree A) (f : forest A) : sum.inr _ f ≺ sum.inr _ (forest.cons t f) :=
definition tree_forest.height_lt.cons₂ {A : Type} (t : tree A) (f : forest A) : sum.inr f ≺ sum.inr (forest.cons t f) :=
have aux : forest.height f < forest.height (forest.cons t f), from
lt_succ_of_le (max.right _ _),
aux
@ -65,35 +65,35 @@ find_decl bool.ff ≠ bool.tt
definition map.F {A B : Type} (f : A → B) (tf₁ : tree_forest A) : (Π tf₂ : tree_forest A, tf₂ ≺ tf₁ → map.res B tf₂) → map.res B tf₁ :=
sum.cases_on tf₁
(λ t : tree A, tree.cases_on t
(λ a₁ f₁ (r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inl (forest A) (tree.node a₁ f₁) → map.res B tf₂),
show map.res B (sum.inl (forest A) (tree.node a₁ f₁)), from
have rf₁ : map.res B (sum.inr _ f₁), from r (sum.inr _ f₁) (tree_forest.height_lt.node a₁ f₁),
(λ a₁ f₁ (r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inl (tree.node a₁ f₁) → map.res B tf₂),
show map.res B (sum.inl (tree.node a₁ f₁)), from
have rf₁ : map.res B (sum.inr f₁), from r (sum.inr f₁) (tree_forest.height_lt.node a₁ f₁),
have nf₁ : forest B, from sum.cases_on (dpr₁ rf₁)
(λf (h : kind (sum.inl (forest B) f) = kind (sum.inr (tree A) f₁)), absurd (eq.symm h) bool.ff_ne_tt)
(λf (h : kind (sum.inl f) = kind (sum.inr f₁)), absurd (eq.symm h) bool.ff_ne_tt)
(λf h, f)
(dpr₂ rf₁),
dpair (sum.inl (forest B) (tree.node (f a₁) nf₁)) rfl))
dpair (sum.inl (tree.node (f a₁) nf₁)) rfl))
(λ f : forest A, forest.cases_on f
(λ r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inr (tree A) (forest.nil A) → map.res B tf₂,
show map.res B (sum.inr (tree A) (forest.nil A)), from
dpair (sum.inr (tree B) (forest.nil B)) rfl)
(λ t₁ f₁ (r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inr (tree A) (forest.cons t₁ f₁) → map.res B tf₂),
show map.res B (sum.inr (tree A) (forest.cons t₁ f₁)), from
have rt₁ : map.res B (sum.inl _ t₁), from r (sum.inl _ t₁) (tree_forest.height_lt.cons₁ t₁ f₁),
have rf₁ : map.res B (sum.inr _ f₁), from r (sum.inr _ f₁) (tree_forest.height_lt.cons₂ t₁ f₁),
(λ r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inr (forest.nil A) → map.res B tf₂,
show map.res B (sum.inr (forest.nil A)), from
dpair (sum.inr (forest.nil B)) rfl)
(λ t₁ f₁ (r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inr (forest.cons t₁ f₁) → map.res B tf₂),
show map.res B (sum.inr (forest.cons t₁ f₁)), from
have rt₁ : map.res B (sum.inl t₁), from r (sum.inl t₁) (tree_forest.height_lt.cons₁ t₁ f₁),
have rf₁ : map.res B (sum.inr f₁), from r (sum.inr f₁) (tree_forest.height_lt.cons₂ t₁ f₁),
have nt₁ : tree B, from sum.cases_on (dpr₁ rt₁)
(λ t h, t)
(λ f h, absurd h bool.ff_ne_tt)
(dpr₂ rt₁),
have nf₁ : forest B, from sum.cases_on (dpr₁ rf₁)
(λf (h : kind (sum.inl (forest B) f) = kind (sum.inr (tree A) f₁)), absurd (eq.symm h) bool.ff_ne_tt)
(λf (h : kind (sum.inl f) = kind (sum.inr f₁)), absurd (eq.symm h) bool.ff_ne_tt)
(λf h, f)
(dpr₂ rf₁),
dpair (sum.inr (tree B) (forest.cons nt₁ nf₁)) rfl))
dpair (sum.inr (forest.cons nt₁ nf₁)) rfl))
definition map {A B : Type} (f : A → B) (tf : tree_forest A) : map.res B tf :=
well_founded.fix (@map.F A B f) tf
eval map succ (sum.inl (forest nat) (tree.node 2 (forest.cons (tree.node 1 (forest.nil nat)) (forest.nil nat))))
eval map succ (sum.inl (tree.node 2 (forest.cons (tree.node 1 (forest.nil nat)) (forest.nil nat))))
end manual