From c35d29dcf48c42dbab15a751db0636d224c17048 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 18 Mar 2024 16:21:38 +0100 Subject: [PATCH] make simp_add available in the entire game #54 --- Game/Levels/Algorithm/L04add_algo3.lean | 1 + Game/Metadata.lean | 5 +- Game/Tactic/LeanExprBasic.lean | 342 ------------------------ Game/Tactic/Simp.lean | 49 ---- Game/Tactic/SimpAdd.lean | 38 +++ 5 files changed, 40 insertions(+), 395 deletions(-) delete mode 100644 Game/Tactic/LeanExprBasic.lean delete mode 100644 Game/Tactic/Simp.lean create mode 100644 Game/Tactic/SimpAdd.lean diff --git a/Game/Levels/Algorithm/L04add_algo3.lean b/Game/Levels/Algorithm/L04add_algo3.lean index d661046..50ad280 100644 --- a/Game/Levels/Algorithm/L04add_algo3.lean +++ b/Game/Levels/Algorithm/L04add_algo3.lean @@ -1,4 +1,5 @@ import Game.Levels.Algorithm.L03add_algo2 +import ImportGraph World "Algorithm" Level 4 diff --git a/Game/Metadata.lean b/Game/Metadata.lean index 85cb142..24a2ecf 100644 --- a/Game/Metadata.lean +++ b/Game/Metadata.lean @@ -14,10 +14,7 @@ import Game.Tactic.Rw import Game.Tactic.Use import Game.Tactic.Ne import Game.Tactic.Xyzzy +import Game.Tactic.SimpAdd -- import Std.Tactic.RCases -- import Game.Tactic.Have -- import Game.Tactic.LeftRight - --- TODO: Why does this not work here?? --- We do not want `simp` to be able to do anything unless we unlock it manually. -attribute [-simp] MyNat.succ.injEq diff --git a/Game/Tactic/LeanExprBasic.lean b/Game/Tactic/LeanExprBasic.lean deleted file mode 100644 index 8914815..0000000 --- a/Game/Tactic/LeanExprBasic.lean +++ /dev/null @@ -1,342 +0,0 @@ -/- -copied from mathlib - -TODO: Just copied because some tactics depend on it, -probably can golf the copies of the mathlib tactics in -this game so that this isn't needed. --/ -import Lean -import Std.Lean.Expr -import Std.Data.List.Basic - -/-! -# Additional operations on Expr and related types - -This file defines basic operations on the types expr, name, declaration, level, environment. - -This file is mostly for non-tactics. --/ - -namespace Lean - -namespace BinderInfo - -/-! ### Declarations about `BinderInfo` -/ - -/-- The brackets corresponding to a given `BinderInfo`. -/ -def brackets : BinderInfo → String × String -| BinderInfo.implicit => ("{", "}") -| BinderInfo.strictImplicit => ("{{", "}}") -| BinderInfo.instImplicit => ("[", "]") -| _ => ("(", ")") - -end BinderInfo - -namespace Name - -/-! ### Declarations about `name` -/ - -/-- Find the largest prefix `n` of a `Name` such that `f n != none`, then replace this prefix -with the value of `f n`. -/ -def mapPrefix (f : Name → Option Name) (n : Name) : Name := Id.run do - if let some n' := f n then return n' - match n with - | anonymous => anonymous - | str n' s => mkStr (mapPrefix f n') s - | num n' i => mkNum (mapPrefix f n') i - -/-- Build a name from components. For example ``from_components [`foo, `bar]`` becomes - ``` `foo.bar```. - It is the inverse of `Name.components` on list of names that have single components. -/ -def fromComponents : List Name → Name := go .anonymous where - /-- Auxiliary for `Name.fromComponents` -/ - go : Name → List Name → Name - | n, [] => n - | n, s :: rest => go (s.updatePrefix n) rest - -/-- Update the last component of a name. -/ -def updateLast (f : String → String) : Name → Name -| .str n s => .str n (f s) -| n => n - -/-- Get the last field of a name as a string. -Doesn't raise an error when the last component is a numeric field. -/ -def getString : Name → String -| .str _ s => s -| .num _ n => toString n -| .anonymous => "" - -/-- `nm.splitAt n` splits a name `nm` in two parts, such that the *second* part has depth `n`, i.e. - `(nm.splitAt n).2.getNumParts = n` (assuming `nm.getNumParts ≥ n`). - Example: ``splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat)``. -/ -def splitAt (nm : Name) (n : Nat) : Name × Name := - let (nm2, nm1) := (nm.componentsRev.splitAt n) - (.fromComponents <| nm1.reverse, .fromComponents <| nm2.reverse) - -/-- `isPrefixOf? pre nm` returns `some post` if `nm = pre ++ post`. - Note that this includes the case where `nm` has multiple more namespaces. - If `pre` is not a prefix of `nm`, it returns `none`. -/ -def isPrefixOf? (pre nm : Name) : Option Name := - if pre == nm then - some anonymous - else match nm with - | anonymous => none - | num p' a => (isPrefixOf? pre p').map (·.num a) - | str p' s => (isPrefixOf? pre p').map (·.str s) - -/-- Lean 4 makes declarations which are technically not internal -(that is, head string does not start with `_`) but which sometimes should -be treated as such. For example, the `to_additive` attribute needs to -transform `proof_1` constants generated by `Lean.Meta.mkAuxDefinitionFor`. -This might be better fixed in core, but until then, this method can act -as a polyfill. This method only looks at the name to decide whether it is probably internal. -Note: this declaration also occurs as `shouldIgnore` in the Lean 4 file `test/lean/run/printDecls`. --/ -def isInternal' (declName : Name) : Bool := - declName.isInternal || - match declName with - | .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s - | _ => true - -end Name - - -namespace ConstantInfo - -/-- Checks whether this `ConstantInfo` is a definition, -/ -def isDef : ConstantInfo → Bool - | defnInfo _ => true - | _ => false - -/-- Checks whether this `ConstantInfo` is a theorem, -/ -def isThm : ConstantInfo → Bool - | thmInfo _ => true - | _ => false - -/-- Update `ConstantVal` (the data common to all constructors of `ConstantInfo`) -in a `ConstantInfo`. -/ -def updateConstantVal : ConstantInfo → ConstantVal → ConstantInfo - | defnInfo info, v => defnInfo {info with toConstantVal := v} - | axiomInfo info, v => axiomInfo {info with toConstantVal := v} - | thmInfo info, v => thmInfo {info with toConstantVal := v} - | opaqueInfo info, v => opaqueInfo {info with toConstantVal := v} - | quotInfo info, v => quotInfo {info with toConstantVal := v} - | inductInfo info, v => inductInfo {info with toConstantVal := v} - | ctorInfo info, v => ctorInfo {info with toConstantVal := v} - | recInfo info, v => recInfo {info with toConstantVal := v} - -/-- Update the name of a `ConstantInfo`. -/ -def updateName (c : ConstantInfo) (name : Name) : ConstantInfo := - c.updateConstantVal {c.toConstantVal with name} - -/-- Update the type of a `ConstantInfo`. -/ -def updateType (c : ConstantInfo) (type : Expr) : ConstantInfo := - c.updateConstantVal {c.toConstantVal with type} - -/-- Update the level parameters of a `ConstantInfo`. -/ -def updateLevelParams (c : ConstantInfo) (levelParams : List Name) : - ConstantInfo := - c.updateConstantVal {c.toConstantVal with levelParams} - -/-- Update the value of a `ConstantInfo`, if it has one. -/ -def updateValue : ConstantInfo → Expr → ConstantInfo - | defnInfo info, v => defnInfo {info with value := v} - | thmInfo info, v => thmInfo {info with value := v} - | opaqueInfo info, v => opaqueInfo {info with value := v} - | d, _ => d - -/-- Turn a `ConstantInfo` into a declaration. -/ -def toDeclaration! : ConstantInfo → Declaration - | defnInfo info => Declaration.defnDecl info - | thmInfo info => Declaration.thmDecl info - | axiomInfo info => Declaration.axiomDecl info - | opaqueInfo info => Declaration.opaqueDecl info - | quotInfo _ => panic! "toDeclaration for quotInfo not implemented" - | inductInfo _ => panic! "toDeclaration for inductInfo not implemented" - | ctorInfo _ => panic! "toDeclaration for ctorInfo not implemented" - | recInfo _ => panic! "toDeclaration for recInfo not implemented" - -end ConstantInfo - -open Meta - -/-- Same as `mkConst`, but with fresh level metavariables. -/ -def mkConst' (constName : Name) : MetaM Expr := do - return mkConst constName (← (← getConstInfo constName).levelParams.mapM fun _ => mkFreshLevelMVar) - -namespace Expr - -/-! ### Declarations about `Expr` -/ - -/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/ -def constName (e : Expr) : Name := - e.constName?.getD Name.anonymous - -def bvarIdx? : Expr → Option Nat - | bvar idx => some idx - | _ => none - -/-- Return the function (name) and arguments of an application. -/ -def getAppFnArgs (e : Expr) : Name × Array Expr := - withApp e λ e a => (e.constName, a) - -/-- Turn an expression that is a natural number literal into a natural number. -/ -def natLit! : Expr → Nat - | lit (Literal.natVal v) => v - | _ => panic! "nat literal expected" - -/-- If an `Expr` has form `.fvar n`, then returns `some n`, otherwise `none`. -/ -def fvarId? : Expr → Option FVarId - | .fvar n => n - | _ => none - -/-- `isConstantApplication e` checks whether `e` is syntactically an application of the form - `(fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ` where `H` does not contain the variable `xₙ`. In other words, - it does a syntactic check that the expression does not depend on `yₙ`. -/ -def isConstantApplication (e : Expr) := -e.isApp && aux e.getAppNumArgs'.pred e.getAppFn' e.getAppNumArgs' -where - /-- `aux depth e n` checks whether the body of the `n`-th lambda of `e` has loose bvar - `depth - 1`. -/ - aux (depth : Nat) : Expr → Nat → Bool - | .lam _ _ b _, n + 1 => aux depth b n - | e, 0 => !e.hasLooseBVar (depth - 1) - | _, _ => false - -open Meta - -/-- Check that an expression contains no metavariables (after instantiation). -/ --- There is a `TacticM` level version of this, but it's useful to have in `MetaM`. -def ensureHasNoMVars (e : Expr) : MetaM Unit := do - let e ← instantiateMVars e - if e.hasExprMVar then - throwError "tactic failed, resulting expression contains metavariables{indentExpr e}" - -/-- Construct the term of type `α` for a given natural number -(doing typeclass search for the `OfNat` instance required). -/ -def ofNat (α : Expr) (n : Nat) : MetaM Expr := do - mkAppOptM ``OfNat.ofNat #[α, mkRawNatLit n, none] - -/-- Construct the term of type `α` for a given integer -(doing typeclass search for the `OfNat` and `Neg` instances required). -/ -def ofInt (α : Expr) : Int → MetaM Expr -| Int.ofNat n => Expr.ofNat α n -| Int.negSucc n => do mkAppM ``Neg.neg #[← Expr.ofNat α (n+1)] - -/-- - Return `some n` if `e` is one of the following - - A nat literal (numeral) - - `Nat.zero` - - `Nat.succ x` where `isNumeral x` - - `OfNat.ofNat _ x _` where `isNumeral x` -/ -partial def numeral? (e : Expr) : Option Nat := - if let some n := e.natLit? then n - else - let f := e.getAppFn - if !f.isConst then none - else - let fName := f.constName! - if fName == ``Nat.succ && e.getAppNumArgs == 1 then (numeral? e.appArg!).map Nat.succ - else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then numeral? (e.getArg! 1) - else if fName == ``Nat.zero && e.getAppNumArgs == 0 then some 0 - else none - -/-- Test if an expression is either `Nat.zero`, or `OfNat.ofNat 0`. -/ -def zero? (e : Expr) : Bool := - match e.numeral? with - | some 0 => true - | _ => false - --- Edit -variable {M} - -def modifyAppArgM [Functor M] [Pure M] (modifier : Expr → M Expr) : Expr → M Expr - | app f a => mkApp f <$> modifier a - | e => pure e - -def modifyAppArg (modifier : Expr → Expr) : Expr → Expr := - modifyAppArgM (M := Id) modifier - -def modifyRevArg (modifier : Expr → Expr): Nat → Expr → Expr - | 0 => modifyAppArg modifier - | (i+1) => modifyAppArg (modifyRevArg modifier i) - -/-- Given `f a₀ a₁ ... aₙ₋₁`, runs `modifier` on the `i`th argument or -returns the original expression if out of bounds. -/ -def modifyArg (modifier : Expr → Expr) (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr := - modifyRevArg modifier (n - i - 1) e - -def getRevArg? : Expr → Nat → Option Expr - | app _ a, 0 => a - | app f _, i+1 => getRevArg! f i - | _, _ => none - -/-- Given `f a₀ a₁ ... aₙ₋₁`, returns the `i`th argument or none if out of bounds. -/ -def getArg? (e : Expr) (i : Nat) (n := e.getAppNumArgs): Option Expr := - getRevArg? e (n - i - 1) - -/-- Given `f a₀ a₁ ... aₙ₋₁`, runs `modifier` on the `i`th argument. -An argument `n` may be provided which says how many arguments we are expecting `e` to have. -/ -def modifyArgM [Monad M] (modifier : Expr → M Expr) (e : Expr) (i : Nat) (n := e.getAppNumArgs) : - M Expr := do - let some a := getArg? e i | return e - let a ← modifier a - return modifyArg (fun _ ↦ a) e i n - -/-- Traverses an expression `e` and renames bound variables named `old` to `new`. -/ -def renameBVar (e : Expr) (old new : Name) : Expr := - match e with - | app fn arg => app (fn.renameBVar old new) (arg.renameBVar old new) - | lam n ty bd bi => - lam (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi - | forallE n ty bd bi => - forallE (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi - | e => e - -open Lean.Meta in -/-- `getBinderName e` returns `some n` if `e` is an expression of the form `∀ n, ...` -and `none` otherwise. -/ -def getBinderName (e : Expr) : MetaM (Option Name) := do - match ← withReducible (whnf e) with - | .forallE (binderName := n) .. | .lam (binderName := n) .. => pure (some n) - | _ => pure none - -open Lean.Elab.Term -/-- Annotates a `binderIdent` with the binder information from an `fvar`. -/ -def addLocalVarInfoForBinderIdent (fvar : Expr) : TSyntax ``binderIdent → TermElabM Unit -| `(binderIdent| $n:ident) => Elab.Term.addLocalVarInfo n fvar -| tk => Elab.Term.addLocalVarInfo (Unhygienic.run `(_%$tk)) fvar - -/-- If `e` has a structure as type with field `fieldName`, `mkDirectProjection e fieldName` creates -the projection expression `e.fieldName` -/ -def mkDirectProjection (e : Expr) (fieldName : Name) : MetaM Expr := do - let type ← whnf (← inferType e) - let .const structName us := type.getAppFn | throwError "{e} doesn't have a structure as type" - let some projName := getProjFnForField? (← getEnv) structName fieldName | - throwError "{structName} doesn't have field {fieldName}" - return mkAppN (.const projName us) (type.getAppArgs.push e) - -/-- If `e` has a structure as type with field `fieldName` (either directly or in a parent -structure), `mkProjection e fieldName` creates the projection expression `e.fieldName` -/ -def mkProjection (e : Expr) (fieldName : Name) : MetaM Expr := do - let .const structName _ := (← whnf (←inferType e)).getAppFn | - throwError "{e} doesn't have a structure as type" - let some baseStruct := findField? (← getEnv) structName fieldName | - throwError "No parent of {structName} has field {fieldName}" - let mut e := e - for projName in (getPathToBaseStructure? (← getEnv) baseStruct structName).get! do - let type ← whnf (← inferType e) - let .const _structName us := type.getAppFn | throwError "{e} doesn't have a structure as type" - e := mkAppN (.const projName us) (type.getAppArgs.push e) - mkDirectProjection e fieldName - -end Expr - -/-- Get the projections that are projections to parent structures. Similar to `getParentStructures`, - except that this returns the (last component of the) projection names instead of the parent names. --/ -def getFieldsToParents (env : Environment) (structName : Name) : Array Name := - getStructureFields env structName |>.filter fun fieldName => - isSubobjectField? env structName fieldName |>.isSome - -end Lean diff --git a/Game/Tactic/Simp.lean b/Game/Tactic/Simp.lean deleted file mode 100644 index 4e6dc80..0000000 --- a/Game/Tactic/Simp.lean +++ /dev/null @@ -1,49 +0,0 @@ -import Game.Tactic.LeanExprBasic -import Lean.Elab.Tactic.Basic -import Game.Tactic.Rfl - -/-! # `simp` tactic - -Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`. --/ - -namespace MyNat - -open Lean Meta Elab Tactic - --- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a - -/-- -The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or -non-dependent hypotheses. It has many variants: -- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`. -- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged - with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions. - If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with - `f` are used. This provides a convenient way to unfold `f`. -- `simp [*]` simplifies the main goal target using the lemmas tagged with the - attribute `[simp]` and all hypotheses. -- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas. -- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged - with the attribute `[simp]`, but removes the ones named `idᵢ`. -- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If - the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis - `hᵢ` is introduced, but the old one remains in the local context. -- `simp at *` simplifies all the hypotheses and the target. -- `simp [*] at *` simplifies target and all (propositional) hypotheses using the - other hypotheses. --/ -syntax (name := simp) "simp" (config)? (discharger)? (&" only")? - (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic - -/- - "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)? --/ -@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do - let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false) - let usedSimps ← dischargeWrapper.with fun discharge? => - simpLocation ctx discharge? (expandOptLocation stx[5]) - if tactic.simp.trace.get (← getOptions) then - traceSimpCall stx usedSimps - -end MyNat diff --git a/Game/Tactic/SimpAdd.lean b/Game/Tactic/SimpAdd.lean new file mode 100644 index 0000000..160c85b --- /dev/null +++ b/Game/Tactic/SimpAdd.lean @@ -0,0 +1,38 @@ +import Game.MyNat.Addition + +namespace MyNat + +-- TODO: Is there a better way to do this instead of reproving these +-- basic theorems? + +theorem add_assocₓ (a b c : ℕ) : a + b + c = a + (b + c) := by + induction c with + | zero => + rw [zero_eq_0, add_zero, add_zero] + | succ n hn => + rw [add_succ, add_succ, add_succ, hn] + +theorem succ_addₓ : succ b + a = succ (b + a) := by + induction a with + | zero => + rw [zero_eq_0, add_zero, add_zero] + | succ a ha => + rw [add_succ, add_succ, ha] + +theorem add_commₓ (a b : ℕ) : a + b = b + a := by + induction b with + | zero => + have zero_add : 0 + a = a := by + induction a with + | zero => rw [zero_eq_0, add_zero] + | succ a ha => + rw [add_succ, ha] + rw [zero_eq_0, add_zero, zero_add] + | succ b hb => + rw [add_succ, succ_addₓ, hb] + +theorem add_left_commₓ (a b c : ℕ) : a + (b + c) = b + (a + c) := by + rw [← add_assocₓ, add_commₓ a b, add_assocₓ] + +macro "simp_add" : tactic => `(tactic|( + simp only [add_assocₓ, add_left_commₓ, add_commₓ]))