From cbae6a2ca0d92a27a94153a0960b81fd020273ca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Jan 2015 17:04:17 -0800 Subject: [PATCH] test(tests/lean/run): define list filter function using recursive equations --- tests/lean/run/eq20.lean | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 tests/lean/run/eq20.lean diff --git a/tests/lean/run/eq20.lean b/tests/lean/run/eq20.lean new file mode 100644 index 000000000..1ca5a107f --- /dev/null +++ b/tests/lean/run/eq20.lean @@ -0,0 +1,31 @@ +import data.list +open nat list + +context + parameter {A : Type} + parameter (p : A → Prop) + parameter [H : decidable_pred p] + include H + + definition filter : list A → list A, + filter nil := nil, + filter (a :: l) := if p a then a :: filter l else filter l + + theorem filter_nil : filter nil = nil := + rfl + + theorem filter_cons (a : A) (l : list A) : filter (a :: l) = if p a then a :: filter l else filter l := + rfl + + open eq.ops + + theorem filter_cons_of_pos {a : A} (l : list A) (h : p a) : filter (a :: l) = a :: filter l := + if_pos h ▸ filter_cons a l + + theorem filter_cons_of_neg {a : A} (l : list A) (h : ¬ p a) : filter (a :: l) = filter l := + if_neg h ▸ filter_cons a l +end + +check @filter +check @filter_cons_of_pos +check @filter_cons_of_neg