Grace/Cumulus/List/Filter.g17

Open in Workbench Download source

Imports

TakeDrop · Set.Indicator

Declarations

Source

1-- Filtering a list by membership in a set: the entries kept, their2-- support, and how filtering passes through concatenation and reversal3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.List.Filter9import TakeDrop10import Set.Indicator1112-- Membership in S as a Boolean, through the natural-valued indicator.13def memberTest (S x : Set) : Bool := BoolOps.not(isZero(indicator(S, x)))1415theorem memberTest.true (S x : Set)16  requires member : x ∈ S17  shows memberTest(S, x) = Bool.true18proof19  have one := indicator.member with member20  simp [memberTest, one, isZero, BoolOps.not]2122theorem memberTest.false (S x : Set)23  requires absent : ¬(x ∈ S)24  shows memberTest(S, x) = Bool.false25proof26  have zero := indicator.absent with absent27  simp [memberTest, zero, isZero, BoolOps.not]2829theorem memberTest.congr (S T x y : Set)30  requires equivalent : x ∈ S ↔ y ∈ T31  shows memberTest(S, x) = memberTest(T, y)32proof33  have same := indicator.congr with equivalent34  simp [memberTest, same]3536def listFilter {A : Set} (S : Set) (xs : List(A)) → Set37  | S, List.nil => []38  | S, List.cons(a, tail) =>39    boolChoice(memberTest(S, a), a :: listFilter(S, tail), listFilter(S, tail))40  descends xs4142theorem listFilter.nil (A S : Set)43  shows listFilter{A}(S, []) = []44proof45  simp [listFilter]4647theorem listFilter.cons_member (A S a : Set) (xs : List(A))48  requires element : a ∈ A49  requires member : a ∈ S50  shows listFilter{A}(S, a :: xs) = a :: listFilter{A}(S, xs)51proof52  have test := memberTest.true with member53  simp [listFilter, test, boolChoice]5455theorem listFilter.cons_other (A S a : Set) (xs : List(A))56  requires element : a ∈ A57  requires absent : ¬(a ∈ S)58  shows listFilter{A}(S, a :: xs) = listFilter{A}(S, xs)59proof60  have test := memberTest.false with absent61  simp [listFilter, test, boolChoice]6263theorem listFilter.closed (A S : Set) (xs : List(A))64  shows List(A, listFilter{A}(S, xs))65proof66  induction xs67  | List.nil =>68    rw listFilter.nil69    typecheck70  | List.cons(a, tail) using ih =>71    have element : a ∈ A by assumption72    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto73    cases alternatives with member | absent74    . rw listFilter.cons_member75      typecheck76    . rw listFilter.cons_other77      exact ih7879theorem listFilter.length_le (A S : Set) (xs : List(A))80  shows length{A}(listFilter{A}(S, xs)) ≤ length{A}(xs)81proof82  induction xs83  | List.nil =>84    rw [listFilter.nil, length.nil]85    arith86  | List.cons(a, tail) using ih =>87    have element : a ∈ A by assumption88    have filtered := listFilter.closed at A, S, tail with *89    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto90    rw length.cons91    cases alternatives with member | absent92    . rw [listFilter.cons_member, length.cons]93      arith94    . rw listFilter.cons_other95      arith9697theorem listFilter.append (A S : Set) (xs ys : List(A))98  shows listFilter{A}(S, append(ys, xs)) =99    append(listFilter{A}(S, ys), listFilter{A}(S, xs))100proof101  induction xs102  | List.nil =>103    have filtered := listFilter.closed at A, S, ys with *104    rw [append.nil, listFilter.nil, append.nil]105    rfl106  | List.cons(a, tail) using ih =>107    have element : a ∈ A by assumption108    have appended := append.closed at A, tail, ys with *109    have filteredTail := listFilter.closed at A, S, tail with *110    have filteredYs := listFilter.closed at A, S, ys with *111    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto112    rw append.cons113    cases alternatives with member | absent114    . rw [listFilter.cons_member, listFilter.cons_member, ih, append.cons]115      rfl116    . rw [listFilter.cons_other, listFilter.cons_other, ih]117      rfl118119theorem listFilter.mem_support (A S y : Set) (xs : List(A))120  requires member : y ∈ listSupport{A}(listFilter{A}(S, xs))121  shows y ∈ listSupport{A}(xs) ∧ y ∈ S122proof123  induction xs124  | List.nil =>125    intro member126    rw [listFilter.nil, listSupport.nil] at member127    exfalso128    exact set.empty with member129  | List.cons(a, tail) using ih =>130    intro member131    have element : a ∈ A by assumption132    have filtered := listFilter.closed at A, S, tail with *133    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto134    cases alternatives with inS | absent135    . rw listFilter.cons_member at member136      have split := listSupport.mem_cons_iff.forward with element, member137      cases split with head | rest138      . rw head139        have headIn := listSupport.mem_cons_self at A, a, tail with element140        exact ⟨headIn, inS⟩141      . obtain ⟨inner, yS⟩ := ih with rest142        have outer := listSupport.mem_cons_of_mem with element, inner143        exact ⟨outer, yS⟩144    . rw listFilter.cons_other at member145      obtain ⟨inner, yS⟩ := ih with member146      have outer := listSupport.mem_cons_of_mem with element, inner147      exact ⟨outer, yS⟩148149theorem listFilter.support_subset (A S : Set) (xs : List(A))150  shows listSupport{A}(listFilter{A}(S, xs)) ⊆ listSupport{A}(xs)151proof152  intros y hy153  have both := listFilter.mem_support with hy154  exact both.left155156theorem listFilter.support_in (A S : Set) (xs : List(A))157  shows listSupport{A}(listFilter{A}(S, xs)) ⊆ S158proof159  intros y hy160  have both := listFilter.mem_support with hy161  exact both.right162163theorem listFilter.mem_support_of (A S y : Set) (xs : List(A))164  requires member : y ∈ listSupport{A}(xs)165  requires inS : y ∈ S166  shows y ∈ listSupport{A}(listFilter{A}(S, xs))167proof168  induction xs169  | List.nil =>170    intro member171    rw listSupport.nil at member172    exfalso173    exact set.empty with member174  | List.cons(a, tail) using ih =>175    intro member176    have element : a ∈ A by assumption177    have filtered := listFilter.closed at A, S, tail with *178    have split := listSupport.mem_cons_iff.forward with element, member179    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto180    cases alternatives with aS | absent181    . rw listFilter.cons_member182      cases split with head | rest183      . rw head184        exact listSupport.mem_cons_self with element185      . have inner := ih with rest186        exact listSupport.mem_cons_of_mem with element, inner187    . rw listFilter.cons_other188      cases split with head | rest189      . rw head at inS190        exfalso191        exact absent with inS192      . exact ih with rest193194theorem listFilter.mem_support_iff (A S y : Set) (xs : List(A))195  shows y ∈ listSupport{A}(listFilter{A}(S, xs)) ↔ y ∈ listSupport{A}(xs) ∧ y ∈ S196proof197  constructor198  . intro member199    exact listFilter.mem_support with member200  . intro both201    obtain ⟨member, inS⟩ := both202    exact listFilter.mem_support_of with member, inS203204theorem listFilter.support (A S : Set) (xs : List(A))205  shows listSupport{A}(listFilter{A}(S, xs)) = listSupport{A}(xs) ∩ S206proof207  ext y208  have kept := listFilter.mem_support_iff at A, S, y, xs with *209  have meet := intersection.membership at listSupport{A}(xs), S, y210  tauto211212theorem listFilter.all (A S : Set) (xs : List(A))213  requires covered : listSupport{A}(xs) ⊆ S214  shows listFilter{A}(S, xs) = xs215proof216  induction xs217  | List.nil =>218    intro covered219    exact listFilter.nil at A, S220  | List.cons(a, tail) using ih =>221    intro covered222    have element : a ∈ A by assumption223    have headIn := listSupport.mem_cons_self at A, a, tail with element224    have member := covered with a, headIn225    have rest : listSupport{A}(tail) ⊆ S226      intros y hy227      have outer := listSupport.mem_cons_of_mem with element, hy228      exact covered with y, outer229    have inner := ih with rest230    rw [listFilter.cons_member, inner]231    rfl232233theorem listFilter.carrier (A : Set) (xs : List(A))234  shows listFilter{A}(A, xs) = xs235proof236  have covered := listSupport.subset at A, xs with *237  exact listFilter.all with covered238239theorem listFilter.none (A S : Set) (xs : List(A))240  requires disjoint : ∀ y ∈ listSupport{A}(xs), ¬(y ∈ S)241  shows listFilter{A}(S, xs) = []242proof243  induction xs244  | List.nil =>245    intro disjoint246    exact listFilter.nil at A, S247  | List.cons(a, tail) using ih =>248    intro disjoint249    have element : a ∈ A by assumption250    have headIn := listSupport.mem_cons_self at A, a, tail with element251    have absent := disjoint with a, headIn252    have rest : ∀ y ∈ listSupport{A}(tail), ¬(y ∈ S)253      intros y hy254      have outer := listSupport.mem_cons_of_mem with element, hy255      exact disjoint with y, outer256    have inner := ih with rest257    rw [listFilter.cons_other, inner]258    rfl259260theorem listFilter.empty (A : Set) (xs : List(A))261  shows listFilter{A}(∅, xs) = []262proof263  have disjoint : ∀ y ∈ listSupport{A}(xs), ¬(y ∈ ∅)264    intros y hy265    exact set.empty at y266  exact listFilter.none with disjoint267268theorem listFilter.eq_nil (A S : Set) (xs : List(A))269  requires empty : listFilter{A}(S, xs) = []270  shows ∀ y ∈ listSupport{A}(xs), ¬(y ∈ S)271proof272  intros y hy inS273  have member := listFilter.mem_support_of with hy, inS274  rw [empty, listSupport.nil] at member275  exact set.empty with member276277theorem listFilter.nil_iff (A S : Set) (xs : List(A))278  shows listFilter{A}(S, xs) = [] ↔ ∀ y ∈ listSupport{A}(xs), ¬(y ∈ S)279proof280  constructor281  . intro empty282    exact listFilter.eq_nil with empty283  . intro disjoint284    exact listFilter.none with disjoint285286theorem listFilter.congr (A S T : Set) (xs : List(A))287  requires agreement : ∀ y ∈ listSupport{A}(xs), (y ∈ S ↔ y ∈ T)288  shows listFilter{A}(S, xs) = listFilter{A}(T, xs)289proof290  induction xs291  | List.nil =>292    intro agreement293    rw [listFilter.nil, listFilter.nil]294    rfl295  | List.cons(a, tail) using ih =>296    intro agreement297    have element : a ∈ A by assumption298    have headIn := listSupport.mem_cons_self at A, a, tail with element299    have head := agreement with a, headIn300    have rest : ∀ y ∈ listSupport{A}(tail), (y ∈ S ↔ y ∈ T)301      intros y hy302      have outer := listSupport.mem_cons_of_mem with element, hy303      exact agreement with y, outer304    have inner := ih with rest305    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto306    cases alternatives with inS | absent307    . have inT : a ∈ T := head.forward with inS308      rw [listFilter.cons_member, listFilter.cons_member, inner]309      rfl310    . have notT : ¬(a ∈ T)311        intro inT312        have inS := head.backward with inT313        exact absent with inS314      rw [listFilter.cons_other, listFilter.cons_other, inner]315      rfl316317theorem listFilter.filter (A S T : Set) (xs : List(A))318  shows listFilter{A}(S, listFilter{A}(T, xs)) = listFilter{A}(S ∩ T, xs)319proof320  induction xs321  | List.nil =>322    rw [listFilter.nil, listFilter.nil, listFilter.nil]323    rfl324  | List.cons(a, tail) using ih =>325    have element : a ∈ A by assumption326    have filtered := listFilter.closed at A, T, tail with *327    have alternativesT : a ∈ T ∨ ¬(a ∈ T) by tauto328    have alternativesS : a ∈ S ∨ ¬(a ∈ S) by tauto329    cases alternativesT with inT | notT330    . rw listFilter.cons_member331      cases alternativesS with inS | notS332      . have both : a ∈ S ∩ T by simp333        rw [listFilter.cons_member, listFilter.cons_member, ih]334        rfl335      . have notBoth : ¬(a ∈ S ∩ T) by simp336        rw [listFilter.cons_other, listFilter.cons_other, ih]337        rfl338    . have notBoth : ¬(a ∈ S ∩ T) by simp339      rw [listFilter.cons_other, listFilter.cons_other, ih]340      rfl341342theorem listFilter.idempotent (A S : Set) (xs : List(A))343  shows listFilter{A}(S, listFilter{A}(S, xs)) = listFilter{A}(S, xs)344proof345  have covered := listFilter.support_in at A, S, xs with *346  exact listFilter.all with covered347348theorem listFilter.commutative (A S T : Set) (xs : List(A))349  shows listFilter{A}(S, listFilter{A}(T, xs)) = listFilter{A}(T, listFilter{A}(S, xs))350proof351  rw [listFilter.filter, listFilter.filter, intersection.commutative]352  rfl353354theorem listFilter.singleton_member (A S a : Set)355  requires element : a ∈ A356  requires member : a ∈ S357  shows listFilter{A}(S, a :: []) = a :: []358proof359  have test := memberTest.true with member360  simp [listFilter, test, boolChoice]361362theorem listFilter.singleton_other (A S a : Set)363  requires element : a ∈ A364  requires absent : ¬(a ∈ S)365  shows listFilter{A}(S, a :: []) = []366proof367  have test := memberTest.false with absent368  simp [listFilter, test, boolChoice]369370theorem listFilter.reverse (A S : Set) (xs : List(A))371  shows listFilter{A}(S, reverse(xs)) = reverse(listFilter{A}(S, xs))372proof373  induction xs374  | List.nil =>375    rw [reverse.nil, listFilter.nil, reverse.nil]376    rfl377  | List.cons(a, tail) using ih =>378    have element : a ∈ A by assumption379    have single : List(A, a :: []) by typecheck380    have reversed : List(A, reverse(tail)) by typecheck381    have filtered := listFilter.closed at A, S, tail with *382    have filteredReversed := listFilter.closed at A, S, reverse(tail) with *383    have reversedFiltered : List(A, reverse(listFilter{A}(S, tail))) by typecheck384    rw [reverse.cons, listFilter.append, ih]385    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto386    cases alternatives with member | absent387    . rw [listFilter.singleton_member, listFilter.cons_member, reverse.cons]388      rfl389    . rw [listFilter.singleton_other, listFilter.cons_other, append.right_unit]390      rfl391392theorem listFilter.replicate_member (A S x : Set) (n : Nat)393  requires element : x ∈ A394  requires member : x ∈ S395  shows listFilter{A}(S, listReplicate(n, x)) = listReplicate(n, x)396proof397  have list := listReplicate.closed at A, x, n with element398  have covered := listReplicate.support_subset at A, x, n with element399  have inside : listSupport{A}(listReplicate(n, x)) ⊆ S400    intros y hy401    have single := covered with y, hy402    have equal := singleton.membership.forward with single403    rw equal404    exact member405  exact listFilter.all with inside406407theorem listFilter.replicate_other (A S x : Set) (n : Nat)408  requires element : x ∈ A409  requires absent : ¬(x ∈ S)410  shows listFilter{A}(S, listReplicate(n, x)) = []411proof412  have list := listReplicate.closed at A, x, n with element413  have covered := listReplicate.support_subset at A, x, n with element414  have disjoint : ∀ y ∈ listSupport{A}(listReplicate(n, x)), ¬(y ∈ S)415    intros y hy416    have single := covered with y, hy417    have equal := singleton.membership.forward with single418    rw equal419    exact absent420  exact listFilter.none with disjoint421422-- The kept and the discarded entries together account for the length.423theorem listFilter.length_add_complement (A S : Set) (xs : List(A))424  shows length{A}(listFilter{A}(S, xs)) + length{A}(listFilter{A}(A ∖ S, xs)) =425    length{A}(xs)426proof427  induction xs428  | List.nil =>429    rw [listFilter.nil, listFilter.nil, length.nil, add.right_unit]430    rfl431  | List.cons(a, tail) using ih =>432    have element : a ∈ A by assumption433    have kept := listFilter.closed at A, S, tail with *434    have discarded := listFilter.closed at A, A ∖ S, tail with *435    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto436    rw length.cons437    cases alternatives with member | absent438    . have notDifference : ¬(a ∈ A ∖ S) by simp439      rw [listFilter.cons_member, listFilter.cons_other, length.cons]440      have shift : succ(length{A}(listFilter{A}(S, tail))) + length{A}(listFilter{A}(A ∖ S, tail)) =441        succ(length{A}(listFilter{A}(S, tail)) + length{A}(listFilter{A}(A ∖ S, tail)))442        simp [add, add.succ_right]443      rw [shift, ih]444      rfl445    . have inDifference : a ∈ A ∖ S by simp446      rw [listFilter.cons_other, listFilter.cons_member, length.cons, add.succ_right, ih]447      rfl448449theorem listFilter.complement_length_le (A S : Set) (xs : List(A))450  shows length{A}(listFilter{A}(A ∖ S, xs)) ≤ length{A}(xs)451proof452  have total := listFilter.length_add_complement at A, S, xs with *453  have kept := listFilter.closed at A, S, xs with *454  have discarded := listFilter.closed at A, A ∖ S, xs with *455  rw ← total456  arith457458theorem listFilter.length_eq_of_all (A S : Set) (xs : List(A))459  requires full : length{A}(listFilter{A}(S, xs)) = length{A}(xs)460  shows listFilter{A}(S, xs) = xs461proof462  have total := listFilter.length_add_complement at A, S, xs with *463  have kept := listFilter.closed at A, S, xs with *464  have discarded := listFilter.closed at A, A ∖ S, xs with *465  rw full at total466  have padded : length{A}(xs) + length{A}(listFilter{A}(A ∖ S, xs)) = length{A}(xs) + 0467    rw add.right_unit468    exact total469  have zero := add.left_cancel with padded470  have emptyComplement := length.eq_zero with zero471  have disjoint := listFilter.eq_nil with emptyComplement472  have covered : listSupport{A}(xs) ⊆ S473    intros y hy474    have yA := listSupport.subset at A, xs with *475    have inA := yA with y, hy476    have notDifference := disjoint with y, hy477    have alternatives : y ∈ S ∨ ¬(y ∈ S) by tauto478    cases alternatives with inS | notS479    . exact inS480    . have inDifference : y ∈ A ∖ S by simp481      exfalso482      exact notDifference with inDifference483  exact listFilter.all with covered484