f89ed40618
This introduces the `ArgsPacker` module and abstraction, to replace the exising `PackDomain`/`PackMutual` code. The motivation was that we now have more uses besides `Fix.lean` (`GuessLex` and `FunInd`), and the code was spread in various places. The goals are * consistent function naming withing the the `PSigma` handling, the `PSum` handling, and the combined interface * avoid taking a type apart just based on the `PSigma`/`PSum` nesting, to be robust in case the user happens to be using `PSigma`/`PSum` somewhere. Therefore, always pass an `arity` or `numFuncs` or `varNames` around. * keep all the `PSigma`/`PSum` encoding logic contained within one module (`ArgsPacker`), and keep that module independent of its users (so no `EqnInfos` visible here). * pick good variable names when matching on a packed argument * the unary function now is either called `fun1._unary` or `fun1._mutual`, never `fun1._unary._mutual`. This file has less heavy dependencies than `PackMutual` had, so build parallelism is improved as well.
67 lines
2.8 KiB
Text
67 lines
2.8 KiB
Text
inductive Term where
|
|
| const : String → Term
|
|
| app : String → List Term → Term
|
|
|
|
namespace Term
|
|
|
|
mutual
|
|
def numConsts : Term → Nat
|
|
| const _ => 1
|
|
| app _ cs => numConstsLst cs
|
|
|
|
def numConstsLst : List Term → Nat
|
|
| [] => 0
|
|
| c :: cs => numConsts c + numConstsLst cs
|
|
end
|
|
|
|
mutual
|
|
def replaceConst (a b : String) : Term → Term
|
|
| const c => if a == c then const b else const c
|
|
| app f cs => app f (replaceConstLst a b cs)
|
|
|
|
def replaceConstLst (a b : String) : List Term → List Term
|
|
| [] => []
|
|
| c :: cs => replaceConst a b c :: replaceConstLst a b cs
|
|
end
|
|
|
|
derive_functional_induction replaceConst
|
|
|
|
/--
|
|
info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2 : List Term → Prop) (case1 : motive2 [])
|
|
(case2 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1))
|
|
(case3 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1))
|
|
(case4 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs))
|
|
(case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a : Term), motive1 a
|
|
-/
|
|
#guard_msgs in
|
|
#check replaceConst.induct
|
|
|
|
theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
|
|
apply replaceConst.induct
|
|
(motive1 := fun e => numConsts (replaceConst a b e) = numConsts e)
|
|
(motive2 := fun es => numConstsLst (replaceConstLst a b es) = numConstsLst es)
|
|
case case1 => simp [replaceConstLst, numConstsLst, *]
|
|
case case2 => intro c h; guard_hyp h :ₛ (a == c) = true; simp [replaceConst, numConsts, *]
|
|
case case3 => intro c h; guard_hyp h :ₛ ¬(a == c) = true; simp [replaceConst, numConsts, *]
|
|
case case4 =>
|
|
intros f cs ih
|
|
guard_hyp ih :ₛnumConstsLst (replaceConstLst a b cs) = numConstsLst cs
|
|
simp [replaceConst, numConsts, *]
|
|
case case5 =>
|
|
intro c cs ih₁ ih₂
|
|
guard_hyp ih₁ :ₛ numConsts (replaceConst a b c) = numConsts c
|
|
guard_hyp ih₂ :ₛ numConstsLst (replaceConstLst a b cs) = numConstsLst cs
|
|
simp [replaceConstLst, numConstsLst, *]
|
|
|
|
theorem numConsts_replaceConst' (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
|
|
apply replaceConst.induct
|
|
(motive1 := fun e => numConsts (replaceConst a b e) = numConsts e)
|
|
(motive2 := fun es => numConstsLst (replaceConstLst a b es) = numConstsLst es)
|
|
<;> intros <;> simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *]
|
|
|
|
theorem numConsts_replaceConst'' (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
|
|
induction e using replaceConst.induct (a := a) (b := b)
|
|
(motive2 := fun es => numConstsLst (replaceConstLst a b es) = numConstsLst es) <;>
|
|
simp [replaceConst, numConsts, replaceConstLst, numConstsLst, *]
|
|
|
|
end Term
|