chore(library): remove id_locked

library/init/meta/simp_tactic.lean

@@ -468,7 +468,7 @@ private meta def loop (cfg : simp_config) (discharger : tactic unit) (to_unfold
        to_expr ``(@false.rec %%tgt %%new_fact_pr) >>= exact
      else do
        h0_type     ← infer_type h,
-       let new_fact_pr := mk_id_locked_proof new_h_type new_fact_pr,
+       let new_fact_pr := mk_id_proof new_h_type new_fact_pr,
        new_es      ← update_simp_lemmas es new_fact_pr,
        new_r       ← update_simp_lemmas r new_fact_pr,
        let new_r := {new_type := new_h_type, pr := new_pr, ..e} :: new_r,

library/init/meta/tactic.lean

@@ -1146,26 +1146,6 @@ meta def any_of {α β} : list α → (α → tactic β) → tactic β
                    end
 end list
 
-/-
-  Define id_locked using meta-programming because we don't have
-  syntax for setting reducibility_hints.
-
-  See module init.meta.declaration.
-
-  Remark: id_locked is used in the builtin implementation of tactic.change
--/
-run_cmd do
- let l  := level.param `l,
- let Ty : pexpr := expr.sort l,
- type ← to_expr ``(Π {α : %%Ty}, α → α),
- val  ← to_expr ``(λ {α : %%Ty} (a : α), a),
- add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)
-
-lemma id_locked_eq {α : Type u} (a : α) : id_locked a = a :=
-rfl
-
-attribute [inline] id_locked
-
 /-
   Define id_rhs using meta-programming because we don't have
   syntax for setting reducibility_hints.
@@ -1201,18 +1181,18 @@ meta instance : monad task :=
  bind_pure_comp_eq_map := undefined}
 
 namespace tactic
-meta def mk_id_locked_proof (prop : expr) (pr : expr) : expr :=
-expr.app (expr.app (expr.const ``id_locked [level.zero]) prop) pr
+meta def mk_id_proof (prop : expr) (pr : expr) : expr :=
+expr.app (expr.app (expr.const ``id [level.zero]) prop) pr
 
-meta def mk_id_locked_eq (lhs : expr) (rhs : expr) (pr : expr) : tactic expr :=
+meta def mk_id_eq (lhs : expr) (rhs : expr) (pr : expr) : tactic expr :=
 do prop ← mk_app `eq [lhs, rhs],
-   return $ mk_id_locked_proof prop pr
+   return $ mk_id_proof prop pr
 
 meta def replace_target (new_target : expr) (pr : expr) : tactic unit :=
 do t ← target,
    assert `htarget new_target, swap,
    ht        ← get_local `htarget,
-   locked_pr ← mk_id_locked_eq t new_target pr,
+   locked_pr ← mk_id_eq t new_target pr,
    mk_eq_mpr locked_pr ht >>= exact
 
 end tactic

src/library/app_builder.cpp

@@ -1125,9 +1125,13 @@ expr mk_ite(type_context & ctx, expr const & c, expr const & t, expr const & e)
     return mk_app(ctx, get_ite_name(), 5, mask, args);
 }
 
-expr mk_id_locked(type_context & ctx, expr const & type, expr const & h) {
+expr mk_id(type_context & ctx, expr const & type, expr const & h) {
     level lvl = get_level(ctx, type);
-    return mk_app(mk_constant(get_id_locked_name(), {lvl}), type, h);
+    return mk_app(mk_constant(get_id_name(), {lvl}), type, h);
+}
+
+expr mk_id(type_context & ctx, expr const & h) {
+    return mk_id(ctx, ctx.infer(h), h);
 }
 
 expr mk_id_rhs(type_context & ctx, expr const & h) {

src/library/app_builder.h

@@ -180,8 +180,10 @@ expr mk_false_rec(type_context & ctx, expr const & c, expr const & H);
 /* (if c then t else e) */
 expr mk_ite(type_context & ctx, expr const & c, expr const & t, expr const & e);
 
-/* (id_locked type h) */
-expr mk_id_locked(type_context & ctx, expr const & type, expr const & h);
+/* (@id type h) */
+expr mk_id(type_context & ctx, expr const & type, expr const & h);
+/* (id h) */
+expr mk_id(type_context & ctx, expr const & h);
 
 /* (id_rhs h) */
 expr mk_id_rhs(type_context & ctx, expr const & h);

src/library/constants.cpp

@@ -49,7 +49,6 @@ name const * g_decidable = nullptr;
 name const * g_decidable_to_bool = nullptr;
 name const * g_distrib = nullptr;
 name const * g_dite = nullptr;
-name const * g_id = nullptr;
 name const * g_empty = nullptr;
 name const * g_Exists = nullptr;
 name const * g_eq = nullptr;
@@ -127,7 +126,7 @@ name const * g_heq_symm = nullptr;
 name const * g_heq_trans = nullptr;
 name const * g_heq_of_eq = nullptr;
 name const * g_hole_command = nullptr;
-name const * g_id_locked = nullptr;
+name const * g_id = nullptr;
 name const * g_id_rhs = nullptr;
 name const * g_id_delta = nullptr;
 name const * g_if_neg = nullptr;
@@ -431,7 +430,6 @@ void initialize_constants() {
     g_decidable_to_bool = new name{"decidable", "to_bool"};
     g_distrib = new name{"distrib"};
     g_dite = new name{"dite"};
-    g_id = new name{"id"};
     g_empty = new name{"empty"};
     g_Exists = new name{"Exists"};
     g_eq = new name{"eq"};
@@ -509,7 +507,7 @@ void initialize_constants() {
     g_heq_trans = new name{"heq", "trans"};
     g_heq_of_eq = new name{"heq_of_eq"};
     g_hole_command = new name{"hole_command"};
-    g_id_locked = new name{"id_locked"};
+    g_id = new name{"id"};
     g_id_rhs = new name{"id_rhs"};
     g_id_delta = new name{"id_delta"};
     g_if_neg = new name{"if_neg"};
@@ -814,7 +812,6 @@ void finalize_constants() {
     delete g_decidable_to_bool;
     delete g_distrib;
     delete g_dite;
-    delete g_id;
     delete g_empty;
     delete g_Exists;
     delete g_eq;
@@ -892,7 +889,7 @@ void finalize_constants() {
     delete g_heq_trans;
     delete g_heq_of_eq;
     delete g_hole_command;
-    delete g_id_locked;
+    delete g_id;
     delete g_id_rhs;
     delete g_id_delta;
     delete g_if_neg;
@@ -1196,7 +1193,6 @@ name const & get_decidable_name() { return *g_decidable; }
 name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; }
 name const & get_distrib_name() { return *g_distrib; }
 name const & get_dite_name() { return *g_dite; }
-name const & get_id_name() { return *g_id; }
 name const & get_empty_name() { return *g_empty; }
 name const & get_Exists_name() { return *g_Exists; }
 name const & get_eq_name() { return *g_eq; }
@@ -1274,7 +1270,7 @@ name const & get_heq_symm_name() { return *g_heq_symm; }
 name const & get_heq_trans_name() { return *g_heq_trans; }
 name const & get_heq_of_eq_name() { return *g_heq_of_eq; }
 name const & get_hole_command_name() { return *g_hole_command; }
-name const & get_id_locked_name() { return *g_id_locked; }
+name const & get_id_name() { return *g_id; }
 name const & get_id_rhs_name() { return *g_id_rhs; }
 name const & get_id_delta_name() { return *g_id_delta; }
 name const & get_if_neg_name() { return *g_if_neg; }

src/library/constants.h

@@ -51,7 +51,6 @@ name const & get_decidable_name();
 name const & get_decidable_to_bool_name();
 name const & get_distrib_name();
 name const & get_dite_name();
-name const & get_id_name();
 name const & get_empty_name();
 name const & get_Exists_name();
 name const & get_eq_name();
@@ -129,7 +128,7 @@ name const & get_heq_symm_name();
 name const & get_heq_trans_name();
 name const & get_heq_of_eq_name();
 name const & get_hole_command_name();
-name const & get_id_locked_name();
+name const & get_id_name();
 name const & get_id_rhs_name();
 name const & get_id_delta_name();
 name const & get_if_neg_name();

src/library/constants.txt

@@ -44,7 +44,6 @@ decidable
 decidable.to_bool
 distrib
 dite
-id
 empty
 Exists
 eq
@@ -122,7 +121,7 @@ heq.symm
 heq.trans
 heq_of_eq
 hole_command
-id_locked
+id
 id_rhs
 id_delta
 if_neg

src/library/tactic/change_tactic.cpp

@@ -24,11 +24,11 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) {
             /*
                We use the proof term
 
-                  (@id_locked (g->get_type()) new_M)
+                  (@id (g->get_type()) new_M)
 
                to create a "checkpoint". See discussion at issue #1260
             */
-            expr  pr  = mk_id_locked(ctx, g->get_type(), new_M);
+            expr  pr  = mk_id(ctx, g->get_type(), new_M);
             mctx.assign(head(s.goals()), pr);
             list<expr> new_gs(new_M, tail(s.goals()));
             return tactic::mk_success(set_mctx_goals(s, mctx, new_gs));

src/library/tactic/smt/congruence_closure.cpp

@@ -1149,7 +1149,7 @@ expr congruence_closure::mk_proof(expr const & lhs, expr const & rhs, expr const
     } else if (H == *g_refl_mark) {
         expr type  = heq_proofs ? mk_heq(m_ctx, lhs, rhs) : mk_eq(m_ctx, lhs, rhs);
         expr proof = heq_proofs ? mk_heq_refl(m_ctx, lhs) : mk_eq_refl(m_ctx, lhs);
-        return mk_app(mk_constant(get_id_locked_name(), {mk_level_zero()}), type, proof);
+        return mk_app(mk_constant(get_id_name(), {mk_level_zero()}), type, proof);
     } else if (is_cc_theory_proof(H)) {
         return expand_delayed_cc_proofs(*this, get_cc_theory_proof_arg(H));
     } else {

src/library/tactic/smt/smt_state.cpp

@@ -260,7 +260,7 @@ static expr_pair preprocess_forward(type_context & ctx, defeq_can_state & dcs, s
     } else if (r.get_new() == type) {
         return mk_pair(type, h);
     } else {
-        return mk_pair(r.get_new(), mk_id_locked(ctx, r.get_new(), h));
+        return mk_pair(r.get_new(), mk_id(ctx, r.get_new(), h));
     }
 }
 

tests/lean/anc1.lean.expected.out

@@ -3,7 +3,7 @@
 anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry
 ⟨1, _⟩ : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
-Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
+Exists.intro 1 (id (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from ⟨Hb, Ha⟩ :
   ∀ (A B C : Prop), A → B → C → B ∧ A
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A ∧ C ∧ A, from ⟨Hb, ⟨Ha, ⟨Hc, Ha⟩⟩⟩ :

tests/lean/run/check_constants.lean

@@ -49,7 +49,6 @@ run_cmd script_check_id `decidable
 run_cmd script_check_id `decidable.to_bool
 run_cmd script_check_id `distrib
 run_cmd script_check_id `dite
-run_cmd script_check_id `id
 run_cmd script_check_id `empty
 run_cmd script_check_id `Exists
 run_cmd script_check_id `eq
@@ -127,7 +126,7 @@ run_cmd script_check_id `heq.symm
 run_cmd script_check_id `heq.trans
 run_cmd script_check_id `heq_of_eq
 run_cmd script_check_id `hole_command
-run_cmd script_check_id `id_locked
+run_cmd script_check_id `id
 run_cmd script_check_id `id_rhs
 run_cmd script_check_id `id_delta
 run_cmd script_check_id `if_neg