fix(tests/lean): some of the simplifier tests

library/init/nat.lean

@@ -154,6 +154,9 @@ namespace nat
 
   protected theorem lt_irrefl (n : ℕ) : ¬n < n := not_succ_le_self
 
+  theorem lt_self_iff_false (n : ℕ) : n < n ↔ false :=
+  iff_false_intro (λ H, absurd H (nat.lt_irrefl n))
+
   theorem self_lt_succ (n : ℕ) : n < succ n := !nat.le_refl
 
   theorem self_lt_succ_iff_true [simp] (n : ℕ) : n < succ n ↔ true :=

tests/lean/simplifier1.hlean

@@ -6,12 +6,12 @@ constants (T : Type.{l}) (x1 x2 x3 x4 x5 x6 : T) (f : T → T → T)
 constants (f_comm : ∀ x y, f x y = f y x)
           (f_l : ∀ x y z, f (f x y) z = f x (f y z))
           (f_r : ∀ x y z, f x (f y z) = f y (f x z))
-
+namespace tst
 attribute f_comm [simp]
 attribute f_l [simp]
 attribute f_r [simp]
-
+end tst
-#simplify eq 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))
+#simplify eq tst 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))
 
 open is_trunc
 
@@ -19,9 +19,9 @@ constants g : Π (x y : nat), x ≠ y → Type₁
 constants a b c : nat
 constants H₁ : a ≠ b
 constants H₂ : a = c
-attribute H₂ [simp]
+namespace tst attribute H₂ [simp] end tst
 
 definition ne_is_hprop [instance] (a b : nat) : is_hprop (a ≠ b) :=
 sorry
-
+-- TODO(Daniel): simplifier seems to have applied unnecessary step (see: (eq.nrec ... (eq.refl ..)))
-#simplify eq 0 (g a b H₁)
+#simplify eq tst 0 (g a b H₁)

tests/lean/simplifier1.lean

@@ -1,10 +1,10 @@
 /- Basic rewriting with eq without congruence or conditionals -/
 universe l
 constant T : Type.{l}
-constants (x y z : T) (f g h : T → T) 
+constants (x y z : T) (f g h : T → T)
 constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
 
-attribute Hfxgy [simp]
+namespace tst attribute Hfxgy [simp] end tst
-#simplify eq 2 (f x)
+#simplify eq tst 2 (f x)
-attribute Hgyhz [simp]
+namespace tst attribute Hgyhz [simp] end tst
-#simplify eq 2 (f x)
+#simplify eq tst 2 (f x)

tests/lean/simplifier10.lean

@@ -1,19 +1,18 @@
 import logic.connectives logic.quantifiers
 
 universe l
-constants (T : Type.{l}) (x y z : T) (P : T → Prop) (Q : T → T → T → Prop) (R W V : T → T → Prop) 
+constants (T : Type.{l}) (x y z : T) (P : T → Prop) (Q : T → T → T → Prop) (R W V : T → T → Prop)
 constants (px : P x) (wxz : W x z) (vzy : V z y)
 constants (H : ∀ (x y z : T), P x → W x z → V z y → (Q z y x ↔ R x y))
-attribute px [simp]
+namespace tst
+attribute px true_iff [simp]
 attribute wxz [simp]
 attribute vzy [simp]
 attribute H [simp]
+end tst
 
-#simplify iff 0 P x
+#simplify iff tst 0 P x
-#simplify iff 0 W x z
+#simplify iff tst 0 W x z
-#simplify iff 0 V z y
+#simplify iff tst 0 V z y
-#simplify iff 0 Q z y x
+#simplify iff tst 0 Q z y x
-#simplify iff 0 V z y ↔ Q z y x
+#simplify iff tst 0 V z y ↔ Q z y x
-
-
-

tests/lean/simplifier11.lean

@@ -5,29 +5,29 @@ namespace if_congr
 constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c)
           {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v)
 
-local attribute dec_b [instance]
+attribute dec_b [instance]
-local attribute dec_c [instance]
+ attribute dec_c [instance]
-local attribute h_c [simp]
+ attribute h_c [simp]
-local attribute h_t [simp]
+ attribute h_t [simp]
-local attribute h_e [simp]
+ attribute h_e [simp]
 
 attribute if_congr [congr]
 
-#simplify eq 0 (ite b x y)
+#simplify eq if_congr 0 (ite b x y)
 end if_congr
 
 namespace if_ctx_simp_congr
 constants {A : Type} {b c : Prop} (dec_b : decidable b)
           {x y u v : A} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v)
 
-local attribute dec_b [instance]
+ attribute dec_b [instance]
-local attribute h_c [simp]
+ attribute h_c [simp]
-local attribute h_t [simp]
+ attribute h_t [simp]
-local attribute h_e [simp]
+ attribute h_e [simp]
 
 attribute if_ctx_simp_congr [congr]
-
+-- TODO(Daniel): lean_unreachable
-#simplify eq 0 (ite b x y)
+#simplify eq if_ctx_simp_congr 0 (ite b x y)
 
 end if_ctx_simp_congr
 
@@ -35,28 +35,28 @@ namespace if_congr_prop
 constants {b c x y u v : Prop} (dec_b : decidable b) (dec_c : decidable c)
           (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v))
 
-local attribute dec_b [instance]
+ attribute dec_b [instance]
-local attribute dec_c [instance]
+ attribute dec_c [instance]
-local attribute h_c [simp]
+ attribute h_c [simp]
-local attribute h_t [simp]
+ attribute h_t [simp]
-local attribute h_e [simp]
+ attribute h_e [simp]
 
 attribute if_congr_prop [congr]
 
-#simplify iff 0 (ite b x y)
+#simplify iff if_congr_prop 0 (ite b x y)
 end if_congr_prop
 
 namespace if_ctx_simp_congr_prop
 constants (b c x y u v : Prop) (dec_b : decidable b)
           (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬ c → (y ↔ v))
 
-local attribute dec_b [instance]
+ attribute dec_b [instance]
-local attribute h_c [simp]
+ attribute h_c [simp]
-local attribute h_t [simp]
+ attribute h_t [simp]
-local attribute h_e [simp]
+ attribute h_e [simp]
 
 attribute if_ctx_simp_congr_prop [congr]
-#simplify iff 0 (ite b x y)
+#simplify iff if_ctx_simp_congr_prop 0 (ite b x y)
 
 end if_ctx_simp_congr_prop
 
@@ -64,11 +64,11 @@ namespace if_simp_congr_prop
 constants (b c x y u v : Prop) (dec_b : decidable b)
           (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v)
 
-local attribute dec_b [instance]
+ attribute dec_b [instance]
-local attribute h_c [simp]
+ attribute h_c [simp]
-local attribute h_t [simp]
+ attribute h_t [simp]
-local attribute h_e [simp]
+ attribute h_e [simp]
 
 attribute if_simp_congr_prop [congr]
-#simplify iff 0 (ite b x y)
+#simplify iff if_simp_congr_prop 0 (ite b x y)
 end if_simp_congr_prop

tests/lean/simplifier12.lean

@@ -7,4 +7,4 @@ constants (T : Type.{l}) (s : algebra.comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
 
-#simplify eq 0 x2 + (1 * g x1 + 0 + (f x3 * 3 * 1 * (x2 + 0 + g x1 * 7) * x2 * 1)) + 5 * (x4 + f x1)
+#simplify eq simplifier.som 0 x2 + (1 * g x1 + 0 + (f x3 * 3 * 1 * (x2 + 0 + g x1 * 7) * x2 * 1)) + 5 * (x4 + f x1)

tests/lean/simplifier13.lean

@@ -3,7 +3,8 @@ constants (T : Type.{l}) (f : T →  T → T) (g : T → T)
 constants (P : T → Prop) (Q : Prop) (Hfg : ∀ (x : T), f x x = g x)
 constants (c : Π (x y z : T), P x → P y → P z → Q)
 constants (x y z : T) (px : P (f x x)) (py : P (f y y)) (pz : P (g z))
-
+namespace tst
 attribute Hfg [simp]
-
+end tst
-#simplify eq 0 c (f x x) (f y y) (g z) px py pz
+-- TODO(Daniel): extra step? Similar to simplifier1.hlean
+#simplify eq tst 0 c (f x x) (f y y) (g z) px py pz

tests/lean/simplifier14.lean.expected.out

@@ -1 +1,18 @@
-TODO
+(refl): x1
+x1 * 2
+x1 * 3
+x1 * 4
+x1 * 4
+x1 * 5
+x1 * (1 + -1)
+x1 * (1 + (1 + -1))
+x1 * (1 + (1 + -2))
+x1 * (1 + (1 + (-1 + -1)))
+x1 * 5
+x2 * (1 + -1) + x1 * (1 + -1)
+x2 * (1 + (1 + -2)) + x1 * (1 + (1 + (1 + -3)))
+x1 * 2 + x2 * (1 + -1)
+x2 * 2 + (x1 * 3 + x2 * x1 * (1 + (1 + -32)))
+x1 + (-0 + x3 * x2 * (3 + -2))
+x1 * 2 + (x3 * x2 * 3 + (x3 * x1 * (1 + -3) + x2 * x1 * (1 + (1 + -2))))
+x1 * 2 + x2 * (1 + -1)

tests/lean/simplifier2.lean

@@ -1,11 +1,10 @@
 /- Basic rewriting with eq and lambda without congruence or conditionals -/
 universe l
 constant T : Type.{l}
-constants (x y z : T) (f g h : T → T) 
+constants (x y z : T) (f g h : T → T)
 constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
 
-attribute Hfxgy [simp]
+namespace tst attribute Hfxgy [simp] end tst
-#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), g y
+#simplify eq tst 0 (λ a b c : bool, f x) -- λ (a b c : bool), g y
-attribute Hgyhz [simp]
+namespace tst attribute Hgyhz [simp] end tst
-#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), h z
+#simplify eq tst 0 (λ a b c : bool, f x) -- λ (a b c : bool), h z
-

tests/lean/simplifier3.lean

@@ -7,13 +7,13 @@ constant T : Type.{l}
 constants (x y z : T → T) (f g h : (T →  T) → (T →  T)) (a b c : T)
 constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) (Hab : a = b) (Hbc : b = c)
 
-
+namespace tst
 attribute Hfxgy [simp]
 attribute Hgyhz [simp]
 attribute Hab [simp]
 attribute Hbc [simp]
-
+end tst
-#simplify eq 2 (f x a)
+#simplify eq tst 2 (f x a)
 
 end test_congr
 
@@ -23,9 +23,9 @@ universes l1 l2
 constants (T : Type.{l1}) (U : T → Type.{l2})
 constants (f g : Π (x:T), U x) (x y : T)
 constants (Hfg : f = g) (Hxy : x = y)
-
+namespace tst
 attribute Hfg [simp]
 attribute Hxy [simp]
-
+end tst
-#simplify eq 2 (f x)
+#simplify eq tst 2 (f x)
 end test_congr_fun

tests/lean/simplifier4.lean

@@ -3,17 +3,17 @@ import logic.connectives data.nat
 
 universe l
 constant T : Type.{l}
-constants (x y z : T) (f g h : T → T) 
+constants (x y z : T) (f g h : T → T)
-constants (R : T → T → Prop) 
+constants (R : T → T → Prop)
 constants (R_refl : ∀ x, R x x) (R_sym : ∀ x y, R x y →  R y x) (R_trans : ∀ x y z, R x y → R y z → R x z)
 constants (Hfxgy : R (f x) (g y)) (Hgyhz : R (g y) (h z))
 
-attribute R_refl [refl]
+namespace tst attribute R_refl [refl] end tst
-attribute R_sym [symm]
+namespace tst attribute R_sym [symm] end tst
-#simplify R 2 (f x) -- f x
+#simplify R tst 2 (f x) -- f x
-attribute R_trans [trans]
+namespace tst attribute R_trans [trans] end tst
-#simplify R 2 (f x) -- f x
+#simplify R tst 2 (f x) -- f x
-attribute Hfxgy [simp]
+namespace tst attribute Hfxgy [simp] end tst
-#simplify R 2 (f x) -- f x
+#simplify R tst 2 (f x) -- f x
-attribute Hgyhz [simp]
+namespace tst attribute Hgyhz [simp] end tst
-#simplify R 2 (f x) -- f x
+#simplify R tst 2 (f x) -- f x

tests/lean/simplifier5.lean

@@ -1,13 +1,16 @@
 /- Basic rewriting with iff with congr_iff -/
 import logic.connectives
 open nat
-#simplify iff 2 (@le nat nat_has_le 0 0) -- true
+namespace tst
-#simplify iff 2 (@le nat nat_has_le 0 1) -- true
+attribute iff_self true_iff_false self_lt_succ_iff_true zero_lt_succ_iff_true zero_le_iff_true succ_le_self_iff_false succ_le_self_iff_false lt_self_iff_false [simp]
-#simplify iff 2 (@le nat nat_has_le 0 2) -- true
+end tst
-#simplify iff 2 (@lt nat nat_has_lt 0 0) -- false
+#simplify iff tst 2 (@le nat nat_has_le 0 0) -- true
-#simplify iff 2 (@lt nat nat_has_lt 0 (succ 0)) -- true
+#simplify iff tst 2 (@le nat nat_has_le 0 1) -- true
-#simplify iff 2 (@lt nat nat_has_lt 1 (succ 1)) -- true
+#simplify iff tst 2 (@le nat nat_has_le 0 2) -- true
-#simplify iff 2 (@lt nat nat_has_lt 0 (succ (succ 0))) -- true
+#simplify iff tst 2 (@lt nat nat_has_lt 0 0) -- false
-#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 0) -- true
+#simplify iff tst 2 (@lt nat nat_has_lt 0 (succ 0)) -- true
-#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 1) -- true
+#simplify iff tst 2 (@lt nat nat_has_lt 1 (succ 1)) -- true
-#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @lt nat nat_has_lt 0 0) -- false
+#simplify iff tst 2 (@lt nat nat_has_lt 0 (succ (succ 0))) -- true
+#simplify iff tst 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 0) -- true
+#simplify iff tst 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 1) -- true
+#simplify iff tst 2 (@le nat nat_has_le 0 0 ↔ @lt nat nat_has_lt 0 0) -- false

tests/lean/simplifier6.lean

@@ -1,28 +1,31 @@
 /- Basic pi congruence -/
 import logic.connectives logic.quantifiers
 
-attribute congr_forall [congr]
-attribute congr_imp [congr]
-
 namespace pi_congr1
 constants (p1 q1 p2 q2 p3 q3 : Prop) (H1 : p1 ↔ q1) (H2 : p2 ↔ q2) (H3 : p3 ↔ q3)
-local attribute H1 [simp]
+namespace tst
-local attribute H2 [simp]
+attribute congr_forall [congr]
-local attribute H3 [simp]
+attribute congr_imp    [congr]
+attribute H1 [simp]
+attribute H2 [simp]
+attribute H3 [simp]
+end tst
 
-#simplify iff 1 p1
+#simplify iff tst 1 p1 -- Broken?
-#simplify iff 1 p1 →  p2
+#simplify iff tst 1 p1 →  p2
-#simplify iff 1 p1 →  p2 → p3
+#simplify iff tst 1 p1 →  p2 → p3
 
 end pi_congr1
 
 namespace pi_congr2
 universe l
 constants (T : Type.{l}) (P Q : T → Prop) (H : ∀ (x : T), P x ↔ Q x)
-local attribute H [simp]
+namespace tst
+attribute H [simp]
+end tst
 constant (x : T)
 
-#simplify iff 1 (∀ (x : T), P x)
+#simplify iff tst 1 (∀ (x : T), P x)
 
 
 end pi_congr2

tests/lean/simplifier7.lean

@@ -4,13 +4,13 @@ import logic.connectives
 constants (P1 Q1 P2 Q2 P3 Q3 : Prop) (H1 : P1 ↔ Q1) (H2 : P2 ↔ Q2) (H3 : P3 ↔ Q3)
 constants (f g : Prop → Prop → Prop)
 constants (Hf : and = f) (Hg : f = g)
-
+namespace tst
 attribute H1 [simp]
 attribute H2 [simp]
 attribute H3 [simp]
 attribute Hf [simp]
 attribute Hg [simp]
+end tst
 
-
+#simplify iff tst 2 (and P1 (and P2 P3))
-#simplify iff 2 (and P1 (and P2 P3))
+#simplify iff tst 2 (and P1 (iff P2 P3))
-#simplify iff 2 (and P1 (iff P2 P3))

tests/lean/simplifier8.lean

@@ -6,8 +6,10 @@ constants (f_comm : ∀ x y, f x y = f y x)
           (f_l : ∀ x y z, f (f x y) z = f x (f y z))
           (f_r : ∀ x y z, f x (f y z) = f y (f x z))
 
+namespace tst
 attribute f_comm [simp]
 attribute f_l [simp]
 attribute f_r [simp]
+end tst
 
-#simplify eq 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))
+#simplify eq tst 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))

tests/lean/simplifier9.lean

@@ -1,30 +1,30 @@
 -- Rewriting with (tmp)-local hypotheses
 import logic.quantifiers
 
+namespace tst
 attribute congr_forall [congr]
 attribute congr_imp [congr]
+end tst
 
 universe l
-constants (T : Type.{l}) (P Q : T → Prop) 
+constants (T : Type.{l}) (P Q : T → Prop)
 
 set_option simplify.max_steps 50000
 constants (x y : T)
+-- TODO(Daniel): the following is looping...
+#simplify iff tst 0 x = y →  x = y
+#simplify iff tst 0 T → x = y →  x = y
+#simplify iff tst 0 ∀ z : T, x = z → x = y
+#simplify iff tst 0 ∀ z : T, z = x → x = z
+#simplify iff tst 0 ∀ (z w : T), x = y →  x = y
+#simplify iff tst 0 ∀ (z w : T), x = y →  P x
 
-#simplify iff 0 x = y →  x = y
+#simplify iff tst 0 ∀ (H : ∀ x, P x ↔ Q x), P x
-#simplify iff 0 T → x = y →  x = y
+#simplify iff tst 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), P x
-#simplify iff 0 ∀ z : T, x = z → x = y
-#simplify iff 0 ∀ z : T, z = x → x = z
-#simplify iff 0 ∀ (z w : T), x = y →  x = y
-#simplify iff 0 ∀ (z w : T), x = y →  P x
-
-#simplify iff 0 ∀ (H : ∀ x, P x ↔ Q x), P x
-#simplify iff 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), P x
-
-#simplify iff 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x
-#simplify iff 0 (∀ (x : T), P x ↔ Q x) →  P x
-#simplify iff 0 (∀ (x : T), P x ↔ Q x) →  P x
-#simplify iff 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) →  P x
-
-#simplify iff 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) →  P x
 
+#simplify iff tst 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x
+#simplify iff tst 0 (∀ (x : T), P x ↔ Q x) →  P x
+#simplify iff tst 0 (∀ (x : T), P x ↔ Q x) →  P x
+#simplify iff tst 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) →  P x
 
+#simplify iff tst 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) →  P x