[Agda] How does one debug a programme that one has proved correct?
Philip Wadler
wadler at inf.ed.ac.uk
Fri May 4 22:03:47 CEST 2018
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/
On 4 May 2018 at 16:30, Ulf Norell <ulf.norell at gmail.com> wrote:
> 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/35239f79/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180504/35239f79/attachment.ksh>
More information about the Agda
mailing list