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.