Coq 如何定位和转换假设以证明它们是错误的？答案

【问题标题】：Coq how to target and transform hypotheses to show that they're false?Coq 如何定位和转换假设以证明它们是错误的？
【发布时间】：2017-07-11 22:15:27
【问题描述】：

我试图证明如果两个布尔值列表相等（使用以明显方式在结构上遍历列表的相等定义），那么它们具有相同的长度。

然而，在这样做的过程中，我最终遇到了一个假设是错误的/无人居住的情况，但不是字面上的False（因此不能成为contradiction 策略的目标）。

这是我目前所拥有的。

Require Import Coq.Lists.List.
Require Export Coq.Bool.Bool.

Require Import Lists.List.
Import ListNotations.

Open Scope list_scope.
Open Scope nat_scope.



Fixpoint list_bool_eq (a : list bool) (b: list bool) : bool :=
  match (a, b) with
  | ([], []) => true
  | ([], _) => false
  | (_, []) => false
  | (true::a', true::b') => list_bool_eq a' b'
  | (false::a', false::b') => list_bool_eq a' b'
  | _ => false
  end.

Fixpoint length (a : list bool) : nat :=
  match a with
  | [] => O
  | _::a' => S (length a')
  end.

Theorem equal_implies_same_length : forall (a b : list bool) , (list_bool_eq a b) = true ->  (length a) = (length b).
intros.
induction a.
induction b.
simpl. reflexivity.

在此之后，coqide 显示的 coq 的“目标状态”（正确的词是什么？）如下所示。

2 subgoals
a : bool
b : list bool
H : list_bool_eq [] (a :: b) = true
IHb : list_bool_eq [] b = true -> length [] = length b
______________________________________(1/2)
length [] = length (a :: b)
______________________________________(2/2)
length (a :: a0) = length b

清除一些无关的细节......

Focus 1.
clear IHb.

我们得到

1 subgoal
a : bool
b : list bool
H : list_bool_eq [] (a :: b) = true
______________________________________(1/1)
length [] = length (a :: b)

对于我们人类来说，length [] = length (a :: b) 显然是假的/无人居住，但这没关系，因为 H : list_bool_eq [] (a :: b) = true 也是假的。

但是，假设H 并不是字面意义上的False，所以我们不能只使用contradiction。

我如何定位/“从 Coq 的角度将注意力集中在假设 H 上，以便我可以证明它是无人居住的。是否有类似于证明子弹-, +, *, { ... } 的东西在我的证明中创建了一个新的上下文，专门用于表明给定的假设是错误的？

【问题讨论】：

标签： coq

【解决方案1】：

如果你简化你的假设（simpl in H），你会发现它等价于false = true。此时，您可以使用easy 策略来结束目标，即使它们在语法上等于False，也能够消除这种“明显”的矛盾。事实上，您甚至不需要事先进行简化； easy 应该足够强大，可以自己找出矛盾之处。

（最好证明以下更强的结果：forall l1 l2, list_bool_eq l1 l2 = true <-> l1 = l2。）

【讨论】：