How to convince Coq this dependent pattern match is exhaustive?

Question

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 :=
| Head {t ts} :
  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
  | @Head
      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
  | @Head
      Timestamp1 (Timestamp1 :: t_rest)
      Timestamp2 (@Head Timestamp1 t_rest' Timestamp2 rest) =>
      Some (Build _ (Head Timestamp2 (Head Timestamp2 rest)))
  | _ => None
  end.

2. 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
  | @Head
      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?

Answer 1

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
        Some (Build _ (Head Timestamp2 (Head Timestamp2 rest)))
  | _ => fun st => None
  end.

thanks to one wise man...