ffbea840bf
If here is only one plausible measure, there is no point having the `GuessLex` code see if it is terminating, running all the tactics, only for the `MkFix` code then run the tactics again. So if there is only one plausible measure (non-mutual recursion with only one varying parameter), just use that measure. Side benefit: If the function isn’t terminating, more detailed error messages are shown (failing proof goals), located at the recursive calls.
113 lines
3.4 KiB
Text
113 lines
3.4 KiB
Text
/-!
|
||
This files tests Lean's ability to guess the right lexicographic order.
|
||
|
||
TODO: Once lean spits out the guessed order (probably guarded by an
|
||
option), turn this on and check the output.
|
||
|
||
When writing tests for GuesLex, keep in mind that it doesn't do anything
|
||
when there is only one plausible measure (one function, only one varying argument).
|
||
-/
|
||
|
||
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)
|
||
|
||
def ackermann2 (n m : Nat) := match n, m with
|
||
| m, 0 => m + 1
|
||
| 0, .succ n => ackermann2 1 n
|
||
| .succ m, .succ n => ackermann2 (ackermann2 m (n + 1)) n
|
||
|
||
def ackermannList (n m : List Unit) := match n, m with
|
||
| [], m => () :: m
|
||
| ()::n, [] => ackermannList n [()]
|
||
| ()::n, ()::m => ackermannList n (ackermannList (()::n) m)
|
||
|
||
def foo2 : Nat → Nat → Nat
|
||
| .succ n, 1 => foo2 n 1
|
||
| .succ n, 2 => foo2 (.succ n) 1
|
||
| n, 3 => foo2 (.succ n) 2
|
||
| .succ n, 4 => foo2 (if n > 10 then n else .succ n) 3
|
||
| n, 5 => foo2 (n - 1) 4
|
||
| n, .succ m => foo2 n m
|
||
| _, _ => 0
|
||
|
||
mutual
|
||
def even : Nat → Bool
|
||
| 0 => true
|
||
| .succ n => not (odd n)
|
||
def odd : Nat → Bool
|
||
| 0 => false
|
||
| .succ n => not (even n)
|
||
end
|
||
|
||
mutual
|
||
def evenWithFixed (m : String) : Nat → Bool
|
||
| 0 => true
|
||
| .succ n => not (oddWithFixed m n)
|
||
def oddWithFixed (m : String) : Nat → Bool
|
||
| 0 => false
|
||
| .succ n => not (evenWithFixed m n)
|
||
end
|
||
|
||
def ping (n : Nat) := pong n
|
||
where pong : Nat → Nat
|
||
| 0 => 0
|
||
| .succ n => ping n
|
||
|
||
def hasForbiddenArg (n : Nat) (_h : n = n) (m : Nat) : Nat :=
|
||
match n, m with
|
||
| 0, 0 => 0
|
||
| .succ m, n => hasForbiddenArg m rfl n
|
||
| m, .succ n => hasForbiddenArg (.succ m) rfl n
|
||
|
||
/-!
|
||
Example from “Finding Lexicographic Orders for Termination Proofs in
|
||
Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow,
|
||
10.1007/978-3-540-74591-4_5
|
||
-/
|
||
def blowup : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat
|
||
| 0, 0, 0, 0, 0, 0, 0, 0 => 0
|
||
| 0, 0, 0, 0, 0, 0, 0, .succ i => .succ (blowup i i i i i i i i)
|
||
| 0, 0, 0, 0, 0, 0, .succ h, i => .succ (blowup h h h h h h h i)
|
||
| 0, 0, 0, 0, 0, .succ g, h, i => .succ (blowup g g g g g g h i)
|
||
| 0, 0, 0, 0, .succ f, g, h, i => .succ (blowup f f f f f g h i)
|
||
| 0, 0, 0, .succ e, f, g, h, i => .succ (blowup e e e e f g h i)
|
||
| 0, 0, .succ d, e, f, g, h, i => .succ (blowup d d d e f g h i)
|
||
| 0, .succ c, d, e, f, g, h, i => .succ (blowup c c d e f g h i)
|
||
| .succ b, c, d, e, f, g, h, i => .succ (blowup b c d e f g h i)
|
||
|
||
-- Let’s try to confuse the lexicographic guessing function's
|
||
-- unpacking of packed n-ary arguments
|
||
def confuseLex1 : Nat → @PSigma Nat (fun _ => Nat) → Nat
|
||
| 0, _p => 0
|
||
| .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x, .succ y⟩
|
||
|
||
def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat
|
||
| ⟨_,0⟩ => 0
|
||
| ⟨0,_⟩ => 0
|
||
| ⟨.succ y,.succ n⟩ => confuseLex2 ⟨y,n⟩
|
||
|
||
def dependent : (n : Nat) → (m : Fin n) → Nat
|
||
| 0, i => Fin.elim0 i
|
||
| .succ 0, 0 => 0
|
||
| .succ (.succ n), 0 => dependent (.succ n) ⟨n, n.lt_succ_self⟩
|
||
| .succ (.succ n), ⟨.succ m, h⟩ =>
|
||
dependent (.succ (.succ n)) ⟨m, Nat.lt_of_le_of_lt (Nat.le_succ _) h⟩
|
||
|
||
|
||
-- An example based on a real world problem, condensed by Leo
|
||
inductive Expr where
|
||
| add (a b : Expr)
|
||
| val (n : Nat)
|
||
|
||
mutual
|
||
def eval (a : Expr) : Nat :=
|
||
match a with
|
||
| .add x y => eval_add (x, y)
|
||
| .val n => n
|
||
|
||
def eval_add (a : Expr × Expr) : Nat :=
|
||
match a with
|
||
| (x, y) => eval x + eval y
|
||
end
|