作者热门文章
- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我正在阅读 Computational Type Theory and Interactive Theorem Proving with Coq 这本书,并且其中一个练习是让我写下类型的术语:
forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x
我尝试了显而易见的:
Fail Definition L7 : forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x :=
fun (p:bool -> Prop) =>
fun (x:bool) =>
fun (tt:x = true -> p true) =>
fun (ff:x = false -> p false) =>
match x with
| true => tt (eq_refl true)
| false => ff (eq_refl false)
end.
和不太明显的:
Definition bool_dec : forall (x:bool), x = true \/ x = false :=
fun (x:bool) =>
match x with
| true => or_introl (eq_refl true)
| false => or_intror (eq_refl false)
end.
Fail Definition L8 : forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x :=
fun (p:bool -> Prop) =>
fun (x:bool) =>
fun (tt:x = true -> p true) =>
fun (ff:x = false -> p false) =>
match bool_dec x with
| or_introl p => tt p
| or_intror p => ff p
end.
我知道会有一个技巧 match ... in ... return ...
或一些护航模式业务,导致我陷入困境,但我一直花一个小时在这上面,想继续前进。谁能把我从痛苦中解救出来?
最佳答案
首先,您可以像这样在嵌套函数中使用一次关键字fun
fun (p:bool -> Prop)
(x:bool)
(tt:x = true -> p true)
(ff:x = false -> p false) =>
match x with
| true => tt (eq_refl true)
| false => ff (eq_refl false)
end.
现在,一个好的方法是使用策略生成证明(此类对象),然后使用Print
来查看对象是什么。
Theorem L7 : forall (p:bool -> Prop) (x:bool), (x = true -> p true) -> (x = false -> p false) -> p x.
Proof.
intros. destruct x.
- apply H. reflexivity.
- apply H0. reflexivity.
Qed.
Print L7.
输出将是
L7 =
fun (p : bool -> Prop)
(x : bool)
(H : x = true -> p true)
(H0 : x = false -> p false)
=>
(if x as b
return
((b = true -> p true) ->
(b = false -> p false) ->
p b)
then
fun
(H1 : true = true -> p true)
(_ : true = false ->
p false) =>
H1 eq_refl
else
fun
(_ : false = true -> p true)
(H2 : false = false ->
p false) =>
H2 eq_refl) H H0
: forall
(p : bool -> Prop)
(x : bool),
(x = true -> p true) ->
(x = false -> p false) ->
p x
Arguments L7 _%function_scope
_%bool_scope (_
_)%function_scope
关于coq - 寻找一些比赛技巧或车队模式,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/60891430/
我正在为我的现货队列使用 t3a.large 实例,但是我无法在 CreditSpecifications=standard 模式下启动现货队列以节省成本。有人能告诉我如何在 CFT 中实现这一目标吗
我是一名优秀的程序员,十分优秀!