diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 419f6b8ed0..d20eebfab0 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -302,7 +302,11 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat] | no_idea => unreachable! -/-- Given an expression `e`, produce `sizeOf e` with a suitable instance. -/ +/-- +Given an expression `e`, produce `sizeOf e` with a suitable instance. +NB: We must use the instance of the type of the function parameter! +The concrete argument at hand may have a different (still def-eq) typ. +-/ def mkSizeOf (e : Expr) : MetaM Expr := do let ty ← inferType e let lvl ← getLevel ty @@ -315,8 +319,8 @@ def mkSizeOf (e : Expr) : MetaM Expr := do For a given recursive call, and a choice of parameter and argument index, try to prove equality, < or ≤. -/ -def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) : - MetaM GuessLexRel := do +def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) + (paramIdx argIdx : Nat) : MetaM GuessLexRel := do rcc.ctxt.run do let param := rcc.params[paramIdx]! let arg := rcc.args[argIdx]! @@ -407,7 +411,7 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel return .eq /-- -Given a predefinition with value `fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ...`, +Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`, where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal. This is the case for types such as `Prop`, `Type u`, etc. These arguments should not be considered when guessing a well-founded relation. @@ -425,6 +429,47 @@ def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) result := result.push i return result +/-- +Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`, +where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff the +`WellFoundedRelation` of `aᵢ` goes via `SizeOf`, and `aᵢ` does not depend on `y₁`…. + +These are the parameters for which we omit an explicit call to `sizeOf` in the termination argument. + +We only use this in the non-mutual case; in the mutual case we would have to additional check +if the parameters that line up in the actual `TerminationWF` have the same type. +-/ +def getSizeOfParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) := + lambdaTelescope preDef.value fun xs _ => do + let xs : Array Expr := xs[fixedPrefixSize:] + let mut result := #[] + for x in xs, i in [:xs.size] do + try + let t ← inferType x + if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then continue + let u ← getLevel t + let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t) + let soi ← synthInstance (.app (.const ``SizeOf [u]) t) + if ← isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi) then + result := result.push i + catch _ => + pure () + return result + +/-- +Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`, +where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `aᵢ` is `Nat`. +These are parameters where we can definitely omit the call to `sizeOf`. +-/ +def getNatParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) := + lambdaTelescope preDef.value fun xs _ => do + let xs : Array Expr := xs[fixedPrefixSize:] + let mut result := #[] + for x in xs, i in [:xs.size] do + let t ← inferType x + if ← withReducible (isDefEq t (.const `Nat [])) then + result := result.push i + return result /-- Generate all combination of arguments, skipping those that are forbidden. @@ -539,23 +584,26 @@ combination of these measures. The parameters are * `measures`: The measures to be used. -/ def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name)) - (measures : Array MutualMeasure) : MetaM TerminationWF := do + (needsNoSizeOf : Array (Array Nat)) (measures : Array MutualMeasure) : MetaM TerminationWF := do varNamess.mapIdxM fun funIdx varNames => do let idents := varNames.map mkIdent let measureStxs ← measures.mapM fun | .args varIdxs => do let varIdx := varIdxs[funIdx]! let v := idents[varIdx]! - -- Print `sizeOf` as such, unless it is shadowed. - -- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`. - -- But it could also be shadowed by an earlier parameter (including the fixed prefix), - -- so look for unqualified (single tick) occurrences in `originalVarNames` - let sizeOfIdent := - if originalVarNamess[funIdx]!.any (· = `sizeOf) then - mkIdent ``sizeOf -- fully qualified - else - mkIdent (← unresolveNameGlobal ``sizeOf) - `($sizeOfIdent $v) + if needsNoSizeOf[funIdx]!.contains varIdx then + `($v) + else + -- Print `sizeOf` as such, unless it is shadowed. + -- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`. + -- But it could also be shadowed by an earlier parameter (including the fixed prefix), + -- so look for unqualified (single tick) occurrences in `originalVarNames` + let sizeOfIdent := + if originalVarNamess[funIdx]!.any (· = `sizeOf) then + mkIdent ``sizeOf -- fully qualified + else + mkIdent (← unresolveNameGlobal ``sizeOf) + `($sizeOfIdent $v) | .func funIdx' => if funIdx' == funIdx then `(1) else `(0) let body ← mkTupleSyntax measureStxs return { ref := .missing, vars := idents, body, synthetic := true } @@ -668,11 +716,20 @@ def explainFailure (declNames : Array Name) (varNamess : Array (Array Name)) r := r ++ (← explainMutualFailure declNames varNamess rcs) return r -end Lean.Elab.WF.GuessLex +/-- +Shows the termination measure used to the user, and implements `termination_by?` +-/ +def reportWF (preDefs : Array PreDefinition) (wf : TerminationWF) : MetaM Unit := do + let extraParamss := preDefs.map (·.termination.extraParams) + let wf' := trimTermWF extraParamss wf + for preDef in preDefs, term in wf' do + if showInferredTerminationBy.get (← getOptions) then + logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}" + if let some ref := preDef.termination.terminationBy?? then + Tactic.TryThis.addSuggestion ref (← term.unexpand) -namespace Lean.Elab.WF - -open Lean.Elab.WF.GuessLex +end GuessLex +open GuessLex /-- Main entry point of this module: @@ -683,14 +740,17 @@ terminates. See the module doc string for a high-level overview. def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) : MetaM TerminationWF := do - let extraParamss := preDefs.map (·.termination.extraParams) let originalVarNamess ← preDefs.mapM originalVarNames let varNamess ← originalVarNamess.mapM (naryVarNames fixedPrefixSize ·) let arities := varNamess.map (·.size) trace[Elab.definition.wf] "varNames is: {varNamess}" - let forbiddenArgs ← preDefs.mapM fun preDef => - getForbiddenByTrivialSizeOf fixedPrefixSize preDef + let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize) + let needsNoSizeOf ← + if preDefs.size = 1 then + preDefs.mapM (getSizeOfParams fixedPrefixSize) + else + preDefs.mapM (getNatParams fixedPrefixSize) -- The list of measures, including the measures that order functions. -- The function ordering measures come last @@ -698,7 +758,9 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) -- If there is only one plausible measure, use that if let #[solution] := measures then - return ← buildTermWF originalVarNamess varNamess #[solution] + let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf #[solution] + reportWF preDefs wf + return wf -- Collect all recursive calls and extract their context let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities @@ -708,15 +770,8 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) match ← liftMetaM <| solve measures callMatrix with | .some solution => do - let wf ← buildTermWF originalVarNamess varNamess solution - - let wf' := trimTermWF extraParamss wf - for preDef in preDefs, term in wf' do - if showInferredTerminationBy.get (← getOptions) then - logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}" - if let some ref := preDef.termination.terminationBy?? then - Tactic.TryThis.addSuggestion ref (← term.unexpand) - + let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf solution + reportWF preDefs wf return wf | .none => let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs diff --git a/tests/lean/guessLex.lean b/tests/lean/guessLex.lean index 9fabe2b711..c836ab72d7 100644 --- a/tests/lean/guessLex.lean +++ b/tests/lean/guessLex.lean @@ -87,6 +87,7 @@ def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat | ⟨0,_⟩ => 0 | ⟨.succ y,.succ n⟩ => confuseLex2 ⟨y,n⟩ +-- NB: uses sizeOf to make the termination argument non-dependent def dependent : (n : Nat) → (m : Fin n) → Nat | 0, i => Fin.elim0 i | .succ 0, 0 => 0 @@ -94,6 +95,11 @@ def dependent : (n : Nat) → (m : Fin n) → Nat | .succ (.succ n), ⟨.succ m, h⟩ => dependent (.succ (.succ n)) ⟨m, Nat.lt_of_le_of_lt (Nat.le_succ _) h⟩ +-- NB: does not use sizeOf, as parameters in the fixed prefix are fine. +def dependentWithFixedPrefix (n : Nat) : (m : Fin n) → (acc : Nat) → Nat + | ⟨0, _⟩, acc => acc + | ⟨i+1, h⟩, acc => dependentWithFixedPrefix n ⟨i, Nat.lt_of_succ_lt h⟩ (acc + i) + -- An example based on a real world problem, condensed by Leo inductive Expr where | add (a b : Expr) @@ -110,6 +116,7 @@ def eval_add (a : Expr × Expr) : Nat := | (x, y) => eval x + eval y end + namespace VarNames /-! Test that varnames are inferred nicely. -/ @@ -127,24 +134,97 @@ def shadow2 (some_n : Nat) : Nat → Nat | .succ n => shadow2 (some_n + 1) n decreasing_by decreasing_tactic + +-- The following test whether `sizeOf` is properly printed, and possibly qualified +-- For this we need a type that needs an explicit “sizeOf”. + +structure OddNat where nat : Nat +instance : WellFoundedRelation OddNat := measure (fun ⟨n⟩ => n+1) + +-- Just to check that sizeOf is actually used +def oddNat : OddNat → Nat + | ⟨0⟩ => 0 + | ⟨.succ n⟩ => oddNat ⟨n⟩ +decreasing_by decreasing_tactic + -- Shadowing `sizeOf`, as a varying paramter -def shadowSizeOf1 (sizeOf : Nat) : Nat → Nat - | 0 => 0 - | .succ n => shadowSizeOf1 (sizeOf + 1) n +def shadowSizeOf1 (sizeOf : Nat) : OddNat → Nat + | ⟨0⟩ => 0 + | ⟨.succ n⟩ => shadowSizeOf1 (sizeOf + 1) ⟨n⟩ decreasing_by decreasing_tactic -- Shadowing `sizeOf`, as a fixed paramter -def shadowSizeOf2 (sizeOf : Nat) : Nat → Nat → Nat - | 0, m => m - | .succ n, m => shadowSizeOf2 sizeOf n m +def shadowSizeOf2 (sizeOf : Nat) : OddNat → Nat → Nat + | ⟨0⟩, m => m + | ⟨.succ n⟩, m => shadowSizeOf2 sizeOf ⟨n⟩ m decreasing_by decreasing_tactic -- Shadowing `sizeOf`, as something in the environment def sizeOf : Nat := 2 -def qualifiedSizeOf (m : Nat) : Nat → Nat - | 0 => 0 - | .succ n => qualifiedSizeOf (m + 1) n +def qualifiedSizeOf (m : Nat) : OddNat → Nat + | ⟨0⟩ => 0 + | ⟨.succ n⟩ => qualifiedSizeOf (m + 1) ⟨n⟩ decreasing_by decreasing_tactic end VarNames + + +namespace MutualNotNat1 + +-- A type that isn't Nat, checking that the inferred argument uses `sizeOf` so that +-- the types of the termination argument aligns. +structure OddNat2 where nat : Nat +instance : SizeOf OddNat2 := ⟨fun n => n.nat⟩ +@[simp] theorem OddNat2.sizeOf_eq (n : OddNat2) : sizeOf n = n.nat := rfl +mutual +def foo : Nat → Nat + | 0 => 0 + | n+1 => bar ⟨n⟩ +def bar : OddNat2 → Nat + | ⟨0⟩ => 0 + | ⟨n+1⟩ => foo n +end +end MutualNotNat1 + +namespace MutualNotNat2 +-- A type that is defeq to Nat, but with a different `sizeOf`, checking that the +-- inferred argument uses `sizeOf` so that the types of the termination argument aligns. +def OddNat3 := Nat +instance : SizeOf OddNat3 := ⟨fun n => 42 - @id Nat n⟩ +@[simp] theorem OddNat3.sizeOf_eq (n : OddNat3) : sizeOf n = 42 - @id Nat n := rfl +mutual +def foo : Nat → Nat + | 0 => 0 + | n+1 => + if h : n < 42 then bar (42 - n) else 0 + -- termination_by x1 => x1 + decreasing_by simp_wf; simp [OddNat3]; omega +def bar (o : OddNat3) : Nat := if h : @id Nat o < 41 then foo (41 - @id Nat o) else 0 + -- termination_by sizeOf o + decreasing_by simp_wf; simp [id] at *; omega +end +namespace MutualNotNat2 + +namespace MutualNotNat3 +-- A varant of the above, but where the type of the parameter refined to `Nat`. +-- This tests if `GuessLex` is inferring the `SizeOf` instance based on the type of the +-- concrete parameter/argument (wrong, but status quo), or based on the types in the function +-- signature (correct, todo) +def OddNat3 := Nat +instance : SizeOf OddNat3 := ⟨fun n => 42 - @id Nat n⟩ +@[simp] theorem OddNat3.sizeOf_eq (n : OddNat3) : sizeOf n = 42 - @id Nat n := rfl +mutual +def foo : Nat → Nat + | 0 => 0 + | n+1 => + if h : n < 42 then bar (42 - n) else 0 + -- termination_by x1 => x1 + decreasing_by simp_wf; simp [OddNat3]; omega +def bar : OddNat3 → Nat + | Nat.zero => 0 + | n+1 => if h : n < 41 then foo (40 - n) else 0 + -- termination_by x1 => sizeOf x1 + decreasing_by simp_wf; omega +end +namespace MutualNotNat3 diff --git a/tests/lean/guessLex.lean.expected.out b/tests/lean/guessLex.lean.expected.out index 7101d313ae..737e10af6a 100644 --- a/tests/lean/guessLex.lean.expected.out +++ b/tests/lean/guessLex.lean.expected.out @@ -1,41 +1,65 @@ Inferred termination argument: -termination_by (sizeOf n, sizeOf m) +termination_by (n, m) Inferred termination argument: -termination_by (sizeOf m, sizeOf n) +termination_by (m, n) Inferred termination argument: -termination_by (sizeOf n, sizeOf m) +termination_by (n, m) Inferred termination argument: -termination_by x1 x2 => (sizeOf x2, sizeOf x1) +termination_by x1 x2 => (x2, x1) +Inferred termination argument: +termination_by x1 => x1 +Inferred termination argument: +termination_by x1 => x1 +Inferred termination argument: +termination_by x1 => x1 +Inferred termination argument: +termination_by x1 => x1 +Inferred termination argument: +termination_by x1 => (x1, 0) +Inferred termination argument: +termination_by (n, 1) +Inferred termination argument: +termination_by (m, n) +Inferred termination argument: +termination_by x1 x2 x3 x4 x5 x6 x7 x8 => (x8, x7, x6, x5, x4, x3, x2, x1) Inferred termination argument: termination_by x1 => sizeOf x1 Inferred termination argument: -termination_by x1 => sizeOf x1 +termination_by x1 x2 => (x1, sizeOf x2) Inferred termination argument: -termination_by x1 => sizeOf x1 -Inferred termination argument: -termination_by x1 => sizeOf x1 -Inferred termination argument: -termination_by x1 => (sizeOf x1, 0) -Inferred termination argument: -termination_by (sizeOf n, 1) -Inferred termination argument: -termination_by (sizeOf m, sizeOf n) -Inferred termination argument: -termination_by x1 x2 x3 x4 x5 x6 x7 x8 => - (sizeOf x8, sizeOf x7, sizeOf x6, sizeOf x5, sizeOf x4, sizeOf x3, sizeOf x2, sizeOf x1) -Inferred termination argument: -termination_by x1 x2 => (sizeOf x1, sizeOf x2) +termination_by x1 x2 => x1 Inferred termination argument: termination_by (sizeOf a, 1) Inferred termination argument: termination_by (sizeOf a, 0) Inferred termination argument: -termination_by x2' => sizeOf x2' +termination_by x2' => x2' Inferred termination argument: -termination_by x2 => sizeOf x2 +termination_by x2 => x2 +Inferred termination argument: +termination_by x1 => sizeOf x1 Inferred termination argument: termination_by x2 => SizeOf.sizeOf x2 Inferred termination argument: termination_by x1 x2 => SizeOf.sizeOf x1 Inferred termination argument: termination_by x2 => SizeOf.sizeOf x2 +Inferred termination argument: +termination_by x1 => x1 +Inferred termination argument: +termination_by x1 => sizeOf x1 +Inferred termination argument: +termination_by x1 => x1 +Inferred termination argument: +termination_by sizeOf o +guessLex.lean:217:0-229:3: error: Could not find a decreasing measure. +The arguments relate at each recursive call as follows: +(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) +Call from MutualNotNat2.MutualNotNat2.MutualNotNat3.foo to MutualNotNat2.MutualNotNat2.MutualNotNat3.bar at 221:23-35: + x1 +x1 < +Call from MutualNotNat2.MutualNotNat2.MutualNotNat3.bar to MutualNotNat2.MutualNotNat2.MutualNotNat3.foo at 226:30-42: + x1 +x1 ? + +Please use `termination_by` to specify a decreasing measure. diff --git a/tests/lean/guessLexTricky.lean.expected.out b/tests/lean/guessLexTricky.lean.expected.out index 6e98a304c0..816a3a696a 100644 --- a/tests/lean/guessLexTricky.lean.expected.out +++ b/tests/lean/guessLexTricky.lean.expected.out @@ -1,6 +1,6 @@ Inferred termination argument: -termination_by (sizeOf y, 1, 0) +termination_by (y, 1, 0) Inferred termination argument: -termination_by (sizeOf y, 0, 1) +termination_by (y, 0, 1) Inferred termination argument: -termination_by (sizeOf y, 0, 0) +termination_by (y, 0, 0) diff --git a/tests/lean/guessLexTricky2.lean.expected.out b/tests/lean/guessLexTricky2.lean.expected.out index 24db6dc1bf..d27a0e6ab4 100644 --- a/tests/lean/guessLexTricky2.lean.expected.out +++ b/tests/lean/guessLexTricky2.lean.expected.out @@ -1,4 +1,4 @@ Inferred termination argument: -termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 0) +termination_by x1 x2 x3 => (x1, x2, 0) Inferred termination argument: -termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 1) +termination_by x1 x2 x3 => (x1, x2, 1) diff --git a/tests/lean/interactive/terminationBySuggestion.lean b/tests/lean/interactive/terminationBySuggestion.lean index 928c0cc081..cb6480bcc0 100644 --- a/tests/lean/interactive/terminationBySuggestion.lean +++ b/tests/lean/interactive/terminationBySuggestion.lean @@ -1,7 +1,19 @@ - def ackermann (n m : Nat) := match n, m with | 0, m => m + 1 | .succ n, 0 => ackermann n 1 | .succ n, .succ m => ackermann n (ackermann (n + 1) m) termination_by? --^ codeAction + +-- Check hat we print this even if there is only one plausible measure +def onlyOneMeasure (n : Nat) := match n with + | 0 => 0 + | .succ n => onlyOneMeasure n +termination_by? + --^ codeAction + +def anonymousMeasure : Nat → Nat + | 0 => 0 + | .succ n => anonymousMeasure n +termination_by? + --^ codeAction diff --git a/tests/lean/interactive/terminationBySuggestion.lean.expected.out b/tests/lean/interactive/terminationBySuggestion.lean.expected.out index a1c73f09d8..b0624016ed 100644 --- a/tests/lean/interactive/terminationBySuggestion.lean.expected.out +++ b/tests/lean/interactive/terminationBySuggestion.lean.expected.out @@ -1,4 +1,4 @@ -{"title": "Try this: termination_by (sizeOf n, sizeOf m)", +{"title": "Try this: termination_by (n, m)", "kind": "quickfix", "isPreferred": true, "edit": @@ -7,6 +7,30 @@ {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, "edits": [{"range": - {"start": {"line": 5, "character": 0}, - "end": {"line": 5, "character": 15}}, - "newText": "termination_by (sizeOf n, sizeOf m)"}]}]}} + {"start": {"line": 4, "character": 0}, + "end": {"line": 4, "character": 15}}, + "newText": "termination_by (n, m)"}]}]}} +{"title": "Try this: termination_by n", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, + "edits": + [{"range": + {"start": {"line": 11, "character": 0}, + "end": {"line": 11, "character": 15}}, + "newText": "termination_by n"}]}]}} +{"title": "Try this: termination_by x1 => x1", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, + "edits": + [{"range": + {"start": {"line": 17, "character": 0}, + "end": {"line": 17, "character": 15}}, + "newText": "termination_by x1 => x1"}]}]}} diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out index f185b622f2..6c181f5080 100644 --- a/tests/lean/issue2981.lean.expected.out +++ b/tests/lean/issue2981.lean.expected.out @@ -3,11 +3,11 @@ Tactic is run (ideally only twice) Tactic is run (ideally only twice) Tactic is run (ideally only once, in most general context) n : Nat -⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n) +⊢ (invImage (fun a => a) instWellFoundedRelation).1 n (Nat.succ n) Tactic is run (ideally only twice, in most general context) Tactic is run (ideally only twice, in most general context) n : Nat ⊢ sizeOf n < sizeOf (Nat.succ n) n m : Nat -⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 } +⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 } { fst := Nat.succ n, snd := m }