The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi Arthur,

You were right! A little but further in my development, I needed a theorem similar to in_map:

Theorem contains_map:

  forall X (xs: list X) Y (f: X -> Y) (x: X), contains xs x -> contains (map f xs) (f x).

However, since contains is too strong, I was only able to prove it requiring the decidability of A. One thing interesting is that, while trying to prove contains_map, the Coq context suggested to me that the theorem also holds when f is injective, which is indeed true:

Theorem contains_map:

  forall X (xs: list X) Y (f: X -> Y) (x: X), 

    (forall a b, a <> b -> f a <> f b) ->

      contains xs x -> contains (map f xs) (f x).

Proof.

  intros X xs Y f x f_is_injective H.

  induction xs.

  {

    inversion H.

  }

  {

    simpl.

    destruct H.

    {

      left.

      congruence.

    }

    {

      right.

      split.

      {        

        apply f_is_injective. (* Here we use the fact that f is injective *)

        apply H.

      }

      {

        apply IHxs.

        apply H.

      }

    }

  }

Qed.

Sincerely,

Saulo

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

If you really need the stronger variant, I'm afraid you need decidability in one way or another.

For instance, you mentioned your stronger version of In, which would give the result for free. The problem with that variant is that it does not allow you to prove "contains x l -> contains x (y :: l)" for types without decidable equality, and this property is crucial for showing many results involving In. You may be able to prove instances of this principle for some concrete values of "x" and "y", but in the general case there's nothing we can do about it.

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

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.