Let's define two helper types:
Inductive AB : Set := A | B.
Inductive XY : Set := X | Y.
Then two other types that depend on XY
and AB
Inductive Wrapped : AB -> XY -> Set :=
| W : forall (ab : AB) (xy : XY), Wrapped ab xy
| WW : forall (ab : AB), Wrapped ab (match ab with A => X | B => Y end)
.
Inductive Wrapper : XY -> Set :=
WrapW : forall (xy : XY), Wrapped A xy -> Wrapper xy.
Note the WW
constructor – it can only be value of types Wrapped A X
and Wrapped B Y
.
Now I would like to pattern match on Wrapper Y
:
Definition test (wr : Wrapper Y): nat :=
match wr with
| WrapW Y w =>
match w with
| W A Y => 27
end
end.
but I get error
Error: Non exhaustive pattern-matching: no clause found for pattern WW _
Why does it happen? Wrapper
forces contained Wrapped
to be A
version, the type signature forces Y
and WW
constructor forbids being A
and Y
simultaneously. I don't understand why this case is being even considered, while I am forced to check it which seems to be impossible.
How to workaround this situation?
The solution turned out to be simple but tricky:
Definition test (wr : Wrapper Y): nat.
refine (match wr with
| WrapW Y w =>
match w in Wrapped ab xy return ab = A -> xy = Y -> nat with
| W A Y => fun _ _ => 27
| _ => fun _ _ => _
end eq_refl eq_refl
end);
[ | |destruct a]; congruence.
Defined.
The issue was that Coq didn't infer some necessary invariants to realize that WW
case is ridiculous. I had to explicitly give it a proof for it.
In this solution I changed match
to return a function that takes two proofs and brings them to the context of our actual result:
ab
is apparently A
xy
is apparently Y
I have covered real cases ignoring these assumptions, and I deferred "bad" cases to be proven false later which turned to be trivial. I was forced to pass the eq_refl
s manually, but it worked and does not look that bad.