(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
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)
if b then true else false $\rightarrow$ b
, but with dependent pattern matching and the commuting conversions (my second rule and the other related rules written in "Proofs and Types"), this seems to be equivalent to my first rule. $\endgroup$