The Coq mailing list

[Erik Silkensen <eriksilkensen AT gmail.com>]

Ok, thanks.  I don’t know if this makes a difference, but anyway for context my goal is to define a step-indexed semantics in Coq where one of the rules looks kind of like

(forall k,

  k <= k’ ->

  eval term val k -> P) ->

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

eval term val (S k')

so there’s a premise with a negative occurrence of eval.  I thought, if I can’t write this as an Inductive relation, maybe I could write it as a Fixpoint, where I could tell Coq k is the decreasing argument, and then that’s where I ran into wanting to recur with some k <= k’ and tried to extract that into the first code I sent.

On Nov 2, 2013, at 6:58 AM, Chris Dams <chris.dams.nl AT gmail.com> wrote:

Thanks for such a quick reply and for the pointer to well_founded_induction lt_wf.  Does this mean I should be using the Fix tactic?  Or Function or Program Fixpoint?  I think I’m getting stuck on how syntactically it should look for this basic example.  Thanks again.

I would not use fix or Fixpoint in that case. I would just apply well_founded_induction lt_wf by either using the apply tactic or providing it with arguments by typing them by hand.