Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Erik Silkensen <eriksilkensen AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Writing a recursive function that's not quite structurally recursive?
  • Date: Sat, 2 Nov 2013 02:15:11 -0400

Hi all,

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.

Thanks for any help.

-Erik


Archive powered by MHonArc 2.6.18.

Top of Page