From 60d5e87a66d2564966e39dafe60d78721e0628f3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Aug 2014 09:04:39 -0700 Subject: [PATCH] test(tests/lean/run): add matrix test Signed-off-by: Leonardo de Moura --- tests/lean/run/matrix.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 tests/lean/run/matrix.lean diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean new file mode 100644 index 000000000..a26ff9f3e --- /dev/null +++ b/tests/lean/run/matrix.lean @@ -0,0 +1,20 @@ +import logic + +variable matrix.{l} : Type.{l} → Type.{l} +variable same_dim {A : Type} : matrix A → matrix A → Prop +variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A + +theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add A m1 m2 H1 = @add A m1 m2 H2 := +have eq : H1 = H2, from rfl, +subst eq rfl + +theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' := +subst H1 (subst H2 H) + +theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) := +have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq_rec (eq_rec H H1) H2), from + assume H1 H2, rfl, +have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2), from + subst H1 (subst H2 base), +calc @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2) : general H1 H2 + ... = @add A m1' m2' (same_dim_eq_args H1 H2 H) : same_dim_irrel