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.
225 lines
6 KiB
Text
225 lines
6 KiB
Text
namespace Ex0
|
||
|
||
-- NB: no parameter
|
||
theorem elim_without_param {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) : motive n :=
|
||
case1 _
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_without_param
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_without_param
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using (elim_without_param) -- Error: unexpected eliminator resulting type
|
||
case case1 n => rfl
|
||
|
||
end Ex0
|
||
|
||
namespace Ex1
|
||
|
||
-- NB: p before motive
|
||
theorem elim_with_param (p : Bool) {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) : motive n :=
|
||
if p then case1 _ else case1 _
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param
|
||
case p => exact true -- uninstantiated parameters becomes goal
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_with_param
|
||
case p => exact true -- uninstantiated parameters becomes goal
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param (p := true)
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param true
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- not really a useful idiom, but it better works:
|
||
induction n using fun motive case1 n => @elim_with_param true motive case1 n
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- NB: no renaming of cases this way?
|
||
induction n using fun motive the_case n => @elim_with_param true motive the_case n
|
||
case case1 n => rfl
|
||
|
||
end Ex1
|
||
|
||
namespace Ex2
|
||
|
||
-- NB: p after motive
|
||
theorem elim_with_param {motive : Nat → Prop} (case1 : ∀ n, motive n) (n : Nat) (p : Bool) : motive n :=
|
||
if p then case1 _ else case1 _
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param
|
||
case p => exact true
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_with_param
|
||
case p => exact true
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using elim_with_param (p := true)
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
induction n using @elim_with_param (p := true)
|
||
case case1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- This renames the cases with unhelpful names
|
||
induction n using elim_with_param _ _ true
|
||
case x_1 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- We can put in custom names
|
||
induction n using elim_with_param ?case2 _ true
|
||
case case2 n => rfl
|
||
|
||
example (n : Nat) : n = n := by
|
||
-- not really a useful idiom, but it works:
|
||
induction n using fun motive case1 n => @elim_with_param motive case1 n true
|
||
case case1 n => rfl
|
||
|
||
end Ex2
|
||
|
||
namespace Ex3
|
||
|
||
-- Mutual induction, multiple motives
|
||
|
||
mutual
|
||
inductive A : Type u where | mkA : B → A | A : A
|
||
inductive B : Type u where | mkB : A → B
|
||
end
|
||
|
||
-- NB: A.rec is configured as elab_as_elim,
|
||
-- but in `using` it should not matter
|
||
|
||
-- For comparison, a copy without that attribute
|
||
noncomputable def A_rec := @A.rec
|
||
|
||
set_option linter.unusedVariables false
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using A.rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using A_rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial -- Error: type mismatch
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using @A.rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial
|
||
|
||
example (a : A) : True := by
|
||
-- motive_2 becomes a mvar
|
||
induction a using @A_rec
|
||
case mkA b IH =>
|
||
refine True.rec ?_ IH -- A hack to instantiate the motive_2 mvar
|
||
exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => show True; exact trivial
|
||
|
||
example (a : A) : True := by
|
||
induction a using fun motive_1 => @A.rec motive_1 (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
example (a : A) : True := by
|
||
induction a using fun motive_1 => @A_rec motive_1 (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
example (a : A) : True := by
|
||
induction a using @A.rec (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
example (a : A) : True := by
|
||
induction a using @A_rec (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
example (a : A) : True := by
|
||
-- A.rec is marked elab_as_elim, and normally elaborating
|
||
-- #check A.rec (motive_2 := fun b => True)
|
||
-- fails with
|
||
-- > failed to elaborate eliminator, expected type is not available
|
||
-- so we elaborate with heedElabAsElim := false
|
||
induction a using A.rec (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
example (a : A) : True := by
|
||
induction a using A_rec (motive_2 := fun b => True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH => exact trivial
|
||
|
||
end Ex3
|
||
|
||
namespace Ex4
|
||
|
||
-- We can use parameters as elaborators
|
||
|
||
set_option linter.unusedVariables false in
|
||
example
|
||
(α : Type u)
|
||
(ela : ∀ {motive : α → Prop} (case1 : ∀ (x : α), motive x) (x : α), motive x)
|
||
(x : α)
|
||
: x = x := by
|
||
induction x using ela
|
||
case case1 x => rfl
|
||
|
||
end Ex4
|
||
|
||
namespace Ex5
|
||
|
||
-- Multiple motives, different number of extra assumptions
|
||
|
||
mutual
|
||
inductive A : Type u where | mkA : B → A | A : A
|
||
inductive B : Type u where | mkB : A → B
|
||
end
|
||
|
||
set_option linter.unusedVariables false in
|
||
example (a : A) : True := by
|
||
induction a using A.rec (motive_2 := fun b => (heq : b = b) -> True)
|
||
case mkA b IH => exact trivial
|
||
case A => exact trivial
|
||
case mkB b IH h => exact trivial
|
||
|
||
end Ex5
|