Coq 如何定位和转换假设以证明它们是错误的?
Coq how to target and transform hypotheses to show that they're false?
我试图证明如果两个布尔值列表相等(使用以明显方式在结构上遍历列表的相等性定义),那么它们具有相同的长度。
然而,在这样做的过程中,我最终遇到了一个假设是 false/uninhabited,但不是字面上的 False
(因此不能成为 [= =15=]战术)。
这是我目前所拥有的。
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 显示的 "goal state"(正确的词是什么?)如下所示。
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)
显然是 false/uninhabited,但这没关系,因为 H : list_bool_eq [] (a :: b) = true
也是错误的。
但是假设H
并不是字面上的False
,所以我们不能直接用contradiction
.
我如何定位/"focus my attention from the perspective of Coq" 假设 H
以便我可以证明它无人居住。是否有大致类似于证明子弹 -, +, *, { ... }
的东西,它在我的证明中创建一个新的上下文,专门用于证明给定的假设是错误的?
如果你简化你的假设 (simpl in H
),你会发现它等价于 false = true
。到那时,您可以使用 easy
策略来完成目标,即使它们在句法上等同于 False
,它也能够消除此类 "obvious" 的矛盾。事实上,您甚至不需要事先进行简化; easy
应该强大到能自己搞清楚什么是矛盾的
(最好证明下面更强的结果:forall l1 l2, list_bool_eq l1 l2 = true <-> l1 = l2
。)
我试图证明如果两个布尔值列表相等(使用以明显方式在结构上遍历列表的相等性定义),那么它们具有相同的长度。
然而,在这样做的过程中,我最终遇到了一个假设是 false/uninhabited,但不是字面上的 False
(因此不能成为 [= =15=]战术)。
这是我目前所拥有的。
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 显示的 "goal state"(正确的词是什么?)如下所示。
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)
显然是 false/uninhabited,但这没关系,因为 H : list_bool_eq [] (a :: b) = true
也是错误的。
但是假设H
并不是字面上的False
,所以我们不能直接用contradiction
.
我如何定位/"focus my attention from the perspective of Coq" 假设 H
以便我可以证明它无人居住。是否有大致类似于证明子弹 -, +, *, { ... }
的东西,它在我的证明中创建一个新的上下文,专门用于证明给定的假设是错误的?
如果你简化你的假设 (simpl in H
),你会发现它等价于 false = true
。到那时,您可以使用 easy
策略来完成目标,即使它们在句法上等同于 False
,它也能够消除此类 "obvious" 的矛盾。事实上,您甚至不需要事先进行简化; easy
应该强大到能自己搞清楚什么是矛盾的
(最好证明下面更强的结果:forall l1 l2, list_bool_eq l1 l2 = true <-> l1 = l2
。)