- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我试图在 Coq 中定义并证明正确的一个函数,它可以有效地区分两个排序列表。因为它并不总是在结构上较小的项上递归(第一个或第二个列表较小),Fixpoint
不会接受它,所以我尝试使用 Program Fixpoint
反而。
尝试使用策略 simpl
证明函数的属性时或 program_simpl
, Coq 花费几分钟计算,然后产生一个巨大的术语,数百行。我想知道我是否在使用 Program Fixpoint
错误的方式,或者在推理时是否应该使用其他策略而不是简化?
我还想知道在这样的参数中包含正确性所需的属性是否是一个好习惯,或者最好有一个单独的包装函数,它将正确性属性作为参数,并使这个函数只需要两个列表进行比较?
请注意,我确实尝试定义了一个更简单的 make_diff
版本。 ,它只以 l1 和 l2 作为参数并固定了类型 A
和关系 R
,但这仍然产生了一个巨大的术语,当 program_simpl
或 simpl
战术被应用。
*编辑:我的包含是(尽管这里可能不需要它们):
Require Import Coq.Sorting.Sorted.
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Definitions.
Require Import Recdef.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.
Definition is_decidable (A : Type) (R : relation A) := forall x y, {R x y} + {~(R x y)}.
Definition eq_decidable (A : Type) := forall (x y : A), { x = y } + { ~ (x = y) }.
Inductive diff (X: Type) : Type :=
| add : X -> diff X
| remove : X -> diff X
| update : X -> X -> diff X.
Program Fixpoint make_diff (A : Type)
(R : relation A)
(dec : is_decidable A R)
(eq_dec : eq_decidable A)
(trans : transitive A R)
(lt_neq : (forall x y, R x y -> x <> y))
(l1 l2 : list A)
{measure (length l1 + length l2) } : list (diff A) :=
match l1, l2 with
| nil, nil => nil
| nil, (new_h::new_t) => (add A new_h) :: (make_diff A R dec eq_dec trans lt_neq nil new_t)
| (old_h::old_t), nil => (remove A old_h) :: (make_diff A R dec eq_dec trans lt_neq old_t nil)
| (old_h::old_t) as old_l, (new_h::new_t) as new_l =>
if dec old_h new_h
then (remove A old_h) :: make_diff A R dec eq_dec trans lt_neq old_t new_l
else if eq_dec old_h new_h
then (update A old_h new_h) :: make_diff A R dec eq_dec trans lt_neq old_t new_t
else (add A new_h) :: make_diff A R dec eq_dec trans lt_neq old_l new_t
end.
Next Obligation.
Proof.
simpl.
generalize dependent (length new_t).
generalize dependent (length old_t).
auto with arith.
Defined.
Next Obligation.
Proof.
simpl.
generalize dependent (length new_t).
generalize dependent (length old_t).
auto with arith.
Defined.
最佳答案
在这种特殊情况下,我们可以去掉 Program Fixpoint
并使用简单的 Fixpoint
.因为在每次递归调用时我们都会调用 make_diff
在第一个列表的尾部或第二个列表的尾部,我们可以嵌套两个定点函数,如下所示。 (我在这里使用了 Section
机制以避免传递太多相同的参数)
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Relations.Relations.
Section Make_diff.
Variable A : Type.
Variable R : relation A.
Variable dec : is_decidable A R.
Variable eq_dec : eq_decidable A.
Variable trans : transitive A R.
Variable lt_neq : forall x y, R x y -> x <> y.
Fixpoint make_diff (l1 l2 : list A) : list (diff A) :=
let fix make_diff2 l2 :=
match l1, l2 with
| nil, nil => nil
| nil, new_h::new_t => (add A new_h) :: make_diff2 new_t
| old_h::old_t, nil => (remove A old_h) :: make_diff old_t nil
| old_h::old_t, new_h::new_t =>
if dec old_h new_h
then (remove A old_h) :: make_diff old_t l2
else if eq_dec old_h new_h
then (update A old_h new_h) :: make_diff old_t new_t
else (add A new_h) :: make_diff2 new_t
end
in make_diff2 l2.
End Make_diff.
Section
机制不会在生成的签名中包含未使用的参数。这是一个幼稚的测试:
(* make the first 2 arguments implicit *)
Arguments make_diff [A R] _ _ _ _.
Require Import Coq.Arith.Arith.
Compute make_diff lt_dec Nat.eq_dec [1;2;3] [4;5;6].
(* = [remove nat 1; remove nat 2; remove nat 3; add nat 4; add nat 5; add nat 6]
: list (diff nat) *)
关于coq - 如何处理 Coq 中 Program Fixpoint 生成的非常大的术语?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/44612214/
我正在尝试理解 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 ) 的部分。 我尝试过导入整
我是一名优秀的程序员,十分优秀!