From 7a2ae8d40b1a3a0bc8fa959d5ccd4672af53d017 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Dec 2016 18:26:57 -0800 Subject: [PATCH] test(tests/lean/run/ematch1): add ematching example --- tests/lean/run/ematch1.lean | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/lean/run/ematch1.lean diff --git a/tests/lean/run/ematch1.lean b/tests/lean/run/ematch1.lean new file mode 100644 index 0000000000..50a4f2f6aa --- /dev/null +++ b/tests/lean/run/ematch1.lean @@ -0,0 +1,33 @@ +constant f : nat → nat +constant g : nat → nat +axiom Ax : ∀ x, (: f (g x) :) = x + +open tactic + +meta def add_insts : list (expr × expr) → tactic unit +| [] := skip +| ((inst, pr)::r) := do + assertv `_einst inst pr, + add_insts r + +meta def ematch_test (h : name) (e : expr) : tactic unit := +do cc ← cc_state.mk_using_hs, + ems ← return $ ematch_state.mk 10000, + hlemma ← hinst_lemma.mk_from_decl h, + (r, cc, ems) ← ematch cc ems hlemma e, + add_insts r + +example (a b c : nat) : f a = b → a = g c → f a ≠ c → false := +by do + intros, + e ← to_expr `(f a), + ematch_test `Ax e, + trace_state, + cc + +example (a b c : nat) : f a = b → a = g c → f a = c := +by do + intros, + e ← to_expr `(f a), + ematch_test `Ax e, + cc