在 Coq 中求解线性方程组

Question

我需要证明这个方程组没有解（原因是它是超定的）。 在 Coq 中是否有一种简单的方法来做到这一点？ IE。战术或图书馆？

Require Import Reals.
Open Scope R.

Lemma no_solution:
  forall 
    b11 b12 b13 b14 b21 b22 b23 b24 b31 b32 b33 b34
    r r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 : R,
   1 = r * b11 + r0 * b21 + r1 * b31    ->
   0 = r * b12 + r0 * b22 + r1 * b32    ->
   0 = r * b13 + r0 * b23 + r1 * b33    ->
   0 = r * b14 + r0 * b24 + r1 * b34    ->
   0 = r2 * b11 + r3 * b21 + r4 * b31   ->
   1 = r2 * b12 + r3 * b22 + r4 * b32   ->
   0 = r2 * b13 + r3 * b23 + r4 * b33   ->
   0 = r2 * b14 + r3 * b24 + r4 * b34   ->
   0 = r5 * b11 + r6 * b21 + r7 * b31   ->
   0 = r5 * b12 + r6 * b22 + r7 * b32   ->
   1 = r5 * b13 + r6 * b23 + r7 * b33   ->
   0 = r5 * b14 + r6 * b24 + r7 * b34   ->
   0 = r8 * b11 + r9 * b21 + r10 * b31  ->
   0 = r8 * b12 + r9 * b22 + r10 * b32  ->
   0 = r8 * b13 + r9 * b23 + r10 * b33  ->
   1 = r8 * b14 + r9 * b24 + r10 * b34  ->
   False.

Answer 1

如果我理解得很好，这一堆方程不可能同时为真，因为它需要 3x4 矩阵的秩高于 3。

您的结果的主要定理在mathematical components library 中称为mulmx_max_rank。我有更多的工作将您对问题的非结构化呈现与 使用矩阵构造一个而不是找到正确的定理。本实验是在 coq-8.7 中进行的，coq-mathcomp-ssreflect 和 coq-mathcomp-algebra 通过 opam（包的版本 1.6.2）加载。

请注意，此结果适用于任何字段结构。

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory Num.Theory.

Open Scope ring_scope.

Section Solving_linear_equation_systems_in_Coq.
Variable R : fieldType.

Definition seq2matrix m n (s : seq (seq R)) :=
  \matrix_(i < m, j < n)
     nth 0 (nth nil s i) j.

Lemma no_solution:
  forall 
    b11 b12 b13 b14 b21 b22 b23 b24 b31 b32 b33 b34
    r r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 : R,
   1 = r * b11 + r0 * b21 + r1 * b31    ->
   0 = r * b12 + r0 * b22 + r1 * b32    ->
   0 = r * b13 + r0 * b23 + r1 * b33    ->
   0 = r * b14 + r0 * b24 + r1 * b34    ->
   0 = r2 * b11 + r3 * b21 + r4 * b31   ->
   1 = r2 * b12 + r3 * b22 + r4 * b32   ->
   0 = r2 * b13 + r3 * b23 + r4 * b33   ->
   0 = r2 * b14 + r3 * b24 + r4 * b34   ->
   0 = r5 * b11 + r6 * b21 + r7 * b31   ->
   0 = r5 * b12 + r6 * b22 + r7 * b32   ->
   1 = r5 * b13 + r6 * b23 + r7 * b33   ->
   0 = r5 * b14 + r6 * b24 + r7 * b34   ->
   0 = r8 * b11 + r9 * b21 + r10 * b31  ->
   0 = r8 * b12 + r9 * b22 + r10 * b32  ->
   0 = r8 * b13 + r9 * b23 + r10 * b33  ->
   1 = r8 * b14 + r9 * b24 + r10 * b34  ->
   False.
Proof.
move => b11 b12 b13 b14 b21 b22 b23 b24 b31 b32 b33 b34
   r r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 eq1 eq2 eq3 eq4
   eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq15 eq16.
set Inp := seq2matrix 4 3 
           [:: [:: r; r0; r1];
               [:: r2; r3; r4];
               [:: r5; r6; r7];
               [:: r8; r9; r10]].
set B := seq2matrix 3 4 [:: [:: b11; b12; b13; b14];
                            [:: b21; b22; b23; b24];
                            [:: b31; b32; b33; b34]].
suff abs: Inp *m B = 1%:M.
  have : (\rank (Inp *m B) <= 3)%N by apply: mulmx_max_rank.
  by rewrite abs mxrank1.
by apply/matrixP=> [[ [ | [ | [ | [ | ?]]]] pi]]
   [ [ | [ | [ | [ | ?]]]] pj] //;
 rewrite /Inp /seq2matrix /= !(mxE, big_ord_recr, big_ord0) //= add0r /=
  -?(eq1, eq2, eq3, eq4, eq5, eq6, eq7, eq8, eq9, eq10, eq11, eq12).
Qed.

End Solving_linear_equation_systems_in_Coq.