From 2b9fded6b7dec84189327b3eb77d9bcd5624cc16 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Aug 2021 18:37:12 -0700 Subject: [PATCH] feat: add `splitter` theorem --- src/Lean/Meta/Match/MatchEqs.lean | 61 +++++++++++++++++++------------ 1 file changed, 37 insertions(+), 24 deletions(-) diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 977841e5ed..63f468f4d6 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -10,6 +10,8 @@ import Lean.Meta.Tactic.SplitIf namespace Lean.Meta.Match +-- TODO enviroment extension for caching conditional equation lemmas and splitter for match auxiliary declarations. + private def isMatchValue (e : Expr) : Bool := e.isNatLit || e.isCharLit || e.isStringLit @@ -125,7 +127,7 @@ where /-- Construct new local declarations `xs` with types `altTypes`, and then execute `f xs` -/ -private partial def withElimAlts (altTypes : Array Expr) (f : Array Expr → MetaM α) : MetaM α := do +private partial def withSplitterAlts (altTypes : Array Expr) (f : Array Expr → MetaM α) : MetaM α := do let rec go (i : Nat) (xs : Array Expr) : MetaM α := do if h : i < altTypes.size then let hName := (`h).appendIndexAfter (i+1) @@ -136,21 +138,26 @@ private partial def withElimAlts (altTypes : Array Expr) (f : Array Expr → Met go 0 #[] /-- - Construct a proof for the elimination principle generated by `mkEquationsfor`. + Construct a proof for the splitter generated by `mkEquationsfor`. The proof uses the definition of the `match`-declaration as a template (argument `template`). - `alts` are free variables corresponding to alternatives of the `match` auxiliary declaration being processed. - `altNews` are the new free variables which contains aditional hypotheses that ensure they are only used when the previous overlapping alternatives are not applicable. -/ -private partial def mkElimProof (template : Expr) (alts altsNew : Array Expr) : MetaM Expr := do +private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (alts altsNew : Array Expr) : MetaM Expr := do trace[Meta.Match.matchEqs] "proof template: {template}" let map := mkMap let (proof, mvarIds) ← convertTemplate map |>.run #[] - trace[Meta.Match.matchEqs] "elim proof: {proof}" + trace[Meta.Match.matchEqs] "splitter proof: {proof}" for mvarId in mvarIds do - trace[Meta.Match.matchEqs] "elim subgoal:\n{MessageData.ofGoal mvarId}" - -- TODO: close goal `mvarId` - check proof -- TODO remove - return proof + trace[Meta.Match.matchEqs] "subgoal {mkMVar mvarId}, {repr (← getMVarDecl mvarId).kind}, {← isExprMVarAssigned mvarId}\n{MessageData.ofGoal mvarId}" + let (_, mvarId) ← intros mvarId + let mvarId ← tryClearMany mvarId (alts.map (·.fvarId!)) + unless (← contradictionCore mvarId {}) do + -- TODO + trace[Meta.Match.matchEqs] "failed to generate splitter, unsolved subgoal\n{MessageData.ofGoal mvarId}" + admit mvarId + -- throwError "failed to generate splitter for match auxiliary declaration '{matchDeclName}', unsolved subgoal:\n{MessageData.ofGoal mvarId}" + instantiateMVars proof where mkMap : NameMap Expr := do let mut m := {} @@ -186,14 +193,14 @@ where addExtraParams (e : Expr) : StateRefT (Array MVarId) MetaM Expr := do trace[Meta.Match.matchEqs] "addExtraParams {e}" - let (mvars, _, _) ← forallMetaTelescope (← inferType e) (kind := MetavarKind.syntheticOpaque) + let (mvars, _, _) ← forallMetaTelescopeReducing (← inferType e) (kind := MetavarKind.syntheticOpaque) modify fun s => s ++ (mvars.map (·.mvarId!)) return mkAppN e mvars /-- - Create conditional equations and elimination principle for the given - match auxiliary declaration. -/ + Create conditional equations and splitter for the given match auxiliary declaration. -/ partial def mkEquationsFor (matchDeclName : Name) : MetaM Unit := do + -- TODO: do not assume `mkEquationsFor` was not already generated let constInfo ← getConstInfo matchDeclName let us := constInfo.levelParams.map mkLevelParam let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function" @@ -205,11 +212,11 @@ partial def mkEquationsFor (matchDeclName : Name) : MetaM Unit := do let discrs := xs[firstDiscrIdx : firstDiscrIdx + matchInfo.numDiscrs] let mut notAlts := #[] let mut idx := 1 - let mut elimAltTypes := #[] + let mut splitterAltTypes := #[] for alt in alts do let altType ← inferType alt trace[Meta.debug] ">> {altType}" - let (notAlt, elimAltType) ← forallTelescopeReducing altType fun ys altResultType => do + let (notAlt, splitterAltType) ← forallTelescopeReducing altType fun ys altResultType => do let (ys, rhsArgs) ← toFVarsRHSArgs ys altResultType let patterns := altResultType.getAppArgs let mut hs := #[] @@ -217,7 +224,7 @@ partial def mkEquationsFor (matchDeclName : Name) : MetaM Unit := do hs := hs.push (← instantiateForall notAlt patterns) hs ← simpHs hs patterns.size trace[Meta.Match.matchEqs] "hs: {hs}" - let elimAltType ← mkForallFVars ys (← hs.foldrM (init := altResultType) mkArrow) + let splitterAltType ← mkForallFVars ys (← hs.foldrM (init := altResultType) mkArrow) -- Create a proposition for representing terms that do not match `patterns` let mut notAlt := mkConst ``False for discr in discrs.toArray.reverse, pattern in patterns.reverse do @@ -238,20 +245,26 @@ partial def mkEquationsFor (matchDeclName : Name) : MetaM Unit := do type := thmType value := thmVal } - return (notAlt, elimAltType) + return (notAlt, splitterAltType) notAlts := notAlts.push notAlt - elimAltTypes := elimAltTypes.push elimAltType - trace[Meta.Match.matchEqs] "elimAltType: {elimAltType}" + splitterAltTypes := splitterAltTypes.push splitterAltType + trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}" idx := idx + 1 - -- Define eliminator with conditional/refined alternatives - withElimAlts elimAltTypes fun altsNew => do - let elimType ← mkForallFVars (params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew) matchResultType - trace[Meta.Match.matchEqs] "elimType: {elimType}" + -- Define splitter with conditional/refined alternatives + withSplitterAlts splitterAltTypes fun altsNew => do + let elimParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew + let elimType ← mkForallFVars elimParams matchResultType + trace[Meta.Match.matchEqs] "splitterType: {elimType}" let template ← mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts) let template ← deltaExpand template (. == constInfo.name) - let elimVal ← mkElimProof template alts altsNew - -- TODO: construct value of type `elimType` - return () + let elimVal ← mkLambdaFVars elimParams (← mkSplitterProof matchDeclName template alts altsNew) + let elimName := matchDeclName ++ `elim + addDecl <| Declaration.thmDecl { + name := elimName + levelParams := constInfo.levelParams + type := elimType + value := elimVal + } builtin_initialize registerTraceClass `Meta.Match.matchEqs