From 46db59d1d9aa8091728729be13b598a143cda0fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jun 2024 06:43:46 +0200 Subject: [PATCH] fix: `split` (for `if`-expressions) should work on non-propositional goals (#4349) Remark: when splitting an `if-then-else` term, the subgoals now have tags `isTrue` and `isFalse` instead of `inl` and `inr`. closes #4313 --------- Co-authored-by: Mario Carneiro --- src/Init/Data/AC.lean | 12 ++++++------ src/Init/Data/Array/DecidableEq.lean | 8 ++++---- src/Init/Data/BitVec/Lemmas.lean | 4 ++-- src/Init/Data/Int/DivModLemmas.lean | 8 ++++---- src/Init/System/IO.lean | 5 +---- src/Lean/Meta/Tactic/Cases.lean | 11 +++++++++++ src/Lean/Meta/Tactic/SplitIf.lean | 13 +++++++------ src/lake/Lake/Util/Compare.lean | 10 +++++++--- tests/lean/run/4313.lean | 27 +++++++++++++++++++++++++++ 9 files changed, 69 insertions(+), 29 deletions(-) create mode 100644 tests/lean/run/4313.lean diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean index ffae0489a5..0f7c240c43 100644 --- a/src/Init/Data/AC.lean +++ b/src/Init/Data/AC.lean @@ -146,8 +146,8 @@ theorem Context.evalList_mergeIdem (ctx : Context α) (h : ContextInformation.is | nil => simp [mergeIdem, mergeIdem.loop] split - case inl h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp] - rfl + next h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp] + next => rfl | cons z zs => by_cases h₂ : x = y case pos => @@ -191,11 +191,11 @@ theorem Context.evalList_insert . simp [evalList, h.1, EvalInformation.evalOp] | step y z zs ih => simp [insert] at *; split - case inl => rfl - case inr => + next => rfl + next => split - case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] - case inr => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] + next => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] + next => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] theorem Context.evalList_sort_congr (ctx : Context α) diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index 5ca1b8cf48..7927202f4d 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -27,17 +27,17 @@ decreasing_by decreasing_trivial_pre_omega theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by simp [Array.isEqv] split - case inr => intro; contradiction - case inl hsz => + next hsz => intro h have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _ + next => intro; contradiction theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i = true := by unfold Array.isEqvAux split - case inl h => simp [h, isEqvAux_self a (i+1)] - case inr h => simp [h] + next h => simp [h, isEqvAux_self a (i+1)] + next h => simp [h] termination_by a.size - i decreasing_by decreasing_trivial_pre_omega diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 27398f8200..be6b55ec89 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -244,10 +244,10 @@ theorem toInt_eq_msb_cond (x : BitVec w) : theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by simp only [toInt_eq_toNat_cond] split - case inl g => + next g => rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel] omega - case inr g => + next g => rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel] omega diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index a86717a575..be5fef7131 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1075,9 +1075,9 @@ theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n * y) n = Int.bmo theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by rw [bmod_def x n] split - case inl p => + next p => simp only [emod_add_bmod_congr] - case inr p => + next p => rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg] simp @@ -1088,9 +1088,9 @@ theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n theorem bmod_mul_bmod : Int.bmod (Int.bmod x n * y) n = Int.bmod (x * y) n := by rw [bmod_def x n] split - case inl p => + next p => simp - case inr p => + next p => rw [Int.sub_mul, Int.sub_eq_add_neg, ← Int.mul_neg] simp diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index c1b76378fe..7071b16a65 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -253,12 +253,9 @@ instance : ToString TaskState := ⟨TaskState.toString⟩ @[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α := return t.get -local macro "nonempty_list" : tactic => - `(tactic| exact Nat.zero_lt_succ _) - /-- Wait until any of the tasks in the given list has finished, then return its result. -/ @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α)) - (h : tasks.length > 0 := by nonempty_list) : BaseIO α := + (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α := return tasks[0].get /-- Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread. -/ diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index 52ee5ac4ed..36dfb280ad 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -323,6 +323,17 @@ def _root_.Lean.MVarId.byCases (mvarId : MVarId) (p : Expr) (hName : Name := `h) throwError "'byCases' tactic failed, unexpected number of subgoals" return ((← toByCasesSubgoal s₁), (← toByCasesSubgoal s₂)) +/-- +Given `dec : Decidable p`, split the goal in two subgoals: one containing the hypothesis `h : p` and another containing `h : ¬ p`. +-/ +def _root_.Lean.MVarId.byCasesDec (mvarId : MVarId) (p : Expr) (dec : Expr) (hName : Name := `h) : MetaM (ByCasesSubgoal × ByCasesSubgoal) := do + let mvarId ← mvarId.assert `hByCases (mkApp (mkConst ``Decidable) p) dec + let (fvarId, mvarId) ← mvarId.intro1 + let #[s₁, s₂] ← mvarId.cases fvarId #[{ varNames := [hName] }, { varNames := [hName] }] | + throwError "'byCasesDec' tactic failed, unexpected number of subgoals" + -- We flip `s₁` and `s₂` because `isFalse` is the first contructor. + return ((← toByCasesSubgoal s₂), (← toByCasesSubgoal s₁)) + builtin_initialize registerTraceClass `Meta.Tactic.cases end Lean.Meta diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean index 2dab6a5455..32d954df6f 100644 --- a/src/Lean/Meta/Tactic/SplitIf.lean +++ b/src/Lean/Meta/Tactic/SplitIf.lean @@ -68,23 +68,24 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge := def mkDischarge? (useDecide := false) : MetaM Simp.Discharge := return discharge? (← getLCtx).numIndices useDecide -/-- Return the condition of an `if` expression to case split. -/ -partial def findIfToSplit? (e : Expr) : Option Expr := +/-- Return the condition and decidable instance of an `if` expression to case split. -/ +private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) := if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then let cond := iteApp.getArg! 1 5 + let dec := iteApp.getArg! 2 5 -- Try to find a nested `if` in `cond` - findIfToSplit? cond |>.getD cond + findIfToSplit? cond |>.getD (cond, dec) else none def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do let e ← instantiateMVars e - if let some cond := findIfToSplit? e then + if let some (cond, decInst) := findIfToSplit? e then let hName ← match hName? with | none => mkFreshUserName `h | some hName => pure hName - trace[Meta.Tactic.splitIf] "splitting on {cond}" - return some (← mvarId.byCases cond hName) + trace[Meta.Tactic.splitIf] "splitting on {decInst}" + return some (← mvarId.byCasesDec cond decInst hName) else return none diff --git a/src/lake/Lake/Util/Compare.lean b/src/lake/Lake/Util/Compare.lean index a125964442..d0fab1a62a 100644 --- a/src/lake/Lake/Util/Compare.lean +++ b/src/lake/Lake/Util/Compare.lean @@ -51,9 +51,13 @@ instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α} [Decidable (a < a')] (h : compareOfLessAndEq a a' = .eq) : a = a' := by unfold compareOfLessAndEq at h - split at h; case inl => exact False.elim h - split at h; case inr => exact False.elim h - assumption + split at h + next => + exact False.elim h + next => + split at h + next => assumption + next => exact False.elim h theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α} [Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq := by diff --git a/tests/lean/run/4313.lean b/tests/lean/run/4313.lean new file mode 100644 index 0000000000..7f20536081 --- /dev/null +++ b/tests/lean/run/4313.lean @@ -0,0 +1,27 @@ +example {A B : Prop} {p : Prop} [Decidable p] (h : if p then A else B) : + A ∨ B := by + split at h + · exact .inl h + · exact .inr h + +example {A B : Type} {p : Prop} [Decidable p] (h : if p then A else B) : + Sum A B := by + split at h + · exact .inl h + · exact .inr h + +example {A B : Type} (h : match b with | true => A | false => B) : + Sum A B := by + split at h + · exact .inl h + · exact .inr h + +open Int in +theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by + rw [bmod_def x n] + split -- `split` now generates the more meaningful `isTrue` and `isFalse` tags. + case isTrue p => + simp only [emod_add_bmod_congr] + case isFalse p => + rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg] + simp