prove preservation of binders-unique

[ivoysey]

to iterate preservation in the intended way, down a series of small steps, you really want to also show that the resultant d' is binders-unique,

  preservation : {Δ : hctx} {d d' : ihexp} {τ : htyp} {Γ : tctx} →
             binders-unique d →
             Δ , Γ ⊢ d :: τ →
             d ↦ d' →
             Δ , Γ ⊢ d' :: τ × binders-unique d'  

this isn't shown now, which is not great but it's as not-great as if it was: we're already asking the reader to have willing suspension of disbelief about alpha conversion to produce the first argument the 0th time they apply preservation to such a derivation, so it's no worse to ask them to do that linearly many times. it's still a little tacky, though.

here are some scraps of proof fragments that work towards that; i'm removing them from the file now in preparation for AE submission but i believe the approach is fundimentally correct. i just haven't worked out the details yet.

  lem-bd-ε1 : ∀{ d ε d0} → d == ε ⟦ d0 ⟧ → binders-unique d → binders-unique d0
  lem-bd-ε1 FHOuter bd = bd
  lem-bd-ε1 (FHAp1 eps) (BUAp bd bd₁ x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHAp2 eps) (BUAp bd bd₁ x) = lem-bd-ε1 eps bd₁
  lem-bd-ε1 (FHNEHole eps) (BUNEHole bd x) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHCast eps) (BUCast bd) = lem-bd-ε1 eps bd
  lem-bd-ε1 (FHFailedCast eps) (BUFailedCast bd) = lem-bd-ε1 eps bd

this is incomplete; need something for the substutitions, per usual

  mutual
    bu-subst : ∀{d1 d2 x} → binders-unique d1 → binders-unique d2 → unbound-in x d1 → binders-unique ([ d2 / x ] d1)
    bu-subst BUHole bu2 ub = BUHole
    bu-subst {x = x} (BUVar {x = y}) bu2 UBVar with natEQ y x
    bu-subst BUVar bu2 UBVar | Inl refl = bu2
    bu-subst BUVar bu2 UBVar | Inr x₂ = BUVar
    bu-subst {x = x} (BULam {x = y}  bu1 x₂) bu2 (UBLam2 x₃ ub) with natEQ y x
    bu-subst (BULam bu1 x₃) bu2 (UBLam2 x₄ ub) | Inl refl = BULam bu1 ub -- can also abort here; odd                                                                                 
    bu-subst (BULam bu1 x₃) bu2 (UBLam2 x₄ ub) | Inr x₂ = BULam (bu-subst bu1 bu2 ub) { }0
    bu-subst (BUEHole x₁) bu2 (UBHole x₂) = BUEHole { }1
    bu-subst (BUNEHole bu1 x₁) bu2 (UBNEHole x₂ ub) = BUNEHole (bu-subst bu1 bu2 ub) { }2
    bu-subst (BUAp bu1 bu2 x₁) bu3 (UBAp ub ub₁) = BUAp (bu-subst bu1 bu3 ub) (bu-subst bu2 bu3 ub₁) { }3
    bu-subst (BUCast bu1) bu2 (UBCast ub) = BUCast (bu-subst bu1 bu2 ub)
    bu-subst (BUFailedCast bu1) bu2 (UBFailedCast ub) = BUFailedCast (bu-subst bu1 bu2 ub)

complete up to the substitution lemma:

  bu-trans : ∀{d0 d0'} → binders-unique d0 → d0 →> d0' → binders-unique d0'
  bu-trans BUHole ()
  bu-trans BUVar ()
  bu-trans (BULam bu x₁) ()
  bu-trans (BUEHole x) ()
  bu-trans (BUNEHole bu x) ()
  bu-trans (BUAp (BULam bu x₁) bu₁ (BDLam x₂ x₃)) ITLam = bu-subst bu bu₁ x₁
  bu-trans (BUAp (BUCast bu) bu₁ (BDCast x)) ITApCast = BUCast (BUAp bu (BUCast bu₁) (lem-bd-into-cast x))
  bu-trans (BUCast bu) ITCastID = bu
  bu-trans (BUCast (BUCast bu)) (ITCastSucceed x) = bu
  bu-trans (BUCast (BUCast bu)) (ITCastFail x x₁ x₂) = BUFailedCast bu
  bu-trans (BUCast bu) (ITGround x) = BUCast (BUCast bu)
  bu-trans (BUCast bu) (ITExpand x) = BUCast (BUCast bu)
  bu-trans (BUFailedCast bu) ()

kind of a different approach, more like what we're doing before. @cyrus- thinks i'll have to invent a judgement relating epsilons as well.

  lem3 : ∀{d1 d2 d3} → d1 →> d3 → binders-disjoint d1 d2 → binders-disjoint d3 d2
  lem3 ITLam (BDAp (BDLam disj x₁) disj₁) = subst-disjoint disj x₁ disj₁
  lem3 ITCastID (BDCast disj) = disj
  lem3 (ITCastSucceed x) (BDCast (BDCast disj)) = disj
  lem3 (ITCastFail x x₁ x₂) (BDCast (BDCast disj)) = BDFailedCast disj
  lem3 ITApCast (BDAp (BDCast disj) disj₁) = BDCast (BDAp disj (BDCast disj₁))
  lem3 (ITGround x) (BDCast disj) = BDCast (BDCast disj)
  lem3 (ITExpand x) (BDCast disj) = BDCast (BDCast disj)

needed in lem3

  subst-disjoint : ∀{d1 d2 d3 x} → binders-disjoint d1 d2 → unbound-in x d2 → binders-disjoint d3 d2 →  binders-disjoint ([ d3 / x ] d1) d2
  subst-disjoint = { }4

i think part of cyrus's approach? i forget

  decomp1 : ∀{d0 d1 d2 ε} → d1 == ε ⟦ d0 ⟧ → binders-disjoint d1 d2 → binders-disjoint d0 d2
  decomp1 = { }0

no idea what this is

  lem2 : ∀{d1 d2 d3} → d1 ↦ d3 → binders-disjoint d1 d2 → binders-disjoint d3 d2
  lem2 (Step FHOuter () FHOuter) BDConst
  lem2 (Step FHOuter () x₃) BDVar
  lem2 (Step FHOuter () x₃) (BDLam disj x₄)
  lem2 (Step FHOuter () FHOuter) (BDHole x₃)
  lem2 (Step FHOuter () FHOuter) (BDNEHole x₃ disj)
  lem2 (Step (FHNEHole x) x₁ (FHNEHole x₂)) (BDNEHole x₃ disj) = BDNEHole x₃ (lem2 (Step x x₁ x₂) disj)
  lem2 (Step FHOuter ITLam FHOuter) (BDAp (BDLam disj x₁) disj₁) = subst-disjoint disj x₁ disj₁
  lem2 (Step FHOuter ITApCast FHOuter) (BDAp (BDCast disj) disj₁) = BDCast (BDAp disj (BDCast disj₁))

  lem2 (Step (FHAp1 x₁) ITLam (FHAp1 x₂)) (BDAp disj disj₁) = BDAp { }1 disj₁

  lem2 (Step (FHAp1 x) ITCastID (FHAp1 x₂)) (BDAp disj disj₁) = { }2
  lem2 (Step (FHAp1 x) (ITCastSucceed x₁) (FHAp1 x₂)) (BDAp disj disj₁) = { }3
  lem2 (Step (FHAp1 x) (ITCastFail x₁ x₂ x₃) (FHAp1 x₄)) (BDAp disj disj₁) = { }4
  lem2 (Step (FHAp1 x) ITApCast (FHAp1 x₂)) (BDAp disj disj₁) = { }5
  lem2 (Step (FHAp1 x) (ITGround x₁) (FHAp1 x₂)) (BDAp disj disj₁) = { }6
  lem2 (Step (FHAp1 x) (ITExpand x₁) (FHAp1 x₂)) (BDAp disj disj₁) = { }7
  lem2 (Step (FHAp2 x) x₁ (FHAp2 x₂)) (BDAp disj disj₁) = { }8
  lem2 step (BDCast disj) = { }9
  lem2 step (BDFailedCast disj) = { }10

the all-in-one approach; gets a bit bogged down in book keeping

  lem' : ∀{d d'} → d ↦ d' → binders-unique d → binders-unique d'
  lem' (Step FHOuter () FHOuter) BUHole
  lem' (Step FHOuter () FHOuter) BUVar
  lem' (Step FHOuter () FHOuter) (BULam bd x₄)
  lem' (Step FHOuter () FHOuter) (BUEHole x₃)

  lem' (Step FHOuter () FHOuter) (BUNEHole bd x₃)
  lem' (Step (FHNEHole x) x₁ (FHNEHole x₂)) (BUNEHole bd x₃) = BUNEHole (lem' (Step x x₁ x₂) bd) x₃

  lem' (Step FHOuter ITLam FHOuter) (BUAp (BULam bd x₁) bd₁ (BDLam x₃ x₂)) = bu-subst bd bd₁ x₁
  lem' (Step FHOuter ITApCast FHOuter) (BUAp (BUCast bd) bd₁ (BDCast x₃)) = BUCast (BUAp bd (BUCast bd₁) {lem-bd-cast }11) -- easy lemma, i think?                                   
  lem' (Step (FHAp1 x) x₁ (FHAp1 x₂)) (BUAp bd bd₁ x₃) = BUAp (lem' (Step x x₁ x₂) bd) bd₁ {Step x x₁ x₂ }12
  lem' (Step (FHAp2 x) x₁ (FHAp2 x₂)) (BUAp bd bd₁ x₃) = BUAp bd (lem' (Step x x₁ x₂) bd₁) {(Step x x₁ x₂) }13

  lem' (Step FHOuter ITCastID FHOuter) (BUCast bd) = bd
  lem' (Step FHOuter (ITCastSucceed x) FHOuter) (BUCast (BUCast bd)) = bd
  lem' (Step FHOuter (ITCastFail x x₁ x₂) FHOuter) (BUCast (BUCast bd)) = BUFailedCast bd
  lem' (Step FHOuter (ITGround x) FHOuter) (BUCast bd) = BUCast (BUCast bd)
  lem' (Step FHOuter (ITExpand x) FHOuter) (BUCast bd) = BUCast (BUCast bd)
  lem' (Step (FHCast x) x₁ (FHCast x₂)) (BUCast bd) = BUCast (lem' (Step x x₁ x₂) bd)

  lem' (Step FHOuter () FHOuter) (BUFailedCast bd)
  lem' (Step (FHFailedCast x) x₁ (FHFailedCast x₂)) (BUFailedCast bd) = BUFailedCast (lem' (Step x x₁ x₂) bd)