# Zulip Chat Archive

## Stream: general

### Topic: simplifier

#### Sebastien Gouezel (Oct 23 2018 at 09:27):

I'm realizing I don't understand how the simplifier works. I have a complicated goal involving product spaces, and in the middle of this goal there is the expression `(f, x).fst`

. When I apply `simp`

to my goal, it does not reduce to `f`

. To help simp, I wrote down an auxiliary statement exactly with the good types and elements `f`

and `x`

, but still it does not help `simp`

. Even when I turn on `set_option pp.all true`

I can't see what is wrong.

My helper lemma is `should_help : (prod.mk f x).fst = f`

. Fully expanded, it reads

should_help : @eq.{(max u v)+1} (@bounded_continuous_function.{u v} α β _inst_1 _inst_2) (@prod.fst.{(max u v) u} (@bounded_continuous_function.{u v} α β _inst_1 _inst_2) α (@prod.mk.{(max u v) u} (@bounded_continuous_function.{u v} α β _inst_1 _inst_2) α f x)) f

And in my goal I have the lines

(@prod.fst.{(max u v) u} (@bounded_continuous_function.{u v} α β _inst_1 _inst_2) α (@prod.mk.{(max u v) u} (@bounded_continuous_function.{u v} α β _inst_1 _inst_2) α f x))

Can someone explain why `simp [should_help]`

does not reduce this term to `f`

? (I can certainly work it around, but still I would be very happy to understand what is going on here...)

#### Gabriel Ebner (Oct 23 2018 at 09:29):

Does `dsimp`

work?

#### Sebastien Gouezel (Oct 23 2018 at 09:32):

Yes it does.

#### Gabriel Ebner (Oct 23 2018 at 09:38):

Then welcome to dependent type theory! Basically `simp`

can only rewrite at non-dependent arguments. The automatically generated congruence lemmas only have hypotheses for the non-dependent arguments. We could also rewrite at dependent arguments, but then you'd get casts all over the place.

#### Sebastien Gouezel (Oct 23 2018 at 09:45):

OK. Not sure I really understand: is the problem the fact that my type is `@bounded_continuous_function.{u v} α β _inst_1 _inst_2`

, so depending on other types and instances? In any case, thanks a lot, I will add `dsimp`

to my toolbox and try to apply it when `simp`

does not work, even if I don't know why. (And this is a perfectly well-defined and efficient algorithm!)

#### Gabriel Ebner (Oct 23 2018 at 09:53):

No, I think the problem is that `prod.fst ...`

*occurs* as a subterm of some dependent argument, and hence simp cannot reach it.

#### Floris van Doorn (Oct 23 2018 at 17:23):

Consider the following example: suppose `h`

has type `is_prime (1+n)`

and somewhere in the goal I have `⟨1+n, h⟩`

as a subterm. Suppose I want to rewrite `1+n`

to `n+1`

using (using `rw [add.comm 1 n]`

or `simp`

) then I get the subterm `⟨1+n, h⟩`

, but this is not type correct: `h`

has type `is_prime (1+n)`

, not type `is_prime (n+1)`

. Therefore, `rw`

and `simp`

will fail if you do this.

Now we modify the example, and `h`

has type `is_prime (1+4)`

. `1+4`

and `5`

are definitionally equal, which implies that `h`

*also* has type `is_prime 5`

. Therefore, if your goal contains `⟨2+3, h⟩`

you are allowed to rewrite this to `⟨5, h⟩`

. However, `simp`

and `rw`

will not do this for you, but `dsimp`

(which only rewrites with definitional equalities) happily will.

#### Mario Carneiro (Oct 23 2018 at 17:28):

simp should handle this

#### Mario Carneiro (Oct 23 2018 at 17:42):

simp will produce a term like `⟨1+n, cast (add_comm 1 n) h⟩`

#### Floris van Doorn (Oct 23 2018 at 18:26):

Oh yeah, my example is wrong, `simp`

does handly my case correctly.

#### Floris van Doorn (Oct 23 2018 at 18:30):

but only because `is_prime`

is a proposition. If you replace `is_prime`

by `vector bool`

or anything else living in `Type*`

, then what I described is correct.

#### Mario Carneiro (Oct 23 2018 at 18:38):

Actually it will work as long as the second argument is a subsingleton. This is because this cast thing is being inserted by the congr lemma, that automatically discharges subsingleton arguments (even if they are in Type)

#### Alexander Bentkamp (Jun 05 2019 at 12:51):

We found a strange behavior with the simplifier setup. The congruence rule `if_simp_congr`

introduces an extra term `@decidable_of_decidable_of_iff`

even though nothing is rewritten under the if-then-else, which then leads to subtle unification failures.

Here is an example:

local attribute [instance, priority 0] classical.prop_decidable inductive tree (α : Type) | leaf : ℕ → α → tree | inner : ℕ → tree → tree → tree export tree (leaf inner) variable {α : Type} noncomputable def depth : tree α → α → α → ℕ | (leaf _ _) _ _ := 0 | (inner _ l r) a b := if a = b then depth l a b + 1 else 0 set_option pp.implicit true set_option trace.simplify.perm true set_option trace.simplify.congruence true -- local attribute [-congr] if_simp_congr example (a b : α) (w : ℕ) (l r : tree α) : depth (inner w l r) a b = 0 := begin simp [depth], end

#### Mario Carneiro (Jun 05 2019 at 14:49):

simp is rewriting under the if though; it changes `depth + 1`

to `1 + depth`

#### Mario Carneiro (Jun 05 2019 at 14:50):

you get the right answer with `dsimp [depth]`

or `simp only [depth]`

#### Alexander Bentkamp (Jun 05 2019 at 20:07):

Mario Carneiro: simp is rewriting under the if though; it changes

`depth + 1`

to`1 + depth`

Oh, right. I didn't notice that. The problem can also be avoided by using `1 + depth`

in the definition, which would probably be a useful thing to do anyway.

#### Mario Carneiro (Jun 05 2019 at 20:19):

I think simp is just doing a silly thing here

#### Mario Carneiro (Jun 05 2019 at 20:20):

I prefer `depth + 1`

since it's definitionally `succ depth`

Last updated: May 06 2021 at 21:09 UTC