Stream: new members

Topic: finishing from false

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".

Scott Morrison (Jul 31 2019 at 22:58):

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

cantor.lean

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)

Floris van Doorn (Jul 31 2019 at 23:02):

No, the problem is already earlier.

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


Vlad Firoiu (Jul 31 2019 at 23:03):

I think the goal gets weird when I do cases h

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.

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)

Vlad Firoiu (Jul 31 2019 at 23:06):

Ah ok, I'll keep that in mind.

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.

Vlad Firoiu (Jul 31 2019 at 23:07):

Maybe because g is defined with let?

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]).

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)

Vlad Firoiu (Jul 31 2019 at 23:16):

Ah that makes my proof much simpler! Thank you!

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