finishing from false

Stream: new members

[Vlad Firoiu]

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]

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

[Vlad Firoiu]

cantor.lean

[Floris van Doorn]

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

[Floris van Doorn]

No, the problem is already earlier.

[Floris van Doorn]

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]

I think the goal gets weird when I do cases h

[Floris van Doorn]

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

[Floris van Doorn]

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]

Ah ok, I'll keep that in mind.

[Vlad Firoiu]

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

[Vlad Firoiu]

Maybe because g is defined with let?

[Floris van Doorn]

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

[Floris van Doorn]

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]

Ah that makes my proof much simpler! Thank you!

[Floris van Doorn]

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