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.
117 lines
3.9 KiB
Text
117 lines
3.9 KiB
Text
import Lean
|
||
open Lean
|
||
|
||
namespace Ex
|
||
inductive LE : Nat → Nat → Prop
|
||
| refl : LE n n
|
||
| succ : LE n m → LE n m.succ
|
||
|
||
|
||
def typeOf {α : Sort u} (a : α) := α
|
||
|
||
theorem LE.trans' : LE m n → LE n o → LE m o
|
||
| h1, refl => h1
|
||
| h1, succ h2 => succ (trans' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
|
||
|
||
inductive Even : Nat → Prop
|
||
| zero : Even 0
|
||
| ss : Even n → Even n.succ.succ
|
||
|
||
theorem Even_brecOn : typeOf @Even.brecOn = ∀ {motive : (a : Nat) → Even a → Prop} {a : Nat} (x : Even a),
|
||
(∀ (a : Nat) (x : Even a), @Even.below motive a x → motive a x) → motive a x := rfl
|
||
|
||
theorem Even.add : Even n → Even m → Even (n+m) := by
|
||
intro h1 h2
|
||
induction h2 with
|
||
| zero => exact h1
|
||
| ss h2 ih => exact ss ih
|
||
|
||
theorem Even.add' : Even n → Even m → Even (n+m)
|
||
| h1, zero => h1
|
||
| h1, ss h2 => ss (add' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
|
||
|
||
theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
|
||
rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
|
||
|
||
inductive Power2 : Nat → Prop
|
||
| base : Power2 1
|
||
| ind : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
|
||
|
||
theorem Power2_brecOn : typeOf @Power2.brecOn = ∀ {motive : (a : Nat) → Power2 a → Prop} {a : Nat} (x : Power2 a),
|
||
(∀ (a : Nat) (x : Power2 a), @Power2.below motive a x → motive a x) → motive a x := rfl
|
||
|
||
theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
|
||
intro h1 h2
|
||
induction h2 with
|
||
| base => simp_all
|
||
| ind h2 ih => exact mul_left_comm .. ▸ ind ih
|
||
|
||
/- The following example fails because the structural recursion cannot be performed on the `Nat`s and
|
||
the `brecOn` construction doesn't work for inductive predicates (?????) -/
|
||
set_option trace.Elab.definition.structural true in
|
||
set_option trace.Meta.IndPredBelow.match true in
|
||
set_option pp.explicit true in
|
||
theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
|
||
| h1, base => by simp_all
|
||
| h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
|
||
|
||
inductive tm : Type :=
|
||
| C : Nat → tm
|
||
| P : tm → tm → tm
|
||
|
||
open tm
|
||
|
||
set_option hygiene false in
|
||
infixl:40 " ==> " => step
|
||
inductive step : tm → tm → Prop :=
|
||
| ST_PlusConstConst : ∀ n1 n2,
|
||
P (C n1) (C n2) ==> C (n1 + n2)
|
||
| ST_Plus1 : ∀ t1 t1' t2,
|
||
t1 ==> t1' →
|
||
P t1 t2 ==> P t1' t2
|
||
| ST_Plus2 : ∀ n1 t2 t2',
|
||
t2 ==> t2' →
|
||
P (C n1) t2 ==> P (C n1) t2'
|
||
|
||
def deterministic {X : Type} (R : X → X → Prop) :=
|
||
∀ x y1 y2 : X, R x y1 → R x y2 → y1 = y2
|
||
|
||
theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ =>
|
||
@step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ =>
|
||
match hy₁, hy₂ with
|
||
| step.below.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl
|
||
| step.below.ST_Plus1 _ _ _ hy₁ _ ih, step.ST_Plus1 _ t₁' _ _ => by rw [←ih t₁']; assumption
|
||
| step.below.ST_Plus1 _ _ _ hy₁ _ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁
|
||
| step.below.ST_Plus2 _ _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw [←ih t₂]; assumption
|
||
| step.below.ST_Plus2 _ _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁
|
||
) y₂ hy₂
|
||
|
||
section NestedRecursion
|
||
|
||
axiom f : Nat → Nat
|
||
|
||
inductive is_nat : Nat -> Prop
|
||
| Z : is_nat 0
|
||
| S {n} : is_nat n → is_nat (f n)
|
||
|
||
axiom P : Nat → Prop
|
||
axiom F0 : P 0
|
||
axiom F1 : P (f 0)
|
||
axiom FS {n : Nat} : P n → P (f (f n))
|
||
|
||
-- we would like to write this
|
||
theorem foo : ∀ {n}, is_nat n → P n
|
||
| _, is_nat.Z => F0
|
||
| _, is_nat.S is_nat.Z => F1
|
||
| _, is_nat.S (is_nat.S h) => FS (foo h)
|
||
|
||
theorem foo' : ∀ {n}, is_nat n → P n := fun h =>
|
||
@is_nat.brecOn (fun n hn => P n) _ h fun n h ih =>
|
||
match ih with
|
||
| is_nat.below.Z => F0
|
||
| is_nat.below.S _ is_nat.below.Z _ => F1
|
||
| is_nat.below.S _ (is_nat.below.S _ b hx) h₂ => FS hx
|
||
|
||
end NestedRecursion
|
||
|
||
end Ex
|