Stream: Coq users

Topic: is there contradiction?

view this post on Zulip sara lee (Feb 24 2023 at 17:52):

H0 : In a [c']
H1 : In b [c']

a b c' are nat. May i have both above hypothesis at same time? When there is one element in the list then presence of
a and b in list is not possible.

view this post on Zulip Guillaume Melquiond (Feb 24 2023 at 18:00):

You can have both if a = b.

view this post on Zulip Laurent Théry (Feb 24 2023 at 18:10):

Require Import List.
Import ListNotations.

Check in_inv.
Check in_nil.

Goal forall (a b c : nat), In a [c] -> In b [c] -> a = b.
Proof.
intros a b c H0 H1.
destruct (in_inv H0) as [H2|H2].
- destruct (in_inv H1) as [H3|H3].
  + now rewrite <- H2.
  + now destruct (in_nil H3).
- now destruct (in_nil H2).
Qed.

Last updated: Oct 04 2023 at 23:01 UTC