ฉันกำลังพยายามใช้มาริซใน Coq ฉันพบห้องสมุด la ที่ทำสิ่งที่ฉันต้องการอย่างแน่นอน แต่เนื่องจาก 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 จะเป็นศูนย์ และ ณ จุดนี้ ฉันยังขาดไอเดียนิดหน่อย ใครสามารถช่วยฉันได้บ้าง?
