Zulip Chat Archive

Stream: new members

Topic: Closing negated goals quickly


view this post on Zulip Eric Wieser (Jun 15 2020 at 20:25):

I have left as my goal:

hnp : ¬p head,
hnq : ¬q head
 ¬(p head  q head)

Is there a quick tactic-mode incantation to finish off?

view this post on Zulip Bhavik Mehta (Jun 15 2020 at 20:27):

tactic#tautology

view this post on Zulip Eric Wieser (Jun 15 2020 at 20:27):

tauto by itself does not work

view this post on Zulip Bhavik Mehta (Jun 15 2020 at 20:28):

Or maybe tauto!

view this post on Zulip Eric Wieser (Jun 15 2020 at 20:28):

intro h, cases h, exact hnp h, exact hnq h does but feels clumsy.

view this post on Zulip Bhavik Mehta (Jun 15 2020 at 20:28):

If not finish should do it too

view this post on Zulip Eric Wieser (Jun 15 2020 at 20:29):

import tactic being missing strikes again. tauto worked after all
Thanks!

view this post on Zulip Eric Wieser (Jun 15 2020 at 20:36):

Another goal I'm struggling to close quickly:

hs : (filter (λ (x : α), p x  q x) tail).length  (filter p tail).length + (filter q tail).length,
 (filter (λ (x : α), p x  q x) tail).length + 1  (filter p tail).length + 1 + ((filter q tail).length + 1)

rw doesn't seem to work here, and finish works in my installation but not the codewars one.

view this post on Zulip Reid Barton (Jun 15 2020 at 20:37):

linarith should be smart enough for this one

view this post on Zulip Eric Wieser (Jun 15 2020 at 20:38):

Bingo, knew I'd seen this type of issue before.


Last updated: May 14 2021 at 03:27 UTC