用无法证明的子目标卡住证明引理
Stuck proving lemma with unprovable subgoals
我正在尝试证明基于以下定义的引理。
Section lemma.
Variable A : Type.
Variable P : A -> Prop.
Variable P_dec : forall x, {P x}+{~P x}.
Inductive vector : nat -> Type :=
| Vnil : vector O
| Vcons : forall {n}, A -> vector n -> vector (S n).
Arguments Vcons {_} _ _.
Fixpoint countPV {n: nat} (v : vector n): nat :=
match v with
| Vnil => O
| Vcons x v' => if P_dec x then S (countPV v') else countPV v'
end.
我要证明的引理如下
Lemma lem: forall (n:nat) (a:A) (v:vector n),
S n = countPV (Vcons a v) -> (P a /\ n = countPV v).
我已经尝试了很多东西,目前我正处于这一点。
Proof.
intros n a v.
unfold not in P_dec.
simpl.
destruct P_dec.
- intros.
split.
* exact p.
* apply eq_add_S.
exact H.
- intros.
split.
此时上下文:
2 subgoals
A : Type
P : A -> Prop
P_dec : forall x : A, {P x} + {P x -> False}
n : nat
a : A
v : vector n
f : P a -> False
H : S n = countPV v
______________________________________(1/2)
P a
______________________________________(2/2)
n = countPV v
我的问题是,我似乎被两个无法证明的子目标所困,而且可用的上下文似乎也没有帮助。任何人都可以为我提供一些继续前进的指导吗?
编辑:
我通过反证 H:
证明了引理
assert (countPV v <= n).
* apply countNotBiggerThanConstructor.
* omega.
Qed.
其中 countNotBiggerThanConstructor 是:
Lemma countNotBiggerThanConstructor: forall {n : nat} (v: vector n), countPV v <= n.
Proof.
intros n v.
induction v.
- reflexivity.
- simpl.
destruct P_dec.
+ apply le_n_S in IHv.
assumption.
+ apply le_S.
assumption.
Qed.
请注意,H 不可能为真。这是一件好事,如果你能证明 False,你就可以证明任何事情。所以接下来我会做 contradict H
(你不需要最后一个 split
)。
总的来说,我觉得你的证明有点乱。我建议考虑如何在纸上证明这个引理并尝试在 Coq 中做到这一点。我不是 Coq 方面的专家,但我认为它也会帮助您意识到,在这种情况下您需要使用矛盾。
(编辑:顺便说一句,暗示这个引理不成立的其他答案是错误的,但我不能以我的 1 声誉发表评论)
我正在尝试证明基于以下定义的引理。
Section lemma.
Variable A : Type.
Variable P : A -> Prop.
Variable P_dec : forall x, {P x}+{~P x}.
Inductive vector : nat -> Type :=
| Vnil : vector O
| Vcons : forall {n}, A -> vector n -> vector (S n).
Arguments Vcons {_} _ _.
Fixpoint countPV {n: nat} (v : vector n): nat :=
match v with
| Vnil => O
| Vcons x v' => if P_dec x then S (countPV v') else countPV v'
end.
我要证明的引理如下
Lemma lem: forall (n:nat) (a:A) (v:vector n),
S n = countPV (Vcons a v) -> (P a /\ n = countPV v).
我已经尝试了很多东西,目前我正处于这一点。
Proof.
intros n a v.
unfold not in P_dec.
simpl.
destruct P_dec.
- intros.
split.
* exact p.
* apply eq_add_S.
exact H.
- intros.
split.
此时上下文:
2 subgoals
A : Type
P : A -> Prop
P_dec : forall x : A, {P x} + {P x -> False}
n : nat
a : A
v : vector n
f : P a -> False
H : S n = countPV v
______________________________________(1/2)
P a
______________________________________(2/2)
n = countPV v
我的问题是,我似乎被两个无法证明的子目标所困,而且可用的上下文似乎也没有帮助。任何人都可以为我提供一些继续前进的指导吗?
编辑:
我通过反证 H:
证明了引理assert (countPV v <= n).
* apply countNotBiggerThanConstructor.
* omega.
Qed.
其中 countNotBiggerThanConstructor 是:
Lemma countNotBiggerThanConstructor: forall {n : nat} (v: vector n), countPV v <= n.
Proof.
intros n v.
induction v.
- reflexivity.
- simpl.
destruct P_dec.
+ apply le_n_S in IHv.
assumption.
+ apply le_S.
assumption.
Qed.
请注意,H 不可能为真。这是一件好事,如果你能证明 False,你就可以证明任何事情。所以接下来我会做 contradict H
(你不需要最后一个 split
)。
总的来说,我觉得你的证明有点乱。我建议考虑如何在纸上证明这个引理并尝试在 Coq 中做到这一点。我不是 Coq 方面的专家,但我认为它也会帮助您意识到,在这种情况下您需要使用矛盾。
(编辑:顺便说一句,暗示这个引理不成立的其他答案是错误的,但我不能以我的 1 声誉发表评论)