coq - 指导完成证明
问题描述
我将不胜感激完成此证明的一些指导。我被困在最后一个admit
(我已经完成了其他的没有问题,但我省略了真正的证明)。
我根据我的推理添加了评论,因为我认为它比我试图在一段中描述它解释得更好。
这是正在使用的函数的定义:
In =
fix In (A : Type) (x : A) (l : list A) {struct l} : Prop := match l with
| [ ] => False
| x' :: l' => x' = x \/ In A x l'
end
: forall A : Type, A -> list A -> Prop
Argument A is implicit and maximally inserted
Argument scopes are [type_scope _ _]
map =
fix map (X Y : Type) (f : X -> Y) (l : list X) {struct l} : list Y := match l with
| [ ] => [ ]
| h :: t => f h :: map X Y f t
end
: forall X Y : Type, (X -> Y) -> list X -> list Y
Arguments X, Y are implicit and maximally inserted
Argument scopes are [type_scope type_scope function_scope _]
这是引理:
Lemma foo :
forall (A B : Type) (f : A -> B) (l : list A) (y : B),
In y (map f l) <->
exists x, f x = y /\ In x l.
Proof.
intros A B f l y. split.
- admit.
- induction l as [|x0 l' HIl'].
* admit.
* (*
HIl': (exists x : A, f x = y /\ In x l') -> In y (map f l')
Goal: (exists x : A, f x = y /\ In x (x0 :: l')) -> In y (map f (x0 :: l'))
*)
intros H. simpl.
(*
Goal: f x0 = y \/ In y (map f l')
*)
right.
(*
Taking the right side, because if `f x0 = y`, then the induction
hypothesis would tell us nothing.
*)
apply HIl'.
(*
Goal: exists x : A, f x = y /\ In x l'
*)
destruct H as [x1 H']. exists x1.
(*
This `x1` should be the element that is in both `l'` and `x0 ::
l'`, because we discarded the case when `f x0 = y`.
Goal: f x1 = y /\ In x1 l'
*)
destruct H' as [H'l H'r]. split.
+ (* Goal: fx1 = y *) apply H'l .
+ (* Goal: In x1 l' *)
(*
`x1` must be in `l'`, because we know it is in x0 :: l` by H'r:
H'r: In x1 (x0 :: l')
and we discarded the case where `f x0 = y`.
*)
destruct H'r as [H'rl | H'rr].
{ (* Stuck!!! *) admit. }
{ apply H'rr. } Abort.
解决方案
Lemma foo :
forall (A B : Type) (f : A -> B) (l : list A) (y : B),
In y (map f l) <->
exists x, f x = y /\ In x l.
Proof.
- admit.
- induction l as [|x0 l' HIl'].
* admit.
* (*
-- HIl': (exists x : A, f x = y /\ In x l') -> In y (map f l')
-- Goal: (exists x : A, f x = y /\ In x (x0 :: l')) -> In y (map f (x0 :: l'))
*)
intros H. simpl.
(*
-- Goal: f x0 = y \/ In y (map f l')
you might need to destruct H first.
*)
destruct H.
destruct H.
(* right. *)
(*
-- Taking the right side, because if `f x0 = y`, then the induction
-- hypothesis would tell us nothing.
acatually, consider x = x0, we can subst and just apply H here.
we will destruct on H0 to analysis case x = x0 || In x l'.
*)
destruct H0. {
left.
rewrite H0.
assumption.
}
(* in this case we select rhs. *)
{
right.
apply HIl'.
exists x.
split. {
assumption.
}
{
assumption.
}
}
Admitted.
对不起,我在工作,我想我会在一分钟内编辑这个。
你会注意到In x l
应该破坏假设然后单独分析。当你对 l 进行归纳时,它取代了 to In x (x0 :: l)
,连词应该保持 forx = x0
或In x l
。
推荐阅读
- javascript - Laravel - React,强制 Axios 进行拒绝/捕获
- neo4j - NEO4j Cypher 查询以连接节点数为条件返回路径
- ios - 在 Swift 4 中的 UITableView 的 didSelectRowAt 中指定单元格选择范围
- arrays - Swift - 嵌套字典
- reactjs - 我需要从手机麦克风获取音频流并在 linux 中播放
- ios - 更新 UIImageView 而不重新加载所有数据
- postgresql - 如何使用 codeigniter 进行操作
- python - 每当 null 被强制进入模型的字段时,转到默认字符串
- azure - 作为数组复制()的参数在资源中不起作用
- python - 将字符串从列表插入数据框公式以在熊猫中循环计算