From 5626431c7f4ac5d37491f36f8b11587bc405cc3d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Dec 2015 14:35:14 -0800 Subject: [PATCH] test(tests/lean/run): use 'simp' when testing the simplifier --- tests/lean/run/blast_simp1.lean | 12 ++++++------ tests/lean/run/blast_simp2.lean | 4 +--- tests/lean/run/blast_simp3.lean | 10 +--------- 3 files changed, 8 insertions(+), 18 deletions(-) diff --git a/tests/lean/run/blast_simp1.lean b/tests/lean/run/blast_simp1.lean index cb290d523..39fcb27eb 100644 --- a/tests/lean/run/blast_simp1.lean +++ b/tests/lean/run/blast_simp1.lean @@ -1,17 +1,17 @@ example (a b c : Prop) : a ∧ b ∧ c ↔ c ∧ b ∧ a := -by blast +by simp example (a b c : Prop) : a ∧ false ∧ c ↔ false := -by blast +by simp example (a b c : Prop) : a ∨ false ∨ b ↔ b ∨ a := -by blast +by simp example (a b c : Prop) : ¬ true ∨ false ∨ b ↔ b := -by blast +by simp example (a b c : Prop) : if true then a else b ↔ if false then b else a := -by blast +by simp example (a b : Prop) : a ∧ not a ↔ false := -by blast +by simp diff --git a/tests/lean/run/blast_simp2.lean b/tests/lean/run/blast_simp2.lean index 1839a8b73..adbd26971 100644 --- a/tests/lean/run/blast_simp2.lean +++ b/tests/lean/run/blast_simp2.lean @@ -1,6 +1,4 @@ -set_option blast.recursor false - definition tst1 (a b : Prop) : a ∧ b ∧ true → b ∧ a := -by blast +by simp print tst1 diff --git a/tests/lean/run/blast_simp3.lean b/tests/lean/run/blast_simp3.lean index c83b1dbb2..cbbb6b549 100644 --- a/tests/lean/run/blast_simp3.lean +++ b/tests/lean/run/blast_simp3.lean @@ -1,11 +1,3 @@ -set_option blast.simp false - example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ → (λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) := -by blast - -set_option blast.simp true - -example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ → - (λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) := -by blast +by simp