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.
- Another way to ask this question is : how to convince the coq that
rest
has typet_rest
(below)? Right now coq 'thinks' thatrest
has typet_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.
- 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?
rest
has typet_rest
? (edited the post too) $\endgroup$