From 6fbbf66565adde395eb5e1738e3bdf64d920aa36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 29 Nov 2014 13:28:01 -0800 Subject: [PATCH] test(tests/lean/run/vector): define 'map' on vector using brec_on and new inversion tactic --- tests/lean/run/vector.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index c2d1ea2971..8e9e2ead0f 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -94,4 +94,26 @@ namespace vector example : add (1 :: 2 :: vnil) (3 :: 5 :: vnil) = 4 :: 7 :: vnil := rfl + definition map {A B C : Type} {n : nat} (f : A → B → C) (w : vector A n) (v : vector B n) : vector C n := + let P := λ (n : nat) (v : vector A n), vector B n → vector C n in + @brec_on A P n w + (λ (n : nat) (w : vector A n), + begin + cases w with (n₁, h₁, t₁), + show @below A P zero vnil → vector B zero → vector C zero, from + λ b v, vnil, + show @below A P (succ n₁) (h₁ :: t₁) → vector B (succ n₁) → vector C (succ n₁), from + λ b v, + begin + cases v with (n₂, h₂, t₂), + have r : vector B n₂ → vector C n₂, from pr₁ b, + (f h₁ h₂) :: r t₂, + end + end) v + + example : map num.add (1 :: 2 :: vnil) (3 :: 5 :: vnil) = 4 :: 7 :: vnil := + rfl + + print definition map + end vector