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

chore(library/standard/data/sum): remove hints, they are not needed after the fix

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-21 21:44:02 -07:00
parent 1fdc483ab9
commit fdd37fb1f3
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/standard/data/sum.lean
View file

@ -32,19 +32,19 @@ sum_rec H1 H2 s
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 @subst _ _ _ f H H1,
have H2 : f (inl B a2), from subst H H1,
H2
theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
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 @subst _ _ _ f H H1,
have H2 : f (inr A b), from subst H H1,
H2
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 @subst _ _ _ f H H1,
have H2 : f (inr A b2), from subst H H1,
H2
theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) :=
@ -61,15 +61,15 @@ rec_on s1
rec_on s2
(take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
(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)))
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 (symm H4)) (assume H4, false_elim _ H4),
show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
have H3 : (inr A b1 = inl B a2) ↔ false,
from iff_intro (assume H4, inl_neq_inr (symm 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 H2 b1 b2))
end sum