Grace/Cumulus/List/Count.g17

Open in Workbench Download source

Imports

Filter

Declarations

Source

1-- Occurrences of an element in a list: the count, its interaction with2-- concatenation, reversal, filtering, and constant lists, and positivity3-- as membership in the support4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.List.Count10import Filter1112def listCount {A : Set} (x : Set) (xs : List(A)) → Set13  | x, List.nil => 014  | x, List.cons(a, tail) => add(indicator({x}, a), listCount(x, tail))15  descends xs1617theorem listCount.nil (A x : Set)18  shows listCount{A}(x, []) = 019proof20  simp [listCount]2122theorem listCount.cons (A x a : Set) (xs : List(A))23  requires element : a ∈ A24  shows listCount{A}(x, a :: xs) = indicator({x}, a) + listCount{A}(x, xs)25proof26  simp [listCount]2728theorem listCount.natural (A x : Set) (xs : List(A))29  shows Nat(listCount{A}(x, xs))30proof31  induction xs32  | List.nil =>33    rw listCount.nil34    typecheck35  | List.cons(a, tail) using ih =>36    have element : a ∈ A by assumption37    have mark := indicator.natural at {x}, a38    rw listCount.cons39    typecheck4041theorem listCount.cons_self (A x : Set) (xs : List(A))42  requires element : x ∈ A43  shows listCount{A}(x, x :: xs) = 1 + listCount{A}(x, xs)44proof45  have mark := indicator.singleton_self at x46  rw [listCount.cons, mark]47  rfl4849theorem listCount.cons_other (A x a : Set) (xs : List(A))50  requires element : a ∈ A51  requires different : x ≠ a52  shows listCount{A}(x, a :: xs) = listCount{A}(x, xs)53proof54  have mark := indicator.singleton_other with different55  have natural := listCount.natural at A, x, xs with *56  rw [listCount.cons, mark, add.left_unit]57  rfl5859theorem listCount.singleton_self (A x : Set)60  requires element : x ∈ A61  shows listCount{A}(x, x :: []) = 162proof63  have mark := indicator.singleton_self at x64  simp [listCount, mark, add]6566theorem listCount.singleton_other (A x a : Set)67  requires element : a ∈ A68  requires different : x ≠ a69  shows listCount{A}(x, a :: []) = 070proof71  have mark := indicator.singleton_other with different72  simp [listCount, mark, add]7374theorem listCount.append (A x : Set) (xs ys : List(A))75  shows listCount{A}(x, append(ys, xs)) = listCount{A}(x, xs) + listCount{A}(x, ys)76proof77  induction xs78  | List.nil =>79    have natural := listCount.natural at A, x, ys with *80    rw [append.nil, listCount.nil, add.left_unit]81    rfl82  | List.cons(a, tail) using ih =>83    have element : a ∈ A by assumption84    have appended := append.closed at A, tail, ys with *85    have mark := indicator.natural at {x}, a86    have tailNat := listCount.natural at A, x, tail with *87    have ysNat := listCount.natural at A, x, ys with *88    rw [append.cons, listCount.cons, ih, listCount.cons, add.associative]89    rfl9091theorem listCount.reverse (A x : Set) (xs : List(A))92  shows listCount{A}(x, reverse(xs)) = listCount{A}(x, xs)93proof94  induction xs95  | List.nil =>96    rw reverse.nil97    rfl98  | List.cons(a, tail) using ih =>99    have element : a ∈ A by assumption100    have single : List(A, a :: []) by typecheck101    have reversed : List(A, reverse(tail)) by typecheck102    have mark := indicator.natural at {x}, a103    have tailNat := listCount.natural at A, x, tail with *104    have nilList : List(A, []) by typecheck105    rw [reverse.cons, listCount.append, ih, listCount.cons, listCount.cons, listCount.nil]106    rw [add.right_unit, add.commutative]107    rfl108109theorem listCount.le_length (A x : Set) (xs : List(A))110  shows listCount{A}(x, xs) ≤ length{A}(xs)111proof112  induction xs113  | List.nil =>114    rw [listCount.nil, length.nil]115    arith116  | List.cons(a, tail) using ih =>117    have element : a ∈ A by assumption118    have tailNat := listCount.natural at A, x, tail with *119    rw [listCount.cons, length.cons]120    have alternatives : x = a ∨ x ≠ a by tauto121    cases alternatives with same | different122    . have mark : indicator({x}, a) = 1123        rw same124        exact indicator.singleton_self at a125      rw mark126      arith127    . have mark := indicator.singleton_other with different128      rw [mark, add.left_unit]129      arith130131theorem listCount.positive_of_mem (A x : Set) (xs : List(A))132  requires member : x ∈ listSupport{A}(xs)133  shows 0 < listCount{A}(x, xs)134proof135  induction xs136  | List.nil =>137    intro member138    rw listSupport.nil at member139    exfalso140    exact set.empty with member141  | List.cons(a, tail) using ih =>142    intro member143    have element : a ∈ A by assumption144    have tailNat := listCount.natural at A, x, tail with *145    have split := listSupport.mem_cons_iff.forward with element, member146    rw listCount.cons147    cases split with head | rest148    . have mark : indicator({x}, a) = 1149        rw head150        exact indicator.singleton_self at a151      rw mark152      arith153    . have inner := ih with rest154      have mark := indicator.natural at {x}, a155      arith156157theorem listCount.mem_of_positive (A x : Set) (xs : List(A))158  requires positive : 0 < listCount{A}(x, xs)159  shows x ∈ listSupport{A}(xs)160proof161  induction xs162  | List.nil =>163    intro positive164    rw listCount.nil at positive165    exfalso166    exact Less.irreflexive with Naturals.constructor.zero, positive167  | List.cons(a, tail) using ih =>168    intro positive169    have element : a ∈ A by assumption170    have tailNat := listCount.natural at A, x, tail with *171    have alternatives : x = a ∨ x ≠ a by tauto172    cases alternatives with same | different173    . rw same174      exact listSupport.mem_cons_self with element175    . rw listCount.cons_other at positive176      have inner := ih with positive177      exact listSupport.mem_cons_of_mem with element, inner178179theorem listCount.positive_iff (A x : Set) (xs : List(A))180  shows 0 < listCount{A}(x, xs) ↔ x ∈ listSupport{A}(xs)181proof182  constructor183  . intro positive184    exact listCount.mem_of_positive with positive185  . intro member186    exact listCount.positive_of_mem with member187188theorem listCount.zero_of_absent (A x : Set) (xs : List(A))189  requires absent : ¬(x ∈ listSupport{A}(xs))190  shows listCount{A}(x, xs) = 0191proof192  have natural := listCount.natural at A, x, xs with *193  have shape := natural.zero_or_successor at listCount{A}(x, xs) with natural194  cases shape with zero | successor195  . exact zero196  . obtain ⟨k, kNat, equal⟩ := successor197    have positive : 0 < listCount{A}(x, xs)198      rw equal199      arith200    have member := listCount.mem_of_positive with positive201    exfalso202    exact absent with member203204theorem listCount.absent_of_zero (A x : Set) (xs : List(A))205  requires zero : listCount{A}(x, xs) = 0206  shows ¬(x ∈ listSupport{A}(xs))207proof208  intro member209  have positive := listCount.positive_of_mem with member210  rw zero at positive211  exact Less.irreflexive with Naturals.constructor.zero, positive212213theorem listCount.zero_iff (A x : Set) (xs : List(A))214  shows listCount{A}(x, xs) = 0 ↔ ¬(x ∈ listSupport{A}(xs))215proof216  constructor217  . intro zero218    exact listCount.absent_of_zero with zero219  . intro absent220    exact listCount.zero_of_absent with absent221222theorem listCount.outside_carrier (A x : Set) (xs : List(A))223  requires outside : ¬(x ∈ A)224  shows listCount{A}(x, xs) = 0225proof226  have absent : ¬(x ∈ listSupport{A}(xs))227    intro member228    have subset := listSupport.subset at A, xs with *229    have inA := subset with x, member230    exact outside with inA231  exact listCount.zero_of_absent with absent232233theorem listCount.replicate_self (A x : Set) (n : Nat)234  requires element : x ∈ A235  shows listCount{A}(x, listReplicate(n, x)) = n236proof237  induction n238  | zero =>239    rw [listReplicate.zero, listCount.nil]240    rfl241  | succ(k) using ih =>242    have list := listReplicate.closed at A, x, k with element243    rw [listReplicate.succ, listCount.cons_self, ih, add.commutative, add.right_one]244    rfl245246theorem listCount.replicate_other (A x y : Set) (n : Nat)247  requires element : x ∈ A248  requires different : y ≠ x249  shows listCount{A}(y, listReplicate(n, x)) = 0250proof251  have absent : ¬(y ∈ listSupport{A}(listReplicate(n, x)))252    intro member253    have equal := listReplicate.mem_support with element, member254    exact different with equal255  exact listCount.zero_of_absent with absent256257theorem listCount.filter_member (A S x : Set) (xs : List(A))258  requires member : x ∈ S259  shows listCount{A}(x, listFilter{A}(S, xs)) = listCount{A}(x, xs)260proof261  induction xs262  | List.nil =>263    rw listFilter.nil264    rfl265  | List.cons(a, tail) using ih =>266    have element : a ∈ A by assumption267    have filtered := listFilter.closed at A, S, tail with *268    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto269    cases alternatives with inS | absent270    . rw [listFilter.cons_member, listCount.cons, listCount.cons, ih]271      rfl272    . have different : x ≠ a273        intro same274        rw same at member275        exact absent with member276      rw [listFilter.cons_other, listCount.cons_other, ih]277      rfl278279theorem listCount.filter_other (A S x : Set) (xs : List(A))280  requires absent : ¬(x ∈ S)281  shows listCount{A}(x, listFilter{A}(S, xs)) = 0282proof283  have filtered := listFilter.closed at A, S, xs with *284  have outside : ¬(x ∈ listSupport{A}(listFilter{A}(S, xs)))285    intro member286    have both := listFilter.mem_support with member287    exact absent with both.right288  exact listCount.zero_of_absent with outside289290-- The count is the length of the entries equal to x.291theorem listCount.filter_length (A x : Set) (xs : List(A))292  shows listCount{A}(x, xs) = length{A}(listFilter{A}({x}, xs))293proof294  induction xs295  | List.nil =>296    rw [listCount.nil, listFilter.nil, length.nil]297    rfl298  | List.cons(a, tail) using ih =>299    have element : a ∈ A by assumption300    have filtered := listFilter.closed at A, {x}, tail with *301    have alternatives : x = a ∨ x ≠ a by tauto302    cases alternatives with same | different303    . have elementX : x ∈ A304        rw same305        exact element306      have inSingle : x ∈ {x} := singleton.self at x307      rw [← same, listCount.cons_self, listFilter.cons_member, length.cons, ih]308      rw [add.commutative, add.right_one]309      rfl310    . have notSingle : ¬(a ∈ {x})311        intro inSingle312        have equal := singleton.membership.forward with inSingle313        symm at equal314        exact different with equal315      rw [listCount.cons_other, listFilter.cons_other, ih]316      rfl317318theorem listCount.take_add_drop (A x : Set) (xs : List(A)) (n : Nat)319  shows listCount{A}(x, listTake{A}(n, xs)) + listCount{A}(x, listDrop{A}(n, xs)) =320    listCount{A}(x, xs)321proof322  have split := listTake.append_drop at A, xs, n with *323  have taken := listTake.closed at A, xs, n with *324  have dropped := listDrop.closed at A, xs, n with *325  have counts := listCount.append at A, x, listTake{A}(n, xs), listDrop{A}(n, xs) with *326  rw split at counts327  symm328  exact counts329330theorem listCount.cons_le (A x a : Set) (xs : List(A))331  requires element : a ∈ A332  shows listCount{A}(x, xs) ≤ listCount{A}(x, a :: xs)333proof334  have mark := indicator.natural at {x}, a335  have tailNat := listCount.natural at A, x, xs with *336  rw listCount.cons337  arith338339theorem listCount.eq_length (A x : Set) (xs : List(A))340  requires element : x ∈ A341  requires full : listCount{A}(x, xs) = length{A}(xs)342  shows xs = listReplicate(length{A}(xs), x)343proof344  have filtered := listFilter.closed at A, {x}, xs with *345  rw listCount.filter_length at full346  have same := listFilter.length_eq_of_all with full347  have covered := listFilter.support_in at A, {x}, xs with *348  rw same at covered349  exact List.constant_of_support with element, covered350351theorem listCount.le_of_support_subset (A x : Set) (xs : List(A))352  requires element : x ∈ A353  requires covered : listSupport{A}(xs) ⊆ {x}354  shows listCount{A}(x, xs) = length{A}(xs)355proof356  have constant := List.constant_of_support with element, covered357  have count := listCount.replicate_self at A, x, length{A}(xs) with element358  rw ← constant at count359  exact count360