(I'm not sure if I should post this here rather than at Theoretical Computer Science, I've found a lot of type theory related questions on MathOverflow)
I'm working in Martin-Löf type theory with inductive types. Everything I say below for booleans should be understood with the type of booleans replaced by any inductive type, but for simplicity I'll do it in the case of boolean with
match with written as
if then else.
My question is about two reduction rules that I've never seen studied anywhere but that seems rather natural to me. I'd like to know if those rules have an "official" name and where I could read about them.
The first one (that I'm calling "lazy match") has the form
b : bool $\vdash$ if b then u else u $\rightarrow$ u : A
A is a type,
b : bool $\vdash$ u : A and "$\rightarrow$" is reduction (definitional equality, if you prefer).
I know there is a problem with this rule if
b does not terminate, but I'm interested here in type theory as a logical system, so everything is supposed to terminate.
The second one (that I'm calling "deep match") is about exchanging two
match and has the form
b : bool $\vdash$ if (if b then s else t) then u else v $\rightarrow$ if b then (if s then u else v) else (if t then u else v) : A
A is a type,
b : bool $\vdash$ s, t : bool and
b : bool $\vdash$ u, v : A
Intuitively, when you match a match expression, the outer match can be distributed in the branches of the inner match.
Where can I read about these rules? Or are there obvious problems that I haven't seen? (there are perhaps problems with inductive predicates (as opposed to inductive types), but you can restrict it to inductive types)