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."
- [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, AUGER Cédric, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Rui Baptista, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, AUGER Cédric, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Adam Chlipala, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
Archive powered by MHonArc 2.6.18.