Eliminating erased argument with only one valid case

Question

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)

Answer 1

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)