Tap

imbrem · Jun 11, 2024 · 69f63f6 · 69f63f6
1 parent e28fa7e
commit 69f63f6
Show file tree

Hide file tree

Showing 8 changed files with 40 additions and 35 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.9.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.8.0-rc2
		leanprover/lean4:v4.9.0-rc1