The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

By the way, Christian probably meant

Fixpoint foo (T : Type) (s : list T) := 
 match s with 
 | x :: (y :: s') as ys' => foo T ys'
 | _ => s
 end.

in his example and not

Fixpoint foo (T : Type) (s : list T) :=
 match s with
 | x :: (y :: s' as ys') => foo T ys'
 | _ => s
 end.

because “as” binds stronger than “::”.

This syntax is a common source of confusion — I myself this the same thing 
once too and due to
a rather weak spec all my proofs went through :)

Hope this helps,
Anton

> On 11 Jan 2021, at 00:07, Christian Doczkal <christian.doczkal AT inria.fr> 
> wrote:
> 
> If I understand your problem correctly, then there is a confusion about
> what is "structurally smaller". Consider the following two definitions:
> 
> Require Import List.
> 
> Fail Fixpoint foo (T : Type) (s : list T) := 
>  match s with 
>  | x :: y :: s' => foo T (y :: s')
>  | _ => s
>  end.
> 
> Fixpoint foo (T : Type) (s : list T) := 
>  match s with 
>  | x :: (y :: s' as ys') => foo T ys'
>  | _ => s
>  end.
> 
> 
> The first one fails because "y::s'" (i.e. a combination of two terms
> "y" and "s'") is *not* considered structurally smaller than s. 
> 
> However, the above matches are just shorthands for two nested matches
> and one can give names to the intermediate results using "as", as shown
> above. 
> 
> I hope this helps!
> 
> Best,
> Christian
> 
> PS. It might help do minimize ones examples before posting to the
> list. 
> 
> On Sun, 2021-01-10 at 16:40 -0300, Patricia Peratto wrote:
>> I want to select the smallest value from a list of A elements over
>> which is defined
>> an order relation.
>> 
>> I have defined:
>> 
>> Theorem False_el (A:Type)(x:False):A.
>> exact (False_rect A x).
>> Qed.
>> 
>> Theorem not_empty_list (A:Type)(l:list A)(q:l=nil)
>> (p:not(l=nil)): A.
>> exact (False_el A (p q)).
>> Qed.
>> 
>> Inductive trich (A:Type):Type:=
>> |Lt (x y:A):trich A
>> |Le (x y:A):trich A.
>> 
>> Parameter decide_trich: forall(A:Type)(x y:A),trich A.
>> 
>> Definition min (A:Type)(x y:A)(z:trich A): A :=
>> match (z) with
>> | Lt _ x y => x
>> | Le _ x y => y
>> end.
>> 
>> Fixpoint selsmaller (A:Type)(l:list A)
>> (p:not (l=nil)):A :=
>> match l with
>> | nil => not_empty_list A nil
>> (eq_refl nil) p
>> | cons x nil => x
>> | cons x y =>
>> let z:=(selsmaller y) in
>> min A x z (decide_trich A x z)
>> end.
>> 
>> Since does not substitute l by nil in p I change the definition of
>> selsmaller in
>> the following way: I add the following definitions:
>> 
>> Definition nil_cons_Prop (A:Type)(l:list A) : Prop :=
>> match l with
>> | nil => False
>> | cons x y => True
>> end.
>> 
>> Parameter eq_subst : forall (A:Type)
>> (x y:A)(P:A->Prop)(q:x=y),P x-> P y.
>> 
>> Theorem neq_nil_cons (A:Type)(x:A)(y:list A):
>> not(cons x y=nil).
>> intro.
>> apply (eq_subst (list A) (cons x y) nil (nil_cons_Prop A) H I).
>> Qed.
>> 
>> Fixpoint selsmaller (A:Type)(l:list A):
>> (not (l=nil))->A :=
>> match l with
>> | nil => (fun (p:not(nil=nil))=>
>> not_empty_list A nil
>> (eq_refl nil) p)
>> 
>> | cons x nil => (fun p =>x)
>> 
>> | cons x (cons y w) =>
>> (fun p => let z:=(selsmaller A(cons y w)
>> (neq_nil_cons A y w)) in
>> min A x z (decide_trich A x z))
>> end.
>> 
>> I have got the message: Cannot guess decreasing argument of fix
>> but the recursive argument (cons y w) is structurally smaller.
>> 
>> I don´t know how to continue.
>> 
>> Regards,
>> Patricia
>