From 57bc6e9afb87ba0350c71187e814efd1b7eeeaac Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Sun, 22 Oct 2023 23:51:42 +0100 Subject: [PATCH 01/10] Return a list of initial goals for have --- Examples.lean | 2 +- lean/BetterParser.lean | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Examples.lean b/Examples.lean index 6050498..2500db9 100644 --- a/Examples.lean +++ b/Examples.lean @@ -12,7 +12,7 @@ import Lean import Paperproof example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by - have h3 : m + 3 ≤ 9 := by calc + have h3 : m + 3 ≤ 9 := calc m + 3 ≤ 2 * n - 1 := by gcongr _ ≤ 2 * 5 - 1 := by gcongr _ = 9 := by norm_num diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index 4bf1140..fe3f073 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -34,7 +34,7 @@ structure TacticApplication where inductive ProofStep := | tacticApp (t : TacticApplication) | haveDecl (t: TacticApplication) - (initialGoal: String) + (initialGoals: List GoalInfo) (subSteps : List ProofStep) deriving Inhabited, ToJson, FromJson @@ -143,10 +143,8 @@ partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : R allGoals} let goals := (goalsBefore ++ goalsAfter).foldl HashSet.erase (noInEdgeGoals allGoals steps) - let [initialGoal] := goals.toList -- TODO: have ⟨ p, q ⟩ : (a = a) × (b = b) := ⟨ by rfl, by rfl ⟩ isn't supported yet - | throwThe RequestError ⟨.invalidParams, s!"exactly one orphaned goal is expected for have with goalsAfter {toJson goalsAfter}, but found {toJson goals.toList}"⟩ - return {steps := [.haveDecl tacticApp initialGoal.type steps], + return {steps := [.haveDecl tacticApp goals.toList steps], allGoals := HashSet.empty.insertMany (goalsBefore ++ goalsAfter)} | `(tactic| rw [$_,*] $(_)?) | `(tactic| rewrite [$_,*] $(_)?) => From 8d0a3b173dc3e50b041aa03c82dca927ce76faaf Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 14:41:34 +0100 Subject: [PATCH 02/10] Grab all have pattern (presumably) --- Examples.lean | 2 +- lean/BetterParser.lean | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/Examples.lean b/Examples.lean index 2500db9..4e36774 100644 --- a/Examples.lean +++ b/Examples.lean @@ -12,7 +12,7 @@ import Lean import Paperproof example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by - have h3 : m + 3 ≤ 9 := calc + have h3 := by calc m + 3 ≤ 2 * n - 1 := by gcongr _ ≤ 2 * 5 - 1 := by gcongr _ = 9 := by norm_num diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index fe3f073..f6c7ebc 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -134,9 +134,7 @@ partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : R -- It's a tactic combinator match tInfo.stx with - -- TODO: can we grab all have's as one pattern match branch? - | `(tactic| have $_:letPatDecl) - | `(tactic| have $_ : $_ := $_) => + | `(tactic| have $_:haveDecl) => -- Something like `have p : a = a := rfl` if steps.isEmpty then return {steps := [.tacticApp tacticApp], From 58c39a03271443024c371cf8cb8992bb4010b815 Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 14:54:49 +0100 Subject: [PATCH 03/10] Fix infering have type with no explicit type annotation --- lean/BetterParser.lean | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index f6c7ebc..6d63053 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -57,7 +57,7 @@ partial def findFVars (ctx: ContextInfo) (infoTree : InfoTree): List FVarId := | _ => none -- Returns GoalInfo about unassigned goals from the provided list of goals -def getGoals (ctx : ContextInfo) (goals : List MVarId) (mctx : MetavarContext) : RequestM (List GoalInfo) := do +def getGoals (printCtx: ContextInfo) (goals : List MVarId) (mctx : MetavarContext) : RequestM (List GoalInfo) := do goals.filterMapM fun id => do let some decl := mctx.findDecl? id | return none @@ -66,7 +66,7 @@ def getGoals (ctx : ContextInfo) (goals : List MVarId) (mctx : MetavarContext) : return none -- to get tombstones in name ✝ for unreachable hypothesis let lctx := decl.lctx |>.sanitizeNames.run' {options := {}} - let ppContext := {ctx with mctx}.toPPContext lctx + let ppContext := printCtx.toPPContext lctx let hyps ← lctx.foldlM (init := []) (fun acc decl => do if decl.isAuxDecl || decl.isImplementationDetail then return acc @@ -88,8 +88,15 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : RequestM (List Goa -- We want to filter out `focus` like tactics which don't do any assignments -- therefore we check all goals on whether they were assigned during the tactic let goalMVars := tInfo.goalsBefore ++ tInfo.goalsAfter - let goalsBefore ← getGoals ctx goalMVars tInfo.mctxBefore - let goalsAfter ← getGoals ctx goalMVars tInfo.mctxAfter + -- For printing purposes we always need to use the latest mctx assignments. For example in + -- have h := by calc + -- 3 ≤ 4 := by trivial + -- 4 ≤ 5 := by trivial + -- at mctxBefore type of `h` is `?m.260`, but by the time calc is elaborated at mctxAfter + -- it's known to be `3 ≤ 5` + let printCtx := {ctx with mctx := tInfo.mctxAfter} + let goalsBefore ← getGoals printCtx goalMVars tInfo.mctxBefore + let goalsAfter ← getGoals printCtx goalMVars tInfo.mctxAfter let commonGoals := goalsBefore.filter fun g => goalsAfter.contains g return ⟨ goalsBefore.filter (!commonGoals.contains ·), goalsAfter.filter (!commonGoals.contains ·) ⟩ From c05f3ae98ab5bbdbb1891518fdb18b8bd492005b Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 14:58:56 +0100 Subject: [PATCH 04/10] Adopt example for multi-declare have before fixing initial goals --- Examples.lean | 3 ++- lean/BetterParser.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Examples.lean b/Examples.lean index 4e36774..5edb260 100644 --- a/Examples.lean +++ b/Examples.lean @@ -12,7 +12,8 @@ import Lean import Paperproof example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by - have h3 := by calc + have ⟨ p, q ⟩ : (3 = 3) ∧ (4 = 4) := ⟨ by rfl, by rfl ⟩ + have h3 := calc m + 3 ≤ 2 * n - 1 := by gcongr _ ≤ 2 * 5 - 1 := by gcongr _ = 9 := by norm_num diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index 6d63053..5753a34 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -148,7 +148,7 @@ partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : R allGoals} let goals := (goalsBefore ++ goalsAfter).foldl HashSet.erase (noInEdgeGoals allGoals steps) - -- TODO: have ⟨ p, q ⟩ : (a = a) × (b = b) := ⟨ by rfl, by rfl ⟩ isn't supported yet + -- TODO: have ⟨ p, q ⟩ : (3 = 3) ∧ (4 = 4) := ⟨ by rfl, by rfl ⟩ isn't supported yet return {steps := [.haveDecl tacticApp goals.toList steps], allGoals := HashSet.empty.insertMany (goalsBefore ++ goalsAfter)} | `(tactic| rw [$_,*] $(_)?) From 9046cc18c3aa001be2914350264030ec87379fba Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 16:00:56 +0100 Subject: [PATCH 05/10] Support multiple byWindows (aka haveWindows) in tactics --- .../services/CreateElement/createArrows.ts | 30 +++- .../CreateElement/createWindowInsides.ts | 5 +- .../services/updateUI/services/converter.ts | 158 +++++++++++------- app/types/ConvertedProofTree.ts | 6 +- app/types/LeanProofTree.ts | 9 +- 5 files changed, 131 insertions(+), 77 deletions(-) diff --git a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createArrows.ts b/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createArrows.ts index 4a4917d..1b57381 100644 --- a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createArrows.ts +++ b/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createArrows.ts @@ -75,13 +75,29 @@ const createArrows = (shared: UIShared): UIElement => { }); // 3. Draw arrows between this tactic and `have` windows - if (tactic.haveWindowId && tactic.hypArrows[0]) { - const window = getWindowByHypId(shared.proofTree, tactic.hypArrows[0].toIds[0]); - if (!window) return - const fromWindowId = findIdInApp(shared.editor, CreateId.window(tactic.haveWindowId)); - const toTacticId = findIdInApp(shared.editor, CreateId.hypTactic(tactic.id, null, window.id)); - if (!fromWindowId || !toTacticId) return - DrawShape.arrow(shared.editor, fromWindowId, toTacticId, "goalArrow"); + for (const haveWindowId of tactic.haveWindowIds) { + if (tactic.hypArrows[0]) { + const window = getWindowByHypId( + shared.proofTree, + tactic.hypArrows[0].toIds[0] + ); + if (!window) return; + const fromWindowId = findIdInApp( + shared.editor, + CreateId.window(haveWindowId) + ); + const toTacticId = findIdInApp( + shared.editor, + CreateId.hypTactic(tactic.id, null, window.id) + ); + if (!fromWindowId || !toTacticId) return; + DrawShape.arrow( + shared.editor, + fromWindowId, + toTacticId, + "goalArrow" + ); + } } }); } diff --git a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts b/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts index 11dc445..f2cec63 100644 --- a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts +++ b/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts @@ -129,8 +129,9 @@ const createWindowInsides = (shared: UIShared, parentId: TLParentId | undefined, ); const haveWindows = shared.proofTree.windows - .filter(w => tactic.haveWindowId === w.id) - .map(w => createWindow(shared, parentId, w, depth + 1)); + .filter((w) => tactic.haveWindowIds.includes(w.id)) + .map((w) => createWindow(shared, parentId, w, depth + 1)); + console.log("HAVE WINDOWS", tactic.haveWindowIds, haveWindows); const hTree: UIHypTree = { tactic: vStack(0, [hStack(shared.inBetweenMargin, haveWindows), tacticNode]), level, diff --git a/app/src/services/updateUI/services/converter.ts b/app/src/services/updateUI/services/converter.ts index a934511..4229e03 100644 --- a/app/src/services/updateUI/services/converter.ts +++ b/app/src/services/updateUI/services/converter.ts @@ -216,7 +216,11 @@ const addToEquivalentIds = (pretty : ConvertedProofTree, beforeId : string, afte } } -const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWindowId : string | null = null) => { +const handleTacticApp = ( + tactic: LeanTactic, + pretty: ConvertedProofTree, + haveWindowIds: string[] = [] +) => { // We assume `tactic.goalsBefore[0]` is always the goal the tactic worked on! // Is it fair to assume? So far seems good. const mainGoalBefore = tactic.goalsBefore[0]; @@ -245,19 +249,20 @@ const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWi const nextGoal = tactic.goalsAfter[0]; pretty.tactics.push({ - id : newTacticId(), - text : tactic.tacticString, - dependsOnIds : tactic.tacticDependsOn, - goalArrows : [], - hypArrows : [], + id: newTacticId(), + text: tactic.tacticString, + dependsOnIds: tactic.tacticDependsOn, + goalArrows: [], + hypArrows: [], // success arrows are better not drawn (noisy!), we should just mark the tactic as 🎉. // .dependsOnIds will convey all the information we want to see. - isSuccess : nextGoal ? '🎉' : 'For all goals, 🎉!', + isSuccess: nextGoal ? "🎉" : "For all goals, 🎉!", successGoalId: mainGoalBefore.id, + haveWindowIds, }); } // - we updated the goal! - else if (relevantGoalsAfter.length === 1) { + else if (relevantGoalsAfter.length === 1) { const updatedGoal = relevantGoalsAfter[0]; // 1. Draw goal nodes and arrows @@ -273,31 +278,37 @@ const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWi currentWindow.goalNodes.push({ text: updatedGoal.type, name: updatedGoal.username, - id : updatedGoal.id + id: updatedGoal.id, }); - prettyGoalArrows = [{ - fromId: mainGoalBefore.id, - toId: updatedGoal.id - }]; + prettyGoalArrows = [ + { + fromId: mainGoalBefore.id, + toId: updatedGoal.id, + }, + ]; } // 2. Draw hypothesis nodes and arrows const hypsBefore = mainGoalBefore.hyps; - const hypsAfter = updatedGoal.hyps; - let [prettyHypNodes, prettyHypArrows] = drawNewHypothesisLayer(pretty, hypsBefore, hypsAfter); + const hypsAfter = updatedGoal.hyps; + let [prettyHypNodes, prettyHypArrows] = drawNewHypothesisLayer( + pretty, + hypsBefore, + hypsAfter + ); if (prettyHypNodes.length > 0) { currentWindow.hypNodes.push(prettyHypNodes); } pretty.tactics.push({ - id : newTacticId(), - text : tactic.tacticString, - dependsOnIds : tactic.tacticDependsOn, - goalArrows : prettyGoalArrows, - hypArrows : prettyHypArrows, - isSuccess : false, - ...(haveWindowId && { haveWindowId }) + id: newTacticId(), + text: tactic.tacticString, + dependsOnIds: tactic.tacticDependsOn, + goalArrows: prettyGoalArrows, + hypArrows: prettyHypArrows, + isSuccess: false, + haveWindowIds, }); } // - we forked the goal! @@ -305,15 +316,19 @@ const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWi // 1. Draw goal nodes and arrows const prettyGoalArrows = relevantGoalsAfter.map((goal) => ({ fromId: mainGoalBefore.id, - toId: goal.id + toId: goal.id, })); const prettyHypArrows: Tactic["hypArrows"] = []; // We are creating new child windows const childWindows = relevantGoalsAfter.map((goal) => { const hypsBefore = mainGoalBefore.hyps; - const hypsAfter = goal.hyps; - const [prettyHypNodes, prettyHypArrowsForAChild] = drawNewHypothesisLayer(pretty, hypsBefore, hypsAfter); + const hypsAfter = goal.hyps; + const [prettyHypNodes, prettyHypArrowsForAChild] = drawNewHypothesisLayer( + pretty, + hypsBefore, + hypsAfter + ); prettyHypArrows.push(...prettyHypArrowsForAChild); return { @@ -323,30 +338,34 @@ const handleTacticApp = (tactic: LeanTactic, pretty : ConvertedProofTree, haveWi { text: goal.type, name: goal.username, - id: goal.id - } + id: goal.id, + }, ], - hypNodes: prettyHypNodes.length > 0 ? [prettyHypNodes] : [] - } + hypNodes: prettyHypNodes.length > 0 ? [prettyHypNodes] : [], + }; }); pretty.windows.push(...childWindows); pretty.tactics.push({ - id : newTacticId(), - text : tactic.tacticString, - dependsOnIds : tactic.tacticDependsOn, - goalArrows : prettyGoalArrows, - hypArrows : prettyHypArrows, - isSuccess : false + id: newTacticId(), + text: tactic.tacticString, + dependsOnIds: tactic.tacticDependsOn, + goalArrows: prettyGoalArrows, + hypArrows: prettyHypArrows, + isSuccess: false, + haveWindowIds, }); } -} +}; -const drawInitialGoal = (initialMainGoal: LeanGoal, pretty : ConvertedProofTree) => { +const drawInitialGoal = ( + initialMainGoal: LeanGoal, + pretty: ConvertedProofTree +) => { const hypNodes = initialMainGoal.hyps.map((hyp: LeanHypothesis) => ({ text: hyp.type, name: hyp.username, - id : hyp.id + id: hyp.id, })); const initialWindow = { id: newWindowId(), @@ -355,55 +374,64 @@ const drawInitialGoal = (initialMainGoal: LeanGoal, pretty : ConvertedProofTree) { text: initialMainGoal.type, name: initialMainGoal.username, - id : initialMainGoal.id - } + id: initialMainGoal.id, + }, ], - hypNodes: hypNodes.length > 0 ? [hypNodes.reverse()] : [] + hypNodes: hypNodes.length > 0 ? [hypNodes.reverse()] : [], }; pretty.windows.push(initialWindow); -} +}; +// TODO: Refactor it since this function relies on obsolete assumptions: +// - There is only one initial goal (can be multiple `have := `) +// - Order of tactics in steps reflects the order of the proof. const getInitialGoal = (subSteps: LeanProofTree): LeanGoal | undefined => { const firstStep = subSteps[0]; - if ('tacticApp' in firstStep) { + if ("tacticApp" in firstStep) { return firstStep.tacticApp.t.goalsBefore[0]; - } else if ('haveDecl' in firstStep) { + } else if ("haveDecl" in firstStep) { return firstStep.haveDecl.t.goalsBefore[0]; } -} +}; -const recursive = (subSteps : LeanProofTree, pretty : ConvertedProofTree) => { +const recursive = (subSteps: LeanProofTree, pretty: ConvertedProofTree) => { subSteps.forEach((subStep) => { - if ('tacticApp' in subStep) { + if ("tacticApp" in subStep) { handleTacticApp(subStep.tacticApp.t, pretty); - } else if ('haveDecl' in subStep) { - const haveWindowId = newWindowId(); - - handleTacticApp(subStep.haveDecl.t, pretty, haveWindowId); - - const initialGoal = getInitialGoal(subStep.haveDecl.subSteps)!; - - const initialWindow : Window = { - id: haveWindowId, + } else if ("haveDecl" in subStep) { + // TODO: Remove when new lean version reporting is set up. + const initialGoals = + "initialGoals" in subStep.haveDecl + ? subStep.haveDecl.initialGoals + : [getInitialGoal(subStep.haveDecl.subSteps)!]; + console.log("Inital", initialGoals); + const windows = initialGoals.map((goal) => ({ + id: newWindowId(), // Parent window is such that has our goalId as a hypothesis. // `have`'s fvarid won't equal `have's` mvarid however - so the only way to match them would be by the username. many `have`s may have the same username though, so let's just store out parentId. parentId: "haveWindow", goalNodes: [ { - text: initialGoal.type, - name: initialGoal.username, - id : initialGoal.id - } + text: goal.type, + name: goal.username, + id: goal.id, + }, ], // `have`s don't introduce any new hypotheses - hypNodes: [] - }; - pretty.windows.push(initialWindow); + hypNodes: [], + })); + + handleTacticApp( + subStep.haveDecl.t, + pretty, + windows.map((w) => w.id) + ); + pretty.windows.push(...windows); recursive(subStep.haveDecl.subSteps, pretty); } - }) -} + }); +}; const postprocess = (pretty: ConvertedProofTree): ConvertedProofTree => { pretty.tactics.forEach((tactic) => { diff --git a/app/types/ConvertedProofTree.ts b/app/types/ConvertedProofTree.ts index d50a8ff..ea7545a 100644 --- a/app/types/ConvertedProofTree.ts +++ b/app/types/ConvertedProofTree.ts @@ -31,7 +31,11 @@ export interface Tactic { // hmm isSuccess: boolean | string; successGoalId?: string; - haveWindowId?: string + // TODO: Those are actually `byWindow`s which were used to create + // parameters for this tactic. For example in + // `have := ` + // there are 2 `byWindow`s. + haveWindowIds: string[]; } export interface ConvertedProofTree { diff --git a/app/types/LeanProofTree.ts b/app/types/LeanProofTree.ts index cc1669e..1fe1d37 100644 --- a/app/types/LeanProofTree.ts +++ b/app/types/LeanProofTree.ts @@ -29,8 +29,13 @@ export type LeanHaveDecl = { haveDecl: { t: LeanTactic; subSteps: LeanProofTree; - initialGoal: string; - } + } & ( + | { version: undefined; initialGoal: string } + | { + version: 2; + initialGoals: LeanGoal[]; + } + ); }; export type LeanProofTree = (LeanTacticApp | LeanHaveDecl)[]; From 86e98b71a0b7fa7082a19c79708698f0a14cf8bc Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 16:09:14 +0100 Subject: [PATCH 06/10] Sort initial goals in parser --- .../services/CreateElement/createWindowInsides.ts | 7 ++++--- app/src/services/updateUI/services/converter.ts | 1 - lean/BetterParser.lean | 4 +++- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts b/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts index f2cec63..17aa741 100644 --- a/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts +++ b/app/src/services/updateUI/services/buildProofTree/services/CreateElement/createWindowInsides.ts @@ -128,10 +128,11 @@ const createWindowInsides = (shared: UIShared, parentId: TLParentId | undefined, CreateId.hypTactic(tactic.id, hypArrow.fromId, window.id) ); - const haveWindows = shared.proofTree.windows - .filter((w) => tactic.haveWindowIds.includes(w.id)) + const haveWindows = tactic.haveWindowIds + .flatMap( + (id) => shared.proofTree.windows.find((w) => w.id === id) ?? [] + ) .map((w) => createWindow(shared, parentId, w, depth + 1)); - console.log("HAVE WINDOWS", tactic.haveWindowIds, haveWindows); const hTree: UIHypTree = { tactic: vStack(0, [hStack(shared.inBetweenMargin, haveWindows), tacticNode]), level, diff --git a/app/src/services/updateUI/services/converter.ts b/app/src/services/updateUI/services/converter.ts index 4229e03..9054f79 100644 --- a/app/src/services/updateUI/services/converter.ts +++ b/app/src/services/updateUI/services/converter.ts @@ -404,7 +404,6 @@ const recursive = (subSteps: LeanProofTree, pretty: ConvertedProofTree) => { "initialGoals" in subStep.haveDecl ? subStep.haveDecl.initialGoals : [getInitialGoal(subStep.haveDecl.subSteps)!]; - console.log("Inital", initialGoals); const windows = initialGoals.map((goal) => ({ id: newWindowId(), // Parent window is such that has our goalId as a hypothesis. diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index 5753a34..cc22952 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -148,8 +148,10 @@ partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : R allGoals} let goals := (goalsBefore ++ goalsAfter).foldl HashSet.erase (noInEdgeGoals allGoals steps) + -- Important for have := calc for example, e.g. calc 3 < 4 ... 4 < 5 ... + let sortedGoals := goals.toArray.insertionSort (·.id < ·.id) -- TODO: have ⟨ p, q ⟩ : (3 = 3) ∧ (4 = 4) := ⟨ by rfl, by rfl ⟩ isn't supported yet - return {steps := [.haveDecl tacticApp goals.toList steps], + return {steps := [.haveDecl tacticApp sortedGoals.toList steps], allGoals := HashSet.empty.insertMany (goalsBefore ++ goalsAfter)} | `(tactic| rw [$_,*] $(_)?) | `(tactic| rewrite [$_,*] $(_)?) => From 91397b61cc8d6a176e949c0508b187a7adb79d21 Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 16:22:11 +0100 Subject: [PATCH 07/10] Add simple example to improve depends on --- Examples.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Examples.lean b/Examples.lean index 5edb260..4d3210b 100644 --- a/Examples.lean +++ b/Examples.lean @@ -11,8 +11,13 @@ import Mathlib.Algebra.GCDMonoid.Multiset import Lean import Paperproof +theorem simple_ex (n m : ℕ) + (h1 : ∀ {a b : Nat}, a + b = b + a) + (h2 : ∀ {a b : Nat}, a = b + b): + n + m = m + n := by + simp [h1, h2] + example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by - have ⟨ p, q ⟩ : (3 = 3) ∧ (4 = 4) := ⟨ by rfl, by rfl ⟩ have h3 := calc m + 3 ≤ 2 * n - 1 := by gcongr _ ≤ 2 * 5 - 1 := by gcongr From 23c1ba7f3cc550711f5f7b7e270246cd22b8be6d Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 17:07:34 +0100 Subject: [PATCH 08/10] Use what was assigned to metavariable instead of parsing syntax WIP --- lean/BetterParser.lean | 37 +++++++++++++++++++++++-------------- 1 file changed, 23 insertions(+), 14 deletions(-) diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index cc22952..90fa51b 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -50,11 +50,22 @@ def noInEdgeGoals (allGoals : HashSet GoalInfo) (steps : List ProofStep) : HashS -- Some of the orphaned goals might be matched by tactics in sibling subtrees, e.g. for tacticSeq. (steps.bind stepGoalsAfter).foldl HashSet.erase allGoals -partial def findFVars (ctx: ContextInfo) (infoTree : InfoTree): List FVarId := - (InfoTree.context ctx infoTree).deepestNodes fun _ i _ => - match i with - | .ofTermInfo ti => if let .fvar id := ti.expr then some id else none - | _ => none +/- + Instead of doing parsing of what user wrote (it wouldn't work for linarith etc), + let's do the following. + We have assigned something to our goal in mctxAfter. + All the fvars used in these assignments are what was actually used instead of what was in syntax. +-/ +def findHypsUsedByTactic (goalId: MVarId) (goalDecl : MetavarDecl) (mctxAfter : MetavarContext) : MetaM (List String) := do + let some expr := mctxAfter.eAssignment.find? goalId + | return [] + + let fvarIds := (collectFVars {} expr).fvarIds + let fvars := fvarIds.filterMap goalDecl.lctx.find? + let proofFvars ← fvars.filterM (Meta.isProof ·.toExpr) + let pretty := proofFvars.map (fun x => x.userName) + dbg_trace s!"Used {pretty}" + return proofFvars.map (fun x => x.fvarId.name.toString) |>.toList -- Returns GoalInfo about unassigned goals from the provided list of goals def getGoals (printCtx: ContextInfo) (goals : List MVarId) (mctx : MetavarContext) : RequestM (List GoalInfo) := do @@ -122,21 +133,19 @@ partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : R -- For example a tactic like `done` which ensures there are no unsolved goals, -- or `focus` which only leaves one goal, however has no information for the tactic tree -- Note: tactic like `have` changes the goal as it adds something to the context - if goalsBefore.isEmpty then - return {steps, allGoals} - - let some mainGoalDecl := tInfo.goalsBefore.head?.bind tInfo.mctxBefore.findDecl? + let some mainGoalId := tInfo.goalsBefore.head? + | return {steps, allGoals} + let some mainGoalDecl := tInfo.mctxBefore.findDecl? mainGoalId | return {steps, allGoals} - -- Find names to get decls - let fvarIds := cs.toList.map (findFVars ctx) |>.join - let fvars := fvarIds.filterMap mainGoalDecl.lctx.find? - let proofFvars ← fvars.filterM (λ decl => ctx.runMetaM mainGoalDecl.lctx (Meta.isProof decl.toExpr)) + let tacticDependsOn ← + ctx.runMetaM mainGoalDecl.lctx + (findHypsUsedByTactic mainGoalId mainGoalDecl tInfo.mctxAfter) let tacticApp: TacticApplication := { tacticString, goalsBefore, goalsAfter, - tacticDependsOn := proofFvars.map fun decl => s!"{decl.fvarId.name.toString}" + tacticDependsOn } -- It's a tactic combinator From ee10acb64dea78a68932c4f32c951e2ac69710d0 Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 17:59:39 +0100 Subject: [PATCH 09/10] Instantiate mvars before querying fvars --- lean/BetterParser.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index 90fa51b..fc2477f 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -60,11 +60,13 @@ def findHypsUsedByTactic (goalId: MVarId) (goalDecl : MetavarDecl) (mctxAfter : let some expr := mctxAfter.eAssignment.find? goalId | return [] - let fvarIds := (collectFVars {} expr).fvarIds + -- Need to instantiate it to get all fvars + let fullExpr ← instantiateExprMVars expr |>.run + let fvarIds := (collectFVars {} fullExpr).fvarIds let fvars := fvarIds.filterMap goalDecl.lctx.find? let proofFvars ← fvars.filterM (Meta.isProof ·.toExpr) - let pretty := proofFvars.map (fun x => x.userName) - dbg_trace s!"Used {pretty}" + -- let pretty := proofFvars.map (fun x => x.userName) + -- dbg_trace s!"Used {pretty}" return proofFvars.map (fun x => x.fvarId.name.toString) |>.toList -- Returns GoalInfo about unassigned goals from the provided list of goals From c44e22f613354f48dba4cbd6ce8bb3fd9ed0427c Mon Sep 17 00:00:00 2001 From: Anton Kovsharov Date: Fri, 27 Oct 2023 18:21:14 +0100 Subject: [PATCH 10/10] Return check for empty goals since it breaks some proofs otherwise --- lean/BetterParser.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lean/BetterParser.lean b/lean/BetterParser.lean index fc2477f..4eb4f08 100644 --- a/lean/BetterParser.lean +++ b/lean/BetterParser.lean @@ -135,6 +135,9 @@ partial def BetterParser (context: Option ContextInfo) (infoTree : InfoTree) : R -- For example a tactic like `done` which ensures there are no unsolved goals, -- or `focus` which only leaves one goal, however has no information for the tactic tree -- Note: tactic like `have` changes the goal as it adds something to the context + if goalsBefore.isEmpty then + return {steps, allGoals} + let some mainGoalId := tInfo.goalsBefore.head? | return {steps, allGoals} let some mainGoalDecl := tInfo.mctxBefore.findDecl? mainGoalId