simplifier

Stream: general

[Sebastien Gouezel]

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]

Does dsimp work?

[Sebastien Gouezel]

Yes it does.

[Gabriel Ebner]

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]

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]

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]

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]

simp should handle this

[Mario Carneiro]

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

[Floris van Doorn]

Oh yeah, my example is wrong, simp does handly my case correctly.

[Floris van Doorn]

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]

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]

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]

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

[Mario Carneiro]

you get the right answer with dsimp [depth] or simp only [depth]

[Alexander Bentkamp]

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]

I think simp is just doing a silly thing here

[Mario Carneiro]

I prefer depth + 1 since it's definitionally succ depth