The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Just a remark on the specific example by Patricia.
The condition  l <> nil is trivial in the recursive calls of selsmaller, thus 
we have a simple solution:, with a helper function.

Variable A: Type.
Variable compare : A -> A -> comparison.

Definition min (x y:A) := match (compare x y)
                            with
                            | Lt | Eq => x | _ => y
                            end.

  Fixpoint select_help m l :=
    match l with
      nil => m
    |  x :: l => min m (select_help x l)
    end.

  Definition selsmaller (l:list A) : l <> nil -> A :=
    match l with
      nil =>  (fun p: nil <> nil => False_rect _ (p (refl_equal nil)))
    | x :: l => fun p =>  select_help x l
    end.


  
Best regards,
Pierre

> Le 10 janv. 2021 à 22:07, Christian Doczkal <christian.doczkal AT inria.fr> a 
> écrit :
> 
> 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
>