continuity tactic and caching failure

Stream: general

[Sebastien Gouezel]

While playing with irreducible continuity, I tried to have a look at what makes the continuity tactic too slow to be really usable. A good example is trans in path_connected.lean, in which two lines are written by hand since continuity is too slow. Put back a continuity there. With set_option trace.class_instances true, one can see that Lean tries several times to find the same instance, with the message caching failure for ...

[Sebastien Gouezel]

@Gabriel Ebner , is that something to be expected?

[Gabriel Ebner]

This is definitely the opposite of expected.

[Sebastien Gouezel]

That's what I was expecting :-)

[Gabriel Ebner]

Weirdly enough, if you insert have : has_mul X, apply_instance instead of continuity, then it fails quickly (and the cache works as expected).

[Sebastien Gouezel]

More minimal example:

import topology.instances.real

set_option trace.class_instances true

def f (X : Type*) (n : ℕ) : Prop := sorry

lemma foo1 (X : Type*) (n : ℕ) [has_mul X] : f X n := sorry

lemma foo2 (X : Type*) (n : ℕ) [has_mul X] : f X n := sorry

lemma bar (X : Type*) (n : ℕ) : f X n :=
begin
  apply_rules [foo1, foo2],
end

The instance trace shows that the instance cache created when trying to apply foo1 is not used when trying to apply foo2.

[Sebastien Gouezel]

This means that continuity will try to infer instances zillions of times (each time it applies a new lemma, it tries again to solve the instances). It's not surprising it's slow then!

[Gabriel Ebner]

Then continuity is even worse, because the cache doesn't work at all there. (There are some cached failure for with apply_rules but not with continuity)

[Sebastien Gouezel]

Yes, it's true, continuity is even worse. If I get it correctly, continuity is essentially apply_rules called from tidy, so both are probably doing something wrong with respect to caching (or caching is doing something wrong with respects to tactics). I don't remember doing anything fancy when I wrote apply_rules, but my tactic writing skills are not really developed :)

[Sebastien Gouezel]

Even more basic example:

import topology.instances.real

set_option trace.class_instances true

def f (X : Type*) (n : ℕ) : Prop := sorry

lemma foo1 (X : Type*) (n : ℕ) [has_mul X] : f X n := sorry

lemma foo2 (X : Type*) (n : ℕ) [field X] : f X n := sorry

lemma bar (X : Type*) (n : ℕ) : f X n :=
begin
  apply foo1 <|> apply foo2,
end

apply foo1 fails, but the instance cache is not preserved for the apply foo2 search. This is normal since <|> does not preserve anything when the first branch fails, if I understand correctly. Instead, one would need a more clever combinator, doing first the instance search for foo1 (and adding it to the instance cache), and then applying foo1 if possible, or going to the foo2 branch if necessary. This is above my pay grade, though :-(

[Sebastien Gouezel]

In fact, I think I know how to fix the apply_rules issue, precisely by replacing the combinator <|> which ditches the state after the application of apply foo1 (and therefore the newly built instance cache) before calling apply foo2. With a new combinator that propagates the state, the instance cache seems to be kept. The code is

section
open interaction_monad.result

parameter {state : Type}
local notation `m` := interaction_monad state

meta def interaction_monad_orelse_propagating_state {α : Type u} (t₁ t₂ : m α) : m α :=
λ s, interaction_monad.result.cases_on (t₁ s)
  success
  (λ e₁ ref₁ s', interaction_monad.result.cases_on (t₂ s')
     success
     exception)
end

meta def apply_list_expr (opt : apply_cfg) : list (tactic expr) → tactic unit
| []     := fail "no matching rule"
| (h::t) :=
@interaction_monad_orelse_propagating_state tactic_state _
  (do e ← h, interactive.concat_tags (apply e opt))
  (apply_list_expr t)

instead of the original

meta def apply_list_expr (opt : apply_cfg) : list (tactic expr) → tactic unit
| []     := fail "no matching rule"
| (h::t) := (do e ← h, interactive.concat_tags (apply e opt)) <|> apply_list_expr t

Does it makes sense, or I am overlooking an obvious issue? (the tests for apply_rules pass as well with the new version)

[Sebastien Gouezel]

@Gabriel Ebner , in fact the problem in the continuity application doesn't seem to be related to the continuitytactic, it already shows up with a single apply. Maybe related to the way caching works along different instance search paths? In topology/path_connected.lean, if you replace the line 298

    { exact ((path.continuous γ).comp continuous_proj_I).comp (continuous_const.mul continuous_id')},

with

    { apply continuous.mul, },

of course this fails, but the instance search message is too long, truncated at 262144 characters, and there are a lot of caching failure for linear_ordered_field X in the instance trace.

[Sebastien Gouezel]

(I guess the linear_ordered_field instances are in fact not the same wrt how the multiplication would be defined, so they count as different)

[Gabriel Ebner]

This is interesting.

[Gabriel Ebner]

Sebastien Gouezel said:

(I guess the linear_ordered_field instances are in fact not the same wrt how the multiplication would be defined, so they count as different)

The caching mechanism assumes that all instances are definitionally equal. It won't try to find an instance twice.

[Sebastien Gouezel]

Then it's really weird

[Sebastien Gouezel]

Issue registered as lean#504. I could not minimize further than

import topology.algebra.infinite_sum

set_option trace.class_instances true

lemma blah (α : Type*) [topological_space α] (f : ℝ → α) : continuous f :=
begin
  apply continuous.mul,
end

(the trace of the failing apply is really scary)

[Sebastien Gouezel]

lean#505. @Gabriel Ebner is amazing, but we already knew that :smiley: