## Stream: Coq users

### Topic: How to prove things about function defined using Program

#### Lessness (Oct 17 2020 at 21:10):

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

#### Paolo Giarrusso (Oct 17 2020 at 21:48):

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

#### Paolo Giarrusso (Oct 17 2020 at 21:48):

The Equations plugin does it too.

#### Paolo Giarrusso (Oct 17 2020 at 21:48):

And unfolding lemmas are all but easy to prove.

#### Lessness (Oct 17 2020 at 22:01):

Thank you very much! Function did the work.

#### Paolo Giarrusso (Oct 18 2020 at 04:01):

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