Consider the following small (typed) language with conditionals :
Inductive const := | BOOL (b : bool) | INT (n : nat). Inductive exp := | CONST (c : const) | IFV (e1 e2 e3 : exp) | ADD (e1 e2 : exp). Inductive ty := | TINT | TBOOL.
The typing judgement is given by:
Inductive hastype : exp -> ty -> Prop := | T_BOOL : forall b, hastype (CONST b) TBOOL | T_INT : forall n, hastype (CONST (INT n)) TINT | T_IFV : forall e1 e2 e3 ty, hastype e1 TBOOL -> hastype e2 ty -> hastype e3 ty -> hastype (IFV e1 e2 e3) ty | T_ADD : forall e1 e2, hastype e1 TINT -> hastype e2 TINT -> hastype (ADD e1 e2) TINT.
Now define a program transformation which consists in lifting the
IFV nodes outside of nested expressions to the top level of the term. We define a type for the target of the transformation:
Inductive uexp := | UCONST (c : const) | UADD (e1 e2 : uexp). Inductive sexp := | SIFV (e1 : bool) (e2 e3 : sexp) | SEXP (e : uexp).
(Note that in this type the condition of
SIFV is always a literal boolean.)
The transformation itself is defined by:
Fixpoint bool_of_exp e := match e with | UCONST (BOOL b) => Some b | _ => None end. Definition dummy := SEXP (UCONST (INT 42)). Fixpoint push (e : exp) (f : uexp -> sexp) : sexp := match e with | CONST c => f (UCONST c) | IFV e1 e2 e3 => push e1 (fun e1 => match bool_of_exp e1 with | Some b => SIFV b (push e2 f) (push e3 f) | None => dummy (* cannot happen if [e] is well typed *) end) | ADD e1 e2 => push e1 (fun e1 => push e2 (fun e2 => f (UADD e1 e2))) end. Definition doit e := push e SEXP.
(if true then 1 else 2) + 5 to
if true then 1 + 5 else 2 + 5 (in obvious notation).
QUESTION: When reasoning about this function, I would like to deduce that the
dummy branch is never taken if the input of the
push is well-typed, but I do not see how to do it (or even how to write it in Coq). I can imagine two possible approaches:
try to give a stronger signature to
pushso that it becomes “type-preserving”, but this would involve passing proofs of well-typedness around and I don’t know how to do that.
Noneused for the “badly-typed” case, but then I am afraid of all the extra book-keeping that will imply in every statement (and proof) involving it.
Does this look reasonable? Should I be looking along these lines or should I try a completely different approach?
Any suggestions or comments would be appreciated!