Which tactic to refute`exists x, P x`

?

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

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

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)

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

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

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

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)`

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

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

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

And `P x`

is False for all x.

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

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

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.

`assert (forall x, ~(P x))`

which also can accept `by tactic`

Thanks, will try that.

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

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?

I'll have to discard one case.

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

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

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)

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

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

that said, ` destruct (Nat.eqb_spec n 2)`

is often nicer to deal with

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

) or the propositional reality (`n<2`

)

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

`<?`

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.

Ah yeah ltb_spec is correct

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

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

Last updated: Jan 29 2023 at 01:02 UTC