Stream: Coq users

Topic: How to Deal with ill-formed Recursion


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: .

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 07 2024 at 14:54):

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

view this post on Zulip Julia Dijkstra (Jan 07 2024 at 14:55):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 07 2024 at 14:58):

you need to end each one with Qed.

view this post on Zulip Julia Dijkstra (Jan 07 2024 at 14:59):

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

view this post on Zulip 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