fix(library/blast/simplifier): remove unnecessary casts

src/library/blast/simplifier.cpp

@@ -50,7 +50,7 @@
 #define LEAN_DEFAULT_SIMPLIFY_FUSE false
 #endif
 #ifndef LEAN_DEFAULT_SIMPLIFY_NUMERALS
-#define LEAN_DEFAULT_SIMPLIFY_NUMERALS true
+#define LEAN_DEFAULT_SIMPLIFY_NUMERALS false
 #endif
 
 namespace lean {
@@ -198,6 +198,7 @@ class simplifier {
     }
 
     expr unfold_reducible_instances(expr const & e);
+    expr remove_unnecessary_casts(expr const & e);
 
     bool instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned num_emeta,
                             list<expr> const & emetas, list<bool> const & instances);
@@ -801,27 +802,59 @@ optional<result> simplifier::synth_congr(expr const & e, F && simp) {
     expr proof = congr_lemma->get_proof();
     expr type = congr_lemma->get_type();
     unsigned i = 0;
-    bool simplified = false;
+    bool has_proof = false;
+    bool has_cast = false;
     buffer<expr> locals;
     for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
             proof = mk_app(proof, args[i]);
             type = instantiate(binding_body(type), args[i]);
             if (ckind == congr_arg_kind::Eq) {
                 result r_arg = simp(args[i]);
-                if (r_arg.has_proof()) simplified = true;
+                if (r_arg.has_proof()) has_proof = true;
                 r_arg = finalize(r_arg);
                 proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
                 type = instantiate(binding_body(type), r_arg.get_new());
                 type = instantiate(binding_body(type), r_arg.get_proof());
+            } else if (ckind == congr_arg_kind::Cast) {
+                has_cast = true;
             }
             i++;
         });
     lean_assert(is_eq(type));
     buffer<expr> type_args;
     get_app_args(type, type_args);
-    expr & new_e = type_args[2];
+    expr e_new = remove_unnecessary_casts(type_args[2]);
-    if (simplified) return optional<result>(result(new_e, proof));
+    if (has_proof) return optional<result>(result(e_new, proof));
-    else return optional<result>(result(new_e));
+    else return optional<result>(result(e_new));
+}
+
+expr simplifier::remove_unnecessary_casts(expr const & e) {
+    buffer<expr> args;
+    expr f = get_app_args(e, args);
+    fun_info f_info = get_fun_info(f, args.size());
+    int i = -1;
+    for_each(f_info.get_params_info(), [&](param_info const & p_info) {
+            i++;
+            if (p_info.is_subsingleton()) {
+                while (is_constant(get_app_fn(args[i]))) {
+                    buffer<expr> cast_args;
+                    expr f_cast = get_app_args(args[i], cast_args);
+                    name n_f = const_name(f_cast);
+                    if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) {
+                        lean_assert(cast_args.size() == 6);
+                        expr major_premise = cast_args[5];
+                        expr f_major_premise = get_app_fn(major_premise);
+                        if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name())
+                            args[i] = cast_args[3];
+                        else
+                            return;
+                    } else {
+                        return;
+                    }
+                }
+            }
+        });
+    return mk_app(f, args);
 }
 
 /* Fusion */

tests/lean/simplifier10.lean

@@ -4,15 +4,14 @@ 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 (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))
-namespace tst
+
 attribute px true_iff [simp]
 attribute wxz [simp]
 attribute vzy [simp]
 attribute H [simp]
-end tst
 
-#simplify iff tst 0 P x
+#simplify iff env 0 P x
-#simplify iff tst 0 W x z
+#simplify iff env 0 W x z
-#simplify iff tst 0 V z y
+#simplify iff env 0 V z y
-#simplify iff tst 0 Q z y x
+#simplify iff env 0 Q z y x
-#simplify iff tst 0 V z y ↔ Q z y x
+#simplify iff env 0 V z y ↔ Q z y x

tests/lean/simplifier11.lean

@@ -13,7 +13,7 @@ attribute dec_b [instance]
 
 attribute if_congr [congr]
 
-#simplify eq if_congr 0 (ite b x y)
+#simplify eq env 0 (ite b x y)
 end if_congr
 
 namespace if_ctx_simp_congr
@@ -26,8 +26,8 @@ constants {A : Type} {b c : Prop} (dec_b : decidable b)
 attribute h_e [simp]
 
 attribute if_ctx_simp_congr [congr]
--- TODO(Daniel): lean_unreachable
+
-#simplify eq if_ctx_simp_congr 0 (ite b x y)
+#simplify eq env 0 (ite b x y)
 
 end if_ctx_simp_congr
 
@@ -43,7 +43,7 @@ constants {b c x y u v : Prop} (dec_b : decidable b) (dec_c : decidable c)
 
 attribute if_congr_prop [congr]
 
-#simplify iff if_congr_prop 0 (ite b x y)
+#simplify iff env 0 (ite b x y)
 end if_congr_prop
 
 namespace if_ctx_simp_congr_prop
@@ -56,7 +56,7 @@ constants (b c x y u v : Prop) (dec_b : decidable b)
  attribute h_e [simp]
 
 attribute if_ctx_simp_congr_prop [congr]
-#simplify iff if_ctx_simp_congr_prop 0 (ite b x y)
+#simplify iff env 0 (ite b x y)
 
 end if_ctx_simp_congr_prop
 
@@ -70,5 +70,5 @@ constants (b c x y u v : Prop) (dec_b : decidable b)
  attribute h_e [simp]
 
 attribute if_simp_congr_prop [congr]
-#simplify iff if_simp_congr_prop 0 (ite b x y)
+#simplify iff env 0 (ite b x y)
 end if_simp_congr_prop

tests/lean/simplifier13.lean

@@ -3,8 +3,7 @@ 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
+
--- TODO(Daniel): extra step? Similar to simplifier1.hlean
+#simplify eq env 0 c (f x x) (f y y) (g z) px py pz
-#simplify eq tst 0 c (f x x) (f y y) (g z) px py pz

tests/lean/simplifier13.lean.expected.out

@@ -1 +1 @@
-c (g x) (g y) (g z) (eq.rec px (Hfg x)) (eq.rec py (Hfg y)) (eq.rec pz (eq.refl (g z)))
+c (g x) (g y) (g z) (eq.rec px (Hfg x)) (eq.rec py (Hfg y)) pz

tests/lean/simplifier3.lean

@@ -7,13 +7,12 @@ 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 tst 2 (f x a)
+#simplify eq env 2 (f x a)
 
 end test_congr
 
@@ -23,9 +22,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 tst 2 (f x)
+#simplify eq env 2 (f x)
 end test_congr_fun

tests/lean/simplifier4.lean

@@ -8,12 +8,12 @@ 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))
 
-namespace tst attribute R_refl [refl] end tst
+attribute R_refl [refl]
-namespace tst attribute R_sym [symm] end tst
+attribute R_sym [symm]
-#simplify R tst 2 (f x) -- f x
+#simplify R env 2 (f x) -- f x
-namespace tst attribute R_trans [trans] end tst
+attribute R_trans [trans]
-#simplify R tst 2 (f x) -- f x
+#simplify R env 2 (f x) -- f x
-namespace tst attribute Hfxgy [simp] end tst
+attribute Hfxgy [simp]
-#simplify R tst 2 (f x) -- f x
+#simplify R env 2 (f x) -- f x
-namespace tst attribute Hgyhz [simp] end tst
+attribute Hgyhz [simp]
-#simplify R tst 2 (f x) -- f x
+#simplify R env 2 (f x) -- f x

tests/lean/simplifier4.lean.expected.out

@@ -1,4 +1,4 @@
-<refl>
+(refl): f x
-<refl>
+(refl): f x
 R (f x) (g y)
 R (f x) (h z)

tests/lean/simplifier5.lean

@@ -1,16 +1,16 @@
 /- Basic rewriting with iff with congr_iff -/
 import logic.connectives
 open nat
-namespace tst
+
-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]
+attribute not_true [simp]
-end tst
+
-#simplify iff tst 2 (@le nat nat_has_le 0 0) -- true
+#simplify iff env 2 (@le nat nat_has_le 0 0) -- true
-#simplify iff tst 2 (@le nat nat_has_le 0 1) -- true
+#simplify iff env 2 (@le nat nat_has_le 0 1) -- true
-#simplify iff tst 2 (@le nat nat_has_le 0 2) -- true
+#simplify iff env 2 (@le nat nat_has_le 0 2) -- true
-#simplify iff tst 2 (@lt nat nat_has_lt 0 0) -- false
+#simplify iff env 2 (@lt nat nat_has_lt 0 0) -- false
-#simplify iff tst 2 (@lt nat nat_has_lt 0 (succ 0)) -- true
+#simplify iff env 2 (@lt nat nat_has_lt 0 (succ 0)) -- true
-#simplify iff tst 2 (@lt nat nat_has_lt 1 (succ 1)) -- true
+#simplify iff env 2 (@lt nat nat_has_lt 1 (succ 1)) -- true
-#simplify iff tst 2 (@lt nat nat_has_lt 0 (succ (succ 0))) -- true
+#simplify iff env 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 env 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 env 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
+#simplify iff env 2 (@le nat nat_has_le 0 0 ↔ @lt nat nat_has_lt 0 0) -- false

tests/lean/simplifier6.lean

@@ -3,29 +3,28 @@ import logic.connectives logic.quantifiers
 
 namespace pi_congr1
 constants (p1 q1 p2 q2 p3 q3 : Prop) (H1 : p1 ↔ q1) (H2 : p2 ↔ q2) (H3 : p3 ↔ q3)
-namespace tst
+
 attribute congr_forall [congr]
 attribute congr_imp    [congr]
 attribute H1 [simp]
 attribute H2 [simp]
 attribute H3 [simp]
-end tst
 
-#simplify iff tst 1 p1 -- Broken?
+#simplify iff env 1 p1 -- Broken?
-#simplify iff tst 1 p1 →  p2
+#simplify iff env 1 p1 →  p2
-#simplify iff tst 1 p1 →  p2 → p3
+#simplify iff env 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)
-namespace tst
+attribute congr_forall [congr]
 attribute H [simp]
-end tst
+
 constant (x : T)
 
-#simplify iff tst 1 (∀ (x : T), P x)
+#simplify iff env 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 tst 2 (and P1 (iff P2 P3))
+#simplify iff env 2 (and P1 (and P2 P3))
+#simplify iff env 2 (and P1 (iff P2 P3))

tests/lean/simplifier8.lean

@@ -6,10 +6,9 @@ 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 tst 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))
+#simplify eq env 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))

tests/lean/simplifier9.lean

@@ -1,30 +1,28 @@
 -- 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)
 
 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 tst 0 ∀ (H : ∀ x, P x ↔ Q x), P x
+#simplify iff env 0 x = y →  x = y
-#simplify iff tst 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), P x
+#simplify iff env 0 T → x = y →  x = y
+#simplify iff env 0 ∀ z : T, x = z → x = y
+#simplify iff env 0 ∀ z : T, z = x → x = z
+#simplify iff env 0 ∀ (z w : T), x = y →  x = y
+#simplify iff env 0 ∀ (z w : T), x = y →  P x
 
-#simplify iff tst 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x
+#simplify iff env 0 ∀ (H : ∀ x, P x ↔ Q x), P x
-#simplify iff tst 0 (∀ (x : T), P x ↔ Q x) →  P x
+#simplify iff env 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), 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
+#simplify iff env 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x
+#simplify iff env 0 (∀ (x : T), P x ↔ Q x) →  P x
+#simplify iff env 0 (∀ (x : T), P x ↔ Q x) →  P x
+#simplify iff env 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) →  P x
+
+#simplify iff env 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) →  P x

tests/lean/simplifier_norm_num.lean

@@ -8,51 +8,51 @@ universe l
 constants (A : Type.{l}) (A_comm_ring : comm_ring A)
 attribute A_comm_ring [instance]
 
-#simplify eq 0 (0:A) + 1
+#simplify eq env 0 (0:A) + 1
-#simplify eq 0 (1:A) + 0
+#simplify eq env 0 (1:A) + 0
-#simplify eq 0 (1:A) + 1
+#simplify eq env 0 (1:A) + 1
-#simplify eq 0 (0:A) + 2
+#simplify eq env 0 (0:A) + 2
-#simplify eq 0 (1:A) + 2
+#simplify eq env 0 (1:A) + 2
-#simplify eq 0 (2:A) + 1
+#simplify eq env 0 (2:A) + 1
-#simplify eq 0 (3:A) + 1
+#simplify eq env 0 (3:A) + 1
-#simplify eq 0 (2:A) + 2
+#simplify eq env 0 (2:A) + 2
-#simplify eq 0 (4:A) + 1
+#simplify eq env 0 (4:A) + 1
-#simplify eq 0 (3:A) + 2
+#simplify eq env 0 (3:A) + 2
-#simplify eq 0 (2:A) + 3
+#simplify eq env 0 (2:A) + 3
-#simplify eq 0 (0:A) + 6
+#simplify eq env 0 (0:A) + 6
-#simplify eq 0 (3:A) + 3
+#simplify eq env 0 (3:A) + 3
-#simplify eq 0 (4:A) + 2
+#simplify eq env 0 (4:A) + 2
-#simplify eq 0 (5:A) + 1
+#simplify eq env 0 (5:A) + 1
-#simplify eq 0 (4:A) + 3
+#simplify eq env 0 (4:A) + 3
-#simplify eq 0 (1:A) + 6
+#simplify eq env 0 (1:A) + 6
-#simplify eq 0 (6:A) + 1
+#simplify eq env 0 (6:A) + 1
-#simplify eq 0 (5:A) + 28
+#simplify eq env 0 (5:A) + 28
-#simplify eq 0 (0 : A) + (2 + 3) + 7
+#simplify eq env 0 (0 : A) + (2 + 3) + 7
-#simplify eq 0 (70 : A) + (33 + 2)
+#simplify eq env 0 (70 : A) + (33 + 2)
 
-#simplify eq 0 (23000000000 : A) + 22000000000
+#simplify eq env 0 (23000000000 : A) + 22000000000
 
-#simplify eq 0 (0 : A) * 0
+#simplify eq env 0 (0 : A) * 0
-#simplify eq 0 (0 : A) * 1
+#simplify eq env 0 (0 : A) * 1
-#simplify eq 0 (0 : A) * 2
+#simplify eq env 0 (0 : A) * 2
-#simplify eq 0 (2 : A) * 0
+#simplify eq env 0 (2 : A) * 0
-#simplify eq 0 (1 : A) * 0
+#simplify eq env 0 (1 : A) * 0
-#simplify eq 0 (1 : A) * 1
+#simplify eq env 0 (1 : A) * 1
-#simplify eq 0 (2 : A) * 1
+#simplify eq env 0 (2 : A) * 1
-#simplify eq 0 (1 : A) * 2
+#simplify eq env 0 (1 : A) * 2
-#simplify eq 0 (2 : A) * 2
+#simplify eq env 0 (2 : A) * 2
-#simplify eq 0 (3 : A) * 2
+#simplify eq env 0 (3 : A) * 2
-#simplify eq 0 (2 : A) * 3
+#simplify eq env 0 (2 : A) * 3
-#simplify eq 0 (4 : A) * 1
+#simplify eq env 0 (4 : A) * 1
-#simplify eq 0 (1 : A) * 4
+#simplify eq env 0 (1 : A) * 4
-#simplify eq 0 (3 : A) * 3
+#simplify eq env 0 (3 : A) * 3
-#simplify eq 0 (3 : A) * 4
+#simplify eq env 0 (3 : A) * 4
-#simplify eq 0 (4 : A) * 4
+#simplify eq env 0 (4 : A) * 4
-#simplify eq 0 (11 : A) * 2
+#simplify eq env 0 (11 : A) * 2
-#simplify eq 0 (15 : A) * 6
+#simplify eq env 0 (15 : A) * 6
-#simplify eq 0 (123456 : A) * 123456
+#simplify eq env 0 (123456 : A) * 123456
 
-#simplify eq 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733)
+#simplify eq env 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733)
 
 -- The following test is too slow
 -- #simplify eq 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536