Zulip Chat Archive

Stream: new members

Topic: finishing from false


view this post on Zulip Vlad Firoiu (Jul 31 2019 at 22:57):

Very basic question here: I have h_false : false in my hypotheses, but I can't seem to finish the proof. If I try cases h_false, I get a "infer type failed".

view this post on Zulip Scott Morrison (Jul 31 2019 at 22:58):

That should usually work. Can you post a minimal working example for us?

view this post on Zulip Vlad Firoiu (Jul 31 2019 at 22:59):

cantor.lean

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:00):

Somehow the apply flip_neq tactic corrupted your goal, and whatever you do afterwards fails. (even sorry)

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:02):

No, the problem is already earlier.

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:02):

Here is a working version of your proof:

lemma cantor {f : nat -> pow_nat} : not (surjective f) :=
begin
intro H,
let g := λ (x : nat), flip_bool (f x x),
have h := H g,

cases h,
have asd : f h_w h_w = g h_w,
rw h_h,

have gh : g = (λ (x : ), flip_bool (f x x)),
refl,

have not_asd : not (f h_w h_w = g h_w),
rw gh,
simp,
apply flip_neq,
have h_false := not_asd asd,
--sorry,
cases h_false,

end

view this post on Zulip Vlad Firoiu (Jul 31 2019 at 23:03):

I think the goal gets weird when I do cases h

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:03):

I just changed two of your let with have. In general you should use let for definitions and have for proofs.

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:04):

Yes, that is correct, the problem is with let h := ..., cases h. Apparently the cases tactic does not work for local constants that have a body (i.e. are introduced with a let)

view this post on Zulip Vlad Firoiu (Jul 31 2019 at 23:06):

Ah ok, I'll keep that in mind.

view this post on Zulip Vlad Firoiu (Jul 31 2019 at 23:07):

Is there a way to get rid of gh? I first tried to unfold g but it didn't work.

view this post on Zulip Vlad Firoiu (Jul 31 2019 at 23:07):

Maybe because g is defined with let?

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:10):

Yes, you can do dsimp [g] (or a variant: dsimp only [g], simp [g], simp only [g]).

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:13):

Also, you can just do:

have not_asd : not (f h_w h_w = g h_w),
apply flip_neq

apply (and many other tactics, like exact) will automatically unfold definitions for you (and variables introduced by let)

view this post on Zulip Vlad Firoiu (Jul 31 2019 at 23:16):

Ah that makes my proof much simpler! Thank you!

view this post on Zulip Floris van Doorn (Jul 31 2019 at 23:23):

However, tactics like rw and simp generally don't unfold definitions for you.


Last updated: May 16 2021 at 20:13 UTC