From beee6e63c221884b7ad527830b2dd09897b13a72 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Fri, 6 Dec 2024 18:06:39 +0000 Subject: [PATCH] Versiom bump --- DeBruijnSSA/BinSyntax/Rewrite/Term/Step.lean | 10 +- .../BinSyntax/Rewrite/Term/Uniform.lean | 12 ++- DeBruijnSSA/BinSyntax/Typing/Ty.lean | 4 +- lake-manifest.json | 102 +++++++++--------- lakefile.lean | 6 +- lean-toolchain | 2 +- 6 files changed, 70 insertions(+), 66 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Step.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Step.lean index 4964ca9..e502e0c 100644 --- 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 index 0603e3f..41c323f 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Uniform.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Uniform.lean @@ -92,13 +92,15 @@ 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) @@ -106,13 +108,15 @@ theorem Wf.Cong.wk_res {P : Ctx α ε → Ty α × ε → Term φ → Term φ | 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 index e1d6f6a..2e2e3b4 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Ty.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Ty.lean @@ -197,7 +197,7 @@ 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) @@ -205,7 +205,7 @@ theorem Ty.IsInitial.mono {A B : Ty α} (h : A ≤ B) (hi : IsInitial A) : IsIni | 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 index 5572007..8416946 100644 --- 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 index ad97204..278e334 100644 --- 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 index 6d9e70f..cf25a98 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc3 +leanprover/lean4:v4.15.0-rc1