Proof in Coq with named parameters in constructors

user_17193393 0
Viewed 49

I'm trying to prove mapCCoption. If you compare the definition of BB to CC, they are the same except in CC the named type parameters are in the constructor. This prevents me from completing the proof because when I destruct an object of type CC option a I lose any information about type 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].
???
coq
1 Answers

In this case you should use inversion instead of destruct:

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.
user_143149440
Related