I ran into an issue with a recursive function that doesn't understand that it will eventually terminate. I hacked a "fuel" variable into it to make it behave, but I would really prefer to have a clean implementation if at all possible. What would be the way to do this? I found some material on well-founded relations, but there was so much clutter around that I'm not familiar with yet, that I couldn't make out what's what.

```
Fixpoint norm_neg (p: form) (n: nat): form :=
match n with
| 0 => p
| S n' =>
match p with
(* Base cases. *)
| FNeg (FVar sym) => <{ ~sym }>
| <{ ~true }> => <{ false }>
| <{ ~false }> => <{ true }>
| <{ ~(p /\ q) }> => FOr (norm_neg <{ ~p }> n') (norm_neg <{ ~q }> n')
| <{ ~(p \/ q) }> => FAnd (norm_neg <{ ~p }> n') (norm_neg <{ ~q }> n')
| <{ ~(p -> q) }> => FAnd (norm_neg p n') (norm_neg <{ ~q }> n')
| <{ ~~p }> => norm_neg p n'
(* Recursive cases. *)
| FVar sym => <{ sym }>
| <{ true }> => <{ true }>
| <{ false }> => <{ false }>
| <{ p /\ q }> => FAnd (norm_neg p n') (norm_neg q n')
| <{ p \/ q }> => FOr (norm_neg p n') (norm_neg q n')
| <{ p -> q }> => FImp (norm_neg p n') (norm_neg q n')
end
end.
```

the standard advice on encoding functions with tricky variants (termination measures) is to use Equations: https://github.com/mattam82/Coq-Equations

Specifically, you'll want to define and prove the measure `WellFounded`

separately, then do a `wf`

declaration, as demonstrated here: https://github.com/mattam82/Coq-Equations/blob/main/examples/general_recursion.v

there are of course tons of different ways to do these function encodings other than Equations, some of them are compared here: https://coq.discourse.group/t/fixpoint-with-two-decreasing-arguments/544

I don't think the course I am following allows anything outside of the standard library sadly :sweat_smile: .

the Discourse post I linked shows some Stdlib-only approaches. Please consider asking your course responsible to allow the full Coq Platform (which includes Equations), which is anyway the officially recommended way to install and use Coq.

I will let them know and I am currently giving the discourse page a shot to see if I can figure it out! Thanks.

Well I seem to have implemented a Program Fixpoint now, but I is not recognized later on in my file. What gives?

```
Fixpoint depth (p: form): nat :=
match p with
| FVar sym => 0
| <{ true }> => 0
| <{ false }> => 0
| <{ p /\ q }> => 1 + depth p + depth q
| <{ p \/ q }> => 1 + depth p + depth q
| <{ p -> q }> => 1 + depth p + depth q
| <{ ~p }> => 1 + depth p
end.
Program Fixpoint norm_neg (p: form) {measure (depth p)}: form :=
match p with
(* Base cases. *)
| FNeg (FVar sym) => <{ ~sym }>
| <{ ~true }> => <{ false }>
| <{ ~false }> => <{ true }>
| <{ ~(p /\ q) }> => FOr (norm_neg <{ ~p }>) (norm_neg <{ ~q }>)
| <{ ~(p \/ q) }> => FAnd (norm_neg <{ ~p }>) (norm_neg <{ ~q }>)
| <{ ~(p -> q) }> => FAnd (norm_neg p) (norm_neg <{ ~q }>)
| <{ ~~p }> => norm_neg p
(* Recursive cases. I will again write them all out :P. *)
| FVar sym => <{ sym }>
| <{ true }> => <{ true }>
| <{ false }> => <{ false }>
| <{ p /\ q }> => FAnd (norm_neg p) (norm_neg q)
| <{ p \/ q }> => FOr (norm_neg p) (norm_neg q)
| <{ p -> q }> => FImp (norm_neg p) (norm_neg q)
end.
Next Obligation.
simpl. lia.
Qed.
```

you might have several obligations to prove. Try another `Next Obligation.`

Everytime I call Next Obligation it generates the same goal? I can seemingly keep going forever.

you will get at least one goal per recursive call (modulo what the default Program Fixpoint solver tactic does). So at least 6 goals. Inevitably, a lot of them will be similar.

Well, it simply repeats though:

```
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
Next Obligation.
simpl. lia.
```

you need to end each one with `Qed.`

Oh that's it! That was a crazy amount of Qed spam still haha.

you can try doing `Local Obligation Tactic := simpl; lia.`

before the `Program Fixpoint`

, and most (all?) obligations will likely disappear

Last updated: Jun 13 2024 at 21:01 UTC