The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> I don't understand how is defined the order
> relation in Fixpoint definitions. The
> recursive call is in a smaller argument.

It has to be smaller in a syntactic sense, and 
destructing-then-reconstructing doesn't work.
Consider:

Fixpoint bla n :=
  match n with
  | 0 | 1 => 0
  | S (S n0) => bla (S n0)
  end.

this doesn't work because (S n0) is directly from the match on n
(note the error is different: since there's only 1 argument there's no 
guessing to do)

A fixpoint with the same meaning which is accepted is

Fixpoint bla n :=
  match n with
  | 0 | 1 => 0
  | S (S n0 as n1) => bla n1
  end.

In your case it's a bit trickier because you need the proof of 
nonemptiness to recurse
I guess you can use something like


Fixpoint last (A:Set)(s:queue A):
  (s <> nilq _) -> A:=
  match s with
  | nilq _ => (fun p => (False_elim A (p (eq_refl _))))
  | consq _ x y =>
    fun _ =>
      match y return (y <> nilq _ -> A) -> A with
      | nilq _ => fun _ => x
      | consq _ _ _ => fun last => last (not_eq_consq_nilq _ _ _)
      end (last _ y)
  end.

TBH I didn't write this in one go, I went through tactics first to 
figure out the layout of the thing (specifically to figure out the use 
of a cut around the match)

Gaëtan Gilbert

On 28/03/2019 23:51, 
psperatto AT gmail.com
 wrote:
> I have defined a set of queues of type A
> and other functions as follows:
>
> Inductive queue (A:Set):Set :=
> | nilq  : queue A
> | consq : A-> queue A-> queue A.
>
> Fixpoint ins_back (A:Set)(a:A)(s:queue A):
> (queue A):=
> match s with
> | nilq _ => consq _ a (nilq _)
> | consq _ x y => consq _ x (ins_back _ a y)
> end.
>
> Theorem False_elim (A:Set)(f:False):A.
> elim f.
> Qed.
>
> Fixpoint set_queue (A:Set)(s:queue A): Prop:=
> match s with
> | nilq _ => False
> | consq _ x y => True
> end.
>
>
> Theorem eq_subst (A:Set)(x y :A)(P:A->Prop)
> (e:(eq x y))(i:(P y)) : P x.
> rewrite -> e.
> exact i.
> Qed.
>
> Theorem not_eq_consq_nilq (A:Set)(x:A)
> (y:queue A): not (eq (consq A x y)(nilq A)).
> intro.
> exact (eq_subst (queue A) (nilq A)
>        (consq A x y)(set_queue A)
>         (eq_sym H) I).
> Qed.
>
> I want to define a recursive function that
> computes the last element on a non-empty
> queue.
>
> To this end I've defined:
>
> Fixpoint last (A:Set)(s:queue A):
> (not (eq s (nilq A))) -> A:=
> match s with
> | nilq _ => (fun p =>
> (False_elim A (p (eq_refl _))))
> | consq _ x (nilq _) => (fun p => x)
> | consq _ x (consq _ x2 y) =>
> (fun p => last _ (consq _ x2 y)
> (not_eq_consq_nilq _ x2 y))
> end.
>
> I get the message:
> Cannot guess decreasing argument of fix.
>
> I don't understand how is defined the order
> relation in Fixpoint definitions. The
> recursive call is in a smaller argument.
>
> Someone can help me ???
>
> Regards,
> Patricia
>
>
>
> ------------------------------------------------------------------------
> Avast logo <https://www.avast.com/antivirus>      
>
> El software de antivirus Avast ha analizado este correo electrónico en 
> busca de virus.
> www.avast.com <https://www.avast.com/antivirus>
>
>
> <#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>