matrix - Coq 矩阵操作

Question

我正在尝试在 Coq 中使用 marices。我发现 la library 完全符合我的需要，但是在 Coq 中非常新，我无法找到一种方法来证明有意义的属性。

图书馆是SQIRE ，它定义了一个矩阵:

Definition Matrix (m n : nat) := nat -> nat -> C.

现在，项目中有一些工作示例，例如:

Definition V0 : Vector 2 := 
  fun x y => match x, y with 
          | 0, 0 => C1
          | 1, 0 => C0
          | _, _ => C0
          end.

(所以 V0 是列向量 (1,0) )

Definition I (n : nat) : Matrix n n := 
  (fun x y => if (x =? y) && (x <? n) then C1 else C0).

和

Lemma Mmult00 : Mmult (adjoint V0) V0 = I 1. Proof. solve_matrix. Qed.

所以我尝试的第一件事是:

Definition test : Matrix 2 2 :=
  fun x y => match x, y with
          | 0, 0 => 0
          | 0, 1 => 1
          | 1, 0 => 2
          | 1, 1 => 3
          | _, _ => 0
          end.

Definition test2 : Matrix 2 2 :=
  fun x y => match x, y with
          | 0, 0 => 0
          | 0, 1 => 2
          | 1, 0 => 4
          | 1, 1 => 6
          | _, _ => 0
          end.

Lemma double : test2 = 2 .* test. Proof. solve_matrix. Qed.

这里没有运气。所以我然后尝试不列举案例:

Lemma testouille : test2 = 2 .* test.
Proof.
  autounfold with U_db.
  prep_matrix_equality.
  assert (x = 0 \/ x = 1 \/ x >= 2)%nat as X.
  omega.
  destruct X as [X|X].
  - { (* x = 0 *)
      subst.
      assert (y = 0 \/ y = 1 \/ y >= 2)%nat as Y.
      omega.
      destruct Y as [Y|Y].
      - { (* y = 0 *)
          subst.
          simpl.
          field.
        }
      - {
          destruct Y as [Y|Y].
          - { (* y = 1 *)
              subst.
              simpl.
              field.
            }
          - { (* y >= 2 *)
              subst. (* I can't operate for each y, recursions ?*)
              simpl.
              field.
            }
        }
    }
  - { 
      destruct X as [X|X].
      - { (* x = 1 *)
          subst.
          assert (y = 0 \/ y = 1 \/ y >= 2)%nat as Y.
          omega.
          destruct Y as [Y|Y].
          - { (* y = 0 *)
              subst.
              simpl.
              field.
            }
          - {
              destruct Y as [Y|Y].
              - { (* y = 1 *)
                  subst.
                  simpl.
                  field.
                }
              - { (* y >= 2 *)
                  subst. (* I can't operate for each y, recursions ?*)
                  simpl.
                  field.
                }
            }
        }
      - { (* x >= 2, I can't operate for each x, recursions ?*)
          subst.
          simpl.
          field.
        }
    } 
Qed.

但这也不起作用，Coq 似乎无法猜测如果 x 大于 1，则 test x y为零。在这一点上，我有点缺乏想法。有人能来救我吗？

Answer 1

它看起来像 solve_matrix就是不知道是什么test和 test2是展开它们。

以下是两种可能的解决方案:

Lemma double : test2 = 2 .* test. Proof. unfold test, test2. solve_matrix. Qed.

Hint Unfold test test2 : U_db.

Lemma double' : test2 = 2 .* test. Proof. solve_matrix. Qed.

对于更长的证明，您将不得不实际销毁 y两次以便 Coq 可以对其进行模式匹配(您可以使用 omega 来解决其他情况)。还有一种策略叫做 destruct_m_eq这将为您完成将事情分解成案例的工作。这是您引理的较短手动证明:

Lemma testouille : test2 = 2 .* test.
Proof.
  autounfold with U_db.
  prep_matrix_equality.
  unfold test, test2.
  destruct_m_eq.
  all: lca.
Qed.

相关，我推荐战术 lia和 lra用于解决整数和实数等式，以及派生的策略 lca对于复数等式。 ( field 在你的证明中似乎有几次失败。)

为了更轻松地介绍 QWIRE 的矩阵库(由 SQIR 使用)，我推荐 Verified Quantum Computing ，尽管它确实做了一些未反射(reflect)在 QWIRE 主分支中的更改。