Manipulasi matriks Coq

Saya mencoba menggunakan marices di Coq. Saya menemukan perpustakaan yang melakukan apa yang saya butuhkan, tetapi karena masih sangat baru di Coq, saya tidak dapat menemukan cara untuk membuktikan properti yang bermakna.

Pustakanya adalah SQIRE, dan mendefinisikan matriks sebagai berikut:

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

Sekarang, Ada beberapa contoh kerja dalam proyek seperti:

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

(jadi V0 adalah vektor kolom (1,0) )

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

Dan

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

Jadi hal pertama yang saya coba adalah ini:

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.

Dan tidak beruntung di sini. Jadi saya kemudian mencoba untuk tidak menyebutkan kasusnya:

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.

Tapi ini tidak berhasil juga, Coq sepertinya tidak bisa menebak bahwa jika x lebih besar dari 1, maka test x y adalah nol. Dan saat ini, saya agak kekurangan ide. Bisakah seseorang datang menyelamatkan saya?


matrix coq
person Assombrance Andreson    schedule 04.02.2020    source sumber

Jawaban (1)


arrow_upward
2
arrow_downward

Sepertinya solve_matrix tidak tahu apa yang harus dilakukan test dan test2 untuk membuka lipatannya.

Berikut dua solusi yang mungkin:

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.

Untuk bukti yang lebih panjang, Anda harus menghancurkan y dua kali agar Coq dapat mencocokkan polanya (Anda dapat menggunakan omega untuk menyelesaikan kasus lainnya). Ada juga taktik yang disebut destruct_m_eq yang akan berhasil memecah berbagai kasus menjadi beberapa kasus untuk Anda. Berikut bukti manual singkat dari lemma Anda:

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

Sehubungan dengan itu, saya merekomendasikan taktik lia dan lra untuk menyelesaikan persamaan bilangan bulat dan real, dan taktik turunan lca untuk persamaan bilangan kompleks. (field sepertinya gagal dalam beberapa contoh dalam pembuktian Anda.)

Untuk pengenalan yang lebih ringan tentang pustaka matriks QWIRE (digunakan oleh SQIR), saya merekomendasikan Komputasi Kuantum Terverifikasi, meskipun itu membuat beberapa perubahan yang tidak tercermin di cabang utama QWIRE.

person Rand00    schedule 04.02.2020