1

我需要证明这个方程组没有解（原因是它是超定的）。在 Coq 中有简单的方法吗？即战术或图书馆？

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.
4

1 回答 1

5

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

您的结果的主要定理mulmx_max_rank在数学组件库中调用。我有更多的工作将您对问题的非结构化表示与使用矩阵的结构化表示联系起来，而不是找到正确的定理。这个实验是在 coq-8.7 中进行的，使用coq-mathcomp-ssreflect并通过（包的版本）coq-mathcomp-algebra加载。opam1.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.
于 2018-02-06T09:55:01.613 回答