greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

make simp_add available in the entire game #54

Browse Source
This commit is contained in:
Jon Eugster
2024-03-18 16:21:38 +01:00
parent 61ce8321ef
commit c35d29dcf4
5 changed files with 40 additions and 395 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
Game/Levels/Algorithm/L04add_algo3.lean
View File

@@ -1,4 +1,5 @@
import Game.Levels.Algorithm.L03add_algo2 import Game.Levels.Algorithm.L03add_algo2
import ImportGraph
World "Algorithm" World "Algorithm"
Level 4 Level 4

5
Game/Metadata.lean
View File

@@ -14,10 +14,7 @@ import Game.Tactic.Rw
import Game.Tactic.Use import Game.Tactic.Use
import Game.Tactic.Ne import Game.Tactic.Ne
import Game.Tactic.Xyzzy import Game.Tactic.Xyzzy
import Game.Tactic.SimpAdd
-- import Std.Tactic.RCases -- import Std.Tactic.RCases
-- import Game.Tactic.Have -- import Game.Tactic.Have
-- import Game.Tactic.LeftRight -- 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

342
Game/Tactic/LeanExprBasic.lean
View File

@@ -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

49
Game/Tactic/Simp.lean
View File

@@ -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

38
Game/Tactic/SimpAdd.lean Normal file
View File

@@ -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ₓ]))