From bf2adb20e784fef5e3fea90ad32803d180e919b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Dec 2013 07:12:34 -0800 Subject: [PATCH] feat(library/tactic): add disj_hyp_tactic Signed-off-by: Leonardo de Moura --- src/library/tactic/boolean.cpp | 95 ++++++++++++++++++++++++++++ src/library/tactic/boolean.h | 3 + tests/lean/tactic7.lean | 50 +++++++++++++++ tests/lean/tactic7.lean.expected.out | 28 ++++++++ 4 files changed, 176 insertions(+) create mode 100644 tests/lean/tactic7.lean create mode 100644 tests/lean/tactic7.lean.expected.out diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp index 68f64de60..b241412a2 100644 --- a/src/library/tactic/boolean.cpp +++ b/src/library/tactic/boolean.cpp @@ -156,6 +156,90 @@ tactic conj_hyp_tactic(bool all) { }); } +optional disj_hyp_tactic_core(name const & goal_name, name const & hyp_name, proof_state const & s) { + buffer> new_goals_buf; + expr H; + expr conclusion; + for (auto const & p1 : s.get_goals()) { + check_interrupted(); + if (p1.first == goal_name) { + goal const & g = p1.second; + buffer new_hyp_buf1; + buffer new_hyp_buf2; + conclusion = g.get_conclusion(); + for (auto const & p2 : g.get_hypotheses()) { + if (p2.first == hyp_name) { + H = p2.second; + if (!is_or(H)) + return none_proof_state(); // tactic failed + new_hyp_buf1.emplace_back(p2.first, arg(H, 1)); + new_hyp_buf2.emplace_back(p2.first, arg(H, 2)); + } else { + new_hyp_buf1.push_back(p2); + new_hyp_buf2.push_back(p2); + } + } + if (!H) + return none_proof_state(); // tactic failed + new_goals_buf.emplace_back(name(goal_name, 1), update(g, new_hyp_buf1)); + new_goals_buf.emplace_back(name(goal_name, 2), update(g, new_hyp_buf2)); + } else { + new_goals_buf.push_back(p1); + } + } + if (!H) + return none_proof_state(); // tactic failed + goals new_gs = to_list(new_goals_buf.begin(), new_goals_buf.end()); + proof_builder pb = s.get_proof_builder(); + proof_builder new_pb = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { + proof_map new_m(m); + expr pr1 = find(m, name(goal_name, 1)); + expr pr2 = find(m, name(goal_name, 2)); + pr1 = Fun(hyp_name, arg(H, 1), pr1); + pr2 = Fun(hyp_name, arg(H, 2), pr2); + new_m.insert(goal_name, DisjCases(arg(H, 1), arg(H, 2), conclusion, mk_constant(hyp_name), pr1, pr2)); + new_m.erase(name(goal_name, 1)); + new_m.erase(name(goal_name, 2)); + return pb(new_m, a); + }); + return some_proof_state(s, new_gs, new_pb); +} + +tactic disj_hyp_tactic(name const & goal_name, name const & hyp_name) { + return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return disj_hyp_tactic_core(goal_name, hyp_name, s); + }); +} + +tactic disj_hyp_tactic(name const & hyp_name) { + return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + for (auto const & p1 : s.get_goals()) { + check_interrupted(); + goal const & g = p1.second; + for (auto const & p2 : g.get_hypotheses()) { + if (p2.first == hyp_name) + return disj_hyp_tactic_core(p1.first, hyp_name, s); + } + } + return none_proof_state(); // tactic failed + }); +} + +tactic disj_hyp_tactic() { + return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + for (auto const & p1 : s.get_goals()) { + check_interrupted(); + goal const & g = p1.second; + for (auto const & p2 : g.get_hypotheses()) { + if (is_or(p2.second)) + return disj_hyp_tactic_core(p1.first, p2.first, s); + } + } + return none_proof_state(); // tactic failed + }); +} + + static int mk_conj_tactic(lua_State * L) { int nargs = lua_gettop(L); return push_tactic(L, conj_tactic(nargs == 0 ? true : lua_toboolean(L, 1))); @@ -171,9 +255,20 @@ static int mk_conj_hyp_tactic(lua_State * L) { return push_tactic(L, conj_hyp_tactic(nargs == 0 ? true : lua_toboolean(L, 1))); } +static int mk_disj_hyp_tactic(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) + return push_tactic(L, disj_hyp_tactic()); + else if (nargs == 1) + return push_tactic(L, disj_hyp_tactic(to_name_ext(L, 1))); + else + return push_tactic(L, disj_hyp_tactic(to_name_ext(L, 1), to_name_ext(L, 2))); +} + void open_boolean(lua_State * L) { SET_GLOBAL_FUN(mk_conj_tactic, "conj_tactic"); SET_GLOBAL_FUN(mk_imp_tactic, "imp_tactic"); SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic"); + SET_GLOBAL_FUN(mk_disj_hyp_tactic, "disj_hyp_tactic"); } } diff --git a/src/library/tactic/boolean.h b/src/library/tactic/boolean.h index 9bf6e2b06..2d9beb2a6 100644 --- a/src/library/tactic/boolean.h +++ b/src/library/tactic/boolean.h @@ -10,5 +10,8 @@ namespace lean { tactic conj_tactic(bool all = true); tactic conj_hyp_tactic(bool all = true); tactic imp_tactic(name const & H_name = name("H"), bool all = true); +tactic disj_hyp_tactic(name const & goal_name, name const & hyp_name); +tactic disj_hyp_tactic(name const & hyp_name); +tactic disj_hyp_tactic(); void open_boolean(lua_State * L); } diff --git a/tests/lean/tactic7.lean b/tests/lean/tactic7.lean new file mode 100644 index 000000000..cfb58d367 --- /dev/null +++ b/tests/lean/tactic7.lean @@ -0,0 +1,50 @@ +Variable Eq {A : Type U+1} (a b : A) : Bool +Infix 50 === : Eq +Axiom EqSubst {A : Type U+1} {a b : A} (P : A -> Bool) (H1 : P a) (H2 : a === b) : P b +Axiom EqRefl {A : Type U+1} (a : A) : a === a +Theorem EqSymm {A : Type U+1} {a b : A} (H : a === b) : b === a := + EqSubst (fun x, x === a) (EqRefl a) H +Theorem EqTrans {A : Type U+1} {a b c : A} (H1 : a === b) (H2 : b === c) : a === c := + EqSubst (fun x, a === x) H1 H2 +Theorem EqCongr {A B : Type U+1} (f : A -> B) {a b : A} (H : a === b) : (f a) === (f b) := + EqSubst (fun x, (f a) === (f x)) (EqRefl (f a)) H +Theorem EqCongr1 {A : Type U+1} {B : A -> Type U+1} {f g : Pi x : A, B x} (a : A) (H : f === g) : (f a) === (g a) := + EqSubst (fun h : (Pi x : A, B x), (f a) === (h a)) (EqRefl (f a)) H +Axiom ProofIrrelevance (P : Bool) (pr1 pr2 : P) : pr1 === pr2 +Axiom EqCast {A B : Type U} (H : A === B) (a : A) : B +Axiom EqCastHom {A B : Type U} {a1 a2 : A} (HAB : A === B) (H : a1 === a2) : (EqCast HAB a1) === (EqCast HAB a2) +Axiom EqCastRefl {A : Type U} (a : A) : (EqCast (EqRefl A) a) === a + +Variable Vector : (Type U) -> Nat -> (Type U) +Variable empty {A : Type U} : Vector A 0 +Variable append {A : Type U} {m n : Nat} (v1 : Vector A m) (v2 : Vector A n) : Vector A (m + n) +Axiom Plus0 (n : Nat) : (n + 0) === n +Theorem VectorPlus0 (A : Type U) (n : Nat) : (Vector A (n + 0)) === (Vector A n) := + EqSubst (fun x : Nat, (Vector A x) === (Vector A n)) + (EqRefl (Vector A n)) + (EqSymm (Plus0 n)) +Set pp::implicit true +(* Check fun (A : Type) (n : Nat), VectorPlus0 A n *) +Axiom AppendNil {A : Type} {n : Nat} (v : Vector A n) : (EqCast (VectorPlus0 A n) (append v empty)) === v + +Variable List : Type U -> Type U. +Variables A B : Type U +Axiom H1 : A === B. +Theorem LAB : (List A) === (List B) := + EqCongr List H1 +Variable l1 : List A +Variable l2 : List B +Variable H2 : (EqCast LAB l1) == l2 + + +(* +Theorem EqCastInv {A B : Type U} (H : A === B) (a : A) : (EqCast (EqSymm H) (EqCast H a)) === a := +*) + +(* +Variable ReflCast : Pi (A : Type U) (a : A) (H : Eq (Type U) A A), Eq A (Casting A A H a) a +Theorem AppEq (A : Type U) (B : A -> Type U) (a b : A) (H : Eq A a b) : (Eq (Type U) (B b) (B a)) := + EqCongr A (Type U) B b a (EqSymm A a b H) +Theorem EqCongr2 (A : Type U) (B : A -> Type U) (f : Pi x : A, B x) (a b : A) (H : Eq A a b) : Eq (B a) (f a) (Casting (B b) (B a) (AppEq A B a b H) (f a)) (f b) := + EqSubst (B a) a b (fun x : A, Eq (B a) (f a) (Casting (B x) (B a) (AppEq A B a b H) (f a)) (f x) +*) \ No newline at end of file diff --git a/tests/lean/tactic7.lean.expected.out b/tests/lean/tactic7.lean.expected.out new file mode 100644 index 000000000..99a5c5a6b --- /dev/null +++ b/tests/lean/tactic7.lean.expected.out @@ -0,0 +1,28 @@ + Set: pp::colors + Set: pp::unicode + Assumed: Eq + Assumed: EqSubst + Assumed: EqRefl + Proved: EqSymm + Proved: EqTrans + Proved: EqCongr + Proved: EqCongr1 + Assumed: ProofIrrelevance + Assumed: EqCast + Assumed: EqCastHom + Assumed: EqCastRefl + Assumed: Vector + Assumed: empty + Assumed: append + Assumed: Plus0 + Proved: VectorPlus0 + Set: lean::pp::implicit + Assumed: AppendNil + Assumed: List + Assumed: A + Assumed: B + Assumed: H1 + Proved: LAB + Assumed: l1 + Assumed: l2 + Assumed: H2