From 091754d3ffafb8c2abfbcda20e653916390efa7b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Nov 2024 17:46:41 -0800 Subject: [PATCH 01/23] fix: propagate `Simp.Config` when reducing terms and checking definitional equality in `simp` This PR ensures that the configuration in `Simp.Config` is used when reducing terms and checking definitional equality in `simp`. closes #5455 TODO: fix broken tests --- src/Lean/Meta/Tactic/Simp/Main.lean | 11 ++++++----- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 8 ++++---- src/Lean/Meta/Tactic/Simp/Types.lean | 7 ++++++- tests/lean/run/2670.lean | 17 +++++++++++++++-- tests/lean/run/5455.lean | 23 +++++++++++++++++++++++ tests/lean/run/heapSort.lean | 3 ++- 6 files changed, 56 insertions(+), 13 deletions(-) create mode 100644 tests/lean/run/5455.lean diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 2413b4be9d9a..f35de4eb6278 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -57,7 +57,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do match e? with | none => pure none | some e => - match (← reduceProj? e.getAppFn) with + match (← withSimpMetaConfig <| reduceProj? e.getAppFn) with | some f => return some (mkAppN f e.getAppArgs) | none => return none if projInfo.fromClass then @@ -152,7 +152,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do withDefault <| unfoldDefinition? e else if (← isMatchDef fName) then let some value ← withDefault <| unfoldDefinition? e | return none - let .reduced value ← reduceMatcher? value | return none + let .reduced value ← withSimpMetaConfig <| reduceMatcher? value | return none return some value else return none @@ -166,6 +166,7 @@ private def reduceStep (e : Expr) : SimpM Expr := do let f := e.getAppFn if f.isMVar then return (← instantiateMVars e) + withSimpMetaConfig do if cfg.beta then if f.isHeadBetaTargetFn false then return f.betaRev e.getAppRevArgs @@ -256,7 +257,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do withFreshCache do f def simpProj (e : Expr) : SimpM Result := do - match (← reduceProj? e) with + match (← withSimpMetaConfig <| reduceProj? e) with | some e => return { expr := e } | none => let s := e.projExpr! @@ -484,7 +485,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do let rhs := hType.appArg! rhs.withApp fun m zs => do let val ← mkLambdaFVars zs r.expr - unless (← isDefEq m val) do + unless (← withSimpMetaConfig <| isDefEq m val) do throwCongrHypothesisFailed let mut proof ← r.getProof if hType.isAppOf ``Iff then @@ -528,7 +529,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul let args := e.getAppArgs e := mkAppN e.getAppFn args[:numArgs] extraArgs := args[numArgs:].toArray - if (← isDefEq lhs e) then + if (← withSimpMetaConfig <| isDefEq lhs e) then let mut modified := false for i in c.hypothesesPos do let x := xs[i]! diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index b68829fa9bc6..906cb240540b 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -117,7 +117,7 @@ private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do recordTriedSimpTheorem thm.origin let rec go (e : Expr) : SimpM (Option Result) := do - if (← isDefEq lhs e) then + if (← withSimpMetaConfig <| isDefEq lhs e) then unless (← synthesizeArgs thm.origin bis xs) do return none let proof? ← if (← useImplicitDefEqProof thm) then @@ -342,7 +342,7 @@ def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do def simpMatch : Simproc := fun e => do unless (← getConfig).iota do return .continue - if let some e ← reduceRecMatcher? e then + if let some e ← withSimpMetaConfig <| reduceRecMatcher? e then return .visit { expr := e } let .const declName _ := e.getAppFn | return .continue @@ -549,7 +549,7 @@ private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do -- well-behaved discharger. See comment at `Methods.wellBehavedDischarge` else if !contextual && localDecl.index >= lctxInitIndices then return none - else if (← isDefEq e localDecl.type) then + else if (← withSimpMetaConfig <| isDefEq e localDecl.type) then return some localDecl.toExpr else return none @@ -591,7 +591,7 @@ def dischargeRfl (e : Expr) : SimpM (Option Expr) := do forallTelescope e fun xs e => do let some (t, a, b) := e.eq? | return .none unless a.getAppFn.isMVar || b.getAppFn.isMVar do return .none - if (← withReducible <| isDefEq a b) then + if (← withSimpMetaConfig <| isDefEq a b) then trace[Meta.Tactic.simp.discharge] "Discharging with rfl: {e}" let u ← getLevel t let proof := mkApp2 (.const ``rfl [u]) t a diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 786ea79c82f8..0e3fbae9ec35 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -131,7 +131,6 @@ private def mkIndexConfig (c : Config) : ConfigWithKey := /-- Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`. -/ --- TODO: use `metaConfig` at `isDefEq`. It is not being used yet because it will break Mathlib. private def mkMetaConfig (c : Config) : ConfigWithKey := { c with proj := if c.proj then .yesWithDelta else .no @@ -237,6 +236,12 @@ For example, if the user has set `simp (config := { zeta := false })`, @[inline] def withSimpIndexConfig (x : SimpM α) : SimpM α := do withConfigWithKey (← readThe Simp.Context).indexConfig x +/-- +Executes `x` using a `MetaM` configuration for inferred from `Simp.Config`. +-/ +@[inline] def withSimpMetaConfig (x : SimpM α) : SimpM α := do + withConfigWithKey (← readThe Simp.Context).metaConfig x + @[extern "lean_simp"] opaque simp (e : Expr) : SimpM Result diff --git a/tests/lean/run/2670.lean b/tests/lean/run/2670.lean index 7120e52b5ee4..d533c89bfc85 100644 --- a/tests/lean/run/2670.lean +++ b/tests/lean/run/2670.lean @@ -19,5 +19,18 @@ theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by | a::as, n => by rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as] simp [enumFrom, f] - rw [Array.foldr_eq_foldr_toList] - simp [go] -- Should close the goal + rw [←Array.foldr_toList] + simp [f] at go -- We must unfold `f` at `go`, or use `+zetaDelta`. See next theorem + simp [go] + +open List in +theorem enumFrom_eq_enumFromTR'' : @enumFrom = @enumFromTR' := by + funext α n l; simp only [enumFromTR'] + let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc) + let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l) + | [], n => rfl + | a::as, n => by + rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as] + simp [enumFrom, f] + rw [←Array.foldr_toList] + simp +zetaDelta [go] diff --git a/tests/lean/run/5455.lean b/tests/lean/run/5455.lean new file mode 100644 index 000000000000..f963187962d2 --- /dev/null +++ b/tests/lean/run/5455.lean @@ -0,0 +1,23 @@ +variable {α : Type} + +theorem test1 {n : Nat} {f : Fin n → α} : False := by + let c (i : Fin n) : Nat := i + let d : Fin n → Nat × Nat := fun i => (c i, c i + 1) + have : ∀ i, (d i).2 ≠ c i * 2 := by + fail_if_success simp only -- should not unfold `d` or `i` + guard_target =ₛ ∀ (i : Fin n), (d i).snd ≠ c i * 2 + simp +zetaDelta only -- `d` and `i` are now unfolded + guard_target =ₛ ∀ (i : Fin n), i.val + 1 ≠ i.val * 2 + sorry + sorry + +opaque f : Nat → Nat +axiom f_ax (x : Nat): f (f x) = x + +theorem test2 (a : Nat) : False := by + let d : Nat → Nat × Nat := fun i => (f a, i) + have : f (d 1).1 = a := by + fail_if_success simp only [f_ax] -- f_ax should be applicable + simp +zetaDelta only [f_ax] -- f_ax is applicable if zetaDelta := true + done + sorry diff --git a/tests/lean/run/heapSort.lean b/tests/lean/run/heapSort.lean index d54b543c496e..8ed93a6e97b3 100644 --- a/tests/lean/run/heapSort.lean +++ b/tests/lean/run/heapSort.lean @@ -166,7 +166,8 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α | none => out | some x => have : a.popMax.size < a.size := by - simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one + simp +zetaDelta + exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one loop a.popMax (out.push x) termination_by a.size decreasing_by assumption From d52870c8fb04953a0342fdddf015703ce8c5239a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2024 17:08:32 -0800 Subject: [PATCH 02/23] chore: add instance `Repr Meta.Config` --- src/Lean/Meta/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 581fe806a206..c22b0b564fd3 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -187,7 +187,7 @@ structure Config where Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/ zetaDelta : Bool := true - deriving Inhabited + deriving Inhabited, Repr /-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/ private def Config.toKey (c : Config) : UInt64 := From a164f2179fa684880b01550166a11cac0312f287 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2024 17:35:54 -0800 Subject: [PATCH 03/23] fix: configuration plumbing in `simp` --- src/Lean/Meta/Tactic/Simp/Types.lean | 45 ++++++++++++++++++++++++---- 1 file changed, 39 insertions(+), 6 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 0e3fbae9ec35..7f1f822906f0 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -122,8 +122,18 @@ private def updateArith (c : Config) : CoreM Config := do /-- Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing. -/ -private def mkIndexConfig (c : Config) : ConfigWithKey := - { c with +private def mkIndexConfig (c : Config) : MetaM ConfigWithKey := do + let curr ← Meta.getConfig + return { curr with + beta := c.beta + iota := c.iota + zeta := c.zeta + zetaDelta := c.zetaDelta + etaStruct := c.etaStruct + /- + When indexing terms we disable projection to ensure a term such as `f ((a, b).1)` + is an instance of the pattern `f (?x.1)` + -/ proj := .no transparency := .reducible : Meta.Config }.toConfigWithKey @@ -131,8 +141,31 @@ private def mkIndexConfig (c : Config) : ConfigWithKey := /-- Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`. -/ -private def mkMetaConfig (c : Config) : ConfigWithKey := - { c with +private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do + let curr ← Meta.getConfig + return { curr with + /- + Remark: We do **not** propagate `c.beta` to the `Meta.Config` used for `isDefEq` in `simp`. + Reason: When solving a unification constraint such as `?x =?= t`, we also unify their types, + and we often need beta-reduction for them. For example, suppose `t` is a recursor, then + its type will often produce an application such as `(fun x => Nat) 0` where `fun x => Nat` is the + motive of the recursor. If `?x` has type `Nat`, the unification will fail without beta. + + Not propagating `beta`, may surprise users, in examples such as + ``` + opaque f : Nat → Nat + @[simp] axiom f_ax : f (no_index 0) = 1 + example : f ((fun x => x) 0) = 1 := by + simp -beta -- Oh no, it succeeds because the term was beta-reduced by `isDefEq`. + ``` + The example above looks artificial. If users complain, we can try a more complicated solution + that forces `beta := true` only when `isDefEq` is unifying the type of a meta-variable with the + type of the term being assigned to it. + -/ + iota := c.iota + zeta := c.zeta + zetaDelta := c.zetaDelta + etaStruct := c.etaStruct proj := if c.proj then .yesWithDelta else .no transparency := .reducible : Meta.Config }.toConfigWithKey @@ -141,8 +174,8 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) ( let config ← updateArith config return { config, simpTheorems, congrTheorems - metaConfig := mkMetaConfig config - indexConfig := mkIndexConfig config + metaConfig := (← mkMetaConfig config) + indexConfig := (← mkIndexConfig config) } def Context.setConfig (context : Context) (config : Config) : Context := From 690252dfb2e87ebd30c1c095498fab3c215ed59f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2024 17:36:59 -0800 Subject: [PATCH 04/23] test: for `simp` configuration plumbing --- .../lean/run/simpConfigPropagationIssue1.lean | 13 ++++ .../lean/run/simpConfigPropagationIssue2.lean | 63 +++++++++++++++++++ .../lean/run/simpConfigPropagationIssue3.lean | 36 +++++++++++ 3 files changed, 112 insertions(+) create mode 100644 tests/lean/run/simpConfigPropagationIssue1.lean create mode 100644 tests/lean/run/simpConfigPropagationIssue2.lean create mode 100644 tests/lean/run/simpConfigPropagationIssue3.lean diff --git a/tests/lean/run/simpConfigPropagationIssue1.lean b/tests/lean/run/simpConfigPropagationIssue1.lean new file mode 100644 index 000000000000..be3e5e84d6c0 --- /dev/null +++ b/tests/lean/run/simpConfigPropagationIssue1.lean @@ -0,0 +1,13 @@ +namespace Option + +variable {α : Type _} + +instance liftOrGet_isCommutative (f : α → α → α) [Std.Commutative f] : + Std.Commutative (liftOrGet f) := + ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, Std.Commutative.comm]⟩ + +instance liftOrGet_isAssociative (f : α → α → α) [Std.Associative f] : + Std.Associative (liftOrGet f) := + ⟨fun a b c ↦ by cases a <;> cases b <;> cases c <;> simp [liftOrGet, Std.Associative.assoc]⟩ + +end Option diff --git a/tests/lean/run/simpConfigPropagationIssue2.lean b/tests/lean/run/simpConfigPropagationIssue2.lean new file mode 100644 index 000000000000..7dfea300e6a5 --- /dev/null +++ b/tests/lean/run/simpConfigPropagationIssue2.lean @@ -0,0 +1,63 @@ +namespace Std.Range + +/-- The number of elements contained in a `Std.Range`. -/ +def numElems (r : Range) : Nat := + if r.step = 0 then + -- This is a very weird choice, but it is chosen to coincide with the `forIn` impl + if r.stop ≤ r.start then 0 else r.stop + else + (r.stop - r.start + r.step - 1) / r.step + +theorem numElems_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.numElems = 0 := sorry + +private theorem numElems_le_iff {start stop step i} (hstep : 0 < step) : + (stop - start + step - 1) / step ≤ i ↔ stop ≤ start + step * i := + sorry + +theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r.step) : x ∈ r := by + sorry + +theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range) + (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) : + forIn' r init f = + forIn + ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r) + init (fun ⟨a, h⟩ => f a h) := by + let ⟨start, stop, step⟩ := r + let L := List.range' start (numElems ⟨start, stop, step⟩) step + let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h + suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _ + intro H; dsimp only [forIn', Range.forIn'] + if h : start < stop then + simp [numElems, Nat.not_le.2 h, L]; split + · subst step + suffices ∀ n H init, + forIn'.loop start stop 0 f n start (Nat.le_refl _) init = + forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ .. + intro n; induction n with (intro H init; unfold forIn'.loop; simp [*]) -- fails here, can't unfold + | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl + · next step0 => + have hstep := Nat.pos_of_ne_zero step0 + suffices ∀ fuel l i hle H, l ≤ fuel → + (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init, + forIn'.loop start stop step f fuel i hle init = + forIn ((List.range' i l step).pmap Subtype.mk H) init f' by + refine this _ _ _ _ _ + ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..))) + (fun _ => (numElems_le_iff hstep).symm) _ + conv => lhs; rw [← Nat.one_mul stop] + exact Nat.mul_le_mul_right stop hstep + intro fuel; induction fuel with intro l i hle H h1 h2 init + | zero => simp [forIn'.loop, Nat.le_zero.1 h1] + | succ fuel ih => + cases l with + | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)] + | succ l => + have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..)) + (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by + rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff] + have := h2 0; simp at this + rw [forIn'.loop]; simp [this, ih]; rfl + else + simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L] + cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h] diff --git a/tests/lean/run/simpConfigPropagationIssue3.lean b/tests/lean/run/simpConfigPropagationIssue3.lean new file mode 100644 index 000000000000..cc238c06d1e5 --- /dev/null +++ b/tests/lean/run/simpConfigPropagationIssue3.lean @@ -0,0 +1,36 @@ +namespace Ordering + +@[simp] theorem swap_swap {o : Ordering} : o.swap.swap = o := by cases o <;> rfl + +@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap ↔ o₁ = o₂ := + ⟨fun h => by simpa using congrArg swap h, congrArg _⟩ + +end Ordering + +/-- `OrientedCmp cmp` asserts that `cmp` is determined by the relation `cmp x y = .lt`. -/ +class OrientedCmp (cmp : α → α → Ordering) : Prop where + /-- The comparator operation is symmetric, in the sense that if `cmp x y` equals `.lt` then + `cmp y x = .gt` and vice versa. -/ + symm (x y) : (cmp x y).swap = cmp y x + +namespace OrientedCmp + +theorem cmp_eq_gt [OrientedCmp cmp] : cmp x y = .gt ↔ cmp y x = .lt := by + rw [← Ordering.swap_inj, symm]; exact .rfl + +end OrientedCmp + +/-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/ +class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where + /-- The comparator operation is transitive. -/ + le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt + +namespace TransCmp +variable [TransCmp cmp] +open OrientedCmp + +theorem ge_trans (h₁ : cmp x y ≠ .lt) (h₂ : cmp y z ≠ .lt) : cmp x z ≠ .lt := by + have := @TransCmp.le_trans _ cmp _ z y x + simp [cmp_eq_gt] at * + -- `simp` did not fire at `this` + exact this h₂ h₁ From f35f247b011d277627b2cb4985771c8c71fe50fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2024 17:39:14 -0800 Subject: [PATCH 05/23] test: make test more robust --- tests/lean/run/heapSort.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/tests/lean/run/heapSort.lean b/tests/lean/run/heapSort.lean index 8ed93a6e97b3..fc76b691a183 100644 --- a/tests/lean/run/heapSort.lean +++ b/tests/lean/run/heapSort.lean @@ -176,15 +176,18 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α attribute [simp] Array.heapSort.loop /-- -info: Array.heapSort.loop.eq_1.{u_1} {α : Type u_1} (gt : α → α → Bool) (a : BinaryHeap α gt) (out : Array α) : - Array.heapSort.loop gt a out = +info: Array.heapSort.loop.eq_1 fun a b => + decide + (a < + b) : ∀ (a : BinaryHeap Nat fun y x => decide (x < y)) (out : Array Nat), + Array.heapSort.loop (fun a b => decide (a < b)) a out = match e : a.max with | none => out | some x => let_fun this := ⋯; - Array.heapSort.loop gt a.popMax (out.push x) + Array.heapSort.loop (fun a b => decide (a < b)) a.popMax (out.push x) -/ #guard_msgs in -#check Array.heapSort.loop.eq_1 +#check Array.heapSort.loop.eq_1 (fun (a b : Nat) => a < b) attribute [simp] BinaryHeap.heapifyDown From 8999d3ca79d54932087d51a1f4b7924b559bdabc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2024 17:51:31 -0800 Subject: [PATCH 06/23] chore: fix stage2 issue chore: fix stage2 issues --- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/List/Impl.lean | 2 +- src/Lean/Data/RArray.lean | 2 +- src/Lean/Elab/PatternVar.lean | 2 +- src/Std/Sat/AIG/Basic.lean | 6 +++--- src/Std/Sat/AIG/CNF.lean | 6 +++--- src/Std/Sat/AIG/Relabel.lean | 2 +- .../BVDecide/LRAT/Internal/Formula/RatAddResult.lean | 2 +- .../BVDecide/LRAT/Internal/Formula/RupAddResult.lean | 9 ++++----- src/Std/Time/Date/ValidDate.lean | 2 +- 10 files changed, 17 insertions(+), 18 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 4252bd32c1dd..943f629e4e81 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -814,7 +814,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h induction a, i, h using Array.eraseIdx.induct with | @case1 a i h h' a' ih => unfold eraseIdx - simp [h', a', ih] + simp +zetaDelta [h', a', ih] | case2 a i h h' => unfold eraseIdx simp [h'] diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index e01f04335392..5fb32bf0b59c 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -332,7 +332,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) := rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as] simp [enumFrom, f] rw [← Array.foldr_toList] - simp [go] + simp +zetaDelta [go] /-! ## Other list operations -/ diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean index 54b7fd5612b2..a1b9d66d2500 100644 --- a/src/Lean/Data/RArray.lean +++ b/src/Lean/Data/RArray.lean @@ -55,7 +55,7 @@ where go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n) case case1 => simp [ofFn.go, size]; omega - case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega + case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega section Meta open Lean diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 9e2dce4bdfa5..2948a36f6117 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -159,7 +159,7 @@ private def processVar (idStx : Syntax) : M Syntax := do private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do if h₁ : s₁.vars.size = s₂.vars.size then for h₂ : i in [startingAt:s₁.vars.size] do - if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all) then return false + if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all +zetaDelta) then return false true else false diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean index cf12873255e3..4a12ef54dce9 100644 --- a/src/Std/Sat/AIG/Basic.lean +++ b/src/Std/Sat/AIG/Basic.lean @@ -471,7 +471,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α := have := input.lhs.ref.hgate have := input.rhs.ref.hgate omega - ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ /-- Add a new input node to the AIG in `aig`. Note that this version is only meant for proving, @@ -487,7 +487,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α := split at h2 · apply aig.invariant <;> assumption · contradiction - ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ /-- Add a new constant node to `aig`. Note that this version is only meant for proving, @@ -503,7 +503,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α := split at h2 · apply aig.invariant <;> assumption · contradiction - ⟨{ decls, invariant, cache }, ⟨g, by simp [decls]⟩⟩ + ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩ end AIG diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean index 95ecaa3ae8d5..b43ced351dff 100644 --- a/src/Std/Sat/AIG/CNF.lean +++ b/src/Std/Sat/AIG/CNF.lean @@ -505,7 +505,7 @@ def State.addConst (state : State aig) (idx : Nat) (h : idx < aig.decls.size) let newCnf := Decl.constToCNF (.inr ⟨idx, h⟩) b have hinv := toCNF.State.Inv_constToCNF htip let ⟨cache, hcache⟩ := cache.addConst idx h htip - ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩ /-- Add the CNF for a `Decl.atom` to the state. @@ -517,7 +517,7 @@ def State.addAtom (state : State aig) (idx : Nat) (h : idx < aig.decls.size) let newCnf := Decl.atomToCNF (.inr ⟨idx, h⟩) (.inl a) have hinv := toCNF.State.Inv_atomToCNF htip let ⟨cache, hcache⟩ := cache.addAtom idx h htip - ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩ /-- Add the CNF for a `Decl.gate` to the state. @@ -537,7 +537,7 @@ def State.addGate (state : State aig) {hlb} {hrb} (idx : Nat) (h : idx < aig.dec rinv have hinv := toCNF.State.Inv_gateToCNF htip let ⟨cache, hcache⟩ := cache.addGate idx h htip hl hr - ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [hcache]⟩ + ⟨⟨newCnf ++ cnf, cache, State.Inv_append hinv inv⟩, by simp [newCnf, hcache]⟩ /-- Evaluate the CNF contained within the state. diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean index f06433ffaae9..ae33a8346006 100644 --- a/src/Std/Sat/AIG/Relabel.lean +++ b/src/Std/Sat/AIG/Relabel.lean @@ -65,7 +65,7 @@ def relabel (r : α → β) (aig : AIG α) : AIG β := cache, invariant := by intro idx lhs rhs linv rinv hbound hgate - simp [decls] at hgate + simp +zetaDelta [decls] at hgate have := Decl.relabel_gate hgate apply aig.invariant assumption diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean index be25f5ad8be3..ac09debb1f56 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean @@ -224,7 +224,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p have insertRupUnits_rw : (insertRupUnits f (negate c)).1 = ⟨(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits, (insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments⟩ := rfl - simp only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints, + simp +zetaDelta only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints, clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck, restoreAssignments_performRupCheck fc fc_assignments_size, ← insertRupUnits_rw, clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 4ba79bcc390f..b91c8178abc0 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen ⟨units.size, units_size_lt_updatedUnits_size⟩ have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1 refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩ - simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq] + simp +zetaDelta only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq] constructor · rfl · constructor @@ -131,7 +131,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen exact k_property · intro h simp only [← h, not_true, mostRecentUnitIdx] at hk - exact hk rfl rw [Array.getElem_push_lt _ _ _ k_in_bounds] rw [i_eq_l] at h2 exact h2 ⟨k.1, k_in_bounds⟩ @@ -193,7 +192,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen constructor · rw [Array.getElem_push_lt units l j.1 j.2, h1] · constructor - · simp [i_eq_l, ← hl] + · simp +zetaDelta [i_eq_l, ← hl] rfl · constructor · simp only [i_eq_l] @@ -228,7 +227,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩ simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq] constructor - · simp [i_eq_l, ← hl] + · simp +zetaDelta [i_eq_l, ← hl] rfl · constructor · rw [Array.getElem_push_lt units l j.1 j.2, h1] @@ -1328,7 +1327,7 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by rw [size_assignments_insertRupUnits f (negate c)] exact f_readyForRupAdd.2.1 - simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck, + simp +zetaDelta only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck, restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by rw [rupAddSuccess] diff --git a/src/Std/Time/Date/ValidDate.lean b/src/Std/Time/Date/ValidDate.lean index bd38c6520d26..ce74efb4eeba 100644 --- a/src/Std/Time/Date/ValidDate.lean +++ b/src/Std/Time/Date/ValidDate.lean @@ -48,7 +48,7 @@ def ofOrdinal (ordinal : Day.Ordinal.OfYear leap) : ValidDate leap := let bounded := Bounded.LE.mk ordinal.val (And.intro h h₁) |>.sub acc let bounded : Bounded.LE 1 monthDays.val := bounded.cast (by omega) (by omega) let days₁ : Day.Ordinal := ⟨bounded.val, And.intro bounded.property.left (Int.le_trans bounded.property.right monthDays.property.right)⟩ - ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp)⟩ + ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp +zetaDelta)⟩ else by let h₂ := Int.not_le.mp h₁ From 06c2e4308e47654afb90b5cea9b9f9acc3316a34 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Nov 2024 16:21:07 -0800 Subject: [PATCH 07/23] chore: remove new broken test It has been affected by recent changes to the Std library. --- .../lean/run/simpConfigPropagationIssue2.lean | 63 ------------------- 1 file changed, 63 deletions(-) delete mode 100644 tests/lean/run/simpConfigPropagationIssue2.lean diff --git a/tests/lean/run/simpConfigPropagationIssue2.lean b/tests/lean/run/simpConfigPropagationIssue2.lean deleted file mode 100644 index 7dfea300e6a5..000000000000 --- a/tests/lean/run/simpConfigPropagationIssue2.lean +++ /dev/null @@ -1,63 +0,0 @@ -namespace Std.Range - -/-- The number of elements contained in a `Std.Range`. -/ -def numElems (r : Range) : Nat := - if r.step = 0 then - -- This is a very weird choice, but it is chosen to coincide with the `forIn` impl - if r.stop ≤ r.start then 0 else r.stop - else - (r.stop - r.start + r.step - 1) / r.step - -theorem numElems_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.numElems = 0 := sorry - -private theorem numElems_le_iff {start stop step i} (hstep : 0 < step) : - (stop - start + step - 1) / step ≤ i ↔ stop ≤ start + step * i := - sorry - -theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r.step) : x ∈ r := by - sorry - -theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range) - (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) : - forIn' r init f = - forIn - ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r) - init (fun ⟨a, h⟩ => f a h) := by - let ⟨start, stop, step⟩ := r - let L := List.range' start (numElems ⟨start, stop, step⟩) step - let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h - suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _ - intro H; dsimp only [forIn', Range.forIn'] - if h : start < stop then - simp [numElems, Nat.not_le.2 h, L]; split - · subst step - suffices ∀ n H init, - forIn'.loop start stop 0 f n start (Nat.le_refl _) init = - forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ .. - intro n; induction n with (intro H init; unfold forIn'.loop; simp [*]) -- fails here, can't unfold - | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl - · next step0 => - have hstep := Nat.pos_of_ne_zero step0 - suffices ∀ fuel l i hle H, l ≤ fuel → - (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init, - forIn'.loop start stop step f fuel i hle init = - forIn ((List.range' i l step).pmap Subtype.mk H) init f' by - refine this _ _ _ _ _ - ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..))) - (fun _ => (numElems_le_iff hstep).symm) _ - conv => lhs; rw [← Nat.one_mul stop] - exact Nat.mul_le_mul_right stop hstep - intro fuel; induction fuel with intro l i hle H h1 h2 init - | zero => simp [forIn'.loop, Nat.le_zero.1 h1] - | succ fuel ih => - cases l with - | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)] - | succ l => - have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..)) - (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by - rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff] - have := h2 0; simp at this - rw [forIn'.loop]; simp [this, ih]; rfl - else - simp [List.range', h, numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), L] - cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h] From f284af1f7ebb222e5bec7d0284f05436dd8f4a32 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2024 18:10:57 -0800 Subject: [PATCH 08/23] fix: `Context.setConfig` must update `metaConfig` and `indexConfig` fields This PR fixes a bug at `Context.setConfig`. It was not propagating the configuration to the redundant fields (cache) `metaConfig` and `indexConfig`. --- src/Lean/Meta/Tactic/Simp/Types.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 7f1f822906f0..b89c6bc0bc5a 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -178,8 +178,12 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) ( indexConfig := (← mkIndexConfig config) } -def Context.setConfig (context : Context) (config : Config) : Context := - { context with config } +def Context.setConfig (context : Context) (config : Config) : MetaM Context := do + return { context with + config + metaConfig := (← mkMetaConfig config) + indexConfig := (← mkIndexConfig config) + } def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context := { c with simpTheorems } From 56fb2a17b358f6abe0e4bac749c0743cc1f215bb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2024 18:36:02 -0800 Subject: [PATCH 09/23] fix: use infer type config when checking types at metavariable assignment This PR fixes an issue at `isDefEq`. We must use the liberal infer type `MetaM` config when checking types at the assignment `?m := v`. --- src/Lean/Meta/ExprDefEq.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index b9e8bd9016fe..08ee1a34075e 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -381,7 +381,7 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool := -- must check whether types are definitionally equal or not, before assigning and returning true let mvarType ← inferType mvar let vType ← inferType v - if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then + if (← withAtLeastTransparency .default <| withInferTypeConfig <| Meta.isExprDefEqAux mvarType vType) then mvar.mvarId!.assign v pure true else From edcec55b75e2b0e976976d8e41767e0d44603628 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2024 18:45:59 -0800 Subject: [PATCH 10/23] test: add `split_ifs` mwe from Mathlib --- tests/lean/run/splitIfIssue.lean | 249 +++++++++++++++++++++++++++++++ 1 file changed, 249 insertions(+) create mode 100644 tests/lean/run/splitIfIssue.lean diff --git a/tests/lean/run/splitIfIssue.lean b/tests/lean/run/splitIfIssue.lean new file mode 100644 index 000000000000..893629649eb6 --- /dev/null +++ b/tests/lean/run/splitIfIssue.lean @@ -0,0 +1,249 @@ +import Lean.Elab.Tactic.Location +import Lean.Meta.Tactic.SplitIf +import Lean.Elab.Tactic.Simp + +section Mathlib.Tactic.Core + +open Lean Elab Tactic + +namespace Lean.Elab.Tactic +#check Parser.Tactic.allGoals +def allGoals (tac : TacticM Unit) : TacticM Unit := do + let mvarIds ← getGoals + let mut mvarIdsNew := #[] + for mvarId in mvarIds do + unless (← mvarId.isAssigned) do + setGoals [mvarId] + try + tac + mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals) + catch ex => + if (← read).recover then + logException ex + mvarIdsNew := mvarIdsNew.push mvarId + else + throw ex + setGoals mvarIdsNew.toList + +/-- Simulates the `<;>` tactic combinator. First runs `tac1` and then runs + `tac2` on all newly-generated subgoals. +-/ +def andThenOnSubgoals (tac1 : TacticM Unit) (tac2 : TacticM Unit) : TacticM Unit := + focus do tac1; allGoals tac2 + +end Lean.Elab.Tactic + +end Mathlib.Tactic.Core + +section Mathlib.Tactic.SplitIfs + +namespace Mathlib.Tactic + +open Lean Elab.Tactic Parser.Tactic Lean.Meta + +/-- A position where a split may apply. +-/ +private inductive SplitPosition +| target +| hyp (fvarId: FVarId) + +/-- Collects a list of positions pointed to by `loc` and their types. +-/ +private def getSplitCandidates (loc : Location) : TacticM (List (SplitPosition × Expr)) := +match loc with +| Location.wildcard => do + let candidates ← (← getLCtx).getFVarIds.mapM + (fun fvarId ↦ do + let typ ← instantiateMVars (← inferType (mkFVar fvarId)) + return (SplitPosition.hyp fvarId, typ)) + pure ((SplitPosition.target, ← getMainTarget) :: candidates.toList) +| Location.targets hyps tgt => do + let candidates ← (← hyps.mapM getFVarId).mapM + (fun fvarId ↦ do + let typ ← instantiateMVars (← inferType (mkFVar fvarId)) + return (SplitPosition.hyp fvarId, typ)) + if tgt + then return (SplitPosition.target, ← getMainTarget) :: candidates.toList + else return candidates.toList + +/-- Return the condition and decidable instance of an `if` expression to case split. -/ +private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) := + match e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars with + | some iteApp => + let cond := iteApp.getArg! 1 5 + let dec := iteApp.getArg! 2 5 + -- Try to find a nested `if` in `cond` + findIfToSplit? cond |>.getD (cond, dec) + | none => none + +/-- Finds an if condition to split. If successful, returns the position and the condition. +-/ +private def findIfCondAt (loc : Location) : TacticM (Option (SplitPosition × Expr)) := do + for (pos, e) in (← getSplitCandidates loc) do + if let some (cond, _) := findIfToSplit? e + then return some (pos, cond) + return none + +/-- `Simp.Discharge` strategy to use in `reduceIfsAt`. Delegates to +`SplitIf.discharge?`, and additionally supports discharging `True`, to +better match the behavior of mathlib3's `split_ifs`. +-/ +private def discharge? (e : Expr) : SimpM (Option Expr) := do + let e ← instantiateMVars e + if let some e1 ← (← SplitIf.mkDischarge? false) e + then return some e1 + if e.isConstOf `True + then return some (mkConst `True.intro) + return none + +/-- Simplifies if-then-else expressions after cases have been split out. +-/ +private def reduceIfsAt (loc : Location) : TacticM Unit := do + let ctx ← SplitIf.getSimpContext + let ctx ← ctx.setConfig { ctx.config with failIfUnchanged := false } + let _ ← simpLocation ctx (← ({} : Simp.SimprocsArray).add `reduceCtorEq false) discharge? loc + pure () + +/-- Splits a single if-then-else expression and then reduces the resulting goals. +Has a similar effect as `SplitIf.splitIfTarget?` or `SplitIf.splitIfLocalDecl?` from +core Lean 4. We opt not to use those library functions so that we can better mimic +the behavior of mathlib3's `split_ifs`. +-/ +private def splitIf1 (cond : Expr) (hName : Name) (loc : Location) : TacticM Unit := do + let splitCases := + evalTactic (← `(tactic| by_cases $(mkIdent hName) : $(← Elab.Term.exprToSyntax cond))) + andThenOnSubgoals splitCases (reduceIfsAt loc) + +/-- Pops off the front of the list of names, or generates a fresh name if the +list is empty. +-/ +private def getNextName (hNames: IO.Ref (List (TSyntax `Lean.binderIdent))) : MetaM Name := do + match ← hNames.get with + | [] => mkFreshUserName `h + | n::ns => do hNames.set ns + if let `(binderIdent| $x:ident) := n + then pure x.getId + else pure `_ + +/-- Returns `true` if the condition or its negation already appears as a hypothesis. +-/ +private def valueKnown (cond : Expr) : TacticM Bool := do + let not_cond := mkApp (mkConst `Not) cond + for h in ← getLocalHyps do + let ty ← instantiateMVars (← inferType h) + if cond == ty then return true + if not_cond == ty then return true + return false + +/-- Main loop of split_ifs. Pulls names for new hypotheses from `hNames`. +Stops if it encounters a condition in the passed-in `List Expr`. +-/ +private partial def splitIfsCore + (loc : Location) + (hNames : IO.Ref (List (TSyntax `Lean.binderIdent))) : + List Expr → TacticM Unit := fun done ↦ withMainContext do + let some (_,cond) ← findIfCondAt loc + | Meta.throwTacticEx `split_ifs (← getMainGoal) "no if-then-else conditions to split" + + -- If `cond` is `¬p` then use `p` instead. + let cond := if cond.isAppOf `Not then cond.getAppArgs[0]! else cond + + if done.contains cond then return () + let no_split ← valueKnown cond + if no_split then + andThenOnSubgoals (reduceIfsAt loc) (splitIfsCore loc hNames (cond::done) <|> pure ()) + else do + let hName ← getNextName hNames + andThenOnSubgoals (splitIf1 cond hName loc) ((splitIfsCore loc hNames (cond::done)) <|> + pure ()) + +/-- Splits all if-then-else-expressions into multiple goals. +Given a goal of the form `g (if p then x else y)`, `split_ifs` will produce +two goals: `p ⊢ g x` and `¬p ⊢ g y`. +If there are multiple ite-expressions, then `split_ifs` will split them all, +starting with a top-most one whose condition does not contain another +ite-expression. +`split_ifs at *` splits all ite-expressions in all hypotheses as well as the goal. +`split_ifs with h₁ h₂ h₃` overrides the default names for the hypotheses. +-/ +syntax (name := splitIfs) "split_ifs" (location)? (" with" (ppSpace colGt binderIdent)+)? : tactic + +elab_rules : tactic +| `(tactic| split_ifs $[$loc:location]? $[with $withArg*]?) => + let loc := match loc with + | none => Location.targets #[] true + | some loc => expandLocation loc + let names := match withArg with + | none => [] + | some args => args.toList + withMainContext do + let names ← IO.mkRef names + splitIfsCore loc names [] + for name in ← names.get do + logWarningAt name m!"unused name: {name}" + +end Mathlib.Tactic + +end Mathlib.Tactic.SplitIfs + +section Mathlib.Order.Defs + +class Preorder (α : Type _) extends LE α, LT α where + +class PartialOrder (α : Type _) extends Preorder α where + +class LinearOrder (α : Type _) extends PartialOrder α, Min α, Max α, Ord α where + /-- In a linearly ordered type, we assume the order relations are all decidable. -/ + decidableLE : DecidableRel (· ≤ · : α → α → Prop) + /-- In a linearly ordered type, we assume the order relations are all decidable. -/ + decidableEq : DecidableEq α + /-- In a linearly ordered type, we assume the order relations are all decidable. -/ + decidableLT : DecidableRel (· < · : α → α → Prop) + min := fun a b => if a ≤ b then a else b + max := fun a b => if a ≤ b then b else a + +variable [LinearOrder α] {a b c : α} + +instance (priority := 900) (a b : α) : Decidable (a < b) := LinearOrder.decidableLT a b +instance (priority := 900) (a b : α) : Decidable (a ≤ b) := LinearOrder.decidableLE a b +instance (priority := 900) (a b : α) : Decidable (a = b) := LinearOrder.decidableEq a b + +end Mathlib.Order.Defs + +section Mathlib.Order.Lattice + +universe u v w + +variable {α : Type u} + +class SemilatticeSup (α : Type u) extends PartialOrder α where + sup : α → α → α + +class Lattice (α : Type u) extends SemilatticeSup α + +end Mathlib.Order.Lattice + +open Lean Meta Elab Tactic in +/-- `guard_goal_nums n` succeeds if there are exactly `n` goals and fails otherwise. -/ +elab (name := guardGoalNums) "guard_goal_nums " n:num : tactic => do + let numGoals := (← getGoals).length + guard (numGoals = n.getNat) <|> + throwError "expected {n.getNat} goals but found {numGoals}" + +example (a m tl : α) (f : α → β) [LinearOrder β] : + (if f (if f a < f m then m else a) < f tl then some tl else some (if f a < f m then m else a)) = + if f a < f (if f m < f tl then tl else m) then some (if f m < f tl then tl else m) else some a := by + split_ifs + guard_goal_nums 7 + all_goals sorry + +instance LinearOrder.toLattice {α : Type u} [o : LinearOrder α] : Lattice α := + let __spread := o + { __spread with sup := max } + +example (a m tl : α) (f : α → β) [LinearOrder β] : + (if f (if f a < f m then m else a) < f tl then some tl else some (if f a < f m then m else a)) = + if f a < f (if f m < f tl then tl else m) then some (if f m < f tl then tl else m) else some a := by + split_ifs + guard_goal_nums 7 + all_goals sorry From df504308c58661c50a9be1dc5bdc1064046eb63e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Nov 2024 11:31:15 -0800 Subject: [PATCH 11/23] fix: ensure `withInferTypeConfig` does not override unrelated configuration options --- src/Lean/Meta/ExprDefEq.lean | 13 +++++++------ src/Lean/Meta/InferType.lean | 21 +++++++++++++-------- 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 08ee1a34075e..8f26f5fa1eba 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -380,12 +380,13 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool := else -- must check whether types are definitionally equal or not, before assigning and returning true let mvarType ← inferType mvar - let vType ← inferType v - if (← withAtLeastTransparency .default <| withInferTypeConfig <| Meta.isExprDefEqAux mvarType vType) then - mvar.mvarId!.assign v - pure true - else - pure false + withInferTypeConfig do + let vType ← inferType v + if (← Meta.isExprDefEqAux mvarType vType) then + mvar.mvarId!.assign v + pure true + else + pure false /-- Auxiliary method for solving constraints of the form `?m xs := v`. diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 710d385450ee..5ff735e9da17 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -177,15 +177,20 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do modifyInferTypeCache fun c => c.insert key type return type -private def defaultConfig : ConfigWithKey := - { : Config }.toConfigWithKey - -private def allConfig : ConfigWithKey := - { transparency := .all : Config }.toConfigWithKey +/-- +Ensure `MetaM` configuration is strong enough for inferring/checking types. +For example, `beta := true` is essential when type checking. -@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := do - let cfg := if (← getTransparency) == .all then allConfig else defaultConfig - withConfigWithKey cfg x +Remark: we previously use the default configuration here, but this is problematic +because it overrides unrelated configurations. +-/ +@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := + withAtLeastTransparency .default do + let cfg ← getConfig + if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj != .no then + x + else + withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x @[export lean_infer_type] def inferTypeImp (e : Expr) : MetaM Expr := From 3ada283ab17c012b9e2d9e2060ce690544ec8275 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Nov 2024 11:44:13 -0800 Subject: [PATCH 12/23] chore: remove workaround --- src/Lean/Meta/Tactic/Simp/Types.lean | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index b89c6bc0bc5a..d0e20e3ca9a0 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -144,24 +144,7 @@ Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`. private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do let curr ← Meta.getConfig return { curr with - /- - Remark: We do **not** propagate `c.beta` to the `Meta.Config` used for `isDefEq` in `simp`. - Reason: When solving a unification constraint such as `?x =?= t`, we also unify their types, - and we often need beta-reduction for them. For example, suppose `t` is a recursor, then - its type will often produce an application such as `(fun x => Nat) 0` where `fun x => Nat` is the - motive of the recursor. If `?x` has type `Nat`, the unification will fail without beta. - - Not propagating `beta`, may surprise users, in examples such as - ``` - opaque f : Nat → Nat - @[simp] axiom f_ax : f (no_index 0) = 1 - example : f ((fun x => x) 0) = 1 := by - simp -beta -- Oh no, it succeeds because the term was beta-reduced by `isDefEq`. - ``` - The example above looks artificial. If users complain, we can try a more complicated solution - that forces `beta := true` only when `isDefEq` is unifying the type of a meta-variable with the - type of the term being assigned to it. - -/ + beta := c.beta iota := c.iota zeta := c.zeta zetaDelta := c.zetaDelta From 7c472e45d3540f8ec0f457f331a5853a7776142d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Nov 2024 11:48:23 -0800 Subject: [PATCH 13/23] test: `simp -beta` --- tests/lean/run/betaSimp.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 tests/lean/run/betaSimp.lean diff --git a/tests/lean/run/betaSimp.lean b/tests/lean/run/betaSimp.lean new file mode 100644 index 000000000000..bdacf4b204eb --- /dev/null +++ b/tests/lean/run/betaSimp.lean @@ -0,0 +1,5 @@ +opaque f : Nat → Nat +@[simp] axiom f_ax : f (no_index 0) = 1 +example : f ((fun x => x) 0) = 1 := by + fail_if_success simp -beta -- should fail + simp From 9ba3b6c6602568c2631453ed3d5748c875584882 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 26 Nov 2024 11:43:03 +1100 Subject: [PATCH 14/23] add test for mod_cast failure --- tests/lean/run/6123_mod_cast.lean | 189 ++++++++++++++++++++++++++++++ 1 file changed, 189 insertions(+) create mode 100644 tests/lean/run/6123_mod_cast.lean diff --git a/tests/lean/run/6123_mod_cast.lean b/tests/lean/run/6123_mod_cast.lean new file mode 100644 index 000000000000..4bfa0cc37229 --- /dev/null +++ b/tests/lean/run/6123_mod_cast.lean @@ -0,0 +1,189 @@ + +section Mathlib.Order.Defs + +variable {α : Type _} + +section Preorder + +class Preorder (α : Type _) extends LE α, LT α where + le_refl : ∀ a : α, a ≤ a + le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c + lt := fun a b => a ≤ b ∧ ¬b ≤ a + lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl + +end Preorder + +section PartialOrder + +class PartialOrder (α : Type _) extends Preorder α where + le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b + +end PartialOrder + +section LinearOrder + +class LinearOrder (α : Type _) extends PartialOrder α, Min α, Max α, Ord α where + le_total (a b : α) : a ≤ b ∨ b ≤ a + decidableLE : DecidableRel (· ≤ · : α → α → Prop) + decidableEq : DecidableEq α + decidableLT : DecidableRel (· < · : α → α → Prop) + min := fun a b => if a ≤ b then a else b + max := fun a b => if a ≤ b then b else a + min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl + max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl + compare a b := compareOfLessAndEq a b + compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b + +end LinearOrder + +end Mathlib.Order.Defs + +section Mathlib.Order.Notation + +class Bot (α : Type _) where + bot : α + +notation "⊥" => Bot.bot + +attribute [match_pattern] Bot.bot + +end Mathlib.Order.Notation + +section Mathlib.Order.Basic + +variable {α : Type _} + +/-- An order is dense if there is an element between any pair of distinct comparable elements. -/ +class DenselyOrdered (α : Type _) [LT α] : Prop where + /-- An order is dense if there is an element between any pair of distinct elements. -/ + dense : ∀ a₁ a₂ : α, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂ + +theorem exists_between [LT α] [DenselyOrdered α] : ∀ {a₁ a₂ : α}, a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂ := + DenselyOrdered.dense _ _ + +theorem le_of_forall_le_of_dense [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} + (h : ∀ a, a₂ < a → a₁ ≤ a) : a₁ ≤ a₂ := sorry + +end Mathlib.Order.Basic + +section Mathlib.Order.BoundedOrder + +universe u + +variable {α : Type u} + +/-- An order is an `OrderBot` if it has a least element. +We state this using a data mixin, holding the value of `⊥` and the least element constraint. -/ +class OrderBot (α : Type u) [LE α] extends Bot α where + /-- `⊥` is the least element -/ + bot_le : ∀ a : α, ⊥ ≤ a + +section OrderBot + +variable [LE α] [OrderBot α] {a : α} + +@[simp] +theorem bot_le : ⊥ ≤ a := + OrderBot.bot_le a + +end OrderBot + +end Mathlib.Order.BoundedOrder + +section Mathlib.Order.TypeTags + +variable {α : Type _} + +def WithBot (α : Type _) := Option α + +namespace WithBot + +@[coe, match_pattern] def some : α → WithBot α := + Option.some + +instance coe : Coe α (WithBot α) := + ⟨some⟩ + +instance bot : Bot (WithBot α) := + ⟨none⟩ + +@[elab_as_elim, induction_eliminator, cases_eliminator] +def recBotCoe {C : WithBot α → Sort _} (bot : C ⊥) (coe : ∀ a : α, C a) : ∀ n : WithBot α, C n + | ⊥ => bot + | (a : α) => coe a + +end WithBot + +end Mathlib.Order.TypeTags + +variable {α β γ δ : Type _} + +namespace WithBot + +variable {a b : α} + +@[simp, norm_cast] +theorem coe_inj : (a : WithBot α) = b ↔ a = b := + Option.some_inj + +@[simp] +theorem bot_ne_coe : ⊥ ≠ (a : WithBot α) := + nofun + +section LE + +variable [LE α] + +instance (priority := 10) le : LE (WithBot α) := + ⟨fun o₁ o₂ => ∀ a : α, o₁ = ↑a → ∃ b : α, o₂ = ↑b ∧ a ≤ b⟩ + +@[simp, norm_cast] +theorem coe_le_coe : (a : WithBot α) ≤ b ↔ a ≤ b := by + simp [LE.le] + +instance orderBot : OrderBot (WithBot α) where + bot_le _ := fun _ h => Option.noConfusion h + +theorem le_coe_iff : ∀ {x : WithBot α}, x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b + | (b : α) => by simp + | ⊥ => by simp + +end LE + +section LT + +variable [LT α] + +instance (priority := 10) lt : LT (WithBot α) := + ⟨fun o₁ o₂ : WithBot α => ∃ b : α, o₂ = ↑b ∧ ∀ a : α, o₁ = ↑a → a < b⟩ + +@[simp, norm_cast] +theorem coe_lt_coe : (a : WithBot α) < b ↔ a < b := by + simp [LT.lt] + +end LT + +instance preorder [Preorder α] : Preorder (WithBot α) where + le := (· ≤ ·) + lt := (· < ·) + lt_iff_le_not_le := sorry + le_refl _ a ha := sorry + le_trans _ _ _ h₁ h₂ a ha := sorry + +end WithBot + +namespace WithBot + +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +theorem le_of_forall_lt_iff_le [LinearOrder α] [DenselyOrdered α] + {x y : WithBot α} : (∀ z : α, x < z → y ≤ z) ↔ y ≤ x := by + refine ⟨fun h ↦ ?_, fun h z x_z ↦ sorry⟩ + induction x with + | bot => sorry + | coe x => + rw [le_coe_iff] + rintro y rfl + exact le_of_forall_le_of_dense (by exact_mod_cast h) + +end WithBot From 5f8bfa3a1ef4ee14fc7253274a321823e1d543c8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 27 Nov 2024 11:19:02 +1100 Subject: [PATCH 15/23] chore: add minimization of Mathlib problem from Mathlib.CategoryTheory.Category.Cat.Adjunction --- tests/lean/run/6123_cat_adjunction.lean | 498 ++++++++++++++++++++++++ 1 file changed, 498 insertions(+) create mode 100644 tests/lean/run/6123_cat_adjunction.lean diff --git a/tests/lean/run/6123_cat_adjunction.lean b/tests/lean/run/6123_cat_adjunction.lean new file mode 100644 index 000000000000..af810102dea2 --- /dev/null +++ b/tests/lean/run/6123_cat_adjunction.lean @@ -0,0 +1,498 @@ +section Mathlib.CategoryTheory.ConcreteCategory.Bundled + +universe u v + +namespace CategoryTheory + +variable {c : Type u → Type v} + +structure Bundled (c : Type u → Type v) : Type max (u + 1) v where + α : Type u + str : c α := by infer_instance + +set_option checkBinderAnnotations false in +def Bundled.of {c : Type u → Type v} (α : Type u) [str : c α] : Bundled c := + ⟨α, str⟩ + +end CategoryTheory + +end Mathlib.CategoryTheory.ConcreteCategory.Bundled + +section Mathlib.Logic.Equiv.Defs + +open Function + +universe u v + +variable {α : Sort u} {β : Sort v} + +structure Equiv (α : Sort _) (β : Sort _) where + protected toFun : α → β + protected invFun : β → α + +infixl:25 " ≃ " => Equiv + +protected def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩ + +end Mathlib.Logic.Equiv.Defs + +section Mathlib.Combinatorics.Quiver.Basic + +universe v v₁ v₂ u u₁ u₂ + +class Quiver (V : Type u) where + Hom : V → V → Sort v + +infixr:10 " ⟶ " => Quiver.Hom + +structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where + obj : V → W + map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y) + +end Mathlib.Combinatorics.Quiver.Basic + +section Mathlib.CategoryTheory.Category.Basic + +universe v u + +namespace CategoryTheory + +class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where + id : ∀ X : obj, Hom X X + comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z) + +scoped notation "𝟙" => CategoryStruct.id +scoped infixr:80 " ≫ " => CategoryStruct.comp + +class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where + +end CategoryTheory + +end Mathlib.CategoryTheory.Category.Basic + +section Mathlib.CategoryTheory.Functor.Basic + +namespace CategoryTheory + +universe v v₁ v₂ v₃ u u₁ u₂ u₃ + +structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] + extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where + +infixr:26 " ⥤ " => Functor + +namespace Functor + +section + +variable (C : Type u₁) [Category.{v₁} C] + +protected def id : C ⥤ C where + obj X := X + map f := f + +notation "𝟭" => Functor.id + +variable {C} + +theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl + +theorem id_map {X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f := rfl + +end + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + {E : Type u₃} [Category.{v₃} E] + +def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where + obj X := G.obj (F.obj X) + map f := G.map (F.map f) + +@[simp] theorem comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F.comp G).obj X = G.obj (F.obj X) := rfl + +infixr:80 " ⋙ " => Functor.comp + +theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) : + (F ⋙ G).map f = G.map (F.map f) := rfl + +end Functor + +end CategoryTheory + +end Mathlib.CategoryTheory.Functor.Basic + +section Mathlib.CategoryTheory.NatTrans + +namespace CategoryTheory + +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + +structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where + app : ∀ X : C, F.obj X ⟶ G.obj X + naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f + +namespace NatTrans + +/-- `NatTrans.id F` is the identity natural transformation on a functor `F`. -/ +protected def id (F : C ⥤ D) : NatTrans F F where + app X := 𝟙 (F.obj X) + naturality := sorry + +variable {F G H : C ⥤ D} + +def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where + app X := α.app X ≫ β.app X + naturality := sorry + +end NatTrans + +end CategoryTheory + + +end Mathlib.CategoryTheory.NatTrans + +section Mathlib.CategoryTheory.Functor.Category + +namespace CategoryTheory + +universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄ + +variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] + +variable {C D} + +instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where + Hom F G := NatTrans F G + id F := NatTrans.id F + comp α β := NatTrans.vcomp α β + +end CategoryTheory + +end Mathlib.CategoryTheory.Functor.Category + +section Mathlib.CategoryTheory.EqToHom + +universe v₁ u₁ + +namespace CategoryTheory + +variable {C : Type u₁} [Category.{v₁} C] + +def eqToHom {X Y : C} (p : X = Y) : X ⟶ Y := by rw [p]; exact 𝟙 _ + +end CategoryTheory + +end Mathlib.CategoryTheory.EqToHom + +section Mathlib.CategoryTheory.Functor.Const + +universe v₁ v₂ v₃ u₁ u₂ u₃ + +open CategoryTheory + +namespace CategoryTheory.Functor + +variable (J : Type u₁) [Category.{v₁} J] +variable {C : Type u₂} [Category.{v₂} C] + +def const : C ⥤ J ⥤ C where + obj X := + { obj := fun _ => X + map := fun _ => 𝟙 X } + map f := { app := fun _ => f, naturality := sorry } + +end CategoryTheory.Functor + + +end Mathlib.CategoryTheory.Functor.Const + +section Mathlib.CategoryTheory.DiscreteCategory + +namespace CategoryTheory + +universe v₁ v₂ v₃ u₁ u₁' u₂ u₃ + +structure Discrete (α : Type u₁) where + as : α + +instance discreteCategory (α : Type u₁) : Category (Discrete α) where + Hom X Y := ULift (PLift (X.as = Y.as)) + id _ := ULift.up (PLift.up rfl) + comp {X Y Z} g f := by + cases X + cases Y + cases Z + rcases f with ⟨⟨⟨⟩⟩⟩ + exact g + +namespace Discrete + +variable {α : Type u₁} + +theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as := + i.down.down + +protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y := + eqToHom sorry + +variable {C : Type u₂} [Category.{v₂} C] + +def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where + obj := F ∘ Discrete.as + map {X Y} f := by + dsimp + rcases f with ⟨⟨h⟩⟩ + exact eqToHom (congrArg _ h) + +end Discrete + +end CategoryTheory + + +end Mathlib.CategoryTheory.DiscreteCategory + +section Mathlib.CategoryTheory.Types + +namespace CategoryTheory + +universe v v' w u u' + +instance types : Category (Type u) where + Hom a b := a → b + id _ := id + comp f g := g ∘ f + +end CategoryTheory + +end Mathlib.CategoryTheory.Types + +section Mathlib.CategoryTheory.Bicategory.Basic + +namespace CategoryTheory + +universe w v u + +open Category + +class Bicategory (B : Type u) extends CategoryStruct.{v} B where + homCategory : ∀ a b : B, Category.{w} (a ⟶ b) := by infer_instance + +end CategoryTheory + +end Mathlib.CategoryTheory.Bicategory.Basic + +section Mathlib.CategoryTheory.Bicategory.Strict + +namespace CategoryTheory + +universe w v u + +variable (B : Type u) [Bicategory.{w, v} B] + +instance (priority := 100) StrictBicategory.category : Category B where + +end CategoryTheory + +end Mathlib.CategoryTheory.Bicategory.Strict + +section Mathlib.CategoryTheory.Category.Cat + +universe v u + +namespace CategoryTheory + +open Bicategory + +def Cat := + Bundled Category.{v, u} + +namespace Cat + +instance : CoeSort Cat (Type u) := + ⟨Bundled.α⟩ + +instance str (C : Cat.{v, u}) : Category.{v, u} C := + Bundled.str C + +def of (C : Type u) [Category.{v} C] : Cat.{v, u} := + Bundled.of C + +instance bicategory : Bicategory.{max v u, max v u} Cat.{v, u} where + Hom C D := C ⥤ D + id C := 𝟭 C + comp F G := F ⋙ G + homCategory := fun _ _ => Functor.category + +@[simp] theorem of_α (C) [Category C] : (of C).α = C := rfl + +def objects : Cat.{v, u} ⥤ Type u where + obj C := C + map F := F.obj + +instance (X : Cat.{v, u}) : Category (objects.obj X) := (inferInstance : Category X) + +end Cat + +def typeToCat : Type u ⥤ Cat where + obj X := Cat.of (Discrete X) + map := fun {X} {Y} f => by + dsimp + exact Discrete.functor (Discrete.mk ∘ f) + +@[simp] theorem typeToCat_obj (X : Type u) : typeToCat.obj X = Cat.of (Discrete X) := rfl +@[simp] theorem typeToCat_map {X Y : Type u} (f : X ⟶ Y) : + typeToCat.map f = Discrete.functor (Discrete.mk ∘ f) := rfl + +end CategoryTheory + + +end Mathlib.CategoryTheory.Category.Cat + +section Mathlib.CategoryTheory.Adjunction.Basic + +namespace CategoryTheory + +open Category + +universe v₁ v₂ v₃ u₁ u₂ u₃ + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] + +structure Adjunction (F : C ⥤ D) (G : D ⥤ C) where + unit : 𝟭 C ⟶ F.comp G + counit : G.comp F ⟶ 𝟭 D + +infixl:15 " ⊣ " => Adjunction + +namespace Adjunction + +structure CoreHomEquivUnitCounit (F : C ⥤ D) (G : D ⥤ C) where + homEquiv : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y) + unit : 𝟭 C ⟶ F ⋙ G + counit : G ⋙ F ⟶ 𝟭 D + homEquiv_counit : ∀ {X Y g}, (homEquiv X Y).symm.toFun g = F.map g ≫ counit.app Y + +variable {F : C ⥤ D} {G : D ⥤ C} + +def mk' (adj : CoreHomEquivUnitCounit F G) : F ⊣ G where + unit := adj.unit + counit := adj.counit + +end Adjunction + +end CategoryTheory + + +end Mathlib.CategoryTheory.Adjunction.Basic + +section Mathlib.CategoryTheory.IsConnected + +universe w₁ w₂ v₁ v₂ u₁ u₂ + +noncomputable section + +open CategoryTheory.Category + +namespace CategoryTheory + +class IsPreconnected (J : Type u₁) [Category.{v₁} J] : Prop where + iso_constant : + ∀ {α : Type u₁} (F : J ⥤ Discrete α) (j : J), False + +class IsConnected (J : Type u₁) [Category.{v₁} J] extends IsPreconnected J : Prop where + [is_nonempty : Nonempty J] + +variable {J : Type u₁} [Category.{v₁} J] + +def Zag (j₁ j₂ : J) : Prop := sorry + +def Zigzag : J → J → Prop := sorry + +def Zigzag.setoid (J : Type u₂) [Category.{v₁} J] : Setoid J where + r := Zigzag + iseqv := sorry + +end CategoryTheory + +end + +end Mathlib.CategoryTheory.IsConnected + +section Mathlib.CategoryTheory.ConnectedComponents + +universe v₁ v₂ v₃ u₁ u₂ + +noncomputable section + +namespace CategoryTheory + +variable {J : Type u₁} [Category.{v₁} J] + +def ConnectedComponents (J : Type u₁) [Category.{v₁} J] : Type u₁ := + Quotient (Zigzag.setoid J) + +def Functor.mapConnectedComponents {K : Type u₂} [Category.{v₂} K] (F : J ⥤ K) + (x : ConnectedComponents J) : ConnectedComponents K := + x |> Quotient.lift (Quotient.mk (Zigzag.setoid _) ∘ F.obj) sorry + +def ConnectedComponents.functorToDiscrete (X : Type _) + (f : ConnectedComponents J → X) : J ⥤ Discrete X where + obj Y := Discrete.mk (f (Quotient.mk (Zigzag.setoid _) Y)) + map g := Discrete.eqToHom sorry + +def ConnectedComponents.liftFunctor (J) [Category J] {X : Type _} (F :J ⥤ Discrete X) : + (ConnectedComponents J → X) := + Quotient.lift (fun c => (F.obj c).as) sorry + +end CategoryTheory + +end + +end Mathlib.CategoryTheory.ConnectedComponents + +universe v u +namespace CategoryTheory.Cat + +variable (X : Type u) (C : Cat) + +private def typeToCatObjectsAdjHomEquiv : (typeToCat.obj X ⟶ C) ≃ (X ⟶ Cat.objects.obj C) where + toFun f x := f.obj ⟨x⟩ + invFun := Discrete.functor + +private def typeToCatObjectsAdjCounitApp : (Cat.objects ⋙ typeToCat).obj C ⥤ C where + obj := Discrete.as + map := eqToHom ∘ Discrete.eq_of_hom + +/-- `typeToCat : Type ⥤ Cat` is left adjoint to `Cat.objects : Cat ⥤ Type` -/ +def typeToCatObjectsAdj : typeToCat ⊣ Cat.objects := + Adjunction.mk' { + homEquiv := typeToCatObjectsAdjHomEquiv + unit := sorry + counit := { + app := typeToCatObjectsAdjCounitApp + naturality := sorry } + homEquiv_counit := by + intro X Y g + simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, of_α, id_eq] + rfl } + +def connectedComponents : Cat.{v, u} ⥤ Type u where + obj C := ConnectedComponents C + map F := Functor.mapConnectedComponents F + +def connectedComponentsTypeToCatAdj : connectedComponents ⊣ typeToCat := + Adjunction.mk' { + homEquiv := sorry + unit := + { app:= fun C ↦ ConnectedComponents.functorToDiscrete _ (𝟙 (connectedComponents.obj C)) + naturality := by + intro X Y f + simp_all only [Functor.id_obj, Functor.comp_obj, typeToCat_obj, Functor.id_map, + Functor.comp_map, typeToCat_map, of_α, id_eq] + rfl } + counit := sorry + homEquiv_counit := sorry } + +end CategoryTheory.Cat From 38fd4e69d5cb72277cb83e93a70f0deedbbddd8b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Nov 2024 14:15:59 -0800 Subject: [PATCH 16/23] fix: `withInferTypeConfig` --- src/Lean/Meta/InferType.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 5ff735e9da17..82a447c0d393 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -187,7 +187,7 @@ because it overrides unrelated configurations. @[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := withAtLeastTransparency .default do let cfg ← getConfig - if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj != .no then + if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj == .yesWithDelta then x else withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x From c0c366646581740a05fc3572785420f9add82663 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Nov 2024 16:17:14 -0800 Subject: [PATCH 17/23] fix: refine `Meta.Config.beta` behavior --- src/Lean/Meta/WHNF.lean | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 067ab7d7bbd8..f841770ee236 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -572,7 +572,17 @@ where return (← go <| mkAppN (b.instantiate1 v) args) let f := f.getAppFn let f' ← go f - if cfg.beta && f'.isLambda then + /- + If `f'` is a lambda, then we perform beta-reduction here IF + 1- `cfg.beta` is enabled, OR + 2- `f` was not a lambda expression. That is, `f` was reduced, and the beta-reduction step is part + of this step. This is similar to allowing beta-reduction while unfolding expressions even if `cfg.beta := false`. + + We added case 2 because a failure at `norm_cast`. See test `6123_mod_cast.lean`. + Another possible fix to this test is to set `beta := true` at the `Simp.Config` value at + `NormCast.lean`. + -/ + if f'.isLambda && (cfg.beta || !f.isLambda) then let revArgs := e.getAppRevArgs go <| f'.betaRev revArgs else if let some eNew ← whnfDelayedAssigned? f' e then From 439e1e8eebfbc42e78c1cbfe02af6dca2ff59a76 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Dec 2024 16:34:42 -0800 Subject: [PATCH 18/23] fix: do not propagate `beta` and `zeta` from `Simp.Config` to `Meta.Config` See new comment. --- src/Lean/Meta/Tactic/Simp/Types.lean | 29 ++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index d0e20e3ca9a0..e757efef7832 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -144,9 +144,34 @@ Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`. private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do let curr ← Meta.getConfig return { curr with - beta := c.beta + /- + We have decided **not** to propagate `beta` and `zeta` from `Simp.Config` to `Meta.Config`. + The reason is that the `norm_cast` tactic uses `simp` but disables `beta` and `zeta` because + users may not want, for example, their let-expressions to be expanded when using `norm_cast`. + Recall that setting `zeta := true` (and `beta := true`) can dramatically increase term size. + + However, if `beta` and `zeta` are propagated, several occurrences of `norm_cast` fail in Mathlib + because `simp` theorems fail to be applied. This happens when trying to match a theorem's LHS + with the actual term while `beta` and `zeta` are disabled and propagated to `Meta.Config`. + Matching requires `beta` and `zeta` enabled to check for definitional equality. + + That said, not propagating `beta` and `zeta` to `Meta.Config` also has downsides. + For example, it can lead to issues similar to #5455, where the problem is caused by + not propagating `zetaDelta` instead of `beta`. See the following example: + ``` + opaque f : Nat → Nat + @[simp] axiom f_ax : f (no_index 0) = 1 + example : f ((fun x => x) 0) = 1 := by + -- some users may expect the following `simp -beta` to fail, but it succeeds if `beta` is not propagated. + fail_if_success simp -beta + simp + ``` + However, no similar issue has been + reported for `beta` or `zeta` so far, suggesting this may be a minor drawback. + -/ + -- beta := c.beta + -- zeta := c.zeta iota := c.iota - zeta := c.zeta zetaDelta := c.zetaDelta etaStruct := c.etaStruct proj := if c.proj then .yesWithDelta else .no From b85220c373afc0b0175c6dbbfa3ee2d7746df599 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Dec 2024 16:35:44 -0800 Subject: [PATCH 19/23] chore: remove broken test --- tests/lean/run/betaSimp.lean | 5 ----- 1 file changed, 5 deletions(-) delete mode 100644 tests/lean/run/betaSimp.lean diff --git a/tests/lean/run/betaSimp.lean b/tests/lean/run/betaSimp.lean deleted file mode 100644 index bdacf4b204eb..000000000000 --- a/tests/lean/run/betaSimp.lean +++ /dev/null @@ -1,5 +0,0 @@ -opaque f : Nat → Nat -@[simp] axiom f_ax : f (no_index 0) = 1 -example : f ((fun x => x) 0) = 1 := by - fail_if_success simp -beta -- should fail - simp From 0a383499011450773c76d6e46efddc5f1223c61b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2024 13:58:00 -0800 Subject: [PATCH 20/23] feat: use `withInferTypeConfig` while processing implicit arguments We were using ``` withAtLeastTransparency TransparencyMode.default ``` before this commit, but this is problematic when tactics such as `simp` have modified important configuration options such `beta` and `zeta` --- src/Lean/Meta/ExprDefEq.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 8f26f5fa1eba..71ef14f4d0f4 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -304,14 +304,14 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta if info.isInstImplicit then discard <| trySynthPending a₁ discard <| trySynthPending a₂ - unless (← withAtLeastTransparency TransparencyMode.default <| Meta.isExprDefEqAux a₁ a₂) do + unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false for i in postponedHO do let a₁ := args₁[i]! let a₂ := args₂[i]! let info := finfo.paramInfo[i]! if info.isInstImplicit then - unless (← withAtLeastTransparency TransparencyMode.default <| Meta.isExprDefEqAux a₁ a₂) do + unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false else unless (← Meta.isExprDefEqAux a₁ a₂) do @@ -1583,7 +1583,7 @@ private def etaEq (t s : Expr) : Bool := Then, we can enable the flag only when applying `simp` and `rw` theorems. -/ private def withProofIrrelTransparency (k : MetaM α) : MetaM α := - withAtLeastTransparency .default k + withInferTypeConfig k private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do if (← getConfig).proofIrrelevance then From b9521192ca24fa26d0202eae4d93fcd021cd1f5b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2024 14:02:05 -0800 Subject: [PATCH 21/23] chore: remove hack at `mkMetaConfig` We expect the previous commit will fix issues with `norm_cast`. Recall that in the previous commit we use `withInferTypeConfig` to process implicit arguments --- src/Lean/Meta/Tactic/Simp/Types.lean | 29 ++-------------------------- tests/lean/run/betaSimp.lean | 5 +++++ 2 files changed, 7 insertions(+), 27 deletions(-) create mode 100644 tests/lean/run/betaSimp.lean diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index e757efef7832..a8113e2ecb47 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -144,33 +144,8 @@ Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`. private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do let curr ← Meta.getConfig return { curr with - /- - We have decided **not** to propagate `beta` and `zeta` from `Simp.Config` to `Meta.Config`. - The reason is that the `norm_cast` tactic uses `simp` but disables `beta` and `zeta` because - users may not want, for example, their let-expressions to be expanded when using `norm_cast`. - Recall that setting `zeta := true` (and `beta := true`) can dramatically increase term size. - - However, if `beta` and `zeta` are propagated, several occurrences of `norm_cast` fail in Mathlib - because `simp` theorems fail to be applied. This happens when trying to match a theorem's LHS - with the actual term while `beta` and `zeta` are disabled and propagated to `Meta.Config`. - Matching requires `beta` and `zeta` enabled to check for definitional equality. - - That said, not propagating `beta` and `zeta` to `Meta.Config` also has downsides. - For example, it can lead to issues similar to #5455, where the problem is caused by - not propagating `zetaDelta` instead of `beta`. See the following example: - ``` - opaque f : Nat → Nat - @[simp] axiom f_ax : f (no_index 0) = 1 - example : f ((fun x => x) 0) = 1 := by - -- some users may expect the following `simp -beta` to fail, but it succeeds if `beta` is not propagated. - fail_if_success simp -beta - simp - ``` - However, no similar issue has been - reported for `beta` or `zeta` so far, suggesting this may be a minor drawback. - -/ - -- beta := c.beta - -- zeta := c.zeta + beta := c.beta + zeta := c.zeta iota := c.iota zetaDelta := c.zetaDelta etaStruct := c.etaStruct diff --git a/tests/lean/run/betaSimp.lean b/tests/lean/run/betaSimp.lean new file mode 100644 index 000000000000..bdacf4b204eb --- /dev/null +++ b/tests/lean/run/betaSimp.lean @@ -0,0 +1,5 @@ +opaque f : Nat → Nat +@[simp] axiom f_ax : f (no_index 0) = 1 +example : f ((fun x => x) 0) = 1 := by + fail_if_success simp -beta -- should fail + simp From 2a5775e90935dde80d6416b04b722effe2ccbf6e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2024 16:01:42 -0800 Subject: [PATCH 22/23] feat: `zetaDeltaSet` feature --- src/Lean/Elab/Tactic/Simp.lean | 16 ++++++++++++++++ src/Lean/Meta/Basic.lean | 25 +++++++++++++++++++++++++ src/Lean/Meta/Tactic/Simp/Main.lean | 7 ++++--- src/Lean/Meta/Tactic/Simp/Types.lean | 5 +++++ src/Lean/Meta/WHNF.lean | 4 +++- tests/lean/run/zetaDeltaSet.lean | 13 +++++++++++++ 6 files changed, 66 insertions(+), 4 deletions(-) create mode 100644 tests/lean/run/zetaDeltaSet.lean diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index e7bbedcd80dd..9f0ad956db4c 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -173,6 +173,8 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr syntax simpErase := "-" ident -/ let go := withMainContext do + let zetaDeltaSet ← toZetaDeltaSet stx ctx + withZetaDeltaSet zetaDeltaSet do let mut thmsArray := ctx.simpTheorems let mut thms := thmsArray[0]! let mut simprocs := simprocs @@ -234,6 +236,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr logException ex else throw ex + let ctx := ctx.setZetaDeltaSet zetaDeltaSet return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg } -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions. -- This affects `addSimpTheorem`. @@ -277,6 +280,19 @@ where else return .none + /-- If `zetaDelta := false`, create a `FVarId` set with all local let declarations in the `simp` argument list. -/ + toZetaDeltaSet (stx : Syntax) (ctx : Simp.Context) : TacticM FVarIdSet := do + if ctx.config.zetaDelta then return {} + let mut s : FVarIdSet := {} + for arg in stx[1].getSepArgs do + if arg.getKind == ``Lean.Parser.Tactic.simpLemma then + if arg[0].isNone && arg[1].isNone then + let term := arg[2] + let .expr (.fvar fvarId) ← resolveSimpIdTheorem? term | pure () + if (← fvarId.getDecl).isLet then + s := s.insert fvarId + return s + @[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self] structure MkSimpContextResult where diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index c22b0b564fd3..7e0a25e97bba 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -445,6 +445,13 @@ register_builtin_option maxSynthPendingDepth : Nat := { structure Context where private config : Config := {} private configKey : UInt64 := config.toKey + /-- + If `config.zetaDelta := false`, we may select specific local declarations to be unfolded using + the field `zetaDeltaSet`. Note that, we do not include this field in the `Config` structure + because this field is not taken into account while caching results. + Moreover, we reset all caches whenever setting it. + -/ + zetaDeltaSet : FVarIdSet := {} /-- Local context -/ lctx : LocalContext := {} /-- Local instances in `lctx`. -/ @@ -1092,6 +1099,24 @@ Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true` @[inline] def withTrackingZetaDelta (x : n α) : n α := withConfig (fun cfg => { cfg with trackZetaDelta := true }) x +def withZetaDeltaSetImp (s : FVarIdSet) (x : MetaM α) : MetaM α := do + if s.isEmpty then + x + else + let cacheSaved := (← get).cache + modify fun s => { s with cache := {} } + try + withReader (fun ctx => { ctx with zetaDeltaSet := s }) x + finally + modify fun s => { s with cache := cacheSaved } + +/-- +`withZetaDeltaSet s x` executes `x` with `zetaDeltaSet := s`. +The cache is reset while executing `x`. +-/ +def withZetaDeltaSet (s : FVarIdSet) : n α → n α := + mapMetaM <| withZetaDeltaSetImp s + @[inline] def withoutProofIrrelevance (x : n α) : n α := withConfig (fun cfg => { cfg with proofIrrelevance := false }) x diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index f35de4eb6278..3cf9b3e68e3f 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -765,9 +765,10 @@ where trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}" simpLoop e --- TODO: delete -@[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α := - withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x +@[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α := do + withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| + withZetaDeltaSet ctx.zetaDeltaSet <| + withReducible x def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do let ctx ← ctx.setLctxInitIndices diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index a8113e2ecb47..de0977ba5d99 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -54,6 +54,8 @@ abbrev CongrCache := ExprMap (Option CongrTheorem) structure Context where private mk :: config : Config := {} + /-- Local declarations to propagate to `Meta.Context` -/ + zetaDeltaSet : FVarIdSet := {} metaConfig : ConfigWithKey := default indexConfig : ConfigWithKey := default /-- `maxDischargeDepth` from `config` as an `UInt32`. -/ @@ -183,6 +185,9 @@ def Context.setFailIfUnchanged (c : Context) (flag : Bool) : Context := def Context.setMemoize (c : Context) (flag : Bool) : Context := { c with config.memoize := flag } +def Context.setZetaDeltaSet (c : Context) (s : FVarIdSet) : Context := + { c with zetaDeltaSet := s } + def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool := ctx.simpTheorems.isDeclToUnfold declName diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index f841770ee236..7550e62579c6 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -349,7 +349,9 @@ end -- Let-declarations marked as implementation detail should always be unfolded -- We initially added this feature for `simp`, and added it here for consistency. let cfg ← getConfig - unless cfg.zetaDelta || decl.isImplementationDetail do return e + if !decl.isImplementationDetail && !cfg.zetaDelta then + if !(← read).zetaDeltaSet.contains fvarId then + return e if cfg.trackZetaDelta then modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId } whnfEasyCases v k diff --git a/tests/lean/run/zetaDeltaSet.lean b/tests/lean/run/zetaDeltaSet.lean new file mode 100644 index 000000000000..ef3d96b71482 --- /dev/null +++ b/tests/lean/run/zetaDeltaSet.lean @@ -0,0 +1,13 @@ +opaque f : Nat → Nat + +example (a : Nat) : True := by + let x := a + have h1 : f x = 2 := sorry + suffices f a = 2 by sorry + simp only [h1, x] + +example : True := by + let x := 37 + have : x = 2 := sorry + suffices 37 = 2 by sorry + simp only [this, x] From de18902bc71eef371aa9499463c62a1735666d4b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2024 16:42:39 -0800 Subject: [PATCH 23/23] fix: do not check deprecated constants when constructing `zetaDeltaSet` This PR also moves `checkDeprecated` to `Term.Context`. --- src/Lean/Elab/Tactic/Simp.lean | 19 ++++++++++--------- src/Lean/Elab/Term.lean | 20 +++++++++++++++----- 2 files changed, 25 insertions(+), 14 deletions(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 9f0ad956db4c..c3b78a77aefa 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -283,15 +283,16 @@ where /-- If `zetaDelta := false`, create a `FVarId` set with all local let declarations in the `simp` argument list. -/ toZetaDeltaSet (stx : Syntax) (ctx : Simp.Context) : TacticM FVarIdSet := do if ctx.config.zetaDelta then return {} - let mut s : FVarIdSet := {} - for arg in stx[1].getSepArgs do - if arg.getKind == ``Lean.Parser.Tactic.simpLemma then - if arg[0].isNone && arg[1].isNone then - let term := arg[2] - let .expr (.fvar fvarId) ← resolveSimpIdTheorem? term | pure () - if (← fvarId.getDecl).isLet then - s := s.insert fvarId - return s + Term.withoutCheckDeprecated do -- We do not want to report deprecated constants in the first pass + let mut s : FVarIdSet := {} + for arg in stx[1].getSepArgs do + if arg.getKind == ``Lean.Parser.Tactic.simpLemma then + if arg[0].isNone && arg[1].isNone then + let term := arg[2] + let .expr (.fvar fvarId) ← resolveSimpIdTheorem? term | pure () + if (← fvarId.getDecl).isLet then + s := s.insert fvarId + return s @[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self] diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 2cf45a174831..7735095a8c1d 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -326,6 +326,10 @@ structure Context where `refine' (fun x => _) -/ holesAsSyntheticOpaque : Bool := false + /-- + If `checkDeprecated := true`, then `Linter.checkDeprecated` when creating constants. + -/ + checkDeprecated : Bool := true abbrev TermElabM := ReaderT Context $ StateRefT State MetaM abbrev TermElab := Syntax → Option Expr → TermElabM Expr @@ -2026,6 +2030,10 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do trace[Elab.letrec] "mvarId root: {mkMVar mvarId}" return (← get).letRecsToLift.any (·.mvarId == mvarId) +private def checkDeprecatedCore (constName : Name) : TermElabM Unit := do + if (← read).checkDeprecated then + Linter.checkDeprecated constName + /-- Create an `Expr.const` using the given name and explicit levels. Remark: fresh universe metavariables are created if the constant has more universe @@ -2033,9 +2041,8 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do If `checkDeprecated := true`, then `Linter.checkDeprecated` is invoked. -/ -def mkConst (constName : Name) (explicitLevels : List Level := []) (checkDeprecated := true) : TermElabM Expr := do - if checkDeprecated then - Linter.checkDeprecated constName +def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do + checkDeprecatedCore constName let cinfo ← getConstInfo constName if explicitLevels.length > cinfo.levelParams.length then throwError "too many explicit universe levels for '{constName}'" @@ -2046,7 +2053,10 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) (checkDepreca def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do if let .const declName _ := e.getAppFn then - withRef ref do Linter.checkDeprecated declName + withRef ref do checkDeprecatedCore declName + +@[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α → m α := + withTheReader Context (fun ctx => { ctx with checkDeprecated := false }) private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do candidates.foldlM (init := []) fun result (declName, projs) => do @@ -2058,7 +2068,7 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels : At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of `TermElabResult`s. -/ - let const ← mkConst declName explicitLevels (checkDeprecated := false) + let const ← withoutCheckDeprecated <| mkConst declName explicitLevels return (const, projs) :: result def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do