Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Program Fixpoint and Nested fix expressions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Program Fixpoint and Nested fix expressions


Chronological Thread 
  • From: Tj Barclay <tjbarclay AT ku.edu>
  • To: <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Program Fixpoint and Nested fix expressions
  • Date: Mon, 14 Sep 2020 17:48:25 -0500
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass (sender ip is 129.237.34.11) smtp.rcpttodomain=inria.fr smtp.mailfrom=ku.edu; dmarc=bestguesspass action=none header.from=ku.edu; dkim=none (message not signed); arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=Abd3VEfjajeB/pgyzimPDZRyYuV4BOUJXs5IrWy5/oI=; b=Z4NcLCbJjTgk8t8+UgTTlpy8PyohOesTvBdlTCWAquC5t+nEmQc70RsCy9Fj9J7AraGtFYw1unQ9MZnnmW+dJPF2Kskv6IUPxKamdM94FqcA7gftb5SpGUxcGUrM3tMvJPm/Sh5rN/JyESY6bU0I2TAD1P5phnE1mr53HTxouD2r4QdqUz4wNoG+lHOPM6hshNF1ogrUfMLHIiIMa6sCNgrX/MqLnb6WanT/lzmy3Zdharc26dN4XHcSHSKZm0N1WcXobNNxedlUUuzhRFK3Kdzwcq73vAACktsRxxf2TGARz5KA2GeyJdyUQcQLMaPgtI0hCYIBab7bAgib+BOPrQ==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=d3W8xDYg+XUSZsMjtbbRSn6P3ZBIrKTeibXkVC42uzLC23IkXTfB7K+pI6XDUMq4L/fJtGFyoLsK4uQU0bYjQKSWl6X3rFxSYL8xYloRHfYZo2WkjWXcMu4jQFSwpRE3NP7lrZ+RKhjzlwLQ+uabrJO7H2G3gkFft5fJ22YF1NAkF7R3NFg8L+VNr6GS2PtuWKTGd5mv0mgjHFskgms8BbM395NX5jhUFufzLNnPiNZ40xMfktXBvYtGNPRaRyEbOV7ffWDOMPONfRmdJ7EV7r8LNjGofcsQoRWQ53jcf0IawWhAUs5yYRobOOb861gS3O99U096yAgg21iHI4oIrg==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tjbarclay AT ku.edu; spf=Pass smtp.mailfrom=tjbarclay AT ku.edu; spf=Pass smtp.helo=postmaster AT NAM11-DM6-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:5yfmcBLGvsnOA2BBBdmcpTZWNBhigK39O0sv0rFitYgeLvvxwZ3uMQTl6Ol3ixeRBMOHsqwC0rCK+PC5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe8bL9oMRm6swrcusYVjId/N6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9g61VoB2jpxJxzY3abpyLOvVif6PQZskVSXZbU8tLSyBNHoGxYo0SBOQBJ+ZYqIz9qkMQoxu8GAKhGfngyiVUiX/yx6I70/kqHAba3AwiBN0Bqm7Uo8nxNKgIUeG416rIzSjZY/xIxDj99ZHFfxY8qv6DQbx+a9DeyVUzFwzblFWQr5ToMT2X2+kRrWSV4fRtWOyvhmM5twx/rCWjy9ouh4fHho8Y1lDK+Dh5zos7K9C2RlB2bN6kHpZQuS+UOIR7T94tTWxupS00yaUGtIa0cSQW0pgr2gLTZv6df4SW/B7uWvydLSp2iX54YL6zmgi+/Ey6xuHiWMS50kxGojdKn9XWq3wA0xre4dWdRPRn5EeuwzOP2hjT6u5aJUA0krLWJYY9z7A3i5YfrF3PECHxlkj3laOWcV4r9fay5+Tgf7XmuoSTN4hpigH4L6sigNS/Af4/MggSQWeU5fi81Lzk/U3/WrlKieA2krXdsJDdIsQbpbS1DBNS0oYm8xq/DjGm38oEnXQfI19JZAiLg5X1N1zMOvz0E+mzjlq2nDt2yf3KI6XtApDXIXjClLfhc6x960lZyAcr0dBf5YlbBasbIP3vXk/+rtzZAwQ6Mwyp2eroFshy1p4GVWKVHqCZKL/SsUOP5u83P+aMY5YVtC/hJPgh+v7hlmQ0mUQdfKmsxZsYcmq0HvVgI0WDYHrjmM0NEWkQvll2cOu/3FaFSHtYY2u4d6M6/DAyToy8W9TtXIeo1YCDlA2yBJZSb3EOXkyOG37yfIGNSt8PdWSfLtI3wW9MbqSoV4J0jULmjwT90bcydrOIqB1djorq0Z1O38OWjQs7pW53EoKQ33zfFzglzFNNfCc/2eVEmWI4z16C1aZihPkIR99Oof5FT1VjbMOO/6lBE9n3Hzn5UJKJRVKhHor0JxgUF4t07/pQJkF3FpOlkwzJ2DesD/kNjbuXCZco86XamX/sO8J6zHWA364k3QAr



On Mon, Sep 14, 2020 at 11:41 AM Christian Doczkal <christian.doczkal AT inria.fr> wrote:
It might be worthwhile to point out that the particular example you give is indeed structurally recursive. That is, the following, which is basically just removing the "Program" and "{measure _}" parts actually works:

Christian is right here. I was so focused on the nested fix aspect of my made up example that I neglected to add another twist to the example that actually results in it not being syntactically structurally recursive.

(* Size of arb lists *)
Fixpoint size_arb_list (al : list arb) : nat :=
  match al with
  | [] => 0
  | a::al' => size_arb a + size_arb_list al'
  end.

(* flatten function for list of arb *)
 Fixpoint flatten (al : list arb) {measure (size_arb_list al)}: list nat :=
  match al with
  | [] => []
  | [A n] => [n]
  | [B n l] => n :: (fix flatten_list (arbs : list (nat * arb)) : list nat :=
                   match arbs with
                   | [] => []
                   | (n',a')::arbs' => n' :: (flatten [a'] ++ flatten_list arbs')
                   end) l
  | a::al' => flatten [a] ++ flatten al'
  end.

---------------------------------

I really appreciate your, and all the others, feedback on this problem.

Best,
TJ



Archive powered by MHonArc 2.6.19+.

Top of Page