refactor: instances that "hide" coercions
Example: ``` instance [CoeHTCT α β] [Add β] : HAdd α β β where hAdd a b := Add.add a b ```
This commit is contained in:
Leonardo de Moura
parent
452b717a97
commit
4b58c4cc02
5 changed files with 142 additions and 192 deletions
|
|
@ -145,53 +145,3 @@ instance [CoeFun α (fun _ => β)] : CoeTail α β where
|
|||
|
||||
instance [CoeSort α β] : CoeTail α β where
|
||||
coe a := coeSort a
|
||||
|
||||
/- Coe and heterogeneous operators, we use `CoeHTCT` instead of `CoeT` to avoid expensive coercions such as `CoeDep` -/
|
||||
|
||||
instance [CoeHTCT α β] [Add β] : HAdd α β β where
|
||||
hAdd a b := Add.add a b
|
||||
|
||||
instance [CoeHTCT α β] [Add β] : HAdd β α β where
|
||||
hAdd a b := Add.add a b
|
||||
|
||||
instance [CoeHTCT α β] [Sub β] : HSub α β β where
|
||||
hSub a b := Sub.sub a b
|
||||
|
||||
instance [CoeHTCT α β] [Sub β] : HSub β α β where
|
||||
hSub a b := Sub.sub a b
|
||||
|
||||
instance [CoeHTCT α β] [Mul β] : HMul α β β where
|
||||
hMul a b := Mul.mul a b
|
||||
|
||||
instance [CoeHTCT α β] [Mul β] : HMul β α β where
|
||||
hMul a b := Mul.mul a b
|
||||
|
||||
instance [CoeHTCT α β] [Div β] : HDiv α β β where
|
||||
hDiv a b := Div.div a b
|
||||
|
||||
instance [CoeHTCT α β] [Div β] : HDiv β α β where
|
||||
hDiv a b := Div.div a b
|
||||
|
||||
instance [CoeHTCT α β] [Mod β] : HMod α β β where
|
||||
hMod a b := Mod.mod a b
|
||||
|
||||
instance [CoeHTCT α β] [Mod β] : HMod β α β where
|
||||
hMod a b := Mod.mod a b
|
||||
|
||||
instance [CoeHTCT α β] [Append β] : HAppend α β β where
|
||||
hAppend a b := Append.append a b
|
||||
|
||||
instance [CoeHTCT α β] [Append β] : HAppend β α β where
|
||||
hAppend a b := Append.append a b
|
||||
|
||||
instance [CoeHTCT α β] [OrElse β] : HOrElse α β β where
|
||||
hOrElse a b := OrElse.orElse a b
|
||||
|
||||
instance [CoeHTCT α β] [OrElse β] : HOrElse β α β where
|
||||
hOrElse a b := OrElse.orElse a b
|
||||
|
||||
instance [CoeHTCT α β] [AndThen β] : HAndThen α β β where
|
||||
hAndThen a b := AndThen.andThen a b
|
||||
|
||||
instance [CoeHTCT α β] [AndThen β] : HAndThen β α β where
|
||||
hAndThen a b := AndThen.andThen a b
|
||||
|
|
|
|||
|
|
@ -78,10 +78,10 @@ instance : LT JsonNumber :=
|
|||
|
||||
instance (a b : JsonNumber) : Decidable (a < b) :=
|
||||
inferInstanceAs (Decidable (lt a b = true))
|
||||
|
||||
|
||||
instance : Ord JsonNumber where
|
||||
compare x y :=
|
||||
if x < y then Ordering.lt
|
||||
compare x y :=
|
||||
if x < y then Ordering.lt
|
||||
else if x > y then Ordering.gt
|
||||
else Ordering.eq
|
||||
|
||||
|
|
@ -99,7 +99,7 @@ protected def toString : JsonNumber → String
|
|||
let exp := if exp < 0 then exp else 0
|
||||
let e' := (10 : Int) ^ (e - exp.natAbs)
|
||||
let left := (m / e').repr
|
||||
let right := e' + m % e'
|
||||
let right := e' + coe m % e'
|
||||
|>.repr.toSubstring.drop 1
|
||||
|>.dropRightWhile (fun c => c = '0')
|
||||
|>.toString
|
||||
|
|
@ -188,14 +188,14 @@ def getNum? : Json → Except String JsonNumber
|
|||
| _ => throw "number expected"
|
||||
|
||||
def getObjVal? : Json → String → Except String Json
|
||||
| obj kvs, k =>
|
||||
| obj kvs, k =>
|
||||
match kvs.find compare k with
|
||||
| some v => v
|
||||
| none => throw s!"property not found: {k}"
|
||||
| _ , _ => throw "object expected"
|
||||
|
||||
def getArrVal? : Json → Nat → Except String Json
|
||||
| arr a, i =>
|
||||
| arr a, i =>
|
||||
match a.get? i with
|
||||
| some v => v
|
||||
| none => throw s!"index out of bounds: {i}"
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
|
|||
| u::us => do
|
||||
let mut m := m!".\{{u}"
|
||||
for u in us do
|
||||
m := m ++ ", " ++ u
|
||||
m := m ++ ", " ++ toMessageData u
|
||||
return m ++ "}"
|
||||
|
||||
private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
|
||||
|
|
|
|||
|
|
@ -280,7 +280,7 @@ partial def Struct.allDefault (s : Struct) : Bool :=
|
|||
| FieldVal.nested s => allDefault s
|
||||
|
||||
def formatField (formatStruct : Struct → Format) (field : Field Struct) : Format :=
|
||||
Format.joinSep field.lhs " . " ++ " := " ++
|
||||
Format.joinSep field.lhs " . " ++ format " := " ++
|
||||
match field.val with
|
||||
| FieldVal.term v => v.prettyPrint
|
||||
| FieldVal.nested s => formatStruct s
|
||||
|
|
|
|||
|
|
@ -16,11 +16,11 @@ open Match
|
|||
register_builtin_option maxBackwardChainingDepth : Nat := {
|
||||
defValue := 10
|
||||
descr := "The maximum search depth used in the backwards chaining part of the proof of `brecOn` for inductive predicates."
|
||||
}
|
||||
}
|
||||
|
||||
/--
|
||||
The context used in the creation of the `below` scheme for inductive predicates.
|
||||
-/
|
||||
-/
|
||||
structure Context where
|
||||
motives : Array (Name × Expr)
|
||||
typeInfos : Array InductiveVal
|
||||
|
|
@ -40,7 +40,7 @@ structure Variables where
|
|||
motives : Array Expr
|
||||
innerType : Expr
|
||||
deriving Inhabited
|
||||
|
||||
|
||||
/--
|
||||
Collection of variables used to keep track of the local context used in the `brecOn` proof.
|
||||
-/
|
||||
|
|
@ -58,46 +58,46 @@ def mkContext (declName : Name) : MetaM Context := do
|
|||
let motives ←motiveTypes.mapIdxM fun j motive => do
|
||||
(←motiveName motiveTypes j.val, motive)
|
||||
let headers := typeInfos.mapM $ mkHeader motives indVal.numParams
|
||||
return {
|
||||
return {
|
||||
motives := motives
|
||||
typeInfos := typeInfos
|
||||
numParams := indVal.numParams
|
||||
headers := ←headers
|
||||
belowNames := ←indVal.all.toArray.map (· ++ `below) }
|
||||
where
|
||||
motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name :=
|
||||
if motiveTypes.size > 1
|
||||
where
|
||||
motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name :=
|
||||
if motiveTypes.size > 1
|
||||
then mkFreshUserName s!"motive_{i.succ}"
|
||||
else mkFreshUserName "motive"
|
||||
|
||||
mkHeader
|
||||
(motives : Array (Name × Expr))
|
||||
(numParams : Nat)
|
||||
mkHeader
|
||||
(motives : Array (Name × Expr))
|
||||
(numParams : Nat)
|
||||
(indVal : InductiveVal) : MetaM Expr := do
|
||||
let header ← forallTelescope indVal.type fun xs t => do
|
||||
withNewBinderInfos (xs.map fun x => (x.fvarId!, BinderInfo.implicit)) $
|
||||
mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) t
|
||||
addMotives motives numParams header
|
||||
|
||||
addMotives (motives : Array (Name × Expr)) (numParams : Nat) : Expr → MetaM Expr :=
|
||||
motives.foldrM (fun (motiveName, motive) t =>
|
||||
forallTelescope t fun xs s => do
|
||||
addMotives (motives : Array (Name × Expr)) (numParams : Nat) : Expr → MetaM Expr :=
|
||||
motives.foldrM (fun (motiveName, motive) t =>
|
||||
forallTelescope t fun xs s => do
|
||||
let motiveType ← instantiateForall motive xs[:numParams]
|
||||
withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do
|
||||
mkForallFVars (xs.insertAt numParams motive) s)
|
||||
|
||||
motiveType (indVal : InductiveVal) : MetaM Expr :=
|
||||
|
||||
motiveType (indVal : InductiveVal) : MetaM Expr :=
|
||||
forallTelescope indVal.type fun xs t => do
|
||||
mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) (mkSort levelZero)
|
||||
|
||||
mkIndValConst (indVal : InductiveVal) : Expr :=
|
||||
mkConst indVal.name $ indVal.levelParams.map mkLevelParam
|
||||
|
||||
partial def mkCtorType
|
||||
(ctx : Context)
|
||||
(belowIdx : Nat)
|
||||
(originalCtor : ConstructorVal) : MetaM Expr :=
|
||||
forallTelescope originalCtor.type fun xs t => addHeaderVars
|
||||
|
||||
partial def mkCtorType
|
||||
(ctx : Context)
|
||||
(belowIdx : Nat)
|
||||
(originalCtor : ConstructorVal) : MetaM Expr :=
|
||||
forallTelescope originalCtor.type fun xs t => addHeaderVars
|
||||
{ innerType := t
|
||||
indVal := #[]
|
||||
motives := #[]
|
||||
|
|
@ -110,13 +110,13 @@ where
|
|||
(ctx.belowNames[idx], fun _ => pure header)
|
||||
|
||||
withLocalDeclsD headersWithNames fun xs =>
|
||||
addMotives { vars with indVal := xs }
|
||||
addMotives { vars with indVal := xs }
|
||||
|
||||
addMotives (vars : Variables) := do
|
||||
let motiveBuilders ← ctx.motives.mapM fun (motiveName, motiveType) =>
|
||||
(motiveName, BinderInfo.implicit, fun _ =>
|
||||
let motiveBuilders ← ctx.motives.mapM fun (motiveName, motiveType) =>
|
||||
(motiveName, BinderInfo.implicit, fun _ =>
|
||||
instantiateForall motiveType vars.params)
|
||||
withLocalDecls motiveBuilders fun xs =>
|
||||
withLocalDecls motiveBuilders fun xs =>
|
||||
modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0
|
||||
|
||||
modifyBinders (vars : Variables) (i : Nat) := do
|
||||
|
|
@ -131,24 +131,24 @@ where
|
|||
else modifyBinders { vars with target := vars.target.push binder } i.succ
|
||||
else rebuild vars
|
||||
|
||||
rebuild (vars : Variables) :=
|
||||
rebuild (vars : Variables) :=
|
||||
vars.innerType.withApp fun f args => do
|
||||
let hApp :=
|
||||
mkAppN
|
||||
let hApp :=
|
||||
mkAppN
|
||||
(mkConst originalCtor.name $ ctx.typeInfos[0].levelParams.map mkLevelParam)
|
||||
(vars.params ++ vars.args)
|
||||
let innerType := mkAppN vars.indVal[belowIdx] $
|
||||
vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
|
||||
let x ← mkForallFVars vars.target innerType
|
||||
let x ← mkForallFVars vars.target innerType
|
||||
replaceTempVars vars x
|
||||
|
||||
replaceTempVars (vars : Variables) (ctor : Expr) :=
|
||||
let levelParams :=
|
||||
let levelParams :=
|
||||
ctx.typeInfos[0].levelParams.map mkLevelParam
|
||||
|
||||
ctor.replaceFVars vars.indVal $ ctx.belowNames.map fun indVal =>
|
||||
mkConst indVal levelParams
|
||||
|
||||
|
||||
checkCount (domain : Expr) : MetaM Bool := do
|
||||
let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
|
||||
let (_, cnt) ←run $ transform domain fun e => do
|
||||
|
|
@ -158,15 +158,15 @@ where
|
|||
set $ cnt + 1
|
||||
TransformStep.visit e
|
||||
|
||||
if cnt > 1 then
|
||||
if cnt > 1 then
|
||||
throwError "only arrows are allowed as premises. Multiple recursive occurrences detected:{indentExpr domain}"
|
||||
|
||||
|
||||
return cnt == 1
|
||||
|
||||
mkBelowBinder
|
||||
(vars : Variables)
|
||||
(binder : Expr)
|
||||
(domain : Expr)
|
||||
|
||||
mkBelowBinder
|
||||
(vars : Variables)
|
||||
(binder : Expr)
|
||||
(domain : Expr)
|
||||
{α : Type} (k : Nat → Expr → MetaM α) : MetaM α := do
|
||||
forallTelescope domain fun xs t => do
|
||||
let fail _ := do
|
||||
|
|
@ -174,33 +174,33 @@ where
|
|||
|
||||
t.withApp fun f args => do
|
||||
if let some name := f.constName? then
|
||||
if let some idx := ctx.typeInfos.findIdx?
|
||||
if let some idx := ctx.typeInfos.findIdx?
|
||||
fun indVal => indVal.name == name then
|
||||
let indVal := ctx.typeInfos[idx]
|
||||
let hApp := mkAppN binder xs
|
||||
let t :=
|
||||
let t :=
|
||||
mkAppN vars.indVal[idx] $
|
||||
vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
|
||||
let newDomain ← mkForallFVars xs t
|
||||
|
||||
|
||||
withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain (k idx)
|
||||
else fail ()
|
||||
else fail ()
|
||||
|
||||
mkMotiveBinder
|
||||
(vars : Variables)
|
||||
(indValIdx : Nat)
|
||||
(binder : Expr)
|
||||
(domain : Expr)
|
||||
mkMotiveBinder
|
||||
(vars : Variables)
|
||||
(indValIdx : Nat)
|
||||
(binder : Expr)
|
||||
(domain : Expr)
|
||||
{α : Type} (k : Expr → MetaM α) : MetaM α := do
|
||||
forallTelescope domain fun xs t => do
|
||||
t.withApp fun f args => do
|
||||
let hApp := mkAppN binder xs
|
||||
let t := mkAppN vars.motives[indValIdx] $ args[ctx.numParams:] ++ #[hApp]
|
||||
let newDomain ← mkForallFVars xs t
|
||||
|
||||
withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain k
|
||||
|
||||
|
||||
withLocalDecl (←copyVarName binder.fvarId!) binder.binderInfo newDomain k
|
||||
|
||||
copyVarName (oldName : FVarId) : MetaM Name := do
|
||||
let binderDecl ← getLocalDecl oldName
|
||||
mkFreshUserName binderDecl.userName
|
||||
|
|
@ -209,13 +209,13 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor :=
|
|||
let ctorInfo ← getConstInfoCtor ctor
|
||||
let name := ctor.updatePrefix ctx.belowNames[i]
|
||||
let type ← mkCtorType ctx i ctorInfo
|
||||
return {
|
||||
return {
|
||||
name := name
|
||||
type := type }
|
||||
|
||||
def mkInductiveType
|
||||
(ctx : Context)
|
||||
(i : Fin ctx.typeInfos.size)
|
||||
def mkInductiveType
|
||||
(ctx : Context)
|
||||
(i : Fin ctx.typeInfos.size)
|
||||
(indVal : InductiveVal) : MetaM InductiveType := do
|
||||
return {
|
||||
name := ctx.belowNames[i]
|
||||
|
|
@ -224,8 +224,8 @@ def mkInductiveType
|
|||
|
||||
def mkBelowDecl (ctx : Context) : MetaM Declaration := do
|
||||
let lparams := ctx.typeInfos[0].levelParams
|
||||
Declaration.inductDecl
|
||||
lparams
|
||||
Declaration.inductDecl
|
||||
lparams
|
||||
(ctx.numParams + ctx.motives.size)
|
||||
(←ctx.typeInfos.mapIdxM $ mkInductiveType ctx).toList
|
||||
ctx.typeInfos[0].isUnsafe
|
||||
|
|
@ -234,24 +234,24 @@ partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
|
|||
if depth = 0 then false
|
||||
else
|
||||
withMVarContext m do
|
||||
let lctx ← getLCtx
|
||||
let lctx ← getLCtx
|
||||
let mTy ← getMVarType m
|
||||
lctx.anyM fun localDecl =>
|
||||
if localDecl.isAuxDecl then
|
||||
false
|
||||
else
|
||||
lctx.anyM fun localDecl =>
|
||||
if localDecl.isAuxDecl then
|
||||
false
|
||||
else
|
||||
commitWhen do
|
||||
let (mvars, _, t) ← forallMetaTelescope localDecl.type
|
||||
if ←isDefEq mTy t then
|
||||
if ←isDefEq mTy t then
|
||||
assignExprMVar m (mkAppN localDecl.toExpr mvars)
|
||||
mvars.allM fun v =>
|
||||
mvars.allM fun v =>
|
||||
isExprMVarAssigned v.mvarId! <||> backwardsChaining v.mvarId! (depth - 1)
|
||||
else false
|
||||
|
||||
|
||||
partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) : MetaM Expr := do
|
||||
let main ← mkFreshExprSyntheticOpaqueMVar type
|
||||
let (m, vars) ← intros main.mvarId!
|
||||
let [m] ← applyIH m vars |
|
||||
let [m] ← applyIH m vars |
|
||||
throwError "applying the induction hypothesis should only return one goal"
|
||||
let ms ← induction m vars
|
||||
let ms ← applyCtors ms
|
||||
|
|
@ -268,11 +268,11 @@ where
|
|||
return (m, ⟨params, motives, indices, witness, indHyps⟩)
|
||||
|
||||
applyIH (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
|
||||
match ←vars.indHyps.findSomeM?
|
||||
match ←vars.indHyps.findSomeM?
|
||||
(fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with
|
||||
| some goals => goals
|
||||
| none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}"
|
||||
|
||||
|
||||
induction (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
|
||||
let params := vars.params.map mkFVar
|
||||
let motives := vars.motives.map mkFVar
|
||||
|
|
@ -282,17 +282,17 @@ where
|
|||
forallTelescope motive fun xs _ => do
|
||||
mkLambdaFVars xs $ mkAppN (mkConst ctx.belowNames[idx] levelParams) $ (params ++ motives ++ xs)
|
||||
let recursorInfo ← getConstInfo $ mkRecName indVal.name
|
||||
let recLevels :=
|
||||
if recursorInfo.numLevelParams > levelParams.length
|
||||
then levelZero::levelParams
|
||||
else levelParams
|
||||
let recLevels :=
|
||||
if recursorInfo.numLevelParams > levelParams.length
|
||||
then levelZero::levelParams
|
||||
else levelParams
|
||||
let recursor ← mkAppN (mkConst recursorInfo.name $ recLevels) $ params ++ motives
|
||||
apply m recursor
|
||||
|
||||
apply m recursor
|
||||
|
||||
applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
|
||||
let mss ← ms.toArray.mapIdxM fun idx m => do
|
||||
let m ← introNPRec m
|
||||
(←getMVarType m).withApp fun below args =>
|
||||
let m ← introNPRec m
|
||||
(←getMVarType m).withApp fun below args =>
|
||||
withMVarContext m do
|
||||
args.back.withApp fun ctor ctorArgs => do
|
||||
let ctorName := ctor.constName!.updatePrefix below.constName!
|
||||
|
|
@ -300,24 +300,24 @@ where
|
|||
let ctorInfo ← getConstInfoCtor ctorName
|
||||
let (mvars, _, t) ← forallMetaTelescope ctorInfo.type
|
||||
let ctor := mkAppN ctor mvars
|
||||
apply m ctor
|
||||
apply m ctor
|
||||
return mss.foldr List.append []
|
||||
|
||||
introNPRec (m : MVarId) : MetaM MVarId := do
|
||||
if (←getMVarType m).isForall then introNPRec (←intro1P m).2 else m
|
||||
|
||||
|
||||
closeGoal (vars : BrecOnVariables) (maxDepth : Nat) (m : MVarId) : MetaM Unit := do
|
||||
unless ←isExprMVarAssigned m do
|
||||
let m ← introNPRec m
|
||||
unless ←backwardsChaining m maxDepth do
|
||||
withMVarContext m do
|
||||
throwError "couldn't solve by backwards chaining ({``maxBackwardChainingDepth} = {maxDepth}): {MessageData.ofGoal m}"
|
||||
|
||||
|
||||
def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
|
||||
let type ← mkType
|
||||
let indVal := ctx.typeInfos[idx]
|
||||
let name := indVal.name ++ brecOnSuffix
|
||||
Declaration.thmDecl {
|
||||
Declaration.thmDecl {
|
||||
name := name
|
||||
levelParams := indVal.levelParams
|
||||
type := type
|
||||
|
|
@ -331,22 +331,22 @@ where
|
|||
let motiveBinders ← ctx.motives.mapIdxM $ mkIH params motives
|
||||
withLocalDeclsD motiveBinders fun ys => do
|
||||
mkForallFVars (xs ++ ys) (mkAppN motives[idx] indices)
|
||||
mkIH
|
||||
mkIH
|
||||
(params : Array Expr)
|
||||
(motives : Array Expr)
|
||||
(idx : Fin ctx.motives.size)
|
||||
(idx : Fin ctx.motives.size)
|
||||
(motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do
|
||||
let name :=
|
||||
if ctx.motives.size > 1
|
||||
then mkFreshUserName s!"ih_{idx.val.succ}"
|
||||
else mkFreshUserName "ih"
|
||||
let ih ← instantiateForall motive.2 params
|
||||
let mkDomain _ :=
|
||||
let mkDomain _ :=
|
||||
forallTelescope ih fun ys t => do
|
||||
let levels := ctx.typeInfos[idx].levelParams.map mkLevelParam
|
||||
let args := params ++ motives ++ ys
|
||||
let premise :=
|
||||
mkAppN
|
||||
mkAppN
|
||||
(mkConst ctx.belowNames[idx.val] levels) args
|
||||
let conclusion :=
|
||||
mkAppN motives[idx] ys
|
||||
|
|
@ -359,22 +359,22 @@ partial def getBelowIndices (ctorName : Name) : MetaM $ Array Nat := do
|
|||
let belowCtorInfo ← getConstInfoCtor (ctorName.updatePrefix $ ctorInfo.induct ++ `below)
|
||||
let belowInductInfo ← getConstInfoInduct belowCtorInfo.induct
|
||||
forallTelescope ctorInfo.type fun xs t => do
|
||||
loop xs belowCtorInfo.type #[] 0 0
|
||||
loop xs belowCtorInfo.type #[] 0 0
|
||||
|
||||
where
|
||||
loop
|
||||
(xs : Array Expr)
|
||||
(rest : Expr)
|
||||
(belowIndices : Array Nat)
|
||||
(xIdx yIdx : Nat) : MetaM $ Array Nat := do
|
||||
where
|
||||
loop
|
||||
(xs : Array Expr)
|
||||
(rest : Expr)
|
||||
(belowIndices : Array Nat)
|
||||
(xIdx yIdx : Nat) : MetaM $ Array Nat := do
|
||||
if xIdx ≥ xs.size then belowIndices else
|
||||
let x := xs[xIdx]
|
||||
let xTy ← inferType x
|
||||
let yTy := rest.bindingDomain!
|
||||
if ←isDefEq xTy yTy then
|
||||
if ←isDefEq xTy yTy then
|
||||
let rest ← instantiateForall rest #[x]
|
||||
loop xs rest (belowIndices.push yIdx) (xIdx + 1) (yIdx + 1)
|
||||
else
|
||||
else
|
||||
forallBoundedTelescope rest (some 1) fun ys rest =>
|
||||
loop xs rest belowIndices xIdx (yIdx + 1)
|
||||
|
||||
|
|
@ -389,33 +389,33 @@ private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Na
|
|||
/-- This function adds an additional `below` discriminant to a matcher application.
|
||||
It is used for modifying the patterns, such that the structural recursion can use the new
|
||||
`below` predicate instead of the original one and thus be used prove structural recursion.
|
||||
|
||||
|
||||
It takes as parameters:
|
||||
- matcherApp: a matcher application
|
||||
- belowMotive: the motive, that the `below` type should carry
|
||||
- below: an expression from the local context that is the `below` version of a predicate
|
||||
and can be used for structural recursion
|
||||
- idx: the index of the original predicate discriminant.
|
||||
|
||||
|
||||
It returns:
|
||||
- A matcher application as an expression
|
||||
- A side-effect for adding the matcher to the environment -/
|
||||
partial def mkBelowMatcher
|
||||
(matcherApp : MatcherApp)
|
||||
(belowMotive : Expr)
|
||||
(matcherApp : MatcherApp)
|
||||
(belowMotive : Expr)
|
||||
(below : Expr)
|
||||
(idx : Nat) : MetaM $ Expr × MetaM Unit := do
|
||||
let mkMatcherInput ← getMkMatcherInputInContext matcherApp
|
||||
let (indName, belowType, motive, matchType) ←
|
||||
let (indName, belowType, motive, matchType) ←
|
||||
forallBoundedTelescope mkMatcherInput.matchType mkMatcherInput.numDiscrs fun xs t => do
|
||||
let (indName, belowType) ← belowType belowMotive xs idx
|
||||
let matchType ←
|
||||
let matchType ←
|
||||
withLocalDeclD (←mkFreshUserName `h_below) belowType fun h_below => do
|
||||
mkForallFVars (xs.push h_below) t
|
||||
let motive ← newMotive belowType xs
|
||||
(indName, belowType.replaceFVars xs matcherApp.discrs, motive, matchType)
|
||||
|
||||
let lhss ← mkMatcherInput.lhss.mapM $ addBelowPattern indName
|
||||
let lhss ← mkMatcherInput.lhss.mapM $ addBelowPattern indName
|
||||
let alts ← mkMatcherInput.lhss.zip lhss |>.toArray.zip matcherApp.alts |>.mapIdxM fun idx ((oldLhs, lhs), alt) => do
|
||||
withExistingLocalDecls (oldLhs.fvarDecls ++ lhs.fvarDecls) do
|
||||
lambdaTelescope alt fun xs t => do
|
||||
|
|
@ -427,8 +427,8 @@ partial def mkBelowMatcher
|
|||
| 0, n+1 => xs[1:]
|
||||
| _, _ => xs
|
||||
let t := t.replaceFVars xs[:oldFVars.size] fvars[:oldFVars.size]
|
||||
trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size].toArray ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray}"
|
||||
let newAlt ← mkLambdaFVars (fvars[:oldFVars.size].toArray ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray) t
|
||||
trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray}"
|
||||
let newAlt ← mkLambdaFVars (fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:].toArray) t
|
||||
trace[Meta.IndPredBelow.match] "alt {idx}:\n{alt} ↦ {newAlt}"
|
||||
newAlt
|
||||
|
||||
|
|
@ -447,20 +447,20 @@ partial def mkBelowMatcher
|
|||
let newApp := mkAppN newApp alts
|
||||
(newApp, res.addMatcher)
|
||||
|
||||
where
|
||||
where
|
||||
addBelowPattern (indName : Name) (lhs : AltLHS) : MetaM AltLHS := do
|
||||
withExistingLocalDecls lhs.fvarDecls do
|
||||
let patterns := lhs.patterns.toArray
|
||||
let originalPattern := patterns[idx]
|
||||
let (fVars, belowPattern) ← convertToBelow indName patterns[idx]
|
||||
withExistingLocalDecls fVars.toList do
|
||||
let patterns := patterns.push belowPattern
|
||||
let patterns := patterns.push belowPattern
|
||||
let patterns := patterns.set! idx (←toInaccessible originalPattern)
|
||||
{ lhs with patterns := patterns.toList, fvarDecls := lhs.fvarDecls ++ fVars.toList }
|
||||
|
||||
|
||||
/--
|
||||
this function changes the type of the pattern from the original type to the `below` version thereof.
|
||||
Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't
|
||||
Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't
|
||||
simply recursively change all occurrences, but rather, we recursively change occurences of the constructor.
|
||||
As such there are only a few cases:
|
||||
- the pattern is a constructor from the original type. Here we need to:
|
||||
|
|
@ -471,20 +471,20 @@ where
|
|||
- it is an `as` pattern. Here the contstructor could be hidden inside of it.
|
||||
- it is a variable. Here you we need to introduce a fresh variable of a different type.
|
||||
-/
|
||||
convertToBelow (indName : Name)
|
||||
(originalPattern : Pattern) : MetaM $ Array LocalDecl × Pattern := do
|
||||
convertToBelow (indName : Name)
|
||||
(originalPattern : Pattern) : MetaM $ Array LocalDecl × Pattern := do
|
||||
match originalPattern with
|
||||
| Pattern.ctor ctorName us params fields =>
|
||||
| Pattern.ctor ctorName us params fields =>
|
||||
let ctorInfo ← getConstInfoCtor ctorName
|
||||
|
||||
|
||||
let belowCtor ← getConstInfoCtor $ ctorName.updatePrefix $ ctorInfo.induct ++ `below
|
||||
let belowIndices ← IndPredBelow.getBelowIndices ctorName
|
||||
let belowIndices := belowIndices[ctorInfo.numParams:].toArray.map (· - belowCtor.numParams)
|
||||
|
||||
-- belowFieldOpts starts off with an array of empty fields.
|
||||
-- We then go over pattern's fields and set the appropriate fields to values.
|
||||
-- In general, there are fewer `fields` than `belowFieldOpts`, because the
|
||||
-- `belowCtor` carries a `below`, a non-`below` and a `motive` version of each
|
||||
-- In general, there are fewer `fields` than `belowFieldOpts`, because the
|
||||
-- `belowCtor` carries a `below`, a non-`below` and a `motive` version of each
|
||||
-- field that occurs in a recursive application of the inductive predicate.
|
||||
-- `belowIndices` is a mapping from non-`below` to the `below` version of each field.
|
||||
let mut belowFieldOpts := mkArray belowCtor.numFields none
|
||||
|
|
@ -494,32 +494,32 @@ where
|
|||
|
||||
let belowParams := params.toArray.push belowMotive
|
||||
let belowCtorExpr := mkAppN (mkConst belowCtor.name us) belowParams
|
||||
let (additionalFVars, belowFields) ← transformFields belowCtorExpr indName belowFieldOpts
|
||||
|
||||
let (additionalFVars, belowFields) ← transformFields belowCtorExpr indName belowFieldOpts
|
||||
|
||||
withExistingLocalDecls additionalFVars.toList do
|
||||
let ctor := Pattern.ctor belowCtor.name us belowParams.toList belowFields.toList
|
||||
trace[Meta.IndPredBelow.match] "{originalPattern.toMessageData} ↦ {ctor.toMessageData}"
|
||||
(additionalFVars, ctor)
|
||||
| Pattern.as varId p =>
|
||||
(additionalFVars, ctor)
|
||||
| Pattern.as varId p =>
|
||||
let (additionalFVars, p) ← convertToBelow indName p
|
||||
(additionalFVars, Pattern.as varId p)
|
||||
| Pattern.var varId =>
|
||||
| Pattern.var varId =>
|
||||
let var := mkFVar varId
|
||||
(←inferType var).withApp fun ind args => do
|
||||
let (_, tgtType) ← belowType belowMotive #[var] 0
|
||||
withLocalDeclD (←mkFreshUserName `h) tgtType fun h => do
|
||||
let localDecl ← getFVarLocalDecl h
|
||||
(#[localDecl], Pattern.var h.fvarId!)
|
||||
| p => (#[], p)
|
||||
| p => (#[], p)
|
||||
|
||||
transformFields belowCtor indName belowFieldOpts :=
|
||||
transformFields belowCtor indName belowFieldOpts :=
|
||||
let rec loop
|
||||
(belowCtor : Expr)
|
||||
(belowCtor : Expr)
|
||||
(belowFieldOpts : Array $ Option Pattern)
|
||||
(belowFields : Array Pattern)
|
||||
(belowFields : Array Pattern)
|
||||
(additionalFVars : Array LocalDecl) : MetaM (Array LocalDecl × Array Pattern) := do
|
||||
if belowFields.size ≥ belowFieldOpts.size then (additionalFVars, belowFields) else
|
||||
if let some belowField := belowFieldOpts[belowFields.size] then
|
||||
if let some belowField := belowFieldOpts[belowFields.size] then
|
||||
let belowFieldExpr ← belowField.toExpr
|
||||
let belowCtor := mkApp belowCtor belowFieldExpr
|
||||
let patTy ← inferType belowFieldExpr
|
||||
|
|
@ -529,54 +529,54 @@ where
|
|||
let (fvars, transformedField) ← convertToBelow indName belowField
|
||||
withExistingLocalDecls fvars.toList do
|
||||
let belowFieldOpts := belowFieldOpts.set! (belowFields.size + 1) transformedField
|
||||
let belowField :=
|
||||
match belowField with
|
||||
| Pattern.ctor .. => Pattern.inaccessible belowFieldExpr
|
||||
let belowField :=
|
||||
match belowField with
|
||||
| Pattern.ctor .. => Pattern.inaccessible belowFieldExpr
|
||||
| _ => belowField
|
||||
loop belowCtor belowFieldOpts (belowFields.push belowField) (additionalFVars ++ fvars)
|
||||
else
|
||||
loop belowCtor belowFieldOpts (belowFields.push belowField) additionalFVars
|
||||
loop belowCtor belowFieldOpts (belowFields.push belowField) additionalFVars
|
||||
else
|
||||
let ctorType ← inferType belowCtor
|
||||
withLocalDeclD (←mkFreshUserName `a) ctorType.bindingDomain! fun a => do
|
||||
let localDecl ← getFVarLocalDecl a
|
||||
loop (mkApp belowCtor a) belowFieldOpts (belowFields.push $ Pattern.var a.fvarId!) (additionalFVars.push localDecl)
|
||||
loop (mkApp belowCtor a) belowFieldOpts (belowFields.push $ Pattern.var a.fvarId!) (additionalFVars.push localDecl)
|
||||
loop belowCtor belowFieldOpts #[] #[]
|
||||
|
||||
toInaccessible : Pattern → MetaM Pattern
|
||||
|
||||
toInaccessible : Pattern → MetaM Pattern
|
||||
| Pattern.inaccessible p => Pattern.inaccessible p
|
||||
| Pattern.var v => Pattern.var v
|
||||
| p => do Pattern.inaccessible $ ←p.toExpr
|
||||
|
||||
newMotive (belowType : Expr) (ys : Array Expr) : MetaM Expr :=
|
||||
newMotive (belowType : Expr) (ys : Array Expr) : MetaM Expr :=
|
||||
lambdaTelescope matcherApp.motive fun xs t => do
|
||||
let numDiscrs := matcherApp.discrs.size
|
||||
withLocalDeclD (←mkFreshUserName `h_below) (←belowType.replaceFVars ys xs) fun h_below => do
|
||||
let motive ← mkLambdaFVars (xs[:numDiscrs] ++ #[h_below] ++ xs[numDiscrs:]) t
|
||||
trace[Meta.IndPredBelow.match] "motive := {motive}"
|
||||
motive
|
||||
|
||||
|
||||
def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
|
||||
xs.findSomeM? fun x => do
|
||||
let xTy ← inferType x
|
||||
xTy.withApp fun f args =>
|
||||
xTy.withApp fun f args =>
|
||||
match f.constName?, xs.indexOf? x with
|
||||
| some name, some idx => do
|
||||
if ←isInductivePredicate name then
|
||||
let (_, belowTy) ← belowType motive xs idx
|
||||
let below ← mkFreshExprSyntheticOpaqueMVar belowTy
|
||||
try
|
||||
try
|
||||
trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
|
||||
if ←backwardsChaining below.mvarId! 10 then
|
||||
trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
|
||||
if ←xs.anyM (isDefEq below) then none else (below, idx.val)
|
||||
else
|
||||
else
|
||||
trace[Meta.IndPredBelow.match] "could not find below term in the local context"
|
||||
none
|
||||
catch _ => none
|
||||
else none
|
||||
| _, _ => none
|
||||
|
||||
|
||||
def mkBelow (declName : Name) : MetaM Unit := do
|
||||
if (←isInductivePredicate declName) then
|
||||
let x ← getConstInfoInduct declName
|
||||
|
|
@ -598,4 +598,4 @@ builtin_initialize
|
|||
registerTraceClass `Meta.IndPredBelow
|
||||
registerTraceClass `Meta.IndPredBelow.match
|
||||
|
||||
end Lean.Meta.IndPredBelow
|
||||
end Lean.Meta.IndPredBelow
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue