New dead code spec and LetRec

[jaccokrijnen]

DeadCode2 needs different rules for LetRec, since its scoping has to be checked in all bindings of the resulting let term.

These rules are problematic for LetRec:

  | dc_delete_binding : ∀ rec b bs t t',

      (* Syntactic approximation of a pure binding *)
      pure_binding [] b ->

      (* Its bound variables do not occur free in the post-term *)
      disjoint (bvb b) (fv t') ->
      disjoint (btvb b) (ftv t') ->

      dc (Let rec       bs  t) t' ->
      dc (Let rec (b :: bs) t) t'

  | dc_keep_binding : ∀ rec b b' bs bs' t t',
      dc t t' ->
      Compat_Binding dc b b' ->
      dc (Let rec       bs  t) (Let rec        bs'  t') ->
      dc (Let rec (b :: bs) t) (Let rec (b' :: bs') t')

Because scoping in letrec is non-linear. For example:

let rec
  x1 = t1 -- x2 appears in t1
  x2 = t2
in t -- x2 does not appear in t

We can construct a wrong post-term using dc_keep_binding and then dc_delete_binding:

let rec
  x1 = t1 -- x2 appears in t1
in t -- x2 does not appear in t

Since x2 still appears in the RHS of x1.

[jaccokrijnen]

Note that the old definition of dead_code did not have this problem, but would require an extra lemma to be proven (that uniqueness and well_scopped imply a property similar to what we require to add in the new version of dead_code). Therefore, it doesn't seem simpler to revert to the old definition.