## Stream: Coq users

### Topic: How to Deal with ill-formed Recursion

#### Julia Dijkstra (Jan 07 2024 at 14:14):

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.
``````

#### Karl Palmskog (Jan 07 2024 at 14:29):

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

#### Karl Palmskog (Jan 07 2024 at 14:32):

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

#### Julia Dijkstra (Jan 07 2024 at 14:34):

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

#### Karl Palmskog (Jan 07 2024 at 14:36):

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.

#### Julia Dijkstra (Jan 07 2024 at 14:38):

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

#### Julia Dijkstra (Jan 07 2024 at 14:45):

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.
``````

#### Karl Palmskog (Jan 07 2024 at 14:54):

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

#### Julia Dijkstra (Jan 07 2024 at 14:55):

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

#### Karl Palmskog (Jan 07 2024 at 14:57):

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.

#### Julia Dijkstra (Jan 07 2024 at 14:58):

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.
``````

#### Karl Palmskog (Jan 07 2024 at 14:58):

you need to end each one with `Qed.`

#### Julia Dijkstra (Jan 07 2024 at 14:59):

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

#### Karl Palmskog (Jan 07 2024 at 15:01):

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