diff --git a/tests/lean/blast_back2.lean b/tests/lean/blast_back2.lean deleted file mode 100644 index 90efa0a38c..0000000000 --- a/tests/lean/blast_back2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/blast_back2.lean.expected.out b/tests/lean/blast_back2.lean.expected.out deleted file mode 100644 index 6be95dbdba..0000000000 --- a/tests/lean/blast_back2.lean.expected.out +++ /dev/null @@ -1 +0,0 @@ -blast_back2.lean:1:0: warning: using 'exit' to interrupt Lean diff --git a/tests/lean/blast_cc_not_provable.lean b/tests/lean/blast_cc_not_provable.lean deleted file mode 100644 index f98efa2f29..0000000000 --- a/tests/lean/blast_cc_not_provable.lean +++ /dev/null @@ -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 diff --git a/tests/lean/blast_cc_not_provable.lean.expected.out b/tests/lean/blast_cc_not_provable.lean.expected.out deleted file mode 100644 index ee378f1db4..0000000000 --- a/tests/lean/blast_cc_not_provable.lean.expected.out +++ /dev/null @@ -1 +0,0 @@ -blast_cc_not_provable.lean:1:0: warning: using 'exit' to interrupt Lean diff --git a/tests/lean/run/abstract_notation.lean b/tests/lean/run/abstract_notation.lean deleted file mode 100644 index 789ac40326..0000000000 --- a/tests/lean/run/abstract_notation.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast1.lean b/tests/lean/run/blast1.lean deleted file mode 100644 index d14be931f6..0000000000 --- a/tests/lean/run/blast1.lean +++ /dev/null @@ -1,6 +0,0 @@ -exit - -set_option blast.strategy "preprocess" - -example (a b : Prop) (Ha : a) (Hb : b) : a := -by blast diff --git a/tests/lean/run/blast10.lean b/tests/lean/run/blast10.lean deleted file mode 100644 index 444e1146bf..0000000000 --- a/tests/lean/run/blast10.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast11.lean b/tests/lean/run/blast11.lean deleted file mode 100644 index ff3946b529..0000000000 --- a/tests/lean/run/blast11.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast12.lean b/tests/lean/run/blast12.lean deleted file mode 100644 index 69bacbfd0e..0000000000 --- a/tests/lean/run/blast12.lean +++ /dev/null @@ -1,7 +0,0 @@ -exit - -import data.nat -open nat - -example (a b : nat) : 0 + a + b + 1 = 1 + a + b := -by simp diff --git a/tests/lean/run/blast13.lean b/tests/lean/run/blast13.lean deleted file mode 100644 index 7f20c7daab..0000000000 --- a/tests/lean/run/blast13.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast14.lean b/tests/lean/run/blast14.lean deleted file mode 100644 index a0f0f06b30..0000000000 --- a/tests/lean/run/blast14.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast15.lean b/tests/lean/run/blast15.lean deleted file mode 100644 index 556e10e34c..0000000000 --- a/tests/lean/run/blast15.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast16.lean b/tests/lean/run/blast16.lean deleted file mode 100644 index b4a9163173..0000000000 --- a/tests/lean/run/blast16.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast17.lean b/tests/lean/run/blast17.lean deleted file mode 100644 index 224ea5bb40..0000000000 --- a/tests/lean/run/blast17.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast2.lean b/tests/lean/run/blast2.lean deleted file mode 100644 index e8fe2e2ae8..0000000000 --- a/tests/lean/run/blast2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast20.lean b/tests/lean/run/blast20.lean deleted file mode 100644 index e747fb74e3..0000000000 --- a/tests/lean/run/blast20.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast3.lean b/tests/lean/run/blast3.lean deleted file mode 100644 index b7ac9272a8..0000000000 --- a/tests/lean/run/blast3.lean +++ /dev/null @@ -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₂ diff --git a/tests/lean/run/blast4.lean b/tests/lean/run/blast4.lean deleted file mode 100644 index 7b4d5cb677..0000000000 --- a/tests/lean/run/blast4.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast5.lean b/tests/lean/run/blast5.lean deleted file mode 100644 index da827dc274..0000000000 --- a/tests/lean/run/blast5.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast6.lean b/tests/lean/run/blast6.lean deleted file mode 100644 index c8516c8eb4..0000000000 --- a/tests/lean/run/blast6.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast7.lean b/tests/lean/run/blast7.lean deleted file mode 100644 index ff7f0466e5..0000000000 --- a/tests/lean/run/blast7.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast8.lean b/tests/lean/run/blast8.lean deleted file mode 100644 index c02d3c46b4..0000000000 --- a/tests/lean/run/blast8.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast9.lean b/tests/lean/run/blast9.lean deleted file mode 100644 index 5d2ddda510..0000000000 --- a/tests/lean/run/blast9.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_back1.lean b/tests/lean/run/blast_back1.lean deleted file mode 100644 index 4d60644a07..0000000000 --- a/tests/lean/run/blast_back1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_backward_action_missing_normalize.lean b/tests/lean/run/blast_backward_action_missing_normalize.lean deleted file mode 100644 index 257a0fb53a..0000000000 --- a/tests/lean/run/blast_backward_action_missing_normalize.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_by_contradiction.lean b/tests/lean/run/blast_by_contradiction.lean deleted file mode 100644 index 209a21df62..0000000000 --- a/tests/lean/run/blast_by_contradiction.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc1.lean b/tests/lean/run/blast_cc1.lean deleted file mode 100644 index 09a8c8182e..0000000000 --- a/tests/lean/run/blast_cc1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc10.lean b/tests/lean/run/blast_cc10.lean deleted file mode 100644 index e79640f423..0000000000 --- a/tests/lean/run/blast_cc10.lean +++ /dev/null @@ -1,7 +0,0 @@ -exit -set_option blast.strategy "cc" - -definition t1 (a b : nat) : (a = b ↔ a = b) := -by blast - -print t1 diff --git a/tests/lean/run/blast_cc11.lean b/tests/lean/run/blast_cc11.lean deleted file mode 100644 index 71e860c815..0000000000 --- a/tests/lean/run/blast_cc11.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc12.lean b/tests/lean/run/blast_cc12.lean deleted file mode 100644 index 7c4c5b5efa..0000000000 --- a/tests/lean/run/blast_cc12.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc13.lean b/tests/lean/run/blast_cc13.lean deleted file mode 100644 index f5672d7076..0000000000 --- a/tests/lean/run/blast_cc13.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc14.lean b/tests/lean/run/blast_cc14.lean deleted file mode 100644 index 5eb38895b5..0000000000 --- a/tests/lean/run/blast_cc14.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc2.lean b/tests/lean/run/blast_cc2.lean deleted file mode 100644 index 2842ec05af..0000000000 --- a/tests/lean/run/blast_cc2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc3.lean b/tests/lean/run/blast_cc3.lean deleted file mode 100644 index e5b1ac1e83..0000000000 --- a/tests/lean/run/blast_cc3.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc4.lean b/tests/lean/run/blast_cc4.lean deleted file mode 100644 index ae7a7b51ec..0000000000 --- a/tests/lean/run/blast_cc4.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc5.lean b/tests/lean/run/blast_cc5.lean deleted file mode 100644 index 1541e95150..0000000000 --- a/tests/lean/run/blast_cc5.lean +++ /dev/null @@ -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 --/ diff --git a/tests/lean/run/blast_cc6.lean b/tests/lean/run/blast_cc6.lean deleted file mode 100644 index e43f3c8a17..0000000000 --- a/tests/lean/run/blast_cc6.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc7.lean b/tests/lean/run/blast_cc7.lean deleted file mode 100644 index a94dc84e37..0000000000 --- a/tests/lean/run/blast_cc7.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc9.lean b/tests/lean/run/blast_cc9.lean deleted file mode 100644 index c2a85e36d6..0000000000 --- a/tests/lean/run/blast_cc9.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq1.lean b/tests/lean/run/blast_cc_heq1.lean deleted file mode 100644 index b65331cf19..0000000000 --- a/tests/lean/run/blast_cc_heq1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq2.lean b/tests/lean/run/blast_cc_heq2.lean deleted file mode 100644 index eb019dc2f0..0000000000 --- a/tests/lean/run/blast_cc_heq2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq3.lean b/tests/lean/run/blast_cc_heq3.lean deleted file mode 100644 index 930d36c4eb..0000000000 --- a/tests/lean/run/blast_cc_heq3.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq4.lean b/tests/lean/run/blast_cc_heq4.lean deleted file mode 100644 index 90fa99ee99..0000000000 --- a/tests/lean/run/blast_cc_heq4.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq5.lean b/tests/lean/run/blast_cc_heq5.lean deleted file mode 100644 index 1ac090e7ca..0000000000 --- a/tests/lean/run/blast_cc_heq5.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq6.lean b/tests/lean/run/blast_cc_heq6.lean deleted file mode 100644 index 884802b263..0000000000 --- a/tests/lean/run/blast_cc_heq6.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq8.lean b/tests/lean/run/blast_cc_heq8.lean deleted file mode 100644 index cf7fcd20ec..0000000000 --- a/tests/lean/run/blast_cc_heq8.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_heq9.lean b/tests/lean/run/blast_cc_heq9.lean deleted file mode 100644 index c3627d55b6..0000000000 --- a/tests/lean/run/blast_cc_heq9.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_missed.lean b/tests/lean/run/blast_cc_missed.lean deleted file mode 100644 index fe826178de..0000000000 --- a/tests/lean/run/blast_cc_missed.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_noconfusion.lean b/tests/lean/run/blast_cc_noconfusion.lean deleted file mode 100644 index 3401375f89..0000000000 --- a/tests/lean/run/blast_cc_noconfusion.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_subsingleton1.lean b/tests/lean/run/blast_cc_subsingleton1.lean deleted file mode 100644 index 020ba1bf96..0000000000 --- a/tests/lean/run/blast_cc_subsingleton1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_cc_subsingleton2.lean b/tests/lean/run/blast_cc_subsingleton2.lean deleted file mode 100644 index bb49969b7a..0000000000 --- a/tests/lean/run/blast_cc_subsingleton2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_congr_bug.lean b/tests/lean/run/blast_congr_bug.lean deleted file mode 100644 index 1961d0522e..0000000000 --- a/tests/lean/run/blast_congr_bug.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_discr_tree_annot_bug.lean b/tests/lean/run/blast_discr_tree_annot_bug.lean deleted file mode 100644 index ab4d8188bb..0000000000 --- a/tests/lean/run/blast_discr_tree_annot_bug.lean +++ /dev/null @@ -1,5 +0,0 @@ -exit -constants (P : ℕ → Prop) (Q : Prop) -lemma foo [intro!] [forward] : (: P 0 :) → Q := sorry -example : P 0 → Q := -by grind diff --git a/tests/lean/run/blast_discr_tree_bug.lean b/tests/lean/run/blast_discr_tree_bug.lean deleted file mode 100644 index 85a1cd6458..0000000000 --- a/tests/lean/run/blast_discr_tree_bug.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch1.lean b/tests/lean/run/blast_ematch1.lean deleted file mode 100644 index 46fd99f5c4..0000000000 --- a/tests/lean/run/blast_ematch1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch10.lean b/tests/lean/run/blast_ematch10.lean deleted file mode 100644 index 73dc1db87d..0000000000 --- a/tests/lean/run/blast_ematch10.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch2.lean b/tests/lean/run/blast_ematch2.lean deleted file mode 100644 index affa4288f9..0000000000 --- a/tests/lean/run/blast_ematch2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch3.lean b/tests/lean/run/blast_ematch3.lean deleted file mode 100644 index 2721418397..0000000000 --- a/tests/lean/run/blast_ematch3.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch4.lean b/tests/lean/run/blast_ematch4.lean deleted file mode 100644 index 80786faed1..0000000000 --- a/tests/lean/run/blast_ematch4.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch5.lean b/tests/lean/run/blast_ematch5.lean deleted file mode 100644 index 4fb2531bd6..0000000000 --- a/tests/lean/run/blast_ematch5.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch6.lean b/tests/lean/run/blast_ematch6.lean deleted file mode 100644 index 124a974f4f..0000000000 --- a/tests/lean/run/blast_ematch6.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch8.lean b/tests/lean/run/blast_ematch8.lean deleted file mode 100644 index 752c05207b..0000000000 --- a/tests/lean/run/blast_ematch8.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch9.lean b/tests/lean/run/blast_ematch9.lean deleted file mode 100644 index 86ba7e1461..0000000000 --- a/tests/lean/run/blast_ematch9.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_cast1.lean b/tests/lean/run/blast_ematch_cast1.lean deleted file mode 100644 index 5ababe724e..0000000000 --- a/tests/lean/run/blast_ematch_cast1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_cast2.lean b/tests/lean/run/blast_ematch_cast2.lean deleted file mode 100644 index 8d90a35aaa..0000000000 --- a/tests/lean/run/blast_ematch_cast2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_cast3.lean b/tests/lean/run/blast_ematch_cast3.lean deleted file mode 100644 index 1cfd86eacc..0000000000 --- a/tests/lean/run/blast_ematch_cast3.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_heq1.lean b/tests/lean/run/blast_ematch_heq1.lean deleted file mode 100644 index f4d72e6e03..0000000000 --- a/tests/lean/run/blast_ematch_heq1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_heq2.lean b/tests/lean/run/blast_ematch_heq2.lean deleted file mode 100644 index 9ca400acd5..0000000000 --- a/tests/lean/run/blast_ematch_heq2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_heq3.lean b/tests/lean/run/blast_ematch_heq3.lean deleted file mode 100644 index 36215473fc..0000000000 --- a/tests/lean/run/blast_ematch_heq3.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_heq4.lean b/tests/lean/run/blast_ematch_heq4.lean deleted file mode 100644 index 39607cdb89..0000000000 --- a/tests/lean/run/blast_ematch_heq4.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_list.lean b/tests/lean/run/blast_ematch_list.lean deleted file mode 100644 index 62517f848f..0000000000 --- a/tests/lean/run/blast_ematch_list.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_ss1.lean b/tests/lean/run/blast_ematch_ss1.lean deleted file mode 100644 index 2b852385db..0000000000 --- a/tests/lean/run/blast_ematch_ss1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_sum.lean b/tests/lean/run/blast_ematch_sum.lean deleted file mode 100644 index d74091e83b..0000000000 --- a/tests/lean/run/blast_ematch_sum.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_ematch_uni_issue.lean b/tests/lean/run/blast_ematch_uni_issue.lean deleted file mode 100644 index 4735ea6199..0000000000 --- a/tests/lean/run/blast_ematch_uni_issue.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_equiv_tests.lean b/tests/lean/run/blast_equiv_tests.lean deleted file mode 100644 index bbecee5271..0000000000 --- a/tests/lean/run/blast_equiv_tests.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_flat.lean b/tests/lean/run/blast_flat.lean deleted file mode 100644 index 9f91c5940e..0000000000 --- a/tests/lean/run/blast_flat.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_fun_info_bug.lean b/tests/lean/run/blast_fun_info_bug.lean deleted file mode 100644 index 66ed44f257..0000000000 --- a/tests/lean/run/blast_fun_info_bug.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_grind1.lean b/tests/lean/run/blast_grind1.lean deleted file mode 100644 index 0624d1cc74..0000000000 --- a/tests/lean/run/blast_grind1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_meta.lean b/tests/lean/run/blast_meta.lean deleted file mode 100644 index 973cc062c0..0000000000 --- a/tests/lean/run/blast_meta.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_meta_bug.lean b/tests/lean/run/blast_meta_bug.lean deleted file mode 100644 index 74a4198e35..0000000000 --- a/tests/lean/run/blast_meta_bug.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_multiple_nots.lean b/tests/lean/run/blast_multiple_nots.lean deleted file mode 100644 index cf14cb860b..0000000000 --- a/tests/lean/run/blast_multiple_nots.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_pattern_inference_bug.lean b/tests/lean/run/blast_pattern_inference_bug.lean deleted file mode 100644 index d76b30d335..0000000000 --- a/tests/lean/run/blast_pattern_inference_bug.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_rec_eq.lean b/tests/lean/run/blast_rec_eq.lean deleted file mode 100644 index 4dbf8df1b4..0000000000 --- a/tests/lean/run/blast_rec_eq.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_recursor1.lean b/tests/lean/run/blast_recursor1.lean deleted file mode 100644 index 98326b24b0..0000000000 --- a/tests/lean/run/blast_recursor1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp1.lean b/tests/lean/run/blast_simp1.lean deleted file mode 100644 index f955883f45..0000000000 --- a/tests/lean/run/blast_simp1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp2.lean b/tests/lean/run/blast_simp2.lean deleted file mode 100644 index c45d199776..0000000000 --- a/tests/lean/run/blast_simp2.lean +++ /dev/null @@ -1,5 +0,0 @@ -exit -definition tst1 (a b : Prop) : a ∧ b ∧ true → b ∧ a := -by simp - -print tst1 diff --git a/tests/lean/run/blast_simp3.lean b/tests/lean/run/blast_simp3.lean deleted file mode 100644 index 422360f5ab..0000000000 --- a/tests/lean/run/blast_simp3.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp4.lean b/tests/lean/run/blast_simp4.lean deleted file mode 100644 index 919a550e87..0000000000 --- a/tests/lean/run/blast_simp4.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp5.lean b/tests/lean/run/blast_simp5.lean deleted file mode 100644 index ba4a521a2c..0000000000 --- a/tests/lean/run/blast_simp5.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp_st1.lean b/tests/lean/run/blast_simp_st1.lean deleted file mode 100644 index e0841d7e8e..0000000000 --- a/tests/lean/run/blast_simp_st1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp_subsingleton.lean b/tests/lean/run/blast_simp_subsingleton.lean deleted file mode 100644 index 57cd0143f5..0000000000 --- a/tests/lean/run/blast_simp_subsingleton.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp_subsingleton2.lean b/tests/lean/run/blast_simp_subsingleton2.lean deleted file mode 100644 index ea98911750..0000000000 --- a/tests/lean/run/blast_simp_subsingleton2.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_simp_sum.lean b/tests/lean/run/blast_simp_sum.lean deleted file mode 100644 index b0b884f8ff..0000000000 --- a/tests/lean/run/blast_simp_sum.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_trace.lean b/tests/lean/run/blast_trace.lean deleted file mode 100644 index d4a7c5ad21..0000000000 --- a/tests/lean/run/blast_trace.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_tuple1.lean b/tests/lean/run/blast_tuple1.lean deleted file mode 100644 index 6ab5f07e77..0000000000 --- a/tests/lean/run/blast_tuple1.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_unit.lean b/tests/lean/run/blast_unit.lean deleted file mode 100644 index de36aa73d9..0000000000 --- a/tests/lean/run/blast_unit.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_unit_cc.lean b/tests/lean/run/blast_unit_cc.lean deleted file mode 100644 index 7f199e5e14..0000000000 --- a/tests/lean/run/blast_unit_cc.lean +++ /dev/null @@ -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 --/ diff --git a/tests/lean/run/blast_unit_dep.lean b/tests/lean/run/blast_unit_dep.lean deleted file mode 100644 index b7950da772..0000000000 --- a/tests/lean/run/blast_unit_dep.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_unit_edges.lean b/tests/lean/run/blast_unit_edges.lean deleted file mode 100644 index a2d84591bc..0000000000 --- a/tests/lean/run/blast_unit_edges.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_unit_preprocess.lean b/tests/lean/run/blast_unit_preprocess.lean deleted file mode 100644 index 7b226829e4..0000000000 --- a/tests/lean/run/blast_unit_preprocess.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/blast_vector_test.lean b/tests/lean/run/blast_vector_test.lean deleted file mode 100644 index bd936eefef..0000000000 --- a/tests/lean/run/blast_vector_test.lean +++ /dev/null @@ -1,97 +0,0 @@ -exit -import data.nat -open nat - -lemma addl_eq_add [simp] (n m : nat) : (:n ⊕ m:) = n + m := -!add_eq_addl - --- Casting notation -notation `⟨`:max a `⟩`:0 := cast (by inst_simp) a - -inductive vector (A : Type) : nat → Type := -| nil {} : vector A zero -| cons : Π {n}, A → vector A n → vector A (succ n) - -namespace vector - -notation a :: b := cons a b -notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l - -variable {A : Type} - -private definition append_aux : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m) -| 0 m [] w := w -| (succ n) m (a::v) w := a :: (append_aux v w) - -theorem append_aux_nil_left [simp] {n : nat} (v : vector A n) : append_aux [] v == v := -!heq.refl - -theorem append_aux_cons [simp] {n m : nat} (h : A) (t : vector A n) (v : vector A m) : append_aux (h::t) v == h :: (append_aux t v) := -!heq.refl - -definition append {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) := -⟨append_aux v w⟩ - -section - -theorem append_nil_left [simp] {n : nat} (v : vector A n) : append [] v == v := -by unfold append ; inst_simp - -theorem append_cons [simp] {n m : nat} (h : A) (t : vector A n) (v : vector A m) : (: append (h::t) v :) == (: h::(append t v) :) := -by unfold append ; inst_simp -end - -theorem append_nil_right [simp] {n : nat} (v : vector A n) : append v [] == v := -by rec_inst_simp - -attribute succ_add [simp] - -theorem append_assoc [simp] {n₁ n₂ n₃ : nat} (v₁ : vector A n₁) (v₂ : vector A n₂) (v₃ : vector A n₃) : append v₁ (append v₂ v₃) == append (append v₁ v₂) v₃ := -by rec_inst_simp - -definition concat : Π {n : nat}, vector A n → A → vector A (succ n) -| concat [] a := [a] -| concat (b::v) a := b :: concat v a - -theorem concat_nil [simp] (a : A) : concat [] a = [a] := -rfl - -theorem concat_cons [simp] {n : nat} (b : A) (v : vector A n) (a : A) : concat (b :: v) a = b :: concat v a := -rfl - -definition reverse : Π {n : nat}, vector A n → vector A n -| 0 [] := [] -| (n+1) (x :: xs) := concat (reverse xs) x - -theorem reverse_nil [simp] : reverse [] = @nil A := -rfl - -theorem reverse_cons [simp] {n : nat} (a : A) (v : vector A n) : reverse (a::v) = concat (reverse v) a := -rfl - -theorem reverse_concat [simp] : ∀ {n : nat} (xs : vector A n) (a : A), reverse (concat xs a) = a :: reverse xs := -by rec_inst_simp - -theorem reverse_reverse [simp] : ∀ {n : nat} (xs : vector A n), reverse (reverse xs) = xs := -by rec_inst_simp - -theorem append_reverse_cons [simp] {n : nat} (v : vector A n) : ∀ (m : ℕ) (w : vector A m) (a : A), - append v (reverse (cons a w)) == concat (append v (reverse w)) a := -by induction v; inst_simp; inst_simp - -theorem reverse_append [simp] : ∀ {n m : nat} (v : vector A n) (w : vector A m), - reverse (append v w) == append (reverse w) (reverse v) := -by rec_inst_simp - -definition vplus : Π {n : ℕ} (v₁ v₂ : vector ℕ n), vector ℕ n -| nat.zero [] [] := [] -| (nat.succ m) (x::xs) (y::ys) := (x + y) :: vplus xs ys - -lemma vplus.def1 [simp] : vplus [] [] = @nil ℕ := rfl -lemma vplus.def2 [simp] {n : ℕ} (v₁ v₂ : vector ℕ n) (a₁ a₂ : ℕ) : (: vplus (a₁ :: v₁) (a₂ :: v₂) :) = (a₁ + a₂) :: vplus v₁ v₂ := rfl - -lemma vplus_weird {n₁ n₂ : ℕ} (v₁ : vector ℕ n₁) (v₂ : vector ℕ n₂) (a b : ℕ) : - vplus (a :: append v₁ v₂) ⟨b :: append v₂ v₁⟩ == (a + b) :: vplus (append v₁ v₂) ⟨append v₂ v₁⟩ := - by inst_simp - -end vector diff --git a/tests/lean/run/eassumption.lean b/tests/lean/run/eassumption.lean deleted file mode 100644 index 9b2a9284d0..0000000000 --- a/tests/lean/run/eassumption.lean +++ /dev/null @@ -1,7 +0,0 @@ -exit -variable p : nat → Prop -variable q : nat → Prop -variables a b c : nat - -example : p c → p b → q b → p a → ∃ x, p x ∧ q x := -by blast diff --git a/tests/lean/run/flycheck_blast_cc_heq7.lean b/tests/lean/run/flycheck_blast_cc_heq7.lean deleted file mode 100644 index 504445efe9..0000000000 --- a/tests/lean/run/flycheck_blast_cc_heq7.lean +++ /dev/null @@ -1,6 +0,0 @@ -exit -set_option blast.cc.heq true - -set_option trace.app_builder true -definition t3 (a b : nat) : (a = b) == (b = a) := -by blast diff --git a/tests/lean/run/simplifier1.lean b/tests/lean/run/simplifier1.lean deleted file mode 100644 index f507a2f5e5..0000000000 --- a/tests/lean/run/simplifier1.lean +++ /dev/null @@ -1,12 +0,0 @@ -exit -constant P : Type₁ -constant P_sub : subsingleton P -attribute P_sub [instance] -constant q : P → nat → Prop - -set_option blast.simp false -set_option trace.blast true -set_option trace.cc true - -example (a : nat) (h₁ h₂ : P) : q h₁ a = q h₂ a := -by blast