CODEWITHSUNDEEP
equalitycoq
krokodil
krokodil

Reputation: 1366

eq_rect and natrual type indices

I have a Matrix record type indexed by two natural numbers (matrix dimensions). When manipulating matrix expressions I got sub-expressions which contains a lot of eq_rect calls to convert between matrix types with convertible dimensions (such as a*b and b*a). What would be a good strategy to prove something like lemma shown below? I am not looking for an exact proof but rather for advice on general techniques for dealing with this kind of proofs. For example I see nested eq_refl calls. Could these be merged? Can I use heterogenous equality to simplify my expressions? Please advice. Example:

Require Export Utf8_core.
Require Import Coq.Arith.Arith.

Record Matrix (m n : nat).

Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q):
  Matrix (m*p) (n*q). Admitted.
Definition mp {m n p: nat} (A: Matrix n m) (B: Matrix m p):
  Matrix n p. Admitted.

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

Definition D (n:nat) : Matrix n n. Admitted.
Definition I (n:nat): Matrix n n. Admitted.
Definition T (m n:nat): Matrix m m. Admitted.
Definition L (m n:nat): Matrix m m. Admitted.

Local Open Scope matrix_scope.

Lemma Foo:
  forall (m0 n0 v : nat) (eqH : (m0 * v * n0 * v)%nat = (m0 * v * (n0 * v))%nat)
    (eqH0 : (m0 * (n0 * v) * v)%nat = (m0 * v * (n0 * v))%nat)
    (eqH1 : (m0 * (n0 * v * v))%nat = (m0 * v * (n0 * v))%nat)
    (eqH2 : (n0 * (v * v))%nat = (n0 * v * v)%nat)
    (eqH3 : (m0 * (n0 * v) * v)%nat = (m0 * (n0 * v * v))%nat)
    (eqH4 : (m0 * n0 * v * v)%nat = (m0 * v * (n0 * v))%nat)
    (eqH5 : (m0 * v * (n0 * v))%nat = (m0 * v * n0 * v)%nat)
    (eqH6 : (n0 * v * v)%nat = (n0 * (v * v))%nat)
    (eqH7 : (m0 * n0 * v * v)%nat = (m0 * (n0 * v * v))%nat),

    eq_rect (m0 * v * n0 * v)%nat (fun (n:nat) => Matrix (m0 * v * (n0 * v)) n)
            (eq_rect (m0 * v * n0 * v)%nat (λ m : nat, Matrix m (m0 * v * n0 * v))
                     (D (m0 * v) ⊗ I n0 ⊗ I v) (m0 * v * (n0 * v))%nat eqH)
            (m0 * v * (n0 * v))%nat eqH * T (m0 * v * (n0 * v)) (n0 * v) *
    eq_rect (m0 * (n0 * v) * v)%nat (λ n : nat, Matrix (m0 * v * (n0 * v)) n)
            (eq_rect (m0 * (n0 * v * v))%nat (λ m : nat, Matrix m (m0 * (n0 * v) * v))
                     ((I m0
                         ⊗ eq_rect (n0 * (v * v))%nat (λ n : nat, Matrix (n0 * v * v) n)
                         ((L (n0 * v) v ⊗ I v) *
                          eq_rect (n0 * (v * v))%nat (λ m : nat, Matrix m (n0 * (v * v)))
                                  (I n0 ⊗ L (v * v) v) (n0 * v * v)%nat eqH2)
                         (n0 * v * v)%nat eqH2 * (D (n0 * v) ⊗ I v)) *
                      eq_rect (m0 * (n0 * v) * v)%nat (λ m : nat, Matrix m (m0 * (n0 * v) * v))
                              (L (m0 * (n0 * v)) m0 ⊗ I v) (m0 * (n0 * v * v))%nat eqH3)
                     (m0 * v * (n0 * v))%nat eqH1) (m0 * v * (n0 * v))%nat eqH0 =
    eq_rect (m0 * n0 * v * v)%nat (λ n : nat, Matrix (m0 * v * (n0 * v)) n)
            (eq_rect (m0 * v * n0 * v)%nat (λ m : nat, Matrix m (m0 * n0 * v * v))
                     ((D (m0 * v) ⊗ I n0 ⊗ I v) *
                      eq_rect (m0 * v * (n0 * v))%nat (λ m : nat, Matrix m (m0 * v * (n0 * v)))
                              (T (m0 * v * (n0 * v)) (n0 * v)) (m0 * v * n0 * v)%nat eqH5 *
                      eq_rect (m0 * (n0 * v * v))%nat (λ m : nat, Matrix m (m0 * (n0 * v * v)))
                              (I m0
                                 ⊗ (L (n0 * v) v ⊗ I v) *
                               eq_rect (n0 * (v * v))%nat (λ m : nat, Matrix m (n0 * (v * v)))
                                       (I n0 ⊗ L (v * v) v) (n0 * v * v)%nat eqH2 *
                               eq_rect (n0 * v * v)%nat (λ m : nat, Matrix m (n0 * v * v))
                                       (D (n0 * v) ⊗ I v) (n0 * (v * v))%nat eqH6)
                              (m0 * v * (n0 * v))%nat eqH1 *
                      eq_rect (m0 * n0 * v * v)%nat (λ m : nat, Matrix m (m0 * n0 * v * v))
                              (L (m0 * n0 * v) m0 ⊗ I v) (m0 * (n0 * v * v))%nat eqH7)
                     (m0 * v * (n0 * v))%nat eqH) (m0 * v * (n0 * v))%nat eqH4.

Upvotes: 2

Views: 95

Answers (1)

ejgallego
ejgallego

Reputation: 6852

My first thought is that you should avoid getting into such complex expressions.

You can make your code more readable by using some implicit parameters, but even then, I would suggest that you study some mature matrix libraries like matrix.v and once you are comfortable with them you redo you example again. Hopefully this will avoid some casting.

[Hint: not a single eq_rect should appear in your lemma, at most a couple of castings]

What is the main statement you'd like to prove?

Upvotes: 1

Related Questions