coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
- To: "psperatto AT gmail.com" <psperatto AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] order in fixpoint
- Date: Thu, 28 Mar 2019 23:07:43 +0000
- Accept-language: en-CA, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM04-CO1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:lbTnNBeQTUyPzyr29Dk/4JFJlGMj4u6mDksu8pMizoh2WeGdxcWyZB7h7PlgxGXEQZ/co6odzbaP6+awBCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfb9+Nha7oAXMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+t6LplSALziCcfKTE27H3XhMJ3jKJeuh2hphp/yJPQbIyaMPdye6XQds4YS2VcRMZcTyxPDJ2hYYsTAeQPPuhYoIvhqFQBthaxHxWgCP/1xzNUmnP6wKs32PkhHwHc2wwgGsoDvnDOo9XuM6cSV/2+wLDLwjXDaPNW3zj945XVfBAhv/6MW71wfdPMwkctCgPOk1KdqYL4MDOV1+UNqHaX4/Z9We6zkGMnqwZxoiSqxsg2i4nJgpgZxUzD9SV82Ys4I8CzRkB8Yd6hCpRQtieaOpNsTcM8WW5oozo6xqcatp68eSgG0Jsnxx/Da/yHboiH+QjvVOeWITp+mXlre6q/ig69/ES80OHxUte43ExXoiZZiNXBtXEA2wTd6seZSfZx4kKs1DOB1w3T6uxLPUU5mrfHJ5I8wrM9k54evVjeESL1nUj6kaybelgq9+Wu9u/peK/ppoWGOI9xkgz+Mrohmsi4AekgKgYDQ2+V9fiz2bH640D3WahGguQxkqbCrp/WP8MbprOlAwBO1YYj9hC/ACq83NQAh3kHK05FdwybgIj1OlHOJ/b4Ae24g1SxjDdrw/fGPrriApnXMnfDl7Lhca58605a1gUz0chS6p1IBr0bJP//RFX9uMHEAhMjMAG5wv7rCNBn2YMfXWKPDLWZMKTXsVKQ6OIgPumMZY4OuDrjN/Qp+uLigGQ5mV8aYamp2IEYaHG8Hvh8P0qZZn/sjs8bEWgWpgo+UPDqiFqaXDFPYHayRrsw6S0/CIK7FojOXZutgbyE3CejBJJafGFGClaWEXfpbYqIQfkMaDjBavNmx3YcTqCsUYY9yRaGuwrzyr4hJe3RsGVMrYn72cJ8+/HUvR43/D1wSc+a1jfJByt/mXpNTDsr1oh+p1Z8wxGNy+Iw1/dfDJlY4+5DegY8L5/VieJgXYPcQAXEK/WAU1GgCpCUATY3QZoKw9IIbAM1O8jq2h7P3zixWedMz5SLA4Ax+6PYmXP2IpAumD79yKA9ggx+EYN0Pmq8i/sjplGCVb6MqF2QkuORTYpZ2SfM8GmZym/X5xNYVxJ1WKTBG3sYYxmP9Iir1gb5V7arTI8fHE5Z08fbcflKbcHshFRCAvzkPYaGOj/jqyKLHR+Ng4i0Qs/qdmEagHqPLmEhy1xW1lHfcA80C2Gmvn7UCyFoGRT3eUTw/OJiqXS9CEgp0wWNaE4n3L2wqEcY
Sent: March 28, 2019 6:51 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] order in fixpoint
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.
|
- [Coq-Club] order in fixpoint, psperatto, 03/28/2019
- Re: [Coq-Club] order in fixpoint, Jason -Zhong Sheng- Hu, 03/29/2019
- Re: [Coq-Club] order in fixpoint, Gaëtan Gilbert, 03/29/2019
Archive powered by MHonArc 2.6.18.