trivial question on boolean logic

Stream: new members

[David Lin]

Hi, I am trying to solve "lemma question_2a_false : ¬ (∀ P Q : Prop, (P → Q) → (Q → P))"

Currently, I did

intro h,
have h2 := h false true,

which end up with showing (false → true) → true → false |- false.

But I cannot get the last step. I would assume trivial works, but it doesn't.

[David Lin]

Hmm, I think I have found a workaround. Instead of using have, I use apply.

intro h,
apply h false true,
trivial,
trivial,

Nevertheless, I am still interested to see what one can do with the previous strategy.

[Eric Wieser]

Can you show the example where "trivial doesn't work"?

[Eric Wieser]

It's likely you're getting hit by the difference between docs#trivial and docs#tactic.interactive.trivial

[David Lin]

I am probably using "trivial" in a nonprecise way. I am mainly thinking h2 -> false, can be done by simple computation of boolean logic. So I guess there might be some one line solution like exact h2 (?)
image.png

[David Lin]

So the question is, what is the last line that finishes the goal?

[Eric Wieser]

This might be a good exercise in leaning how to use term mode interactively

[Eric Wieser]

Start with λ h, _ as your entire proof (instead of a begin / end)

[Eric Wieser]

You'll get an error on the _ which tells you what the goal is

[Eric Wieser]

You can replace it with h false true _ _ and you'll have two "holes" left to fill

[David Lin]

I think I get the second hole, but not sure about the other one

λ h, h false true _ trivial

[Eric Wieser]

The other hole is false → true, right? That's true by definition of false.

[Eric Wieser]

One way you can solve it is (by trivial) which is essentially what your original proof did

[Kevin Buzzard]

Tactics like simp * at * and finish might help here

[Yakov Pechersky]

itauto should be complete for these too

[Eric Wieser]

The actual thing you need to fill the hole is

docs#false.elim