coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Castéran Pierre <pierre.casteran AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] recursive call
- Date: Sun, 10 Jan 2021 23:38:18 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.casteran AT gmail.com; spf=Pass smtp.mailfrom=pierre.casteran AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f41.google.com
- Ironport-phdr: 9a23:cwEY7hx/cgfqFMbXCy+O+j09IxM/srCxBDY+r6Qd2usUIJqq85mqBkHD//Il1AaPAdyEragY2qGP7fmocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalsIBi5qQjdudQajIp/Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lKJVrw6uqRNw3oDabo+VOuR8ca3eet0XXnZBXt9UVyBdAoOwc4kCAuwcNuhYtYn9oF4OoAOgCAa2H+Pv1iVPhmXs0q08y+svCwDG0xI6H9IUrnvfsdL4NL8TUe+r1qnI1yvMY+lK1jjn84jIbg4uoeuWUrJ2asfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvWv6hhXQ9pAFtvjig2N0sio/Ri48Rzl3J9zt0zZgoKNCkVEN2f9GqHYVMuiyaOYV7RsEvTW9stSs4xbMKp5C2cDYXxJkoyRPSb+CKfpSH7B/iSOucJypzinF9eL+nmRq+7Uytxvf/W8S0ylpGsDRJnsTWun0CyhDf8taLReFh8ku83DuAyxvc5vxALE0xl6fUMJ4sz7s+m5UNrUjPAir7lUXqg6OIdkgp//Wk5uvob7r6o5KRNZF4hwP6P6krhMOyD/43PRIIUmOG4+qzzqfj8lf8QLhSjv05jK3ZsJfCKMQevKG5AgtV3p8t6halEjuqydoYkHYaIF5fdxKHiI/pO17KIP/mF/uwn1OskDJzy/DHOL3uHInNI2DdnLv9ebtx8U1RxQopwdxB+Z5YF6sNLf3uVkPpsdzXFB45Mwi6w+b9D9V905sTWXqOAqCHKqPSq0GH6vgzLOaWf48VpCjyK+I/6P7olnI5llodcrOo3ZsTcny3AvNmI0CBbXr2ntgBCXsKvhY5TOHylFKCVidTa2+uUKI4+zE0E5mrDZzDR4ComLyOxj23HpxQZmBcC1CDC23kd4ueW6REVCXHKch41zcASLKJSok71BjouhWp5aBgK7//8zYENIjq0u9N5uDJjxx6oSR1At6H3ieGRnpok3kBQRc52al+pQp2zVLVgvswuOBRCdEGv6ABaQw9L5OJl7UnWeC3YRrIe5KycHjjQtiiBmtsHNc4wttLfFwkXtv+11bM2C2lB7JTnLuOVsRto/DsmkPpLsM48E7okawojl0oWMxKbDT0iat29gyVDInMwRzAy/SaMJ8E1SuIz1+tiHKUtRgBAgF1WKTBG3sYYxmOoA==
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
>
- [Coq-Club] recursive call, Patricia Peratto, 01/10/2021
- Re: [Coq-Club] recursive call, Christian Doczkal, 01/10/2021
- Re: [Coq-Club] recursive call, Castéran Pierre, 01/10/2021
- Re: [Coq-Club] recursive call, Anton Trunov, 01/11/2021
- Re: [Coq-Club] recursive call, Christian Doczkal, 01/10/2021
Archive powered by MHonArc 2.6.19+.