Stream: Coq users

Topic: How to prove things about function defined using Program


view this post on Zulip 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.
Admitted.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 17 2020 at 21:48):

The Equations plugin does it too.

view this post on Zulip Paolo Giarrusso (Oct 17 2020 at 21:48):

And unfolding lemmas are all but easy to prove.

view this post on Zulip Lessness (Oct 17 2020 at 22:01):

Thank you very much! Function did the work.

view this post on Zulip Paolo Giarrusso (Oct 18 2020 at 04:01):

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

view this post on Zulip Paolo Giarrusso (Oct 18 2020 at 04:05):

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: Feb 06 2023 at 13:03 UTC