在Coq中使用构造函数中的命名参数进行证明

Question

我想证明mapCCoption。如果你比较BB和CC的定义，它们是相同的，除了CC的命名类型参数在构造函数中。这阻止了我完成证明，因为当我销毁CC option a类型的对象时，我丢失了关于option类型的任何信息。

Inductive BB (m : Type -> Type) (a : Type) : Type :=
| bb : m a -> BB m a.
Inductive CC : (Type -> Type) -> Type -> Type :=
| cc (m : Type -> Type) (a : Type) : m a -> CC m a.
Theorem mapBBoption (a : Type) (b : Type) (f : a -> b) (x : BB option a) : BB option b.
Proof.
apply bb.
destruct x as [o].
destruct o as [a0|].
- apply (Some (f a0)).
- apply None.
Qed.
Theorem mapCCoption (a : Type) (b : Type) (f : a -> b) (x : CC option a) : CC option b.
Proof.
apply cc.
destruct x as [m1 a1 o].
???

Answer 1

在这种情况下，你应该使用反转而不是析构:

Theorem mapCCoption (a : Type) (b : Type) (f : a -> b) (x : CC option a) : CC option b.
Proof.
apply cc.
inversion x as [m1 a1 o].
inversion o as [a0|].
- apply (Some (f a0)).
- apply None.
Qed.