From fb574af873d7109164a5a10c3d995334a124f84d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Jun 2022 19:38:54 -0700 Subject: [PATCH] fix: `mkSplitterProof` This commit fixes the first issue reported at #1179 closes #1179 --- src/Lean/Meta/Match/MatchEqs.lean | 194 ++++++++++++++++++++++++++---- tests/lean/run/1179b.lean | 19 +++ 2 files changed, 190 insertions(+), 23 deletions(-) create mode 100644 tests/lean/run/1179b.lean diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index ac6d207f83..b0e0861c58 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -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}" diff --git a/tests/lean/run/1179b.lean b/tests/lean/run/1179b.lean new file mode 100644 index 0000000000..6448ceaadd --- /dev/null +++ b/tests/lean/run/1179b.lean @@ -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