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?

`eapply succ_ne_zero; exact H`

or `apply succ_ne_zero in H;exact H`

should work

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`

?

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

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