I have defined infinite streams as follows:
record Stream (A : Set) : Set where
coinductive
field head : A
field tail : Stream A
and an inductive type which shows that some element in a stream eventually satisfies a predicate:
data Eventually {A} (P : A -> Set) (xs : Stream A) : Set where
here : P (head xs) -> Eventually P xs
there : Eventually P (tail xs) -> Eventually P xs
I would like to write a function which skips over elements of the stream until the head of the stream satisfies a predicate. To ensure termination, we must know that an element eventually satisfies the predicate, else we could loop forever. Hence, the definition of Eventually must be passed as an argument. Furthermore, the function should not computationally depend on the Eventually predicate, as it is just there to prove termination, so I would like it to be an erased argument.
dropUntil : {A : Set} {P : A -> Set} (decide : ∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually P xs → Stream A
dropUntil decide xs ev with decide (head xs)
... | yes prf = xs
... | no contra = dropUntil decide (tail xs) ?
Here is the problem - I would like to fill in the hole in the definition. From contra in scope, we know that the head of the stream does not satisfy P, and hence by definition of eventually, some element in the tail of the stream must satisfy P. If Eventually wasn't erased in this context, we could simply pattern match on the predicate, and prove the here case impossible. Normally in these scenarios I would write an erased auxiliary function, on the lines of:
@0 eventuallyInv : ∀ {A} {P : A → Set} {xs : Stream A} → Eventually P xs → ¬ P (head xs) → Eventually P (tail xs)
eventuallyInv (here x) contra with contra x
... | ()
eventuallyInv (there ev) contra = ev
The problem with this approach is that the Eventually proof is the structurally recursive argument in dropUntil, and calling this auxiliary function does not pass the termination checker as Agda does not "look inside" the function definition.
Another approach I tried is inlining the above erased function into the definition of dropUntil. Unfortunately, I had no luck with this approach either - using the definition of case ... of like described here https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html did not pass the termination checker either.
I have written an equivalent program in Coq which is accepted (using Prop rather than erased types), so I am confident that my reasoning is correct. The main reason why Coq accepted the definition and Agda doesn't is that Coq's termination checker expands function definitions, and hence the "auxiliary erased function" approach succeeds.
EDIT:
This is my attempt using sized types, however it does not pass the termination checker and I can't figure out why.
record Stream (A : Set) : Set where
coinductive
field
head : A
tail : Stream A
open Stream
data Eventually {A} (P : A → Set) (xs : Stream A) : Size → Set where
here : ∀ {i} → P (head xs) → Eventually P xs (↑ i)
there : ∀ {i} → Eventually P (tail xs) i → Eventually P xs (↑ i)
@0 eventuallyInv : ∀ {A P i} {xs : Stream A} → Eventually P xs (↑ i) → ¬ P (head xs) → Eventually P (tail xs) i
eventuallyInv (here p) ¬p with ¬p p
... | ()
eventuallyInv (there ev) ¬p = ev
dropUntil : ∀ {A P i} → (∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually P xs (↑ i) → Stream A
dropUntil decide xs ev with decide (head xs)
... | yes p = xs
... | no ¬p = dropUntil decide (tail xs) (eventuallyInv ev ¬p)
In your case you can work with a weaker notion of Eventually which matches what dropUntil actually needs to know. It's also single constructor so you can match on it even when erased.
data Eventually' {A} (P : A -> Set) (xs : Stream A) : Set where
next : (¬ P (head xs) → Eventually' P (tail xs)) → Eventually' P xs
eventuallyInv : ∀ {A} {P : A → Set} {xs : Stream A} → (ev : Eventually P xs) → Eventually' P xs
eventuallyInv (here p) = next \ np → ⊥-elim (np p)
eventuallyInv (there ev) = next \ np → eventuallyInv ev
dropUntil' : {A : Set} {P : A -> Set} (decide : ∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually' P xs → Stream A
dropUntil' decide xs (next ev) with decide (head xs)
... | yes prf = xs
... | no contra = dropUntil' decide (tail xs) (ev contra)
dropUntil : {A : Set} {P : A -> Set} (decide : ∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually P xs → Stream A
dropUntil decide xs ev = dropUntil' decide xs (eventuallyInv ev)