## Stream: Coq users

### Topic: Proof with inequality and false assumption

#### 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?

#### 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

#### 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`?

#### 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.
``````

#### 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