coq - 逻辑:All_In 无法展开嵌套的 forall
问题描述
我面临一个非常奇怪的问题:coq 不想将 forall 变量移动到上下文中。
在过去,它是这样的:
Example and_exercise :
forall n m : nat, n + m = 0 -> n = 0 /\ m = 0.
Proof.
intros n m.
它生成:
n, m : nat
============================
n + m = 0 -> n = 0 /\ m = 0
但是当我们在 forall 里面有 forall 时,它就不起作用了:
(* Auxilliary definition *)
Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
(* ... *)
Lemma All_In :
forall T (P : T -> Prop) (l : list T),
(forall x, In x l -> P x) <->
All P l.
Proof.
intros T P l. split.
- intros H.
在此之后我们得到:
T : Type
P : T -> Prop
l : list T
H : forall x : T, In x l -> P x
============================
All P l
但是如何将 x 移出 H 并将其分解成更小的部分?我试过了:
destruct H as [x H1].
但它给出了一个错误:
Error: Unable to find an instance for the variable x.
它是什么?怎么修?
解决方案
问题在于它forall
嵌套在蕴涵的左侧而不是右侧。x
从形式的假设引入是没有意义的forall x, P x
,就像在另一个证明的上下文中引入n
in是没有意义的一样。plus_comm : forall n m, n + m = m + n
相反,您需要通过在正确的位置应用H
假设来使用它。我不能给你这个问题的答案,但你可能想参考dist_not_exists
同一章中的练习。
推荐阅读
- java - Java - 对泛型 X 的引用应该被参数化
- java - 添加 Java JNI -Xcheck:jni 选项以在 Android Studio 中运行命令
- here-api - 使用 here-api 查找门牌号为 17 1/2 的地址
- python - AttributeError: 'NoneType' object has no attribute 'send' ,当我尝试将带有机器人的消息发送到特定的不和谐频道时
- pine-script - 回测 - 如果在上一次收盘和新交易之间没有发生条件,则不开仓
- javascript - MongoDB 使用聚合管道计算单个用户的所有喜欢和帖子
- uncertainty - 执行不确定性 - 蒙特卡罗分析 - 在 Brightway2 中使用 Ecoinvent
- javascript - 链接没有返回值的承诺的最佳实践
- html - CSS 布局 - 网格或弹性
- ringcentral - 在来电时打开网页