coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christian Doczkal <christian.doczkal AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] recursive call
- Date: Sun, 10 Jan 2021 22:07:41 +0100
- Organization: INRIA
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+.