- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
遵循章节GeneralRec 中给出的示例在 Chlipala 书中,我正在尝试编写归并排序算法。
这是我的代码
Require Import Nat.
Fixpoint insert (x:nat) (l: list nat) : list nat :=
match l with
| nil => x::nil
| y::l' => if leb x y then
x::l
else
y::(insert x l')
end.
Fixpoint merge (l1 l2 : list nat) : list nat :=
match l1 with
| nil => l2
| x::l1' => insert x (merge l1' l2)
end.
Fixpoint split (l : list nat) : list nat * list nat :=
match l with
| nil => (nil,nil)
| x::nil => (x::nil,nil)
| x::y::l' =>
let (ll,lr) := split l' in
(x::ll,y::lr)
end.
Definition lengthOrder (l1 l2 : list nat) :=
length l1 < length l2.
Theorem lengthOrder_wf : well_founded lengthOrder.
Admitted.
Fixpoint
写mergeSort函数。因为函数在结构上没有递减:
Fixpoint mergeSort (l: list nat) : list nat :=
if leb (length l) 1 then l
else
let (ll,lr) := split l in
merge (mergeSort ll) (mergeSort lr).
Program Fixpoint
或
Definition
使用术语
Fix
(如在 Chlipala 书中)。
Definition mergeSort : list nat -> list nat.
refine (Fix lengthOrder_wf (fun (l: list nat) => list nat)
(fun (l : list nat) => (fun mergeSort : (forall ls : list nat, lengthOrder ls l -> list nat )=>
if leb (length l) 1 then
let (ll,lr) := split l in
merge (mergeSort ll _) (mergeSort lr _)
else
l))).
2 subgoals, subgoal 1 (ID 65)
l : list nat
mergeSort : forall ls : list nat, lengthOrder ls l -> list nat
ll, lr : list nat
============================
lengthOrder ll l
subgoal 2 (ID 66) is:
lengthOrder lr l
Definition mergeSort : list nat -> list nat.
refine (Fix lengthOrder_wf (fun _ => list nat)
(fun (ls : list nat)
(mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat) =>
if Compare_dec.le_lt_dec 2 (length ls)
then let lss := split ls in
merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
else ls)).
2 subgoals, subgoal 1 (ID 68)
ls : list nat
mergeSort : forall ls' : list nat, lengthOrder ls' ls -> list nat
l : 2 <= length ls
lss := split ls : list nat * list nat
============================
lengthOrder (fst lss) ls
subgoal 2 (ID 69) is:
lengthOrder (snd lss) ls
最佳答案
很容易看出,您需要进行两项更改才能获得 A. Chlipala 的解决方案。
1)做split
的时候你需要记住ll
和 lr
来自split,否则它们将是一些任意列表,它们不可能比原始列表l
短.
以下代码无法保存此类信息:
let (ll,lr) := split l in
merge (mergeSort ll _) (mergeSort lr _)
let lss := split ls in
merge (mergeSort (fst lss) _) (mergeSort (snd lss) _)
ll
和
lr
来自
split l
发生这种情况是因为
let (ll,lr)
只是
match
变相(参见手册,
§2.2.3)。
split l
在我们对其进行模式匹配之前,它不会出现在目标或上下文中的任何地方。我们只是随意地将其引入定义中。这就是为什么模式匹配没有给我们任何东西——我们不能替换
split l
在目标或上下文中使用其“特殊情况”(
(ll,lr)
),因为没有
split l
任何地方。
=
),还有另一种方法:
(let (ll, lr) as s return (s = split l -> list nat) := split l in
fun split_eq => merge (mergeSort ll _) (mergeSort lr _)) eq_refl
remember
战术。我们已经摆脱了
fst
和
snd
,但这是一个巨大的矫枉过正,我不会推荐它。
ll
和
lr
短于
l
当
2 <= length l
.
if
-表达式是
match
变相也是如此(它适用于具有恰好两个构造函数的任何归纳数据类型),我们需要一些机制来记住
leb 2 (length l) = true
在
then
分支。同样,因为我们没有
leb
在任何地方,这些信息都会丢失。
leb 2 (length l)
作为一个方程(就像我们在第一部分中所做的那样),或 bool
(因此它可以代表两种选择),但它还应该记住我们需要的一些额外信息。然后我们可以对比较结果进行模式匹配并提取信息,当然,在这种情况下必须是 2 <= length l
的证明。 . m <= n
证明的类型在
leb m n
的情况下返回
true
和一个证明,比如说,
m > n
除此以外。
sumbool
:
Inductive sumbool (A B : Prop) : Set :=
left : A -> {A} + {B} | right : B -> {A} + {B}
{A} + {B}
只是
sumbool A B
的符号(语法糖) .
bool
,它有两个构造函数,但另外它还记得两个命题之一的证明
A
和
B
.它的优势超过
bool
当您使用
if
对其进行案例分析时显示: 你得到
A
的证明在
then
分支和
B
的证明在
else
分支。换句话说,您可以使用事先保存的上下文,而
bool
不携带任何上下文(仅在程序员的脑海中)。
else
分支,但我们想得到
2 <= length l
在我们的
then
分支。所以,让我们问问 Coq 是否已经有一个返回类型的比较函数:
Search (_ -> _ -> {_ <= _} + {_}).
(*
output:
le_lt_dec: forall n m : nat, {n <= m} + {m < n}
le_le_S_dec: forall n m : nat, {n <= m} + {S m <= n}
le_ge_dec: forall n m : nat, {n <= m} + {n >= m}
le_gt_dec: forall n m : nat, {n <= m} + {n > m}
le_dec: forall n m : nat, {n <= m} + {~ n <= m}
*)
if leb 2 (length l) then ...
与
if le_lt_dec 2 (length l) ...
并获取
2 <= length
在证明上下文中,这将使我们完成证明。
关于coq - 使用 Fix 或 Program Fixpoint 在 Coq 中编写有根据的程序,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/42285235/
关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。 想改善这个问题吗?更新问题,使其成为 on-topic对于堆栈溢出。 3年前关闭。 Improve thi
有人知道可以在线使用 FIX 实用程序来验证修复消息吗?即:接受修复消息并检查诸如正文长度和校验和之类的内容。谢谢 最佳答案 https://fixspec.com 上有一个修复日志解码器.当您输入一
在FIX服务器上发送订单请求并更改标签的顺序。 如果我想要输出由我安排的序列(而不是被服务器修改)。 public void send50(Order order) { quickfix.fi
我正在用 C++ 构建一个 FIX 引擎,但我没有引用来了解什么是好的性能数字。考虑到网络时间和 FIX 解析时间,客户端向服务器发送 FIX 消息的最佳时间(以微秒为单位)是多少?还有人知道这个简单
关闭。这个问题不符合Stack Overflow guidelines .它目前不接受答案。 要求提供代码的问题必须表现出对所解决问题的最低限度理解。包括尝试过的解决方案、为什么它们不起作用,以及
我不明白为什么我的固定背景开始出现,因为它有时没有被固定。 这是一个非常特殊的案例,我知道如何解决它。 您可以删除: .row2 position:relative 或 row1 div -webki
我看过三列的例子(fixed fluid fixed)。但是,我需要一个四列解决方案的示例。 两个外部列是固定的。两个内柱是流动的。 固定 |流体 |流体 |固定 最佳答案 您可以使用 calc .
我试图说服自己输入 Fix和功能 fix是一回事。 但我找不到他们的定义之间的相关性 -- definition of fix fix :: (p -> p) -> p fix f = let {x
这是我已经在这里提出的另一个问题的后续How can I play a single tone or custom wave with Delphi? 长话短说,我使用 MMSystem 的 wave
刚刚完成一个站点并遇到位置问题:已在 IE7 上修复。我用谷歌搜索并尝试了不同的 Doctypes,但固定区域在 IE7 上仍然不在位。 我没有 IE7,但一位客户员工有,我可以使用在线 IE 渲染器
我有我的 设置为 background-attachment: fixed但这留下了我的标签正常滚动。如果我设置 position: fixed到我的标签,它们会跳转到页面顶部。有什么办法可以做与 b
我有一个包含标题页(导航栏)的 php 页面。我想将导航栏显示为固定标题,但每当将其位置更改为固定时,它都会删除滚动条(水平和垂直)并且我无法滚动页面。如果我想保持我的标题固定并且我不想固定位置。我怎
已结束。此问题不符合 Stack Overflow guidelines .它目前不接受答案。 要求我们推荐或查找工具、库或最喜欢的场外资源的问题对于 Stack Overflow 来说是无关紧要的,
我正在使用 jquery mobile,对于页眉/页脚,我使用的是 data-position="fixed"。 但是,当我们滚动页面时......页眉页脚消失并在滚动停止时重新出现.. 有没有一种方
我正在尝试连接到使用 FIX 5.0 的代理 我想利用 quickfixj以方便和快速地实现。 这行吗?我假设 5.0 extends(可以这么说)以前版本的功能,但我不想走得太远,结果导致更多问题,
如何放置 position:fixed内容在页面背景中的容器,而其他内容在其上滚动,同时仍然保持点击背景元素的能力? 效果类似于前景内容在固定背景上滚动的视差滚动情况,但我希望能够将 HTML 放在背
我尝试将 z-index 设置为 body 下的某些位置为 fixed 的元素 示例如下: HTML menu content ....
我花了几个小时寻找这个问题的答案,但其他人提供解决方案的场景似乎比我的稍微简单一些。 有没有办法在固定大小的 div 中放置一个 position:fixed 元素,而该元素不会溢出 div? 换句话
此问题已在 SO 和其他地方多次报告,但我找不到任何有效的解决方案。 如果您有固定位置的 div 和固定附加的背景,在某些特定情况下,在 Google Chrome 上呈现会出现错误(在 Firefo
我想在我网站的页面顶部创建一个标题栏,但我在布局方面遇到了问题。以下是我想要的结果: goal http://ambiguities.ca/images/goal.png 这是 html:
我是一名优秀的程序员,十分优秀!