From 14ca2d407d3ad5de129f9870e04fc9728b2bf629 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Mar 2015 17:47:01 -0800 Subject: [PATCH] test(tests/lean/run): add match-with nested in tactic test --- tests/lean/run/match_tac4.lean | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/lean/run/match_tac4.lean diff --git a/tests/lean/run/match_tac4.lean b/tests/lean/run/match_tac4.lean new file mode 100644 index 000000000..b7e9ec153 --- /dev/null +++ b/tests/lean/run/match_tac4.lean @@ -0,0 +1,33 @@ +notation `⟪`:max t:(foldr `,` (e r, and.intro e r)) `⟫`:0 := t + +check ⟪ trivial, trivial, trivial ⟫ + +theorem tst (a b c d : Prop) : a ∧ b ∧ c ∧ d ↔ d ∧ c ∧ b ∧ a := +begin + apply iff.intro, + begin + intro H, + match H with + | ⟪ H₁, H₂, H₃, H₄ ⟫ := ⟪ H₄, H₃, H₂, H₁ ⟫ + end + end, + begin + intro H, + match H with + | ⟪ H₁, H₂, H₃, H₄ ⟫ := + begin + repeat [apply and.intro | assumption] + end + end + end +end + +print definition tst + +theorem tst2 (a b c d : Prop) : a ∧ b ∧ c ∧ d ↔ d ∧ c ∧ b ∧ a := +begin + apply iff.intro, + repeat (intro H; repeat [cases H with (H', H) | apply and.intro | assumption]) +end + +print definition tst2