Versiom bump

imbrem · Dec 6, 2024 · beee6e6 · beee6e6
1 parent fa87326
commit beee6e6
Show file tree

Hide file tree

Showing 6 changed files with 70 additions and 66 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Step.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Step.lean
@@ -52,11 +52,11 @@ theorem TStep.wk_res {Γ : Ctx α ε} {L L'} (h : L ≤ L') {r r'}
   | initial di d d' => initial di (d.wk_res h) (d'.wk_res h)
   | terminal de de' => by
     cases L'
-    cases h with
-    | intro l r =>
-      simp only at *
-      cases l
-      exact terminal de de'
+    have l : Ty.LE _ _ := h.1
+    have r := h.2
+    simp only at *
+    cases l
+    exact terminal de de'
 
 theorem TStep.let1_beta_drop {Γ : Ctx α ε} {a b : Term φ} (ha : a.Wf Γ ⟨A, ⊥⟩) (hb : b.Wf Γ V)
   : TStep Γ V (let1 a b.wk0) b

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Uniform.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Uniform.lean
@@ -92,27 +92,31 @@ theorem Wf.Cong.wk_res {P : Ctx α ε → Ty α × ε → Term φ → Term φ
   | pair_left _ hb Ia =>
     cases V' with
     | mk V' e' =>
-    cases hV.1 with
+    have h : Ty.LE _ _ := hV.1
+    cases h with
     | prod hl hr =>
     exact pair_left (Ia ⟨hl, hV.2⟩) (hb.wk_res ⟨hr, hV.2⟩)
   | pair_right ha _ Ia =>
     cases V' with
     | mk V' e' =>
-    cases hV.1 with
+    have h : Ty.LE _ _ := hV.1
+    cases h with
     | prod hl hr =>
     exact pair_right (ha.wk_res ⟨hl, hV.2⟩) (Ia ⟨hr, hV.2⟩)
   | let2_bound _ hb Ia => exact let2_bound (Ia ⟨le_refl _, hV.2⟩) (hb.wk_res hV)
   | let2_body ha _ Ia => exact let2_body (ha.wk_eff hV.2) (Ia hV)
   | inl _ Ia =>
     cases V' with
     | mk V' e' =>
-    cases hV.1 with
+    have h : Ty.LE _ _ := hV.1
+    cases h with
     | coprod hl hr =>
     exact inl (Ia ⟨hl, hV.2⟩)
   | inr _ Ia =>
     cases V' with
     | mk V' e' =>
-    cases hV.1 with
+    have h : Ty.LE _ _ := hV.1
+    cases h with
     | coprod hl hr =>
     exact inr (Ia ⟨hr, hV.2⟩)
   | case_disc _ hb hc Ia => exact case_disc (Ia ⟨le_refl _, hV.2⟩) (hb.wk_res hV) (hc.wk_res hV)

diff --git a/DeBruijnSSA/BinSyntax/Typing/Ty.lean b/DeBruijnSSA/BinSyntax/Typing/Ty.lean
@@ -197,15 +197,15 @@ theorem Ty.LE.eq [d : DiscreteOrder α] {A B : Ty α} : LE A B → A = B
 instance [DiscreteOrder α] : DiscreteOrder (Ty α) where
   le_eq _ _ := Ty.LE.eq
 
-theorem Ty.IsInitial.mono {A B : Ty α} (h : A ≤ B) (hi : IsInitial A) : IsInitial B
+theorem Ty.IsInitial.mono {A B : Ty α} (h : Ty.LE A B) (hi : IsInitial A) : IsInitial B
   := by induction h with
   | prod _ _ Il Ir => cases hi with
     | prod_left hl => exact prod_left (Il hl)
     | prod_right hr => exact prod_right (Ir hr)
   | coprod _ _ Il Ir => cases hi with | coprod hl hr => exact coprod (Il hl) (Ir hr)
   | _ => cases hi <;> constructor
 
-theorem Ty.IsInitial.anti {A B : Ty α} (h : A ≤ B) (hi : IsInitial B) : IsInitial A
+theorem Ty.IsInitial.anti {A B : Ty α} (h : Ty.LE A B) (hi : IsInitial B) : IsInitial A
   := by induction h with
   | prod _ _ Il Ir => cases hi with
     | prod_left hl => exact prod_left (Il hl)

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,52 +1,42 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/imbrem/discretion.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "f46c0445cc86ad2bc973edf8c5b2bd88bd91913b",
-   "name": "batteries",
+   "scope": "",
+   "rev": "1e2e8b40079b3cbe6ce20e17611616ea878747ed",
+   "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
-   "name": "Qq",
+   "scope": "",
+   "rev": "a4bbd290638a8b8ef8896655cf1fa98fba66a337",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
-   "inherited": true,
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
-   "name": "aesop",
+   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
-   "name": "Cli",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -55,51 +45,61 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
+   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
-   "name": "LeanSearchClient",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.48",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/plausible",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
-   "name": "plausible",
+   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "4fafb9f5b76af48f96d2366beee76af2113161f7",
-   "name": "mathlib",
+   "scope": "leanprover-community",
+   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
+   "inputRev": "v4.14.0",
+   "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/imbrem/discretion.git",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "955b94eb753e7952bf657109073b92e26fe5f455",
-   "name": "discretion",
+   "scope": "leanprover-community",
+   "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "DeBruijnSSA",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -10,13 +10,13 @@ package «DeBruijnSSA» where
   -- add any additional package configuration options here
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "master"
 
 require discretion from git
   "https://github.com/imbrem/discretion.git" @ "main"
 
-meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+-- meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
+-- require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
 @[default_target]
 lean_lib «DeBruijnSSA» where

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc3
+leanprover/lean4:v4.15.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.14.0-rc3
		leanprover/lean4:v4.15.0-rc1