WIP feat: certify recursive normalization candidates

.github/scripts/check_sorry_frontier.pl

@@ -53,6 +53,8 @@
   "Lean4Lean/Verify/Typing/Lemmas.lean\0TrProj.instL"      => 1,
   # Tier V - checker verification, blocked on Tiers S/P
   "Lean4Lean/Verify/Level.lean\0NormLevel.subsumption_eval"     => 1,
+  "Lean4Lean/Verify/Level.lean\0isEquiv_wf"                    => 1,
+  "Lean4Lean/Verify/Environment.lean\0addDecl.WF"              => 1,
   "Lean4Lean/Verify/TypeChecker/InferType.lean\0inferProj.WF"   => 1,
   "Lean4Lean/Verify/TypeChecker/WHNF.lean\0reduceRecursor.WF"   => 1,
   "Lean4Lean/Verify/TypeChecker/WHNF.lean\0reduceProj.WF"       => 1,

.github/workflows/ci.yml

@@ -0,0 +1,58 @@
+name: CI
+
+on:
+  push:
+    branches: [master]
+  pull_request:
+  workflow_dispatch:
+
+# A newer push to the same branch supersedes an in-flight run; master runs are
+# never cancelled, since those are the ones that populate the build cache.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.ref != 'refs/heads/master' }}
+
+jobs:
+  build:
+    name: Build and self-check
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+    steps:
+      - uses: actions/checkout@v7
+
+      # Installs the toolchain pinned in `lean-toolchain` and runs `lake build`,
+      # i.e. the `defaultTargets`: the `Lean4Lean` library, the `lean4lean` exe,
+      # `Lean4Lean.Theory`, `Lean4Lean.Verify` and `Lean4Lean.Tests`. The proofs
+      # in `Verify` deliberately contain `sorry`s, so warnings must not fail the
+      # build. `Lean4Lean.Experimental` is WIP and is not a default target.
+      - name: Build
+        uses: leanprover/lean-action@v1
+        with:
+          use-mathlib-cache: false
+
+      # `Lean4Lean.Experimental` is WIP and deliberately not a default target, but it still has to
+      # compile. `sorry`s here are expected, as in `Verify`.
+      - name: Build Lean4Lean.Experimental
+        run: lake build Lean4Lean.Experimental
+
+      # `lake build` only establishes that lean4lean compiles; these check that it still
+      # *works*. The two modes exercise different code paths, so both are worth running.
+
+      # Module-at-a-time replay, against an environment built from the module's imports.
+      # This is the path that goes through `replayFromImports`, including the compacted
+      # region handling that regressed into a SIGSEGV, so keep it as a regression test.
+      #
+      # One small module on purpose: `main` spawns an unbounded `IO.asTask` per module and
+      # each replay imports the world, so peak RSS scales with the fan-out and a large
+      # prefix (e.g. `Lean4Lean`) is OOM-killed. Widen once replay uses a bounded task
+      # pool, as lean4checker does.
+      - name: Replay Init.Core through lean4lean
+        run: lake exe lean4lean Init.Core
+
+      # `--fresh` instead rechecks the module *and all its imports* into an empty
+      # environment -- ~43k declarations, the closest thing to an end-to-end kernel test.
+      # Single-threaded and `withImportModules`-bracketed, so it stays cheap on memory.
+      # Core only: modules importing `Lean` currently fail with "type checker does not
+      # support loose bound variables" (digama0/lean4lean#17).
+      - name: Recheck Init.System.IO and its imports from scratch
+        run: lake exe lean4lean --fresh Init.System.IO

.gitignore

@@ -1,4 +1,6 @@
 /.lake
 /result
 /.direnv
-/plans
+# Keep scratch plans local while versioning the authoritative execution ladder.
+/plans/*
+!/plans/roadmap.md

Lean4Lean/Declaration.lean

@@ -2,6 +2,21 @@ import Lean.Declaration
 
 
 namespace Lean
+
+/--
+The value of a constant for the purpose of delta reduction: definitions and theorems have one,
+opaques do not. This mirrors the C++ `constant_info::has_value()`/`get_value()` pair.
+
+This is deliberately *not* `ConstantInfo.value?`, whose meaning changed in lean4#12973: it now
+excludes theorems, but `constant_info::has_value()` was left untouched by that PR, so the kernel
+still delta-unfolds theorems: `type_checker::is_delta` uses this predicate to select candidates,
+and `instantiate_value_lparams` uses it before reading their values.
+-/
+def ConstantInfo.deltaValue? : ConstantInfo → Option Expr
+  | .defnInfo {value, ..} => some value
+  | .thmInfo {value, ..} => some value
+  | _ => none
+
 namespace ReducibilityHints
 
 def lt' : ReducibilityHints → ReducibilityHints → Bool -- lean4#2750

Lean4Lean/Environment.lean

@@ -53,9 +53,9 @@ def addTheorem (env : Environment) (v : TheoremVal) (check := true) (fuel : Fuel
   if check then
     -- TODO(Leo): we must add support for handling tasks here
     M.run env (safety := .safe) (lctx := {}) (lparams := v.levelParams) (fuel := fuel) do
+      checkConstantVal env v.toConstantVal
       if !(← isProp v.type) then
         throw <| .thmTypeIsNotProp env v.name v.type
-      checkConstantVal env v.toConstantVal
       let valType ← TypeChecker.checkType v.value
       if !(← isDefEq valType v.type) then
         throw <| .declTypeMismatch env (.thmDecl v) valType

Lean4Lean/Environment/Basic.lean

@@ -43,9 +43,10 @@ def primitives : NameSet := .ofList [
 /--
 Returns true iff `constName` is a non-recursive inductive datatype that has only one constructor and no indices.
 
-Such types have special kernel support. This must be in sync with `is_structure_like`.
+Such types have special kernel support (e.g. the eta rule).
+This must be in sync with `is_non_rec_structure()`.
 -/
-def isStructureLike (env : Environment) (constName : Name) : Bool :=
+def isNonRecStructure (env : Environment) (constName : Name) : Bool :=
   match env.find? constName with
   | some (.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true
   | _ => false

Lean4Lean/Experimental/NormalEq.lean

@@ -5,7 +5,7 @@ import Lean4Lean.Theory.Typing.Pattern
 
 namespace Lean4Lean
 
-open VExpr
+open Lean4Lean VExpr
 
 variable (IsDefEqU : List VExpr → VExpr → VExpr → Prop) (Γ₀ : List VExpr) in
 inductive IsDefEqCtx : List VExpr → List VExpr → Prop

Lean4Lean/Experimental/SExpr.lean

@@ -2,6 +2,7 @@ import Lean4Lean.Theory.Typing.Lemmas
 import Lean4Lean.Theory.Typing.Pattern
 
 namespace Lean4Lean
+open Lean4Lean
 
 inductive Classification where
   | ctor (arity : Nat)

Lean4Lean/Experimental/ShapeLogRel.lean

@@ -1,6 +1,7 @@
 import Lean4Lean.Experimental.SExpr
 
 namespace Lean4Lean
+open Lean4Lean
 
 namespace SExpr
 variable [Params]
@@ -2156,9 +2157,7 @@ theorem WShape.ctor'_join {l l' : List (WShape n)} {c : Name}
     exact ih (fun z hz => h2' z (.tail _ hz))
   · rw [dif_pos (key.mpr (.inr h2))]; simp [ctor, bot, Shape.bot_join]
     have h1' : ∀ x ∈ l, x.1 ≤ Shape.bot := by
-      have ⟨hIs, hNZ⟩ : IsStruct c = true ∧ ¬ListNonZero l := by
-        refine ⟨?_, fun hNZ => h1 fun _ => hNZ⟩
-        by_contra hIs; exact h1 fun h => (hIs h).elim
+      have ⟨_, hNZ⟩ := Decidable.not_imp_iff_and_not.1 h1
       simp [ListNonZero] at hNZ; exact hNZ
     congr 1; clear h1 h2 key
     induction h with | nil => rfl | @cons x y L L' hh _ ih
@@ -2531,7 +2530,7 @@ theorem Shape.HasType.unfold_iff {m a : Shape n} : HasType m a ↔ HasTypeU m a
     | indTy => rfl
     | forallE => simpa [HasType, hasType] using h
   | sort => cases n <;> rfl
-  | forallE H => simpa [HasType, hasType, hasType.core.iff] using H
+  | forallE H => simpa [HasType, hasType, hasType.core.iff, HasTypePi] using H
   | lam H => simp [HasType, hasType, hasType.core.iff]; exact H
   | ctor | indTy => rfl
 
@@ -3440,7 +3439,7 @@ theorem LE_Interp.Matches.head_wf (H : Matches p c rargs m) (wf : p.WF cl top k)
 theorem LE_Interp.Matches.head_wf_eq (H : Matches p c rargs m) (wf : p.WF cl top k) :
     cl c = some (if top then .symb (k + rargs.length) else .ctor (k + rargs.length)) := by
   induction H generalizing k with
-  | const => simpa using wf
+  | const => simpa [Pattern.WF] using wf
   | var _ ih =>
     have := ih (k := k + 1) wf
     rw [List.length_cons]; rw [Nat.add_succ, ← Nat.succ_add]; exact this
@@ -3615,8 +3614,8 @@ theorem pat_arity (hP : Params.Pat p r) (h : Arity (.const c) n p) :
   clear r hP h; intro cl n k h1 h2
   induction h2 generalizing k with
   | refl => simpa only [Nat.zero_add]
-  | var _ ih => simpa [Nat.succ_add] using ih _ h1
-  | app _ ih => simpa [Nat.succ_add] using ih _ h1.1
+  | var _ ih => simpa [Nat.succ_add, ← Nat.add_assoc] using ih _ h1
+  | app _ ih => simpa [Nat.succ_add, ← Nat.add_assoc] using ih _ h1.1
 
 theorem LE_Interp.Matches.lift (le : n ≤ n') (H : Matches (n := n) p c rargs m) :
     ∃ m', Matches p c (rargs.map (.lift n')) m' ∧ ∀ p, m p ≤ m' p ∧ m' p ≤ m p := by
@@ -4627,7 +4626,7 @@ structure StrongSoundEq (Γ : List SExpr) (M N A : SExpr) : Prop where
   left : StrongSound Γ M A
   right : StrongSound Γ N A
 
-theorem SoundEq.rfl : SoundEq Γ M M := fun _ _ _ _ => .rfl
+protected theorem SoundEq.rfl : SoundEq Γ M M := fun _ _ _ _ => .rfl
 theorem SoundEq.symm : SoundEq Γ M N → SoundEq Γ N M := fun H _ _ W _ => (H W).symm
 theorem StrongSoundEq.hasType : StrongSoundEq Γ M N A → StrongSound Γ M A ∧ StrongSound Γ N A
   | ⟨_, _, h1, h2⟩ => ⟨h1, h2⟩
@@ -4713,7 +4712,8 @@ theorem SoundEq.forallE_inv (H : SoundEq Γ (.forallE A B) (.forallE A' B'))
       · refine fun _ => ⟨_, WShape.bot_le, .bot' (.bot' .sort), ?_⟩
         simpa [WShapeFun.single_app] using .rfl
       · intro x h'; cases h'.bot_r
-        simpa [WShapeFun.single_app] using h.mono_l fun _ => TShape.bot_le'
+        simpa [WShapeFun.single_app, show m.2.T = m from rfl] using
+          h.mono_l fun _ => TShape.bot_le'
     | @cons Γ ρ A a x b1 b2 b3 b4 =>
       let k := max (max x.1 m.1) a.1
       have hk := Nat.max_le.1 (Nat.le_refl k); simp [Nat.max_le] at hk

Lean4Lean/Experimental/Stratified.lean

@@ -4,7 +4,7 @@ import Lean4Lean.Theory.Typing.Strong
 namespace Lean4Lean
 namespace VEnv
 
-open VExpr
+open Lean4Lean VExpr
 
 def DefInv (env : VEnv) (U : Nat) (Γ : List VExpr) : VExpr → VExpr → Prop
   | .forallE A B, .forallE A' B' =>

Lean4Lean/Experimental/StratifiedUntyped.lean

@@ -4,7 +4,7 @@ import Lean4Lean.Theory.Typing.Strong
 namespace Lean4Lean
 namespace VEnv
 
-open VExpr
+open Lean4Lean VExpr
 
 section
 set_option hygiene false

Lean4Lean/Experimental/Stronger.lean

@@ -2,7 +2,7 @@ import Lean4Lean.Theory.Typing.Lemmas
 
 namespace Lean4Lean
 
-open VExpr
+open Lean4Lean VExpr
 
 structure VEnv'.VConstant extends Lean4Lean.VConstant where
   level : VLevel
@@ -339,10 +339,12 @@ theorem IsDefEqStrong.instL (H : env.IsDefEqStrong U Γ e1 e2 A u) :
   | defeqL _ _ h3 _ ih => exact .defeqL (.inst hls) (.inst hls) (VLevel.inst_congr_l h3) ih
   | beta _ _ _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 ih6 =>
     simpa using .beta (.inst hls) (.inst hls) ih1 ih2 ih3 ih4
-      (by simpa using ih5) (by simpa using ih6)
+      (by simpa [VExpr.instL, VLevel.inst] using ih5)
+      (by simpa [VExpr.instL, VLevel.inst] using ih6)
   | eta _ _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
     simpa [VExpr.instL] using .eta (.inst hls) (.inst hls) ih1 ih2
-      (by simpa [VCtx.instL] using ih3) ih4 (by simpa [VExpr.instL] using ih5)
+      (by simpa [VCtx.instL, VExpr.instL, VLevel.inst] using ih3) ih4
+      (by simpa [VCtx.instL, VExpr.instL, VLevel.inst] using ih5)
   | proofIrrel _ _ _ ih1 ih2 ih3 =>
     exact .proofIrrel ih1 ih2 ih3
   | extra h1 h2 h3 h4 _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>