Stream: Coq users

Topic: Difference between two commands


view this post on Zulip pianke (Feb 19 2023 at 05:18):

1)I have hypothesis that a exists in l . I should write it as (In a l or List.In a l)?
2) During induction i get In a [].This is wrong statement in the presence of hypothesis
(In a l). How to prove it wrong?

view this post on Zulip Laurent Théry (Feb 19 2023 at 08:12):

1) They are the same

Require Import List.
Import ListNotations.

Locate In.
Check In.
Check List.In.
Check Lists.List.In.
Check Coq.Lists.List.In.

view this post on Zulip Laurent Théry (Feb 19 2023 at 08:14):

2) There is a theorem in_nil

Require Import List.
Import ListNotations.

Check in_nil.

Goal forall (a : nat) (P : Prop), In a [] -> P.
Proof.
intros a P H.
Check (@in_nil _ a).
destruct (@in_nil _ a).
exact H.
Qed.

Last updated: Jun 18 2024 at 09:02 UTC