08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
827 lines
22 KiB
Text
827 lines
22 KiB
Text
import Lean.Elab.Command
|
||
import Lean.Elab.PreDefinition.WF.Eqns
|
||
import Lean.Meta.Tactic.FunInd
|
||
|
||
set_option guard_msgs.diff true
|
||
|
||
namespace Unary
|
||
|
||
def ackermann : (Nat × Nat) → Nat
|
||
| (0, m) => m + 1
|
||
| (n+1, 0) => ackermann (n, 1)
|
||
| (n+1, m+1) => ackermann (n, ackermann (n + 1, m))
|
||
termination_by p => p
|
||
|
||
/--
|
||
info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m))
|
||
(case2 : ∀ (n : Nat), motive (n, 1) → motive (n.succ, 0))
|
||
(case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ))
|
||
(a✝ : Nat × Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check ackermann.induct
|
||
|
||
end Unary
|
||
|
||
namespace Binary
|
||
|
||
def ackermann : Nat → Nat → Nat
|
||
| 0, m => m + 1
|
||
| n+1, 0 => ackermann n 1
|
||
| n+1, m+1 => ackermann n (ackermann (n + 1) m)
|
||
termination_by n m => (n, m)
|
||
|
||
/--
|
||
info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
|
||
(case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0)
|
||
(case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) (a✝ a✝¹ : Nat) :
|
||
motive a✝ a✝¹
|
||
-/
|
||
#guard_msgs in
|
||
#check ackermann.induct
|
||
|
||
end Binary
|
||
|
||
universe u
|
||
|
||
inductive Tree | node : List Tree → Tree
|
||
def Tree.rev : Tree → Tree
|
||
| node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ => t.rev) |>.reverse)
|
||
|
||
/--
|
||
info: Tree.rev.induct (motive : Tree → Prop)
|
||
(case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (a✝ : Tree) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check Tree.rev.induct
|
||
|
||
|
||
def fib : Nat → Nat
|
||
| 0 => 1
|
||
| 1 => 1
|
||
| n+2 => fib n + fib (n+1)
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
|
||
(case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check fib.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def have_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
have h2 : n < n+1 := Nat.lt_succ_self n
|
||
have_tailrec n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
|
||
(a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check have_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def have_non_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
Nat.succ <|
|
||
have h2 : n < n+1 := Nat.lt_succ_self n
|
||
have_non_tailrec n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
|
||
(a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check have_non_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def let_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
let h2 : n < n+1 := Nat.lt_succ_self n
|
||
let_tailrec n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
|
||
(a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check let_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def let_non_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
Nat.succ <|
|
||
let h2 : n < n+1 := Nat.lt_succ_self n
|
||
let_non_tailrec n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
|
||
(a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check let_non_tailrec.induct
|
||
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_ite_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
if n % 2 = 0 then
|
||
with_ite_tailrec n
|
||
else
|
||
with_ite_tailrec (n-1)
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
|
||
(case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
|
||
(case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive (n - 1) → motive n.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_ite_tailrec.induct
|
||
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_ite_non_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| 1 => 1
|
||
| n+2 =>
|
||
Nat.succ <|
|
||
if n % 2 = 0 then
|
||
with_ite_non_tailrec (n+1)
|
||
else
|
||
with_ite_non_tailrec n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
|
||
(case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_ite_non_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_dite_non_tailrec (n : Nat) : Nat :=
|
||
Nat.succ <|
|
||
if h : n - 1 < n then
|
||
with_dite_non_tailrec (n-1)
|
||
else
|
||
0
|
||
termination_by n
|
||
|
||
/--
|
||
info: with_dite_non_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (x - 1 < x → motive (x - 1)) → motive x)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check with_dite_non_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_dite_tailrec (n : Nat) : Nat :=
|
||
if h : n - 1 < n then
|
||
with_dite_tailrec (n-1)
|
||
else
|
||
0
|
||
termination_by n
|
||
|
||
/--
|
||
info: with_dite_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), x - 1 < x → motive (x - 1) → motive x)
|
||
(case2 : ∀ (x : Nat), ¬x - 1 < x → motive x) (n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check with_dite_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_bif_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
bif n % 2 == 0 then
|
||
with_bif_tailrec n
|
||
else
|
||
with_bif_tailrec (n-1)
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_bif_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
|
||
(case2 : ∀ (n : Nat), (n % 2 == 0) = true → motive n → motive n.succ)
|
||
(case3 : ∀ (n : Nat), (n % 2 == 0) = false → motive (n - 1) → motive n.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_bif_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_match_refining_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
match n with
|
||
| 0 => with_match_refining_tailrec 0
|
||
| m => with_match_refining_tailrec m
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0))
|
||
(case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_match_refining_tailrec.induct
|
||
|
||
|
||
|
||
def with_arg_refining_match1 (i : Nat) : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
if h : i = 0 then 0 else with_arg_refining_match1 (i - 1) n
|
||
termination_by i
|
||
|
||
/--
|
||
info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0)
|
||
(case2 : ∀ (n : Nat), motive 0 n.succ) (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i n.succ)
|
||
(i a✝ : Nat) : motive i a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_arg_refining_match1.induct
|
||
|
||
def with_arg_refining_match2 (i : Nat) (n : Nat) : Nat :=
|
||
if i = 0 then 0 else match n with
|
||
| 0 => 0
|
||
| n+1 => with_arg_refining_match2 (i - 1) n
|
||
termination_by i
|
||
|
||
/--
|
||
info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), motive 0 n)
|
||
(case2 : ∀ (i : Nat), ¬i = 0 → motive i 0)
|
||
(case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i n.succ) (i n : Nat) : motive i n
|
||
-/
|
||
#guard_msgs in
|
||
#check with_arg_refining_match2.induct
|
||
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_other_match_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
match n % 2 with
|
||
| 0 => with_other_match_tailrec n
|
||
| _ => with_other_match_tailrec n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
|
||
(case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
|
||
(case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_other_match_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_mixed_match_tailrec : Nat → Nat → Nat → Nat → Nat := fun a b c d =>
|
||
match a, h: b, c % 2, h : d % 2 with
|
||
| 0, _, _, _ => 0
|
||
| a+1, x, y, z => with_mixed_match_tailrec a x y z
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 x : Nat), motive 0 x a a_1)
|
||
(case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive a_2.succ x a a_1) (a✝ a✝¹ a✝² a✝³ : Nat) :
|
||
motive a✝ a✝¹ a✝² a✝³
|
||
-/
|
||
#guard_msgs in
|
||
#check with_mixed_match_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_mixed_match_tailrec2 : Nat → Nat → Nat → Nat → Nat → Nat := fun n a b c d =>
|
||
match n with
|
||
| 0 => 0
|
||
| n+1 =>
|
||
match a, h: b, c % 2, h : d % 2 with
|
||
| 0, _, _, _ => 0
|
||
| a+1, x, y, z => with_mixed_match_tailrec2 n a x y z
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop)
|
||
(case1 : ∀ (a a_1 a_2 a_3 : Nat), motive 0 a a_1 a_2 a_3) (case2 : ∀ (a a_1 n x : Nat), motive n.succ 0 x a a_1)
|
||
(case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive n.succ a_2.succ x a a_1)
|
||
(a✝ a✝¹ a✝² a✝³ a✝⁴ : Nat) : motive a✝ a✝¹ a✝² a✝³ a✝⁴
|
||
-/
|
||
#guard_msgs in
|
||
#check with_mixed_match_tailrec2.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_match_non_tailrec : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
Nat.succ <|
|
||
match n % 2 with
|
||
| 0 => with_match_non_tailrec n
|
||
| _ => with_match_non_tailrec n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
|
||
(a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_match_non_tailrec.induct
|
||
|
||
set_option linter.unusedVariables false in
|
||
def with_match_non_tailrec_refining : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
Nat.succ <|
|
||
match n with
|
||
| 0 => with_match_non_tailrec_refining 0
|
||
| m => with_match_non_tailrec_refining m
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : motive 0)
|
||
(case2 :
|
||
∀ (n : Nat),
|
||
(match n with
|
||
| 0 => motive 0
|
||
| m => motive m) →
|
||
motive n.succ)
|
||
(a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_match_non_tailrec_refining.induct
|
||
|
||
|
||
def with_overlap : Nat → Nat
|
||
| 0 => 0
|
||
| 1 => 1
|
||
| 2 => 2
|
||
| 3 => 3
|
||
| n+1 => with_overlap n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3)
|
||
(case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) (a✝ : Nat) :
|
||
motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check with_overlap.induct
|
||
|
||
namespace UnusedExtraParams
|
||
|
||
-- This test how unused fixed function parameters are handled.
|
||
-- See comment in the code
|
||
|
||
def unary (base : Nat) : Nat → Nat
|
||
| 0 => base
|
||
| n+1 => unary base n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: UnusedExtraParams.unary.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
|
||
(a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check unary.induct
|
||
|
||
def binary (base : Nat) : Nat → Nat → Nat
|
||
| 0, m => base + m
|
||
| n+1, m => binary base n m
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: UnusedExtraParams.binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
|
||
(case2 : ∀ (n m : Nat), motive n m → motive n.succ m) (a✝ a✝¹ : Nat) : motive a✝ a✝¹
|
||
-/
|
||
#guard_msgs in
|
||
#check binary.induct
|
||
|
||
end UnusedExtraParams
|
||
|
||
namespace NonTailrecMatch
|
||
|
||
def match_non_tail (n : Nat ) : Bool :=
|
||
n = 42 || match n with
|
||
| 0 => true
|
||
| 1 => true
|
||
| n+2 => match_non_tail n && match_non_tail (n+1)
|
||
termination_by n
|
||
|
||
def match_non_tail_induct
|
||
{motive : Nat → Prop}
|
||
(case1 : forall n, (IH : match n with | 0 => True | n+1 => motive n) → motive n)
|
||
(n : Nat) : motive n :=
|
||
WellFounded.fix Nat.lt_wfRel.wf (fun n IH =>
|
||
match n with
|
||
| 0 => case1 0 True.intro
|
||
| n+1 =>
|
||
case1 (n+1) (IH n (Nat.lt_succ_self _))
|
||
) n
|
||
|
||
|
||
/--
|
||
info: NonTailrecMatch.match_non_tail.induct (motive : Nat → Prop)
|
||
(case1 :
|
||
∀ (x : Nat),
|
||
(match x with
|
||
| 0 => True
|
||
| 1 => True
|
||
| n.succ.succ => motive n ∧ motive (n + 1)) →
|
||
motive x)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check match_non_tail.induct
|
||
|
||
|
||
theorem match_non_tail_eq_true (n : Nat) : match_non_tail n = true := by
|
||
induction n using match_non_tail.induct
|
||
case case1 n IH =>
|
||
unfold match_non_tail
|
||
split <;> dsimp at IH <;> simp [IH]
|
||
|
||
end NonTailrecMatch
|
||
|
||
|
||
namespace AsPattern
|
||
|
||
def foo (n : Nat) :=
|
||
match n with
|
||
| 0 => 0
|
||
| x@(n+1) => x + foo n
|
||
termination_by n
|
||
|
||
/--
|
||
info: AsPattern.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
|
||
|
||
def bar (n : Nat) :=
|
||
1 +
|
||
match n with
|
||
| 0 => 0
|
||
| x@(n+1) => x + bar n
|
||
termination_by n
|
||
|
||
/--
|
||
info: AsPattern.bar.induct (motive : Nat → Prop)
|
||
(case1 :
|
||
∀ (x : Nat),
|
||
(match x with
|
||
| 0 => True
|
||
| x@h:n.succ => motive n) →
|
||
motive x)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check bar.induct
|
||
|
||
end AsPattern
|
||
|
||
namespace GramSchmidt
|
||
|
||
-- this tried to reproduce a problem with gramSchmidt,
|
||
-- with more proofs from `simp` abstracting over the IH.
|
||
-- I couldn't quite reproduce it, but let's keep it.
|
||
|
||
def below (n i : Nat) := i < n
|
||
|
||
@[simp]
|
||
def below_lt (n i : Nat) (h : below n i) : i < n := h
|
||
|
||
def sum_below (n : Nat) (f : (i : Nat) → below n i → Nat) :=
|
||
match n with
|
||
| 0 => 0
|
||
| n+1 => sum_below n (fun i hi => f i (Nat.lt_succ_of_le (Nat.le_of_lt hi))) +
|
||
f n (Nat.lt_succ_self n)
|
||
|
||
def foo (n : Nat) :=
|
||
1 + sum_below n (fun i _ => foo i)
|
||
termination_by n
|
||
decreasing_by simp [below_lt, *]
|
||
|
||
/--
|
||
info: GramSchmidt.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (i : Nat), below x i → motive i) → motive x)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
end GramSchmidt
|
||
|
||
namespace Have
|
||
|
||
def foo {α} (x : α) : List α → Nat
|
||
| .nil => 0
|
||
| .cons _y ys =>
|
||
let this := foo x ys
|
||
this
|
||
termination_by xs => xs
|
||
/--
|
||
info: Have.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
|
||
(case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
|
||
def bar {α} (x : α) : List α → Nat
|
||
| .nil => 0
|
||
| .cons _y ys =>
|
||
have this := bar x ys
|
||
this
|
||
termination_by xs => xs
|
||
|
||
/--
|
||
info: Have.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
|
||
(case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check bar.induct
|
||
|
||
end Have
|
||
|
||
|
||
namespace RecCallInDisrs
|
||
|
||
def foo : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 => if foo n = 0 then 1 else 0
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0)
|
||
(case2 : ∀ (n : Nat), foo n = 0 → motive n → motive n.succ)
|
||
(case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
|
||
set_option linter.unusedVariables false in
|
||
def bar : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 => match _h : n, bar n with
|
||
| 0, 0 => 0
|
||
| 0, _ => 1
|
||
| m+1, _ => bar m
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0))
|
||
(case3 : (bar 0 = 0 → False) → motive 0 → motive (Nat.succ 0))
|
||
(case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check bar.induct
|
||
|
||
end RecCallInDisrs
|
||
|
||
namespace EvenOdd
|
||
|
||
mutual
|
||
def even : (m : Nat) → Bool -- NB: Does this parameter name appear in the inductions?
|
||
| 0 => true
|
||
| n+1 => odd n
|
||
termination_by n => n
|
||
def odd : Nat → Bool
|
||
| 0 => false
|
||
| n+1 => even n
|
||
termination_by n => n
|
||
end
|
||
|
||
/--
|
||
info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
|
||
(case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (m : Nat) : motive1 m
|
||
-/
|
||
#guard_msgs in
|
||
#check even.induct
|
||
|
||
/--
|
||
info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
|
||
(case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive2 a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check odd.induct
|
||
|
||
/--
|
||
info: EvenOdd.even.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0)
|
||
(case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case3 : motive2 0)
|
||
(case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : (∀ (m : Nat), motive1 m) ∧ ∀ (a : Nat), motive2 a
|
||
-/
|
||
#guard_msgs in
|
||
#check even.mutual_induct
|
||
|
||
end EvenOdd
|
||
|
||
namespace Tree
|
||
|
||
inductive Tree : Type
|
||
| node : List Tree → Tree
|
||
|
||
mutual
|
||
def Tree.map (f : Tree → Tree) : Tree → Tree
|
||
| Tree.node ts => Tree.node (map_forest f ts)
|
||
|
||
def Tree.map_forest (f : Tree → Tree) (ts : List Tree) : List Tree :=
|
||
ts.attach.map (fun ⟨t, _ht⟩ => Tree.map f t)
|
||
end
|
||
|
||
/--
|
||
info: Tree.Tree.map.induct (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
|
||
(case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
|
||
(case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (a✝ : Tree) : motive1 a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check Tree.map.induct
|
||
|
||
/--
|
||
info: Tree.Tree.map_forest.induct (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
|
||
(case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
|
||
(case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (ts : List Tree) : motive2 ts
|
||
-/
|
||
#guard_msgs in
|
||
#check Tree.map_forest.induct
|
||
|
||
/--
|
||
info: Tree.Tree.map.mutual_induct (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
|
||
(case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
|
||
(case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) :
|
||
(∀ (a : Tree), motive1 a) ∧ ∀ (ts : List Tree), motive2 ts
|
||
-/
|
||
#guard_msgs in
|
||
#check Tree.map.mutual_induct
|
||
|
||
end Tree
|
||
|
||
namespace DefaultArgument
|
||
|
||
-- Default arguments should not be copied over
|
||
|
||
def unary (fixed : Bool := false) (n : Nat := 0) : Nat :=
|
||
match n with
|
||
| 0 => 0
|
||
| n+1 => unary fixed n
|
||
termination_by n
|
||
|
||
/--
|
||
info: DefaultArgument.unary.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check unary.induct
|
||
|
||
def foo (fixed : Bool := false) (n : Nat) (m : Nat := 0) : Nat :=
|
||
match n with
|
||
| 0 => m
|
||
| n+1 => foo fixed n m
|
||
termination_by n
|
||
|
||
/--
|
||
info: DefaultArgument.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
end DefaultArgument
|
||
|
||
namespace Nary
|
||
|
||
def foo : Nat → Nat → (k : Nat) → Fin k → Nat
|
||
| 0, _, _, _ => 0
|
||
| _, 0, _, _ => 0
|
||
| _, _, 0, _ => 0
|
||
| _, _, 1, _ => 0
|
||
| n+1, m+1, k+2, _ => foo n m (k+1) ⟨0, Nat.zero_lt_succ _⟩
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop) (case1 : ∀ (k x : Nat) (x_1 : Fin k), motive 0 x k x_1)
|
||
(case2 : ∀ (k x : Nat), (x = 0 → False) → ∀ (x_2 : Fin k), motive x 0 k x_2)
|
||
(case3 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 0), motive x x_1 0 a)
|
||
(case4 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 1), motive x x_1 1 a)
|
||
(case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a)
|
||
(a✝ a✝¹ k : Nat) (a✝² : Fin k) : motive a✝ a✝¹ k a✝²
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
end Nary
|
||
|
||
namespace Dite
|
||
|
||
def foo (n : Nat) : Nat :=
|
||
let j := n - 1
|
||
if _h : j < n then
|
||
foo j
|
||
else
|
||
42
|
||
|
||
/--
|
||
info: Dite.foo.induct (motive : Nat → Prop)
|
||
(case1 :
|
||
∀ (x : Nat),
|
||
have j := x - 1;
|
||
j < x → motive j → motive x)
|
||
(case2 :
|
||
∀ (x : Nat),
|
||
have j := x - 1;
|
||
¬j < x → motive x)
|
||
(n : Nat) : motive n
|
||
-/
|
||
#guard_msgs in
|
||
#check Dite.foo.induct
|
||
|
||
end Dite
|
||
|
||
|
||
namespace PreserveParams
|
||
|
||
/-
|
||
Tests that cleaning up the goal state does not throw away useful equalties
|
||
relating varying parameters to fixed ones.
|
||
-/
|
||
|
||
def foo (a : Nat) : Nat → Nat
|
||
| 0 => 0
|
||
| n+1 =>
|
||
if a = 23 then 23 else
|
||
if a = n then 42 else
|
||
foo a n
|
||
termination_by n => n
|
||
|
||
/--
|
||
info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motive 0)
|
||
(case2 : ∀ (n : Nat), a = 23 → motive n.succ) (case3 : ¬a = 23 → motive a.succ)
|
||
(case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) (a✝ : Nat) : motive a✝
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
|
||
end PreserveParams
|
||
|
||
namespace Mutual_Induct
|
||
|
||
/-! Tests that `mutual_induct` is properly reserved. -/
|
||
|
||
mutual
|
||
def even : Nat → Bool
|
||
| 0 => true
|
||
| n+1 => odd n
|
||
termination_by n => n
|
||
def odd : Nat → Bool
|
||
| 0 => false
|
||
| n+1 => even n
|
||
termination_by n => n
|
||
end
|
||
|
||
-- The following tests uses that guard_msgs reverts the environment,
|
||
-- so they all test that the mutual induct is really generated by these commands
|
||
|
||
/--
|
||
info: Mutual_Induct.even.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0)
|
||
(case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case3 : motive2 0)
|
||
(case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : (∀ (a : Nat), motive1 a) ∧ ∀ (a : Nat), motive2 a
|
||
-/
|
||
#guard_msgs in
|
||
#check even.mutual_induct
|
||
|
||
-- The .mutual_induct only exists on the first declaration:
|
||
|
||
/-- error: Unknown constant `Mutual_Induct.odd.mutual_induct` -/
|
||
#guard_msgs in
|
||
#check odd.mutual_induct
|
||
|
||
/-- info: false -/
|
||
#guard_msgs in
|
||
open Lean Lean.Elab in
|
||
run_meta
|
||
logInfo m!"{Lean.Tactic.FunInd.isFunInductName (← getEnv) `Mutual_Induct.odd.mutual_induct}"
|
||
|
||
def nonmutual : Nat → Bool
|
||
| 0 => true
|
||
| n+1 => nonmutual n
|
||
|
||
/-- error: Unknown constant `Mutual_Induct.nonmutual.mutual_induct` -/
|
||
#guard_msgs in
|
||
#check nonmutual.mutual_induct
|
||
|
||
/-- error: Unknown constant `id.mutual_induct` -/
|
||
#guard_msgs in
|
||
set_option pp.mvars false in
|
||
#check id.mutual_induct
|
||
|
||
end Mutual_Induct
|