upd. What I would like to do is to put a = RedNode' .. into current context (when using refine). I found this technique here https://stackoverflow.com/questions/27316254/coq-keeping-information-in-a-match-statement .
This code works:
Inductive color : Set := Red | Black.
Inductive rbtree : color -> nat -> Set :=
| Leaf : rbtree Black 0
| RedNode : forall n, rbtree Black n -> nat -> rbtree Black n -> rbtree Red n
| BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
Inductive rtree : nat -> Set :=
| RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
Definition balance1 n (a : rtree n) (data : nat) c2 (t : rbtree c2 n)
: { c : color & rbtree c (S n) }.
refine(
match a with
| RedNode' _ c0 _ t1 y t2 => fun Heqa => _
end (eq_refl a)).
My question is in next (slightly modified definition) of balance1:
Definition balance1 n (a : rtree n) (data : nat) c2 (t : rbtree c2 n)
: { c : color & rbtree c (S n) }.
refine(
match a as ax in rtreen nx return a = ax -> _ with
| RedNode' _ c0 _ t1 y t2 => fun Heqa => _
end (eq_refl a)).
And now coq does not see that a and ax the same because it is not able to see that n and nx are the same.
What is going on and how to express equality between n and nx (so, coq will see I can have a = ax)?
(an example is taken from CPDT).
