feat(library/tactic): add disj_hyp_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/tactic/boolean.cpp

@@ -156,6 +156,90 @@ tactic conj_hyp_tactic(bool all) {
         });
 }
 
+optional<proof_state> disj_hyp_tactic_core(name const & goal_name, name const & hyp_name, proof_state const & s) {
+    buffer<std::pair<name, goal>> 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<hypothesis> new_hyp_buf1;
+            buffer<hypothesis> 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<proof_state> {
+            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<proof_state> {
+            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<proof_state> {
+            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");
 }
 }

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);
 }

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)
+*)

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