Zulip Chat Archive

Stream: general

Topic: equation lemmas and simp


Sean Leather (Mar 01 2018 at 07:18):

What is the effect of putting @[simp] on a def defined with pattern-matching equations? Does it annotate the equation lemmas with @[simp]?

Sean Leather (Mar 01 2018 at 07:29):

When I look at #print <def-name>._main.equations._eqn_1, it only has @[_refl_lemma].

Simon Hudon (Mar 01 2018 at 07:30):

what do you see if you look at the other equations? (see them listed in #print prefix <def-name>)

Sean Leather (Mar 01 2018 at 07:33):

I had to use a fully-qualified <def-name>, but that's a useful command:

#print prefix tts.typ.open
tts.typ.open : Π {V : Type}, list (typ V)  typ V  typ V
tts.typ.open._main : Π {V : Type}, list (typ V)  typ V  typ V
tts.typ.open._main._meta_aux : Π {V : Type}, list (typ V)  typ V  typ V
tts.typ.open._main.equations._eqn_1 :  {V : Type} (ts : list (typ V)) (i : ), typ.open._main ts (varb i) = option.get_or_else (list.nth ts i) (varb 0)
tts.typ.open._main.equations._eqn_2 :  {V : Type} (ts : list (typ V)) (x : V), typ.open._main ts (varf x) = varf x
tts.typ.open._main.equations._eqn_3 :  {V : Type} (ts : list (typ V)) (t₁ t₂ : typ V),
  typ.open._main ts (arr t₁ t₂) = arr (typ.open._main ts t₁) (typ.open._main ts t₂)
tts.typ.open._sunfold : Π {V : Type}, list (typ V)  typ V  typ V
tts.typ.open.equations._eqn_1 :  {V : Type} (ts : list (typ V)) (i : ), typ.open ts (varb i) = option.get_or_else (list.nth ts i) (varb 0)
tts.typ.open.equations._eqn_2 :  {V : Type} (ts : list (typ V)) (x : V), typ.open ts (varf x) = varf x
tts.typ.open.equations._eqn_3 :  {V : Type} (ts : list (typ V)) (t₁ t₂ : typ V),
  typ.open ts (arr t₁ t₂) = arr (typ.open ts t₁) (typ.open ts t₂)

Simon Hudon (Mar 01 2018 at 07:34):

What if you look at #print tts.typ.open.equations._eqn_1 ?

Sean Leather (Mar 01 2018 at 07:35):

#print tts.typ.open.equations._eqn_1
@[_refl_lemma]
theorem tts.typ.open.equations._eqn_1 :  {V : Type} (ts : list (typ V)) (i : ), typ.open ts (varb i) = option.get_or_else (list.nth ts i) (varb 0) :=
λ {V : Type} (ts : list (typ V)), typ.open._main.equations._eqn_1 ts

Simon Hudon (Mar 01 2018 at 07:36):

That's curious. The effect I see is as if those equations were labeled with simp. I wonder if simp is implied by _refl_lemma

Sean Leather (Mar 01 2018 at 07:37):

@[_refl_lemma] is there whether or not I use @[simp].

Simon Hudon (Mar 01 2018 at 07:37):

We can check something else:

run_cmd attribute.get_instances `simp >>= trace

Simon Hudon (Mar 01 2018 at 07:38):

Correction:

run_cmd attribute.get_instances `simp >>= tactic.trace ∘ list.take 3

Sean Leather (Mar 01 2018 at 07:39):

parsing at line 7[tts.typ.open, finset.sort_to_finset, finset.sort_nodup]

Sean Leather (Mar 01 2018 at 07:40):

@Simon Hudon: What does that mean?

Simon Hudon (Mar 01 2018 at 07:41):

so the whole thing is labelled as simp. The simp tactic must have some logic to retrieve the equations related to a definition.

Sean Leather (Mar 01 2018 at 07:41):

Could be.

Simon Hudon (Mar 01 2018 at 07:42):

attribute.get_instance ```simp``` gives you the list of the names that are labelled with simp. It works with any attribute. Every definition is appended at the beginning so taking only 3 of them was enough and I wanted to see if more than one name was being labelled

Sean Leather (Mar 01 2018 at 07:44):

library/init/meta/simp_tactic.lean:

/-- `get_eqn_lemmas_for deps d` returns the automatically generated equational lemmas for definition d.
   If deps is tt, then lemmas for automatically generated auxiliary declarations used to define d are also included. -/
meta constant get_eqn_lemmas_for : bool  name  tactic (list name)

Simon Hudon (Mar 01 2018 at 07:44):

Could be.

It could mean that the behavior can differ from that of using simp lemma or it could just be a way of compressing the list of simp lemmas.

Simon Hudon (Mar 01 2018 at 07:44):

Nice! Thanks!

Sean Leather (Mar 01 2018 at 07:47):

This is with set_option trace.simplify true:

3. [simplify.rewrite] [tts.typ.open.equations._eqn_3]: typ.open ts (arr t₁_a t₁_a_1) ==> arr (typ.open ts t₁_a) (typ.open ts t₁_a_1)
[simplify] eq: typ.open ts t₁_a
[simplify] eq: ts
[simplify] eq: t₁_a
[simplify] eq: typ.open

Sean Leather (Mar 01 2018 at 07:50):

So, it seems to be that simp uses the equation lemmas if a def is annotated with @[simp]. This makes me wonder why more definitions in the standard library and mathlib aren't @[simp]. It also makes me wonder if I should use @[simp] def more instead of writing equation lemmas myself.

Sean Leather (Mar 01 2018 at 07:52):

library/init/meta/interactive.lean:

private meta def simp_lemmas.resolve_and_add (s : simp_lemmas) (u : list name) (n : name) (ref : pexpr) : tactic (simp_lemmas × list name) :=
do
  p  resolve_name n,
  check_no_overload p,
  -- unpack local refs
  let e := p.erase_annotations.get_app_fn.erase_annotations,
  match e with
  | const n _           :=
    (do b  is_valid_simp_lemma_cnst n, guard b, save_const_type_info n ref, s  s.add_simp n, return (s, u))
    <|>
    (do eqns  get_eqn_lemmas_for tt n, guard (eqns.length > 0), save_const_type_info n ref, s  add_simps s eqns, return (s, u))
    <|>
    (do env  get_env, guard (env.is_projection n).is_some, return (s, n::u))
    <|>
    report_invalid_simp_lemma n
  | _ :=
    (do e  i_to_expr_no_subgoals p, b  is_valid_simp_lemma e, guard b, try (save_type_info e ref), s  s.add e, return (s, u))
    <|>
    report_invalid_simp_lemma n
  end

Simon Hudon (Mar 01 2018 at 07:54):

To your second question: I think you should, it's often less repetitive

Simon Hudon (Mar 01 2018 at 07:54):

I don't know how to answer your first question

Sebastian Ullrich (Mar 01 2018 at 10:01):

There's also #print attribute simp

Sebastian Ullrich (Mar 01 2018 at 10:01):

I believe Leo rather wants us to use simp! than to tag every single def with [simp]

Sean Leather (Mar 01 2018 at 10:03):

There's also #print attribute simp

error: invalid #print command

Sebastian Ullrich (Mar 01 2018 at 10:08):

Ah, this is fun. You can do #print [refl], but not #print [simp].

Sean Leather (Mar 01 2018 at 10:09):

simp!:

  • Add iota_eqn : bool field to simp_config. simp {iota_eqn := tt} uses all non trivial equation lemmas generated by equation/pattern-matching compiler. A lemma is considered non trivial if it is not of the form forall x_1 ... x_n, f x_1 ... x_n = t and a proof by reflexivity. simp! is a shorthand for simp {iota_eqn := tt}. For example, given the goal ... |- [1,2].map nat.succ = t, simp! reduces the left-hand-side of the equation to [nat.succ 1, nat.succ 2]. In this example, simp! is equivalent to simp [list.map].

Moses Schönfinkel (Mar 01 2018 at 10:10):

Getting closer to Coq cbn :).

Sean Leather (Mar 01 2018 at 10:11):

“non-trivial equation lemmas” - What does this imply about the trivial equation lemmas, which all of mine probably are?

Sean Leather (Mar 01 2018 at 10:14):

Ah, this is fun. You can do #print [refl], but not #print [simp].

Is that just a matter of forgetting to include simp somewhere?

Sean Leather (Mar 01 2018 at 10:15):

#print [_refl_lemma] works.

Sebastian Ullrich (Mar 01 2018 at 10:17):

No, #print [simp] is just a different syntax https://github.com/leanprover/lean/blob/39270fd46f49fecb30649f5ec527da7bbd4cdb13/tests/lean/run/simplifier_custom_relations.lean#L23

Sebastian Ullrich (Mar 01 2018 at 10:17):

So yeah, #print [simp] default works

Sean Leather (Mar 01 2018 at 10:18):

“non-trivial equation lemmas” - What does this imply about the trivial equation lemmas, which all of mine probably are?

Considering this comment, I think the description in doc/changes.md above is either confusing or misleading:

+(iota_eqn : bool           := ff) -- reduce using all equation lemmas generated by equation/pattern-matching compiler

Sebastian Ullrich (Mar 01 2018 at 10:19):

No, "non-trivial" basically means "defined by pattern matching"

Sebastian Ullrich (Mar 01 2018 at 10:19):

I.e. "more than one equation"

Sean Leather (Mar 01 2018 at 10:21):

So, could you replace “non trivial equation lemmas generated by equation/pattern-matching compiler. A lemma is considered non trivial if it is not of the form forall x_1 ... x_n, f x_1 ... x_n = t and a proof by reflexivity” above with “equation lemmas generated by equation/pattern-matching compiler” and the statement would be the same?

Sebastian Ullrich (Mar 01 2018 at 10:30):

I'm not sure anymore. Perhaps the iota_eqn comment should instead be extended with a "non-trivial"

Sean Leather (Mar 01 2018 at 10:34):

So yeah, #print [simp] default works

Yeah, it's nice to see my equation lemmas appear in that list after adding @[simp] to a def.

Sean Leather (Mar 01 2018 at 10:35):

I'm not sure if there are any alternative arguments to #print [simp]. It doesn't appear to take a prefix or identifier name: unknown simp_lemmas collection.

Sean Leather (Mar 01 2018 at 10:59):

I get syntax errors on the second simp! in induction xs; [simp!, {cases ts, simp!}].

Sean Leather (Mar 01 2018 at 11:01):

But induction xs; [simp!, {cases ts, simp {iota_eqn := tt}}] works.

Sebastian Ullrich (Mar 01 2018 at 11:28):

!} is a separate token used for hole commands


Last updated: Dec 20 2023 at 11:08 UTC