I have below statement in hypothesis
H: In S(S(S(S(S(S( a)))))) [2;3;4;5].
The natural number S(S(S(S(S(S( a)))))) will not exist in the list,for all vaues of a (0 or S a).
1) Could i prove above is wrong statement?
2) On the basis of this , H may i close any goal statement?
3) When simplify above, I get message " unknown a". How i can solve it?
1) Indeed the hypothesis H
implies False
.
2) Using exfalso
you can deduce any statement from a proof of False
.
Here is some corresponding Coq code:
From Coq Require Import List.
Import ListNotations.
Goal forall P a, In (S(S(S(S(S(S(a))))))) [2;3;4;5] -> P.
Proof.
intros P a H. exfalso.
repeat (destruct H; [ discriminate H | cbn in H ]).
exact H.
Qed.
thanks.
Last updated: Oct 13 2024 at 01:02 UTC