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

Julia Dijkstra has marked this topic as resolved.

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?

which version? they all work for me

The Program Fixpoint. As soon as I use a `simpl`

tactic it uses up all my memory and hangs coq.

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

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

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.

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

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

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

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.

That proof gives you an unfolding lemma.

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