在 Coq 中几乎只使用重写来证明一个定理 - 没有 "cleverness"
Proving a theorem in Coq using almost only rewrites - no "cleverness"
我正在尝试制定一个问题,以便仅重写就足够了
来证明目标。我想避免 "clever" 使用命题,而是使用
可以通过 Coq 计算的布尔值。
我定义了一个布尔测试函数 member
returns true iff 一个元素在列表中,
different
如果两个列表中都没有元素,则 returns 为真。
我想证明我可以只使用 member
.
将 different
重写成一个表达式
Theorem different_member: forall xs ys y,
different xs ys = ((negb (member y ys)) || negb (member y xs)).
((negb X || Y)
形式是布尔蕴涵)
作为热身和现实检验,我想证明
Theorem diff_mem:
forall xs ys,
different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
继续的方法是在 xs 上进行归纳,但我在最后一步一直搞砸了。
非常感谢您对这两个定理的帮助!这里是开发的相关部分。
Require Import Arith.
Require Import List.
Require Import Bool.
Import List.ListNotations.
Open Scope list.
Open Scope bool.
Fixpoint member x ys :=
match ys with
| [] => false
| y :: ys' => (beq_nat x y) || (member x ys')
end.
Lemma mem1: forall x, member x [] = false.
Proof. auto. Qed.
Lemma mem2: forall x y l, member x (y::l) = (beq_nat x y) || (member x l).
Proof. auto. Qed.
Fixpoint different xs ys :=
match xs with
| [] => true
| x::xs' => (negb (member x ys)) && (different xs' ys)
end.
Lemma diff1: forall ys, different [] ys = true.
Proof. auto. Qed.
Lemma diff2: forall x xs ys,
different (x::xs) ys = (negb (member x ys)) && (different xs ys).
Proof. auto. Qed.
Theorem diff_mem1: forall xs ys, different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
Proof.
Abort.
Theorem different_member:
forall xs ys y, different xs ys =
((negb (member y ys)) || negb (member y xs)).
Proof.
Abort.
编辑:
这里是diff_mem1
定理的证明。 (睡在上面,在 ProofGeneral 中开始敲打它之前思考有时会有所帮助……)。另一个定理的证明遵循相同的结构。
然而,问题和最终目标仍然是如何通过重写和提示完全解决它,这样人们就可以(几乎)做到 induction xs; auto.
.
Theorem diff_mem1: forall xs ys,
different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
Proof.
induction xs as [|a xs]; intros ys Hdiff y Hxs Hys.
- inversion Hxs.
- (* we assume y is a member of ys, and of (a::xs) *)
(* it is also assumed that (a::xs) is different from ys *)
(* consider the cases y=a and y<>a *)
remember (beq_nat y a) as Q; destruct Q.
+ (* this case is absurd since y is a member of both ys and (y::xs) *)
apply eq_sym in HeqQ; apply beq_nat_true in HeqQ.
subst a.
simpl in Hdiff.
rewrite Hys in Hdiff.
inversion Hdiff.
+ (* this case is also absurd since y is a member of both ys and xs *)
simpl in Hdiff, Hxs.
rewrite <- HeqQ in Hxs.
simpl in Hxs.
rewrite Bool.andb_true_iff in Hdiff; destruct Hdiff as [_ Hdiff1].
destruct (IHxs ys Hdiff1 y Hxs Hys).
Qed.
编辑2:
我将关闭它,因为@Arthur 给出了我在最初尝试中失败的原因的正确答案,但为了完整起见,我想按照我的目标添加一个解决方案。
我写了一个 Ltac 策略 my_simple_rewrite
,它做了很多 try rewrite with lemma_x in *
(大约 20 个不同的引理,只是从左到右重写)。它们是关于 bool
和上面的 mem1
、mem2
、diff1
和 diff2
的简单引理。为了证明这个定理我用了它,并且只指定了归纳变量xs
和哪个bool
表达式进行案例分析(使用自制的Ltac bool_destruct
),得到了以下证明。
Theorem different_member:
forall xs ys, different xs ys = true ->
forall y, ((negb (member y ys)) || negb (member y xs)) = true.
Proof.
induction xs as [| a xs]; intros; my_simple_rewrite.
- congruence.
- try
match goal with
| [ HH:_ |- _] => (generalize (IHxs ys HH y); intro IH)
end;
bool_destruct (member a ys);
bool_destruct (member y ys);
bool_destruct (member a xs);
bool_destruct (member y xs);
bool_destruct (beq_nat y a);
my_simple_rewrite;
congruence.
Qed.
想法是这几乎可以自动化。可以自动选择要破坏的术语,并注意它试图用任何它可以攻击的东西来实例化归纳假设 - ("if it works, fine! otherwise try the next alternative...").
为了将来参考,完整的发展在https://gist.github.com/larsr/10b6f4817b5117b335cc
你的结果的问题是它不成立。例如,尝试
Compute different [2] [1; 2]. (* false *)
Compute (negb (member 1 [2]) || negb (member 1 [1; 2])). (* true *)
发生这种情况是因为,为了获得相反的结果,我们需要右侧对所有 y
都有效。正确的形式是:
forall xs ys,
different xs ys = true <->
(forall y, negb (member y xs) || negb (member x xs)).
不过,将某些结果指定为布尔方程会让它们在许多情况下使用起来更方便,这一点是正确的。这种风格被大量使用,例如,在 Ssreflect 库中,他们在那里编写定理,例如:
eqn_leq : forall m n, (m == n) = (m <= n) && (n <= m)
此处,==
和 <=
运算符是布尔函数,用于测试自然数的相等性和顺序。第一个是通用的,适用于使用布尔相等函数声明的任何类型,在 Ssreflect.
中称为 eqType
这是使用 Ssreflect 的定理版本:
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq.
Section Different.
Variable T : eqType.
Implicit Types xs ys : seq T.
Fixpoint disjoint xs ys :=
match xs with
| [::] => true
| x :: xs' => (x \notin ys) && disjoint xs' ys
end.
Lemma disjointP xs ys :
reflect (forall x, x \in xs -> x \notin ys)
(disjoint xs ys).
Proof.
elim: xs=> [|x xs IH] /=; first exact: ReflectT.
apply/(iffP andP)=> [[x_nin /IH {IH} IH] x'|xsP].
by rewrite inE=> /orP [/eqP ->|] //; auto.
apply/andP; rewrite xsP /= ?inE ?eqxx //.
apply/IH=> x' x'_in; apply: xsP.
by rewrite inE x'_in orbT.
Qed.
End Different.
我已将 different
重命名为 disjoint
,并使用了 Ssreflect 列表成员运算符 \in
和 \notin
,可用于包含任何 [= 中的元素的列表18=]。请注意,disjointP
的语句具有从 bool
到 Prop
的隐式转换(将 b
映射到 b = true
),并且它用 reflect
谓词,您可以认为它类似于 "if and only if" 连接词,但将 Prop
与 bool
相关联。
Ssreflect 广泛使用 reflect
谓词和 view 机制(您在证明脚本中看到的 /
符号)在布尔值和同一事实的命题陈述。因此,虽然我们不能用简单的布尔相等来表示等价性,但我们可以使用 reflect
谓词保持大部分便利。例如:
Goal forall n, n \in [:: 1; 2; 3] -> n \notin [:: 4; 5; 6].
Proof. by apply/disjointP. Qed.
这里发生的事情是 Coq 使用 disjointP
将上述目标转换为 disjoint [:: 1; 2; 3] [:: 4; 5; 6]
([:: ... ]
只是列表的 Ssreflect 符号),并且可以发现该目标是仅通过计算为真。
我正在尝试制定一个问题,以便仅重写就足够了 来证明目标。我想避免 "clever" 使用命题,而是使用 可以通过 Coq 计算的布尔值。
我定义了一个布尔测试函数 member
returns true iff 一个元素在列表中,
different
如果两个列表中都没有元素,则 returns 为真。
我想证明我可以只使用 member
.
different
重写成一个表达式
Theorem different_member: forall xs ys y,
different xs ys = ((negb (member y ys)) || negb (member y xs)).
((negb X || Y)
形式是布尔蕴涵)
作为热身和现实检验,我想证明
Theorem diff_mem:
forall xs ys,
different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
继续的方法是在 xs 上进行归纳,但我在最后一步一直搞砸了。
非常感谢您对这两个定理的帮助!这里是开发的相关部分。
Require Import Arith.
Require Import List.
Require Import Bool.
Import List.ListNotations.
Open Scope list.
Open Scope bool.
Fixpoint member x ys :=
match ys with
| [] => false
| y :: ys' => (beq_nat x y) || (member x ys')
end.
Lemma mem1: forall x, member x [] = false.
Proof. auto. Qed.
Lemma mem2: forall x y l, member x (y::l) = (beq_nat x y) || (member x l).
Proof. auto. Qed.
Fixpoint different xs ys :=
match xs with
| [] => true
| x::xs' => (negb (member x ys)) && (different xs' ys)
end.
Lemma diff1: forall ys, different [] ys = true.
Proof. auto. Qed.
Lemma diff2: forall x xs ys,
different (x::xs) ys = (negb (member x ys)) && (different xs ys).
Proof. auto. Qed.
Theorem diff_mem1: forall xs ys, different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
Proof.
Abort.
Theorem different_member:
forall xs ys y, different xs ys =
((negb (member y ys)) || negb (member y xs)).
Proof.
Abort.
编辑:
这里是diff_mem1
定理的证明。 (睡在上面,在 ProofGeneral 中开始敲打它之前思考有时会有所帮助……)。另一个定理的证明遵循相同的结构。
然而,问题和最终目标仍然是如何通过重写和提示完全解决它,这样人们就可以(几乎)做到 induction xs; auto.
.
Theorem diff_mem1: forall xs ys,
different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
Proof.
induction xs as [|a xs]; intros ys Hdiff y Hxs Hys.
- inversion Hxs.
- (* we assume y is a member of ys, and of (a::xs) *)
(* it is also assumed that (a::xs) is different from ys *)
(* consider the cases y=a and y<>a *)
remember (beq_nat y a) as Q; destruct Q.
+ (* this case is absurd since y is a member of both ys and (y::xs) *)
apply eq_sym in HeqQ; apply beq_nat_true in HeqQ.
subst a.
simpl in Hdiff.
rewrite Hys in Hdiff.
inversion Hdiff.
+ (* this case is also absurd since y is a member of both ys and xs *)
simpl in Hdiff, Hxs.
rewrite <- HeqQ in Hxs.
simpl in Hxs.
rewrite Bool.andb_true_iff in Hdiff; destruct Hdiff as [_ Hdiff1].
destruct (IHxs ys Hdiff1 y Hxs Hys).
Qed.
编辑2:
我将关闭它,因为@Arthur 给出了我在最初尝试中失败的原因的正确答案,但为了完整起见,我想按照我的目标添加一个解决方案。
我写了一个 Ltac 策略 my_simple_rewrite
,它做了很多 try rewrite with lemma_x in *
(大约 20 个不同的引理,只是从左到右重写)。它们是关于 bool
和上面的 mem1
、mem2
、diff1
和 diff2
的简单引理。为了证明这个定理我用了它,并且只指定了归纳变量xs
和哪个bool
表达式进行案例分析(使用自制的Ltac bool_destruct
),得到了以下证明。
Theorem different_member:
forall xs ys, different xs ys = true ->
forall y, ((negb (member y ys)) || negb (member y xs)) = true.
Proof.
induction xs as [| a xs]; intros; my_simple_rewrite.
- congruence.
- try
match goal with
| [ HH:_ |- _] => (generalize (IHxs ys HH y); intro IH)
end;
bool_destruct (member a ys);
bool_destruct (member y ys);
bool_destruct (member a xs);
bool_destruct (member y xs);
bool_destruct (beq_nat y a);
my_simple_rewrite;
congruence.
Qed.
想法是这几乎可以自动化。可以自动选择要破坏的术语,并注意它试图用任何它可以攻击的东西来实例化归纳假设 - ("if it works, fine! otherwise try the next alternative...").
为了将来参考,完整的发展在https://gist.github.com/larsr/10b6f4817b5117b335cc
你的结果的问题是它不成立。例如,尝试
Compute different [2] [1; 2]. (* false *)
Compute (negb (member 1 [2]) || negb (member 1 [1; 2])). (* true *)
发生这种情况是因为,为了获得相反的结果,我们需要右侧对所有 y
都有效。正确的形式是:
forall xs ys,
different xs ys = true <->
(forall y, negb (member y xs) || negb (member x xs)).
不过,将某些结果指定为布尔方程会让它们在许多情况下使用起来更方便,这一点是正确的。这种风格被大量使用,例如,在 Ssreflect 库中,他们在那里编写定理,例如:
eqn_leq : forall m n, (m == n) = (m <= n) && (n <= m)
此处,==
和 <=
运算符是布尔函数,用于测试自然数的相等性和顺序。第一个是通用的,适用于使用布尔相等函数声明的任何类型,在 Ssreflect.
eqType
这是使用 Ssreflect 的定理版本:
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq.
Section Different.
Variable T : eqType.
Implicit Types xs ys : seq T.
Fixpoint disjoint xs ys :=
match xs with
| [::] => true
| x :: xs' => (x \notin ys) && disjoint xs' ys
end.
Lemma disjointP xs ys :
reflect (forall x, x \in xs -> x \notin ys)
(disjoint xs ys).
Proof.
elim: xs=> [|x xs IH] /=; first exact: ReflectT.
apply/(iffP andP)=> [[x_nin /IH {IH} IH] x'|xsP].
by rewrite inE=> /orP [/eqP ->|] //; auto.
apply/andP; rewrite xsP /= ?inE ?eqxx //.
apply/IH=> x' x'_in; apply: xsP.
by rewrite inE x'_in orbT.
Qed.
End Different.
我已将 different
重命名为 disjoint
,并使用了 Ssreflect 列表成员运算符 \in
和 \notin
,可用于包含任何 [= 中的元素的列表18=]。请注意,disjointP
的语句具有从 bool
到 Prop
的隐式转换(将 b
映射到 b = true
),并且它用 reflect
谓词,您可以认为它类似于 "if and only if" 连接词,但将 Prop
与 bool
相关联。
Ssreflect 广泛使用 reflect
谓词和 view 机制(您在证明脚本中看到的 /
符号)在布尔值和同一事实的命题陈述。因此,虽然我们不能用简单的布尔相等来表示等价性,但我们可以使用 reflect
谓词保持大部分便利。例如:
Goal forall n, n \in [:: 1; 2; 3] -> n \notin [:: 4; 5; 6].
Proof. by apply/disjointP. Qed.
这里发生的事情是 Coq 使用 disjointP
将上述目标转换为 disjoint [:: 1; 2; 3] [:: 4; 5; 6]
([:: ... ]
只是列表的 Ssreflect 符号),并且可以发现该目标是仅通过计算为真。