I encountered problems when I tried using Program. I can’t prove the following thing (at the end with Admitted):

```
Require Import Permutation List Lia Program.
Set Implicit Arguments.
Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
Inductive variable := aux | num: value -> variable.
Inductive assignment := assign: variable -> variable -> assignment.
Inductive comparison := GT: forall (more less: value), comparison.
Inductive step :=
| assignments: forall (L: list assignment), step
| conditional: forall (c: comparison) (positive negative: step), step.
Definition algorithm := list step.
Fixpoint add_assignments (L: list assignment) (s: step): step :=
match s with
| assignments L0 => assignments (L ++ L0)
| conditional c pos neg => conditional c (add_assignments L pos) (add_assignments L neg)
end.
Definition add_assignments_to_algorithm (L: list assignment) (a: algorithm): algorithm :=
match a with
| nil => conditional (GT x0 x1) (assignments L) (assignments L) :: nil
| x :: t => add_assignments L x :: t
end.
Program Fixpoint compactify_algorithm (a: algorithm) {measure (length a)}: algorithm :=
match a with
| nil => nil
| assignments L :: nil => conditional (GT x0 x1) (assignments L) (assignments L) :: nil
| assignments L :: (x :: t) as tail => compactify_algorithm (add_assignments_to_algorithm L tail)
| conditional c pos neg :: t => conditional c pos neg :: compactify_algorithm t
end.
Theorem compactify_algorithm_aux (a: algorithm) (L: list assignment) (x: step):
compactify_algorithm (assignments L :: x :: a) = compactify_algorithm (add_assignments_to_algorithm L (x :: a)).
Proof.
Admitted.
```

You need an unfolding lemma, proving that compactify_algorithm actually satisfies its defining equation. I was told recently that Function proves them automatically.

The Equations plugin does it too.

And unfolding lemmas are all but easy to prove.

Thank you very much! Function did the work.

BTW, how does the result look like? I haven't used Function much :sweat_smile:

Ah nevermind, https://coq.inria.fr/distrib/current/refman/using/libraries/funind.html#advanced-recursive-functions lists the answer: you get compactify_algorithm_equation

Last updated: Jun 17 2024 at 22:01 UTC