The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Patricia,

In the context of the request H0, ys is *defined* as ys := x::s

hence eq_refl would give you a valid proof term for H0. 

For instance, you could try this:

Require Import List Arith Lia.

Theorem neq_nil_cons (A:Type) (x:A)(y:list A)(z:list A)(p:cons x y = z): not (z=nil).

Proof. now subst. Qed.

Fixpoint proof1 (A:Type)(l:list A) : 2 <= length l -> tail l <> nil.

Proof.

  refine( match l with 

    | x :: (y :: s) as ys => fun _ => neq_nil_cons A y s ys _

    | _ => _

  end).

  1,2: now simpl; lia. (* here are the other cases nil and _::nil *)

  reflexivity. (* here is the place of H0 *)

Qed.

Best,

Dominique

---

De: "Patricia Peratto" <psperatto AT vera.com.uy>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Lundi 17 Mai 2021 19:55:30
Objet: [Coq-Club] proof with as

I have proved a theorem:

Theorem neq_nil_cons (A:Type(x:A)(y:list A)(z:list A)(p:cons x y = z): not (z=nil).

I have a Fixpoint:

Fixpoint proof1 (A:Type)(l:list A) :=

match l with

| x :: (y :: s) as ys => neq_nil_cons A y s ys H0

| _ => something

end.

In the place of H0 I need a proof that (cons y s)=ys.

How I can do this?

Regards,

Patricia