[Agda] Building Coinductive Trees, Agsy Internal Error

[Brandon Moore]

Thanks Andreas.

Yours suggestion of switching to an inductive version of the predicate
simplifies some of the proof. I've got everything to go through now,
including a soundness proof that prefixes of an infinite tree
unrolled from the function making partial trees are equal to
the partial trees produced by that tree builder.

I suspect parts of the code can still be greatly improved.
Also, I ran into an error in proof automation along the way.
I haven't tried to minimize the example, but instructions
for reproducing it are at the bottom of this file. Are there
known problems with suggesting hints whose bodies are
left as holes?


The preliminaries of the code are the same as before,
until the consistency predicate on tree builders.

\begin{code}
module CTest where
open import Data.Nat
open import Coinduction
open import Relation.Binary.PropositionalEquality
open import Data.Product

data P : ℕ → Set where
  Truncated : P 0
  Con1 : (n : ℕ) → P n → P (suc n)
  Con2 : (n : ℕ) → P n → P n → P (suc n)

data C : Set where
  Con1 : ∞ C → C
  Con2 : ∞ C → ∞ C → C

builder = (n : ℕ) → P n
\end{code}

The truncation operation is replaced by an inductive
subtree predicate. It seems the left-biased
definition of + computes nicely here.

\begin{code}
data SubTree {m : ℕ} :
  ∀ {n} → P n → P (n + m) → Set
 where
  subTrunc : ∀ (v : P m) → SubTree Truncated v
  subCon1 : ∀ {n} (v : P n) (l : P (n + m))
    → SubTree v l → SubTree (Con1 _ v) (Con1 _ l)
  subCon2 : ∀ {n} (vl vr : P n) (l r : P (n + m))
    → SubTree vl l → SubTree vr r → SubTree (Con2 _ vl vr) (Con2 _ l r)

wfInd : builder → Set
wfInd b = (n m : ℕ) → SubTree (b n) (b (n + m))
\end{code}

Now it's much easier to show a relationship between
corresponding children of related trees, and a little
easier to refute impossible cases. Also, I don't have
to prove lemmas that non-empty subtrees of a tree have
the same root constructor as the original tree.

It's still a bit messier than I'd like, but enough
simpler that I've finished all the cases.

\begin{code}
b1 : (b : builder) → wfInd b → b 1 ≡ Con1 _ Truncated → builder
b1 b wf eq n with b 1 | b (suc n) | wf 1 n
b1 b wf refl n | .(Con1 _ _) | Con1 .n y | wfn = y
b1 b wf refl n | .(Con1 _ _) | Con2 .n _ _  | ()

b1Wf : (b : builder) (wf : wfInd b) (eq : b 1 ≡ Con1 _ Truncated) → wfInd (b1 b wf eq)
b1Wf b wf eq n m  with b 1 | b (suc n) | wf 1 n | b (suc (n + m)) | wf 1 (n + m) | wf (suc n) m
b1Wf b wf refl n m | .(Con1 _ _) | Con1 .n y | _ | Con1 .(n + m) y' | _ | subCon1 .y .y' y0 = y0
b1Wf b wf refl n m | .(Con1 _ _) | Con1 .n _ | _ | Con2 .(n + m) _ _ | () | _
b1Wf b wf refl n m | .(Con1 _ _) | Con2 .n _ _ | () | _ | _ | _

b2l : (b : builder) → wfInd b → b 1 ≡ Con2 _ Truncated Truncated → builder
b2l b wf eq n with b 1 | b (suc n) | wf 1 n
b2l b wf refl n | .(Con2 _ _ _) | Con2 .n y _ | wfn = y
b2l b wf refl n | .(Con2 _ _ _) | Con1 .n _ | ()

b2lWf : (b : builder) (wf : wfInd b) (eq : b 1 ≡ Con2 _ Truncated Truncated) → wfInd (b2l b wf eq)
b2lWf b wf eq n m  with b 1 | b (suc n) | wf 1 n | b (suc (n + m)) | wf 1 (n + m) | wf (suc n) m
b2lWf b wf refl n m | .(Con2 _ _ _) | Con2 .n y y1 | _ | Con2 .(n + m) y' y1' | _ | subCon2 .y .y1 .y' .y1' y0 _ = y0
b2lWf b wf refl n m | .(Con2 _ _ _) | Con2 .n _ _ | _ | Con1 .(n + m) _ | () | _
b2lWf b wf refl n m | .(Con2 _ _ _) | Con1 .n _ | () | _ | _ | _

b2r : (b : builder) → wfInd b → b 1 ≡ Con2 _ Truncated Truncated → builder
b2r b wf eq n with b 1 | b (suc n) | wf 1 n
b2r b wf refl n | .(Con2 _ _ _) | Con2 .n _ y | wfn = y
b2r b wf refl n | .(Con2 _ _ _) | Con1 .n _ | ()

b2rWf : (b : builder) (wf : wfInd b) (eq : b 1 ≡ Con2 _ Truncated Truncated) → wfInd (b2r b wf eq)
b2rWf b wf eq n m  with b 1 | b (suc n) | wf 1 n | b (suc (n + m)) | wf 1 (n + m) | wf (suc n) m
b2rWf b wf refl n m | .(Con2 _ _ _) | Con2 .n y y1 | _ | Con2 .(n + m) y' y1' | _ | subCon2 .y .y1 .y' .y1' _ y0 = y0
b2rWf b wf refl n m | .(Con2 _ _ _) | Con2 .n _ _ | _ | Con1 .(n + m) _ | () | _
b2rWf b wf refl n m | .(Con2 _ _ _) | Con1 .n _ | () | _ | _ | _
\end{code}

Now, as before, these can be used to unroll an infinite tree.

\begin{code}
unroll : ∃ wfInd → C
unroll (b , wf) with inspect (b 1)
unroll (b , wf) | Con1 .0 Truncated with-≡ eq
  = Con1 (♯ unroll (b1 b wf eq , b1Wf b wf eq))
unroll (b , wf) | Con2 .0 Truncated Truncated with-≡ eq
  = Con2 (♯ unroll (b2l b wf eq , b2lWf b wf eq)) (♯ unroll (b2r b wf eq , b2rWf b wf eq))
\end{code}

I should prove soundness. This seems to need some lemmas about the decomposition above.

\begin{code}
truncate : (n : ℕ) → C → P n
truncate 0 _ = Truncated
truncate (suc n) (Con1 y) = Con1 n (truncate n (♭ y))
truncate (suc n) (Con2 y y') = Con2 n (truncate n (♭ y)) (truncate n (♭ y'))

break1 : (b : builder) (wf : wfInd b) (eq : b 1 ≡ Con1 0 Truncated) → (n : ℕ) → b (suc n) ≡ Con1 n (b1 b wf eq n)
-- break1 = ?
break1 b wf eq n with b 1 | b (suc n) | wf 1 n
break1 b wf refl n | .(_) | Con1 .n y | _ = refl
break1 b wf refl n | .(_) | Con2 .n _ _ | ()

break2 : (b : builder) (wf : wfInd b) (eq : b 1 ≡ Con2 0 Truncated Truncated) → (n : ℕ) → b (suc n) ≡ Con2 n (b2l b wf eq n) (b2r b wf eq n)
-- break2 = ?
break2 b wf eq n with b 1 | b (suc n) | wf 1 n
break2 b wf refl n | .(_) | Con2 .n y y' | _ = refl
break2 b wf refl n | .(_) | Con1 .n _ | ()

unroll-sound : (b : builder) → (wf : wfInd b) → (n : ℕ) → b n ≡ truncate n (unroll (b , wf))
unroll-sound b wf zero with b 0; ... | Truncated = refl
unroll-sound b wf (suc n) with inspect (b 1)
unroll-sound b wf (suc n) | Con1 .0 Truncated with-≡ eq
  with unroll-sound (b1 b wf eq) (b1Wf b wf eq) n
... | us rewrite sym us = break1 b wf eq n
unroll-sound b wf (suc n) | Con2 .0 Truncated Truncated with-≡ eq
  with unroll-sound (b2l b wf eq) (b2lWf b wf eq) n | unroll-sound (b2r b wf eq) (b2rWf b wf eq) n
... | us1 | us2 rewrite sym us1 | sym us2 = break2 b wf eq n
-- unroll-sound b wf (suc n) | Con2 .0 Truncated Truncated with-≡ eq | us1 | us2 rewrite sym us1 | sym us2 = {!break2!}
\end{code}

There is an internal error in proof automation if you replace the
last line of unroll-sound with the commented version, replace the
definitions of break1 and break2 with a hole as in the commented
lines, and then try to find automatically a solution in the last
hole (with break2 provided as a hint).

Here's the error:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Auto/Convert.hs:444