Grace/Cumulus/List/Prefix.g17

Open in Workbench Download source

Imports

Index

Declarations

Source

1-- Prefixes and suffixes as relations between lists: order laws, the2-- characterizations by take and drop, and what they preserve3-- 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.Prefix9import Index1011-- xs is an initial segment of ys.12predicate ListPrefix (A xs ys : Set) := ∃ zs, List(A, zs) ∧ ys = append(zs, xs)1314-- xs is a final segment of ys.15predicate ListSuffix (A xs ys : Set) := ∃ zs, List(A, zs) ∧ ys = append(xs, zs)1617theorem ListPrefix.reflexive (A : Set) (xs : List(A))18  shows ListPrefix(A, xs, xs)19proof20  have nilList : List(A, []) by typecheck21  refine ⟨[], nilList, ?_⟩22  rw append.right_unit23  rfl2425theorem ListPrefix.nil (A : Set) (ys : List(A))26  shows ListPrefix(A, [], ys)27proof28  refine ⟨ys, assumption, ?_⟩29  simp [append]3031theorem ListPrefix.append (A : Set) (xs zs : List(A))32  shows ListPrefix(A, xs, append(zs, xs))33proof34  refine ⟨zs, assumption, rfl⟩3536theorem ListPrefix.transitive (A : Set) (xs ys zs : List(A))37  requires first : ListPrefix(A, xs, ys)38  requires second : ListPrefix(A, ys, zs)39  shows ListPrefix(A, xs, zs)40proof41  obtain ⟨us, usList, equalYs⟩ := first42  obtain ⟨vs, vsList, equalZs⟩ := second43  have appended : List(A, append(vs, us)) by typecheck44  refine ⟨append(vs, us), appended, ?_⟩45  rw [equalZs, equalYs, append.associative]46  rfl4748theorem ListPrefix.length (A : Set) (xs ys : List(A))49  requires prefix : ListPrefix(A, xs, ys)50  shows length{A}(xs) ≤ length{A}(ys)51proof52  obtain ⟨zs, zsList, equal⟩ := prefix53  rw equal54  exact append.length_left_le at A, xs, zs with *5556theorem ListPrefix.eq_take (A : Set) (xs ys : List(A))57  requires prefix : ListPrefix(A, xs, ys)58  shows xs = listTake{A}(length{A}(xs), ys)59proof60  obtain ⟨zs, zsList, equal⟩ := prefix61  rw [equal, listTake.append_self]62  rfl6364theorem ListPrefix.take (A : Set) (ys : List(A)) (n : Nat)65  shows ListPrefix(A, listTake{A}(n, ys), ys)66proof67  have dropped := listDrop.closed at A, ys, n with *68  refine ⟨listDrop{A}(n, ys), dropped, ?_⟩69  symm70  exact listTake.append_drop at A, ys, n with *7172theorem ListPrefix.iff_take (A : Set) (xs ys : List(A))73  shows ListPrefix(A, xs, ys) ↔ xs = listTake{A}(length{A}(xs), ys)74proof75  constructor76  . intro prefix77    exact ListPrefix.eq_take with prefix78  . intro equal79    have taken := ListPrefix.take at A, ys, length{A}(xs) with *80    rwa ← equal at taken8182theorem ListPrefix.antisymmetric (A : Set) (xs ys : List(A))83  requires first : ListPrefix(A, xs, ys)84  requires second : ListPrefix(A, ys, xs)85  shows xs = ys86proof87  have forward := ListPrefix.length with first88  have backward := ListPrefix.length with second89  have same := LessEqual.antisymmetric with forward, backward90  have taken := ListPrefix.eq_take with first91  rw [taken, same, listTake.self]92  rfl9394theorem ListPrefix.of_eq_length (A : Set) (xs ys : List(A))95  requires prefix : ListPrefix(A, xs, ys)96  requires same : length{A}(xs) = length{A}(ys)97  shows xs = ys98proof99  have taken := ListPrefix.eq_take with prefix100  rw [taken, same, listTake.self]101  rfl102103theorem ListPrefix.cons (A a : Set) (xs ys : List(A))104  requires element : a ∈ A105  requires prefix : ListPrefix(A, xs, ys)106  shows ListPrefix(A, a :: xs, a :: ys)107proof108  obtain ⟨zs, zsList, equal⟩ := prefix109  refine ⟨zs, zsList, ?_⟩110  rw [equal, append.cons]111  rfl112113theorem ListPrefix.cons_cancel (A a : Set) (xs ys : List(A))114  requires element : a ∈ A115  requires prefix : ListPrefix(A, a :: xs, a :: ys)116  shows ListPrefix(A, xs, ys)117proof118  obtain ⟨zs, zsList, equal⟩ := prefix119  refine ⟨zs, zsList, ?_⟩120  rw append.cons at equal121  have appended : List(A, append(zs, xs)) by typecheck122  exact List.cons_tail with equal123124theorem ListPrefix.coefficient (A z : Set) (xs ys : List(A)) (n : Nat)125  requires prefix : ListPrefix(A, xs, ys)126  requires bound : n < length{A}(xs)127  shows listCoefficient{A}(z, xs, n) = listCoefficient{A}(z, ys, n)128proof129  obtain ⟨zs, zsList, equal⟩ := prefix130  rw equal131  symm132  exact listCoefficient.append_left with bound133134theorem ListPrefix.support_subset (A : Set) (xs ys : List(A))135  requires prefix : ListPrefix(A, xs, ys)136  shows listSupport{A}(xs) ⊆ listSupport{A}(ys)137proof138  obtain ⟨zs, zsList, equal⟩ := prefix139  rw equal140  intros y hy141  exact listSupport.mem_append_left with hy142143theorem ListPrefix.count_le (A x : Set) (xs ys : List(A))144  requires prefix : ListPrefix(A, xs, ys)145  shows listCount{A}(x, xs) ≤ listCount{A}(x, ys)146proof147  obtain ⟨zs, zsList, equal⟩ := prefix148  have xsNat := listCount.natural at A, x, xs with *149  have zsNat := listCount.natural at A, x, zs with *150  rw [equal, listCount.append]151  arith152153theorem ListPrefix.of_cons (A a : Set) (xs ys : List(A))154  requires element : a ∈ A155  requires prefix : ListPrefix(A, a :: xs, ys)156  shows ∃ tail, List(A, tail) ∧ ys = a :: tail ∧ ListPrefix(A, xs, tail)157proof158  obtain ⟨zs, zsList, equal⟩ := prefix159  have appended : List(A, append(zs, xs)) by typecheck160  refine ⟨append(zs, xs), appended, ?_, ?_⟩161  . rw [equal, append.cons]162    rfl163  . exact ⟨zs, zsList, rfl⟩164165theorem ListPrefix.map (A B f : Set) (xs ys : List(A))166  requires function : f : A → B167  requires prefix : ListPrefix(A, xs, ys)168  shows ListPrefix(B, listMap{A}(f, xs), listMap{A}(f, ys))169proof170  obtain ⟨zs, zsList, equal⟩ := prefix171  have mapped : List(B, listMap{A}(f, zs)) by exact listMap.closed with function172  refine ⟨listMap{A}(f, zs), mapped, ?_⟩173  rw equal174  exact listMap.append with function175176-- Suffixes.177theorem ListSuffix.reflexive (A : Set) (xs : List(A))178  shows ListSuffix(A, xs, xs)179proof180  have nilList : List(A, []) by typecheck181  refine ⟨[], nilList, ?_⟩182  rw append.nil183  rfl184185theorem ListSuffix.nil (A : Set) (ys : List(A))186  shows ListSuffix(A, [], ys)187proof188  refine ⟨ys, assumption, ?_⟩189  rw append.right_unit190  rfl191192theorem ListSuffix.append (A : Set) (xs zs : List(A))193  shows ListSuffix(A, xs, append(xs, zs))194proof195  refine ⟨zs, assumption, rfl⟩196197theorem ListSuffix.cons (A a : Set) (xs ys : List(A))198  requires element : a ∈ A199  requires suffix : ListSuffix(A, xs, ys)200  shows ListSuffix(A, xs, a :: ys)201proof202  obtain ⟨zs, zsList, equal⟩ := suffix203  have consList : List(A, a :: zs) by typecheck204  refine ⟨a :: zs, consList, ?_⟩205  rw [equal, append.cons]206  rfl207208theorem ListSuffix.tail (A a : Set) (xs : List(A))209  requires element : a ∈ A210  shows ListSuffix(A, xs, a :: xs)211proof212  have reflexive := ListSuffix.reflexive at A, xs with *213  exact ListSuffix.cons with element, reflexive214215theorem ListSuffix.transitive (A : Set) (xs ys zs : List(A))216  requires first : ListSuffix(A, xs, ys)217  requires second : ListSuffix(A, ys, zs)218  shows ListSuffix(A, xs, zs)219proof220  obtain ⟨us, usList, equalYs⟩ := first221  obtain ⟨vs, vsList, equalZs⟩ := second222  have appended : List(A, append(us, vs)) by typecheck223  refine ⟨append(us, vs), appended, ?_⟩224  rw [equalZs, equalYs, ← append.associative]225  rfl226227theorem ListSuffix.length (A : Set) (xs ys : List(A))228  requires suffix : ListSuffix(A, xs, ys)229  shows length{A}(xs) ≤ length{A}(ys)230proof231  obtain ⟨zs, zsList, equal⟩ := suffix232  rw equal233  exact append.length_right_le at A, zs, xs with *234235theorem ListSuffix.drop (A : Set) (ys : List(A)) (n : Nat)236  shows ListSuffix(A, listDrop{A}(n, ys), ys)237proof238  have taken := listTake.closed at A, ys, n with *239  refine ⟨listTake{A}(n, ys), taken, ?_⟩240  symm241  exact listTake.append_drop at A, ys, n with *242243theorem ListSuffix.eq_drop (A : Set) (xs ys : List(A))244  requires suffix : ListSuffix(A, xs, ys)245  shows ∃ n, Nat(n) ∧ xs = listDrop{A}(n, ys)246proof247  obtain ⟨zs, zsList, equal⟩ := suffix248  have zsNat : Nat(length{A}(zs)) by typecheck249  refine ⟨length{A}(zs), zsNat, ?_⟩250  rw [equal, listDrop.append_self]251  rfl252253theorem ListSuffix.antisymmetric (A : Set) (xs ys : List(A))254  requires first : ListSuffix(A, xs, ys)255  requires second : ListSuffix(A, ys, xs)256  shows xs = ys257proof258  obtain ⟨zs, zsList, equal⟩ := first259  have forward := ListSuffix.length with first260  have backward := ListSuffix.length with second261  have same := LessEqual.antisymmetric with forward, backward262  have lengths : length{A}(append(xs, zs)) = length{A}(xs)263    rw ← equal264    symm265    exact same266  rw length.append at lengths267  have padded : length{A}(zs) + length{A}(xs) = 0 + length{A}(xs)268    rw add.left_unit269    exact lengths270  have zero := add.right_cancel with padded271  have empty := length.eq_zero with zero272  rw [equal, empty, append.nil]273  rfl274275theorem ListSuffix.of_eq_length (A : Set) (xs ys : List(A))276  requires suffix : ListSuffix(A, xs, ys)277  requires same : length{A}(xs) = length{A}(ys)278  shows xs = ys279proof280  obtain ⟨zs, zsList, equal⟩ := suffix281  have lengths : length{A}(append(xs, zs)) = length{A}(xs)282    rw ← equal283    symm284    exact same285  rw length.append at lengths286  have padded : length{A}(zs) + length{A}(xs) = 0 + length{A}(xs)287    rw add.left_unit288    exact lengths289  have zero := add.right_cancel with padded290  have empty := length.eq_zero with zero291  rw [equal, empty, append.nil]292  rfl293294theorem ListSuffix.support_subset (A : Set) (xs ys : List(A))295  requires suffix : ListSuffix(A, xs, ys)296  shows listSupport{A}(xs) ⊆ listSupport{A}(ys)297proof298  obtain ⟨zs, zsList, equal⟩ := suffix299  rw equal300  intros y hy301  exact listSupport.mem_append_right with hy302303theorem ListSuffix.count_le (A x : Set) (xs ys : List(A))304  requires suffix : ListSuffix(A, xs, ys)305  shows listCount{A}(x, xs) ≤ listCount{A}(x, ys)306proof307  obtain ⟨zs, zsList, equal⟩ := suffix308  have xsNat := listCount.natural at A, x, xs with *309  have zsNat := listCount.natural at A, x, zs with *310  rw [equal, listCount.append]311  arith312313-- Reversal exchanges prefixes and suffixes.314theorem ListPrefix.reverse (A : Set) (xs ys : List(A))315  requires prefix : ListPrefix(A, xs, ys)316  shows ListSuffix(A, reverse(xs), reverse(ys))317proof318  obtain ⟨zs, zsList, equal⟩ := prefix319  have reversed : List(A, reverse(zs)) by typecheck320  refine ⟨reverse(zs), reversed, ?_⟩321  rw [equal, reverse.append]322  rfl323324theorem ListSuffix.reverse (A : Set) (xs ys : List(A))325  requires suffix : ListSuffix(A, xs, ys)326  shows ListPrefix(A, reverse(xs), reverse(ys))327proof328  obtain ⟨zs, zsList, equal⟩ := suffix329  have reversed : List(A, reverse(zs)) by typecheck330  refine ⟨reverse(zs), reversed, ?_⟩331  rw [equal, reverse.append]332  rfl333334theorem ListPrefix.iff_reverse (A : Set) (xs ys : List(A))335  shows ListPrefix(A, xs, ys) ↔ ListSuffix(A, reverse(xs), reverse(ys))336proof337  constructor338  . intro prefix339    exact ListPrefix.reverse with prefix340  . intro suffix341    have reversedXs : List(A, reverse(xs)) by typecheck342    have reversedYs : List(A, reverse(ys)) by typecheck343    have back := ListSuffix.reverse at A, reverse(xs), reverse(ys) with suffix344    rw [reverse.involutive, reverse.involutive] at back345    exact back346347theorem ListSuffix.map (A B f : Set) (xs ys : List(A))348  requires function : f : A → B349  requires suffix : ListSuffix(A, xs, ys)350  shows ListSuffix(B, listMap{A}(f, xs), listMap{A}(f, ys))351proof352  obtain ⟨zs, zsList, equal⟩ := suffix353  have mapped : List(B, listMap{A}(f, zs)) by exact listMap.closed with function354  refine ⟨listMap{A}(f, zs), mapped, ?_⟩355  rw equal356  exact listMap.append with function357358theorem ListPrefix.filter (A S : Set) (xs ys : List(A))359  requires prefix : ListPrefix(A, xs, ys)360  shows ListPrefix(A, listFilter{A}(S, xs), listFilter{A}(S, ys))361proof362  obtain ⟨zs, zsList, equal⟩ := prefix363  have filtered := listFilter.closed at A, S, zs with *364  refine ⟨listFilter{A}(S, zs), filtered, ?_⟩365  rw equal366  exact listFilter.append at A, S, xs, zs with *367368theorem ListSuffix.filter (A S : Set) (xs ys : List(A))369  requires suffix : ListSuffix(A, xs, ys)370  shows ListSuffix(A, listFilter{A}(S, xs), listFilter{A}(S, ys))371proof372  obtain ⟨zs, zsList, equal⟩ := suffix373  have filtered := listFilter.closed at A, S, zs with *374  refine ⟨listFilter{A}(S, zs), filtered, ?_⟩375  rw equal376  exact listFilter.append at A, S, zs, xs with *377