# How to convince Coq this dependent pattern match is exhaustive?

The stack definition and a test function to work with it are given below. The code works (when compiling example you will see an error, it is my problem).

Require Import Coq.Lists.List.
Import List.ListNotations.

Inductive type1 : Set :=
| Unit1 : type1
| Timestamp1 : type1
| Option1 : type1 -> type1.

Inductive type2 : type1 -> Set :=
| Unit2 : type2 Unit1
| Timestamp2 : type2 Timestamp1
| Option2 {t} :
type2 t -> type2 (Option1 t).

Definition stack_t := list type1.

Inductive stack : stack_t -> Set :=
type2 t ->
stack ts ->
stack (t :: ts)
| Empty :
stack [].

Record stacks (s1 : stack_t) : Set := Build {
st1 : stack s1;
}.

Definition test2 {ts_inp} (st_inp : stack ts_inp) : option (stacks ts_inp) :=
match st_inp in stack ts_inp_cp1 with
Timestamp1 ((Timestamp1 :: t_rest) as t_xrest)
Timestamp2 (@Head Timestamp1 t_rest' Timestamp2 rest as xrest) =>
match
xrest
in
stack t_xrest
return
stack (Timestamp1 :: t_rest) -> option (stacks (Timestamp1 :: Timestamp1 :: t_rest))
with
| _ => fun '(Head Timestamp2 rest) => None
end xrest
| _ => None
end.


System complains about Non exhaustive pattern-matching*. So, how to convince coq that this pattern matching is exhaustive?

Some more explanations.

1. Another way to ask this question is : how to convince the coq that rest has type t_rest (below)? Right now coq 'thinks' that rest has type t_rest' as far as I can see from the error message. (Meaning that answer produces most likely the same result for me).
Definition test {ts_inp} (st_inp : stack ts_inp) : option (stacks ts_inp) :=
match st_inp in stack ts_inp_cp1 with
Timestamp1 (Timestamp1 :: t_rest)
Timestamp2 (@Head Timestamp1 t_rest' Timestamp2 rest) =>
| _ => None
end.

1. This particular case can be solved by given an alias to internal stack
Definition test1 {ts_inp} (st_inp : stack ts_inp) : option (stacks ts_inp) :=
match st_inp in stack ts_inp_cp1 with
Timestamp1 (Timestamp1 :: t_rest)
Timestamp2 (@Head Timestamp1 t_rest' Timestamp2 rest as st) =>
Some (Build _ (Head Timestamp2 st))
| _ => None
end.


but this is not the case for me sometimes, unfortunately.

*Btw.. if it is 4:20 of morning here, can we think it is actually rather exhaustive pattern matching?

• Could you please complete the sentence "How to?" It is not clear what you are asking. How to what? Jul 4, 2022 at 8:44
• Thank you. it is: How to convince coq that rest has type t_rest ? (edited the post too) Jul 4, 2022 at 10:41

kind of this works for me

Definition test4 t_st : stack t_st -> option (stacks t_st) :=
match t_st as t_st' return stack t_st' -> option (stacks t_st') with
| Timestamp1 :: (Timestamp1 :: t_rest0 as t_xrest0) =>
fun '(@Head Timestamp1 ((Timestamp1::t_rest) as t_xrest) x xrest) =>
let rest : stack t_rest :=
let '(@Head Timestamp1 t_rest1 y rest2) := xrest in rest2 in