From 84b54ad02785b019cc216881dd62ca4c7b0b6aaa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Nov 2015 06:43:48 -0800
Subject: [PATCH] test(tests/lean/run): disable recursor tactic and add tests
 for unit+cc

---
 tests/lean/run/blast24.lean |  2 +-
 tests/lean/run/blast25.lean |  2 +-
 tests/lean/run/blast26.lean |  2 +-
 tests/lean/run/blast27.lean | 17 +++++++++++++++++
 4 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/blast27.lean

diff --git a/tests/lean/run/blast24.lean b/tests/lean/run/blast24.lean
index 43731cb27..2c9009dcd 100644
--- a/tests/lean/run/blast24.lean
+++ b/tests/lean/run/blast24.lean
@@ -1,12 +1,12 @@
 -- Basic (propositional) forward chaining with clauses
 constants (A B C D E : Prop)
+set_option blast.recursor false
 
 definition lemma1 : A → (A ∨ B → C) → C := by blast
 definition lemma2 : B → (A ∨ B → C) → C := by blast
 definition lemma3 : A → B → (A → B ∨ C → D) → D := by blast
 definition lemma4 : A → B → (A → B ∨ C ∨ C → D) → D := by blast
 definition lemma5 : A → B → (E ∨ A ∨ E → E ∨ B ∨ C ∨ C → D) → D := by blast
-
 definition lemma6 : A → (A → B → C) → ¬ C → ¬ B := by blast
 definition lemma7 : ¬ D → B → (A → E ∨ B ∨ C ∨ C → D) → ¬ A := by blast
 definition lemma8 : ¬ D → B → (A ∨ E → E ∨ B ∨ C ∨ C → D) → ¬ (A ∨ E) := by blast
diff --git a/tests/lean/run/blast25.lean b/tests/lean/run/blast25.lean
index 0aad3e3d8..2d7e84e5e 100644
--- a/tests/lean/run/blast25.lean
+++ b/tests/lean/run/blast25.lean
@@ -1,6 +1,6 @@
 -- Basic (propositional) forward chaining with conjunctive conclusions
 constants (A B C D E : Prop)
-set_option pp.all true
+set_option blast.recursor false
 
 definition lemma1 : B → (A → (¬ B) ∧ C) → ¬ A := by blast
 definition lemma2 : ¬ B → (A → B ∧ C) → ¬ A := by blast
diff --git a/tests/lean/run/blast26.lean b/tests/lean/run/blast26.lean
index 7c1407488..06c399b60 100644
--- a/tests/lean/run/blast26.lean
+++ b/tests/lean/run/blast26.lean
@@ -1,10 +1,10 @@
 -- Basic (propositional) forward chaining with disjunctive antecedents and conjunctive conclusions
 constants (A B C D E F : Prop)
+set_option blast.recursor false
 
 definition lemma1 : B → (A ∨ E → (¬ B) ∧ C) → ¬ (A ∨ E) := by blast
 definition lemma2 : ¬ B → (A ∨ E → B ∧ C) → ¬ (A ∨ E) := by blast
 definition lemma3 : A → ¬ D → (A ∨ E → B → C ∧ D) → ¬ B := by blast
 definition lemma4 : A → ¬ E → (A → B → E ∧ F) → ¬ B := by blast
-
 definition lemma5 : (A → B) → ¬ B → ¬ A := by blast
 definition lemma6 : (A → B ∧ C) → ¬ B → ¬ A := by blast
diff --git a/tests/lean/run/blast27.lean b/tests/lean/run/blast27.lean
new file mode 100644
index 000000000..b46ec0d51
--- /dev/null
+++ b/tests/lean/run/blast27.lean
@@ -0,0 +1,17 @@
+-- Basic (propositional) forward chaining with conjunctive conclusions
+constants (a b c d e : nat)
+constants (p : nat → Prop)
+constants (q : nat → nat → Prop)
+constants (f : nat → nat)
+set_option blast.recursor false
+set_option blast.subst    false
+
+definition lemma1  : a = d → b = e → p b → (p a → (¬ p e) ∧ p c) → ¬ p d := by blast
+definition lemma2a : ¬ p b → (p d → p b ∧ p c) → d = e → e = a → ¬ p a := by blast
+definition lemma2b : ¬ p (f b) → (p (f a) → p (f d) ∧ p (f c)) → b = d → ¬ p (f a) := by blast
+definition lemma3  : p (f (f b)) → (p (f a) → p (f c) ∧ (¬ p (f (f (f (f b)))))) → b = f b → ¬ p (f a) := by blast
+definition lemma4a : b = f b → ¬ p (f (f b)) → (p a → q c c ∧ p (f (f (f (f (f b)))))) → ¬ p a := by blast
+definition lemma4b : b = f b → ¬ p (f (f b)) → (p a → q c c ∧ q e c ∧ q d e ∧ p (f (f (f (f (f b))))) ∧ q e d) → ¬ p a :=
+by blast
+definition lemma5 : p b → (p (f a) → (¬ p b) ∧ p e ∧ p c) → ¬ p (f a) := by blast
+definition lemma6 : ¬ (q b a) → d = a → (p a → p e ∧ (q b d) ∧ p c) → ¬ p a := by blast