Skip to content

Commit

Permalink
Tap
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem committed Jun 25, 2024
1 parent eef79c4 commit ac91c4f
Show file tree
Hide file tree
Showing 2 changed files with 182 additions and 28 deletions.
204 changes: 179 additions & 25 deletions DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,8 @@ inductive WfD.CongD (P : Ctx α ε → LCtx α → Region φ → Region φ → S
β.WfD Γ (R ++ L) →
(hG : ∀i : Fin n, (G i).WfD (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
(i : Fin n) →
CongD P (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L) r r' →
CongD P Γ L (Region.cfg β n (Function.update G i r)) (Region.cfg β n (Function.update G i r'))
CongD P (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L) (G i) g' →
CongD P Γ L (Region.cfg β n G) (Region.cfg β n (Function.update G i g'))

def WfD.CongD.left {P : Ctx α ε → LCtx α → Region φ → Region φ → Sort _} {Γ L r r'}
(toLeft : ∀{Γ L r r'}, P Γ L r r' → r.WfD Γ L) : CongD P Γ L r r' → r.WfD Γ L
Expand All @@ -55,10 +55,8 @@ def WfD.CongD.left {P : Ctx α ε → LCtx α → Region φ → Region φ → So
| cfg_block R hR dβ dG i pr => WfD.cfg _ R hR dβ (λk => by
if h : k = i then
cases h
simp only [Function.update_same]
exact (pr.left toLeft)
else
simp only [ne_eq, h, not_false_eq_true, Function.update_noteq]
exact dG k
)

Expand Down Expand Up @@ -194,10 +192,10 @@ def TStepD.symm {Γ L} {r r' : Region φ} : TStepD Γ L r r' → TStepD Γ L r'
| terminal e e' d => terminal e' e d

inductive TStep : (Γ : Ctx α ε) → (L : LCtx α) → (r r' : Region φ) → Prop
| step {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → StepD Γ.effect r r' → TStep Γ L r r'
| step_op {Γ L r r'} : r.WfD Γ L → r'.WfD Γ L → StepD Γ.effect r' r → TStep Γ L r r'
| initial {Γ L} : Γ.IsInitial → r.WfD Γ L → r'.WfD Γ L → TStep Γ L r r'
| terminal {Γ L} : e.WfD Γ ⟨Ty.unit, ⊥⟩ → e'.WfD Γ ⟨Ty.unit, ⊥⟩ → r.WfD (⟨Ty.unit, ⊥⟩::Γ) L
| step {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → StepD Γ.effect r r' → TStep Γ L r r'
| step_op {Γ L r r'} : r.Wf Γ L → r'.Wf Γ L → StepD Γ.effect r' r → TStep Γ L r r'
| initial {Γ L} : Γ.IsInitial → r.Wf Γ L → r'.Wf Γ L → TStep Γ L r r'
| terminal {Γ L} : e.Wf Γ ⟨Ty.unit, ⊥⟩ → e'.Wf Γ ⟨Ty.unit, ⊥⟩ → r.Wf (⟨Ty.unit, ⊥⟩::Γ) L
→ TStep Γ L (let1 e r) (let1 e' r)

theorem TStep.symm {Γ L} {r r' : Region φ} : TStep Γ L r r' → TStep Γ L r' r
Expand All @@ -206,36 +204,192 @@ theorem TStep.symm {Γ L} {r r' : Region φ} : TStep Γ L r r' → TStep Γ L r'
| initial i d d' => initial i d' d
| terminal e e' d => terminal e' e d

inductive WfD.Cong (P : Ctx α ε → LCtx α → Region φ → Region φ → Prop)
theorem TStep.left {Γ L} {r r' : Region φ} : TStep Γ L r r' → r.Wf Γ L
| TStep.step d _ _ => d
| TStep.step_op d _ _ => d
| TStep.initial _ d _ => d
| TStep.terminal de _ dr => dr.let1 de

theorem TStep.right {Γ L} {r r' : Region φ} : TStep Γ L r r' → r'.Wf Γ L
| TStep.step _ d _ => d
| TStep.step_op _ d _ => d
| TStep.initial _ _ d => d
| TStep.terminal _ de dr => dr.let1 de

inductive Wf.Cong (P : Ctx α ε → LCtx α → Region φ → Region φ → Prop)
: Ctx α ε → LCtx α → Region φ → Region φ → Prop
| step : P Γ L r r' → Cong P Γ L r r'
| case_left : e.WfD Γ ⟨Ty.coprod A B, ⊥⟩ → Cong P (⟨A, ⊥⟩::Γ) L r r' → s.WfD (⟨B, ⊥⟩::Γ) L
| case_left : e.Wf Γ ⟨Ty.coprod A B, ⊥⟩ → Cong P (⟨A, ⊥⟩::Γ) L r r' → s.Wf (⟨B, ⊥⟩::Γ) L
→ Cong P Γ L (Region.case e r s) (Region.case e r' s)
| case_right : e.WfD Γ ⟨Ty.coprod A B, ⊥⟩ → r.WfD (⟨A, ⊥⟩::Γ) L → Cong P (⟨B, ⊥⟩::Γ) L s s'
| case_right : e.Wf Γ ⟨Ty.coprod A B, ⊥⟩ → r.Wf (⟨A, ⊥⟩::Γ) L → Cong P (⟨B, ⊥⟩::Γ) L s s'
→ Cong P Γ L (Region.case e r s) (Region.case e r s')
| let1 : e.WfD Γ ⟨A, e'⟩ → Cong P (⟨A, ⊥⟩::Γ) L r r'
→ Cong P Γ L (Region.let1 e r) (Region.let1 e r')
| let2 : e.WfD Γ ⟨Ty.prod A B, e'⟩ → Cong P (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L r r'
→ Cong P Γ L (Region.let2 e r) (Region.let2 e r')
| let1 : a.Wf Γ ⟨A, e⟩ → Cong P (⟨A, ⊥⟩::Γ) L r r'
→ Cong P Γ L (Region.let1 a r) (Region.let1 a r')
| let2 : a.Wf Γ ⟨Ty.prod A B, e⟩ → Cong P (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L r r'
→ Cong P Γ L (Region.let2 a r) (Region.let2 a r')
| cfg_entry (R : LCtx α) :
(hR : R.length = n) →
Cong P Γ (R ++ L) β β' →
(∀i : Fin n, (G i).WfD (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
(∀i : Fin n, (G i).Wf (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
Cong P Γ L (Region.cfg β n G) (Region.cfg β' n G)
| cfg_block (R : LCtx α) :
(hR : R.length = n) →
β.WfD Γ (R ++ L) →
(hG : ∀i : Fin n, (G i).WfD (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
β.Wf Γ (R ++ L) →
(hG : ∀i : Fin n, (G i).Wf (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
(i : Fin n) →
Cong P (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L) r r' →
Cong P Γ L (Region.cfg β n (Function.update G i r)) (Region.cfg β n (Function.update G i r'))
Cong P (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L) (G i) g' →
Cong P Γ L (Region.cfg β n G) (Region.cfg β n (Function.update G i g'))

theorem Wf.Cong.left {P : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L r r'}
(toLeft : ∀{Γ L r r'}, P Γ L r r' → r.Wf Γ L) : Wf.Cong P Γ L r r' → r.Wf Γ L
| Wf.Cong.step p => toLeft p
| Wf.Cong.case_left de pr ds => case de (pr.left toLeft) ds
| Wf.Cong.case_right de dr ps => case de dr (ps.left toLeft)
| Wf.Cong.let1 de pr => Wf.let1 de (pr.left toLeft)
| Wf.Cong.let2 de pr => Wf.let2 de (pr.left toLeft)
| Wf.Cong.cfg_entry R hR pβ dG => Wf.cfg _ R hR (pβ.left toLeft) dG
| Wf.Cong.cfg_block R hR dβ dG i pr => Wf.cfg _ R hR dβ (λk => by
if h : k = i then
cases h
exact (pr.left toLeft)
else
exact dG k
)

theorem Wf.Cong.right {P : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L r r'}
(toRight : ∀{Γ L r r'}, P Γ L r r' → r'.Wf Γ L) : Wf.Cong P Γ L r r' → r'.Wf Γ L
| Wf.Cong.step p => toRight p
| Wf.Cong.case_left de pr ds => case de (pr.right toRight) ds
| Wf.Cong.case_right de dr ps => case de dr (ps.right toRight)
| Wf.Cong.let1 de pr => Wf.let1 de (pr.right toRight)
| Wf.Cong.let2 de pr => Wf.let2 de (pr.right toRight)
| Wf.Cong.cfg_entry R hR pβ dG => Wf.cfg _ R hR (pβ.right toRight) dG
| Wf.Cong.cfg_block R hR dβ dG i pr => Wf.cfg _ R hR dβ (λk => by
if h : k = i then
cases h
simp only [Function.update_same]
exact (pr.right toRight)
else
simp only [ne_eq, h, not_false_eq_true, Function.update_noteq]
exact dG k
)

theorem Wf.Cong.eqv_iff {P : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L r r'}
(toLeft : ∀{Γ L r r'}, P Γ L r r' → r.Wf Γ L)
(toRight : ∀{Γ L r r'}, P Γ L r r' → r'.Wf Γ L)
(p : EqvGen (Wf.Cong P Γ L) r r') : r.Wf Γ L ↔ r'.Wf Γ L
:= by induction p with
| rel _ _ h => exact ⟨λ_ => h.right toRight, λ_ => h.left toLeft⟩
| refl => rfl
| symm _ _ _ I => exact I.symm
| trans _ _ _ _ _ Il Ir => exact Il.trans Ir

theorem Wf.Cong.case_left_eqv
{P : Ctx α ε → LCtx α → Region φ → Region φ → Prop}
(e : Term φ) (he : e.Wf Γ ⟨Ty.coprod A B, ⊥⟩)
(p : EqvGen (Wf.Cong P (⟨A, ⊥⟩::Γ) L) r r')
(s : Region φ) (hs : s.Wf (⟨B, ⊥⟩::Γ) L)
: EqvGen (Wf.Cong P Γ L) (Region.case e r s) (Region.case e r' s)
:= by induction p with
| rel _ _ h => exact EqvGen.rel _ _ (h.case_left he hs)
| refl _ => exact EqvGen.refl _
| symm _ _ _ I => exact I.symm
| trans _ _ _ _ _ Il Ir => exact Il.trans _ _ _ Ir

theorem Wf.Cong.case_right_eqv
{P : Ctx α ε → LCtx α → Region φ → Region φ → Prop}
(e : Term φ) (he : e.Wf Γ ⟨Ty.coprod A B, ⊥⟩)
(r : Region φ) (hr : r.Wf (⟨A, ⊥⟩::Γ) L)
(p : EqvGen (Wf.Cong P (⟨B, ⊥⟩::Γ) L) s s')
: EqvGen (Wf.Cong P Γ L) (Region.case e r s) (Region.case e r s')
:= by induction p with
| rel _ _ h => exact EqvGen.rel _ _ (h.case_right he hr)
| refl _ => exact EqvGen.refl _
| symm _ _ _ I => exact I.symm
| trans _ _ _ _ _ Il Ir => exact Il.trans _ _ _ Ir

theorem Wf.Cong.let1_eqv
{P : Ctx α ε → LCtx α → Region φ → Region φ → Prop}
(a : Term φ) (ha : a.Wf Γ ⟨A, e⟩)
(p : EqvGen (Wf.Cong P (⟨A, ⊥⟩::Γ) L) r r')
: EqvGen (Wf.Cong P Γ L) (Region.let1 a r) (Region.let1 a r')
:= by induction p with
| rel _ _ h => exact EqvGen.rel _ _ (h.let1 ha)
| refl _ => exact EqvGen.refl _
| symm _ _ _ I => exact I.symm
| trans _ _ _ _ _ Il Ir => exact Il.trans _ _ _ Ir

theorem Wf.Cong.let2_eqv
{P : Ctx α ε → LCtx α → Region φ → Region φ → Prop}
(a : Term φ) (ha : a.Wf Γ ⟨Ty.prod A B, e⟩)
(p : EqvGen (Wf.Cong P (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L) r r')
: EqvGen (Wf.Cong P Γ L) (Region.let2 a r) (Region.let2 a r')
:= by induction p with
| rel _ _ h => exact EqvGen.rel _ _ (h.let2 ha)
| refl _ => exact EqvGen.refl _
| symm _ _ _ I => exact I.symm
| trans _ _ _ _ _ Il Ir => exact Il.trans _ _ _ Ir

theorem Wf.Cong.cfg_entry_eqv
{P : Ctx α ε → LCtx α → Region φ → Region φ → Prop}
(R : LCtx α) (hR : R.length = n)
(p : EqvGen (Wf.Cong P Γ (R ++ L)) β β')
(dG : ∀i : Fin n, (G i).Wf (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L))
: EqvGen (Wf.Cong P Γ L) (Region.cfg β n G) (Region.cfg β' n G)
:= by induction p with
| rel _ _ h => exact EqvGen.rel _ _ (h.cfg_entry R hR dG)
| refl _ => exact EqvGen.refl _
| symm _ _ _ I => exact I.symm
| trans _ _ _ _ _ Il Ir => exact Il.trans _ _ _ Ir

theorem Wf.Cong.cfg_block_eqv
{P : Ctx α ε → LCtx α → Region φ → Region φ → Prop}
(R : LCtx α) (hR : R.length = n)
(β)
(dβ : β.Wf Γ (R ++ L))
(dG : ∀i : Fin n, (G i).Wf (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L))
(i : Fin n)
(p : EqvGen (Wf.Cong P (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) (G i) g')
(toLeft : ∀{Γ L r r'}, P Γ L r r' → r.Wf Γ L)
: EqvGen (Wf.Cong P Γ L) (Region.cfg β n G) (Region.cfg β n (Function.update G i g'))
:= by
generalize hg : G i = g
rw [hg] at p
induction p generalizing G with
| rel _ _ h => sorry--exact EqvGen.rel _ _ (h.cfg_block R hR dβ dG i)
| refl _ =>
rw [<-hg, Function.update_eq_self]
exact EqvGen.refl _
| symm x y hxy I =>
have I := @I (Function.update G i x)
rw [Function.update_idem, <-hg, Function.update_eq_self] at I
apply (I _ (by simp)).symm
intro k
if h : k = i then
cases h
rw [Function.update_same]
sorry
else
rw [Function.update_noteq h]
exact dG k
| trans _ _ _ _ _ Il Ir =>
sorry

def CStep (Γ : Ctx α ε) (L : LCtx α) (r r' : Region φ) : Prop
:= Wf.Cong TStep Γ L r r'

def InS.CStep {Γ : Ctx α ε} {L : LCtx α} (r r' : InS φ Γ L) : Prop
:= Region.CStep Γ L r.val r'.val

instance InS.Setoid (φ) [EffInstSet φ (Ty α) ε] (Γ : Ctx α ε) (L : LCtx α) : Setoid (InS φ Γ L)
:= EqvGen.Setoid InS.CStep

def Eqv (φ)
[EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
(Γ : Ctx α ε) (L : LCtx α)
:= Quot (WfD.Cong (TStep (φ := φ)) Γ L)
theorem InS.let1_congr {Γ : Ctx α ε} {L : LCtx α}
{r r' : InS φ _ L} (a : Term φ) (da : a.Wf Γ ⟨A, e⟩)
(hr : r ≈ r') : InS.let1 a da r ≈ InS.let1 a da r'
:= sorry

-- TODO: Eqv.br, Eqv.case, Eqv.let1, Eqv2.let2, Eqv.cfg ...
def Eqv (φ) [EffInstSet φ (Ty α) ε] (Γ : Ctx α ε) (L : LCtx α) := Quotient (InS.Setoid φ Γ L)

end Region

Expand Down
6 changes: 3 additions & 3 deletions DeBruijnSSA/BinSyntax/Typing.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -728,15 +728,15 @@ def Region.InS.br {Γ : Ctx α ε} {L : LCtx α} (ℓ) (a : Term φ)
(hℓ : L.Trg ℓ A) (ha : a.Wf Γ ⟨A, ⊥⟩) : InS φ Γ L
:= ⟨Region.br ℓ a, Region.Wf.br hℓ ha⟩

def Region.InS.let1 {Γ : Ctx α ε} {L : LCtx α} (a : Term φ) (A e)
def Region.InS.let1 {Γ : Ctx α ε} {L : LCtx α} {A e} (a : Term φ)
(ha : a.Wf Γ ⟨A, e⟩) (t : InS φ (⟨A, ⊥⟩::Γ) L) : InS φ Γ L
:= ⟨Region.let1 a t.1, Region.Wf.let1 ha t.2⟩

def Region.InS.let2 {Γ : Ctx α ε} {L : LCtx α} (a : Term φ) (A B e)
def Region.InS.let2 {Γ : Ctx α ε} {L : LCtx α} {A B e} (a : Term φ)
(ha : a.Wf Γ ⟨(Ty.prod A B), e⟩) (t : InS φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L) : InS φ Γ L
:= ⟨Region.let2 a t.1, Region.Wf.let2 ha t.2⟩

def Region.InS.case {Γ : Ctx α ε} {L : LCtx α} (a : Term φ) (A B e)
def Region.InS.case {Γ : Ctx α ε} {L : LCtx α} {A B e} (a : Term φ)
(ha : a.Wf Γ ⟨Ty.coprod A B, e⟩) (s : InS φ (⟨A, ⊥⟩::Γ) L) (t : InS φ (⟨B, ⊥⟩::Γ) L) : InS φ Γ L
:= ⟨Region.case a s.1 t.1, Region.Wf.case ha s.2 t.2⟩

Expand Down

0 comments on commit ac91c4f

Please sign in to comment.