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

fix(library/data/finset/basic): type error on the finset.induction proof

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-08 11:02:06 -07:00
parent 12bad8794b
commit 3aac370629
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/data/finset/basic.lean
View file

@ -194,9 +194,9 @@ protected theorem induction {P : finset A → Prop}
∀s, P s := ∀s, P s :=
take s, take s,
quot.induction_on s quot.induction_on s
take u, (take u,
subtype.destruct u subtype.destruct u
take l, (take l,
list.induction_on l list.induction_on l
(assume nodup_l, H1) (assume nodup_l, H1)
(take a l', (take a l',
@ -206,7 +206,12 @@ quot.induction_on s
assert nodup_l' : nodup l', from nodup_of_nodup_cons nodup_al', assert nodup_l' : nodup l', from nodup_of_nodup_cons nodup_al',
assert P_l' : P (quot.mk (subtype.tag l' nodup_l')), from IH nodup_l', assert P_l' : P (quot.mk (subtype.tag l' nodup_l')), from IH nodup_l',
assert H4 : P (insert a (quot.mk (subtype.tag l' nodup_l'))), from H2 anl' P_l', assert H4 : P (insert a (quot.mk (subtype.tag l' nodup_l'))), from H2 anl' P_l',
begin rewrite [eq.symm H3], apply H4 end) begin
revert nodup_al',
rewrite [-H3],
intros,
apply H4
end)))
protected theorem induction_on {P : finset A → Prop} (s : finset A) protected theorem induction_on {P : finset A → Prop} (s : finset A)
(H1 : P empty) (H1 : P empty)