The Coq mailing list

[<psperatto AT gmail.com>]

 

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

 

---

El software de antivirus Avast ha analizado este correo electrónico en busca de virus. www.avast.com