The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Hi Saulo,

In order to prove this theorem, you need to assume that E has decidable equality:

Require Import Coq.Lists.List.

Import ListNotations.

Theorem strong_in_inv:

  forall E (l: list E) e f,

    (forall x y : E, x = y \/ x <> y) ->

    In f (e :: l) -> e = f \/ (e <> f /\ In f l).

Proof.

  intros R l e f eq_dec.

  simpl.

  destruct (eq_dec e f) as [H | H].

  - intros _. left. trivial.

  - intros [? | H']; try congruence.

    now right; split; trivial.

Qed.

Em seg, 22 de fev de 2016 às 12:27, Saulo Araujo <saulo2 AT gmail.com> escreveu:

Hi,

I am in the middle of a proof in which I need the following theorem:

Theorem strong_in_inv:

  forall E (l: list E) e f,

    In f (e :: l) -> e = f \/ (e <> f /\ In f l).

Unfortunately, I was not able to complete the proof below:

Proof.

  intros.

  simpl in H.

  destruct H.

  {

    left.

    apply H.

  }

  {

    right.

    split.

    {

(* I am stuck here! *)

    }

    {

      apply H.

    }

  }

Qed.