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

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