open import 1Lab.Reflection
open import 1Lab.Prelude hiding (absurd)

open import Data.List.Membership
open import Data.List.Base

open import Meta.Foldable
module 1Lab.Reflection.List where

Reflection utilities for listsπŸ”—

The following patterns are useful.

pattern `List `A = def (quote List) (unknown h∷ `A v∷ [])

pattern _`∷_ `x `xs = con (quote List._∷_) (unknown h∷ unknown h∷ `x v∷ `xs v∷ [])
pattern `[] = con (quote List.[]) (unknown h∷ unknown h∷ [])

pattern _`∷?_ `x `xs = con (quote List._∷_) (`x v∷ `xs v∷ [])
pattern `[]? = con (quote List.[]) []

We can quote lists of terms to get a quoted list, and we can unquote terms to lists of terms, so long as the spine of the list can be fully reduced.

quoteList : List Term β†’ Term
quoteList = foldr _`∷_ `[]

{-# TERMINATING #-}
unquoteList : Term β†’ TC (List Term)
unquoteList `xs =
  reduce `xs >>= Ξ» where
    `[] β†’ pure []
    (`x `∷ `xs) β†’ `x ∷_ <$> unquoteList `xs
    (meta m _) β†’ block-on-meta m
    `xs β†’ typeError [ "unquoteList: can't unquote " , termErr `xs , " because it cannot be reduced to whnf." ]

We also provide patterns for list membership.

pattern _`βˆˆβ‚—_ `x `xs = def (quote _βˆˆβ‚—_) (unknown h∷ unknown h∷ `x v∷ `xs v∷ [])

pattern `here `p = con (quote _βˆˆβ‚—_.here) (unknown h∷ unknown h∷ unknown h∷ unknown h∷ `p v∷ [])
pattern `there `mem = con (quote _βˆˆβ‚—_.there) (unknown h∷ unknown h∷ unknown h∷ unknown h∷ `mem v∷ [])

pattern `here? `p = con (quote _βˆˆβ‚—_.here) (`p v∷ [])
pattern `there? `mem = con (quote _βˆˆβ‚—_.there) (`mem v∷ [])

Proof automation for unique membershipπŸ”—

Writing proofs that is-contr (x βˆˆβ‚— xs) is a common but tedious task, so we provide some macros for constructing them.

Our first helper function walks down a list, searching for an element while accumulating a term for the proof that the element is in the list, as well as patterns for matching that element and an absurd pattern.

private
  find-member-with
    : (`x : Term) (`xs : Term) (spine : List Term)
    β†’ Term β†’ Pattern β†’ Pattern
    β†’ TC (Term Γ— Pattern Γ— Pattern Γ— List Term)
  find-member-with `x `xs [] `mem `found `not-found =
    typeError [ "has-member: could not find " , termErr `x , " in " , termErr `xs ]
  find-member-with `x `xs (`y ∷ spine) `mem `found `not-found =
    unifies? `x `y >>= Ξ» where
      true β†’ pure (`mem , `found , `not-found , spine)
      false β†’
        find-member-with `x `xs spine (`there `mem) (`there? `found) (`there? `not-found)

Our second helper also iterates through the list, but instead constructs absurd clauses for each element.

private
  refute-member-with
    : (`x : Term) (`xs : Term) (spine : List Term)
    β†’ Pattern β†’ List Clause
    β†’ List Clause
  refute-member-with `x `xs [] `not-found clauses = clauses
  refute-member-with `x `xs (`y ∷ spine) `not-found clauses =
    let `not-found-clause = absurd-clause (("_" , argN (`x `βˆˆβ‚— `xs)) ∷ []) (`not-found v∷ [])
    in refute-member-with `x `xs spine (`there? `not-found) (`not-found-clause ∷ clauses)

Our macro then calls these two helpers in sequence, and packages the results into a contr.

  unique-member-worker
    : βˆ€ {β„“} {A : Type β„“}
    β†’ (x : A) (xs : List A)
    β†’ Term
    β†’ TC ⊀
  unique-member-worker x xs hole = do
    `x ← quoteTC x
    spine ← traverse quoteTC xs
    let `xs = quoteList spine
    (`mem , `found , `not-found , rest) ←
          find-member-with `x `xs spine
            (`here (con (quote reflα΅’) []))
            (`here? (con (quote reflα΅’) []))
            (`here? (absurd 0))
    let clauses =
          refute-member-with `x `xs rest
            (`there? `not-found)
            (clause [] (`found v∷ []) (def (quote refl) []) ∷ [])
    unify hole (con (quote contr) (`mem v∷ pat-lam clauses [] v∷ []))

unique-member!
  : βˆ€ {β„“} {A : Type β„“}
  β†’ {x : A} {xs : List A}
  β†’ {@(tactic unique-member-worker x xs) mem : is-contr (x βˆˆβ‚— xs)}
  β†’ is-contr (x βˆˆβ‚— xs)
unique-member! {mem = mem} = mem

We also get a macros for proving that an element is either in or not in a list en-passant.

private
  member-worker
    : βˆ€ {β„“} {A : Type β„“}
    β†’ (x : A) (xs : List A)
    β†’ Term
    β†’ TC ⊀
  member-worker x xs hole = do
    `x ← quoteTC x
    spine ← traverse quoteTC xs
    let `xs = quoteList spine
    (`mem , _ , _ , _) ←
          find-member-with `x `xs spine
            (`here (con (quote reflα΅’) []))
            (`here? (con (quote reflα΅’) []))
            (`here? (absurd 0))
    unify hole `mem

  not-member-worker
    : βˆ€ {β„“} {A : Type β„“}
    β†’ (x : A) (xs : List A)
    β†’ Term
    β†’ TC ⊀
  not-member-worker x xs hole = do
    `x ← quoteTC x
    `xs ← traverse quoteTC xs
    let clauses = refute-member-with `x (quoteList `xs) `xs (`here? (absurd 0)) []
    unify hole (pat-lam clauses [])

member!
  : βˆ€ {β„“} {A : Type β„“}
  β†’ {x : A} {xs : List A}
  β†’ {@(tactic member-worker x xs) mem : x ∈ xs}
  β†’ x ∈ xs
member! {mem = mem} = mem

not-member!
  : βˆ€ {β„“} {A : Type β„“}
  β†’ {x : A} {xs : List A}
  β†’ {@(tactic not-member-worker x xs) not-mem : x βˆ‰ xs}
  β†’ x βˆ‰ xs
not-member! {not-mem = not-mem} = not-mem

ExamplesπŸ”—

private
  member-example : true ∈ [ false , true , false , true , false ]
  member-example = member!

  not-member-example : true βˆ‰ [ false , false , false ]
  not-member-example = not-member!

  unique-member-example : is-contr (true ∈ [ false , true , false , false ])
  unique-member-example = unique-member!