From 0abb937126ab48bfee4e975570dd400be73c5921 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Fri, 27 Sep 2024 21:16:10 +0100 Subject: [PATCH] Left case of distributivity shunt --- .../BinSyntax/Rewrite/Region/Uniform.lean | 6 +-- .../Rewrite/Term/Compose/Distrib.lean | 19 ++++++++- .../Rewrite/Term/Compose/Product.lean | 41 +++++++++++++++++-- DeBruijnSSA/BinSyntax/Syntax.lean | 4 +- .../BinSyntax/Syntax/Compose/Region.lean | 2 +- .../BinSyntax/Syntax/Rewrite/Region/Cong.lean | 2 +- .../Syntax/Rewrite/Region/Directed.lean | 4 +- .../Syntax/Rewrite/Region/Reduce.lean | 4 +- .../Syntax/Rewrite/Region/Rewrite.lean | 2 +- .../BinSyntax/Syntax/Subst/Region.lean | 24 +++++------ .../BinSyntax/Syntax/Subst/Terminator.lean | 6 +-- .../BinSyntax/Typing/Region/LSubst.lean | 2 +- lake-manifest.json | 4 +- 13 files changed, 85 insertions(+), 35 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean index 1de0c73..e01ede9 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean @@ -452,7 +452,7 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ funext i cases i using Fin.elim1 simp only [Subst.liftn_one, ← Subst.vlift_lift_comm, Fin.isValue, Fin.elim1_zero, vwk1_lsubst] - simp [Subst.vlift, <-Function.comp.assoc, vwk2_comp_vwk1] + simp [Subst.vlift, <-Function.comp_assoc, vwk2_comp_vwk1] · simp only [BinSyntax.Region.lsubst, Subst.liftn_one, cfg.injEq, heq_eq_eq, true_and] funext i cases i using Fin.elim1 @@ -511,7 +511,7 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ split · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply, Subst.extend, ↓reduceIte, vsubst0_var0_vwk1, *] - simp [vwk1_lsubst, <-Function.comp.assoc, vwk2_comp_vwk1] + simp [vwk1_lsubst, <-Function.comp_assoc, vwk2_comp_vwk1] · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply, Subst.liftn, add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right, vsubst0_var0_vwk1] @@ -526,7 +526,7 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ split · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply, Subst.fromFCFG, ↓reduceDIte, vsubst0_var0_vwk1, *] - simp [vwk1_lsubst, <-Function.comp.assoc, vwk2_comp_vwk1] + simp [vwk1_lsubst, <-Function.comp_assoc, vwk2_comp_vwk1] · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply, Subst.liftn, add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right, vsubst0_var0_vwk1] simp only [vwk1_lwk] diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean index c2740fb..870a9cc 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean @@ -124,8 +124,23 @@ theorem Eqv.split_rtimes_pi_r_distl_pure {X A B C : Ty α} {Γ : Ctx α ε} (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv) := by apply distl_seq_injective conv => rhs; rw [seq_assoc, distl_distl_inv, nil_seq] - rw [distl, coprod_seq] - sorry + rw [distl, coprod_seq, sum] + congr 1 + · rw [seq_assoc, seq_assoc, dup_pure, split, pair_tensor_pure, pair_rtimes, seq_distl_inv] + conv => + lhs + simp only [← seq_assoc, rtimes_pi_r, let2_pair, nil_seq] + simp only [seq, inj_l, wk1_inl, wk1_nil] + simp [let1_beta_pure, subst0_var0_wk1, wk1_inj_l, coprod, case_inl, seq_inj_l] + apply congrArg + simp [ + split, pair_ltimes_pure, nil_seq, rtimes, tensor, wk1_pair, seq_assoc_inv, reassoc_inv_let2, + reassoc_inv_beta, nil, pi_r, pr + ] + rw [<-Pure.let2_dist_pair (ha := by simp)] + simp [seq, let1_beta_pure, inj_l] + · sorry + -- rw [seq_distl_inv] -- simp [ -- seq_rtimes, split, distl_inv, seq_let2, coprod_seq, sum, wk1_seq, wk1_coprod, diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean index 7fa287e..8bf22d4 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean @@ -326,6 +326,15 @@ theorem Eqv.seq_reassoc_inv {X Y A B C : Ty α} {Γ : Ctx α ε} : a ;;' reassoc_inv b = reassoc_inv (a ;;' b) := by rw [seq, wk1_reassoc_inv, let1_reassoc_inv]; rfl +theorem Eqv.subst_reassoc_inv {A B C : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ} + {a : Eqv φ Δ ⟨A.prod (B.prod C), e⟩} + : (reassoc_inv a).subst σ = reassoc_inv (a.subst σ) := by + induction a using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl + +theorem Eqv.reassoc_inv_subst {A B C : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ} + {a : Eqv φ Δ ⟨A.prod (B.prod C), e⟩} + : reassoc_inv (a.subst σ) = (reassoc_inv a).subst σ := subst_reassoc_inv.symm + def Eqv.pi_l {A B : Ty α} {Γ : Ctx α ε} : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨A, e⟩ := nil.pl @@ -900,14 +909,26 @@ theorem Eqv.Pure.tensor_seq_right {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ : (hr : r.Pure) : tensor l r ;;' tensor l' r' = tensor (l ;;' l') (r ;;' r') := tensor_seq_of_comm (hr.right_central _) -theorem Eqv.tensor_seq_pure {A B B' C C' : Ty α} {Γ : Ctx α ε} - {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B', ⊥⟩} +theorem Eqv.tensor_seq_pure {A A' B B' C C' : Ty α} {Γ : Ctx α ε} + {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨A', ⊥⟩::Γ) ⟨B', ⊥⟩} {l' : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, ⊥⟩} {r' : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C', ⊥⟩} : tensor l r ;;' tensor l' r' = tensor (l ;;' l') (r ;;' r') := Eqv.Pure.tensor_seq_left (by simp) +theorem Eqv.tensor_ltimes_pure {A A' B B' C : Ty α} {Γ : Ctx α ε} + {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {l' : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, ⊥⟩} + {r : Eqv φ (⟨A', ⊥⟩::Γ) ⟨B', ⊥⟩} + : tensor l r ;;' ltimes l' B' = tensor (l ;;' l') r := by + rw [ltimes, tensor_seq_pure, seq_nil] + +theorem Eqv.tensor_rtimes {A A' B B' C : Ty α} {Γ : Ctx α ε} + {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩} + {r : Eqv φ (⟨A', ⊥⟩::Γ) ⟨B', e⟩} {r' : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C, e⟩} + : tensor l r ;;' rtimes B r' = tensor l (r ;;' r') := by + rw [<-ltimes_rtimes, <-seq_assoc, rtimes_rtimes, ltimes_rtimes] + theorem Eqv.Pure.dup {A B : Ty α} {Γ : Ctx α ε} - (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩) : l.Pure → l ;;' split = split ;;' l.tensor l + {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩} : l.Pure → l ;;' split = split ;;' l.tensor l | ⟨l, hl⟩ => by cases hl rw [seq_tensor] @@ -920,6 +941,10 @@ theorem Eqv.Pure.dup {A B : Ty α} {Γ : Ctx α ε} ext k cases k using Fin.cases <;> rfl +theorem Eqv.dup_pure {A B : Ty α} {Γ : Ctx α ε} + {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} : l ;;' split = split ;;' l.tensor l + := Eqv.Pure.dup (by simp) + @[simp] theorem Eqv.wk_eff_split {A : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi} : (split (φ := φ) (Γ := Γ) (A := A) (e := lo)).wk_eff h = split := rfl @@ -1284,3 +1309,13 @@ theorem Eqv.Pure.pair_eta {A B : Ty α} {Γ : Ctx α ε} {p : Eqv φ Γ ⟨A.pro theorem Eqv.pair_eta_pure {A B : Ty α} {Γ : Ctx α ε} {p : Eqv φ Γ ⟨A.prod B, ⊥⟩} : pair p.pl p.pr = p := Eqv.Pure.pair_eta (by simp) + +theorem Eqv.ltimes_pi_l {A B : Ty α} {Γ : Ctx α ε} {l : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩} + : ltimes l C ;;' pi_l = pi_l ;;' l := by + simp [ltimes, tensor, seq_let2, pair_pi_l, pi_l_seq] + +theorem Eqv.rtimes_pi_r {A B : Ty α} {Γ : Ctx α ε} {r : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩} + : rtimes C r ;;' pi_r = pi_r ;;' r := by + simp only [rtimes, tensor, wk1_nil, seq_let2, wk1_pi_r, pi_r_seq] + rw [pair_pi_r] + exact ⟨(var 1 Ctx.Var.shead.step), rfl⟩ diff --git a/DeBruijnSSA/BinSyntax/Syntax.lean b/DeBruijnSSA/BinSyntax/Syntax.lean index 4d39757..d6ef976 100644 --- a/DeBruijnSSA/BinSyntax/Syntax.lean +++ b/DeBruijnSSA/BinSyntax/Syntax.lean @@ -208,8 +208,8 @@ theorem TRegion.coe_toRegion_vsubst (σ : Term.Subst φ) (t : TRegion φ) def BBCFG.toTCFG : BBCFG φ ≃ TCFG φ where toFun := λG => ⟨G.length, TRegion.ofBBRegion ∘ G.targets⟩ invFun := λG => ⟨G.length, TRegion.ofBBRegion.symm ∘ G.targets⟩ - left_inv := λ⟨_, _⟩ => by simp [<-Function.comp.assoc] - right_inv := λ⟨_, _⟩ => by simp [<-Function.comp.assoc] + left_inv := λ⟨_, _⟩ => by simp [<-Function.comp_assoc] + right_inv := λ⟨_, _⟩ => by simp [<-Function.comp_assoc] /-- Convert a terminator CFG to a basic block CFG -/ def TCFG.toBBCFG : TCFG φ ≃ BBCFG φ := BBCFG.toTCFG.symm diff --git a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean index 6cc561e..056ba1e 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean @@ -228,7 +228,7 @@ theorem lsubst_vlift_lift_append {r₀ r₁ : Region φ} {σ : Region.Subst φ} vwk1_lsubst, vsubst_lsubst, Term.wk, Nat.liftWk ] congr - · simp only [<-Function.comp.assoc, vwk1, vwk2, <-vwk_comp] + · simp only [<-Function.comp_assoc, vwk1, vwk2, <-vwk_comp] apply congrFun apply congrArg funext r diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean index e25de62..8396b35 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean @@ -326,7 +326,7 @@ theorem Cong.fv_eq {P : Region φ → Region φ → Sort _} {r r' : Region φ} funext k simp only [<-Function.comp_apply (f := Multiset.liftnFv 1)] simp only [<-Function.comp_apply (g := G)] - rw [Function.comp.assoc] + rw [Function.comp_assoc] rw [Function.update_eq_self] | _ => simp [*] diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean index f73031d..7e5a2ab 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean @@ -205,7 +205,7 @@ def RWD.cast {P} {Γ : ℕ → ε} {r₀ r₀' r₁ r₁' : Region φ} (hr₀ : -- (by -- rw [ -- <-Fin.comp_addCases, --- <-Function.comp.assoc, +-- <-Function.comp_assoc, -- lwk_lwk, comp_lwk, -- Fin.swapAdd -- ] @@ -347,7 +347,7 @@ def RWD.cfg_blocks {P} {Γ : ℕ → ε} (β n) (G G' : Fin n → Region φ) -- (cfg β n G) := -- (cast_trg (swap_cfg (β.lwk (n.liftnWk (· + m))) n (lwk (n.liftnWk (· + m)) ∘ G) m G') -- (by rw [ --- Fin.comp_addCases, lwk_lwk, <-Function.comp.assoc, comp_lwk, +-- Fin.comp_addCases, lwk_lwk, <-Function.comp_assoc, comp_lwk, -- Fin.toNatWk_swapAdd_comp_liftnWk_add] -- )).comp -- (dead_cfg_left β m _ n G) diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean index 396dbe7..109302c 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean @@ -272,13 +272,13 @@ theorem Reduce.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Red -- rw [sup_assoc, sup_comm (r.effect _), <-sup_assoc] -- simp -- | wk_cfg _ _ _ _ _ => --- simp only [effect_cfg, effect_lwk, <-Function.comp.assoc, effect_comp_lwk] +-- simp only [effect_cfg, effect_lwk, <-Function.comp_assoc, effect_comp_lwk] -- apply sup_le_sup_left -- apply Fin.sup_comp_le -- | dead_cfg_left _ _ _ _ => -- simp only [effect_cfg, effect_lwk, Fin.comp_addCases, Fin.sup_addCases] -- apply sup_le_sup_left -- apply le_sup_of_le_right --- rw [<-Function.comp.assoc, effect_comp_lwk] +-- rw [<-Function.comp_assoc, effect_comp_lwk] -- | ucfg β n G => -- simp only [effect_cfg, Region.ucfg, effect_lsubst, Fin.sup_ucfg] diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean index ab01ac2..b416ad3 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean @@ -130,7 +130,7 @@ def RewriteD.cast {r₀ r₀' r₁ r₁' : Region φ} (h₀ : r₀ = r₀') (h -- funext i -- simp [Region.effect_lwk] -- -- | cfg_fuse β n G k ρ hρ => --- -- simp only [effect_cfg, effect_lwk, <-Function.comp.assoc, effect_comp_lwk] +-- -- simp only [effect_cfg, effect_lwk, <-Function.comp_assoc, effect_comp_lwk] -- -- apply congrArg -- -- rw [Fin.sup_comp_surj _ hρ] -- | let1_eta => sorry diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean index 9d1541c..f48139a 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean @@ -308,7 +308,7 @@ theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n) : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by - simp only [vlift, vwk1, <-Function.comp.assoc] + simp only [vlift, vwk1, <-Function.comp_assoc] apply congrArg₂ funext i simp only [Function.comp_apply, vwk_vwk] @@ -378,11 +378,11 @@ theorem Subst.vwk_liftWk_comp_liftn (σ : Subst φ) (ρ) theorem Subst.vwk_liftWk_liftWk_comp_vlift (σ : Subst φ) (ρ) : vwk (Nat.liftWk (Nat.liftWk ρ)) ∘ σ.vlift = vlift (vwk (Nat.liftWk ρ) ∘ σ) := by - simp only [vlift, vwk1, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftWk_comp_succ] + simp only [vlift, vwk1, ← Function.comp_assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftWk_comp_succ] theorem Subst.vwk_liftWk_liftnWk_comp_vliftn (n : ℕ) (σ : Subst φ) (ρ) : vwk (Nat.liftWk (Nat.liftnWk n ρ)) ∘ σ.vliftn n = vliftn n (vwk (Nat.liftWk ρ) ∘ σ) := by - simp only [vliftn, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftnWk_comp_add] + simp only [vliftn, ← Function.comp_assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftnWk_comp_add] theorem vwk_lsubst (σ ρ) (t : Region φ) : (t.lsubst σ).vwk ρ = (t.vwk ρ).lsubst (vwk (Nat.liftWk ρ) ∘ σ) @@ -400,12 +400,12 @@ theorem vwk1_lsubst (σ) (t : Region φ) theorem vwk1_lsubst_vlift (σ : Subst φ) (t : Region φ) : (t.lsubst σ.vlift).vwk1 = t.vwk1.lsubst σ.vlift.vlift - := by simp only [Subst.vlift, vwk1_lsubst, ←Function.comp.assoc, vwk2_comp_vwk1] + := by simp only [Subst.vlift, vwk1_lsubst, ←Function.comp_assoc, vwk2_comp_vwk1] theorem vwk2_lsubst_vlift₂ (σ : Subst φ) (t : Region φ) : (t.lsubst σ.vlift.vlift).vwk2 = t.vwk2.lsubst σ.vlift.vlift.vlift := by - simp only [Subst.vlift, vwk2, vwk_lsubst, vwk1, <-vwk_comp, <-Function.comp.assoc] + simp only [Subst.vlift, vwk2, vwk_lsubst, vwk1, <-vwk_comp, <-Function.comp_assoc] congr apply congrFun apply congrArg @@ -419,16 +419,16 @@ theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ) simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply] generalize τ m = t rw [vwk_lsubst] - simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ] + simp only [<-Function.comp_assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ] theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift := σ.vliftn_comp 1 τ theorem Subst.lwk_comp_vlift (ρ) (σ : Subst φ) : lwk ρ ∘ σ.vlift = vlift (lwk ρ ∘ σ) - := by simp only [vlift, vwk1, <-Function.comp.assoc, vwk_comp_lwk] + := by simp only [vlift, vwk1, <-Function.comp_assoc, vwk_comp_lwk] theorem Subst.lwk_comp_vliftn (ρ) (σ : Subst φ) (n) : lwk ρ ∘ σ.vliftn n = vliftn n (lwk ρ ∘ σ) - := by simp only [vliftn, <-Function.comp.assoc, vwk_comp_lwk] + := by simp only [vliftn, <-Function.comp_assoc, vwk_comp_lwk] theorem Subst.vlift_comp_lwk (σ : Subst φ) (ρ) : vlift (σ ∘ ρ) = σ.vlift ∘ ρ := rfl @@ -469,7 +469,7 @@ theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = ( case isFalse h => rw [lwk_lsubst, lsubst_lwk] congr - rw [lwk_comp_vlift, vlift, vlift, Function.comp.assoc, liftn_comp_add] + rw [lwk_comp_vlift, vlift, vlift, Function.comp_assoc, liftn_comp_add] theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by have h := Subst.liftn_comp 1 σ τ @@ -516,8 +516,8 @@ theorem llsubst_lcomp (σ τ : Subst φ) : llsubst (σ.lcomp τ) = llsubst σ funext k simp only [Function.comp_apply, vwk, Term.wk, Nat.liftWk_zero, let1.injEq, true_and, vwk_vwk] congr - simp only [<-Nat.liftWk_comp, Nat.liftWk_comp_succ, <-Function.comp.assoc] - rw [Function.comp.assoc, Nat.liftWk_comp_succ, Function.comp.assoc] + simp only [<-Nat.liftWk_comp, Nat.liftWk_comp_succ, <-Function.comp_assoc] + rw [Function.comp_assoc, Nat.liftWk_comp_succ, Function.comp_assoc] theorem llsubst_llsubst (σ τ : Subst φ) (t : Region φ) : (t.llsubst τ).llsubst σ = t.llsubst (σ.lcomp τ) @@ -603,7 +603,7 @@ theorem vsubst_lift₃_vwk2 {ρ : Term.Subst φ} {r : Region φ} theorem vsubst_lift_lift_comp_vlift {ρ : Term.Subst φ} {σ : Subst φ} : (vsubst ρ.lift.lift ∘ σ.vlift) = Subst.vlift (vsubst ρ.lift ∘ σ) := by - rw [Subst.vlift, <-Function.comp.assoc, vsubst_lift_lift_comp_vwk1]; rfl + rw [Subst.vlift, <-Function.comp_assoc, vsubst_lift_lift_comp_vwk1]; rfl theorem Subst.vsubst_lift_comp_liftn (σ : Subst φ) (ρ : Term.Subst φ) : vsubst ρ.lift ∘ σ.liftn n = liftn n (vsubst ρ.lift ∘ σ) := by diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean index da5fab7..14d55c8 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean @@ -287,7 +287,7 @@ theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n) : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by - simp only [vlift, vwk1, <-Function.comp.assoc] + simp only [vlift, vwk1, <-Function.comp_assoc] apply congrArg₂ funext i simp only [Function.comp_apply, vwk_vwk] @@ -350,7 +350,7 @@ theorem vwk_lsubst (σ ρ) (t : Terminator φ) | _ => simp only [vwk, lsubst, *] congr <;> simp only [ - Subst.vlift, vwk1, <-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ + Subst.vlift, vwk1, <-Function.comp_assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ ] theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ) @@ -360,7 +360,7 @@ theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ) simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply] generalize τ m = t rw [vwk_lsubst] - simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ] + simp only [<-Function.comp_assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ] theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift := σ.vliftn_comp 1 τ diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean index 8c83f9c..51f5672 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean @@ -672,7 +672,7 @@ theorem Region.InS.vwk1_lsubst_vlift {Γ : Ctx α ε} {L K : LCtx α} simp only [Set.mem_setOf_eq, vwk1, coe_vwk, Ctx.InS.coe_wk1, coe_lsubst, Subst.InS.coe_vlift, Subst.vlift, Region.vwk_lsubst] congr - simp only [<-Function.comp.assoc, Region.vwk1, <-Region.vwk_comp] + simp only [<-Function.comp_assoc, Region.vwk1, <-Region.vwk_comp] apply congrFun apply congrArg apply congrArg diff --git a/lake-manifest.json b/lake-manifest.json index 05d7475..5b9b573 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "418c53780957030e8fd99d2007872a87ad82d9e6", + "rev": "7da2960d5ff6656028a8d2bece5370ad5859b270", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "64879d94466c15f3832a5eb1e85efbdc7956d2da", + "rev": "632e2ca5a9a34f2f541ebfaa91795816fd679370", "name": "discretion", "manifestFile": "lake-manifest.json", "inputRev": "main",