Матрица манипуляций Coq - PullRequest
Новая
       6

Матрица манипуляций Coq

2 голосов
/ 04 февраля 2020

Я пытаюсь использовать матрицы в Coq. Я нашел библиотеку, которая делает именно то, что мне нужно, но, будучи очень новой в 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 равно нулю. И на данный момент, я немного не хватает идей. Может ли кто-нибудь прийти мне на помощь?

1 Ответ

2 голосов
/ 04 февраля 2020

Похоже, 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, чтобы решить другие дела). Также есть тактика c, называемая 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 для решения целых и действительных равенств, а также производные тактики c lca для сложных числовые равенства (В вашем доказательстве в некоторых случаях field, похоже, произошел сбой.)

Для более легкого знакомства с библиотекой матриц QWIRE (используемой SQIR) я рекомендую Проверенные квантовые вычисления , хотя вносит некоторые изменения, не отраженные в основной ветке QWIRE.

...