CODEWITHSUNDEEP
coq
qbn qsj
qbn qsj

Reputation: 33

Proof in Coq with named parameters in constructors

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].
???

Upvotes: 3

Views: 134

Answers (1)

M Soegtrop
M Soegtrop

Reputation: 1438

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.

Upvotes: 2

Related Questions