How to prove basic properties of `scanr` in Agda involving branch reasoning?

Question

I’m working on a proof involving the scanr function in Agda and have encountered difficulties with branch reasoning. The proof seems straightforward, but implementing it is proving to be tricky. Here’s the code I’m working with:

open import Data.List using (List; []; _∷_; [_]; _++_; foldl; foldr; map; scanl; scanr)
open import Data.Bool using (Bool; true; false)
-contra : false ≡ true → ∀{ℓ} {P : Set ℓ} → P
-contra ()

is-empty : ∀{A : Set} → (xs : List A) → Bool
is-empty [] = true
is-empty (x ∷ xs) = false

scanr-not-empty : {A B : Set} (f : A → B → B) (e : B) (xs : List A) → is-empty (scanr f e xs) ≡ false
scanr-not-empty f e [] = refl
scanr-not-empty f e (x ∷ xs) with scanr f e xs in p'
... | []     = -contra (trans (sym (scanr-not-empty f e xs)) (cong is-empty p'))
... | y ∷ ys = refl

listFir : {A : Set} (xs : List A) → is-empty xs ≡ false → A
listFir (x ∷ xs) p = x
scanFir : {A B : Set} (f : A → B → B) (e : B) (xs : List A) → B 
scanFir f e xs = listFir (scanr f e xs) (scanr-not-empty f e xs)

scanFi : {A B : Set} (f : A → B → B) (e : B) (x : A) (xs : List A) → 
  scanFir f e (x ∷ xs) ≡ f x (scanFir f e xs)
scanFi f e x xs = {!!}

And the standard library definition of scanr might be useful here:

scanr : (A → B → B) → B → List A → List B
scanr f e []       = e ∷ []
scanr f e (x ∷ xs) with scanr f e xs
... | []     = []                -- dead branch
... | y ∷ ys = f x y ∷ y ∷ ys

Could someone provide guidance on how to approach this proof, particularly how to handle the branches in the reasoning? I’m new to this, so thanks in advance for any pointers!

Answer 1

Quite an annoying problem indeed. Here's how to make it work:

scanFi : {A B : Set} (f : A → B → B) (e : B) (x : A) (xs : List A) →
  scanFir f e (x ∷ xs) ≡ f x (scanFir f e xs)
scanFi f e x xs with scanr f e xs | scanr-not-empty f e xs | scanr-not-empty f e (x ∷ xs)
... | []     | () | ()
... | y ∷ ys | _  | _  = refl

Basically scanr f e xs appears in both scanr-not-empty f e xs and scanr-not-empty f e (x ∷ xs) and so you have to add those to the with-expression in order for scanr f e xs to be rewritten in their types consistently with the rest of the expression. If these two aren't added to the with-expression, then a fresh variable w is substituted for scanr f e xs in only half the places and you get a type error.

You can learn more about this wrinkle here.

Answer 2

It's even a 'wrinkle'-y definition in the first place, partly because of the dead-code branch (dependent types are supposed to help us avoid such things), and partly because, as the answer already given shows, proving properties of functions defined using with requires ... more with, and that's not necessarily always easy to get your head round.

Consider, for example, what it might be to rewrite the definition of scanr to use Data.List.NonEmpty, to guarantee that the result is... non-empty. Not a 'magic' fix, and changing the interface to a function is not always available to us, but here it might shed light on the problem, as an 'experimental'/exploratory approach...

There are other ways to deal with the problem: basically by defining the 'graph view of a function' (illustrated here, but not in the standard library), but that (perhaps) involves paging in more stuff, esp. about view-based programming as a 'style', than ... is necessarily always easy to get your head round.

A further alternative, using an 'irrelevant instance' version (this is a 'more modern' approach to using boolean pre-/post-conditions on functions) of the Bool-valued is-empty predicate defined in the OP (itself implementable as not ∘ null), may be seen in this PR on the Agda stdlib. This solution exhibits much in common with @effectfully's approach, but streamlines that solution to support an irrefutable (one match only) with analysis of scanr...