From ac9d6c2021ba66725ecda8f6d6c77cb4488d43a3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Jan 2016 13:52:42 -0800
Subject: [PATCH] refactor(library/data/bool): cleanup bool proofs and fix bxor
 definition

---
 library/data/bool.lean                        | 127 ++++++++++--------
 .../blast/recursor/recursor_strategy.cpp      |   2 +-
 src/library/blast/strategies/portfolio.cpp    |   9 +-
 .../lean/interactive/alias.input.expected.out |  10 ++
 4 files changed, 91 insertions(+), 57 deletions(-)

diff --git a/library/data/bool.lean b/library/data/bool.lean
index 924be9440..6a1e42211 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -3,16 +3,14 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-
 import logic.eq
-open eq eq.ops decidable
 
 namespace bool
   local attribute bor [reducible]
   local attribute band [reducible]
 
   theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
-  bool.cases_on b (or.inl rfl) (or.inr rfl)
+  by rec_simp
 
   theorem cond_ff [simp] {A : Type} (t e : A) : cond ff t e = e :=
   rfl
@@ -20,16 +18,14 @@ namespace bool
   theorem cond_tt [simp] {A : Type} (t e : A) : cond tt t e = t :=
   rfl
 
-  theorem eq_tt_of_ne_ff : ∀ {a : bool}, a ≠ ff → a = tt
-  | @eq_tt_of_ne_ff tt H := rfl
-  | @eq_tt_of_ne_ff ff H := absurd rfl H
+  theorem eq_tt_of_ne_ff : ∀ {a : bool}, a ≠ ff → a = tt :=
+  by rec_simp
 
-  theorem eq_ff_of_ne_tt : ∀ {a : bool}, a ≠ tt → a = ff
-  | @eq_ff_of_ne_tt tt H := absurd rfl H
-  | @eq_ff_of_ne_tt ff H := rfl
+  theorem eq_ff_of_ne_tt : ∀ {a : bool}, a ≠ tt → a = ff :=
+  by rec_simp
 
   theorem absurd_of_eq_ff_of_eq_tt {B : Prop} {a : bool} (H₁ : a = ff) (H₂ : a = tt) : B :=
-  absurd (H₁⁻¹ ⬝ H₂) ff_ne_tt
+  by rec_simp
 
   theorem tt_bor [simp] (a : bool) : bor tt a = tt :=
   rfl
@@ -37,80 +33,67 @@ namespace bool
   notation a || b := bor a b
 
   theorem bor_tt [simp] (a : bool) : a || tt = tt :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
   theorem ff_bor [simp] (a : bool) : ff || a = a :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
   theorem bor_ff [simp] (a : bool) : a || ff = a :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
   theorem bor_self [simp] (a : bool) : a || a = a :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
-  theorem bor.comm [simp] (a b : bool) : a || b = b || a :=
-  by cases a; repeat (cases b | reflexivity)
+  theorem bor_comm [simp] (a b : bool) : a || b = b || a :=
+  by rec_simp
 
-  theorem bor.assoc [simp] (a b c : bool) : (a || b) || c = a || (b || c) :=
-  match a with
-  | ff := by rewrite *ff_bor
-  | tt := by rewrite *tt_bor
-  end
+  theorem bor_assoc [simp] (a b c : bool) : (a || b) || c = a || (b || c) :=
+  by rec_simp
+
+  theorem bor_left_comm [simp] (a b c : bool) : a || (b || c) = b || (a || c) :=
+  by rec_simp
 
   theorem or_of_bor_eq {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
-  bool.rec_on a
-    (suppose ff || b = tt,
-      have b = tt, from !ff_bor ▸ this,
-      or.inr this)
-    (suppose tt || b = tt,
-      or.inl rfl)
+  by rec_simp
 
   theorem bor_inl {a b : bool} (H : a = tt) : a || b = tt :=
-  by rewrite H
+  by rec_simp
 
   theorem bor_inr {a b : bool} (H : b = tt) : a || b = tt :=
-  bool.rec_on a (by rewrite H) (by rewrite H)
+  by rec_simp
 
   theorem ff_band [simp] (a : bool) : ff && a = ff :=
   rfl
 
   theorem tt_band [simp] (a : bool) : tt && a = a :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
   theorem band_ff [simp] (a : bool) : a && ff = ff :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
   theorem band_tt [simp] (a : bool) : a && tt = a :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
   theorem band_self [simp] (a : bool) : a && a = a :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
-  theorem band.comm [simp] (a b : bool) : a && b = b && a :=
-  bool.cases_on a
-    (bool.cases_on b rfl rfl)
-    (bool.cases_on b rfl rfl)
+  theorem band_comm [simp] (a b : bool) : a && b = b && a :=
+  by rec_simp
 
-  theorem band.assoc [simp] (a b c : bool) : (a && b) && c = a && (b && c) :=
-  match a with
-  | ff := by rewrite *ff_band
-  | tt := by rewrite *tt_band
-  end
+  theorem band_assoc [simp] (a b c : bool) : (a && b) && c = a && (b && c) :=
+  by rec_simp
+
+  theorem band_left_comm [simp] (a b c : bool) : a && (b && c) = b && (a && c) :=
+  by rec_simp
 
   theorem band_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
-  or.elim (dichotomy a)
-    (suppose a = ff,
-      absurd (by inst_simp) ff_ne_tt)
-    (suppose a = tt, this)
+  by rec_simp
 
   theorem band_intro {a b : bool} (H₁ : a = tt) (H₂ : b = tt) : a && b = tt :=
-  by rewrite [H₁, H₂]
+  by rec_simp
 
   theorem band_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
-  band_elim_left (!band.comm ⬝ H)
-
-  theorem bnot_bnot [simp] (a : bool) : bnot (bnot a) = a :=
-  bool.cases_on a rfl rfl
+  by rec_simp
 
   theorem bnot_false [simp] : bnot ff = tt :=
   rfl
@@ -118,11 +101,47 @@ namespace bool
   theorem bnot_true [simp] : bnot tt = ff :=
   rfl
 
+  theorem bnot_bnot [simp] (a : bool) : bnot (bnot a) = a :=
+  by rec_simp
+
   theorem eq_tt_of_bnot_eq_ff {a : bool} : bnot a = ff → a = tt :=
-  bool.cases_on a (by contradiction) (λ h, rfl)
+  by rec_simp
 
   theorem eq_ff_of_bnot_eq_tt {a : bool} : bnot a = tt → a = ff :=
-  bool.cases_on a (λ h, rfl) (by contradiction)
+  by rec_simp
 
-  definition bxor (x:bool) (y:bool) := cond x (bnot y) y
+  definition bxor : bool → bool → bool
+  | ff ff := ff
+  | ff tt := tt
+  | tt ff := tt
+  | tt tt := ff
+
+  lemma ff_bxor_ff [simp] : bxor ff ff = ff := rfl
+  lemma ff_bxor_tt [simp] : bxor ff tt = tt := rfl
+  lemma tt_bxor_ff [simp] : bxor tt ff = tt := rfl
+  lemma tt_bxor_tt [simp] : bxor tt tt = ff := rfl
+
+  lemma bxor_self [simp] (a : bool) : bxor a a = ff :=
+  by rec_simp
+
+  lemma bxor_ff [simp] (a : bool) : bxor a ff = a :=
+  by rec_simp
+
+  lemma bxor_tt [simp] (a : bool) : bxor a tt = bnot a :=
+  by rec_simp
+
+  lemma ff_bxor [simp] (a : bool) : bxor ff a = a :=
+  by rec_simp
+
+  lemma tt_bxor [simp] (a : bool) : bxor tt a = bnot a :=
+  by rec_simp
+
+  lemma bxor_comm [simp] (a b : bool) : bxor a b = bxor b a :=
+  by rec_simp
+
+  lemma bxor_assoc [simp] (a b c : bool) : bxor (bxor a b) c = bxor a (bxor b c) :=
+  by rec_simp
+
+  lemma bxor_left_comm [simp] (a b c : bool) : bxor a (bxor b c) = bxor b (bxor a c) :=
+  by rec_simp
 end bool
diff --git a/src/library/blast/recursor/recursor_strategy.cpp b/src/library/blast/recursor/recursor_strategy.cpp
index 2352462c5..dd0940a35 100644
--- a/src/library/blast/recursor/recursor_strategy.cpp
+++ b/src/library/blast/recursor/recursor_strategy.cpp
@@ -146,7 +146,7 @@ strategy rec_and_then(strategy const & S, rec_candidate_selector const & selecto
     return [=]() { // NOLINT
         state s = curr_state();
         unsigned max_rounds = get_blast_recursion_max_rounds(ios().get_options());
-        for (unsigned i = 1; i <= max_rounds; i++) {
+        for (unsigned i = 0; i <= max_rounds; i++) {
             lean_trace_search(tout() << "starting recursor strategy with max #" << i << " round(s)\n";);
             curr_state() = s;
             if (auto pr = rec_strategy_fn(S, selector, i)())
diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp
index 792c4b92e..2eb333127 100644
--- a/src/library/blast/strategies/portfolio.cpp
+++ b/src/library/blast/strategies/portfolio.cpp
@@ -7,9 +7,10 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/sstream.h"
 #include "library/blast/actions/assert_cc_action.h"
-#include "library/blast/simplifier/simplifier_strategies.h"
+#include "library/blast/actions/no_confusion_action.h"
 #include "library/blast/unit/unit_actions.h"
 #include "library/blast/forward/ematch.h"
+#include "library/blast/simplifier/simplifier_strategies.h"
 #include "library/blast/recursor/recursor_strategy.h"
 #include "library/blast/backward/backward_action.h"
 #include "library/blast/backward/backward_strategy.h"
@@ -54,7 +55,11 @@ static optional<expr> apply_ematch() {
 static optional<expr> apply_ematch_simp() {
     flet<bool> set(get_config().m_ematch, true);
     return mk_action_strategy("ematch_simp",
-                              assert_cc_action,
+                              [](hypothesis_idx hidx) {
+                                  Try(no_confusion_action(hidx));
+                                  TrySolve(assert_cc_action(hidx));
+                                  return action_result::new_branch();
+                              },
                               unit_propagate,
                               ematch_simp_action)();
 }
diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out
index b7ab8cbea..f1ca174f2 100644
--- a/tests/lean/interactive/alias.input.expected.out
+++ b/tests/lean/interactive/alias.input.expected.out
@@ -3,11 +3,15 @@
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINFINDP
+bool.tt_bxor_tt|eq (bool.bxor bool.tt bool.tt) bool.ff
+bool.tt_bxor_ff|eq (bool.bxor bool.tt bool.ff) bool.tt
 bool.bor_tt|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt
 bool.band_tt|∀ (a : bool), eq (bool.band a bool.tt) a
 bool.tt|bool
+bool.bxor_tt|∀ (a : bool), eq (bool.bxor a bool.tt) (bool.bnot a)
 bool.eq_tt_of_bnot_eq_ff|eq (bool.bnot ?a) bool.ff → eq ?a bool.tt
 bool.eq_ff_of_bnot_eq_tt|eq (bool.bnot ?a) bool.tt → eq ?a bool.ff
+bool.ff_bxor_tt|eq (bool.bxor bool.ff bool.tt) bool.tt
 bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B
 bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt
 tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
@@ -15,6 +19,7 @@ bool.tt_band|∀ (a : bool), eq (bool.band bool.tt a) a
 bool.cond_tt|∀ (t e : ?A), eq (bool.cond bool.tt t e) t
 bool.ff_ne_tt|eq bool.ff bool.tt → false
 bool.eq_ff_of_ne_tt|ne ?a bool.tt → eq ?a bool.ff
+bool.tt_bxor|∀ (a : bool), eq (bool.bxor bool.tt a) (bool.bnot a)
 bool.tt_bor|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt
 -- ENDFINDP
 -- BEGINWAIT
@@ -23,10 +28,15 @@ bool.tt_bor|∀ (a : bool), eq (bool.bor bool.tt a) bool.tt
 tt|bool
 tt_bor|∀ (a : bool), eq (bor tt a) tt
 tt_band|∀ (a : bool), eq (band tt a) a
+tt_bxor|∀ (a : bool), eq (bxor tt a) (bnot a)
+tt_bxor_tt|eq (bxor tt tt) ff
+tt_bxor_ff|eq (bxor tt ff) tt
 bor_tt|∀ (a : bool), eq (bor a tt) tt
 band_tt|∀ (a : bool), eq (band a tt) a
+bxor_tt|∀ (a : bool), eq (bxor a tt) (bnot a)
 eq_tt_of_bnot_eq_ff|eq (bnot ?a) ff → eq ?a tt
 eq_ff_of_bnot_eq_tt|eq (bnot ?a) tt → eq ?a ff
+ff_bxor_tt|eq (bxor ff tt) tt
 absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B
 eq_tt_of_ne_ff|ne ?a ff → eq ?a tt
 tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic