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: Dec 20 2023 at 11:08 UTC