Stream: Coq users

Topic: Refuting exists


view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:30):

Which tactic to refuteexists x, P x?

view this post on Zulip jco (Jul 17 2020 at 06:38):

if you have it above the line, you would destruct it then derive a contradiction. below the line I don't know if there is a generic way to do it besides deriving a contradiction above the line

view this post on Zulip jco (Jul 17 2020 at 06:38):

like if you think it's not true, you could instead prove ~(exists x, P x).

view this post on Zulip jco (Jul 17 2020 at 06:39):

but in general if there is something below the line that you think is not true, then you gotta change what you're trying to prove (because you can't prove something untrue, after all)

view this post on Zulip jco (Jul 17 2020 at 06:40):

imagine you have H(exists x, Px) above the line though, but you have proven that ~(exists x, Px)...then you do exfalso, apply lemma H, assumption and you're done

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:40):

You mean, create a new hypothesis and apply it to the goal or something?

view this post on Zulip jco (Jul 17 2020 at 06:40):

Valéry Croizier said:

You mean, create a new hypothesis and apply it to the goal or something?

if you have exists x, P x as a goal and it is not true, you have two possibilities. 1. you have a contradiction above the line (so your goal doesn't really matter) 2. you need to change your theorem as it isn't true

view this post on Zulip jco (Jul 17 2020 at 06:41):

like if you have mytheorem: stuff stuff, exists x Px but it turns out that "exists x, P x" is not true, then you need to chang eit to mytheorem: stuff stuff, ~(exists x, P x)

view this post on Zulip jco (Jul 17 2020 at 06:41):

your goal doesn't really give you any information, as it is what you are trying to prove. if your goal is not true, either you have a contradiction above the line, or you gotta change what you're trying to prove

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:42):

This exists happens in a branch of a case that I need to discard.

view this post on Zulip jco (Jul 17 2020 at 06:42):

yeah maybe a minimal case would help make things more concrete? but usually if you're dealing with branches, if only one branch is actually possible, then you derive a contradiction above the line

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:43):

And P x is False for all x.

view this post on Zulip jco (Jul 17 2020 at 06:43):

so if you have forall x, ~(P x) above the line, then you also have exists x, P x above the line, you can derive a contradiction

view this post on Zulip jco (Jul 17 2020 at 06:44):

H: forall x, ~(P x)
H1: exists x, P x
======
destruct H1.
exfalso.
eapply H.
apply H1.

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:44):

This looks like a good strategy. Now, how do I create a new hypothesis above the line in Coq? In Lean I use have...by.

view this post on Zulip jco (Jul 17 2020 at 06:45):

assert (forall x, ~(P x))

view this post on Zulip jco (Jul 17 2020 at 06:45):

which also can accept by tactic

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:45):

Thanks, will try that.

view this post on Zulip jco (Jul 17 2020 at 06:45):

assert (forall x, ~(P x)) by lemma_proving_this

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:53):

BTW, somewhere else in the proof I need to check 2 cases n < 2 and n >= 2. Is there some way to do that with case or induction?

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:53):

I'll have to discard one case.

view this post on Zulip jco (Jul 17 2020 at 06:55):

destruct (n<2) should work to give you the cases

view this post on Zulip jco (Jul 17 2020 at 06:56):

The Omega tactic is also great for dealing with arithmetic and < <= etc (you still gotta destruct to get the cases though)

view this post on Zulip jco (Jul 17 2020 at 06:57):

You might want to look into eqb_spec (I think, from memory). It uses reflection to be nicer to work with in some cases (using the decidability of booleans to give you the relevant Props above the line)

view this post on Zulip Valéry Croizier (Jul 17 2020 at 06:59):

destruct(n<2) says that this is not an inductive product, while n is nat.

view this post on Zulip jco (Jul 17 2020 at 07:01):

whoops, that's what I get for doing this on my phone :) destruct (n <? 2) eqn:E will do it, and the eqn:E will keep it above the line

view this post on Zulip jco (Jul 17 2020 at 07:02):

that said, destruct (Nat.eqb_spec n 2) is often nicer to deal with

view this post on Zulip jco (Jul 17 2020 at 07:02):

depends on whether or not you need to deal with the boolean reality (eg n <? 2 = true) or the propositional reality (n<2)

view this post on Zulip jco (Jul 17 2020 at 07:03):

omega is very useful in many cases evolving <= and <

view this post on Zulip Valéry Croizier (Jul 17 2020 at 07:09):

<? is a syntax error. Nat.eqb_spec works better, even if it creates only one case n=2. I tried Nat.ltb_spec and it creates a case n<2, which is better.

view this post on Zulip jco (Jul 17 2020 at 07:10):

Ah yeah ltb_spec is correct

view this post on Zulip jco (Jul 17 2020 at 07:10):

sorry, was on my phone so couldn't check the details in a repl

view this post on Zulip Valéry Croizier (Jul 17 2020 at 07:10):

My bad. It creates 2 cases, so this is what I was looking for. Thanks.


Last updated: Jan 29 2023 at 01:02 UTC