The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Wed, May 11, 2016 at 9:56 AM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Thanks! It would be very helpful if Program will work with Lemmas again.

It quite a blow up of a code to add extra definition for each such lemma.

There is one more thing I've noticed about obligations produced by Program. In this example:

Require Import Coq.Arith.Arith.

Require Coq.Program.Tactics.

Record Matrix (m n : nat).

Definition KroneckerProduct {m n p q: nat} (A: Matrix m n) (B: Matrix p q):

  Matrix (m*p) (n*q). Admitted.

Notation "x ⊗ y" := (KroneckerProduct x y) (at level 50, left associativity) : matrix_scope.

Local Open Scope matrix_scope.

Obligation Tactic := (Tactics.program_simpl; subst; auto with arith; try ring).

Program Definition KroneckerProduct_assoc_def

        {xr xc yr yc zr zc: nat}

        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc) :=

  x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z.

Fact KroneckerProduct_assoc

     {xr xc yr yc zr zc: nat}

     (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):

  KroneckerProduct_assoc_def x y z.

Admitted.

If we examine resulting definition of KroneckerProduct_assoc_def:

KroneckerProduct_assoc_def = 

fun (xr xc yr yc zr zc : nat) (x : Matrix xr xc) (y : Matrix yr yc)

  (z : Matrix zr zc) =>

x ⊗ (y ⊗ z) =

eq_rect (xc * yc * zc) (fun n : nat => Matrix (xr * (yr * zr)) n)

  (eq_rect (xr * yr * zr) (fun m : nat => Matrix m (xc * yc * zc)) 

     (x ⊗ y ⊗ z) (xr * (yr * zr))

     (KroneckerProduct_assoc_def_obligation_1 xr xc yr yc zr zc x y z))

  (xc * (yc * zc))

  (KroneckerProduct_assoc_def_obligation_2 xr xc yr yc zr zc x y z)

     : forall xr xc yr yc zr zc : nat,

       Matrix xr xc -> Matrix yr yc -> Matrix zr zc -> Prop

The obligations are generated as:

KroneckerProduct_assoc_def_obligation_1 = 

fun (xr xc yr yc zr zc : nat) (_ : Matrix xr xc) (_ : Matrix yr yc)

  (_ : Matrix zr zc) => eq_sym (Nat.mul_assoc xr yr zr)

     : forall xr xc yr yc zr zc : nat,

       Matrix xr xc ->

       Matrix yr yc -> Matrix zr zc -> xr * yr * zr = xr * (yr * zr)

KroneckerProduct_assoc_def_obligation_2 = 

fun (xr xc yr yc zr zc : nat) (_ : Matrix xr xc) (_ : Matrix yr yc)

  (_ : Matrix zr zc) => eq_sym (Nat.mul_assoc xc yc zc)

     : forall xr xc yr yc zr zc : nat,

       Matrix xr xc ->

       Matrix yr yc -> Matrix zr zc -> xc * yc * zc = xc * (yc * zc)

My first observation is that they do not need to depend on Matrix. The second is that once unused Matrix dependencies are removed the both obligations are the same. Finally, they could be just replaced by (eq_sym (Nat.mul_assoc _ _ _)):

Definition KroneckerProduct_assoc_def'

           {xr xc yr yc zr zc: nat}

           (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc) :=

  x ⊗ (y ⊗ z) =

  eq_rect (xc * yc * zc) (fun n : nat => Matrix (xr * (yr * zr)) n)

          (eq_rect (xr * yr * zr) (fun m : nat => Matrix m (xc * yc * zc))

                   (x ⊗ y ⊗ z) (xr * (yr * zr))

                   (eq_sym (Nat.mul_assoc xr yr zr)))

          (xc * (yc * zc))

          (eq_sym (Nat.mul_assoc xc yc zc)).

I have a lot of Program-generated obligations for trivial arithmetic equivalencies and at some point they become unwieldy to manage. So simpler definitions will help.

Perhaps there are any better ways of dealing with this? I am planning to do a lot of rewriting of matrix expressions and depending on the order of constructing them the sub-expressions for dimensionality differ, usually up to commutativity/associativity (as in the example above). So I end up with expressions heavily littered with eq_rects which look like laborious to prove manually.

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060