The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Thanks a lot Artur! 

Unfortunately I need to use this theorem with a dependent type in which the tactic decide equality is not being able to do its job. I was able to manually prove that the equality of this type is decidable. However, since this proof ended being a little big, I was wondering if by giving a stronger definition of In, I could refraim from having to prove decidability.

Saulo

On Mon, Feb 22, 2016 at 2:32 PM, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

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.