@@ -1,509 +0,0 @@
import Lean
import Mathlib . Tactic . DeriveTraversable
import Spa . Language . Base
import Spa . Language . Tagged . Id
/- !
# The `derive_tagged` command
`derive_tagged T₁ T₂ … Tₙ` takes a family of (possibly mutually recursive)
inductive types and generates, for each `Tᵢ`:
* a *tagged* mirror inductive `Tᵢ.Tagged (τ : Type)`, in which every constructor
carries a leading `tag : τ` field and every field whose type is a family
member is retyped to its `.Tagged τ` counterpart;
* `Tᵢ.Tagged.erase : Tᵢ.Tagged τ → Tᵢ`, forgetting all tags;
* `Tᵢ.tag : Tᵢ → ℕ × ℕ
`RawId` (its postorder index) by a single unified traversal that threads a
counter; the whole family shares one counter, so identifiers are unique across
types.
The generated declarations have exactly the shape of the hand - written reference;
see `Spa / Language / Tagged / Basic.lean` (which invokes this command) and the proofs
in `Spa / Language / Tagged / Properties.lean`.
Scope: the generator handles non - indexed inductives whose constructor fields are
either scalars or *direct* references to a family member (which covers the object
language). Nested occurrences such as `List Tᵢ` are not supported.
-/
open Lean Elab Command Meta
namespace Spa . DeriveTagged
/-- One constructor field, classified as a recursive family reference or a scalar
(whose type syntax we keep verbatim for the mirror inductive). -/
structure FieldData where
isRec : Bool
recType : Name
typeStx : Term
/-- A constructor: its original (full) name, short name, and fields. -/
structure CtorData where
origName : Name
shortName : Name
fields : Array FieldData
/-- A family member together with its constructors. -/
structure TypeData where
name : Name
ctors : Array CtorData
def taggedOf ( n : Name ) : Name : = n + + `Tagged
def eraseOf ( n : Name ) : Name : = n + + `Tagged + + `erase
def rootTagOf ( n : Name ) : Name : = n + + `Tagged + + `rootTag
def tagOf ( n : Name ) : Name : = n + + `tag
def foldTagsOf ( n : Name ) : Name : = n + + `Tagged + + `foldTags
def wfOf ( n : Name ) : Name : = n + + `Tagged + + `WF
def narrowOf ( n : Name ) : Name : = n + + `Tagged + + `narrow
def narrowEraseOf ( n : Name ) : Name : = n + + `Tagged + + `narrow_erase
def tagLeOf ( n : Name ) : Name : = n + + `tag_le
def tagRootTagPostOf ( n : Name ) : Name : = n + + `tag_rootTag_post
def tagWfOf ( n : Name ) : Name : = n + + `tag_wf
/-- Project the `i` - th conjunct (1 - based) out of `hyp`, which has type a
right - nested `And` of `total` conjuncts, e.g. `hyp |>.2 |>.2 |>.1`. -/
def projAnd { m : Type → Type } [ Monad m ] [ MonadQuotation m ]
( hyp : Term ) ( i total : Nat ) : m Term : = do
let mut t : = hyp
for _ in [ 0 : i - 1 ] do
t ← ` ( $ t | > . 2 )
if i < total then
t ← ` ( $ t | > . 1 )
return t
/-- Combine a non - empty array of propositions into a right - nested conjunction. -/
def mkAndR { m : Type → Type } [ Monad m ] [ MonadQuotation m ]
( cs : Array Term ) : m Term : = do
let mut t : = cs . back!
for c in cs . pop . reverse do
t ← ` ( $ c ∧ $ t )
return t
/-- For a constructor, return one entry per *recursive* field: its argument
identifier, the family member it references, and the start - counter expression at
which it is tagged (`n`, then `(a.tag n).2`, …) — the same threading `mkTag`
uses. -/
def recChildren ( cd : CtorData ) ( argNames : Array Ident ) ( nStart : Term ) :
CommandElabM ( Array ( Ident × Name × Term ) ) : = do
let mut res : Array ( Ident × Name × Term ) : = # [ ]
let mut cur : = nStart
for ( f , a ) in cd . fields . zip argNames do
if f . isRec then
res : = res . push ( a , f . recType , cur )
cur ← ` ( ( $ ( mkIdent ( tagOf f . recType ) ) $ a $ cur ) | > . 2 )
return res
/-- Inspect the family, classifying each constructor field. -/
def gather ( family : Array Name ) ( τ : Ident ) : TermElabM ( Array TypeData ) : = do
let famSet : NameSet : = family . foldl ( · . insert · ) { }
family . mapM fun tn = > do
let iv ← getConstInfoInduct tn
let ctors ← iv . ctors . toArray . mapM fun cn = > do
let cv ← getConstInfoCtor cn
let fields ← forallTelescopeReducing cv . type fun args _ = > do
let fieldArgs : = args . extract iv . numParams args . size
fieldArgs . mapM fun a = > do
let ty ← inferType a
match ty . getAppFn . constName? with
| some hn = >
if famSet . contains hn then
return { isRec : = true , recType : = hn , typeStx : = ← ` ( $ ( mkIdent ( taggedOf hn ) ) $ τ ) }
else
return { isRec : = false , recType : = default , typeStx : = ← Lean . PrettyPrinter . delab ty }
| none = >
return { isRec : = false , recType : = default , typeStx : = ← Lean . PrettyPrinter . delab ty }
return { origName : = cn , shortName : = cn . componentsRev . head! , fields }
return { name : = tn , ctors }
/-- The arrow type `τ → <fields…> → Self τ` of a tagged constructor. -/
def ctorArrow ( cd : CtorData ) ( self : Term ) ( τ : Ident ) : TermElabM Term : = do
let mut t : = self
for f in cd . fields . reverse do
t ← ` ( $ ( f . typeStx ) → $ t )
` ( $ τ → $ t )
/-- The tagged mirror inductives, one per family member. The family is a DAG
(`Expr ← BasicStmt ← Stmt`), not genuinely mutual, so they are emitted as
separate inductives in dependency order rather than a `mutual` block.
`Functor` / `Traversable` instances are derived separately by `mkDeriveInstances`
below rather than via an inline `deriving` clause. -/
def mkInductives ( tds : Array TypeData ) ( τ : Ident ) :
CommandElabM ( Array ( TSyntax `command ) ) : = do
tds . mapM fun td = > do
let self ← ` ( $ ( mkIdent ( taggedOf td . name ) ) $ τ )
let ctors ← td . ctors . mapM fun cd = > do
let aty ← Command . liftTermElabM ( ctorArrow cd self τ )
` ( Lean . Parser . Command . ctor | | $ ( mkIdent cd . shortName ) : ident : $ aty )
` ( command | inductive $ ( mkIdent ( taggedOf td . name ) ) : ident ( $ τ : Type ) where $ ctors * )
/-- A `deriving instance Functor, Traversable for Tᵢ.Tagged` command per family
member. Since every tagged type is a single - parameter, direct - recursive
inductive in `τ`, Mathlib's deriving handler produces clean (`sorry` - free)
instances, giving `map`, `traverse`, and the `Traversable.foldr` / `toList` folds
for free.
These are emitted as *separate* commands in dependency order (rather than an
inline `deriving` clause on each inductive) for two reasons: deriving
`Stmt.Tagged` needs the `Expr.Tagged` / `BasicStmt.Tagged` instances already in
scope, and — because every member's type name ends in `.Tagged` — the handler's
auto - generated instance name (`instFunctorTagged`, built from the type's last
component) collides across the family unless each derive sees the environment
the previous one updated; separate commands give it that, so the names
disambiguate to `instFunctorTagged`, `instFunctorTagged_1`, ….
The hand - written `foldTags` is retained alongside these: it is a
structural - recursion fold that `simp` / `decide` reduce cleanly, unlike the
abstract `Traversable.foldr` (defined via the `FreeMonoid` / `Const` applicative),
which reduces under `decide` / `rfl` but not naive `simp` unfolding. -/
def mkDeriveInstances ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
tds . mapM fun td = >
` ( command | deriving instance Functor , Traversable for $ ( mkIdent ( taggedOf td . name ) ) )
/-- The `erase` functions, one per family member (separate defs in dependency
order — each calls only already - defined lower members). -/
def mkErase ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
tds . mapM fun td = > do
let mut pats : Array Term : = # [ ]
let mut rhss : Array Term : = # [ ]
for cd in td . ctors do
let argNames : = ( Array . range cd . fields . size ) . map ( fun i = > mkIdent ( . mkSimple s! " a{i} " ) )
let pat ← ` ( $ ( mkIdent ( taggedOf td . name + + cd . shortName ) ) _ $ argNames * )
let eraseArgs ← ( cd . fields . zip argNames ) . mapM fun ( f , a ) = >
if f . isRec then ` ( $ ( mkIdent ( eraseOf f . recType ) ) $ a ) else pure a
let rhs ← ` ( $ ( mkIdent cd . origName ) $ eraseArgs * )
pats : = pats . push pat
rhss : = rhss . push rhs
` ( command | def $ ( mkIdent ( eraseOf td . name ) ) { τ : Type } :
$ ( mkIdent ( taggedOf td . name ) ) τ → $ ( mkIdent td . name ) : =
fun x = > match x with $ [ | $ pats = > $ rhss ] * )
/-- The `rootTag` accessors (one non - recursive `def` per type). -/
def mkRootTag ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let tIdent : = mkIdent `t
tds . mapM fun td = > do
let mut pats : Array Term : = # [ ]
let mut rhss : Array Term : = # [ ]
for cd in td . ctors do
let hole ← ` ( _ )
let wilds : = Array . mkArray cd . fields . size hole
pats : = pats . push ( ← ` ( $ ( mkIdent ( taggedOf td . name + + cd . shortName ) ) $ tIdent $ wilds * ) )
rhss : = rhss . push tIdent
` ( command | def $ ( mkIdent ( rootTagOf td . name ) ) { τ : Type } :
$ ( mkIdent ( taggedOf td . name ) ) τ → τ : =
fun x = > match x with $ [ | $ pats = > $ rhss ] * )
/-- The postorder `tag` functions, one per family member (separate defs in
dependency order). -/
def mkTag ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let nId : = mkIdent ``Spa.RawId
tds . mapM fun td = > do
let mut pats : Array Term : = # [ ]
let mut rhss : Array Term : = # [ ]
for cd in td . ctors do
let argNames : = ( Array . range cd . fields . size ) . map ( fun i = > mkIdent ( . mkSimple s! " a{i} " ) )
let pat ← ` ( $ ( mkIdent cd . origName ) $ argNames * )
let mut cur : Term ← ` ( n )
let mut lets : Array ( Ident × Term ) : = # [ ]
let mut taggedArgs : Array Term : = # [ ]
let mut ri : = 0
for ( f , a ) in cd . fields . zip argNames do
if f . isRec then
let rName : = mkIdent ( . mkSimple s! " r{ri} " )
let rhsCall ← ` ( $ ( mkIdent ( tagOf f . recType ) ) $ a $ cur )
lets : = lets . push ( rName , rhsCall )
taggedArgs : = taggedArgs . push ( ← ` ( $ rName | > . 1 ) )
cur ← ` ( $ rName | > . 2 )
ri : = ri + 1
else
taggedArgs : = taggedArgs . push a
let last : = cur
let tagged ← ` ( $ ( mkIdent ( taggedOf td . name + + cd . shortName ) )
( ⟨ $ last ⟩ : $ nId ) $ taggedArgs * )
let mut body ← ` ( ( $ tagged , $ last + 1 ) )
for ( rName , rhs ) in lets . reverse do
body ← ` ( let $ rName : = $ rhs ; $ body )
pats : = pats . push pat
rhss : = rhss . push body
` ( command | def $ ( mkIdent ( tagOf td . name ) ) :
$ ( mkIdent td . name ) → Nat → $ ( mkIdent ( taggedOf td . name ) ) $ nId × Nat : =
fun e n = > match e with $ [ | $ pats = > $ rhss ] * )
/-- The tag - fold functions: `foldTags f acc t` applies `f` to every tag in `t`,
right - to - left, threading `acc`. This is the `Foldable` / `foldr` - over - tags the
hand - written collectors (e.g. `subtreeIds`) reduce to. One separate def per
family member (the family is a DAG, so no `mutual` block is needed). -/
def mkFoldTags ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let τ : = mkIdent `τ
let m : = mkIdent `M
let fId : = mkIdent `f
let accId : = mkIdent `acc
let tagId : = mkIdent `t
tds . mapM fun td = > do
let mut pats : Array Term : = # [ ]
let mut rhss : Array Term : = # [ ]
for cd in td . ctors do
let argNames : = ( Array . range cd . fields . size ) . map ( fun i = > mkIdent ( . mkSimple s! " a{i} " ) )
let pat ← ` ( $ ( mkIdent ( taggedOf td . name + + cd . shortName ) ) $ tagId $ argNames * )
let mut body : Term : = accId
for ( fld , a ) in ( cd . fields . zip argNames ) . reverse do
if fld . isRec then
body ← ` ( $ ( mkIdent ( foldTagsOf fld . recType ) ) $ fId $ body $ a )
body ← ` ( $ fId $ tagId $ body )
pats : = pats . push pat
rhss : = rhss . push body
` ( command | def $ ( mkIdent ( foldTagsOf td . name ) ) { $ τ : ident : Type } { $ m : ident : Type }
( $ fId : $ τ → $ m → $ m ) ( $ accId : $ m ) :
$ ( mkIdent ( taggedOf td . name ) ) $ τ → $ m : =
fun x = > match x with $ [ | $ pats = > $ rhss ] * )
/-- The well - formedness predicate `T.Tagged.WF : T.Tagged RawId → Prop`: every
recursive child's root tag has a strictly smaller postorder index than the node's
own tag, and each child is itself well - formed. Leaf constructors are `True`. -/
def mkWF ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let tId : = mkIdent `t
let rawId : = mkIdent ``Spa.RawId
tds . mapM fun td = > do
let mut pats : Array Term : = # [ ]
let mut rhss : Array Term : = # [ ]
for cd in td . ctors do
let hasRec : = cd . fields . any ( · . isRec )
let mut patArgs : Array Term : = # [ ]
let mut recArgs : Array Ident : = # [ ]
let mut i : = 0
for f in cd . fields do
if f . isRec then
let a : = mkIdent ( . mkSimple s! " a{i} " )
patArgs : = patArgs . push a
recArgs : = recArgs . push a
else
patArgs : = patArgs . push ( ← ` ( _ ) )
i : = i + 1
let tagBind : Term ← if hasRec then ` ( $ tId ) else ` ( _ )
let pat ← ` ( $ ( mkIdent ( taggedOf td . name + + cd . shortName ) ) $ tagBind $ patArgs * )
let rhs ← if recArgs . isEmpty then ` ( True ) else do
let bounds ← recArgs . mapM fun a = > ` ( $ ( a ) . rootTag . post < $ ( tId ) . post )
let wfs ← recArgs . mapM fun a = > ` ( $ ( a ) . WF )
mkAndR ( bounds + + wfs )
pats : = pats . push pat
rhss : = rhss . push rhs
` ( command | def $ ( mkIdent ( wfOf td . name ) ) :
$ ( mkIdent ( taggedOf td . name ) ) $ rawId → Prop : =
fun x = > match x with $ [ | $ pats = > $ rhss ] * )
/-- The `narrow` coercion `T.Tagged RawId → T.Tagged (Fin N)`, given a bound on
the root tag and a well - formedness proof. Each node's tag becomes the `Fin N`
built from its postorder index, and recursion threads the bound through `lt_trans`
and the (definitionally unfolded) `WF` conjunction. -/
def mkNarrow ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let rawId : = mkIdent ``Spa.RawId
let tId : = mkIdent `t
let nId : = mkIdent `N
let hId : = mkIdent `h
let hwfId : = mkIdent `hwf
let tgId : = mkIdent `tg
tds . mapM fun td = > do
let self ← ` ( $ ( mkIdent ( taggedOf td . name ) ) $ rawId )
let mut patss : Array ( Array Term ) : = # [ ]
let mut rhss : Array Term : = # [ ]
for cd in td . ctors do
let argNames : = ( Array . range cd . fields . size ) . map fun i = > mkIdent ( . mkSimple s! " a{i} " )
let ctorPat ← ` ( $ ( mkIdent ( taggedOf td . name + + cd . shortName ) ) $ tgId $ argNames * )
let k : = ( cd . fields . filter ( · . isRec ) ) . size
let mut newArgs : Array Term : = # [ ]
let mut ri : = 0
for ( f , a ) in cd . fields . zip argNames do
if f . isRec then
let bound ← projAnd hwfId ( ri + 1 ) ( 2 * k )
let wf ← projAnd hwfId ( k + ri + 1 ) ( 2 * k )
newArgs : = newArgs . push ( ← ` ( $ ( a ) . narrow ( lt_trans $ bound $ hId ) $ wf ) )
ri : = ri + 1
else
newArgs : = newArgs . push a
let built ← ` ( $ ( mkIdent ( taggedOf td . name + + cd . shortName ) ) ⟨ $ ( tgId ) . post , $ hId ⟩ $ newArgs * )
let nPat ← ` ( _ )
let hPat ← ` ( $ hId )
let hwfPat : Term ← if k = = 0 then ` ( _ ) else ` ( $ hwfId )
patss : = patss . push # [ ctorPat , nPat , hPat , hwfPat ]
rhss : = rhss . push built
` ( command | def $ ( mkIdent ( narrowOf td . name ) ) : ( $ tId : $ self ) → { $ nId : ℕ } →
$ ( tId ) . rootTag . post < $ nId → $ ( tId ) . WF → $ ( mkIdent ( taggedOf td . name ) ) ( Fin $ nId )
$ [ | $ [ $ patss ] , * = > $ rhss ] * )
/-- `T.tag_rootTag_post`: the root tag of a freshly tagged node is exactly one
below the threaded - out counter, i.e. the node itself is numbered last (postorder).
A uniform `cases <;> simp` discharges every constructor. -/
def mkTagRootTagPost ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let eId : = mkIdent `e
let nId : = mkIdent `n
tds . mapM fun td = >
` ( command | theorem $ ( mkIdent ( tagRootTagPostOf td . name ) )
( $ eId : $ ( mkIdent td . name ) ) ( $ nId : ℕ ) :
( $ ( eId ) . tag $ nId ) . 1 . rootTag . post + 1 = ( $ ( eId ) . tag $ nId ) . 2 : = by
cases $ eId : ident < ; >
simp [ $ ( mkIdent ( tagOf td . name ) ) : ident , $ ( mkIdent ( rootTagOf td . name ) ) : ident ] )
/-- `T.tag_le`: tagging only ever advances the counter (`n ≤ (e.tag n).2`).
Proved by induction; each arm threads the counter through its recursive children
(using the relevant `tag_le` / induction hypothesis) and closes with `omega`. -/
def mkTagLe ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let eId : = mkIdent `e
let nId : = mkIdent `n
tds . mapM fun td = > do
let mut ctorLabels : Array Ident : = # [ ]
let mut binderss : Array ( Array Ident ) : = # [ ]
let mut tacs : Array ( TSyntax ``Lean.Parser.Tactic.tacticSeq ) : = # [ ]
for cd in td . ctors do
let argNames : = ( Array . range cd . fields . size ) . map fun i = > mkIdent ( . mkSimple s! " a{i} " )
let mut ihBinders : Array Ident : = # [ ]
let mut haveTacs : Array ( TSyntax `tactic ) : = # [ ]
let mut cur : Term ← ` ( $ nId )
let mut i : = 0
for ( f , a ) in cd . fields . zip argNames do
if f . isRec then
let fact ← if f . recType = = td . name then
` ( $ ( mkIdent ( . mkSimple s! " ih{i} " ) ) $ cur )
else
` ( $ ( mkIdent ( tagLeOf f . recType ) ) $ a $ cur )
if f . recType = = td . name then
ihBinders : = ihBinders . push ( mkIdent ( . mkSimple s! " ih{i} " ) )
haveTacs : = haveTacs . push ( ← ` ( tactic | have : = $ fact ) )
cur ← ` ( ( $ ( mkIdent ( tagOf f . recType ) ) $ a $ cur ) | > . 2 )
i : = i + 1
let simpTac ← ` ( tactic | simp only [ $ ( mkIdent ( tagOf td . name ) ) : ident ] )
let omegaTac ← ` ( tactic | omega )
let allTacs : = # [ simpTac ] + + haveTacs + + # [ omegaTac ]
ctorLabels : = ctorLabels . push ( mkIdent cd . shortName )
binderss : = binderss . push ( argNames + + ihBinders )
tacs : = tacs . push ( ← ` ( tacticSeq | $ [ $ allTacs ] * ) )
` ( command | theorem $ ( mkIdent ( tagLeOf td . name ) ) ( $ eId : $ ( mkIdent td . name ) ) ( $ nId : ℕ ) :
$ nId ≤ ( $ ( eId ) . tag $ nId ) . 2 : = by
induction $ eId : ident generalizing $ nId : ident with
$ [ | $ ctorLabels : ident $ binderss * = > $ tacs ] * )
/-- `T.tag_wf`: a freshly tagged term is well - formed. Each recursive child's
bound conjunct is closed by `omega` from that child's `tag_rootTag_post` plus the
`tag_le` of every later child (which bounds the threaded - out counter), and each
well - formedness conjunct is the child's induction hypothesis / `tag_wf`. -/
def mkTagWf ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let eId : = mkIdent `e
let nId : = mkIdent `n
tds . mapM fun td = > do
let mut ctorLabels : Array Ident : = # [ ]
let mut binderss : Array ( Array Ident ) : = # [ ]
let mut tacs : Array ( TSyntax ``Lean.Parser.Tactic.tacticSeq ) : = # [ ]
for cd in td . ctors do
let argNames : = ( Array . range cd . fields . size ) . map fun i = > mkIdent ( . mkSimple s! " a{i} " )
-- recursive children: (arg, recType, startCounter, sameType?, fieldIndex)
let mut recs : Array ( Ident × Name × Term × Bool × Nat ) : = # [ ]
let mut cur : Term ← ` ( $ nId )
let mut i : = 0
for ( f , a ) in cd . fields . zip argNames do
if f . isRec then
recs : = recs . push ( a , f . recType , cur , f . recType = = td . name , i )
cur ← ` ( ( $ ( mkIdent ( tagOf f . recType ) ) $ a $ cur ) | > . 2 )
i : = i + 1
let k : = recs . size
let ihBinders : = ( recs . filter ( · . 2 . 2 . 2 . 1 ) ) . map fun r = > mkIdent ( . mkSimple s! " ih{r.2.2.2.2} " )
let tac : TSyntax ``Lean.Parser.Tactic.tacticSeq ← if k = = 0 then
` ( tacticSeq | exact True . intro )
else do
let mut comps : Array Term : = # [ ]
-- bound conjuncts
for idx in [ 0 : k ] do
let ( a , rt , s , _ , _ ) : = recs [ idx ] !
let mut bHaves : Array ( TSyntax `tactic ) : =
# [ ← ` ( tactic | have : = $ ( mkIdent ( tagRootTagPostOf rt ) ) $ a $ s ) ]
for j in [ idx + 1 : k ] do
let ( aj , rtj , sj , _ , _ ) : = recs [ j ] !
bHaves : = bHaves . push ( ← ` ( tactic | have : = $ ( mkIdent ( tagLeOf rtj ) ) $ aj $ sj ) )
bHaves : = bHaves . push ( ← ` ( tactic | omega ) )
comps : = comps . push ( ← ` ( by $ ( ← ` ( tacticSeq | $ [ $ bHaves ] * ) ) ) )
-- well-formedness conjuncts
for idx in [ 0 : k ] do
let ( a , rt , s , same , fi ) : = recs [ idx ] !
comps : = comps . push < | ← if same then ` ( $ ( mkIdent ( . mkSimple s! " ih{fi} " ) ) $ s )
else ` ( $ ( mkIdent ( tagWfOf rt ) ) $ a $ s )
let simpTac ← ` ( tactic | simp only
[ $ ( mkIdent ( tagOf td . name ) ) : ident , $ ( mkIdent ( wfOf td . name ) ) : ident ] )
let exactTac ← ` ( tactic | exact ⟨ $ comps , * ⟩ )
` ( tacticSeq | $ [ $ ( # [ simpTac , exactTac ] ) ] * )
ctorLabels : = ctorLabels . push ( mkIdent cd . shortName )
binderss : = binderss . push ( argNames + + ihBinders )
tacs : = tacs . push tac
` ( command | theorem $ ( mkIdent ( tagWfOf td . name ) ) ( $ eId : $ ( mkIdent td . name ) ) ( $ nId : ℕ ) :
( $ ( eId ) . tag $ nId ) . 1 . WF : = by
induction $ eId : ident generalizing $ nId : ident with
$ [ | $ ctorLabels : ident $ binderss * = > $ tacs ] * )
/-- `T.Tagged.narrow_erase`: narrowing the tag type does not change the erased
(untagged) term. A per - constructor `simp` with the local `narrow` / `erase`
equations, the lower members' `narrow_erase`, and the induction hypotheses. -/
def mkNarrowErase ( tds : Array TypeData ) : CommandElabM ( Array ( TSyntax `command ) ) : = do
let rawId : = mkIdent ``Spa.RawId
let tId : = mkIdent `t
let nId : = mkIdent `N
let hId : = mkIdent `h
let hwfId : = mkIdent `hwf
let tgId : = mkIdent `tg
tds . mapM fun td = > do
let mut ctorLabels : Array Ident : = # [ ]
let mut binderss : Array ( Array Ident ) : = # [ ]
let mut tacs : Array ( TSyntax ``Lean.Parser.Tactic.tacticSeq ) : = # [ ]
for cd in td . ctors do
let argNames : = ( Array . range cd . fields . size ) . map fun i = > mkIdent ( . mkSimple s! " a{i} " )
let mut lemmas : Array Term : =
# [ ← ` ( $ ( mkIdent ( narrowOf td . name ) ) ) , ← ` ( $ ( mkIdent ( eraseOf td . name ) ) ) ]
let mut ihBinders : Array Ident : = # [ ]
let mut seenLower : Array Name : = # [ ]
let mut i : = 0
for f in cd . fields do
if f . isRec then
if f . recType = = td . name then
let ih : = mkIdent ( . mkSimple s! " ih{i} " )
ihBinders : = ihBinders . push ih
lemmas : = lemmas . push ( ← ` ( $ ih ) )
else if ! seenLower . contains f . recType then
seenLower : = seenLower . push f . recType
lemmas : = lemmas . push ( ← ` ( $ ( mkIdent ( narrowEraseOf f . recType ) ) ) )
i : = i + 1
let introTac ← ` ( tactic | intro $ nId $ hId $ hwfId )
let simpTac ← ` ( tactic | simp [ $ [ $ lemmas : term ] , * ] )
ctorLabels : = ctorLabels . push ( mkIdent cd . shortName )
binderss : = binderss . push ( # [ tgId ] + + argNames + + ihBinders )
tacs : = tacs . push ( ← ` ( tacticSeq | $ [ $ ( # [ introTac , simpTac ] ) ] * ) )
` ( command | theorem $ ( mkIdent ( narrowEraseOf td . name ) ) :
( $ tId : $ ( mkIdent ( taggedOf td . name ) ) $ rawId ) → ∀ { $ nId : ℕ }
( $ hId : $ ( tId ) . rootTag . post < $ nId ) ( $ hwfId : $ ( tId ) . WF ) ,
( $ ( tId ) . narrow $ hId $ hwfId ) . erase = $ ( tId ) . erase : = by
intro $ tId : ident
induction $ tId : ident with
$ [ | $ ctorLabels : ident $ binderss * = > $ tacs ] * )
/-- `derive_tagged T₁ … Tₙ` — generate tagged mirrors, `erase`, and `tag` for the
given family of inductives. -/
syntax ( name : = deriveTaggedCmd ) " derive_tagged " ident + : command
@[ command_elab deriveTaggedCmd ]
def elabDeriveTagged : CommandElab : = fun stx = > do
match stx with
| ` ( derive_tagged $ ids * ) = >
let family ← ids . mapM fun i = > Command . liftCoreM ( realizeGlobalConstNoOverload i )
let τ : = mkIdent `τ
let tds ← Command . liftTermElabM ( gather family τ )
for d in ( ← mkInductives tds τ ) do elabCommand d
for d in ( ← mkDeriveInstances tds ) do elabCommand d
for d in ( ← mkRootTag tds ) do elabCommand d
for d in ( ← mkErase tds ) do elabCommand d
for d in ( ← mkTag tds ) do elabCommand d
for d in ( ← mkFoldTags tds ) do elabCommand d
for d in ( ← mkWF tds ) do elabCommand d
for d in ( ← mkNarrow tds ) do elabCommand d
for d in ( ← mkTagRootTagPost tds ) do elabCommand d
for d in ( ← mkTagLe tds ) do elabCommand d
for d in ( ← mkTagWf tds ) do elabCommand d
for d in ( ← mkNarrowErase tds ) do elabCommand d
| _ = > throwUnsupportedSyntax
end Spa . DeriveTagged
