From 0eec29abe483b8849693632d8911e7fb668c5c41 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Sat, 22 Aug 2026 15:03:32 -0400 Subject: [PATCH 1/2] feat: update to Lean v4.33.1 and mirror its kernel changes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v4.33.1 is a kernel release, so this is more than a toolchain bump. Five of its six kernel changes are mirrored here; the sixth was already satisfied. - lean4#14582: `Environment.addInductive` runs `checkUniformIndOccs` before nested-inductive elimination, rejecting occurrences of a datatype being declared that are not applied to the declaration's parameters and universe levels. Occurrences erased by a later `whnf`, and permuted universe levels, are now rejected where they were previously accepted. - lean4#14806: replace the union-find `EquivManager` positive cache with a hash-ordered pair set (`succeededBefore`/`cacheSuccess`), so `isDefEq` no longer depends on the order pairs were checked in. `isDefEq` is a sound but incomplete semi-decision procedure and so is not transitive; closing over its successes made results order-dependent. `Lean4Lean/EquivManager.lean` and `Lean4Lean/Verify/EquivManager.lean` are deleted, and the cache invariant is now `DefEqCache.WF` in `Verify/TypeChecker/Basic.lean`. This also drops `ptrEqExpr_eq` from the axiom dependencies of every `#print axioms` guard that reached it through `quickIsDefEq`. - lean4#14807: no change needed. `isProp` already routed through `ensureSortCore`, so this fork never had the bug upstream fixed. - lean4#14808: `AddInductive.checkRecursors` type-checks each generated recursor and verifies that each computation rule is type-preserving. - lean4#14843: `toCtorWhenStruct` takes a sort-ensuring `isNeverProp` callback rather than matching on `whnf (inferType eType)` with an `unreachable!` fallback, so a non-sort type raises a kernel error. The deliberate `isNeverZero`/`!isAlwaysZero` divergence is preserved. - lean4#14849: bound `Nat` numeral size via a new `FuelConfig.natMaxSize` (default 128 MB, matching `LEAN_NAT_MAX_SIZE`). Literals entering the kernel and the numerals `reduceNat` computes are checked; `reducePow` and the new `reduceShiftLeft` bound their results before forming them, replacing the old `reducePowMaxExp` exponent cap. Batteries stays pinned at v4.33.0: no patch release was cut for v4.33.1, and those sources build unchanged under the new toolchain. Tests: `Tests/UniformIndOccs.lean` ports upstream's `tests/elab/issue_14576_nonuniform.lean` (five rejections, three acceptances) plus the mutual defeq-parameter case from `tests/elab/inductiveDefeqParams.lean`. `Tests/NestedInductive.lean` gains `badUniformDecl`, whose ill-typed dropped parameter sits beside a uniform occurrence so the uniformity check cannot preempt the nested-parameter check it is testing. Docs: ledger entries D018 (toolchain) and D021 (the kernel mirroring), plus fixes to two stale claims in `divergences.md` — `addMutual` described lean4#14608/#14632 as unreleased though they landed in v4.33.0-rc2, and the `restoreNested` entry said lean4lean retains lean4#14621, which it does not. Sorry frontier unchanged at 22. --- Lean4Lean/Audit/SorryFrontier.lean | 1 - Lean4Lean/EquivManager.lean | 64 ---- Lean4Lean/FuelConfig.lean | 4 + Lean4Lean/Inductive/Add.lean | 95 +++++ Lean4Lean/Inductive/Reduce.lean | 13 +- Lean4Lean/Std/Basic.lean | 31 +- Lean4Lean/Tests.lean | 1 + Lean4Lean/Tests/NestedInductive.lean | 25 ++ Lean4Lean/Tests/UniformIndOccs.lean | 177 +++++++++ Lean4Lean/TypeChecker.lean | 137 +++++-- Lean4Lean/Verify/Axioms.lean | 2 +- .../Environment/ConstructorValidation.lean | 11 +- .../ConstructorValidityReplay.lean | 1 - .../Environment/IndexedVecConstructors.lean | 5 +- .../Environment/IndexedVecSemanticReplay.lean | 8 - .../Verify/Environment/InductiveFixtures.lean | 328 ++++++----------- .../Environment/InductiveReplayMatrix.lean | 1 - .../Verify/Environment/Normalization.lean | 48 --- .../Environment/SingletonParityReplay.lean | 2 - Lean4Lean/Verify/EquivManager.lean | 337 ------------------ Lean4Lean/Verify/TypeChecker/Basic.lean | 125 ++++--- Lean4Lean/Verify/TypeChecker/InferType.lean | 5 +- Lean4Lean/Verify/TypeChecker/IsDefEq.lean | 35 +- Lean4Lean/Verify/TypeChecker/Reduce.lean | 128 +++++-- README.md | 4 +- divergences.md | 12 +- flake.lock | 6 +- lean-toolchain | 2 +- plans/roadmap.md | 2 +- upstream-divergence.md | 68 +++- 30 files changed, 815 insertions(+), 863 deletions(-) delete mode 100644 Lean4Lean/EquivManager.lean create mode 100644 Lean4Lean/Tests/UniformIndOccs.lean delete mode 100644 Lean4Lean/Verify/EquivManager.lean diff --git a/Lean4Lean/Audit/SorryFrontier.lean b/Lean4Lean/Audit/SorryFrontier.lean index d1c98fb6..0889b8e0 100644 --- a/Lean4Lean/Audit/SorryFrontier.lean +++ b/Lean4Lean/Audit/SorryFrontier.lean @@ -58,7 +58,6 @@ import Lean4Lean.Verify.Environment.Normalization import Lean4Lean.Verify.Environment.NormalizationMatrix import Lean4Lean.Verify.Environment.SingletonParityMatrix import Lean4Lean.Verify.Environment.SingletonParityReplay -import Lean4Lean.Verify.EquivManager import Lean4Lean.Verify.Expr import Lean4Lean.Verify.Level import Lean4Lean.Verify.LocalContext diff --git a/Lean4Lean/EquivManager.lean b/Lean4Lean/EquivManager.lean deleted file mode 100644 index 51cb3f00..00000000 --- a/Lean4Lean/EquivManager.lean +++ /dev/null @@ -1,64 +0,0 @@ -import Batteries.Data.UnionFind.Basic -import Lean4Lean.PtrEq - -namespace Lean4Lean -open Lean - -abbrev EquivManager.NodeRef := Nat -open EquivManager - -structure EquivManager where - uf : Batteries.UnionFind := {} - toNodeMap : ExprMap NodeRef := {} - -namespace EquivManager - -def find (n : NodeRef) : StateM EquivManager NodeRef := fun m => - if h : n < m.uf.size then - let ⟨uf, root, _⟩ := m.uf.find ⟨n, h⟩ - (root, { m with uf }) - else (n, m) - -def merge (m : EquivManager) (n1 n2 : NodeRef) : EquivManager := - if h1 : n1 < m.uf.size then - if h2 : n2 < m.uf.size then - { m with uf := m.uf.union ⟨n1, h1⟩ ⟨n2, h2⟩ } - else m - else m - -def toNode (e : Expr) : StateM EquivManager NodeRef := fun m => do - if let some r := m.toNodeMap[e]? then - return (r, m) - let { uf, toNodeMap } := m - let r := uf.size - (r, { uf := uf.push, toNodeMap := toNodeMap.insert e r }) - -variable (useHash : Bool) in -def isEquiv (e1 e2 : Expr) : StateM EquivManager Bool := do - if ptrEqExpr e1 e2 then return true - if useHash && e1.hash != e2.hash then return false - if e1.isBVar && e2.isBVar then return e1.bvarIdx! == e2.bvarIdx! - let r1 ← find (← toNode e1) - let r2 ← find (← toNode e2) - if r1 == r2 then return true - let result ← - match e1, e2 with - | .const c1 l1, .const c2 l2 => pure <| c1 == c2 && l1 == l2 - | .mvar a1, .mvar a2 | .fvar a1, .fvar a2 - | .sort a1, .sort a2 | .lit a1, .lit a2 => pure <| a1 == a2 - | .app f1 a1, .app f2 a2 => isEquiv f1 f2 <&&> isEquiv a1 a2 - | .lam _ d1 b1 _, .lam _ d2 b2 _ => isEquiv d1 d2 <&&> isEquiv b1 b2 - | .mdata _ a1, .mdata _ a2 => isEquiv a1 a2 - | .forallE _ d1 b1 _, .forallE _ d2 b2 _ => isEquiv d1 d2 <&&> isEquiv b1 b2 - | .proj _ i1 e1, .proj _ i2 e2 => pure (i1 == i2) <&&> isEquiv e1 e2 - | .letE _ t1 v1 b1 _, .letE _ t2 v2 b2 _ => isEquiv t1 t2 <&&> isEquiv v1 v2 <&&> isEquiv b1 b2 - | _, _ => return false - if result then - modify (merge · r1 r2) - return result -termination_by e1 - -def addEquiv (m : EquivManager) (e1 e2 : Expr) : EquivManager := - let (r1, m) := toNode e1 m - let (r2, m) := toNode e2 m - merge m r1 r2 diff --git a/Lean4Lean/FuelConfig.lean b/Lean4Lean/FuelConfig.lean index 32eb3966..7709ade9 100644 --- a/Lean4Lean/FuelConfig.lean +++ b/Lean4Lean/FuelConfig.lean @@ -28,4 +28,8 @@ structure FuelConfig where recDepth : Nat := 10000 /-- Shared fuel for the structural loops in `Inductive/Add.lean`. -/ inductiveFuel : Nat := 1000 + /-- Upper bound, in bytes, on the `Nat` numerals the kernel will accept or compute while + reducing `Nat` literals. Bounds the memory and time a single reduction can consume. The + native kernel spells this bound `LEAN_NAT_MAX_SIZE` and defaults it to the same 128 MB. -/ + natMaxSize : Nat := 134217728 -- 128 MB; a literal so `simp` cannot renormalize it deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson diff --git a/Lean4Lean/Inductive/Add.lean b/Lean4Lean/Inductive/Add.lean index e665dcd0..b0971bd1 100644 --- a/Lean4Lean/Inductive/Add.lean +++ b/Lean4Lean/Inductive/Add.lean @@ -107,6 +107,11 @@ instance : MonadLCtx M where @[inline] def withEnv (env : Environment) (x : M α) : M α := withReader (fun c => { c with env }) x +/-- Run an action under a different universe parameter list. The recursors are checked under +their own parameters, which carry the extra eliminator level the declaration itself lacks. -/ +@[inline] def withLParams (lparams : List Name) (x : M α) : M α := + withReader (fun c => { c with lparams }) x + /-- Run a closed-metadata action without inheriting validation-local declarations. All other reader fields, including the staged environment and fuel, are preserved exactly. -/ @@ -2652,6 +2657,39 @@ def mkRecRules (indTypes : Array InductiveType) (elimLevel : Level) (stats : Ind rules := rules.push rule return rules.toList +/-- Defensively type-checks the generated recursors. + +`run` installs a recursor and its computation rules without re-checking them. This verifies that +(1) each recursor's type is well typed, and (2) each computation rule is type-preserving: reducing +the recursor applied to a constructor yields a term whose type is the recursor's declared result +type. This catches a recursor whose minor-premise type and reduction rule disagree; checking only +that a rule's right-hand side has *some* type is insufficient, because an under-applied minor +premise is still a well-typed (function) term. -/ +def checkRecursors (indTypes : Array InductiveType) (elimLevel : Level) + (stats : InductiveStats) (motives minors : Array Expr) : M Unit := do + let {lparams, ..} ← read + let lvls := getRecLevels elimLevel stats.levels + withLParams (getRecLevelParams elimLevel lparams) do + for h : dIdx in [:indTypes.size] do + let indType := indTypes[dIdx] + let recName := mkRecName indType.name + let recCi ← (← read).env.get recName + -- (1) The recursor type must be well typed. + _ ← (TypeChecker.checkType recCi.type : TypeChecker.M Expr) + let recPre := mkAppN (mkAppN (mkAppN (.const recName lvls) stats.params) motives) minors + -- (2) Each computation rule must preserve types. + for ctor in indType.ctors do + mkRecInfos.loopCtorArgs stats ctor.type fun t bu _ => do + let (_, itIndices) := getIIndices stats t + let introApp := mkAppN (mkAppN (.const ctor.name stats.levels) stats.params) bu + let lhs := (mkAppN recPre itIndices).app introApp + let expected ← inferType lhs + let reduct ← whnf lhs + let actual ← inferType reduct + unless ← isDefEq actual expected do + throw <| .other s!"generated recursor computation rule for '{ctor.name + }' is not type-preserving" + def run (nparams : Nat) (types : List InductiveType) (numNested : Nat) : M Environment := do let isUnsafe := (← read).safety != .safe let indTypes := types.toArray @@ -2694,6 +2732,7 @@ def run (nparams : Nat) (types : List InductiveType) (numNested : Nat) : M Envir numIndices := stats.nindices[dIdx]! name, all, numMotives, numMinors, rules, k, isUnsafe } + withEnv env <| checkRecursors indTypes elimLevel stats motives minors pure env end AddInductive @@ -2939,6 +2978,61 @@ def checkNoNestedAux (n : Name) (e : Expr) : Except Exception Unit := do | _ => false).isSome then throw <| .other s!"invalid declaration '{n}', it uses the reserved prefix '_nested'" +/-- Checks the occurrence of a datatype being declared at the head of `e`, if there is one. +Returns `true` when the occurrence was checked and `e`'s subterms need not be revisited. -/ +def checkUniformIndOcc (lvls : List Level) (indNames : List Name) (nparams : Nat) + (e : Expr) (offset : Nat) : Except Exception Bool := do + let .const c ls := e.getAppFn | return false + unless indNames.contains c do return false + let args := e.getAppArgs + -- Over-applied: descend, so that occurrences in the indices are checked too. The parameter + -- application itself is visited as a subterm of `e` and checked then. + if args.size > nparams then return false + let ok := args.size == nparams && offset ≥ nparams && ls == lvls + && (List.range nparams).all fun i => args[i]! == .bvar (offset - 1 - i) + unless ok do + throw <| .other s!"invalid occurrence of datatype '{c}' being declared: it must be applied \ + to the parameters and universe levels of the mutual declaration" + return true + +/-- Checks that every occurrence of a datatype being declared in `e` is applied to the +declaration's universe levels and to its parameters, which at binder depth `offset` are the bound +variables `#(offset-1) … #(offset-nparams)`. That those binders really are the parameters is +established later, by the parameter check in `checkConstructors`. -/ +def checkUniformIndOccsIn (lvls : List Level) (indNames : List Name) (nparams : Nat) : + Expr → Nat → Except Exception Unit + | e, offset => do + if ← checkUniformIndOcc lvls indNames nparams e offset then return + match e with + | .forallE _ d b _ | .lam _ d b _ => + checkUniformIndOccsIn lvls indNames nparams d offset + checkUniformIndOccsIn lvls indNames nparams b (offset + 1) + | .letE _ t v b _ => + checkUniformIndOccsIn lvls indNames nparams t offset + checkUniformIndOccsIn lvls indNames nparams v offset + checkUniformIndOccsIn lvls indNames nparams b (offset + 1) + | .app f a => + checkUniformIndOccsIn lvls indNames nparams f offset + checkUniformIndOccsIn lvls indNames nparams a offset + | .mdata _ b => checkUniformIndOccsIn lvls indNames nparams b offset + | .proj _ _ b => checkUniformIndOccsIn lvls indNames nparams b offset + | _ => pure () + +/-- Runs `checkUniformIndOccsIn` over every constructor type of the declaration. + +Later phases inspect the constructor types modulo `whnf`, which can erase an occurrence (as in +`(fun _ => Unit) (T Nat)`), and the parametric arguments of a nested occurrence are dropped from +the auxiliary declaration altogether, so a non-uniform occurrence could escape checking there. +Reduction never creates an occurrence of a datatype being declared, since those are not yet in the +environment, so checking the syntactic occurrences here covers all of them. -/ +def checkUniformIndOccs (lparams : List Name) (nparams : Nat) (types : List InductiveType) : + Except Exception Unit := do + let lvls := lparams.map Level.param + let indNames := types.map (·.name) + for indType in types do + for ctor in indType.ctors do + checkUniformIndOccsIn lvls indNames nparams ctor.type 0 + def Environment.addInductive (env : Environment) (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe allowPrimitive : Bool) (fuel : FuelConfig := {}) : Except Exception Environment := do @@ -2947,6 +3041,7 @@ def Environment.addInductive (env : Environment) (lparams : List Name) (nparams for ctor in indType.ctors do env.checkNoMVarNoFVar ctor.name ctor.type checkNoNestedAux ctor.name ctor.type + checkUniformIndOccs lparams nparams types let res ← ElimNestedInductive.run fuel.inductiveFuel nparams types env |>.run' { lvls := lparams.map .param, newTypes := types.toArray } let numNested := res.aux2nested.size diff --git a/Lean4Lean/Inductive/Reduce.lean b/Lean4Lean/Inductive/Reduce.lean index cdac9f9e..6fdd3925 100644 --- a/Lean4Lean/Inductive/Reduce.lean +++ b/Lean4Lean/Inductive/Reduce.lean @@ -9,6 +9,7 @@ open Kernel section variable [Monad m] (env : Environment) (whnf : Expr → m Expr) (inferType : Expr → m Expr) (isDefEq : Expr → Expr → m Bool) + (isNeverProp : Expr → m Bool) def getFirstCtor (dName : Name) : Option Name := do let some (.inductInfo info) := env.find? dName | none @@ -60,8 +61,11 @@ def toCtorWhenStruct (inductName : Name) (e : Expr) : m Expr := do return e let eType ← whnf (← inferType e) if !eType.getAppFn.isConstOf inductName then return e - let .sort u ← whnf (← inferType eType) | unreachable! - unless u.isNeverZero do return e + -- Lean tests `is_prop eType` and declines to expand when it holds; lean4lean instead requires + -- the level to be *never* zero, so an uncertain level declines too (see `divergences.md`). + -- Either way the level comes from a sort-ensuring check, so a non-sort type raises a kernel + -- error rather than reaching an unreachable branch. + unless ← isNeverProp eType do return e return expandEtaStruct env eType e def getRecRuleFor (rval : RecursorVal) (major : Expr) : Option RecursorRule := do @@ -78,7 +82,8 @@ constructor to everything before the indices in the recursor application (its pa and minor premises) and then to the fields of the constructor application; any arguments after the major premise are re-applied to the result. -/ def inductiveReduceRec [Monad m] (env : Environment) (e : Expr) - (whnf : Expr → m Expr) (inferType : Expr → m Expr) (isDefEq : Expr → Expr → m Bool) : + (whnf : Expr → m Expr) (inferType : Expr → m Expr) (isDefEq : Expr → Expr → m Bool) + (isNeverProp : Expr → m Bool) : m (Option Expr) := do let .const recFn ls := e.getAppFn | return none let some (.recInfo info) := env.find? recFn | return none @@ -91,7 +96,7 @@ def inductiveReduceRec [Monad m] (env : Environment) (e : Expr) match ← whnf major with | .lit (.natVal n) => major := .natLitToConstructor n | .lit (.strVal s) => major ← whnf (.strLitToConstructor s) - | e => major ← toCtorWhenStruct env whnf inferType info.getMajorInduct e + | e => major ← toCtorWhenStruct env whnf inferType isNeverProp info.getMajorInduct e let some rule := getRecRuleFor info major | return none let majorArgs := major.getAppArgs if rule.nfields > majorArgs.size then return none diff --git a/Lean4Lean/Std/Basic.lean b/Lean4Lean/Std/Basic.lean index 2a057dbb..fcbd96c9 100644 --- a/Lean4Lean/Std/Basic.lean +++ b/Lean4Lean/Std/Basic.lean @@ -1,7 +1,6 @@ import Batteries.CodeAction import Batteries.Data.Array.Lemmas import Batteries.Data.HashMap.Basic -import Batteries.Data.UnionFind.Basic import Batteries.Tactic.SeqFocus open Std @@ -217,6 +216,12 @@ instance [BEq α] [PartialEquivBEq α] [BEq β] [PartialEquivBEq β] : PartialEq instance [BEq α] [EquivBEq α] [BEq β] [EquivBEq β] : EquivBEq (α × β) where rfl := by simp [(· == ·)] +instance [BEq α] [Hashable α] [LawfulHashable α] [BEq β] [Hashable β] [LawfulHashable β] : + LawfulHashable (α × β) where + hash_eq a b h := by + simp [(· == ·)] at h + simp [hash, LawfulHashable.hash_eq _ _ h.1, LawfulHashable.hash_eq _ _ h.2] + instance [BEq α] [PartialEquivBEq α] : PartialEquivBEq (List α) where symm := by simp [(· == ·)]; intro a b @@ -257,27 +262,3 @@ instance : LawfulEqOrd UInt64 where end UInt64 -namespace Batteries.UnionFind - -@[simp] theorem size_empty : (∅ : UnionFind).size = 0 := rfl - -@[simp] theorem size_push (uf : UnionFind) : uf.push.size = uf.size + 1 := by - simp [push, size] - -@[simp] theorem size_link (uf : UnionFind) (i j hi) : (uf.link i j hi).size = uf.size := by - simp [link, size] - -@[simp] theorem size_union (uf : UnionFind) (i j) : (uf.union i j).size = uf.size := by - simp [union, size] - -theorem Equiv.eq_of_ge_size (h : Equiv uf a b) (h2 : uf.size ≤ a) : a = b := by - simp [Equiv, rootD, Nat.not_lt.2 h2] at h; split at h - · have := (uf.root ⟨b, ‹_›⟩).2; omega - · exact h - -theorem Equiv.lt_size (h : Equiv uf a b) : a < uf.size ↔ b < uf.size := - suffices ∀ {a b}, Equiv uf a b → b < uf.size → a < uf.size from ⟨this h.symm, this h⟩ - fun h h1 => Nat.not_le.1 fun h2 => Nat.not_le.2 h1 <| h.eq_of_ge_size h2 ▸ h2 - - -end Batteries.UnionFind diff --git a/Lean4Lean/Tests.lean b/Lean4Lean/Tests.lean index 29d37108..d592b956 100644 --- a/Lean4Lean/Tests.lean +++ b/Lean4Lean/Tests.lean @@ -1,5 +1,6 @@ import Lean4Lean.Tests.Toolchain import Lean4Lean.Tests.Environment +import Lean4Lean.Tests.UniformIndOccs import Lean4Lean.Tests.LevelStd import Lean4Lean.Tests.LiteralReadiness import Lean4Lean.Tests.NotationPreludeReplay diff --git a/Lean4Lean/Tests/NestedInductive.lean b/Lean4Lean/Tests/NestedInductive.lean index 9e73c868..b8a237fe 100644 --- a/Lean4Lean/Tests/NestedInductive.lean +++ b/Lean4Lean/Tests/NestedInductive.lean @@ -29,6 +29,22 @@ def treeDecl : Declaration := (tree (.bvar 1)) .default) .default }] }] false +/-- As above, but the dropped parametric argument is ill typed while every occurrence of the +datatype being declared stays uniform, so the uniformity check of lean4#14582 does not preempt +the nested-parameter check this test is about. -/ +def badUniformDecl : Declaration := + .inductDecl [] 1 + [{ name := `Bad1 + type := .forallE `α (.sort 1) (.sort 1) .default + ctors := [{ + name := `Bad1.node + type := .forallE `α (.sort 1) + (.forallE `es + (mkApp2 (mkConst ``Prod [.zero, .zero]) + (mkApp (mkConst `Bad1 []) (.bvar 0)) (mkConst ``Bool.true)) + (mkApp (mkConst `Bad1 []) (.bvar 1)) .default) .default }] }] + false + /-- As above, but the dropped parametric argument `Tree0 Bool.true` is ill typed. -/ def badDecl : Declaration := .inductDecl [] 1 @@ -59,4 +75,13 @@ run_meta do | .ok _ => throwError "nested inductive with an ill-typed parameter was accepted" | .error _ => pure () + -- The same, with the ill-typed parameter beside a uniform occurrence, so the rejection has to + -- come from the nested-parameter check rather than the uniformity check. + match Lean4Lean.addDecl kenv badUniformDecl with + | .ok _ => throwError "nested inductive with an ill-typed parameter was accepted" + | .error (.other msg) => + if "invalid occurrence of datatype".isPrefixOf msg then + throwError "the uniformity check preempted the nested-parameter check" + | .error _ => pure () + end Lean4Lean.Tests.NestedInductive diff --git a/Lean4Lean/Tests/UniformIndOccs.lean b/Lean4Lean/Tests/UniformIndOccs.lean new file mode 100644 index 00000000..f132a676 --- /dev/null +++ b/Lean4Lean/Tests/UniformIndOccs.lean @@ -0,0 +1,177 @@ +import Lean4Lean.Environment + +/-! +The kernel rejects inductive declarations in which a datatype being declared occurs applied to +something other than the parameters and universe levels of the declaration (lean4#14582, the +follow-up to lean4#14576). + +The front end already enforces this and normalizes the occurrences it accepts, so the declarations +below are assembled by hand and handed straight to `Environment.addInductive`. The cases mirror +`tests/elab/issue_14576_nonuniform.lean` upstream. +-/ + +namespace Lean4Lean.Tests.UniformIndOccs + +open Lean Kernel + +/-- Dependencies the fixtures below refer to: a two-element type, two parametric wrappers that +drop or keep their argument, and an identity on types. -/ +inductive W : Type where | mk (p : Bool) +inductive L (α : Type) : Type where | mk +inductive L2 (α : Type) (β : Type) : Type where | mk (a : α) +def Ignore (_ : Type) : Type := Unit +def IdT (α : Type 1) : Type 1 := α + +/-- Runs `addInductive` on a hand-built declaration and reports whether the uniformity check +fired. Any other kernel error is reported as such, so a case that fails downstream instead is not +mistaken for a success of this check. -/ +def addInd (env : Kernel.Environment) (lparams : List Name) (nparams : Nat) + (types : List InductiveType) : Except String Unit := + match Lean4Lean.Environment.addInductive env lparams nparams types false false with + | .ok _ => .ok () + | .error (.other msg) => + if "invalid occurrence of datatype".isPrefixOf msg then .error "nonuniform" + else .error s!"other: {msg}" + | .error _ => .error "other: a structured kernel exception" + +/-- The occurrence check must reject `name`'s declaration. -/ +def expectNonuniform (env : Kernel.Environment) (label : String) (lparams : List Name) + (nparams : Nat) (types : List InductiveType) : Except String Unit := + match addInd env lparams nparams types with + | .ok _ => .error s!"{label}: a non-uniform occurrence was accepted" + | .error "nonuniform" => .ok () + | .error e => .error s!"{label}: expected the uniformity error, got {e}" + +/-- `name`'s declaration must be accepted outright. -/ +def expectAccepted (env : Kernel.Environment) (label : String) (lparams : List Name) + (nparams : Nat) (types : List InductiveType) : Except String Unit := + match addInd env lparams nparams types with + | .ok _ => .ok () + | .error e => .error s!"{label}: a well-formed declaration was rejected ({e})" + +/-- The occurrence check must not fire for `name`'s declaration; it may still fail downstream. -/ +def expectNotNonuniform (env : Kernel.Environment) (label : String) (lparams : List Name) + (nparams : Nat) (types : List InductiveType) : Except String Unit := + match addInd env lparams nparams types with + | .error "nonuniform" => .error s!"{label}: the uniformity check rejected a uniform occurrence" + | _ => .ok () + +run_meta do + let env := (← getEnv).toKernelEnv + let mut checks : Array (Except String Unit) := #[] + let ns := `Lean4Lean.Tests.UniformIndOccs + let W := mkConst (ns ++ `W) + let Wmkfalse := mkApp (mkConst (ns ++ `W.mk)) (mkConst ``false) + let L := mkConst (ns ++ `L) + let L2 := mkConst (ns ++ `L2) + let Ignore := mkConst (ns ++ `Ignore) + let IdT := mkConst (ns ++ `IdT) + let ind name type ctorName ctorType : List InductiveType := + [{ name, type, ctors := [{ name := ctorName, type := ctorType }] }] + + -- The parametric arguments of a nested occurrence `I Ds is` are dropped from the auxiliary + -- declaration the kernel generates, so a non-uniform occurrence inside `Ds` escaped checking. + let E := mkConst `E + checks := checks.push <| expectNonuniform env "nested" [] 1 <| ind `E + (mkForall `w .default W (mkSort 1)) `E.mk + (mkForall `w .default W <| + mkForall `l .default (mkApp L (mkApp E Wmkfalse)) (mkApp E (mkBVar 1))) + + -- A non-uniform occurrence may also hide behind a redex in a phantom argument, where the + -- positivity check never fires. + let F := mkConst `F + let redex := mkApp (mkLambda `g .default (mkForall `_ .default W (mkSort 1)) + (mkApp (mkBVar 0) Wmkfalse)) F + checks := checks.push <| expectNonuniform env "phantom redex" [] 1 <| ind `F + (mkForall `w .default W (mkSort 1)) `F.mk + (mkForall `w .default W <| + mkForall `l .default (mkApp2 L2 (mkApp F (mkBVar 0)) redex) (mkApp F (mkBVar 1))) + + -- The occurrence may also sit in an index of a dropped parameter. + let G := mkConst `G + checks := checks.push <| expectNonuniform env "index of dropped parameter" [] 1 <| ind `G + (mkForall `w .default W (mkForall `i .default (mkSort 1) (mkSort 1))) `G.mk + (mkForall `w .default W <| + mkForall `l .default (mkApp L (mkApp2 G (mkBVar 0) (mkApp G Wmkfalse))) + (mkApp2 G (mkBVar 1) (mkConst ``Nat))) + + -- An occurrence that a later `whnf` erases is rejected too: the field of `D.mk` reduces to + -- `Unit`, so this declaration was accepted before lean4#14582. + let D := mkConst `D + checks := checks.push <| expectNonuniform env "erased by whnf" [] 1 <| ind `D + (mkForall `p .default (mkSort 1) (mkSort 1)) `D.mk + (mkForall `p .default (mkSort 1) <| + mkForall `_ .default (mkApp Ignore (mkApp D (mkConst ``Nat))) (mkApp D (mkBVar 1))) + + -- The universe levels must be uniform as well; this too was accepted before lean4#14582. + checks := checks.push <| expectNonuniform env "permuted universe levels" [`u, `v] 1 <| ind `U + (mkForall `p .default (mkSort 1) (mkSort 1)) `U.mk + (mkForall `p .default (mkSort 1) <| + mkForall `_ .default (mkApp L (mkApp (mkConst `U [.param `v, .param `u]) (mkBVar 0))) + (mkApp (mkConst `U [.param `u, .param `v]) (mkBVar 1))) + + -- A datatype without parameters is unconstrained by this check, so the occurrence of `H` in the + -- index of the dropped parameter is accepted. + let H := mkConst `H + let HNat := mkApp H (mkConst ``Nat) + checks := checks.push <| expectNotNonuniform env "no parameters" [] 0 <| ind `H + (mkForall `i .default (mkSort 1) (mkSort 1)) `H.mk + (mkForall `l .default (mkApp L (mkApp H HNat)) HNat) + + -- A constructor's parameter binder only has to be *definitionally equal* to the corresponding + -- parameter of the type former, which the constructor check verifies. The occurrence check must + -- therefore accept an occurrence applied to that binder, here `p : IdT Type` for `p : Type`. + let V := mkConst `V + checks := checks.push <| expectNotNonuniform env "defeq parameter binder" [] 1 <| ind `V + (mkForall `p .default (mkSort 1) (mkSort 1)) `V.mk + (mkForall `p .default (mkApp IdT (mkSort 1)) <| + mkForall `l .default (mkApp L (mkApp V (mkBVar 0))) (mkApp V (mkBVar 1))) + + -- A constructor type whose leading binders are not the parameters is rejected downstream, so + -- this check need not (and does not) recognize the situation: `C.mk` applies `C` to a + -- `let`-bound variable, which looks like the parameter at that binder depth. + let C := mkConst `C + checks := checks.push <| expectNotNonuniform env "let-bound lookalike parameter" [] 1 <| ind `C + (mkForall `p .default (mkSort 1) (mkSort 1)) `C.mk + (.letE `x (mkSort 1) (mkConst ``Nat) + (mkForall `p .default (mkSort 1) (mkApp C (mkBVar 1))) false) + + -- The parameter types of the datatypes in a mutual declaration only have to agree up to + -- definitional equality, and the constructors of both take the parameter type of the *first* + -- type former. Neither the occurrence check nor the recursor check may reject that + -- (lean4#14808's `tests/elab/inductiveDefeqParams.lean`). + let type1 := mkSort 1 + let idType := mkApp2 (mkConst ``id [.succ (.succ (.succ .zero))]) (mkSort 2) type1 + let Id1 := mkConst `Id1 + let Id2 := mkConst `Id2 + checks := checks.push <| expectAccepted env "defeq mutual parameters" [] 1 + [{ name := `Id1 + type := mkForall `a .default type1 (mkSort 1) + ctors := [{ + name := `Id1.mk + type := mkForall `a .default type1 <| + mkForall `_ .default (mkApp Id2 (mkBVar 0)) (mkApp Id1 (mkBVar 1)) }] }, + { name := `Id2 + type := mkForall `a .default idType (mkSort 1) + ctors := [{ + name := `Id2.mk + type := mkForall `a .default type1 <| + mkForall `_ .default (mkApp Id1 (mkBVar 0)) (mkApp Id2 (mkBVar 1)) }] }] + + for check in checks do + if let .error msg := check then throwError msg + +/-- Uniform occurrences are still accepted, including through a reducible wrapper and across a +mutual block. These go through the front end, so they exercise the check as `addDecl` runs it. -/ +inductive Good (p : Type) where + | mk : List (Good p) → Good p + +inductive T (p : Type) where + | mk : Ignore (T (id p)) → List (T p) → T p + +mutual + inductive A (p : Type) where | mk : List (B p) → A p + inductive B (p : Type) where | mk : Array (A p) → B p +end + +end Lean4Lean.Tests.UniformIndOccs diff --git a/Lean4Lean/TypeChecker.lean b/Lean4Lean/TypeChecker.lean index 70b28f54..c3eefde1 100644 --- a/Lean4Lean/TypeChecker.lean +++ b/Lean4Lean/TypeChecker.lean @@ -1,10 +1,10 @@ import Lean4Lean.Declaration +import Lean4Lean.PtrEq import Lean4Lean.Level import Lean4Lean.Quot import Lean4Lean.Inductive.Reduce import Lean4Lean.Instantiate import Lean4Lean.ForEachExprV -import Lean4Lean.EquivManager import Lean4Lean.FuelConfig namespace Lean4Lean @@ -19,7 +19,7 @@ structure TypeChecker.State where inferTypeC : InferCache := {} whnfCoreCache : ExprMap Expr := {} whnfCache : ExprMap Expr := {} - eqvManager : EquivManager := {} + success : Std.HashSet (Expr × Expr) := {} failure : Std.HashSet (Expr × Expr) := {} unfold : ExprMap Expr := {} @@ -98,6 +98,55 @@ def ensureForallCore (e s : Expr) : RecM Expr := do if e.isForall then return e throw <| .funExpected (← getEnv) (← getLCtx) s +/-- Upper bound on the size in bytes of `n`'s runtime representation, mirroring the kernel's +`lean_nat_size_in_bytes`: a scalar occupies one machine word, and a bignum occupies its GMP limb +count times the limb size. -/ +def natSizeInBytes (n : Nat) : Nat := + let bits := n.log2 + 1 + -- `n` is boxed once it no longer fits in a machine word minus its tag bit. + if bits ≤ 63 then 8 else 8 * ((bits + 63) / 64) + +/-- Rejects a `Nat` numeral whose size exceeds `natMaxSize`. `numBytes` is an upper bound on the +numeral's size, so this may be called before computing it. -/ +def checkNatSize (numBytes : Nat) : RecM Unit := do + if numBytes > (← readThe Context).fuel.natMaxSize then + throw <| .other "the kernel refused a `Nat` numeral because its size exceeds the maximum; \ + raise the `natMaxSize` bound to allow it" + +/-- `Nat.pow` and `Nat.shiftLeft` take their second argument (the exponent, resp. the shift +amount) as a machine `UInt32` in the kernel, so reject one that does not fit rather than +overflowing. -/ +def checkCountArg (count : Nat) (op : String) : RecM Unit := do + if count ≥ UInt32.size then + throw <| .other s!"the kernel refused to evaluate `{op}` because its second argument does \ + not fit in a 32-bit unsigned integer" + +/-- Bounds the numerals entering the kernel (e.g. source literals) by the same limit `reduceNat` +enforces on the ones it computes. -/ +def checkLitSize (l : Literal) : RecM Unit := do + if let .natVal n := l then checkNatSize (natSizeInBytes n) + +/-- `checkNatSize`, conditionally: the size check the binary `Nat` operations that can grow a +numeral without bound run on their result. -/ +def checkNatSizeIf (checkSize : Bool) (numBytes : Nat) : RecM Unit := do + if checkSize then checkNatSize numBytes + +/-- Rejects `base ^ exp` when it would exceed `natMaxSize`, without forming it: the result +occupies at most `natSizeInBytes base * exp` bytes (a `base` of `0` or `1` yields `0`/`1`), and +the bound is compared by division so the product is never formed either. -/ +def checkPowSize (base exp : Nat) : RecM Unit := do + checkCountArg exp "Nat.pow" + if base > 1 && exp != 0 && natSizeInBytes base > (← readThe Context).fuel.natMaxSize / exp then + throw <| .other "the kernel refused to evaluate `Nat.pow` because the result would exceed \ + the maximum numeral size; raise the `natMaxSize` bound to allow it" + +/-- Rejects `v <<< shift` when it would exceed `natMaxSize`, without forming it: the result is +`v * 2 ^ shift`, which occupies about `natSizeInBytes v + shift / 8` bytes. `0 <<< _` is `0`. -/ +def checkShiftLeftSize (v shift : Nat) : RecM Unit := do + if v != 0 then + checkCountArg shift "Nat.shiftLeft" + checkNatSize (natSizeInBytes v + shift / 8 + 1) + /-- Checks that `l` does not contain any level parameters not found in the context `tc`. -/ def checkLevel (tc : Context) (l : Level) : Except Exception Unit := do if let some n2 := l.getUndefParam tc.lparams then @@ -164,6 +213,26 @@ def inferForall (e : Expr) (inferOnly : Bool) : RecM Expr := loop #[] #[] e wher let s ← ensureSortCore r e return .sort <| us.foldr mkLevelIMax' s.sortLevel! +/-- Whether `t` and `s` have already been found definitionally equal. + +The pair is keyed on the order of the two hashes, so a later query finds the entry whichever way +round it presents the pair. This is a plain set of pairs rather than an equivalence-closure +structure on purpose: `isDefEq` is a sound but incomplete semi-decision procedure and so is not +transitive, and taking the transitive closure of its successes would make its result depend on the +order in which pairs were checked (lean4#14806). -/ +def succeededBefore (success : Std.HashSet (Expr × Expr)) (t s : Expr) : Bool := + if t.hash < s.hash then + success.contains (t, s) + else if t.hash > s.hash then + success.contains (s, t) + else + success.contains (t, s) || success.contains (s, t) + +@[inherit_doc succeededBefore] +def cacheSuccess (t s : Expr) : M Unit := do + let k := if t.hash ≤ s.hash then (t, s) else (s, t) + modify fun st => { st with success := st.success.insert k } + /-- Returns whether `t` and `s` are definitionally equal according to Lean's algorithmic definitional equality judgment. @@ -176,14 +245,14 @@ def isDefEqCore (t s : Expr) : RecM Bool := fun m => m.isDefEqCore t s @[inherit_doc isDefEqCore] def isDefEq (t s : Expr) : RecM Bool := do - -- Syntactically equivalent expressions are definitionally equal without - -- consulting or mutating the equivalence manager. Besides avoiding - -- needless work, this keeps exact checker executions compositional when an - -- application argument has precisely the declared domain type. + -- Syntactically equivalent expressions are definitionally equal without consulting or + -- extending the success cache. Besides avoiding needless work, this keeps exact checker + -- executions compositional when an application argument has precisely the declared domain + -- type. if t == s then return true let r ← isDefEqCore t s if r then - modify fun st => { st with eqvManager := st.eqvManager.addEquiv t s } + cacheSuccess t s pure r /-- Infers the type of application `e`, assuming that `e` is already well-typed. -/ @@ -229,6 +298,11 @@ def getSortLevel (e : Expr) : RecM Level := do zero. -/ def isProp (e : Expr) : RecM Bool := return (← getSortLevel e).isAlwaysZero +/-- Checks if `e` is definitely not a proposition, that is, if its type is a sort whose level +cannot normalize to zero under any instantiation. This is strictly stronger than `!(← isProp e)`, +which also holds for the levels that could go either way. -/ +def isNeverProp (e : Expr) : RecM Bool := return (← getSortLevel e).isNeverZero + def invalidProj (e : Expr) : RecM α := do throw <| .invalidProj (← getEnv) (← getLCtx) e @@ -284,6 +358,7 @@ def inferType' (e : Expr) (inferOnly : Bool) : RecM Expr := do return r let r ← match e with | .lit l => + checkLitSize l if !inferOnly then match l with | .natVal _ => _ ← (← getEnv).get ``Nat @@ -342,7 +417,7 @@ def reduceRecursor (e : Expr) : RecM (Option Expr) := do if env.quotInit then if let some r ← quotReduceRec e whnf then return r - if let some r ← inductiveReduceRec env e whnf inferType isDefEq then + if let some r ← inductiveReduceRec env e whnf inferType isDefEq isNeverProp then return r return none @@ -470,19 +545,31 @@ def rawNatLitExt? (e : Expr) : Option Nat := if e == .natZero then some 0 else e /-- Reduces the application `f a b` to a Nat literal if `a` and `b` can be reduced to Nat literals. +`checkSize` bounds the size of the result, for the operations that can grow a numeral without +bound when iterated. Their operands are already bounded, so computing the result before checking +it is cheap. + Note: `f` should have an (efficient) external implementation. -/ -def reduceBinNatOp (f : Nat → Nat → Nat) (a b : Expr) : RecM (Option Expr) := do +def reduceBinNatOp (f : Nat → Nat → Nat) (a b : Expr) (checkSize := false) : RecM (Option Expr) := do let some v1 := rawNatLitExt? (← whnf a) | return none let some v2 := rawNatLitExt? (← whnf b) | return none + checkNatSizeIf checkSize (natSizeInBytes (f v1 v2)) return some <| .lit <| .natVal <| f v1 v2 -def reducePowMaxExp : Nat := 1 <<< 24 - +/-- Reduces `Nat.pow a b`. Unlike the other binary operations this bounds the result *before* +computing it, since a small exponent already denotes an unrepresentable numeral. -/ def reducePow (a b : Expr) : RecM (Option Expr) := do - let some v1 := rawNatLitExt? (← whnf a) | return none - let some v2 := rawNatLitExt? (← whnf b) | return none - if v2 > reducePowMaxExp then return none - return some <| .lit <| .natVal <| Nat.pow v1 v2 + let some base := rawNatLitExt? (← whnf a) | return none + let some exp := rawNatLitExt? (← whnf b) | return none + checkPowSize base exp + return some <| .lit <| .natVal <| Nat.pow base exp + +/-- Reduces `Nat.shiftLeft a b`, bounding the result before computing it. -/ +def reduceShiftLeft (a b : Expr) : RecM (Option Expr) := do + let some v := rawNatLitExt? (← whnf a) | return none + let some shift := rawNatLitExt? (← whnf b) | return none + checkShiftLeftSize v shift + return some <| .lit <| .natVal <| v <<< shift /-- Reduces the application `f a b` to a boolean expression if `a` and `b` can be reduced to Nat literals. @@ -504,12 +591,13 @@ def reduceNat (e : Expr) : RecM (Option Expr) := do let f := e.appFn! if Expr.structuralEq f (.const ``Nat.succ []) then let some v := rawNatLitExt? (← whnf e.appArg!) | return none + checkNatSize (natSizeInBytes (v + 1)) return some <| .lit <| .natVal <| v + 1 else if nargs == 2 then let .app (.app (.const f _) a) b := e | return none - if f == ``Nat.add then return ← reduceBinNatOp Nat.add a b - if f == ``Nat.sub then return ← reduceBinNatOp Nat.sub a b - if f == ``Nat.mul then return ← reduceBinNatOp Nat.mul a b + if f == ``Nat.add then return ← reduceBinNatOp Nat.add a b (checkSize := true) + if f == ``Nat.sub then return ← reduceBinNatOp Nat.sub a b (checkSize := true) + if f == ``Nat.mul then return ← reduceBinNatOp Nat.mul a b (checkSize := true) if f == ``Nat.pow then return ← reducePow a b if f == ``Nat.gcd then return ← reduceBinNatOp Nat.gcd a b if f == ``Nat.mod then return ← reduceBinNatOp Nat.mod a b @@ -519,7 +607,7 @@ def reduceNat (e : Expr) : RecM (Option Expr) := do if f == ``Nat.land then return ← reduceBinNatOp Nat.land a b if f == ``Nat.lor then return ← reduceBinNatOp Nat.lor a b if f == ``Nat.xor then return ← reduceBinNatOp Nat.xor a b - if f == ``Nat.shiftLeft then return ← reduceBinNatOp Nat.shiftLeft a b + if f == ``Nat.shiftLeft then return ← reduceShiftLeft a b if f == ``Nat.shiftRight then return ← reduceBinNatOp Nat.shiftRight a b return none @@ -596,12 +684,9 @@ equality, and otherwise decides two sorts by level equivalence and two literals returning `.false` where these disagree. Two lambdas or two for-alls are handed to `isDefEqLambda`/`isDefEqForall`, which may return either. All remaining cases — including two constants, two free variables, two applications and two projections — are deferred. -/ -def quickIsDefEq (t s : Expr) (useHash := false) : RecM LBool := do - -- optimization for terms that are already α-equivalent or were previously checked - if ← modifyGet fun (.mk a1 a2 a3 a4 a5 a6 a7 (eqvManager := m)) => - let (b, m) := m.isEquiv useHash t s - (b, .mk a1 a2 a3 a4 a5 a6 a7 (eqvManager := m)) - then return .true +def quickIsDefEq (t s : Expr) : RecM LBool := do + -- cheap structural check, plus the positive `isDefEq` cache + if t == s || succeededBefore (← get).success t s then return .true match t, s with | .lam .., .lam .. => toLBoolM <| isDefEqLambda t s | .forallE .., .forallE .. => toLBoolM <| isDefEqForall t s @@ -844,7 +929,7 @@ def isDefEqUnitLike (t s : Expr) : RecM Bool := do @[inherit_doc isDefEqCore] def isDefEqCore' (t s : Expr) : RecM Bool := do - let r ← quickIsDefEq t s (useHash := true) + let r ← quickIsDefEq t s if r != .undef then return r == .true if (!t.hasFVar || (← readThe Context).eagerReduce) && s.isConstOf ``true then diff --git a/Lean4Lean/Verify/Axioms.lean b/Lean4Lean/Verify/Axioms.lean index f620c116..28073cd4 100644 --- a/Lean4Lean/Verify/Axioms.lean +++ b/Lean4Lean/Verify/Axioms.lean @@ -122,7 +122,7 @@ namespace Level `Lean.Level.normalize` and four of its helpers are `partial def`s, so they are opaque and nothing can be proved about them. The `Total` namespace below is a clause-by-clause copy of -[Lean's `Lean/Level.lean`](https://github.com/leanprover/lean4/blob/v4.33.0-rc2/src/Lean/Level.lean#L319-L404), +[Lean's `Lean/Level.lean`](https://github.com/leanprover/lean4/blob/v4.33.1/src/Lean/Level.lean#L319-L404), under the same names, with the termination proofs supplied. That makes `normalize_eq` below a purely syntactic trust assumption, checkable by reading the two definitions side by side; `Lean4Lean.Tests.LevelStd` also checks it on a finite corpus of levels. diff --git a/Lean4Lean/Verify/Environment/ConstructorValidation.lean b/Lean4Lean/Verify/Environment/ConstructorValidation.lean index 467ce916..a76c1baa 100644 --- a/Lean4Lean/Verify/Environment/ConstructorValidation.lean +++ b/Lean4Lean/Verify/Environment/ConstructorValidation.lean @@ -522,7 +522,7 @@ theorem CandidateIsDefEqObservation.observe_eq rw [observeCandidateIsDefEq_of_run context lhs rhs observation.valid] /-- The verified implementation equality checker accepts a syntactically -identical pair without inspecting or mutating its equivalence manager. -/ +identical pair without inspecting or extending its success cache. -/ theorem candidateIsDefEqRefl (context : Context) (source : Expr) : CandidateIsDefEqStep.Valid ⟨context, source, source⟩ := by @@ -8724,7 +8724,6 @@ info: 'Lean4Lean.VInductDecl.StagedNormalizationCandidatePreFamilyInput.checkedW sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -8760,7 +8759,6 @@ info: 'Lean4Lean.VInductDecl.StagedNormalizationCandidatePreFamilyInput.viewDecl sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -8796,7 +8794,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateSemanticRun.ofGenerationShape' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -8832,7 +8829,6 @@ info: 'Lean4Lean.VInductDecl.NormalizationCandidateSemanticRun.producedPackageOf sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -8868,7 +8864,6 @@ info: 'Lean4Lean.VInductDecl.ProducedGenerationShapeCandidate.producedPackage' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -8904,7 +8899,6 @@ info: 'Lean4Lean.VInductDecl.ProducedGenerationShapeCandidate.exactProducedPacka sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -8940,7 +8934,6 @@ info: 'Lean4Lean.VInductDecl.StagedNormalizationCandidatePreFamilyInput.exists' sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -8976,7 +8969,6 @@ info: 'Lean4Lean.VInductDecl.StagedNormalizationCandidatePostFamilyInput.exists' sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -9031,7 +9023,6 @@ info: 'Lean4Lean.VInductDecl.StagedNormalizationCandidateUniverseInput.exists' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, diff --git a/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean b/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean index e7fab338..55ed4343 100644 --- a/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean +++ b/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean @@ -11366,7 +11366,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.cvmStagedPreFamilyInput' depends on axi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, diff --git a/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean b/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean index cf9da634..5b90c637 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean @@ -887,6 +887,7 @@ theorem nilCandidateInductiveReduceRec (fun e => TypeChecker.Inner.whnf e) (fun e => TypeChecker.Inner.inferType e) TypeChecker.Inner.isDefEq + TypeChecker.Inner.isNeverProp methods (tcContext nilCandidateAlphaLctx) state = .ok (none, state) := by unfold inductiveReduceRec @@ -1656,9 +1657,9 @@ def ctorIndexedVecApp (alpha index : Expr) : Expr := theorem ctorIndexedVecInductiveReduceRec {m : Type → Type} [Monad m] (alpha index : Expr) (whnf inferType : Expr → m Expr) - (isDefEq : Expr → Expr → m Bool) : + (isDefEq : Expr → Expr → m Bool) (isNeverProp : Expr → m Bool) : inductiveReduceRec ctorEnv (ctorIndexedVecApp alpha index) - whnf inferType isDefEq = pure none := by + whnf inferType isDefEq isNeverProp = pure none := by unfold inductiveReduceRec rw [ctorIndexedVecAppGetAppFn] simp only diff --git a/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean b/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean index 4132bf55..f820d63f 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean @@ -3233,7 +3233,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecProducedSemanticHierarchy_exi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -3269,7 +3268,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecProducedPostFamilySemantic_ex sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -3305,7 +3303,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecProducedPreFamilySemantic_exi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -3341,7 +3338,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecProducedSemanticHierarchy_con sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -3439,7 +3435,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecSemanticExactProducedGenerati sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -3475,7 +3470,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecSemanticGenerationCandidateSe sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -3511,7 +3505,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecSemanticProducedGenerationCan sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -3547,7 +3540,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.indexedVecSemantic_trEnv'_checked' depe sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, diff --git a/Lean4Lean/Verify/Environment/InductiveFixtures.lean b/Lean4Lean/Verify/Environment/InductiveFixtures.lean index 123b2923..46bd5635 100644 --- a/Lean4Lean/Verify/Environment/InductiveFixtures.lean +++ b/Lean4Lean/Verify/Environment/InductiveFixtures.lean @@ -4,7 +4,6 @@ import Lean4Lean.Inductive.Add import Lean4Lean.Theory.Meta import Lean4Lean.Theory.InductiveFixtures import Lean4Lean.Theory.Typing.Meta -import Batteries.Data.UnionFind.Lemmas /-! End-to-end replay fixtures for inductive environment alignment. @@ -3069,10 +3068,10 @@ private def annotatedPiOutParamArgState : TypeChecker.State := inferTypeC := annotatedPiOutParamFnState.inferTypeC.insert (.sort .zero) (.sort (.succ .zero)) } -private def annotatedPiWithEqvManager - (state : TypeChecker.State) (m : EquivManager) : +private def annotatedPiWithSuccessCache + (state : TypeChecker.State) (m : Std.HashSet (Expr × Expr)) : TypeChecker.State := - { state with eqvManager := m } + { state with success := m } private theorem annotatedPiIsDefEqSort (fuel : Nat) @@ -4317,9 +4316,9 @@ private def annotatedPiDomainBetaState (state : TypeChecker.State) : private theorem annotatedPiInductiveReduceRecDomain {m : Type → Type} [Monad m] (whnf inferType : Expr → m Expr) - (isDefEq : Expr → Expr → m Bool) : + (isDefEq : Expr → Expr → m Bool) (isNeverProp : Expr → m Bool) : inductiveReduceRec annotatedPiTypeKernelEnv annotatedPiRawDomainKernel - whnf inferType isDefEq = + whnf inferType isDefEq isNeverProp = pure none := by unfold inductiveReduceRec rw [show annotatedPiRawDomainKernel.getAppFn = @@ -4603,13 +4602,6 @@ private theorem annotatedPiDomain_whnfM : rw [annotatedPiWhnfLoopDomainConcrete] simp [Functor.map, StateT.map, Except.map] -private theorem annotatedPiPtrDomainSortFalse : - ptrEqExpr annotatedPiRawDomainKernel (.sort .zero) = false := by - apply Bool.eq_false_iff.mpr - intro h - have heq := ptrEqExpr_eq h - cases heq - @[simp] private theorem annotatedPiApp_beq_sort (fn arg : Expr) (u : Level) : ((.app fn arg : Expr) == .sort u) = false := by @@ -4617,87 +4609,58 @@ private theorem annotatedPiPtrDomainSortFalse : rw [Expr.eqv_eq] rfl -@[simp] private theorem annotatedPiUnionFind_coe_root - (self : Batteries.UnionFind) (x : Fin self.size) : - (self.root x : Nat) = self.rootD x := by - rw [Batteries.UnionFind.rootD, dif_pos x.isLt] - -private theorem annotatedPiEmptyEqv_isEquivDomainSort : - ∃ m : EquivManager, - EquivManager.isEquiv true - annotatedPiRawDomainKernel (.sort .zero) - ({} : EquivManager) = - (false, m) := by - let r := EquivManager.isEquiv true - annotatedPiRawDomainKernel (.sort .zero) - ({} : EquivManager) - refine ⟨r.2, Prod.ext ?_ rfl⟩ - dsimp only [r] - rw [EquivManager.isEquiv.eq_def] - simp only [annotatedPiPtrDomainSortFalse, Bool.false_eq_true, - if_false, Bool.true_and] - split - · rfl - · have hroot (n : Nat) : - ({} : Batteries.UnionFind).rootD n = n := by rfl - simp [annotatedPiRawDomainKernel, Expr.isBVar, annotatedPiApp_beq_sort, StateT.pure, pure, - Bind.bind, StateT.bind, EquivManager.toNode, EquivManager.find, hroot] - +/-- `quickIsDefEq` only reads the success cache, so whichever answer the cache gives, the state +comes back unchanged and the result is `.true` or `.undef` -- never `.false`, since an application +and a sort are not settled structurally. -/ private theorem annotatedPiQuickIsDefEqDomainInitial (methods : TypeChecker.Methods) - (context : TypeChecker.Context) (initial : EquivManager) : - ∃ (r : LBool) (m : EquivManager), + (context : TypeChecker.Context) (initial : Std.HashSet (Expr × Expr)) : + ∃ (r : LBool) (m : Std.HashSet (Expr × Expr)), TypeChecker.Inner.quickIsDefEq - annotatedPiRawDomainKernel (.sort .zero) true - methods context ({ eqvManager := initial } : TypeChecker.State) = - .ok (r, ({ eqvManager := m } : TypeChecker.State)) ∧ + annotatedPiRawDomainKernel (.sort .zero) + methods context ({ success := initial } : TypeChecker.State) = + .ok (r, ({ success := m } : TypeChecker.State)) ∧ (r = .true ∨ r = .undef) := by - let q := EquivManager.isEquiv true - annotatedPiRawDomainKernel (.sort .zero) initial - rcases hq : q with ⟨b, m⟩ - have hq' : EquivManager.isEquiv true - annotatedPiRawDomainKernel (.sort .zero) initial = (b, m) := by - simpa [q] using hq - cases b - · refine ⟨.undef, m, ?_, Or.inr rfl⟩ - simp [TypeChecker.Inner.quickIsDefEq, modifyGet, MonadStateOf.modifyGet, monadLift, - MonadLift.monadLift, StateT.modifyGet, pure, Except.pure, hq', Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + have hb : (annotatedPiRawDomainKernel == Expr.sort .zero) = false := + annotatedPiApp_beq_sort .. + by_cases h : TypeChecker.Inner.succeededBefore initial + annotatedPiRawDomainKernel (.sort .zero) = true + · refine ⟨.true, initial, ?_, Or.inl rfl⟩ + simp [TypeChecker.Inner.quickIsDefEq, hb, h, Bind.bind, ReaderT.bind, StateT.bind, Except.bind, + pure, ReaderT.pure, StateT.pure, Except.pure] + · simp only [Bool.not_eq_true] at h + refine ⟨.undef, initial, ?_, Or.inr rfl⟩ + simp [TypeChecker.Inner.quickIsDefEq, hb, h, Bind.bind, ReaderT.bind, StateT.bind, Except.bind, + pure] rfl - · refine ⟨.true, m, ?_, Or.inl rfl⟩ - simp [TypeChecker.Inner.quickIsDefEq, modifyGet, - MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, - StateT.modifyGet, pure, ReaderT.pure, StateT.pure, - Except.pure, hq', Bind.bind, ReaderT.bind, StateT.bind, - Except.bind] @[simp] private theorem annotatedPiWhnfCoreOutParamConstCheap - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.whnfCore (.const ``outParam [.succ .zero]) true (TypeChecker.Methods.withFuel (fuel + 2)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.const ``outParam [.succ .zero], - ({ eqvManager := m } : TypeChecker.State)) := by + ({ success := m } : TypeChecker.State)) := by rfl private theorem annotatedPiWhnfCoreDomainCheap - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.whnfCore annotatedPiRawDomainKernel true (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (annotatedPiRawDomainKernel, - ({ eqvManager := m } : TypeChecker.State)) := by + ({ success := m } : TypeChecker.State)) := by change TypeChecker.Inner.whnfCore' (.app (.const ``outParam [.succ .zero]) (.sort .zero)) true (TypeChecker.Methods.withFuel (fuel + 2)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.app (.const ``outParam [.succ .zero]) (.sort .zero), - ({ eqvManager := m } : TypeChecker.State)) + ({ success := m } : TypeChecker.State)) unfold TypeChecker.Inner.whnfCore' simp only [normalizationRecMBind, normalizationRecMGet, Std.HashMap.getElem?_empty] rw [Expr.withRevApp_eq] @@ -4730,18 +4693,18 @@ private theorem annotatedPiWhnfCoreDomainCheap Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', Level.substParams'] private def annotatedPiOutParamInferOnlyState - (m : EquivManager) : TypeChecker.State := + (m : Std.HashSet (Expr × Expr)) : TypeChecker.State := { inferTypeI := ({} : InferCache).insert (.const ``outParam [.succ .zero]) annotatedPiOutParamFnType, - eqvManager := m } + success := m } private theorem annotatedPiInferTypeOutParamOnly - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.inferType (.const ``outParam [.succ .zero]) true (TypeChecker.Methods.withFuel (fuel + 2)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (annotatedPiOutParamFnType, annotatedPiOutParamInferOnlyState m) := by change @@ -4749,7 +4712,7 @@ private theorem annotatedPiInferTypeOutParamOnly (.const ``outParam [.succ .zero]) true (TypeChecker.Methods.withFuel (fuel + 1)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (annotatedPiOutParamFnType, annotatedPiOutParamInferOnlyState m) unfold TypeChecker.Inner.inferType' @@ -4758,11 +4721,11 @@ private theorem annotatedPiInferTypeOutParamOnly Bind.bind, ReaderT.bind, StateT.bind, Except.bind] private theorem annotatedPiInferAppDomainOnly - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.inferApp annotatedPiRawDomainKernel (TypeChecker.Methods.withFuel (fuel + 2)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.sort (.succ .zero), annotatedPiOutParamInferOnlyState m) := by unfold TypeChecker.Inner.inferApp @@ -4775,25 +4738,25 @@ private theorem annotatedPiInferAppDomainOnly simp [TypeChecker.Inner.inferApp.loop, annotatedPiOutParamFnType] private def annotatedPiDomainInferOnlyState - (m : EquivManager) : TypeChecker.State := + (m : Std.HashSet (Expr × Expr)) : TypeChecker.State := { inferTypeI := (({} : InferCache).insert (.const ``outParam [.succ .zero]) annotatedPiOutParamFnType).insert annotatedPiRawDomainKernel (.sort (.succ .zero)), - eqvManager := m } + success := m } private theorem annotatedPiInferTypeDomainOnlyAny - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.inferType annotatedPiRawDomainKernel true (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.sort (.succ .zero), annotatedPiDomainInferOnlyState m) := by change TypeChecker.Inner.inferType' annotatedPiRawDomainKernel true (TypeChecker.Methods.withFuel (fuel + 2)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.sort (.succ .zero), annotatedPiDomainInferOnlyState m) rw [show annotatedPiRawDomainKernel = .app (.const ``outParam [.succ .zero]) (.sort .zero) by rfl] @@ -4808,12 +4771,12 @@ private theorem annotatedPiInferTypeDomainOnlyAny simp [annotatedPiOutParamInferOnlyState] private theorem annotatedPiInferTypeDomainOnly998 - (m : EquivManager) : + (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.inferType' (.app (.const ``outParam [.succ .zero]) (.sort .zero)) true (TypeChecker.Methods.withFuel 9998) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.sort (.succ .zero), annotatedPiDomainInferOnlyState m) := by unfold TypeChecker.Inner.inferType' simp [Expr.hasLooseBVars, Expr.looseBVarRange', @@ -4825,26 +4788,26 @@ private theorem annotatedPiInferTypeDomainOnly998 rw [show TypeChecker.Inner.inferApp annotatedPiRawDomainKernel (TypeChecker.Methods.withFuel 9998) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.sort (.succ .zero), annotatedPiOutParamInferOnlyState m) by simpa only [Nat.reduceAdd] using annotatedPiInferAppDomainOnly 9996 m] simp [annotatedPiOutParamInferOnlyState] private def annotatedPiSortOneInferOnlyState - (m : EquivManager) : TypeChecker.State := + (m : Std.HashSet (Expr × Expr)) : TypeChecker.State := { annotatedPiDomainInferOnlyState m with inferTypeI := (annotatedPiDomainInferOnlyState m).inferTypeI.insert (.sort (.succ .zero)) (.sort (.succ (.succ .zero))) } @[simp] private theorem annotatedPiDomainInferOnlyState_sortOneMiss - (m : EquivManager) : + (m : Std.HashSet (Expr × Expr)) : (annotatedPiDomainInferOnlyState m).inferTypeI[ (.sort (.succ .zero) : Expr)]? = none := by simp [annotatedPiDomainInferOnlyState, annotatedPiRawDomainKernel, annotatedPiOutParamFnType] private theorem annotatedPiInferTypeSortOneOnly - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.inferType (.sort (.succ .zero)) true (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker @@ -4873,7 +4836,7 @@ private theorem annotatedPiInferTypeSortOneOnly rfl private theorem annotatedPiIsPropSortOneFalse - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.isProp (.sort (.succ .zero)) (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker @@ -4885,12 +4848,12 @@ private theorem annotatedPiIsPropSortOneFalse rfl private theorem annotatedPiIsDefEqProofIrrelDomain - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.isDefEqProofIrrel annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = + ({ success := m } : TypeChecker.State) = .ok (.undef, annotatedPiSortOneInferOnlyState m) := by unfold TypeChecker.Inner.isDefEqProofIrrel simp only [normalizationRecMBind] @@ -4972,7 +4935,7 @@ private theorem annotatedPiUnfoldDomainOfMiss rfl private theorem annotatedPiWhnfCoreDomainBetaCheap - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.whnfCore annotatedPiDomainBetaKernel true (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker @@ -5015,22 +4978,14 @@ private theorem annotatedPiQuickIsDefEqSortZeroAny (methods : TypeChecker.Methods) (context : TypeChecker.Context) (initial : TypeChecker.State) : - ∃ m : EquivManager, - TypeChecker.Inner.quickIsDefEq (.sort .zero) (.sort .zero) false + ∃ m : Std.HashSet (Expr × Expr), + TypeChecker.Inner.quickIsDefEq (.sort .zero) (.sort .zero) methods context initial = - .ok (.true, annotatedPiWithEqvManager initial m) := by - let r := EquivManager.isEquiv false - (.sort .zero) (.sort .zero) initial.eqvManager - rcases hr : r with ⟨b, m⟩ - have hr' : EquivManager.isEquiv false - (.sort .zero) (.sort .zero) initial.eqvManager = (b, m) := by - simpa [r] using hr - refine ⟨m, ?_⟩ - cases b <;> - simp [TypeChecker.Inner.quickIsDefEq, modifyGet, MonadStateOf.modifyGet, monadLift, - MonadLift.monadLift, StateT.modifyGet, pure, ReaderT.pure, StateT.pure, Except.pure, hr', - annotatedPiWithEqvManager, Level.isEquiv, Level.isEquiv', Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + .ok (.true, annotatedPiWithSuccessCache initial m) := by + -- The two sides are syntactically equal, so the structural check settles it without the cache. + refine ⟨initial.success, ?_⟩ + simp [TypeChecker.Inner.quickIsDefEq, annotatedPiWithSuccessCache, pure, ReaderT.pure, + StateT.pure, Except.pure, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] private theorem annotatedPiIsDeltaDomain : TypeChecker.Inner.isDelta annotatedPiTypeKernelEnv @@ -5057,7 +5012,7 @@ private theorem annotatedPiIsDeltaDomain : rfl private theorem annotatedPiDeltaDomain - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : (TypeChecker.Inner.unfoldDefinition annotatedPiRawDomainKernel >>= fun e => TypeChecker.Inner.whnfCore e.get! true) (TypeChecker.Methods.withFuel (fuel + 3)) @@ -5078,15 +5033,15 @@ private theorem annotatedPiDeltaDomain rw [annotatedPiWhnfCoreDomainBetaCheap fuel] private theorem annotatedPiLazyDeltaStepDomain - (fuel : Nat) (m : EquivManager) : - ∃ m' : EquivManager, + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : + ∃ m' : Std.HashSet (Expr × Expr), TypeChecker.Inner.lazyDeltaReductionStep annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker (annotatedPiSortOneInferOnlyState m) = .ok (.bool true, - annotatedPiWithEqvManager + annotatedPiWithSuccessCache (annotatedPiOutParamUnfoldState (annotatedPiSortOneInferOnlyState m)) m') := by obtain ⟨m', hquick⟩ := annotatedPiQuickIsDefEqSortZeroAny @@ -5114,7 +5069,7 @@ private theorem annotatedPiLazyDeltaStepDomain rfl @[simp] private theorem annotatedPiIsDefEqOffsetDomain - (fuel : Nat) (m : EquivManager) : + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : TypeChecker.Inner.isDefEqOffset annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 3)) @@ -5131,15 +5086,15 @@ private theorem annotatedPiLazyDeltaStepDomain Expr.natZero] private theorem annotatedPiLazyDeltaLoopDomain - (fuel : Nat) (m : EquivManager) : - ∃ m' : EquivManager, + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : + ∃ m' : Std.HashSet (Expr × Expr), TypeChecker.Inner.lazyDeltaReduction.loop annotatedPiRawDomainKernel (.sort .zero) 1000 (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker (annotatedPiSortOneInferOnlyState m) = .ok (.bool true, - annotatedPiWithEqvManager + annotatedPiWithSuccessCache (annotatedPiOutParamUnfoldState (annotatedPiSortOneInferOnlyState m)) m') := by obtain ⟨m', hstep⟩ := annotatedPiLazyDeltaStepDomain fuel m @@ -5182,15 +5137,15 @@ private theorem annotatedPiLazyDeltaLoopDomain rfl private theorem annotatedPiLazyDeltaDomain - (fuel : Nat) (m : EquivManager) : - ∃ m' : EquivManager, + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : + ∃ m' : Std.HashSet (Expr × Expr), TypeChecker.Inner.lazyDeltaReduction annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker (annotatedPiSortOneInferOnlyState m) = .ok (.bool true, - annotatedPiWithEqvManager + annotatedPiWithSuccessCache (annotatedPiOutParamUnfoldState (annotatedPiSortOneInferOnlyState m)) m') := by obtain ⟨m', hloop⟩ := annotatedPiLazyDeltaLoopDomain fuel m @@ -5208,33 +5163,16 @@ private theorem annotatedPiLazyDeltaDomain exact hloop private theorem annotatedPiQuickIsDefEqDomainAny - (fuel : Nat) (m : EquivManager) : - ∃ (r : LBool) (m' : EquivManager), + (fuel : Nat) (m : Std.HashSet (Expr × Expr)) : + ∃ (r : LBool) (m' : Std.HashSet (Expr × Expr)), TypeChecker.Inner.quickIsDefEq - annotatedPiRawDomainKernel (.sort .zero) false + annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := m } : TypeChecker.State) = - .ok (r, ({ eqvManager := m' } : TypeChecker.State)) ∧ - (r = .true ∨ r = .undef) := by - let q := EquivManager.isEquiv false - annotatedPiRawDomainKernel (.sort .zero) m - rcases hq : q with ⟨b, m'⟩ - have hq' : EquivManager.isEquiv false - annotatedPiRawDomainKernel (.sort .zero) m = (b, m') := by - simpa [q] using hq - cases b - · refine ⟨.undef, m', ?_, Or.inr rfl⟩ - simp [TypeChecker.Inner.quickIsDefEq, modifyGet, MonadStateOf.modifyGet, monadLift, - MonadLift.monadLift, StateT.modifyGet, pure, Except.pure, hq', Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] - rfl - · refine ⟨.true, m', ?_, Or.inl rfl⟩ - simp [TypeChecker.Inner.quickIsDefEq, modifyGet, - MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, - StateT.modifyGet, pure, ReaderT.pure, StateT.pure, - Except.pure, hq', Bind.bind, ReaderT.bind, StateT.bind, - Except.bind] + ({ success := m } : TypeChecker.State) = + .ok (r, ({ success := m' } : TypeChecker.State)) ∧ + (r = .true ∨ r = .undef) := + annotatedPiQuickIsDefEqDomainInitial _ _ m @[simp] private theorem annotatedPiWhnfCoreSortCheap (fuel : Nat) (state : TypeChecker.State) : @@ -5245,13 +5183,13 @@ private theorem annotatedPiQuickIsDefEqDomainAny rfl private theorem annotatedPiIsDefEqCoreDomain - (fuel : Nat) (initial : EquivManager := {}) : + (fuel : Nat) (initial : Std.HashSet (Expr × Expr) := {}) : ∃ state : TypeChecker.State, TypeChecker.Inner.isDefEqCore' annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (true, state) := by obtain ⟨r, m, hquick, hr⟩ := annotatedPiQuickIsDefEqDomainInitial (TypeChecker.Methods.withFuel (fuel + 3)) @@ -5264,7 +5202,7 @@ private theorem annotatedPiIsDefEqCoreDomain simp only rw [show (LBool.true != LBool.undef) = true by rfl] simp only [if_true] - exact ⟨({ eqvManager := m } : TypeChecker.State), rfl⟩ + exact ⟨({ success := m } : TypeChecker.State), rfl⟩ · subst r simp only rw [show (LBool.undef != LBool.undef) = false by rfl] @@ -5292,7 +5230,7 @@ private theorem annotatedPiIsDefEqCoreDomain rw [normalizationRecMBind] obtain ⟨m'', hlazy⟩ := annotatedPiLazyDeltaDomain fuel m rw [hlazy] - refine ⟨annotatedPiWithEqvManager + refine ⟨annotatedPiWithSuccessCache (annotatedPiOutParamUnfoldState (annotatedPiSortOneInferOnlyState m)) m'', ?_⟩ rfl @@ -5306,7 +5244,7 @@ private theorem annotatedPiIsDefEqCoreDomain · subst r rw [show (LBool.true != LBool.undef) = true by rfl] simp only [if_true] - refine ⟨({ eqvManager := m' } : TypeChecker.State), ?_⟩ + refine ⟨({ success := m' } : TypeChecker.State), ?_⟩ rfl · subst r rw [show (LBool.undef != LBool.undef) = false by rfl] @@ -5319,18 +5257,18 @@ private theorem annotatedPiIsDefEqCoreDomain rw [normalizationRecMBind] obtain ⟨m'', hlazy⟩ := annotatedPiLazyDeltaDomain fuel m' rw [hlazy] - refine ⟨annotatedPiWithEqvManager + refine ⟨annotatedPiWithSuccessCache (annotatedPiOutParamUnfoldState (annotatedPiSortOneInferOnlyState m')) m'', ?_⟩ rfl private theorem annotatedPiDomain_isDefEqInner - (fuel : Nat) (initial : EquivManager := {}) : + (fuel : Nat) (initial : Std.HashSet (Expr × Expr) := {}) : ∃ state : TypeChecker.State, TypeChecker.Inner.isDefEq annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 4)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (true, state) := by obtain ⟨state, hcore⟩ := annotatedPiIsDefEqCoreDomain fuel initial have hcore' : @@ -5338,14 +5276,14 @@ private theorem annotatedPiDomain_isDefEqInner annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 4)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (true, state) := by change TypeChecker.Inner.isDefEqCore' annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel (fuel + 3)) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (true, state) exact hcore unfold TypeChecker.Inner.isDefEq @@ -6014,7 +5952,7 @@ private theorem annotatedPiInferTypeFamilyAfterDomainOnly_literal : whnfCoreCache := (annotatedPiDomainInferOnlyState {}).whnfCoreCache whnfCache := (annotatedPiDomainInferOnlyState {}).whnfCache - eqvManager := (annotatedPiDomainInferOnlyState {}).eqvManager + success := (annotatedPiDomainInferOnlyState {}).success failure := (annotatedPiDomainInferOnlyState {}).failure unfold := (annotatedPiDomainInferOnlyState {}).unfold } = .ok (.sort (.succ .zero), annotatedPiFamilyInferOnlyState) := by @@ -8774,24 +8712,24 @@ private theorem annotatedPiAlignedViewCtorKernel_eq : set_option maxRecDepth 10000 in private theorem annotatedPiDomain_isDefEqInner9999 - (initial : EquivManager) : + (initial : Std.HashSet (Expr × Expr)) : ∃ state : TypeChecker.State, TypeChecker.Inner.isDefEq annotatedPiRawDomainKernel (.sort .zero) (TypeChecker.Methods.withFuel 9999) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (true, state) := by simpa only [Nat.reduceAdd] using annotatedPiDomain_isDefEqInner 9995 initial private theorem annotatedPiInnerView_isDefEqForall - (initial : EquivManager) : + (initial : Std.HashSet (Expr × Expr)) : ∃ state : TypeChecker.State, TypeChecker.Inner.isDefEqForall annotatedPiInnerKernel annotatedPiViewInnerKernel #[] (TypeChecker.Methods.withFuel 9999) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (true, state) := by obtain ⟨state, domainRun⟩ := annotatedPiDomain_isDefEqInner9999 initial @@ -8800,7 +8738,7 @@ private theorem annotatedPiInnerView_isDefEqForall ((.sort .zero : Expr).instantiateRev #[]) (TypeChecker.Methods.withFuel 9999) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (true, state) := by simpa [Expr.instantiateRev] using domainRun refine ⟨state, ?_⟩ @@ -8816,37 +8754,32 @@ private theorem annotatedPiInnerView_isDefEqForall Expr.looseBVarRange'] private theorem annotatedPiInnerView_quickIsDefEq - (initial : EquivManager) : + (initial : Std.HashSet (Expr × Expr)) : ∃ state : TypeChecker.State, TypeChecker.Inner.quickIsDefEq - annotatedPiInnerKernel annotatedPiViewInnerKernel true + annotatedPiInnerKernel annotatedPiViewInnerKernel (TypeChecker.Methods.withFuel 9999) annotatedPiCtorCandidateContext.toTypeChecker - ({ eqvManager := initial } : TypeChecker.State) = + ({ success := initial } : TypeChecker.State) = .ok (.true, state) := by - let q := EquivManager.isEquiv true annotatedPiInnerKernel - annotatedPiViewInnerKernel initial - rcases hq : q with ⟨equal, manager⟩ - have hq' : EquivManager.isEquiv true annotatedPiInnerKernel - annotatedPiViewInnerKernel initial = (equal, manager) := by - simpa [q] using hq - cases equal - · obtain ⟨state, forallRun⟩ := - annotatedPiInnerView_isDefEqForall manager + by_cases hc : (annotatedPiInnerKernel == annotatedPiViewInnerKernel || + TypeChecker.Inner.succeededBefore initial + annotatedPiInnerKernel annotatedPiViewInnerKernel) = true + -- Settled structurally or by the cache: the state comes back untouched. + · refine ⟨({ success := initial } : TypeChecker.State), ?_⟩ + unfold TypeChecker.Inner.quickIsDefEq + simp [hc, pure, ReaderT.pure, StateT.pure, Except.pure, + Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + -- Otherwise both sides are for-alls and the match hands off to `isDefEqForall`. + · simp only [Bool.not_eq_true] at hc + obtain ⟨state, forallRun⟩ := annotatedPiInnerView_isDefEqForall initial refine ⟨state, ?_⟩ - unfold annotatedPiInnerKernel annotatedPiViewInnerKernel at hq' forallRun ⊢ + unfold annotatedPiInnerKernel annotatedPiViewInnerKernel at hc forallRun ⊢ unfold TypeChecker.Inner.quickIsDefEq - simp [modifyGet, MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, StateT.modifyGet, pure, - Except.pure, hq', Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [hc, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] unfold toLBoolM rw [normalizationRecMBind, forallRun] rfl - · refine ⟨({ eqvManager := manager } : TypeChecker.State), ?_⟩ - unfold TypeChecker.Inner.quickIsDefEq - simp [modifyGet, MonadStateOf.modifyGet, monadLift, - MonadLift.monadLift, StateT.modifyGet, pure, ReaderT.pure, - StateT.pure, Except.pure, hq', - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] private theorem annotatedPiInnerView_isDefEqInner : ∃ state : TypeChecker.State, @@ -10753,7 +10686,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerFamily_candidateRun_exists' sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -10804,7 +10736,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerFamily_candidateView_tr' dep sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -10840,7 +10771,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerNormalizationCandidateRun' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -10876,7 +10806,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerCandidateNormalization_eq' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -10938,7 +10867,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasRecField_hasType_checked' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11050,7 +10978,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerFamily_isType_checked' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11086,7 +11013,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerCtor_isType_checked' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11122,7 +11048,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerNormalization_wf_checked' de sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11158,7 +11083,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasRecNormalization_wf_checked' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11194,7 +11118,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerBlock_wf_checked' depends on sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11230,7 +11153,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerProducedSemanticHierarchy_ex sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11266,7 +11188,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerProducedPostFamilySemantic_e sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11302,7 +11223,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerProducedPreFamilySemantic_ex sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11338,7 +11258,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerGenerationCandidateSemanticR sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11374,7 +11293,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerGenerationCandidateRun' depe sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11410,7 +11328,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerGenerationCandidatePackage' sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11480,7 +11397,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerExactProducedGenerationCandi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11516,7 +11432,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerProducedGenerationCandidateP sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11552,7 +11467,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormer_addInductCertified_checked' sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11588,7 +11502,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerGenerationChecked_wf_checked sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11624,7 +11537,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasRecBlock_wf_checked' depends on ax sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11660,7 +11572,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasRecGenerationChecked_wf_checked' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11696,7 +11607,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormerAddInductTraceChecked' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11732,7 +11642,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasFormer_trEnv'_checked' depends on sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11768,7 +11677,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasRecAddInductTraceChecked' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11804,7 +11712,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.aliasRec_trEnv'_checked' depends on axi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11909,7 +11816,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiProducedSemanticHierarchy_ex sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11945,7 +11851,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiProducedPostFamilySemantic_e sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -11981,7 +11886,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiProducedPreFamilySemantic_ex sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12017,7 +11921,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiNormalizationCandidateRun' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12053,7 +11956,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiGenerationCandidateSemanticR sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12089,7 +11991,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiGenerationCandidateRun' depe sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12125,7 +12026,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiGenerationCandidatePackage' sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12251,7 +12151,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiExactProducedGenerationCandi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12287,7 +12186,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiProducedGenerationCandidateP sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12323,7 +12221,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPi_addInductCertified' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12359,7 +12256,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiGenerationChecked_wf_checked sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12395,7 +12291,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPiAddInductTraceChecked' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -12431,7 +12326,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.annotatedPi_trEnv'_checked' depends on sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, diff --git a/Lean4Lean/Verify/Environment/InductiveReplayMatrix.lean b/Lean4Lean/Verify/Environment/InductiveReplayMatrix.lean index b907c9e3..5ad88ca9 100644 --- a/Lean4Lean/Verify/Environment/InductiveReplayMatrix.lean +++ b/Lean4Lean/Verify/Environment/InductiveReplayMatrix.lean @@ -718,7 +718,6 @@ info: 'Lean4Lean.CompleteInductiveReplay.completeReplayMatrix_metadataComplete' sorryAx, Classical.choice, Lean4Lean.ptrEqConstantInfo_eq, - Lean4Lean.ptrEqExpr_eq, Quot.sound, Lean.Expr.abstractRange_eq, Lean.Expr.abstract_eq, diff --git a/Lean4Lean/Verify/Environment/Normalization.lean b/Lean4Lean/Verify/Environment/Normalization.lean index 805b3fb1..63493f9b 100644 --- a/Lean4Lean/Verify/Environment/Normalization.lean +++ b/Lean4Lean/Verify/Environment/Normalization.lean @@ -5346,7 +5346,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprRun.view_isType_of_terminalSort' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5382,7 +5381,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprSemanticRootRun.source_isType_of_termi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5440,7 +5438,6 @@ info: 'Lean4Lean.VInductDecl.CandidateFamilyStagedInput.rawWF' depends on axioms sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5476,7 +5473,6 @@ info: 'Lean4Lean.VInductDecl.CandidateFamilyStagedInput.postContext' depends on sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5512,7 +5508,6 @@ info: 'Lean4Lean.VInductDecl.CandidateFamilyStagedInput.postContextRun' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5548,7 +5543,6 @@ info: 'Lean4Lean.VInductDecl.CandidateFamilyStagedInput.postFamily' depends on a sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5585,7 +5579,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprSemanticRootInput.exists' depends on a sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5621,7 +5614,6 @@ info: 'Lean4Lean.VInductDecl.CandidateConstructorSemanticListInput.exists' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5657,7 +5649,6 @@ info: 'Lean4Lean.VInductDecl.NormalizationCandidateSemanticInput.exists_ofProduc sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5693,7 +5684,6 @@ info: 'Lean4Lean.VInductDecl.StagedNormalizationCandidateSemanticInput.exists' d sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5729,7 +5719,6 @@ info: 'Lean4Lean.VInductDecl.CandidateFamilySemanticGenerationRun.run' depends o sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5765,7 +5754,6 @@ info: 'Lean4Lean.VInductDecl.CandidateSemanticNormalizedCtorListRun.run' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5801,7 +5789,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateSemanticRun.run' depends on axio sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5837,7 +5824,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateSemanticShapeRun.run' depends on sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5914,7 +5900,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateSemanticRun.package' depends on sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -5950,7 +5935,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateSemanticRun.producedPackage' dep sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6031,7 +6015,6 @@ info: 'Lean4Lean.TypeChecker.candidateCheckTypeStep_exists_translation' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6073,7 +6056,6 @@ info: 'Lean4Lean.TypeChecker.IsDefEqRun.isDefEqU' depends on axioms: [propext, sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6123,7 +6105,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprRun.exists_ofCandidate' depends on axi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6159,7 +6140,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprRun.exists_ofCandidateFVars' depends o sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6213,7 +6193,6 @@ info: 'Lean4Lean.TypeChecker.CandidateNodeRun.exists_ofCandidate' depends on axi sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6249,7 +6228,6 @@ info: 'Lean4Lean.TypeChecker.CandidateNodeRun.evidence' depends on axioms: [prop sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6285,7 +6263,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprRun.evidence' depends on axioms: [prop sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6327,7 +6304,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprRun.view_tr' depends on axioms: [prope sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6363,7 +6339,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprRootRun.evidence' depends on axioms: [ sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6399,7 +6374,6 @@ info: 'Lean4Lean.TypeChecker.TelDefEqEvidence.telDefEq' depends on axioms: [prop sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6441,7 +6415,6 @@ info: 'Lean4Lean.TypeChecker.TelResultDefEqEvidence.replacePrefix' depends on ax sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6477,7 +6450,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprRun.spineEvidence' depends on axioms: sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6513,7 +6485,6 @@ info: 'Lean4Lean.TypeChecker.CandidateExprSpineRun.evidenceAt' depends on axioms sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6579,7 +6550,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateRun.typeEnv_wf' depends on axiom sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6615,7 +6585,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateRun.familyConst_hasType' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6651,7 +6620,6 @@ info: 'Lean4Lean.VInductDecl.CandidateNormalizedCtorRun.rightType_ofChecked' dep sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6693,7 +6661,6 @@ info: 'Lean4Lean.VInductDecl.CandidateNormalizedCtorRun.normalizedCtorRun' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6729,7 +6696,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidateRun.wf' depends on axioms: [prop sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6773,7 +6739,6 @@ info: 'Lean4Lean.VInductDecl.CandidateConstructorListRun.evidence' depends on ax sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6817,7 +6782,6 @@ info: 'Lean4Lean.VInductDecl.NormalizationCandidateRun.normalizationRun' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6853,7 +6817,6 @@ info: 'Lean4Lean.VInductDecl.NormalizedCtorRun.wf' depends on axioms: [propext, sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6889,7 +6852,6 @@ info: 'Lean4Lean.VInductDecl.GenerationRun.wf' depends on axioms: [propext, sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6939,7 +6901,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidatePackage.certificate' depends on sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -6975,7 +6936,6 @@ info: 'Lean4Lean.VInductDecl.GenerationCandidatePackage.addInductTrace' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7011,7 +6971,6 @@ info: 'Lean4Lean.VInductDecl.StagedNormalizationCandidateSemanticInput.construct sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7047,7 +7006,6 @@ info: 'Lean4Lean.VInductDecl.NormalizationBlockRun.wf' depends on axioms: [prope sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7083,7 +7041,6 @@ info: 'Lean4Lean.VInductDecl.CandidateBlockFamilySemanticListRun.sameHeaders' de sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7119,7 +7076,6 @@ info: 'Lean4Lean.VInductDecl.CandidateBlockFamilySemanticListRun.evidence' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7155,7 +7111,6 @@ info: 'Lean4Lean.VInductDecl.CandidateBlockFamilySemanticInput.exists' depends o sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7191,7 +7146,6 @@ info: 'Lean4Lean.VInductDecl.CandidateBlockFamilySemanticListInput.exists' depen sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7227,7 +7181,6 @@ info: 'Lean4Lean.VInductDecl.NormalizationCandidateBlockSemanticInput.exists' de sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -7263,7 +7216,6 @@ info: 'Lean4Lean.VInductDecl.NormalizationCandidateBlockSemanticInput.exists_ofP sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, diff --git a/Lean4Lean/Verify/Environment/SingletonParityReplay.lean b/Lean4Lean/Verify/Environment/SingletonParityReplay.lean index 1448d428..104d20fd 100644 --- a/Lean4Lean/Verify/Environment/SingletonParityReplay.lean +++ b/Lean4Lean/Verify/Environment/SingletonParityReplay.lean @@ -2758,7 +2758,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.singletonNormalizationReplays' depends sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, @@ -2794,7 +2793,6 @@ info: 'Lean4Lean.InductiveReplayFixtures.singletonReplayMatrix' depends on axiom sorryAx, Classical.choice, ptrEqConstantInfo_eq, - ptrEqExpr_eq, Quot.sound, Expr.abstractRange_eq, Expr.abstract_eq, diff --git a/Lean4Lean/Verify/EquivManager.lean b/Lean4Lean/Verify/EquivManager.lean deleted file mode 100644 index f9ecc163..00000000 --- a/Lean4Lean/Verify/EquivManager.lean +++ /dev/null @@ -1,337 +0,0 @@ -import Batteries.Data.UnionFind.Lemmas -import Lean4Lean.Verify.Environment.Lemmas -import Lean4Lean.EquivManager -import Lean4Lean.Verify.TypeChecker.Basic - -namespace Lean4Lean.EquivManager -open Lean hiding Environment Exception -open Batteries Kernel - -inductive RelevantEq : Expr → Expr → Prop - | bvar : RelevantEq (.bvar i) (.bvar i) - | fvar : RelevantEq (.fvar i) (.fvar i) - | mvar : RelevantEq (.mvar i) (.mvar i) - | sort : RelevantEq (.sort u) (.sort u) - | const : RelevantEq (.const n ls) (.const n ls) - | app : RelevantEq f₁ f₂ → RelevantEq a₁ a₂ → RelevantEq (.app f₁ a₁) (.app f₂ a₂) - | lam : RelevantEq d₁ d₂ → RelevantEq b₁ b₂ → RelevantEq (.lam _ d₁ b₁ _) (.lam _ d₂ b₂ _) - | forallE : RelevantEq d₁ d₂ → RelevantEq b₁ b₂ → - RelevantEq (.forallE _ d₁ b₁ _) (.forallE _ d₂ b₂ _) - | letE : RelevantEq t₁ t₂ → RelevantEq v₁ v₂ → RelevantEq b₁ b₂ → - RelevantEq (.letE _ t₁ v₁ b₁ _) (.letE _ t₂ v₂ b₂ _) - | lit : RelevantEq (.lit l) (.lit l) - | mdata : RelevantEq e₁ e₂ → RelevantEq (.mdata _ e₁) (.mdata _ e₂) - | proj : RelevantEq e₁ e₂ → RelevantEq (.proj _ i e₁) (.proj _ i e₂) - -theorem RelevantEq.rfl : RelevantEq e e := by - induction e with - | bvar => exact .bvar - | fvar => exact .fvar - | mvar => exact .mvar - | sort => exact .sort - | const => exact .const - | lit => exact .lit - | app _ _ ih1 ih2 => exact .app ih1 ih2 - | lam _ _ _ _ ih1 ih2 => exact .lam ih1 ih2 - | forallE _ _ _ _ ih1 ih2 => exact .forallE ih1 ih2 - | letE _ _ _ _ _ ih1 ih2 ih3 => exact .letE ih1 ih2 ih3 - | mdata _ _ ih => exact .mdata ih - | proj _ _ _ ih => exact .proj ih - -theorem RelevantEq.symm (H1 : RelevantEq e₁ e₂) : RelevantEq e₂ e₁ := by - induction H1 with - | bvar | fvar | mvar | sort | const | lit => exact .rfl - | app _ _ ih1 ih2 => exact .app ih1 ih2 - | lam _ _ ih1 ih2 => exact .lam ih1 ih2 - | forallE _ _ ih1 ih2 => exact .forallE ih1 ih2 - | letE _ _ _ ih1 ih2 ih3 => exact .letE ih1 ih2 ih3 - | mdata _ ih => exact .mdata ih - | proj _ ih => exact .proj ih - -theorem RelevantEq.of_eqv : e₁ == e₂ → RelevantEq e₁ e₂ := by - simp [(· == ·)]; induction e₁ generalizing e₂ - all_goals - cases e₂ <;> try change false = _ → _; rintro ⟨⟩ - simp [Expr.eqv']; intros; subst_vars; try simp [rfl, *] - all_goals grind [RelevantEq] - -theorem RelevantEq.trans (H1 : RelevantEq e₁ e₂) (H2 : RelevantEq e₂ e₃) : RelevantEq e₁ e₃ := by - induction H1 generalizing e₃ with - | bvar | fvar | mvar | sort | const | lit => exact H2 - | app h1 h2 ih1 ih2 => let .app r1 r2 := H2; exact .app (ih1 r1) (ih2 r2) - | lam h1 h2 ih1 ih2 => let .lam r1 r2 := H2; exact .lam (ih1 r1) (ih2 r2) - | forallE h1 h2 ih1 ih2 => let .forallE r1 r2 := H2; exact .forallE (ih1 r1) (ih2 r2) - | letE h1 h2 h3 ih1 ih2 ih3 => let .letE r1 r2 r3 := H2; exact .letE (ih1 r1) (ih2 r2) (ih3 r3) - | mdata h1 ih => let .mdata r1 := H2; exact .mdata (ih r1) - | proj h1 ih => let .proj r1 := H2; exact .proj (ih r1) - -variable {env : VEnv} {Us : List Name} {Δ : VLCtx} - -theorem IsDefEqE.relevant (H : RelevantEq e₁ e₂) : IsDefEqE env us Δ e₁ e₂ := by - induction H with - | bvar | fvar | mvar | sort | const | lit => exact .rfl - | app _ _ ih1 ih2 => exact .app ih1 ih2 - | lam _ _ ih1 ih2 => exact .lam ih1 ih2 - | forallE _ _ ih1 ih2 => exact .forallE ih1 ih2 - | letE _ _ _ ih1 ih2 ih3 => exact .letE ih1 ih2 ih3 - | mdata _ ih => exact .mdata ih - | proj _ ih => exact .proj ih - -variable! (henv : VEnv.WF env) (hΔ : VLCtx.IsDefEq env Us.length Δ₁ Δ₂) in -theorem RelevantEq.uniq (eq : RelevantEq e₁ e₂) - (H1 : TrExprS env Us Δ₁ e₁ e₁') (H2 : TrExprS env Us Δ₂ e₂ e₂') : - env.IsDefEqU Us.length Δ₁.toCtx e₁' e₂' := by - induction H1 generalizing e₂ Δ₂ e₂' with - | bvar l1 => cases eq; let .bvar r1 := H2; exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩ - | fvar l1 => cases eq; let .fvar r1 := H2; exact ⟨_, (hΔ.find?_uniq henv l1 r1).2⟩ - | sort l1 => - cases eq; let .sort r1 := H2; cases l1.symm.trans r1 - exact ⟨_, VEnv.HasType.sort (.of_ofLevel l1)⟩ - | const l1 l2 l3 => - cases eq; let .const r1 r2 r3 := H2; cases l1.symm.trans r1; cases l2.symm.trans r2 - exact (TrExprS.const l1 l2 l3).wf henv hΔ.wf - | app l1 l2 _ _ ih3 ih4 => - let .app eq1 eq2 := eq; let .app _ _ r3 r4 := H2 - exact ⟨_, .appDF - (ih3 hΔ eq1 r3 |>.of_l henv hΔ.wf.toCtx l1) - (ih4 hΔ eq2 r4 |>.of_l henv hΔ.wf.toCtx l2)⟩ - | lam l1 _ _ ih2 ih3 => - let .lam eq1 eq2 := eq; let ⟨_, l1⟩ := l1; let .lam _ r2 r3 := H2 - have hA := ih2 hΔ eq1 r2 |>.of_l henv hΔ.wf.toCtx l1 - have ⟨_, hb⟩ := ih3 (hΔ.cons nofun <| .vlam hA) eq2 r3 - exact ⟨_, .lamDF hA hb⟩ - | forallE l1 l2 _ _ ih3 ih4 => - let .forallE eq1 eq2 := eq; let ⟨_, l1'⟩ := l1; let ⟨_, l2⟩ := l2; let .forallE _ _ r3 r4 := H2 - have hA := ih3 hΔ eq1 r3 |>.of_l henv hΔ.wf.toCtx l1' - have hB := ih4 (hΔ.cons nofun <| .vlam hA) eq2 r4 |>.of_l (Γ := _::_) henv ⟨hΔ.wf.toCtx, l1⟩ l2 - exact ⟨_, .forallEDF hA hB⟩ - | letE l1 _ _ _ ih2 ih3 ih4 => - let .letE eq1 eq2 eq3 := eq; have hΓ := hΔ.wf.toCtx; let .letE _ r2 r3 r4 := H2 - have ⟨_, hb⟩ := l1.isType henv hΓ - refine ih4 (hΔ.cons nofun ?_) eq3 r4 - exact .vlet (ih3 hΔ eq2 r3 |>.of_l henv hΓ l1) (ih2 hΔ eq1 r2 |>.of_l henv hΓ hb) - | lit _ _ ih1 => cases eq; let .lit _ r2 := H2; exact ih1 hΔ .rfl r2 - | mdata _ ih1 => let .mdata eq := eq; let .mdata r1 := H2; exact ih1 hΔ eq r1 - | proj _ l2 ih1 => - let .proj eq := eq; let .proj r1 r2 := H2 - exact l2.uniq henv hΔ.defeqCtx r2 (ih1 hΔ eq r1) - -theorem IsDefEqE.trExpr - (henv : env.WF) (noBV : Δ.NoBV) (H1 : IsDefEqE env Us Δ r₁ r₂) (hΔ : Δ'.WF env Us.length) - (W : Δ.BVLift Δ' dn 0 n 0) (hr : RelevantEq r₁ e₁) (he : TrExprS env Us Δ' e₁ e') : - ∃ e₂, RelevantEq r₂ e₂ ∧ TrExpr env Us Δ' e₂ e' := by - induction H1 generalizing e₁ Δ' e' dn n with - | rfl => exact ⟨_, hr, he.trExpr henv hΔ⟩ - | trans _ _ ih1 ih2 => - let ⟨em, a1, _, a2, a3⟩ := ih1 hΔ W hr he - have ⟨_, b1, b2⟩ := ih2 hΔ W a1 a2 - exact ⟨_, b1, b2.defeq henv hΔ a3⟩ - | defeq h1 h2 => - have h1' := h1.weakBV henv W; have h2' := h2.weakBV henv W - rw [Expr.liftLooseBVars_eq_self (noBV ▸ h1.closed.looseBVarRange_le)] at h1' - rw [Expr.liftLooseBVars_eq_self (noBV ▸ h2.closed.looseBVarRange_le)] at h2' - exact ⟨_, .rfl, h2'.defeq henv hΔ (hr.uniq henv (.refl henv hΔ) h1' he)⟩ - | app _ _ ih1 ih2 => - let .app hr1 hr2 := hr; let .app a1 a2 a3 a4 := he - let ⟨_, b1, b2⟩ := ih1 hΔ W hr1 a3 - let ⟨_, c1, c2⟩ := ih2 hΔ W hr2 a4 - exact ⟨_, .app b1 c1, .app henv hΔ.toCtx a1 a2 b2 c2⟩ - | lam _ _ ih1 ih2 => - let .lam hr1 hr2 := hr; let .lam a1 a2 a3 := he - let ⟨_, b1, b2⟩ := ih1 hΔ W hr1 a2 - let ⟨_, c1, c2⟩ := ih2 (by exact ⟨hΔ, nofun, a1⟩) (.skip _ W) hr2 a3 - exact ⟨_, .lam b1 c1, .lam (name := default) (bi := default) henv hΔ a1 b2 c2⟩ - | forallE _ _ ih1 ih2 => - let .forallE hr1 hr2 := hr; let .forallE a1 a2 a3 a4 := he - let ⟨_, b1, b2⟩ := ih1 hΔ W hr1 a3 - let ⟨_, c1, c2⟩ := ih2 (by exact ⟨hΔ, nofun, a1⟩) (.skip _ W) hr2 a4 - exact ⟨_, .forallE b1 c1, .forallE (name := default) (bi := default) henv hΔ a1 a2 b2 c2⟩ - | letE _ _ _ ih1 ih2 ih3 => - let .letE hr1 hr2 hr3 := hr; let .letE a1 a2 a3 a4 := he - let ⟨_, b1, b2⟩ := ih1 hΔ W hr1 a2 - let ⟨_, c1, c2⟩ := ih2 hΔ W hr2 a3 - let ⟨_, d1, d2⟩ := ih3 (by exact ⟨hΔ, nofun, a1⟩) (.skip _ W) hr3 a4 - exact ⟨_, .letE b1 c1 d1, .letE (name := default) (nd := default) henv hΔ a1 b2 c2 d2⟩ - | mdata _ ih => - let .mdata hr := hr; let .mdata a1 := he; let ⟨_, b1, b2⟩ := ih hΔ W hr a1 - exact ⟨_, .mdata b1, .mdata (d := default) b2⟩ - | proj _ ih => - let .proj hr := hr; let .proj a1 a2 := he - have ⟨_, b1, b2⟩ := ih hΔ W hr a1 - exact ⟨_, .proj b1, .proj henv hΔ b2 a2⟩ - -theorem IsDefEqE.uniq (henv : env.WF) (noBV : Δ.NoBV) (hΔ : Δ.WF env Us.length) - (he₁ : TrExprS env Us Δ e₁ e₁') (he₂ : TrExprS env Us Δ e₂ e₂') - (eq : IsDefEqE env Us Δ e₁ e₂) : env.IsDefEqU Us.length Δ.toCtx e₁' e₂' := by - have ⟨_, a1, _, a2, a3⟩ := eq.trExpr henv noBV hΔ .refl .rfl he₁ - exact .symm <| a1.uniq henv (.refl henv hΔ) he₂ a2 |>.trans henv hΔ a3 - -protected structure LE (m₁ m₂ : EquivManager) where - uf : m₁.uf.Equiv i₁ i₂ → m₂.uf.Equiv i₁ i₂ - toNodeMap {e : Expr} : m₁.toNodeMap[e]? = some i → m₂.toNodeMap[e]? = some i - -instance : LE EquivManager := ⟨EquivManager.LE⟩ - -theorem LE.rfl {m : EquivManager} : m ≤ m := ⟨id, id⟩ - -theorem LE.trans {m₁ m₂ m₃ : EquivManager} (h1 : m₁ ≤ m₂) (h2 : m₂ ≤ m₃) : m₁ ≤ m₃ := - ⟨h2.1 ∘ h1.1, h2.2 ∘ h1.2⟩ - -variable (env Us Δ) in -def M.WF (m : EquivManager) (x : StateM EquivManager α) (P : α → EquivManager → Prop) := - m.WF env Us Δ → ∀ ⦃a m'⦄, x.run m = (a, m') → m'.WF env Us Δ ∧ m ≤ m' ∧ P a m' - -theorem M.WF.stateWF {P : α → EquivManager → Prop} - (H : m.WF env Us Δ → M.WF env Us Δ m x P) : - M.WF env Us Δ m x P := fun h => H h h - -protected theorem M.WF.pure {a : α} {P : α → EquivManager → Prop} (H : P a m) : - M.WF env Us Δ m (pure a) P := by - rintro wf _ _ ⟨⟩; exact ⟨wf, .rfl, H⟩ - -protected theorem M.WF.bind {x : StateM EquivManager β} {f : β → StateM EquivManager γ} - (h1 : M.WF env Us Δ m x P) (h2 : ∀ a m', m ≤ m' → P a m' → M.WF env Us Δ m' (f a) Q) : - M.WF env Us Δ m (x >>= f) Q := by - intro wf a m₁; simp [bind, StateT.run, StateT.bind]; split; intro eq - have ⟨wf, a1, a2⟩ := (h1 wf ‹_› :) - have ⟨wf, b1, b2⟩ := h2 _ _ a1 a2 wf eq - exact ⟨wf, a1.trans b1, b2⟩ - -protected theorem M.WF.mono {x : StateM EquivManager β} - (h1 : M.WF env Us Δ m x P) (h2 : ∀ a m', m ≤ m' → P a m' → Q a m') : - M.WF env Us Δ m x Q := by - simpa using h1.bind fun _ _ a1 a2 => .pure (h2 _ _ a1 a2) - -protected theorem M.WF.bind_le {x : StateM EquivManager β} {f : β → StateM EquivManager γ} - (h1 : M.WF env Us Δ m x P) (le : m₀ ≤ m) - (h2 : ∀ a m', m₀ ≤ m' → P a m' → M.WF env Us Δ m' (f a) Q) : - M.WF env Us Δ m (x >>= f) Q := h1.bind fun _ _ a1 => h2 _ _ (le.trans a1) - -protected theorem M.WF.andM {x y : StateM EquivManager Bool} - (h1 : M.WF env Us Δ m x fun b _ => b → P) - (h2 : ∀ {m}, M.WF env Us Δ m y fun b _ => b → Q) : - M.WF env Us Δ m (x <&&> y) fun b _ => b → P ∧ Q := by - refine h1.bind fun b _ _ h1 => ?_; cases b <;> [exact .pure nofun; skip] - refine h2.mono fun _ _ _ h2 h => ⟨h1 rfl, h2 h⟩ - -theorem find.WF : M.WF env Us Δ m (EquivManager.find i) fun j m => m.uf.Equiv i j := by - intro wf a m'; simp [StateT.run, find]; split <;> rintro ⟨⟩ - · refine ⟨⟨?_, ?_⟩, ⟨by simp [UnionFind.equiv_find], id⟩, ?_⟩ - · simp; exact wf.wf - · simp [UnionFind.equiv_find]; exact wf.defeq - · simp [UnionFind.equiv_find]; exact .rfl - · exact ⟨wf, .rfl, .rfl⟩ - -theorem merge.WF (wf : m.WF env Us Δ) - (he : IsDefEqE env Us Δ e₁ e₂) - (hi : m.toNodeMap[e₁]? = some i) (hj : m.toNodeMap[e₂]? = some j) : - (merge m i j).WF env Us Δ ∧ m ≤ merge m i j := by - simp [merge]; iterate 2 split <;> [skip; exact ⟨wf, .rfl⟩] - refine ⟨⟨?_, ?_⟩, ⟨by simp [UnionFind.equiv_union]; exact .inl, by simp⟩⟩ - · simp; exact wf.wf - · simp [UnionFind.equiv_union] - rintro _ _ _ _ h1 h2 (h3 | ⟨h3, h4⟩ | ⟨h3, h4⟩) - · exact wf.defeq h1 h2 h3 - · refine (wf.defeq h1 hi h3).trans he |>.trans (wf.defeq hj h2 h4) - · exact (wf.defeq h1 hj h3).trans he.symm |>.trans (wf.defeq hi h2 h4) - -theorem toNode.WF : - M.WF env Us Δ m (EquivManager.toNode e) fun n m => m.toNodeMap[e]? = some n := by - intro wf a m'; simp [StateT.run, toNode]; split <;> rintro ⟨⟩ <;> [exact ⟨wf, .rfl, ‹_›⟩; skip] - refine ⟨{ wf {i} := ?_, defeq h1 h2 h3 := ?_ }, ⟨by simp, ?_⟩, by simp⟩ - · simp [Std.HashMap.getElem?_insert] - refine ⟨fun h => ?_, fun ⟨_, h⟩ => ?_⟩ - · obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h - · have ⟨e', h⟩ := wf.wf.1 h - exists e'; rwa [if_neg]; intro eq - rename_i hn _ _; exact hn _ (Std.HashMap.getElem?_congr eq ▸ h) - · exact ⟨e, by simp⟩ - · split at h - · cases h; apply Nat.lt_succ_self - · exact Nat.lt_succ_of_lt (wf.wf.2 ⟨_, h⟩) - · simp [Std.HashMap.getElem?_insert] at h1 h2 h3 - split at h1 <;> split at h2 <;> rename_i a1 a2 - · exact .relevant <| .of_eqv <| BEq.trans (BEq.symm a1) a2 - · cases h1; cases Nat.ne_of_gt (wf.wf.2 ⟨_, h2⟩) (h3.eq_of_ge_size (Nat.le_refl _)) - · cases h2; cases Nat.ne_of_gt (wf.wf.2 ⟨_, h1⟩) (h3.symm.eq_of_ge_size (Nat.le_refl _)) - · exact wf.defeq h1 h2 h3 - · simp [Std.HashMap.getElem?_insert] - intro _ _ h; rwa [if_neg]; rename_i h' _ _ - exact fun eq => h' _ (Std.HashMap.getElem?_congr eq ▸ h) - -theorem isEquiv.WF : - M.WF env Us Δ m (isEquiv useHash e₁ e₂) fun b _ => b → IsDefEqE env Us Δ e₁ e₂ := by - unfold isEquiv; split <;> [exact .pure fun _ => ptrEqExpr_eq ‹_› ▸ .rfl; skip] - split <;> [exact .pure nofun; split] - · rename_i h; refine .pure ?_ - simp only [Bool.and_eq_true, Expr.isBVar] at h - split at h <;> cases h.1; split at h <;> cases h.2 - simp [Expr.bvarIdx!]; rintro ⟨⟩; exact .rfl - refine toNode.WF.bind fun i₁ _ _ a1 => find.WF.bind fun j₁ _ le₁ a2 => ?_ - refine toNode.WF.bind fun i₂ _ le₂ b1 => find.WF.bind fun j₂ m₀ le₃ b2 => ?_ - refine .stateWF fun wf => ?_ - replace a1 := le₁.trans le₂ |>.trans le₃ |>.toNodeMap a1 - replace a2 := le₂.trans le₃ |>.uf a2 - replace b1 := le₃.toNodeMap b1 - extract_lets F4 - split - · rename_i h; simp at h; cases h; refine .pure fun _ => wf.defeq a1 b1 (a2.trans b2.symm) - have {m b} (le₄ : m₀ ≤ m) (H : b = true → IsDefEqE env Us Δ e₁ e₂) : - M.WF env Us Δ m (F4 b) fun b _ => b → IsDefEqE env Us Δ e₁ e₂ := by - dsimp only [F4]; split <;> [skip; exact .pure H] - intro wf a _; simp; rintro ⟨⟩ - replace a1 := le₄.toNodeMap a1; replace a2 := le₄.uf a2 - replace b1 := le₄.toNodeMap b1; replace b2 := le₄.uf b2 - have ⟨r₁, hr₁⟩ := wf.wf.1 <| a2.lt_size.1 <| wf.wf.2 ⟨_, a1⟩ - have ⟨r₂, hr₂⟩ := wf.wf.1 <| b2.lt_size.1 <| wf.wf.2 ⟨_, b1⟩ - suffices IsDefEqE env Us Δ r₁ r₂ from have ⟨wf, h⟩ := merge.WF wf this hr₁ hr₂; ⟨wf, h, H⟩ - exact (wf.defeq a1 hr₁ a2).symm.trans <| .trans (H ‹_›) (wf.defeq b1 hr₂ b2) - simp; split - · apply this .rfl; simp; rintro rfl rfl; exact .rfl - · apply this .rfl; simp; rintro rfl; exact .rfl - · apply this .rfl; simp; rintro rfl; exact .rfl - · apply this .rfl; simp; rintro rfl; exact .rfl - · apply this .rfl; simp; rintro rfl; exact .rfl - · exact .bind (.andM isEquiv.WF isEquiv.WF) fun _ _ le H => - this le fun hb => .app (H hb).1 (H hb).2 - · exact .bind (.andM isEquiv.WF isEquiv.WF) fun _ _ le H => - this le fun hb => .lam (H hb).1 (H hb).2 - · exact .bind isEquiv.WF fun _ _ le H => this le fun hb => .mdata (H hb) - · exact .bind (.andM isEquiv.WF isEquiv.WF) fun _ _ le H => - this le fun hb => .forallE (H hb).1 (H hb).2 - · exact .bind (.andM (.pure id) isEquiv.WF) fun _ _ le H => - this le fun hb => (by simpa using (H hb).1) ▸ .proj (H hb).2 - · exact .bind (.andM isEquiv.WF <| .andM isEquiv.WF isEquiv.WF) fun _ _ le H => - this le fun hb => .letE (H hb).1 (H hb).2.1 (H hb).2.2 - · exact .pure nofun - -end EquivManager - -namespace TypeChecker.Inner - -open EquivManager in -theorem addEquiv.WF {c : VContext} {s : VState} (he₁ : c.TrExprS e₁ e') (he₂ : c.TrExpr e₂ e') : - RecM.WF c s (modify fun st => { st with eqvManager := st.eqvManager.addEquiv e₁ e₂ }) - fun _ _ => True := by - rintro _ mwf wf _ _ ⟨⟩ - let ⟨_, _, a1, a2, ewf, a4⟩ := wf.ectx - refine ⟨{ s with toState := _ }, rfl, .rfl, { wf with ectx := ⟨_, _, a1, a2, ?_, a4⟩ }, trivial⟩ - simp [addEquiv]; split; rename_i h1; split; rename_i h2 - have ⟨ewf, b2, b3⟩ := toNode.WF ewf h1 - have ⟨ewf, c2, c3⟩ := toNode.WF ewf h2 - refine (merge.WF ewf ?_ (c2.toNodeMap b3) c3).1 - exact .defeq (he₁.weakFV' c.Ewf a2 a1) (he₂.weakFV' c.Ewf a2 a1) - -theorem isDefEq.WF {c : VContext} {s : VState} - (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') : - RecM.WF c s (isDefEq e₁ e₂) fun b _ => b → c.IsDefEqU e₁' e₂' := by - unfold isDefEq - split - · rename_i heq - exact .pure fun _ => - (he₁.eqv heq).uniq c.Ewf (.refl c.Ewf c.Δwf) he₂ - simp only [] - refine (isDefEqCore.WF he₁ he₂).bind fun b _ _ hb => ?_ - simp; split - · exact (addEquiv.WF he₁ ⟨_, he₂, (hb ‹_›).symm⟩).map fun _ _ _ _ => hb - · exact .pure hb diff --git a/Lean4Lean/Verify/TypeChecker/Basic.lean b/Lean4Lean/Verify/TypeChecker/Basic.lean index 877b073f..3eed5c5b 100644 --- a/Lean4Lean/Verify/TypeChecker/Basic.lean +++ b/Lean4Lean/Verify/TypeChecker/Basic.lean @@ -42,64 +42,66 @@ open Lean hiding Environment Exception open Kernel open scoped _root_.List -namespace EquivManager +namespace DefEqCache variable {env : VEnv} {Us : List Name} {Δ : VLCtx} -variable (env Us Δ) in -inductive IsDefEqE : Expr → Expr → Prop - | rfl : IsDefEqE e e - | trans : IsDefEqE e₁ e₂ → IsDefEqE e₂ e₃ → IsDefEqE e₁ e₃ - | defeq : TrExprS env Us Δ e₁ e' → TrExpr env Us Δ e₂ e' → IsDefEqE e₁ e₂ - | app : IsDefEqE f₁ f₂ → IsDefEqE a₁ a₂ → IsDefEqE (.app f₁ a₁) (.app f₂ a₂) - | lam : IsDefEqE d₁ d₂ → IsDefEqE b₁ b₂ → IsDefEqE (.lam _ d₁ b₁ _) (.lam _ d₂ b₂ _) - | forallE : IsDefEqE d₁ d₂ → IsDefEqE b₁ b₂ → IsDefEqE (.forallE _ d₁ b₁ _) (.forallE _ d₂ b₂ _) - | letE : IsDefEqE t₁ t₂ → IsDefEqE v₁ v₂ → IsDefEqE b₁ b₂ → - IsDefEqE (.letE _ t₁ v₁ b₁ _) (.letE _ t₂ v₂ b₂ _) - | mdata : IsDefEqE e₁ e₂ → IsDefEqE (.mdata _ e₁) (.mdata _ e₂) - | proj : IsDefEqE e₁ e₂ → IsDefEqE (.proj _ i e₁) (.proj _ i e₂) - -theorem IsDefEqE.symm (H1 : IsDefEqE env Us Δ e₁ e₂) : IsDefEqE env Us Δ e₂ e₁ := by - induction H1 with - | rfl => exact .rfl - | trans _ _ ih1 ih2 => exact .trans ih2 ih1 - | defeq h1 h2 => let ⟨_, h2, h3⟩ := h2; exact .defeq h2 ⟨_, h1, h3.symm⟩ - | app _ _ ih1 ih2 => exact .app ih1 ih2 - | lam _ _ ih1 ih2 => exact .lam ih1 ih2 - | forallE _ _ ih1 ih2 => exact .forallE ih1 ih2 - | letE _ _ _ ih1 ih2 ih3 => exact .letE ih1 ih2 ih3 - | mdata _ ih => exact .mdata ih - | proj _ ih => exact .proj ih + +/-- The relation the positive `isDefEq` cache records: both kernel expressions translate to +definitionally equal `VExpr`s. + +Unlike the union-find manager it replaces, this relation is deliberately *not* closed under +transitivity or congruence. `isDefEq` is a sound but incomplete semi-decision procedure and so is +not transitive, and closing over its successes would make the checker's answers depend on the order +in which pairs were presented (lean4#14806). -/ +def IsDefEqE (env : VEnv) (Us : List Name) (Δ : VLCtx) (e₁ e₂ : Expr) : Prop := + ∃ e', TrExprS env Us Δ e₁ e' ∧ TrExpr env Us Δ e₂ e' + +theorem IsDefEqE.symm (H : IsDefEqE env Us Δ e₁ e₂) : IsDefEqE env Us Δ e₂ e₁ := + let ⟨_, h1, _, h2, h3⟩ := H; ⟨_, h2, _, h1, h3.symm⟩ + +/-- The cache is keyed by a `BEq` hash set, so a lookup may present expressions that are only +`Expr.eqv`-equal to the ones recorded. -/ +theorem IsDefEqE.eqv (H : IsDefEqE env Us Δ e₁ e₂) (h₁ : e₁ == e₁') (h₂ : e₂ == e₂') : + IsDefEqE env Us Δ e₁' e₂' := + let ⟨_, h1, _, h2, h3⟩ := H; ⟨_, h1.eqv h₁, _, h2.eqv h₂, h3⟩ variable! (henv : env.WF) (W : VLCtx.FVLift' Δ Δ' 0 n 0) (hΔ : VLCtx.WF env Us.length Δ') in -theorem IsDefEqE.weak' (H1 : IsDefEqE env Us Δ e₁ e₂) : IsDefEqE env Us Δ' e₁ e₂ := by - induction H1 with - | rfl => exact .rfl - | trans _ _ ih1 ih2 => exact .trans ih1 ih2 - | defeq h1 h2 => exact .defeq (h1.weakFV' henv W hΔ) (h2.weakFV' henv W hΔ) - | app _ _ ih1 ih2 => exact .app ih1 ih2 - | lam _ _ ih1 ih2 => exact .lam ih1 ih2 - | forallE _ _ ih1 ih2 => exact .forallE ih1 ih2 - | letE _ _ _ ih1 ih2 ih3 => exact .letE ih1 ih2 ih3 - | mdata _ ih => exact .mdata ih - | proj _ ih => exact .proj ih +theorem IsDefEqE.weak' (H : IsDefEqE env Us Δ e₁ e₂) : IsDefEqE env Us Δ' e₁ e₂ := + let ⟨_, h1, h2⟩ := H; ⟨_, h1.weakFV' henv W hΔ, h2.weakFV' henv W hΔ⟩ -variable (env Us Δ) in -structure WF (m : EquivManager) where - wf {i} : i < m.uf.size ↔ ∃ e : Expr, m.toNodeMap[e]? = some i - defeq {e₁ e₂ : Expr} {i₁ i₂} : - m.toNodeMap[e₁]? = some i₁ → m.toNodeMap[e₂]? = some i₂ → m.uf.Equiv i₁ i₂ → - IsDefEqE env Us Δ e₁ e₂ +theorem IsDefEqE.uniq (henv : env.WF) (hΔ : Δ.WF env Us.length) + (he₁ : TrExprS env Us Δ e₁ e₁') (he₂ : TrExprS env Us Δ e₂ e₂') + (eq : IsDefEqE env Us Δ e₁ e₂) : env.IsDefEqU Us.length Δ.toCtx e₁' e₂' := + let ⟨_, h1, _, h2, h3⟩ := eq + (he₁.uniq henv (.refl henv hΔ) h1).trans henv hΔ <| + h3.symm.trans henv hΔ (h2.uniq henv (.refl henv hΔ) he₂) -theorem WF.empty : WF env Us Δ {} where - wf := by simp - defeq := by simp +variable (env Us Δ) in +/-- Well-formedness of the positive `isDefEq` cache: every pair it answers `true` for really is a +pair of definitionally equal expressions. -/ +def WF (m : Std.HashSet (Expr × Expr)) : Prop := + ∀ ⦃p : Expr × Expr⦄, p ∈ m → IsDefEqE env Us Δ p.1 p.2 + +theorem WF.empty : WF env Us Δ {} := by simp [WF] + +theorem WF.insert (wf : WF env Us Δ m) (H : IsDefEqE env Us Δ e₁ e₂) : + WF env Us Δ (m.insert (e₁, e₂)) := by + intro p hp + rcases Std.HashSet.mem_insert.1 hp with h | h + · obtain ⟨q₁, q₂⟩ := p + have h' : ((e₁ == q₁) && (e₂ == q₂)) = true := h + rw [Bool.and_eq_true] at h' + exact H.eqv h'.1 h'.2 + · exact wf h + +theorem WF.contains (wf : WF env Us Δ m) (h : m.contains (e₁, e₂)) : + IsDefEqE env Us Δ e₁ e₂ := wf (Std.HashSet.contains_iff_mem.1 h) variable! (henv : env.WF) (W : VLCtx.FVLift' Δ Δ' 0 n 0) (hΔ : VLCtx.WF env Us.length Δ') in -theorem WF.weak' (wf : WF env Us Δ m) : WF env Us Δ' m where - wf := wf.wf - defeq h1 h2 h3 := wf.defeq h1 h2 h3 |>.weak' henv W hΔ +theorem WF.weak' (wf : WF env Us Δ m) : WF env Us Δ' m := + fun _ h => (wf h).weak' henv W hΔ -end EquivManager +end DefEqCache /-- Exact alignment between one host structure record and the registered Theory artifact used to interpret primitive projections. The positional @@ -410,7 +412,7 @@ class VState.WF (c : VContext) (s : VState) where trctx : c.TrLCtx ngen_wf : ∀ fv ∈ c.vlctx.fvars, s.ngen.Reserves fv ectx : ∃ Δ' n, Δ'.WF c.venv c.lparams.length ∧ c.vlctx.FVLift' Δ' 0 n 0 ∧ - s.eqvManager.WF c.venv c.lparams Δ' ∧ ∀ fv ∈ Δ'.fvars, s.ngen.Reserves fv + DefEqCache.WF c.venv c.lparams Δ' s.success ∧ ∀ fv ∈ Δ'.fvars, s.ngen.Reserves fv inferTypeI_wf : s.inferTypeI.WF c s inferTypeC_wf : s.inferTypeC.WF c s whnfCore_wf : WHNFCache.WF c s s.whnfCoreCache @@ -1027,6 +1029,29 @@ theorem isDefEqCore.WF {c : VContext} {s : VState} RecM.WF c s (isDefEqCore e₁ e₂) fun b _ => b → c.IsDefEqU e₁' e₂' := fun _ wf => wf.isDefEqCore he₁ he₂ +theorem cacheSuccess.WF {c : VContext} {s : VState} (he₁ : c.TrExprS e₁ e') (he₂ : c.TrExpr e₂ e') : + RecM.WF c s (cacheSuccess e₁ e₂) fun _ _ => True := by + rintro _ mwf wf _ _ ⟨⟩ + let ⟨_, _, a1, a2, ewf, a4⟩ := wf.ectx + refine ⟨{ s with toState := _ }, rfl, .rfl, { wf with ectx := ⟨_, _, a1, a2, ?_, a4⟩ }, trivial⟩ + -- The insertion is keyed on the two hashes, so either order can be the one recorded. + have H : DefEqCache.IsDefEqE c.venv c.lparams _ e₁ e₂ := + ⟨_, he₁.weakFV' c.Ewf a2 a1, he₂.weakFV' c.Ewf a2 a1⟩ + simp only []; split <;> [exact ewf.insert H; exact ewf.insert H.symm] + +theorem isDefEq.WF {c : VContext} {s : VState} + (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') : + RecM.WF c s (isDefEq e₁ e₂) fun b _ => b → c.IsDefEqU e₁' e₂' := by + unfold isDefEq + split + · rename_i heq + exact .pure fun _ => (he₁.eqv heq).uniq c.Ewf (.refl c.Ewf c.Δwf) he₂ + simp only [] + refine (isDefEqCore.WF he₁ he₂).bind fun b _ _ hb => ?_ + simp; split + · exact (cacheSuccess.WF he₁ ⟨_, he₂, (hb ‹_›).symm⟩).map fun _ _ _ _ => hb + · exact .pure hb + theorem inferType.WF' {c : VContext} {s : VState} (h1 : e.FVarsIn (· ∈ c.vlctx.fvars)) (hinf : inferOnly = true → ∃ e', c.TrExprS e e') : RecM.WF c s (inferType e inferOnly) fun ty _ => ∃ e' ty', c.TrTyping e ty e' ty' := diff --git a/Lean4Lean/Verify/TypeChecker/InferType.lean b/Lean4Lean/Verify/TypeChecker/InferType.lean index 1dd8e012..031ba02f 100644 --- a/Lean4Lean/Verify/TypeChecker/InferType.lean +++ b/Lean4Lean/Verify/TypeChecker/InferType.lean @@ -1,5 +1,4 @@ import Lean4Lean.Verify.TypeChecker.Reduce -import Lean4Lean.Verify.EquivManager open Lean4Lean @@ -992,7 +991,9 @@ theorem inferType'.WF · exact { wf with inferTypeC_wf := hic wf.inferTypeC_wf } · exact { wf with inferTypeI_wf := hic wf.inferTypeI_wf } split - · extract_lets G1; split <;> [split; skip] + · extract_lets G1 + refine (checkLitSize.WF (Q := fun _ s' => s' = _) rfl).bind fun _ _ _ h => ?_ + subst h; split <;> [split; skip] · refine .getEnv <| (M.WF.liftExcept envGet.WF).lift.bind fun _ _ _ h => ?_ have ⟨_, h, _⟩ := c.trenv.find? h <| (c.safePrimitives h (literal_is_primitive (.inl rfl))).1 ▸ DefinitionSafety.le_safe diff --git a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean index 359ae2b7..faff37e2 100644 --- a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean +++ b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean @@ -1,6 +1,5 @@ import Lean4Lean.Verify.TypeChecker.Reduce import Lean4Lean.Verify.TypeChecker.InferType -import Lean4Lean.Verify.EquivManager open Lean4Lean @@ -149,23 +148,25 @@ theorem isDefEqForall.WF {c : VContext} {s : VState} theorem quickIsDefEq.WF {c : VContext} {s : VState} (he₁ : c.TrExprS e₁ e₁') (he₂ : c.TrExprS e₂ e₂') : - RecM.WF c s (quickIsDefEq e₁ e₂ useHash) fun b _ => b = .true → c.IsDefEqU e₁' e₂' := by + RecM.WF c s (quickIsDefEq e₁ e₂) fun b _ => b = .true → c.IsDefEqU e₁' e₂' := by unfold quickIsDefEq - refine .bind (Q := fun b _ => b = true → c.IsDefEqU e₁' e₂') ?_ fun _ _ _ h => ?_ - · intro _ mwf wf _ s₁ eq - simp [modifyGet, MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, StateT.modifyGet, - pure, Except.pure] at eq - split at eq; rename_i b _ b' m hm - change let s' := _; (_, s') = _ at eq; extract_lets s' at eq - injection eq; subst b' s₁ - let ⟨_, _, a1, a2, ewf, a4⟩ := wf.ectx - have ⟨ewf, _, h1⟩ := EquivManager.isEquiv.WF ewf hm - refine let vs' := { s with toState := s' }; ⟨vs', rfl, .rfl, { wf with ectx := ?_ }, ?_⟩ - · exact ⟨_, _, a1, a2, ewf, a4⟩ - · intro h; apply (VEnv.IsDefEqU.weak'_iff c.Ewf a1 a2.toCtx).1 - exact (h1 h).uniq c.Ewf (a2.bvars_eq.trans c.mlctx.noBV) - a1 (he₁.weakFV' c.Ewf a2 a1) (he₂.weakFV' c.Ewf a2 a1) - split <;> [exact .pure fun _ => h ‹_›; split] + refine .stateWF fun wf => .get ?_ + split <;> [rename_i hcache; skip] + · refine .pure fun _ => ?_ + rcases Bool.or_eq_true_iff.1 hcache with h | h + · exact (he₁.eqv h).uniq c.Ewf (.refl c.Ewf c.Δwf) he₂ + -- The cache is keyed on the two hashes, so the recorded pair may be either way round. + let ⟨_, _, a1, a2, ewf, _⟩ := wf.ectx + refine (VEnv.IsDefEqU.weak'_iff c.Ewf a1 a2.toCtx).1 <| + DefEqCache.IsDefEqE.uniq c.Ewf a1 + (he₁.weakFV' c.Ewf a2 a1) (he₂.weakFV' c.Ewf a2 a1) ?_ + unfold succeededBefore at h + split at h; · exact ewf.contains h + split at h; · exact (ewf.contains h).symm + rcases Bool.or_eq_true_iff.1 h with h | h + · exact ewf.contains h + · exact (ewf.contains h).symm + split · exact .toLBoolM <| c.withMLC_self ▸ isDefEqLambda.WF (subst := #[]) (fvs := []) rfl (c.withMLC_self ▸ he₁) (c.withMLC_self ▸ he₂) · exact .toLBoolM <| c.withMLC_self ▸ diff --git a/Lean4Lean/Verify/TypeChecker/Reduce.lean b/Lean4Lean/Verify/TypeChecker/Reduce.lean index f8a14781..6041886c 100644 --- a/Lean4Lean/Verify/TypeChecker/Reduce.lean +++ b/Lean4Lean/Verify/TypeChecker/Reduce.lean @@ -18,30 +18,64 @@ theorem rawNatLitExt?.WF {c : VContext} (H : rawNatLitExt? e = some n) (he : c.T have hn := this.lit_has_type exact ⟨hn, this.unique (by trivial) (TrExprS.natLit c.hasPrimitives hn n).1⟩ -def reduceBinNatOpG (guard : Nat → Nat → Prop) [DecidableRel guard] - (f : Nat → Nat → Nat) (a b : Expr) : RecM (Option Expr) := do - let some v1 := rawNatLitExt? (← whnf a) | return none - let some v2 := rawNatLitExt? (← whnf b) | return none - if guard v1 v2 then return none - return some <| .lit <| .natVal <| f v1 v2 +/-- `checkNatSize` either throws or leaves the state alone, so it is transparent to any +postcondition that already holds. -/ +theorem checkNatSize.WF {c : VContext} {s : VState} {Q : Unit → VState → Prop} (H : Q () s) : + RecM.WF c s (checkNatSize n) Q := by + unfold checkNatSize; exact .readThe (by split <;> [exact .throw; exact .pure H]) -theorem reduceBinNatOpG.WF {guard} [DecidableRel guard] {c : VContext} +@[inherit_doc checkNatSize.WF] +theorem checkCountArg.WF {c : VContext} {s : VState} {Q : Unit → VState → Prop} (H : Q () s) : + RecM.WF c s (checkCountArg n op) Q := by + unfold checkCountArg; split <;> [exact .throw; exact .pure H] + +@[inherit_doc checkNatSize.WF] +theorem checkLitSize.WF {c : VContext} {s : VState} {Q : Unit → VState → Prop} (H : Q () s) : + RecM.WF c s (checkLitSize l) Q := by + unfold checkLitSize; split <;> [exact checkNatSize.WF H; exact .pure H] + +@[inherit_doc checkNatSize.WF] +theorem checkNatSizeIf.WF {c : VContext} {s : VState} {Q : Unit → VState → Prop} (H : Q () s) : + RecM.WF c s (checkNatSizeIf checkSize n) Q := by + unfold checkNatSizeIf; split <;> [exact checkNatSize.WF H; exact .pure H] + +@[inherit_doc checkNatSize.WF] +theorem checkPowSize.WF {c : VContext} {s : VState} {Q : Unit → VState → Prop} (H : Q () s) : + RecM.WF c s (checkPowSize base exp) Q := by + unfold checkPowSize + exact (checkCountArg.WF H).bind fun _ _ _ H => + .readThe (by split <;> [exact .throw; exact .pure H]) + +@[inherit_doc checkNatSize.WF] +theorem checkShiftLeftSize.WF {c : VContext} {s : VState} {Q : Unit → VState → Prop} (H : Q () s) : + RecM.WF c s (checkShiftLeftSize v shift) Q := by + unfold checkShiftLeftSize + split <;> [exact (checkCountArg.WF H).bind fun _ _ _ H => checkNatSize.WF H; exact .pure H] + +/-- The shared skeleton of the binary `Nat` reductions: reduce both operands to literals, run a +size `check` that can only throw, and return the literal `f v1 v2`. -/ +theorem reduceBinNatOpCore.WF {c : VContext} {check : Nat → Nat → RecM Unit} + (hcheck : ∀ {v1 v2 s'} {Q : Unit → VState → Prop}, Q () s' → RecM.WF c s' (check v1 v2) Q) (he : c.TrExprS (.app (.app (.const fc ls) a) b) e') (hprim : Environment.primitives.contains fc) (heval : c.venv.ReflectsNatNatNat fc f) : - RecM.WF c s (reduceBinNatOpG guard f a b) fun oe _ => ∀ e₁, oe = some e₁ → - c.FVarsBelow (.app (.app (.const fc ls) a) b) e₁ ∧ c.TrExpr e₁ e' := by + RecM.WF c s (do + let some v1 := rawNatLitExt? (← whnf a) | return none + let some v2 := rawNatLitExt? (← whnf b) | return none + check v1 v2 + return some <| .lit <| .natVal <| f v1 v2) + fun oe _ => ∀ e₁, oe = some e₁ → + c.FVarsBelow (.app (.app (.const fc ls) a) b) e₁ ∧ c.TrExpr e₁ e' := by let .app hb1 hb2 hf hb := he let .app ha1 ha2 hf ha := hf let .const h1 h2 h3 := hf - unfold reduceBinNatOpG refine (whnf.WF ha).bind fun a₁ _ _ ⟨a1, _, a2, a3⟩ => ?_ split <;> [rename_i v1 h; exact .pure nofun] obtain ⟨hn, rfl⟩ := rawNatLitExt?.WF h a2 refine (whnf.WF hb).bind fun b₁ _ _ ⟨b1, _, b2, b3⟩ => ?_ split <;> [rename_i v2 h; exact .pure nofun] cases (rawNatLitExt?.WF h b2).2 - split <;> [exact .pure nofun; rename_i h] + refine (hcheck (Q := fun _ _ => True) trivial).bind fun _ _ _ _ => ?_ refine .pure ?_; rintro _ ⟨⟩; refine ⟨fun _ _ _ => trivial, ?_⟩ have ⟨ci, c1, _⟩ := c.trenv.find?_iff.2 ⟨_, h1⟩ have ⟨_, c3⟩ := c.safePrimitives c1 hprim @@ -56,6 +90,33 @@ theorem reduceBinNatOpG.WF {guard} [DecidableRel guard] {c : VContext} have := ha1.appDF a3 |>.toU.of_r c.Ewf c.Δwf hb1 exact ⟨_, .appDF this b3⟩ +theorem reduceBinNatOp.WF {c : VContext} + (he : c.TrExprS (.app (.app (.const fc ls) a) b) e') + (hprim : Environment.primitives.contains fc) + (heval : c.venv.ReflectsNatNatNat fc f) : + RecM.WF c s (reduceBinNatOp f a b checkSize) fun oe _ => ∀ e₁, oe = some e₁ → + c.FVarsBelow (.app (.app (.const fc ls) a) b) e₁ ∧ c.TrExpr e₁ e' := by + unfold reduceBinNatOp + exact reduceBinNatOpCore.WF (fun H => checkNatSizeIf.WF H) he hprim heval + +theorem reducePow.WF {c : VContext} + (he : c.TrExprS (.app (.app (.const fc ls) a) b) e') + (hprim : Environment.primitives.contains fc) + (heval : c.venv.ReflectsNatNatNat fc Nat.pow) : + RecM.WF c s (reducePow a b) fun oe _ => ∀ e₁, oe = some e₁ → + c.FVarsBelow (.app (.app (.const fc ls) a) b) e₁ ∧ c.TrExpr e₁ e' := by + unfold reducePow + exact reduceBinNatOpCore.WF (fun H => checkPowSize.WF H) he hprim heval + +theorem reduceShiftLeft.WF {c : VContext} + (he : c.TrExprS (.app (.app (.const fc ls) a) b) e') + (hprim : Environment.primitives.contains fc) + (heval : c.venv.ReflectsNatNatNat fc (· <<< ·)) : + RecM.WF c s (reduceShiftLeft a b) fun oe _ => ∀ e₁, oe = some e₁ → + c.FVarsBelow (.app (.app (.const fc ls) a) b) e₁ ∧ c.TrExpr e₁ e' := by + unfold reduceShiftLeft + exact reduceBinNatOpCore.WF (fun H => checkShiftLeftSize.WF H) he hprim heval + theorem reduceBinNatPred.WF {c : VContext} (he : c.TrExprS (.app (.app (.const fc ls) a) b) e') (hprim : Environment.primitives.contains fc) @@ -97,32 +158,44 @@ theorem reduceNat.WF {c : VContext} (he : c.TrExprS e e') : cases h1 : nargs == 1 <;> simp only [Bool.false_eq_true, ↓reduceIte] · cases nargs == 2 <;> [exact hP ▸ .pure nofun; simp only [↓reduceIte]] split <;> [rename_i f ls a b; exact hP ▸ .pure nofun] - have hfun guard {g fc G} [DecidableRel guard] (hprim : fc ∈ prims) + have hfun checkSize {g fc G} (hprim : fc ∈ prims) (heval : c.venv.ReflectsNatNatNat fc g) (hG : RecM.WF c s G P) : - RecM.WF c s (do if f == fc then {return ← reduceBinNatOpG guard g a b}; G) P := by + RecM.WF c s (do if f == fc then {return ← reduceBinNatOp g a b checkSize}; G) P := by + split <;> [rename_i h; exact hG] + simp at h ⊢; subst h + exact hP ▸ reduceBinNatOp.WF he (hprims.2 hprim) heval + have hpow {fc G} (hprim : fc ∈ prims) + (heval : c.venv.ReflectsNatNatNat fc Nat.pow) (hG : RecM.WF c s G P) : + RecM.WF c s (do if f == fc then {return ← reducePow a b}; G) P := by + split <;> [rename_i h; exact hG] + simp at h ⊢; subst h + exact hP ▸ reducePow.WF he (hprims.2 hprim) heval + have hshl {fc G} (hprim : fc ∈ prims) + (heval : c.venv.ReflectsNatNatNat fc (· <<< ·)) (hG : RecM.WF c s G P) : + RecM.WF c s (do if f == fc then {return ← reduceShiftLeft a b}; G) P := by split <;> [rename_i h; exact hG] simp at h ⊢; subst h - exact hP ▸ reduceBinNatOpG.WF he (hprims.2 hprim) heval + exact hP ▸ reduceShiftLeft.WF he (hprims.2 hprim) heval have hpred {g fc G} (hprim : fc ∈ prims) (heval : c.venv.ReflectsNatNatBool fc g) (hG : RecM.WF c s G P) : RecM.WF c s (do if f == fc then {return ← reduceBinNatPred g a b}; G) P := by split <;> [rename_i h; exact hG] simp at h ⊢; subst h exact hP ▸ reduceBinNatPred.WF he (hprims.2 hprim) heval - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natAdd - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natSub - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natMul - apply hfun _ (by simp [prims]) c.hasPrimitives.natPow - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natGcd - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natMod - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natDiv + apply hfun true (by simp [prims]) c.hasPrimitives.natAdd + apply hfun true (by simp [prims]) c.hasPrimitives.natSub + apply hfun true (by simp [prims]) c.hasPrimitives.natMul + apply hpow (by simp [prims]) c.hasPrimitives.natPow + apply hfun false (by simp [prims]) c.hasPrimitives.natGcd + apply hfun false (by simp [prims]) c.hasPrimitives.natMod + apply hfun false (by simp [prims]) c.hasPrimitives.natDiv apply hpred (by simp [prims]) c.hasPrimitives.natBEq apply hpred (by simp [prims]) c.hasPrimitives.natBLE - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natLAnd - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natLOr - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natXor - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natShiftLeft - apply hfun (fun _ _ => False) (by simp [prims]) c.hasPrimitives.natShiftRight + apply hfun false (by simp [prims]) c.hasPrimitives.natLAnd + apply hfun false (by simp [prims]) c.hasPrimitives.natLOr + apply hfun false (by simp [prims]) c.hasPrimitives.natXor + apply hshl (by simp [prims]) c.hasPrimitives.natShiftLeft + apply hfun false (by simp [prims]) c.hasPrimitives.natShiftRight exact hP ▸ .pure nofun · split <;> [rename_i h2; exact hP ▸ .pure nofun] simp [nargs, Expr.getAppNumArgs_eq] at h1; subst fn @@ -132,7 +205,8 @@ theorem reduceNat.WF {c : VContext} (he : c.TrExprS e e') : refine (whnf.WF ha).bind fun a₁ _ _ ⟨a1, _, a2, a3⟩ => ?_ split <;> [rename_i n h; exact hP ▸ .pure nofun] obtain ⟨hn, rfl⟩ := rawNatLitExt?.WF h a2 - refine hP ▸ .pure ?_; rintro _ ⟨⟩; refine ⟨fun _ _ _ => trivial, ?_⟩ + refine hP ▸ (checkNatSize.WF (Q := fun _ _ => True) trivial).map fun _ _ _ _ => ?_ + rintro _ ⟨⟩; refine ⟨fun _ _ _ => trivial, ?_⟩ have ⟨ci, c1, _⟩ := c.trenv.find?_iff.2 ⟨_, h1⟩ have ⟨c2, c3⟩ := c.safePrimitives c1 <| hprims.2 (by simp [prims]) have ⟨d1, d2, d3⟩ := c.trenv.find?_uniq c1 h1; cases h2 diff --git a/README.md b/README.md index 412d98c8..732d7c1d 100644 --- a/README.md +++ b/README.md @@ -118,8 +118,8 @@ If you run this as is (with no additional arguments), it will check every olean * `Basic.lean`: translating environments * `Lemmas.lean`: properties of `TrEnv` * `TypeChecker` - * `Basic.lean`: typechecker invariants - * `EquivManager.lean`: invariants for the union-find defeq cache + * `Basic.lean`: typechecker invariants, including the defeq cache + * `Reduce.lean`: correctness of the `Nat` literal reductions * `InferType.lean`: correctness of `inferType` * `WHNF.lean`: correctness of `whnf` * `IsDefEq.lean`: correctness of `isDefEq` diff --git a/divergences.md b/divergences.md index 31f00674..3dc76131 100644 --- a/divergences.md +++ b/divergences.md @@ -6,13 +6,13 @@ This is a list of places where lean4lean deliberately has different behavior fro * [`Lean4Lean.Environment.checkPrimitiveDef`](Lean4Lean/Primitive.lean), `checkPrimitiveInductive`: Lean does not check that primitives are declared with the correct types and definitional behavior, except in the case of `Eq` which is used in the declaration of `Quot`. This is required for soundness, but Lean is able to get away with it because Lean ships its prelude and using an alternative prelude is not supported. * [`Lean4Lean.TypeChecker.Inner.inferType'`](Lean4Lean/TypeChecker.lean), literal case: The original code was not checking that the literal type actually exists. Again, this is okay provided that the prelude is trusted. * [`Lean4Lean.TypeChecker.Inner.tryStringLitExpansionCore`](Lean4Lean/TypeChecker.lean): there is a counterproductive `whnf` call in this function which is removed in Lean4lean. -* [`Lean.Level.normalize`](https://github.com/leanprover/lean4/blob/v4.33.0/src/Lean/Level.lean), `isEquiv`, `geq`: Lean's standard-library level operations currently differ from the C++ kernel implementation; [leanprover/lean4#14356](https://github.com/leanprover/lean4/pull/14356) tracks aligning them. Lean4lean routes typechecker sort and constant-level-list equality through the primed comparisons in [`Lean4Lean/Level.lean`](Lean4Lean/Level.lean) (`isEquiv'`, `isEquivList`), which are verified sound and complete for the `NormLevel` semantics and use the standard-library operations — themselves verified in [`Lean4Lean/Verify/LevelStd.lean`](Lean4Lean/Verify/LevelStd.lean) — as a sound fast path. +* [`Lean.Level.normalize`](https://github.com/leanprover/lean4/blob/v4.33.1/src/Lean/Level.lean), `isEquiv`, `geq`: Lean's standard-library level operations currently differ from the C++ kernel implementation; [leanprover/lean4#14356](https://github.com/leanprover/lean4/pull/14356) tracks aligning them. Lean4lean routes typechecker sort and constant-level-list equality through the primed comparisons in [`Lean4Lean/Level.lean`](Lean4Lean/Level.lean) (`isEquiv'`, `isEquivList`), which are verified sound and complete for the `NormLevel` semantics and use the standard-library operations — themselves verified in [`Lean4Lean/Verify/LevelStd.lean`](Lean4Lean/Verify/LevelStd.lean) — as a sound fast path. * [`Lean4Lean.checkConstantVal`](Lean4Lean/Environment.lean): The original implementation would call `check` which sets the level params and then unsets them afterward, and then `ensure_sort` would run in a context without any level params. In lean4lean the monad is parameterized over level params, so they remain the same across the two calls. * [`Lean4Lean.toCtorWhenStruct`](Lean4Lean/Inductive/Reduce.lean), `inferProj`: both kernels now recognize `Prop` using normalized universe levels ([leanprover/lean4#14613](https://github.com/leanprover/lean4/pull/14613)). Lean4lean remains more conservative for uncertain levels, using `isNeverZero` where Lean uses `!isAlwaysZero`. Lean's choice would be unsound if its level algorithm did not reject the true equation `imax 1 u ≤ u`: `inductive T.{u} : Sort u where mk : Bool → T` would otherwise permit an analogue of the construction in #14613. -* [`Lean4Lean.EquivManager.isEquiv`](Lean4Lean/EquivManager.lean), [`Lean4Lean.TypeChecker.Inner.isDefEqCore'`](Lean4Lean/TypeChecker.lean), `reduceProj`: when comparing two projections, and when reducing one, lean4lean uses only the projection index, while the C++ kernel also compares the structure name ([leanprover/lean4#14631](https://github.com/leanprover/lean4/pull/14631), [#14632](https://github.com/leanprover/lean4/pull/14632)). The name has already been checked by the time either happens: [`inferProj`](Lean4Lean/TypeChecker.lean) rejects `.proj S i e` unless the type of `e` whnfs to an application of `S` itself. Comparison and reduction only ever see projections that have been through type inference, so re-comparing the name there is redundant. -* [`Lean4Lean.Environment.addInductive`](Lean4Lean/Inductive/Add.lean): [leanprover/lean4#14621](https://github.com/leanprover/lean4/pull/14621) rechecks the declarations produced by nested-inductive elimination — the restored constructor types, the restored recursor types and the recursor rules' right-hand sides. Lean4lean does not. Upstream describes these as redundant sanity checks that "may prevent soundness bugs if the nested-inductive code is still missing any required validations"; they establish no precondition that a later step consumes. Lean4lean aims to prove the elimination correct rather than to recheck its output, and a speculative check would only add proof obligations without contributing an invariant. The check of the nested applications `I Ds` from [#14577](https://github.com/leanprover/lean4/pull/14577) is kept, because those arguments are dropped from the auxiliary declarations and so are not covered by checking the block. +* [`Lean4Lean.TypeChecker.Inner.isDefEqCore'`](Lean4Lean/TypeChecker.lean), `reduceProj`: when comparing two projections, and when reducing one, lean4lean uses only the projection index, while the C++ kernel also compares the structure name ([leanprover/lean4#14631](https://github.com/leanprover/lean4/pull/14631), [#14632](https://github.com/leanprover/lean4/pull/14632)). The name has already been checked by the time either happens: [`inferProj`](Lean4Lean/TypeChecker.lean) rejects `.proj S i e` unless the type of `e` whnfs to an application of `S` itself. Comparison and reduction only ever see projections that have been through type inference, so re-comparing the name there is redundant. +* [`Lean4Lean.Environment.addInductive`](Lean4Lean/Inductive/Add.lean): [leanprover/lean4#14621](https://github.com/leanprover/lean4/pull/14621) rechecks the declarations produced by nested-inductive elimination — the restored constructor types, the restored recursor types and the recursor rules' right-hand sides. Lean4lean does not. Upstream describes these as redundant sanity checks that "may prevent soundness bugs if the nested-inductive code is still missing any required validations"; they establish no precondition that a later step consumes. Lean4lean aims to prove the elimination correct rather than to recheck its output, and a speculative check would only add proof obligations without contributing an invariant. The check of the nested applications `I Ds` from [#14577](https://github.com/leanprover/lean4/pull/14577) is kept, because those arguments are dropped from the auxiliary declarations and so are not covered by checking the block. The recursor check from [#14808](https://github.com/leanprover/lean4/pull/14808) is also kept, for a different reason than #14621's: it guards the ordinary recursor generation path, which the `is_def_eq` cache bug of [#14806](https://github.com/leanprover/lean4/pull/14806) could corrupt, so it decides what the kernel accepts rather than re-deriving a property of a translation lean4lean intends to prove correct. * [`Lean4Lean.checkNoNestedAux`](Lean4Lean/Inductive/Add.lean): [leanprover/lean4#14616](https://github.com/leanprover/lean4/pull/14616) rejects the reserved `_nested` prefix in both the inductive types and the constructor types of a declaration; lean4lean checks only the constructor types. The bug that check fixes is specific to constructors: nested occurrences are rewritten to the auxiliary types in constructor types only (`replaceAllNested`), and rewritten back the same way (`restoreNested`), so an inductive's own type is carried through both directions verbatim and cannot acquire a type it was not checked at. A `_nested` name written in an inductive type also cannot resolve in the first place: the auxiliary types are declared in the same block, so they are not in the environment while that block's types are checked (unlike constructor types, which are checked once the block's types, auxiliaries included, are present), and they never survive into the final environment. Lean's check additionally reserves the whole `_nested` namespace against unrelated user declarations, which lean4lean does not. -* [`Lean4Lean.ElimNestedInductive.Result.restoreNested`](Lean4Lean/Inductive/Add.lean), `restoreCtorName`: [leanprover/lean4#14632](https://github.com/leanprover/lean4/pull/14632) turned the `lean_assert`s in the nested-inductive restoration into kernel exceptions; lean4lean keeps `unreachable!` and `assert!`. The branches are unreachable: `restoreCtorName` runs only for the recursors of the auxiliary types the elimination generates, whose constructors are exactly the keys of `aux2nested`, and the nested occurrences stored there are applications of a constant by construction. Upstream's stated motivation is that the assertions vanish in a release build and the C++ consumers then read out of bounds; the corresponding accesses here are total, so there is nothing to read out of bounds. Note that if one of these invariants were broken anyway, `unreachable!` would continue with a default value rather than reject; the restored constructor and recursor types are re-checked in the final environment ([#14621](https://github.com/leanprover/lean4/pull/14621)), which lean4lean retains, but a restored rule constructor *name* is not covered by that pass. -* [`Lean4Lean.FuelConfig`](Lean4Lean/FuelConfig.lean): since [leanprover/lean4#13956](https://github.com/leanprover/lean4/pull/13956), the native kernel bounds mutually recursive checking through the `maxRecDepth` option. Lean4lean exposes several independent fuel counters instead, because its Lean definitions also need explicit termination witnesses. Replay comparison therefore uses each implementation's default bound unless an explicit lean4lean fuel configuration is supplied. +* [`Lean4Lean.ElimNestedInductive.Result.restoreNested`](Lean4Lean/Inductive/Add.lean), `restoreCtorName`: [leanprover/lean4#14632](https://github.com/leanprover/lean4/pull/14632) turned the `lean_assert`s in the nested-inductive restoration into kernel exceptions; lean4lean keeps `unreachable!` and `assert!`. The branches are unreachable: `restoreCtorName` runs only for the recursors of the auxiliary types the elimination generates, whose constructors are exactly the keys of `aux2nested`, and the nested occurrences stored there are applications of a constant by construction. Upstream's stated motivation is that the assertions vanish in a release build and the C++ consumers then read out of bounds; the corresponding accesses here are total, so there is nothing to read out of bounds. Note that if one of these invariants were broken anyway, `unreachable!` would continue with a default value rather than reject. Upstream re-checks the restored constructor and recursor types in the final environment ([#14621](https://github.com/leanprover/lean4/pull/14621)), which would catch a corrupted type — though not a corrupted rule constructor *name*, which that pass does not cover. Lean4lean does not run #14621 (see the `addInductive` entry above), so it rests on the invariants themselves rather than on a downstream recheck. +* [`Lean4Lean.FuelConfig`](Lean4Lean/FuelConfig.lean): since [leanprover/lean4#13956](https://github.com/leanprover/lean4/pull/13956), the native kernel bounds mutually recursive checking through the `maxRecDepth` option. Lean4lean exposes several independent fuel counters instead, because its Lean definitions also need explicit termination witnesses. Replay comparison therefore uses each implementation's default bound unless an explicit lean4lean fuel configuration is supplied. The `natMaxSize` field is the same structure's home for the `Nat` numeral bound of [leanprover/lean4#14849](https://github.com/leanprover/lean4/pull/14849); the default matches the native kernel's 128 MB, but it is set per run rather than through the `LEAN_NAT_MAX_SIZE` environment variable, since reading the environment inside the kernel monad would make checking depend on ambient state. * [`Lean4Lean.addDefinition`](Lean4Lean/Environment.lean) (`unsafe` branch), [`addMutual`](Lean4Lean/Environment.lean): an `unsafe`/`partial` definition may be recursive, so its body is checked in an environment that already contains the declaration. The C++ kernel adds `constant_info(d)` there -- the full definition, value included -- so the body can delta-unfold the very constant being defined. Lean4lean adds it as an axiom of the same type instead: the body may still *refer* to the block's constants, but cannot unfold them. So for example `unsafe def foo : Nat := (fun (_ : foo = 1) => 1) rfl` is accepted by the C++ kernel, but rejected by L4L: checking the argument requires `foo =?= 1`, which succeeds by unfolding `foo` to its own body and reducing. Read literally, that rule makes a typing fact about the constant available while establishing it, and implementing this in `IsDefEq` directly degenerates completely, allowing even things like `unsafe def bar : Nat := "hi"` by using the typing judgment to justify itself. The gap is confined to `unsafe`/`partial` code, which carries no logical content. -* [`Lean4Lean.addMutual`](Lean4Lean/Environment.lean): lean4lean requires the declarations of a mutual block to carry the same universe parameters and to have distinct names. Both checks are in kernel PRs that are not yet released ([leanprover/lean4#14608](https://github.com/leanprover/lean4/pull/14608), [#14632](https://github.com/leanprover/lean4/pull/14632)); the released kernel checks only that the safety annotations agree. Lean4lean needs them rather than merely matching them: the block is checked under a single `M.run`, whose level parameters are fixed for the whole run, and the model adds the block's constants one at a time with `VEnv.addConsts`, which fails on a repeated name. +* [`Lean4Lean.addMutual`](Lean4Lean/Environment.lean): no longer a divergence — [leanprover/lean4#14608](https://github.com/leanprover/lean4/pull/14608) and [#14632](https://github.com/leanprover/lean4/pull/14632) released in v4.33.0-rc2, so both kernels now require the declarations of a mutual block to carry the same universe parameters and to have distinct names. Retained here because lean4lean needs the two checks rather than merely matching them: the block is checked under a single `M.run`, whose level parameters are fixed for the whole run, and the model adds the block's constants one at a time with `VEnv.addConsts`, which fails on a repeated name. Regression coverage is in [`Lean4Lean.Tests.KernelHardening`](Lean4Lean/Tests/KernelHardening.lean). diff --git a/flake.lock b/flake.lock index 6a270fc6..90e87903 100644 --- a/flake.lock +++ b/flake.lock @@ -24,11 +24,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1786543565, - "narHash": "sha256-zHMoHO85jizkIXH0OfnvabpNLTl90rR3GCc1h/e2sx4=", + "lastModified": 1787412565, + "narHash": "sha256-M1y7JYDUzvOSYv0DWcCCmkL2DqDfQZePsKDrQf/Or6U=", "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "4026c657eecf16beea7d266ce32933ef3d7db2e5", + "rev": "1ecad9d6f99cf3255a858861c9a2e6966cdd0290", "type": "github" }, "original": { diff --git a/lean-toolchain b/lean-toolchain index 025e5954..a8afa7d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.33.1 diff --git a/plans/roadmap.md b/plans/roadmap.md index b31bb46a..4320e369 100644 --- a/plans/roadmap.md +++ b/plans/roadmap.md @@ -77,7 +77,7 @@ required for the final release; they can be reached in separate milestones. |---|---| | Ladder position | **L4L-16 active** (semantic environment bridge and sort inversion). L4L-18B completed first on 2026-08-12: proof-carrying pattern contractions, an explicit registered-equation join contract, beta-collapsed generated-iota/`quotDefEq` coverage, and `VEnv.LE` transport now form the fork-owned interface (design note `plans/l4l-18b-extension-interface-design.md`, ledger D020). The former L4L-17 merged in on 2026-08-13 (joint route; second resolution in the sort-inversion decision note). Slices 16A and 16B′ are complete at checkpoints `quyyrlks`/`pxluxmvm`; the WHNF/determinism layer and mirror-spine refactor landed at `wolxmups`/`mvmrxuus`; 16D0 is complete in the active working tree (`SExprParamsD0.lean`, D0a + definition-extended D0b, `d0SortInvS`); 16C′ joint leaf closure remains active (§5), with publication held until it measures clean | | Current formalization source | the L4L-18B checkpoint (jj change `oluxtqyk`) descends from the L4L-15B checkpoint `7c1e89fc` (jj change `xuzusmnl`) and is published at `jcb/formalization2` after the complete gate passed | -| Parent lineage | the L4L-15B implementation descends from the v4.33 reconciliation merge `99a7f8ae7b89` (second parent: digama `upstream/master` `b292275c`); Lean on v4.33.0 final, lean4-nix on `argumentcomputer/lean4-nix` (upstream pins v4.33.0-rc2 — ledger D018) | +| Parent lineage | the L4L-15B implementation descends from the v4.33 reconciliation merge `99a7f8ae7b89` (second parent: digama `upstream/master` `b292275c`); Lean on v4.33.1, lean4-nix on `argumentcomputer/lean4-nix` (upstream pins v4.33.0-rc2 — ledger D018; v4.33.1 kernel changes mirrored per D021) | | Fixed `master` baseline | `1a16b72d2e35932a82aa501beb29ef2c3d072580` — local `master` bookmark (corrected 2026-08-12; the row previously carried a fork formalization hash that no `master` ref ever pointed at). The v4.33 reconciliation merged the later digama `upstream/master` `b292275c` as its second parent without moving `master`; `origin/master` has since moved (see remote drift) | | Remote drift (re-verified 2026-08-14 via GitHub API; local `upstream/master` was never fetched past `b292275c`, so any reconcile begins with a fetch) | digama master is now **four** commits past the merged `b292275c`, tip `4b60e53d` (2026-08-14): stage-2 replay perf (clean-apply), the normalize-backed level-algorithm enable (half-absorbed — the fork independently made the `isEquivList` change in `99a7f8ae`; residue is the `geq'` flip inside `checkConstructors`), a proj-reduction restructure that conflicts with the fork's sorry-free `reduceProj.WF` (upstream's own version rests on a new sorry), and a neutral K-target reorder — checker-side work landing in L4L-19A/B territory; per-commit analysis and a defer-recommendation (reconcile as L4L-19's first action) in the local untracked note `plans/l4l-16-boundary-digama-drift.md`; the reconcile-or-defer decision remains due at the L4L-16 boundary (§7). `origin/master` moved one commit to `715bfaff` ("verify: prove soundness of the standard library normalize") — already an ancestor of the fork's formalization line (the `eval_normalize`/`eval_normalize_total` proofs are in-tree), so content is absorbed and only the ref recording changed | | Trust frontier | exactly 16 sorried proof declarations (10 Tier V, 6 Tier R; `NormalEq.parRed` carries two tokens) plus six kernel-rejection recovery declarations — 22 compiled allowlist entries — and 34 custom-axiom declarations; all are pinned by exact audits. L4L-15B removed the two structure-eta checker roots from the direct frontier; their inherited L4L-16--19 dependencies remain explicit in exact axiom guards | diff --git a/upstream-divergence.md b/upstream-divergence.md index 0af2c810..991eec7d 100644 --- a/upstream-divergence.md +++ b/upstream-divergence.md @@ -223,7 +223,8 @@ Audit baseline after the complete L4L-12B literal-readiness checkpoint `upstream/master` `b292275c` ("perf: skip the NormLevel for levels with no essential imax"; upstream advanced past the planned `1a16b72d` before the merge executed, so the reconciliation took the actual head). Toolchain - v4.33.0 final (upstream pins v4.33.0-rc2 — see D018); lean4-nix input + v4.33.1 (upstream pins v4.33.0-rc2 — see D018; the v4.33.1 kernel changes + are mirrored per D021); lean4-nix input repointed to `argumentcomputer/lean4-nix` (`fromToolchainFile` API). Upstream absorbed since `ef849dfb`: verified standard-library level operations (`Verify/LevelStd.lean`) plus sound-and-complete primed @@ -1091,14 +1092,18 @@ to the replacement. structure artifact, and proves constructive quotient initialization, emptying the six entries. -## D018 — v4.33.0 final toolchain (upstream pins v4.33.0-rc2) +## D018 — v4.33.1 toolchain (upstream pins v4.33.0-rc2) - **Status:** intentional-fork (temporary) -- **Delta:** `lean-toolchain` pins `leanprover/lean4:v4.33.0` and batteries - `v4.33.0` because `argumentcomputer/lean4-nix` vendors released toolchains - only; upstream pins `v4.33.0-rc2`. -- **Removal condition:** upstream bumps to the final release (expected - imminently); no code delta is attached to this row. +- **Delta:** `lean-toolchain` pins `leanprover/lean4:v4.33.1` because + `argumentcomputer/lean4-nix` vendors released toolchains only; upstream pins + `v4.33.0-rc2`. Batteries stays pinned at its `v4.33.0` tag: the project cut + no patch release for v4.33.1, and its v4.33.0 sources build unchanged under + the v4.33.1 toolchain. +- **Note:** v4.33.1 is a kernel release. The six kernel changes it carries are + accounted for in this fork — see D021. +- **Removal condition:** upstream bumps to a released toolchain of v4.33.1 or + later; no code delta is attached to this row. ## D019 — registered structure eta in Theory @@ -1180,6 +1185,55 @@ to the replacement. represents beta-collapsed tower rules without a trusted shape or soundness oracle, and the fork migrates. +## D021 — v4.33.1 kernel changes mirrored ahead of upstream + +- **Status:** implemented intentional fork divergence (2026-08-22); upstream + lean4lean still targets v4.33.0-rc2 and carries none of these. +- **Delta:** v4.33.1 is a kernel release. Each of its six kernel changes is + accounted for here — five mirrored, one already satisfied: + - lean4#14582 — `Environment.addInductive` runs `checkUniformIndOccs` before + nested-inductive elimination, rejecting any occurrence of a datatype being + declared that is not applied to the declaration's parameters and universe + levels. Occurrences erased by a later `whnf`, and permuted universe levels, + are now rejected where they were previously accepted. + - lean4#14806 — the union-find `EquivManager` positive cache is replaced by a + hash-ordered pair set (`succeededBefore`/`cacheSuccess`), so results no + longer depend on the order pairs were checked in. `Lean4Lean/EquivManager.lean` + and `Lean4Lean/Verify/EquivManager.lean` are deleted; the cache invariant is + now `DefEqCache.WF` in `Verify/TypeChecker/Basic.lean`. + - lean4#14807 — no delta: `isProp` already routed through `ensureSortCore`, + so lean4lean never had the bug. Upstream has converged on this fork's + behavior. + - lean4#14808 — `AddInductive.checkRecursors` type-checks each generated + recursor and verifies that each computation rule is type-preserving. + - lean4#14843 — `toCtorWhenStruct` takes a sort-ensuring `isNeverProp` + callback instead of matching on `whnf (inferType eType)` with an + `unreachable!` fallback, so a non-sort type raises a kernel error. The + `isNeverZero`/`!isAlwaysZero` divergence recorded in `divergences.md` is + preserved. + - lean4#14849 — `natMaxSize` (a new `FuelConfig` field, default 128 MB, the + same bound `LEAN_NAT_MAX_SIZE` sets natively) bounds literals entering the + kernel and the numerals `reduceNat` computes. `reducePow` and the new + `reduceShiftLeft` bound their results before forming them. +- **Downstream impact:** `TypeChecker.State.eqvManager` is now + `TypeChecker.State.success : Std.HashSet (Expr × Expr)`; `quickIsDefEq` lost + its `useHash` parameter and no longer mutates state. `inductiveReduceRec` and + `toCtorWhenStruct` take an extra `isNeverProp` callback. `FuelConfig` gained + `natMaxSize` — write its default as a literal, not `128 * 1024 * 1024`, since + `simp` renormalizes the arithmetic and desynchronizes fixture contexts. +- **Tests:** `Lean4Lean/Tests/UniformIndOccs.lean` ports upstream's + `tests/elab/issue_14576_nonuniform.lean` (five rejection cases, three + acceptance cases) plus the mutual defeq-parameter case from + `tests/elab/inductiveDefeqParams.lean`. `Tests/NestedInductive.lean` gained + `badUniformDecl`, whose ill-typed dropped parameter sits beside a uniform + occurrence so the uniformity check cannot preempt the nested-parameter check. +- **Axiom note:** no new axiom or `sorry`; the frontier is unchanged at 22. + Dropping the union-find cache removes `ptrEqExpr_eq` from the axiom + dependencies of every `#print axioms` guard that reached it through + `quickIsDefEq`. +- **Removal condition:** upstream lean4lean adopts v4.33.1 and mirrors these + kernel changes; the fork then rebases onto its versions. + ## Review checklist At each publish or ix pin boundary: From c56f165f63d4928c3d945c874144444f740c9a02 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Sat, 22 Aug 2026 15:03:41 -0400 Subject: [PATCH 2/2] ci: add scheduled toolchain and dependency update workflow Runs `argumentcomputer/lean-update` daily against `dev`, opening an `update/lean-{release}` PR whether or not the build passes, so an incompatible release surfaces as a failing PR to review rather than silently not appearing. `pinned-tags` bump mode suits this package: batteries is pinned to a Lean version tag rather than tracking a branch, so its `rev` moves with the toolchain. Only the Lean half is automated -- `flake.nix` resolves the toolchain through lean4-nix's vendored release table, which lags a release, so bumping the `lean4-nix` input stays a manual follow-up on the update PR. Requires the TOKEN_APP_ID and TOKEN_APP_PRIVATE_KEY secrets already used by repo-sync.yml; pushes made with GITHUB_TOKEN would not trigger CI. --- .github/workflows/update.yml | 55 ++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 .github/workflows/update.yml diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml new file mode 100644 index 00000000..03b7f223 --- /dev/null +++ b/.github/workflows/update.yml @@ -0,0 +1,55 @@ +name: Update Lean toolchain and pinned deps + +on: + schedule: + # Daily at 00:00 UTC + - cron: "0 0 * * *" + workflow_dispatch: + +permissions: + contents: write + pull-requests: write + +jobs: + update: + runs-on: ubuntu-latest + steps: + # create-pull-request takes its base from the checked-out branch, and the + # action passes no `base` of its own, so this is what points the update PR + # at `dev`. `dev` is already the default branch; naming it keeps the PR + # off `master`, which only mirrors digama0/lean4lean (see repo-sync.yml) + # and would discard the commit on its next force-sync. + - uses: actions/checkout@v7 + with: + ref: dev + + # Mint a token from the GitHub App so the opened PR triggers CI; pushes + # made with GITHUB_TOKEN do not. Same App as repo-sync.yml. + - uses: actions/create-github-app-token@v3 + id: app-token + with: + client-id: ${{ secrets.TOKEN_APP_ID }} + private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }} + + # `dev` carries the fork's bump_mode/release_channel support; `main` only + # mirrors upstream, which silently ignores these inputs. `pinned-tags` + # suits this package: batteries is pinned to a Lean version tag rather + # than tracking a branch, so its `rev` moves with the toolchain; a + # dependency pinned to a commit hash is reported and left alone. A PR is + # opened on an update/lean-{release} branch whether or not the build + # passes, so an incompatible release shows up as a failing PR to review -- + # expected here, where a toolchain bump can break the kernel internals + # this package mirrors. + # + # Only the Lean half is automated. flake.nix resolves the toolchain from + # `lean-toolchain` through lean4-nix's vendored release table, so nix.yml + # fails at evaluation on a release that table has not recorded yet. Those + # hashes arrive through lean4-nix's own lean-update PR, which will not + # have merged by the time this job runs, so bumping the `lean4-nix` flake + # input here would only add unrelated churn. It stays a manual follow-up + # on the update PR once lean4-nix has landed the release. + - uses: argumentcomputer/lean-update@dev + with: + bump_mode: pinned-tags + on_update_fails: pr + token: ${{ steps.app-token.outputs.token }}