Stream: math-comp analysis

Topic: Rewriting takes long time, how to debug?

view this post on Zulip abab9579 (Sep 08 2022 at 00:50):

Hello, I have a code which hangs for so long on rewrite tactic.
I profiled it, it turns out rewrite in ssreflect cannot be broken down into inner invocations.

total time:  69.352s

 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─rewrite (ssrrwargs) (ssrclauses) ------ 100.0% 100.0%       1   69.352s

 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─rewrite (ssrrwargs) (ssrclauses) ------ 100.0% 100.0%       1   69.352s

It runs for so long, but it is not infinite loop - it stops at 69.352s.
Let's say this is rewrite fooE.
Funny thing is, rewrite {1}fooE terminates instantly. rewrite {2}fooE runs indefinitely long, though.
What is the possible cause of this? How do I debug this problem? I do not even know where to look for.

Thanks in advance!

view this post on Zulip Cyril Cohen (Sep 08 2022 at 13:50):

Can we have a concrete piece of code where rewrite takes time?

view this post on Zulip abab9579 (Sep 11 2022 at 11:51):

Oh right, this topic should be in #math-comp analysis . Sorry..

Basically, I have this setup for bounded operators.
Then, I define frechet differential in different file :

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum matrix.
From mathcomp Require Import boolp reals classical_sets signed topology functions.
From mathcomp Require Import prodnormedzmodule normedtype landau forms derive.
From mathcomp Require Import ring.
From manifolds Require Import lineartopo.

Set Implicit Arguments.

Import GRing.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section FrechetDiff.
Context (R: realType) (U V: normedModType R).

Definition frechet_diff (f : U -> V) x : {bounded U -> V} :=
  xget 0 [set df : {bounded U -> V} | 'd f x = df].

Definition fdiffble (f: U -> V) := forall x, differentiable f x.

End FrechetDiff.

Arguments fdiffble {R} {U V} f.

Notation "''D' f" := (@frechet_diff _ _ _ f) (at level 100, f at level 0).


Lemma frechet_diffE (R: realType) (U V: normedModType R) (f : U -> V) x :
  differentiable f x -> 'D f x = 'd f x :> {linear U -> V}.
Proof.
move=> Hf. have HC : linear_conti ('d f x).
- rewrite in_setE /=. by have := diff_continuous Hf.
pose df := BddLinear HC.
rewrite /frechet_diff (@xget_subset1 _ 0 _ df) //.
move=> da db /= ->. apply/val_inj.
Qed.

Section FrechetProps.
Context (R: realType) (U V W: normedModType R).
Implicit Types (f g : U -> V).

Lemma frechet_diff_cst c : 'D (cst c) = 0 :> (U -> {bounded U -> V}).
Proof.
apply/funext=> x. apply/val_inj=> /=.
rewrite frechet_diffE; last by apply/differentiable_cst.
apply/linear_eq/diff_cst.
Qed.

Lemma frechet_diffD f g : fdiffble f -> fdiffble g ->
  'D (f + g) = 'D f + 'D g.
Proof.
move=> Hf Hg. apply/funext=> x. apply/val_inj=> /=.
rewrite frechet_diffE.

The last line, rewrite frechet_diffE, takes tens of seconds to execute.

view this post on Zulip Notification Bot (Sep 11 2022 at 11:52):

A message was moved here from #math-comp users > Rewriting takes long time, how to debug? by Karl Palmskog.

view this post on Zulip Notification Bot (Sep 11 2022 at 11:53):

abab9579 has marked this topic as resolved.

view this post on Zulip abab9579 (Sep 11 2022 at 11:53):

(Moved to math-comp analysis)

view this post on Zulip Karl Palmskog (Sep 11 2022 at 11:58):

better to move the whole thing, I think

view this post on Zulip Notification Bot (Sep 11 2022 at 11:58):

Karl Palmskog has marked this topic as unresolved.

view this post on Zulip Notification Bot (Sep 11 2022 at 11:59):

This topic was moved here from #math-comp users > Rewriting takes long time, how to debug? by Karl Palmskog.

view this post on Zulip Pierre Roux (Sep 11 2022 at 14:01):

Just a wild guess: the following means that, in order to rewrite frechet_diffE, rewrite has to find a linear structure on something somewhere in the goal, which can be difficult.

Lemma frechet_diffE (R: realType) (U V: normedModType R) (f : U -> V) x :
  differentiable f x -> 'D f x = 'd f x :> {linear U -> V}.

To better see this, you can

Set Printing All.
Check frechet_difE

view this post on Zulip abab9579 (Sep 11 2022 at 14:21):

Wow, it gives huge type.

frechet_diffE
     : forall (R : Real.type)
         (U
          V : @NormedModule.type (Real.numDomainType R) (Phant (Real.sort R)))
         (f : forall
                _ : @NormedModule.sort (Real.numDomainType R)
                      (Phant (Real.sort R)) U,
              @NormedModule.sort (Real.numDomainType R)
                (Phant (Real.sort R)) V)
         (x : @Filtered.sort
                (@NormedModule.sort (Real.numDomainType R)
                   (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)
                (Topological.filteredType
                   (@NormedModule.topologicalType
                      (Real.numDomainType R)
                      (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)))
         (_ : @differentiable_def (Real.numDomainType R) U V f
                (@nbhs_filter_on
                   (@NormedModule.topologicalType
                      (Real.numDomainType R)
                      (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)
                   x)
                (Phantom
                   (set
                      (set
                         (@NormedModule.sort (Real.numDomainType R)
                            (Phant
                               (Num.NumDomain.sort (Real.numDomainType R))) U)))
                   (@filter_of
                      (@NormedModule.sort (Real.numDomainType R)
                         (Phant (Num.NumDomain.sort (Real.numDomainType R)))
                         U)
                      (Topological.filteredType
                         (@NormedModule.topologicalType
                            (Real.numDomainType R)
                            (Phant
                               (Num.NumDomain.sort (Real.numDomainType R))) U))
                      x
                      (Phantom
                         (@Filtered.sort
                            (@NormedModule.sort (Real.numDomainType R)
                               (Phant
                                  (Num.NumDomain.sort (Real.numDomainType R)))
                               U)
                            (Topological.filteredType
                               (@NormedModule.topologicalType
                                  (Real.numDomainType R)
                                  (Phant
                                     (Num.NumDomain.sort
                                        (Real.numDomainType R))) U))) x)))),
       @eq
         (@GRing.Linear.map (Num.NumDomain.ringType (Real.numDomainType R))
            (@NormedModule.lmodType (Real.numDomainType R)
               (Phant
                  (GRing.Ring.sort
                     (Num.NumDomain.ringType (Real.numDomainType R)))) U)
            (@GRing.Lmodule.zmodType
               (Num.NumDomain.ringType (Real.numDomainType R))
               (Phant
                  (GRing.Ring.sort
                     (Num.NumDomain.ringType (Real.numDomainType R))))
               (@NormedModule.lmodType (Real.numDomainType R)
                  (Phant
                     (GRing.Ring.sort
                        (Num.NumDomain.ringType (Real.numDomainType R)))) V))
            (@GRing.scale (Num.NumDomain.ringType (Real.numDomainType R))
               (@NormedModule.lmodType (Real.numDomainType R)
                  (Phant
                     (GRing.Ring.sort
                        (Num.NumDomain.ringType (Real.numDomainType R)))) V))
            (Phant
               (forall
                  _ : @NormedModule.sort (Real.numDomainType R)
                        (Phant (Real.sort R)) U,
                @NormedModule.sort (Real.numDomainType R)
                  (Phant (Real.sort R)) V)))
         (@bdval R U V
            (Phant
               (forall
                  _ : @NormedModule.sort (Real.numDomainType R)
                        (Phant (Real.sort R)) U,
                @NormedModule.sort (Real.numDomainType R)
                  (Phant (Real.sort R)) V)) (@frechet_diff R U V f x))
         (@diff (Real.numDomainType R) U V
            (@nbhs_filter_on
               (@NormedModule.topologicalType (Real.numDomainType R)
                  (Phant (Num.NumDomain.sort (Real.numDomainType R))) U) x)
            (Phantom
               (set
                  (set
                     (@NormedModule.sort (Real.numDomainType R)
                        (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)))
               (@filter_of
                  (@NormedModule.sort (Real.numDomainType R)
                     (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)
                  (Topological.filteredType
                     (@NormedModule.topologicalType
                        (Real.numDomainType R)
                        (Phant (Num.NumDomain.sort (Real.numDomainType R))) U))
                  x
                  (Phantom
                     (@Filtered.sort
                        (@NormedModule.sort (Real.numDomainType R)
                           (Phant (Num.NumDomain.sort (Real.numDomainType R)))
                           U)
                        (Topological.filteredType
                           (@NormedModule.topologicalType
                              (Real.numDomainType R)
                              (Phant
                                 (Num.NumDomain.sort (Real.numDomainType R)))
                              U))) x))) f)

view this post on Zulip abab9579 (Sep 11 2022 at 14:23):

I don't see finding linear structure part though.

view this post on Zulip Karl Palmskog (Sep 11 2022 at 14:26):

the "huge" part is due to this, but it's at least better than this

view this post on Zulip Pierre Roux (Sep 11 2022 at 14:31):

The equality is on Linear, the left hand side has bdval at its head, I guess, this came from unfolding frechet_diff. Maybe locking frechet_diff could help.

view this post on Zulip abab9579 (Sep 11 2022 at 15:15):

This does not improve the performance:

Definition frechet_diff (f : U -> V) x : {bounded U -> V} :=
  locked xget 0 [set df : {bounded U -> V} | 'd f x = df].

Where should I lock instead?

view this post on Zulip Pierre Roux (Sep 11 2022 at 15:17):

What about?

Definition frechet_diff (f : U -> V) x : {bounded U -> V} :=
  locked (xget 0 [set df : {bounded U -> V} | 'd f x = df]).

view this post on Zulip abab9579 (Sep 11 2022 at 15:25):

Definition frechet_diff (f : U -> V) x : {bounded U -> V} :=
  locked (xget 0 [set df : {bounded U -> V} | 'd f x = df]).

Problem still persists with this ^

The type is still this:

frechet_diff : forall (R : Real.type)
      (U V : @NormedModule.type (Real.numDomainType R) (Phant (Real.sort R)))
      (f : forall
             _ : @NormedModule.sort (Real.numDomainType R)
                   (Phant (Real.sort R)) U,
           @NormedModule.sort (Real.numDomainType R) (Phant (Real.sort R)) V)
      (x : @Filtered.sort
             (@NormedModule.sort (Real.numDomainType R)
                (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)
             (Topological.filteredType
                (@NormedModule.topologicalType (Real.numDomainType R)
                   (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)))
      (_ : @differentiable_def (Real.numDomainType R) U V f
             (@nbhs_filter_on
                (@NormedModule.topologicalType (Real.numDomainType R)
                   (Phant (Num.NumDomain.sort (Real.numDomainType R))) U) x)
             (Phantom
                (set
                   (set
                      (@NormedModule.sort (Real.numDomainType R)
                         (Phant (Num.NumDomain.sort (Real.numDomainType R)))
                         U)))
                (@filter_of
                   (@NormedModule.sort (Real.numDomainType R)
                      (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)
                   (Topological.filteredType
                      (@NormedModule.topologicalType
                         (Real.numDomainType R)
                         (Phant (Num.NumDomain.sort (Real.numDomainType R)))
                         U)) x
                   (Phantom
                      (@Filtered.sort
                         (@NormedModule.sort (Real.numDomainType R)
                            (Phant
                               (Num.NumDomain.sort (Real.numDomainType R))) U)
                         (Topological.filteredType
                            (@NormedModule.topologicalType
                               (Real.numDomainType R)
                               (Phant
                                  (Num.NumDomain.sort (Real.numDomainType R)))
                               U))) x)))),
    @eq
      (@GRing.Linear.map (Num.NumDomain.ringType (Real.numDomainType R))
         (@NormedModule.lmodType (Real.numDomainType R)
            (Phant
               (GRing.Ring.sort
                  (Num.NumDomain.ringType (Real.numDomainType R)))) U)
         (@GRing.Lmodule.zmodType
            (Num.NumDomain.ringType (Real.numDomainType R))
            (Phant
               (GRing.Ring.sort
                  (Num.NumDomain.ringType (Real.numDomainType R))))
            (@NormedModule.lmodType (Real.numDomainType R)
               (Phant
                  (GRing.Ring.sort
                     (Num.NumDomain.ringType (Real.numDomainType R)))) V))
         (@GRing.scale (Num.NumDomain.ringType (Real.numDomainType R))
            (@NormedModule.lmodType (Real.numDomainType R)
               (Phant
                  (GRing.Ring.sort
                     (Num.NumDomain.ringType (Real.numDomainType R)))) V))
         (Phant
            (forall
               _ : @NormedModule.sort (Real.numDomainType R)
                     (Phant (Real.sort R)) U,
             @NormedModule.sort (Real.numDomainType R)
               (Phant (Real.sort R)) V)))
      (@bdval R U V
         (Phant
            (forall
               _ : @NormedModule.sort (Real.numDomainType R)
                     (Phant (Real.sort R)) U,
             @NormedModule.sort (Real.numDomainType R)
               (Phant (Real.sort R)) V)) (@frechet_diff R U V f x))
      (@diff (Real.numDomainType R) U V
         (@nbhs_filter_on
            (@NormedModule.topologicalType (Real.numDomainType R)
               (Phant (Num.NumDomain.sort (Real.numDomainType R))) U) x)
         (Phantom
            (set
               (set
                  (@NormedModule.sort (Real.numDomainType R)
                     (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)))
            (@filter_of
               (@NormedModule.sort (Real.numDomainType R)
                  (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)
               (Topological.filteredType
                  (@NormedModule.topologicalType (Real.numDomainType R)
                     (Phant (Num.NumDomain.sort (Real.numDomainType R))) U))
               x
               (Phantom
                  (@Filtered.sort
                     (@NormedModule.sort (Real.numDomainType R)
                        (Phant (Num.NumDomain.sort (Real.numDomainType R))) U)
                     (Topological.filteredType
                        (@NormedModule.topologicalType
                           (Real.numDomainType R)
                           (Phant (Num.NumDomain.sort (Real.numDomainType R)))
                           U))) x))) f)

view this post on Zulip Pierre Roux (Sep 11 2022 at 16:54):

Ok, the problem is probably not the fact that rewrite unfolds frechet_diff but rather probably the fact that you have this bdval (don't know what it is) around frechet diff. If you don't have it in you goal, that could explain why rewrite is in trouble.

view this post on Zulip Pierre Roux (Sep 11 2022 at 16:56):

Can't you replace :> {linear U -> V} by :> {bounded U -> V} (the type of frechet_diff) in frechet_diffE?

view this post on Zulip abab9579 (Sep 11 2022 at 22:59):

No, this is impossible. 'd f x : {linear U -> V}, and {bounded U -> V} is subtype of it, there is no way to automatically get the latter from former.
After apply/funext=> x. apply/val_inj=> /=., the equation effectively becomes
bdval ('D (f + g) x) = bdval ('D f x) + bdval ('D g x)
So there is definitely bdval.

view this post on Zulip abab9579 (Sep 11 2022 at 22:59):

The setup of {bounded U -> V} and bdval is here: https://gist.github.com/Abastro/036f5c410dae630106dd75440746887b

view this post on Zulip Pierre Roux (Sep 12 2022 at 08:45):

Ok, thanks for the explanation, then I'm afraid you have no other choice than Set Printing All and inspect the goal and frechet_diffE to pinpoint the difference.

view this post on Zulip abab9579 (Sep 12 2022 at 08:46):

Oh. So.. should I look into the unfolded terms and compare them?

view this post on Zulip Pierre Roux (Sep 12 2022 at 08:47):

If you think they should be the same, yes.

view this post on Zulip Pierre Roux (Sep 12 2022 at 08:49):

If you have both bdval and frechet_diff in both the lemma and the goal, then the difference likely lies in the other arguments (of bdval or grechet_diff)

Last updated: Sep 28 2023 at 11:01 UTC