Grace/Cumulus/List/Permutation.g17

Open in Workbench Download source

Imports

Count

Declarations

Source

1-- Permutations of lists: equality of all counts, its equivalence laws,2-- splitting a list at an occurrence, and invariance of length, support,3-- and filtering4-- 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.Permutation10import Count1112-- Two lists are permutations of each other when every element occurs13-- equally often in both.14predicate ListPermutation (A xs ys : Set) :=15  ∀ x, listCount{A}(x, xs) = listCount{A}(x, ys)1617theorem ListPermutation.count (A x : Set) (xs ys : List(A))18  requires permutation : ListPermutation(A, xs, ys)19  shows listCount{A}(x, xs) = listCount{A}(x, ys)20proof21  exact permutation with x2223theorem ListPermutation.of_eq (A : Set) (xs ys : List(A))24  requires equal : xs = ys25  shows ListPermutation(A, xs, ys)26proof27  unfold ListPermutation28  intro x29  rw equal30  rfl3132theorem ListPermutation.reflexive (A : Set) (xs : List(A))33  shows ListPermutation(A, xs, xs)34proof35  unfold ListPermutation36  intro x37  rfl3839theorem ListPermutation.symmetric (A : Set) (xs ys : List(A))40  requires permutation : ListPermutation(A, xs, ys)41  shows ListPermutation(A, ys, xs)42proof43  unfold ListPermutation44  intro x45  have count := permutation with x46  symm at count47  exact count4849theorem ListPermutation.transitive (A : Set) (xs ys zs : List(A))50  requires first : ListPermutation(A, xs, ys)51  requires second : ListPermutation(A, ys, zs)52  shows ListPermutation(A, xs, zs)53proof54  unfold ListPermutation55  intro x56  have left := first with x57  have right := second with x58  rw left59  exact right6061theorem ListPermutation.cons (A a : Set) (xs ys : List(A))62  requires element : a ∈ A63  requires permutation : ListPermutation(A, xs, ys)64  shows ListPermutation(A, a :: xs, a :: ys)65proof66  unfold ListPermutation67  intro x68  have count := permutation with x69  rw [listCount.cons, listCount.cons, count]70  rfl7172theorem ListPermutation.cons_cancel (A a : Set) (xs ys : List(A))73  requires element : a ∈ A74  requires permutation : ListPermutation(A, a :: xs, a :: ys)75  shows ListPermutation(A, xs, ys)76proof77  unfold ListPermutation78  intro x79  have count := permutation with x80  have mark := indicator.natural at {x}, a81  rw [listCount.cons, listCount.cons] at count82  exact add.left_cancel with count8384theorem ListPermutation.append_right (A : Set) (xs ys zs : List(A))85  requires permutation : ListPermutation(A, xs, ys)86  shows ListPermutation(A, append(zs, xs), append(zs, ys))87proof88  unfold ListPermutation89  intro x90  have count := permutation with x91  rw [listCount.append, listCount.append, count]92  rfl9394theorem ListPermutation.append_left (A : Set) (xs ys zs : List(A))95  requires permutation : ListPermutation(A, xs, ys)96  shows ListPermutation(A, append(xs, zs), append(ys, zs))97proof98  unfold ListPermutation99  intro x100  have count := permutation with x101  rw [listCount.append, listCount.append, count]102  rfl103104theorem ListPermutation.append (A : Set) (xs ys us vs : List(A))105  requires first : ListPermutation(A, xs, ys)106  requires second : ListPermutation(A, us, vs)107  shows ListPermutation(A, append(us, xs), append(vs, ys))108proof109  unfold ListPermutation110  intro x111  have left := first with x112  have right := second with x113  rw [listCount.append, listCount.append, left, right]114  rfl115116theorem ListPermutation.append_commutative (A : Set) (xs ys : List(A))117  shows ListPermutation(A, append(ys, xs), append(xs, ys))118proof119  unfold ListPermutation120  intro x121  have xsNat := listCount.natural at A, x, xs with *122  have ysNat := listCount.natural at A, x, ys with *123  rw [listCount.append, listCount.append, add.commutative]124  rfl125126theorem ListPermutation.reverse (A : Set) (xs : List(A))127  shows ListPermutation(A, reverse(xs), xs)128proof129  unfold ListPermutation130  intro x131  exact listCount.reverse at A, x, xs with *132133theorem ListPermutation.swap (A a b : Set) (xs : List(A))134  requires first : a ∈ A135  requires second : b ∈ A136  shows ListPermutation(A, a :: b :: xs, b :: a :: xs)137proof138  unfold ListPermutation139  intro x140  have inner : List(A, b :: xs) by typecheck141  have other : List(A, a :: xs) by typecheck142  have markA := indicator.natural at {x}, a143  have markB := indicator.natural at {x}, b144  have count := listCount.natural at A, x, xs with *145  rw [listCount.cons, listCount.cons, listCount.cons, listCount.cons]146  exact add.swap at indicator({x}, b), listCount{A}(x, xs), indicator({x}, a) with *147148theorem ListPermutation.middle (A a : Set) (xs ys : List(A))149  requires element : a ∈ A150  shows ListPermutation(A, append(ys, a :: xs), a :: append(ys, xs))151proof152  unfold ListPermutation153  intro x154  have whole : List(A, a :: xs) by typecheck155  have appended := append.closed at A, xs, ys with *156  have mark := indicator.natural at {x}, a157  have xsNat := listCount.natural at A, x, xs with *158  have ysNat := listCount.natural at A, x, ys with *159  rw [listCount.append, listCount.cons, listCount.cons, listCount.append]160  exact add.associative at listCount{A}(x, xs), listCount{A}(x, ys), indicator({x}, a) with *161162theorem ListPermutation.rotate (A : Set) (xs : List(A)) (n : Nat)163  shows ListPermutation(A, xs, append(listTake{A}(n, xs), listDrop{A}(n, xs)))164proof165  have split := listTake.append_drop at A, xs, n with *166  have taken := listTake.closed at A, xs, n with *167  have dropped := listDrop.closed at A, xs, n with *168  have swapped := ListPermutation.append_commutative at A, listTake{A}(n, xs), listDrop{A}(n, xs) with *169  rwa split at swapped170171theorem ListPermutation.mem_support (A y : Set) (xs ys : List(A))172  requires permutation : ListPermutation(A, xs, ys)173  requires member : y ∈ listSupport{A}(xs)174  shows y ∈ listSupport{A}(ys)175proof176  have positive := listCount.positive_of_mem with member177  have count := permutation with y178  rw count at positive179  exact listCount.mem_of_positive with positive180181theorem ListPermutation.support (A : Set) (xs ys : List(A))182  requires permutation : ListPermutation(A, xs, ys)183  shows listSupport{A}(xs) = listSupport{A}(ys)184proof185  have back := ListPermutation.symmetric with permutation186  ext y187  constructor188  . intro member189    exact ListPermutation.mem_support with permutation, member190  . intro member191    exact ListPermutation.mem_support with back, member192193theorem ListPermutation.nil (A : Set) (xs : List(A))194  requires permutation : ListPermutation(A, xs, [])195  shows xs = []196proof197  have support := ListPermutation.support with permutation198  rw listSupport.nil at support199  exact listSupport.eq_empty with support200201theorem ListPermutation.filter (A S : Set) (xs ys : List(A))202  requires permutation : ListPermutation(A, xs, ys)203  shows ListPermutation(A, listFilter{A}(S, xs), listFilter{A}(S, ys))204proof205  unfold ListPermutation206  intro x207  have alternatives : x ∈ S ∨ ¬(x ∈ S) by tauto208  cases alternatives with member | absent209  . have left := listCount.filter_member at A, S, x, xs with member210    have right := listCount.filter_member at A, S, x, ys with member211    rw [left, right]212    exact permutation with x213  . have left := listCount.filter_other at A, S, x, xs with absent214    have right := listCount.filter_other at A, S, x, ys with absent215    rw [left, right]216    rfl217218-- A list is split at any element of its support.219theorem listSupport.split (A a : Set) (xs : List(A))220  requires member : a ∈ listSupport{A}(xs)221  shows ∃ front, List(A, front) ∧ ∃ back, List(A, back) ∧ xs = append(a :: back, front)222proof223  induction xs224  | List.nil =>225    intro member226    rw listSupport.nil at member227    exfalso228    exact set.empty with member229  | List.cons(b, tail) using ih =>230    intro member231    have element : b ∈ A by assumption232    have split := listSupport.mem_cons_iff.forward with element, member233    cases split with head | rest234    . have nilList : List(A, []) by typecheck235      refine ⟨[], nilList, tail, assumption, ?_⟩236      rw head237      simp [append]238    . obtain ⟨front, frontList, back, backList, equal⟩ := ih with rest239      have subset := listSupport.subset at A, tail with *240      have aA := subset with a, rest241      have frontCons : List(A, b :: front) by typecheck242      have backCons : List(A, a :: back) by typecheck243      refine ⟨b :: front, frontCons, back, backList, ?_⟩244      rw [append.cons, ← equal]245      rfl246247-- Removing the head of a permuted list from the other side.248theorem ListPermutation.cons_split (A a : Set) (xs ys : List(A))249  requires element : a ∈ A250  requires permutation : ListPermutation(A, a :: xs, ys)251  shows ∃ front, List(A, front) ∧ ∃ back, List(A, back) ∧252    ys = append(a :: back, front) ∧ ListPermutation(A, xs, append(back, front))253proof254  have headIn := listSupport.mem_cons_self at A, a, xs with element255  have member := ListPermutation.mem_support with permutation, headIn256  obtain ⟨front, frontList, back, backList, equal⟩ := listSupport.split with member257  refine ⟨front, frontList, back, backList, equal, ?_⟩258  unfold ListPermutation259  intro x260  have count := permutation with x261  have backCons : List(A, a :: back) by typecheck262  have mark := indicator.natural at {x}, a263  have xsNat := listCount.natural at A, x, xs with *264  have frontNat := listCount.natural at A, x, front with *265  have backNat := listCount.natural at A, x, back with *266  rw [equal, listCount.cons, listCount.append, listCount.cons] at count267  rw listCount.append268  have shuffled : listCount{A}(x, front) + (indicator({x}, a) + listCount{A}(x, back)) =269    indicator({x}, a) + (listCount{A}(x, front) + listCount{A}(x, back))270    exact add.swap at indicator({x}, a), listCount{A}(x, back), listCount{A}(x, front) with *271  rw shuffled at count272  exact add.left_cancel with count273274theorem ListPermutation.length (A : Set) (xs ys : List(A))275  requires permutation : ListPermutation(A, xs, ys)276  shows length{A}(xs) = length{A}(ys)277proof278  induction xs generalizing ys279  | List.nil =>280    intros ys ysList permutation281    have back := ListPermutation.symmetric with permutation282    have empty := ListPermutation.nil with back283    rw empty284    rfl285  | List.cons(a, tail) using ih =>286    intros ys ysList permutation287    have element : a ∈ A by assumption288    obtain ⟨front, frontList, back, backList, equal, rest⟩ :=289      ListPermutation.cons_split with element, permutation290    have appended := append.closed at A, front, back with *291    have inner := ih with append(back, front), appended, rest292    have backCons : List(A, a :: back) by typecheck293    rw [equal, length.cons, inner, length.append, length.append, length.cons]294    have shift : succ(length{A}(front) + length{A}(back)) = length{A}(front) + succ(length{A}(back))295      rw add.succ_right296      rfl297    exact shift298299theorem ListPermutation.singleton (A a : Set) (xs : List(A))300  requires element : a ∈ A301  requires permutation : ListPermutation(A, a :: [], xs)302  shows xs = a :: []303proof304  obtain ⟨front, frontList, back, backList, equal, rest⟩ :=305    ListPermutation.cons_split with element, permutation306  have appended := append.closed at A, front, back with *307  have back2 := ListPermutation.symmetric with rest308  have empty := ListPermutation.nil with back2309  have both := append.eq_nil with empty310  obtain ⟨frontNil, backNil⟩ := both311  rw [equal, frontNil, backNil]312  simp [append]313314theorem ListPermutation.replicate (A x : Set) (xs : List(A)) (n : Nat)315  requires element : x ∈ A316  requires permutation : ListPermutation(A, xs, listReplicate(n, x))317  shows xs = listReplicate(n, x)318proof319  have list := listReplicate.closed at A, x, n with element320  have support := ListPermutation.support with permutation321  have lengths := ListPermutation.length with permutation322  have covered := listReplicate.support_subset at A, x, n with element323  rw ← support at covered324  have constant := List.constant_of_support with element, covered325  rw [listReplicate.length] at lengths326  rw lengths at constant327  exact constant328329theorem ListPermutation.length_filter (A S : Set) (xs ys : List(A))330  requires permutation : ListPermutation(A, xs, ys)331  shows length{A}(listFilter{A}(S, xs)) = length{A}(listFilter{A}(S, ys))332proof333  have filtered := ListPermutation.filter at A, S, xs, ys with permutation334  have leftList := listFilter.closed at A, S, xs with *335  have rightList := listFilter.closed at A, S, ys with *336  exact ListPermutation.length with filtered337