[Agda] How does one debug a programme that one has proved correct?
Ulf Norell
ulf.norell at gmail.com
Fri May 4 21:30:24 CEST 2018
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
On Fri, May 4, 2018 at 7:44 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> 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/
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180504/a77ba257/attachment.html>
More information about the Agda
mailing list