Доступ к первому элементу матрицы в Isabelle

Доступ к «первому» элементу матрицы

Я хочу написать доказательство тривиального случая определителя матрицы, когда матрица состоит всего из одного элемента (т. е. мощность 'n равна единице).

Таким образом, определитель (или det A) является единственным элементом в матрице.

Однако мне непонятно, как ссылаться на один элемент матрицы. Я попробовал A $ zero $ zero, но это не сработало.

Мой текущий способ продемонстрировать проблему — написать ∀a∈(UNIV :: 'n set). det A = A $ a $ a. Предполагается, что мощность числового типа равна единице.

Как правильно записать это тривиальное доказательство детерминантов?

Вот мой текущий код:

theory Notepad
imports
  Main
  "~~/src/HOL/Library/Polynomial"
  "~~/src/HOL/Algebra/Ring"
  "~~/src/HOL/Library/Numeral_Type"
  "~~/src/HOL/Library/Permutations"
  "~~/src/HOL/Multivariate_Analysis/Determinants"
  "~~/src/HOL/Multivariate_Analysis/L2_Norm"
  "~~/src/HOL/Library/Numeral_Type"
begin


lemma det_one_element_matrix:
fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite"
assumes "card(UNIV :: 'n set) = 1"
shows "∀a∈(UNIV :: 'n set). det A = A $ a $ a"
proof-

  (*sledgehammer proof of 1, 2 and ?thesis *)
  have 1: "∀a∈(UNIV :: 'n set). UNIV = {a}"   
  by (metis (full_types) Set.set_insert UNIV_I assms card_1_exists ex_in_conv)

  have 2:
  "det A = (∏i∈UNIV. A $ i $ i)" 
  by (metis (mono_tags, lifting) "1" UNIV_I det_diagonal singletonD)

  from 1 2 show ?thesis by (metis setprod_singleton)

qed

ОБНОВЛЕНИЕ:

К сожалению, это часть большей теоремы, которая уже доказана для мощности 'n∷finite > 1. В этой теореме тип матрицы A зафиксирован как A :: "('a::comm_ring_1)^'n∷finite^'n∷finite, и в этой большей теореме используется определение определителя.

Поэтому я не думаю, что смогу изменить тип моей матрицы A на ('a::comm_ring_1)^1^1), чтобы решить большую теорему.


matrix isabelle
person mrsteve    schedule 23.03.2014    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Я чувствую, что мой предыдущий ответ в целом является лучшим решением, если его можно использовать, поэтому я оставлю его как есть. В вашем случае, когда вы не можете использовать этот подход, к сожалению, все становится немного сложнее.

Что вам нужно показать, так это то, что:

  • В вашем типе 'n может быть только один элемент, поэтому все элементы равны;

  • Кроме того, определение det также ссылается на перестановки, поэтому нам нужно показать, что существует только одна функция типа 'n ⇒ 'n, которая оказывается равной функции id.

Имея их на месте, мы можем провести доказательство следующим образом:

lemma det_one_element_matrix:
  fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite"
  assumes "card(UNIV :: 'n set) = 1"
  shows "det A = A $ x $ x"
proof-
  have 0: "⋀x y. (x :: 'n) = y"
    by (metis (full_types) UNIV_I assms card_1_exists)

  hence 1: "(UNIV :: 'n set) = {x}"
    by auto

  have 2: "(UNIV :: ('n ⇒ 'n) set) = {id}"
    by (auto intro!: ext simp: 0)

  thus ?thesis
    by (auto simp: det_def permutes_def 0 1 2 sign_id)
qed
person davidg    schedule 25.03.2014

arrow_upward
1
arrow_downward

Использование A $ zero $ zero (или A $ 0 $ 0) не сработало бы, потому что векторы индексируются от 1: A $ 0 $ 0 не определено, что затрудняет доказательство чего-либо.

Немного поигравшись сам, я пришел к следующей лемме:

lemma det_one_element_matrix:
   "det (A :: ('a::comm_ring_1)^1^1) = A $ 1 $ 1"
  by (clarsimp simp: det_def sign_def)

Вместо того, чтобы использовать тип 'a :: finite и предполагать, что его мощность равна 1, я использовал стандартный тип Isabelle 1, который кодирует оба этих факта в самом типе. (Похожие типы существуют для всех числительных, так что вы можете писать что-то вроде 'a ^ 23 ^ 72)

Между прочим, после ввода приведенной выше леммы auto solve_direct быстро сообщил мне, что что-то уже существует в библиотеке с таким же результатом, лемма с именем det_1.

person davidg    schedule 23.03.2014
comment
Я добавил следующее обновление к моему вопросу: К сожалению, это часть более крупной теоремы, которая уже доказана для мощности 'n∷finite › 1. В этой теореме тип матрицы A фиксируется как A :: ('a ::comm_ring_1)^'n∷finite^'n∷finite и определение определителя используется в этой большей теореме. Поэтому я не думаю, что смогу изменить тип моей матрицы A на ('a::comm_ring_1)^1^1), чтобы решить мою большую теорему. - person mrsteve; 24.03.2014