Grace/Cumulus/Cardinal/ListSupport.g17

Open in Workbench Download source

Imports

Sum · Core.List

Declarations

Source

1-- Finite list supports and finiteness of their subsets (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.ListSupport8import Sum9import Core.List1011def listSupport {C : Set} (xs : List(C)) → Set12  | List.nil => ∅13  | List.cons(x, tail) => insert(x, listSupport(tail))1415theorem listSupport.nil (C : Set)16  shows listSupport{C}([]) = ∅17proof18  simp [listSupport]1920theorem listSupport.cons (C x : Set) (xs : List(C))21  requires hx : x ∈ C22  shows listSupport{C}(x :: xs) = insert(x, listSupport{C}(xs))23proof24  simp [listSupport]2526theorem Finite.insert (A x : Set)27  requires finite : Finite(A)28  shows Finite(insert(x, A))29proof30  have casesX : x ∈ A ∨ ¬(x ∈ A) by tauto31  cases casesX with member | fresh32  . have same : insert(x, A) = A33      ext y34      simp35    rwa same36  . obtain ⟨n, natural, equinumerous⟩ := finite37    obtain ⟨f, bijective⟩ := equinumerous38    have nFresh := membership.irreflexive at n39    have extended := adjoinMap.bijective with bijective, fresh, nFresh40    have successor := natural.successor_as_insert with natural41    have nextNat := Naturals.constructor.succ with natural42    have cardinality : HasCardinality(insert(x, A), succ(n))43      unfold HasCardinality44      refine ⟨nextNat, ?_⟩45      witness adjoinMap(f, x, n)46      rwa successor47    exact Finite.from_cardinality with cardinality4849theorem listSupport.subset (C : Set) (xs : List(C))50  shows listSupport{C}(xs) ⊆ C51proof52  induction xs53  | List.nil =>54    rw listSupport55    exact empty.subset56  | List.cons(x, tail) using ih =>57    rw listSupport58    have member : x ∈ C by assumption59    simp6061theorem listSupport.append (C : Set) (ys xs : List(C))62  shows listSupport{C}(ListOps.append{C}(ys, xs)) = listSupport{C}(xs) ∪ listSupport{C}(ys)63proof64  induction xs65  | List.nil =>66    simp [ListOps.append, listSupport]67    ext x68    simp69  | List.cons(x, tail) using ih =>70    simp [ListOps.append, listSupport, ih]71    ext y72    simp7374-- Remove the head if it is present; recurse on a subset of the tail support.75theorem listSupport.finite_subsets (C : Set) (xs : List(C))76  shows ∀ S, S ⊆ listSupport{C}(xs) → Finite(S)77proof78  induction xs79  | List.nil =>80    intros S subset81    rw listSupport at subset82    have equal : S = ∅83      apply Subset.antisymmetric with subset84      exact empty.subset85    rw equal86    exact Finite.empty87  | List.cons(x, tail) using ih =>88    intros S subset89    rw listSupport at subset90    have casesX : x ∈ S ∨ ¬(x ∈ S) by tauto91    cases casesX with member | absent92    . have restSubset : S ∖ {x} ⊆ listSupport{C}(tail) by simp93      have restFinite := ih with S ∖ {x}, restSubset94      have restored : insert(x, S ∖ {x}) = S95        ext y96        have equalityCases : y = x ∨ y ≠ x by tauto97        cases equalityCases with equal | distinct98        . rw equal99          have left := insert.self at x, S ∖ {x}100          tauto101        . settle with insert.membership, difference.membership, singleton.membership102      have finite := Finite.insert at S ∖ {x}, x with restFinite103      rwa restored at finite104    . have restSubset : S ⊆ listSupport{C}(tail) by simp105      exact ih with S, restSubset106107theorem listSupport.finite (C : Set) (xs : List(C))108  shows Finite(listSupport{C}(xs))109proof110  have subsets := listSupport.finite_subsets at C, xs111  have reflexive : listSupport{C}(xs) ⊆ listSupport{C}(xs) by simp [Subset]112  exact subsets with listSupport{C}(xs), reflexive113114-- List every value on a natural prefix, without choosing from any family.115theorem FunctionBetween.list_cover_prefix (n : Nat)116  shows ∀ f, ∀ D, ∀ C, FunctionBetween(f, D, C) → n ⊆ D →117    ∃ xs, List(C, xs) ∧ (∀ i ∈ n, f(i) ∈ listSupport{C}(xs))118proof119  induction n120  | zero =>121    intros f D C function subset122    have nil : List(C, []) by typecheck123    refine ⟨[], nil, ?_⟩124    intros i hi125    have emptyMember : i ∈ ∅ by rwa ← nat.zero126    simp127  | succ(k) using ih =>128    intros f D C function subset129    have successor := natural.successor_as_insert at k with assumption130    have kIn : k ∈ succ(k) by simp131    have prefixSubset : k ⊆ D by simp132    have kInD : k ∈ D by simp133    have valueIn := FunctionBetween.apply_closed with function, kInD134    obtain ⟨xs, listX, covers⟩ := ih with f, D, C, function, prefixSubset135    have listNext : List(C, f(k) :: xs) by typecheck136    refine ⟨f(k) :: xs, listNext, ?_⟩137    intros i hi138    rw successor at hi139    have alternatives := insert.membership.forward with hi140    rw listSupport141    cases alternatives with equal | previous142    . rw equal143      exact insert.self144    . have old := covers with i, previous145      exact insert.contains with old146147theorem Finite.list_cover (S : Set)148  requires finite : Finite(S)149  shows ∃ xs, List(S, xs) ∧ S ⊆ listSupport{S}(xs)150proof151  obtain ⟨n, natural, equinumerous⟩ := finite152  obtain ⟨f, bijective⟩ := equinumerous153  have inverse := converse.function_of_bijective with bijective154  have injective := Bijective.injective with bijective155  have function := Injective.function with injective156  have reflexive : n ⊆ n by simp [Subset]157  have enumeration := FunctionBetween.list_cover_prefix with natural158  obtain ⟨xs, listX, covers⟩ := enumeration with converse(f, S, n), n, S, inverse, reflexive159  refine ⟨xs, listX, ?_⟩160  intros x hx161  have indexIn := FunctionBetween.apply_closed with function, hx162  have recovered := Bijective.inverse_apply with bijective, hx163  have member := covers with f(x), indexIn164  rwa recovered at member165166theorem Finite.subset (S T : Set)167  requires finite : Finite(T)168  requires subset : S ⊆ T169  shows Finite(S)170proof171  obtain ⟨xs, listX, covers⟩ := Finite.list_cover with finite172  have included := Subset.transitive with subset, covers173  have subsets := listSupport.finite_subsets with listX174  exact subsets with S, included175176theorem List.weaken (C D : Set) (xs : List(C))177  requires subset : C ⊆ D178  shows List(D, xs)179proof180  induction xs181  | List.nil => typecheck182  | List.cons(x, tail) using ih =>183    have member := subset with x, assumption184    typecheck185186theorem listSupport.change_carrier (C D : Set) (xs : List(C))187  requires subset : C ⊆ D188  shows listSupport{C}(xs) = listSupport(D, xs)189proof190  induction xs191  | List.nil => simp [listSupport]192  | List.cons(x, tail) using ih =>193    have listD := List.weaken with *194    have member := subset with x195    simp [listSupport, ih]196197theorem Finite.cover_in (S C : Set)198  requires finite : Finite(S)199  requires subset : S ⊆ C200  shows ∃ xs, List(C, xs) ∧ S ⊆ listSupport{C}(xs)201proof202  obtain ⟨xs, listX, covers⟩ := Finite.list_cover with finite203  have listC := List.weaken at S, C, xs with *204  have same := listSupport.change_carrier at S, C, xs with *205  rw same at covers206  refine ⟨xs, listC, covers⟩207208theorem Finite.union (S T : Set)209  requires left : Finite(S)210  requires right : Finite(T)211  shows Finite(S ∪ T)212proof213  have subsetS := union2.subset_left at S, T214  have subsetT := union2.subset_right at S, T215  obtain ⟨xs, listX, coverX⟩ := Finite.cover_in with left, subsetS216  obtain ⟨ys, listY, coverY⟩ := Finite.cover_in with right, subsetT217  have combined : List(S ∪ T, ListOps.append{S ∪ T}(ys, xs)) by typecheck218  have equation := listSupport.append at S ∪ T, ys, xs with *219  have covered : S ∪ T ⊆ listSupport{S ∪ T}(ListOps.append{S ∪ T}(ys, xs))220    rw equation221    simp [Subset, union2.membership]222  have subsets := listSupport.finite_subsets with combined223  exact subsets with S ∪ T, covered224