notational leakage

Stream: general

[Kevin Buzzard]

My understanding of idiomatic Lean is that a lot of simple terms have some kind of "canonical form", and when writing Lean code (especially simp lemmas) one should write each such term in its canonical form rather than any of the defeq other forms which can be used, because defeq is fine for rfl but not for rw.

In the past, when things have not come out in the "canonical form" which I want them to be, this was user error, because this user in particular had no idea about this canonical form philosophy until recently.

I'm now attempting to stick to it rigidly whilst writing teaching materials. Here is an example where I decide that 0 (i.e. has_zero.zero) is my canonical form for mynat.zero and then a mynat.zero appears:

inductive mynat
| zero : mynat
| succ : mynat → mynat

-- I want to never see mynat.zero again
instance : has_zero mynat := ⟨mynat.zero⟩

namespace mynat

definition add : mynat → mynat → mynat
| n 0 := n
| n (succ p) := succ (add n p)

instance : has_add mynat := ⟨mynat.add⟩

theorem zero_add : ∀ x : mynat, 0 + x = x :=
begin
  intro x,
  induction x with d hd,
  { -- ⊢ 0 + zero = zero -- leakage of "zero" i.e. mynat.zero
    sorry
  },
  { -- inductive case is fine
    sorry
  }
end

/-
⊢ @eq.{1} mynat (@has_add.add.{0} mynat mynat.has_add (@has_zero.zero.{0} mynat mynat.has_zero) mynat.zero) mynat.zero
-/

I was thinking I could just fix this with my own induction function, which does all the rewriting of mynat.zero to has_zero.zero. But I can't do it, because the induction tactic eats some new variable names and this is convenient, so I would have to write my own tactic to do this. I don't know where to start with writing tactics though. I think that in practice all I want to do is some kind of repeat {rw (show mynat.zero = (0 : mynat), from rfl) at *}, after every application of any tactic which leaks.

Does anyone have any advice on how to make Lean a bit more noob-friendly here? I just want it to work for beginners and them never ever see zero.

[Johan Commelin]

Also, this doesn't seem to happen when you reprove zero_add for Lean's version of nat, right?

[Johan Commelin]

Let me check.

[Johan Commelin]

1 goal
case nat.zero
⊢ 0 + 0 = 0

[Johan Commelin]

theorem zero_add' : ∀ x : ℕ, 0 + x = x :=
begin
  intro x,
  induction x with d hd,
  { -- ⊢ 0 + 0 = 0 -- no leakage of "zero"
    sorry
  },
  { -- inductive case is fine
    sorry
  }
end

[Johan Commelin]

So somehow the induction tactic picked up that nat.zero is not canonical form, and it should use 0.

[Mario Carneiro]

It's not that hard to use a custom recursor, including getting names for the variables in the cases. You just use refine:

refine mynat.rec_on' n _ (λ m IH, _),

[Mario Carneiro]

This doesn't happen for nat because the pretty printer has magic to print nat.zero as 0 even though it's not the same as has_zero.zero nat

[Mario Carneiro]

so the leakage is still happening, you just can't see it because of the pp

[Mario Carneiro]

We could try writing an induction' which doesn't have a broken using clause. I never use it because the refine version is shorter, but if the using clause was triggered automatically with an attribute that could be a lot of value added for custom recursors

[Johan Commelin]

I think this could be quite helpful to beginners...

[Johan Commelin]

In some sense the induction tactic is quite useless as it is.

[Johan Commelin]

I would wish that refine blah.rec_on _ _ _ isn't "idiomatic". Because the informal proof says "use induction on x". It would be great if you could actually type induction x in the Lean proof.

[Johan Commelin]

And I wouldn't want a using clause, that's very verbose. I'd rather have some sort of attribute.

[Johan Commelin]

If we tag mynat.custom_rec_on with @induction then the induction' tactic could pick that up, right?

[Mario Carneiro]

that's the idea

[Mario Carneiro]

I like refine because it's the swiss army knife of lean tactics

[Mario Carneiro]

it's very straightforward to use and less to remember

[Mario Carneiro]

and it doesn't have gotchas like apply

[Johan Commelin]

Sure refine is great as Swiss army knife. But it doesn't give you the semantics that induction has.

[Johan Commelin]

If you want people to see in a glance what the idea behind the proof is...

[Johan Commelin]

Of course you can get almost every where with refine, rw and maybe occasionally a simp [foo,bar].

[Johan Commelin]

But if you want to write "beautiful, beginner-friendly proofs"...

[Kevin Buzzard]

What I need are non-leaky tactics, maybe called induction' and cases', so that

induction' n with d hd,

is the same as

  induction n with d hd,
  repeat {all_goals {rw (show mynat.zero = (0 : mynat), from rfl) at *}},
  repeat {all_goals {rw (show mynat.le = @has_le.le mynat _, from rfl) at *}},

etc etc

and induction' should fail iff induction fails.

Are these trivial to write?

[Kevin Buzzard]

I also want a rewrite tactic which does not try rfl at the end. Is this already in Lean?

[Chris Hughes]

Does this work?

namespace tactic.interactive

open tactic.interactive interactive.types expr lean lean.parser tactic interactive

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
`[repeat {all_goals {rw (show mynat.zero = (0 : mynat), from rfl) at *}},
  repeat {all_goals {rw (show mynat.le = @has_le.le mynat _, from rfl) at *}}]

end tactic.interactive

[Chris Hughes]

You could also write a recursor using has_zero.zero and do induction ... using

[Mario Carneiro]

It would be better to use change mynat.zero with 0 at * instead of rw rfl like that

[Kevin Buzzard]

For the rw with no refl I just copied a bunch of private defs from core and then deleted a random line and I think I got lucky:

import tactic.interactive

open lean
open lean.parser

local postfix `?`:9001 := optional
local postfix *:9001 := many

namespace tactic
namespace interactive
open interactive interactive.types expr

private meta def resolve_name' (n : name) : tactic expr :=
do {
  p ← resolve_name n,
  match p with
  | expr.const n _ := mk_const n -- create metavars for universe levels
  | _              := i_to_expr p
  end
}

private meta def rw_goal (cfg : rewrite_cfg) (rs : list rw_rule) : tactic unit :=
rs.mmap' $ λ r, do
 save_info r.pos,
 eq_lemmas ← get_rule_eqn_lemmas r,
 orelse'
   (do e ← to_expr' r.rule, rewrite_target e {symm := r.symm, ..cfg})
   (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_target e {symm := r.symm, ..cfg})
   (eq_lemmas.empty)

private meta def uses_hyp (e : expr) (h : expr) : bool :=
e.fold ff $ λ t _ r, r || to_bool (t = h)

private meta def rw_hyp (cfg : rewrite_cfg) : list rw_rule → expr → tactic unit
| []      hyp := skip
| (r::rs) hyp := do
  save_info r.pos,
  eq_lemmas ← get_rule_eqn_lemmas r,
  orelse'
    (do e ← to_expr' r.rule, when (not (uses_hyp e hyp)) $ rewrite_hyp e hyp {symm := r.symm, ..cfg} >>= rw_hyp rs)
    (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_hyp e hyp {symm := r.symm, ..cfg} >>= rw_hyp rs)
    (eq_lemmas.empty)

private meta def rw_core (rs : parse rw_rules) (loca : parse location) (cfg : rewrite_cfg) : tactic unit :=
match loca with
| loc.wildcard := loca.try_apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
| _            := loca.apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
end >> (returnopt rs.end_pos >>= save_info <|> skip)

meta def rw' (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
propagate_tags (rw_core q l cfg)

end interactive
end tactic

Is this a silly way to do it? I just deleted one of the >> lines after end in rw_core

[Mario Carneiro]

like I said, use change with instead of rw

[Kenny Lau]

use erw

[Kevin Buzzard]

change with just looks more complicated than rw. I have a working rw'. I don't mind writing new tactics. To be honest I don't even mind modding core Lean for this project, it's a standalone thing.

[Kevin Buzzard]

Chris I'll try your induction code when I get back in front of Lean. Thanks!

[Johan Commelin]

@Kevin Buzzard I think Mario means that you should use change with inside induction' instead of using rw there.

[Kevin Buzzard]

I just want one tactic which is simple to apply and which doesn't leak. I am not sure I understand what is being suggested.

[Kevin Buzzard]

At the minute I am writing

induction n with d hd,
clear_up_leaks,
{ ... } { ... }

[Kevin Buzzard]

and I want to write

induction' n with d hd
{ -- no leaks here}
{ -- or here}

[Johan Commelin]

Right, and Mario says that clear_up_leaks should use change instead of rw.

[Johan Commelin]

We might want an attribute @antileak or something like that, that will change terms into defeq terms that are more canonical.

[Johan Commelin]

I guess we could also use dsimp for this?

[Johan Commelin]

@Kevin Buzzard what happens if you write a simp lemma (tagged with @[simp] that says mynat.zero = 0 := rfl.
And then you call induction n with d hd; dsimp.

[Johan Commelin]

Similarly you will want mynat.succ n = n + 1 := rfl.

[Johan Commelin]

Is that sufficient to clear up the leaks?

[Kevin Buzzard]

That's strictly worse than clear_up_leaks because formally it's the same thing ("apply a tactic and then type something which you don't want") and secondly simp will close various goals, like rfl goals -- it does too much.

[Mario Carneiro]

using change with will not close any goals

[Mario Carneiro]

And I am talking about the definition of induction', like Johan says

[Mario Carneiro]

This works:

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
all_goals `[
  try {change mynat.zero with (0 : mynat) at *},
  try {change mynat.le with (≤) at *},
  try {change @mynat.succ with (λ n, n + 1) at *, dsimp only at *}]

theorem zero_add : ∀ x : mynat, x = x :=
begin
  intro x,
  induction' x with d hd,
  -- ⊢ 0 + 0 = 0
  -- 0 + d = d ⊢ 0 + (d + 1) = d + 1
end

Unfortunately change with does not support arguments in the lemmas, so I use some beta reduction at the end there. I don't think it will use rfl at the end though. Also propagate_tags undoes the work for some reason, so you can't use case with this

[Kevin Buzzard]

So this induction' thing, and rw' and also this structure_helper thing are all attempts to write more user-friendly ways of doing stuff. The idea is that we are shielding the users from Lean's weak spots here. And we're also shielding the user from definitions and recursion; I want to ask them to only prove theorems.

[Mario Carneiro]

Yes, but you could say that about any tactic

[Scott Morrison]

I agree you can say this about any tactic, but Kevin is implicitly making a point dear to my heart here --- whenever something is even slightly painful, we should grind away on it, by building suitable tactics, until it becomes smooth and easy. The payoff for building tactics that make life easier is really high!

[Kevin Buzzard]

Both Scott and I are speaking as mathematicians who have to deal with questions from undergrads of the form "why doesn't this rewrite work?" and we give technical answers involving pp.all but we'd rather the rewrite just worked ;-)

[Kevin Buzzard]

This works:

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
all_goals `[
  try {change mynat.zero with (0 : mynat) at *},
  try {change mynat.le with (≤) at *},
  try {change @mynat.succ with (λ n, n + 1) at *, dsimp only at *}]

What do I need to open to make this compile?

unknown identifier 'parse'
unknown identifier 'cases_arg_p'
unknown identifier 'parse'
unknown identifier 'with_ident_list'

Regarding succ, are you suggesting that n + 1 is the canonical way of writing succ n? I had assumed it was the other way around.

[Mario Carneiro]

inductive mynat
| zero : mynat
| succ : mynat → mynat

-- I want to never see mynat.zero again
instance : has_zero mynat := ⟨mynat.zero⟩

instance : has_one mynat := ⟨mynat.succ 0⟩

namespace mynat

definition add : mynat → mynat → mynat
| n 0 := n
| n (succ p) := succ (add n p)

instance : has_add mynat := ⟨mynat.add⟩

end mynat

namespace tactic.interactive

open tactic.interactive interactive.types expr lean lean.parser tactic interactive

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
all_goals `[
  try {change mynat.zero with (0 : mynat) at *},
  try {change mynat.le with (≤) at *},
  try {change @mynat.succ with (λ n, n + 1) at *, dsimp only at *}]

end tactic.interactive

namespace mynat

theorem zero_add : ∀ x : mynat, x = x :=
begin
  intro x,
  induction' x with d hd,
  -- ⊢ 0 + 0 = 0
  -- 0 + d = d ⊢ 0 + (d + 1) = d + 1
end

[Kevin Buzzard]

Thanks. What I am surprised about is that you want to replace succ with + 1. I decided in my development that succ x was more canonical than x + 1. Is there anything wrong with this decision?

[Johan Commelin]

I guess that it doesn't look very "mathematical"...

[Mario Carneiro]

I don't really care one away or another... the lean magic is pretty strong in being able to conflate them for nat. The only downside of n+1 is simp has a nasty habit of changing it to 1+n

[Johan Commelin]

Isn't that because add_comm is a simp-lemma for some reason?

[Johan Commelin]

I've seen it show up in the results of squeeze_simp.

[Keeley Hoek]

I'm adamant that definitions should be able have attached a way to format themselves, and probably implementing this with an attribute would work really well. Then e.g. once has_zero is defined zero can remember it is always 0, and there is no chasing of potential leakage everywhere. Another nice thing would be for vector_space vs module; if the scalar ring is (in expr land) an application of discrete_field.to_ring then print vector_space, else print module, etc.

[Kevin Buzzard]

Surprisingly, this modified tactic still leaks (although I can't see why):

inductive mynat
| zero : mynat
| succ : mynat → mynat

-- I want to never see mynat.zero again
instance : has_zero mynat := ⟨mynat.zero⟩

instance : has_one mynat := ⟨mynat.succ 0⟩

namespace mynat

definition add : mynat → mynat → mynat
| n 0 := n
| n (succ p) := succ (add n p)

instance : has_add mynat := ⟨mynat.add⟩

end mynat

namespace tactic.interactive

open tactic.interactive interactive.types expr lean lean.parser tactic interactive

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
all_goals `[
  try {change mynat.zero with (0 : mynat) at *},
  try {change mynat.le with (≤) at *},
  try {change @mynat.succ with (λ n, n + 1) at *, dsimp only at *}]

end tactic.interactive

namespace mynat

lemma eq_zero_of_add_right_eq_self {{a b : mynat}} : a + b = a → b = 0 :=
begin
  intro h,
  induction' a with a ha,
  { -- leakage
    -- h : zero + b = zero
    sorry
  }, sorry
end

end mynat

[Mario Carneiro]

what changed?

[Mario Carneiro]

the tactic looks the same

[Kevin Buzzard]

Oh -- I can see why!

example (x : mynat) (h : mynat.zero + x = x + (0 : mynat)) : false :=
begin
  -- h : zero + x = x + 0
    change mynat.zero with (0 : mynat) at *,
  -- h : zero + x = x + 0
    change mynat.zero with (0 : mynat) at h,
  -- h : 0 + x = x + 0
  sorry
end

Is this a bug in change @Mario Carneiro ?

[Kevin Buzzard]

[sorry -- by "this modified tactic" I mean "your tactic", not "I modified your tactic"]

[Mario Carneiro]

that's interesting. It looks like a bug (I mean it's definitely not intended behavior)

[Kevin Buzzard]

sigh

[Johan Commelin]

We need formally verified tactics

[Kevin Buzzard]

My workaround:

try {rw' (show mynat.zero = (0 : mynat), from rfl) at *},

where rw' is my modded rw which doesn't try to close goals with rfl

[Mario Carneiro]

It's written in lean, so you can just fix it

[Mario Carneiro]

We need formally verified tactics

You joke, but...

[Kevin Buzzard]

I can't understand meta code so I can't.

/--
`change u` replaces the target `t` of the main goal to `u` provided that `t` is well formed with respect to the local context of the main goal and `t` and `u` are definitionally equal.

`change u at h` will change a local hypothesis to `u`.

`change t with u at h1 h2 ...` will replace `t` with `u` in all the supplied hypotheses (or `*`), or in the goal if no `at` clause is specified, provided that `t` and `u` are definitionally equal.
-/
meta def change (q : parse texpr) : parse (tk "with" *> texpr)? → parse location → tactic unit
| none (loc.ns [none]) := do e ← i_to_expr q, change_core e none
| none (loc.ns [some h]) := do eq ← i_to_expr q, eh ← get_local h, change_core eq (some eh)
| none _ := fail "change-at does not support multiple locations"
| (some w) l :=
  do u ← mk_meta_univ,
     ty ← mk_meta_var (sort u),
     eq ← i_to_expr ``(%%q : %%ty),
     ew ← i_to_expr ``(%%w : %%ty),
     let repl := λe : expr, e.replace (λ a n, if a = eq then some ew else none),
     l.try_apply
       (λh, do e ← infer_type h, change_core (repl e) (some h))
       (do g ← target, change_core (repl g) none)

[Mario Carneiro]

I don't see why at * would fail and at h would succeed. The last three lines are basically executing change ... at x, change ... at h, change ... at |-

[Kevin Buzzard]

Can you reproduce? My post should be a MWE

[Kevin Buzzard]

sorry, that's nonsense.

[Kevin Buzzard]

inductive mynat
| zero : mynat
| succ : mynat → mynat

-- I want to never see mynat.zero again
instance : has_zero mynat := ⟨mynat.zero⟩

instance : has_one mynat := ⟨mynat.succ 0⟩

namespace mynat

definition add : mynat → mynat → mynat
| n 0 := n
| n (succ p) := succ (add n p)

instance : has_add mynat := ⟨mynat.add⟩

end mynat

namespace tactic.interactive

open tactic.interactive interactive.types expr lean lean.parser tactic interactive

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
all_goals `[
  try {change mynat.zero with (0 : mynat) at *},
  try {change mynat.le with (≤) at *},
  try {change @mynat.succ with (λ n, n + 1) at *, dsimp only at *}]

end tactic.interactive

namespace mynat

lemma eq_zero_of_add_right_eq_self {{a b : mynat}} : a + b = a → b = 0 :=
begin
  intro h,
  induction' a with a ha,
  { -- leakage
    -- h : zero + b = zero
    change mynat.zero with (0 : mynat) at *,
    sorry
  }, sorry
end

example (x : mynat) (h : mynat.zero + x = x + (0 : mynat)) (h2 : 2 + 2 = 4) : false :=
begin
  -- h : zero + x = x + 0
    change mynat.zero with (0 : mynat) at *,
  -- h : zero + x = x + 0
    change mynat.zero with (0 : mynat) at h,
  -- h : 0 + x = x + 0
  sorry
end

end mynat

[Kevin Buzzard]

That's a WE

[Mario Carneiro]

Aha, I found the problem. Here's a standalone tactic that does the same thing as the change with line, with irrelevant things removed:

open tactic expr
example (x : mynat) (h : mynat.zero + x = x + (0 : mynat)) : false :=
begin
  -- h : zero + x = x + 0
  (do let repl := λe : expr, e.replace (λ a n,
      if a = `(mynat.zero) then some `(0 : mynat) else none),
    let hyp_tac (h) := (do
      e ← infer_type h,
      num_reverted : ℕ ← revert h,
      expr.pi n bi d b ← target,
      tactic.change $ expr.pi n bi (repl e) b,
      intron num_reverted),
    [x, h] ← tactic.local_context,
    tactic.try_lst $ [x, /- <- delete -/ h].map hyp_tac),
end

[Mario Carneiro]

The tactic fails in this case, but if you remove the x, on the last line then it works

[Kenny Lau]

run_cmd mk_simp_attr `leakage

namespace tactic.interactive

open tactic.interactive interactive.types expr lean lean.parser tactic interactive

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
all_goals `[try { dsimp only with leakage at * }]

end tactic.interactive


inductive mynat
| zero : mynat
| succ : mynat → mynat

instance : has_zero mynat := ⟨mynat.zero⟩
-- I want to never see mynat.zero again
@[leakage] theorem mynat_zero_eq_zero : mynat.zero = 0 := rfl

instance : has_one mynat := ⟨mynat.succ 0⟩

namespace mynat

definition add : mynat → mynat → mynat
| n 0 := n
| n (succ p) := succ (add n p)

instance : has_add mynat := ⟨mynat.add⟩
-- I want to never see mynat.succ again
@[leakage] theorem mynat_succ_eq_add_one (n) : mynat.succ n = n+1 := rfl

lemma eq_zero_of_add_right_eq_self {{a b : mynat}} : a + b = a → b = 0 :=
begin
  intro h,
  induction' a with a ha,
  { -- no leakage
    -- h : 0 + b = 0
    sorry
  }, sorry
end

example (x : mynat) (h : mynat.zero + x = x + (0 : mynat)) (h2 : 2 + 2 = 4) : false :=
begin
  -- h : zero + x = x + 0
    change mynat.zero with (0 : mynat) at *,
  -- h : zero + x = x + 0
    change mynat.zero with (0 : mynat) at h,
  -- h : 0 + x = x + 0
  sorry
end

end mynat

[Kevin Buzzard]

I like the look of this

[Johan Commelin]

We need formally verified tactics

You joke, but...

What makes you think that I'm joking :grinning:

[Mario Carneiro]

The reason it fails is because the change ... at x, while not doing anything to the type, changes the internal name of the local variable because it is reverted and re-introduced, and this also changes the variable h so that the old reference is dangling and fails to achieve the desired result

[Kevin Buzzard]

@Kenny Lau can you do me a cases' too?

[Kevin Buzzard]

Currently I just cut and paste the cases tactic and then add stuff to the end

[Kevin Buzzard]

do tactic.interactive.induction hp none ids none, -- it's that line I need for cases

[Mario Carneiro]

Alternatively, if only the second line is a tactic, then you can write cases foo, unleak

[Kenny Lau]

run_cmd mk_simp_attr `leakage

namespace tactic.interactive

open tactic.interactive interactive.types expr lean lean.parser tactic interactive

meta def induction' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.induction hp none ids none,
all_goals `[try { dsimp only with leakage at * }]

meta def cases' (hp : parse cases_arg_p) (ids : parse with_ident_list) : tactic unit :=
do tactic.interactive.cases hp ids,
all_goals `[try { dsimp only with leakage at * }]

end tactic.interactive


inductive mynat
| zero : mynat
| succ : mynat → mynat

instance : has_zero mynat := ⟨mynat.zero⟩
-- I want to never see mynat.zero again
@[leakage] theorem mynat_zero_eq_zero : mynat.zero = 0 := rfl

instance : has_one mynat := ⟨mynat.succ 0⟩

namespace mynat

definition add : mynat → mynat → mynat
| n 0 := n
| n (succ p) := succ (add n p)

instance : has_add mynat := ⟨mynat.add⟩
-- I want to never see mynat.succ again
@[leakage] theorem mynat_succ_eq_add_one (n) : mynat.succ n = n+1 := rfl

lemma eq_zero_of_add_right_eq_self {{a b : mynat}} : a + b = a → b = 0 :=
begin
  intro h,
  cases' a with n,
  { -- no leakage
    -- h : 0 + b = 0
    sorry },
  { -- no leakage
    -- h : n + 1 + b = n + 1
    sorry }
end

end mynat

[Mario Carneiro]

I'm not sure I like this "duplicate every tactic" approach

[Kenny Lau]

me neither

[Kenny Lau]

unleak is good

[Kenny Lau]

Alternatively, if only the second line is a tactic, then you can write cases foo, unleak

cases foo; unleak

[Mario Carneiro]

your version unleaks everywhere so it's the same

[Mario Carneiro]

but it's probably more idiomatic to drop the all_goals and use ;

[Rob Lewis]

There's an (interactive) change' tactic that's supposted to deal with the naming issue in change. https://github.com/leanprover-community/mathlib/pull/712

[Kenny Lau]

or just write dsimp only with leakage

[Kenny Lau]

(accidental promotion of simp attributes)

[Kenny Lau]

(I've always been adamant about the widespread use of simp attribute)

[Keeley Hoek]

Someone could add a little custom tactic hook so unleak gets run between every line when you write begin [unleak] ... end

[Andrew Ashworth]

i haven't tried this but could you get around with pp.notation and custom notation? Is it possible to hack the pretty printer in any way?

[Andrew Ashworth]

hmm, i wonder if there is a vscode extension that watches tabs and can perform regex find and replace

[Kevin Buzzard]

I'm not sure I like this "duplicate every tactic" approach

How do we make Lean more user-friendly for beginners?

[Kevin Buzzard]

i haven't tried this but could you get around with pp.notation and custom notation? Is it possible to hack the pretty printer in any way?

The problem with this is that if the pretty printer is printing both mynat.zero and has_zero.zero as 0 then rw will still be failing and the error message will be incomprehensible.

[Mario Carneiro]

I would rather fix the original tactics rather than inventing new variations on existing things, which is more stuff for the newcomer to learn. If the set of tactics becomes too large, that itself will present a learning curve penalty

[Tim Daly]

Is there a "stack exchange" list somewhere that demonstrates each tactic? As a beginner it would be useful to see how and why to apply each tactic with a working example.

[Kevin Buzzard]

Here's something I knocked up very quickly last year, which covers some of the basics.

http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/tactics/tacticindex.html

This summer I fully intend to make something a lot more professional.

For the more advanced tactics,

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md

is invaluable.

[Kevin Buzzard]

I would rather fix the original tactics rather than inventing new variations on existing things, which is more stuff for the newcomer to learn. If the set of tactics becomes too large, that itself will present a learning curve penalty

For this notational leakage issue I am making a standalone thing; ultimately I would like induction to actually run induction'. Fixing this sort of issue in general is a different question. I like the idea of a custom recursor written with the canonical notation which gets tagged somehow and then picked up by the tactic in general.

So while I'm here, how can I actually override what happens when a user types induction in tactic mode? Editing core lean is fine. But the problem is that just changing the name of the induction tactic in core Lean will break everything, I would imagine. I'd rather have some other namespace open and with a higher priority.

[Mario Carneiro]

sadly lean interactive tactics don't work like that

[Mario Carneiro]

for it to get picked up you have to call it tactic.interactive.induction, and there can only be one of that

[Kevin Buzzard]

There are all sorts of ways I can work around this, e.g. processing user input before feeding it to Lean.

[Johan Commelin]

Can't one of @Keeley Hoek's

begin [ninja-mode]
  induction n,
end

make this work?

[Mario Carneiro]

yes, but that requires rewriting every tactic

[Rob Lewis]

It should actually be easy to define an alias newtac for tactic and automatically copy every declaration in tactic.interactive to newtac.interactive. Skip the ones you want to change, then use begin [newtac] ... end blocks. Not the prettiest workaround though.

[Mario Carneiro]

It would be great if there was an option or command line flag to set the default environment

[Johannes Hölzl]

I would vote for a per-module option (e.g. extend theory, so we can write noncomputable mathlib theory or mathlib theory)

[Keeley Hoek]

@Mario Carneiro Using my addition to lean 3.5.0 you can at least set the default monad for an interactive block.

[Keeley Hoek]

You create a new executor instance with priority higher than the default.

[Kevin Buzzard]

I am completely open to using 3.5.x with this project. It would be ideal if we could use induction a with d hd rather than induction'. My vision is that the user can only edit the stuff in a textbox within some begin end block (and can't see all the jibberish outside the block).