diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 68024947..0776dff9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,16 +23,18 @@ jobs: # 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. + # `Lean4Lean.Theory`, `Lean4Lean.Verify` and `Lean4Lean.Tests`. `--wfail` + # keeps that surface warning-free for consumers that build it that way; + # the frontier `sorry`s are annotated at their declarations, so they no + # longer count. `Lean4Lean.Experimental` is not a default target. - name: Build uses: leanprover/lean-action@v1 with: - use-mathlib-cache: false + build-args: --wfail # `Lean4Lean.Experimental` is WIP and deliberately not a default target, but it still has to - # compile. `sorry`s here are expected, as in `Verify`. + # compile. No `--wfail`: this is parked proof work outside the audited surface, so its + # `sorry`s are unannotated on purpose and stay visible as warnings. - name: Build Lean4Lean.Experimental run: lake build Lean4Lean.Experimental @@ -43,7 +45,7 @@ jobs: # literals the way a source grep can. Not a default target, so it is built # explicitly here; the surface it imports is already built above. - name: Check sorry frontier - run: lake build Lean4Lean.Audit.SorryFrontier + run: lake build --wfail Lean4Lean.Audit.SorryFrontier # `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. diff --git a/Lean4Lean/Audit/SorryFrontier.lean b/Lean4Lean/Audit/SorryFrontier.lean index 2d2806c1..d1c98fb6 100644 --- a/Lean4Lean/Audit/SorryFrontier.lean +++ b/Lean4Lean/Audit/SorryFrontier.lean @@ -105,6 +105,15 @@ is intentionally not imported. Runs as a build-time `run_cmd`, not an executable: `lake build` of this module is the whole check. + +Because this audit is what guards the frontier, every allowlisted declaration +that would log Lean's "declaration uses `sorry`" warning carries `set_option +warn.sorry false in` at its definition, which keeps `lake build --wfail` clean +for downstream consumers. (The `#guard_msgs`-pinned fixtures below need no +annotation: their warning is captured by the pinned message.) Suppressing the +warning costs no safety here, since the check reads `sorryAx` out of the +environment: a sorry that is new, moved, or renamed still fails this build, and +one added without the annotation also still fails `--wfail`. -/ open Lean Lean.Elab.Command diff --git a/Lean4Lean/Inductive/Add.lean b/Lean4Lean/Inductive/Add.lean index 4f057747..e665dcd0 100644 --- a/Lean4Lean/Inductive/Add.lean +++ b/Lean4Lean/Inductive/Add.lean @@ -264,13 +264,10 @@ theorem checkInductiveTypes_singleton_zero_of_whnf_sort cases hfuel_eq : context.fuel.inductiveFuel with | zero => omega | succ fuel => - simp [checkInductiveTypes, checkInductiveTypes.loopInd, - checkInductiveTypes.loopInd.loop, singletonInductiveStats, - readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, Bind.bind, Pure.pure, ReaderT.pure, - Except.bind, Except.pure, liftTypeChecker_apply, - hclosed, hcheck, hwhnf, hensure, hfuel_eq, - InductiveStats.initial, Expr.sortLevel!] + simp [checkInductiveTypes, checkInductiveTypes.loopInd, checkInductiveTypes.loopInd.loop, + singletonInductiveStats, readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read, + ReaderT.bind, Bind.bind, Pure.pure, Except.bind, Except.pure, liftTypeChecker_apply, hclosed, + hcheck, hwhnf, hensure, hfuel_eq, InductiveStats.initial, Expr.sortLevel!] /-- Transparent occurrence test for constants in the inductive block. @@ -1241,8 +1238,7 @@ theorem checkInductiveTypes_singleton_of_candidate (List.map Level.param context.lparams)).indConsts).isEmpty = true from rfl)] simp only [Expr.sortLevel!, InductiveStats.initial, Nat.zero_add] - simp only [ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, Except.pure, - Except.bind] + simp only [ReaderT.bind, Bind.bind, Except.pure, Except.bind] rw [checkInductiveTypes.loopInd.eq_1] have hdone : ¬1 < #[indType].size := by simp rw [dif_neg hdone] @@ -1320,7 +1316,7 @@ def isDefEqSteps : domainCandidate.isDefEqSteps ++ bodyCandidate.isDefEqSteps /-- Every retained WHNF observation is an exact checker execution. -/ -def allValid : (candidate : CandidateExprTrace context source) → +theorem allValid : (candidate : CandidateExprTrace context source) → ∀ step ∈ candidate.steps, step.Valid | .terminal context source _ result _ valid, step, h => by simp only [steps, List.mem_singleton] at h @@ -1334,7 +1330,7 @@ def allValid : (candidate : CandidateExprTrace context source) → · exact body.allValid step h /-- Every retained full-check observation is an exact checker execution. -/ -def allChecksValid : (candidate : CandidateExprTrace context source) → +theorem allChecksValid : (candidate : CandidateExprTrace context source) → ∀ step ∈ candidate.checkSteps, step.Valid | .terminal context source inferred _ checked _, step, h => by simp only [checkSteps, List.mem_singleton] at h @@ -1349,7 +1345,7 @@ def allChecksValid : (candidate : CandidateExprTrace context source) → /-- Every retained binder-domain equality is an exact successful checker execution. -/ -def allIsDefEqValid : (candidate : CandidateExprTrace context source) → +theorem allIsDefEqValid : (candidate : CandidateExprTrace context source) → ∀ step ∈ candidate.isDefEqSteps, step.Valid | .terminal .., step, h => by simp [isDefEqSteps] at h | .forallE _ _ _ _ _ _ _ _ _ annotationsEq _ _ domain body, diff --git a/Lean4Lean/Inductive/EliminationTrace.lean b/Lean4Lean/Inductive/EliminationTrace.lean index b62cf3e5..b3c17465 100644 --- a/Lean4Lean/Inductive/EliminationTrace.lean +++ b/Lean4Lean/Inductive/EliminationTrace.lean @@ -104,8 +104,7 @@ theorem run rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply] have notField : ¬ argIdx ≥ stats.params.size := Nat.not_le.mpr isParameter - simp only [notField, if_false, ReaderT.pure, Pure.pure, - ReaderT.bind, Bind.bind, Except.bind, Except.pure] + simp only [notField, if_false, Bind.bind] exact ih | proofField context fuel argIdx toCheck name domain body binderInfo sortResult isField ensureStep isProp tail ih => @@ -114,8 +113,7 @@ theorem run simp only [isField, if_true, ReaderT.bind, Bind.bind, liftTypeChecker_apply] rw [ensureStep] - simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true, - if_false, Pure.pure] + simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true, if_false] exact ih | dataField context fuel argIdx toCheck name domain body binderInfo sortResult isField ensureStep isProp tail ih => @@ -124,7 +122,7 @@ theorem run simp only [isField, if_true, ReaderT.bind, Bind.bind, liftTypeChecker_apply] rw [ensureStep] - simp only [Except.bind, isProp, Bool.not_false, if_true, Pure.pure] + simp only [Except.bind, isProp, Bool.not_false, if_true] exact ih | terminal context source fuel argIdx toCheck notForall => cases source <;> diff --git a/Lean4Lean/Theory/Inductive.lean b/Lean4Lean/Theory/Inductive.lean index 24f876e0..bfd7f5f3 100644 --- a/Lean4Lean/Theory/Inductive.lean +++ b/Lean4Lean/Theory/Inductive.lean @@ -2110,7 +2110,7 @@ def NormalizedFamily.generationShape (np : Nat) family.ctorPairs.all (NormalizedCtor.generationShape np) def NormalizedCheckedBlock.rawParams {source : VInductDecl} - (block : NormalizedCheckedBlock source) : List VExpr := + (_block : NormalizedCheckedBlock source) : List VExpr := blockParams source.nparams source.types def NormalizedCheckedBlock.familyPairs {source : VInductDecl} @@ -2727,7 +2727,7 @@ def NormalizedBlockCtor.rawResult {source : VInductDecl} /-- Normalized constructor result reconstructed with the stored owner name. -/ def NormalizedBlockCtor.resultTarget {source : VInductDecl} - (gen : BlockGenerationChecked source) + (_gen : BlockGenerationChecked source) (constructor : NormalizedBlockCtor) : VExpr := VExpr.appN (.const constructor.familyName (VLevel.params source.uvars)) diff --git a/Lean4Lean/Theory/NestedInductive.lean b/Lean4Lean/Theory/NestedInductive.lean index b8d6a386..38d12913 100644 --- a/Lean4Lean/Theory/NestedInductive.lean +++ b/Lean4Lean/Theory/NestedInductive.lean @@ -385,7 +385,7 @@ namespace NestedBlockChecked variable {source : VInductDecl} /-- The main family name owning the restored recursor inventory. -/ -def mainName (nested : NestedBlockChecked source) : Name := +def mainName (_nested : NestedBlockChecked source) : Name := match source.types with | ty :: _ => ty.name | [] => .anonymous diff --git a/Lean4Lean/Theory/Projection.lean b/Lean4Lean/Theory/Projection.lean index 771d9e85..5951d058 100644 --- a/Lean4Lean/Theory/Projection.lean +++ b/Lean4Lean/Theory/Projection.lean @@ -356,7 +356,7 @@ private theorem VExpr.instRevAt_appN_projection | cons arg args ih => simp only [VExpr.instRevAt, VExpr.instN_appN] rw [ih] - simp only [List.map_map, Function.comp_def, VExpr.instRevAt] + simp only [List.map_map, Function.comp_def] private theorem VExpr.map_instRevAt_closedN (args es : List VExpr) (k : Nat) (hclosed : ∀ e ∈ es, e.ClosedN k) : @@ -902,8 +902,7 @@ def projectionMinorType (view : VStructureView) (view.structureType levels params).instL ls = view.structureType (levels.map (VLevel.inst ls)) (params.map (VExpr.instL ls)) := by - simp [structureType, VExpr.instL_appN, VExpr.instL, - VLevel.inst_inst, Function.comp_def] + simp [structureType, VExpr.instL_appN, VExpr.instL] @[simp] theorem structureType_liftN (view : VStructureView) (levels : List VLevel) (params : List VExpr) (n k : Nat) : @@ -924,8 +923,7 @@ def projectionMinorType (view : VStructureView) (view.specializedFields levels params).map (VExpr.instL ls) = view.specializedFields (levels.map (VLevel.inst ls)) (params.map (VExpr.instL ls)) := by - simp [specializedFields, VExpr.instL_instRevAt, - VExpr.instL_instL, VLevel.inst_inst, Function.comp_def] + simp [specializedFields, VExpr.instL_instRevAt, VExpr.instL_instL, Function.comp_def] private def projectionCode (view : VStructureView) (levels : List VLevel) (params allFields : List VExpr) @@ -1070,10 +1068,8 @@ private theorem projectionCode_instN (view : VStructureView) · simp [projectionCode, ProjectionCode.instN, VExpr.inst, VExpr.instN_lamN_projection, VExpr.instTelN_length, hminorVar] - · simp [projectionCode, ProjectionCode.instN, VExpr.inst, - VExpr.instN_appN, VExpr.instN_lamN_projection, - VExpr.instTelN_length, ← VExpr.lift_instN_lo, - VExpr.instTelN_lift_projection, List.map_append, + · simp [projectionCode, ProjectionCode.instN, VExpr.inst, VExpr.instN_appN, + VExpr.instN_lamN_projection, VExpr.instTelN_length, ← VExpr.lift_instN_lo, List.map_append, List.map_map, Function.comp_def, hmotive, hminorVar] private def projectionCodes.go (view : VStructureView) @@ -1347,8 +1343,7 @@ private theorem projectionCodes.go_get?_typeFn (view : VStructureView) (projectionCodes.go view levels params allFields structType fields fieldSorts (i + 1) (previous ++ [head])).take j := by - simp [head, projectionCodes.go, List.take, - List.append_assoc] + simp [head, projectionCodes.go, List.append_assoc] rw [hpref] simpa only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using htypeFn @@ -1999,7 +1994,7 @@ private theorem WF.motiveLevel_projectionLevels rw [← structureType_liftN] apply projectionCodes.go_liftN · rfl - · simp [VExpr.liftTelN_length] + · simp @[simp] theorem WF.projectionCodes_instN (self : VStructureView.WF view env) (henv : env.Ordered) @@ -2014,7 +2009,7 @@ private theorem WF.motiveLevel_projectionLevels rw [← structureType_instN] apply projectionCodes.go_instN · rfl - · simp [VExpr.instTelN_length] + · simp /-- The exact lower-layer structure-eta descriptor generated by a checked structure view. Its projector syntax is the deterministic projector program @@ -2131,7 +2126,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.constructorParamsSpine (self : VStructureView.WF view env) (henv : env.Ordered) {U : Nat} {Γ : List VExpr} (levels : List VLevel) (hlevels : ∀ level ∈ levels, level.WF U) - (hlevelsLength : levels.length = view.uvars) + (_hlevelsLength : levels.length = view.uvars) (params : List VExpr) (hparamsLength : params.length = view.nparams) (paramsSpine : ∃ resultLevel, env.SpineWF U Γ (view.familyType.instL levels) @@ -2228,7 +2223,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.familyParamsSpine_of_constructor (self : VStructureView.WF view env) (henv : env.Ordered) {U : Nat} {Γ : List VExpr} (levels : List VLevel) (hlevels : ∀ level ∈ levels, level.WF U) - (hlevelsLength : levels.length = view.uvars) + (_hlevelsLength : levels.length = view.uvars) (params : List VExpr) (hparamsLength : params.length = view.nparams) {target cursor : VExpr} (constructorSpine : env.SpineWF U Γ @@ -2321,7 +2316,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.specializedFields_onSortTel (self : VStructureView.WF view env) (henv : env.Ordered) {U : Nat} {Γ : List VExpr} (levels : List VLevel) (hlevels : ∀ level ∈ levels, level.WF U) - (hlevelsLength : levels.length = view.uvars) + (_hlevelsLength : levels.length = view.uvars) (params : List VExpr) (hparamsLength : params.length = view.nparams) (paramsSpine : ∃ resultLevel, env.SpineWF U Γ (view.familyType.instL levels) @@ -2505,7 +2500,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType (hmotiveLevel : view.generation.motiveLevel.inst (view.projectionLevels fieldSort levels) = fieldSort) - (structIsType : env.IsType U Γ + (_structIsType : env.IsType U Γ (view.structureType levels params)) {typeFn minor major : VExpr} (typeFnType : env.HasType U Γ typeFn @@ -2623,31 +2618,17 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType (view.specializedFields levels params) typeFn) (.forallE (view.structureType levels params).lift (.app (typeFn.liftN 2) (.bvar 0))) := by - simp [gen, pLevels, recRest, k, ni, - VInductDecl.GenerationChecked.minorTypes, - VInductDecl.GenerationChecked.minorTypesAux, - VInductDecl.GenerationChecked.minorType, - VInductDecl.GenerationChecked.idxTel, - VInductDecl.NormalizedCtor.fieldsR, - VInductDecl.NormalizedCtor.recArgsR, - VInductDecl.NormalizedCtor.resultIndicesR, - VInductDecl.ihsFromRecArgs, - VStructureView.projectionMinorType, - VStructureView.projectionConstructorApp, - view.constructor_eq, view.raw_indices_eq, - hresultIndices, view.recursive_eq, - VExpr.instL_forallN, VExpr.instL_appN, - VExpr.liftTelN_instL, - VExpr.instL_instL, VExpr.instN_forallN, - VExpr.instTelN, - VExpr.instRevAt_forallN_projection, - VExpr.instRevAt_forallE_projection, - VExpr.instN_appN, VExpr.instRev, - VExpr.instRev_appN, List.map_append, - VExpr.bvarRevRange, List.map_append, + simp [gen, pLevels, recRest, k, ni, VInductDecl.GenerationChecked.minorTypes, + VInductDecl.GenerationChecked.minorTypesAux, VInductDecl.GenerationChecked.minorType, + VInductDecl.GenerationChecked.idxTel, VInductDecl.NormalizedCtor.fieldsR, + VInductDecl.NormalizedCtor.recArgsR, VInductDecl.NormalizedCtor.resultIndicesR, + VInductDecl.ihsFromRecArgs, VStructureView.projectionMinorType, + VStructureView.projectionConstructorApp, view.constructor_eq, view.raw_indices_eq, + hresultIndices, view.recursive_eq, VExpr.instL_forallN, VExpr.instL_appN, + VExpr.liftTelN_instL, VExpr.instL_instL, VExpr.instN_forallN, VExpr.instTelN, + VExpr.instRevAt_forallN_projection, List.map_append, VExpr.bvarRevRange, List.map_append, List.map_map, Function.comp_def, - VStructureView.sourceLevels_projectionLevels view fieldSort levels - hlevelsLength, hparamsLength] + VStructureView.sourceLevels_projectionLevels view fieldSort levels hlevelsLength] change VExpr.forallE _ _ = VExpr.forallE _ _ congr 1 · have hfieldTel := @@ -2685,9 +2666,8 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType (view.constructor.rawFields view.source.nparams).length := by simp [VStructureView.specializedFields, VStructureView.fields] - simp only [VExpr.forallN, VExpr.instL, - VExpr.bvarRevRange_map_instL, - hliftedLength, hspecializedLength, hparamsLength] + simp only [VExpr.forallN, VExpr.instL, VExpr.bvarRevRange_map_instL, hliftedLength, + hspecializedLength] rw [hsourceLevels] have hbody := VExpr.projectionMinorBody_shape view.constructorName levels @@ -2702,10 +2682,8 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType (VLevel.params' view.source.uvars view.generation.elimination.offset).map (VLevel.inst pLevels) = levels at hsourceLevels - simp only [VExpr.forallN, VExpr.liftTelN, List.zipIdx_nil, - List.map_nil, VExpr.instTelN, Nat.add_zero, - VExpr.instL, VExpr.instL_appN, - VExpr.bvarRevRange_map_instL, VExpr.instL] + simp only [VExpr.forallN, VExpr.liftTelN, List.zipIdx_nil, List.map_nil, VExpr.instTelN, + VExpr.instL, VExpr.instL_appN, VExpr.bvarRevRange_map_instL, VExpr.instL] rw [hsourceLevels] simpa [gen, hparamsLength, VStructureView.structureType] using (VExpr.projectionMajorTail_shape view.name levels params typeFn) @@ -3294,7 +3272,7 @@ theorem TrProj.mono {env env' : VEnv} (henv : env ≤ env') params_length := self.params_length paramsSpine := self.paramsSpine.imp fun _ h => h.monoProjection henv majorType := self.majorType.mono henv - program := self.program.imp fun code ⟨hcode, hresult, htype⟩ => + program := self.program.imp fun _ ⟨hcode, hresult, htype⟩ => ⟨hcode, hresult, htype.mono henv⟩ /-- Weakening acts pointwise on the explicit parameters, major, and computed @@ -3511,6 +3489,7 @@ structure RegisteredStructureHeadInversion (env : VEnv) : Prop where Nonempty (ProjectionConstructorAlignment env U Γ view levels params idx code constructorName runtimeMajor runtimeField) +set_option warn.sorry false in /-- Public Tier-R registered-head inversion statement. L4L-16/17 discharge the underlying constant-head theorem; projection structural laws consume only this stable interface and therefore shed `sorryAx` automatically when it is diff --git a/Lean4Lean/Theory/Typing/ChurchRosser.lean b/Lean4Lean/Theory/Typing/ChurchRosser.lean index 8ebfddae..93e7fe7c 100644 --- a/Lean4Lean/Theory/Typing/ChurchRosser.lean +++ b/Lean4Lean/Theory/Typing/ChurchRosser.lean @@ -1845,6 +1845,7 @@ theorem StructEq.parRed_right (H : StructEq Γ e₁ e₂) have ⟨_, heq⟩ := H.defeq hΓ exact H.trans_right hΓ ⟨_, R.defeq hΓ heq.hasType.2⟩ +set_option warn.sorry false in variable! (hΓ : OnCtx Γ (IsType env univs)) in theorem NormalEq.parRed (H1 : Γ ⊢ e₁ ≡ₚ e₂) (H2 : Γ ⊢ e₂ ≫ e₂') : ∃ e₁', Γ ⊢ e₁ ≫* e₁' ∧ Γ ⊢ e₁' ≡ₚ e₂' := by diff --git a/Lean4Lean/Theory/Typing/InductiveLemmas.lean b/Lean4Lean/Theory/Typing/InductiveLemmas.lean index a07ade99..58db9cb9 100644 --- a/Lean4Lean/Theory/Typing/InductiveLemmas.lean +++ b/Lean4Lean/Theory/Typing/InductiveLemmas.lean @@ -51,7 +51,7 @@ theorem inst_bvar_of_closedN (h : ClosedN e (k+1)) : simp only [instVar] rcases Nat.lt_trichotomy i k with h' | rfl | h' · simp [h', liftVar_lt h'] - · simp [liftVar_le (Nat.le_refl _), liftN, liftVar_base, Nat.add_comm] + · simp [liftVar_le (Nat.le_refl _), liftN] · omega theorem ClosedN.appN {f : VExpr} (hf : f.ClosedN k) {as : List VExpr} @@ -1526,7 +1526,7 @@ theorem HasType.hasConst_false_of_absent typed.const_inv henv hΓ rw [absent] at present contradiction - · simpa [VExpr.hasConst, equality] + · simp [VExpr.hasConst, equality] | app function argument functionIH argumentIH => obtain ⟨domain, body, functionType, argumentType⟩ := typed.app_inv henv hΓ @@ -1672,7 +1672,7 @@ theorem onTel_of_free {env : VEnv} {U : Nat} : ∀ {As Γ}, (∀ A ∈ As, ∀ Γ', env.IsType U Γ' A) → OnTel env U Γ As | [], _, _ => trivial | _ :: _, _, h => - ⟨h _ (.head _) _, onTel_of_free fun A h' Γ' => h _ (.tail _ h') Γ'⟩ + ⟨h _ (.head _) _, onTel_of_free fun _ h' Γ' => h _ (.tail _ h') Γ'⟩ theorem OnTel.append {env : VEnv} {U : Nat} : ∀ {As Bs Γ}, OnTel env U Γ As → OnTel env U (As.reverse ++ Γ) Bs → OnTel env U Γ (As ++ Bs) @@ -1705,7 +1705,7 @@ theorem OnTel.weakN {env : VEnv} {U n : Nat} (henv : env.Ordered) : ∀ {As Γ Γ' k}, Ctx.LiftN n k Γ Γ' → OnTel env U Γ As → OnTel env U Γ' (VExpr.liftTelN n As k) | [], _, _, _, _, _ => trivial - | _ :: As, _, _, _, W, ⟨hA, hT⟩ => + | _ :: _, _, _, _, W, ⟨hA, hT⟩ => ⟨hA.weakN henv W, OnTel.weakN henv W.succ hT⟩ /-- Universe instantiation of a telescope. -/ @@ -1888,7 +1888,7 @@ theorem recArgs_ge {U : Nat} {T : Name} {np ni : Nat} : ∀ {Bs : List VExpr} {j split at h · next r₀ hr₀ => rcases List.mem_cons.1 h with rfl | h - · simpa [(recArg?_eq hr₀).1] + · simp [(recArg?_eq hr₀).1] · exact Nat.le_of_succ_le (recArgs_ge _ h) · exact Nat.le_of_succ_le (recArgs_ge _ h) @@ -2111,7 +2111,7 @@ previous IH binders. -/ theorem RecArg.minorIH_shift (r : RecArg) (m p : Nat) (hj : r.fieldIndex < m) : r.minorIH m p = (r.minorIH m 0).liftN p := by - simp only [RecArg.minorIH, VExpr.liftN_forallN, VExpr.liftTelN_length] + simp only [RecArg.minorIH, VExpr.liftN_forallN] rw [← r.minorBinders_shift m p] rw [show (r.minorBinders m 0).length = r.binders.length by simp [RecArg.minorBinders, VExpr.liftTelN_length], Nat.zero_add] @@ -2131,7 +2131,7 @@ theorem RecArg.minorIH_shift (r : RecArg) (m p : Nat) simp only [Function.comp_apply, Nat.add_zero] rw [VExpr.liftN'_liftN_hi] · congr 1 - simp only [Function.comp_apply, Nat.add_zero, VExpr.liftN_appN] + simp only [Nat.add_zero, VExpr.liftN_appN] rw [show (VExpr.bvar (m - 1 - r.fieldIndex + r.binders.length)).liftN p r.binders.length = .bvar (m - 1 - r.fieldIndex + p + r.binders.length) from by @@ -2169,7 +2169,7 @@ theorem RecArg.minorIH_zero_lift_ruleIH (r : RecArg) (m k : Nat) (r.fieldIndex + r.binders.length) + (m-r.fieldIndex) from by omega, VExpr.liftN_liftN_mid e k (m-r.fieldIndex) (by omega)] · congr 1 - simp only [Function.comp_apply, VExpr.liftN_appN] + simp only [VExpr.liftN_appN] rw [show (VExpr.bvar (m - 1 - r.fieldIndex + r.binders.length)).liftN k (m + r.binders.length) = .bvar (m - 1 - r.fieldIndex + r.binders.length) from by @@ -3501,13 +3501,11 @@ theorem familyApp_hasType {family : NormalizedFamily} simp only [List.map_reverse] at hresult have hctxChecked := ((S.emittedFamilyTel hfamily).instL (U' := gen.recUvars) gen.sourceLevels_wf).ctx - simp only [List.map_nil, List.append_nil, - List.map_reverse] at hctxChecked + simp only [List.map_nil, List.append_nil] at hctxChecked have hresultChecked := hresult.defeqDFC S.ord hctxChecked have hctxGeneration := ((S.generationFamilyTel hfamily).instL (U' := gen.recUvars) gen.sourceLevels_wf).ctx - simp only [List.map_nil, List.append_nil, - List.map_reverse] at hctxGeneration + simp only [List.map_nil, List.append_nil] at hctxGeneration have hresultGeneration := hresultChecked.defeqDFC S.ord (hctxGeneration.symm S.ord) have hresult' : env.IsDefEq gen.recUvars @@ -3575,6 +3573,9 @@ namespace GenerationEnv variable {source : VInductDecl} {gen : GenerationChecked source} {env : VEnv} (S : GenerationEnv gen env) include S +-- `S` is included throughout so every lemma below is reachable as `S.lemma`, +-- including those whose statement and proof never mention it. +set_option linter.unusedSectionVars false /-- The final mixed-generation invariant is monotone once the larger environment is known to remain ordered. -/ @@ -3988,13 +3989,11 @@ theorem familyApp_hasType : simp only [List.map_reverse] at hresult have hctxChecked := (S.emittedFamilyTel.instL (U' := gen.recUvars) gen.sourceLevels_wf).ctx - simp only [List.map_nil, List.append_nil, - List.map_reverse] at hctxChecked + simp only [List.map_nil, List.append_nil] at hctxChecked have hresultChecked := hresult.defeqDFC S.ord hctxChecked have hctxGeneration := (S.generationFamilyTel.instL (U' := gen.recUvars) gen.sourceLevels_wf).ctx - simp only [List.map_nil, List.append_nil, - List.map_reverse] at hctxGeneration + simp only [List.map_nil, List.append_nil] at hctxGeneration have hresultGeneration := hresultChecked.defeqDFC S.ord (hctxGeneration.symm S.ord) have hresult' : env.IsDefEq (gen.recUvars) @@ -5977,9 +5976,7 @@ theorem recBase_hasType {family : NormalizedFamily} exact S.recursor_hasType hfamily hrec have hspine := VEnv.HasType.appN_selfSpine (env := env) (U := gen.recUvars) hf - simp only [BlockGenerationChecked.recType, - List.reverse_append, List.append_nil, List.append_assoc, - List.length_append, List.length_reverse, + simp only [List.reverse_append, List.append_nil, List.append_assoc, List.length_append, gen.minorTypes_length, gen.motiveTypes_length] at hspine rw [show gen.paramsTel.length = source.nparams from by simpa [BlockGenerationChecked.paramsTel] using @@ -6601,8 +6598,7 @@ theorem blockRuleCall_hasType have hbaseLift : (gen.recBase m r.targetType).liftN r.binders.length = gen.recBase (m+r.binders.length) r.targetType := by - simp only [BlockGenerationChecked.recBase, VExpr.liftN_appN, - VExpr.liftN, List.map_map] + simp only [BlockGenerationChecked.recBase, VExpr.liftN_appN, VExpr.liftN] rw [bvarRevRange_liftN_ge _ _ _ _ (Nat.zero_le _)] apply congrArg (VExpr.appN _) apply VExpr.bvarRevRange_congr @@ -6845,7 +6841,7 @@ theorem minorApp_hasType {i : Nat} rw [show m+0+rs.length = m+rs.length by omega, VExpr.liftN_liftN_midN e d k rs.length (Nat.zero_le _)] · congr 1 - simp only [Function.comp_apply] + simp only [] rw [show m+0+rs.length = m+rs.length by omega, VExpr.liftN_appN, VExpr.liftN_appN, List.map_append, List.map_append, @@ -6982,6 +6978,9 @@ namespace GenerationEnv variable {source : VInductDecl} {gen : GenerationChecked source} {env : VEnv} (S : GenerationEnv gen env) include S +-- `S` is included throughout so every lemma below is reachable as `S.lemma`, +-- including those whose statement and proof never mention it. +set_option linter.unusedSectionVars false /-- Checked field semantics for one paired constructor, re-indexed onto the raw block header used by mixed generation. -/ @@ -7251,8 +7250,7 @@ theorem recArg_transport {ctor : NormalizedCtor} (hprefix.symm S.ord) have hfull := htelGeneration.extendDefEqCtx hprefix have hspGeneration := hspChecked.defeqDFC S.ord (hfull.symm S.ord) - simp only [RecArg.instL, VExpr.instL_forallN, - VExpr.liftTelN_instL, List.map_reverse] at htelGeneration hspGeneration + simp only [VExpr.instL_forallN, VExpr.liftTelN_instL] at htelGeneration hspGeneration have hjlen : ((ctor.fieldsR source.uvars source.nparams gen.elimination).take r₀.fieldIndex).length = r₀.fieldIndex := by @@ -7436,6 +7434,9 @@ namespace GenerationEnv variable {source : VInductDecl} {gen : GenerationChecked source} {env : VEnv} (S : GenerationEnv gen env) include S +-- `S` is included throughout so every lemma below is reachable as `S.lemma`, +-- including those whose statement and proof never mention it. +set_option linter.unusedSectionVars false /-- One mixed generalized induction-hypothesis entry is a type. The bound field keeps its raw domain; `emittedField_defeq` converts it to the retained @@ -8655,6 +8656,9 @@ namespace GenerationEnv variable {source : VInductDecl} {gen : GenerationChecked source} {env : VEnv} (S : GenerationEnv gen env) include S +-- `S` is included throughout so every lemma below is reachable as `S.lemma`, +-- including those whose statement and proof never mention it. +set_option linter.unusedSectionVars false /-! ## Mixed iota-rule preservation -/ @@ -8784,12 +8788,8 @@ theorem recBase_hasType exact S.recursor_hasType hrec have hspine := HasType.appN_selfSpine (env := env) (U := gen.recUvars) hf - simp only [GenerationChecked.recType, - List.reverse_append, List.reverse_cons, - List.append_nil, List.append_assoc, - List.singleton_append, List.length_append, - List.length_cons, List.length_reverse, - gen.minorTypes_length] at hspine + simp only [List.reverse_append, List.reverse_cons, List.append_nil, List.append_assoc, + List.singleton_append, List.length_append, List.length_cons, gen.minorTypes_length] at hspine rw [show gen.paramsTel.length = source.nparams from by simp [GenerationChecked.paramsTel, S.generationParams_length], @@ -9807,8 +9807,7 @@ theorem minorApp_hasType {i : Nat} {ctor : NormalizedCtor} source.uvars source.nparams gen.elimination).length)).liftN (ctor.fieldsR source.uvars source.nparams gen.elimination).length := by - simp only [GenerationChecked.minorType, - rs, hrs] + simp only [GenerationChecked.minorType, rs] conv => lhs; rw [VExpr.liftN_forallN, VExpr.liftTelN_liftTelN, liftTelN_congr _ _ @@ -10015,7 +10014,7 @@ theorem minorApp_hasType {i : Nat} {ctor : NormalizedCtor} gen.block.ctorPairs.length rs.length (Nat.zero_le _)] · congr 1 - simp only [Function.comp_apply] + simp only [] rw [show (ctor.fieldsR source.uvars source.nparams gen.elimination).length + @@ -10500,6 +10499,9 @@ structure Stage3Env (env : VEnv) (U : Nat) (T : Name) (np : Nat) (l : VLevel) variable {env : VEnv} {U : Nat} {T : Name} {np : Nat} {l : VLevel} {ty : VInductiveType} (S : Stage3Env env U T np l ty) include S +-- `S` is included throughout so every lemma below is reachable as `S.lemma`, +-- including those whose statement and proof never mention it. +set_option linter.unusedSectionVars false theorem Stage3Env.mono {env' : VEnv} (henv : env ≤ env') (ord' : env'.Ordered) : Stage3Env env' U T np l ty where @@ -10824,8 +10826,7 @@ theorem Stage3Env.recArg_transport {c : VConstVal} (hc : c ∈ ty.ctors) simp [ctorFieldsR, paramsTel, List.map_reverse, List.map_take] rw [hctx] at htel₁ rw [List.map_append, List.map_reverse, hctx] at hsp₁ - simp only [RecArg.instL, VExpr.instL_forallN, VExpr.liftTelN_instL, - List.map_reverse] at htel₁ hsp₁ + simp only [VExpr.instL_forallN, VExpr.liftTelN_instL] at htel₁ hsp₁ have hjlen : ((ctorFieldsR U np c).take r₀.fieldIndex).length = r₀.fieldIndex := by simp only [ctorFieldsR, List.length_take, List.length_map] @@ -11937,9 +11938,8 @@ theorem Stage3Env.recBase_hasType S.recType_closedN.liftN_eq (Nat.zero_le _)] exact S.recConst_hasType hrec have hspine := HasType.appN_selfSpine (env := env) (U := U+1) hf - simp only [recType, List.reverse_append, List.reverse_cons, List.append_nil, - List.append_assoc, List.singleton_append, List.length_append, List.length_cons, - List.length_reverse, minorTypes_length] at hspine + simp only [List.reverse_append, List.reverse_cons, List.append_nil, List.append_assoc, + List.singleton_append, List.length_append, List.length_cons, minorTypes_length] at hspine rw [show (paramsTel U np ty).length = np from by simp [paramsTel, List.length_map, S.hlen], VExpr.bvarRevRange_congr' Δ.length (show @@ -11986,9 +11986,8 @@ theorem Stage3Env.recBaseRec_hasType S.recTypeRec_closedN.liftN_eq (Nat.zero_le _)] exact S.recConstRec_hasType hrec have hspine := HasType.appN_selfSpine (env := env) (U := U+1) hf - simp only [recTypeRec, List.reverse_append, List.reverse_cons, List.append_nil, - List.append_assoc, List.singleton_append, List.length_append, List.length_cons, - List.length_reverse, minorTypesRec_length] at hspine + simp only [List.reverse_append, List.reverse_cons, List.append_nil, List.append_assoc, + List.singleton_append, List.length_append, List.length_cons, minorTypesRec_length] at hspine rw [show (paramsTel U np ty).length = np from by simp [paramsTel, List.length_map, S.hlen], VExpr.bvarRevRange_congr' Δ.length (show @@ -12362,8 +12361,8 @@ theorem Stage3Env.ctorAppRule_hasType {c : VConstVal} (hc : c ∈ ty.ctors) : have hlen : (VExpr.liftTelN 1 (ctorFieldsR U np c) 0).length = (ctorFieldsR U np c).length := VExpr.liftTelN_length .. rw [hlen] at h - simp only [List.nil_append, List.length_nil, Nat.zero_add, VExpr.liftN_appN, - VExpr.liftN, List.map_append, List.map_map] at h + simp only [List.length_nil, Nat.zero_add, VExpr.liftN_appN, VExpr.liftN, List.map_append, + List.map_map] at h rw [VExpr.liftTelN_liftTelN, bvarRevRange_liftN_ge _ _ _ _ (by omega), VExpr.bvarRevRange_liftN_high _ _ _ _ (by omega)] at h @@ -12403,8 +12402,8 @@ theorem Stage3Env.ctorAppRuleRec_hasType {c : VConstVal} (hc : c ∈ ty.ctors) : have hlen : (VExpr.liftTelN 1 (ctorFieldsR U np c) 0).length = (ctorFieldsR U np c).length := VExpr.liftTelN_length .. rw [hlen] at h - simp only [List.nil_append, List.length_nil, Nat.zero_add, VExpr.liftN_appN, - VExpr.liftN, List.map_append, List.map_map] at h + simp only [List.length_nil, Nat.zero_add, VExpr.liftN_appN, VExpr.liftN, List.map_append, + List.map_map] at h rw [VExpr.liftTelN_liftTelN, bvarRevRange_liftN_ge _ _ _ _ (by omega), VExpr.bvarRevRange_liftN_high _ _ _ _ (by omega)] at h @@ -12974,7 +12973,7 @@ theorem Stage3Env.minorApp_hasType {i : Nat} {c : VConstVal} VExpr.bvarRevRange rs.length (ctorFieldsR U np c).length)]))).liftN ty.ctors.length (ctorFieldsR U np c).length)).liftN (ctorFieldsR U np c).length := by - simp only [minorType, rs, hrs, ElimMode.large_sourceLevels] + simp only [minorType, rs, ElimMode.large_sourceLevels] conv => lhs; rw [VExpr.liftN_forallN, VExpr.liftTelN_liftTelN, liftTelN_congr _ _ (show (1:Nat) + ((ctorFieldsR U np c).length + ty.ctors.length) = @@ -13049,7 +13048,7 @@ theorem Stage3Env.minorApp_hasType {i : Nat} {c : VConstVal} (ctorFieldsR U np c).length + rs.length from by omega, VExpr.liftN_liftN_mid e ty.ctors.length rs.length (Nat.zero_le _)] · congr 1 - simp only [Function.comp_apply] + simp only [] rw [show (ctorFieldsR U np c).length + 0 + rs.length = (ctorFieldsR U np c).length + rs.length from by omega] rw [VExpr.liftN_appN, VExpr.liftN_appN, List.map_append, List.map_append, @@ -13167,7 +13166,7 @@ theorem Stage3Env.minorAppRec_hasType {i : Nat} {c : VConstVal} VExpr.bvarRevRange rs.length (ctorFieldsR U np c).length)]))).liftN ty.ctors.length (ctorFieldsR U np c).length)).liftN (ctorFieldsR U np c).length := by - simp only [minorTypeRec, rs, hrs, ElimMode.large_sourceLevels] + simp only [minorTypeRec, rs, ElimMode.large_sourceLevels] conv => lhs; rw [VExpr.liftN_forallN, VExpr.liftTelN_liftTelN, liftTelN_congr _ _ (show (1:Nat) + ((ctorFieldsR U np c).length + ty.ctors.length) = @@ -13242,7 +13241,7 @@ theorem Stage3Env.minorAppRec_hasType {i : Nat} {c : VConstVal} (ctorFieldsR U np c).length + rs.length from by omega, VExpr.liftN_liftN_mid e ty.ctors.length rs.length (Nat.zero_le _)] · congr 1 - simp only [Function.comp_apply] + simp only [] rw [show (ctorFieldsR U np c).length + 0 + rs.length = (ctorFieldsR U np c).length + rs.length from by omega] rw [VExpr.liftN_appN, VExpr.liftN_appN, List.map_append, List.map_append, diff --git a/Lean4Lean/Theory/Typing/Injectivity.lean b/Lean4Lean/Theory/Typing/Injectivity.lean index 462173f7..971ded23 100644 --- a/Lean4Lean/Theory/Typing/Injectivity.lean +++ b/Lean4Lean/Theory/Typing/Injectivity.lean @@ -8,9 +8,11 @@ A bunch of important structural theorems which we can't prove :( namespace Lean4Lean namespace VEnv +set_option warn.sorry false in theorem IsDefEqU.sort_inv (henv : VEnv.WF env) (hΓ : OnCtx Γ (env.IsType U)) (h1 : env.IsDefEqU U Γ (.sort u) (.sort v)) : u ≈ v := sorry +set_option warn.sorry false in theorem IsDefEqU.forallE_inv_stratified (henv : VEnv.WF env) (hΓ : OnCtx Γ (env.IsType U)) (h1 : env.IsDefEqU U Γ (.forallE A B) (.forallE A' B')) (h2 : env.HasTypeStratified U Γ (.forallE A B) V true n) @@ -30,5 +32,6 @@ theorem IsDefEqU.forallE_inv (henv : VEnv.WF env) (hΓ : OnCtx Γ (env.IsType U) let ⟨⟨_, a1, _⟩, _, a2, _⟩ := IsDefEqU.forallE_inv_stratified henv hΓ h1 h2 h3 ⟨⟨_, a1⟩, _, a2⟩ +set_option warn.sorry false in theorem IsDefEqU.sort_forallE_inv (henv : VEnv.WF env) (hΓ : OnCtx Γ (env.IsType U)) : ¬env.IsDefEqU U Γ (.sort u) (.forallE A B) := sorry diff --git a/Lean4Lean/Theory/Typing/Pattern.lean b/Lean4Lean/Theory/Typing/Pattern.lean index 44faa7f6..5b7108b2 100644 --- a/Lean4Lean/Theory/Typing/Pattern.lean +++ b/Lean4Lean/Theory/Typing/Pattern.lean @@ -363,16 +363,15 @@ theorem Pattern.varN_const_inter_some : intro n' p h cases n' with | zero => - simp [Pattern.varN, Pattern.inter] at h + simp [Pattern.inter] at h exact ⟨h.1, rfl, h.2.symm⟩ - | succ n' => simp [Pattern.varN, Pattern.inter] at h + | succ n' => simp [Pattern.inter] at h | succ n ih => intro n' p h cases n' with - | zero => simp [Pattern.varN, Pattern.inter] at h + | zero => simp [Pattern.inter] at h | succ n' => - simp only [Pattern.varN, Pattern.inter, bind, Option.bind_eq_some_iff, - Option.pure_def, Option.some.injEq] at h + simp only [Pattern.inter, bind, Option.bind_eq_some_iff, Option.pure_def, Option.some.injEq] at h obtain ⟨q, hq, rfl⟩ := h obtain ⟨rfl, rfl, rfl⟩ := ih hq exact ⟨rfl, rfl, rfl⟩ @@ -396,10 +395,9 @@ theorem Pattern.app_inter_varN_const_some {f a : Pattern} ∃ n' q, n = n' + 1 ∧ f.inter (Pattern.varN (.const c) n') = some q ∧ p = .app q a := by cases n with - | zero => simp [Pattern.varN, Pattern.inter] at h + | zero => simp [Pattern.inter] at h | succ n' => - simp only [Pattern.varN, Pattern.inter, bind, Option.bind_eq_some_iff, - Option.pure_def, Option.some.injEq] at h + simp only [Pattern.inter, bind, Option.bind_eq_some_iff, Option.pure_def, Option.some.injEq] at h obtain ⟨q, hq, rfl⟩ := h exact ⟨n', q, rfl, hq, rfl⟩ diff --git a/Lean4Lean/Theory/Typing/UniqueTyping.lean b/Lean4Lean/Theory/Typing/UniqueTyping.lean index 13ed6c39..be1e3430 100644 --- a/Lean4Lean/Theory/Typing/UniqueTyping.lean +++ b/Lean4Lean/Theory/Typing/UniqueTyping.lean @@ -168,6 +168,7 @@ theorem IsDefEqU.trans (henv : VEnv.WF env) (hΓ : OnCtx Γ (env.IsType U)) (h1 : env.IsDefEqU U Γ e₁ e₂) (h2 : env.IsDefEqU U Γ e₂ e₃) : env.IsDefEqU U Γ e₁ e₃ := h1.imp fun _ h1 => let ⟨_, h2⟩ := h2; h1.trans_l henv hΓ h2 +set_option warn.sorry false in variable! (henv : VEnv.WF env) (hΓ : OnCtx Γ' (env.IsType U)) in theorem IsDefEqU.weakN_iff (W : Ctx.LiftN n k Γ Γ') : env.IsDefEqU U Γ' (e1.liftN n k) (e2.liftN n k) ↔ env.IsDefEqU U Γ e1 e2 := by diff --git a/Lean4Lean/Verify/Environment.lean b/Lean4Lean/Verify/Environment.lean index 85ec879c..2bfe3ab5 100644 --- a/Lean4Lean/Verify/Environment.lean +++ b/Lean4Lean/Verify/Environment.lean @@ -111,6 +111,7 @@ theorem addOpaque.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) (v : Op exact .opaque (ci' := ci') ⟨⟨htr, hname⟩, hvalue.mono hto⟩ (by rwa [← old.map_wf.find?'_eq_find?]) (hci.mono hto) hadd old +set_option warn.sorry false in /- Tier V (L4L-19B): upstream's v4.33 proof of this statement was vacuous — it derived `False` from a successful `checkEqType` run via `TrEnv'.no_inductInfo`, which is refutable on this fork (the inductive @@ -205,6 +206,7 @@ theorem addMutual.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) · obtain ⟨v, -, h⟩ := this.forall_exists_r ci hc; exact h.2.1 · obtain ⟨v, -, h⟩ := hbody.forall_exists_r ci hc; exact h.2 +set_option warn.sorry false in /-- Successful checked addition preserves well-formedness and extends every safety-indexed abstract environment. The only declaration form still outstanding is inductives, which need a constructive `AddInduct` model. -/ diff --git a/Lean4Lean/Verify/Environment/Boundaries.lean b/Lean4Lean/Verify/Environment/Boundaries.lean index 5b800d2a..0cbaeb93 100644 --- a/Lean4Lean/Verify/Environment/Boundaries.lean +++ b/Lean4Lean/Verify/Environment/Boundaries.lean @@ -27,6 +27,7 @@ structure PrimitiveResult (checked : VEnv) (v : DefinitionVal) (allow : Bool) : venv.addConst v.name ci'.toVConstant = some env' → (env'.addDefEq ci'.toDefEq).HasPrimitives +set_option warn.sorry false in /-- Verification boundary for Lean4Lean's syntactic primitive-definition recognizer. -/ theorem checkPrimitiveDef.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) (v : DefinitionVal) : diff --git a/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean b/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean index e6f5fbf6..1f30c808 100644 --- a/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean +++ b/Lean4Lean/Verify/Environment/CandidateIdentityReplay.lean @@ -64,7 +64,7 @@ structure CandidateLocalContextRun namespace CandidateLocalContextRun -def empty (context : AddInductive.Context) +theorem empty (context : AddInductive.Context) (h : context.lctx = ({} : LocalContext)) : CandidateLocalContextRun context where wf := by rw [h]; exact LocalContext.WF.nil @@ -85,7 +85,7 @@ theorem fresh (run : CandidateLocalContextRun context) : exact NameGenerator.not_reserves_self (by simpa [AddInductive.Context.freshFVarId] using reserved) -def push (run : CandidateLocalContextRun context) +theorem push (run : CandidateLocalContextRun context) (name : Name) (binderInfo : BinderInfo) (type : Expr) : CandidateLocalContextRun (context.pushLocalDecl name binderInfo type) where @@ -309,7 +309,7 @@ private theorem candidateReduceRecursorFVarApp_none (TypeChecker.Methods.withFuel 9999) context.toTypeChecker state = .ok (context.env, state) by rfl] - simp only [Except.bind] + simp only [] rw [hquot] have hfn : (.app (.fvar fnId) (.fvar argId) : Expr).getAppFn = .fvar fnId := by rfl @@ -328,15 +328,13 @@ private theorem candidateWhnfCoreFVarAppFVar_refl .ok (.app (.fvar fnId) (.fvar argId), ({} : TypeChecker.State)) := by unfold TypeChecker.Inner.whnfCore' - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, Pure.pure] rw [show (get : TypeChecker.RecM TypeChecker.State) (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (({} : TypeChecker.State), ({} : TypeChecker.State)) by rfl] - simp only [Except.bind, Std.HashMap.getElem?_empty] - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp only [Std.HashMap.getElem?_empty] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind] have hfn : (.app (.fvar fnId) (.fvar argId) : Expr).getAppFn = .fvar fnId := by rfl have hargs : (.app (.fvar fnId) (.fvar argId) : Expr).getAppRevArgs = @@ -411,18 +409,16 @@ private theorem candidateWhnfLoopFVarAppFVar_refl (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (context.env, ({} : TypeChecker.State)) by rfl] - simp only [Except.bind] + simp only [] rw [candidateWhnfCoreFVarAppFVar_refl context fnId argId hquot hnotlet] - simp only [Except.bind] + simp only [] rw [candidateReduceNativeFVarAppFVar_none context fnId argId ({} : TypeChecker.State)] - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, Pure.pure] rw [candidateReduceNatFVarAppFVar_none context fnId argId ({} : TypeChecker.State)] - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind] rw [candidateUnfoldDefinitionFVarAppFVar_none context fnId argId ({} : TypeChecker.State)] rfl @@ -451,21 +447,19 @@ theorem candidateWhnfFVarAppFVar_refl context.toTypeChecker ({} : TypeChecker.State)) = .ok (.app (.fvar fnId) (.fvar argId)) unfold TypeChecker.Inner.whnf' - simp only [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp only [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, Pure.pure] rw [show (get : TypeChecker.RecM TypeChecker.State) (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (({} : TypeChecker.State), ({} : TypeChecker.State)) by rfl] - simp only [Except.bind, Std.HashMap.getElem?_empty] - simp only [readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, StateT.bind, Except.bind, Bind.bind, + simp only [Std.HashMap.getElem?_empty] + simp only [readThe, MonadReaderOf.read, ReaderT.bind, StateT.bind, Except.bind, Bind.bind, ReaderT.pure, StateT.pure, Except.pure, Pure.pure] rw [show (liftM read : TypeChecker.RecM TypeChecker.Context) (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (context.toTypeChecker, ({} : TypeChecker.State)) by rfl] - simp only [Except.bind] + simp only [] rw [show context.toTypeChecker.eagerReduce = false by rfl] simp only [Bool.false_eq_true, ↓reduceIte] rw [show context.toTypeChecker.fuel.whnf = 100000 by @@ -500,7 +494,7 @@ private theorem candidateReduceRecursorConstFVarFVar_none (TypeChecker.Methods.withFuel 9999) context.toTypeChecker state = .ok (context.env, state) by rfl] - simp only [Except.bind] + simp only [] rw [hquot] have hfn : (.app (.app (.const constName levels) (.fvar arg1)) @@ -523,15 +517,13 @@ private theorem candidateWhnfCoreConstFVarFVar_refl .ok (.app (.app (.const constName levels) (.fvar arg1)) (.fvar arg2), ({} : TypeChecker.State)) := by unfold TypeChecker.Inner.whnfCore' - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, Pure.pure] rw [show (get : TypeChecker.RecM TypeChecker.State) (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (({} : TypeChecker.State), ({} : TypeChecker.State)) by rfl] - simp only [Except.bind, Std.HashMap.getElem?_empty] - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp only [Std.HashMap.getElem?_empty] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind] have hfn : (.app (.app (.const constName levels) (.fvar arg1)) (.fvar arg2) : Expr).getAppFn = .const constName levels := by @@ -575,7 +567,7 @@ private theorem candidateUnfoldDefinitionCoreConst_none (TypeChecker.Methods.withFuel 9999) context.toTypeChecker state = .ok (context.env, state) by rfl] - simp only [Except.bind] + simp only [] unfold TypeChecker.Inner.isDelta rw [show (Expr.const constName levels).getAppFn = .const constName levels by rfl] @@ -605,8 +597,7 @@ private theorem candidateUnfoldDefinitionConstFVarFVar_none simp only [if_true, ReaderT.bind, StateT.bind, Except.bind, Bind.bind] rw [candidateUnfoldDefinitionCoreConst_none context constName levels state info hfind] - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [ReaderT.pure, StateT.pure, Except.pure, Pure.pure] private theorem candidateWhnfLoopConstFVarFVar_refl (context : AddInductive.Context) (constName : Name) @@ -633,17 +624,15 @@ private theorem candidateWhnfLoopConstFVarFVar_refl (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (context.env, ({} : TypeChecker.State)) by rfl] - simp only [Except.bind] + simp only [] rw [candidateWhnfCoreConstFVarFVar_refl context constName levels arg1 arg2 info hquot hfind] - simp only [Except.bind] + simp only [] rw [candidateReduceNativeConstFVarFVar_none context constName levels arg1 arg2 ({} : TypeChecker.State)] - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, Pure.pure] rw [hreduceNat] - simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [ReaderT.bind, StateT.bind, Except.bind, Bind.bind] rw [candidateUnfoldDefinitionConstFVarFVar_none context constName levels arg1 arg2 ({} : TypeChecker.State) info hfind] rfl @@ -681,21 +670,19 @@ theorem candidateWhnfConstFVarFVar_refl .ok (.app (.app (.const constName levels) (.fvar arg1)) (.fvar arg2)) unfold TypeChecker.Inner.whnf' - simp only [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp only [ReaderT.bind, StateT.bind, Except.bind, Bind.bind, Pure.pure] rw [show (get : TypeChecker.RecM TypeChecker.State) (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (({} : TypeChecker.State), ({} : TypeChecker.State)) by rfl] - simp only [Except.bind, Std.HashMap.getElem?_empty] - simp only [readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, StateT.bind, Except.bind, Bind.bind, + simp only [Std.HashMap.getElem?_empty] + simp only [readThe, MonadReaderOf.read, ReaderT.bind, StateT.bind, Except.bind, Bind.bind, ReaderT.pure, StateT.pure, Except.pure, Pure.pure] rw [show (liftM read : TypeChecker.RecM TypeChecker.Context) (TypeChecker.Methods.withFuel 9999) context.toTypeChecker ({} : TypeChecker.State) = .ok (context.toTypeChecker, ({} : TypeChecker.State)) by rfl] - simp only [Except.bind] + simp only [] rw [show context.toTypeChecker.eagerReduce = false by rfl] simp only [Bool.false_eq_true, ↓reduceIte] rw [show context.toTypeChecker.fuel.whnf = 100000 by diff --git a/Lean4Lean/Verify/Environment/ConstructorValidation.lean b/Lean4Lean/Verify/Environment/ConstructorValidation.lean index 0f3ca3bf..467ce916 100644 --- a/Lean4Lean/Verify/Environment/ConstructorValidation.lean +++ b/Lean4Lean/Verify/Environment/ConstructorValidation.lean @@ -727,10 +727,10 @@ def build : (positivityTrace : ConstructorPositivityTrace stats ctor argIdx context source fuel) → Except Exception (ConstructorPositivityAlignmentTrace positivityTrace) - | .absent context source result fuel whnfStep occurs => do + | .absent context source _ fuel whnfStep occurs => do let sourceCheck ← checkConstructorAlignedExpr context source pure <| .absent sourceCheck - | .forallE context source fuel name domain body binderInfo whnfStep occurs + | .forallE context source fuel _ domain _ _ _ occurs domainFree tailTrace => do let sourceCheck ← checkConstructorAlignedExpr context source let domainCheck ← checkConstructorAlignedExpr context domain @@ -749,7 +749,7 @@ def build : | _ => throw <| .other "consumed positivity domain did not check as a type" - | .target context source result fuel targetIdx whnfStep occurs terminal + | .target context source _ fuel _ _ occurs terminal valid => do let sourceCheck ← checkConstructorAlignedExpr context source pure <| .target sourceCheck @@ -791,8 +791,8 @@ def build : argIdx context source) → Except Exception (ConstructorPositivityModeAlignmentTrace positivityTrace) - | .skipped unsafeEq => pure <| .skipped - | .safe unsafeEq positivityTrace => do + | .skipped _ => pure <| .skipped + | .safe _ positivityTrace => do let alignment ← ConstructorPositivityAlignmentTrace.build positivityTrace pure <| .safe alignment @@ -885,8 +885,8 @@ def build : (view : Expr) → Except Exception (ConstructorViewAlignmentTrace validationTrace view) | .parameter context parameterFuel parameterArgIdx parameterName domain - parameterBody parameterBinderInfo param parameterType parameterAt - parameterTypeRun validationDefEq tailTrace, + parameterBody parameterBinderInfo param parameterType _ + _ _ tailTrace, .forallE viewName viewDomain viewBody viewBinderInfo => do let domainCheck ← checkConstructorAlignedExpr context domain let viewDomainCheck ← checkConstructorAlignedExpr context viewDomain @@ -907,7 +907,7 @@ def build : | .parameter .., _ => throw <| .other "candidate and validation constructor telescopes differ" | .ordinary context ordinaryFuel ordinaryArgIdx name domain body binderInfo - sortResult noParameter ensureType universeTrace positivityTrace tailTrace, + _ _ _ _ positivityTrace tailTrace, .forallE viewName viewDomain viewBody viewBinderInfo => do let domainCheck ← checkConstructorAlignedExpr context domain let viewDomainCheck ← checkConstructorAlignedExpr context viewDomain @@ -1024,7 +1024,7 @@ def build : (ConstructorCandidateAlignmentTrace stats isUnsafe familyIdx context validationTrace candidates) | .nil seen, .nil => pure <| .nil seen - | .cons seen head tail fresh closed rootCheck typeTrace tailTrace, + | .cons seen head tail _ _ _ typeTrace tailTrace, .cons candidate candidates => do let rootScope ← checkConstructorAlignedExpr context.withEmptyLocalContext head.type @@ -1698,7 +1698,7 @@ theorem ConstructorTypeValidationTrace.universeLoop_of_semantics sortResult.sortLevel! = true := by simpa only [ConstructorUniverseTrace.semantic] using semantic.1 rw [valid] - simp only [Pure.pure] + simp only [] exact ih semantic.2 | terminal context source fuel argIdx terminal valid => cases source <;> try rfl @@ -1809,7 +1809,7 @@ theorem ConstructorTypeValidationTrace.universeSemantics_of_loop cases success | true => rw [valid] at success - simp only [Pure.pure] at success + simp only [] at success exact ⟨valid, ih success⟩ | terminal => rfl @@ -2665,7 +2665,7 @@ theorem ConstructorPreFamilyRecursiveTrace.forallE_build_eq rw [domainCheck.check_eq, ensureType.observe_eq, consumedCheck.check_eq] simp only [Bind.bind, Except.bind] rw [annotations.observe_eq] - simp only [Bind.bind, Except.bind] + simp only [] rw [dif_pos fresh, tailRun] rfl @@ -3280,7 +3280,7 @@ private theorem drop_eq_cons_of_getElem?_eq_some cases index with | zero => simp at atIndex - simpa [atIndex] + simp [atIndex] | succ index => simp at atIndex ⊢ simpa [Nat.add_assoc, Nat.add_comm 1] using ih atIndex @@ -3368,7 +3368,7 @@ theorem afterParameters rw [sizeEq] at argIdxEq subst argIdx have dropEq : stats.params.toList.drop stats.params.size = [] := by - simpa using List.drop_length stats.params.toList + simp rw [dropEq] at instantiation have viewEq : (.forallE name domain body binderInfo) = rest := Except.ok.inj (by @@ -3394,7 +3394,7 @@ theorem afterParameters rw [sizeEq] at argIdxEq subst argIdx have dropEq : stats.params.toList.drop stats.params.size = [] := by - simpa using List.drop_length stats.params.toList + simp rw [dropEq] at instantiation have viewEq : (.forallE name domain body binderInfo) = rest := Except.ok.inj (by @@ -3412,7 +3412,7 @@ theorem afterParameters by_cases argIdxEq : argIdx = stats.params.size · subst argIdx have dropEq : stats.params.toList.drop stats.params.size = [] := by - simpa using List.drop_length stats.params.toList + simp rw [dropEq] at instantiation have viewEq : source = rest := Except.ok.inj (by @@ -3537,7 +3537,7 @@ theorem afterParameters rw [sizeEq] at argIdxEq subst argIdx have dropEq : stats.params.toList.drop stats.params.size = [] := by - simpa using List.drop_length stats.params.toList + simp rw [dropEq] at instantiation injection instantiation with restEq subst rest @@ -3566,7 +3566,7 @@ theorem afterParameters by_cases argIdxEq : argIdx = stats.params.size · subst argIdx have dropEq : stats.params.toList.drop stats.params.size = [] := by - simpa using List.drop_length stats.params.toList + simp rw [dropEq] at instantiation have viewEq : view = rest := Except.ok.inj instantiation subst rest @@ -3997,10 +3997,9 @@ private theorem abstract1_instantiate_self (expression.abstract1 id depth).instantiate1' (.fvar id) depth = expression := by induction expression generalizing depth <;> - simp_all [Closed, Expr.abstract1, Expr.instantiate1', beq_iff_eq] <;> - split <;> - simp_all [Expr.instantiate1', Expr.liftLooseBVars'] <;> - omega + simp_all [Closed, Expr.abstract1, Expr.instantiate1', beq_iff_eq] + split <;> + simp_all [Expr.instantiate1', Expr.liftLooseBVars'] private theorem abstract_instantiate_self (expression : Expr) (id : FVarId) (closed : Closed expression) : @@ -5039,7 +5038,7 @@ theorem FVarsIn.consumeTypeAnnotations (scope : FVarsIn predicate source) : FVarsIn predicate (AddInductive.consumeTypeAnnotations source) := by fun_induction AddInductive.consumeTypeAnnotations source <;> - simp_all [AddInductive.consumeTypeAnnotations, FVarsIn] + simp_all [FVarsIn] theorem instantiateFamilyParameters_unique (sourceUnique : TrExprS.IsUnique source) @@ -5712,11 +5711,11 @@ theorem ConstructorPreFamilyIndexSpineSemanticRun.baseSpine_lift sort after removing a verified free-variable context extension. -/ theorem ensureTypeRun_baseType {env typeEnv : VEnv} {Us : List Name} - {base actual view : VLCtx} {source result : Expr} + {base actual view : VLCtx} {source : Expr} {source' actual' : VExpr} {fieldLevel : VLevel} {n : Lift} (henv : VEnv.WF env) (typeEnvOrdered : VEnv.Ordered typeEnv) (addType : env ≤ typeEnv) - (baseWF : VLCtx.WF env Us.length base) + (_baseWF : VLCtx.WF env Us.length base) (viewDefEq : VLCtx.IsDefEq env Us.length actual view) (viewUnique : TrExprS.IsUniqueCtx actual view) (viewLift : VLCtx.FVLift' base view 0 n 0) @@ -5765,7 +5764,7 @@ theorem ensureTypeRun_baseType_mono (actualType : typeEnv.HasType Us.length actual.toCtx actual' (.sort fieldLevel)) : typeEnv.HasType Us.length base.toCtx source' (.sort fieldLevel) := by - exact ensureTypeRun_baseType (result := source) typeEnvWF + exact ensureTypeRun_baseType typeEnvWF typeEnvWF.ordered VEnv.LE.rfl (baseWF.mono addType) (viewDefEq.mono addType) viewUnique viewLift sourceUnique sourceClosed sourceFVars sourceTr (actualTr.mono addType) @@ -5802,7 +5801,7 @@ theorem ensureTypeRun_commonType have fullEq : fullTarget = baseTarget.lift' fullLift := fullTr.unique sourceUnique (baseTr.weakFV' typeEnvWF.ordered fullExtension fullWF) - have baseType := ensureTypeRun_baseType (result := source) + have baseType := ensureTypeRun_baseType henv typeEnvWF.ordered addType baseWF viewDefEq viewUnique viewExtension sourceUnique sourceClosed sourceFVars baseTr actualTr actualType @@ -6565,8 +6564,8 @@ theorem AnalyzerPostContextState.push (typeEnvWF : VEnv.WF typeEnv) {source : Expr} {analyzer postRaw postView postConsumed : VExpr} {rawLevel : VLevel} {fv : FVarId} {postDeps : List FVarId} - (sourceUnique : TrExprS.IsUnique source) - (sourceClosed : Closed source) + (_sourceUnique : TrExprS.IsUnique source) + (_sourceClosed : Closed source) (analyzerTr : TrExprS typeEnv Us full source analyzer) (postViewTr : TrExprS typeEnv Us postActual source postView) (postRawType : typeEnv.HasType Us.length postActual.toCtx postRaw @@ -6693,7 +6692,7 @@ theorem ordinaryField_baseTypes env.HasType Us.length base.toCtx source' (.sort fieldLevel) ∧ fieldLevel ≈ rawLevel ∧ (resultLevel = .zero ∨ fieldLevel ≤ resultLevel) := by - have baseField := ensureTypeRun_baseType (result := source) henv + have baseField := ensureTypeRun_baseType henv typeEnvWF.ordered addType baseWF viewDefEq viewUnique viewLift sourceUnique sourceClosed sourceFVars sourceTr actualTr actualType have postViewType : typeEnv.HasType Us.length postActual.toCtx postView' @@ -6725,7 +6724,7 @@ theorem ordinaryField_baseTypes theorem ordinaryConsumed_defeq {env typeEnv : VEnv} {Us : List Name} - {actual postActual : VLCtx} {source rawSource rawConsumed sourceConsumed : Expr} + {actual postActual : VLCtx} {source _rawSource _rawConsumed _sourceConsumed : Expr} {actualSource' actualConsumed' postRaw' postView' postConsumed' : VExpr} (typeEnvWF : VEnv.WF typeEnv) (addType : env ≤ typeEnv) (actualWF : VLCtx.WF env Us.length actual) @@ -6799,7 +6798,10 @@ end ConstructorValidation namespace ConstructorValidation -open AddInductive TypeChecker VEnv +open AddInductive TypeChecker +-- `VEnv` here resolves to these two namespaces; `_root_.Lean4Lean.VEnv` is +-- shadowed by the enclosing namespace, so name both explicitly. +open _root_.Lean4Lean.ConstructorValidation.VEnv _root_.Lean4Lean.TypeChecker.VEnv /-- Every full-context free variable not deliberately omitted by D3 is still present in the family-free common context. -/ @@ -6901,10 +6903,8 @@ theorem terminal_exactAnalyzer {stats : AddInductive.InductiveStats} {familyIdx : Nat} {familyIndices : Expr} {context : AddInductive.Context} {contextRun : AddInductive.ConstructorContextRun env Us context} - {source : Expr} {argIdx : Nat} {removed : List FVarId} - {recursiveStarted : Bool} + {source : Expr} {valid : AddInductive.isValidIndAppIdx stats source familyIdx = true} - {independent : AddInductive.constructorIndependentOf source removed = true} {spineTrace : AddInductive.ConstructorPreFamilyIndexSpineTrace context familyIndices (source.getAppArgs.toList.drop stats.params.size)} {expected' : VExpr} @@ -7345,7 +7345,7 @@ theorem constructorFields_exactAnalyzer (consumeTypeAnnotations domain)).ngen = (d2Context.pushLocalDecl name₂ binderInfo₂ (consumeTypeAnnotations rawDomain)).ngen := by - simpa only [AddInductive.Context.pushLocalDecl, ngenEq] + simp only [AddInductive.Context.pushLocalDecl, ngenEq] have nextIndexLength : (VExpr.liftTelN 1 commonIndices 0).length = stats.nindices[familyIdx]! := by @@ -7385,7 +7385,7 @@ theorem constructorFields_exactAnalyzer List.append_assoc, VLCtx.toCtx, List.length_cons, VExpr.liftN_liftN, Nat.add_comm] using tailSpine | terminal sourceRun₂ viewRun₂ => - cases d2Alignment <;> simp_all [Expr.isForall] + cases d2Alignment; simp_all [Expr.isForall] | @recursive context recursiveArgIdx removed recursiveStarted name domain body binderInfo noParameter isRecursive independent fieldTrace fresh tailTrace contextRun recursiveRun tail ih => @@ -7636,7 +7636,7 @@ theorem constructorFields_exactAnalyzer List.append_assoc, VLCtx.toCtx, List.length_cons, VExpr.liftN_liftN, Nat.add_comm] using tailSpine | terminal sourceRun₂ viewRun₂ => - cases d2Alignment <;> simp_all [Expr.isForall] + cases d2Alignment; simp_all [Expr.isForall] | @terminal context source terminalArgIdx removed recursiveStarted valid independent spineTrace contextRun expected spine => have shape := isValidIndAppIdx_shape valid @@ -7652,9 +7652,7 @@ theorem constructorFields_exactAnalyzer unfold ConstructorFieldsRunResult refine ⟨trivial, ?_⟩ simpa using terminal_exactAnalyzer - (argIdx := terminalArgIdx) (removed := removed) - (recursiveStarted := recursiveStarted) (valid := valid) - (independent := independent) (resultTarget := resultTarget) + (valid := valid) (resultTarget := resultTarget) spine henv typeEnvWF addType d3State familyCommonTr familyFullTr familyUnique indexLength familyHead sourceUnique sourceClosed @@ -7679,7 +7677,7 @@ theorem stagedIndexCount_eq constructorContext env Us candidate source) (normalization : NormalizationCandidateSemanticRun env Us candidate source) (generation : GenerationChecked source) - (analysis : normalization.root.normalization.generation? = + (_analysis : normalization.root.normalization.generation? = some generation) (shape : normalization.generationShape = true) : (input.postFamilyInput.universeInput.staged.family.validation.stats diff --git a/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean b/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean index 43cafde0..e7fab338 100644 --- a/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean +++ b/Lean4Lean/Verify/Environment/ConstructorValidityReplay.lean @@ -255,7 +255,7 @@ theorem cvmFamilyCandidateBuild : constructorValidityMatrixContext] using produced exact exactProduced.singleton_build -def cvmFamilyIdentityEvidence : +theorem cvmFamilyIdentityEvidence : TypeChecker.CandidateExprIdentityReplay.Evidence cvmFamilyIdentityReplay cvmCandidate.families.singleton.familyType.type.trace := @@ -824,39 +824,39 @@ def cvmCtorFunctionArgContext : AddInductive.Context := cvmCtorDirectContext.pushLocalDecl `y .default cvmCtorFunctionDomain.bindingDomain! -def cvmCtorRootLocalRun : +theorem cvmCtorRootLocalRun : TypeChecker.CandidateLocalContextRun cvmConstructorContext := .empty _ rfl -def cvmCtorAlphaLocalRun : +theorem cvmCtorAlphaLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorAlphaContext := cvmCtorRootLocalRun.push `α .implicit cvmCtorAlphaDomain -def cvmCtorPLocalRun : +theorem cvmCtorPLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorPContext := cvmCtorAlphaLocalRun.push `P .implicit cvmCtorPDomain -def cvmCtorXLocalRun : +theorem cvmCtorXLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorXContext := cvmCtorPLocalRun.push `x .default cvmCtorXDomain -def cvmCtorProofLocalRun : +theorem cvmCtorProofLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorProofContext := cvmCtorXLocalRun.push `proof .default cvmCtorProofDomain -def cvmCtorDirectLocalRun : +theorem cvmCtorDirectLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorDirectContext := cvmCtorProofLocalRun.push `direct .default cvmCtorDirectDomain -def cvmCtorFunctionLocalRun : +theorem cvmCtorFunctionLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorFunctionContext := cvmCtorDirectLocalRun.push `function .default cvmCtorFunctionDomain -def cvmCtorLaterLocalRun : +theorem cvmCtorLaterLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorLaterContext := cvmCtorFunctionLocalRun.push `later .default cvmCtorLaterDomain -def cvmCtorLaterProofLocalRun : +theorem cvmCtorLaterProofLocalRun : TypeChecker.CandidateLocalContextRun cvmCtorLaterProofContext := cvmCtorLaterLocalRun.push `laterProof .default cvmCtorLaterProofDomain @@ -1336,7 +1336,7 @@ def cvmCtorIdentityReplay : constructorValidityMatrixKernelCtor.type := cvmCtorIdentityShape.replay -def cvmCtorIdentityEvidence : +theorem cvmCtorIdentityEvidence : TypeChecker.CandidateExprIdentityReplay.Evidence cvmCtorIdentityReplay cvmCandidate.families.singleton.constructors.singleton.type.trace := @@ -1545,7 +1545,7 @@ theorem prbFamilyCandidateBuild : propRecursiveBoundaryContext] using produced exact exactProduced.singleton_build -def prbFamilyIdentityEvidence : +theorem prbFamilyIdentityEvidence : TypeChecker.CandidateExprIdentityReplay.Evidence prbFamilyIdentityReplay prbCandidate.families.singleton.familyType.type.trace := @@ -2341,7 +2341,7 @@ def prbCtorIdentityReplay : propRecursiveBoundaryKernelCtor.type := prbCtorIdentityShape.replay -def prbCtorIdentityEvidence : +theorem prbCtorIdentityEvidence : TypeChecker.CandidateExprIdentityReplay.Evidence prbCtorIdentityReplay prbCandidate.families.singleton.constructors.singleton.type.trace := @@ -2497,8 +2497,7 @@ theorem prbFamilyTerminalContext_eq : omega | forallE domainCandidate bodyCandidate source_eq consumed_eq domainIdentity bodyIdentity => - simp only [AddInductive.CandidateExprTrace.spineLength, - AddInductive.CandidateExprTrace.terminalContext] + simp only [AddInductive.CandidateExprTrace.terminalContext] cases bodyIdentity with | terminal result_eq => simp only [AddInductive.CandidateExprTrace.spineLength] at spineLength @@ -2532,12 +2531,12 @@ theorem prbConstructorValidationContext_eq : { prbValidationFamilyContext with env := prbConstructorContext.env } := by rw [prbConstructorValidationContext, prbFamilyTerminalContext_eq] -def prbValidationAlphaLocalRun : +theorem prbValidationAlphaLocalRun : TypeChecker.CandidateLocalContextRun prbValidationAlphaContext := (TypeChecker.CandidateLocalContextRun.empty prbFamilyContext rfl).push `α .default (.sort (.succ (.param `u))) -def prbValidationFamilyLocalRun : +theorem prbValidationFamilyLocalRun : TypeChecker.CandidateLocalContextRun prbValidationFamilyContext := prbValidationAlphaLocalRun.push prbValidationAName .default prbFamilyContext.freshExpr @@ -2545,7 +2544,7 @@ def prbValidationFamilyLocalRun : def prbValidationRootContext : AddInductive.Context := { prbValidationFamilyContext with env := prbConstructorContext.env } -def prbValidationRootLocalRun : +theorem prbValidationRootLocalRun : TypeChecker.CandidateLocalContextRun prbValidationRootContext where wf := prbValidationFamilyLocalRun.wf reserves := prbValidationFamilyLocalRun.reserves @@ -2727,27 +2726,20 @@ theorem prbValidationAfterParam_shape : theorem prbValidationAfterA_shape : prbValidationAfterParam.bindingBody!.instantiate1 prbValidationAExpr = prbValidationAfterA := by - simp [prbValidationAfterParam, prbValidationAfterA, - prbValidationNextDomain, prbValidationTerminal, - prbValidationFamilyApp, prbValidationAExpr, - prbValidationRootContext, prbValidationFamilyContext, - prbValidationAlphaContext, prbFamilyContext, + simp [prbValidationAfterParam, prbValidationAfterA, prbValidationNextDomain, + prbValidationFamilyApp, prbValidationAExpr, prbValidationRootContext, + prbValidationFamilyContext, prbValidationAlphaContext, prbFamilyContext, propRecursiveBoundaryContext, AddInductive.Context.freshExpr, - TypeChecker.candidateLiftLooseBVarsFVar, - Expr.bindingBody!, - Expr.instantiate1_eq, Expr.instantiate1'] + TypeChecker.candidateLiftLooseBVarsFVar, Expr.bindingBody!, Expr.instantiate1_eq, + Expr.instantiate1'] theorem prbValidationTerminal_shape : prbValidationAfterA.bindingBody!.instantiate1 prbValidationAContext.freshExpr = prbValidationTerminal := by - simp [prbValidationAfterA, prbValidationTerminal, - prbValidationFamilyApp, prbValidationAExpr, - prbValidationRootContext, prbValidationAContext, - prbValidationFamilyContext, prbValidationAlphaContext, - prbFamilyContext, propRecursiveBoundaryContext, - AddInductive.Context.freshExpr, - TypeChecker.candidateInstantiateFVar, - Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1'] + simp [prbValidationAfterA, prbValidationTerminal, prbValidationFamilyApp, prbValidationAExpr, + prbValidationRootContext, prbValidationAContext, prbValidationFamilyContext, + prbValidationAlphaContext, prbFamilyContext, propRecursiveBoundaryContext, + AddInductive.Context.freshExpr, Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1'] theorem prbValidationTarget_shape : prbValidationNextDomain.bindingBody!.instantiate1 @@ -2756,15 +2748,15 @@ theorem prbValidationTarget_shape : prbValidationFamilyApp, Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1'] -def prbValidationALocalRun : +theorem prbValidationALocalRun : TypeChecker.CandidateLocalContextRun prbValidationAContext := prbValidationRootLocalRun.push `a .default prbValidationAlpha -def prbValidationNextLocalRun : +theorem prbValidationNextLocalRun : TypeChecker.CandidateLocalContextRun prbValidationNextContext := prbValidationALocalRun.push `next .default prbValidationNextDomain -def prbValidationBLocalRun : +theorem prbValidationBLocalRun : TypeChecker.CandidateLocalContextRun prbValidationBContext := prbValidationALocalRun.push `b .default prbValidationAlpha @@ -2883,18 +2875,12 @@ theorem prbValidationFamilyGet : Level.getUndefParam, Level.forEach, Level.hasParam_eq, Level.hasParam'] rfl - simp [ - propRecursiveBoundaryKernelType, propRecursiveBoundaryInfo, - ConstantInfo.levelParams, ConstantInfo.isUnsafe, - ConstantInfo.instantiateTypeLevelParams, ConstantInfo.toConstantVal, - ConstantVal.instantiateTypeLevelParams, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', - Syntax.structEq_eq, - Level.substParams', hsafety, hlparams, + simp [propRecursiveBoundaryKernelType, propRecursiveBoundaryInfo, ConstantInfo.levelParams, + ConstantInfo.isUnsafe, ConstantInfo.instantiateTypeLevelParams, ConstantInfo.toConstantVal, + ConstantVal.instantiateTypeLevelParams, Expr.instantiateLevelParams_eq, hsafety, hlparams, hlevel, Bind.bind, Except.bind, Pure.pure, Except.pure] - simp [Expr.instantiateLevelParamsCore', Level.substParams', - propRecursiveBoundaryKernelType, propRecursiveBoundaryInfo, - ConstantInfo.type, ConstantInfo.toConstantVal] + simp [Expr.instantiateLevelParamsCore', Level.substParams', ConstantInfo.type, + ConstantInfo.toConstantVal] def prbValidationFamilyTail (alpha : Expr) : Expr := .forallE prbValidationAName alpha (.sort .zero) .default @@ -2982,10 +2968,8 @@ theorem prbInferAppCoreOf (stateArg.inferTypeC.insert (.app fn arg) (body.instantiate1 arg)) }) := by unfold TypeChecker.Inner.inferType' - simp [hclosed, hcache, hfn, harg, heager, - prbEnsureForallExact, prbSelfDefEq, - Expr.instantiate1_eq, Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + simp [hclosed, hcache, hfn, harg, heager, prbSelfDefEq, Expr.instantiate1_eq, Bind.bind, + ReaderT.bind, StateT.bind, Except.bind] theorem prbInferTypeForallCore (fuel : Nat) (context : TypeChecker.Context) @@ -3011,8 +2995,7 @@ theorem prbInferTypeForallCore open private mkLevelIMaxCore mkLevelMaxCore from Lean.Level in @[simp] theorem prbMkLevelIMaxSuccParamZero : mkLevelIMax' (.succ (.param `u)) .zero = .zero := by - simp [mkLevelIMax', mkLevelIMaxCore, mkLevelMax', mkLevelMaxCore, - Level.isNeverZero, Level.isZero] + simp [mkLevelIMax', mkLevelIMaxCore, Level.isNeverZero, Level.isZero] def prbValidationConstState (state : TypeChecker.State) : TypeChecker.State := prbReplayInsert state @@ -3112,12 +3095,8 @@ theorem prbValidationNextInternalFresh : simp only [List.not_mem_nil, or_false] at membership rcases membership with rfl | rfl | rfl all_goals - simp [LocalDecl.fvarId, prbValidationNextInternalBId, - prbValidationNextAlphaState, prbReplayInsert, - prbValidationAlpha, prbValidationAId, prbValidationIndexId, - prbValidationAlphaId, prbValidationRootContext, - prbValidationFamilyContext, prbValidationAlphaContext, - prbFamilyContext, propRecursiveBoundaryContext, + simp [LocalDecl.fvarId, prbValidationNextInternalBId, prbValidationNextAlphaState, + prbReplayInsert, prbValidationAlpha, prbFamilyContext, propRecursiveBoundaryContext, AddInductive.Context.freshExpr, AddInductive.Context.freshFVarId] at equal all_goals injection equal all_goals simp [NameGenerator.next] at * @@ -3366,8 +3345,7 @@ theorem prbValidationNextBodyInferExists : (.fvar prbValidationNextInternalBId) (.fvar prbValidationAlphaId) (.sort .zero) prbValidationAName .default - (by simp [prbValidationFamilyApp, prbValidationFirstApp, - Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [prbValidationFirstApp, Expr.hasLooseBVars, Expr.looseBVarRange']) appMiss firstRun argRun (by rfl) refine ⟨prbValidationCachedFamilyAppState prbValidationNextBodyState prbValidationAlphaId prbValidationNextInternalBId, ?_⟩ @@ -3428,8 +3406,7 @@ theorem prbValidationNextDomainCheckValid : ).instantiateRev #[Expr.fvar prbValidationNextInternalBId] = prbValidationFamilyApp (.fvar prbValidationNextInternalBId) by - simp [prbValidationFamilyApp, Expr.instantiateRev_eq, - Expr.instantiate_eq, Expr.instantiate1_eq, Expr.instantiate1']] + simp [prbValidationFamilyApp, Expr.instantiateRev_eq, Expr.instantiate_eq, Expr.instantiate1']] simp only [Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [show TypeChecker.Inner.inferType (prbValidationFamilyApp @@ -3450,8 +3427,7 @@ theorem prbValidationNextDomainCheckValid : prbValidationAContext.toTypeChecker ({} : TypeChecker.State) bodyFinalState `b prbValidationAlpha (prbValidationFamilyApp (.bvar 0)) (.sort .zero) .default - (by simp [prbValidationNextDomain, prbValidationFamilyApp, - Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [prbValidationFamilyApp, Expr.hasLooseBVars, Expr.looseBVarRange']) Std.HashMap.getElem?_empty (by simpa [prbValidationNextDomain] using forallRun) unfold AddInductive.CandidateCheckTypeStep.Valid @@ -3504,8 +3480,7 @@ theorem prbValidationInferFirstAppCore (.fvar alphaId) (.sort (.succ (.param `u))) (.forallE prbValidationAName (.bvar 0) (.sort .zero) .default) `α .default - (by simp [prbValidationFirstApp, Expr.hasLooseBVars, - Expr.looseBVarRange']) happ + (by simp [Expr.hasLooseBVars, Expr.looseBVarRange']) happ (by simpa [prbValidationAName, propRecursiveBoundaryKernelType, propRecursiveBoundaryInfo, ConstantInfo.type, ConstantInfo.toConstantVal, Expr.bindingBody!, @@ -3548,16 +3523,13 @@ theorem prbValidationFamilyAppCheckValid have argMiss : (prbValidationFirstAppState initial alphaId).inferTypeC[ (.fvar argId : Expr)]? = none := by have initialMiss : initial.inferTypeC[(.fvar argId : Expr)]? = none := by - simpa [initial] using - (Std.HashMap.getElem?_empty (k := (.fvar argId : Expr)) - (v := Expr)) + simp [initial] have idBeq : ((.fvar alphaId : Expr) == .fvar argId) = false := by change Expr.eqv (.fvar alphaId) (.fvar argId) = false rw [Expr.eqv_eq] simp [Expr.eqv', hne] - simp [prbValidationFirstAppState, prbValidationAlphaState, - prbValidationConstState, prbReplayInsert, - prbValidationFirstApp, idBeq, initialMiss] + simp [prbValidationFirstAppState, prbValidationAlphaState, prbValidationConstState, + prbReplayInsert, prbValidationFirstApp, idBeq] intro hmem have hsome := Std.HashMap.mem_iff_isSome_getElem?.mp hmem simp [initialMiss] at hsome @@ -3575,9 +3547,8 @@ theorem prbValidationFamilyAppCheckValid (prbValidationArgumentState initial alphaId argId) (prbValidationFirstApp (.fvar alphaId)) (.fvar argId) (.fvar alphaId) (.sort .zero) prbValidationAName .default - (by simp [prbValidationFamilyApp, prbValidationFirstApp, - Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [initial, prbValidationFamilyApp]) firstRun argRun (by rfl) + (by simp [prbValidationFirstApp, Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [initial]) firstRun argRun (by rfl) unfold AddInductive.CandidateCheckTypeStep.Valid change TypeChecker.M.run context.env context.safety context.lctx context.lparams context.fuel @@ -4331,8 +4302,7 @@ def prbStagedPostFamilyInput : rw [prbStagedStats_eq, prbStatsParams_eq] at noParameter simp at noParameter | terminal context source fuel argIdx terminal valid => - simp [propRecursiveBoundaryKernelType, propRecursiveBoundaryKernelCtor, - propRecursiveBoundaryMkInfo, ConstantInfo.type, + simp [propRecursiveBoundaryKernelCtor, propRecursiveBoundaryMkInfo, ConstantInfo.type, ConstantInfo.toConstantVal, Expr.isForall] at terminal def prbPreFamilyContextReplay : AddInductive.Context := @@ -4560,9 +4530,7 @@ theorem prbPreFamilyInferSortZeroCoreReplay .ok (.sort (.succ .zero), prbReplayInsert state (.sort .zero) (.sort (.succ .zero))) := by unfold TypeChecker.Inner.inferType' - simp [Expr.hasLooseBVars, Expr.looseBVarRange', miss, - prbPreFamilyCheckLevelZeroReplay, - prbReplayInsert, Bind.bind, ReaderT.bind, + simp [Expr.hasLooseBVars, Expr.looseBVarRange', miss, prbReplayInsert, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] theorem prbPreFamilyIndexTelescopeCheckValidReplay @@ -4652,9 +4620,7 @@ theorem prbPreFamilyIndexTelescopeCheckValidReplay prbValidationAName prbValidationAlpha (.sort .zero) (.sort (mkLevelIMax' (.succ (.param `u)) (.succ .zero))) .default - (by simp [prbPreFamilyIndexTelescopeReplay, - prbValidationAlpha_shape, Expr.hasLooseBVars, - Expr.looseBVarRange']) Std.HashMap.getElem?_empty forallRun + (by simp [prbValidationAlpha_shape, Expr.hasLooseBVars, Expr.looseBVarRange']) Std.HashMap.getElem?_empty forallRun unfold AddInductive.CandidateCheckTypeStep.Valid change TypeChecker.M.run context.env context.safety context.lctx context.lparams context.fuel @@ -4822,12 +4788,9 @@ theorem prbPreFamilyFamilyAppValidReplay (arg : Expr) #[.const propRecursiveBoundaryKernelType.name [.param `u]] arg = false := by simpa [prbStagedIndConstsReplay_eq] using argFree - simp +decide [AddInductive.isValidIndAppIdx, - prbStagedParamsReplay_eq, prbStagedNindicesReplay_eq, - prbStagedIndConstsReplay_eq, - prbValidationFamilyAppGetAppFnReplay, - prbValidationFamilyAppGetAppArgsReplay, - prbExprBneSelfReplay, parameterSelf, argFree', Expr.constName!] + simp +decide [AddInductive.isValidIndAppIdx, prbStagedParamsReplay_eq, prbStagedNindicesReplay_eq, + prbStagedIndConstsReplay_eq, prbValidationFamilyAppGetAppFnReplay, + prbValidationFamilyAppGetAppArgsReplay, prbExprBneSelfReplay, argFree'] theorem prbPreFamilyTargetValidReplay : AddInductive.isValidIndAppIdx @@ -4835,8 +4798,7 @@ theorem prbPreFamilyTargetValidReplay : prbValidationTarget 0 = true := by apply prbPreFamilyFamilyAppValidReplay rw [prbStagedIndConstsReplay_eq] - simp [AddInductive.hasIndOcc, prbValidationTarget, - prbValidationFamilyApp, prbValidationBExpr_shape] + simp [AddInductive.hasIndOcc, prbValidationBExpr_shape] theorem prbPreFamilyTerminalValidReplay : AddInductive.isValidIndAppIdx @@ -4844,8 +4806,7 @@ theorem prbPreFamilyTerminalValidReplay : prbValidationTerminal 0 = true := by apply prbPreFamilyFamilyAppValidReplay rw [prbStagedIndConstsReplay_eq] - simp [AddInductive.hasIndOcc, prbValidationTerminal, - prbValidationFamilyApp, prbValidationAExpr_shape] + simp [AddInductive.hasIndOcc, prbValidationAExpr_shape] theorem prbPreFamilyAIdNeRemovedReplay : prbValidationAId ≠ prbPreFamilyAContextReplay.freshFVarId := by @@ -5327,8 +5288,7 @@ theorem prbSafetyRunDirect : (prbValidationFamilyApp prbValidationAExpr) .default) 2 [] false 998 = .ok recursiveViewTrace := by - simp only [prbValidationAfterA, - AddInductive.ConstructorPreFamilyViewTrace.build] + simp only [AddInductive.ConstructorPreFamilyViewTrace.build] split · rename_i parameter parameterAt rw [noParameterTwo] at parameterAt @@ -5429,7 +5389,7 @@ theorem prbSafetyRunDirect : rootAlphaConsumed.check_eq] simp only [Bind.bind, Except.bind] rw [rootAlphaAnnotations.observe_eq] - simp only [Bind.bind, Except.bind] + simp only [] rw [dif_pos prbPreFamilyRootFreshReplay] have ordinaryTailRun' : AddInductive.ConstructorPreFamilyViewTrace.build @@ -5655,8 +5615,7 @@ theorem cvmFamilyTerminalContextTest_eq : omega | forallE domainCandidate bodyCandidate source_eq consumed_eq domainIdentity bodyIdentity => - simp only [AddInductive.CandidateExprTrace.spineLength, - AddInductive.CandidateExprTrace.terminalContext] + simp only [AddInductive.CandidateExprTrace.terminalContext] cases bodyIdentity with | terminal result_eq => simp only [AddInductive.CandidateExprTrace.spineLength] at spineLength @@ -5698,16 +5657,16 @@ theorem cvmConstructorValidationContextTest_root : rw [cvmConstructorValidationContextTest_eq] rfl -def cvmValidationAlphaLocalRunTest : +theorem cvmValidationAlphaLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationAlphaContextTest := (TypeChecker.CandidateLocalContextRun.empty cvmFamilyContext rfl).push `α .default (.sort (.succ (.param `u))) -def cvmValidationFamilyLocalRunTest : +theorem cvmValidationFamilyLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationFamilyContextTest := cvmValidationAlphaLocalRunTest.push `P .default cvmValidationPDomainTest -def cvmValidationRootLocalRunTest : +theorem cvmValidationRootLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationRootContextTest where wf := cvmValidationFamilyLocalRunTest.wf reserves := cvmValidationFamilyLocalRunTest.reserves @@ -5933,7 +5892,7 @@ theorem cvmEnsureTypeOfInferOnlyTest simpa [AddInductive.Context.toTypeChecker] using run] rfl -def cvmValidationXLocalRunTest : +theorem cvmValidationXLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationXContextTest := cvmValidationRootLocalRunTest.push `x .default (AddInductive.consumeTypeAnnotations cvmCtorXDomain) @@ -6004,14 +5963,11 @@ theorem cvmValidationProofInferOnlyTest : #[.fvar cvmValidationXIdTest] := by rfl unfold TypeChecker.Inner.inferType' - simp [Expr.hasLooseBVars, Expr.looseBVarRange', - TypeChecker.Inner.inferApp, TypeChecker.Inner.inferApp.loop, - appFn, appArgs, pRun, cvmValidationPDomainTest, - cvmValidationProofFinalStateTest, - cvmValidationProofPStateTest, cvmInferOnlyInsertTest, - cvmCtorProofDomainValidationShapeTest, Expr.instantiateRev_eq, - Expr.instantiate_eq, Expr.instantiate1_eq, Expr.instantiate1', - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.hasLooseBVars, Expr.looseBVarRange', TypeChecker.Inner.inferApp, + TypeChecker.Inner.inferApp.loop, appFn, appArgs, pRun, cvmValidationPDomainTest, + cvmValidationProofFinalStateTest, cvmValidationProofPStateTest, cvmInferOnlyInsertTest, + cvmCtorProofDomainValidationShapeTest, Expr.instantiateRev_eq, Expr.instantiate_eq, + Expr.instantiate1', Bind.bind, ReaderT.bind, StateT.bind, Except.bind] theorem cvmValidationProofEnsureTest : AddInductive.ConstructorEnsureTypeStep.Valid @@ -6069,15 +6025,12 @@ theorem cvmCtorAfterProofForallTest : exact cvmTerminalLparams_eq unfold cvmDeclaredInfo AddInductive.singletonDeclaredInfo rw [terminalLparams] - simp [constructorValidityMatrixKernelType, - constructorValidityMatrixInfo, ConstantInfo.levelParams, - ConstantInfo.instantiateTypeLevelParams, ConstantInfo.toConstantVal, - ConstantVal.instantiateTypeLevelParams, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', - Level.substParams', Bind.bind, Except.bind, Pure.pure, Except.pure] - simp [Expr.instantiateLevelParamsCore', Level.substParams', - constructorValidityMatrixKernelType, constructorValidityMatrixInfo, - ConstantInfo.type, ConstantInfo.toConstantVal] + simp [constructorValidityMatrixKernelType, constructorValidityMatrixInfo, + ConstantInfo.levelParams, ConstantInfo.instantiateTypeLevelParams, ConstantInfo.toConstantVal, + ConstantVal.instantiateTypeLevelParams, Expr.instantiateLevelParams_eq, Bind.bind, Except.bind, + Pure.pure, Except.pure] + simp [Expr.instantiateLevelParamsCore', Level.substParams', ConstantInfo.type, + ConstantInfo.toConstantVal] theorem cvmKernelFamilyTypeShapeTest : constructorValidityMatrixKernelType.type = @@ -6336,12 +6289,12 @@ theorem cvmCtorAfterDirectForallTest : cvmCtorAfterDirect.bindingBody! .default := by simp_cvm_ctor_expr -def cvmValidationProofLocalRunTest : +theorem cvmValidationProofLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationProofContextTest := cvmValidationXLocalRunTest.push `proof .default (AddInductive.consumeTypeAnnotations cvmCtorProofDomain) -def cvmValidationDirectLocalRunTest : +theorem cvmValidationDirectLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationDirectContextTest := cvmValidationProofLocalRunTest.push `direct .default (AddInductive.consumeTypeAnnotations cvmCtorDirectDomain) @@ -6512,8 +6465,7 @@ theorem cvmValidationFunctionInferOnlyTest : ((.const constructorValidityMatrixKernelType.name [.param `u] : Expr).app (.fvar cvmValidationAlphaIdTest)).app (.fvar cvmValidationPIdTest) by - simp [Expr.instantiateRev_eq, Expr.instantiate_eq, - Expr.instantiate1_eq, Expr.instantiate1']] + simp [Expr.instantiateRev_eq, Expr.instantiate_eq, Expr.instantiate1']] simp only [Bind.bind, ReaderT.bind, StateT.bind, Except.bind] have bodyRunExplicit : TypeChecker.Inner.inferType' (((.const constructorValidityMatrixKernelType.name @@ -6602,7 +6554,7 @@ theorem cvmCtorAfterFunctionForallTest : cvmCtorAfterFunction.bindingBody! .default := by simp_cvm_ctor_expr -def cvmValidationFunctionLocalRunTest : +theorem cvmValidationFunctionLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationFunctionContextTest := cvmValidationDirectLocalRunTest.push `function .default (AddInductive.consumeTypeAnnotations cvmCtorFunctionDomain) @@ -6731,13 +6683,10 @@ theorem cvmInferTypePredicateApplicationOnlyTest rfl unfold TypeChecker.Inner.inferType' rw [closed] - simp [TypeChecker.Inner.inferApp, TypeChecker.Inner.inferApp.loop, - appFn, appArgs, predicateRun, cvmValidationPDomainTest, - cvmValidationPredicateApplicationTest, - cvmValidationPredicateApplicationStateTest, - cvmValidationPredicateStateTest, cvmInferOnlyInsertTest, - Expr.instantiateRev_eq, Expr.instantiate_eq, - Expr.instantiate1_eq, Expr.instantiate1', + simp [TypeChecker.Inner.inferApp, TypeChecker.Inner.inferApp.loop, appFn, appArgs, predicateRun, + cvmValidationPDomainTest, cvmValidationPredicateApplicationTest, + cvmValidationPredicateApplicationStateTest, cvmValidationPredicateStateTest, + cvmInferOnlyInsertTest, Expr.instantiateRev_eq, Expr.instantiate_eq, Expr.instantiate1', Bind.bind, ReaderT.bind, StateT.bind, Except.bind] theorem cvmValidationPFindInProofTest : @@ -6767,7 +6716,7 @@ theorem cvmValidationPFindInFunctionTest : (AddInductive.consumeTypeAnnotations cvmCtorFunctionDomain) cvmValidationPFindInDirectTest -def cvmValidationLaterLocalRunTest : +theorem cvmValidationLaterLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationLaterContextTest := cvmValidationFunctionLocalRunTest.push `later .default (AddInductive.consumeTypeAnnotations cvmCtorLaterDomain) @@ -6787,24 +6736,18 @@ def cvmValidationLaterIdTest : FVarId := theorem cvmCtorLaterProofDomainValidationShapeTest : cvmCtorLaterProofDomain = cvmValidationPredicateApplicationTest cvmValidationPIdTest (.fvar cvmValidationLaterIdTest) := by - simp [cvmCtorLaterProofDomain, cvmCtorAfterLater, - cvmCtorAfterFunction, cvmCtorAfterDirect, cvmCtorAfterProof, - cvmCtorAfterX, cvmCtorAfterP, cvmCtorAfterAlpha, - cvmValidationPredicateApplicationTest, cvmValidationPIdTest, - cvmValidationLaterIdTest, cvmValidationFunctionContextTest, - cvmValidationDirectContextTest, cvmValidationProofContextTest, - cvmValidationXContextTest, cvmValidationRootContextTest, - cvmValidationFamilyContextTest, cvmValidationAlphaContextTest, - cvmValidationPDomainTest, cvmFamilyContext, - cvmCtorFunctionContext, cvmCtorDirectContext, - cvmCtorProofContext, cvmCtorXContext, cvmCtorPContext, - cvmCtorAlphaContext, cvmConstructorContext, - constructorValidityMatrixContext, constructorValidityMatrixKernelCtor, - constructorValidityMatrixMkInfo, ConstantInfo.type, - ConstantInfo.toConstantVal, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshExpr, AddInductive.Context.freshFVarId, - AddInductive.consumeTypeAnnotations, Expr.bindingDomain!, - Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1'] + simp [cvmCtorLaterProofDomain, cvmCtorAfterLater, cvmCtorAfterFunction, cvmCtorAfterDirect, + cvmCtorAfterProof, cvmCtorAfterX, cvmCtorAfterP, cvmCtorAfterAlpha, + cvmValidationPredicateApplicationTest, cvmValidationPIdTest, cvmValidationLaterIdTest, + cvmValidationFunctionContextTest, cvmValidationDirectContextTest, cvmValidationProofContextTest, + cvmValidationXContextTest, cvmValidationRootContextTest, cvmValidationFamilyContextTest, + cvmValidationAlphaContextTest, cvmValidationPDomainTest, cvmFamilyContext, + cvmCtorFunctionContext, cvmCtorDirectContext, cvmCtorProofContext, cvmCtorXContext, + cvmCtorPContext, cvmCtorAlphaContext, cvmConstructorContext, constructorValidityMatrixContext, + constructorValidityMatrixKernelCtor, constructorValidityMatrixMkInfo, ConstantInfo.type, + ConstantInfo.toConstantVal, AddInductive.Context.pushLocalDecl, AddInductive.Context.freshExpr, + AddInductive.Context.freshFVarId, Expr.bindingDomain!, Expr.bindingBody!, Expr.instantiate1_eq, + Expr.instantiate1'] theorem cvmValidationLaterDepthTest : cvmValidationLaterContextTest.fuel.recDepth = 10000 := by @@ -6955,11 +6898,8 @@ theorem cvmUniverseSemanticsTest : have universeSemantic : universeTrace.semantic = true := by unfold AddInductive.ConstructorUniverseTrace.semantic rw [cvmStatsResultLevelTest] - simp [Expr.sortLevel!, - AddInductive.ConstructorUniverseTrace.semantic, - AddInductive.constructorUniverseSemanticGe, - AddInductive.levelStructGe, - AddInductive.levelStructEq] + simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe, + AddInductive.levelStructGe, AddInductive.levelStructEq] rw [universeSemantic] simp only [Bool.true_and] let sourceEq := cvmFirstFieldSourceTest.trans @@ -6987,10 +6927,8 @@ theorem cvmUniverseSemanticsTest : have universeSemantic : universeTrace.semantic = true := by unfold AddInductive.ConstructorUniverseTrace.semantic rw [cvmStatsResultLevelTest] - simp [Expr.sortLevel!, - AddInductive.constructorUniverseSemanticGe, - AddInductive.levelStructGe, - AddInductive.levelStructEq] + simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe, + AddInductive.levelStructGe] rw [universeSemantic] simp only [Bool.true_and] let sourceEq := cvmSecondFieldSourceTest.trans @@ -7122,8 +7060,7 @@ theorem cvmUniverseSemanticsTest : rw [cvmStatsResultLevelTest] simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe, - AddInductive.levelStructGe, - AddInductive.levelStructEq] + AddInductive.levelStructGe] rw [universeSemantic] simp only [Bool.true_and] let sourceEq := cvmSixthFieldSourceTest.trans @@ -7378,16 +7315,13 @@ theorem cvmValidationFamilyGetTest : Level.getUndefParam, Level.forEach, Level.hasParam_eq, Level.hasParam'] rfl - simp [constructorValidityMatrixKernelType, - constructorValidityMatrixInfo, ConstantInfo.levelParams, - ConstantInfo.isUnsafe, ConstantInfo.instantiateTypeLevelParams, + simp [constructorValidityMatrixKernelType, constructorValidityMatrixInfo, + ConstantInfo.levelParams, ConstantInfo.isUnsafe, ConstantInfo.instantiateTypeLevelParams, ConstantInfo.toConstantVal, ConstantVal.instantiateTypeLevelParams, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', - Syntax.structEq_eq, Level.substParams', safety, lparams, - levelCheck, Bind.bind, Except.bind, Pure.pure, Except.pure] - simp [Expr.instantiateLevelParamsCore', Level.substParams', - constructorValidityMatrixKernelType, constructorValidityMatrixInfo, - ConstantInfo.type, ConstantInfo.toConstantVal] + Expr.instantiateLevelParams_eq, safety, lparams, levelCheck, Bind.bind, Except.bind, Pure.pure, + Except.pure] + simp [Expr.instantiateLevelParamsCore', Level.substParams', ConstantInfo.type, + ConstantInfo.toConstantVal] def cvmValidationFamilyConstStateTest (state : TypeChecker.State) : TypeChecker.State := @@ -7504,7 +7438,7 @@ theorem cvmValidationFamilyApplicationCheckTest (.sort (.succ (.param `u))) .default) `α .default (by simp [Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [initial, cvmValidationFirstAppFullTest]) + (by simp [initial]) (by simpa [cvmKernelFamilyTypeShapeTest] using familyRun) alphaRun (by rfl) have firstRun' : TypeChecker.Inner.inferType' @@ -7547,10 +7481,8 @@ theorem cvmValidationFamilyApplicationCheckTest (.forallE cvmValidationIndexNameTest (.fvar alphaId) (.sort .zero) .default) (.sort (.succ (.param `u))) `P .default - (by simp [cvmValidationFamilyApplicationTest, - cvmValidationFirstAppFullTest, Expr.hasLooseBVars, - Expr.looseBVarRange']) - (by simp [initial, cvmValidationFamilyApplicationTest]) + (by simp [cvmValidationFirstAppFullTest, Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [initial]) firstRun' predicateRun (by rfl) unfold AddInductive.CandidateCheckTypeStep.Valid change TypeChecker.M.run context.env context.safety context.lctx @@ -7648,9 +7580,8 @@ theorem cvmValidationPredicateApplicationCheckTest (.fvar predicateId) (.fvar argumentId) (.fvar cvmValidationAlphaIdTest) (.sort .zero) cvmValidationIndexNameTest .default - (by simp [cvmValidationPredicateApplicationTest, - Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [initial, cvmValidationPredicateApplicationTest]) + (by simp [Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [initial]) predicateRun argumentRun (by rfl) unfold AddInductive.CandidateCheckTypeStep.Valid change TypeChecker.M.run context.env context.safety context.lctx @@ -7774,7 +7705,7 @@ theorem cvmValidationDirectCheckTest : cvmValidationAlphaFindInProofTest cvmValidationPFindInProofTest (by rfl) (by rfl) (by rfl) (by rfl) -def cvmValidationLaterProofLocalRunTest : +theorem cvmValidationLaterProofLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationLaterProofContextTest := cvmValidationLaterLocalRunTest.push `laterProof .default (AddInductive.consumeTypeAnnotations cvmCtorLaterProofDomain) @@ -7882,8 +7813,7 @@ theorem cvmValidationInferFirstAppAlphaCachedCoreTest (.sort .zero) .default) (.sort (.succ (.param `u))) .default) `α .default - (by simp [cvmValidationFirstAppFullTest, - Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [Expr.hasLooseBVars, Expr.looseBVarRange']) firstMiss (by simpa [cvmKernelFamilyTypeShapeTest] using familyRun) alphaRun (by rfl) @@ -7945,9 +7875,7 @@ theorem cvmValidationFamilyApplicationAlphaCachedCoreTest (.forallE cvmValidationIndexNameTest (.fvar alphaId) (.sort .zero) .default) (.sort (.succ (.param `u))) `P .default - (by simp [cvmValidationFamilyApplicationTest, - cvmValidationFirstAppFullTest, - Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [cvmValidationFirstAppFullTest, Expr.hasLooseBVars, Expr.looseBVarRange']) applicationMiss firstRun predicateRun (by rfl) simpa [cvmValidationFamilyApplicationTest, cvmValidationFirstAppFullTest, @@ -8001,12 +7929,8 @@ theorem cvmValidationFunctionFullInternalFreshTest : rcases membership with rfl | rfl | rfl | rfl | rfl all_goals simp [LocalDecl.fvarId, cvmValidationFunctionFullInternalIdTest, - cvmValidationFunctionFullAlphaStateTest, prbReplayInsert, - cvmValidationXIdTest, cvmValidationPIdTest, - cvmValidationAlphaIdTest, cvmValidationRootContextTest, - cvmValidationFamilyContextTest, cvmValidationAlphaContextTest, - cvmFamilyContext, constructorValidityMatrixContext, - AddInductive.Context.freshExpr, AddInductive.Context.freshFVarId] + cvmValidationFunctionFullAlphaStateTest, prbReplayInsert, cvmValidationAlphaIdTest, + cvmFamilyContext, constructorValidityMatrixContext, AddInductive.Context.freshFVarId] at equal all_goals injection equal all_goals simp [NameGenerator.next] at * @@ -8066,12 +7990,9 @@ theorem cvmValidationFunctionCheckTest : · simp [cvmValidationFunctionFullInternalStateTest, cvmValidationFunctionFullAlphaStateTest, cvmValidationFirstAppFullTest, prbReplayInsert] - · simp [cvmValidationFamilyCachedFirstAppStateTest, - cvmValidationFamilyConstStateTest, - cvmValidationFunctionFullInternalStateTest, - cvmValidationFunctionFullAlphaStateTest, - cvmValidationFirstAppFullTest, prbReplayInsert, - cvmValidationAlphaNePTest] + · simp [cvmValidationFamilyCachedFirstAppStateTest, cvmValidationFamilyConstStateTest, + cvmValidationFunctionFullInternalStateTest, cvmValidationFunctionFullAlphaStateTest, + cvmValidationFirstAppFullTest, prbReplayInsert] · simp [cvmValidationFunctionFullInternalStateTest, cvmValidationFunctionFullAlphaStateTest, cvmValidationFamilyApplicationTest, prbReplayInsert] @@ -8126,8 +8047,7 @@ theorem cvmValidationFunctionCheckTest : ((.const constructorValidityMatrixKernelType.name [.param `u] : Expr).app (.fvar cvmValidationAlphaIdTest)).app (.fvar cvmValidationPIdTest) by - simp [Expr.instantiateRev_eq, Expr.instantiate_eq, - Expr.instantiate1_eq, Expr.instantiate1']] + simp [Expr.instantiateRev_eq, Expr.instantiate_eq, Expr.instantiate1']] simp only [Bind.bind, ReaderT.bind, StateT.bind, Except.bind] have bodyRunExplicit : TypeChecker.Inner.inferType' (((.const constructorValidityMatrixKernelType.name @@ -8252,7 +8172,7 @@ def cvmValidationProofCheckedTest : cvmCtorProofDomain := cvmCheckedOfValidTest _ _ _ (by rw [cvmCtorProofDomainValidationShapeTest] - simp [cvmValidationPredicateApplicationTest, FVarsIn, Level.hasMVar'] + simp [FVarsIn] constructor · change (cvmValidationXContextTest.lctx.find? cvmValidationPIdTest).isSome = true @@ -8309,7 +8229,7 @@ def cvmValidationLaterProofCheckedTest : cvmCtorLaterProofDomain := cvmCheckedOfValidTest _ _ _ (by rw [cvmCtorLaterProofDomainValidationShapeTest] - simp [cvmValidationPredicateApplicationTest, FVarsIn, Level.hasMVar'] + simp [cvmValidationPredicateApplicationTest, FVarsIn] constructor · change (cvmValidationLaterContextTest.lctx.find? cvmValidationPIdTest).isSome = true @@ -8346,8 +8266,7 @@ def cvmValidationTerminalCheckedTest : AddInductive.consumeTypeAnnotations cvmCtorProofDomain = cvmCtorProofDomain := by rw [cvmCtorProofDomainValidationShapeTest] - simp [cvmValidationPredicateApplicationTest, - AddInductive.consumeTypeAnnotations] + simp [AddInductive.consumeTypeAnnotations] @[simp] theorem cvmValidationConsumeDirectTest : AddInductive.consumeTypeAnnotations cvmCtorDirectDomain = @@ -8382,8 +8301,7 @@ theorem cvmCtorPDomainValidationShapeTest : cvmCtorPDomain = .forallE cvmCtorPDomain.bindingName! (.fvar cvmValidationAlphaIdTest) (.sort .zero) .default := by simp_cvm_ctor_expr - simp [cvmValidationAlphaIdTest, cvmFamilyContext, - cvmConstructorContext, constructorValidityMatrixContext, + simp [cvmValidationAlphaIdTest, cvmFamilyContext, constructorValidityMatrixContext, AddInductive.Context.freshFVarId] theorem cvmValidationCtorPDomainCheckTest : @@ -8512,7 +8430,7 @@ def cvmValidationFunctionPosContextTest : AddInductive.Context := cvmValidationDirectContextTest.pushLocalDecl `y .default (.fvar cvmValidationAlphaIdTest) -def cvmValidationFunctionPosLocalRunTest : +theorem cvmValidationFunctionPosLocalRunTest : TypeChecker.CandidateLocalContextRun cvmValidationFunctionPosContextTest := cvmValidationDirectLocalRunTest.push `y .default (.fvar cvmValidationAlphaIdTest) @@ -8615,8 +8533,7 @@ theorem cvmValidationProofHasNoIndOccTest : cvmCtorProofDomain = false := by rw [cvmStagedIndConstsTest_eq, cvmCtorProofDomainValidationShapeTest] - simp [AddInductive.hasIndOcc, - cvmValidationPredicateApplicationTest] + simp [AddInductive.hasIndOcc] theorem cvmValidationDirectHasIndOccTest : AddInductive.hasIndOcc @@ -9706,7 +9623,7 @@ def cvmPreFamilyFunctionInnerContextTest : AddInductive.Context := cvmPreFamilyAfterDirectContextTest.pushLocalDecl `y .default (.fvar cvmValidationAlphaIdTest) -def cvmAdvanceLocalRunTest +theorem cvmAdvanceLocalRunTest (run : TypeChecker.CandidateLocalContextRun context) : TypeChecker.CandidateLocalContextRun context.advanceFresh where wf := run.wf @@ -9715,41 +9632,41 @@ def cvmAdvanceLocalRunTest exact NameGenerator.Reserves.mono NameGenerator.LE.next (run.reserves decl membership) -def cvmPreFamilyRootLocalRunTest : +theorem cvmPreFamilyRootLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyContextTest := cvmValidationFamilyLocalRunTest -def cvmPreFamilyXLocalRunTest : +theorem cvmPreFamilyXLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyXContextTest := cvmPreFamilyRootLocalRunTest.push `x .default (AddInductive.consumeTypeAnnotations cvmCtorXDomain) -def cvmPreFamilyProofLocalRunTest : +theorem cvmPreFamilyProofLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyProofContextTest := cvmPreFamilyXLocalRunTest.push `proof .default (AddInductive.consumeTypeAnnotations cvmCtorProofDomain) -def cvmPreFamilyAfterDirectLocalRunTest : +theorem cvmPreFamilyAfterDirectLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyAfterDirectContextTest := cvmAdvanceLocalRunTest cvmPreFamilyProofLocalRunTest -def cvmPreFamilyAfterFunctionLocalRunTest : +theorem cvmPreFamilyAfterFunctionLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyAfterFunctionContextTest := cvmAdvanceLocalRunTest cvmPreFamilyAfterDirectLocalRunTest -def cvmPreFamilyLaterLocalRunTest : +theorem cvmPreFamilyLaterLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyLaterContextTest := cvmPreFamilyAfterFunctionLocalRunTest.push `later .default (AddInductive.consumeTypeAnnotations cvmCtorLaterDomain) -def cvmPreFamilyLaterProofLocalRunTest : +theorem cvmPreFamilyLaterProofLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyLaterProofContextTest := cvmPreFamilyLaterLocalRunTest.push `laterProof .default (AddInductive.consumeTypeAnnotations cvmCtorLaterProofDomain) -def cvmPreFamilyFunctionInnerLocalRunTest : +theorem cvmPreFamilyFunctionInnerLocalRunTest : TypeChecker.CandidateLocalContextRun cvmPreFamilyFunctionInnerContextTest := cvmPreFamilyAfterDirectLocalRunTest.push `y .default @@ -10098,7 +10015,7 @@ def cvmPreFamilyPredicateCheckedTest (cvmValidationPredicateApplicationTest cvmValidationPIdTest (.fvar argumentId)) := .ofRun (by - simp [cvmValidationPredicateApplicationTest, FVarsIn, Level.hasMVar'] + simp [cvmValidationPredicateApplicationTest, FVarsIn] constructor · change (context.lctx.find? cvmValidationPIdTest).isSome = true rw [predicateFind] @@ -10517,7 +10434,7 @@ theorem cvmPreFamilyOrdinaryBuildEqTest consumedCheck.check_eq] simp only [Bind.bind, Except.bind] rw [annotations.observe_eq] - simp only [Bind.bind, Except.bind] + simp only [] rw [dif_pos fresh, tailRun] rfl · rename_i recursive diff --git a/Lean4Lean/Verify/Environment/DeepNestedReplay.lean b/Lean4Lean/Verify/Environment/DeepNestedReplay.lean index da669047..7b9e0431 100644 --- a/Lean4Lean/Verify/Environment/DeepNestedReplay.lean +++ b/Lean4Lean/Verify/Environment/DeepNestedReplay.lean @@ -111,7 +111,7 @@ theorem biBoxCheckedWF : biBoxChecked.WF VEnv.empty := by hresult, hindices, hparams] exact .nil -def biBoxGenerationWF : biBoxGeneration.WF VEnv.empty := by +theorem biBoxGenerationWF : biBoxGeneration.WF VEnv.empty := by exact biBoxCheckedWF.identityGeneration .empty def biBoxTypeEnv : VEnv := @@ -145,7 +145,7 @@ theorem biBoxTypeEnvOrdered : biBoxTypeEnv.Ordered := theorem biBoxCtorEnvOrdered : biBoxCtorEnv.Ordered := replayCtorEnv_ordered07 biBoxGenerationWF rfl biBoxTypeEnvOrdered rfl -def biBoxGenerationEnv : +theorem biBoxGenerationEnv : VInductDecl.GenerationEnv biBoxGeneration biBoxCtorEnv := replayGenerationEnv07 biBoxGenerationWF rfl rfl biBoxCtorEnvOrdered diff --git a/Lean4Lean/Verify/Environment/Extension.lean b/Lean4Lean/Verify/Environment/Extension.lean index 1529846d..223d8f5c 100644 --- a/Lean4Lean/Verify/Environment/Extension.lean +++ b/Lean4Lean/Verify/Environment/Extension.lean @@ -244,6 +244,7 @@ def TrMutualHeader (bs : DefinitionSafety) (venv : VEnv) (env : Environment) ci.toVConstant.WF venv ∧ env.find? v.name = none ∧ Environment.primitives.contains v.name = false +set_option warn.sorry false in /-- A model of the temporary environment in which a mutual block's bodies are checked: every member has been added as an axiom, so a body may refer to any member of the block (including itself) but cannot delta-unfold it. -/ @@ -298,6 +299,7 @@ theorem VEnvAt.addAxioms {env : Environment} {venv : VEnv} {bs : DefinitionSafet Environment.find?_add_of_ne wf.tr.map_wf _ (hax ▸ hd.2.2.1) (hax ▸ hne) h.2.2.1, h.2.2.2⟩ +set_option warn.sorry false in /-- Add a whole mutual block. The headers were checked in `env`, the bodies in the temporary environment holding the entire block, which is `base` on the model side; `TrEnv'.mutualDef` consumes exactly that split. @@ -394,6 +396,7 @@ theorem addMutualBlock.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) projectionReady {sf} := (readiness sf).1 structureEtaReady {sf} := (readiness sf).2 } +set_option warn.sorry false in theorem addConstCore.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) (ci : ConstantInfo) (ci' : VConstVal) (checkSafety : DefinitionSafety) (visible_le : ∀ safety, safety ≤ ci.safety → safety ≤ checkSafety) @@ -480,6 +483,7 @@ theorem addConst.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) addConstCore.WF wf ci ci' checkSafety visible_le htr hci hn (by simp_all) (fun _ _ _ hadd hp => hp.addConst_of_not_primitive hnonprim hadd) step +set_option warn.sorry false in theorem addDef.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) (v : DefinitionVal) (ci' : VDefVal) (checkSafety : DefinitionSafety) (visible_le : ∀ safety, safety ≤ (ConstantInfo.defnInfo v).safety → safety ≤ checkSafety) @@ -555,6 +559,7 @@ theorem addDef.WF {env : Environment} {ves : VEnvs} (wf : ves.WF env) projectionReady {safety} := (readiness safety).1 structureEtaReady {safety} := (readiness safety).2 } +set_option warn.sorry false in /-- The unsafe branch of `addDefinition`. The constant is added to the environment as an axiom *before* its body is checked, so the body is translated in the extended environment `base` and the whole step is justified by `TrEnv'.mutualDef` with a one-element block. diff --git a/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean b/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean index f963b5e5..fca8d3c9 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecCandidate.lean @@ -869,13 +869,11 @@ theorem indexedVecPreFamilyNatCheckTypeM (lctx : LocalContext) : (indexedVecTypeCheckerContext lctx) ``Nat [] true = .ok (.sort (.succ .zero)) := by unfold Lean4Lean.TypeChecker.Inner.inferConstant - simp [indexedVecTypeCheckerContext, indexedVecKernel_get_nat, - natInfo, ConstantInfo.levelParams, ConstantInfo.isUnsafe, + simp [indexedVecTypeCheckerContext, indexedVecKernel_get_nat, natInfo, ConstantInfo.levelParams, ConstantInfo.instantiateTypeLevelParams, ConstantInfo.toConstantVal, - ConstantVal.instantiateTypeLevelParams, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', - Level.substParams', Bind.bind, Except.bind, - Pure.pure, Except.pure] + ConstantVal.instantiateTypeLevelParams, Expr.instantiateLevelParams_eq, + Expr.instantiateLevelParamsCore', Level.substParams', Bind.bind, Except.bind, Pure.pure, + Except.pure] private def indexedVecPreFamilyNatInferOnlyState : Lean4Lean.TypeChecker.State := @@ -938,9 +936,7 @@ private theorem indexedVecPreFamilyIndexNatCore (lctx : LocalContext) : (indexedVecTypeCheckerContext lctx) ({} : Lean4Lean.TypeChecker.State) = .ok (.sort (.succ .zero), indexedVecInnerNatState) := by - simpa [indexedVecInnerNatState] using - (indexedVecInferTypeNatCore 9998 lctx - ({} : Lean4Lean.TypeChecker.State) Std.HashMap.getElem?_empty) + simp [indexedVecInnerNatState] private theorem indexedVecPreFamilyIndexWithLocalDecl (lctx : LocalContext) diff --git a/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean b/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean index a5b06902..10745878 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecConsReplay.lean @@ -62,12 +62,9 @@ def replayFirstApp (alpha : Expr) : Expr := ((consAlphaExpr : Expr) == consNExpr) = false := by change Expr.eqv consAlphaExpr consNExpr = false rw [Expr.eqv_eq] - simp [Expr.eqv', consAlphaExpr, consNExpr, consAlphaId, consNId, - consAlphaContext, consRootContext, ctorContext, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshExpr, - AddInductive.Context.freshFVarId, - NameGenerator.next, NameGenerator.curr] + simp [Expr.eqv', consAlphaExpr, consNExpr, consAlphaContext, consRootContext, ctorContext, + AddInductive.Context.pushLocalDecl, AddInductive.Context.freshExpr, + AddInductive.Context.freshFVarId, NameGenerator.next, NameGenerator.curr] @[simp] theorem replayAlphaIdBeqNId : ((.fvar consAlphaId : Expr) == .fvar consNId) = false := by @@ -393,9 +390,8 @@ theorem replayInferConsHeadFirstApp (fuel : Nat) : (replayInferFirstAppFVarCore fuel consHeadContext.lctx ({} : TypeChecker.State) consAlphaId (by simp) - (by simp [replayInsert, Expr.eqv_eq]) - (by simp [replayFirstApp, consAlphaExprShape, - Expr.eqv_eq]) + (by simp [replayInsert]) + (by simp [replayFirstApp]) consAlphaFindInHead) theorem replayInferConsHeadN (fuel : Nat) : @@ -408,8 +404,7 @@ theorem replayInferConsHeadN (fuel : Nat) : consHeadFirstAppState consNId (.const ``Nat []) (index := 1) (name := consNName) (bi := .implicit) (kind := .default) - (by simp [consHeadFirstAppState, replayInsert, - replayFirstApp, replayAlphaBeqN]) + (by simp [consHeadFirstAppState, replayInsert, replayFirstApp]) consNFindInHead) theorem replayInferConsTailDomainCore (fuel : Nat) : @@ -424,8 +419,7 @@ theorem replayInferConsTailDomainCore (fuel : Nat) : consAlphaExpr consNExpr (by simp [ctorIndexedVecApp, consAlphaExprShape, consNExprShape, Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [ctorIndexedVecApp, consAlphaExprShape, - consNExprShape, Expr.eqv_eq]) + (by simp [ctorIndexedVecApp, consAlphaExprShape, consNExprShape]) (replayInferConsHeadFirstApp fuel) (replayInferConsHeadN fuel) (by rfl)) theorem replayInferConsTailDomain : @@ -478,8 +472,8 @@ theorem replayInferConsTailFirstApp : (replayInferFirstAppFVarCore 9999 consTailContext.lctx ({} : TypeChecker.State) consAlphaId (by simp) - (by simp [replayInsert, Expr.eqv_eq]) - (by simp [replayFirstApp, Expr.eqv_eq]) + (by simp [replayInsert]) + (by simp [replayFirstApp]) consAlphaFindInTail) theorem replayInferConsTailSucc : @@ -490,12 +484,10 @@ theorem replayInferConsTailSucc : simpa [consTailSuccState, consNExprShape] using (replayInferSuccFVarCore 9999 consTailContext.lctx consTailFirstAppState consNId - (by simp [consTailFirstAppState, replayInsert, - replayFirstApp, Expr.eqv_eq]) + (by simp [consTailFirstAppState, replayInsert, replayFirstApp]) (by simp [consTailFirstAppState, replayInsert, replayFirstApp]) - (by simp [consTailFirstAppState, replayInsert, - replaySuccApp, replayFirstAppBeqSuccApp]) + (by simp [consTailFirstAppState, replayInsert, replaySuccApp]) consNFindInTail) theorem replayInferConsTerminal : @@ -513,8 +505,7 @@ theorem replayInferConsTerminal : consAlphaExpr (replaySuccApp consNExpr) (by simp [ctorIndexedVecApp, replaySuccApp, Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [ctorIndexedVecApp, replaySuccApp, - Expr.eqv_eq, Expr.eqv']) + (by simp [ctorIndexedVecApp, replaySuccApp]) replayInferConsTailFirstApp replayInferConsTailSucc (by rfl)) @@ -591,7 +582,7 @@ def consAfterHeadCheckState : TypeChecker.State := (ctorIndexedVecApp (.fvar consAlphaId) (.fvar consNId)) (replaySuccApp (.fvar consNId)) = false rw [Expr.eqv_eq] - simp [Expr.eqv', ctorIndexedVecApp, replayFirstApp, replaySuccApp] + simp [Expr.eqv', ctorIndexedVecApp, replaySuccApp] @[simp] theorem replayTailDomainBeqTerminal : (ctorIndexedVecApp (.fvar consAlphaId) (.fvar consNId) == @@ -602,7 +593,7 @@ def consAfterHeadCheckState : TypeChecker.State := (ctorIndexedVecApp (.fvar consAlphaId) (replaySuccApp (.fvar consNId))) = false rw [Expr.eqv_eq] - simp [Expr.eqv', ctorIndexedVecApp, replayFirstApp, replaySuccApp] + simp [Expr.eqv', ctorIndexedVecApp, replaySuccApp] @[simp] theorem replayFirstAppBeqTerminal : (replayFirstApp (.fvar consAlphaId) == @@ -669,9 +660,7 @@ theorem consAfterHeadCheckFirstCache : unfold consHeadNState replayInsert rw [Std.HashMap.getElem?_insert] rw [show (consNExpr == replayFirstApp (.fvar consAlphaId)) = false by - simpa [consNExprShape, replayFirstApp] using - (replayFVarBeqApp consNId - (.const ``IndexedVec [.param `u]) (.fvar consAlphaId))] + simp [consNExprShape, replayFirstApp]] simp only [Bool.false_eq_true, if_false] unfold consHeadFirstAppState replayInsert rw [Std.HashMap.getElem?_insert] @@ -700,27 +689,21 @@ theorem consAfterHeadCheckNCache : theorem consAfterHeadCheckSuccMiss : consAfterHeadCheckState.inferTypeC[(.const ``Nat.succ [] : Expr)]? = none := by - simp [consAfterHeadCheckState, consTailDomainFinalState, - consHeadNState, consHeadFirstAppState, replayInsert, - consTailDomain, replayFirstApp, Std.HashMap.getElem?_insert, - Expr.eqv_eq, Expr.eqv'] + simp [consAfterHeadCheckState, consTailDomainFinalState, consHeadNState, consHeadFirstAppState, + replayInsert, consTailDomain, replayFirstApp] theorem consAfterHeadCheckSuccAppMiss : consAfterHeadCheckState.inferTypeC[ replaySuccApp (.fvar consNId)]? = none := by - simp [consAfterHeadCheckState, consTailDomainFinalState, - consHeadNState, consHeadFirstAppState, replayInsert, - consTailDomain, replayFirstApp, replaySuccApp, - Std.HashMap.getElem?_insert, Expr.eqv_eq, Expr.eqv'] + simp [consAfterHeadCheckState, consTailDomainFinalState, consHeadNState, consHeadFirstAppState, + replayInsert, consTailDomain, replayFirstApp, replaySuccApp] theorem consAfterHeadCheckTerminalMiss : consAfterHeadCheckState.inferTypeC[ ctorIndexedVecApp (.fvar consAlphaId) (replaySuccApp (.fvar consNId))]? = none := by - simp [consAfterHeadCheckState, consTailDomainFinalState, - consHeadNState, consHeadFirstAppState, replayInsert, - consTailDomain, ctorIndexedVecApp, replayFirstApp, replaySuccApp, - Std.HashMap.getElem?_insert, Expr.eqv_eq, Expr.eqv'] + simp [consAfterHeadCheckState, consTailDomainFinalState, consHeadNState, consHeadFirstAppState, + replayInsert, consTailDomain, ctorIndexedVecApp, replayFirstApp, replaySuccApp] def consAfterHeadCheckSuccState : TypeChecker.State := replayInsert consAfterHeadCheckState (.const ``Nat.succ []) @@ -766,10 +749,8 @@ theorem replayConsAfterHeadCheckTypeM : (TypeChecker.Methods.withFuel 9999) (tcContext consHeadContext.lctx) ({} : TypeChecker.State)) = _ unfold consAfterHead consTailDomain TypeChecker.Inner.inferType' - simp [Expr.hasLooseBVars, Expr.looseBVarRange', - TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, - TypeChecker.Inner.inferApp, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.hasLooseBVars, Expr.looseBVarRange', TypeChecker.Inner.inferForall, + TypeChecker.Inner.inferForall.loop, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [show TypeChecker.Inner.inferType' (.app (.app (.const ``IndexedVec [.param `u]) (.fvar consAlphaId)) @@ -845,14 +826,10 @@ theorem consAfterNCheckHeadFresh : have h := LocalContext.WF.find?_eq_find?_toList (fv := consAfterNCheckHeadId) consNContextWF rw [h] - simp [consAfterNCheckHeadId, consAfterNHeadDomainState, - replayInsert, consNContext, consAlphaContext, consRootContext, - ctorContext, consAlphaId, consNId, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consAfterNCheckHeadId, consAfterNHeadDomainState, replayInsert, consNContext, + consAlphaContext, consRootContext, ctorContext, consAlphaId, AddInductive.Context.pushLocalDecl, + AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, LocalContext.toList, + LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] intro x hx change some x ∈ (PersistentArray.empty : PersistentArray (Option LocalDecl)).toList' at hx @@ -868,14 +845,10 @@ theorem consAfterNCheckNFind : some (.cdecl 1 consNId consNName (.const ``Nat []) .implicit .default) := by rw [consAfterNCheckLctxWF.find?_eq_find?_toList] - simp [consAfterNCheckLctx, consAfterNCheckHeadId, - consAfterNHeadDomainState, replayInsert, - consNContext, consAlphaContext, consRootContext, ctorContext, - consAlphaId, consNId, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consAfterNCheckLctx, consAfterNCheckHeadId, consAfterNHeadDomainState, replayInsert, + consNContext, consAlphaContext, consRootContext, ctorContext, consAlphaId, consNId, + AddInductive.Context.pushLocalDecl, AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, + LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] theorem consAfterNCheckAlphaCache : consAfterNCheckState.inferTypeC[(.fvar consAlphaId : Expr)]? = @@ -996,30 +969,24 @@ theorem consAfterNCheckTailNCache : theorem consAfterNCheckTailSuccMiss : consAfterNCheckTailState.inferTypeC[ (.const ``Nat.succ [] : Expr)]? = none := by - simp [consAfterNCheckTailState, consAfterNCheckTailDomainState, - consAfterNCheckNState, consAfterNCheckFirstAppState, - consAfterNCheckState, consAfterNHeadDomainState, - replayInsert, ctorIndexedVecApp, replayFirstApp, - Expr.eqv_eq, Expr.eqv'] + simp [consAfterNCheckTailState, consAfterNCheckTailDomainState, consAfterNCheckNState, + consAfterNCheckFirstAppState, consAfterNCheckState, consAfterNHeadDomainState, replayInsert, + ctorIndexedVecApp, replayFirstApp] theorem consAfterNCheckTailSuccAppMiss : consAfterNCheckTailState.inferTypeC[ replaySuccApp (.fvar consNId)]? = none := by - simp [consAfterNCheckTailState, consAfterNCheckTailDomainState, - consAfterNCheckNState, consAfterNCheckFirstAppState, - consAfterNCheckState, consAfterNHeadDomainState, - replayInsert, ctorIndexedVecApp, replayFirstApp, replaySuccApp, - Expr.eqv_eq, Expr.eqv'] + simp [consAfterNCheckTailState, consAfterNCheckTailDomainState, consAfterNCheckNState, + consAfterNCheckFirstAppState, consAfterNCheckState, consAfterNHeadDomainState, replayInsert, + ctorIndexedVecApp, replayFirstApp, replaySuccApp] theorem consAfterNCheckTailTerminalMiss : consAfterNCheckTailState.inferTypeC[ ctorIndexedVecApp (.fvar consAlphaId) (replaySuccApp (.fvar consNId))]? = none := by - simp [consAfterNCheckTailState, consAfterNCheckTailDomainState, - consAfterNCheckNState, consAfterNCheckFirstAppState, - consAfterNCheckState, consAfterNHeadDomainState, - replayInsert, ctorIndexedVecApp, replayFirstApp, replaySuccApp, - Expr.eqv_eq, Expr.eqv'] + simp [consAfterNCheckTailState, consAfterNCheckTailDomainState, consAfterNCheckNState, + consAfterNCheckFirstAppState, consAfterNCheckState, consAfterNHeadDomainState, replayInsert, + ctorIndexedVecApp, replayFirstApp, replaySuccApp] def consAfterNCheckSuccState : TypeChecker.State := replayInsert consAfterNCheckTailState (.const ``Nat.succ []) @@ -1100,7 +1067,7 @@ theorem replayConsAfterNCheckTypeM : rw [htail] simp only [ensureSortExact] rw [withLocalDeclEq] - simp only [Expr.instantiate1'] + simp only [] have hterminal : TypeChecker.Inner.inferType (((.const ``IndexedVec [.param `u] : Expr).app @@ -1135,11 +1102,8 @@ open private mkLevelIMaxCore mkLevelMaxCore from Lean.Level in @[simp] theorem replayMkLevelIMaxSuccZeroSuccParam : mkLevelIMax' (.succ .zero) (.succ (.param `u)) = .succ (.param `u) := by - simp [mkLevelIMax', mkLevelIMaxCore, mkLevelMax', mkLevelMaxCore, - Level.isNeverZero, Level.isZero, Level.isExplicit, - Level.hasMVar', Level.hasParam', - Level.getOffset, - Level.getOffsetAux, Level.getLevelOffset] + simp [mkLevelIMax', mkLevelIMaxCore, mkLevelMax', mkLevelMaxCore, Level.isNeverZero, Level.isZero, + Level.isExplicit, Level.hasMVar', Level.hasParam', Level.getOffset, Level.getOffsetAux] def consAfterAlphaNatState : TypeChecker.State := replayInsert ({} : TypeChecker.State) (.const ``Nat []) @@ -1170,13 +1134,10 @@ theorem consAfterAlphaCheckNFresh : have h := LocalContext.WF.find?_eq_find?_toList (fv := consAfterAlphaCheckNId) consAlphaContextWF rw [h] - simp [consAfterAlphaCheckNId, consAfterAlphaNatState, replayInsert, - consAlphaContext, consRootContext, ctorContext, - consAlphaId, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consAfterAlphaCheckNId, consAfterAlphaNatState, replayInsert, consAlphaContext, + consRootContext, ctorContext, AddInductive.Context.pushLocalDecl, + AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, LocalContext.toList, + LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] intro x hx change some x ∈ (PersistentArray.empty : PersistentArray (Option LocalDecl)).toList' at hx @@ -1193,14 +1154,10 @@ theorem consAfterAlphaCheckAlphaFind : some (.cdecl 0 consAlphaId consAlphaName (.sort (.succ (.param `u))) .implicit .default) := by rw [consAfterAlphaCheckNLctxWF.find?_eq_find?_toList] - simp [consAfterAlphaCheckNLctx, consAfterAlphaCheckNId, - consAfterAlphaNatState, replayInsert, - consAlphaContext, consRootContext, ctorContext, - consAlphaId, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consAfterAlphaCheckNLctx, consAfterAlphaCheckNId, consAfterAlphaNatState, replayInsert, + consAlphaContext, consRootContext, ctorContext, consAlphaId, AddInductive.Context.pushLocalDecl, + AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, LocalContext.toList, + LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] theorem consAfterAlphaCheckAlphaMiss : consAfterAlphaCheckNState.inferTypeC[ @@ -1240,16 +1197,11 @@ theorem consAfterAlphaCheckHeadFresh : have h := LocalContext.WF.find?_eq_find?_toList (fv := consAfterAlphaCheckHeadId) consAfterAlphaCheckNLctxWF rw [h] - simp [consAfterAlphaCheckHeadId, consAfterAlphaHeadDomainState, - consAfterAlphaCheckNState, consAfterAlphaCheckNId, - consAfterAlphaNatState, replayInsert, - consAfterAlphaCheckNLctx, consAlphaContext, - consRootContext, ctorContext, consAlphaId, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consAfterAlphaCheckHeadId, consAfterAlphaHeadDomainState, consAfterAlphaCheckNState, + consAfterAlphaCheckNId, consAfterAlphaNatState, replayInsert, consAfterAlphaCheckNLctx, + consAlphaContext, consRootContext, ctorContext, consAlphaId, AddInductive.Context.pushLocalDecl, + AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, LocalContext.toList, + LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] intro x hx change some x ∈ (PersistentArray.empty : PersistentArray (Option LocalDecl)).toList' at hx @@ -1267,16 +1219,12 @@ theorem consAfterAlphaCheckNFind : some (.cdecl 1 consAfterAlphaCheckNId consNName (.const ``Nat []) .implicit .default) := by rw [consAfterAlphaCheckHeadLctxWF.find?_eq_find?_toList] - simp [consAfterAlphaCheckHeadLctx, consAfterAlphaCheckHeadId, - consAfterAlphaHeadDomainState, consAfterAlphaCheckNState, - consAfterAlphaCheckNLctx, consAfterAlphaCheckNId, - consAfterAlphaNatState, replayInsert, - consAlphaContext, consRootContext, ctorContext, - consAlphaId, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consAfterAlphaCheckHeadLctx, consAfterAlphaCheckHeadId, consAfterAlphaHeadDomainState, + consAfterAlphaCheckNState, consAfterAlphaCheckNLctx, consAfterAlphaCheckNId, + consAfterAlphaNatState, replayInsert, consAlphaContext, consRootContext, ctorContext, + consAlphaId, AddInductive.Context.pushLocalDecl, AddInductive.Context.freshFVarId, + LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, + NameGenerator.curr] theorem consAfterAlphaCheckAlphaCache : consAfterAlphaCheckHeadState.inferTypeC[ @@ -1304,12 +1252,8 @@ theorem consAfterAlphaCheckAlphaCache : change Expr.eqv (.fvar consAlphaId) (.fvar consAfterAlphaCheckNId) = false rw [Expr.eqv_eq] - simp [Expr.eqv', consAlphaId, consAfterAlphaCheckNId, - consAfterAlphaNatState, replayInsert, - consAlphaContext, consRootContext, ctorContext, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - NameGenerator.next, NameGenerator.curr] + simp [Expr.eqv', consAlphaId, consAfterAlphaCheckNId, consAfterAlphaNatState, replayInsert, + consRootContext, ctorContext, AddInductive.Context.freshFVarId, NameGenerator.curr] theorem consAfterAlphaCheckFamilyMiss : consAfterAlphaCheckHeadState.inferTypeC[ @@ -1394,12 +1338,8 @@ def consAfterAlphaCheckTailState : TypeChecker.State := change Expr.eqv (.fvar consAfterAlphaCheckNId) (.fvar consAlphaId) = false rw [Expr.eqv_eq] - simp [Expr.eqv', consAlphaId, consAfterAlphaCheckNId, - consAfterAlphaNatState, replayInsert, - consAlphaContext, consRootContext, ctorContext, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - NameGenerator.next, NameGenerator.curr] + simp [Expr.eqv', consAlphaId, consAfterAlphaCheckNId, consAfterAlphaNatState, replayInsert, + consRootContext, ctorContext, AddInductive.Context.freshFVarId, NameGenerator.curr] @[simp] theorem replayNatConstBeqSucc : ((.const ``Nat [] : Expr) == .const ``Nat.succ []) = false := by @@ -1421,7 +1361,7 @@ def consAfterAlphaCheckTailState : TypeChecker.State := change Expr.eqv (ctorIndexedVecApp alpha n) (replaySuccApp n) = false rw [Expr.eqv_eq] - simp [Expr.eqv', ctorIndexedVecApp, replayFirstApp, replaySuccApp] + simp [Expr.eqv', ctorIndexedVecApp, replaySuccApp] @[simp] theorem replayIndexedVecAppBeqIndexedVecSucc (alpha : Expr) (id : FVarId) : @@ -1656,7 +1596,7 @@ theorem replayConsAfterAlphaCheckTypeM : rw [htail] simp only [ensureSortExact] rw [withLocalDeclEq] - simp [Expr.instantiate1'] + simp have hterminal : TypeChecker.Inner.inferType (((.const ``IndexedVec [.param `u] : Expr).app @@ -1742,11 +1682,9 @@ theorem consRootCheckAlphaFind : some (.cdecl 0 consRootCheckAlphaId consAlphaName (.sort (.succ (.param `u))) .implicit .default) := by rw [consRootCheckAlphaLctxWF.find?_eq_find?_toList] - simp [consRootCheckAlphaLctx, consRootCheckAlphaId, - consRootContext, ctorContext, nilRootSortState, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consRootCheckAlphaLctx, consRootCheckAlphaId, consRootContext, ctorContext, + nilRootSortState, LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, + NameGenerator.curr] theorem consRootCheckNatMiss : consRootCheckAlphaState.inferTypeC[ @@ -1781,13 +1719,10 @@ theorem consRootCheckNFresh : have h := LocalContext.WF.find?_eq_find?_toList (fv := consRootCheckNId) consRootCheckAlphaLctxWF rw [h] - simp [consRootCheckNId, consRootCheckNatState, - consRootCheckAlphaState, consRootCheckAlphaLctx, - consRootCheckAlphaId, nilRootSortState, replayInsert, - consRootContext, ctorContext, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consRootCheckNId, consRootCheckNatState, consRootCheckAlphaState, consRootCheckAlphaLctx, + consRootCheckAlphaId, nilRootSortState, replayInsert, consRootContext, ctorContext, + LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, + NameGenerator.curr] intro x hx change some x ∈ (PersistentArray.empty : PersistentArray (Option LocalDecl)).toList' at hx @@ -1804,12 +1739,9 @@ theorem consRootCheckAlphaFindInN : some (.cdecl 0 consRootCheckAlphaId consAlphaName (.sort (.succ (.param `u))) .implicit .default) := by rw [consRootCheckNLctxWF.find?_eq_find?_toList] - simp [consRootCheckNLctx, consRootCheckNId, - consRootCheckNatState, consRootCheckAlphaState, - consRootCheckAlphaLctx, consRootCheckAlphaId, - nilRootSortState, replayInsert, consRootContext, ctorContext, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, + simp [consRootCheckNLctx, consRootCheckNId, consRootCheckNatState, consRootCheckAlphaState, + consRootCheckAlphaLctx, consRootCheckAlphaId, nilRootSortState, replayInsert, consRootContext, + ctorContext, LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] theorem consRootCheckAlphaMiss : @@ -1849,14 +1781,11 @@ theorem consRootCheckHeadFresh : have h := LocalContext.WF.find?_eq_find?_toList (fv := consRootCheckHeadId) consRootCheckNLctxWF rw [h] - simp [consRootCheckHeadId, consRootCheckHeadDomainState, - consRootCheckNState, consRootCheckNId, consRootCheckNatState, - consRootCheckAlphaState, consRootCheckAlphaLctx, - consRootCheckAlphaId, nilRootSortState, replayInsert, - consRootCheckNLctx, consRootContext, ctorContext, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consRootCheckHeadId, consRootCheckHeadDomainState, consRootCheckNState, consRootCheckNId, + consRootCheckNatState, consRootCheckAlphaState, consRootCheckAlphaLctx, consRootCheckAlphaId, + nilRootSortState, replayInsert, consRootCheckNLctx, consRootContext, ctorContext, + LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, + NameGenerator.curr] intro x hx change some x ∈ (PersistentArray.empty : PersistentArray (Option LocalDecl)).toList' at hx @@ -1873,15 +1802,11 @@ theorem consRootCheckNFind : some (.cdecl 1 consRootCheckNId consNName (.const ``Nat []) .implicit .default) := by rw [consRootCheckHeadLctxWF.find?_eq_find?_toList] - simp [consRootCheckHeadLctx, consRootCheckHeadId, - consRootCheckHeadDomainState, consRootCheckNState, - consRootCheckNLctx, consRootCheckNId, consRootCheckNatState, - consRootCheckAlphaState, consRootCheckAlphaLctx, - consRootCheckAlphaId, nilRootSortState, replayInsert, - consRootContext, ctorContext, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consRootCheckHeadLctx, consRootCheckHeadId, consRootCheckHeadDomainState, + consRootCheckNState, consRootCheckNLctx, consRootCheckNId, consRootCheckNatState, + consRootCheckAlphaState, consRootCheckAlphaLctx, consRootCheckAlphaId, nilRootSortState, + replayInsert, consRootContext, ctorContext, LocalContext.mkLocalDecl, LocalContext.toList, + LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] @[simp] theorem replayConsRootAlphaIdBeqNId : ((.fvar consRootCheckAlphaId : Expr) == @@ -2166,7 +2091,7 @@ theorem replayConsRootCheckTypeM : rw [hhead] simp only [ensureSortExact] rw [withLocalDeclEq] - simp [Expr.instantiate1'] + simp have htail : TypeChecker.Inner.inferType (((.const ``IndexedVec [.param `u] : Expr).app @@ -2192,7 +2117,7 @@ theorem replayConsRootCheckTypeM : rw [htail] simp only [ensureSortExact] rw [withLocalDeclEq] - simp [Expr.instantiate1'] + simp have hterminal : TypeChecker.Inner.inferType (((.const ``IndexedVec [.param `u] : Expr).app @@ -2267,8 +2192,7 @@ theorem consHeadAnnotationTraceBuild : theorem consTailAnnotationTraceBuild : AddInductive.CandidateTypeAnnotationTrace.build consTailDomain = ⟨consTailDomain, .identity _⟩ := by - simp [AddInductive.CandidateTypeAnnotationTrace.build, - consTailDomain, consAlphaExprShape, consNExprShape] + simp [AddInductive.CandidateTypeAnnotationTrace.build, consTailDomain] theorem consAlphaAnnotationsBuild : AddInductive.buildCandidateTypeAnnotations @@ -2863,7 +2787,7 @@ def indexedVecNormalizationCandidate : families := .cons indexedVecFamilyListCandidate .nil /-- Source-indexed evidence for the complete `IndexedVec` family-type list. -/ -def indexedVecFamilyTypeListProduced : +theorem indexedVecFamilyTypeListProduced : AddInductive.CandidateFamilyTypeListProduced indexedVecFamilyCandidateContext (.cons indexedVecFamilyListCandidate.familyType .nil) := by @@ -2886,7 +2810,7 @@ theorem indexedVecFamilyTypeListCandidateProduced : /-- The two constructor positions are assembled in source order. The dependent list indices rule out truncating, swapping, or reusing either constructor proof. -/ -def indexedVecConstructorListProduced : +theorem indexedVecConstructorListProduced : AddInductive.CandidateConstructorListProduced ctorContext indexedVecFamilyListCandidate.constructors := by have hnil : AddInductive.buildCandidateExpr indexedVecNilInfo.type @@ -2915,7 +2839,7 @@ theorem indexedVecConstructorListCandidateProduced : /-- Source-indexed evidence for complete family assembly after constructor normalization. -/ -def indexedVecFamilyListProduced : +theorem indexedVecFamilyListProduced : AddInductive.CandidateFamilyListProduced ctorContext (.cons indexedVecFamilyListCandidate.familyType .nil) indexedVecNormalizationCandidate.families := by diff --git a/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean b/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean index 3a913f38..cf9da634 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecConstructors.lean @@ -116,10 +116,8 @@ def tcContext (lctx : LocalContext := {}) : TypeChecker.Context where rw [ConstantInfo.instantiateTypeLevelParams, ConstantVal.instantiateTypeLevelParams, Expr.instantiateLevelParams_eq] - simp [indexedVecInfo, ConstantInfo.type, - ConstantInfo.toConstantVal, - Expr.instantiateLevelParamsCore', Level.substParams', - Syntax.structEq_eq] + simp [indexedVecInfo, ConstantInfo.type, ConstantInfo.toConstantVal, + Expr.instantiateLevelParamsCore', Level.substParams'] @[simp] theorem inferConstantFamily (lctx) : TypeChecker.Inner.inferConstant (tcContext lctx) ``IndexedVec @@ -134,13 +132,7 @@ def tcContext (lctx : LocalContext := {}) : TypeChecker.Context where ({ env := ctorEnv, lctx := lctx, lparams := [`u] } : TypeChecker.Context) (.param `u) = .ok () by simpa [tcContext] using checkLevelParam lctx] - simp [indexedVecInfo, indexedVecInfoInstantiate, - ConstantInfo.levelParams, ConstantInfo.isUnsafe, - ConstantInfo.instantiateTypeLevelParams, ConstantInfo.toConstantVal, - ConstantVal.instantiateTypeLevelParams, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', - Level.substParams', Bind.bind, Except.bind, - Pure.pure, Except.pure] + simp [indexedVecInfo, Bind.bind, Except.bind, Pure.pure, Except.pure] @[simp] theorem inferConstantNat (lctx) : TypeChecker.Inner.inferConstant (tcContext lctx) ``Nat [] false = @@ -382,10 +374,8 @@ theorem inferAppCoreOf (stateArg.inferTypeC.insert (.app fn arg) (body.instantiate1 arg)) }) := by unfold TypeChecker.Inner.inferType' - simp [hclosed, hcache, hfn, harg, - heager, ensureForallExact, selfDefEq, - Expr.instantiate1_eq, Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + simp [hclosed, hcache, hfn, harg, heager, selfDefEq, Expr.instantiate1_eq, Bind.bind, + ReaderT.bind, StateT.bind, Except.bind] theorem inferTypeForallCore (fuel : Nat) (context : TypeChecker.Context) @@ -457,9 +447,7 @@ theorem inferNilFamily : .ok (indexedVecInfo.type, nilFamilyState) := by simpa [nilFamilyState] using (inferTypeFamilyCore 9998 nilAlphaLctx nilBodyInitialState (by - simp [nilBodyInitialState, nilRootSortState, - Std.HashMap.getElem?_insert, - Expr.eqv_eq])) + simp [nilBodyInitialState, nilRootSortState])) theorem inferNilAlpha : TypeChecker.Inner.inferType' (.fvar nilAlphaId) false @@ -470,8 +458,7 @@ theorem inferNilAlpha : (inferTypeFVarCore 9998 nilAlphaLctx nilFamilyState nilAlphaId (.sort (.succ (.param `u))) (index := 0) (name := `α) (bi := .implicit) (kind := .default) (by - simp [nilFamilyState, nilBodyInitialState, nilRootSortState, - Std.HashMap.getElem?_insert, Expr.eqv_eq]) nilAlphaFind) + simp [nilFamilyState, nilBodyInitialState, nilRootSortState]) nilAlphaFind) theorem inferNilFirstApp : TypeChecker.Inner.inferType' nilFirstApp false @@ -485,9 +472,7 @@ theorem inferNilFirstApp : (by simp [Expr.hasLooseBVars, Expr.looseBVarRange']) (by - simp [nilBodyInitialState, nilRootSortState, - Std.HashMap.getElem?_insert, - Expr.eqv_eq]) + simp [nilBodyInitialState, nilRootSortState]) (by simpa [indexedVecInfoTypeShape] using inferNilFamily) inferNilAlpha (by rfl) simpa [nilFirstApp, nilFirstAppState, vecFamilyTail, @@ -500,9 +485,8 @@ theorem inferNilZero : .ok (.const ``Nat [], nilZeroState) := by simpa [nilZeroState] using (inferTypeZeroCore 9998 nilAlphaLctx nilFirstAppState (by - simp [nilFirstAppState, nilAlphaState, nilFamilyState, - nilBodyInitialState, nilRootSortState, nilFirstApp, - Std.HashMap.getElem?_insert, Expr.eqv_eq])) + simp [nilFirstAppState, nilAlphaState, nilFamilyState, nilBodyInitialState, nilRootSortState, + nilFirstApp])) theorem inferNilBodyExists : ∃ finalState, TypeChecker.Inner.inferType nilBodyExpr false @@ -519,10 +503,8 @@ theorem inferNilBodyExists : ∃ finalState, nilBodyInitialState nilFirstAppState nilZeroState nilFirstApp (.const ``Nat.zero []) (.const ``Nat []) (.sort (.succ (.param `u))) vecIndexName .default - (by simp [nilBodyExpr, nilFirstApp, - Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [nilBodyExpr, nilBodyInitialState, nilRootSortState, - Std.HashMap.getElem?_insert, Expr.eqv_eq]) + (by simp [nilFirstApp, Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp [nilBodyInitialState, nilRootSortState]) (by simpa [vecFamilyTail] using inferNilFirstApp) inferNilZero (by rfl) simpa [nilBodyExpr, nilFirstApp, @@ -604,9 +586,8 @@ theorem nilRootInferForallExists : ∃ finalState, (((.const ``IndexedVec [.param `u] : Expr).app (.bvar 0)).app (.const ``Nat.zero [])).instantiateRev (#[] |>.push (.fvar nilAlphaId)) = nilBodyExpr by - simp [nilCtorBodyRaw, nilBodyExpr, nilAlphaId, - Expr.instantiateRev_eq, Expr.instantiate_eq, - Expr.instantiate1', Expr.liftLooseBVars_zero]] + simp [nilBodyExpr, nilAlphaId, Expr.instantiateRev_eq, Expr.instantiate_eq, Expr.instantiate1', + Expr.liftLooseBVars_zero]] simp only [Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [hbody] simp only @@ -813,9 +794,8 @@ theorem inferNilCandidateFirstApp : nilCandidateAlphaState (.const ``IndexedVec [.param `u]) (.fvar nilCandidateAlphaId) (.sort (.succ (.param `u))) vecFamilyTail `α .default - (by simp [nilCandidateFirstApp, Expr.hasLooseBVars, - Expr.looseBVarRange']) - (by simp [nilCandidateFirstApp]) inferNilCandidateFamily + (by simp [Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp) inferNilCandidateFamily (by simpa [indexedVecInfoTypeShape] using inferNilCandidateAlpha) (by rfl) simpa [nilCandidateFirstApp, nilCandidateFirstAppState, @@ -830,9 +810,8 @@ theorem inferNilCandidateZero : simpa [nilCandidateZeroState] using (inferTypeZeroCore 9999 nilCandidateAlphaLctx nilCandidateFirstAppState (by - simp [nilCandidateFirstAppState, nilCandidateAlphaState, - nilCandidateFamilyState, nilCandidateFirstApp, - Expr.eqv_eq])) + simp [nilCandidateFirstAppState, nilCandidateAlphaState, nilCandidateFamilyState, + nilCandidateFirstApp])) theorem inferNilCandidateBodyExists : ∃ finalState, TypeChecker.Inner.inferType nilCandidateBody false @@ -850,9 +829,8 @@ theorem inferNilCandidateBodyExists : ∃ finalState, ({} : TypeChecker.State) nilCandidateFirstAppState nilCandidateZeroState nilCandidateFirstApp (.const ``Nat.zero []) (.const ``Nat []) (.sort (.succ (.param `u))) vecIndexName .default - (by simp [nilCandidateBodyExpr, nilCandidateFirstApp, - Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [nilCandidateBodyExpr]) inferNilCandidateFirstApp + (by simp [nilCandidateFirstApp, Expr.hasLooseBVars, Expr.looseBVarRange']) + (by simp) inferNilCandidateFirstApp inferNilCandidateZero (by rfl) simpa [nilCandidateBodyExpr, nilCandidateFirstApp, Expr.instantiate1_eq, Expr.instantiate1'] using h @@ -927,7 +905,7 @@ theorem nilCandidateReduceRecursor simp only [nilRecMBind, nilRecMGetEnv] rw [show (tcContext nilCandidateAlphaLctx).env = ctorEnv by rfl] rw [hquot] - simp only [Bool.false_eq_true, if_false, nilRecMBind, nilRecMPure] + simp only [Bool.false_eq_true, if_false, nilRecMBind] rw [nilCandidateInductiveReduceRec methods state] rfl @@ -951,8 +929,7 @@ theorem nilCandidateWhnfCoreInitial (n : Nat) : false (TypeChecker.Methods.withFuel (n + 1)) (tcContext nilCandidateAlphaLctx) ({} : TypeChecker.State) = _ unfold TypeChecker.Inner.whnfCore' - simp only [nilRecMPure, nilRecMBind, nilRecMGet, - Std.HashMap.getElem?_empty] + simp only [nilRecMBind, nilRecMGet, Std.HashMap.getElem?_empty] rw [Expr.withRevApp_eq] simp only [nilRecMBind] rw [show @@ -962,9 +939,8 @@ theorem nilCandidateWhnfCoreInitial (n : Nat) : (Expr.const ``Nat.zero [])).getAppFn = (Expr.const ``IndexedVec [.param `u]) by rfl] rw [nilCandidateWhnfCoreFamily n ({} : TypeChecker.State)] - simp [nilCandidateBodyShape, nilCandidateBodyExpr, - nilCandidateFirstApp, nilCandidateReduceRecursor, - Expr.structuralEq, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [nilCandidateBodyExpr, nilCandidateFirstApp, Expr.structuralEq, Bind.bind, ReaderT.bind, + StateT.bind, Except.bind] rw [show .app (.app (.const ``IndexedVec [.param `u]) (.fvar nilCandidateAlphaId)) (.const ``Nat.zero []) = @@ -990,9 +966,8 @@ theorem nilCandidateWhnfCoreInitial (n : Nat) : methods (tcContext nilCandidateAlphaLctx) state = .ok (none, state) := by rw [nilCandidateBodyShape] - simp [TypeChecker.Inner.reduceNat, nilCandidateBodyExpr, - nilCandidateFirstApp, Expr.getAppNumArgs_eq, - Expr.getAppArgsRevList, Expr.appFn!, Expr.structuralEq] + simp [TypeChecker.Inner.reduceNat, nilCandidateBodyExpr, nilCandidateFirstApp, + Expr.getAppNumArgs_eq, Expr.getAppArgsRevList] theorem nilCandidateIsDeltaFamily : TypeChecker.Inner.isDelta ctorEnv @@ -1042,11 +1017,11 @@ theorem nilCandidateWhnfLoop : rw [show 9999 = 9998 + 1 by rfl] simp only [nilRecMBind, nilRecMGetEnv] rw [nilCandidateWhnfCoreInitial 9998] - simp only [nilRecMBind] + simp only [] rw [nilCandidateReduceNative] - simp only [nilRecMBind, nilRecMPure] + simp only [nilRecMBind] rw [nilCandidateReduceNat] - simp only [nilRecMBind, nilRecMPure] + simp only [nilRecMBind] rw [nilCandidateUnfoldBody] rfl @@ -1399,42 +1374,30 @@ def consTerminal : Expr := theorem consAfterAlphaShape : consNTypeRaw.instantiate1 consRootContext.freshExpr = consAfterAlpha := by - simp [consNTypeRaw, consHeadTypeRaw, consTailTypeRaw, - consTerminalRaw, consAfterAlpha, consAlphaExpr, - consRootContext, ctorContext, - AddInductive.Context.freshExpr, - Expr.instantiate1_eq, Expr.instantiate1', - Expr.liftLooseBVars_zero] + simp [consNTypeRaw, consHeadTypeRaw, consTailTypeRaw, consTerminalRaw, consAfterAlpha, + consAlphaExpr, consRootContext, ctorContext, AddInductive.Context.freshExpr, + Expr.instantiate1_eq, Expr.instantiate1'] theorem consAfterNShape : consAfterAlpha.bindingBody!.instantiate1 consAlphaContext.freshExpr = consAfterN := by - simp [consAfterAlpha, consAfterN, consAlphaExpr, consNExpr, - consRootContext, consAlphaContext, ctorContext, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshExpr, - Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1', - Expr.liftLooseBVars_zero] + simp [consAfterAlpha, consAfterN, consAlphaExpr, consNExpr, consRootContext, consAlphaContext, + ctorContext, AddInductive.Context.pushLocalDecl, AddInductive.Context.freshExpr, + Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1'] theorem consAfterHeadShape : consAfterN.bindingBody!.instantiate1 consNContext.freshExpr = consAfterHead := by - simp [consAfterN, consAfterHead, consTailDomain, - consAlphaExpr, consNExpr, consRootContext, consAlphaContext, - consNContext, ctorContext, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshExpr, - Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1', - Expr.liftLooseBVars_zero] + simp [consAfterN, consAfterHead, consTailDomain, consAlphaExpr, consNExpr, consRootContext, + consAlphaContext, consNContext, ctorContext, AddInductive.Context.pushLocalDecl, + AddInductive.Context.freshExpr, Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1'] theorem consTerminalShape : consAfterHead.bindingBody!.instantiate1 consHeadContext.freshExpr = consTerminal := by - simp [consAfterHead, consTerminal, consAlphaExpr, consNExpr, - consRootContext, consAlphaContext, consNContext, - consHeadContext, ctorContext, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshExpr, Expr.bindingBody!, - Expr.instantiate1_eq, Expr.instantiate1', - Expr.liftLooseBVars_zero] + simp [consAfterHead, consTerminal, consAlphaExpr, consNExpr, consRootContext, consAlphaContext, + consNContext, consHeadContext, ctorContext, AddInductive.Context.pushLocalDecl, + AddInductive.Context.freshExpr, Expr.bindingBody!, Expr.instantiate1_eq, Expr.instantiate1'] @[simp] theorem consAlphaExprShape : consAlphaExpr = .fvar consAlphaId := by @@ -1548,66 +1511,48 @@ theorem consAlphaFindInHead : some (.cdecl 0 consAlphaId consAlphaName (.sort (.succ (.param `u))) .implicit .default) := by rw [consHeadContextWF.find?_eq_find?_toList] - simp [consHeadContext, consNContext, consAlphaContext, - consRootContext, ctorContext, consAlphaId, consNId, consHeadId, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, - LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consHeadContext, consNContext, consAlphaContext, consRootContext, ctorContext, consAlphaId, + AddInductive.Context.pushLocalDecl, AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, + LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] theorem consAlphaFindInN : consNContext.lctx.find? consAlphaId = some (.cdecl 0 consAlphaId consAlphaName (.sort (.succ (.param `u))) .implicit .default) := by rw [consNContextWF.find?_eq_find?_toList] - simp [consNContext, consAlphaContext, consRootContext, ctorContext, - consAlphaId, consNId, AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, LocalContext.mkLocalDecl, - LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consNContext, consAlphaContext, consRootContext, ctorContext, consAlphaId, + AddInductive.Context.pushLocalDecl, AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, + LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] theorem consNFindInHead : consHeadContext.lctx.find? consNId = some (.cdecl 1 consNId consNName (.const ``Nat []) .implicit .default) := by rw [consHeadContextWF.find?_eq_find?_toList] - simp [consHeadContext, consNContext, consAlphaContext, - consRootContext, ctorContext, consAlphaId, consNId, consHeadId, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, - LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consHeadContext, consNContext, consAlphaContext, consRootContext, ctorContext, consAlphaId, + consNId, AddInductive.Context.pushLocalDecl, AddInductive.Context.freshFVarId, + LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, + NameGenerator.curr] theorem consAlphaFindInTail : consTailContext.lctx.find? consAlphaId = some (.cdecl 0 consAlphaId consAlphaName (.sort (.succ (.param `u))) .implicit .default) := by rw [consTailContextWF.find?_eq_find?_toList] - simp [consTailContext, consHeadContext, consNContext, - consAlphaContext, consRootContext, ctorContext, - consAlphaId, consNId, consHeadId, consTailId, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, - LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consTailContext, consHeadContext, consNContext, consAlphaContext, consRootContext, + ctorContext, consAlphaId, AddInductive.Context.pushLocalDecl, AddInductive.Context.freshFVarId, + LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, NameGenerator.next, + NameGenerator.curr] theorem consNFindInTail : consTailContext.lctx.find? consNId = some (.cdecl 1 consNId consNName (.const ``Nat []) .implicit .default) := by rw [consTailContextWF.find?_eq_find?_toList] - simp [consTailContext, consHeadContext, consNContext, - consAlphaContext, consRootContext, ctorContext, - consAlphaId, consNId, consHeadId, consTailId, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshFVarId, - LocalContext.mkLocalDecl_toList, - LocalContext.mkLocalDecl, LocalContext.toList, LocalDecl.fvarId, - NameGenerator.next, NameGenerator.curr] + simp [consTailContext, consHeadContext, consNContext, consAlphaContext, consRootContext, + ctorContext, consAlphaId, consNId, AddInductive.Context.pushLocalDecl, + AddInductive.Context.freshFVarId, LocalContext.mkLocalDecl, LocalContext.toList, + LocalDecl.fvarId, NameGenerator.next, NameGenerator.curr] /-! ## Reusable post-family atom observations -/ @@ -1694,7 +1639,7 @@ theorem ctorFVarWhnfM (TypeChecker.Methods.withFuel 9999) (tcContext lctx) ({} : TypeChecker.State) = .ok (lctx, ({} : TypeChecker.State)) by rfl] - simp [TypeChecker.Inner.isLetFVar, hfind, nilRecMPure] + simp [TypeChecker.Inner.isLetFVar, hfind] rfl /-! A uniform WHNF observation for opaque applications of the inserted @@ -1731,7 +1676,7 @@ theorem ctorIndexedVecReduceRecursor simp only [nilRecMBind, nilRecMGetEnv] rw [show (tcContext lctx).env = ctorEnv by rfl] rw [hquot] - simp only [Bool.false_eq_true, if_false, nilRecMBind, nilRecMPure] + simp only [Bool.false_eq_true, if_false, nilRecMBind] rw [ctorIndexedVecInductiveReduceRec] rfl @@ -1750,16 +1695,14 @@ theorem ctorIndexedVecWhnfCoreInitial (tcContext lctx) ({} : TypeChecker.State) = .ok (ctorIndexedVecApp alpha index, ({} : TypeChecker.State)) := by unfold ctorIndexedVecApp TypeChecker.Inner.whnfCore' - simp only [nilRecMPure, nilRecMBind, nilRecMGet, - Std.HashMap.getElem?_empty] + simp only [nilRecMBind, nilRecMGet, Std.HashMap.getElem?_empty] rw [Expr.withRevApp_eq] simp only [nilRecMBind] rw [show (Expr.app (Expr.app (Expr.const ``IndexedVec [.param `u]) alpha) index).getAppFn = Expr.const ``IndexedVec [.param `u] by rfl] rw [ctorIndexedVecWhnfCoreFamily lctx n ({} : TypeChecker.State)] - simp [ctorIndexedVecApp, ctorIndexedVecReduceRecursor, - Expr.structuralEq, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.structuralEq, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [show Expr.app (Expr.app (Expr.const ``IndexedVec [.param `u]) alpha) index = ctorIndexedVecApp alpha index by rfl] @@ -1782,9 +1725,8 @@ theorem ctorIndexedVecWhnfCoreInitial (methods : TypeChecker.Methods) (state : TypeChecker.State) : TypeChecker.Inner.reduceNat (ctorIndexedVecApp alpha index) methods (tcContext lctx) state = .ok (none, state) := by - simp [ctorIndexedVecApp, TypeChecker.Inner.reduceNat, - Expr.getAppNumArgs_eq, Expr.getAppArgsRevList, - Expr.appFn!, Expr.structuralEq] + simp [ctorIndexedVecApp, TypeChecker.Inner.reduceNat, Expr.getAppNumArgs_eq, + Expr.getAppArgsRevList] theorem ctorIndexedVecUnfoldFamily (lctx : LocalContext) (methods : TypeChecker.Methods) @@ -1822,11 +1764,11 @@ theorem ctorIndexedVecWhnfLoop rw [show 9999 = 9998 + 1 by rfl] simp only [nilRecMBind, nilRecMGetEnv] rw [ctorIndexedVecWhnfCoreInitial lctx alpha index 9998] - simp only [nilRecMBind] + simp only [] rw [ctorIndexedVecReduceNative] - simp only [nilRecMBind, nilRecMPure] + simp only [nilRecMBind] rw [ctorIndexedVecReduceNat] - simp only [nilRecMBind, nilRecMPure] + simp only [nilRecMBind] rw [ctorIndexedVecUnfold] rfl diff --git a/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean b/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean index 7e324643..81ea7e78 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecOuterReplay.lean @@ -49,9 +49,8 @@ theorem validationFamilyEnvNotContains : theorem validationFamilyEnvCheckName : indexedVecKernelEnv.checkName ``IndexedVec false = .ok () := by - simp [Kernel.Environment.checkName, validationFamilyEnvNotContains, - Kernel.Environment.primitives, NameSet.ofList, NameSet.contains, - Bind.bind, Except.bind, Pure.pure, Except.pure] + simp [Kernel.Environment.checkName, validationFamilyEnvNotContains, Kernel.Environment.primitives, + NameSet.ofList, NameSet.contains, Pure.pure, Except.pure] theorem indexedVecDeclareRoot : AddInductive.declareInductiveTypes indexedVecCandidateInductiveStats 1 @@ -1213,9 +1212,7 @@ theorem indexedVecValidationTailPositivity : indexedVecValidationAlpha indexedVecValidationNExpr] simp only [Except.bind] rw [indexedVecValidationTailHasIndOcc] - simp only [Bool.not_true, Bool.false_eq_true, if_false, - ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, - Except.bind, Except.pure] + simp only [Bool.not_true, Bool.false_eq_true, if_false, Pure.pure] rw [indexedVecValidationAppIsValid indexedVecValidationNExpr indexedVecValidationNHasNoIndOcc] rfl @@ -1259,9 +1256,7 @@ theorem indexedVecValidationNilLoop : simp only [Except.bind] rw [AddInductive.liftTypeChecker_apply] rw [indexedVecValidationParamIsDefEq] - simp only [if_true, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [if_true] simpa [indexedVecValidationNilResult, ctorIndexedVecApp, indexedVecKernelNil, indexedVecNilInfo, ConstantInfo.name, ConstantInfo.toConstantVal, @@ -1327,9 +1322,7 @@ theorem indexedVecValidationConsLoopTail : (Expr.sort (.succ (.param `u))).sortLevel! = true from by simp [Expr.sortLevel!, indexedVecCandidateInductiveStats_resultLevel, AddInductive.levelStructGe, AddInductive.levelStructEq])] - simp only [↓reduceIte, Bool.not_false, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [↓reduceIte, Bool.not_false, ReaderT.bind, Bind.bind, Except.bind] rw [indexedVecValidationTailPositivity] rw [AddInductive.withLocalDecl_apply] rw [indexedVecValidationConsumeTail] @@ -1364,9 +1357,7 @@ theorem indexedVecValidationConsLoopHead : (Expr.sort (.succ (.param `u))).sortLevel! = true from by simp [Expr.sortLevel!, indexedVecCandidateInductiveStats_resultLevel, AddInductive.levelStructGe, AddInductive.levelStructEq])] - simp only [↓reduceIte, Bool.not_false, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [↓reduceIte, Bool.not_false, ReaderT.bind, Bind.bind, Except.bind] rw [indexedVecValidationAlphaPositivity] rw [AddInductive.withLocalDecl_apply] rw [indexedVecValidationConsumeAlpha] @@ -1407,9 +1398,7 @@ theorem indexedVecValidationConsLoopN : (Expr.sort (.succ .zero)).sortLevel! = true from by simp [Expr.sortLevel!, indexedVecCandidateInductiveStats_resultLevel, AddInductive.levelStructGe])] - simp only [↓reduceIte, Bool.not_false, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [↓reduceIte, Bool.not_false, ReaderT.bind, Bind.bind, Except.bind] rw [indexedVecValidationNatPositivity] rw [AddInductive.withLocalDecl_apply] rw [indexedVecValidationConsumeNat] @@ -1454,9 +1443,7 @@ theorem indexedVecValidationConsLoop : simp only [Except.bind] rw [AddInductive.liftTypeChecker_apply] rw [indexedVecValidationParamIsDefEq] - simp only [if_true, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [if_true] simpa [indexedVecValidationConsAfterParam] using indexedVecValidationConsLoopN @@ -1652,7 +1639,7 @@ theorem indexedVecValidationNilSetDoesNotContainCons : ConstantInfo.name, ConstantInfo.toConstantVal, NameSet.contains, NameSet.insert] rw [Std.TreeSet.contains_insert (t := (∅ : NameSet))] - simp +decide [beq_iff_eq, Std.LawfulBEqCmp.compare_eq_iff_beq] + simp +decide set_option linter.unusedSimpArgs false in theorem indexedVecValidationCheckConstructors : diff --git a/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean b/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean index a16e5f42..4132bf55 100644 --- a/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean +++ b/Lean4Lean/Verify/Environment/IndexedVecSemanticReplay.lean @@ -116,16 +116,16 @@ theorem indexedVecKernelEnv_noProjectionReady (name : Name) : (s := ({} : ConstMap)) SMap.WF.empty] by_cases hRec : ``Nat.rec = name · subst name - simp [SMap.find?, natRecInfo] + simp [natRecInfo] · by_cases hSucc : ``Nat.succ = name · subst name - simp [hRec, SMap.find?, natSuccInfo] + simp [hRec, natSuccInfo] · by_cases hZero : ``Nat.zero = name · subst name - simp [hRec, hSucc, SMap.find?, natZeroInfo] + simp [hRec, hSucc, natZeroInfo] · by_cases hNat : ``Nat = name · subst name - simp [hRec, hSucc, hZero, SMap.find?, natInfo] + simp [hRec, hSucc, hZero, natInfo] · simp [hRec, hSucc, hZero, hNat, SMap.find?] theorem indexedVecKernelEnv_noStructureEta (name : Name) : @@ -140,16 +140,16 @@ theorem indexedVecKernelEnv_noStructureEta (name : Name) : (s := ({} : ConstMap)) SMap.WF.empty] by_cases hRec : ``Nat.rec = name · subst name - simp [SMap.find?, natRecInfo] + simp [natRecInfo] · by_cases hSucc : ``Nat.succ = name · subst name - simp [hRec, SMap.find?, natSuccInfo] + simp [hRec, natSuccInfo] · by_cases hZero : ``Nat.zero = name · subst name - simp [hRec, hSucc, SMap.find?, natZeroInfo] + simp [hRec, hSucc, natZeroInfo] · by_cases hNat : ``Nat = name · subst name - simp [hRec, hSucc, hZero, SMap.find?, natInfo] + simp [hRec, hSucc, hZero, natInfo] · simp [hRec, hSucc, hZero, hNat, SMap.find?] theorem indexedVecTypeEnv_noProjectionReady (name : Name) : @@ -166,19 +166,19 @@ theorem indexedVecTypeEnv_noProjectionReady (name : Name) : (s := ({} : ConstMap)) SMap.WF.empty] by_cases hVec : ``IndexedVec = name · subst name - simp [SMap.find?, indexedVecInfo] + simp [indexedVecInfo] · by_cases hRec : ``Nat.rec = name · subst name - simp [hVec, SMap.find?, natRecInfo] + simp [hVec, natRecInfo] · by_cases hSucc : ``Nat.succ = name · subst name - simp [hVec, hRec, SMap.find?, natSuccInfo] + simp [hVec, hRec, natSuccInfo] · by_cases hZero : ``Nat.zero = name · subst name - simp [hVec, hRec, hSucc, SMap.find?, natZeroInfo] + simp [hVec, hRec, hSucc, natZeroInfo] · by_cases hNat : ``Nat = name · subst name - simp [hVec, hRec, hSucc, hZero, SMap.find?, natInfo] + simp [hVec, hRec, hSucc, hZero, natInfo] · simp [hVec, hRec, hSucc, hZero, hNat, SMap.find?] theorem indexedVecTypeEnv_noStructureEta (name : Name) : @@ -194,19 +194,19 @@ theorem indexedVecTypeEnv_noStructureEta (name : Name) : (s := ({} : ConstMap)) SMap.WF.empty] by_cases hVec : ``IndexedVec = name · subst name - simp [SMap.find?, indexedVecInfo] + simp [indexedVecInfo] · by_cases hRec : ``Nat.rec = name · subst name - simp [hVec, SMap.find?, natRecInfo] + simp [hVec, natRecInfo] · by_cases hSucc : ``Nat.succ = name · subst name - simp [hVec, hRec, SMap.find?, natSuccInfo] + simp [hVec, hRec, natSuccInfo] · by_cases hZero : ``Nat.zero = name · subst name - simp [hVec, hRec, hSucc, SMap.find?, natZeroInfo] + simp [hVec, hRec, hSucc, natZeroInfo] · by_cases hNat : ``Nat = name · subst name - simp [hVec, hRec, hSucc, hZero, SMap.find?, natInfo] + simp [hVec, hRec, hSucc, hZero, natInfo] · simp [hVec, hRec, hSucc, hZero, hNat, SMap.find?] private theorem addConst_constants {env env' : VEnv} {name : Name} @@ -1889,7 +1889,7 @@ private theorem indexedVecPreFamilySuccFVarCheckTypeM (.const ``Nat.succ []) (.fvar id) (.const ``Nat []) (.const ``Nat []) `n .default (by simp [Expr.hasLooseBVars, Expr.looseBVarRange']) - (by simp [replaySuccApp]) succRun argumentRun (by rfl) + (by simp) succRun argumentRun (by rfl) change Except.map (fun x : Expr × TypeChecker.State => x.1) (TypeChecker.Inner.inferType' (replaySuccApp (.fvar id)) false (TypeChecker.Methods.withFuel 9999) @@ -2609,7 +2609,7 @@ private theorem indexedVecPreFamilySafetyRun : simp [AddInductive.constructorIndependentOf])] simp only [Bind.bind, Except.bind] rw [alphaAnnotations.observe_eq] - simp only [Bind.bind, Except.bind] + simp only [] rw [dif_pos nFresh] rw [explicitHeadTailRun] exact ⟨_, rfl⟩ @@ -2698,7 +2698,7 @@ private theorem indexedVecPreFamilySafetyRun : simp [AddInductive.constructorIndependentOf])] simp only [Bind.bind, Except.bind] rw [baseNatAnnotations.observe_eq] - simp only [Bind.bind, Except.bind] + simp only [] rw [dif_pos baseFresh] rw [explicitNTailRun] exact ⟨_, rfl⟩ @@ -2812,10 +2812,8 @@ private theorem indexedVecPreFamilySafetyRun : rw [indexedVecPreFamilyIndexTelescope_eq] rw [indexedVecValidationStatsParams] rw [indexedVecInfoTypeShape] - simp [AddInductive.instantiateFamilyParameters, vecFamilyTail, - vecIndexName, - indexedVecPreFamilyIndexTelescope, Expr.instantiate1_eq, - Expr.instantiate1', Pure.pure, Except.pure] + simp [AddInductive.instantiateFamilyParameters, vecFamilyTail, vecIndexName, + Expr.instantiate1_eq, Expr.instantiate1', Pure.pure, Except.pure] unfold AddInductive.checkConstructorPreFamilySafety have translationUnique : (AddInductive.theoryTranslationUnique indexedVecInfo.type && @@ -3020,21 +3018,21 @@ theorem indexedVecSemantic_normalization_eq : indexedVecSemanticNormalizationCandidateRun.normalization = indexedVecChecked.identityGeneration.block.normalization := rfl -def indexedVecSemanticFamilySpineRun : +theorem indexedVecSemanticFamilySpineRun : TypeChecker.CandidateExprSpineRun natFinalEnv [`u] indexedVecFamilyCandidate indexedVecType.type indexedVecType.type := indexedVecSemanticFamilySemanticRootRun.spine indexedVecFamilyCandidate_identity.storedSpine -def indexedVecSemanticNilSpineRun : +theorem indexedVecSemanticNilSpineRun : TypeChecker.CandidateExprSpineRun indexedVecTypeEnv [`u] nilCandidate indexedVecType.ctors[0].type indexedVecType.ctors[0].type := indexedVecSemanticNilSemanticRootRun.spine nilCandidate_identity.storedSpine -def indexedVecSemanticConsSpineRun : +theorem indexedVecSemanticConsSpineRun : TypeChecker.CandidateExprSpineRun indexedVecTypeEnv [`u] consCandidate indexedVecType.ctors[1].type indexedVecType.ctors[1].type := diff --git a/Lean4Lean/Verify/Environment/InductiveFixtures.lean b/Lean4Lean/Verify/Environment/InductiveFixtures.lean index 38a1d312..123b2923 100644 --- a/Lean4Lean/Verify/Environment/InductiveFixtures.lean +++ b/Lean4Lean/Verify/Environment/InductiveFixtures.lean @@ -2964,9 +2964,7 @@ private theorem annotatedPiExceptPure ``outParam [.succ .zero] false = .ok (.forallE `α (.sort (.succ .zero)) (.sort (.succ .zero)) .default) := by - simpa [annotatedPiCtorCandidateContext, - AddInductive.Context.toTypeChecker] using - annotatedPiInferConstantOutParam ({} : LocalContext) + simp [annotatedPiCtorCandidateContext, AddInductive.Context.toTypeChecker] @[simp] private theorem annotatedPiEnsureForall (name dom body bi source methods context state) : @@ -3107,7 +3105,7 @@ private def annotatedPiOuterName : Name := @[simp] private theorem annotatedPiFamilyType_noLooseBVars : annotatedPiInfo.type.hasLooseBVars = false := by rw [show annotatedPiInfo.type = .sort (.succ .zero) by rfl] - simp [annotatedPiInfo, Expr.hasLooseBVars, Expr.looseBVarRange'] + simp [Expr.hasLooseBVars, Expr.looseBVarRange'] @[simp] private theorem emptyCheckTypeCache_annotatedPiFamily : (({} : TypeChecker.State).inferTypeC)[annotatedPiInfo.type]? = none := by @@ -3117,9 +3115,8 @@ private def annotatedPiOuterName : Name := TypeChecker.Inner.checkLevel annotatedPiFamilyCandidateContext.toTypeChecker (.succ .zero) = .ok () := by - simp [TypeChecker.Inner.checkLevel, annotatedPiFamilyCandidateContext, - AddInductive.Context.toTypeChecker, Level.getUndefParam, Level.forEach, - Level.hasParam_eq, Level.hasParam'] + simp [TypeChecker.Inner.checkLevel, Level.getUndefParam, Level.forEach, Level.hasParam_eq, + Level.hasParam'] rfl @[simp] private theorem annotatedPiRecMGet (methods context state) : @@ -3293,9 +3290,8 @@ private theorem annotatedPiFamily_checkTypeInner : .ok (.sort (.succ (.succ .zero)), annotatedPiFamilyCheckTypeState) unfold TypeChecker.Inner.inferType' - simp [annotatedPiFamilyCheckTypeState, annotatedPiInfo, - Expr.hasLooseBVars, Expr.looseBVarRange', Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + simp [annotatedPiFamilyCheckTypeState, Expr.hasLooseBVars, Expr.looseBVarRange', Bind.bind, + ReaderT.bind, StateT.bind, Except.bind] private theorem annotatedPiFamily_checkTypeM : TypeChecker.M.run annotatedPiFamilyCandidateContext.env @@ -3358,20 +3354,12 @@ private theorem annotatedPiCtor_checkTypeM : ({} : TypeChecker.State)) = .ok (.sort (.succ .zero)) unfold TypeChecker.Inner.inferType' - simp [Expr.hasLooseBVars, Expr.looseBVarRange', - Expr.eqv_eq, Std.HashMap.getElem?_insert, - TypeChecker.Inner.inferType', - TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, - TypeChecker.Inner.inferApp, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.hasLooseBVars, Expr.looseBVarRange', TypeChecker.Inner.inferType', + TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, Bind.bind, ReaderT.bind, + StateT.bind, Except.bind] rw [annotatedPiIsDefEqSort 9997] - simp [annotatedPiOutParamFnType, annotatedPiOutParamArgState, - annotatedPiOutParamFnState, Expr.bindingBody!, - Expr.instantiate1_eq, Expr.instantiate1', - annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, - AddInductive.Context.toTypeChecker, - Std.HashMap.getElem?_insert, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.instantiate1', annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, + AddInductive.Context.toTypeChecker, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [annotatedPiInferTypeFamilyCached (hcache := by apply annotatedPiFamilyCacheAfterForall)] simp [Expr.sortLevel!, annotatedPi_mkLevelIMaxSuccZero] @@ -3942,16 +3930,10 @@ private theorem checkTypeAliasFormerCandidate : (.sort (.succ .zero)) .default) := by unfold TypeChecker.Inner.inferConstant rw [aliasRecNormalization_getRecAlias] - simp [recAliasInfo, recAliasKernelDef, - Bind.bind, Except.bind, - normalizationExceptPure, - aliasRecNormalization_checkLevelSuccZero, - ConstantInfo.levelParams, ConstantInfo.isUnsafe, - ConstantInfo.instantiateTypeLevelParams, - ConstantInfo.toConstantVal, - ConstantVal.instantiateTypeLevelParams, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', - Level.substParams'] + simp [recAliasInfo, recAliasKernelDef, Bind.bind, Except.bind, normalizationExceptPure, + ConstantInfo.levelParams, ConstantInfo.isUnsafe, ConstantInfo.instantiateTypeLevelParams, + ConstantInfo.toConstantVal, ConstantVal.instantiateTypeLevelParams, + Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', Level.substParams'] @[simp] private theorem inferConstantAliasRec : TypeChecker.Inner.inferConstant aliasRecNormalizationRawContext @@ -4035,16 +4017,11 @@ private theorem unfoldTypeFamilyAlias (methods state) : TypeChecker.Inner.unfoldDefinitionCore (.const ``TypeFamilyAlias []) methods aliasFormerNormalizationRawContext state = .ok (some (.sort (.succ .zero)), state) - simp [TypeChecker.Inner.unfoldDefinitionCore, TypeChecker.Inner.isDelta, - Expr.getAppFn, aliasFormerNormalizationRawContext, - aliasFormerNormalization_lookup, Bind.bind, ReaderT.bind, - StateT.bind, Except.bind, typeFamilyAliasInfo, - typeFamilyAliasKernelDef, ConstantInfo.deltaValue?, - TypeChecker.Inner.instantiateDeltaValue, - ConstantInfo.numLevelParams, - ConstantInfo.instantiateValueLevelParams!, ConstantInfo.levelParams, - ConstantInfo.value!, ConstantInfo.toConstantVal, - Expr.instantiateLevelParams] + simp [TypeChecker.Inner.unfoldDefinitionCore, TypeChecker.Inner.isDelta, Expr.getAppFn, + aliasFormerNormalizationRawContext, aliasFormerNormalization_lookup, Bind.bind, ReaderT.bind, + StateT.bind, Except.bind, typeFamilyAliasInfo, typeFamilyAliasKernelDef, + ConstantInfo.deltaValue?, TypeChecker.Inner.instantiateDeltaValue, ConstantInfo.numLevelParams, + ConstantInfo.levelParams, ConstantInfo.toConstantVal, Expr.instantiateLevelParams] private theorem unfoldAliasFormer (methods state) : TypeChecker.Inner.unfoldDefinition (.const ``AliasFormer []) @@ -4314,10 +4291,8 @@ private theorem annotatedPiOutParamWhnfKernelExpr_eq : annotatedPiOutParamWhnfKernelExpr = .lam `α (.sort (.succ .zero)) (.bvar 0) .default := by simp [annotatedPiOutParamWhnfKernelExpr, annotationOutParamInfo, - outParamKernelDef, ConstantInfo.instantiateValueLevelParams!, - ConstantInfo.levelParams, ConstantInfo.value!, - ConstantInfo.toConstantVal, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', + ConstantInfo.instantiateValueLevelParams!, ConstantInfo.levelParams, ConstantInfo.value!, + ConstantInfo.toConstantVal, Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', Level.substParams'] private def annotatedPiOutParamUnfoldState (state : TypeChecker.State) : @@ -4394,8 +4369,7 @@ private theorem annotatedPiWhnfCoreDomainInitial (n) : .ok (.app (.const ``outParam [.succ .zero]) (.sort .zero), ({} : TypeChecker.State)) unfold TypeChecker.Inner.whnfCore' - simp only [normalizationRecMPure, normalizationRecMBind, - normalizationRecMGet, Std.HashMap.getElem?_empty] + simp only [normalizationRecMBind, normalizationRecMGet, Std.HashMap.getElem?_empty] rw [Expr.withRevApp_eq] simp only [normalizationRecMBind] rw [show @@ -4403,9 +4377,7 @@ private theorem annotatedPiWhnfCoreDomainInitial (n) : (.sort .zero)).getAppFn = .const ``outParam [.succ .zero] by rfl] rw [annotatedPiWhnfCoreOutParamConst n ({} : TypeChecker.State)] - simp [annotatedPiRawDomainKernel, annotatedPiReduceRecursorDomain, - Expr.structuralEq, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.structuralEq, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [show .app (.const ``outParam [.succ .zero]) (.sort .zero) = annotatedPiRawDomainKernel by rfl] @@ -4419,17 +4391,13 @@ private theorem annotatedPiUnfoldOutParamCoreInitial (methods) : ({} : TypeChecker.State) = .ok (some annotatedPiOutParamWhnfKernelExpr, annotatedPiOutParamUnfoldState {}) := by - simp [TypeChecker.Inner.unfoldDefinitionCore, TypeChecker.Inner.isDelta, - Expr.getAppFn, annotatedPiCtorCandidateContext, - AddInductive.Context.toTypeChecker, annotatedPiType_lookup_outParam, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind, - annotationOutParamInfo, outParamKernelDef, ConstantInfo.deltaValue?, - TypeChecker.Inner.instantiateDeltaValue, - ConstantInfo.numLevelParams, - ConstantInfo.instantiateValueLevelParams!, ConstantInfo.levelParams, - ConstantInfo.value!, ConstantInfo.toConstantVal, - Expr.instantiateLevelParams, annotatedPiOutParamWhnfKernelExpr, - annotatedPiOutParamUnfoldState] + simp [TypeChecker.Inner.unfoldDefinitionCore, TypeChecker.Inner.isDelta, Expr.getAppFn, + annotatedPiCtorCandidateContext, AddInductive.Context.toTypeChecker, + annotatedPiType_lookup_outParam, Bind.bind, ReaderT.bind, StateT.bind, Except.bind, + annotationOutParamInfo, ConstantInfo.deltaValue?, TypeChecker.Inner.instantiateDeltaValue, + ConstantInfo.numLevelParams, ConstantInfo.instantiateValueLevelParams!, + ConstantInfo.levelParams, ConstantInfo.value!, ConstantInfo.toConstantVal, + Expr.instantiateLevelParams, annotatedPiOutParamWhnfKernelExpr, annotatedPiOutParamUnfoldState] private theorem annotatedPiUnfoldDomainInitial (methods) : TypeChecker.Inner.unfoldDefinition annotatedPiRawDomainKernel @@ -4498,8 +4466,7 @@ private theorem annotatedPiWhnfCoreDomainBeta (n) : rw [annotatedPiDomainBetaKernel, annotatedPiOutParamWhnfKernelExpr_eq] unfold TypeChecker.Inner.whnfCore' - simp only [normalizationRecMPure, normalizationRecMBind, - normalizationRecMGet, annotatedPiOutParamUnfoldState, + simp only [normalizationRecMBind, normalizationRecMGet, annotatedPiOutParamUnfoldState, Std.HashMap.getElem?_empty] rw [Expr.withRevApp_eq] simp only [normalizationRecMBind] @@ -4513,15 +4480,10 @@ private theorem annotatedPiWhnfCoreDomainBeta (n) : (Expr.app (.lam `α (.sort (.succ .zero)) (.bvar 0) .default) (.sort .zero)).getAppRevArgs = #[.sort .zero] by rfl] - simp [TypeChecker.Inner.whnfCore'.loop, - TypeChecker.Inner.whnfCore'.loop.cont, - TypeChecker.Inner.whnfCore'.save, - annotatedPiDomainBetaKernel, - annotatedPiOutParamWhnfKernelExpr_eq, - annotatedPiOutParamUnfoldState, annotatedPiDomainBetaState, - Expr.instantiateRange, Expr.instantiateRevRange, - Expr.instantiate1_eq, Expr.instantiate1', Expr.eqv_eq, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [TypeChecker.Inner.whnfCore'.loop, TypeChecker.Inner.whnfCore'.loop.cont, + TypeChecker.Inner.whnfCore'.save, annotatedPiDomainBetaKernel, + annotatedPiOutParamWhnfKernelExpr_eq, annotatedPiDomainBetaState, Expr.instantiate1', Bind.bind, + ReaderT.bind, StateT.bind, Except.bind] @[simp] private theorem annotatedPiReduceNativeDomain (env methods state) : @@ -4556,21 +4518,21 @@ private theorem annotatedPiWhnfLoopDomain : rw [show 9999 = 9998 + 1 by rfl] simp only [normalizationRecMBind, normalizationRecMGetEnv] rw [annotatedPiWhnfCoreDomainInitial] - simp only [normalizationRecMBind] + simp only [] rw [annotatedPiReduceNativeDomain] - simp only [normalizationRecMBind, normalizationRecMPure] + simp only [normalizationRecMBind] rw [annotatedPiReduceNatDomain] - simp only [normalizationRecMBind, normalizationRecMPure] + simp only [normalizationRecMBind] rw [annotatedPiUnfoldDomainInitial] - simp only [normalizationRecMBind, normalizationRecMPure] + simp only [] unfold TypeChecker.Inner.whnf'.loop simp only [normalizationRecMBind, normalizationRecMGetEnv] rw [annotatedPiWhnfCoreDomainBeta] - simp only [normalizationRecMBind] + simp only [] rw [normalizationReduceNativeSort] - simp only [normalizationRecMBind, normalizationRecMPure] + simp only [normalizationRecMBind] rw [normalizationReduceNatSort] - simp only [normalizationRecMBind, normalizationRecMPure] + simp only [normalizationRecMBind] rw [normalizationUnfoldSort] rfl @@ -4608,14 +4570,10 @@ private theorem annotatedPiDomain_checkTypeM : ({} : TypeChecker.State)) = .ok (.sort (.succ .zero)) unfold annotatedPiRawDomainKernel TypeChecker.Inner.inferType' - simp [Expr.hasLooseBVars, Expr.looseBVarRange', - TypeChecker.Inner.inferType', TypeChecker.Inner.inferApp, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.hasLooseBVars, Expr.looseBVarRange', TypeChecker.Inner.inferType', Bind.bind, + ReaderT.bind, StateT.bind, Except.bind] rw [annotatedPiIsDefEqSort 9999] - simp [annotatedPiOutParamFnType, annotatedPiOutParamArgState, - annotatedPiOutParamFnState, Expr.bindingBody!, - Expr.instantiate1_eq, Expr.instantiate1', - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rfl private theorem annotatedPiDomain_whnfM : @@ -4682,11 +4640,8 @@ private theorem annotatedPiEmptyEqv_isEquivDomainSort : · 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, - EquivManager.merge, hroot] + simp [annotatedPiRawDomainKernel, Expr.isBVar, annotatedPiApp_beq_sort, StateT.pure, pure, + Bind.bind, StateT.bind, EquivManager.toNode, EquivManager.find, hroot] private theorem annotatedPiQuickIsDefEqDomainInitial (methods : TypeChecker.Methods) @@ -4705,11 +4660,9 @@ private theorem annotatedPiQuickIsDefEqDomainInitial 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, ReaderT.pure, StateT.pure, - Except.pure, hq', Bind.bind, ReaderT.bind, StateT.bind, - Except.bind] + 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, @@ -4746,9 +4699,7 @@ private theorem annotatedPiWhnfCoreDomainCheap .ok (.app (.const ``outParam [.succ .zero]) (.sort .zero), ({ eqvManager := m } : TypeChecker.State)) unfold TypeChecker.Inner.whnfCore' - simp only [normalizationRecMPure, normalizationRecMBind, - normalizationRecMGet, annotatedPiWithEqvManager, - Std.HashMap.getElem?_empty] + simp only [normalizationRecMBind, normalizationRecMGet, Std.HashMap.getElem?_empty] rw [Expr.withRevApp_eq] simp only [normalizationRecMBind] rw [show @@ -4756,9 +4707,7 @@ private theorem annotatedPiWhnfCoreDomainCheap (.sort .zero)).getAppFn = .const ``outParam [.succ .zero] by rfl] rw [annotatedPiWhnfCoreOutParamConstCheap fuel] - simp [annotatedPiRawDomainKernel, annotatedPiReduceRecursorDomain, - annotatedPiWithEqvManager, Expr.structuralEq, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.structuralEq, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [show .app (.const ``outParam [.succ .zero]) (.sort .zero) = annotatedPiRawDomainKernel by rfl] @@ -4775,15 +4724,10 @@ private theorem annotatedPiWhnfCoreDomainCheap AddInductive.Context.toTypeChecker] rw [show annotatedPiTypeKernelEnv.get ``outParam = .ok annotationOutParamInfo by exact annotatedPiType_get_outParam] - simp [annotatedPiCtorCandidateContext, - AddInductive.Context.toTypeChecker, annotationOutParamInfo, - annotatedPiOutParamFnType, Bind.bind, Except.bind, - annotatedPiExceptPure, ConstantInfo.levelParams, - ConstantInfo.instantiateTypeLevelParams, - ConstantInfo.toConstantVal, - ConstantVal.instantiateTypeLevelParams, - Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', - Level.substParams'] + simp [annotationOutParamInfo, annotatedPiOutParamFnType, Bind.bind, Except.bind, + annotatedPiExceptPure, ConstantInfo.levelParams, ConstantInfo.instantiateTypeLevelParams, + ConstantInfo.toConstantVal, ConstantVal.instantiateTypeLevelParams, + Expr.instantiateLevelParams_eq, Expr.instantiateLevelParamsCore', Level.substParams'] private def annotatedPiOutParamInferOnlyState (m : EquivManager) : TypeChecker.State := @@ -4828,9 +4772,7 @@ private theorem annotatedPiInferAppDomainOnly #[.sort .zero] by rfl] simp only [normalizationRecMBind] rw [annotatedPiInferTypeOutParamOnly fuel] - simp [TypeChecker.Inner.inferApp.loop, - annotatedPiOutParamFnType, Expr.instantiateRevRange, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [TypeChecker.Inner.inferApp.loop, annotatedPiOutParamFnType] private def annotatedPiDomainInferOnlyState (m : EquivManager) : TypeChecker.State := @@ -4863,9 +4805,7 @@ private theorem annotatedPiInferTypeDomainOnlyAny .app (.const ``outParam [.succ .zero]) (.sort .zero) = annotatedPiRawDomainKernel by rfl] rw [annotatedPiInferAppDomainOnly fuel] - simp [annotatedPiDomainInferOnlyState, - annotatedPiOutParamInferOnlyState, Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + simp [annotatedPiOutParamInferOnlyState] private theorem annotatedPiInferTypeDomainOnly998 (m : EquivManager) : @@ -4889,9 +4829,7 @@ private theorem annotatedPiInferTypeDomainOnly998 .ok (.sort (.succ .zero), annotatedPiOutParamInferOnlyState m) by simpa only [Nat.reduceAdd] using annotatedPiInferAppDomainOnly 9996 m] - simp [annotatedPiDomainInferOnlyState, - annotatedPiOutParamInferOnlyState, Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + simp [annotatedPiOutParamInferOnlyState] private def annotatedPiSortOneInferOnlyState (m : EquivManager) : TypeChecker.State := @@ -4903,8 +4841,7 @@ private def annotatedPiSortOneInferOnlyState (m : EquivManager) : (annotatedPiDomainInferOnlyState m).inferTypeI[ (.sort (.succ .zero) : Expr)]? = none := by - simp [annotatedPiDomainInferOnlyState, annotatedPiRawDomainKernel, - annotatedPiOutParamFnType, Expr.eqv_eq] + simp [annotatedPiDomainInferOnlyState, annotatedPiRawDomainKernel, annotatedPiOutParamFnType] private theorem annotatedPiInferTypeSortOneOnly (fuel : Nat) (m : EquivManager) : @@ -4958,7 +4895,7 @@ private theorem annotatedPiIsDefEqProofIrrelDomain unfold TypeChecker.Inner.isDefEqProofIrrel simp only [normalizationRecMBind] rw [annotatedPiInferTypeDomainOnlyAny fuel] - simp only [normalizationRecMBind] + simp only [] rw [annotatedPiIsPropSortOneFalse fuel] rfl @@ -5056,10 +4993,8 @@ private theorem annotatedPiWhnfCoreDomainBetaCheap rw [annotatedPiDomainBetaKernel, annotatedPiOutParamWhnfKernelExpr_eq] unfold TypeChecker.Inner.whnfCore' - simp only [normalizationRecMPure, normalizationRecMBind, - normalizationRecMGet, annotatedPiOutParamUnfoldState, - annotatedPiSortOneInferOnlyState, - annotatedPiDomainInferOnlyState, Std.HashMap.getElem?_empty] + simp only [normalizationRecMBind, normalizationRecMGet, annotatedPiOutParamUnfoldState, + annotatedPiSortOneInferOnlyState, annotatedPiDomainInferOnlyState, Std.HashMap.getElem?_empty] rw [Expr.withRevApp_eq] simp only [normalizationRecMBind] rw [show @@ -5072,16 +5007,8 @@ private theorem annotatedPiWhnfCoreDomainBetaCheap (Expr.app (.lam `α (.sort (.succ .zero)) (.bvar 0) .default) (.sort .zero)).getAppRevArgs = #[.sort .zero] by rfl] - simp [TypeChecker.Inner.whnfCore'.loop, - TypeChecker.Inner.whnfCore'.loop.cont, - TypeChecker.Inner.whnfCore'.save, - annotatedPiDomainBetaKernel, - annotatedPiOutParamWhnfKernelExpr_eq, - annotatedPiOutParamUnfoldState, - annotatedPiSortOneInferOnlyState, - annotatedPiDomainInferOnlyState, - Expr.instantiateRange, Expr.instantiateRevRange, - Expr.instantiate1_eq, Expr.instantiate1', Expr.eqv_eq, + simp [TypeChecker.Inner.whnfCore'.loop, TypeChecker.Inner.whnfCore'.loop.cont, + TypeChecker.Inner.whnfCore'.save, annotatedPiOutParamWhnfKernelExpr_eq, Expr.instantiate1', Bind.bind, ReaderT.bind, StateT.bind, Except.bind] private theorem annotatedPiQuickIsDefEqSortZeroAny @@ -5100,13 +5027,10 @@ private theorem annotatedPiQuickIsDefEqSortZeroAny 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', Level.isStructEq, - Bind.bind, ReaderT.bind, StateT.bind, - Except.bind] + 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] private theorem annotatedPiIsDeltaDomain : TypeChecker.Inner.isDelta annotatedPiTypeKernelEnv @@ -5203,9 +5127,8 @@ private theorem annotatedPiLazyDeltaStepDomain .app (.const ``outParam [.succ .zero]) (.sort .zero) by rfl] exact annotatedPiApp_beq_const _ _ _ _ unfold TypeChecker.Inner.isDefEqOffset - simp [TypeChecker.Inner.isNatZero, - TypeChecker.Inner.isNatSuccOf?, annotatedPiRawDomainKernel, - Expr.natZero, Bind.bind] + simp [TypeChecker.Inner.isNatZero, TypeChecker.Inner.isNatSuccOf?, annotatedPiRawDomainKernel, + Expr.natZero] private theorem annotatedPiLazyDeltaLoopDomain (fuel : Nat) (m : EquivManager) : @@ -5302,11 +5225,9 @@ private theorem annotatedPiQuickIsDefEqDomainAny 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, ReaderT.pure, StateT.pure, - Except.pure, hq', - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + 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, @@ -5431,8 +5352,7 @@ private theorem annotatedPiDomain_isDefEqInner rw [show (annotatedPiRawDomainKernel == (.sort .zero : Expr)) = false by exact annotatedPiApp_beq_sort _ _ _] - simp only [Bool.false_eq_true, if_false, pure_bind, - normalizationRecMBind] + simp only [Bool.false_eq_true, if_false, normalizationRecMBind] rw [hcore'] exact ⟨_, rfl⟩ @@ -5484,20 +5404,12 @@ private theorem annotatedPiInner_checkTypeM : ({} : TypeChecker.State)) = .ok (.sort (.succ .zero)) unfold annotatedPiInnerKernel TypeChecker.Inner.inferType' - simp [annotatedPiRawDomainKernel, - Expr.hasLooseBVars, Expr.looseBVarRange', - TypeChecker.Inner.inferType', - TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, - TypeChecker.Inner.inferApp, + simp [annotatedPiRawDomainKernel, Expr.hasLooseBVars, Expr.looseBVarRange', + TypeChecker.Inner.inferType', TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [annotatedPiIsDefEqSort 9998] - simp [annotatedPiOutParamFnType, annotatedPiOutParamArgState, - annotatedPiOutParamFnState, Expr.bindingBody!, - Expr.instantiate1_eq, Expr.instantiate1', - annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, - AddInductive.Context.toTypeChecker, - Std.HashMap.getElem?_insert, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [Expr.instantiate1', annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, + AddInductive.Context.toTypeChecker, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] simp [Expr.sortLevel!, annotatedPi_mkLevelIMaxSuccZero] rfl @@ -5926,8 +5838,7 @@ private theorem annotatedPiFamilyEnv_not_contains : private theorem annotatedPiFamilyEnv_checkName : outParamKernelEnv.checkName ``AnnotatedPi false = .ok () := by simp [Kernel.Environment.checkName, annotatedPiFamilyEnv_not_contains, - Kernel.Environment.primitives, NameSet.ofList, NameSet.contains, - Bind.bind, Except.bind, Pure.pure, Except.pure] + Kernel.Environment.primitives, NameSet.ofList, NameSet.contains, Pure.pure, Except.pure] private theorem annotatedPiInner_hasIndOcc : AddInductive.hasIndOcc #[.const ``AnnotatedPi []] @@ -6134,10 +6045,8 @@ private theorem annotatedPiInner_inferTypeInner : TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [annotatedPiInferTypeDomainOnly998] - simp only [TypeChecker.Inner.ensureSortCore, Expr.isSort, - ↓reduceIte, annotatedPiWithLocalDecl, Expr.instantiate1', - annotatedPiRecMPure, Bind.bind, ReaderT.bind, - StateT.bind, Except.bind] + simp only [TypeChecker.Inner.ensureSortCore, Expr.isSort, ↓reduceIte, annotatedPiWithLocalDecl, + annotatedPiRecMPure, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [annotatedPiInferTypeFamilyAfterDomainOnly_literal] simp [Expr.sortLevel!, annotatedPiInnerInferOnlyFinalState, annotatedPiInnerKernel, annotatedPiRawDomainKernel] @@ -6247,8 +6156,7 @@ private theorem annotatedPi_checkPositivity_terminal : (TypeChecker.whnf (.const ``AnnotatedPi [])) = .ok (.const ``AnnotatedPi []) by exact annotatedPiConst_whnfM _] - simp [annotatedPiConst_hasIndOcc, annotatedPiConst_isValidIndApp, - Bind.bind, ReaderT.bind, ReaderT.pure, Pure.pure, + simp [annotatedPiConst_hasIndOcc, annotatedPiConst_isValidIndApp, ReaderT.pure, Pure.pure, Except.bind, Except.pure] private theorem annotatedPi_checkPositivity : @@ -6256,8 +6164,7 @@ private theorem annotatedPi_checkPositivity : annotatedPiInnerKernel annotatedPiMkInfo.name 0 annotatedPiCtorCandidateContext = .ok () := by unfold AddInductive.checkPositivity - simp only [readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, + simp only [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, Pure.pure, Except.bind, Except.pure] rw [show annotatedPiCtorCandidateContext.fuel.inductiveFuel = 999 + 1 by rfl] @@ -6269,17 +6176,13 @@ private theorem annotatedPi_checkPositivity : rw [show AddInductive.hasIndOcc annotatedPiInductiveStats.indConsts annotatedPiInnerKernel = true by exact annotatedPiInner_stats_hasIndOcc] - simp only [Bool.not_true, Bool.false_eq_true, if_false, - ReaderT.pure, Pure.pure, ReaderT.bind, Bind.bind, - Except.bind, Except.pure] + simp only [Bool.not_true, Bool.false_eq_true, if_false, Pure.pure] unfold annotatedPiInnerKernel simp only rw [show AddInductive.hasIndOcc annotatedPiInductiveStats.indConsts annotatedPiRawDomainKernel = false by exact annotatedPiRawDomain_hasIndOcc_false] - simp only [Bool.false_eq_true, if_false, Expr.instantiate1', - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [Bool.false_eq_true, if_false] simpa [withLocalDecl, annotatedPiInnerBodyCandidateContext, withFreshId, MonadLocalNameGenerator.withFreshId, MonadWithReader.withReader, withTheReader, @@ -6446,22 +6349,17 @@ private theorem annotatedPi_checkConstructors : rw [annotatedPiCtor_getEnvM] simp only [Except.bind] unfold AddInductive.checkConstructorsLoop AddInductive.checkConstructorFold - simp +decide [annotatedPiKernelType, annotatedPiKernelCtor, - annotatedPiMkInfo, ConstantInfo.name, ConstantInfo.type, - ConstantInfo.toConstantVal, NameSet.contains] + simp +decide [annotatedPiKernelType, annotatedPiKernelCtor, annotatedPiMkInfo, ConstantInfo.name, + ConstantInfo.type, ConstantInfo.toConstantVal] rw [annotatedPiCtor_noMVarNoFVar_expanded] - simp only [ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [ReaderT.bind, Bind.bind, Except.bind] rw [AddInductive.withEmptyLocalContext_apply] rw [AddInductive.liftTypeChecker_apply] simp only rw [annotatedPiCtor_checkTypeM_empty] - simp only [Except.bind] + simp only [] unfold AddInductive.checkConstructorType - simp +decide [ConstantInfo.type, ConstantInfo.toConstantVal, - AddInductive.liftTypeChecker_apply, - readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, + simp +decide [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, Pure.pure, Except.bind, Except.pure] rw [show annotatedPiCtorCandidateContext.fuel.inductiveFuel = 999 + 1 by rfl] @@ -6476,24 +6374,15 @@ private theorem annotatedPi_checkConstructors : rw [if_pos (show AddInductive.levelStructGe annotatedPiInductiveStats.resultLevel (Expr.sort (.succ .zero)).sortLevel! = true from rfl)] - simp only [Bool.not_false, ↓reduceIte, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp only [Bool.not_false, ↓reduceIte, ReaderT.bind, Bind.bind, Except.bind] rw [annotatedPi_checkPositivity_expanded] - simp only [Except.bind] - simp only [AddInductive.withLocalDecl_apply, - annotatedPiConst_instantiate1, annotatedPiConst_instantiate1', - annotatedPiOuterBodyCandidateContext, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshExpr, AddInductive.Context.freshFVarId, - AddInductive.consumeTypeAnnotations, annotatedPiInnerAnnotations, - annotatedPiInnerKernel, annotatedPiRawDomainKernel, - annotatedPiCtorCandidateContext, - ReaderT.pure, Pure.pure, Except.pure] + simp only [] + simp only [AddInductive.withLocalDecl_apply, annotatedPiConst_instantiate1, + AddInductive.Context.pushLocalDecl, AddInductive.Context.freshFVarId, + AddInductive.consumeTypeAnnotations, annotatedPiCtorCandidateContext] rw [annotatedPi_checkConstructors_terminal_expanded] unfold AddInductive.checkConstructorsLoop AddInductive.checkConstructorFold - simp [ReaderT.pure, Pure.pure, Except.pure, - AddInductive.checkConstructorsLoop] + simp [ReaderT.pure, Pure.pure, Except.pure] private theorem annotatedPi_checkConstructorUniverseSemantics : AddInductive.checkConstructorUniverseListSemantics @@ -6504,8 +6393,7 @@ private theorem annotatedPi_checkConstructorUniverseSemantics : annotatedPiMkInfo, ConstantInfo.type, ConstantInfo.toConstantVal, ReaderT.bind, Bind.bind] unfold AddInductive.checkConstructorUniverseSemantics - simp only [readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, + simp only [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, Pure.pure, Except.bind, Except.pure] rw [show annotatedPiCtorCandidateContext.fuel.inductiveFuel = 999 + 1 by rfl] @@ -6515,16 +6403,8 @@ private theorem annotatedPi_checkConstructorUniverseSemantics : simp only [ReaderT.bind, Bind.bind, AddInductive.liftTypeChecker_apply] rw [annotatedPiInner_ensureTypeM_expanded] simp only [Except.bind] - simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe, - AddInductive.levelStructGe, AddInductive.levelStructEq, Pure.pure] - simp only [AddInductive.withLocalDecl_apply, - annotatedPiConst_instantiate1, annotatedPiConst_instantiate1', - annotatedPiOuterBodyCandidateContext, - AddInductive.Context.pushLocalDecl, - AddInductive.Context.freshExpr, AddInductive.Context.freshFVarId, - AddInductive.consumeTypeAnnotations, annotatedPiInnerAnnotations, - annotatedPiInnerKernel, annotatedPiRawDomainKernel, - annotatedPiCtorCandidateContext] + simp [Expr.sortLevel!, AddInductive.constructorUniverseSemanticGe] + simp only [AddInductive.consumeTypeAnnotations, annotatedPiCtorCandidateContext] unfold AddInductive.checkConstructorUniverseSemantics.loop rfl @@ -6702,7 +6582,7 @@ theorem annotatedPiFamily_candidateTrace : · decide · rfl -private def annotatedPiFamilyTypeListProduced : +private theorem annotatedPiFamilyTypeListProduced : AddInductive.CandidateFamilyTypeListProduced annotatedPiFamilyCandidateContext (.cons annotatedPiFamilyListCandidate.familyType .nil) := by @@ -6719,7 +6599,7 @@ private theorem annotatedPiFamilyTypeList_candidateTrace : .ok (.cons annotatedPiFamilyListCandidate.familyType .nil) := by exact annotatedPiFamilyTypeListProduced.normalize -private def annotatedPiConstructorListProduced : +private theorem annotatedPiConstructorListProduced : AddInductive.CandidateConstructorListProduced annotatedPiCtorCandidateContext annotatedPiFamilyListCandidate.constructors := by @@ -6736,7 +6616,7 @@ private theorem annotatedPiConstructorList_candidateTrace : .ok annotatedPiFamilyListCandidate.constructors := by exact annotatedPiConstructorListProduced.normalize -private def annotatedPiFamilyListProduced : +private theorem annotatedPiFamilyListProduced : AddInductive.CandidateFamilyListProduced annotatedPiCtorCandidateContext (.cons annotatedPiFamilyListCandidate.familyType .nil) @@ -6941,10 +6821,8 @@ private theorem aliasFormerNormalization_not_contains : private theorem aliasFormerNormalization_checkName : aliasFormerNormalizationKernelEnv.checkName ``AliasFormer false = .ok () := by - simp [Kernel.Environment.checkName, - aliasFormerNormalization_not_contains, - Kernel.Environment.primitives, NameSet.ofList, NameSet.contains, - Bind.bind, Except.bind, Pure.pure, Except.pure] + simp [Kernel.Environment.checkName, aliasFormerNormalization_not_contains, + Kernel.Environment.primitives, NameSet.ofList, NameSet.contains, Pure.pure, Except.pure] private theorem aliasFormer_declareInductiveTypes : AddInductive.declareInductiveTypes aliasFormerInductiveStats 0 @@ -7036,23 +6914,16 @@ private theorem aliasFormer_checkConstructors : rw [aliasFormerCtor_getEnvM] simp only [Except.bind] unfold AddInductive.checkConstructorsLoop AddInductive.checkConstructorFold - simp +decide [aliasFormerKernelType, aliasFormerKernelCtor, - aliasFormerMkInfo, ConstantInfo.name, NameSet.contains] - simp +decide [ConstantInfo.type, - ConstantInfo.toConstantVal, - AddInductive.liftTypeChecker_apply, - aliasFormerCtor_noMVarNoFVar, - readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, - Except.bind, Except.pure] + simp +decide [aliasFormerKernelType, aliasFormerKernelCtor, aliasFormerMkInfo, ConstantInfo.name] + simp +decide [ConstantInfo.type, ConstantInfo.toConstantVal, AddInductive.liftTypeChecker_apply, + aliasFormerCtor_noMVarNoFVar, ReaderT.bind, Bind.bind, Except.bind] rw [aliasFormerCtor_checkTypeM_of_empty ({ decls := { root := PersistentArrayNode.node #[], tail := #[] } } : LocalContext) rfl] - simp only [Except.bind] + simp only [] unfold AddInductive.checkConstructorType - simp only [readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, + simp only [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, Pure.pure, Except.bind, Except.pure] rw [show aliasFormerCtorCandidateContext.fuel.inductiveFuel = 999 + 1 by rfl] @@ -7070,8 +6941,7 @@ private theorem aliasFormer_checkConstructorUniverseSemantics : aliasFormerMkInfo, ConstantInfo.type, ConstantInfo.toConstantVal, ReaderT.bind, Bind.bind] unfold AddInductive.checkConstructorUniverseSemantics - simp only [readThe, MonadReaderOf.read, ReaderT.read, - ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, + simp only [readThe, MonadReaderOf.read, ReaderT.read, ReaderT.bind, Bind.bind, Pure.pure, Except.bind, Except.pure] rw [show aliasFormerCtorCandidateContext.fuel.inductiveFuel = 999 + 1 by rfl] @@ -7088,7 +6958,7 @@ theorem aliasFormerFamily_candidateTrace : · decide · rfl -private def aliasFormerFamilyTypeListProduced : +private theorem aliasFormerFamilyTypeListProduced : AddInductive.CandidateFamilyTypeListProduced aliasFormerCandidateContext (.cons aliasFormerFamilyListCandidate.familyType .nil) := by exact .cons (by @@ -7114,7 +6984,7 @@ theorem aliasFormerCtor_candidateTrace : · decide · rfl -private def aliasFormerConstructorListProduced : +private theorem aliasFormerConstructorListProduced : AddInductive.CandidateConstructorListProduced aliasFormerCtorCandidateContext aliasFormerFamilyListCandidate.constructors := by @@ -7131,7 +7001,7 @@ private theorem aliasFormerConstructorList_candidateTrace : .ok aliasFormerFamilyListCandidate.constructors := by exact aliasFormerConstructorListProduced.normalize -private def aliasFormerFamilyListProduced : +private theorem aliasFormerFamilyListProduced : AddInductive.CandidateFamilyListProduced aliasFormerCtorCandidateContext (.cons aliasFormerFamilyListCandidate.familyType .nil) aliasFormerNormalizationCandidate.families := by @@ -7316,8 +7186,7 @@ theorem aliasRecField_checkType : .ok (.sort (.succ .zero), state) rw [aliasRecFieldKernelExpr_eq] unfold TypeChecker.Inner.inferType' - simp only [aliasRecField_noLooseBVars, Bool.false_eq_true, if_false, cond, - normalizationRecMPure, normalizationRecMGet, + simp only [aliasRecField_noLooseBVars, Bool.false_eq_true, if_false, cond, normalizationRecMGet, Std.HashMap.getElem?_empty, normalizationRecMBind] rw [inferTypeRecAliasInitial] simp only @@ -7379,7 +7248,7 @@ def aliasFormerFamilyCheckTypeRun : /-- Recursive semantic interpretation of the exact source-indexed candidate trace. This terminal fixture is the base case used by the generic Pi interpreter for larger metadata. -/ -private def aliasFormerFamilyCandidateRun : +private theorem aliasFormerFamilyCandidateRun : TypeChecker.CandidateExprRun typeFamilyAliasEnv [] aliasFormerFamilyCandidate.trace [] aliasFormerRawType.type aliasFormerViewType.type @@ -7475,13 +7344,11 @@ private def aliasFormerFamilyStage : (s := ({} : ConstMap)) SMap.WF.empty] at h by_cases hAliasFormer : ``AliasFormer = name · subst name - simp [SMap.find?, aliasFormerInfo, typeFamilyAliasInfo] at h + simp [aliasFormerInfo] at h · by_cases hTypeFamilyAlias : ``TypeFamilyAlias = name · subst name - simp [hAliasFormer, SMap.find?, aliasFormerInfo, - typeFamilyAliasInfo] at h - · simp [hAliasFormer, hTypeFamilyAlias, SMap.find?, aliasFormerInfo, - typeFamilyAliasInfo] at h + simp [hAliasFormer, typeFamilyAliasInfo] at h + · simp [hAliasFormer, hTypeFamilyAlias, SMap.find?] at h structureEtaReady := StructureEtaReady.of_no_ctorInfo <| by intro name _info h change aliasFormerTypeMap.find?' name = some (.ctorInfo _info) at h @@ -7491,13 +7358,11 @@ private def aliasFormerFamilyStage : (s := ({} : ConstMap)) SMap.WF.empty] at h by_cases hAliasFormer : ``AliasFormer = name · subst name - simp [SMap.find?, aliasFormerInfo, typeFamilyAliasInfo] at h + simp [aliasFormerInfo] at h · by_cases hTypeFamilyAlias : ``TypeFamilyAlias = name · subst name - simp [hAliasFormer, SMap.find?, aliasFormerInfo, - typeFamilyAliasInfo] at h - · simp [hAliasFormer, hTypeFamilyAlias, SMap.find?, aliasFormerInfo, - typeFamilyAliasInfo] at h + simp [hAliasFormer, typeFamilyAliasInfo] at h + · simp [hAliasFormer, hTypeFamilyAlias, SMap.find?] at h family_lctx_eq := rfl constructorContext_eq := rfl quotInit_eq := rfl @@ -7570,7 +7435,7 @@ private def aliasFormerCtorCandidateNodeRun : aliasFormerCtorCheckTypeRun.expr_tr 10000 9999 (by rfl) (by rfl) -private def aliasFormerCtorCandidateRun : +private theorem aliasFormerCtorCandidateRun : TypeChecker.CandidateExprRun aliasFormerTypeEnv [] aliasFormerCtorCandidate.trace [] aliasFormerRawType.ctors[0].type @@ -7613,13 +7478,13 @@ theorem aliasFormerFamily_isType_checked : typeFamilyAliasEnv.IsType 0 [] aliasFormerRawType.type := aliasFormerFamilyCheckTypeRun.isType -private def aliasFormerFamilySpineRun : +private theorem aliasFormerFamilySpineRun : TypeChecker.CandidateExprSpineRun typeFamilyAliasEnv [] aliasFormerFamilyCandidate aliasFormerRawType.type aliasFormerViewType.type := aliasFormerFamilySemanticRootRun.spine rfl -private def aliasFormerCtorSpineRun : +private theorem aliasFormerCtorSpineRun : TypeChecker.CandidateExprSpineRun aliasFormerTypeEnv [] aliasFormerCtorCandidate aliasFormerRawType.ctors[0].type aliasFormerRawType.ctors[0].type := @@ -7699,7 +7564,7 @@ theorem aliasRecField_hasType_checked : aliasRecRawField (.sort (.succ .zero)) := aliasRecFieldCheckTypeRun.hasType -private def aliasRecFieldEvidenceBase : +private theorem aliasRecFieldEvidenceBase : TypeChecker.DefEqEvidence aliasRecTypeEnv 0 [] aliasRecRawField (.const ``AliasRec []) (.sort (.succ .zero)) := by exact .trans @@ -7708,13 +7573,13 @@ private def aliasRecFieldEvidenceBase : (.refl aliasRecConst_hasType)) (.beta (VEnv.HasType.bvar .zero) aliasRecConst_hasType) -private def aliasRecFieldEvidence : +private theorem aliasRecFieldEvidence : TypeChecker.DefEqEvidence aliasRecTypeEnv 0 [] aliasRecRawField (.const ``AliasRec []) (.sort (.succ .zero)) := .trans (.refl aliasRecField_hasType_checked) aliasRecFieldEvidenceBase -private def aliasRecCtorEvidence : +private theorem aliasRecCtorEvidence : ∃ A, TypeChecker.DefEqEvidence aliasRecTypeEnv 0 [] aliasRecRawType.ctors[0].type aliasRecViewCtor.type A := by exact ⟨.sort (.imax (.succ .zero) (.succ .zero)), @@ -7795,6 +7660,7 @@ private theorem aliasFormerCtorCandidateContext_empty : aliasFormerCtorCandidateContext.withEmptyLocalContext = aliasFormerCtorCandidateContext := rfl +set_option warn.sorry false in theorem aliasFormerAlignmentRun : aliasFormerStagedUniverseInput.staged.constructorValidation.trace.checkCandidateAlignment aliasFormerNormalizationCandidate.families.singleton.constructors @@ -8482,7 +8348,7 @@ private def annotatedPiFamilyCandidateNodeRun : (TrExprS.sort rfl) 10000 9999 rfl rfl -private def annotatedPiFamilyCandidateRun : +private theorem annotatedPiFamilyCandidateRun : TypeChecker.CandidateExprRun outParamEnv [] annotatedPiFamilyCandidate.trace [] annotatedPiRawType.type annotatedPiRawType.type @@ -8510,7 +8376,7 @@ private def annotatedPiFamilyRootRun : annotatedPiRawType.type := annotatedPiFamilySemanticRootRun.root -private def annotatedPiFamilySpineRun : +private theorem annotatedPiFamilySpineRun : TypeChecker.CandidateExprSpineRun outParamEnv [] annotatedPiFamilyCandidate annotatedPiRawType.type annotatedPiRawType.type := @@ -8654,13 +8520,13 @@ private def annotatedPiInnerAnnotationsRun : rfl rfl rfl annotatedPiCtorCandidateContextRun.state_wf annotatedPiInnerSource_tr annotatedPiInnerSource_tr 10000 rfl -private def annotatedPiDomainCandidateRun : +private theorem annotatedPiDomainCandidateRun : TypeChecker.CandidateExprRun annotatedPiTypeEnv [] annotatedPiDomainCandidateTrace [] annotatedPiRawDomain (.sort .zero) (.sort (.succ .zero)) := .terminal annotatedPiDomainCandidateNodeRun -private def annotatedPiInnerBodyCandidateRun : +private theorem annotatedPiInnerBodyCandidateRun : TypeChecker.CandidateExprRun annotatedPiTypeEnv [] annotatedPiInnerBodyCandidateTrace [(some (annotatedPiCtorCandidateContext.freshFVarId, @@ -8673,7 +8539,7 @@ private def annotatedPiInnerBodyCandidateRun : (TypeChecker.CandidateExprRun.terminal annotatedPiInnerBodyCandidateNodeRun) -private def annotatedPiOuterBodyCandidateRun : +private theorem annotatedPiOuterBodyCandidateRun : TypeChecker.CandidateExprRun annotatedPiTypeEnv [] annotatedPiOuterBodyCandidateTrace [(some (annotatedPiCtorCandidateContext.freshFVarId, @@ -8686,7 +8552,7 @@ private def annotatedPiOuterBodyCandidateRun : (TypeChecker.CandidateExprRun.terminal annotatedPiOuterBodyCandidateNodeRun) -private def annotatedPiInnerCandidateRun : +private theorem annotatedPiInnerCandidateRun : TypeChecker.CandidateExprRun annotatedPiTypeEnv [] annotatedPiInnerCandidateTrace [] annotatedPiRawInner annotatedPiViewInner (.sort (.succ .zero)) := by @@ -8699,7 +8565,7 @@ private def annotatedPiInnerCandidateRun : (annotatedPiFamilyConst_hasType [annotatedPiRawDomain]) (annotatedPiFamilyConst_hasType [annotatedPiRawDomain]) rfl -private def annotatedPiCtorCandidateRun : +private theorem annotatedPiCtorCandidateRun : TypeChecker.CandidateExprRun annotatedPiTypeEnv [] annotatedPiCtorCandidate.trace [] annotatedPiRawType.ctors[0].type annotatedPiViewCtor.type @@ -8743,7 +8609,7 @@ private theorem annotatedPiCtorCandidate_storedSpine : Expr.structuralEq_refl, Bool.true_and] rfl -private def annotatedPiCtorSpineRun : +private theorem annotatedPiCtorSpineRun : TypeChecker.CandidateExprSpineRun annotatedPiTypeEnv [] annotatedPiCtorCandidate annotatedPiRawType.ctors[0].type annotatedPiViewCtor.type := @@ -8946,9 +8812,8 @@ private theorem annotatedPiInnerView_isDefEqForall simp only [Bool.false_eq_true, if_false, pure_bind, normalizationRecMBind] rw [domainRun'] - simp [TypeChecker.Inner.isDefEqForall, TypeChecker.Inner.isDefEq, - Expr.hasLooseBVars, Expr.looseBVarRange', Expr.instantiateRev, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [TypeChecker.Inner.isDefEqForall, TypeChecker.Inner.isDefEq, Expr.hasLooseBVars, + Expr.looseBVarRange'] private theorem annotatedPiInnerView_quickIsDefEq (initial : EquivManager) : @@ -8971,10 +8836,8 @@ private theorem annotatedPiInnerView_quickIsDefEq refine ⟨state, ?_⟩ unfold annotatedPiInnerKernel annotatedPiViewInnerKernel at hq' forallRun ⊢ unfold TypeChecker.Inner.quickIsDefEq - simp [modifyGet, MonadStateOf.modifyGet, monadLift, - MonadLift.monadLift, StateT.modifyGet, pure, ReaderT.pure, - StateT.pure, Except.pure, hq', forallRun, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [modifyGet, MonadStateOf.modifyGet, monadLift, MonadLift.monadLift, StateT.modifyGet, pure, + Except.pure, hq', Bind.bind, ReaderT.bind, StateT.bind, Except.bind] unfold toLBoolM rw [normalizationRecMBind, forallRun] rfl @@ -9018,8 +8881,7 @@ private theorem annotatedPiInnerView_isDefEqInner : (.const ``AnnotatedPi []) .default) = false rw [Expr.eqv_eq] rfl] - simp only [Bool.false_eq_true, if_false, pure_bind, - normalizationRecMBind] + simp only [Bool.false_eq_true, if_false, normalizationRecMBind] rw [coreRun] exact ⟨_, rfl⟩ @@ -9107,12 +8969,9 @@ private theorem annotatedPiViewInnerCheckTypeStep_valid : ({} : TypeChecker.State)) = .ok (.sort (.succ .zero)) unfold annotatedPiViewInnerKernel TypeChecker.Inner.inferType' - simp [Expr.hasLooseBVars, Expr.looseBVarRange', - TypeChecker.Inner.inferType', - TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, - Expr.instantiate1_eq, Expr.instantiate1', - annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, - AddInductive.Context.toTypeChecker, + simp [Expr.hasLooseBVars, Expr.looseBVarRange', TypeChecker.Inner.inferType', + TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, Expr.instantiate1', + annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, AddInductive.Context.toTypeChecker, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] simp [Expr.sortLevel!, annotatedPi_mkLevelIMaxSuccZero] rfl @@ -9137,12 +8996,9 @@ private theorem annotatedPiViewInnerInferType_exists (n : Nat) : some (.sort (.succ .zero)) := by refine ⟨annotatedPiViewInnerFinalState, ?_, ?_⟩ · unfold annotatedPiViewInnerKernel TypeChecker.Inner.inferType' - simp [Expr.hasLooseBVars, Expr.looseBVarRange', - TypeChecker.Inner.inferType', - TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, - Expr.instantiate1_eq, Expr.instantiate1', - annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, - AddInductive.Context.toTypeChecker, + simp [Expr.hasLooseBVars, Expr.looseBVarRange', TypeChecker.Inner.inferType', + TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, Expr.instantiate1', + annotatedPiWithLocalDecl, annotatedPiCtorCandidateContext, AddInductive.Context.toTypeChecker, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] simp [Expr.sortLevel!, annotatedPi_mkLevelIMaxSuccZero] rfl @@ -9216,22 +9072,15 @@ private theorem annotatedPiViewCtorCheckTypeStep_valid : outerState houterCache unfold annotatedPiViewInnerKernel at hfamily unfold annotatedPiViewCtorKernel TypeChecker.Inner.inferType' - simp [annotatedPiViewInnerKernel, - Expr.hasLooseBVars, Expr.looseBVarRange', - TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, - Expr.instantiate1_eq, Expr.instantiate1', - annotatedPiWithLocalDecl, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind] + simp [annotatedPiViewInnerKernel, Expr.hasLooseBVars, Expr.looseBVarRange', + TypeChecker.Inner.inferForall, TypeChecker.Inner.inferForall.loop, Expr.instantiate1', + annotatedPiWithLocalDecl, Bind.bind, ReaderT.bind, StateT.bind, Except.bind] rw [hinner] - simp only [TypeChecker.Inner.ensureSortCore, Expr.isSort, ↓reduceIte, - annotatedPiWithLocalDecl, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp only [TypeChecker.Inner.ensureSortCore, Expr.isSort, ↓reduceIte, Bind.bind, ReaderT.pure, + StateT.pure, Except.pure, Pure.pure] rw [hfamily] - simp [TypeChecker.Inner.ensureSortCore, - Expr.sortLevel!, annotatedPi_mkLevelIMaxSuccZero, - Bind.bind, ReaderT.bind, StateT.bind, Except.bind, - ReaderT.pure, StateT.pure, Except.pure, Pure.pure] + simp [Expr.sortLevel!, annotatedPi_mkLevelIMaxSuccZero, ReaderT.pure, StateT.pure, Except.pure, + Pure.pure] rfl private theorem annotatedPiSortZeroCheckTypeStep_valid : @@ -9968,7 +9817,7 @@ private theorem annotatedPiPreFamilySafetyRun : consumedSortZero.check_eq] simp only [Bind.bind, Except.bind] rw [annotations.observe_eq] - simp only [Bind.bind, Except.bind] + simp only [] rw [dif_pos rootFresh] rw [recursiveTailRun] rfl diff --git a/Lean4Lean/Verify/Environment/Lemmas.lean b/Lean4Lean/Verify/Environment/Lemmas.lean index 571de30c..117080ee 100644 --- a/Lean4Lean/Verify/Environment/Lemmas.lean +++ b/Lean4Lean/Verify/Environment/Lemmas.lean @@ -91,7 +91,7 @@ still available at that step's output boundary. -/ theorem AddInductConstant.map_lookup (H : AddInductConstant kind C₁ env₁ ci C₂ env₂) (wf : C₁.WF) : C₂.find? ci.name = some H.info := by - simpa [H.map_add, wf.find?_insert] + simp [H.map_add, wf.find?_insert] /-- An inductive-metadata insertion preserves every lookup already present in the input map. Freshness rules out the only key at which `insert` could diff --git a/Lean4Lean/Verify/Environment/Normalization.lean b/Lean4Lean/Verify/Environment/Normalization.lean index 9d6e6db2..805b3fb1 100644 --- a/Lean4Lean/Verify/Environment/Normalization.lean +++ b/Lean4Lean/Verify/Environment/Normalization.lean @@ -48,10 +48,10 @@ theorem MLCtx.WF.mono ∀ {context : MLCtx} {Us : List Name}, context.WF env Us → context.WF env' Us | .nil, _, _ => trivial - | .vlam fv name type type' binderInfo tail, Us, + | .vlam _ _ _ _ _ _, _, ⟨tailWF, fresh, type_tr, typeWF⟩ => ⟨tailWF.mono henv, fresh, type_tr.mono henv, typeWF.mono henv⟩ - | .vlet fv name type value type' value' tail, Us, + | .vlet _ _ _ _ _ _ _, _, ⟨tailWF, fresh, type_tr, value_tr, valueWF⟩ => ⟨tailWF.mono henv, fresh, type_tr.mono henv, value_tr.mono henv, valueWF.mono henv⟩ @@ -661,9 +661,7 @@ def CandidateContextRun.pushLocalDecl calc run.context.mlctx.lctx = run.context.lctx := run.context.lctx_eq _ = candidateContext.lctx := by - have h := congrArg (fun c : TypeChecker.Context => c.lctx) - run.context_eq - simpa [AddInductive.Context.toTypeChecker] using h + simp have fresh' : run.context.mlctx.lctx.find? candidateContext.freshFVarId = none := by rw [lctx_eq] @@ -899,7 +897,7 @@ theorem DefEqEvidence.isDefEq : .forallEDF domain.isDefEq body.isDefEq /-- Interpret one paired candidate node as typed definitional equality. -/ -def CandidateNodeRun.evidence +theorem CandidateNodeRun.evidence (run : CandidateNodeRun env Us Δ context source inferred result source' result' inferred') : DefEqEvidence env Us.length Δ.toCtx source' result' inferred' := @@ -1399,7 +1397,7 @@ theorem CandidateExprRun.exists_ofCandidateFVars /-- Fold a complete candidate trace into the compositional equality language consumed by `NormalizationRun` and `GenerationRun`. -/ -def CandidateExprRun.evidence +theorem CandidateExprRun.evidence {env : VEnv} {Us : List Name} {candidateContext : AddInductive.Context} {source : Expr} {trace : AddInductive.CandidateExprTrace candidateContext source} @@ -2012,7 +2010,7 @@ inductive TelResultDefEqEvidence (env : VEnv) (U : Nat) : rawResult viewResult resultType /-- Telescope component of a combined spine/result certificate. -/ -def TelResultDefEqEvidence.telescope : +theorem TelResultDefEqEvidence.telescope : TelResultDefEqEvidence env U Γ rawBinders viewBinders rawResult viewResult resultType → TelDefEqEvidence env U Γ rawBinders viewBinders @@ -2020,7 +2018,7 @@ def TelResultDefEqEvidence.telescope : | .forallE domain tail => .cons domain tail.telescope /-- Terminal component, in the context generated by all raw binders. -/ -def TelResultDefEqEvidence.result : +theorem TelResultDefEqEvidence.result : TelResultDefEqEvidence env U Γ rawBinders viewBinders rawResult viewResult resultType → DefEqEvidence env U (rawBinders.reverse ++ Γ) @@ -2039,7 +2037,7 @@ theorem TelResultDefEqEvidence.length_eq : /-- Reify a Theory telescope equality as explicit checker-produced evidence. This direction is useful after telescope operations such as `take`, `drop`, and context transport have rearranged a candidate certificate. -/ -def TelDefEqEvidence.ofTelDefEq : +theorem TelDefEqEvidence.ofTelDefEq : ∀ {Γ As As'}, env.TelDefEq U Γ As As' → TelDefEqEvidence env U Γ As As' | _, [], [], _ => .nil @@ -2047,21 +2045,21 @@ def TelDefEqEvidence.ofTelDefEq : .cons (.ofDefEq head) (TelDefEqEvidence.ofTelDefEq tail) /-- Retain an exact prefix of a checker-produced telescope certificate. -/ -def TelDefEqEvidence.take +theorem TelDefEqEvidence.take (run : TelDefEqEvidence env U Γ As As') (n : Nat) : TelDefEqEvidence env U Γ (As.take n) (As'.take n) := .ofTelDefEq (run.telDefEq.take n) /-- Transport a checker-produced telescope certificate through environment growth. -/ -def TelDefEqEvidence.mono +theorem TelDefEqEvidence.mono (run : TelDefEqEvidence env U Γ As As') (henv : env ≤ env') : TelDefEqEvidence env' U Γ As As' := .ofTelDefEq (run.telDefEq.mono henv) /-- Combine an independently transformed telescope certificate with its terminal result certificate. -/ -def TelResultDefEqEvidence.ofTelescopeResult +theorem TelResultDefEqEvidence.ofTelescopeResult (tel : TelDefEqEvidence env U Γ rawBinders viewBinders) (result : DefEqEvidence env U (rawBinders.reverse ++ Γ) rawResult viewResult resultType) : @@ -2112,7 +2110,7 @@ The two raw prefixes need not be syntactically equal: both are related to the same checked view prefix. The field telescope and terminal result are then transported through the induced context equality, yielding exactly the mixed raw/view context emitted by generation. -/ -def TelResultDefEqEvidence.replacePrefix +theorem TelResultDefEqEvidence.replacePrefix (henv : VEnv.WF env) (newPrefix : TelDefEqEvidence env U [] newRawPrefix viewPrefix) (run : TelResultDefEqEvidence env U [] @@ -2400,7 +2398,7 @@ theorem CandidateExprRun.spineEvidence /-- Replace only the terminal typing index of a combined certificate. The telescope and both result endpoints remain definitionally unchanged. -/ -def TelResultDefEqEvidence.withResult +theorem TelResultDefEqEvidence.withResult (run : TelResultDefEqEvidence env U Γ rawBinders viewBinders rawResult viewResult resultType) (result : DefEqEvidence env U (rawBinders.reverse ++ Γ) @@ -2416,7 +2414,7 @@ def TelResultDefEqEvidence.withResult /-- Fix a candidate terminal equality at a known type of its right endpoint. This is the bridge from the candidate's checker-inferred type to the precise sort required by dependent inductive analysis. -/ -def TelResultDefEqEvidence.ofRightType +theorem TelResultDefEqEvidence.ofRightType (henv : VEnv.WF env) (hΓ : OnCtx Γ (env.IsType U)) (run : TelResultDefEqEvidence env U Γ rawBinders viewBinders rawResult viewResult resultType) @@ -2749,7 +2747,7 @@ def CandidateExprSpineRun (env : VEnv) (Us : List Name) /-- Retaining the recursive semantic root makes the generation spine a direct projection once the executable structural gate has succeeded. -/ -def CandidateExprSemanticRootRun.spine +theorem CandidateExprSemanticRootRun.spine (run : CandidateExprSemanticRootRun env Us candidate source') (storedSpine : candidate.trace.storedSpine = true) : CandidateExprSpineRun env Us candidate source' run.view := @@ -2759,7 +2757,7 @@ def CandidateExprSemanticRootRun.spine generation-ready spine package. The root equalities transport the recursive run out of the verifier's reconstructed context without choosing a different semantic endpoint. -/ -def CandidateExprRootRun.spineOfIdentity +theorem CandidateExprRootRun.spineOfIdentity {env : VEnv} {Us : List Name} {source : Expr} {candidate : AddInductive.CandidateExpr source} {source' : VExpr} (run : CandidateExprRootRun env Us candidate source' source') @@ -3215,7 +3213,7 @@ def NormalizationCandidateBlockSemanticRun.normalization /-- Project the generic verified normalization run for the same raw block and shared staged environment. -/ -def NormalizationCandidateBlockSemanticRun.normalizationRun +theorem NormalizationCandidateBlockSemanticRun.normalizationRun (run : NormalizationCandidateBlockSemanticRun env blockEnv Us candidate rawDecl) : NormalizationBlockRun run.normalization env blockEnv where @@ -4062,7 +4060,7 @@ structure CandidateFamilyGenerationRun /-- Extract the complete family telescope/result certificate at the exact components consumed by `GenerationRun`. -/ -def CandidateFamilyGenerationRun.evidence +theorem CandidateFamilyGenerationRun.evidence {env : VEnv} {Us : List Name} {kernelSource : InductiveType} {source : VInductDecl} {candidate : AddInductive.NormalizationCandidate [kernelSource]} @@ -4131,7 +4129,7 @@ structure CandidateFamilySemanticGenerationShape /-- Recover the existing family-generation run from the single retained semantic owner. -/ -def CandidateFamilySemanticGenerationRun.run +theorem CandidateFamilySemanticGenerationRun.run (run : CandidateFamilySemanticGenerationRun normalization generation) : CandidateFamilyGenerationRun normalization.root generation where spine := normalization.family.type.spine run.storedSpine @@ -4201,7 +4199,7 @@ structure CandidateConstructorSemanticGenerationShape /-- Project the compatibility constructor run without rebuilding or choosing semantic evidence. -/ -def CandidateSemanticNormalizedCtorRun.run +theorem CandidateSemanticNormalizedCtorRun.run (run : CandidateSemanticNormalizedCtorRun block env Us root ctor) : CandidateNormalizedCtorRun block env Us root.root ctor where raw_eq := run.raw_eq @@ -4237,7 +4235,7 @@ theorem CandidateNormalizedCtorRun.viewTel_eq run.viewResult /-- Extract the stored constructor's declared telescope/result evidence. -/ -def CandidateNormalizedCtorRun.declaredEvidence +theorem CandidateNormalizedCtorRun.declaredEvidence {source : VInductDecl} {generation : GenerationChecked source} {env : VEnv} {Us : List Name} {kernelSource : Constructor} @@ -4307,7 +4305,7 @@ The declared path comes directly from the constructor candidate. The emitted path replaces the stored constructor parameter prefix by the checked family parameter prefix used by Lean's recursor generator, transporting fields and result through the induced definitionally equal context. -/ -def CandidateNormalizedCtorRun.normalizedCtorRun +theorem CandidateNormalizedCtorRun.normalizedCtorRun {source : VInductDecl} {generation : GenerationChecked source} {env : VEnv} {Us : List Name} {kernelSource : Constructor} @@ -4802,7 +4800,7 @@ private theorem candidateFullTelComponents (np n : Nat) (e : VExpr) /-- Derive every family component equation from the minimal structural shape and the exact dependent analyzer result. -/ -private def CandidateFamilySemanticGenerationShape.generationRun +private theorem CandidateFamilySemanticGenerationShape.generationRun {env : VEnv} {Us : List Name} {kernelSource : InductiveType} {source : VInductDecl} {candidate : AddInductive.NormalizationCandidate [kernelSource]} @@ -4861,7 +4859,7 @@ private def CandidateFamilySemanticGenerationShape.generationRun /-- Derive one normalized constructor alignment after its positional raw/view equalities have been recovered from the analyzer-owned pair list. -/ -private def CandidateConstructorSemanticGenerationShape.generationRun +private theorem CandidateConstructorSemanticGenerationShape.generationRun {source : VInductDecl} {generation : GenerationChecked source} {env : VEnv} {Us : List Name} {kernelSource : Constructor} diff --git a/Lean4Lean/Verify/Environment/SingletonParityReplay.lean b/Lean4Lean/Verify/Environment/SingletonParityReplay.lean index 88261d5b..1448d428 100644 --- a/Lean4Lean/Verify/Environment/SingletonParityReplay.lean +++ b/Lean4Lean/Verify/Environment/SingletonParityReplay.lean @@ -115,7 +115,7 @@ theorem replayCtorEnv_ordered07 /-- Reconstruct the precise mixed-generation environment after the family and constructor constants have been inserted. Its recursor certificate is what turns exact kernel recursor metadata into a `TrConstVal`. -/ -def replayGenerationEnv07 +theorem replayGenerationEnv07 {source : VInductDecl} {generation : source.GenerationChecked} {inputEnv typeEnv ctorEnv : VEnv} (generationWF : generation.WF inputEnv) @@ -268,7 +268,7 @@ theorem boolDeclWF07 : boolDecl.WF VEnv.empty := by trivial · exact .nil -def boolGenerationWF07 : boolGenerationChecked.WF VEnv.empty := by +theorem boolGenerationWF07 : boolGenerationChecked.WF VEnv.empty := by exact (boolChecked.wf_of_decl boolDeclWF07).identityGeneration .empty def boolTypeEnv07 : VEnv := @@ -308,7 +308,7 @@ theorem boolCtorEnv_ordered07 : boolCtorEnv07.Ordered := replayCtorEnv_ordered07 boolGenerationWF07 rfl boolTypeEnv_ordered07 rfl -def boolGenerationEnv07 : +theorem boolGenerationEnv07 : VInductDecl.GenerationEnv boolGenerationChecked boolCtorEnv07 := replayGenerationEnv07 boolGenerationWF07 rfl rfl boolCtorEnv_ordered07 @@ -479,7 +479,7 @@ theorem listCheckedWF07 : listChecked.WF VEnv.empty := by · trivial · exact .nil -def listGenerationWF07 : listGenerationChecked.WF VEnv.empty := by +theorem listGenerationWF07 : listGenerationChecked.WF VEnv.empty := by exact listCheckedWF07.identityGeneration .empty def listTypeEnv07 : VEnv := @@ -525,7 +525,7 @@ theorem listCtorEnv_ordered07 : listCtorEnv07.Ordered := replayCtorEnv_ordered07 listGenerationWF07 rfl listTypeEnv_ordered07 rfl -def listGenerationEnv07 : +theorem listGenerationEnv07 : VInductDecl.GenerationEnv listGenerationChecked listCtorEnv07 := replayGenerationEnv07 listGenerationWF07 rfl rfl listCtorEnv_ordered07 @@ -702,7 +702,7 @@ theorem optionDeclWF07 : optionDecl.WF VEnv.empty := by · trivial · exact .nil -def optionGenerationWF07 : optionGenerationChecked.WF VEnv.empty := by +theorem optionGenerationWF07 : optionGenerationChecked.WF VEnv.empty := by exact (optionChecked.wf_of_decl optionDeclWF07).identityGeneration .empty def optionTypeEnv07 : VEnv := @@ -748,7 +748,7 @@ theorem optionCtorEnv_ordered07 : optionCtorEnv07.Ordered := replayCtorEnv_ordered07 optionGenerationWF07 rfl optionTypeEnv_ordered07 rfl -def optionGenerationEnv07 : +theorem optionGenerationEnv07 : VInductDecl.GenerationEnv optionGenerationChecked optionCtorEnv07 := replayGenerationEnv07 optionGenerationWF07 rfl rfl optionCtorEnv_ordered07 @@ -925,7 +925,7 @@ theorem prodCheckedWF07 : prodChecked.WF VEnv.empty := by · trivial · exact .nil -def prodGenerationWF07 : prodGenerationChecked.WF VEnv.empty := by +theorem prodGenerationWF07 : prodGenerationChecked.WF VEnv.empty := by exact prodCheckedWF07.identityGeneration .empty def prodTypeEnv07 : VEnv := @@ -958,7 +958,7 @@ theorem prodCtorEnv_ordered07 : prodCtorEnv07.Ordered := replayCtorEnv_ordered07 prodGenerationWF07 rfl prodTypeEnv_ordered07 rfl -def prodGenerationEnv07 : +theorem prodGenerationEnv07 : VInductDecl.GenerationEnv prodGenerationChecked prodCtorEnv07 := replayGenerationEnv07 prodGenerationWF07 rfl rfl prodCtorEnv_ordered07 @@ -1094,7 +1094,7 @@ theorem andCheckedWF07 : andChecked.WF VEnv.empty := by · trivial · exact .nil -def andGenerationWF07 : andGenerationChecked.WF VEnv.empty := by +theorem andGenerationWF07 : andGenerationChecked.WF VEnv.empty := by exact andCheckedWF07.identityGeneration .empty def andTypeEnv07 : VEnv := @@ -1127,7 +1127,7 @@ theorem andCtorEnv_ordered07 : andCtorEnv07.Ordered := replayCtorEnv_ordered07 andGenerationWF07 rfl andTypeEnv_ordered07 rfl -def andGenerationEnv07 : +theorem andGenerationEnv07 : VInductDecl.GenerationEnv andGenerationChecked andCtorEnv07 := replayGenerationEnv07 andGenerationWF07 rfl rfl andCtorEnv_ordered07 @@ -1269,7 +1269,7 @@ theorem orCheckedWF07 : orChecked.WF VEnv.empty := by · trivial · exact .nil -def orGenerationWF07 : orGenerationChecked.WF VEnv.empty := by +theorem orGenerationWF07 : orGenerationChecked.WF VEnv.empty := by exact orCheckedWF07.identityGeneration .empty def orTypeEnv07 : VEnv := @@ -1315,7 +1315,7 @@ theorem orCtorEnv_ordered07 : orCtorEnv07.Ordered := replayCtorEnv_ordered07 orGenerationWF07 rfl orTypeEnv_ordered07 rfl -def orGenerationEnv07 : +theorem orGenerationEnv07 : VInductDecl.GenerationEnv orGenerationChecked orCtorEnv07 := replayGenerationEnv07 orGenerationWF07 rfl rfl orCtorEnv_ordered07 @@ -1478,7 +1478,7 @@ theorem heqCheckedWF07 : heqChecked.WF VEnv.empty := by [.bvar 1, .bvar 0] (.sort .zero) exact .cons (by type_tac) <| .cons (by type_tac) .nil -def heqGenerationWF07 : heqGenerationChecked.WF VEnv.empty := by +theorem heqGenerationWF07 : heqGenerationChecked.WF VEnv.empty := by exact heqCheckedWF07.identityGeneration .empty def heqTypeEnv07 : VEnv := @@ -1511,7 +1511,7 @@ theorem heqCtorEnv_ordered07 : heqCtorEnv07.Ordered := replayCtorEnv_ordered07 heqGenerationWF07 rfl heqTypeEnv_ordered07 rfl -def heqGenerationEnv07 : +theorem heqGenerationEnv07 : VInductDecl.GenerationEnv heqGenerationChecked heqCtorEnv07 := replayGenerationEnv07 heqGenerationWF07 rfl rfl heqCtorEnv_ordered07 @@ -1904,7 +1904,7 @@ theorem finCheckedWF07 : finChecked.WF finInputEnv07 := by · trivial · exact .nil -def finGenerationWF07 : finGenerationChecked.WF finInputEnv07 := by +theorem finGenerationWF07 : finGenerationChecked.WF finInputEnv07 := by exact finCheckedWF07.identityGeneration finInputEnv_ordered07 def finTypeEnv07 : VEnv := @@ -1931,7 +1931,7 @@ theorem finTypeEnv_ordered07 : finTypeEnv07.Ordered := theorem finCtorEnv_ordered07 : finCtorEnv07.Ordered := replayCtorEnv_ordered07 finGenerationWF07 rfl finTypeEnv_ordered07 rfl -def finGenerationEnv07 : +theorem finGenerationEnv07 : VInductDecl.GenerationEnv finGenerationChecked finCtorEnv07 := replayGenerationEnv07 finGenerationWF07 rfl rfl finCtorEnv_ordered07 @@ -2274,7 +2274,7 @@ theorem vectorCheckedWF07 : vectorChecked.WF vectorInputEnv07 := by · trivial · exact .nil -def vectorGenerationWF07 : +theorem vectorGenerationWF07 : vectorGenerationChecked.WF vectorInputEnv07 := by exact vectorCheckedWF07.identityGeneration vectorInputEnv_ordered07 @@ -2306,7 +2306,7 @@ theorem vectorCtorEnv_ordered07 : vectorCtorEnv07.Ordered := replayCtorEnv_ordered07 vectorGenerationWF07 rfl vectorTypeEnv_ordered07 rfl -def vectorGenerationEnv07 : +theorem vectorGenerationEnv07 : VInductDecl.GenerationEnv vectorGenerationChecked vectorCtorEnv07 := replayGenerationEnv07 vectorGenerationWF07 rfl rfl vectorCtorEnv_ordered07 @@ -2453,7 +2453,7 @@ def vectorReplay07 : SingletonReplayArtifact where /-! ### Unit/Empty edge cases -/ -def punitGenerationWF07 : punitGenerationChecked.WF VEnv.empty := by +theorem punitGenerationWF07 : punitGenerationChecked.WF VEnv.empty := by exact (punitChecked.wf_of_decl punitDecl_wf).identityGeneration .empty def punitTypeEnv07 : VEnv := @@ -2486,7 +2486,7 @@ theorem punitCtorEnv_ordered07 : punitCtorEnv07.Ordered := replayCtorEnv_ordered07 punitGenerationWF07 rfl punitTypeEnv_ordered07 rfl -def punitGenerationEnv07 : +theorem punitGenerationEnv07 : VInductDecl.GenerationEnv punitGenerationChecked punitCtorEnv07 := replayGenerationEnv07 punitGenerationWF07 rfl rfl punitCtorEnv_ordered07 @@ -2592,7 +2592,7 @@ def punitReplay07 : SingletonReplayArtifact where transaction := punitAddInduct07 aligned := punitAligned07 -def emptyGenerationWF07 : emptyGenerationChecked.WF VEnv.empty := by +theorem emptyGenerationWF07 : emptyGenerationChecked.WF VEnv.empty := by exact (emptyChecked.wf_of_decl emptyDecl_wf).identityGeneration .empty def emptyTypeEnv07 : VEnv := @@ -2614,7 +2614,7 @@ def emptyMap07 : ConstMap := theorem emptyTypeEnv_ordered07 : emptyTypeEnv07.Ordered := replayTypeEnv_ordered07 .empty emptyGenerationWF07 rfl -def emptyGenerationEnv07 : +theorem emptyGenerationEnv07 : VInductDecl.GenerationEnv emptyGenerationChecked emptyTypeEnv07 := replayGenerationEnv07 emptyGenerationWF07 rfl rfl emptyTypeEnv_ordered07 diff --git a/Lean4Lean/Verify/EquivManager.lean b/Lean4Lean/Verify/EquivManager.lean index 627b3b10..f9ecc163 100644 --- a/Lean4Lean/Verify/EquivManager.lean +++ b/Lean4Lean/Verify/EquivManager.lean @@ -330,7 +330,7 @@ theorem isDefEq.WF {c : VContext} {s : VState} · rename_i heq exact .pure fun _ => (he₁.eqv heq).uniq c.Ewf (.refl c.Ewf c.Δwf) he₂ - simp only [pure_bind] + simp only [] refine (isDefEqCore.WF he₁ he₂).bind fun b _ _ hb => ?_ simp; split · exact (addEquiv.WF he₁ ⟨_, he₂, (hb ‹_›).symm⟩).map fun _ _ _ _ => hb diff --git a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean index be8db9e2..359ae2b7 100644 --- a/Lean4Lean/Verify/TypeChecker/IsDefEq.lean +++ b/Lean4Lean/Verify/TypeChecker/IsDefEq.lean @@ -187,7 +187,7 @@ theorem isDefEqArgs.WF {c : VContext} {s : VState} unfold isDefEqArgs; split <;> (unfold Expr.getAppFn at H) · let .app a1 a2 a3 a4 := he₁ let .app b1 b2 b3 b4 := he₂ - refine (isDefEq.WF a4 b4).bind fun _ _ _ h2 => ?_; extract_lets F + refine (isDefEq.WF a4 b4).bind fun _ _ _ h2 => ?_; extract_lets split <;> [exact .pure nofun; rename_i hb2] refine (isDefEqArgs.WF H a3 b3).mono fun _ _ _ h1 hb1 => ?_ simp at hb2 @@ -296,7 +296,7 @@ theorem tryEtaStructCore.WF_of_structureEta {c : VContext} {s : VState} refine .getEnv ?_ refine (M.WF.liftExcept envGet.WF).lift.bind fun _ci _ _ hfind => ?_ split <;> [skip; exact .pure nofun] - extract_lets F1 F2 + extract_lets F1 split <;> [skip; exact .pure nofun] rename_i hostHead ctorName ctorLevels hhead state hstate hostInfo ctorInfo hargs @@ -376,8 +376,7 @@ theorem tryEtaStructCore.WF_of_structureEta {c : VContext} {s : VState} let params := args'.take artifact.projection.view.nparams let fields := args'.drop artifact.projection.view.nparams have hargsSplit : args' = params ++ fields := by - simpa [params, fields] using - (List.take_append_drop artifact.projection.view.nparams args').symm + simp [params, fields] have hparamsLength : params.length = artifact.projection.view.nparams := by simp [params, hargsLength] have hfieldsLength : fields.length = artifact.projection.view.fields.length := by @@ -449,9 +448,8 @@ theorem tryEtaStructCore.WF_of_structureEta {c : VContext} {s : VState} artifact.projection.view.generation.block artifact.projection.view.constructor).instL levels).instRev args' = artifact.projection.view.structureType levels params := by - simp only [VInductDecl.NormalizedCtor.resultTarget, - VExpr.instL_appN, VExpr.instL, VExpr.instRev_appN, VExpr.instRev, - VExpr.bvarRevRange_map_instL, hresultIndices, List.append_nil] + simp only [VInductDecl.NormalizedCtor.resultTarget, VExpr.instL_appN, VExpr.instL, + VExpr.instRev_appN, VExpr.bvarRevRange_map_instL, hresultIndices, List.append_nil] rw [VLevel.inst_map_id hlevelsLength] rw [VExpr.instRev_closedN args' (by trivial)] rw [hrange'] @@ -513,14 +511,13 @@ theorem tryEtaStructCore.WF_of_structureEta {c : VContext} {s : VState} e₂.getAppArgsList[ctorInfo.numParams + j]? = some F1[ctorInfo.numParams + j] := by rw [← Expr.getAppArgs_toList] - simpa [F1] using List.getElem?_eq_getElem hi + simp [F1] obtain ⟨translated, htranslated, htr⟩ := Lean4Lean.List.Forall₂.getElem?_left hargsTr hselectedList have hfieldGet : args'[ctorInfo.numParams + j]? = some fields[j] := by rw [hargsSplit, List.getElem?_append_right] - · simpa [hnumParams, hparamsLength] using - (List.getElem?_eq_getElem hj) - · simpa [hnumParams, hparamsLength] + · simp [hnumParams, hparamsLength] + · simp [hnumParams, hparamsLength] have : translated = fields[j] := Option.some.inj (htranslated.symm.trans hfieldGet) subst translated @@ -606,7 +603,7 @@ theorem tryEtaStructCore.WF_of_structureEta {c : VContext} {s : VState} · exact hrest.1 hnone k hk, hrest.2⟩) simpa only [etaStep, tryEtaStructFieldStep, pure_bind] using htail - · simp only [hbtrue, if_neg, pure_bind] + · simp only [hbtrue] exact .pure (by simp) have hparamsLe : ctorInfo.numParams ≤ F1.size := by rw [hF1Size, hargsLength, ← hnumParams] @@ -844,7 +841,7 @@ def _root_.Lean4Lean.TypeChecker.ReductionStatus.WF | .unknown e₁ e₂ => c.TrExpr e₁ e₁' ∧ c.TrExpr e₂ e₂' | .bool b => b → c.IsDefEqU e₁' e₂' -def _root_.Lean4Lean.TypeChecker.ReductionStatus.WF.defeq +theorem _root_.Lean4Lean.TypeChecker.ReductionStatus.WF.defeq (h1 : c.IsDefEqU e₁' e₁'') (h2 : c.IsDefEqU e₂' e₂'') (H : ReductionStatus.WF c e₁' e₂' ac r) : ReductionStatus.WF c e₁'' e₂'' ac r := match r, H with diff --git a/Lean4Lean/Verify/TypeChecker/WHNF.lean b/Lean4Lean/Verify/TypeChecker/WHNF.lean index e009e02c..c1aca093 100644 --- a/Lean4Lean/Verify/TypeChecker/WHNF.lean +++ b/Lean4Lean/Verify/TypeChecker/WHNF.lean @@ -3,6 +3,7 @@ import Lean4Lean.Verify.TypeChecker.Reduce namespace Lean4Lean.TypeChecker.Inner open Lean hiding Environment Exception +set_option warn.sorry false in theorem reduceRecursor.WF {c : VContext} {s : VState} (he : c.TrExprS e e') : RecM.WF c s (reduceRecursor e) fun oe _ => ∀ e₁, oe = some e₁ → c.FVarsBelow e e₁ ∧ c.TrExpr e₁ e' := sorry diff --git a/Lean4Lean/Verify/Typing/Lemmas.lean b/Lean4Lean/Verify/Typing/Lemmas.lean index e6a5dc5e..928c7449 100644 --- a/Lean4Lean/Verify/Typing/Lemmas.lean +++ b/Lean4Lean/Verify/Typing/Lemmas.lean @@ -1633,8 +1633,7 @@ theorem ofLevel_mkLevelIMax' · simp_all; exact VLevel.imax_self.symm simp [VLevel.ofLevel]; exact ⟨_, ⟨_, h1, _, h2, rfl⟩, rfl⟩ -variable! {ls : List VLevel} (hls : ∀ l ∈ ls, l.WF U') - (hU : U = ls.length) in +variable! {ls : List VLevel} (hls : ∀ l ∈ ls, l.WF U') in theorem TrProj.instL (H : TrProj env U Γ s i e e') : TrProj env U' (Γ.map (VExpr.instL ls)) s i (e.instL ls) (e'.instL ls) := by @@ -1686,7 +1685,7 @@ theorem TrProj.structuralLaws (henv : VEnv.WF env) : wellFormed H he := H.wf he unique hΓ H1 H2 he := H1.uniq henv hΓ H2 he termSubstitution h₀ W H := H.instN henv.ordered h₀ W - universeInstantiation hls hU H := H.instL hls hU + universeInstantiation hls _ H := H.instL hls /-! The guards below pin both the proved laws and the inherited Tier-R boundary. @@ -1848,7 +1847,7 @@ theorem TrExprS.instL (H : TrExprS env ps Δ e e') : | mdata _ ih => exact .mdata (ih hΔ) | proj _ h2 ih => exact .proj henv (hΔ.instL Hls') (ih hΔ) - (VLCtx.instL_toCtx _ ▸ h2.instL Hls' eq') + (VLCtx.instL_toCtx _ ▸ h2.instL Hls') theorem TrExpr.instL (H : TrExpr env ps Δ e e') : TrExpr env Us (Δ.instL ls') (e.instantiateLevelParams ps ls) (e'.instL ls') := diff --git a/flake.lock b/flake.lock index be751f6e..6a270fc6 100644 --- a/flake.lock +++ b/flake.lock @@ -24,11 +24,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1786463392, - "narHash": "sha256-5ke9p2DFQcF0FxR/RyrYvZymoVcCR1zyVWlnhqfRyf0=", + "lastModified": 1786543565, + "narHash": "sha256-zHMoHO85jizkIXH0OfnvabpNLTl90rR3GCc1h/e2sx4=", "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "c41a770e44a990da275dad0f70da75f22197e597", + "rev": "4026c657eecf16beea7d266ce32933ef3d7db2e5", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 30b04217..447a7265 100644 --- a/flake.nix +++ b/flake.nix @@ -48,24 +48,15 @@ lean = lean4-nix.lib.${system}.fromToolchainFile ./lean-toolchain; # Lake package lake2nix = pkgs.callPackage lean4-nix.lake {inherit lean;}; - # Restrict the Lake build inputs to Lean-relevant files so edits to - # unrelated files (CI, docs, the flake itself) don't invalidate the - # cached Lean derivations. Covers the library/CLI/proof/test/audit - # sources, the manifests lean4-nix reads while evaluating, and the + # Restrict the Lake build inputs to the files `lake build` reads, so + # edits to unrelated files (CI, docs, the flake itself) don't + # invalidate the cached Lean derivations. Keeps `.lean`/`.toml`, the + # manifests lean4-nix reads while evaluating, and the # downstream-consumer fixture built from `${leanSrc}/nix/fixtures`. - # NOTE: a fileset source is left unrealized under `nix flake check - # --no-build` (fails with "path '…-source' is not valid"), so the nix - # CI job builds for real rather than eval-only. - leanSrc = pkgs.lib.fileset.toSource { - root = ./.; - fileset = pkgs.lib.fileset.unions [ - ./lakefile.toml - ./lake-manifest.json - ./lean-toolchain - ./nix/fixtures - (pkgs.lib.fileset.fileFilter (f: f.hasExt "lean") ./.) - ]; - }; + # NOTE: a filtered source is left unrealized under `nix flake check + # --no-build` (fails with "path '…-lake-source' is not valid"), so the + # nix CI job builds for real rather than eval-only. + leanSrc = lake2nix.cleanLakeSource ./.; # Dependencies from lake-manifest.json (batteries). lean4-nix's # default target guess ("batteries" -> "Batteries") is correct, and # batteries ≥ v4.32 ships the shared/static cycle fix that v4.31 @@ -153,7 +144,7 @@ # A check that builds extra Lake targets over the library artifact and # installs nothing: the build — including any elaboration-time # assertions in those targets — is the test. - mkLakeCheck = name: buildTargets: + mkLakeCheck = name: targets: lake2nix.mkPackage ( lakeBuildArgs // reuseLibArgs @@ -161,7 +152,7 @@ inherit name; buildPhase = '' runHook preBuild - ${buildTargets} + lake build ${pkgs.lib.concatStringsSep " " targets} runHook postBuild ''; } @@ -174,16 +165,17 @@ # declaration gains, loses, or renames a `sorry` versus its allowlist. # It is not a default target, so building it over the just-built # surface is the whole check. - proofs = mkLakeCheck "Lean4Lean-proofs" '' - lake build Lean4Lean.Theory Lean4Lean.Verify - lake build Lean4Lean.Audit.SorryFrontier - ''; + proofs = mkLakeCheck "Lean4Lean-proofs" [ + "Lean4Lean.Theory" + "Lean4Lean.Verify" + "Lean4Lean.Audit.SorryFrontier" + ]; # Basic test suite: the `Lean4Lean.Tests.*` regression modules (the # nested-inductive kernel checks and the toolchain audit) run their # assertions at elaboration via `run_meta`/`#guard`, so building the # target is the test run. - tests = mkLakeCheck "Lean4Lean-tests" "lake build Lean4Lean.Tests"; + tests = mkLakeCheck "Lean4Lean-tests" ["Lean4Lean.Tests"]; # Downstream-consumer check: a minimal Lake package that requires # lean4lean, links an executable against the read-only dependency