- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
与其他许多不同,Coq 接受一个可选的显式参数,该参数可用于指示固定点定义的递减结构。
从 Gallina 规范,1.3.4,
Fixpoint ident params {struct ident0 } : type0 := term0
Fixpoint interleave (A : Set) (l1 l2 : list A) : list A :=
match l1 with
| [] => []
| h :: t => h :: interleave l2 t
end
l1
也不是
l2
每个周期都在减少。但是如果我们考虑一个度量,定义为
length l1 + length l2
?那么这个措施显然会减少每次递归。
最佳答案
你有多种选择,最后都归结为结构递归。
前言
From Coq Require Import List.
Import ListNotations.
Set Implicit Arguments.
Fixpoint interleave1 {A} (l1 l2 : list A) {struct l1} : list A :=
match l1, l2 with
| [], _ => l2
| _, [] => l1
| h1 :: t1, h2 :: t2 => h1 :: h2 :: interleave1 t1 t2
end.
fix
的技巧。 es -- 见
this definition of Ackermann function (它不适用于仅
Fixpoint
)。
Program Fixpoint
Program Fixpoint
一种让你自然地编写程序并在以后证明它总是终止的机制。
From Coq Require Import Program Arith.
Program Fixpoint interleave2 {A} (l1 l2 : list A)
{measure (length l1 + length l2)} : list A :=
match l1 with
| [] => l2
| h :: t => h :: interleave2 l2 t
end.
Next Obligation. simpl; rewrite Nat.add_comm; trivial with arith. Qed.
Function
Function
与
Program Fixpoint
相比可能有些限制的命令.您可以了解更多关于它们的差异
here .
From Coq Require Recdef.
Definition sum_len {A} (ls : (list A * list A)) : nat :=
length (fst ls) + length (snd ls).
Function interleave3 {A} (ls : (list A * list A))
{measure sum_len ls} : list A :=
match ls with
| ([], _) => []
| (h :: t, l2) => h :: interleave3 (l2, t)
end.
Proof.
intros A ls l1 l2 h t -> ->; unfold sum_len; simpl; rewrite Nat.add_comm; trivial with arith.
Defined.
From Equations Require Import Equations.
Equations interleave4 {A} (l1 l2 : list A) : list A :=
interleave4 l1 l2 by rec (length l1 + length l2) lt :=
interleave4 nil l2 := l2;
interleave4 (cons h t) l2 := cons h (interleave4 l2 t).
Next Obligation. rewrite Nat.add_comm; trivial with arith. Qed.
Fix
/
Fix_F_2
组合子
mergeSort
功能。顺便说一句,
mergeSort
无需使用
Fix
即可定义函数如果您应用嵌套
fix
我之前提到的技巧。这是一个使用
Fix_F_2
的解决方案组合子,因为我们有两个参数,而不是一个像
mergeSort
:
Definition ordering {A} (l1 l2 : list A * list A) : Prop :=
length (fst l1) + length (snd l1) < length (fst l2) + length (snd l2).
Lemma ordering_wf' {A} : forall (m : nat) (p : list A * list A),
length (fst p) + length (snd p) <= m -> Acc (@ordering A) p.
Proof.
unfold ordering; induction m; intros p H; constructor; intros p'.
- apply Nat.le_0_r, Nat.eq_add_0 in H as [-> ->].
intros contra%Nat.nlt_0_r; contradiction.
- intros H'; eapply IHm, Nat.lt_succ_r, Nat.lt_le_trans; eauto.
Defined.
Lemma ordering_wf {A} : well_founded (@ordering A).
Proof. now red; intro ; eapply ordering_wf'. Defined.
(* it's in the stdlib but unfortunately opaque -- this blocks evaluation *)
Lemma destruct_list {A} (l : list A) :
{ x:A & {tl:list A | l = x::tl} } + { l = [] }.
Proof.
induction l as [|h tl]; [right | left]; trivial.
exists h, tl; reflexivity.
Defined.
Definition interleave5 {A} (xs ys : list A) : list A.
refine (Fix_F_2 (fun _ _ => list A)
(fun (l1 l2 : list A)
(interleave : (forall l1' l2', ordering (l1', l2') (l1, l2) -> list A)) =>
match destruct_list l1 with
| inright _ => l2
| inleft pf => let '(existT _ h (exist _ tl eq)) := pf in
h :: interleave l2 tl _
end) (ordering_wf (xs,ys))).
Proof. unfold ordering; rewrite eq, Nat.add_comm; auto.
Defined.
Check eq_refl : interleave1 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Check eq_refl : interleave2 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Check eq_refl : interleave3 ([1;2;3], [4;5;6]) = [1;4;2;5;3;6].
Fail Check eq_refl : interleave4 [1;2;3] [4;5;6] = [1;4;2;5;3;6]. (* Equations plugin *)
Check eq_refl : interleave5 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
destruct_list
,最后一次检查会发生什么?引理?
关于coq - 教 coq 检查终止,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/48173854/
与其他许多不同,Coq 接受一个可选的显式参数,该参数可用于指示固定点定义的递减结构。 从 Gallina 规范,1.3.4, Fixpoint ident params {struct ident0
就目前而言,这个问题不适合我们的问答形式。我们希望答案得到事实、引用或专业知识的支持,但这个问题可能会引起辩论、争论、投票或扩展讨论。如果您觉得这个问题可以改进并可能重新打开,visit the he
前言:我目前正在学习 ANN,因为我在大约 83 个类别中有大约 18500 张图像。它们将用于训练 ANN 以实时识别大致相等的图像。我按照书中的图像示例进行操作,但它对我不起作用。所以我要回到开头
在我的程序中,我处理有时为 NULL 的 C 风格字符串(类型为 char *)。我想教 cout 优雅地处理这些问题(即打印“(null)”而不是段错误)。 我的第一次尝试: ostream& op
我正在开发一个采用(定制的)微线程解决方案的大型程序。有时我需要调试崩溃。在这种时候,能够从一个微线程切换到另一个微线程是很有用的。 如果我正在进行实时调试,我可以将所有寄存器替换为来自微线程上下文的
我可以教 Notepad++ 在它看到多行注释时应用折叠,其中注释以井号开头,多行注释是连续行上的井号吗? # This is a comment # It continues on the next
我被要求为一个 child 辅导 Pascal。尽管在我设法获得教程之前从未见过 Pascal,但我现在知道的足以教他了。 我给你们写信是想看看是否有人能给我指出一些涉及简单算法的基本练习,比如:对这
按照目前的情况,这个问题不适合我们的问答形式。我们希望答案得到事实、引用或专业知识的支持,但这个问题可能会引发辩论、争论、投票或扩展讨论。如果您觉得这个问题可以改进并可能重新打开,visit the
我正在维护来自外国情报监视法庭的大量编辑文件的文件。 它们带有大段文本,如下所示: 当 OCR 尝试处理此问题时,您会收到如下文本: production of this data on a dail
今年夏天,我将教高中生使用 C++ 编程。我必须在一周内教给他们 Material 。通读了公司给我的教程,他们建议我一开始就在程序中使用“include stdafx.h”。 你觉得呢 includ
我需要在他的笔记本电脑上安装一个 c# ide(免费),我需要下载 sdk 还是 windows 7 带有 c# 编译器? (从头开始设置已经有一段时间了) 最佳答案 你可以试试Visual C# 2
背景 我刚刚在 AWS 上启动了一个新的 Redshift 实例,我可以毫无问题地通过 psql cli 客户端连接到它。 问题 我正在尝试让我的 Rails 3 应用程序连接到 Redshift 盒
我是一名优秀的程序员,十分优秀!