b5122b6a7b
This change * moves `termination_by` and `decreasing_by` next to the function they apply to * simplify the syntax of `termination_by` * apply the `decreasing_by` goal to all goals at once, for better interactive use. See the section in `RELEASES.md` for more details and migration advise. This is a hard breaking change, requiring developers to touch every `termination_by` in their code base. We decided to still do it as a hard-breaking change, because supporting both old and new syntax at the same time would be non-trivial, and not save that much. Moreover, this requires changes to some metaprograms that developers might have written, and supporting both syntaxes at the same time would make _their_ migration harder.
50 lines
2.3 KiB
Text
50 lines
2.3 KiB
Text
decreasing_by.lean:36:0-43:17: error: Could not find a decreasing measure.
|
|
The arguments relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 36:29-43 = ?
|
|
2) 36:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
decreasing_by.lean:66:0-73:19: error: Could not find a decreasing measure.
|
|
The arguments relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 66:29-43 = ?
|
|
2) 66:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic
|
|
decreasing_by.lean:81:0-81:13: error: unsolved goals
|
|
n m : Nat
|
|
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
|
{ fst := n, snd := dec2 m } { fst := n, snd := m }
|
|
|
|
n m : Nat
|
|
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
|
{ fst := dec1 n, snd := 100 } { fst := n, snd := m }
|
|
decreasing_by.lean:91:0-91:22: error: unsolved goals
|
|
case a
|
|
n m : Nat
|
|
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
|
{ fst := n, snd := dec2 m } { fst := n, snd := m }
|
|
|
|
n m : Nat
|
|
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
|
{ fst := dec1 n, snd := 100 } { fst := n, snd := m }
|
|
decreasing_by.lean:99:0-100:22: error: Could not find a decreasing measure.
|
|
The arguments relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 99:29-43 = ?
|
|
2) 99:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
decreasing_by.lean:110:0-113:17: error: unsolved goals
|
|
n m : Nat
|
|
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
|
{ fst := dec1 n, snd := 100 } { fst := n, snd := m }
|
|
decreasing_by.lean:121:0-125:17: error: Could not find a decreasing measure.
|
|
The arguments relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
n m
|
|
1) 121:29-43 = ?
|
|
2) 121:46-62 ? _
|
|
Please use `termination_by` to specify a decreasing measure.
|