Zulip Chat Archive

Stream: general

Topic: notational leakage


view this post on Zulip Kevin Buzzard (Jul 04 2019 at 10:21):

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.

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:25):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:25):

Let me check.

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:26):

1 goal
case nat.zero
 0 + 0 = 0

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:27):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:27):

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

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:28):

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, _),

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:29):

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

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:30):

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

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:32):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:33):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:33):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:34):

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.

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:36):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:36):

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

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:37):

that's the idea

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:37):

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

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:38):

it's very straightforward to use and less to remember

view this post on Zulip Mario Carneiro (Jul 04 2019 at 10:38):

and it doesn't have gotchas like apply

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:41):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:42):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:42):

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

view this post on Zulip Johan Commelin (Jul 04 2019 at 10:43):

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

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 10:19):

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?

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 10:25):

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

view this post on Zulip Chris Hughes (Jul 05 2019 at 10:26):

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

view this post on Zulip Chris Hughes (Jul 05 2019 at 10:27):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 10:28):

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

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 10:49):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 11:04):

like I said, use change with instead of rw

view this post on Zulip Kenny Lau (Jul 05 2019 at 11:04):

use erw

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 11:25):

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.

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 11:25):

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

view this post on Zulip Johan Commelin (Jul 05 2019 at 11:39):

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

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 11:39):

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.

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 11:40):

At the minute I am writing

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

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 11:40):

and I want to write

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

view this post on Zulip Johan Commelin (Jul 05 2019 at 11:46):

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

view this post on Zulip Johan Commelin (Jul 05 2019 at 11:47):

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

view this post on Zulip Johan Commelin (Jul 05 2019 at 11:47):

I guess we could also use dsimp for this?

view this post on Zulip Johan Commelin (Jul 05 2019 at 11:48):

@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.

view this post on Zulip Johan Commelin (Jul 05 2019 at 11:49):

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

view this post on Zulip Johan Commelin (Jul 05 2019 at 11:49):

Is that sufficient to clear up the leaks?

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 11:49):

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.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 12:34):

using change with will not close any goals

view this post on Zulip Mario Carneiro (Jul 05 2019 at 12:34):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 12:49):

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

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 12:56):

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.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 13:02):

Yes, but you could say that about any tactic

view this post on Zulip Scott Morrison (Jul 05 2019 at 14:56):

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!

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 14:57):

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 ;-)

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 17:37):

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.

view this post on Zulip Mario Carneiro (Jul 05 2019 at 17:58):

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

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 19:28):

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?

view this post on Zulip Johan Commelin (Jul 05 2019 at 19:33):

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

view this post on Zulip Mario Carneiro (Jul 05 2019 at 19:54):

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

view this post on Zulip Johan Commelin (Jul 05 2019 at 19:55):

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

view this post on Zulip Johan Commelin (Jul 05 2019 at 19:55):

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

view this post on Zulip Keeley Hoek (Jul 06 2019 at 04:18):

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.

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:37):

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 10:40):

what changed?

view this post on Zulip Mario Carneiro (Jul 07 2019 at 10:41):

the tactic looks the same

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:41):

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 ?

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:42):

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 10:43):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:45):

sigh

view this post on Zulip Johan Commelin (Jul 07 2019 at 10:45):

We need formally verified tactics

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:51):

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 10:51):

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 10:52):

We need formally verified tactics

You joke, but...

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:52):

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)

view this post on Zulip Mario Carneiro (Jul 07 2019 at 10:55):

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 |-

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:56):

Can you reproduce? My post should be a MWE

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:56):

sorry, that's nonsense.

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:56):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 10:57):

That's a WE

view this post on Zulip Mario Carneiro (Jul 07 2019 at 11:22):

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 11:22):

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

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:23):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 11:24):

I like the look of this

view this post on Zulip Johan Commelin (Jul 07 2019 at 11:26):

We need formally verified tactics

You joke, but...

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 11:27):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 11:29):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 11:29):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 11:29):

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 11:30):

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

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:30):

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

view this post on Zulip Mario Carneiro (Jul 07 2019 at 11:31):

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

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:32):

me neither

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:32):

unleak is good

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:32):

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

cases foo; unleak

view this post on Zulip Mario Carneiro (Jul 07 2019 at 11:32):

your version unleaks everywhere so it's the same

view this post on Zulip Mario Carneiro (Jul 07 2019 at 11:33):

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

view this post on Zulip Rob Lewis (Jul 07 2019 at 11:39):

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

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:39):

or just write dsimp only with leakage

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:40):

(accidental promotion of simp attributes)

view this post on Zulip Kenny Lau (Jul 07 2019 at 11:40):

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

view this post on Zulip Keeley Hoek (Jul 07 2019 at 11:41):

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

view this post on Zulip Andrew Ashworth (Jul 07 2019 at 12:06):

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?

view this post on Zulip Andrew Ashworth (Jul 07 2019 at 12:11):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 14:06):

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

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 14:07):

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.

view this post on Zulip Mario Carneiro (Jul 07 2019 at 14:32):

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

view this post on Zulip Tim Daly (Jul 07 2019 at 14:35):

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.

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 14:57):

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.

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 15:01):

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.

view this post on Zulip Mario Carneiro (Jul 07 2019 at 15:07):

sadly lean interactive tactics don't work like that

view this post on Zulip Mario Carneiro (Jul 07 2019 at 15:08):

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

view this post on Zulip Kevin Buzzard (Jul 07 2019 at 15:13):

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

view this post on Zulip Johan Commelin (Jul 07 2019 at 15:32):

Can't one of @Keeley Hoek's

begin [ninja-mode]
  induction n,
end

make this work?

view this post on Zulip Mario Carneiro (Jul 07 2019 at 15:32):

yes, but that requires rewriting every tactic

view this post on Zulip Rob Lewis (Jul 07 2019 at 16:27):

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.

view this post on Zulip Mario Carneiro (Jul 07 2019 at 16:29):

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

view this post on Zulip Johannes Hölzl (Jul 07 2019 at 19:49):

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

view this post on Zulip Keeley Hoek (Jul 08 2019 at 10:00):

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

view this post on Zulip Keeley Hoek (Jul 08 2019 at 10:01):

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

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 10:28):

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).


Last updated: May 18 2021 at 17:44 UTC