refactor(library/tactic/simplify): delete old simplifier

library/init/congr.lean

@@ -14,3 +14,6 @@ propext (forall_congr (λ a, (h a)^.to_iff))
 
 lemma imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=
 propext (imp_congr h₁^.to_iff h₂^.to_iff)
+
+lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → (b = d)) : (a → b) = (c → d) :=
+propext (imp_congr_ctx h₁^.to_iff (λ hc, (h₂ hc)^.to_iff))

library/init/default.lean

@@ -7,9 +7,9 @@ prelude
 import init.core init.logic
 import init.relation init.nat init.prod init.sum init.combinator
 import init.bool init.unit init.num init.sigma init.setoid init.quot
-import init.funext init.function init.subtype init.classical
+import init.funext init.function init.subtype init.classical init.congr
 import init.monad init.option init.state init.fin init.list init.char init.string init.to_string
 import init.monad_combinators init.set
 import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
 import init.wf init.nat_div init.meta init.instances
-import init.sigma_lex init.simplifier init.id_locked init.order init.algebra
+import init.sigma_lex init.id_locked init.order init.algebra

library/init/meta/interactive.lean

@@ -268,33 +268,39 @@ do es ← to_expr_list hs,
    s₁ ← s₀^.append es,
    return $ simp_lemmas.erase s₁ ex
 
-private meta def simp_goal : simp_lemmas → tactic unit
+private meta def simp_goal (cfg : simplify_config) : simp_lemmas → tactic unit
 | s := do
-   (new_target, Heq) ← target >>= s^.simplify_core (simp_goal s) `eq,
+   (new_target, Heq) ← target >>= simplify_core cfg s `eq,
    tactic.assert `Htarget new_target, swap,
    Ht ← get_local `Htarget,
    mk_app `eq.mpr [Heq, Ht] >>= tactic.exact
 
-private meta def simp_hyp (s : simp_lemmas) (h_name : name) : tactic unit :=
+private meta def simp_hyp (cfg : simplify_config) (s : simp_lemmas) (h_name : name) : tactic unit :=
 do h     ← get_local h_name,
    htype ← infer_type h,
-   (new_htype, eqpr) ← s^.simplify_core (simp_goal s) `eq htype,
+   (new_htype, eqpr) ← simplify_core cfg s `eq htype,
    tactic.assert (expr.local_pp_name h) new_htype,
    mk_app `eq.mp [eqpr, h] >>= tactic.exact,
    try $ tactic.clear h
 
-private meta def simp_hyps : simp_lemmas → location → tactic unit
+private meta def simp_hyps (cfg : simplify_config) : simp_lemmas → location → tactic unit
 | s []      := skip
-| s (h::hs) := simp_hyp s h >> simp_hyps s hs
+| s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs
 
-meta def simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
+private meta def simp_core (cfg : simplify_config) (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
 do s ← mk_simp_set attr_names hs ids,
    match loc : _ → tactic unit with
-   | [] := simp_goal s
-   | _  := simp_hyps s loc
+   | [] := simp_goal cfg s
+   | _  := simp_hyps cfg s loc
    end,
    try tactic.triv, try tactic.reflexivity
 
+meta def simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
+simp_core default_simplify_config hs attr_names ids loc
+
+meta def ctx_simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit :=
+simp_core {default_simplify_config with contextual := tt} hs attr_names ids loc
+
 private meta def dsimp_hyps : location → tactic unit
 | []      := skip
 | (h::hs) := get_local h >>= dsimp_at

library/init/meta/simp_tactic.lean

@@ -54,16 +54,6 @@ meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr
 meta def simp_lemmas.drewrite : simp_lemmas → expr → tactic expr :=
 simp_lemmas.drewrite_core reducible
 
-/- Simplify the given expression using [simp] and [congr] lemmas.
-   The first argument is a tactic to be used to discharge proof obligations.
-   The second argument is the name of the relation to simplify over.
-   The third argument is a list of additional expressions to be considered as simp rules.
-   The fourth argument is the expression to be simplified.
-   The result is the simplified expression along with a proof that the new
-   expression is equivalent to the old one.
-   Fails if no simplifications can be performed. -/
-meta constant simp_lemmas.simplify_core : simp_lemmas → tactic unit → name → expr → tactic (expr × expr)
-
 /- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
    The resulting expression is definitionally equal to the input. -/
 meta constant simp_lemmas.dsimplify_core (max_steps : nat) (visit_instances : bool) : simp_lemmas → expr → tactic expr
@@ -204,23 +194,26 @@ meta constant ext_simplify_core
   (r : name) :
   expr → tactic (A × expr × expr)
 
-meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
+meta def simplify (cfg : simplify_config) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
 do lemmas       ← simp_lemmas.mk_default,
    new_lemmas   ← lemmas^.append extra_lemmas,
    e_type       ← infer_type e >>= whnf,
-   new_lemmas^.simplify_core prove_fn `eq e
+   simplify_core cfg new_lemmas `eq e
 
-meta def simplify_goal (prove_fn : tactic unit) (extra_lemmas : list expr) : tactic unit :=
-do (new_target, Heq) ← target >>= simplify prove_fn extra_lemmas,
+meta def simplify_goal (cfg : simplify_config) (extra_lemmas : list expr) : tactic unit :=
+do (new_target, Heq) ← target >>= simplify cfg extra_lemmas,
    assert `Htarget new_target, swap,
    Ht ← get_local `Htarget,
    mk_app `eq.mpr [Heq, Ht] >>= exact
 
 meta def simp : tactic unit :=
-simplify_goal failed [] >> try triv >> try reflexivity
+simplify_goal default_simplify_config [] >> try triv >> try reflexivity
 
 meta def simp_using (Hs : list expr) : tactic unit :=
-simplify_goal failed Hs >> try triv
+simplify_goal default_simplify_config Hs >> try triv
+
+meta def ctx_simp : tactic unit :=
+simplify_goal {default_simplify_config with contextual := tt} [] >> try triv >> try reflexivity
 
 meta def dsimp : tactic unit :=
 do S ← simp_lemmas.mk_default,
@@ -249,23 +242,23 @@ private meta def collect_eqs : list expr → tactic (list expr)
 meta def simp_using_hs : tactic unit :=
 local_context >>= collect_eqs >>= simp_using
 
-meta def simp_core_at (prove_fn : tactic unit) (extra_lemmas : list expr) (H : expr) : tactic unit :=
+meta def simp_core_at (extra_lemmas : list expr) (H : expr) : tactic unit :=
 do when (expr.is_local_constant H = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
    Htype ← infer_type H,
-   (new_Htype, Heq) ← simplify prove_fn extra_lemmas Htype,
+   (new_Htype, Heq) ← simplify default_simplify_config extra_lemmas Htype,
    assert (expr.local_pp_name H) new_Htype,
    mk_app `eq.mp [Heq, H] >>= exact,
    try $ clear H
 
 meta def simp_at : expr → tactic unit :=
-simp_core_at failed []
+simp_core_at []
 
 meta def simp_at_using (Hs : list expr) : expr → tactic unit :=
-simp_core_at failed Hs
+simp_core_at Hs
 
 meta def simp_at_using_hs (H : expr) : tactic unit :=
 do Hs ← local_context >>= collect_eqs,
-   simp_core_at failed (list.filter (ne H) Hs) H
+   simp_core_at (list.filter (ne H) Hs) H
 
 meta def mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) : tactic unit :=
 do (lhs, rhs)     ← target >>= match_eq,

library/init/simplifier.lean

@@ -1,41 +0,0 @@
-prelude
-import init.logic init.classical
-
-universe variables u
-
--- For n-ary support
-class is_associative {A : Type u} (op : A → A → A) :=
-(op_assoc : ∀ x y z : A, op (op x y) z = op x (op y z))
-
-instance : is_associative and :=
-is_associative.mk (λ x y z, propext (@and.assoc x y z))
-
-instance : is_associative or :=
-is_associative.mk (λ x y z, propext (@or.assoc x y z))
-
--- Basic congruence theorems over equality (using propext)
-attribute [congr]
-theorem imp_congr_ctx_eq {P₁ P₂ Q₁ Q₂ : Prop} (H₁ : P₁ = P₂) (H₂ : P₂ → (Q₁ = Q₂)) : (P₁ → Q₁) = (P₂ → Q₂) :=
-propext (imp_congr_ctx H₁^.to_iff (assume p₂, (H₂ p₂)^.to_iff))
-
--- Congruence theorems for flattening
-namespace simplifier
-variables {A : Type u}
-
-theorem congr_bin_op {op op' : A → A → A} (H : op = op') (x y : A) : op x y = op' x y :=
-congr_fun (congr_fun H x) y
-
-theorem congr_bin_arg1 {op : A → A → A} {x x' y : A} (Hx : x = x') : op x y = op x' y :=
-congr_fun (congr_arg op Hx) y
-
-theorem congr_bin_arg2 {op : A → A → A} {x y y' : A} (Hy : y = y') : op x y = op x y' :=
-congr_arg (op x) Hy
-
-theorem congr_bin_args {op : A → A → A} {x x' y y' : A} (Hx : x = x') (Hy : y = y') : op x y = op x' y' :=
-congr (congr_arg op Hx) Hy
-
-theorem assoc_subst {op op' : A → A → A} (H : op = op') (H_assoc : ∀ x y z, op (op x y) z = op x (op y z))
-  : (∀ x y z, op' (op' x y) z = op' x (op' y z)) :=
-H ▸ H_assoc
-
-end simplifier

src/library/constants.cpp

@@ -120,6 +120,8 @@ name const * g_iff_trans = nullptr;
 name const * g_iff_true_intro = nullptr;
 name const * g_imp_congr = nullptr;
 name const * g_imp_congr_eq = nullptr;
+name const * g_imp_congr_ctx = nullptr;
+name const * g_imp_congr_ctx_eq = nullptr;
 name const * g_implies = nullptr;
 name const * g_implies_of_if_neg = nullptr;
 name const * g_implies_of_if_pos = nullptr;
@@ -506,6 +508,8 @@ void initialize_constants() {
     g_iff_true_intro = new name{"iff_true_intro"};
     g_imp_congr = new name{"imp_congr"};
     g_imp_congr_eq = new name{"imp_congr_eq"};
+    g_imp_congr_ctx = new name{"imp_congr_ctx"};
+    g_imp_congr_ctx_eq = new name{"imp_congr_ctx_eq"};
     g_implies = new name{"implies"};
     g_implies_of_if_neg = new name{"implies_of_if_neg"};
     g_implies_of_if_pos = new name{"implies_of_if_pos"};
@@ -893,6 +897,8 @@ void finalize_constants() {
     delete g_iff_true_intro;
     delete g_imp_congr;
     delete g_imp_congr_eq;
+    delete g_imp_congr_ctx;
+    delete g_imp_congr_ctx_eq;
     delete g_implies;
     delete g_implies_of_if_neg;
     delete g_implies_of_if_pos;
@@ -1279,6 +1285,8 @@ name const & get_iff_trans_name() { return *g_iff_trans; }
 name const & get_iff_true_intro_name() { return *g_iff_true_intro; }
 name const & get_imp_congr_name() { return *g_imp_congr; }
 name const & get_imp_congr_eq_name() { return *g_imp_congr_eq; }
+name const & get_imp_congr_ctx_name() { return *g_imp_congr_ctx; }
+name const & get_imp_congr_ctx_eq_name() { return *g_imp_congr_ctx_eq; }
 name const & get_implies_name() { return *g_implies; }
 name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; }
 name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; }

src/library/constants.h

@@ -122,6 +122,8 @@ name const & get_iff_trans_name();
 name const & get_iff_true_intro_name();
 name const & get_imp_congr_name();
 name const & get_imp_congr_eq_name();
+name const & get_imp_congr_ctx_name();
+name const & get_imp_congr_ctx_eq_name();
 name const & get_implies_name();
 name const & get_implies_of_if_neg_name();
 name const & get_implies_of_if_pos_name();

src/library/constants.txt

@@ -115,6 +115,8 @@ iff.trans
 iff_true_intro
 imp_congr
 imp_congr_eq
+imp_congr_ctx
+imp_congr_ctx_eq
 implies
 implies_of_if_neg
 implies_of_if_pos

tests/lean/attribute_bug1.lean.expected.out

@@ -1,9 +1,9 @@
-attribute_bug1.lean:7:0: error: simp tactic failed to simplify
+attribute_bug1.lean:7:0: error: simplify tactic failed to simplify
 state:
 n : ℕ
 ⊢ f n = n + 1
 constant fdef : ∀ (n : ℕ), f n = n + 1
-attribute_bug1.lean:19:0: error: simp tactic failed to simplify
+attribute_bug1.lean:19:0: error: simplify tactic failed to simplify
 state:
 n : ℕ
 ⊢ f n = n + 1

tests/lean/run/1093.lean

@@ -6,6 +6,3 @@ attribute [simp] zadd
 
 example (a : nat) : 0 + a ≤ a :=
 by do simp
-
-example (a : nat) : 0 + a ≥ a :=
-by do simp

tests/lean/run/interactive1.lean

@@ -45,4 +45,4 @@ begin
 end
 open tactic
 example (a b : nat) : a = b → h 0 a = b :=
-begin simp without bla, intros, try reflexivity end -- should fail if bla is used
+begin ctx_simp without bla, intros, try reflexivity end -- should fail if bla is used

tests/lean/run/rw_set4.lean

@@ -7,5 +7,5 @@ sorry
 
 print [congr] default
 
-example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by (simp >> intros >> reflexivity)
-example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by (simp >> intros >> reflexivity)
+example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by (ctx_simp >> intros >> reflexivity)
+example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by (ctx_simp >> intros >> reflexivity)

tests/lean/run/simp1.lean

@@ -6,6 +6,5 @@ lemma bar : g y = z := sorry
 
 open tactic
 
-set_option trace.simplifier.failure true
 example : g (f x y) = z := by simp
 example : g (f x (f x y)) = z := by simp

tests/lean/run/simp_prove_fn.lean

@@ -1,16 +0,0 @@
-open tactic
-
-constants (A : Type.{1}) (x y z w v : A) (f : A → A) (H₁ : f (f x) = f y) (H₂ : f (f y) = f z) (H₃ : f (f z) = w) (g : A → A → A)
-          (H : ∀ a b : A, f (f (f (f a))) = b → f (g a b) = b)
-
-meta definition my_prove_fn : tactic unit :=
-do h₁ ← mk_const `H₁,
-      h₂ ← mk_const `H₂,
-      h₃ ← mk_const `H₃,
-      simp_using [h₁, h₂, h₃], reflexivity
-
-set_option trace.simplifier.prove true
-example : f (g x w) = w  :=
-by do h ← mk_const `H,
-      simplify_goal my_prove_fn [h],
-      reflexivity

tests/lean/run/simplifier_canonize_instances.lean

@@ -1,24 +0,0 @@
-open tactic
-
-set_option pp.implicit true
-
-meta definition simplify_goal_force : tactic unit :=
-do (new_target, Heq) ← target >>= simplify failed [],
-   assert `Htarget new_target, swap,
-   Ht ← get_local `Htarget,
-   mk_app `eq.mpr [Heq, Ht] >>= apply_core transparency.all ff tt,
-   try reflexivity
-
-universe l
-
-constants (f₁ : Π (X : Type*) (X_grp : group X), X)
-constants (f₂ : Π (X : Type*) [X_grp : group X], X)
-constants (A : Type l) (A_grp₁ : group A)
-
-attribute [irreducible] noncomputable definition A_grp₂ : group A := A_grp₁
-attribute [irreducible] noncomputable definition A_grp₃ (t : true) : group A := A_grp₁
-
-set_option simplify.canonize_instances_fixed_point true
-example : @f₂ A A_grp₁ = @f₂ A A_grp₂ := by simplify_goal_force
-example : @f₂ A (A_grp₃ trivial) = @f₂ A A_grp₂ := by simplify_goal_force
-example : @f₂ A (A_grp₃ trivial) = @f₂ A A_grp₂ := by simplify_goal_force

tests/lean/run/simplifier_custom_relations.lean

@@ -26,7 +26,7 @@ print [congr] default
 meta definition relsimp_core (e : expr) : tactic (expr × expr) :=
 do S         ← simp_lemmas.mk_default,
    e_type    ← infer_type e >>= whnf,
-   S^.simplify_core failed `rel e
+   simplify_core default_simplify_config S `rel e
 
 example : rel (h (f x)) z :=
 by do e₁ ← to_expr `(h (f x)),

tests/lean/simplifier_prove_failures.lean

@@ -1,16 +0,0 @@
-open tactic
-
-constants (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R = true)
-attribute [simp] HQR
-
-meta definition prove_skip           : tactic unit := skip
-meta definition prove_fail           : tactic unit := failed
-meta definition prove_partial_assign : tactic unit := mk_const `HPQ >>= apply
-meta definition prove_full_assign    : tactic unit := (mk_const `HPQ >>= apply) >> (mk_const `HP) >>= exact
-
-set_option trace.simplifier.prove true
-
-example : R := by simplify_goal prove_skip []           >> try triv
-example : R := by simplify_goal prove_fail []           >> try triv
-example : R := by simplify_goal prove_partial_assign [] >> try triv
-example : R := by simplify_goal prove_full_assign []    >> try triv

tests/lean/simplifier_prove_failures.lean.expected.out

@@ -1,17 +0,0 @@
-[simplifier.prove] goal: ?m_1 : Q
-[simplifier.prove] prove_fn succeeded but did not return a proof
-simplifier_prove_failures.lean:13:15: error: simp tactic failed to simplify
-state:
-⊢ R
-[simplifier.prove] goal: ?m_1 : Q
-[simplifier.prove] prove_fn failed to prove Q
-simplifier_prove_failures.lean:14:15: error: simp tactic failed to simplify
-state:
-⊢ R
-[simplifier.prove] goal: ?m_1 : Q
-[simplifier.prove] prove_fn succeeded but left an unrecognized metavariable of type P in proof
-simplifier_prove_failures.lean:15:15: error: simp tactic failed to simplify
-state:
-⊢ R
-[simplifier.prove] goal: ?m_1 : Q
-[simplifier.prove] success: HPQ HP : Q