- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我正在尝试制定一个问题,以便只有重写就足够了
来证明目标。我想避免“聪明”地使用命题,而是使用
可以由 Coq 计算的 bool 值。
我定义了一个 bool 测试函数 member
如果元素在列表中,则返回 true,
和 different
如果两个列表中都没有元素,则返回 true。
我想证明我可以重写different
转换成仅使用 member
的表达式.
Theorem different_member: forall xs ys y,
different xs ys = ((negb (member y ys)) || negb (member y xs)).
(negb X || Y)
形式是 bool 含义)。
Theorem diff_mem:
forall xs ys,
different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.
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.
my_simple_rewrite
这做了许多
try rewrite with lemma_x in *
(大约 20 个不同的引理,仅从左到右重写)。它们是关于
bool
的简单引理s 和
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.
最佳答案
你的结果的问题是它不成立。例如,尝试
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)).
eqn_leq : forall m n, (m == n) = (m <= n) && (n <= m)
==
和
<=
运算符是 bool 函数,用于测试自然数的相等性和顺序。第一个是泛型的,适用于任何用 bool 相等函数声明的类型,称为
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
,可用于包含任何元素的列表
eqType
.注意
disjointP
的声明具有来自
bool
的隐式转换至
Prop
(将
b
映射到
b = true
),并且用
reflect
表示谓词,您可以将其视为“当且仅当”连接词,但与
Prop
相关到
bool
.
reflect
谓词和 View 机制(您在证明脚本上看到的
/
标志)在同一事实的 bool 语句和命题语句之间进行转换。因此,虽然我们不能用简单的 bool 相等来说明等价,但我们可以保持
reflect
的许多便利性。谓词。例如:
Goal forall n, n \in [:: 1; 2; 3] -> n \notin [:: 4; 5; 6].
Proof. by apply/disjointP. Qed.
disjointP
将上述目标转换为
disjoint [:: 1; 2; 3] [:: 4; 5; 6]
(
[:: ... ]
只是列表的 Ssreflect 符号),并且可以通过计算发现该目标是正确的。
关于coq - 几乎只使用重写来证明 Coq 中的定理 - 没有 "cleverness",我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/33315458/
我正在尝试理解 Coq 定理: Theorem thm0 : UseCl Pos (PredVP (UsePN john_PN) walk_V) -> UseCl Pos
编辑 Require Import Bool List ZArith. Variable A: Type. Inductive error := | Todo. Induc
我试图在 Coq 中证明以下引理: Lemma not_eq_S2: forall m n, S m <> S n -> m <> n. 这似乎很容易,但我不知道如何完成证明。有人可以帮帮我吗? 谢谢
我想查看我的证明中使用的所有公理。 获取此类信息的最简单方法是什么? 我将使用哪些命令、脚本或工具? 我对所有公理或所有使用过的公理感兴趣。 最佳答案 你应该使用 Print Assumptions
我想以某种方式限制在归纳定义中允许什么样的输入构造函数。说我想说定义二进制数如下: Inductive bin : Type := | O : bin | D : bin -> bin |
Coq 标准库中是否有对自然数进行欧几里德除法的函数?我一直无法找到一个。如果没有,那么从数学上讲,是否有理由不应该有一个? 我想要这个的原因是因为我试图将一个列表分成两个较小的列表。我希望一个列表的
我在将参数传递给 coq 中的产品类型时遇到问题。我有一个看起来像这样的定义, Definition bar (a:Type) := a->Type. 我需要定义一个函数,它接收“a”和“ba
这是本在线类(class)中出现的证明https://softwarefoundations.cis.upenn.edu/plf-current/StlcProp.html#lab222 . Proo
在命题和谓词演算中证明了数十个引理后(有些比其他的更具挑战性,但通常仍然可以在 intro-apply-destruct 自动驾驶仪上证明)我从 ~forall 开始打了一个并立即被捕获。显然,我缺乏
我正在学习命题逻辑和推理规则。析取三段论规则指出,如果我们的前提中有(P 或 Q),并且也有(非 P);然后我们可以到达Q。 我一生都无法弄清楚如何在 Coq 中做到这一点。假设我有: H : A \
从 Coq 引用手册 (8.5p1) 来看,我的印象是 revert是 intro 的倒数,但 generalize 也是如此在某种程度上。例如,revert和 generalize dependen
假设我知道某些自然数是好的。我知道 1 很好,如果 n 很好,那么 3n 就是,如果 n 很好,那么 n+5 就是,这些只是构造好数字的方法。在我看来,这在 Coq 中的充分形式化是 Inductiv
通常在 Coq 中,我发现自己在做以下事情:我有证明目标,例如: some_constructor a c d = some_constructor b c d 而我真的只需要证明a = b因为无论如
我希望能够为不同的归纳定义定义相同的 Coq 符号,并根据参数的类型区分这些符号。 这是一个最小的例子: Inductive type : Type := | TBool : type. Induct
有没有办法对 Coq 的类型类使用递归?例如,在为列表定义显示时,如果您想调用 show递归列表函数,那么你将不得不使用这样的固定点: Require Import Strings.String. R
假设我有一个解决某种引理的奇特策略: Ltac solveFancy := some_preparation; repeat (first [important_step1 | importa
我是 Coq 的新手。我注意到可以使用在 Coq 中定义空集 Inductive Empty_set : Set :=. 是否也可以将函数从空集定义为另一个通用集/类型? 如果是这样怎么办? 最佳答案
有人能给我一个 Coq 中存在实例化和存在泛化的简单例子吗?当我想证明exists x, P ,其中 P是一些 Prop使用 x ,我经常想命名x (如 x0 或类似的),并操纵 P。这可以是 Coq
我见过很多在功能上相互重叠的 Coq 策略。 例如,当您在假设中有确切的结论时,您可以使用 assumption , apply , exact , trivial ,也许还有其他人。其他示例包括 d
我需要使用标准库中称为 Coq.Arith.PeanoNat ( https://coq.inria.fr/library/Coq.Arith.PeanoNat.html ) 的部分。 我尝试过导入整
我是一名优秀的程序员,十分优秀!