Isabelle中带assumes的lemma如何使用ccontr进行归谬证明？

问题描述 #

理解ccontr规则的工作原理，但不确定如何在带有assumption(s)的lemma中使用它：

可正常运行的示例1 #

lemma l1: "A⊆B ⟶ A ∩ B = A"
proof(rule ccontr)
  assume "¬(A⊆B ⟶ A ∩ B = A)"
  then show False
    by auto
qed

报错的示例2（理论等价的引理） #

尝试将引理拆分为assumes...shows...的形式后报错：

lemma l2: 
  assumes P: "A⊆B"
    shows Q: "A ∩ B = A"
proof(rule ccontr)
  assume "¬(P ⟶ Q)"
  then show False ...
qed

报错信息：

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (¬ (P ⟶ Q)) ⟹ False

提出两个问题：

1. 是否可以通过“假设¬Q并结合已有assumes证明False”的形式完成证明？
2. l1和l2逻辑等价是否正确？Isabelle中二者是否存在显著差异？

解答 #

1. 在带assumes的lemma中正确使用ccontr规则 #

可以通过假设¬Q结合已有assumes证明False，核心是匹配ccontr规则对当前目标的转换逻辑：
当lemma的形式是assumes P shows Q时，初始目标是P ⟹ Q。应用ccontr规则后，目标会转换为P ⟹ ¬Q ⟹ False——即基于前提P，假设结论Q不成立，最终推导出矛盾。

正确的代码实现：

lemma l2: 
  assumes P: "A⊆B"
    shows Q: "A ∩ B = A"
proof(rule ccontr)
  assume "¬Q"  -- 假设结论不成立
  from P and this show False by auto  -- 结合已有前提P推导出矛盾
qed

示例2报错的原因：你错误地假设了¬(P ⟶ Q)，但此时当前目标是P ⟹ Q，ccontr规则并不需要你假设整个蕴含式的否定，而是只需要假设结论Q的否定，再结合已有的前提P完成矛盾推导。

2. l1和l2的逻辑等价性与Isabelle中的差异 #

• 逻辑等价性：二者在逻辑上完全等价，因为P ⟶ Q（蕴含式）和P ⟹ Q（元逻辑蕴含）在Isabelle的高阶逻辑中语义一致，都表达“若P成立则Q成立”。
• Isabelle中的实际差异：
  • 可读性：assumes...shows...的结构更清晰，能明确区分前提和结论，尤其是当引理有多个前提时优势明显。
  • 使用便利性：带assumes的引理在后续证明中可以直接引用前提的名字（如l2.P），或通过OF属性快速应用前提（如l2 OF some_subset_fact）；而l1形式的蕴含式需要手动拆分（如using l1[OF P]）。
  • 局部假设管理：assumes中的前提会作为局部假设存在于证明块中，无需手动引入，简化了证明过程的假设管理。

内容的提问来源于stack exchange，提问作者Alicia M.