From 1027d052cb326fb8f64944c3ae5a6f71b7abe012 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Nov 2015 14:01:41 -0800 Subject: [PATCH] test(tests/lean/simplifier1): add HoTT test for simplifier --- tests/lean/simplifier1.hlean | 27 +++++++++++++++++++++++ tests/lean/simplifier1.hlean.expected.out | 2 ++ 2 files changed, 29 insertions(+) create mode 100644 tests/lean/simplifier1.hlean create mode 100644 tests/lean/simplifier1.hlean.expected.out diff --git a/tests/lean/simplifier1.hlean b/tests/lean/simplifier1.hlean new file mode 100644 index 000000000..8c17fde48 --- /dev/null +++ b/tests/lean/simplifier1.hlean @@ -0,0 +1,27 @@ +open nat +-- deeper congruence + +universe l +constants (T : Type.{l}) (x1 x2 x3 x4 x5 x6 : T) (f : T → T → T) +constants (f_comm : ∀ x y, f x y = f y x) + (f_l : ∀ x y z, f (f x y) z = f x (f y z)) + (f_r : ∀ x y z, f x (f y z) = f y (f x z)) + +attribute f_comm [simp] +attribute f_l [simp] +attribute f_r [simp] + +#simplify eq 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6)))) + +open is_trunc + +constants g : Π (x y : nat), x ≠ y → Type₁ +constants a b c : nat +constants H₁ : a ≠ b +constants H₂ : a = c +attribute H₂ [simp] + +definition ne_is_hprop [instance] (a b : nat) : is_hprop (a ≠ b) := +sorry + +#simplify eq 0 (g a b H₁) diff --git a/tests/lean/simplifier1.hlean.expected.out b/tests/lean/simplifier1.hlean.expected.out new file mode 100644 index 000000000..5040023c8 --- /dev/null +++ b/tests/lean/simplifier1.hlean.expected.out @@ -0,0 +1,2 @@ +f x1 (f x2 (f x3 (f x4 (f x5 x6)))) +g c b (eq.nrec (eq.nrec H₁ b (eq.refl b)) c H₂)