Skip to content

[ refactor ] use variables more systematically in Data.List.Fresh{.*} #2916

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jamesmckinna wants to merge 14 commits into
base: master
Choose a base branch
from
Open

[ refactor ] use variables more systematically in Data.List.Fresh{.*} #2916

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
02dba80
refactor: use `variable`s more systematically
jamesmckinna Jan 23, 2026
67ef7e1
refactor: remove `P` from `variable` block
jamesmckinna Jan 27, 2026
6af45e4
refactor: `Properties` follow easily
jamesmckinna Jan 27, 2026
de98e4e
refactor: propagate the `variable` style throughout
jamesmckinna Jan 28, 2026
c20a2c3
Update src/Data/List/Fresh.agda
jamesmckinna Jan 28, 2026
2d081b6
Update src/Data/List/Fresh.agda
jamesmckinna Jan 28, 2026
09c8b5f
Update src/Data/List/Fresh.agda
jamesmckinna Jan 28, 2026
502c903
Update src/Data/List/Fresh.agda
jamesmckinna Jan 28, 2026
563ad4b
fix: module name
jamesmckinna Jan 28, 2026
0acb35e
fix: bug in `import`s
jamesmckinna Jan 28, 2026
cfc60a6
refactor: `Any.Properties`s
jamesmckinna Jan 28, 2026
d1d7a7c
fix: quantifier prefix
jamesmckinna Jan 28, 2026
ab384a4
final tweaks
jamesmckinna Jan 28, 2026
64250e8
Merge branch 'agda:master' into refactor-fresh
jamesmckinna Jan 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
128 changes: 66 additions & 62 deletions src/Data/List/Fresh.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,9 @@ open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Function.Base using (_∘′_; flip; id; _on_)
open import Relation.Nullary using (does)
open import Relation.Unary as U using (Pred)
open import Relation.Binary.Core using (Rel)
import Relation.Binary.Definitions as B using (Reflexive)
open import Relation.Unary as Unary using (Pred; Decidable)
open import Relation.Binary.Core using (Rel; REL)
open import Relation.Binary.Definitions as Binary using (Reflexive)
open import Relation.Nary using (_⇒_; ∀[_])


Expand All @@ -34,6 +34,10 @@ private
a b p r s : Level
A : Set a
B : Set b
R : Rel A r
S : Rel A s
x y : A


------------------------------------------------------------------------
-- Basic type
Expand All @@ -44,11 +48,11 @@ private
module _ {a} (A : Set a) (R : Rel A r) where

data List# : Set (a ⊔ r)
fresh : (a : A) (as : List#) → Set r
fresh : REL A List# r

data List# where
[] : List#
cons : (a : A) (as : List#) → fresh a as → List#
cons : (x : A) (xs : List#) → fresh x xs → List#

-- Whenever R can be reconstructed by η-expansion (e.g. because it is
-- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we
Expand All @@ -64,145 +68,145 @@ module _ {a} (A : Set a) (R : Rel A r) where

-- Convenient notation for freshness making A and R implicit parameters
infix 5 _#_
_#_ : {R : Rel A r} (a : A) (as : List# A R) → Set r
_#_ : REL A (List# A R) _
_#_ = fresh _ _
Comment on lines 69 to 72
Copy link
Collaborator Author

@jamesmckinna jamesmckinna Jan 28, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The whole intention behind this PR is to better support generalisation over R when using List#, and specifically the ability to generalise over arguments xs : List# A R correctly.

Unfortunately, this sometime means that some statements involving x # xs fail to generalise correctly wrt the implied/implicit argument R relative to other generalisation sites in the type. My current solution is to nudge the type checker by sprinkling a few {R = R} implicit bindings where needed, but this seems slightly less satisfactory, when the real culprit seems to be the relation _#_

I see two possible solutions:

  • delegate to using the explicit fresh operation where needed for disambiguation; but this changes the 'visible'/'legible' API when stating lemmas
  • introduce a small additional piece of notation, eg x #[ R ] xs where R needs to be made visible (and for some reason I couldn't seem to do this as syntax...?)

Thoughts? Eg. as

-- Convenient notation for freshness making A (and R) implicit
infix 5 _#[_]_ _#_

_#[_]_ : A → (R : Rel A r) → Pred (List# A R) _
x #[ R ] xs = fresh _ R x xs

_#_ : REL A (List# A R) _
x # xs = x #[ _ ] xs


------------------------------------------------------------------------
-- Operations for modifying fresh lists

module _ {R : Rel A r} {S : Rel B s} (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where
module _ (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where

map : List# A R → List# B S
map-# : ∀ {a} as → a # as → f a # map as
map-# : ∀ xs → x # xs → f x # map xs

map [] = []
map (cons a as ps) = cons (f a) (map as) (map-# as ps)
map (cons x xs ps) = cons (f x) (map xs) (map-# xs ps)

map-# [] _ = _
map-# (a ∷# as) (p , ps) = R⇒S p , map-# as ps
map-# (x ∷# xs) (p , ps) = R⇒S p , map-# xs ps

module _ {R : Rel B r} (f : A → B) where
module _ (f : A → B) where

map₁ : List# A (R on f) → List# B R
map₁ = map f id

module _ {R : Rel A r} {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where
module _ {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where

map₂ : List# A R → List# A S
map₂ = map id R⇒S

------------------------------------------------------------------------
-- Views

data Empty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
data Empty {A : Set a} {R : Rel A r} : Pred (List# A R) (a ⊔ r) where
[] : Empty []

data NonEmpty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
data NonEmpty {A : Set a} {R : Rel A r} : Pred (List# A R) (a ⊔ r) where
cons : ∀ x xs pr → NonEmpty (cons x xs pr)

------------------------------------------------------------------------
-- Operations for reducing fresh lists

length : {R : Rel A r} → List# A R → ℕ
length : List# A R → ℕ
length [] = 0
length (_ ∷# xs) = suc (length xs)

------------------------------------------------------------------------
-- Operations for constructing fresh lists

pattern [_] a = a ∷# []
pattern [_] x = x ∷# []

fromMaybe : {R : Rel A r} → Maybe A → List# A R
fromMaybe : Maybe A → List# A R
fromMaybe nothing = []
fromMaybe (just a) = [ a ]
fromMaybe (just x) = [ x ]

module _ {R : Rel A r} (R-refl : B.Reflexive R) where
module _ (refl : Reflexive {A = A} R) where

replicate : ℕ → A → List# A R
replicate-# : (n : ℕ) (a : A) → a # replicate n a
replicate-# : (n : ℕ) (x : A) → x # replicate n x

replicate zero a = []
replicate (suc n) a = cons a (replicate n a) (replicate-# n a)
replicate zero x = []
replicate (suc n) x = cons x (replicate n x) (replicate-# n x)

replicate-# zero a = _
replicate-# (suc n) a = R-refl , replicate-# n a
replicate-# zero x = _
replicate-# (suc n) x = refl , replicate-# n x

------------------------------------------------------------------------
-- Operations for deconstructing fresh lists

uncons : {R : Rel A r} → List# A R → Maybe (A × List# A R)
uncons : List# A R → Maybe (A × List# A R)
uncons [] = nothing
uncons (a ∷# as) = just (a , as)
uncons (x ∷# xs) = just (x , xs)

head : {R : Rel A r} → List# A R → Maybe A
head : List# A R → Maybe A
head = Maybe.map proj₁ ∘′ uncons

tail : {R : Rel A r} → List# A R → Maybe (List# A R)
tail : List# A R → Maybe (List# A R)
tail = Maybe.map proj₂ ∘′ uncons

take : {R : Rel A r} → ℕ → List# A R → List# A R
take-# : {R : Rel A r} → ∀ n a (as : List# A R) → a # as → a # take n as
take : ℕ → List# A R → List# A R
take-# : ∀ n y (xs : List# A R) → y # xs → y # take n xs
Copy link
Collaborator Author

@jamesmckinna jamesmckinna Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Eg if we were to introduce _#[_]_ then this could typecheck as:

Suggested change
take-# : ∀ n y (xs : List# A R) → y # xs → y # take n xs
take-# : ∀ n y xs → y #[ R ] xs → y # take n xs


take zero xs = []
take (suc n) [] = []
take (suc n) (cons a as ps) = cons a (take n as) (take-# n a as ps)
take (suc n) (cons x xs ps) = cons x (take n xs) (take-# n x xs ps)

take-# zero a xs _ = _
take-# (suc n) a [] ps = _
take-# (suc n) a (x ∷# xs) (p , ps) = p , take-# n a xs ps
take-# zero y xs _ = _
take-# (suc n) y [] ps = _
take-# (suc n) y (x ∷# xs) (p , ps) = p , take-# n y xs ps

drop : {R : Rel A r} → ℕ → List# A R → List# A R
drop zero as = as
drop : ℕ → List# A R → List# A R
drop zero xs = xs
drop (suc n) [] = []
drop (suc n) (a ∷# as) = drop n as
drop (suc n) (x ∷# xs) = drop n xs

module _ {P : Pred A p} (P? : U.Decidable P) where
module _ {P : Pred A p} (P? : Decidable P) where

takeWhile : {R : Rel A r} → List# A R → List# A R
takeWhile-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # takeWhile as
takeWhile : List# A R → List# A R
takeWhile-# : ∀ y (xs : List# A R) → y # xs → y # takeWhile xs
Copy link
Collaborator Author

@jamesmckinna jamesmckinna Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly

Suggested change
takeWhile-# : ∀ y (xs : List# A R) → y # xs → y # takeWhile xs
takeWhile-# : ∀ y xs → y #[ R ] xs → y # takeWhile xs


takeWhile [] = []
takeWhile (cons a as ps) =
if does (P? a) then cons a (takeWhile as) (takeWhile-# a as ps) else []
takeWhile (cons x xs ps) =
if does (P? x) then cons x (takeWhile xs) (takeWhile-# x xs ps) else []

-- this 'with' is needed to cause reduction in the type of 'takeWhile (a ∷# as)'
takeWhile-# a [] _ = _
takeWhile-# a (x ∷# xs) (p , ps) with does (P? x)
... | true = p , takeWhile-# a xs ps
takeWhile-# y [] _ = _
takeWhile-# y (x ∷# xs) (p , ps) with does (P? x)
... | true = p , takeWhile-# y xs ps
... | false = _

dropWhile : {R : Rel A r} → List# A R → List# A R
dropWhile : List# A R → List# A R
dropWhile [] = []
dropWhile aas@(a ∷# as) = if does (P? a) then dropWhile as else aas
dropWhile xxs@(x ∷# xs) = if does (P? x) then dropWhile xs else xxs

filter : {R : Rel A r} → List# A R → List# A R
filter-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # filter as
filter : List# A R → List# A R
filter-# : ∀ y (xs : List# A R) → y # xs → y # filter xs
Copy link
Collaborator Author

@jamesmckinna jamesmckinna Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
filter-# : ∀ y (xs : List# A R) → y # xs → y # filter xs
filter-# : ∀ y xs → y #[ R ] xs → y # filter xs

etc.


filter [] = []
filter (cons a as ps) =
let l = filter as in
if does (P? a) then cons a l (filter-# a as ps) else l
filter (cons x xs ps) =
let l = filter xs in
if does (P? x) then cons x l (filter-# x xs ps) else l

-- this 'with' is needed to cause reduction in the type of 'filter-# a (x ∷# xs)'
filter-# a [] _ = _
filter-# a (x ∷# xs) (p , ps) with does (P? x)
... | true = p , filter-# a xs ps
... | false = filter-# a xs ps
-- this 'with' is needed to cause reduction in the type of 'filter-# y (x ∷# xs)'
filter-# y [] _ = _
filter-# y (x ∷# xs) (p , ps) with does (P? x)
... | true = p , filter-# y xs ps
... | false = filter-# y xs ps

------------------------------------------------------------------------
-- Relationship to List and AllPairs

toList : {R : Rel A r} → List# A R → ∃ (AllPairs R)
toAll : ∀ {R : Rel A r} {a} as → fresh A R a as → All (R a) (proj₁ (toList as))
toList : List# A R → ∃ (AllPairs R)
toAll : (xs : List# A R) → x # xs → All (R x) (proj₁ (toList xs))
Copy link
Collaborator Author

@jamesmckinna jamesmckinna Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
toAll : (xs : List# A R) → x # xs → All (R x) (proj₁ (toList xs))
toAll : ∀ xs → x #[ R ] xs → All (R x) (proj₁ (toList xs))


toList [] = -, []
toList (cons x xs ps) = -, toAll xs ps ∷ proj₂ (toList xs)

toAll [] ps = []
toAll (a ∷# as) (p , ps) = p ∷ toAll as ps
toAll (x ∷# xs) (p , ps) = p ∷ toAll xs ps

fromList : ∀ {R : Rel A r} {xs} → AllPairs R xs → List# A R
fromList-# : ∀ {R : Rel A r} {x xs} (ps : AllPairs R xs) →
fromList : ∀ {xs} → AllPairs R xs → List# A R
fromList-# : ∀ {xs} (ps : AllPairs R xs) →
All (R x) xs → x # fromList ps

fromList [] = []
Expand Down
18 changes: 11 additions & 7 deletions src/Data/List/Fresh/Membership/Setoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,22 +10,26 @@ open import Relation.Binary.Bundles using (Setoid)

module Data.List.Fresh.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where

open import Level using (Level; _⊔_)
open import Level using (Level)
open import Data.List.Fresh using (List#)
open import Data.List.Fresh.Relation.Unary.Any as Any using (Any)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Core using (Rel; REL)
open import Relation.Nullary.Negation.Core using (¬_)

open Setoid S renaming (Carrier to A)

infix 4 _∈_ _∉_
open Setoid S
using (_≈_)
renaming (Carrier to A)

private
variable
r : Level
R : Rel A r


infix 4 _∈_ _∉_

_∈_ : {R : Rel A r} → A → List# A R → Set _
_∈_ : REL A (List# A R) _
x ∈ xs = Any (x ≈_) xs

_∉_ : {R : Rel A r} → A → List# A R → Set _
_∉_ : REL A (List# A R) _
x ∉ xs = ¬ (x ∈ xs)
Loading