在 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.

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

Proof in Coq with named parameters in constructors

coq