Stream: Coq users

Topic: Difference between two commands

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?

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.

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: Oct 04 2023 at 23:01 UTC