Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] order in fixpoint

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] order in fixpoint


Chronological Thread 
  • 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

Hi Patricia,

I don't expect your definition to work because your return type depends on s, so Coq will not be able to figure out the relation of `s` and the result of pattern matching. You will need to make use of extended pattern matching.

You probably want to read Chlipala's CPDT and learn about extended Gallina before programming in this style.

Thanks,
Jason Hu
https://hustmphrrr.github.io/

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of psperatto AT gmail.com <psperatto AT gmail.com>
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

 




Avast logo

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





Archive powered by MHonArc 2.6.18.

Top of Page