From 69f63f68f310981f2a292e100a903420054ad6b6 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Tue, 11 Jun 2024 15:27:18 +0100 Subject: [PATCH] Tap --- DeBruijnSSA/BinSyntax/Effect.lean | 12 +++---- DeBruijnSSA/BinSyntax/Syntax.lean | 3 +- DeBruijnSSA/BinSyntax/Syntax/Definitions.lean | 3 +- DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean | 3 +- DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean | 3 +- DeBruijnSSA/BinSyntax/Syntax/Subst.lean | 35 ++++++++++--------- lake-manifest.json | 14 ++++---- lean-toolchain | 2 +- 8 files changed, 40 insertions(+), 35 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Effect.lean b/DeBruijnSSA/BinSyntax/Effect.lean index e5eb378..70998a6 100644 --- a/DeBruijnSSA/BinSyntax/Effect.lean +++ b/DeBruijnSSA/BinSyntax/Effect.lean @@ -155,7 +155,7 @@ theorem BBRegion.effect_mono {Γ : ℕ → ε} {r : BBRegion φ} {Δ : ℕ → apply sup_le_sup (β.effect_mono H) -- TODO: Fin.sup_le_sup not working here for some reason... induction n with - | zero => rfl + | zero => simp | succ n I => rw [Fin.sup_succ, Fin.sup_succ] apply sup_le_sup @@ -171,7 +171,7 @@ theorem BBRegion.control_effect_mono {Γ : ℕ → ε} {r : BBRegion φ} {Δ : apply sup_le_sup (β.control_effect_mono H) -- TODO: Fin.sup_le_sup not working here for some reason... induction n with - | zero => rfl + | zero => simp | succ n I => rw [Fin.sup_succ, Fin.sup_succ] apply sup_le_sup @@ -189,7 +189,7 @@ theorem TRegion.effect_mono {Γ : ℕ → ε} {r : TRegion φ} {Δ : ℕ → ε} apply sup_le_sup (β.effect_mono H) -- TODO: Fin.sup_le_sup not working here for some reason... induction n with - | zero => rfl + | zero => simp | succ n I => rw [Fin.sup_succ, Fin.sup_succ] apply sup_le_sup @@ -207,7 +207,7 @@ theorem TRegion.control_effect_mono {Γ : ℕ → ε} {r : TRegion φ} {Δ : ℕ apply sup_le_sup (β.effect_mono H) -- TODO: Fin.sup_le_sup not working here for some reason... induction n with - | zero => rfl + | zero => simp | succ n I => rw [Fin.sup_succ, Fin.sup_succ] apply sup_le_sup @@ -230,7 +230,7 @@ theorem Region.effect_mono {Γ : ℕ → ε} {r : Region φ} {Δ : ℕ → ε} apply sup_le_sup (Iβ H) -- TODO: Fin.sup_le_sup not working here for some reason... induction n with - | zero => rfl + | zero => simp | succ n I => rw [Fin.sup_succ, Fin.sup_succ] apply sup_le_sup @@ -253,7 +253,7 @@ theorem Region.control_effect_mono {Γ : ℕ → ε} {r : Region φ} {Δ : ℕ apply sup_le_sup (Iβ H) -- TODO: Fin.sup_le_sup not working here for some reason... induction n with - | zero => rfl + | zero => simp | succ n I => rw [Fin.sup_succ, Fin.sup_succ] apply sup_le_sup diff --git a/DeBruijnSSA/BinSyntax/Syntax.lean b/DeBruijnSSA/BinSyntax/Syntax.lean index e7905d8..69f1803 100644 --- a/DeBruijnSSA/BinSyntax/Syntax.lean +++ b/DeBruijnSSA/BinSyntax/Syntax.lean @@ -1,4 +1,5 @@ -import Discretion.Wk.Fun +import Discretion.Wk.Nat +import Discretion.Wk.Fin import DeBruijnSSA.BinSyntax.Syntax.Definitions import DeBruijnSSA.BinSyntax.Syntax.Fv import DeBruijnSSA.BinSyntax.Syntax.Subst diff --git a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean index c8e5aef..1efa8f5 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean @@ -1,4 +1,5 @@ -import Discretion.Wk.Fun +import Discretion.Wk.Nat +import Discretion.Wk.Fin namespace BinSyntax diff --git a/DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean b/DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean index 03c2f4c..ea20756 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Fv/Basic.lean @@ -1,4 +1,5 @@ -import Discretion.Wk.Fun +import Discretion.Wk.Nat +import Discretion.Wk.Fin import Discretion.Wk.Multiset import Discretion.Wk.Multiset import Mathlib.Data.ENat.Basic diff --git a/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean index 90f98e6..ad0f892 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Fv/Subst.lean @@ -1,4 +1,5 @@ -import Discretion.Wk.Fun +import Discretion.Wk.Nat +import Discretion.Wk.Fin import Discretion.Wk.Multiset import Discretion.Wk.Multiset diff --git a/DeBruijnSSA/BinSyntax/Syntax/Subst.lean b/DeBruijnSSA/BinSyntax/Syntax/Subst.lean index e01e99e..2813f93 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Subst.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Subst.lean @@ -1,4 +1,5 @@ -import Discretion.Wk.Fun +import Discretion.Wk.Nat +import Discretion.Wk.Fin import Discretion.Wk.Multiset import Discretion.Wk.Multiset @@ -255,11 +256,11 @@ theorem substn_succ (n : ℕ) (t : Term φ) | succ m => simp only [substn, Nat.add_lt_add_iff_right, add_left_inj, Nat.add_sub_cancel, Subst.lift] split - case inl => rfl - case inr h => + case isTrue => rfl + case isFalse h => split - case inl => rfl - case inr h' => + case isTrue => rfl + case isFalse h' => simp only [wk, Nat.succ_eq_add_one, var.injEq] rw [Nat.sub_add_cancel] exact Nat.succ_le_of_lt $ Nat.lt_of_le_of_lt @@ -285,15 +286,15 @@ theorem subst_substn_wk (e s : Term φ) (ρ) (n) | var k => simp only [wk, substn, subst, Nat.liftnWk] split - case inl h => + case isTrue h => have h' : k < n + 1 := Nat.lt_succ_of_lt h simp only [wk, h, h', Nat.liftnWk, ↓reduceIte] - case inr h => + case isFalse h => split - case inl h => + case isTrue h => cases h simp - case inr h' => + case isFalse h' => have hn : ¬k ≤ n := match Nat.eq_or_lt_of_not_lt h with | Or.inl h => (h' h).elim | Or.inr h => Nat.not_le_of_lt h @@ -344,11 +345,11 @@ theorem wkn_comp_substn_succ (n : ℕ) (e : Term φ) simp only [Subst.comp, subst, substn, Nat.wkn, alpha, Function.update, eq_rec_constant, Subst.id_apply, dite_eq_ite, Nat.lt_succ_iff] split - case inl h => + case isTrue h => split - case inl h' => simp [Nat.ne_of_lt h'] - case inr h' => simp [Nat.le_antisymm h (Nat.le_of_not_lt h')] - case inr h => + case isTrue h' => simp [Nat.ne_of_lt h'] + case isFalse h' => simp [Nat.le_antisymm h (Nat.le_of_not_lt h')] + case isFalse h => have c : ¬(i + 1 < n) := λc => h (Nat.le_of_lt (Nat.lt_trans (by simp) c)) have c' : i + 1 ≠ n := λc => by cases c; simp at h have c'' : i ≠ n := λc => h (Nat.le_of_eq c) @@ -928,8 +929,8 @@ theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = ( funext k simp only [liftn, comp] split - case inl h => simp [liftn, vlift, h] - case inr h => + case isTrue h => simp [liftn, vlift, h] + case isFalse h => simp only [vlift, ←lsubst_fromLwk_apply, lsubst_lsubst] congr funext k @@ -1389,8 +1390,8 @@ theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = ( funext k simp only [liftn, comp] split - case inl h => simp [liftn, vlift, h] - case inr h => + case isTrue h => simp [liftn, vlift, h] + case isFalse h => rw [lwk_lsubst, lsubst_lwk] congr rw [lwk_comp_vlift, vlift, vlift, Function.comp.assoc, liftn_comp_add] diff --git a/lake-manifest.json b/lake-manifest.json index 6c9080c..6651e61 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,10 +1,10 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "7110da53bf6da84198dba69ca90221c4798ade35", + "rev": "6a63eb6a326181df29d95a84ce1f16c1145e66d8", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "d68b34fabd37681e6732be752b7e90aaac7aa0e0", + "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7", + "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "575993746397014166b6c65b0a711187396a46f5", + "rev": "04738f51441b9f795b327b35b723b88ed6a6cabf", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -67,7 +67,7 @@ {"url": "https://github.com/imbrem/discretion.git", "type": "git", "subDir": null, - "rev": "b8584d3b7305075f532f815d58cda65d31a26233", + "rev": "330816f4be18d3d13b7ee436e728b85e41e1b3d9", "name": "discretion", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 78f39e2..0ba3faf 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc2 +leanprover/lean4:v4.9.0-rc1