From c98e3b6ca866cf0c761ee7570fd2decc56d6b6fd Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 1 Oct 2026 16:09:07 +0000 Subject: [PATCH 1/2] chore: Update Lean to v4.34.1 Toolchain and dependencies bumped by lean-update. --- flake.lock | 6 +++--- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/flake.lock b/flake.lock index 90e8790..e769a76 100644 --- a/flake.lock +++ b/flake.lock @@ -24,11 +24,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1787412565, - "narHash": "sha256-M1y7JYDUzvOSYv0DWcCCmkL2DqDfQZePsKDrQf/Or6U=", + "lastModified": 1790785453, + "narHash": "sha256-d25LPK3rcJKXkUC2XfF9jN5SlUCIwyWDffidGDqxn38=", "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "1ecad9d6f99cf3255a858861c9a2e6966cdd0290", + "rev": "e828640c7710bb571eb052d02f1adb2ed5694c5e", "type": "github" }, "original": { diff --git a/lake-manifest.json b/lake-manifest.json index f18b8d0..0d42444 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "lean4lean", diff --git a/lakefile.toml b/lakefile.toml index c0d82fe..d7a4f38 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["Lean4Lean", "lean4lean", "Lean4Lean.Theory", "Lean4Lean.Verif [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.33.0" +rev = "v4.34.0" [[lean_lib]] name = "Lean4Lean" diff --git a/lean-toolchain b/lean-toolchain index a8afa7d..ba8ebf2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.1 +leanprover/lean4:v4.34.1 From 3525d4bbcbfe1864fc5f8f9c8dddedddcdd4321b Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 1 Oct 2026 14:00:17 -0400 Subject: [PATCH 2/2] fix: Build on Lean v4.34.1 `List.idxOf_cons` now unfolds to an `if` rather than a `bif`, so the `cond_eq_ite` rewrite in `List.idxOf_eq_length_iff` no longer finds its pattern; `split` handles the `if` directly. The toolchain deprecates the `if_*`/`dif_*` conditional lemmas in favour of `ite_*`/`dite_*` names, and moves `List.getElem?_inj` under `List.Nodup`. Each replacement has the same explicit arguments, so these are renames. CI builds with `--wfail`, which turns the deprecation warnings into failures. --- Lean4Lean/Experimental/MoreStepIndexed.lean | 4 +- Lean4Lean/Experimental/SExpr.lean | 2 +- Lean4Lean/Experimental/SExprParamsD2.lean | 8 +- Lean4Lean/Experimental/ShapeLogRel.lean | 82 +++++++++---------- .../Experimental/ShapeLogRelAdequacy.lean | 4 +- Lean4Lean/Experimental/Thierry2.lean | 2 +- Lean4Lean/Inductive/Add.lean | 10 +-- Lean4Lean/Inductive/EliminationTrace.lean | 10 +-- Lean4Lean/Inductive/ValidationTrace.lean | 54 ++++++------ Lean4Lean/Std/Basic.lean | 1 - Lean4Lean/Theory/Typing/InductiveLemmas.lean | 18 ++-- Lean4Lean/Theory/Typing/InductivePattern.lean | 4 +- Lean4Lean/Theory/VExpr.lean | 42 +++++----- .../Environment/CandidateIdentityReplay.lean | 4 +- .../Environment/ConstructorValidation.lean | 12 +-- .../ConstructorValidityReplay.lean | 22 ++--- Lean4Lean/Verify/Environment/Extension.lean | 18 ++-- .../Environment/IndexedVecCandidate.lean | 2 +- .../Environment/IndexedVecConsReplay.lean | 24 +++--- .../Environment/IndexedVecConstructors.lean | 10 +-- .../Environment/IndexedVecOuterReplay.lean | 26 +++--- .../Environment/IndexedVecSemanticReplay.lean | 14 ++-- .../Verify/Environment/InductiveFixtures.lean | 70 ++++++++-------- Lean4Lean/Verify/Expr.lean | 40 ++++----- Lean4Lean/Verify/Level.lean | 70 ++++++++-------- Lean4Lean/Verify/LevelStd.lean | 4 +- Lean4Lean/Verify/LocalContext.lean | 2 +- Lean4Lean/Verify/NormLt.lean | 14 ++-- Lean4Lean/Verify/TypeChecker/IsDefEq.lean | 2 +- Lean4Lean/Verify/Typing/Lemmas.lean | 8 +- 30 files changed, 291 insertions(+), 292 deletions(-) diff --git a/Lean4Lean/Experimental/MoreStepIndexed.lean b/Lean4Lean/Experimental/MoreStepIndexed.lean index 14430d0..5212e3f 100644 --- a/Lean4Lean/Experimental/MoreStepIndexed.lean +++ b/Lean4Lean/Experimental/MoreStepIndexed.lean @@ -168,7 +168,7 @@ theorem Shape.lift_self {s : Shape n} : s.lift = s := by have {α} {lift : α → α} (IH : ∀ {s}, lift s = s) {s} : ShapeFun.lift lift s = s := by simp [ShapeFun.lift]; apply List.map_id''; simp [IH] unfold lift <;> split <;> (try rfl) <;> dsimp - -- · rw [dif_pos ‹_›] + -- · rw [dite_eq_left ‹_›] · rw [Shape.lift_self, this Shape.lift_self] · rw [this Shape.lift_self] @@ -198,7 +198,7 @@ theorem Shape.lift_le_lift {s t : Shape n} (le : n ≤ m) : (s.lift : Shape m) ShapeFun.ble ble s t := by simp only [ShapeFun.ble, ShapeFun.lift, List.all_map, List.any_map, Function.comp_def, ih] -- have sif {i} (h : i ≤ n) : (if h : i ≤ m then .sort i h else .bot : Shape (m+1)) = - -- .sort i (Nat.le_trans h le) := dif_pos _ + -- .sort i (Nat.le_trans h le) := dite_eq_left _ cases s <;> cases t <;> simp [ble, lift, *] omit [Params] in diff --git a/Lean4Lean/Experimental/SExpr.lean b/Lean4Lean/Experimental/SExpr.lean index 18adc38..a799f4a 100644 --- a/Lean4Lean/Experimental/SExpr.lean +++ b/Lean4Lean/Experimental/SExpr.lean @@ -69,7 +69,7 @@ theorem mk_of_wf (h : l.WF univs) : have hm : mk l = if h' : l.WF univs then (⟨_, l, h', rfl⟩ : SLevel) else SLevel.zero := rfl rw [hm] - exact dif_pos h + exact dite_eq_left h @[simp] theorem mk_reify (l : SLevel) : mk (reify l) = l := by rw [mk_of_wf (reify_wf l)] diff --git a/Lean4Lean/Experimental/SExprParamsD2.lean b/Lean4Lean/Experimental/SExprParamsD2.lean index 8e97234..6f222cf 100644 --- a/Lean4Lean/Experimental/SExprParamsD2.lean +++ b/Lean4Lean/Experimental/SExprParamsD2.lean @@ -136,9 +136,9 @@ theorem addConst_le_of_le {e₁ e₂ s₁ s₂ : VEnv} {n : Name} {ci : VConstan have h' : (if n = n' then some ci else e₁.constants n') = some a := h show (if n = n' then some ci else e₂.constants n') = some a by_cases hn : n = n' - · rw [if_pos hn] at h' ⊢ + · rw [ite_eq_left hn] at h' ⊢ exact h' - · rw [if_neg hn] at h' ⊢ + · rw [ite_eq_right hn] at h' ⊢ exact hle.constants h' · exact fun h => hle.defeqs h · exact fun h => hle.structEtas h @@ -1024,7 +1024,7 @@ theorem foldlM_addConst_constants_old {α : Type _} (name : α → Name) · cases hx · cases hx show (if name x = c then some (ci x) else _) = _ - rw [if_neg (hne x (.head _))] + rw [ite_eq_right (hne x (.head _))] theorem foldl_addDefEq_constants : ∀ (dfs : List VDefEq) (env : VEnv) (c : Name), @@ -1739,7 +1739,7 @@ theorem d2Imax_pos (univs : Nat) (u v : @SLevel (d2Params univs)) have hw := hv w show 0 < Lean.Nat.imax (u.1 w) (v.1 w) simp only [Lean.Nat.imax] - rw [if_neg (by omega)] + rw [ite_eq_right (by omega)] exact Nat.lt_of_lt_of_le hw (Nat.le_max_right _ _) theorem d2Succ_pos (univs : Nat) (u : @SLevel (d2Params univs)) : diff --git a/Lean4Lean/Experimental/ShapeLogRel.lean b/Lean4Lean/Experimental/ShapeLogRel.lean index 85b2e5f..e11a3fd 100644 --- a/Lean4Lean/Experimental/ShapeLogRel.lean +++ b/Lean4Lean/Experimental/ShapeLogRel.lean @@ -985,7 +985,7 @@ theorem WShape.mk_ctor {n} (l : List (Shape n)) (wf : Shape.WF (n := n+1) (.ctor · simp [ListNonZero]; let ⟨_, h1, h2⟩ := wf.2 h; exact ⟨_, ⟨_, h1, rfl⟩, h2⟩ · simp [WShape.ctor]; congr 1; rw [List.map_pmap, List.pmap_eq_map, List.map_id'] -theorem WShape.ctor_eq_ctor' : ctor c l h = ctor' c l := by rw [ctor', dif_pos] +theorem WShape.ctor_eq_ctor' : ctor c l h = ctor' c l := by rw [ctor', dite_eq_left] def WShapeFun.bot {n : Nat} : WShapeFun n := ⟨.bot, .bot⟩ @@ -1242,7 +1242,7 @@ theorem WShape.lift_eq_lam' {s : WShape (n+1)} (le : n ≤ m) have eq := congrArg (·.1) eq; simp [lift_val (Nat.succ_le_succ le)] at eq unfold lam' at eq; split at eq <;> rename_i h <;> obtain ⟨⟨⟩, wf⟩ := s <;> simp [lam, Shape.lift] at eq <;> cases eq - · refine .inr ⟨⟨_, wf.1⟩, ?_⟩; rw [lam', dif_pos (by exact (ShapeFun.NonZero.lift_iff le).1 h)] + · refine .inr ⟨⟨_, wf.1⟩, ?_⟩; rw [lam', dite_eq_left (by exact (ShapeFun.NonZero.lift_iff le).1 h)] exact ⟨rfl, WShapeFun.ext (WShapeFun.lift_val le ▸ rfl)⟩ · refine .inl ⟨rfl, WShapeFun.LE.def'.2 fun x y h => ?_⟩; rename_i hn refine ⟨_, _, WShapeFun.mem_bot.2 ⟨rfl, rfl⟩, Shape.bot_le, Decidable.by_contra (hn ⟨_, h, ·⟩)⟩ @@ -1256,8 +1256,8 @@ theorem WShape.lift_ctor {c : Name} {l : List (WShape n)} {hc} (le : n ≤ m) : @[simp] theorem WShape.lift_ctor' {c : Name} {l : List (WShape n)} (le : n ≤ m) : (WShape.ctor' c l).lift (m+1) = .ctor' c (l.map (.lift m)) := by ext1; simp [ctor']; split <;> rename_i hc <;> - [rw [dif_pos ((WShape.ListNonZero.lift_iff le).2 ∘ hc)]; - rw [dif_neg (mt ((WShape.ListNonZero.lift_iff le).1 ∘ ·) hc)]] <;> + [rw [dite_eq_left ((WShape.ListNonZero.lift_iff le).2 ∘ hc)]; + rw [dite_eq_right (mt ((WShape.ListNonZero.lift_iff le).1 ∘ ·) hc)]] <;> simp [lift_val (Nat.succ_le_succ le), ctor, Shape.lift] congr 2; ext1 x; simp [lift_val le] @@ -1654,7 +1654,7 @@ theorem WShape.join_val {a b : WShape n} (h : a.Compat b) : (a.join b).1 = a.1.j simp [WShape.join, h] theorem WShape.Join.le (H : WShape.Join x y z) : x ≤ z ∧ y ≤ z := (H _).1 .rfl theorem WShape.Join.mk (h : x.Compat y) : WShape.Join x y (x.join y) := by - simp only [join, dif_pos h]; exact (WShape.join_prop.2 h).2 + simp only [join, dite_eq_left h]; exact (WShape.join_prop.2 h).2 theorem WShape.Join.compat (H : WShape.Join x y z) : x.Compat y := WShape.Compat.iff.2 ⟨z, (H _).1 .rfl⟩ @@ -1668,8 +1668,8 @@ theorem WShape.Join.iff {x y z : WShape n} : theorem WShape.lift_join {x y : WShape n} (le : n ≤ m) : (x.join y).lift m = (x.lift m).join (y.lift m) := by simp [join]; split <;> rename_i h - · rw [dif_pos ((WShape.Compat.lift le).2 h)]; ext1; simp [lift_val le, Shape.lift_join le] - · rw [dif_neg (mt (WShape.Compat.lift le).1 h), lift_bot] + · rw [dite_eq_left ((WShape.Compat.lift le).2 h)]; ext1; simp [lift_val le, Shape.lift_join le] + · rw [dite_eq_right (mt (WShape.Compat.lift le).1 h), lift_bot] theorem WShapeFun.join_mem {f : WShapeFun n} (hx : (x, y) ∈ f) (hy : (x', y') ∈ f) (hc : x.Compat x') : @@ -1722,7 +1722,7 @@ def WShapeFun.join (x y : WShapeFun n) : WShapeFun n := else .bot theorem WShapeFun.join_val {x y : WShapeFun n} (H : Compat x y) : - (x.join y).1 = x.1.join Shape.join y.1 := by simp [join, dif_pos H] + (x.join y).1 = x.1.join Shape.join y.1 := by simp [join, dite_eq_left H] @[simp] theorem WShape.forallE_join_forallE {a a' : WShape n} {f f' : WShapeFun n} (hc1 : a.Compat a') (hc2 : WShapeFun.Compat f f') : @@ -2130,7 +2130,7 @@ theorem WShape.Join.lam' {a b c : WShapeFun n} : unfold WShape.lam'; split <;> rename_i h · simp [← NonZero.not_iff, h, WShape.LE.def, lam, Shape.lam_le] obtain ⟨_, wf⟩ := z; rintro _ h1 ⟨⟩; refine hz ⟨⟨_, wf.1⟩, ?_⟩ - rw [WShape.lam', dif_pos (by exact wf.2)]; rfl + rw [WShape.lam', dite_eq_left (by exact wf.2)]; rfl · simp [NonZero.not_iff.1 h] simp only [this, H _] @@ -2166,19 +2166,19 @@ theorem WShape.ctor'_join {l l' : List (WShape n)} {c : Name} exact ⟨w, .inr hwL, hwnz⟩ ext1; rw [join_val (Compat.ctor'_ctor' h)] unfold WShape.ctor'; split <;> rename_i h1 <;> split <;> rename_i h2 - · rw [dif_pos (key.mpr (.inl h1))]; simp [ctor, Shape.join] + · rw [dite_eq_left (key.mpr (.inl h1))]; simp [ctor, Shape.join] congr 1; clear h1 h2 key induction h with | nil => rfl | @cons x y L L' hh _ ih => simp [WShape.join_val hh, ih] - · rw [dif_pos (key.mpr (.inl h1))]; simp [ctor, bot, Shape.join_bot] + · rw [dite_eq_left (key.mpr (.inl h1))]; simp [ctor, bot, Shape.join_bot] have h2' : ∀ x ∈ l', x.1 ≤ Shape.bot := by simpa [ListNonZero] using fun hNZ => h2 fun _ => hNZ congr 1; clear h1 h2 key induction h with | nil => rfl | @cons x y L L' hh _ ih have hy_bot : y.1 = .bot := Shape.le_bot.1 (h2' y (.head _)) simp [WShape.join_val hh, hy_bot, Shape.join_bot] exact ih (fun z hz => h2' z (.tail _ hz)) - · rw [dif_pos (key.mpr (.inr h2))]; simp [ctor, bot, Shape.bot_join] + · rw [dite_eq_left (key.mpr (.inr h2))]; simp [ctor, bot, Shape.bot_join] have h1' : ∀ x ∈ l, x.1 ≤ Shape.bot := by have ⟨_, hNZ⟩ := Decidable.not_imp_iff_and_not.1 h1 simp [ListNonZero] at hNZ; exact hNZ @@ -2187,7 +2187,7 @@ theorem WShape.ctor'_join {l l' : List (WShape n)} {c : Name} have hx_bot : x.1 = .bot := Shape.le_bot.1 (h1' x (.head _)) simp [WShape.join_val hh, hx_bot, Shape.bot_join] exact ih fun z hz => h1' z (.tail _ hz) - · rw [dif_neg fun hh => (key.mp hh).elim h1 h2]; rfl + · rw [dite_eq_right fun hh => (key.mp hh).elim h1 h2]; rfl theorem WShape.ctor_le : WShape.ctor c l h ≤ s ↔ ∃ l' h', s = WShape.ctor c l' h' ∧ l.Forall₂ (· ≤ ·) l' := by @@ -2207,7 +2207,7 @@ theorem WShape.ctor'_le_ctor' (h : List.Forall₂ (· ≤ ·) l l') : WShape.ctor' c l ≤ WShape.ctor' c l' := by unfold ctor' split <;> rename_i h1 <;> [skip; exact WShape.bot_le] - rw [dif_pos (WShape.ListNonZero.mono h ∘ h1)] + rw [dite_eq_left (WShape.ListNonZero.mono h ∘ h1)] exact Shape.LE.def.2 ⟨rfl, by simpa⟩ theorem TShape.ctor_le_ctor'_nil @@ -2220,7 +2220,7 @@ theorem TShape.ctor_le_ctor'_nil rw [TShape.LE.def (Nat.succ_le_succ le₁) (Nat.succ_le_succ le₂), WShape.lift_ctor le₁, WShape.lift_ctor' le₂] at hle unfold WShape.ctor' at hle - rw [dif_pos (by simpa [IsStruct, hcl])] at hle + rw [dite_eq_left (by simpa [IsStruct, hcl])] at hle rw [WShape.ctor_le] at hle obtain ⟨l', h', heq, hargs⟩ := hle have ⟨hc, hl'⟩ := WShape.ctor.inj.1 heq @@ -2910,7 +2910,7 @@ theorem WShape.HasType.unfold {m a : WShape n} (H : HasType m a) : HasTypeU m a | forallE h => exact .forallE (a := ⟨_, mwf.1⟩) (b := ⟨_, mwf.2⟩) h | lam h => have := HasTypeU.lam (f := ⟨_, mwf.1⟩) (a := ⟨_, awf.1⟩) (b := ⟨_, awf.2⟩) h - rwa [lam', dif_pos (by exact mwf.2)] at this + rwa [lam', dite_eq_left (by exact mwf.2)] at this | ctor => exact (WShape.mk_ctor _ mwf).2 ▸ .ctor | indTy => exact .indTy @@ -3077,7 +3077,7 @@ theorem WShape.HasType.join {m₁ m₂ a : WShape n} (hJ : m₁.Compat m₂) | ctor => (cases h2.unfold with | bot => exact h1 | ctor | _) <;> simp only [Shape.Compat, Bool.and_eq_true, decide_eq_true_eq] at hJ - simp only [Shape.join, if_pos hJ.1]; exact Shape.HasType.unfold_iff.2 .ctor + simp only [Shape.join, ite_eq_left hJ.1]; exact Shape.HasType.unfold_iff.2 .ctor | indTy => (cases h2.unfold with | bot => exact h1 | indTy => rfl | _) <;> simp only [Shape.Compat, Bool.false_eq_true] at hJ @@ -5442,7 +5442,7 @@ theorem WShape.lift_eq_ctor'_of_classify_ctor simp [IsStruct, hcl] have htarget : IsStruct c → WShape.ListNonZero l := fun hs => (hns hs).elim - rw [WShape.ctor', dif_pos htarget] at eq + rw [WShape.ctor', dite_eq_left htarget] at eq cases s using WShape.casesOn' with | bot => simp only [WShape.lift_bot] at eq @@ -5493,7 +5493,7 @@ private theorem LE_Interp.Matches.unlift_aux simp only [List.map_cons, List.cons.injEq] at heq obtain ⟨hhead, htail⟩ := heq obtain ⟨arity, hcl⟩ := ha.head_wf wf.2 - simp only [Bool.false_eq_true, if_false] at hcl + simp only [Bool.false_eq_true, ite_false] at hcl cases n with | zero => have htarget : IsStruct c' → WShape.ListNonZero rargsArg.reverse := by @@ -5505,7 +5505,7 @@ private theorem LE_Interp.Matches.unlift_aux intro h have h' := congrArg (fun x => x.1) h simp [WShape.ctor, WShape.bot, Shape.bot] at h' - rw [WShape.ctor', dif_pos htarget] at hhead + rw [WShape.ctor', dite_eq_left htarget] at hhead cases head0 using WShape.casesOn with | bot => change WShape.ctor c' rargsArg.reverse htarget = @@ -5521,7 +5521,7 @@ private theorem LE_Interp.Matches.unlift_aux exact WShape.LE.T (by rw [hhead]; exact .rfl) have hbad' : (WShape.sort r0 : WShape (nHigh + 1)).T ≤ (WShape.ctor' c' rargsArg.reverse).T := by - rw [WShape.ctor', dif_pos htarget] + rw [WShape.ctor', dite_eq_left htarget] exact hbad exact (TShape.sort_not_le_ctor' (r := r0) (c := c') (l := rargsArg.reverse) hbad').elim @@ -6844,7 +6844,7 @@ theorem LE_Interp.Witness.appNVarsFocused exact (TShape.Join.mk (hargInterp.compat (hcap path))).le.2 · exact TShape.LE.rfl have hcurrent : argShape.T ≤ mcap' path := by - simp only [mcap', if_pos rfl] + simp only [mcap', ite_eq_left rfl] exact (TShape.Join.mk (hargInterp.compat (hcap path))).le.1 refine ⟨mcap', ?_, funShape.T, hfun, ?_⟩ · intro current @@ -6899,7 +6899,7 @@ theorem LE_Interp.subst : LE_Interp ρ m (M.subst σ) ↔ intro ρ m N H M σ eq have bvar {ρ : Valuation} {m N} {σ : Subst} {j} (hσj : σ j = N) (hN : LE_Interp ρ m N) : ∃ ρ', LE_Interp ρ' m (.bvar j) ∧ ∀ i, LE_Interp ρ (ρ' i) (σ i) := by - refine ⟨fun k => if k = j then m else ⟨0, .bot⟩, .bvar (if_pos rfl ▸ .rfl), fun k => ?_⟩ + refine ⟨fun k => if k = j then m else ⟨0, .bot⟩, .bvar (ite_eq_left rfl ▸ .rfl), fun k => ?_⟩ dsimp; split <;> rename_i ek · subst ek; exact hσj ▸ hN · exact .bot @@ -8039,7 +8039,7 @@ theorem LE_Interp.Witness.TypedRDeep.lam intro ⟨xj, yj⟩ hmem hc obtain ⟨z, hz1, hz2⟩ := WShape.Compat.iff.1 hc have sfApp : sf.app z = e'.lift k := by - rw [WShapeFun.single_app, if_pos hz2] + rw [WShapeFun.single_app, ite_eq_left hz2] obtain ⟨hz, _⟩ := hi1Any z exact .mono ((WShapeFun.app_of_mem hmem).2.trans @@ -8054,7 +8054,7 @@ theorem LE_Interp.Witness.TypedRDeep.lam intro ⟨xj, yj⟩ hmem hc obtain ⟨z, hz1, hz2⟩ := WShape.Compat.iff.1 hc have sbApp : sb.app z = b'.lift k := by - rw [WShapeFun.single_app, if_pos hz2] + rw [WShapeFun.single_app, ite_eq_left hz2] obtain ⟨hz, _⟩ := hi2Any z exact .mono ((WShapeFun.app_of_mem hmem).2.trans @@ -8088,12 +8088,12 @@ theorem LE_Interp.Witness.TypedRDeep.lam (ρ.push x.T) (sf.app x).T F, h.RDeepChildren P := by dsimp only [sf] by_cases hmatch : x'.lift k ≤ x - · rw [WShapeFun.single_app, if_pos hmatch] + · rw [WShapeFun.single_app, ite_eq_left hmatch] exact ⟨heK.mono_l (Valuation.LE.push.2 ⟨.rfl, WShape.LE.T hmatch⟩), ceK.mono_l laws.mono_l (Valuation.LE.push.2 ⟨.rfl, WShape.LE.T hmatch⟩)⟩ - · rw [WShapeFun.single_app, if_neg hmatch] + · rw [WShapeFun.single_app, ite_eq_right hmatch] exact ⟨.bot, .bot⟩ obtain ⟨hs, cs⟩ := hs obtain ⟨_, joined⟩ := cz.compat_join laws.toJoinLaws @@ -8113,12 +8113,12 @@ theorem LE_Interp.Witness.TypedRDeep.lam (ρ.push x.T) (sb.app x).T B, h.RDeepChildren P := by dsimp only [sb] by_cases hmatch : x'.lift k ≤ x - · rw [WShapeFun.single_app, if_pos hmatch] + · rw [WShapeFun.single_app, ite_eq_left hmatch] exact ⟨hbK.mono_l (Valuation.LE.push.2 ⟨.rfl, WShape.LE.T hmatch⟩), cbK.mono_l laws.mono_l (Valuation.LE.push.2 ⟨.rfl, WShape.LE.T hmatch⟩)⟩ - · rw [WShapeFun.single_app, if_neg hmatch] + · rw [WShapeFun.single_app, ite_eq_right hmatch] exact ⟨.bot, .bot⟩ obtain ⟨hs, cs⟩ := hs obtain ⟨_, joined⟩ := cz.compat_join laws.toJoinLaws @@ -8380,7 +8380,7 @@ theorem LE_Interp.Witness.TypedRDeep.forallE intro ⟨xj, yj⟩ hmem hc obtain ⟨z, hz1, hz2⟩ := WShape.Compat.iff.1 hc have sfApp : sf.app z = e'.lift k := by - rw [WShapeFun.single_app, if_pos hz2] + rw [WShapeFun.single_app, ite_eq_left hz2] obtain ⟨hz, _⟩ := hi1Any z exact .mono ((WShapeFun.app_of_mem hmem).2.trans @@ -8411,12 +8411,12 @@ theorem LE_Interp.Witness.TypedRDeep.forallE (ρ.push x.T) (sf.app x).T B, h.RDeepChildren P := by dsimp only [sf] by_cases hmatch : x'.lift k ≤ x - · rw [WShapeFun.single_app, if_pos hmatch] + · rw [WShapeFun.single_app, ite_eq_left hmatch] exact ⟨heK.mono_l (Valuation.LE.push.2 ⟨.rfl, WShape.LE.T hmatch⟩), ceK.mono_l laws.mono_l (Valuation.LE.push.2 ⟨.rfl, WShape.LE.T hmatch⟩)⟩ - · rw [WShapeFun.single_app, if_neg hmatch] + · rw [WShapeFun.single_app, ite_eq_right hmatch] exact ⟨.bot, .bot⟩ obtain ⟨hs, cs⟩ := hs obtain ⟨_, joined⟩ := cz.compat_join laws.toJoinLaws @@ -8544,14 +8544,14 @@ theorem LE_Interp.sound_lam have hc : f₁.Compat sf := by rw [WShapeFun.compat_single]; intro ⟨xj, yj⟩ hmem hc have ⟨z, hz1, hz2⟩ := WShape.Compat.iff.1 hc - have sf_app : sf.app z = e'.2.lift k := by rw [WShapeFun.single_app, if_pos hz2] + have sf_app : sf.app z = e'.2.lift k := by rw [WShapeFun.single_app, ite_eq_left hz2] refine .mono ?_ (sf_app ▸ .rfl) <| WShape.Compat.T_iff.2 <| (hi1_any z).compat (sf_app ▸ he'_at_x'.mono_l (Valuation.LE.push.2 ⟨.rfl, hz2.T⟩)) exact (WShapeFun.app_of_mem hmem).2.trans (WShapeFun.app_mono_r hz1) have hcb : b₁.Compat sb := by rw [WShapeFun.compat_single]; intro ⟨xj, yj⟩ hmem hc have ⟨z, hz1, hz2⟩ := WShape.Compat.iff.1 hc - have sb_app : sb.app z = b'.2.lift k := by rw [WShapeFun.single_app, if_pos hz2] + have sb_app : sb.app z = b'.2.lift k := by rw [WShapeFun.single_app, ite_eq_left hz2] refine .mono ?_ (sb_app ▸ .rfl) <| WShape.Compat.T_iff.2 <| (hi2_any z).compat (sb_app ▸ hb'_at_x'.mono_l (Valuation.LE.push.2 ⟨.rfl, hz2.T⟩)) exact (WShapeFun.app_of_mem hmem).2.trans (WShapeFun.app_mono_r hz1) @@ -8663,7 +8663,7 @@ theorem LE_Interp.sound_forallE have hc : f₁.Compat sf := by rw [WShapeFun.compat_single]; intro ⟨xj, yj⟩ hmem hc have ⟨z, hz1, hz2⟩ := WShape.Compat.iff.1 hc - have sf_app : sf.app z = f'x.2.lift k := by rw [WShapeFun.single_app, if_pos hz2] + have sf_app : sf.app z = f'x.2.lift k := by rw [WShapeFun.single_app, ite_eq_left hz2] refine .mono ?_ (sf_app ▸ .rfl) <| WShape.Compat.T_iff.2 <| (hi1_any z).compat (sf_app ▸ he'_at_x'.mono_l (Valuation.LE.push.2 ⟨.rfl, hz2.T⟩)) exact (WShapeFun.app_of_mem hmem).2.trans (WShapeFun.app_mono_r hz1) @@ -8816,7 +8816,7 @@ theorem SoundEq.forallE_inv (H : SoundEq Γ (.forallE A B) (.forallE A' B')) Valuation.LE.push.2 ⟨.rfl, (TShape.lift_eqv hk.1.1).1⟩ · intro x'; simp [WShapeFun.single_app] split <;> [rename_i h; exact ⟨_, WShape.bot_le, .bot' b4'.isType, WShape.bot_le⟩] - refine ⟨_, h, b4', if_pos ?_ ▸ .rfl⟩; exact .rfl + refine ⟨_, h, b4', ite_eq_left ?_ ▸ .rfl⟩; exact .rfl · intro x' h1; simp [WShapeFun.single_app]; split <;> [rename_i h2; exact .bot] refine h.mono (TShape.lift_eqv hk.1.2).1 |>.mono_l <| Valuation.LE.push.2 ⟨.rfl, ?_⟩ exact (TShape.LE.lift_l hk.1.1).2 h2 @@ -8941,7 +8941,7 @@ theorem LE_Interp.apps_realize_inv (W : Valuation.Fits Γ₀ Γ ρ) have h_lt : rest.length < Ts.length := by omega have h_app := ih (k := k + 1) (m := WShape.T (n := _+1) (.forallE .bot (.single .bot m.2))) h_k_rest h_fun_ty ?_ |>.forallE_inv.2 (X := a) .bot - · rw [WShapeFun.single_app, if_pos .rfl] at h_app + · rw [WShapeFun.single_app, ite_eq_left .rfl] at h_app exact (h_T_eq W).1 h_app · rw [List.drop_eq_getElem_cons h_lt, List.foldr_cons] refine .forallE' .bot .bot ?_ ?_ @@ -9677,7 +9677,7 @@ theorem LE_Interp.strongSound (H : IsDefEqStrong Γ M N A) : StrongSoundEq Γ M have := (WShape.HasDom.single (y := m.2.lift k)).2 <| .inl <| (TShape.HasType.def hk.2.1 hk.2.2).1 a4 refine .mono ?_ <| .app' (.lam' (a3.lift hk.2.2) this fun _ hx => ?_) (a2.lift hk.2.1) - · rw [WShape.lam'_app, WShapeFun.single_app, if_pos .rfl]; exact (TShape.lift_eqv hk.1).2 + · rw [WShape.lam'_app, WShapeFun.single_app, ite_eq_left .rfl]; exact (TShape.lift_eqv hk.1).2 · simp [WShapeFun.single_app]; split <;> [rename_i h; exact .bot] refine (h1.lift hk.1).mono_l <| Valuation.LE.push.2 ⟨.rfl, a1.trans ?_⟩ exact (TShape.LE.lift_l hk.2.1).2 h @@ -10224,7 +10224,7 @@ def LR0 : LogRel Γ 0 where (try exact id) <;> [exact fun _ => trivial; cases le] join_ty {A B m₁ m₂} hC hm₁ hm₂ := by obtain ⟨⟨⟩, _⟩ := m₁ <;> obtain ⟨⟨⟩, _⟩ := m₂ <;> - simp [LR0.TyDefEq, WShape.join, Shape.join, dif_pos hC] + simp [LR0.TyDefEq, WShape.join, Shape.join, dite_eq_left hC] simp [WShape.Compat, Shape.Compat] at hC; subst hC; simp intro u h1 h2 _ h3 h4; exact ⟨u, h1, h2⟩ whr {M M' N N' A m a} hM hN := by @@ -12693,7 +12693,7 @@ def LRS (IH : LogRel Γ n) : LogRel Γ (n+1) where have le_g := WShape.lam'_le_lam'.1 le let ⟨A₁, A₂, u, v, rA, hA1, hA2, hA₂, hE, hP⟩ := h exact ⟨A₁, A₂, u, v, rA, hA1, hA2, hA₂, hE, hP.mono_l le_g hm_lam hm'_lam⟩ - · simp only [WShape.lam', dif_neg hg''nz] at hg'' + · simp only [WShape.lam', dite_eq_right hg''nz] at hg'' cases WShape.le_bot.1 (hg'' ▸ le) · cases hgf' | _ => cases hm @@ -13074,7 +13074,7 @@ theorem LR.DefEq.ctor'_inv LRS.CtorDefEq Γ (LR Γ) M N (WShape.ctor' c fields) := by have hwf : IsStruct c → WShape.ListNonZero fields := by simp [IsStruct, hcl] - rw [WShape.ctor', dif_pos hwf] at ht H + rw [WShape.ctor', dite_eq_left hwf] at ht H have ha : a = WShape.indTy := by apply WShape.ext change Shape.hasType (n := n + 1) diff --git a/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean b/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean index f2c1bfe..abba1e5 100644 --- a/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean +++ b/Lean4Lean/Experimental/ShapeLogRelAdequacy.lean @@ -4472,7 +4472,7 @@ theorem LR.constDefEq ih x₀ y₀ hmem hchildLe hchildLeaf hchildTerm ⟨v, hchildType⟩ hchildSpineX hchildSpineY houtK hAK hy - rw [dif_pos hg] + rw [dite_eq_left hg] refine (LRS.DefEq.lam_forallE (M := xs.foldr (fun a f => f.app a) (.const c ls)) (N := ys.foldr (fun a f => f.app a) (.const c ls)) @@ -4491,7 +4491,7 @@ theorem LR.constDefEq evalChild (Nat.max_eq_right (Nat.le_succ q)) hleaf.aligned hterm hspineX hspineY hp hxy hv hmem hx hy⟩) - · rw [dif_neg hg] + · rw [dite_eq_right hg] exact (LR Γ₀).bot hout.isType | ctor => exact (TShape.ctor_not_le_lam' hlam').elim | indTy => exact (TShape.indTy_not_le_lam' hlam').elim diff --git a/Lean4Lean/Experimental/Thierry2.lean b/Lean4Lean/Experimental/Thierry2.lean index 68de65e..e85d071 100644 --- a/Lean4Lean/Experimental/Thierry2.lean +++ b/Lean4Lean/Experimental/Thierry2.lean @@ -302,7 +302,7 @@ theorem Shape.lift_le_lift {s t : Shape n} (le : n ≤ m) : (s.lift : Shape m) ShapeFun.ble ble s t := by simp only [ShapeFun.ble, ShapeFun.lift, List.all_map, List.any_map, Function.comp_def, ih] -- have sif {i} (h : i ≤ n) : (if h : i ≤ m then .sort i h else .bot : Shape (m+1)) = - -- .sort i (Nat.le_trans h le) := dif_pos _ + -- .sort i (Nat.le_trans h le) := dite_eq_left _ cases s <;> cases t <;> simp [ble, lift, *] theorem Shape.lift_mono {s t : Shape n} : s ≤ t → (s.lift : Shape m) ≤ t.lift := by diff --git a/Lean4Lean/Inductive/Add.lean b/Lean4Lean/Inductive/Add.lean index b0971bd..4706fb0 100644 --- a/Lean4Lean/Inductive/Add.lean +++ b/Lean4Lean/Inductive/Add.lean @@ -1130,7 +1130,7 @@ theorem checkInductiveTypes_loop_of_candidate .ok bodyCandidate.rootWhnf at hvalid rw [show fuel = (fuel - 1) + 1 by omega] simp only [rootWhnf, checkInductiveTypes.loopInd.loop, - Nat.lt_irrefl, if_false, withLocalDecl_apply] + Nat.lt_irrefl, ite_false, withLocalDecl_apply] rw [← hmatch] simp only [ReaderT.bind, Bind.bind, liftTypeChecker_apply] rw [hvalid] @@ -1152,7 +1152,7 @@ theorem checkInductiveTypes_loop_of_candidate (TypeChecker.whnf (body.instantiate1 context.freshExpr)) = .ok bodyCandidate.rootWhnf at hvalid rw [show fuel = (fuel - 1) + 1 by omega] - simp only [rootWhnf, checkInductiveTypes.loopInd.loop, hil, if_true, + simp only [rootWhnf, checkInductiveTypes.loopInd.loop, hil, ite_true, hempty, withLocalDecl_apply] rw [← hmatch] simp only [ReaderT.bind, Bind.bind, liftTypeChecker_apply] @@ -1223,7 +1223,7 @@ theorem checkInductiveTypes_singleton_of_candidate ReaderT.bind, Bind.bind, Pure.pure, Except.pure, Except.bind] rw [checkInductiveTypes.loopInd.eq_1] have hsize : 0 < #[indType].size := by simp - rw [dif_pos hsize] + rw [dite_eq_left hsize] rw [show #[indType][0] = indType by rfl] simp only [readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, Pure.pure, Except.pure, Except.bind, @@ -1239,14 +1239,14 @@ theorem checkInductiveTypes_singleton_of_candidate simp only [ReaderT.bind, Bind.bind, liftTypeChecker_apply] rw [hensure] simp only [Except.bind] - rw [if_pos (show ((InductiveStats.initial + rw [ite_eq_left (show ((InductiveStats.initial (List.map Level.param context.lparams)).indConsts).isEmpty = true from rfl)] simp only [Expr.sortLevel!, InductiveStats.initial, Nat.zero_add] simp only [ReaderT.bind, Bind.bind, Except.pure, Except.bind] rw [checkInductiveTypes.loopInd.eq_1] have hdone : ¬1 < #[indType].size := by simp - rw [dif_neg hdone] + rw [dite_eq_right hdone] simp only [readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, Pure.pure, Except.pure, Except.bind] simp [singletonCandidateInductiveStats, hterminalLparams, diff --git a/Lean4Lean/Inductive/EliminationTrace.lean b/Lean4Lean/Inductive/EliminationTrace.lean index b3c1746..c8e51a5 100644 --- a/Lean4Lean/Inductive/EliminationTrace.lean +++ b/Lean4Lean/Inductive/EliminationTrace.lean @@ -104,25 +104,25 @@ theorem run rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply] have notField : ¬ argIdx ≥ stats.params.size := Nat.not_le.mpr isParameter - simp only [notField, if_false, Bind.bind] + simp only [notField, ite_false, Bind.bind] exact ih | proofField context fuel argIdx toCheck name domain body binderInfo sortResult isField ensureStep isProp tail ih => rw [show fuel + 1 = Nat.succ fuel by omega] rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply] - simp only [isField, if_true, ReaderT.bind, Bind.bind, + simp only [isField, ite_true, ReaderT.bind, Bind.bind, liftTypeChecker_apply] rw [ensureStep] - simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true, if_false] + simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true, ite_false] exact ih | dataField context fuel argIdx toCheck name domain body binderInfo sortResult isField ensureStep isProp tail ih => rw [show fuel + 1 = Nat.succ fuel by omega] rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply] - simp only [isField, if_true, ReaderT.bind, Bind.bind, + simp only [isField, ite_true, ReaderT.bind, Bind.bind, liftTypeChecker_apply] rw [ensureStep] - simp only [Except.bind, isProp, Bool.not_false, if_true] + simp only [Except.bind, isProp, Bool.not_false, ite_true] exact ih | terminal context source fuel argIdx toCheck notForall => cases source <;> diff --git a/Lean4Lean/Inductive/ValidationTrace.lean b/Lean4Lean/Inductive/ValidationTrace.lean index d33182d..52f8e2d 100644 --- a/Lean4Lean/Inductive/ValidationTrace.lean +++ b/Lean4Lean/Inductive/ValidationTrace.lean @@ -131,11 +131,11 @@ theorem run rw [whnf] simp only [Except.bind] rw [occurs] - simp only [Bool.not_true, Bool.false_eq_true, if_false, + simp only [Bool.not_true, Bool.false_eq_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] rw [domainFree] - simp only [Bool.false_eq_true, if_false, withLocalDecl_apply] + simp only [Bool.false_eq_true, ite_false, withLocalDecl_apply] exact ih | target context source result fuel targetIdx whnf occurs terminal valid => unfold checkPositivity.loop @@ -143,7 +143,7 @@ theorem run rw [whnf] simp only [Except.bind] rw [occurs] - simp only [Bool.not_true, Bool.false_eq_true, if_false, + simp only [Bool.not_true, Bool.false_eq_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] cases result <;> @@ -174,7 +174,7 @@ theorem exists_of_run | false => exact ⟨.absent context source result fuel hwhnf hocc⟩ | true => rw [hocc] at success - simp only [Bool.not_true, Bool.false_eq_true, if_false, + simp only [Bool.not_true, Bool.false_eq_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success cases result @@ -183,7 +183,7 @@ theorem exists_of_run cases hdomain : hasIndOcc stats.indConsts domain with | false => rw [hdomain] at success - simp only [Bool.false_eq_true, if_false, + simp only [Bool.false_eq_true, ite_false, withLocalDecl_apply] at success obtain ⟨tail⟩ := ih success exact ⟨.forallE context source fuel name domain body @@ -272,7 +272,7 @@ theorem buildExecution_ok_of_run next hoccurs => exact ⟨_, rfl⟩ next hoccurs => rw [hoccurs] at success - simp only [Bool.not_true, Bool.false_eq_true, if_false, + simp only [Bool.not_true, Bool.false_eq_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success cases result <;> simp only [Expr.isForall] <;> simp only at success @@ -347,7 +347,7 @@ theorem run cases trace with | skipped h => simp [h, ReaderT.pure, Pure.pure, Except.pure] | safe h trace => - simp only [h, Bool.not_false, if_true] + simp only [h, Bool.not_false, ite_true] unfold checkPositivity simpa only [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, @@ -386,7 +386,7 @@ theorem exists_of_run stats isUnsafe ctor argIdx context source) := by cases hUnsafe : isUnsafe with | false => - simp only [hUnsafe, Bool.not_false, if_true] at success + simp only [hUnsafe, Bool.not_false, ite_true] at success unfold checkPositivity at success simp only [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, @@ -420,7 +420,7 @@ theorem buildExecution_ok_of_run cases isUnsafe with | true => exact ⟨_, rfl⟩ | false => - simp only [Bool.not_false, if_true] at success + simp only [Bool.not_false, ite_true] at success unfold checkPositivity at success simp only [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, @@ -520,7 +520,7 @@ theorem run rw [parameterTypeRun] simp only [Except.bind, liftTypeChecker_apply] rw [defeq] - simp only [if_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, + simp only [ite_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] exact ih | ordinary context fuel argIdx name domain body binderInfo sortResult noParameter @@ -546,12 +546,12 @@ theorem run cases universeTrace with | structural valid => rw [valid] - simp only [if_true, ReaderT.pure, Pure.pure, + simp only [ite_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] exact restRun | fallback structuralFailed valid => rw [structuralFailed, valid] - simp only [Bool.true_eq_false, Bool.not_true, if_false, + simp only [Bool.true_eq_false, Bool.not_true, ite_false, Bool.false_eq_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] @@ -602,7 +602,7 @@ theorem exists_of_run change Except.error _ = Except.ok () at success contradiction | true => - simp only [if_true, ReaderT.pure, Pure.pure, + simp only [ite_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success obtain ⟨tail⟩ := ih success @@ -636,7 +636,7 @@ theorem exists_of_run (.forallE name domain body binderInfo) argIdx (fuel + 1)) := by cases isUnsafe with | false => - simp only [Bool.not_false, if_true, + simp only [Bool.not_false, ite_true, ReaderT.bind, Bind.bind] at restSuccess cases hpos : checkPositivity stats domain ctor argIdx context with | error err => simp_all [Except.bind] @@ -658,7 +658,7 @@ theorem exists_of_run binderInfo sortResult hparam hensure universeTrace (.safe rfl positivityTrace) tail⟩ | true => - simp only [Bool.not_true, if_false, + simp only [Bool.not_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure, withLocalDecl_apply] at restSuccess @@ -670,13 +670,13 @@ theorem exists_of_run sortResult.sortLevel! with | true => rw [hstruct] at success - simp only [if_true, ReaderT.pure, Pure.pure, + simp only [ite_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success exact finish (.structural hstruct) success | false => rw [hstruct] at success - simp only [Bool.false_eq_true, if_false] at success + simp only [Bool.false_eq_true, ite_false] at success cases hfallback : (stats.resultLevel.isAlwaysZero || stats.resultLevel.geq sortResult.sortLevel!) with @@ -686,7 +686,7 @@ theorem exists_of_run contradiction | true => rw [hfallback] at success - simp only [Bool.true_eq_false, Bool.not_true, if_false, + simp only [Bool.true_eq_false, Bool.not_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success exact finish (.fallback hstruct hfallback) success @@ -817,7 +817,7 @@ theorem buildExecution_ok_of_run contradiction next heq2 => rw [heq2] at success - simp only [Except.bind, if_true, ReaderT.pure, Pure.pure, + simp only [Except.bind, ite_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.pure] at success obtain ⟨tail, htail⟩ := ih success rw [htail] @@ -852,7 +852,7 @@ theorem buildExecution_ok_of_run intro restSuccess cases isUnsafe with | false => - simp only [Bool.not_false, if_true, + simp only [Bool.not_false, ite_true, ReaderT.bind, Bind.bind] at restSuccess cases hpos : checkPositivity stats domain ctor argIdx context with @@ -870,7 +870,7 @@ theorem buildExecution_ok_of_run exact ⟨ConstructorPositivityModeTrace.buildExecution_ok_of_run hpmSuccess, ih restSuccess⟩ | true => - simp only [Bool.not_true, if_false, + simp only [Bool.not_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure, withLocalDecl_apply] at restSuccess @@ -884,14 +884,14 @@ theorem buildExecution_ok_of_run split next hstruct => rw [hstruct] at success - simp only [if_true, ReaderT.pure, Pure.pure, + simp only [ite_true, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success obtain ⟨⟨positivity, hpm⟩, tail, htail⟩ := finish success rw [hpm, htail] exact ⟨_, rfl⟩ next hstruct => rw [hstruct] at success - simp only [Bool.false_eq_true, if_false] at success + simp only [Bool.false_eq_true, ite_false] at success split next hfallback => rw [hfallback] at success @@ -899,7 +899,7 @@ theorem buildExecution_ok_of_run contradiction next hfallback => rw [hfallback] at success - simp only [Bool.true_eq_false, Bool.not_true, if_false, + simp only [Bool.true_eq_false, Bool.not_true, ite_false, ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, Except.bind, Except.pure] at success obtain ⟨⟨positivity, hpm⟩, tail, htail⟩ := finish success @@ -1157,7 +1157,7 @@ theorem fold_run unfold checkConstructorFold simp only rw [fresh] - simp only [Bool.false_eq_true, if_false, + simp only [Bool.false_eq_true, ite_false, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, Except.bind, Except.pure] rw [closed] @@ -1193,7 +1193,7 @@ theorem exists_of_fold_run contradiction | false => rw [hfresh] at success - simp only [Bool.false_eq_true, if_false, + simp only [Bool.false_eq_true, ite_false, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, Except.bind, Except.pure] at success cases hclosed : context.env.checkNoMVarNoFVar @@ -1261,7 +1261,7 @@ theorem buildExecution_ok_of_fold_run contradiction next hfresh => rw [hfresh] at success - simp only [Bool.false_eq_true, if_false, + simp only [Bool.false_eq_true, ite_false, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, Except.bind, Except.pure] at success split diff --git a/Lean4Lean/Std/Basic.lean b/Lean4Lean/Std/Basic.lean index fcbd96c..b9fd513 100644 --- a/Lean4Lean/Std/Basic.lean +++ b/Lean4Lean/Std/Basic.lean @@ -151,7 +151,6 @@ theorem List.idxOf_eq_length_iff [BEq α] [LawfulBEq α] | nil => exact iff_of_true rfl not_mem_nil | cons b l ih => simp only [length, mem_cons, idxOf_cons] - rw [cond_eq_ite] split <;> rename_i h <;> simp at h · exact iff_of_false (by rintro ⟨⟩) fun H => H <| Or.inl h.symm · simp only [Ne.symm h, false_or] diff --git a/Lean4Lean/Theory/Typing/InductiveLemmas.lean b/Lean4Lean/Theory/Typing/InductiveLemmas.lean index 58db9cb..7ee21a6 100644 --- a/Lean4Lean/Theory/Typing/InductiveLemmas.lean +++ b/Lean4Lean/Theory/Typing/InductiveLemmas.lean @@ -116,7 +116,7 @@ theorem inst_liftN1 : ∀ (e a : VExpr) (k : Nat), (e.liftN 1 k).inst a k = e := split · rfl · next h => - rw [if_neg (by omega), if_neg (by omega)] + rw [ite_eq_right (by omega), ite_eq_right (by omega)] congr 1; omega | sort | const => rfl | app f b ihf ihb => simp [liftN, inst, ihf, ihb] @@ -353,7 +353,7 @@ theorem instRev_bvar_ge : ∀ (es : List VExpr) {i : Nat}, es.length ≤ i → rw [show (VExpr.bvar i).inst e es.length = .bvar (i-1) from by show VExpr.instVar i e es.length = _ unfold VExpr.instVar - rw [if_neg (by omega), if_neg (by omega)], + rw [ite_eq_right (by omega), ite_eq_right (by omega)], instRev_bvar_ge es (by omega)] congr 1 simp only [List.length_cons] @@ -376,7 +376,7 @@ theorem instRev_bvar_lt_cons (es : List VExpr) (e : VExpr) {i : Nat} (hi : i < e congr 1 show VExpr.instVar i e es.length = .bvar i unfold VExpr.instVar - rw [if_pos hi] + rw [ite_eq_left hi] theorem mem_bvarRevRange : ∀ {m off : Nat} {x : VExpr}, x ∈ bvarRevRange off m → ∃ i, x = .bvar i ∧ off ≤ i ∧ i < off + m @@ -399,7 +399,7 @@ theorem map_instRev_bvarRevRange : ∀ (es : List VExpr), show (VExpr.bvar es.length).inst e es.length = e.liftN es.length from by show VExpr.instVar es.length e es.length = _ unfold VExpr.instVar - rw [if_neg (Nat.lt_irrefl _), if_pos rfl]] + rw [ite_eq_right (Nat.lt_irrefl _), ite_eq_left rfl]] exact instRev_liftN_len es e · rw [List.map_congr_left fun x hx => ?_, map_instRev_bvarRevRange es] obtain ⟨i, rfl, -, h2⟩ := mem_bvarRevRange hx @@ -1582,17 +1582,17 @@ theorem _root_.Lean4Lean.VExpr.liftN_succ_inst_bvar (e : VExpr) : show VExpr.instVar (liftVar (s+1) j (k+1)) (.bvar s) k = .bvar (liftVar s j k) unfold liftVar rcases Nat.lt_trichotomy j k with h | rfl | h - · rw [if_pos (Nat.lt_succ_of_lt h), if_pos h] + · rw [ite_eq_left (Nat.lt_succ_of_lt h), ite_eq_left h] simp [VExpr.instVar, h] - · rw [if_pos (Nat.lt_succ_self _), if_neg (Nat.lt_irrefl _)] + · rw [ite_eq_left (Nat.lt_succ_self _), ite_eq_right (Nat.lt_irrefl _)] show VExpr.instVar j (.bvar s) j = _ rw [show VExpr.instVar j (.bvar s) j = (VExpr.bvar s).liftN j from by - unfold VExpr.instVar; rw [if_neg (Nat.lt_irrefl _), if_pos rfl]] + unfold VExpr.instVar; rw [ite_eq_right (Nat.lt_irrefl _), ite_eq_left rfl]] show VExpr.bvar (liftVar j s) = _ rw [liftVar_base, Nat.add_comm] - · rw [if_neg (by omega), if_neg (by omega)] + · rw [ite_eq_right (by omega), ite_eq_right (by omega)] simp only [VExpr.instVar] - rw [if_neg (by omega), if_neg (by omega)] + rw [ite_eq_right (by omega), ite_eq_right (by omega)] congr 1; omega | sort | const => intros; rfl | app f a ihf iha => simp [VExpr.liftN, VExpr.inst, ihf, iha] diff --git a/Lean4Lean/Theory/Typing/InductivePattern.lean b/Lean4Lean/Theory/Typing/InductivePattern.lean index d1c3d28..145d811 100644 --- a/Lean4Lean/Theory/Typing/InductivePattern.lean +++ b/Lean4Lean/Theory/Typing/InductivePattern.lean @@ -450,7 +450,7 @@ theorem families_name_inj {t t' : Nat} {family family' : NormalizedFamily} have hm' : (source.types.map (·.name))[t']? = some family.raw.name := by rw [List.getElem?_map, h1', Option.map_some, hname] obtain ⟨hlt, -⟩ := List.getElem?_eq_some_iff.1 hm - exact (List.getElem?_inj hlt gen.nodup_parts.1).1 (hm.trans hm'.symm) + exact (List.Nodup.getElem?_inj hlt gen.nodup_parts.1).1 (hm.trans hm'.symm) /-- Flattened positions are recoverable from raw constructor names. -/ theorem flatCtors_name_inj {i i' : Nat} {c c' : NormalizedBlockCtor} @@ -469,7 +469,7 @@ theorem flatCtors_name_inj {i i' : Nat} {c c' : NormalizedBlockCtor} hname] rfl obtain ⟨hlt, -⟩ := List.getElem?_eq_some_iff.1 hm - have hii : i = i' := (List.getElem?_inj hlt hnodup).1 (hm.trans hm'.symm) + have hii : i = i' := (List.Nodup.getElem?_inj hlt hnodup).1 (hm.trans hm'.symm) subst hii exact ⟨rfl, Option.some.inj (h.symm.trans h')⟩ diff --git a/Lean4Lean/Theory/VExpr.lean b/Lean4Lean/Theory/VExpr.lean index 7abacc8..5667595 100644 --- a/Lean4Lean/Theory/VExpr.lean +++ b/Lean4Lean/Theory/VExpr.lean @@ -16,8 +16,8 @@ instance : Inhabited VExpr := ⟨.sort .zero⟩ def liftVar (n i : Nat) (k := 0) : Nat := if i < k then i else n + i -theorem liftVar_lt (h : i < k) : liftVar n i k = i := if_pos h -theorem liftVar_le (h : k ≤ i) : liftVar n i k = n + i := if_neg (Nat.not_lt.2 h) +theorem liftVar_lt (h : i < k) : liftVar n i k = i := ite_eq_left h +theorem liftVar_le (h : k ≤ i) : liftVar n i k = n + i := ite_eq_right (Nat.not_lt.2 h) theorem liftVar_base : liftVar n i = n + i := liftVar_le (Nat.zero_le _) @[simp] theorem liftVar_base' : liftVar n i = i + n := Nat.add_comm .. ▸ liftVar_le (Nat.zero_le _) @@ -58,8 +58,8 @@ theorem liftN'_liftN' {e : VExpr} {n1 n2 k1 k2 : Nat} (h1 : k1 ≤ k2) (h2 : k2 induction e generalizing k1 k2 with simp [liftN, liftVar, Nat.add_assoc, *] | bvar i => split <;> rename_i h - · rw [if_pos (Nat.lt_of_lt_of_le h h1)] - · rw [if_neg (mt (fun h => ?_) h), Nat.add_left_comm] + · rw [ite_eq_left (Nat.lt_of_lt_of_le h h1)] + · rw [ite_eq_right (mt (fun h => ?_) h), Nat.add_left_comm] exact (Nat.add_lt_add_iff_left ..).1 (Nat.lt_of_lt_of_le h h2) | lam _ _ _ IH2 | forallE _ _ _ IH2 => rw [IH2 (Nat.succ_le_succ h1) (Nat.succ_le_succ h2)] @@ -83,12 +83,12 @@ theorem liftN'_comm (e : VExpr) (n1 n2 k1 k2 : Nat) (h : k2 ≤ k1) : simp [liftN, liftVar, Nat.add_assoc, Nat.succ_le_succ, *] | bvar i => split <;> rename_i h' - · rw [if_pos (c := _ < n2 + k1)]; split + · rw [ite_eq_left (c := _ < n2 + k1)]; split · exact Nat.lt_add_left _ h' · exact Nat.add_lt_add_left h' _ · have := mt (Nat.lt_of_lt_of_le · h) h' - rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_add_left _ n1)) this), - if_neg this, if_neg (mt (Nat.add_lt_add_iff_left ..).1 h'), Nat.add_left_comm] + rw [ite_eq_right (mt (Nat.lt_of_le_of_lt (Nat.le_add_left _ n1)) this), + ite_eq_right this, ite_eq_right (mt (Nat.add_lt_add_iff_left ..).1 h'), Nat.add_left_comm] theorem lift_liftN' (e : VExpr) (k : Nat) : lift (liftN n e k) = liftN n (lift e) (k+1) := Nat.add_comm .. ▸ liftN'_comm (h := Nat.zero_le _) .. @@ -204,19 +204,19 @@ def instVar (i : Nat) (e : VExpr) (k := 0) : VExpr := theorem liftN_instVar_lo (n : Nat) (e : VExpr) (j k : Nat) (hj : k ≤ j) : liftN n (instVar i e j) k = instVar (liftVar n i k) e (n+j) := by simp [instVar]; split <;> rename_i h - · rw [if_pos]; · rfl + · rw [ite_eq_left]; · rfl simp only [liftVar]; split <;> rename_i hk · exact Nat.lt_add_left _ h · exact Nat.add_lt_add_left h _ split <;> rename_i h' · subst i rw [liftN'_liftN' (h1 := Nat.zero_le _) (h2 := hj), liftVar_le hj, - if_neg (by simp), if_pos rfl, Nat.add_comm] + ite_eq_right (by simp), ite_eq_left rfl, Nat.add_comm] · rw [Nat.not_lt] at h; rw [liftVar_le (Nat.le_trans hj h)] have hk := Nat.lt_of_le_of_ne h (Ne.symm h') let i+1 := i have := Nat.add_lt_add_left hk n - rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)] + rw [ite_eq_right (Nat.lt_asymm this), ite_eq_right (Nat.ne_of_gt this)] simp only [liftN] rw [liftVar_le (Nat.le_trans hj <| by exact Nat.le_of_lt_succ hk)]; rfl @@ -224,7 +224,7 @@ theorem liftN_instVar_hi (i : Nat) (e2 : VExpr) (n k j : Nat) : liftN n (instVar i e2 j) (k+j) = instVar (liftVar n i (k+j+1)) (liftN n e2 k) j := by simp [instVar]; split <;> rename_i h · have := Nat.lt_add_left k h - rw [liftVar_lt <| Nat.lt_succ_of_lt this, if_pos h] + rw [liftVar_lt <| Nat.lt_succ_of_lt this, ite_eq_left h] simp [liftN, liftVar_lt this] split <;> rename_i h' · subst i @@ -236,7 +236,7 @@ theorem liftN_instVar_hi (i : Nat) (e2 : VExpr) (n k j : Nat) : simp [liftVar, Nat.succ_lt_succ_iff]; split <;> rename_i hi · simp [liftN, liftVar_lt hi] · have := Nat.lt_add_left n hk - rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)] + rw [ite_eq_right (Nat.lt_asymm this), ite_eq_right (Nat.ne_of_gt this)] simp [liftN]; rw [liftVar_le (Nat.not_lt.1 hi)] @[simp] theorem instL_instVar : (instVar i e k).instL ls = instVar i (e.instL ls) k := by @@ -300,8 +300,8 @@ theorem inst_liftN (e1 e2 : VExpr) : (liftN 1 e1 k).inst e2 k = e1 := by induction e1 generalizing k with simp [liftN, inst, *] | bvar i => simp only [liftVar, instVar, Nat.add_comm 1]; split <;> [rfl; rename_i h] - rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_succ _)) h), - if_neg (mt (by rintro rfl; apply Nat.lt_succ_self) h)]; rfl + rw [ite_eq_right (mt (Nat.lt_of_le_of_lt (Nat.le_succ _)) h), + ite_eq_right (mt (by rintro rfl; apply Nat.lt_succ_self) h)]; rfl theorem inst_liftN' (e1 e2 : VExpr) : (liftN (n+1) e1 k).inst e2 k = liftN n e1 k := by rw [← liftN'_liftN_hi, inst_liftN] @@ -387,7 +387,7 @@ theorem skips_iff : Skips e n k ↔ Skips' n e k := by have := Nat.not_lt.1 h' let i+1 := i; rw [Nat.add_lt_add_iff_right] at h' have := mt (Nat.lt_of_lt_of_le · (Nat.le_add_right ..)) h' - exact ⟨.bvar i, h'.elim, by simp [liftN, liftVar]; rw [if_neg this, Nat.add_comm]⟩ + exact ⟨.bvar i, h'.elim, by simp [liftN, liftVar]; rw [ite_eq_right this, Nat.add_comm]⟩ | sort u => refine ⟨fun ⟨e', h1, h2⟩ => ?_, fun _ => ⟨.sort u, by simp [Skips', liftN]⟩⟩ cases e' <;> cases h2; simp [Skips'] @@ -476,7 +476,7 @@ theorem inst_instVar_hi (i : Nat) (e2 e3 : VExpr) (k j : Nat) : let i+1 := i simp [inst, instVar] have := Nat.lt_of_le_of_lt (Nat.le_add_left ..) hk - rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)] + rw [ite_eq_right (Nat.lt_asymm this), ite_eq_right (Nat.ne_of_gt this)] theorem inst_inst_hi (e1 e2 e3 : VExpr) (k j : Nat) : inst (e1.inst e2 k) e3 (j+k) = (e1.inst e3 (j+k+1)).inst (e2.inst e3 j) k := by @@ -493,7 +493,7 @@ theorem inst_instVar_lo (i : Nat) (e2 e3 : VExpr) (k j : Nat) : simp [instVar]; split <;> rename_i h · split <;> rename_i h1 · simp only [inst, instVar, h1, reduceIte] - rw [if_pos (Nat.lt_of_lt_of_le h1 (Nat.le_add_left ..))] + rw [ite_eq_left (Nat.lt_of_lt_of_le h1 (Nat.le_add_left ..))] split <;> rename_i h1' · subst i simp [inst, instVar]; rw [liftN'_comm (h := Nat.zero_le _), Nat.add_comm] @@ -504,7 +504,7 @@ theorem inst_instVar_lo (i : Nat) (e2 e3 : VExpr) (k j : Nat) : split <;> rename_i h' · subst i have := Nat.lt_succ_of_le (Nat.le_add_left j k) - rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)] + rw [ite_eq_right (Nat.lt_asymm this), ite_eq_right (Nat.ne_of_gt this)] simp [inst, instVar] suffices liftN (k+j+1) .. = _ by rw [this]; exact inst_liftN .. exact (liftN'_liftN' (Nat.zero_le _) (Nat.le_add_left j k)).symm @@ -513,11 +513,11 @@ theorem inst_instVar_lo (i : Nat) (e2 e3 : VExpr) (k j : Nat) : have hk := Nat.lt_of_add_lt_add_right hk simp [inst, instVar] have := Nat.lt_of_le_of_lt (Nat.le_add_left ..) hk - rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)] + rw [ite_eq_right (Nat.lt_asymm this), ite_eq_right (Nat.ne_of_gt this)] have := Nat.lt_succ_of_lt this - rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)] + rw [ite_eq_right (Nat.lt_asymm this), ite_eq_right (Nat.ne_of_gt this)] simp [inst, instVar] - rw [if_neg (Nat.lt_asymm hk), if_neg (Nat.ne_of_gt hk)] + rw [ite_eq_right (Nat.lt_asymm hk), ite_eq_right (Nat.ne_of_gt hk)] theorem inst_inst_lo (e1 e2 e3 : VExpr) (k j : Nat) : inst (e1.inst e2 (k+j+1)) e3 j = diff --git a/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean b/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean index 1f30c80..16bd819 100644 --- a/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean +++ b/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean @@ -369,7 +369,7 @@ private theorem candidateReduceNatFVarAppFVar_none have hfn : (.app (.fvar fnId) (.fvar argId) : Expr).appFn! = .fvar fnId := by rfl rw [hnargs, hfn] - simp only [show (1 == 1) = true by decide, if_true] + simp only [show (1 == 1) = true by decide, ite_true] rw [show Expr.structuralEq (.fvar fnId) (.const ``Nat.succ []) = false by rfl] rfl @@ -594,7 +594,7 @@ private theorem candidateUnfoldDefinitionConstFVarFVar_none (.fvar arg2) : Expr).getAppFn = .const constName levels := by rfl rw [hisApp, hfn] - simp only [if_true, ReaderT.bind, StateT.bind, Except.bind, Bind.bind] + simp only [ite_true, ReaderT.bind, StateT.bind, Except.bind, Bind.bind] rw [candidateUnfoldDefinitionCoreConst_none context constName levels state info hfind] simp [ReaderT.pure, StateT.pure, Except.pure, Pure.pure] diff --git a/Lean4Lean/Verify/Environment/ConstructorValidation.lean b/Lean4Lean/Verify/Environment/ConstructorValidation.lean index a76c1ba..6fd8892 100644 --- a/Lean4Lean/Verify/Environment/ConstructorValidation.lean +++ b/Lean4Lean/Verify/Environment/ConstructorValidation.lean @@ -478,7 +478,7 @@ theorem checkConstructorAlignedExpr.exists_of_run ∃ checked : ConstructorCheckedExpr context source, checkConstructorAlignedExpr context source = .ok checked := by unfold checkConstructorAlignedExpr - rw [dif_pos hfvars, dif_pos hmvars] + rw [dite_eq_left hfvars, dite_eq_left hmvars] rw [observeCandidateCheckType_of_run context source inferred hrun] exact ⟨_, rfl⟩ @@ -497,7 +497,7 @@ theorem ConstructorCheckedExpr.check_eq have hmvars : source.hasMVar = false := fvarsIn_iff_hasMVar.mp (fvarsIn_iff.mp checked.fvars).2 unfold checkConstructorAlignedExpr - rw [dif_pos hfvars, dif_pos hmvars] + rw [dite_eq_left hfvars, dite_eq_left hmvars] rw [observeCandidateCheckType_of_run context source checked.observation.inferred checked.observation.valid] cases checked @@ -2349,7 +2349,7 @@ theorem ConstructorPreFamilyIndexSpineTrace.build_eq induction trace with | nil expected expectedCheck terminal => simp only [ConstructorPreFamilyIndexSpineTrace.build] - rw [dif_pos terminal, expectedCheck.check_eq] + rw [dite_eq_left terminal, expectedCheck.check_eq] rfl | cons name domain body binderInfo argument arguments expectedCheck step tail ih => @@ -2666,7 +2666,7 @@ theorem ConstructorPreFamilyRecursiveTrace.forallE_build_eq simp only [Bind.bind, Except.bind] rw [annotations.observe_eq] simp only [] - rw [dif_pos fresh, tailRun] + rw [dite_eq_left fresh, tailRun] rfl theorem ConstructorPreFamilyRecursiveTrace.target_build_eq @@ -2680,7 +2680,7 @@ theorem ConstructorPreFamilyRecursiveTrace.target_build_eq cases source <;> simp only [ConstructorPreFamilyRecursiveTrace.build] case forallE => simp [Expr.isForall] at terminal all_goals - rw [dif_pos valid, spine.build_eq] + rw [dite_eq_left valid, spine.build_eq] rfl /-! @@ -3091,7 +3091,7 @@ theorem ConstructorPreFamilyViewTrace.terminal_build_eq cases source <;> simp only [ConstructorPreFamilyViewTrace.build] case forallE => simp [Expr.isForall] at terminal all_goals - rw [dif_pos valid, dif_pos independent, spine.build_eq] + rw [dite_eq_left valid, dite_eq_left independent, spine.build_eq] rfl /-! diff --git a/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean b/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean index 55ed434..bc9b7f9 100644 --- a/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean +++ b/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean @@ -2905,7 +2905,7 @@ theorem prbSelfDefEq (source : Expr) fuel context state : TypeChecker.Inner.isDefEq source source (TypeChecker.Methods.withFuel fuel) context state = .ok (true, state) := by unfold TypeChecker.Inner.isDefEq - rw [if_pos (Expr.eqv_refl _)] + rw [ite_eq_left (Expr.eqv_refl _)] rfl @[simp] theorem prbConstBeqFVar (name : Name) (levels : List Level) @@ -5297,10 +5297,10 @@ theorem prbSafetyRunDirect : · rename_i nonrecursive rw [prbPreFamilyNextDomainHasIndOccReplay] at nonrecursive contradiction - · rw [dif_pos recursiveIndependent] + · rw [dite_eq_left recursiveIndependent] rw [recursiveFieldRunAtContext] simp only [Bind.bind, Except.bind] - rw [dif_pos prbPreFamilyAFreshReplay] + rw [dite_eq_left prbPreFamilyAFreshReplay] rw [recursiveViewTailRunExact] rfl obtain ⟨afterATrace, afterARun⟩ : @@ -5384,13 +5384,13 @@ theorem prbSafetyRunDirect : rw [noParameterOne] at parameterAt contradiction · split - · rw [dif_pos rootIndependent] + · rw [dite_eq_left rootIndependent] rw [rootAlpha.check_eq, rootAlphaEnsure.observe_eq, rootAlphaConsumed.check_eq] simp only [Bind.bind, Except.bind] rw [rootAlphaAnnotations.observe_eq] simp only [] - rw [dif_pos prbPreFamilyRootFreshReplay] + rw [dite_eq_left prbPreFamilyRootFreshReplay] have ordinaryTailRun' : AddInductive.ConstructorPreFamilyViewTrace.build prbStagedUniverseInput.staged.family.validation.stats 0 @@ -5560,7 +5560,7 @@ theorem prbSafetyRunDirect : propRecursiveBoundaryKernelType, propRecursiveBoundaryKernelCtor, propRecursiveBoundaryInfo, propRecursiveBoundaryMkInfo, ConstantInfo.type, ConstantInfo.toConstantVal] - rw [if_pos translationUnique] + rw [ite_eq_left translationUnique] rw [parametersRun] simp only [Bind.bind, Except.bind] rw [listRun] @@ -10429,13 +10429,13 @@ theorem cvmPreFamilyOrdinaryBuildEqTest rw [noParameter] at parameterAt contradiction · split - · rw [dif_pos independent] + · rw [dite_eq_left independent] rw [domainCheck.check_eq, ensureType.observe_eq, consumedCheck.check_eq] simp only [Bind.bind, Except.bind] rw [annotations.observe_eq] simp only [] - rw [dif_pos fresh, tailRun] + rw [dite_eq_left fresh, tailRun] rfl · rename_i recursive rw [nonrecursive] at recursive @@ -10474,9 +10474,9 @@ theorem cvmPreFamilyRecursiveBuildEqTest · rename_i nonrecursive rw [isRecursive] at nonrecursive contradiction - · rw [dif_pos independent, fieldRun] + · rw [dite_eq_left independent, fieldRun] simp only [Bind.bind, Except.bind] - rw [dif_pos fresh, tailRun] + rw [dite_eq_left fresh, tailRun] rfl theorem cvmPreFamilyParameterAtZeroTest : @@ -11296,7 +11296,7 @@ theorem cvmSafetyRunDirectTest : constructorValidityMatrixInfo, constructorValidityMatrixMkInfo, ConstantInfo.type, ConstantInfo.toConstantVal] unfold AddInductive.checkConstructorPreFamilySafety - rw [if_pos translationUnique] + rw [ite_eq_left translationUnique] rw [cvmPreFamilyParametersRunTest] simp only [Bind.bind, Except.bind] rw [listRun] diff --git a/Lean4Lean/Verify/Environment/Extension.lean b/Lean4Lean/Verify/Environment/Extension.lean index 223d8f5..e4cacb1 100644 --- a/Lean4Lean/Verify/Environment/Extension.lean +++ b/Lean4Lean/Verify/Environment/Extension.lean @@ -180,7 +180,7 @@ theorem insertDefs_wf : ∀ {cis : List DefinitionVal} {C : ConstMap}, C.WF → | d :: ds, C, hC, hfr, hnd => by rw [List.map_cons, List.nodup_cons] at hnd refine insertDefs_wf (cis := ds) (hC.insert _ _ (hfr _ (.head _))) (fun e he => ?_) hnd.2 - rw [hC.find?_insert, if_neg]; · exact hfr e (.tail _ he) + rw [hC.find?_insert, ite_eq_right]; · exact hfr e (.tail _ he) simp only [beq_iff_eq]; intro hh exact hnd.1 (List.mem_map.2 ⟨e, he, hh.symm⟩) @@ -224,7 +224,7 @@ theorem TrEnv'.ignoreDefs : ∀ {vs : List DefinitionVal} {C : ConstMap}, have H' := TrEnv'.ignore (ci := .defnInfo d) (hfr _ (.head _)) (hvis _ (.head _)) H show TrEnv' safety (insertDefs (SMap.insert C d.name (.defnInfo d)) ds) Q _ refine TrEnv'.ignoreDefs (fun e he => hvis e (.tail _ he)) (fun e he => ?_) hnd.2 H' - rw [H.map_wf.find?_insert, if_neg]; · exact hfr e (.tail _ he) + rw [H.map_wf.find?_insert, ite_eq_right]; · exact hfr e (.tail _ he) simp only [beq_iff_eq]; intro hh exact hnd.1 (List.mem_map.2 ⟨e, he, hh.symm⟩) @@ -234,7 +234,7 @@ theorem Environment.find?_add_of_ne {env : Environment} (mapWF : env.constants.W have hnone : env.constants.find? ci.name = none := by rwa [← mapWF.find?'_eq_find?] have mapWF' := mapWF.insert ci.name ci hnone change SMap.find?' (env.constants.insert ci.name ci) n = none - rw [mapWF'.find?'_eq_find?, mapWF.find?_insert, if_neg (by simpa using hne)] + rw [mapWF'.find?'_eq_find?, mapWF.find?_insert, ite_eq_right (by simpa using hne)] rwa [Kernel.Environment.find?, mapWF.find?'_eq_find?] at h /-- Data produced by `addMutual`'s header loop for one block member. -/ @@ -343,9 +343,9 @@ theorem addMutualBlock.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) obtain ⟨ves', hves'⟩ := VEnvs.axiom_of_choice hves' have hbaseSf (sf) (hv : sf ≤ bs) : ∃ b, (ves.venv sf).addConsts cis = some b ∧ ves'.venv sf = b.addDefEqs cis := by - have h := hves' sf; rw [if_pos hv] at h; exact h + have h := hves' sf; rw [ite_eq_left hv] at h; exact h have hsame (sf) (hv : ¬ sf ≤ bs) : ves'.venv sf = ves.venv sf := by - have h := hves' sf; rwa [if_neg hv] at h + have h := hves' sf; rwa [ite_eq_right hv] at h refine ⟨ves', ?_, fun sf => by by_cases hv : sf ≤ bs · obtain ⟨b, hb, heq⟩ := hbaseSf sf hv @@ -432,9 +432,9 @@ theorem addConstCore.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) obtain ⟨ves', hves'⟩ := VEnvs.axiom_of_choice hves' have hadd (safety) (hvisible : safety ≤ ci.safety) : (ves.venv safety).addConst ci.name ci'.toVConstant = some (ves'.venv safety) := by - have h := hves' safety; unfold VEnv.AddConst at h; rw [if_pos hvisible] at h; exact h.2.2 + have h := hves' safety; unfold VEnv.AddConst at h; rw [ite_eq_left hvisible] at h; exact h.2.2 have hsame (safety) (hvisible : ¬ safety ≤ ci.safety) : ves'.venv safety = ves.venv safety := by - have h := hves' safety; unfold VEnv.AddConst at h; rwa [if_neg hvisible] at h + have h := hves' safety; unfold VEnv.AddConst at h; rwa [ite_eq_right hvisible] at h refine ⟨ves', ?_, hves'⟩ have readiness : ∀ safety, ProjectionReady (env.add ci) (ves'.venv safety) ∧ @@ -514,11 +514,11 @@ theorem addDef.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) have hbase (safety) (hvisible : safety ≤ (ConstantInfo.defnInfo v).safety) : ∃ base, (ves.venv safety).addConst v.name ci'.toVConstant = some base ∧ ves'.venv safety = base.addDefEq ci'.toDefEq := by - have h := hves' safety; unfold VEnv.AddDef at h; rw [if_pos hvisible] at h + have h := hves' safety; unfold VEnv.AddDef at h; rw [ite_eq_left hvisible] at h obtain ⟨base, _, _, hadd, heq⟩ := h; exact ⟨base, hadd, heq⟩ have hsame (safety) (hvisible : ¬ safety ≤ (ConstantInfo.defnInfo v).safety) : ves'.venv safety = ves.venv safety := by - have h := hves' safety; unfold VEnv.AddDef at h; rwa [if_neg hvisible] at h + have h := hves' safety; unfold VEnv.AddDef at h; rwa [ite_eq_right hvisible] at h refine ⟨ves', ?_, hves'⟩ have readiness : ∀ safety, ProjectionReady (env.add (.defnInfo v)) (ves'.venv safety) ∧ diff --git a/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean b/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean index fca8d3c..6418c16 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean @@ -103,7 +103,7 @@ theorem candidateIsDefEqSelfValid (Lean4Lean.TypeChecker.Methods.withFuel (fuel + 1)) context.toTypeChecker ({} : Lean4Lean.TypeChecker.State)) = .ok true unfold Lean4Lean.TypeChecker.Inner.isDefEq - rw [if_pos (Expr.eqv_refl e)] + rw [ite_eq_left (Expr.eqv_refl e)] rfl def indexedVecTypeCheckerContext diff --git a/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean b/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean index 1074587..5764a66 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean @@ -656,12 +656,12 @@ theorem consAfterHeadCheckFirstCache : simpa only [consTailDomain, ctorIndexedVecApp, consAlphaExprShape, consNExprShape] using replayTailDomainBeqFirstApp] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consHeadNState replayInsert rw [Std.HashMap.getElem?_insert] rw [show (consNExpr == replayFirstApp (.fvar consAlphaId)) = false by simp [consNExprShape, replayFirstApp]] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consHeadFirstAppState replayInsert rw [Std.HashMap.getElem?_insert] rw [show (replayFirstApp consAlphaExpr == @@ -680,7 +680,7 @@ theorem consAfterHeadCheckNCache : (replayAppBeqFVar ((.const ``IndexedVec [.param `u] : Expr).app (.fvar consAlphaId)) (.fvar consNId) consNId)] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consHeadNState replayInsert rw [Std.HashMap.getElem?_insert] rw [show (consNExpr == (.fvar consNId : Expr)) = true by simp] @@ -933,7 +933,7 @@ theorem consAfterNCheckTailFirstCache : unfold consAfterNCheckTailDomainState replayInsert rw [Std.HashMap.getElem?_insert] rw [replayTailDomainBeqFirstApp] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consAfterNCheckNState replayInsert rw [Std.HashMap.getElem?_insert] rw [show ((.fvar consNId : Expr) == @@ -941,7 +941,7 @@ theorem consAfterNCheckTailFirstCache : simpa only [replayFirstApp] using (replayFVarBeqApp consNId (.const ``IndexedVec [.param `u]) (.fvar consAlphaId))] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consAfterNCheckFirstAppState replayInsert rw [Std.HashMap.getElem?_insert] rw [beq_self_eq_true] @@ -960,7 +960,7 @@ theorem consAfterNCheckTailNCache : (replayAppBeqFVar ((.const ``IndexedVec [.param `u] : Expr).app (.fvar consAlphaId)) (.fvar consNId) consNId)] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consAfterNCheckNState replayInsert rw [Std.HashMap.getElem?_insert] rw [beq_self_eq_true] @@ -1420,14 +1420,14 @@ theorem consAfterAlphaCheckTailFirstCache : unfold consAfterAlphaCheckTailDomainState replayInsert rw [Std.HashMap.getElem?_insert] rw [replayIndexedVecAppBeqFirstApp] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consAfterAlphaCheckNInferState replayInsert rw [Std.HashMap.getElem?_insert] rw [show ((.fvar consAfterAlphaCheckNId : Expr) == replayFirstApp (.fvar consAlphaId)) = false by exact replayFVarBeqApp consAfterAlphaCheckNId (.const ``IndexedVec [.param `u]) (.fvar consAlphaId)] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consAfterAlphaCheckFirstAppState replayInsert rw [Std.HashMap.getElem?_insert] rw [beq_self_eq_true] @@ -1449,7 +1449,7 @@ theorem consAfterAlphaCheckTailNCache : ((.const ``IndexedVec [.param `u] : Expr).app (.fvar consAlphaId)) (.fvar consAfterAlphaCheckNId) consAfterAlphaCheckNId] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consAfterAlphaCheckNInferState replayInsert rw [Std.HashMap.getElem?_insert] rw [beq_self_eq_true] @@ -1929,7 +1929,7 @@ theorem consRootCheckTailFirstCache : unfold consRootCheckTailDomainState replayInsert rw [Std.HashMap.getElem?_insert] rw [replayIndexedVecAppBeqFirstApp] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consRootCheckNInferState replayInsert rw [Std.HashMap.getElem?_insert] rw [show ((.fvar consRootCheckNId : Expr) == @@ -1937,7 +1937,7 @@ theorem consRootCheckTailFirstCache : exact replayFVarBeqApp consRootCheckNId (.const ``IndexedVec [.param `u]) (.fvar consRootCheckAlphaId)] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consRootCheckFirstAppState replayInsert rw [Std.HashMap.getElem?_insert] rw [beq_self_eq_true] @@ -1957,7 +1957,7 @@ theorem consRootCheckTailNCache : ((.const ``IndexedVec [.param `u] : Expr).app (.fvar consRootCheckAlphaId)) (.fvar consRootCheckNId) consRootCheckNId] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] unfold consRootCheckNInferState replayInsert rw [Std.HashMap.getElem?_insert] rw [beq_self_eq_true] diff --git a/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean b/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean index 5b90c63..7caef8c 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean @@ -172,7 +172,7 @@ theorem selfDefEq (e : Expr) fuel context state : TypeChecker.Inner.isDefEq e e (TypeChecker.Methods.withFuel fuel) context state = .ok (true, state) := by unfold TypeChecker.Inner.isDefEq - rw [if_pos (Expr.eqv_refl _)] + rw [ite_eq_left (Expr.eqv_refl _)] rfl @[simp] theorem constBeqFVar (name : Name) (levels : List Level) @@ -906,7 +906,7 @@ theorem nilCandidateReduceRecursor simp only [nilRecMBind, nilRecMGetEnv] rw [show (tcContext nilCandidateAlphaLctx).env = ctorEnv by rfl] rw [hquot] - simp only [Bool.false_eq_true, if_false, nilRecMBind] + simp only [Bool.false_eq_true, ite_false, nilRecMBind] rw [nilCandidateInductiveReduceRec methods state] rfl @@ -1002,7 +1002,7 @@ theorem nilCandidateUnfoldBody rw [show nilCandidateBody.isApp = true by rw [nilCandidateBodyShape] rfl] - simp only [if_true] + simp only [ite_true] rw [nilCandidateBodyGetAppFn] simp only [nilRecMBind] rw [nilCandidateUnfoldFamily] @@ -1677,7 +1677,7 @@ theorem ctorIndexedVecReduceRecursor simp only [nilRecMBind, nilRecMGetEnv] rw [show (tcContext lctx).env = ctorEnv by rfl] rw [hquot] - simp only [Bool.false_eq_true, if_false, nilRecMBind] + simp only [Bool.false_eq_true, ite_false, nilRecMBind] rw [ctorIndexedVecInductiveReduceRec] rfl @@ -1748,7 +1748,7 @@ theorem ctorIndexedVecUnfold methods (tcContext lctx) state = .ok (none, state) := by unfold TypeChecker.Inner.unfoldDefinition rw [show (ctorIndexedVecApp alpha index).isApp = true by rfl] - simp only [if_true] + simp only [ite_true] rw [ctorIndexedVecAppGetAppFn] simp only [nilRecMBind] rw [ctorIndexedVecUnfoldFamily] diff --git a/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean b/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean index 81ea7e7..75bb947 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean @@ -1141,7 +1141,7 @@ theorem indexedVecValidationNatPositivity : exact ctorNatWhnfM indexedVecCtorValidationContext.lctx] simp only [Except.bind] rw [indexedVecValidationNatHasNoIndOcc] - simp only [Bool.not_false, if_true, + simp only [Bool.not_false, ite_true, ReaderT.pure, Pure.pure, Except.pure] theorem indexedVecValidationAlphaPositivity : @@ -1173,7 +1173,7 @@ theorem indexedVecValidationAlphaPositivity : indexedVecValidationAlphaId indexedVecValidationAlphaFindInN] simp only [Except.bind] rw [indexedVecValidationAlphaHasNoIndOcc] - simp only [Bool.not_false, if_true, + simp only [Bool.not_false, ite_true, ReaderT.pure, Pure.pure, Except.pure] theorem indexedVecValidationTailPositivity : @@ -1212,7 +1212,7 @@ theorem indexedVecValidationTailPositivity : indexedVecValidationAlpha indexedVecValidationNExpr] simp only [Except.bind] rw [indexedVecValidationTailHasIndOcc] - simp only [Bool.not_true, Bool.false_eq_true, if_false, Pure.pure] + simp only [Bool.not_true, Bool.false_eq_true, ite_false, Pure.pure] rw [indexedVecValidationAppIsValid indexedVecValidationNExpr indexedVecValidationNHasNoIndOcc] rfl @@ -1256,7 +1256,7 @@ theorem indexedVecValidationNilLoop : simp only [Except.bind] rw [AddInductive.liftTypeChecker_apply] rw [indexedVecValidationParamIsDefEq] - simp only [if_true] + simp only [ite_true] simpa [indexedVecValidationNilResult, ctorIndexedVecApp, indexedVecKernelNil, indexedVecNilInfo, ConstantInfo.name, ConstantInfo.toConstantVal, @@ -1317,7 +1317,7 @@ theorem indexedVecValidationConsLoopTail : rw [AddInductive.liftTypeChecker_apply] rw [indexedVecValidationTailEnsureTypeM] simp only [Except.bind] - rw [if_pos (show AddInductive.levelStructGe + rw [ite_eq_left (show AddInductive.levelStructGe indexedVecCandidateInductiveStats.resultLevel (Expr.sort (.succ (.param `u))).sortLevel! = true from by simp [Expr.sortLevel!, indexedVecCandidateInductiveStats_resultLevel, @@ -1352,7 +1352,7 @@ theorem indexedVecValidationConsLoopHead : rw [AddInductive.liftTypeChecker_apply] rw [indexedVecValidationAlphaEnsureTypeM] simp only [Except.bind] - rw [if_pos (show AddInductive.levelStructGe + rw [ite_eq_left (show AddInductive.levelStructGe indexedVecCandidateInductiveStats.resultLevel (Expr.sort (.succ (.param `u))).sortLevel! = true from by simp [Expr.sortLevel!, indexedVecCandidateInductiveStats_resultLevel, @@ -1393,7 +1393,7 @@ theorem indexedVecValidationConsLoopN : rw [AddInductive.liftTypeChecker_apply] rw [indexedVecValidationNatEnsureTypeM] simp only [Except.bind] - rw [if_pos (show AddInductive.levelStructGe + rw [ite_eq_left (show AddInductive.levelStructGe indexedVecCandidateInductiveStats.resultLevel (Expr.sort (.succ .zero)).sortLevel! = true from by simp [Expr.sortLevel!, indexedVecCandidateInductiveStats_resultLevel, @@ -1443,7 +1443,7 @@ theorem indexedVecValidationConsLoop : simp only [Except.bind] rw [AddInductive.liftTypeChecker_apply] rw [indexedVecValidationParamIsDefEq] - simp only [if_true] + simp only [ite_true] simpa [indexedVecValidationConsAfterParam] using indexedVecValidationConsLoopN @@ -1495,7 +1495,7 @@ theorem indexedVecValidationConsUniverseLoopTail : simp only [ReaderT.bind, Bind.bind, AddInductive.liftTypeChecker_apply] rw [indexedVecValidationTailEnsureTypeM] simp only [Except.bind] - rw [if_pos (show AddInductive.constructorUniverseSemanticGe + rw [ite_eq_left (show AddInductive.constructorUniverseSemanticGe indexedVecCandidateInductiveStats.resultLevel (Expr.sort (.succ (.param `u))).sortLevel! = true from by simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe, @@ -1522,7 +1522,7 @@ theorem indexedVecValidationConsUniverseLoopHead : simp only [ReaderT.bind, Bind.bind, AddInductive.liftTypeChecker_apply] rw [indexedVecValidationAlphaEnsureTypeM] simp only [Except.bind] - rw [if_pos (show AddInductive.constructorUniverseSemanticGe + rw [ite_eq_left (show AddInductive.constructorUniverseSemanticGe indexedVecCandidateInductiveStats.resultLevel (Expr.sort (.succ (.param `u))).sortLevel! = true from by simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe, @@ -1550,7 +1550,7 @@ theorem indexedVecValidationConsUniverseLoopN : simp only [ReaderT.bind, Bind.bind, AddInductive.liftTypeChecker_apply] rw [indexedVecValidationNatEnsureTypeM] simp only [Except.bind] - rw [if_pos (show AddInductive.constructorUniverseSemanticGe + rw [ite_eq_left (show AddInductive.constructorUniverseSemanticGe indexedVecCandidateInductiveStats.resultLevel (Expr.sort (.succ .zero)).sortLevel! = true from by simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe, @@ -1655,7 +1655,7 @@ theorem indexedVecValidationCheckConstructors : simp only [indexedVecKernelType, List.toList_toArray, ReaderT.bind, Bind.bind, Except.bind] rw [indexedVecValidationEmptyDoesNotContainNil] - simp only [Bool.false_eq_true, if_false, + simp only [Bool.false_eq_true, ite_false, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, Except.bind, Except.pure] rw [indexedVecNilNoMVarNoFVar] @@ -1671,7 +1671,7 @@ theorem indexedVecValidationCheckConstructors : unfold AddInductive.checkConstructorFold simp only [Except.bind, ReaderT.pure, Pure.pure, Except.pure] rw [indexedVecValidationNilSetDoesNotContainCons] - simp only [Bool.false_eq_true, if_false, + simp only [Bool.false_eq_true, ite_false, ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, Except.bind, Except.pure] rw [indexedVecConsNoMVarNoFVar] diff --git a/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean b/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean index f820d63..3dd847a 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean @@ -2521,9 +2521,9 @@ private theorem indexedVecPreFamilySafetyRun : · rename_i nonrecursive rw [indexedVecValidationTailHasIndOcc] at nonrecursive contradiction - · rw [dif_pos recursiveIndependent, recursiveFieldRun] + · rw [dite_eq_left recursiveIndependent, recursiveFieldRun] simp only [Bind.bind, Except.bind] - rw [dif_pos headFresh] + rw [dite_eq_left headFresh] rw [explicitResultTailRun] exact ⟨_, rfl⟩ obtain ⟨consHeadTailTrace, consHeadTailRun⟩ : @@ -2605,12 +2605,12 @@ private theorem indexedVecPreFamilySafetyRun : · split · rw [alphaChecked.check_eq, alphaEnsure.observe_eq, alphaConsumed.check_eq] - rw [dif_pos (by + rw [dite_eq_left (by simp [AddInductive.constructorIndependentOf])] simp only [Bind.bind, Except.bind] rw [alphaAnnotations.observe_eq] simp only [] - rw [dif_pos nFresh] + rw [dite_eq_left nFresh] rw [explicitHeadTailRun] exact ⟨_, rfl⟩ · rename_i recursive @@ -2694,12 +2694,12 @@ private theorem indexedVecPreFamilySafetyRun : · split · rw [baseNat.check_eq, baseNatEnsure.observe_eq, baseNatConsumed.check_eq] - rw [dif_pos (by + rw [dite_eq_left (by simp [AddInductive.constructorIndependentOf])] simp only [Bind.bind, Except.bind] rw [baseNatAnnotations.observe_eq] simp only [] - rw [dif_pos baseFresh] + rw [dite_eq_left baseFresh] rw [explicitNTailRun] exact ⟨_, rfl⟩ · rename_i recursive @@ -2836,7 +2836,7 @@ private theorem indexedVecPreFamilySafetyRun : simp [AddInductive.theoryTranslationUnique, vecFamilyTail, nilCtorTypeRaw, nilCtorBodyRaw, consCtorTypeRaw, consNTypeRaw, consHeadTypeRaw, consTailTypeRaw, consTerminalRaw] - rw [if_pos translationUnique] + rw [ite_eq_left translationUnique] rw [parametersRun] simp only [Bind.bind, Except.bind] rw [constructorListRun] diff --git a/Lean4Lean/Verify/Environment/InductiveFixtures.lean b/Lean4Lean/Verify/Environment/InductiveFixtures.lean index 46bd563..844d315 100644 --- a/Lean4Lean/Verify/Environment/InductiveFixtures.lean +++ b/Lean4Lean/Verify/Environment/InductiveFixtures.lean @@ -3082,7 +3082,7 @@ private theorem annotatedPiIsDefEqSort (TypeChecker.Methods.withFuel fuel) context initial = .ok (true, initial) := by unfold TypeChecker.Inner.isDefEq - rw [if_pos (Expr.eqv_refl _)] + rw [ite_eq_left (Expr.eqv_refl _)] rfl private def annotatedPiCtorExpectedView : Expr := @@ -4076,7 +4076,7 @@ private theorem unfoldAliasRecFieldInitial (methods) : (.const ``AliasRec [])), recAliasUnfoldState {}) := by rw [aliasRecFieldKernelExpr_eq] unfold TypeChecker.Inner.unfoldDefinition - rw [if_pos (show (Expr.app (.const ``RecAlias [.succ .zero]) + rw [ite_eq_left (show (Expr.app (.const ``RecAlias [.succ .zero]) (.const ``AliasRec [])).isApp = true from rfl)] rw [show (Expr.app (.const ``RecAlias [.succ .zero]) @@ -4334,7 +4334,7 @@ private theorem annotatedPiReduceRecursorDomain .ok (none, state) := by unfold TypeChecker.Inner.reduceRecursor simp only [normalizationRecMBind, normalizationRecMGetEnv] - rw [if_neg (show + rw [ite_eq_right (show ¬(annotatedPiCtorCandidateContext.toTypeChecker.env.quotInit = true) by simp [annotatedPiCtorCandidateContext, AddInductive.Context.toTypeChecker, annotatedPiType_quotInit])] @@ -4412,7 +4412,7 @@ private theorem annotatedPiUnfoldDomainInitial (methods) : .ok (some annotatedPiDomainBetaKernel, annotatedPiOutParamUnfoldState {}) unfold TypeChecker.Inner.unfoldDefinition - rw [if_pos (show (Expr.app (.const ``outParam [.succ .zero]) + rw [ite_eq_left (show (Expr.app (.const ``outParam [.succ .zero]) (.sort .zero)).isApp = true from rfl)] rw [show (Expr.app (.const ``outParam [.succ .zero]) @@ -4899,7 +4899,7 @@ private theorem annotatedPiUnfoldDomainOfMiss .ok (some annotatedPiDomainBetaKernel, annotatedPiOutParamUnfoldState state) unfold TypeChecker.Inner.unfoldDefinition - rw [if_pos (show (Expr.app (.const ``outParam [.succ .zero]) + rw [ite_eq_left (show (Expr.app (.const ``outParam [.succ .zero]) (.sort .zero)).isApp = true from rfl)] rw [show (Expr.app (.const ``outParam [.succ .zero]) @@ -5105,7 +5105,7 @@ private theorem annotatedPiLazyDeltaLoopDomain rw [annotatedPiIsDefEqOffsetDomain fuel] simp only rw [show (LBool.undef != LBool.undef) = false by rfl] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] rw [normalizationRecMBind] rw [normalizationRecMReadContext] simp only @@ -5116,7 +5116,7 @@ private theorem annotatedPiLazyDeltaLoopDomain by simp [Expr.hasFVar_eq, Expr.hasFVar', annotatedPiRawDomainKernel]] - simp only [if_true] + simp only [ite_true] rw [normalizationRecMBind] rw [annotatedPiReduceNatDomain] simp only @@ -5201,17 +5201,17 @@ private theorem annotatedPiIsDefEqCoreDomain · subst r simp only rw [show (LBool.true != LBool.undef) = true by rfl] - simp only [if_true] + simp only [ite_true] exact ⟨({ success := m } : TypeChecker.State), rfl⟩ · subst r simp only rw [show (LBool.undef != LBool.undef) = false by rfl] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] rw [normalizationRecMBind] rw [normalizationRecMReadContext] simp only rw [show ((.sort .zero : Expr).isConstOf ``true) = false by rfl] - simp only [Bool.and_false, Bool.false_eq_true, if_false] + simp only [Bool.and_false, Bool.false_eq_true, ite_false] rw [normalizationRecMBind] rw [annotatedPiWhnfCoreDomainCheap fuel] simp only @@ -5221,12 +5221,12 @@ private theorem annotatedPiIsDefEqCoreDomain cases hptr : (!(ptrEqExpr annotatedPiRawDomainKernel annotatedPiRawDomainKernel && ptrEqExpr (.sort .zero) (.sort .zero))) - · simp only [Bool.false_eq_true, if_false] + · simp only [Bool.false_eq_true, ite_false] rw [normalizationRecMBind] rw [annotatedPiIsDefEqProofIrrelDomain fuel] simp only rw [show (LBool.undef != LBool.undef) = false by rfl] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] rw [normalizationRecMBind] obtain ⟨m'', hlazy⟩ := annotatedPiLazyDeltaDomain fuel m rw [hlazy] @@ -5234,7 +5234,7 @@ private theorem annotatedPiIsDefEqCoreDomain (annotatedPiOutParamUnfoldState (annotatedPiSortOneInferOnlyState m)) m'', ?_⟩ rfl - · simp only [if_true] + · simp only [ite_true] obtain ⟨r, m', hquick', hr⟩ := annotatedPiQuickIsDefEqDomainAny fuel m rw [normalizationRecMBind] @@ -5243,17 +5243,17 @@ private theorem annotatedPiIsDefEqCoreDomain rcases hr with htrue | hundef · subst r rw [show (LBool.true != LBool.undef) = true by rfl] - simp only [if_true] + simp only [ite_true] refine ⟨({ success := m' } : TypeChecker.State), ?_⟩ rfl · subst r rw [show (LBool.undef != LBool.undef) = false by rfl] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] rw [normalizationRecMBind] rw [annotatedPiIsDefEqProofIrrelDomain fuel] simp only rw [show (LBool.undef != LBool.undef) = false by rfl] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] rw [normalizationRecMBind] obtain ⟨m'', hlazy⟩ := annotatedPiLazyDeltaDomain fuel m' rw [hlazy] @@ -5290,7 +5290,7 @@ private theorem annotatedPiDomain_isDefEqInner rw [show (annotatedPiRawDomainKernel == (.sort .zero : Expr)) = false by exact annotatedPiApp_beq_sort _ _ _] - simp only [Bool.false_eq_true, if_false, normalizationRecMBind] + simp only [Bool.false_eq_true, ite_false, normalizationRecMBind] rw [hcore'] exact ⟨_, rfl⟩ @@ -5376,7 +5376,7 @@ private theorem annotatedPiInner_isDefEqM : annotatedPiCtorCandidateContext.toTypeChecker ({} : TypeChecker.State)) = .ok true unfold TypeChecker.Inner.isDefEq - rw [if_pos (Expr.eqv_refl _)] + rw [ite_eq_left (Expr.eqv_refl _)] rfl private theorem annotatedPiConst_checkTypeM (lctx : LocalContext) : @@ -6114,13 +6114,13 @@ private theorem annotatedPi_checkPositivity : rw [show AddInductive.hasIndOcc annotatedPiInductiveStats.indConsts annotatedPiInnerKernel = true by exact annotatedPiInner_stats_hasIndOcc] - simp only [Bool.not_true, Bool.false_eq_true, if_false, Pure.pure] + simp only [Bool.not_true, Bool.false_eq_true, ite_false, Pure.pure] unfold annotatedPiInnerKernel simp only rw [show AddInductive.hasIndOcc annotatedPiInductiveStats.indConsts annotatedPiRawDomainKernel = false by exact annotatedPiRawDomain_hasIndOcc_false] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] simpa [withLocalDecl, annotatedPiInnerBodyCandidateContext, withFreshId, MonadLocalNameGenerator.withFreshId, MonadWithReader.withReader, withTheReader, @@ -6309,7 +6309,7 @@ private theorem annotatedPi_checkConstructors : rw [AddInductive.liftTypeChecker_apply] rw [annotatedPiInner_ensureTypeM_expanded] simp only [Except.bind] - rw [if_pos (show AddInductive.levelStructGe + rw [ite_eq_left (show AddInductive.levelStructGe annotatedPiInductiveStats.resultLevel (Expr.sort (.succ .zero)).sortLevel! = true from rfl)] simp only [Bool.not_false, ↓reduceIte, ReaderT.bind, Bind.bind, Except.bind] @@ -7085,7 +7085,7 @@ private theorem isDefEqSort .ok (true, state) := by refine ⟨initial, ?_⟩ unfold TypeChecker.Inner.isDefEq - rw [if_pos (Expr.eqv_refl _)] + rw [ite_eq_left (Expr.eqv_refl _)] rfl private theorem inferTypeRecAliasInitial : @@ -7124,7 +7124,7 @@ theorem aliasRecField_checkType : .ok (.sort (.succ .zero), state) rw [aliasRecFieldKernelExpr_eq] unfold TypeChecker.Inner.inferType' - simp only [aliasRecField_noLooseBVars, Bool.false_eq_true, if_false, cond, normalizationRecMGet, + simp only [aliasRecField_noLooseBVars, Bool.false_eq_true, ite_false, cond, normalizationRecMGet, Std.HashMap.getElem?_empty, normalizationRecMBind] rw [inferTypeRecAliasInitial] simp only @@ -7135,7 +7135,7 @@ theorem aliasRecField_checkType : isDefEqSort aliasRecNormalizationRawContext (aliasRecFieldArgState (aliasRecFieldFnState {})) dsimp only - rw [if_neg (show ¬((Expr.const ``AliasRec []).isAppOfArity + rw [ite_eq_right (show ¬((Expr.const ``AliasRec []).isAppOfArity `eagerReduce 2 = true) from by simp [aliasRecFamily_notEagerReduce])] simp only [aliasRecFieldFnType_bindingDomain, @@ -7678,7 +7678,7 @@ private theorem aliasFormerPreFamilySafetyRun : aliasFormerCandidateContext (.sort (.succ .zero)) [] = .ok spineTrace := by unfold AddInductive.ConstructorPreFamilyIndexSpineTrace.build - rw [dif_pos sortTerminal, sortCheckedRun] + rw [dite_eq_left sortTerminal, sortCheckedRun] rfl obtain ⟨targetSpineTrace, targetSpineRun⟩ : ∃ targetSpineTrace : AddInductive.ConstructorPreFamilyIndexSpineTrace @@ -7706,7 +7706,7 @@ private theorem aliasFormerPreFamilySafetyRun : rw [inductiveFuel] rw [show 1000 = 999 + 1 by rfl] simp only [AddInductive.ConstructorPreFamilyViewTrace.build] - rw [dif_pos valid, dif_pos independent] + rw [dite_eq_left valid, dite_eq_left independent] rw [targetSpineRun] exact ⟨_, rfl⟩ obtain ⟨listTrace, listRun⟩ : ∃ listTrace, @@ -7726,7 +7726,7 @@ private theorem aliasFormerPreFamilySafetyRun : AddInductive.CandidateConstructor [])).viewTranslationUnique) = true := by rfl - rw [if_pos translationUnique] + rw [ite_eq_left translationUnique] simp [parametersRun, listRun, Bind.bind, Except.bind, Except.pure, Pure.pure] @@ -8747,7 +8747,7 @@ private theorem annotatedPiInnerView_isDefEqForall rw [show (annotatedPiRawDomainKernel == (.sort .zero : Expr)) = false by exact annotatedPiApp_beq_sort _ _ _] - simp only [Bool.false_eq_true, if_false, pure_bind, + simp only [Bool.false_eq_true, ite_false, pure_bind, normalizationRecMBind] rw [domainRun'] simp [TypeChecker.Inner.isDefEqForall, TypeChecker.Inner.isDefEq, Expr.hasLooseBVars, @@ -8814,7 +8814,7 @@ private theorem annotatedPiInnerView_isDefEqInner : (.const ``AnnotatedPi []) .default) = false rw [Expr.eqv_eq] rfl] - simp only [Bool.false_eq_true, if_false, normalizationRecMBind] + simp only [Bool.false_eq_true, ite_false, normalizationRecMBind] rw [coreRun] exact ⟨_, rfl⟩ @@ -9711,7 +9711,7 @@ private theorem annotatedPiPreFamilySafetyRun : annotatedPiInductiveStats 0 (.sort (.succ .zero)) nestedContext (.const ``AnnotatedPi []) 999 = .ok targetTrace := by simp only [AddInductive.ConstructorPreFamilyRecursiveTrace.build] - rw [dif_pos valid, nestedTargetSpineRun] + rw [dite_eq_left valid, nestedTargetSpineRun] rfl obtain ⟨recursiveTailTrace, recursiveTailRun⟩ : ∃ recursiveTailTrace : @@ -9751,7 +9751,7 @@ private theorem annotatedPiPreFamilySafetyRun : simp only [Bind.bind, Except.bind] rw [annotations.observe_eq] simp only [] - rw [dif_pos rootFresh] + rw [dite_eq_left rootFresh] rw [recursiveTailRun] rfl have resultIndependent : AddInductive.constructorIndependentOf @@ -9785,7 +9785,7 @@ private theorem annotatedPiPreFamilySafetyRun : [annotatedPiFamilyCandidateContext.freshFVarId] true 999 = .ok terminalTrace := by simp only [AddInductive.ConstructorPreFamilyViewTrace.build] - rw [dif_pos valid, dif_pos resultIndependent, resultTargetSpineRun] + rw [dite_eq_left valid, dite_eq_left resultIndependent, resultTargetSpineRun] rfl obtain ⟨viewTailTrace, viewTailRun⟩ : ∃ viewTailTrace : AddInductive.ConstructorPreFamilyViewTrace @@ -9833,10 +9833,10 @@ private theorem annotatedPiPreFamilySafetyRun : · rename_i nonrecursive rw [recursive] at nonrecursive contradiction - · rw [dif_pos fieldIndependent] + · rw [dite_eq_left fieldIndependent] rw [recursiveRun] simp only [Bind.bind, Except.bind] - rw [dif_pos rootFresh] + rw [dite_eq_left rootFresh] rw [viewTailRun] rfl have candidateViewEq : annotatedPiConstructorCandidate.type.view = @@ -9890,7 +9890,7 @@ private theorem annotatedPiPreFamilySafetyRun : annotatedPiDomainCandidateTrace, annotatedPiInnerBodyCandidateTrace, annotatedPiOuterBodyCandidateTrace, annotatedPiConst_abstract_singleton] - rw [if_pos translationUnique] + rw [ite_eq_left translationUnique] rw [parametersRun] simp only [Bind.bind, Except.bind] rw [listRun] diff --git a/Lean4Lean/Verify/Expr.lean b/Lean4Lean/Verify/Expr.lean index 02aaeef..0cc85a7 100644 --- a/Lean4Lean/Verify/Expr.lean +++ b/Lean4Lean/Verify/Expr.lean @@ -281,7 +281,7 @@ private theorem mkData_flags (H : br ≤ 2 ^ 20 - 1) : (mkData h br d fv ev lv lp).hasExprMVar = ev ∧ (mkData h br d fv ev lv lp).hasLevelMVar = lv ∧ (mkData h br d fv ev lv lp).hasLevelParam = lp := by - rw [mkData_eq, mkData', if_pos H] + rw [mkData_eq, mkData', ite_eq_left H] rw [Data.hasFVar_eq_getLsbD, Data.hasExprMVar_eq_getLsbD, Data.hasLevelMVar_eq_getLsbD, Data.hasLevelParam_eq_getLsbD] have hh : h.toUInt32.toUInt64.toBitVec ≤ 0xffffffff#64 := @@ -432,7 +432,7 @@ private theorem mkData_flags_of_false (br d h) : (mkData h br d false false false false).hasLevelParam = false := by by_cases H : br ≤ 2 ^ 20 - 1 · exact mkData_flags H - · rw [mkData_eq, mkData', if_neg H] + · rw [mkData_eq, mkData', ite_eq_right H] exact ⟨rfl, rfl, rfl, rfl⟩ private theorem mkData_hasFVar_of_false (br d h) : @@ -461,7 +461,7 @@ private theorem mkAppData_flag (i : Nat) (hi : i < 4) : (Nat.pow 2 20 - 1).toUInt32 := by dsimp +instances [instMaxUInt32, maxOfLe] split <;> exact Data.looseBVarRange_le - rw [mkAppData_eq, mkAppData', if_pos hm] + rw [mkAppData_eq, mkAppData', ite_eq_left hm] generalize (mixHash fData aData).toUInt32 = hash have : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 := by omega rcases this with rfl | rfl | rfl | rfl @@ -686,7 +686,7 @@ attribute [local reducible] Data theorem mkData_looseBVarRange (H : br ≤ 2^20 - 1) : (mkData h br d fv ev lv lp).looseBVarRange.toNat = br := by - rw [mkData_eq, mkData', if_pos H]; dsimp only [Data.looseBVarRange, -Nat.reducePow] + rw [mkData_eq, mkData', ite_eq_left H]; dsimp only [Data.looseBVarRange, -Nat.reducePow] have : br.toUInt64.toUInt32.toNat = br := by simp; omega refine .trans ?_ this; congr 2 refine UInt64.eq_of_toBitVec_eq ?_ @@ -718,7 +718,7 @@ theorem mkAppData_looseBVarRange : (mkAppData fData aData).looseBVarRange = max fData.looseBVarRange aData.looseBVarRange := by have hm : max fData.looseBVarRange aData.looseBVarRange ≤ (Nat.pow 2 20 - 1).toUInt32 := by dsimp +instances [instMaxUInt32, maxOfLe]; split <;> exact Data.looseBVarRange_le - rw [mkAppData_eq, mkAppData', if_pos hm] + rw [mkAppData_eq, mkAppData', ite_eq_left hm] simp [Data.looseBVarRange] at hm dsimp only [Data.looseBVarRange, -Nat.reducePow] generalize (max .. : UInt32) = m at * @@ -905,15 +905,15 @@ theorem liftLooseBVars_liftLooseBVars {e : Expr} {n1 n2 k1 k2 : Nat} induction e generalizing k1 k2 with simp [liftLooseBVars', ← Nat.add_assoc, *] | bvar i => split <;> rename_i h - · rw [if_pos (Nat.lt_of_lt_of_le h h1)] - · rw [if_neg (by omega), Nat.add_assoc] + · rw [ite_eq_left (Nat.lt_of_lt_of_le h h1)] + · rw [ite_eq_right (by omega), Nat.add_assoc] theorem liftLooseBVars_add {e : Expr} {n1 n2 k : Nat} : liftLooseBVars' (liftLooseBVars' e k n1) k n2 = liftLooseBVars' e k (n1+n2) := by induction e generalizing k with simp [liftLooseBVars', *] | bvar i => split; · rfl - rw [if_neg (by omega), Nat.add_assoc] + rw [ite_eq_right (by omega), Nat.add_assoc] theorem liftLooseBVars_comm (e : Expr) (n1 n2 k1 k2 : Nat) (h : k2 ≤ k1) : liftLooseBVars' (liftLooseBVars' e k1 n1) k2 n2 = @@ -922,11 +922,11 @@ theorem liftLooseBVars_comm (e : Expr) (n1 n2 k1 k2 : Nat) (h : k2 ≤ k1) : simp [liftLooseBVars', Nat.add_assoc, Nat.succ_le_succ, *] | bvar i => split <;> rename_i h' - · rw [if_pos (c := _ < n2 + k1)]; split + · rw [ite_eq_left (c := _ < n2 + k1)]; split · exact Nat.lt_add_left _ h' · omega · have := mt (Nat.lt_of_lt_of_le · h) h' - rw [if_neg (by omega), if_neg this, if_neg (by omega), Nat.add_right_comm] + rw [ite_eq_right (by omega), ite_eq_right this, ite_eq_right (by omega), Nat.add_right_comm] theorem liftLooseBVars_looseBVarRange : (liftLooseBVars' e k n).looseBVarRange' ≤ e.looseBVarRange' + n := by @@ -967,7 +967,7 @@ theorem instantiate1'_liftLooseBVars : induction e generalizing s <;> simp [*, instantiate1', liftLooseBVars', Nat.add_right_comm _ _ 1] rename_i i; split; · simp; omega - · rw [if_neg (by omega), if_neg (by omega)]; rfl + · rw [ite_eq_right (by omega), ite_eq_right (by omega)]; rfl theorem instantiate1'_liftLooseBVars_0 (e1 e2 : Expr) : instantiate1' (liftLooseBVars' e1 k 1) e2 k = e1 := by @@ -989,7 +989,7 @@ theorem instantiate1'_instantiate1' (e1 e2 e3 j) : simp [instantiate1', h1, h1', Nat.lt_of_succ_lt_succ h] split <;> rename_i h' · subst i - rw [if_neg (by omega), if_neg (by omega)] + rw [ite_eq_right (by omega), ite_eq_right (by omega)] simp [instantiate1'] suffices liftLooseBVars' _ _ (j+1) = _ by rw [this]; exact instantiate1'_liftLooseBVars_0 .. @@ -998,9 +998,9 @@ theorem instantiate1'_instantiate1' (e1 e2 e3 j) : let i+1 := i have hk := Nat.lt_of_add_lt_add_right hk simp [instantiate1'] - rw [if_neg (by omega), if_neg (by omega), if_neg (by omega), if_neg (by omega)] + rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega)] simp [instantiate1'] - rw [if_neg (Nat.lt_asymm hk), if_neg (Nat.ne_of_gt hk)] + rw [ite_eq_right (Nat.lt_asymm hk), ite_eq_right (Nat.ne_of_gt hk)] @[simp] def instantiateRevList (e : Expr) : List Expr → (k :_:= 0) → Expr | [], _ => e @@ -1101,7 +1101,7 @@ theorem abstract1_comm {e : Expr} {k} (h : a ≠ b) : abstract1 a (abstract1 b e k) k = abstract1 b (abstract1 a e k) (k+1) := by induction e generalizing k with simp_all [abstract1] - | bvar => split <;> [rw [if_pos]; simp [*]] <;> omega + | bvar => split <;> [rw [ite_eq_left]; simp [*]] <;> omega | fvar => split <;> split <;> simp_all [abstract1] theorem abstract1_abstractList {e : Expr} {as : List FVarId} {k} (H : a ∉ as) : @@ -1148,7 +1148,7 @@ theorem abstract1_eq_liftLooseBVars (h : (abstract1 a e k).hasLooseBVar' k = fal theorem lowerLooseBVars_eq_instantiate (h : e.hasLooseBVar' k = false) : e.lowerLooseBVars' (k + 1) 1 = instantiate1' e v k := by induction e generalizing k with simp_all [hasLooseBVar', lowerLooseBVars', instantiate1'] - | bvar j => split <;> [rw [if_pos (by omega)]; rw [if_neg (by omega)]] + | bvar j => split <;> [rw [ite_eq_left (by omega)]; rw [ite_eq_right (by omega)]] theorem hasLooseBVar_of_ge_looseBVarRange {e : Expr} (h : e.looseBVarRange' ≤ k) : e.hasLooseBVar' k = false := by @@ -1161,12 +1161,12 @@ theorem abstract1_lower {e : Expr} (h : e.hasLooseBVar' k₁ = false) (hk : k₁ induction e generalizing k₁ k₂ with simp_all [abstract1, lowerLooseBVars', hasLooseBVar'] | bvar i => split <;> [skip; split] - · rw [if_pos (c := i < k₂ + 1) (by omega), if_pos (by omega)]; simp [*] - · rw [if_pos (c := i < _) (by omega)]; simp [*] - · rw [if_neg (c := i < _) (by omega), if_neg (by omega)]; omega + · rw [ite_eq_left (c := i < k₂ + 1) (by omega), ite_eq_left (by omega)]; simp [*] + · rw [ite_eq_left (c := i < _) (by omega)]; simp [*] + · rw [ite_eq_right (c := i < _) (by omega), ite_eq_right (by omega)]; omega | fvar b => split <;> simp [lowerLooseBVars', -right_eq_ite_iff] - rw [if_neg (by omega)] + rw [ite_eq_right (by omega)] variable (red : Bool) (s : Name → Level) in def instantiateLevelParamsCore' : Expr → Expr diff --git a/Lean4Lean/Verify/Level.lean b/Lean4Lean/Verify/Level.lean index 095c602..c1d5d9f 100644 --- a/Lean4Lean/Verify/Level.lean +++ b/Lean4Lean/Verify/Level.lean @@ -39,7 +39,7 @@ set_option allowUnsafeReducibility true attribute [local reducible] Data theorem mkData_depth (H : d < 2 ^ 24) : (mkData h d hmv hp).depth.toNat = d := by - rw [mkData_eq, mkData', if_neg (Nat.not_lt.2 (Nat.le_sub_one_of_lt H)), Data.depth] + rw [mkData_eq, mkData', ite_eq_right (Nat.not_lt.2 (Nat.le_sub_one_of_lt H)), Data.depth] have : d.toUInt64.toUInt32.toNat = d := by simp; omega refine .trans ?_ this; congr 2 rw [← UInt64.toBitVec_inj] @@ -56,7 +56,7 @@ theorem mkData_depth (H : d < 2 ^ 24) : (mkData h d hmv hp).depth.toNat = d := b bv_decide theorem mkData_hasParam (H : d < 2 ^ 24) : (mkData h d hmv hp).hasParam = hp := by - rw [mkData_eq, mkData', if_neg (Nat.not_lt.2 (Nat.le_sub_one_of_lt H))] + rw [mkData_eq, mkData', ite_eq_right (Nat.not_lt.2 (Nat.le_sub_one_of_lt H))] simp [Data.hasParam, (· == ·), ← UInt64.toBitVec_inj] have : h.toUInt32.toUInt64.toBitVec ≤ 0xffffffff#64 := Nat.le_of_lt_succ h.toUInt32.1.1.2 have hb : ∀ (b : Bool), b.toUInt64.toBitVec ≤ 1#64 := by decide @@ -71,7 +71,7 @@ theorem mkData_hasParam (H : d < 2 ^ 24) : (mkData h d hmv hp).hasParam = hp := cases hp <;> decide theorem mkData_hasMVar (H : d < 2 ^ 24) : (mkData h d hmv hp).hasMVar = hmv := by - rw [mkData_eq, mkData', if_neg (Nat.not_lt.2 (Nat.le_sub_one_of_lt H))] + rw [mkData_eq, mkData', ite_eq_right (Nat.not_lt.2 (Nat.le_sub_one_of_lt H))] simp [Data.hasMVar, (· == ·), ← UInt64.toBitVec_inj] have : h.toUInt32.toUInt64.toBitVec ≤ 0xffffffff#64 := Nat.le_of_lt_succ h.toUInt32.1.1.2 have hb : ∀ (b : Bool), b.toUInt64.toBitVec ≤ 1#64 := by decide @@ -235,7 +235,7 @@ def evalParam (x : Name) : Nat := let i := ls.idxOf x; if i < ls.length then ρ[i]?.getD 0 else 0 theorem evalParam_eq (hv : ls.idxOf x < ls.length) : - evalParam ls ρ x = ρ[List.idxOf x ls]?.getD 0 := if_pos hv + evalParam ls ρ x = ρ[List.idxOf x ls]?.getD 0 := ite_eq_left hv variable (ls : List Name) (ρ : List Nat) in def VarNode.eval (l : VarNode) : Nat := evalParam ls ρ l.var + l.offset @@ -520,7 +520,7 @@ theorem NormLevel.addConst_eval (H : path = [] ∨ acc.contains path) (wf : acc. obtain ⟨hc, hv⟩ := this _ rfl nz exact ⟨Nat.le_trans (Nat.le_max_right ..) hc, hv⟩ · exact this _ h nz - · have := H path; rw [if_pos rfl] at this; split at this <;> + · have := H path; rw [ite_eq_left rfl] at this; split at this <;> refine Nat.le_trans ?_ ((this _ rfl nz).1) · exact Nat.le_refl _ · exact Nat.le_max_left .. @@ -1145,13 +1145,13 @@ theorem NormLevel.subsumption_covers {s : NormLevel} : cases h₀.symm.trans h₁ by_cases hmin : y ∈ (acc.minimize q n₁).var · refine ⟨q, _, y, ?_, hmin, e, hqp⟩ - rw [subsumption_step_get?, if_pos rfl, if_neg] + rw [subsumption_step_get?, ite_eq_left rfl, ite_eq_right] simp only [Node.isEmpty, Bool.and_eq_true, List.isEmpty_iff, not_and] rintro - he; simp [he] at hmin · obtain ⟨p₂, n₂, z, h₂, hz, e₂, hne, hp₂⟩ := minimize_var_dominated (hy₀ _ hy) hmin - exact ⟨p₂, n₂, z, by rw [subsumption_step_get?, if_neg (Ne.symm hne)]; exact h₂, + exact ⟨p₂, n₂, z, by rw [subsumption_step_get?, ite_eq_right (Ne.symm hne)]; exact h₂, hz, e₂.trans e, fun w hw => hqp _ (hp₂ _ hw)⟩ - · exact ⟨q, m, y, by rw [subsumption_step_get?, if_neg (Ne.symm hqp₁)]; exact hq, + · exact ⟨q, m, y, by rw [subsumption_step_get?, ite_eq_right (Ne.symm hqp₁)]; exact hq, hy, e, hqp⟩ theorem NormLevel.subsumption_eval {s : NormLevel} (wf : s.WF) : @@ -1186,12 +1186,12 @@ theorem NormLevel.subsumption_eval {s : NormLevel} (wf : s.WF) : · simp [Node.isEmpty, List.isEmpty_iff] at he; simp [Node.eval, he.1, he.2] · have hget : (if (acc.minimize p₁ n₁).isEmpty then acc.erase p₁ else acc.insert p₁ (acc.minimize p₁ n₁)).get? p₁ = some (acc.minimize p₁ n₁) := by - rw [hins p₁, if_pos rfl, if_neg he] + rw [hins p₁, ite_eq_left rfl, ite_eq_right he] have := H _ _ hget rw [evalPath_le] at this; exact this nz refine ih _ nd.2 (fun p n h => ?_) (fun p n h v hv => ?_) ((ext_le fun m => ?_).trans eq) · have hne : p₁ ≠ p := fun e => nd.1 (by rw [e]; exact List.mem_map_of_mem h) - exact (hins p).trans (if_neg hne) ▸ hl _ _ (.tail _ h) + exact (hins p).trans (ite_eq_right hne) ▸ hl _ _ (.tail _ h) · rw [hins p] at h; split at h · split at h <;> [cases h; skip] cases h; rename_i hp _; subst hp @@ -1202,8 +1202,8 @@ theorem NormLevel.subsumption_eval {s : NormLevel} (wf : s.WF) : · subst hp; cases h₁.symm.trans h refine evalPath_le.2 fun nz => ?_ refine (minimize_eval_iff wfa h₁ (fun q nq hne hq => ?_) nz).1 (hmin_le _ H nz) - exact H _ _ ((hins q).trans (if_neg hne.symm) ▸ hq) - · exact H p n ((hins p).trans (if_neg (Ne.symm hp)) ▸ h) + exact H _ _ ((hins q).trans (ite_eq_right hne.symm) ▸ hq) + · exact H p n ((hins p).trans (ite_eq_right (Ne.symm hp)) ▸ h) · rw [hins p] at h; split at h <;> [skip; exact H _ _ h] split at h <;> [cases h; skip] cases h; rename_i hp _; subst hp @@ -1392,7 +1392,7 @@ theorem Tree.reifyChild_ge {const : Nat} : ∀ child : List (Name × Tree), -- either this child is the witness, in which case it is emitted as `n + const`, or the -- witness is further down and the fold maxes its value in obtain h | h := h - · rw [h]; dsimp only; rw [if_pos (Nat.le_refl const)] + · rw [h]; dsimp only; rw [ite_eq_left (Nat.le_refl const)] simp only [evalOpt_some, eval_mkMax, eval_addOffset, Level.eval] omega · have ih := reifyChild_ge (ls := ls) (ρ := ρ) (μ := μ) child h @@ -2631,7 +2631,7 @@ theorem evalParam_map {f : Name → Nat} (hx : x ∈ ls) : evalParam ls (ls.map theorem evalParam_not_mem (hx : x ∉ ls) : evalParam ls ρ x = 0 := by simp only [evalParam] - rw [if_neg fun h => hx (List.idxOf_lt_length_iff.1 h)] + rw [ite_eq_right fun h => hx (List.idxOf_lt_length_iff.1 h)] theorem evalParam_map_pos {f : Name → Nat} (h : 0 < evalParam ls (ls.map f) z) : z ∈ ls ∧ 0 < f z := by @@ -2741,7 +2741,7 @@ theorem NormLevel.separation {l₁ l₂ : NormLevel} · have hoff := (bound_spec hq).2 _ hv have hev : evalParam ls (ls.map fun z => if z = x then l₂.bound + k + 2 else if z ∈ p then 1 else 0) v.var ≤ 1 := - evalParam_map_le (by rw [if_neg hvx]; split <;> omega) + evalParam_map_le (by rw [ite_eq_right hvx]; split <;> omega) simp only [VarNode.eval] at hvlt exact absurd hvlt (by omega) @@ -2990,7 +2990,7 @@ theorem VarNode.find?_addVar {vs : List VarNode} {x y : Name} {k : Nat} (hvs : V · rw [List.find?_cons_of_neg (by simp [h]), List.find?_cons_of_neg (by simp [← e, h])] · have hne := name_lt_ne (Std.OrientedCmp.lt_of_gt hc) by_cases hy : w.var = y - · rw [if_neg (hy ▸ hne.symm), List.find?_cons_of_pos (by simp [hy]), + · rw [ite_eq_right (hy ▸ hne.symm), List.find?_cons_of_pos (by simp [hy]), List.find?_cons_of_pos (by simp [hy])] · rw [List.find?_cons_of_neg (by simp [hy]), ih hvs.of_cons, List.find?_cons_of_neg (by simp [hne]), List.find?_cons_of_neg (by simp [hy])] @@ -2999,9 +2999,9 @@ theorem NormLevel.addConst_flat {s : NormLevel} {c k : Nat} {vs : List VarNode} (h : s.Flat c vs) : (addConst k [] s).Flat (Nat.max c k) vs := by by_cases hk : k = 0 · subst hk - rw [show Nat.max c 0 = c from Nat.max_zero c, NormLevel.addConst, if_pos (by simp)] + rw [show Nat.max c 0 = c from Nat.max_zero c, NormLevel.addConst, ite_eq_left (by simp)] exact h - · rw [NormLevel.addConst, if_neg (by simp [hk])] + · rw [NormLevel.addConst, ite_eq_right (by simp [hk])] intro p rw [Std.TreeMap.get?_eq_getElem?, Std.TreeMap.getElem?_alter] have hmax : ¬Nat.max c k = 0 := by simp only [Nat.max_eq_zero_iff]; simp [hk] @@ -3011,8 +3011,8 @@ theorem NormLevel.addConst_flat {s : NormLevel} {c k : Nat} {vs : List VarNode} simp only [flatGet] by_cases hc0 : c = 0 · subst hc0 - rw [if_pos rfl, if_neg hmax, show Nat.max 0 k = k from Nat.zero_max k] - · rw [if_neg hc0, if_neg hmax, show Nat.max c k = Nat.max k c from Nat.max_comm c k] + rw [ite_eq_left rfl, ite_eq_right hmax, show Nat.max 0 k = k from Nat.zero_max k] + · rw [ite_eq_right hc0, ite_eq_right hmax, show Nat.max c k = Nat.max k c from Nat.max_comm c k] · rw [← Std.TreeMap.get?_eq_getElem?, h p] match p with | [] => cases he Std.ReflOrd.compare_self @@ -3028,7 +3028,7 @@ theorem NormLevel.addNode_flat {s : NormLevel} {c k : Nat} {vs : List VarNode} { subst hp rw [← Std.TreeMap.get?_eq_getElem?, h [x]] simp only [flatGet] - rw [VarNode.find?_addVar hvs, if_pos rfl] + rw [VarNode.find?_addVar hvs, ite_eq_left rfl] match hfd : vs.find? (·.var == x) with | none => rw [hfd]; rfl | some v => @@ -3043,7 +3043,7 @@ theorem NormLevel.addNode_flat {s : NormLevel} {c k : Nat} {vs : List VarNode} { | [y] => have hxy : x ≠ y := by rintro rfl; exact he Std.ReflOrd.compare_self simp only [flatGet] - rw [VarNode.find?_addVar hvs, if_neg hxy] + rw [VarNode.find?_addVar hvs, ite_eq_right hxy] | _ :: _ :: _ => rfl /-- The entries of a flat map: the root carries the constant (and is absent when it is zero), @@ -3124,7 +3124,7 @@ theorem NormLevel.subsumption_flat {s : NormLevel} {c : Nat} {vs : List VarNode} · simp [Node.isEmpty, hc0] · simp [Node.isEmpty] rw [NormLevel.subsumption_step_get?, hmin acc hacc p₁ n₁ h₁, hne] - simp only [Bool.false_eq_true, if_false] + simp only [Bool.false_eq_true, ite_false] split <;> rename_i hp · subst hp; exact h₁.symm · exact hacc p @@ -3221,16 +3221,16 @@ theorem normalizeAux_congr {A B : NormLevel} (h : ∀ p, A.get? p = B.get? p) (u show (if k = 0 then acc else NormLevel.addVar v k path acc).get? p = (if k = 0 then B else NormLevel.addVar v k path B).get? p by_cases hk : k = 0 - · simp only [if_pos hk]; exact h p - · simp only [if_neg hk]; exact NormLevel.addVar_congr h v k path p + · simp only [ite_eq_left hk]; exact h p + · simp only [ite_eq_right hk]; exact NormLevel.addVar_congr h v k path p | case10 path k acc a => simp only [normalizeAux]; exact h | case11 path k acc a b => simp only [normalizeAux]; exact h | case12 path k acc v path' he => simp only [normalizeAux, he] exact NormLevel.addNode_congr (NormLevel.addConst_congr h k path) v k path' - | case13 path acc v he => simp only [normalizeAux, he, if_pos]; exact h + | case13 path acc v he => simp only [normalizeAux, he, ite_eq_left]; exact h | case14 path k acc v he hk => - simp only [normalizeAux, he, if_neg hk] + simp only [normalizeAux, he, ite_eq_right hk] exact NormLevel.addVar_congr h v k path theorem NormLevel.subsumption_congr {A B : NormLevel} (h : ∀ p, A.get? p = B.get? p) : @@ -3334,14 +3334,14 @@ private theorem NormLevel.Flat.toList {s : NormLevel} {c : Nat} {vs : List VarNo · intro x hx y hy by_cases hc0 : c = 0 · simp [hc0] at hx - · rw [if_neg hc0, List.mem_singleton] at hx + · rw [ite_eq_right hc0, List.mem_singleton] at hx subst hx obtain ⟨w, -, rfl⟩ := List.mem_map.1 hy exact compare_nil_cons · rw [Std.TreeMap.mem_toList_iff_getElem?_eq_some, ← Std.TreeMap.get?_eq_getElem?, h p] constructor <;> intro hp · obtain ⟨rfl, rfl, hc0⟩ | ⟨v, hv, rfl, rfl⟩ := flatGet_eq_some hp - · exact List.mem_append_left _ (by rw [if_neg hc0]; exact List.mem_singleton.2 rfl) + · exact List.mem_append_left _ (by rw [ite_eq_right hc0]; exact List.mem_singleton.2 rfl) · exact List.mem_append_right _ (List.mem_map.2 ⟨v, hv, rfl⟩) · obtain hp | hp := List.mem_append.1 hp · split at hp <;> [cases hp; rename_i hc] @@ -3374,8 +3374,8 @@ theorem NormLevel.Flat.toTree {s : NormLevel} {c : Nat} {vs : List VarNode} have key := flat_toTree_fold s c [] vs [] hvs (fun v => NormLevel.Flat.lexChain_singleton hvs h) (by simp) by_cases hc0 : c = 0 - · subst hc0; rw [if_pos rfl]; exact key - · rw [if_neg hc0]; exact key + · subst hc0; rw [ite_eq_left rfl]; exact key + · rw [ite_eq_right hc0]; exact key /-- The sublevels of a single node keyed at `p`. -/ def Node.HasSub (p : List Name) (n : Node) : Sub → Prop @@ -3460,7 +3460,7 @@ theorem NormLevel.minimize_exact_aux {acc : NormLevel} {p₁ : List Name} {n₁ obtain ⟨hsub, hlek⟩ := hle have hgate : subset compare p₂ p₁ := subset_of_sorted hs₂ hs₁ hsub have hsu : Node.subsume p₁ n p₂ n₂ = n.subsumeBy (p₁.length == p₂.length) n₂ := by - rw [Node.subsume, if_pos hgate] + rw [Node.subsume, ite_eq_left hgate] by_cases hlen : p₁.length = p₂.length · have hqq : p₂ = p₁ := subset_eq hgate hlen.symm have hn₂ : n₂ = n₁ := by @@ -3487,7 +3487,7 @@ theorem NormLevel.minimize_exact_aux {acc : NormLevel} {p₁ : List Name} {n₁ obtain ⟨hsub, hlek⟩ := hle have hgate : subset compare p₂ p₁ := subset_of_sorted hs₂ hs₁ hsub have hsu : Node.subsume p₁ n p₂ n₂ = n.subsumeBy (p₁.length == p₂.length) n₂ := by - rw [Node.subsume, if_pos hgate] + rw [Node.subsume, ite_eq_left hgate] rw [hsu] at hck have hkc : n.const = k := by obtain hc | hc := Node.subsumeBy_const_cases (same := p₁.length == p₂.length) n n₂ @@ -3504,7 +3504,7 @@ theorem NormLevel.minimize_exact_aux {acc : NormLevel} {p₁ : List Name} {n₁ obtain ⟨hsub, rfl, hlek⟩ := hle have hgate : subset compare p₂ p₁ := subset_of_sorted hs₂ hs₁ hsub have hsu : Node.subsume p₁ n p₂ n₂ = n.subsumeBy (p₁.length == p₂.length) n₂ := by - rw [Node.subsume, if_pos hgate] + rw [Node.subsume, ite_eq_left hgate] by_cases hlen : p₁.length = p₂.length · have hqq : p₂ = p₁ := subset_eq hgate hlen.symm have hn₂ : n₂ = n₁ := by @@ -3578,7 +3578,7 @@ theorem NormLevel.subsumption_reduced {s : NormLevel} refine ih _ nd.2 (fun pn' h => ?_) (fun p n h => ?_) (fun p n h => ?_) (fun p n hp hnp t t' hnt ht' hle => ?_) · have hne : p₂ ≠ pn'.1 := fun e => nd.1 (e ▸ List.mem_map_of_mem (f := Prod.fst) h) - rw [hstep, if_neg hne] + rw [hstep, ite_eq_right hne] exact hl _ (.tail _ h) · rw [hstep] at h; split at h <;> rename_i hpe · split at h <;> [cases h; skip] diff --git a/Lean4Lean/Verify/LevelStd.lean b/Lean4Lean/Verify/LevelStd.lean index ca30d7d..3e4e5b9 100644 --- a/Lean4Lean/Verify/LevelStd.lean +++ b/Lean4Lean/Verify/LevelStd.lean @@ -285,7 +285,7 @@ theorem eval_mkMaxAux {lvls : Array Level} | zero => have hie : i = lvls.size := by omega obtain ⟨hp, hpk⟩ := hp (by omega) - rw [Total.mkMaxAux.eq_def, dif_neg (by omega), eval_accMax] + rw [Total.mkMaxAux.eq_def, dite_eq_right (by omega), eval_accMax] have hlast : i - 1 < lvls.size := by omega have hdrop : lvls.toList.drop (i-1) = [lvls[i-1]] := by rw [List.drop_eq_getElem_cons (by simp only [Array.length_toList]; omega)] @@ -487,7 +487,7 @@ theorem eval_normalize_total {l : Level} : eval ρ μ (Total.normalize l) = eval (by simp only [mkLevelMax, Total.size]; omega) rfl] have := isNeverZero_sound (ρ := ρ) (μ := μ) hnz simp only [mkLevelMax, eval, Nat.imax] - rw [if_neg (by omega)] + rw [ite_eq_right (by omega)] · rw [eval_addOffset, eval_mkIMaxAux, IH _ (by omega) rfl, IH _ (by omega) rfl]; rfl · grind [base_of_not_cheap] diff --git a/Lean4Lean/Verify/LocalContext.lean b/Lean4Lean/Verify/LocalContext.lean index 9617275..28660fb 100644 --- a/Lean4Lean/Verify/LocalContext.lean +++ b/Lean4Lean/Verify/LocalContext.lean @@ -302,7 +302,7 @@ theorem TrLCtx'.find?_of_mem (henv : env.WF) (H : TrLCtx' env Us ds Δ) h3.weakFV henv (.skip_fvar _ _ .refl) this · simpa [LocalDecl.type, VLocalDecl.type, VLocalDecl.depth] using h2.weakFV henv (.skip_fvar _ _ .refl) this - · simp at nd; rw [if_neg (by simpa using Ne.symm (nd.1 _ hm))]; simp + · simp at nd; rw [ite_eq_right (by simpa using Ne.symm (nd.1 _ hm))]; simp have ⟨_, _, h1, h2, h3, h4, h5⟩ := h1.find?_of_mem henv nd.2 hm refine ⟨_, _, ⟨_, _, h1, rfl, rfl⟩, fun _ h => h2 _ h.1, fun _ h => h3 _ h.1, ?_, ?_⟩ · simpa using h4.weakFV henv (.skip_fvar _ _ .refl) this diff --git a/Lean4Lean/Verify/NormLt.lean b/Lean4Lean/Verify/NormLt.lean index 446ee0f..65bbed6 100644 --- a/Lean4Lean/Verify/NormLt.lean +++ b/Lean4Lean/Verify/NormLt.lean @@ -278,14 +278,14 @@ private theorem normLtAux_eq : ∀ (l₁ : Level) (k₁ : Nat) (l₂ : Level) (k exact hns | case3 a b k₁ c d k₂ hbeq | case6 a b k₁ c d k₂ hbeq => -- the two levels are syntactically equal: the offsets decide - rw [normLtAux, if_pos hbeq, Bool.eq_iff_iff] + rw [normLtAux, ite_eq_left hbeq, Bool.eq_iff_iff] cases eq_of_beq hbeq show _ ↔ ((baseCmp _ _).then (compare (0 + k₁) (0 + k₂)) == _) rw [baseCmp_refl] simp only [decide_eq_true_eq, Ordering.then, Nat.zero_add, beq_iff_eq, Nat.compare_eq_lt] | case4 a b k₁ c d k₂ hbeq hne ih | case7 a b k₁ c d k₂ hbeq hne ih => -- the heads differ, so the head comparison decides - rw [normLtAux, if_neg (by simpa using hbeq), if_pos hne, ih] + rw [normLtAux, ite_eq_right (by simpa using hbeq), ite_eq_left hne, ih] have hne' : a ≠ c := by simpa using hne have hac : normCmp a c ≠ .eq := fun h => hne' (eq_of_normCmp_eq h) simp only [base_max, base_imax, off_max, off_imax, Nat.add_zero, Nat.zero_add] @@ -294,7 +294,7 @@ private theorem normLtAux_eq : ∀ (l₁ : Level) (k₁ : Nat) (l₂ : Level) (k cases h : normCmp a c <;> simp_all [Ordering.then] | case5 a b k₁ c d k₂ hbeq hne ih | case8 a b k₁ c d k₂ hbeq hne ih => -- the heads agree, so the tail comparison decides - rw [normLtAux, if_neg (by simpa using hbeq), if_neg hne, ih] + rw [normLtAux, ite_eq_right (by simpa using hbeq), ite_eq_right hne, ih] have hac : a = c := by simpa using hne subst hac have hne' : b ≠ d := by rintro rfl; exact absurd (by simp) hbeq @@ -305,19 +305,19 @@ private theorem normLtAux_eq : ∀ (l₁ : Level) (k₁ : Nat) (l₂ : Level) (k rw [normCmp_refl] cases h : normCmp b d <;> simp_all [Ordering.then] | case9 n₁ k₁ n₂ k₂ hbeq => - rw [normLtAux, if_pos hbeq, Bool.eq_iff_iff] + rw [normLtAux, ite_eq_left hbeq, Bool.eq_iff_iff] cases eq_of_beq hbeq show _ ↔ ((baseCmp (Level.param n₁) (Level.param n₁)).then (compare (0 + k₁) (0 + k₂)) == _) rw [baseCmp_refl] simp only [decide_eq_true_eq, Ordering.then, Nat.zero_add, beq_iff_eq, Nat.compare_eq_lt] | case11 n₁ k₁ n₂ k₂ hbeq => - rw [normLtAux, if_pos hbeq, Bool.eq_iff_iff] + rw [normLtAux, ite_eq_left hbeq, Bool.eq_iff_iff] cases eq_of_beq hbeq show _ ↔ ((baseCmp (Level.mvar n₁) (Level.mvar n₁)).then (compare (0 + k₁) (0 + k₂)) == _) rw [baseCmp_refl] simp only [decide_eq_true_eq, Ordering.then, Nat.zero_add, beq_iff_eq, Nat.compare_eq_lt] | case10 n₁ k₁ n₂ k₂ hbeq => - rw [normLtAux, if_neg hbeq] + rw [normLtAux, ite_eq_right hbeq] show _ = ((baseCmp (Level.param n₁) (Level.param n₂)).then (compare (0 + k₁) (0 + k₂)) == _) rw [baseCmp] @@ -325,7 +325,7 @@ private theorem normLtAux_eq : ∀ (l₁ : Level) (k₁ : Nat) (l₂ : Level) (k hbeq (LawfulBEqCmp.compare_eq_iff_beq.1 h) cases h : Name.cmp n₁ n₂ <;> simp_all [Name.lt, Ordering.then] | case12 n₁ k₁ n₂ k₂ hbeq => - rw [normLtAux, if_neg hbeq] + rw [normLtAux, ite_eq_right hbeq] show _ = ((baseCmp (Level.mvar n₁) (Level.mvar n₂)).then (compare (0 + k₁) (0 + k₂)) == _) rw [baseCmp] diff --git a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean index faff37e..8249e80 100644 --- a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean +++ b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean @@ -581,7 +581,7 @@ theorem tryEtaStructCore.WF_of_structureEta {c : VContext} {s : VState} simp only [bind_assoc] refine (isDefEq.WF hprojTr hargTr').bind fun b next _ hb => ?_ by_cases hbtrue : b = true - · simp only [hbtrue, if_pos, pure_bind] + · simp only [hbtrue, ite_eq_left, pure_bind] have hcur : FieldEq (i - ctorInfo.numParams) := ⟨fields[i - ctorInfo.numParams], code, List.getElem?_eq_getElem hj, hcode, hb hbtrue⟩ diff --git a/Lean4Lean/Verify/Typing/Lemmas.lean b/Lean4Lean/Verify/Typing/Lemmas.lean index 928c744..ffddc97 100644 --- a/Lean4Lean/Verify/Typing/Lemmas.lean +++ b/Lean4Lean/Verify/Typing/Lemmas.lean @@ -1862,16 +1862,16 @@ theorem TrExprS.abstract (W : VLCtx.Abstract Δ₀ v₀ d₀ dk k Δ₁ Δ) (H : induction H generalizing dk k Δ with | bvar h1 => exact .bvar <| (W.find? (by nofun)).trans <| by - simp; split <;> [skip; rw [if_neg (by omega), if_neg (by omega)]] <;> exact h1 + simp; split <;> [skip; rw [ite_eq_right (by omega), ite_eq_right (by omega)]] <;> exact h1 | @fvar _ _ _ fv h1 => if h : fv = v₀ then rw [h, W.find?_self] at h1; cases h1 - rw [Expr.abstract1, if_pos (by simp [h])] + rw [Expr.abstract1, ite_eq_left (by simp [h])] exact .bvar <| (W.find? (by nofun)).trans (by simpa using W.find?_self) else have := W.find? (v := .inr fv) (by rintro ⟨⟩; trivial) simp at this - rw [Expr.abstract1, if_neg] + rw [Expr.abstract1, ite_eq_right] · exact .fvar (this.trans h1) · simp; rintro rfl; trivial | sort h1 => exact .sort h1 @@ -2453,7 +2453,7 @@ theorem BetaReduce.cheapBetaReduce (hc : e.Closed) : BetaReduce e e.cheapBetaRed refine .mkAppList <| .inst_reduce hl₁ [] h1 (Expr.instantiateList_eq_self h3) split <;> [rename_i n; exact .refl] have hc := h1.closed hc.getAppFn - simp [Closed] at hc; rw [if_pos hc] + simp [Closed] at hc; rw [ite_eq_left hc] rw [Expr.mkAppRange_eq (l₂ := l₂) (l₃ := []) (by simp [eq]) rfl (by simp [← eq])] conv => lhs; rw [← e.mkAppList_getAppArgsList] simp [eqr]