```------------------------------------------------------------------------
-- The Agda standard library
--
-- 'Sufficient' lists: a structurally inductive view of lists xs
-- as given by xs ≡ non-empty prefix + sufficient suffix
--
-- Useful for termination arguments for function definitions
-- which provably consume a non-empty (but otherwise arbitrary) prefix
-- *without* having to resort to ancillary WF induction on length etc.
-- e.g. lexers, parsers etc.
--
-- Credited by Conor McBride as originally due to James McKinna
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Relation.Unary.Sufficient where

open import Level using (Level; _⊔_)
open import Data.List.Base using (List; []; _∷_; [_]; _++_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

private
variable

a b : Level
A : Set a
x : A
xs : List A

------------------------------------------------------------------------
-- Sufficient builder

suffAcc : {A : Set a} (B :  List A → Set b) (xs : List A) → Set (a ⊔ b)
suffAcc B xs = ∀ {x} {prefix} suffix → xs ≡ x ∷ prefix ++ suffix → B suffix

------------------------------------------------------------------------
-- Sufficient view

data Sufficient {A : Set a} : (xs : List A) → Set a where

acc : ∀ {xs} (ih : suffAcc Sufficient xs) → Sufficient xs

------------------------------------------------------------------------
-- Sufficient properties

-- constructors

module Constructors where

[]⁺ : Sufficient {A = A} []
[]⁺ = acc λ _ ()

∷⁺ : Sufficient xs → Sufficient (x ∷ xs)
∷⁺ {xs = xs} suffices@(acc hyp) = acc λ { _ refl → suf _ refl }
where
suf : ∀ prefix {suffix} → xs ≡ prefix ++ suffix → Sufficient suffix
suf []               refl = suffices
suf (_ ∷ _) {suffix} eq   = hyp suffix eq

-- destructors

module Destructors where

acc-inverse : ∀ ys → Sufficient (x ∷ xs ++ ys) → Sufficient ys
acc-inverse ys (acc hyp) = hyp ys refl

++⁻ : ∀ xs {ys : List A} → Sufficient (xs ++ ys) → Sufficient ys
++⁻ []            suffices = suffices
++⁻ (x ∷ xs) {ys} suffices = acc-inverse ys suffices

∷⁻ : Sufficient (x ∷ xs) → Sufficient xs
∷⁻ {x = x} = ++⁻ [ x ]

------------------------------------------------------------------------
-- Sufficient view covering property

module View where

open Constructors

sufficient : (xs : List A) → Sufficient xs
sufficient []       = []⁺
sufficient (x ∷ xs) = ∷⁺ (sufficient xs)

------------------------------------------------------------------------
-- Recursion on the sufficient view

module _ (B : List A → Set b) (rec : ∀ ys → (ih : suffAcc B ys) → B ys)
where

open View

suffRec′ : ∀ {zs} → Sufficient zs → B zs
suffRec′ {zs} (acc hyp) = rec zs (λ xs eq → suffRec′ (hyp xs eq))

suffRec : ∀ zs → B zs
suffRec zs = suffRec′ (sufficient zs)
```