------------------------------------------------------------------------
-- 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)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4