Coq如何定位并转换假设以表明它们是假的？

我试图证明，如果两个布尔表的列表是相等的（使用一个相等的定义，以明显的方式在结构上列出结构列表），那么它们具有相同的长度。然而，在这样做的过程中，我最终处于一种错误/无人居住的假设，但不是字面上的False（因此不能以contradiction策略为目标）。Coq如何定位并转换假设以表明它们是假的？

这是我到目前为止。

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。

我该如何针对假设H的目标/“将我的注意力从Coq的角度着眼”，这样我就可以证明它是无人居住的。是否有类似于证明子弹-, +, *, { ... }的东西在我的证明中创建了一个新的上下文，专门用于显示给定的假设是错误的？

来源

2017-07-11 Gregory Nisbet

如果你简化你的假设（simpl in H），你会看到它相当于false = true。在这一点上，你可以用easy策略来完成目标，即使它们在语法上等于False，它也能够排除这种“明显”的矛盾。事实上，你甚至不需要事先进行简化; easy应该足够强大以找出矛盾本身。

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

来源

2017-07-11 22:27:44

Coq如何定位并转换假设以表明它们是假的？

回答

相关问题