max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: add Init/MetaTypes to workaround bootstrapping issues

Browse source 
Motivation: we could not set `simp` configuration options at `WFTactics.lean`
This commit is contained in:
Leonardo de Moura 2023-10-29 09:36:46 -07:00
parent a53ec40df1
commit 175a6ab606
4 changed files with 122 additions and 104 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init.lean
View file

@ -17,6 +17,7 @@ import Init.System
import Init.Util
import Init.Dynamic
import Init.ShareCommon
import Init.MetaTypes
import Init.Meta
import Init.NotationExtra
import Init.SimpLemmas

105
src/Init/Meta.lean
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura and Sebastian Ullrich
Additional goodies for writing macros
-/
prelude
import Init.MetaTypes
import Init.Data.Array.Basic
import Init.Data.Option.BasicAux
@ -217,11 +218,6 @@ instance : DecidableEq Name :=
end Name
structure NameGenerator where
namePrefix : Name := `_uniq
idx : Nat := 1
deriving Inhabited
namespace NameGenerator
@[inline] def curr (g : NameGenerator) : Name :=
@ -452,11 +448,6 @@ end Syntax
| none => x
| some ref => withRef ref x
/-- Syntax objects for a Lean module. -/
structure Module where
header : Syntax
commands : Array Syntax
/--
Expand macros in the given syntax.
A node with kind `k` is visited only if `p k` is true.
@ -1203,99 +1194,7 @@ end TSyntax
namespace Meta
inductive TransparencyMode where
| all | default | reducible | instances
deriving Inhabited, BEq, Repr
inductive EtaStructMode where
/-- Enable eta for structure and classes. -/
| all
/-- Enable eta only for structures that are not classes. -/
| notClasses
/-- Disable eta for structures and classes. -/
| none
deriving Inhabited, BEq, Repr
namespace DSimp
structure Config where
zeta : Bool := true
beta : Bool := true
eta : Bool := true
etaStruct : EtaStructMode := .all
iota : Bool := true
proj : Bool := true
decide : Bool := false
autoUnfold : Bool := false
/-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress. -/
failIfUnchanged : Bool := true
/-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded. -/
unfoldPartialApp : Bool := false
deriving Inhabited, BEq, Repr
end DSimp
namespace Simp
def defaultMaxSteps := 100000
structure Config where
maxSteps : Nat := defaultMaxSteps
maxDischargeDepth : Nat := 2
contextual : Bool := false
memoize : Bool := true
singlePass : Bool := false
zeta : Bool := true
beta : Bool := true
eta : Bool := true
etaStruct : EtaStructMode := .all
iota : Bool := true
proj : Bool := true
decide : Bool := true
arith : Bool := false
autoUnfold : Bool := false
/--
If `dsimp := true`, then switches to `dsimp` on dependent arguments where there is no congruence theorem that allows
`simp` to visit them. If `dsimp := false`, then argument is not visited.
-/
dsimp : Bool := true
/-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress. -/
failIfUnchanged : Bool := true
/-- If `ground := true`, then ground terms are reduced. A term is ground when
it does not contain free or meta variables. Reduction is interrupted at a function application `f ...`
if `f` is marked to not be unfolded. -/
ground : Bool := false
/-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded. -/
unfoldPartialApp : Bool := false
deriving Inhabited, BEq, Repr
-- Configuration object for `simp_all`
structure ConfigCtx extends Config where
contextual := true
def neutralConfig : Simp.Config := {
zeta := false
beta := false
eta := false
iota := false
proj := false
decide := false
arith := false
autoUnfold := false
ground := false
}
end Simp
inductive Occurrences where
| all
| pos (idxs : List Nat)
| neg (idxs : List Nat)
deriving Inhabited, BEq
deriving instance Repr for TransparencyMode, EtaStructMode, DSimp.Config, Simp.Config
def Occurrences.contains : Occurrences → Nat → Bool
| all, _ => true

117
src/Init/MetaTypes.lean Normal file
View file

@ -0,0 +1,117 @@
/-
Copyright (c) Leonardo de Moura. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
namespace Lean
structure NameGenerator where
namePrefix : Name := `_uniq
idx : Nat := 1
deriving Inhabited
/-- Syntax objects for a Lean module. -/
structure Module where
header : Syntax
commands : Array Syntax
namespace Meta
inductive TransparencyMode where
| all | default | reducible | instances
deriving Inhabited, BEq
inductive EtaStructMode where
/-- Enable eta for structure and classes. -/
| all
/-- Enable eta only for structures that are not classes. -/
| notClasses
/-- Disable eta for structures and classes. -/
| none
deriving Inhabited, BEq
namespace DSimp
structure Config where
zeta : Bool := true
beta : Bool := true
eta : Bool := true
etaStruct : EtaStructMode := .all
iota : Bool := true
proj : Bool := true
decide : Bool := false
autoUnfold : Bool := false
/-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress. -/
failIfUnchanged : Bool := true
/-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded. -/
unfoldPartialApp : Bool := false
deriving Inhabited, BEq
end DSimp
namespace Simp
def defaultMaxSteps := 100000
structure Config where
maxSteps : Nat := defaultMaxSteps
maxDischargeDepth : Nat := 2
contextual : Bool := false
memoize : Bool := true
singlePass : Bool := false
zeta : Bool := true
beta : Bool := true
eta : Bool := true
etaStruct : EtaStructMode := .all
iota : Bool := true
proj : Bool := true
decide : Bool := true
arith : Bool := false
autoUnfold : Bool := false
/--
If `dsimp := true`, then switches to `dsimp` on dependent arguments where there is no congruence theorem that allows
`simp` to visit them. If `dsimp := false`, then argument is not visited.
-/
dsimp : Bool := true
/-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress. -/
failIfUnchanged : Bool := true
/-- If `ground := true`, then ground terms are reduced. A term is ground when
it does not contain free or meta variables. Reduction is interrupted at a function application `f ...`
if `f` is marked to not be unfolded. -/
ground : Bool := false
/-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded. -/
unfoldPartialApp : Bool := false
deriving Inhabited, BEq
-- Configuration object for `simp_all`
structure ConfigCtx extends Config where
contextual := true
def neutralConfig : Simp.Config := {
zeta := false
beta := false
eta := false
iota := false
proj := false
decide := false
arith := false
autoUnfold := false
ground := false
}
end Simp
inductive Occurrences where
| all
| pos (idxs : List Nat)
| neg (idxs : List Nat)
deriving Inhabited, BEq
end Lean.Meta

3
src/Init/WFTactics.lean
View file

@ -5,12 +5,13 @@ Author: Leonardo de Moura
-/
prelude
import Init.SizeOf
import Init.MetaTypes
import Init.WF
/-- Unfold definitions commonly used in well founded relation definitions.
This is primarily intended for internal use in `decreasing_tactic`. -/
macro "simp_wf" : tactic =>
`(tactic| try simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
`(tactic| try simp (config := { unfoldPartialApp := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
/-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
reasoning after applying lexicographic order lemmas.