Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Erik Silkensen <eriksilkensen AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?
  • Date: Sat, 02 Nov 2013 09:54:27 -0400

On 11/02/2013 02:15 AM, Erik Silkensen wrote:
I was wondering if there’s a way to write a function like

Fixpoint f n :=
match n with
| 0 => True
| S m =>
forall m', m'<= m -> f m'
end.

where the recursive call is with a smaller argument, but it doesn’t come
directly from a constructor, if that makes sense?

You can tell I’m very new to Coq! I was just reading Adam Chlipala’s page on
well-founded recursion (http://adam.chlipala.net/cpdt/html/GeneralRec.html),
and am looking forward to studying it further, but was feeling a bit
overwhelmed at first, and thought I’d ask here in case there’s an easy way
around this example.

For what it's worth, I recommend not trying to write general-recursive functions until you're able to digest that chapter of CPDT. My higher-level meta advice is not to trust your intuitions about what in Coq should be easy, hard, reasonable to learn at the present stage of your studies, etc. CPDT is ordered in a particular way based on my take on appropriate learning order, and quite often you'll do yourself a disservice by "skipping ahead."



Archive powered by MHonArc 2.6.18.

Top of Page