fix: mkSplitterProof
This commit fixes the first issue reported at #1179 closes #1179
This commit is contained in:
Leonardo de Moura
parent
46257dfb0e
commit
fb574af873
2 changed files with 190 additions and 23 deletions
|
|
@ -364,6 +364,9 @@ private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult :=
|
|||
pure ()
|
||||
return InjectionAnyResult.failed
|
||||
|
||||
|
||||
private abbrev ConvertM := ReaderT (FVarIdMap (Expr × Nat × Array Bool)) $ StateRefT (Array MVarId) MetaM
|
||||
|
||||
/--
|
||||
Construct a proof for the splitter generated by `mkEquationsfor`.
|
||||
The proof uses the definition of the `match`-declaration as a template (argument `template`).
|
||||
|
|
@ -375,7 +378,7 @@ private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (al
|
|||
(altArgMasks : Array (Array Bool)) : MetaM Expr := do
|
||||
trace[Meta.Match.matchEqs] "proof template: {template}"
|
||||
let map := mkMap
|
||||
let (proof, mvarIds) ← convertTemplate map |>.run #[]
|
||||
let (proof, mvarIds) ← convertTemplate template |>.run map |>.run #[]
|
||||
trace[Meta.Match.matchEqs] "splitter proof: {proof}"
|
||||
for mvarId in mvarIds do
|
||||
proveSubgoal mvarId
|
||||
|
|
@ -395,28 +398,173 @@ where
|
|||
else
|
||||
argMask
|
||||
|
||||
convertTemplate (m : FVarIdMap (Expr × Nat × Array Bool)) : StateRefT (Array MVarId) MetaM Expr :=
|
||||
transform template fun e => do
|
||||
match e.getAppFn with
|
||||
| Expr.fvar fvarId .. =>
|
||||
match m.find? fvarId with
|
||||
| some (altNew, numParams, argMask) =>
|
||||
trace[Meta.Match.matchEqs] ">> argMask: {argMask}, e: {e}, {altNew}"
|
||||
let mut newArgs := #[]
|
||||
let argMask := trimFalseTrail argMask
|
||||
unless e.getAppNumArgs ≥ argMask.size do
|
||||
throwError "unexpected occurrence of `match`-expression alternative (aka minor premise) while creating splitter/eliminator theorem for `{matchDeclName}`, minor premise is partially applied{indentExpr e}\npossible solution if you are matching on inductive families: add its indices as additional discriminants"
|
||||
for arg in e.getAppArgs, includeArg in argMask do
|
||||
if includeArg then
|
||||
newArgs := newArgs.push arg
|
||||
let eNew := mkAppN altNew newArgs
|
||||
/- Recall that `numParams` does not include the equalities associated with discriminants of the form `h : discr`. -/
|
||||
let (mvars, _, _) ← forallMetaBoundedTelescope (← inferType eNew) (numParams - newArgs.size) (kind := MetavarKind.syntheticOpaque)
|
||||
modify fun s => s ++ (mvars.map (·.mvarId!))
|
||||
let eNew := mkAppN eNew mvars
|
||||
return TransformStep.done eNew
|
||||
| none => return TransformStep.visit e
|
||||
| _ => return TransformStep.visit e
|
||||
/--
|
||||
Auxiliary function used at `convertTemplate` to decide whether to use `convertCastEqRec`.
|
||||
See `convertCastEqRec`. -/
|
||||
isCastEqRec (e : Expr) : ConvertM Bool := do
|
||||
-- TODO: we do not handle `Eq.rec` since we never found an example that needed it.
|
||||
-- If we find one we must extend `convertCastEqRec`.
|
||||
unless e.isAppOf ``Eq.ndrec do return false
|
||||
unless e.getAppNumArgs > 6 do return false
|
||||
for arg in e.getAppArgs[6:] do
|
||||
if arg.isFVar && (← read).contains arg.fvarId! then
|
||||
return true
|
||||
return true
|
||||
|
||||
/--
|
||||
Auxiliary function used at `convertTemplate`. It is needed when the auxiliary `match` declaration had to refine the type of its
|
||||
minor premises during dependent pattern match. For an example, consider
|
||||
```
|
||||
inductive Foo : Nat → Type _
|
||||
| nil : Foo 0
|
||||
| cons (t: Foo l): Foo l
|
||||
|
||||
def Foo.bar (t₁: Foo l₁): Foo l₂ → Bool
|
||||
| cons s₁ => t₁.bar s₁
|
||||
| _ => false
|
||||
attribute [simp] Foo.bar
|
||||
```
|
||||
The auxiliary `Foo.bar.match_1` is of the form
|
||||
```
|
||||
def Foo.bar.match_1.{u_1} : {l₂ : Nat} →
|
||||
(t₂ : Foo l₂) →
|
||||
(motive : Foo l₂ → Sort u_1) →
|
||||
(t₂ : Foo l₂) → ((s₁ : Foo l₂) → motive (Foo.cons s₁)) → ((x : Foo l₂) → motive x) → motive t₂ :=
|
||||
fun {l₂} t₂ motive t₂_1 h_1 h_2 =>
|
||||
(fun t₂_2 =>
|
||||
Foo.casesOn (motive := fun a x => l₂ = a → HEq t₂_1 x → motive t₂_1) t₂_2
|
||||
(fun h =>
|
||||
Eq.ndrec (motive := fun {l₂} =>
|
||||
(t₂ t₂ : Foo l₂) →
|
||||
(motive : Foo l₂ → Sort u_1) →
|
||||
((s₁ : Foo l₂) → motive (Foo.cons s₁)) → ((x : Foo l₂) → motive x) → HEq t₂ Foo.nil → motive t₂)
|
||||
(fun t₂ t₂ motive h_1 h_2 h => Eq.symm (eq_of_heq h) ▸ h_2 Foo.nil) (Eq.symm h) t₂ t₂_1 motive h_1 h_2) --- HERE
|
||||
fun {l} t h =>
|
||||
Eq.ndrec (motive := fun {l} => (t : Foo l) → HEq t₂_1 (Foo.cons t) → motive t₂_1)
|
||||
(fun t h => Eq.symm (eq_of_heq h) ▸ h_1 t) h t)
|
||||
t₂_1 (Eq.refl l₂) (HEq.refl t₂_1)
|
||||
```
|
||||
The `HERE` comment marks the place where the type of `Foo.bar.match_1` minor premises `h_1` and `h_2` is being "refined"
|
||||
using `Eq.ndrec`.
|
||||
|
||||
This function will adjust the motive and minor premise of the `Eq.ndrec` to reflect the new minor premises used in the
|
||||
corresponding splitter theorem.
|
||||
|
||||
We may have to extend this function to handle `Eq.rec` too.
|
||||
|
||||
This function was added to address issue #1179
|
||||
-/
|
||||
convertCastEqRec (e : Expr) : ConvertM Expr := do
|
||||
assert! (← isCastEqRec e)
|
||||
e.withApp fun f args => do
|
||||
let mut argsNew := args
|
||||
let mut isAlt := #[]
|
||||
for i in [6:args.size] do
|
||||
let arg := argsNew[i]
|
||||
if arg.isFVar then
|
||||
match (← read).find? arg.fvarId! with
|
||||
| some (altNew, _, _) =>
|
||||
argsNew := argsNew.set! i altNew
|
||||
trace[Meta.Match.matchEqs] "arg: {arg} : {← inferType arg}, altNew: {altNew} : {← inferType altNew}"
|
||||
isAlt := isAlt.push true
|
||||
| none =>
|
||||
argsNew := argsNew.set! i (← convertTemplate arg)
|
||||
isAlt := isAlt.push false
|
||||
else
|
||||
argsNew := argsNew.set! i (← convertTemplate arg)
|
||||
isAlt := isAlt.push false
|
||||
assert! isAlt.size == args.size - 6
|
||||
let rhs := args[4]
|
||||
let motive := args[2]
|
||||
-- Construct new motive using the splitter theorem minor premise types.
|
||||
let motiveNew ← lambdaTelescope motive fun motiveArgs body => do
|
||||
unless motiveArgs.size == 1 do
|
||||
throwError "unexpected `Eq.ndrec` motive while creating splitter/eliminator theorem for `{matchDeclName}`, expected lambda with 1 binder{indentExpr motive}"
|
||||
let x := motiveArgs[0]
|
||||
forallTelescopeReducing body fun motiveTypeArgs resultType => do
|
||||
unless motiveTypeArgs.size >= isAlt.size do
|
||||
throwError "unexpected `Eq.ndrec` motive while creating splitter/eliminator theorem for `{matchDeclName}`, expected arrow with at least #{isAlt.size} binders{indentExpr body}"
|
||||
let rec go (i : Nat) (motiveTypeArgsNew : Array Expr) : ConvertM Expr := do
|
||||
assert! motiveTypeArgsNew.size == i
|
||||
if h : i < motiveTypeArgs.size then
|
||||
let motiveTypeArg := motiveTypeArgs.get ⟨i, h⟩
|
||||
if i < isAlt.size && isAlt[i] then
|
||||
let altNew := argsNew[6+i] -- Recall that `Eq.ndrec` has 6 arguments
|
||||
let altTypeNew ← inferType altNew
|
||||
trace[Meta.Match.matchEqs] "altNew: {altNew} : {altTypeNew}"
|
||||
-- Replace `rhs` with `x` (the lambda binder in the motive)
|
||||
let mut altTypeNewAbst := (← kabstract altTypeNew rhs).instantiate1 x
|
||||
-- Replace args[6:6+i] with `motiveTypeArgsNew`
|
||||
for j in [:i] do
|
||||
altTypeNewAbst := (← kabstract altTypeNewAbst argsNew[6+j]).instantiate1 motiveTypeArgsNew[j]
|
||||
let localDecl ← getLocalDecl motiveTypeArg.fvarId!
|
||||
withLocalDecl localDecl.userName localDecl.binderInfo altTypeNewAbst fun motiveTypeArgNew =>
|
||||
go (i+1) (motiveTypeArgsNew.push motiveTypeArgNew)
|
||||
else
|
||||
go (i+1) (motiveTypeArgsNew.push motiveTypeArg)
|
||||
else
|
||||
mkLambdaFVars motiveArgs (← mkForallFVars motiveTypeArgsNew resultType)
|
||||
go 0 #[]
|
||||
trace[Meta.Match.matchEqs] "new motive: {motiveNew}"
|
||||
unless (← isTypeCorrect motiveNew) do
|
||||
throwError "failed to construct new type correct motive for `Eq.ndrec` while creating splitter/eliminator theorem for `{matchDeclName}`{indentExpr motiveNew}"
|
||||
argsNew := argsNew.set! 2 motiveNew
|
||||
-- Construct the new minor premise for the `Eq.ndrec` application.
|
||||
-- First, we use `eqRecNewPrefix` to infer the new minor premise binders for `Eq.ndrec`
|
||||
let eqRecNewPrefix := mkAppN f argsNew[:3] -- `Eq.ndrec` minor premise is the fourth argument.
|
||||
let .forallE _ minorTypeNew .. ← whnf (← inferType eqRecNewPrefix) | unreachable!
|
||||
trace[Meta.Match.matchEqs] "new minor type: {minorTypeNew}"
|
||||
let minor := args[3]
|
||||
let minorNew ← forallBoundedTelescope minorTypeNew isAlt.size fun minorArgsNew _ => do
|
||||
let mut minorBodyNew := minor
|
||||
-- We have to extend the mapping to make sure `convertTemplate` can "fix" occurrences of the refined minor premises
|
||||
let mut m ← read
|
||||
for i in [:isAlt.size] do
|
||||
if isAlt[i] then
|
||||
-- `convertTemplate` will correct occurrences of the alternative
|
||||
let alt := args[6+i] -- Recall that `Eq.ndrec` has 6 arguments
|
||||
let some (_, numParams, argMask) := m.find? alt.fvarId! | unreachable!
|
||||
-- We add a new entry to `m` to make sure `convertTemplate` will correct the occurrences of the alternative
|
||||
m := m.insert minorArgsNew[i].fvarId! (minorArgsNew[i], numParams, argMask)
|
||||
unless minorBodyNew.isLambda do
|
||||
throwError "unexpected `Eq.ndrec` minor premise while creating splitter/eliminator theorem for `{matchDeclName}`, expected lambda with at least #{isAlt.size} binders{indentExpr minor}"
|
||||
minorBodyNew := minorBodyNew.bindingBody!
|
||||
minorBodyNew := minorBodyNew.instantiateRev minorArgsNew
|
||||
trace[Meta.Match.matchEqs] "minor premise new body before convertTemplate:{indentExpr minorBodyNew}"
|
||||
minorBodyNew ← withReader (fun _ => m) <| convertTemplate minorBodyNew
|
||||
trace[Meta.Match.matchEqs] "minor premise new body after convertTemplate:{indentExpr minorBodyNew}"
|
||||
mkLambdaFVars minorArgsNew minorBodyNew
|
||||
unless (← isTypeCorrect minorNew) do
|
||||
throwError "failed to construct new type correct minor premise for `Eq.ndrec` while creating splitter/eliminator theorem for `{matchDeclName}`{indentExpr minorNew}"
|
||||
argsNew := argsNew.set! 3 minorNew
|
||||
-- trace[Meta.Match.matchEqs] "argsNew: {argsNew}"
|
||||
trace[Meta.Match.matchEqs] "found cast target {e}"
|
||||
return mkAppN f argsNew
|
||||
|
||||
convertTemplate (e : Expr) : ConvertM Expr :=
|
||||
transform e fun e => do
|
||||
if (← isCastEqRec e) then
|
||||
return .done (← convertCastEqRec e)
|
||||
else match e.getAppFn with
|
||||
| Expr.fvar fvarId .. =>
|
||||
match (← read).find? fvarId with
|
||||
| some (altNew, numParams, argMask) =>
|
||||
trace[Meta.Match.matchEqs] ">> argMask: {argMask}, e: {e}, {altNew}"
|
||||
let mut newArgs := #[]
|
||||
let argMask := trimFalseTrail argMask
|
||||
unless e.getAppNumArgs ≥ argMask.size do
|
||||
throwError "unexpected occurrence of `match`-expression alternative (aka minor premise) while creating splitter/eliminator theorem for `{matchDeclName}`, minor premise is partially applied{indentExpr e}\npossible solution if you are matching on inductive families: add its indices as additional discriminants"
|
||||
for arg in e.getAppArgs, includeArg in argMask do
|
||||
if includeArg then
|
||||
newArgs := newArgs.push arg
|
||||
let eNew := mkAppN altNew newArgs
|
||||
/- Recall that `numParams` does not include the equalities associated with discriminants of the form `h : discr`. -/
|
||||
let (mvars, _, _) ← forallMetaBoundedTelescope (← inferType eNew) (numParams - newArgs.size) (kind := MetavarKind.syntheticOpaque)
|
||||
modify fun s => s ++ (mvars.map (·.mvarId!))
|
||||
let eNew := mkAppN eNew mvars
|
||||
return TransformStep.done eNew
|
||||
| none => return TransformStep.visit e
|
||||
| _ => return TransformStep.visit e
|
||||
|
||||
proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
|
||||
trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}"
|
||||
|
|
|
|||
19
tests/lean/run/1179b.lean
Normal file
19
tests/lean/run/1179b.lean
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
inductive Foo : Nat → Type _
|
||||
| nil : Foo 0
|
||||
| cons (t: Foo l) : Foo l
|
||||
|
||||
def Foo.bar (t₁: Foo l₁) (t₂ : Foo l₂) : Bool :=
|
||||
match t₂ with
|
||||
| cons s₁ => t₁.bar s₁
|
||||
| _ => false
|
||||
|
||||
attribute [simp] Foo.bar
|
||||
|
||||
example (h : t₂ = .nil) : Foo.bar t₁ t₂ = false := by
|
||||
unfold Foo.bar
|
||||
split
|
||||
· contradiction
|
||||
· rfl
|
||||
|
||||
set_option pp.proofs true
|
||||
#print Foo.bar.match_1
|
||||
Loading…
Add table
Reference in a new issue