The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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.
>

Attachment: signature.asc
Description: OpenPGP digital signature