Dennis H (Mar 01 2023 at 10:02): 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 Horapply succ_ne_zero in H;exact Hshould 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.
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: Oct 13 2024 at 01:02 UTC