The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi Clément,

Thanks for pointing out that the theorem is true in a non-constructive setting.

Sincerely,

Saulo

On Mon, Feb 22, 2016 at 2:51 PM, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

Indeed, this theorem does not seem to be true in general. Could it be that it looks intuitively true because it holds in the classical framework?

Require Import List.
Require Import Classical.

Theorem strong_in_inv:
  forall E (l: list E) e f,
    In f (e :: l) -> e = f \/ (e <> f /\ In f l).
Proof.
  intros.
  simpl in H.
  destruct H.
  left; assumption.
  classical_right; tauto.
Qed.

Note how ‘classical_right’ (instead of ‘right’ in your proof) gives you ‘not (e = f)’.

Clément.

On 02/22/2016 12:32 PM, Arthur Azevedo de Amorim 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 <mailto: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.
>