Stream: Coq users

Topic: Proof with inequality and false assumption


view this post on Zulip Dennis H (Mar 01 2023 at 10:02):

So I'm in a situation where I have the following hypotheses and goal:

a, b: mynat
h: S a = 0 -> False
k: S b = 0 -> False
H: S (S a * b + a) = 0
1/1
False

and I have a theorem

succ_ne_zero : forall a : mynat, S a <> 0.

now I know I can do congruence and it will solve the proof right away, but I'm wondering if theres another way to do it manually. Basically, I would say that something like apply (succ_ne_zero _) should solve it too, but it says it cannot find the replacement for the natural number. So doing something like

apply (succ_ne_zero (S a * b + a)).
exact H.

works, but now I have to manually type in the value for the argument. Is there a better way to do this?

view this post on Zulip Gaëtan Gilbert (Mar 01 2023 at 10:04):

eapply succ_ne_zero; exact H or apply succ_ne_zero in H;exact H should work

view this post on Zulip Dennis H (Mar 01 2023 at 10:08):

Gaëtan Gilbert zei:

eapply succ_ne_zero; exact H or apply succ_ne_zero in H;exact H should work

Ah thanks! Just a question, why does eapply work, but not apply?

view this post on Zulip Laurent Théry (Mar 01 2023 at 10:15):

I guess it is because apply tries to find a negation. Negation is encoded as (_ -> False). This should work:

revert H; apply succ_ne_zero.

view this post on Zulip Gaëtan Gilbert (Mar 01 2023 at 10:17):

it's because the goal after eapply has a hole in it S ?x = 0
apply is not allowed to leave holes
https://coq.github.io/doc/master/refman/proof-engine/tactics.html#coq:tacn.eapply


Last updated: Jun 18 2024 at 00:02 UTC