[Agda] How does one debug a programme that one has proved correct?

[Philip Wadler]

I have an Agda formalisation of reduction on raw terms (inspired by a
formalisation of McBride acting on a deBruijn representation). The
formalisation is here:

https://wenkokke.github.io/sf/TypedFresh

Although more elaborate than I would like in parts, at least I succeed in
proving progress and preservation for the system. Combining the two allows
me to write a function that computes the reduction sequence for a term
bounding by a given length. If the reduction sequence is longer than the
specified length n, it returns the sequence of length n with the indicator
"out of gas". I then tried to compute the reduction sequence for two plus
two.

Computing the first four reduction steps takes a couple of minutes rather
than a couple of seconds. Attempting to normalise the term fully (which
should take fourteen reduction steps) does not complete even if run
overnight!

{-
_ : normalise 4 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ 0 ⇒
`if0 `suc (`suc `zero) then ` 0 else
(`Y
(`λ 1 ⇒
(`λ 2 ⇒ (`λ 3 ⇒ `if0 ` 2 then ` 3 else ` 1 · (`pred ` 2) · ` 3))))
· (`pred (`suc (`suc `zero)))
· ` 0)
· (`suc (`suc `zero))
⟶⟚ β-⇒ (Suc (Suc Zero)) ⟩
`if0 `suc (`suc `zero) then `suc (`suc `zero) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
⟶⟚ β-if0-suc (Suc Zero) ⟩
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
∎)
_ = refl
-}

To try to uncover the problem, I attempted a single step at a time. The
first reduction step is fine.

{-
_ : normalise 1 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
_ = refl
-}

The second reduction step yields a huge term. It contains the free variable
_x_1862 where I would have expected a fresh variable name to be computed.
Looking at the four-step reduction above we see the name computed properly,
but when going from the first step to the second it is not. The huge size
of the type derivation suggests why it did not terminate after one day.

Help! Why doesn’t the term reduce? Is there some way to force it to reduce?

Cheers, -- P

{-
_ : normalise 1
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
≡
out-of-gas
((`λ _x_1862 ⇒
(`λ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ⇒
`if0 ` _x_1862 then
` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` _x_1862)
· ` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
`if0
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
then
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
else
(`Y
(`λ
suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
(`λ
suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⇒
(`λ
suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⇒
`if0
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
then
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc
_xs_1887))))))))
else
`
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
·
(`pred
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc
_xs_1887))))))))
·
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬?
(_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc
_xs_1887))))))))))))
·
(`pred
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
·
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢if0
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈) CollectionDec.here
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(S (fresh-lemma CollectionDec.here) Z)
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there CollectionDec.here)
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
Z
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(⊢subst
(λ {w} w∈′ {z₁} →
.Typed.Σ′
(λ {w₁} w∈ {z₂} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w₁ ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016) w∈′
| w ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(λ {z₁} x →
CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there (CollectionDec.there x))
| z₁ ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
_2016))
· ⊢suc (⊢suc ⊢zero))
-}




. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

[Ulf Norell]

Something is indeed strange. Some observations:

- _x_1862 is an unsolved metavariable. If I paste in the term in your
example there
is indeed some yellow. When printing a term Agda hides all implicit
arguments without
regard for whether they can actually be inferred (since this is
impractical to figure out).
This means that you often cannot take a printed term and type check it
without ending
up with some yellow.

- On recent development Agda I can normalise (C-c C-n) `normalise 15 ⊢four`
in a handful of milliseconds. (It requires 15 fuel, and since you forgot
the Suc
in the recursive case of ⊢plus, normalises to two instead of four).
However, trying to prove that it reaches a normal form I get stuck:

IsNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Set
IsNormal (out-of-gas _ _) = ⊥
IsNormal (normal _ _ _) = ⊀

prf : IsNormal (normalise 15 ⊢four)
prf = tt -- does not come back

On the other hand the following variant works fine:

prf' : IsNormal (normalise 15 ⊢four) ≡ ⊀
prf' = refl -- checks in no time

It's all very mysterious. I'll investigate deeper when I get a chance.

/ Ulf

Post by Philip Wadler
I have an Agda formalisation of reduction on raw terms (inspired by a
formalisation of McBride acting on a deBruijn representation). The
https://wenkokke.github.io/sf/TypedFresh
Although more elaborate than I would like in parts, at least I succeed in
proving progress and preservation for the system. Combining the two allows
me to write a function that computes the reduction sequence for a term
bounding by a given length. If the reduction sequence is longer than the
specified length n, it returns the sequence of length n with the indicator
"out of gas". I then tried to compute the reduction sequence for two plus
two.
Computing the first four reduction steps takes a couple of minutes rather
than a couple of seconds. Attempting to normalise the term fully (which
should take fourteen reduction steps) does not complete even if run
overnight!
{-
_ : normalise 4 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ 0 ⇒
`if0 `suc (`suc `zero) then ` 0 else
(`Y
(`λ 1 ⇒
(`λ 2 ⇒ (`λ 3 ⇒ `if0 ` 2 then ` 3 else ` 1 · (`pred ` 2) · ` 3))))
· (`pred (`suc (`suc `zero)))
· ` 0)
· (`suc (`suc `zero))
⟶⟚ β-⇒ (Suc (Suc Zero)) ⟩
`if0 `suc (`suc `zero) then `suc (`suc `zero) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
⟶⟚ β-if0-suc (Suc Zero) ⟩
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
∎)
_ = refl
-}
To try to uncover the problem, I attempted a single step at a time. The
first reduction step is fine.
{-
_ : normalise 1 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
_ = refl
-}
The second reduction step yields a huge term. It contains the free
variable _x_1862 where I would have expected a fresh variable name to be
computed. Looking at the four-step reduction above we see the name computed
properly, but when going from the first step to the second it is not. The
huge size of the type derivation suggests why it did not terminate after
one day.
Help! Why doesn’t the term reduce? Is there some way to force it to reduce?
Cheers, -- P
{-
_ : normalise 1
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
≡
out-of-gas
((`λ _x_1862 ⇒
(`λ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ⇒
`if0 ` _x_1862 then
` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` _x_1862)
· ` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
`if0
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
then
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
else
(`Y
(`λ
suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
(`λ
suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⇒
(`λ
suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⇒
`if0
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
then
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
else
`
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
·
(`pred
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
·
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬?
(_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))))))
·
(`pred
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
·
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢if0
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈) CollectionDec.here
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(S (fresh-lemma CollectionDec.here) Z)
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there CollectionDec.here)
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
Z
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(⊢subst
(λ {w} w∈′ {z₁} →
.Typed.Σ′
(λ {w₁} w∈ {z₂} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w₁ ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016) w∈′
| w ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(λ {z₁} x →
CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there (CollectionDec.there x))
| z₁ ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
_2016))
· ⊢suc (⊢suc ⊢zero))
-}
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Philip Wadler]

Thanks, Ulf! How do I get the most recent development version? It sounds
like that might resolve my problem. Although understanding what went wrong
would still be very helpful indeed, so I would be most appreciative if you
could look into it.

Thanks for pointing out that the definition was wrong. I've fixed the
definition of plus in the repository, so you won't have to contend with the
indignity of (plus two two) yielding two rather than four.

Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell
- _x_1862 is an unsolved metavariable. If I paste in the term in your
example there
is indeed some yellow. When printing a term Agda hides all implicit
arguments without
regard for whether they can actually be inferred (since this is
impractical to figure out).
This means that you often cannot take a printed term and type check it
without ending
up with some yellow.
- On recent development Agda I can normalise (C-c C-n) `normalise 15 ⊢four`
in a handful of milliseconds. (It requires 15 fuel, and since you forgot
the Suc
in the recursive case of ⊢plus, normalises to two instead of four).
IsNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Set
IsNormal (out-of-gas _ _) = ⊥
IsNormal (normal _ _ _) = ⊀
prf : IsNormal (normalise 15 ⊢four)
prf = tt -- does not come back
prf' : IsNormal (normalise 15 ⊢four) ≡ ⊀
prf' = refl -- checks in no time
It's all very mysterious. I'll investigate deeper when I get a chance.
/ Ulf

Post by Philip Wadler
I have an Agda formalisation of reduction on raw terms (inspired by a
formalisation of McBride acting on a deBruijn representation). The
https://wenkokke.github.io/sf/TypedFresh
Although more elaborate than I would like in parts, at least I succeed in
proving progress and preservation for the system. Combining the two allows
me to write a function that computes the reduction sequence for a term
bounding by a given length. If the reduction sequence is longer than the
specified length n, it returns the sequence of length n with the indicator
"out of gas". I then tried to compute the reduction sequence for two plus
two.
Computing the first four reduction steps takes a couple of minutes rather
than a couple of seconds. Attempting to normalise the term fully (which
should take fourteen reduction steps) does not complete even if run
overnight!
{-
_ : normalise 4 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ 0 ⇒
`if0 `suc (`suc `zero) then ` 0 else
(`Y
(`λ 1 ⇒
(`λ 2 ⇒ (`λ 3 ⇒ `if0 ` 2 then ` 3 else ` 1 · (`pred ` 2) · ` 3))))
· (`pred (`suc (`suc `zero)))
· ` 0)
· (`suc (`suc `zero))
⟶⟚ β-⇒ (Suc (Suc Zero)) ⟩
`if0 `suc (`suc `zero) then `suc (`suc `zero) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
⟶⟚ β-if0-suc (Suc Zero) ⟩
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
∎)
_ = refl
-}
To try to uncover the problem, I attempted a single step at a time. The
first reduction step is fine.
{-
_ : normalise 1 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
_ = refl
-}
The second reduction step yields a huge term. It contains the free
variable _x_1862 where I would have expected a fresh variable name to be
computed. Looking at the four-step reduction above we see the name computed
properly, but when going from the first step to the second it is not. The
huge size of the type derivation suggests why it did not terminate after
one day.
Help! Why doesn’t the term reduce? Is there some way to force it to reduce?
Cheers, -- P
{-
_ : normalise 1
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
≡
out-of-gas
((`λ _x_1862 ⇒
(`λ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ⇒
`if0 ` _x_1862 then
` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` _x_1862)
· ` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
`if0
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
then
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
else
(`Y
(`λ
suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
(`λ
suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⇒
(`λ
suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⇒
`if0
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
then
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
else
`
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
·
(`pred
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
·
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬?
(_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))))))
·
(`pred
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
·
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢if0
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈) CollectionDec.here
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(S (fresh-lemma CollectionDec.here) Z)
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there CollectionDec.here)
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
Z
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(⊢subst
(λ {w} w∈′ {z₁} →
.Typed.Σ′
(λ {w₁} w∈ {z₂} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w₁ ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016) w∈′
| w ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(λ {z₁} x →
CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there (CollectionDec.there x))
| z₁ ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
_2016))
· ⊢suc (⊢suc ⊢zero))
-}
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Ulf Norell]

You can clone the Agda repo at https://github.com/agda/agda. I was using
the `stable-2.5`
branch, but I would expect `master` to work the same (the difference is
@saizan's cubical
type theory goodness which is only on master). It should (fingers crossed)
build and install
with `make install-bin` or even `cabal install`.

/ Ulf

Post by Philip Wadler
Thanks, Ulf! How do I get the most recent development version? It sounds
like that might resolve my problem. Although understanding what went wrong
would still be very helpful indeed, so I would be most appreciative if you
could look into it.
Thanks for pointing out that the definition was wrong. I've fixed the
definition of plus in the repository, so you won't have to contend with the
indignity of (plus two two) yielding two rather than four.
Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell
- _x_1862 is an unsolved metavariable. If I paste in the term in your
example there
is indeed some yellow. When printing a term Agda hides all implicit
arguments without
regard for whether they can actually be inferred (since this is
impractical to figure out).
This means that you often cannot take a printed term and type check it
without ending
up with some yellow.
- On recent development Agda I can normalise (C-c C-n) `normalise 15 ⊢four`
in a handful of milliseconds. (It requires 15 fuel, and since you
forgot the Suc
in the recursive case of ⊢plus, normalises to two instead of four).
IsNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Set
IsNormal (out-of-gas _ _) = ⊥
IsNormal (normal _ _ _) = ⊀
prf : IsNormal (normalise 15 ⊢four)
prf = tt -- does not come back
prf' : IsNormal (normalise 15 ⊢four) ≡ ⊀
prf' = refl -- checks in no time
It's all very mysterious. I'll investigate deeper when I get a chance.
/ Ulf

Post by Philip Wadler
I have an Agda formalisation of reduction on raw terms (inspired by a
formalisation of McBride acting on a deBruijn representation). The
https://wenkokke.github.io/sf/TypedFresh
Although more elaborate than I would like in parts, at least I succeed
in proving progress and preservation for the system. Combining the two
allows me to write a function that computes the reduction sequence for a
term bounding by a given length. If the reduction sequence is longer than
the specified length n, it returns the sequence of length n with the
indicator "out of gas". I then tried to compute the reduction sequence for
two plus two.
Computing the first four reduction steps takes a couple of minutes
rather than a couple of seconds. Attempting to normalise the term fully
(which should take fourteen reduction steps) does not complete even if run
overnight!
{-
_ : normalise 4 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ 0 ⇒
`if0 `suc (`suc `zero) then ` 0 else
(`Y
(`λ 1 ⇒
(`λ 2 ⇒ (`λ 3 ⇒ `if0 ` 2 then ` 3 else ` 1 · (`pred ` 2) · ` 3))))
· (`pred (`suc (`suc `zero)))
· ` 0)
· (`suc (`suc `zero))
⟶⟚ β-⇒ (Suc (Suc Zero)) ⟩
`if0 `suc (`suc `zero) then `suc (`suc `zero) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
⟶⟚ β-if0-suc (Suc Zero) ⟩
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
∎)
_ = refl
-}
To try to uncover the problem, I attempted a single step at a time. The
first reduction step is fine.
{-
_ : normalise 1 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (Ο-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
_ = refl
-}
The second reduction step yields a huge term. It contains the free
variable _x_1862 where I would have expected a fresh variable name to be
computed. Looking at the four-step reduction above we see the name computed
properly, but when going from the first step to the second it is not. The
huge size of the type derivation suggests why it did not terminate after
one day.
Help! Why doesn’t the term reduce? Is there some way to force it to reduce?
Cheers, -- P
{-
_ : normalise 1
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
≡
out-of-gas
((`λ _x_1862 ⇒
(`λ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ⇒
`if0 ` _x_1862 then
` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` _x_1862)
· ` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟚ Ο-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
`if0
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
then
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
else
(`Y
(`λ
suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
(`λ
suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⇒
(`λ
suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⇒
`if0
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
then
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
else
`
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
·
(`pred
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
·
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬?
(_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))))))
·
(`pred
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
·
(((λ w →
((λ x → ` x) , _x_1862 ↩ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↩
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢if0
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈) CollectionDec.here
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(S (fresh-lemma CollectionDec.here) Z)
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there CollectionDec.here)
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
Z
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(⊢subst
(λ {w} w∈′ {z₁} →
.Typed.Σ′
(λ {w₁} w∈ {z₂} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w₁ ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016) w∈′
| w ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(λ {z₁} x →
CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there (CollectionDec.there x))
| z₁ ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
_2016))
· ⊢suc (⊢suc ⊢zero))
-}
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Ulf Norell]

Ulf,
Any further progress with this?
Wen downloaded HEAD, but cannot execute even four steps of reduction on
his 2010 MacBook Pro.
I have not downloaded HEAD (I'm cautious about Agda updates because if I
break Agda I'm on my own trying to fix it). With the version below, four
steps of reduction takes five minutes, and full reduction does not complete
overnight.
I'm wondering if perhaps the issue is not version of Agda but available
memory? How much is on your machine?
Any other progress at tracking down what the issue might be?

I'm all but certain that the issue that makes it slow on 2.5.3 is
call-by-name. Development Agda has call-by-need.
I've tracked down the mysterious issue that made some cases check fast and
others not. The problem was that
we accidentally reverted back to call-by-name evaluation in some
situations. I have a patch that just needs some
testing before deployment.

It's not a memory issue. Type checking the file that executes all the way
to normal form requires less than 400M.
My suspicion is that there's a path issue or similar making Wen still run
an old Agda. It would be helpful to see the
result of running

agda --version
agda Test.agda +RTS -s

on this Test.agda:

module Test where

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import TypedFresh

isNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Bool
isNormal (out-of-gas _ _) = false
isNormal (normal _ _ _) = true

proof : isNormal (normalise 15 ⊢four) ≡ true
proof = refl

For reference, if I have up-to-date interface files for the imported
modules, this takes 3s and <400M memory
on my machine with Agda version 2.6.0-20c3e9d.

/ Ulf

[Philip Wadler]

Yay! I downloaded an up-to-date Agda (version 2.6.0-2f2f4f5) and it works
now! A big thank you to Ulf and Wen for their help. -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell

Ulf,
Any further progress with this?
Wen downloaded HEAD, but cannot execute even four steps of reduction on
his 2010 MacBook Pro.
I have not downloaded HEAD (I'm cautious about Agda updates because if I
break Agda I'm on my own trying to fix it). With the version below, four
steps of reduction takes five minutes, and full reduction does not complete
overnight.
I'm wondering if perhaps the issue is not version of Agda but available
memory? How much is on your machine?
Any other progress at tracking down what the issue might be?

I'm all but certain that the issue that makes it slow on 2.5.3 is
call-by-name. Development Agda has call-by-need.
I've tracked down the mysterious issue that made some cases check fast and
others not. The problem was that
we accidentally reverted back to call-by-name evaluation in some
situations. I have a patch that just needs some
testing before deployment.
It's not a memory issue. Type checking the file that executes all the way
to normal form requires less than 400M.
My suspicion is that there's a path issue or similar making Wen still run
an old Agda. It would be helpful to see the
result of running
agda --version
agda Test.agda +RTS -s
module Test where
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import TypedFresh
isNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Bool
isNormal (out-of-gas _ _) = false
isNormal (normal _ _ _) = true
proof : isNormal (normalise 15 ⊢four) ≡ true
proof = refl
For reference, if I have up-to-date interface files for the imported
modules, this takes 3s and <400M memory
on my machine with Agda version 2.6.0-20c3e9d.
/ Ulf

[Philip Wadler]

Ulf, Thanks again for your help. It is a great relief to be able to execute
my proven-correct code!

But there seems to be a further issue. Executing `normalise 100 ⊢four`
terminates quickly. However, if I paste the result into the file and ask
Agda to check that `normalise 100 ⊢four` is equal to the result of its own
execution then type checking still takes forever to terminate (where
"forever" means "longer than five minutes"). I expect this corresponds to
some spot where call-by-name is still used instead of call-by-need.
Fortunately, it is not on my critical path, but I thought I should alert
you to the issue.

I've attached the code, or you can find it at
https://github.com/wenkokke/sf/src/.

Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Philip Wadler
Yay! I downloaded an up-to-date Agda (version 2.6.0-2f2f4f5) and it works
now! A big thank you to Ulf and Wen for their help. -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell

Ulf,
Any further progress with this?
Wen downloaded HEAD, but cannot execute even four steps of reduction on
his 2010 MacBook Pro.
I have not downloaded HEAD (I'm cautious about Agda updates because if I
break Agda I'm on my own trying to fix it). With the version below, four
steps of reduction takes five minutes, and full reduction does not complete
overnight.
I'm wondering if perhaps the issue is not version of Agda but available
memory? How much is on your machine?
Any other progress at tracking down what the issue might be?

I'm all but certain that the issue that makes it slow on 2.5.3 is
call-by-name. Development Agda has call-by-need.
I've tracked down the mysterious issue that made some cases check fast
and others not. The problem was that
we accidentally reverted back to call-by-name evaluation in some
situations. I have a patch that just needs some
testing before deployment.
It's not a memory issue. Type checking the file that executes all the way
to normal form requires less than 400M.
My suspicion is that there's a path issue or similar making Wen still run
an old Agda. It would be helpful to see the
result of running
agda --version
agda Test.agda +RTS -s
module Test where
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import TypedFresh
isNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Bool
isNormal (out-of-gas _ _) = false
isNormal (normal _ _ _) = true
proof : isNormal (normalise 15 ⊢four) ≡ true
proof = refl
For reference, if I have up-to-date interface files for the imported
modules, this takes 3s and <400M memory
on my machine with Agda version 2.6.0-20c3e9d.
/ Ulf

[Ulf Norell]

I believe the problem you've run into is that we don't have explicit
sharing in the
internal terms. The normal form of `normalise 100 ⊢four` is small, but the
weak-head
normal form is huge, and the type checker compares terms for equality by
successive
weak-head reduction steps. The lack of explicit sharing means that
evaluation won't be
shared across reduction steps.

Here are some numbers:

n size of whnf of `normalise n ⊢four` (#nodes in syntax tree)
1 916
2 122,597
3 53,848,821
4 ??
100 ????

/ Ulf

Post by Philip Wadler
Ulf, Thanks again for your help. It is a great relief to be able to
execute my proven-correct code!
But there seems to be a further issue. Executing `normalise 100 ⊢four`
terminates quickly. However, if I paste the result into the file and ask
Agda to check that `normalise 100 ⊢four` is equal to the result of its own
execution then type checking still takes forever to terminate (where
"forever" means "longer than five minutes"). I expect this corresponds to
some spot where call-by-name is still used instead of call-by-need.
Fortunately, it is not on my critical path, but I thought I should alert
you to the issue.
I've attached the code, or you can find it at https://github.com/
wenkokke/sf/src/.
Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Philip Wadler
Yay! I downloaded an up-to-date Agda (version 2.6.0-2f2f4f5) and it works
now! A big thank you to Ulf and Wen for their help. -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell

Ulf,
Any further progress with this?
Wen downloaded HEAD, but cannot execute even four steps of reduction on
his 2010 MacBook Pro.
I have not downloaded HEAD (I'm cautious about Agda updates because if
I break Agda I'm on my own trying to fix it). With the version below, four
steps of reduction takes five minutes, and full reduction does not complete
overnight.
I'm wondering if perhaps the issue is not version of Agda but available
memory? How much is on your machine?
Any other progress at tracking down what the issue might be?

I'm all but certain that the issue that makes it slow on 2.5.3 is
call-by-name. Development Agda has call-by-need.
I've tracked down the mysterious issue that made some cases check fast
and others not. The problem was that
we accidentally reverted back to call-by-name evaluation in some
situations. I have a patch that just needs some
testing before deployment.
It's not a memory issue. Type checking the file that executes all the
way to normal form requires less than 400M.
My suspicion is that there's a path issue or similar making Wen still
run an old Agda. It would be helpful to see the
result of running
agda --version
agda Test.agda +RTS -s
module Test where
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import TypedFresh
isNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Bool
isNormal (out-of-gas _ _) = false
isNormal (normal _ _ _) = true
proof : isNormal (normalise 15 ⊢four) ≡ true
proof = refl
For reference, if I have up-to-date interface files for the imported
modules, this takes 3s and <400M memory
on my machine with Agda version 2.6.0-20c3e9d.
/ Ulf

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Philip Wadler]

Thanks! If I write this up, I will use those numbers. Take this as an
indication that revising the system to exploit sharing would be valuable.
Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell
I believe the problem you've run into is that we don't have explicit
sharing in the
internal terms. The normal form of `normalise 100 ⊢four` is small, but the
weak-head
normal form is huge, and the type checker compares terms for equality by
successive
weak-head reduction steps. The lack of explicit sharing means that
evaluation won't be
shared across reduction steps.
n size of whnf of `normalise n ⊢four` (#nodes in syntax tree)
1 916
2 122,597
3 53,848,821
4 ??
100 ????
/ Ulf

Post by Philip Wadler
Ulf, Thanks again for your help. It is a great relief to be able to
execute my proven-correct code!
But there seems to be a further issue. Executing `normalise 100 ⊢four`
terminates quickly. However, if I paste the result into the file and ask
Agda to check that `normalise 100 ⊢four` is equal to the result of its own
execution then type checking still takes forever to terminate (where
"forever" means "longer than five minutes"). I expect this corresponds to
some spot where call-by-name is still used instead of call-by-need.
Fortunately, it is not on my critical path, but I thought I should alert
you to the issue.
I've attached the code, or you can find it at https://github.com/wenkokke
/sf/src/.
Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Philip Wadler
Yay! I downloaded an up-to-date Agda (version 2.6.0-2f2f4f5) and it
works now! A big thank you to Ulf and Wen for their help. -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell

Ulf,
Any further progress with this?
Wen downloaded HEAD, but cannot execute even four steps of reduction
on his 2010 MacBook Pro.
I have not downloaded HEAD (I'm cautious about Agda updates because if
I break Agda I'm on my own trying to fix it). With the version below, four
steps of reduction takes five minutes, and full reduction does not complete
overnight.
I'm wondering if perhaps the issue is not version of Agda but
available memory? How much is on your machine?
Any other progress at tracking down what the issue might be?

I'm all but certain that the issue that makes it slow on 2.5.3 is
call-by-name. Development Agda has call-by-need.
I've tracked down the mysterious issue that made some cases check fast
and others not. The problem was that
we accidentally reverted back to call-by-name evaluation in some
situations. I have a patch that just needs some
testing before deployment.
It's not a memory issue. Type checking the file that executes all the
way to normal form requires less than 400M.
My suspicion is that there's a path issue or similar making Wen still
run an old Agda. It would be helpful to see the
result of running
agda --version
agda Test.agda +RTS -s
module Test where
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import TypedFresh
isNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Bool
isNormal (out-of-gas _ _) = false
isNormal (normal _ _ _) = true
proof : isNormal (normalise 15 ⊢four) ≡ true
proof = refl
For reference, if I have up-to-date interface files for the imported
modules, this takes 3s and <400M memory
on my machine with Agda version 2.6.0-20c3e9d.
/ Ulf

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Philip Wadler]

Thanks, Ulf. Wen, can you please reply? Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Post by Ulf Norell

Ulf,
Any further progress with this?
Wen downloaded HEAD, but cannot execute even four steps of reduction on
his 2010 MacBook Pro.
I have not downloaded HEAD (I'm cautious about Agda updates because if I
break Agda I'm on my own trying to fix it). With the version below, four
steps of reduction takes five minutes, and full reduction does not complete
overnight.
I'm wondering if perhaps the issue is not version of Agda but available
memory? How much is on your machine?
Any other progress at tracking down what the issue might be?

I'm all but certain that the issue that makes it slow on 2.5.3 is
call-by-name. Development Agda has call-by-need.
I've tracked down the mysterious issue that made some cases check fast and
others not. The problem was that
we accidentally reverted back to call-by-name evaluation in some
situations. I have a patch that just needs some
testing before deployment.
It's not a memory issue. Type checking the file that executes all the way
to normal form requires less than 400M.
My suspicion is that there's a path issue or similar making Wen still run
an old Agda. It would be helpful to see the
result of running
agda --version
agda Test.agda +RTS -s
module Test where
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import TypedFresh
isNormal : ∀ {M A} {⊢M : ε ⊢ M ⩂ A} → Normalise ⊢M → Bool
isNormal (out-of-gas _ _) = false
isNormal (normal _ _ _) = true
proof : isNormal (normalise 15 ⊢four) ≡ true
proof = refl
For reference, if I have up-to-date interface files for the imported
modules, this takes 3s and <400M memory
on my machine with Agda version 2.6.0-20c3e9d.
/ Ulf