max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean): erase old blast tests

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-11 16:18:20 -07:00
parent 083bbdb382
commit f003bd8df8
104 changed files with 0 additions and 1930 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
tests/lean/blast_back2.lean
View file

@ -1,26 +0,0 @@
exit
constant r : nat → Prop
constant s : nat → Prop
constant p : nat → Prop
definition q (a : nat) := p a
lemma rq₁ [intro] [priority 20] : ∀ a, r a → q a :=
sorry
lemma rq₂ [intro] [priority 10] : ∀ a, s a → q a :=
sorry
attribute q [reducible]
definition lemma1 (a : nat) : r a → s a → p a :=
by blast
print lemma1
attribute rq₂ [intro] [priority 30]
definition lemma2 (a : nat) : r a → s a → p a :=
by blast
print lemma2

1
tests/lean/blast_back2.lean.expected.out
View file

@ -1 +0,0 @@
blast_back2.lean:1:0: warning: using 'exit' to interrupt Lean

6
tests/lean/blast_cc_not_provable.lean
View file

@ -1,6 +0,0 @@
exit
set_option blast.strategy "cc"
example (C : nat → Type) (f : Π n, C n → C n) (n m : nat) (c : C n) (d : C m) :
f n == f m → c == d → f n c == f m d :=
by blast

1
tests/lean/blast_cc_not_provable.lean.expected.out
View file

@ -1 +0,0 @@
blast_cc_not_provable.lean:1:0: warning: using 'exit' to interrupt Lean

12
tests/lean/run/abstract_notation.lean
View file

@ -1,12 +0,0 @@
exit
import data.nat
open nat
notation `$`:max := abstract by blast end
definition foo (a b : nat) : a + b = b + a ∧ a = 0 + a :=
and.intro $ $
check foo_1
check foo_2
print foo

6
tests/lean/run/blast1.lean
View file

@ -1,6 +0,0 @@
exit
set_option blast.strategy "preprocess"
example (a b : Prop) (Ha : a) (Hb : b) : a :=
by blast

15
tests/lean/run/blast10.lean
View file

@ -1,15 +0,0 @@
exit
import data.list
set_option blast.strategy "unit"
definition lemma1 : true :=
by blast
open perm
definition lemma2 (l : list nat) : l ~ l :=
by blast
print lemma1
print lemma2

14
tests/lean/run/blast11.lean
View file

@ -1,14 +0,0 @@
exit
import data.nat
open algebra nat
definition lemma1 (a b : nat) : a + b + 0 = b + a :=
by simp
print lemma1
definition lemma2 (a b c : nat) : a + b + 0 + c + a + a + b = 0 + 0 + c + a + b + a + a + b :=
by simp
print lemma2

7
tests/lean/run/blast12.lean
View file

@ -1,7 +0,0 @@
exit
import data.nat
open nat
example (a b : nat) : 0 + a + b + 1 = 1 + a + b :=
by simp

17
tests/lean/run/blast13.lean
View file

@ -1,17 +0,0 @@
exit
import data.list
open perm
set_option blast.strategy "cc"
example (p : Prop) (l : list nat) : ¬ l ~ l → p :=
by blast
example (a : nat) : ¬ a = a → false :=
by blast
example (A : Type) (p : Prop) (a b c : A) : a = b → ¬ b = a → p :=
by blast
example (A : Type) (p : Prop) (a b c : A) : a = b → b ≠ a → p :=
by blast

15
tests/lean/run/blast14.lean
View file

@ -1,15 +0,0 @@
exit
set_option blast.init_depth 10
set_option blast.inc_depth 1000
definition lemma1 (p q : Prop) : p ∧ q → q ∧ p :=
by blast
definition lemma2 (p q r s : Prop) : r ∧ s → p ∧ q → q ∧ p :=
by blast
print lemma2 -- unnecessary and.rec's are not included
example (p q : Prop) : p ∧ p ∧ q ∧ q → q ∧ p :=
by blast

6
tests/lean/run/blast15.lean
View file

@ -1,6 +0,0 @@
exit
definition lemma1 (p : nat → Prop) (q : nat → nat → Prop) : (∃ x y, p x ∧ q x y) → q 0 0 ∧ q 1 1 → (∃ x, p x) :=
by blast
print lemma1

11
tests/lean/run/blast16.lean
View file

@ -1,11 +0,0 @@
exit
set_option trace.blast true
example (p q : Prop) : p ∨ q → q ∨ p :=
by blast
definition lemma1 (p q r s : Prop) (a b : nat) : r ∨ s → p ∨ q → a = b → q ∨ p :=
by blast
print lemma1

6
tests/lean/run/blast17.lean
View file

@ -1,6 +0,0 @@
exit
set_option blast.strategy "preprocess"
example (p q r : Prop) (a b : nat) : true → a = a → q → q → p → p :=
by blast

8
tests/lean/run/blast2.lean
View file

@ -1,8 +0,0 @@
exit
set_option blast.strategy "preprocess"
example (a b : Prop) : forall (Ha : a) (Hb : b), a :=
by blast
example (a b : Prop) : a → b → a :=
by blast

57
tests/lean/run/blast20.lean
View file

@ -1,57 +0,0 @@
exit
open nat
example : ∀ (P Q : nat → Prop), (∀n, Q n → P n) → (∀n, Q n) → P 2 :=
by blast
example : ∀ (P Q : nat → Prop), (∀n m, Q m → P n) → Q 1 → P 2 :=
by blast
example : ∀ (P : nat → Prop) (F : Prop), (∀n, P n) → F → F ∧ P 2 :=
by blast
example : ∀ (F F' : Prop), F ∧ F' → F :=
by blast
attribute and.intro [intro]
example : ∀ (P Q R : nat → Prop) (F : Prop), (F ∧ (∀ n m, (Q m ∧ R n) → P n)) →
(F → R 2) → Q 1 → P 2 ∧ F :=
by blast
-- We should get the following one with simplification and/or heuristic instantiation
-- example : ∀ (P Q : nat → Prop), (∀n, P n ∧ Q n) → P 2 :=
-- by blast
example : ∀ (P Q : nat → Prop) (F : Prop), (∀n, P n) ∧ (∀n, Q n) → P 2 :=
by blast
example : ∀ (F F' : Prop), F → F ∨ F' :=
by blast
example : ∀ (F F' : Prop), F ∨ F' → F' ∨ F :=
by blast
example : ∀ (F1 F2 F3 : Prop), ((¬F1 ∧ F3) ∨ (F2 ∧ ¬F3)) → (F2 → F1) → (F2 → F3) → ¬F2 :=
by blast
example : ∀ (f : nat→Prop), f 2 → ∃x, f x :=
by blast
example : ∀ (f g : nat → Prop), (∀x, f x → g x) → (∃a, f a) → (∃a, g a) :=
by blast
-- We need heuristic inst for the following one
-- example : ∀ (P : nat → Prop), P 0 → (∀x, ¬ P x) → false :=
-- by blast
-- We need heuristic inst for the following one
-- example : ∀ (f g : nat → Prop), (∀x, f x = g x) → g 2 = f 2 :=
-- by blast
example : true ∧ true ∧ true ∧ true ∧ true ∧ true ∧ true :=
by blast
example : ∀ (P : nat → Prop), P 0 → (P 0 → P 1) → (P 1 → P 2) → (P 2) :=
by blast

37
tests/lean/run/blast3.lean
View file

@ -1,37 +0,0 @@
exit
-- TODO(Leo): use better strategy
set_option blast.strategy "constructor"
example (a b c : Prop) : b → c → b ∧ c :=
by blast
example (a b c : Prop) : b → c → c ∧ b :=
by blast
example (a b : Prop) : a → a ∨ b :=
by blast
example (a b : Prop) : b → a ∨ b :=
by blast
example (a b : Prop) : b → a ∨ a ∨ b :=
by blast
example (a b c : Prop) : b → c → a ∨ a ∨ (b ∧ c) :=
by blast
example (p q : nat → Prop) (a b : nat) : p a → q b → ∃ x, p x :=
by blast
example {A : Type} (p q : A → Prop) (a b : A) : q a → p b → ∃ x, p x :=
by blast
lemma foo₁ {A : Type} (p q : A → Prop) (a b : A) : q a → p b → ∃ x, (p x ∧ x = b) ∨ q x :=
by blast
lemma foo₂ {A : Type} (p q : A → Prop) (a b : A) : p b → ∃ x, q x ∨ (p x ∧ x = b) :=
by blast
reveal foo₁ foo₂
print foo₁
print foo₂

20
tests/lean/run/blast4.lean
View file

@ -1,20 +0,0 @@
exit
set_option blast.strategy "preprocess"
lemma T1 (a b : Prop) : false → a :=
by blast
reveal T1
print T1
lemma T2 (a b c : Prop) : ¬ a → b → a → c :=
by blast
reveal T2
print T2
example (a b c : Prop) : a → b → ¬ a → c :=
by blast
example (a b c : Prop) : a → b → b → ¬ a → c :=
by blast

11
tests/lean/run/blast5.lean
View file

@ -1,11 +0,0 @@
exit
set_option blast.strategy "preprocess"
example (a b : nat) : a = b → b = a :=
by blast
example (a b c : nat) : a = b → a = c → b = c :=
by blast
example (p : nat → Prop) (a b c : nat) : a = b → a = c → p b → p c :=
by blast

8
tests/lean/run/blast6.lean
View file

@ -1,8 +0,0 @@
exit
set_option blast.strategy "preprocess"
lemma lemma1 (bv : nat → Type) (n m : nat) (H : n = m) (b1 : bv n) (b2 : bv m) (H2 : eq.rec_on H b1 = b2) : b1 = eq.rec_on (eq.symm H) b2 :=
by blast
reveal lemma1
print lemma1

8
tests/lean/run/blast7.lean
View file

@ -1,8 +0,0 @@
exit
set_option blast.strategy "preprocess"
lemma lemma1 (p : Prop) (a b : nat) : a = b → p → p :=
by blast
reveal lemma1
print lemma1

23
tests/lean/run/blast8.lean
View file

@ -1,23 +0,0 @@
exit
open nat
set_option blast.strategy "preprocess"
lemma l1 (a : nat) : zero = succ a → a = a → false :=
by blast
lemma l2 (p : Prop) (a : nat) : zero = succ a → a = a → p :=
by blast
lemma l3 (a b : nat) : succ (succ a) = succ (succ b) → a = b :=
by blast
lemma l4 (a b : nat) : succ a = succ b → a = b :=
by blast
lemma l5 (a b c : nat) : succ (succ a) = succ (succ b) → c = c :=
by blast
reveal l3 l4 l5
print l3
print l4
print l5

15
tests/lean/run/blast9.lean
View file

@ -1,15 +0,0 @@
exit
import data.list
open list
set_option blast.strategy "preprocess"
example (p : Prop) (a b c : nat) : [a, b, c] = [] → p :=
by blast
set_option blast.strategy "simple"
lemma l1 (a b c d e f : nat) : [a, b, c] = [d, e, f] → a = d ∧ b = e ∧ c = f :=
by blast
reveal l1
print l1

13
tests/lean/run/blast_back1.lean
View file

@ -1,13 +0,0 @@
exit
constant r : nat → Prop
constant p : nat → Prop
definition q (a : nat) := p a
lemma rq [intro] : ∀ a, r a → q a :=
sorry
attribute q [reducible]
example (a : nat) : r a → p a :=
by blast

7
tests/lean/run/blast_backward_action_missing_normalize.lean
View file

@ -1,7 +0,0 @@
exit
constants (P : ℕ → Prop) (R : Prop)
lemma foo [intro!] : (: P 0 :) → R := sorry
constants (P0 : P 0)
attribute P0 [intro!]
example : R :=
by grind -- fails

17
tests/lean/run/blast_by_contradiction.lean
View file

@ -1,17 +0,0 @@
exit
constants P Q : Prop
namespace with_classical
local attribute classical.prop_decidable [instance]
example : Q → (Q → ¬ P → false) → P := by blast
example : Q → (Q → P → false) → ¬ P := by blast
end with_classical
namespace with_decidable
constant P_dec : decidable P
attribute P_dec [instance]
definition foo : Q → (Q → ¬ P → false) → P := by blast
example : Q → (Q → P → false) → ¬ P := by blast
end with_decidable

25
tests/lean/run/blast_cc1.lean
View file

@ -1,25 +0,0 @@
exit
import data.list
constant f {A : Type} : A → A → A
constant g : nat → nat
set_option blast.strategy "cc"
example (a b c : nat) : a = b → g a == g b :=
by blast
example (a b c : nat) : a = b → c = b → f (f a b) (g c) = f (f c a) (g b) :=
by blast
example (a b c d e x y : nat) : a = b → a = x → b = y → c = d → c = e → c = b → a = e :=
by blast
open perm
example (a b c d : list nat) : a ~ b → c ~ b → d ~ c → a ~ d :=
by blast
set_option trace.cc true
example (a b c d : list nat) : a ~ b → c ~ b → d = c → a ~ d :=
by blast

7
tests/lean/run/blast_cc10.lean
View file

@ -1,7 +0,0 @@
exit
set_option blast.strategy "cc"
definition t1 (a b : nat) : (a = b ↔ a = b) :=
by blast
print t1

44
tests/lean/run/blast_cc11.lean
View file

@ -1,44 +0,0 @@
exit
import data.list
set_option blast.strategy "cc"
definition t1 (a b : nat) : (a = b) ↔ (b = a) :=
by blast
print t1
definition t2 (a b : nat) : (a = b) = (b = a) :=
by blast
print t2
definition t3 (a b : nat) : (a = b) == (b = a) :=
by blast
print t3
open perm
definition t4 (a b : list nat) : (a ~ b) ↔ (b ~ a) :=
by blast
definition t5 (a b : list nat) : (a ~ b) = (b ~ a) :=
by blast
definition t6 (a b : list nat) : (a ~ b) == (b ~ a) :=
by blast
definition t7 (p : Prop) (a b : nat) : a = b → b ≠ a → p :=
by blast
definition t8 (a b : Prop) : (a ↔ b) → ((b ↔ a) ↔ (a ↔ b)) :=
by blast
definition t9 (a b c : nat) : b = c → (a = b ↔ c = a) :=
by blast
definition t10 (a b c : list nat) : b ~ c → (a ~ b ↔ c ~ a) :=
by blast
definition t11 (a b c : list nat) : b ~ c → ((a ~ b) = (c ~ a)) :=
by blast

29
tests/lean/run/blast_cc12.lean
View file

@ -1,29 +0,0 @@
exit
set_option blast.strategy "simple"
definition foo1 (a b : nat) (p : Prop) : a = b → (b = a → p) → p :=
by blast
print foo1
definition foo2 (a b c : nat) (p : Prop) : a = b → b = c → (c = a → p) → p :=
by blast
print foo2
definition foo3 (a b c d : nat) (p : Prop) : a ≠ d → (d ≠ a → p) → p :=
by blast
print foo3
attribute not [reducible]
definition foo4 (a b c d : nat) (p : Prop) : a ≠ d → (d ≠ a → p) → p :=
by blast
attribute ne [semireducible]
definition foo5 (a b c d : nat) (p : Prop) : a ≠ d → (d ≠ a → p) → p :=
by blast
print foo5

18
tests/lean/run/blast_cc13.lean
View file

@ -1,18 +0,0 @@
exit
set_option blast.strategy "cc"
example (p : nat → nat → Prop) (f : nat → nat) (a b c d : nat) :
p (f a) (f b) → a = c → b = d → b = c → p (f c) (f c) :=
by blast
example (p : nat → nat → Prop) (a b c d : nat) :
p a b → a = c → b = d → p c d :=
by blast
example (p : nat → nat → Prop) (f : nat → nat) (a b c d : nat) :
p (f (f (f (f (f (f a))))))
(f (f (f (f (f (f b)))))) →
a = c → b = d → b = c →
p (f (f (f (f (f (f c))))))
(f (f (f (f (f (f c)))))) :=
by blast

11
tests/lean/run/blast_cc14.lean
View file

@ -1,11 +0,0 @@
exit
set_option blast.strategy "cc"
constant R : nat → nat → Prop
axiom R_trans : ∀ a b c, R a b → R b c → R a c
attribute R_trans [trans]
set_option blast.subst false
example (a b c : nat) : a = b → R a b → R a a :=
by blast

23
tests/lean/run/blast_cc2.lean
View file

@ -1,23 +0,0 @@
exit
set_option blast.strategy "cc"
example (a b c d : nat) : a == b → b = c → c == d → a == d :=
by blast
example (a b c d : nat) : a = b → b = c → c == d → a == d :=
by blast
example (a b c d : nat) : a = b → b == c → c == d → a == d :=
by blast
example (a b c d : nat) : a == b → b == c → c = d → a == d :=
by blast
example (a b c d : nat) : a == b → b = c → c = d → a == d :=
by blast
example (a b c d : nat) : a = b → b = c → c = d → a == d :=
by blast
example (a b c d : nat) : a = b → b == c → c = d → a == d :=
by blast

17
tests/lean/run/blast_cc3.lean
View file

@ -1,17 +0,0 @@
exit
open nat
set_option blast.strategy "cc"
constant f (a b : nat) : a > b → nat
constant g : nat → nat
definition tst
(a₁ a₂ b₁ b₂ c d : nat)
(H₁ : a₁ > b₁)
(H₂ : a₂ > b₂) :
a₁ = c → a₂ = c →
b₁ = d → d = b₂ →
g (g (f a₁ b₁ H₁)) = g (g (f a₂ b₂ H₂)) :=
by blast
print tst

12
tests/lean/run/blast_cc4.lean
View file

@ -1,12 +0,0 @@
exit
open nat
set_option blast.strategy "cc"
definition tst
(a₁ a₂ b₁ b₂ c d : nat) :
a₁ = c → a₂ = c →
b₁ = d → d = b₂ →
a₁ + b₁ + a₁ = a₂ + b₂ + c :=
by blast
print tst

18
tests/lean/run/blast_cc5.lean
View file

@ -1,18 +0,0 @@
exit
set_option blast.strategy "cc"
example (a b c : Prop) : (a ↔ b) → ((a ∧ (c ∨ b)) ↔ (b ∧ (c ∨ a))) :=
by blast
/-
example (a b c : Prop) : (a ↔ b) → ((a ∧ (c ∨ (b ↔ a))) ↔ (b ∧ (c ∨ (a ↔ b)))) :=
by blast
example (a₁ a₂ b₁ b₂ : Prop) : (a₁ ↔ b₁) → (a₂ ↔ b₂) → (a₁ ∧ a₂ ∧ a₁ ∧ a₂ ↔ b₁ ∧ b₂ ∧ b₁ ∧ b₂) :=
by blast
definition lemma1 (a₁ a₂ b₁ b₂ : Prop) : (a₁ = b₁) → (a₂ ↔ b₂) → (a₁ ∧ a₂ ∧ a₁ ∧ a₂ ↔ b₁ ∧ b₂ ∧ b₁ ∧ b₂) :=
by blast
print lemma1
-/

16
tests/lean/run/blast_cc6.lean
View file

@ -1,16 +0,0 @@
exit
import data.list
set_option blast.strategy "cc"
open perm list
definition tst₁
(A : Type) (l₁ l₂ l₃ l₄ l₅ : list A) :
(l₁ ~ l₂) → (l₃ ~ l₄) → (l₁ ++ l₃ ++ l₅ ++ l₄ ++ l₁) ~ (l₂ ++ l₄ ++ l₅ ++ l₃ ++ l₂) :=
by blast
print tst₁
definition tst₂
(A : Type) (l₁ l₂ l₃ l₄ l₅ : list A) :
(l₁ ~ l₂) → (l₃ = l₄) → (l₁ ++ l₃ ++ l₅ ++ l₄ ++ l₁) ~ (l₂ ++ l₄ ++ l₅ ++ l₃ ++ l₂) :=
by blast

12
tests/lean/run/blast_cc7.lean
View file

@ -1,12 +0,0 @@
exit
set_option blast.strategy "cc"
example (a b c d : Prop)
[d₁ : decidable a] [d₂ : decidable b] [d₃ : decidable c] [d₄ : decidable d]
: (a ↔ b) → (c ↔ d) → ((if (a ∧ c) then true else false) ↔ (if (b ∧ d) then true else false)) :=
by blast
example (a b c d : Prop) (x y z : nat)
[d₁ : decidable a] [d₂ : decidable b] [d₃ : decidable c] [d₄ : decidable d]
: (a ↔ b) → (c ↔ d) → x = y → ((if (a ∧ c ∧ a) then x else y) = (if (b ∧ d ∧ b) then y else x)) :=
by blast

16
tests/lean/run/blast_cc9.lean
View file

@ -1,16 +0,0 @@
exit
import data.list
open perm
set_option blast.strategy "cc"
example (a b : nat) : a = b → (b = a ↔ true) :=
by blast
example (a b c : nat) : a = b → b = c → (true ↔ a = c) :=
by blast
example (l₁ l₂ l₃ : list nat) : l₁ ~ l₂ → l₂ ~ l₃ → (true ↔ l₁ ~ l₃) :=
by blast
example (l₁ l₂ l₃ : list nat) : l₁ ~ l₂ → l₂ = l₃ → (true ↔ l₁ ~ l₃) :=
by blast

33
tests/lean/run/blast_cc_heq1.lean
View file

@ -1,33 +0,0 @@
exit
set_option blast.strategy "cc"
set_option blast.cc.heq true -- make sure heterogeneous congruence lemmas are enabled
example (a b c : Prop) : a = b → b = c → (a ↔ c) :=
by blast
example (a b c : Prop) : a = b → b == c → (a ↔ c) :=
by blast
example (a b c : nat) : a == b → b = c → a == c :=
by blast
example (a b c : nat) : a == b → b = c → a = c :=
by blast
example (a b c d : nat) : a == b → b == c → c == d → a = d :=
by blast
example (a b c d : nat) : a == b → b = c → c == d → a = d :=
by blast
example (a b c : Prop) : a = b → b = c → (a ↔ c) :=
by blast
example (a b c : Prop) : a == b → b = c → (a ↔ c) :=
by blast
example (a b c d : Prop) : a == b → b == c → c == d → (a ↔ d) :=
by blast
definition foo (a b c d : Prop) : a == b → b = c → c == d → (a ↔ d) :=
by blast

12
tests/lean/run/blast_cc_heq2.lean
View file

@ -1,12 +0,0 @@
exit
set_option blast.strategy "cc"
set_option blast.cc.heq true -- make sure heterogeneous congruence lemmas are enabled
example (a b c : nat) (f : nat → nat) : a == b → b = c → f a == f c :=
by blast
example (a b c : nat) (f : nat → nat) : a == b → b = c → f a = f c :=
by blast
example (a b c d : nat) (f : nat → nat) : a == b → b = c → c == f d → f a = f (f d) :=
by blast

18
tests/lean/run/blast_cc_heq3.lean
View file

@ -1,18 +0,0 @@
exit
set_option blast.strategy "cc"
set_option blast.cc.heq true -- make sure heterogeneous congruence lemmas are enabled
axiom vector.{l} : Type.{l} → nat → Type.{l}
axiom app : Π {A : Type} {n m : nat}, vector A m → vector A n → vector A (m+n)
example (n1 n2 n3 : nat) (v1 w1 : vector nat n1) (w1' : vector nat n3) (v2 w2 : vector nat n2) :
n1 = n3 → v1 = w1 → w1 == w1' → v2 = w2 → app v1 v2 == app w1' w2 :=
by blast
example (n1 n2 n3 : nat) (v1 w1 : vector nat n1) (w1' : vector nat n3) (v2 w2 : vector nat n2) :
n1 == n3 → v1 = w1 → w1 == w1' → v2 == w2 → app v1 v2 == app w1' w2 :=
by blast
example (n1 n2 n3 : nat) (v1 w1 v : vector nat n1) (w1' : vector nat n3) (v2 w2 w : vector nat n2) :
n1 == n3 → v1 = w1 → w1 == w1' → v2 == w2 → app w1' w2 == app v w → app v1 v2 = app v w :=
by blast

66
tests/lean/run/blast_cc_heq4.lean
View file

@ -1,66 +0,0 @@
exit
universes l1 l2 l3 l4 l5 l6
constants (A : Type.{l1}) (B : A → Type.{l2}) (C : ∀ (a : A) (ba : B a), Type.{l3})
(D : ∀ (a : A) (ba : B a) (cba : C a ba), Type.{l4})
(E : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba), Type.{l5})
(F : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba) (edcba : E a ba cba dcba), Type.{l6})
(C_ss : ∀ a ba, subsingleton (C a ba))
(a1 a2 a3 : A)
(mk_B1 mk_B2 : ∀ a, B a)
(mk_C1 mk_C2 : ∀ {a} ba, C a ba)
(tr_B : ∀ {a}, B a → B a)
(x y z : A → A)
(f f' : ∀ {a : A} {ba : B a} (cba : C a ba), D a ba cba)
(g : ∀ {a : A} {ba : B a} {cba : C a ba} (dcba : D a ba cba), E a ba cba dcba)
(h : ∀ {a : A} {ba : B a} {cba : C a ba} {dcba : D a ba cba} (edcba : E a ba cba dcba), F a ba cba dcba edcba)
attribute C_ss [instance]
set_option blast.strategy "cc"
set_option blast.cc.heq true
example : ∀ {a a' : A}, a == a' → mk_B1 a == mk_B1 a' :=
by blast
example : ∀ {a a' : A}, a == a' → mk_B2 a == mk_B2 a' :=
by blast
example : a1 == y a2 → mk_B1 a1 == mk_B1 (y a2) :=
by blast
example : a1 == x a2 → a2 == y a1 → mk_B1 (x (y a1)) == mk_B1 (x (y (x a2))) :=
by blast
-- The following examples need subsingleton equality propagation
set_option blast.cc.subsingleton true
example : a1 == y a2 → mk_B1 a1 == mk_B2 (y a2) → f (mk_C1 (mk_B2 a1)) == f (mk_C2 (mk_B1 (y a2))) :=
by blast
example : a1 == y a2 → tr_B (mk_B1 a1) == mk_B2 (y a2) → f (mk_C1 (mk_B2 a1)) == f (mk_C2 (tr_B (mk_B1 (y a2)))) :=
by blast
example : a1 == y a2 → mk_B1 a1 == mk_B2 (y a2) → g (f (mk_C1 (mk_B2 a1))) == g (f (mk_C2 (mk_B1 (y a2)))) :=
by blast
example : a1 == y a2 → tr_B (mk_B1 a1) == mk_B2 (y a2) → g (f (mk_C1 (mk_B2 a1))) == g (f (mk_C2 (tr_B (mk_B1 (y a2))))) :=
by blast
example : a1 == y a2 → a2 == z a3 → a3 == x a1 → mk_B1 a1 == mk_B2 (y (z (x a1))) →
f (mk_C1 (mk_B2 (y (z (x a1))))) == f' (mk_C2 (mk_B1 a1)) →
g (f (mk_C1 (mk_B2 (y (z (x a1)))))) == g (f' (mk_C2 (mk_B1 a1))) :=
by blast
example : a1 == y a2 → a2 == z a3 → a3 == x a1 → mk_B1 a1 == mk_B2 (y (z (x a1))) →
f (mk_C1 (mk_B2 (y (z (x a1))))) == f' (mk_C2 (mk_B1 a1)) →
f' (mk_C1 (mk_B1 a1)) == f (mk_C2 (mk_B2 (y (z (x a1))))) →
g (f (mk_C1 (mk_B1 (y (z (x a1)))))) == g (f' (mk_C2 (mk_B2 a1))) :=
by blast
example : a1 == y a2 → a2 == z a3 → a3 == x a1 → tr_B (mk_B1 a1) == mk_B2 (y (z (x a1))) →
f (mk_C1 (mk_B2 (y (z (x a1))))) == f' (mk_C2 (tr_B (mk_B1 a1))) →
f' (mk_C1 (tr_B (mk_B1 a1))) == f (mk_C2 (mk_B2 (y (z (x a1))))) →
g (f (mk_C1 (tr_B (mk_B1 (y (z (x a1))))))) == g (f' (mk_C2 (mk_B2 a1))) :=
by blast

9
tests/lean/run/blast_cc_heq5.lean
View file

@ -1,9 +0,0 @@
exit
set_option blast.strategy "cc"
set_option blast.cc.heq true
definition ex1 (a b c a' b' c' : nat) : a = a' → b = b' → c = c' → a + b + c + a = a' + b' + c' + a' :=
by blast
set_option pp.beta true
print ex1

19
tests/lean/run/blast_cc_heq6.lean
View file

@ -1,19 +0,0 @@
exit
import data.unit
open unit
set_option blast.strategy "cc"
set_option blast.cc.subsingleton true
set_option blast.cc.heq true
example (a b : unit) : a = b :=
by blast
example (a b : nat) (h₁ : a = 0) (h₂ : b = 0) : a = b → h₁ == h₂ :=
by blast
definition inv' : ∀ (a : nat), a ≠ 0 → nat :=
sorry
example (a b : nat) (h₁ : a ≠ 0) (h₂ : b ≠ 0) : a = b → inv' a h₁ = inv' b h₂ :=
by blast

11
tests/lean/run/blast_cc_heq8.lean
View file

@ -1,11 +0,0 @@
exit
open nat subtype
definition f (x : nat) (y : {n : nat | n > x}) : nat :=
x + elt_of y
set_option blast.subst false
example (h : nat → nat) (a b c d : nat) (Ha : h c > h a) (Hb : h d > h b)
: h a = h b → c = d → f (h a) (tag (h c) Ha) = f (h b) (tag (h d) Hb) :=
by inst_simp

15
tests/lean/run/blast_cc_heq9.lean
View file

@ -1,15 +0,0 @@
exit
open subtype
set_option blast.strategy "cc"
example (f g : Π {A : Type₁}, A → A → A) (h : nat → nat) (a b : nat) :
h = f a → h b = f a b :=
by blast
example (f g : Π {A : Type₁}, A → A → A) (h : nat → nat) (a b : nat) :
h = f a → h b = f a b :=
by blast
example (f g : Π {A : Type₁} (a b : A), {x : A | x ≠ b}) (h : Π (b : nat), {x : nat | x ≠ b}) (a b₁ b₂ : nat) :
h = f a → b₁ = b₂ → h b₁ == f a b₂ :=
by blast

14
tests/lean/run/blast_cc_missed.lean
View file

@ -1,14 +0,0 @@
exit
set_option blast.strategy "cc"
example (C : nat → Type) (f : Π n, C n → C n) (n m : nat) (c : C n) (d : C m) :
f n == f m → c == d → n == m → f n c == f m d :=
by blast
example (f : nat → nat → nat) (a b c d : nat) :
c = d → f a = f b → f a c = f b d :=
by blast
example (f : nat → nat → nat) (a b c d : nat) :
c == d → f a == f b → f a c == f b d :=
by blast

35
tests/lean/run/blast_cc_noconfusion.lean
View file

@ -1,35 +0,0 @@
exit
import data.list
open nat
set_option blast.strategy "cc"
constant f : nat → nat
example (a b c d : nat) : f d = f b → succ a = f b → f d = succ c → a = c :=
by blast
example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = succ c → a = c :=
by blast
example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = zero → false :=
by blast
example (a b c d e : nat) : f d = f b → f e = f b → succ a = f b → f e = 0 → false :=
by blast
open list
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l1 = l2 → l2 = l3 → l4 = [a, b, succ c] → l1 = [c, d, succ e] → l3 = l4 → c = e :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ (succ c)] → l1 = [c, d, succ (succ e)] → l3 = l4 → l1 = l2 → l2 = l3 → c = e :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ c] → l1 = [c, d, 0] → l3 = l4 → l1 = l2 → l2 = l3 → false :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l4 = [a, b, succ c] → l1 = nil → l3 = l4 → l1 = l2 → l2 = l3 → false :=
by blast
example (a b c d e f : nat) (l1 l2 l3 l4 : list nat) : l1 = l2 → l2 = l3 → l4 = [a, b, succ c] → l1 = nil → l3 = l4 → false :=
by blast

29
tests/lean/run/blast_cc_subsingleton1.lean
View file

@ -1,29 +0,0 @@
exit
import data.unit
open nat unit
constant f {A : Type} (a : A) {B : Type} (b : B) : nat
constant g : unit → nat
set_option blast.strategy "cc"
example (a b : unit) : g a = g b :=
by blast
example (a c : unit) (b d : nat) : b = d → f a b = f c d :=
by blast
constant h {A B : Type} : A → B → nat
example (a b c d : unit) : h a b = h c d :=
by blast
definition C [reducible] : nat → Type₁
| nat.zero := unit
| (nat.succ a) := nat
constant g₂ : Π {n : nat}, C n → nat → nat
example (a b : C zero) (c d : nat) : c = d → g₂ a c = g₂ b d :=
by blast

15
tests/lean/run/blast_cc_subsingleton2.lean
View file

@ -1,15 +0,0 @@
exit
import data.unit
open nat unit
set_option blast.strategy "cc"
constant r {A B : Type} : A → B → A
definition ex1 (a b c d : unit) : r a b = r c d :=
by blast
-- The congruence closure module does not automatically merge subsingleton equivalence classes.
--
-- example (a b : unit) : a = b :=
-- by blast

18
tests/lean/run/blast_congr_bug.lean
View file

@ -1,18 +0,0 @@
exit
constant P : Type₁
constant P_sub : subsingleton P
attribute P_sub [instance]
constant q : P → Prop
section
example (h₁ h₂ : P) : q h₁ = q h₂ :=
by simp
end
section
set_option blast.strategy "cc"
example (h₁ h₂ : P) : q h₁ = q h₂ :=
by blast
end

5
tests/lean/run/blast_discr_tree_annot_bug.lean
View file

@ -1,5 +0,0 @@
exit
constants (P : ℕ → Prop) (Q : Prop)
lemma foo [intro!] [forward] : (: P 0 :) → Q := sorry
example : P 0 → Q :=
by grind

19
tests/lean/run/blast_discr_tree_bug.lean
View file

@ -1,19 +0,0 @@
exit
open subtype nat
constant f : Π (a : nat), {b : nat | b > a} → nat
definition f_flat (a : nat) (b : nat) (p : b > a) : nat :=
f a (tag b p)
definition greater [reducible] (a : nat) := {b : nat | b > a}
set_option blast.recursion.structure true
definition f_flat_def [simp] (a : nat) (b : nat) (p : b > a) : f a (tag b p) = f_flat a b p :=
rfl
definition has_property_tag [simp] {A : Type} {p : A → Prop} (a : A) (h : p a) : has_property (tag a h) = h :=
rfl
lemma to_f_flat : ∀ (a : nat) (b : greater a), f a b = f_flat a (elt_of b) (has_property b) :=
by rec_simp

13
tests/lean/run/blast_ematch1.lean
View file

@ -1,13 +0,0 @@
exit
import data.nat
open nat
constant f : nat → nat
constant g : nat → nat
definition lemma1 [forward] : ∀ x, (:g (f x):) = x :=
sorry
set_option blast.strategy "ematch"
example (a b c : nat) : a = f b → a = f c → g a ≠ b → false :=
by blast

9
tests/lean/run/blast_ematch10.lean
View file

@ -1,9 +0,0 @@
exit
attribute iff [reducible]
set_option blast.strategy "ematch"
definition lemma1 (p : nat → Prop) (a b c : nat) : p a → a = b → p b :=
by blast
set_option pp.beta true
print lemma1

13
tests/lean/run/blast_ematch2.lean
View file

@ -1,13 +0,0 @@
exit
import data.nat
open nat
constant f : nat → nat
constant g : nat → nat
definition lemma1 [forward] : ∀ x, g (f x) = x :=
sorry
set_option blast.strategy "ematch"
example (a b : nat) : f a = f b → a = b :=
by blast

36
tests/lean/run/blast_ematch3.lean
View file

@ -1,36 +0,0 @@
exit
import algebra.ring data.nat
namespace foo
variables {A : Type}
section
variables [s : add_comm_monoid A]
include s
attribute add.comm [forward]
attribute add.assoc [forward]
set_option blast.strategy "ematch"
theorem add_comm_three (a b c : A) : a + b + c = c + b + a :=
by blast
theorem add.comm4 : ∀ (n m k l : A), n + m + (k + l) = n + k + (m + l) :=
by blast
end
section
variable [s : group A]
include s
attribute mul.assoc [forward]
attribute mul.left_inv [forward]
attribute one_mul [forward]
set_option blast.strategy "ematch"
theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
by blast
end
end foo

15
tests/lean/run/blast_ematch4.lean
View file

@ -1,15 +0,0 @@
exit
import data.nat
open algebra nat
section
open nat
set_option blast.strategy "ematch"
attribute add.comm [forward]
attribute add.assoc [forward]
example (a b c : nat) : a + b + b + c = c + b + a + b :=
by blast
end

10
tests/lean/run/blast_ematch5.lean
View file

@ -1,10 +0,0 @@
exit
constant subt : nat → nat → Prop
lemma subt_trans [forward] {a b c : nat} : subt a b → subt b c → subt a c :=
sorry
set_option blast.strategy "ematch"
example (a b c d : nat) : subt a b → subt b c → subt c d → subt a d :=
by blast

29
tests/lean/run/blast_ematch6.lean
View file

@ -1,29 +0,0 @@
exit
import algebra.ring data.nat
open algebra
variables {A : Type}
section
variable [s : group A]
include s
set_option blast.strategy "ematch"
attribute mul_one [forward]
attribute mul.assoc [forward]
attribute mul.left_inv [forward]
attribute one_mul [forward]
theorem inv_eq_of_mul_eq_one₁ {a b : A} (H : a * b = 1) : a⁻¹ = b :=
-- This is the kind of theorem that can be easily proved using superposition,
-- but cannot to be proved using E-matching.
-- To prove it using E-matching, we must provide the following auxiliary assertion.
-- E-matching can prove it automatically, and then it is trivial to prove the conclusion
-- using it.
-- Remark: this theorem can also be proved using model-based quantifier instantiation (MBQI) available in Z3.
-- So, we may be able to prove it using qcf.
assert a⁻¹ * 1 = b, by blast,
by blast
end

49
tests/lean/run/blast_ematch8.lean
View file

@ -1,49 +0,0 @@
exit
import algebra.group
open algebra
variables {A : Type}
variables [s : group A]
include s
namespace foo
set_option blast.strategy "ematch"
attribute inv_inv mul.left_inv mul.assoc one_mul mul_one [forward]
theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
calc
a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : by blast
... = 1 : by blast
theorem mul.right_inv₂ (a : A) : a * a⁻¹ = 1 :=
by blast
theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) = b :=
calc
a * (a⁻¹ * b) = a * a⁻¹ * b : by blast
... = 1 * b : by blast
... = b : by blast
theorem mul_inv_cancel_left₂ (a b : A) : a * (a⁻¹ * b) = b :=
by blast
theorem mul_inv (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
inv_eq_of_mul_eq_one
(calc
a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : by blast
... = 1 : by blast)
theorem eq_of_mul_inv_eq_one {a b : A} (H : a * b⁻¹ = 1) : a = b :=
calc
a = a * b⁻¹ * b : by blast
... = 1 * b : by blast
... = b : by blast
-- This is another theorem that can be easily proved using superposition,
-- but cannot to be proved using E-matching.
-- To prove it using E-matching, we must provide the following auxiliary step using calc.
theorem eq_of_mul_inv_eq_one₂ {a b : A} (H : a * b⁻¹ = 1) : a = b :=
calc
a = a * b⁻¹ * b : by blast
... = b : by blast
end foo

9
tests/lean/run/blast_ematch9.lean
View file

@ -1,9 +0,0 @@
exit
constant P : nat → Prop
definition h [reducible] (n : nat) := n
definition foo [forward] : ∀ x, P (h x) := sorry
set_option blast.strategy "ematch"
example (n : nat) : P (h n) :=
by blast

14
tests/lean/run/blast_ematch_cast1.lean
View file

@ -1,14 +0,0 @@
exit
import data.nat
open nat
constant C : nat → Type₁
constant f : ∀ n, C n → C n
lemma fax [forward] (n : nat) (a : C (2*n)) : (: f (2*n) a :) = a :=
sorry
set_option blast.strategy "ematch"
example (n m : nat) (a : C n) : n = 2*m → f n a = a :=
by blast

15
tests/lean/run/blast_ematch_cast2.lean
View file

@ -1,15 +0,0 @@
exit
import data.nat
open nat
constant C : nat → Type₁
constant f : ∀ n, C n → C n
constant g : ∀ n, C n → C n → C n
lemma gffax [forward] (n : nat) (a b : C n) : (: g n (f n a) (f n b) :) = a :=
sorry
set_option blast.strategy "ematch"
example (n m : nat) (a c : C n) (b : C m) : n = m → a == f m b → g n a (f n c) == b :=
by blast

16
tests/lean/run/blast_ematch_cast3.lean
View file

@ -1,16 +0,0 @@
exit
import data.nat
open nat
constant C : nat → Type₁
constant f : ∀ n, C n → C n
constant g : ∀ n, C n → C n → C n
lemma gffax [forward] (n : nat) (a b : C n) : (: g n a b :) = a :=
sorry
set_option blast.strategy "ematch"
set_option trace.blast.ematch true
example (n m : nat) (a c : C n) (b : C m) (e : m = n) : a == b → g n a a == b :=
by blast

16
tests/lean/run/blast_ematch_heq1.lean
View file

@ -1,16 +0,0 @@
exit
import data.nat
open algebra nat
section
open nat
set_option blast.strategy "ematch"
set_option blast.cc.heq true
attribute add.comm [forward]
attribute add.assoc [forward]
example (a b c : nat) : a + b + b + c = c + b + a + b :=
by blast
end

11
tests/lean/run/blast_ematch_heq2.lean
View file

@ -1,11 +0,0 @@
exit
import algebra.group
variable {A : Type}
variable [s : group A]
include s
set_option blast.cc.heq true
example (a : A) : a * 1⁻¹ = a :=
by inst_simp

25
tests/lean/run/blast_ematch_heq3.lean
View file

@ -1,25 +0,0 @@
exit
import data.nat
open nat
constant tuple.{l} : Type.{l} → nat → Type.{l}
constant nil {A : Type} : tuple A 0
constant append {A : Type} {n m : nat} : tuple A n → tuple A m → tuple A (n + m)
infix ` ++ ` := append
axiom append_assoc {A : Type} {n₁ n₂ n₃ : nat} (v₁ : tuple A n₁) (v₂ : tuple A n₂) (v₃ : tuple A n₃) :
(v₁ ++ v₂) ++ v₃ == v₁ ++ (v₂ ++ v₃)
attribute append_assoc [simp]
variables {A : Type}
variables {p m n q : nat}
variables {xs : tuple A m}
variables {ys : tuple A n}
variables {zs : tuple A p}
variables {ws : tuple A q}
example : p = m + n → zs == xs ++ ys → zs ++ ws == xs ++ (ys ++ ws) :=
by inst_simp
example : p = n + m → zs == xs ++ ys → zs ++ ws == xs ++ (ys ++ ws) :=
by inst_simp

10
tests/lean/run/blast_ematch_heq4.lean
View file

@ -1,10 +0,0 @@
exit
universe l
constants (A : Type.{l}) (P : A → Prop) (h : Π (a : A), P a → A) (f g : A → A)
constants (p : ∀ a, P a)
axiom h_simp {a : A} : h (f a) (p (f a)) = a
attribute h_simp [simp]
example {a b : A} : g b = f a → h (g b) (p (g b)) = a :=
by inst_simp

13
tests/lean/run/blast_ematch_list.lean
View file

@ -1,13 +0,0 @@
exit
import data.list
open list
lemma last_singleton [simp] {A : Type} (a : A) : last [a] !cons_ne_nil = a :=
rfl
lemma last_cons_cons [simp] {A : Type} (a₁ a₂ : A) (l : list A) : last (a₁::a₂::l) !cons_ne_nil = last (a₂::l) !cons_ne_nil :=
rfl
theorem last_concat [simp] {A : Type} {x : A} : ∀ {l : list A}, last (concat x l) !concat_ne_nil = x :=
by rec_inst_simp

15
tests/lean/run/blast_ematch_ss1.lean
View file

@ -1,15 +0,0 @@
exit
constant q (a : Prop) (h : decidable a) : Prop
constant r : nat → Prop
constant rdec : ∀ a, decidable (r a)
constant s : nat → nat
axiom qax : ∀ a h, (: q (r (s a)) h :)
attribute qax [forward]
set_option blast.strategy "ematch"
definition ex1 (a : nat) (b : nat) : b = s a → q (r b) (rdec b) :=
by blast
print ex1

33
tests/lean/run/blast_ematch_sum.lean
View file

@ -1,33 +0,0 @@
exit
import data.nat
open nat
definition Sum : nat → (nat → nat) → nat :=
sorry
notation `Σ` binders ` < ` n `, ` r:(scoped f, Sum n f) := r
lemma Sum_const [forward] (n : nat) (c : nat) : (Σ x < n, c) = n * c :=
sorry
lemma Sum_add [forward] (f g : nat → nat) (n : nat) : (Σ x < n, f x + g x) = (Σ x < n, f x) + (Σ x < n, g x) :=
sorry
attribute add.assoc add.comm add.left_comm mul_zero zero_mul mul_one add_zero zero_add one_mul mul.comm mul.assoc mul.left_comm [forward]
set_option blast.strategy "ematch"
example (f : nat → nat) (n : nat) : (Σ x < n, f x + 1) = (Σ x < n, f x) + n :=
by blast
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + h x) = (Σ x < n, h x) + (Σ x < n, f x) + (Σ x < n, g x) :=
by blast
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + h x) = Sum n h + (Σ x < n, f x) + (Σ x < n, g x) :=
by blast
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + 0) = (Σ x < n, f x) + (Σ x < n, g x) :=
by blast
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + h x + 2) = 0 + Sum n h + (Σ x < n, f x) + (Σ x < n, g x) + 2 * n :=
by blast

18
tests/lean/run/blast_ematch_uni_issue.lean
View file

@ -1,18 +0,0 @@
exit
set_option blast.ematch true
variable {A : Type}
definition R : A → A → Prop := sorry
definition R_trans [forward] {a b c : A} : R a b → R b c → R a c := sorry
example (a b c : A) : R a b → R b c → R a c :=
by blast
example {A : Type} (a b c : A) : R a b → R b c → R a c :=
by blast
example {A : Type.{1}} (a b c : A) : R a b → R b c → R a c :=
by blast
universe u
example {A : Type.{u}} (a b c : A) : R a b → R b c → R a c :=
by blast

40
tests/lean/run/blast_equiv_tests.lean
View file

@ -1,40 +0,0 @@
exit
import data.sum data.nat
open function
structure equiv [class] (A B : Type) :=
(to_fun : A → B)
(inv_fun : B → A)
(left_inv : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)
namespace equiv
infix ` ≃ `:50 := equiv
protected definition refl [refl] (A : Type) : A ≃ A :=
mk (@id A) (@id A) (λ x, rfl) (λ x, rfl)
protected definition symm [symm] {A B : Type} : A ≃ B → B ≃ A
| (mk f g h₁ h₂) := mk g f h₂ h₁
protected definition trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A ≃ C
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
mk (f₂ ∘ f₁) (g₁ ∘ g₂)
(show ∀ x, g₁ (g₂ (f₂ (f₁ x))) = x, by intros; rewrite [l₂, l₁]; reflexivity)
(show ∀ x, f₂ (f₁ (g₁ (g₂ x))) = x, by intros; rewrite [r₁, r₂]; reflexivity)
definition arrow_congr₁ {A₁ A₂ B₁ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
mk
(λ (h : A₁ → B₁) (a : A₂), f₂ (h (g₁ a)))
(λ (h : A₂ → B₂) (a : A₁), g₂ (h (f₁ a)))
(λ h, funext (λ a, begin rewrite [l₁, l₂], reflexivity end))
(begin unfold [left_inverse, right_inverse] at *, intros, apply funext, intros, simp end)
local attribute left_inverse right_inverse [reducible]
definition arrow_congr₂ {A₁ A₂ B₁ B₂ : Type} : A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ → B₁) ≃ (A₂ → B₂)
| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) :=
mk (λ h a, f₂ (h (g₁ a))) (λ h a, g₂ (h (f₁ a))) (by simp) (by simp)
end equiv

22
tests/lean/run/blast_flat.lean
View file

@ -1,22 +0,0 @@
exit
open nat subtype
definition f (x : nat) (y : {n : nat | n > x}) : nat :=
x + elt_of y
definition f_flat (x : nat) (y : nat) (H : y > x) : nat :=
f x (tag y H)
lemma f_flat_simp [forward] (x : nat) (y : nat) (H : y > x) : f x (tag y H) = f_flat x y H :=
rfl
set_option trace.simplifier true
set_option trace.blast true
set_option blast.strategy "ematch"
example (a b c d : nat) (Ha : c > a) (Hb : d > b) : a = b → c = d → f a (tag c Ha) = f b (tag d Hb) :=
by blast
example (h : nat → nat) (a b c d : nat) (Ha : h c > h a) (Hb : h d > h b)
: h a = h b → c = d → f (h a) (tag (h c) Ha) = f (h b) (tag (h d) Hb) :=
by blast

11
tests/lean/run/blast_fun_info_bug.lean
View file

@ -1,11 +0,0 @@
exit
definition set (A : Type) := A → Prop
set_option blast.strategy "preprocess"
example {A : Type} (s : set A) (a b : A) : a = b → s a → s b :=
by blast
set_option blast.strategy "cc"
example {A : Type} (s : set A) (a b : A) : a = b → s a → s b :=
by blast

33
tests/lean/run/blast_grind1.lean
View file

@ -1,33 +0,0 @@
exit
set_option blast.strategy "core_grind"
example (a b c : nat) : a = b ∨ a = c → b = c → b = a :=
by blast
example (f : nat → nat) (a b c : nat) : f a = f b ∨ f a = f c → f b = f c → f b = f a :=
by blast
definition ex1 (a : nat) : a = 0 → (λ x, x + a) = (λ x, x + 0) :=
by blast
print ex1
attribute Exists.intro [intro!] -- core_grind only process [intro!] declarations
example (p q : nat → Prop) : (∃ x, p x ∧ q x) → (∃ x, q x) ∧ (∃ x, p x) :=
by blast
set_option blast.strategy "core_grind"
example (a b c : nat) : a = b ∨ a = c → b = c → b = a :=
by blast
example (f : nat → nat) (a b c : nat) : f a = f b ∨ f a = f c → f b = f c → f b = f a :=
by blast
example (a : nat) : a = 0 → (λ x, x + a) = (λ x, x + 0) :=
by blast
set_option trace.blast true
example (p q : nat → Prop) : (∃ x, p x ∧ q x) → (∃ x, q x) ∧ (∃ x, p x) :=
by blast

14
tests/lean/run/blast_meta.lean
View file

@ -1,14 +0,0 @@
exit
constant p : nat → nat → Prop
constant p_trans : ∀ a b c, p a b → p b c → p a c
definition lemma1 (a b c d : nat) : a = d → p b c → p a b → p a c :=
begin
intros,
apply p_trans,
blast,
blast
end
print lemma1

8
tests/lean/run/blast_meta_bug.lean
View file

@ -1,8 +0,0 @@
exit
constants {A : Type.{1}} (P : A → Prop) (Q : A → Prop)
definition H [forward] : ∀ a, (: P a :) → Exists Q := sorry
set_option blast.strategy "ematch"
example (a : A) : P a → Exists Q :=
by blast

30
tests/lean/run/blast_multiple_nots.lean
View file

@ -1,30 +0,0 @@
exit
constants a b c d : Prop
set_option blast.strategy "unit"
example (H : ¬ a → ¬ b → ¬ c ∨ ¬ d) : ¬ a → c → d → ¬ b → false :=
by blast
set_option blast.strategy "preprocess"
example : ¬¬¬¬¬a → ¬¬a → false :=
by blast
example : ¬¬¬¬¬a → ¬¬¬¬a → false :=
by blast
example : ¬¬¬¬¬a → a → false :=
by blast
example : ¬¬a → ¬¬¬¬¬a → false :=
by blast
example : ¬¬¬¬¬a → ¬¬¬¬¬¬¬¬a → false :=
by blast
example : ¬¬¬¬¬a → a → false :=
by blast
example : ¬¬¬¬¬¬¬¬a → ¬¬¬¬¬a → false :=
by blast

9
tests/lean/run/blast_pattern_inference_bug.lean
View file

@ -1,9 +0,0 @@
exit
constant p : nat → Prop
constant q : ∀ a, p a → Prop
lemma ex [forward] : ∀ (a : nat) (h : p a), (:q a h:) := sorry
set_option blast.strategy "ematch"
lemma test (h : p 0) : q 0 h :=
by blast

13
tests/lean/run/blast_rec_eq.lean
View file

@ -1,13 +0,0 @@
exit
open nat
lemma addz [simp] : ∀ a : nat, a + 0 = a := sorry
lemma zadd [simp] : ∀ a : nat, 0 + a = a := sorry
lemma adds [simp] : ∀ a b : nat, a + succ b = succ (a + b) := sorry
lemma sadd [simp] : ∀ a b : nat, succ a + b = succ (a + b) := sorry
definition comm : ∀ a b : nat, a + b = b + a
| a 0 := by simp
| a (succ n) :=
assert a + n = n + a, from !comm,
by simp

17
tests/lean/run/blast_recursor1.lean
View file

@ -1,17 +0,0 @@
exit
constants P Q : nat → Prop
inductive foo : nat → Prop :=
| intro1 : ∀ n, P n → foo n
| intro2 : ∀ n, P n → foo n
definition bar (n : nat) : foo n → P n :=
by blast
print bar
/-
definition bar : ∀ (n : ℕ), foo n → P n :=
foo.rec (λ (n : ℕ) (H.3 : P n), H.3) (λ (n : ℕ) (H.3 : P n), H.3)
-/
definition baz (n : nat) : foo n → foo n ∧ P n :=
by blast --loops

18
tests/lean/run/blast_simp1.lean
View file

@ -1,18 +0,0 @@
exit
example (a b c : Prop) : a ∧ b ∧ c ↔ c ∧ b ∧ a :=
by simp
example (a b c : Prop) : a ∧ false ∧ c ↔ false :=
by simp
example (a b c : Prop) : a ∨ false ∨ b ↔ b ∨ a :=
by simp
example (a b c : Prop) : ¬ true ∨ false ∨ b ↔ b :=
by simp
example (a b c : Prop) : if true then a else b ↔ if false then b else a :=
by simp
example (a b : Prop) : a ∧ not a ↔ false :=
by simp

5
tests/lean/run/blast_simp2.lean
View file

@ -1,5 +0,0 @@
exit
definition tst1 (a b : Prop) : a ∧ b ∧ true → b ∧ a :=
by simp
print tst1

4
tests/lean/run/blast_simp3.lean
View file

@ -1,4 +0,0 @@
exit
example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ →
(λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) :=
by simp

16
tests/lean/run/blast_simp4.lean
View file

@ -1,16 +0,0 @@
exit
import data.nat
open nat
constant f : nat → nat
definition g (a : nat) := a
example (a b : nat) : a + 0 = 0 + g b → f (f b) = f (f a) :=
suppose a + 0 = 0 + g b,
assert a = b, by unfold g at *; simp,
by simp
attribute g [reducible]
example (a b : nat) : a + 0 = 0 + g b → f (f b) = f (f a) :=
by simp

9
tests/lean/run/blast_simp5.lean
View file

@ -1,9 +0,0 @@
exit
definition f : nat → nat := sorry
definition g (a : nat) := f a
lemma gax [simp] : ∀ a, g a = 0 := sorry
attribute g [reducible]
example (a : nat) : f (a + a) = 0 :=
by simp

24
tests/lean/run/blast_simp_st1.lean
View file

@ -1,24 +0,0 @@
exit
import data.nat
open algebra nat
section
open nat
set_option blast.strategy "preprocess" -- make sure simplifier is not used by default
attribute add.comm [simp]
attribute add.assoc [simp]
attribute add.left_comm [simp]
example (a b c : nat) : a + b + b + c = c + b + a + b :=
by simp
example (a b c : nat) : a = b → a + c = c + b :=
by simp
definition f : nat → nat := sorry
example (a b c : nat) : f a = f b → f a + c = c + f b :=
by simp
end

43
tests/lean/run/blast_simp_subsingleton.lean
View file

@ -1,43 +0,0 @@
exit
import data.unit
open nat unit
constant f {A : Type} (a : A) {B : Type} (b : B) : nat
constant g : unit → nat
example (a b : unit) : g a = g b :=
by simp
example (a c : unit) (b d : nat) : b = d → f a b = f c d :=
by simp
constant h {A B : Type} : A → B → nat
example (a b c d : unit) : h a b = h c d :=
by simp
definition C [reducible] : nat → Type₁
| nat.zero := unit
| (nat.succ a) := nat
constant g₂ : Π {n : nat}, C n → nat → nat
example (a b : C zero) (c d : nat) : c = d → g₂ a c = g₂ b d :=
by simp
example (n : nat) (h : zero = n) (a b : C n) (c d : nat) : c = d → g₂ a c = g₂ b d :=
by simp
-- The following one cannot be solved as is
-- example (a c : nat) (b d : unit) : a = c → b = d → f a b = f c d :=
-- by simp
-- But, we can use the following trick
definition f_aux {A B : Type} (a : A) (b : B) := f a b
lemma to_f_aux [simp] {A B : Type} (a : A) (b : B) : f a b = f_aux a b :=
rfl
example (a c : nat) (b d : unit) : a = c → b = d → f a b = f c d :=
by simp

17
tests/lean/run/blast_simp_subsingleton2.lean
View file

@ -1,17 +0,0 @@
exit
import data.unit
open nat unit
constant r {A B : Type} : A → B → A
example (a b c d : unit) : r a b = r c d :=
by simp
example (a b : unit) : a = b :=
by simp
example (a b : unit) : (λ x : nat, a) = (λ y : nat, b) :=
by simp
example (a b : unit) : (λ x : nat, r a b) = (λ y : nat, r b b) :=
by simp

31
tests/lean/run/blast_simp_sum.lean
View file

@ -1,31 +0,0 @@
exit
import data.nat
open - [simp] nat
definition Sum : nat → (nat → nat) → nat :=
sorry
notation `Σ` binders ` < ` n `, ` r:(scoped f, Sum n f) := r
lemma Sum_const [simp] (n : nat) (c : nat) : (Σ x < n, c) = n * c :=
sorry
lemma Sum_add [simp] (f g : nat → nat) (n : nat) : (Σ x < n, f x + g x) = (Σ x < n, f x) + (Σ x < n, g x) :=
sorry
attribute add.assoc add.comm add.left_comm mul_one add_zero zero_add one_mul mul.comm mul.assoc mul.left_comm [simp]
example (f : nat → nat) (n : nat) : (Σ x < n, f x + 1) = (Σ x < n, f x) + n :=
by simp
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + h x) = (Σ x < n, h x) + (Σ x < n, f x) + (Σ x < n, g x) :=
by simp
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + h x) = Sum n h + (Σ x < n, f x) + (Σ x < n, g x) :=
by simp
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + h x + 0) = Sum n h + (Σ x < n, f x) + (Σ x < n, g x) :=
by simp
example (f g h : nat → nat) (n : nat) : (Σ x < n, f x + g x + h x + 2) = 0 + Sum n h + (Σ x < n, f x) + (Σ x < n, g x) + 2 * n :=
by simp

6
tests/lean/run/blast_trace.lean
View file

@ -1,6 +0,0 @@
exit
set_option trace.blast true
set_option trace.blast.action false
example (a b : Prop) : a ∧ b → b ∧ a :=
by blast

17
tests/lean/run/blast_tuple1.lean
View file

@ -1,17 +0,0 @@
exit
import data.nat
open nat
constant tuple.{l} : Type.{l} → nat → Type.{l}
constant nil {A : Type} : tuple A 0
constant cons {A : Type} {n : nat} : A → tuple A n → tuple A (succ n)
constant append {A : Type} {n m : nat} : tuple A n → tuple A m → tuple A (n + m)
infix ` ++ ` := append
axiom append_nil {A : Type} {n : nat} (v : tuple A n) : v ++ nil = v
axiom nil_append {A : Type} {n : nat} (v : tuple A n) : nil ++ v == v
axiom append_assoc {A : Type} {n₁ n₂ n₃ : nat} (v₁ : tuple A n₁) (v₂ : tuple A n₂) (v₃ : tuple A n₃) : (v₁ ++ v₂) ++ v₃ == v₁ ++ (v₂ ++ v₃)
attribute append_nil nil_append append_assoc [simp]
example (A : Type) (n m : nat) (v₁ v₂ : tuple A n) (w₁ w₂ : tuple A m) :
v₁ ++ nil ++ (v₂ ++ w₁) ++ (nil ++ w₂) == v₁ ++ v₂ ++ w₁ ++ w₂ :=
by inst_simp

44
tests/lean/run/blast_unit.lean
View file

@ -1,44 +0,0 @@
exit
-- Testing all possible cases of [unit_action]
set_option blast.strategy "unit"
variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop}
-- H first, all pos
example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) : B₄ := by blast
example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₄) : B₃ := by blast
example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n3 : ¬ B₃) (n3 : ¬ B₄) : B₂ := by blast
example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : B₁ := by blast
example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₃ := by blast
example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₂ := by blast
example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₁ := by blast
-- H last, all pos
example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₄ := by blast
example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₃ := by blast
example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₂ := by blast
example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₁ := by blast
example (a1 : A₁) (a2 : A₂) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₃ := by blast
example (a1 : A₁) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₂ := by blast
example (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₁ := by blast
-- H first, all neg
example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) : ¬ B₄ := by blast
example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b4 : B₄) : ¬ B₃ := by blast
example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b3 : B₃) (b4 : B₄) : ¬ B₂ := by blast
example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ B₁ := by blast
example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₃ := by blast
example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₂ := by blast
example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₁ := by blast
-- H last, all neg
example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₄ := by blast
example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₃ := by blast
example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₂ := by blast
example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₁ := by blast
example (n1 : ¬ A₁) (n2 : ¬ A₂) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₃ := by blast
example (n1 : ¬ A₁) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₂ := by blast
example (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₁ := by blast

21
tests/lean/run/blast_unit_cc.lean
View file

@ -1,21 +0,0 @@
exit
-- Unit propagation with congruence closure
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
-- The following tests require the unit preprocessor to work
/-
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
-/

23
tests/lean/run/blast_unit_dep.lean
View file

@ -1,23 +0,0 @@
exit
constant p : nat → Prop
constant q : Π a, p a → Prop
set_option blast.strategy "unit"
example (a : nat) (h₁ : p a) (h₂ : ∀ h : p a, q a h) : q a h₁ :=
by blast
example (a : nat) (h₂ : ∀ h : p a, q a h) (h₁ : p a) : q a h₁ :=
by blast
example (a b : nat) (H : ∀ (p₁ : p a) (p₂ : p b), q b p₂ → q a p₁) (h₁ : p a) (h₂ : p b) : q b h₂ → q a h₁ :=
by blast
example (a b : nat) (h₂ : p b) (H : ∀ (p₁ : p a) (p₂ : p b), q b p₂ → q a p₁) (h₁ : p a) : q b h₂ → q a h₁ :=
by blast
example (a b : nat) (h₂ : p b) (h₁ : p a) (H : ∀ (p₁ : p a) (p₂ : p b), q b p₂ → q a p₁) : q b h₂ → q a h₁ :=
by blast
example (a b : nat) (h₁ : p a) (H : ∀ (p₁ : p a) (p₂ : p b), q b p₂ → q a p₁) (h₂ : p b) : q b h₂ → q a h₁ :=
by blast

17
tests/lean/run/blast_unit_edges.lean
View file

@ -1,17 +0,0 @@
exit
-- Testing all possible cases of [unit_action]
set_option blast.strategy "unit"
universes l1 l2
variables {A B C : Prop}
variables {X : Type.{l1}} {Y : Type.{l2}}
variables {P : Y → Prop}
-- Types as antecedents
example (H : X → A) (x : X) : A := by blast
example (H : X → A → B) (x : X) (nb : ¬ B) : ¬ A := by blast
example (H : A → X → B → C) (x : X) (a : A) (nc : ¬ C) : ¬ B := by blast
-- Universally quantified facts
example (H : A → X → B → ∀ y : Y, P y) (x : X) (a : A) (nc : ¬ ∀ y : Y, P y) : ¬ B := by blast
example (H : A → X → B → ¬ ∀ y : Y, P y) (x : X) (a : A) (nc : ∀ y : Y, P y) : ¬ B := by blast

14
tests/lean/run/blast_unit_preprocess.lean
View file

@ -1,14 +0,0 @@
exit
-- Testing the unit pre-processor
open simplifier.unit_simp
set_option simplify.max_steps 10000
variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop}
variables {A B C D E F G : Prop}
variables {X : Type.{1}}
example (H : A ∨ B → E) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
example (H : A ∨ B → E) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
example (H : A ∨ B → E ∧ F) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
example (H : A ∨ (B ∧ C) → E ∧ F) (c : C) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast
example (H : A ∨ (B ∧ C) → (G → E ∧ F)) (g : G) (c : C) (nE : ¬ E) : ¬ A ∧ ¬ B := by blast

Some files were not shown because too many files have changed in this diff Show more