Valéry Croizier (Jul 17 2020 at 06:30): Valéry Croizier (Jul 17 2020 at 06:30):Which tactic to refuteexists x, P x?
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
jco (Jul 17 2020 at 06:38):like if you think it's not true, you could instead prove ~(exists x, P x).
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)
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
Valéry Croizier (Jul 17 2020 at 06:40):You mean, create a new hypothesis and apply it to the goal or something?
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
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)
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
Valéry Croizier (Jul 17 2020 at 06:42):This exists happens in a branch of a case that I need to discard.
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
Valéry Croizier (Jul 17 2020 at 06:43):And P x is False for all x.
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
jco (Jul 17 2020 at 06:44):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.
jco (Jul 17 2020 at 06:45):assert (forall x, ~(P x))
jco (Jul 17 2020 at 06:45):which also can accept by tactic
Valéry Croizier (Jul 17 2020 at 06:45):Thanks, will try that.
jco (Jul 17 2020 at 06:45):assert (forall x, ~(P x)) by lemma_proving_this
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?
Valéry Croizier (Jul 17 2020 at 06:53):I'll have to discard one case.
jco (Jul 17 2020 at 06:55):destruct (n<2) should work to give you the cases
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)
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)
Valéry Croizier (Jul 17 2020 at 06:59):destruct(n<2) says that this is not an inductive product, while n is nat.
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
jco (Jul 17 2020 at 07:02):that said, destruct (Nat.eqb_spec n 2) is often nicer to deal with
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)
jco (Jul 17 2020 at 07:03):omega is very useful in many cases evolving <= and <
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.
jco (Jul 17 2020 at 07:10):Ah yeah ltb_spec is correct
jco (Jul 17 2020 at 07:10):sorry, was on my phone so couldn't check the details in a repl
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: Oct 13 2024 at 01:02 UTC