# 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):

- 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: May 16 2021 at 20:13 UTC