1

我面临以下引理的问题，我认为这应该是正确的。我可以通过小步骤使证明工作到某个点，但是我还没有找到证明整个引理的方法。

lemma abc:
  fixes A :: "'a::comm_ring_1^'n^'n" and l :: 'n and c :: 'a
  shows "(χ i j. if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
         (χ i j. if i = l then c * (A $ j $ i) else (A $ j $ i))"
proof -
  (* here is my draft *)
  have th1: "(χ i j. transpose A $ i $ j) = (χ i j. A $ j $ i)"
    by (simp add: det_transpose transpose_def)
  have "(χ i j. if i = l then (transpose A $ i $ j) else (transpose A $ i $ j)) =
    (χ i j. A $ j $ i)" by (metis column_def row_def row_transpose)
  show ?thesis sorry
qed
4

2 回答 2

2

在开始用 Isabelle 证明某事之前，您应该知道如何在纸上证明它（同样有经验的 Isabelle 用户并不总是听从他们自己的建议；））。如果您知道如何在纸上证明它，那么如何将纸质证明翻译成 Isabelle/Isar 可能仍然不明显。但是，它会更容易提供帮助（并表明您理解手头的数学问题，这与伊莎贝尔本身无关）。

在下文中，我将解释如何处理这种证明：

lemma abc:
  fixes A :: "'a::comm_ring_1^'n^'n" and l :: 'n and c :: 'a
  shows "(χ i j. if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
         (χ i j. if i = l then c * (A $ j $ i) else (A $ j $ i))"

我注意到的第一件事是抽象χ i j. ...。如果我要证明一些关于普通 lambda 抽象的东西，我肯定会想在第一步中摆脱它们，例如，为了证明两个函数f和g是相等的，我会证明f x = g xfor all x。这在伊莎贝尔中由规则表达

ext: (⋀x. ?f x = ?g x) ⟹ ?f = ?g

因为我不太了解，Multivariate_Analysis所以我试图找到一个类似的规则χ，通过

find_theorems "(χ i. ?f i) = (χ i. ?g i)"

第一个命中是我正在寻找的，即

Determinants.Cart_lambda_cong: (⋀x. ?f x = ?g x) ⟹ vec_lambda ?f = vec_lambda ?g

因此，我通过两次应用此规则来开始证明（使用，尽可能频繁地应用intro rule-name引入规则）：rule-name

proof (intro Cart_lambda_cong)

现在我必须证明，对于任意i，j当替换 χ 参数时，该语句成立，即

  fix i j
  show "(if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
        (if i = l then c * (A $ j $ i) else (A $ j $ i))"

然后通过应用 的定义完成证明transpose：

    by (simp add: transpose_def)
qed

或者代替上面的逐步证明，我们可以做

by (auto intro!: Cart_lambda_cong simp: transpose_def)

!after告诉系统应该积极地intro应用这个规则（没有它它不起作用!，但不要问我为什么;），我们必须检查应用规则的踪迹才能找出答案）。

于 2013-06-07T01:49:18.300 回答
2

查看引理可以发现，transpose A $ i $ j = A $ j $ i所有A, i,都成立j，简化器可以很容易地证明这一点：

lemma transpose_eq: "⋀i j. transpose A $ i $ j = A $ j $ i" by (simp add: transpose_def)

如果我们用这个方法手动应用这个方程subst，你的引理可以很容易地解决，只需重写if表达式的分支：

lemma abc:
  fixes A :: "'a::comm_ring_1^'n^'n" and l :: 'n and c :: 'a
  shows "(χ i j. if i = l then c * (transpose A $ i $ j) else (transpose A $ i $ j)) = 
         (χ i j. if i = l then c * (A $ j $ i) else (A $ j $ i))"
  apply (subst transpose_eq)
  apply (subst transpose_eq)
  apply (rule refl)
  done

所以，subst我们应该能够使用简化器而不是apply (simp add: transpose_eq)，对吗？它不起作用的原因是由于一致性规则。基本上，简化器知道一条if_weak_cong规则if（所以我们需要删除这条规则：

  apply (simp add: transpose_def cong del: if_weak_cong)

解决了你原来的引理。

有关更深入的答案，请参阅“为什么 Isabelle 不简化我的“if _ then _ else”构造的主体？ ”。

于 2013-06-07T11:00:50.323 回答