mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
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.
27 lines
972 B
Plaintext
27 lines
972 B
Plaintext
theorem ex1 : ∀ {a : Nat}, a * 2 = 2 * a :=
|
|
fun {a} =>
|
|
have h := fun a b => Eq.refl (a * b);
|
|
Eq.mp
|
|
(forall_congr fun a =>
|
|
forall_congr fun b =>
|
|
(fun a a_1 e_a =>
|
|
Eq.rec (motive := fun a_2 e_a => ∀ (a_3 : Nat), (a = a_3) = (a_2 = a_3)) (fun a_2 => Eq.refl (a = a_2)) e_a)
|
|
(a * b) (b * a) (Eq.trans (congrArg (fun _a => _a) (Nat.mul_comm a b)) (Eq.refl (b * a))) (a * b))
|
|
h 2 a
|
|
theorem ex2 : ∀ {a : Nat}, a * 2 = 2 * a :=
|
|
fun {a} =>
|
|
have h := Eq.refl fun x y => x * y;
|
|
congrFun
|
|
(congrFun
|
|
(Eq.mp
|
|
((fun a a_1 e_a =>
|
|
Eq.rec (motive := fun a_2 e_a => ∀ (a_3 : Nat → Nat → Nat), (a = a_3) = (a_2 = a_3))
|
|
(fun a_2 => Eq.refl (a = a_2)) e_a)
|
|
(fun x y => x * y) (fun x y => y * x)
|
|
(funext fun x =>
|
|
id (funext fun y => id (Eq.trans (congrArg (fun _a => _a) (Nat.mul_comm x y)) (Eq.refl (y * x)))))
|
|
Nat.mul)
|
|
h)
|
|
2)
|
|
a
|