Stream: Coq users

Topic: Use of In prdicate


view this post on Zulip zohaze (Jan 04 2023 at 14:59):

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?

view this post on Zulip Olivier Laurent (Jan 04 2023 at 15:16):

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.

view this post on Zulip zohaze (Jan 04 2023 at 16:01):

thanks.


Last updated: Jun 20 2024 at 11:02 UTC