Inefficiency due to use of old equational reasoning syntax

[Boarders]

At the end of the Debruijn chapter there is an exercise:

Exercise mul-example (recommended)

Using the evaluator, confirm that two times two is four.

I am unsure if you had something clever in mind, but using the same brute force techniques as the examples show seems to not work. For example, I get the following (apologies, I used my own notation but I hope it can still easily be followed:

calc2 : mult-E {∅} ∙ two ∙ two ↡ succ (succ (succ (succ zero)))
calc2 = _ ↓⟨ l-↓ (l-↓ β-rec) ⟩ 
        _ ↓⟨ (l-↓ (β-↓ (V-succ (V-succ V-zero)))) ⟩ 
        _ ↓⟨ (β-↓ (V-succ (V-succ V-zero))) ⟩ 
        _ ↓⟨ (β-succ (V-succ V-zero)) ⟩ 
        _ ↓⟨ (l-↓ (l-↓ β-rec)) ⟩ 
        _ ↓⟨ (l-↓ (β-↓ (V-succ (V-succ V-zero)))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (l-↓ (l-↓ β-rec))) ⟩ 
        _ ↓⟨ r-↓ V-lam (l-↓ (β-↓ (V-succ V-zero))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (β-↓ (V-succ (V-succ V-zero)))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (β-succ V-zero)) ⟩ 
        _ ↓⟨ (r-↓ V-lam (l-↓ (l-↓ β-rec))) ⟩
        _ ↓⟨ (r-↓ V-lam (l-↓ (β-↓ (V-succ (V-succ V-zero))))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (r-↓ V-lam (l-↓ (l-↓ β-rec)))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (r-↓ V-lam (l-↓ (β-↓ V-zero)))) ⟩
        _ ↓⟨ (r-↓ V-lam (r-↓ V-lam (β-↓ (V-succ (V-succ V-zero))))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (r-↓ V-lam β-zero)) ⟩ 
        _ ↓⟨ (r-↓ V-lam (β-↓ V-zero)) ⟩ 
        _ ↓⟨ (r-↓ V-lam (β-succ (V-succ V-zero))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (succ-↓ (l-↓ (l-↓ β-rec)))) ⟩ 
        _ ↓⟨ (r-↓ V-lam (succ-↓ (l-↓ (β-↓ (V-succ V-zero))))) ⟩ 
        _ ↓⟨ {!!} ⟩ {!!}

_ : eval (gas 100) (mult-E ∙ (two) ∙ two) ≡ 
  steps
  calc2
  (done (V-succ (V-succ (V-succ (V-succ V-zero)))))
_ = {!!}

At this point typechecking this file takes longer than ten minutes on my laptop (I aborted after that point). Did you have something else in mind for doing this in a more sensible way? I should also mention it is necessary to have these terms inferred as they are absolutely huge (which is surely the cause of the slowdown).

[wenkokke]

They may be a regression in Agda? @gallais?

[wenkokke]

@Boarders What version of Agda are you using?

[Boarders]

I am using version 2.6.2.1 and here is a full gist: https://gist.github.com/Boarders/035ec1e0734d34c69ab4277de5d4ff32 The relevant bit of code is at the bottom of the file and currently commented out.

[wadler]

I tried it and it completed on my machine with no difficulties, within under a second.

[wadler]

Using Agda version 2.6.1.1-fce01db

[andreasabel]

I am using version 2.6.2.1 and here is a full gist: gist.github.com/Boarders/035ec1e0734d34c69ab4277de5d4ff32

It does take a bit, but less than a minute on my 2016 macBook. Probably you lack main memory, because agda-2.6.2.2 has swallowed 3.85 GB (on the System Monitor) when it reaches the state with the three goals.
To be fair, the first goal (?0) is 3600 lines long (in staircase form)... If I show the goal normalized (C-u C-u C-c C-,) it is suddenly tiny (30 lines, staircase code).

It is not unplausible that this could be a regression in Agda 2.6.2; we had a number of regressions caused by a switch from normalization to weak head normalization in some places (https://github.com/agda/agda/pull/4566). Maybe the discussion of whether this is a regression should be carried out on agda/agda#5860.

[andreasabel]

They may be a regression in Agda? @gallais?

Not a regression, according to my investigation. The behaviour is roughly the same since Agda 2.5.4.

[gallais]

Thanks for the investigation Andreas, I had no idea where to start!

[wenkokke]

The problem seems to be https://github.com/agda/agda-stdlib/issues/622! Thanks @andreasabel and @gallais!

@wadler We should rewrite our reasoning primitives along these lines, I think?

[Boarders]

@wenkokke fantastic! Making this change:

data _↡_  {Γ A} : Expr Γ A → Expr Γ A → Set where
  _∎ : (M : Expr Γ A)
    → M ↡ M

  step-↓ : (L : Expr Γ A) {M N : Expr Γ A}
    → M ↡ N
    → L ↓ M
    → L ↡ N

begin_ : ∀ {Γ A} { M N : Expr Γ A}
  → M ↡ N
  → M ↡ N
begin M↡N = M↡N

infixr 2 step-↓
syntax step-↓ l m↡n l↓m = l ↓⟨ l↓m ⟩ m↡n

makes typechecking happen in under 10 seconds.

[wenkokke]

I suppose this change should eventually make it into the book. I think we currently have a tiny bit of text explaining the discongruence between our reasoning syntax definitions and those of the standard library, which should perhaps be expanded.

[wenkokke]

@wenkokke fantastic! Making this change:

data _↡_  {Γ A} : Expr Γ A → Expr Γ A → Set where
  _∎ : (M : Expr Γ A)
    → M ↡ M

  step-↓ : (L : Expr Γ A) {M N : Expr Γ A}
    → M ↡ N
    → L ↓ M
    → L ↡ N

begin_ : ∀ {Γ A} { M N : Expr Γ A}
  → M ↡ N
  → M ↡ N
begin M↡N = M↡N

infixr 2 step-↓
syntax step-↓ l m↡n l↓m = l ↓⟨ l↓m ⟩ m↡n

makes typechecking happen in under 10 seconds.

@Boarders Could you check what happens when you try to regenerate the proof while you have this definition in scope? If it generates the proof with the step variant, it’s a no-go. However, we may be able to fix that using a display pragma.

[wenkokke]

We should use the version from the standard library in exercises.