(I'm not sure if I should post this here rather than at [Theoretical Computer Science](https://cstheory.stackexchange.com/), 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`
> 
> 
> 


where `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` 
> 
> 
> 


where `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)



Reduction rules for inductive types
Your second reduction is called a commutative conversion. You can read about it in Girard, Taylor and Lafont, Proofs and Types, p. 80, for example. The congruence relation with commutative conversions for coproducts is has normal forms, see for instance:


Normalization by evaluation for typed lambda calculus with coproducts,
by T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott


For a strongly normalizing reduction relation for commutative conversions, try:


Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T (1999)
by Felix Joachimski , Ralph Matthes


(EDIT: Three more references. I haven't looked at these, but they sound helpful:)


Exceptional NbE for Sums
by Freiric Barral


P. de Groote. Strong normalization of classical natural deduction with disjunction. In S. Abramsky, editor, Typed
Lambda Calculi and Applications, volume 2044 of Lecture
Notes in Computer Science, pages 182-196. Springer, 2001.


K. Nour and R. David. A short proof of the strong normalization of classical natural deduction with disjunction.
The Journal of Symbolic Logic, 68(4):1277-1288, December
2003.


