Grace/Cumulus/List/NoDup.g17

Open in Workbench Download source

Imports

Range

Declarations

Source

1-- Lists without repeated entries: every count is at most one, and this2-- passes to tails, prefixes, suffixes, filters, reversals, and permutations3-- 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.NoDup9import Range1011predicate ListNoDup (A xs : Set) := ∀ x, listCount{A}(x, xs) ≤ 11213theorem ListNoDup.nil (A : Set)14  shows ListNoDup(A, [])15proof16  unfold ListNoDup17  intro x18  rw listCount.nil19  arith2021theorem ListNoDup.count_le (A x : Set) (xs : List(A))22  requires nodup : ListNoDup(A, xs)23  shows listCount{A}(x, xs) ≤ 124proof25  exact nodup with x2627theorem ListNoDup.count_eq_one (A x : Set) (xs : List(A))28  requires nodup : ListNoDup(A, xs)29  requires member : x ∈ listSupport{A}(xs)30  shows listCount{A}(x, xs) = 131proof32  have upper := nodup with x33  have positive := listCount.positive_of_mem with member34  have natural := listCount.natural at A, x, xs with *35  have lower : 1 ≤ listCount{A}(x, xs) by arith36  exact LessEqual.antisymmetric with upper, lower3738theorem ListNoDup.singleton (A a : Set)39  requires element : a ∈ A40  shows ListNoDup(A, a :: [])41proof42  unfold ListNoDup43  intro x44  have alternatives : x = a ∨ x ≠ a by tauto45  cases alternatives with same | different46  . rw [same, listCount.singleton_self]47    arith48  . rw listCount.singleton_other49    arith5051theorem ListNoDup.head_absent (A a : Set) (xs : List(A))52  requires element : a ∈ A53  requires nodup : ListNoDup(A, a :: xs)54  shows ¬(a ∈ listSupport{A}(xs))55proof56  intro member57  have count := nodup with a58  have positive := listCount.positive_of_mem with member59  have natural := listCount.natural at A, a, xs with *60  rw listCount.cons_self at count61  arith6263theorem ListNoDup.tail (A a : Set) (xs : List(A))64  requires element : a ∈ A65  requires nodup : ListNoDup(A, a :: xs)66  shows ListNoDup(A, xs)67proof68  unfold ListNoDup69  intro x70  have count := nodup with x71  have mark := indicator.natural at {x}, a72  have natural := listCount.natural at A, x, xs with *73  rw listCount.cons at count74  arith7576theorem ListNoDup.cons (A a : Set) (xs : List(A))77  requires element : a ∈ A78  requires absent : ¬(a ∈ listSupport{A}(xs))79  requires nodup : ListNoDup(A, xs)80  shows ListNoDup(A, a :: xs)81proof82  unfold ListNoDup83  intro x84  have natural := listCount.natural at A, x, xs with *85  have alternatives : x = a ∨ x ≠ a by tauto86  cases alternatives with same | different87  . have zero := listCount.zero_of_absent with absent88    rw [same, listCount.cons_self, zero]89    arith90  . rw listCount.cons_other91    exact nodup with x9293theorem ListNoDup.cons_iff (A a : Set) (xs : List(A))94  requires element : a ∈ A95  shows ListNoDup(A, a :: xs) ↔ (¬(a ∈ listSupport{A}(xs)) ∧ ListNoDup(A, xs))96proof97  constructor98  . intro nodup99    have absent := ListNoDup.head_absent with nodup100    have tail := ListNoDup.tail with nodup101    exact ⟨absent, tail⟩102  . intro both103    obtain ⟨absent, tail⟩ := both104    exact ListNoDup.cons with absent, tail105106theorem ListNoDup.of_permutation (A : Set) (xs ys : List(A))107  requires permutation : ListPermutation(A, xs, ys)108  requires nodup : ListNoDup(A, xs)109  shows ListNoDup(A, ys)110proof111  unfold ListNoDup112  intro x113  have count := permutation with x114  rw ← count115  exact nodup with x116117theorem ListNoDup.reverse (A : Set) (xs : List(A))118  requires nodup : ListNoDup(A, xs)119  shows ListNoDup(A, reverse(xs))120proof121  unfold ListNoDup122  intro x123  rw listCount.reverse124  exact nodup with x125126theorem ListNoDup.prefix (A : Set) (xs ys : List(A))127  requires prefix : ListPrefix(A, xs, ys)128  requires nodup : ListNoDup(A, ys)129  shows ListNoDup(A, xs)130proof131  unfold ListNoDup132  intro x133  have bound := ListPrefix.count_le at A, x, xs, ys with prefix134  have upper := nodup with x135  exact LessEqual.transitive with bound, upper136137theorem ListNoDup.suffix (A : Set) (xs ys : List(A))138  requires suffix : ListSuffix(A, xs, ys)139  requires nodup : ListNoDup(A, ys)140  shows ListNoDup(A, xs)141proof142  unfold ListNoDup143  intro x144  have bound := ListSuffix.count_le at A, x, xs, ys with suffix145  have upper := nodup with x146  exact LessEqual.transitive with bound, upper147148theorem ListNoDup.take (A : Set) (xs : List(A)) (n : Nat)149  requires nodup : ListNoDup(A, xs)150  shows ListNoDup(A, listTake{A}(n, xs))151proof152  have taken := listTake.closed at A, xs, n with *153  have prefix := ListPrefix.take at A, xs, n with *154  exact ListNoDup.prefix with prefix, nodup155156theorem ListNoDup.drop (A : Set) (xs : List(A)) (n : Nat)157  requires nodup : ListNoDup(A, xs)158  shows ListNoDup(A, listDrop{A}(n, xs))159proof160  have dropped := listDrop.closed at A, xs, n with *161  have suffix := ListSuffix.drop at A, xs, n with *162  exact ListNoDup.suffix with suffix, nodup163164theorem ListNoDup.filter (A S : Set) (xs : List(A))165  requires nodup : ListNoDup(A, xs)166  shows ListNoDup(A, listFilter{A}(S, xs))167proof168  unfold ListNoDup169  intro x170  have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto171  cases alternatives with member | absent172  . rw listCount.filter_member173    exact nodup with x174  . rw listCount.filter_other175    arith176177theorem ListNoDup.append_disjoint (A : Set) (xs ys : List(A))178  requires first : ListNoDup(A, xs)179  requires second : ListNoDup(A, ys)180  requires disjoint : ∀ x ∈ listSupport{A}(xs), ¬(x ∈ listSupport{A}(ys))181  shows ListNoDup(A, append(ys, xs))182proof183  unfold ListNoDup184  intro x185  have xsNat := listCount.natural at A, x, xs with *186  have ysNat := listCount.natural at A, x, ys with *187  rw listCount.append188  have alternatives : x ∈ listSupport{A}(xs) ∨ ¬(x ∈ listSupport{A}(xs)) by tauto189  cases alternatives with member | absent190  . have other := disjoint with x, member191    have zero := listCount.zero_of_absent with other192    have bound := first with x193    rw zero194    arith195  . have zero := listCount.zero_of_absent with absent196    have bound := second with x197    rw zero198    arith199200theorem ListNoDup.append_left (A : Set) (xs ys : List(A))201  requires nodup : ListNoDup(A, append(ys, xs))202  shows ListNoDup(A, xs)203proof204  have prefix := ListPrefix.append at A, xs, ys with *205  exact ListNoDup.prefix with prefix, nodup206207theorem ListNoDup.append_right (A : Set) (xs ys : List(A))208  requires nodup : ListNoDup(A, append(ys, xs))209  shows ListNoDup(A, ys)210proof211  have suffix := ListSuffix.append at A, ys, xs with *212  exact ListNoDup.suffix with suffix, nodup213214theorem ListNoDup.append_disjoint_supports (A : Set) (xs ys : List(A))215  requires nodup : ListNoDup(A, append(ys, xs))216  shows ∀ x ∈ listSupport{A}(xs), ¬(x ∈ listSupport{A}(ys))217proof218  intros x member other219  have bound := nodup with x220  have left := listCount.positive_of_mem with member221  have right := listCount.positive_of_mem with other222  have xsNat := listCount.natural at A, x, xs with *223  have ysNat := listCount.natural at A, x, ys with *224  rw listCount.append at bound225  arith226227theorem ListNoDup.replicate (A x : Set) (n : Nat)228  requires element : x ∈ A229  requires nodup : ListNoDup(A, listReplicate(n, x))230  shows n ≤ 1231proof232  have list := listReplicate.closed at A, x, n with element233  have bound := nodup with x234  rwa listCount.replicate_self at bound235236theorem ListNoDup.range (n : Nat)237  shows ListNoDup(ℕ, listRange(n))238proof239  have list := listRange.closed at n with *240  unfold ListNoDup241  intro x242  have alternatives : x ∈ listSupport{ℕ}(listRange(n)) ∨ ¬(x ∈ listSupport{ℕ}(listRange(n))) by tauto243  cases alternatives with member | absent244  . have both := listRange.mem_support_iff.forward at n, x with member245    obtain ⟨xNat, below⟩ := both246    have one := listRange.count_below at n, x with below247    rw one248    arith249  . have zero := listCount.zero_of_absent with absent250    rw zero251    arith252