The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

I accidentally sent the previous email before finishing it. I am seding it again, now complete.

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.

I starting to wonder that one cannot prove this theorem because the definition of In is too weak. Is there a reason for not defining In like below:

Fixpoint contains E (l: list E) e :=

  match l with

  | [] => False

  | e' :: l' => e' = e \/ (e' <> e /\ contains l' e)

  end.

Any help will be greatly appreciated,

Saulo

On Mon, Feb 22, 2016 at 2:27 PM, Saulo Araujo <saulo2 AT gmail.com> wrote:

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.