Stream: Coq users

Topic: ✔ How to Deal with ill-formed Recursion


view this post on Zulip Julia Dijkstra (Jan 07 2024 at 15:02):

Honestly, I kind of love the absurd spam haha. Thanks a million for the help again. :blush:

view this post on Zulip Notification Bot (Jan 07 2024 at 15:02):

Julia Dijkstra has marked this topic as resolved.

view this post on Zulip Julia Dijkstra (Jan 07 2024 at 15:43):

Karl Palmskog said:

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

For some reason my computer seems to pretty much blow up because of this fixpoint. Is this normal?

view this post on Zulip Karl Palmskog (Jan 07 2024 at 15:47):

which version? they all work for me

view this post on Zulip Julia Dijkstra (Jan 07 2024 at 15:48):

The Program Fixpoint. As soon as I use a simpl tactic it uses up all my memory and hangs coq.

view this post on Zulip Julia Dijkstra (Jan 07 2024 at 15:51):

The final simpl really kills it :sweat_smile: .

From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Init.Nat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import Arith.EqNat.
From Coq Require Import Lia.
From Coq Require Import Lists.List. Import ListNotations.
From Coq Require Import Logic.FunctionalExtensionality.

From Coq Require Import Program.Wf.
From Coq Require Import Strings.String.
From LF Require Import Maps.

Fixpoint depth (p: form): nat :=
    match p with
    | FVar sym => 0
    | <{ true }> => 0
    | <{ false }> => 0
    | <{ p /\ q }> => 1 + max (depth p) (depth q)
    | <{ p \/ q }> => 1 + max (depth p) (depth q)
    | <{ p -> q }> => 1 + max (depth p) (depth q)
    | <{ ~p }> => 1 + depth p
    end.

Program Fixpoint norm_neg (p: form) {measure (depth p)}: form :=
    match p with
    (* Special 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.
(* Behold: SPAMMMMM!!!! *)
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.
Next Obligation. simpl. lia. Qed.

Theorem norm_neg_correct: forall (p: form) (V: valuation), valid' V (norm_neg p) = valid' V p.
Proof.
    induction p.
    - auto.
    - auto.
    - auto.
    - intros. simpl; destruct p1; destruct p2;

view this post on Zulip Karl Palmskog (Jan 07 2024 at 15:51):

cant replicate locally, but might have to do with transparency/opaqueness, see here: https://coq.inria.fr/refman/addendum/program.html

view this post on Zulip Julia Dijkstra (Jan 07 2024 at 16:40):

I'll be completely honest, I don't understand any of it. Not the equations examples either. I thought it worked, but it didn't at all.

view this post on Zulip Dominique Larchey-Wendling (Jan 07 2024 at 16:46):

Possibly in this case you could add an extra polarity argument and then get structural recursion on the formula argument ?

view this post on Zulip Paolo Giarrusso (Jan 07 2024 at 19:19):

@Julia Dijkstra simpl isn't the right tool anyway, sadly. Program Fixpoint with well-founded recursion is a terrible tool. I know the hacks necessary to use it, but Equations avoids the need for them. Coq's Function command is a bit better too, IIRC, but it's much more limited.

view this post on Zulip Paolo Giarrusso (Jan 07 2024 at 19:20):

The idea from Dominique could be a simpler alternative, too.

view this post on Zulip Paolo Giarrusso (Jan 07 2024 at 19:21):

Why I say terrible? For well-founded fixpoints, it's not obvious they satisfy their defining equations, but a proof is needed. Function and Coq-Equations do it for you. Program Fixpoint does not.

view this post on Zulip Paolo Giarrusso (Jan 07 2024 at 19:23):

That proof gives you an unfolding lemma.

view this post on Zulip Paolo Giarrusso (Jan 07 2024 at 19:24):

Moreover, the actual generated definition contains encoding artifacts, so you typically want to use the unfolding lemma, instead of letting simpl unfold the definition. Equations has some support for doing this, Program does not.


Last updated: Jun 23 2024 at 04:03 UTC