Grace/Cumulus/List/TakeDrop.g17

Open in Workbench Download source

Imports

Replicate

Declarations

Source

1-- Prefixes and suffixes of a list: take and drop, their lengths, how they2-- recombine, and how they read through concatenation, mapping, and indexing3-- 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.TakeDrop9import Replicate1011def listTake {A : Set} (n : Nat) (xs : List(A)) → Set12  | n, List.nil => []13  | n, List.cons(a, tail) =>14    boolChoice(isZero(n), [], a :: listTake(predecessor(n), tail))15  descends xs1617def listDrop {A : Set} (n : Nat) (xs : List(A)) → Set18  | n, List.nil => []19  | n, List.cons(a, tail) =>20    boolChoice(isZero(n), a :: tail, listDrop(predecessor(n), tail))21  descends xs2223theorem listTake.nil (A : Set) (n : Nat)24  shows listTake{A}(n, []) = []25proof26  simp [listTake]2728theorem listTake.zero (A : Set) (xs : List(A))29  shows listTake{A}(0, xs) = []30proof31  induction xs32  | List.nil => simp [listTake]33  | List.cons(a, tail) using ih => simp [listTake, isZero, boolChoice]3435theorem listTake.succ_cons (A a : Set) (xs : List(A)) (n : Nat)36  requires element : a ∈ A37  shows listTake{A}(succ(n), a :: xs) = a :: listTake{A}(n, xs)38proof39  simp [listTake, isZero, predecessor, boolChoice]4041theorem listDrop.nil (A : Set) (n : Nat)42  shows listDrop{A}(n, []) = []43proof44  simp [listDrop]4546theorem listDrop.zero (A : Set) (xs : List(A))47  shows listDrop{A}(0, xs) = xs48proof49  induction xs50  | List.nil => simp [listDrop]51  | List.cons(a, tail) using ih => simp [listDrop, isZero, boolChoice]5253theorem listDrop.succ_cons (A a : Set) (xs : List(A)) (n : Nat)54  requires element : a ∈ A55  shows listDrop{A}(succ(n), a :: xs) = listDrop{A}(n, xs)56proof57  simp [listDrop, isZero, predecessor, boolChoice]5859theorem listTake.closed (A : Set) (xs : List(A)) (n : Nat)60  shows List(A, listTake{A}(n, xs))61proof62  induction xs generalizing n63  | List.nil =>64    intros n nNat65    rw listTake.nil66    typecheck67  | List.cons(a, tail) using ih =>68    intros n nNat69    have element : a ∈ A by assumption70    have whole : List(A, a :: tail) by typecheck71    have shape := natural.zero_or_successor with *72    cases shape with zero | successor73    . rw [zero, listTake.zero]74      typecheck75    . obtain ⟨k, kNat, equal⟩ := successor76      have inner := ih with k, kNat77      rw [equal, listTake.succ_cons]78      typecheck7980theorem listDrop.closed (A : Set) (xs : List(A)) (n : Nat)81  shows List(A, listDrop{A}(n, xs))82proof83  induction xs generalizing n84  | List.nil =>85    intros n nNat86    rw listDrop.nil87    typecheck88  | List.cons(a, tail) using ih =>89    intros n nNat90    have element : a ∈ A by assumption91    have whole : List(A, a :: tail) by typecheck92    have shape := natural.zero_or_successor with *93    cases shape with zero | successor94    . rw [zero, listDrop.zero]95      typecheck96    . obtain ⟨k, kNat, equal⟩ := successor97      have inner := ih with k, kNat98      rw [equal, listDrop.succ_cons]99      exact inner100101-- The prefix followed by the suffix is the list.102theorem listTake.append_drop (A : Set) (xs : List(A)) (n : Nat)103  shows append(listDrop{A}(n, xs), listTake{A}(n, xs)) = xs104proof105  induction xs generalizing n106  | List.nil =>107    intros n nNat108    rw [listTake.nil, listDrop.nil]109    simp [append]110  | List.cons(a, tail) using ih =>111    intros n nNat112    have element : a ∈ A by assumption113    have whole : List(A, a :: tail) by typecheck114    have shape := natural.zero_or_successor with *115    cases shape with zero | successor116    . rw [zero, listTake.zero, listDrop.zero]117      simp [append]118    . obtain ⟨k, kNat, equal⟩ := successor119      have inner := ih with k, kNat120      have taken := listTake.closed at A, tail, k with *121      have dropped := listDrop.closed at A, tail, k with *122      rw [equal, listTake.succ_cons, listDrop.succ_cons, append.cons, inner]123      rfl124125theorem listTake.length_le_count (A : Set) (xs : List(A)) (n : Nat)126  shows length{A}(listTake{A}(n, xs)) ≤ n127proof128  induction xs generalizing n129  | List.nil =>130    intros n nNat131    rw [listTake.nil, length.nil]132    arith133  | List.cons(a, tail) using ih =>134    intros n nNat135    have element : a ∈ A by assumption136    have whole : List(A, a :: tail) by typecheck137    have shape := natural.zero_or_successor with *138    cases shape with zero | successor139    . rw [zero, listTake.zero, length.nil]140      arith141    . obtain ⟨k, kNat, equal⟩ := successor142      have inner := ih with k, kNat143      have taken := listTake.closed at A, tail, k with *144      rw [equal, listTake.succ_cons, length.cons]145      arith146147theorem listTake.length_le (A : Set) (xs : List(A)) (n : Nat)148  shows length{A}(listTake{A}(n, xs)) ≤ length{A}(xs)149proof150  have split := listTake.append_drop at A, xs, n with *151  have taken := listTake.closed at A, xs, n with *152  have dropped := listDrop.closed at A, xs, n with *153  have bound := append.length_left_le at A, listTake{A}(n, xs), listDrop{A}(n, xs) with *154  rwa split at bound155156theorem listDrop.length_le (A : Set) (xs : List(A)) (n : Nat)157  shows length{A}(listDrop{A}(n, xs)) ≤ length{A}(xs)158proof159  have split := listTake.append_drop at A, xs, n with *160  have taken := listTake.closed at A, xs, n with *161  have dropped := listDrop.closed at A, xs, n with *162  have bound := append.length_right_le at A, listTake{A}(n, xs), listDrop{A}(n, xs) with *163  rwa split at bound164165theorem listTake.length (A : Set) (xs : List(A)) (n : Nat)166  requires bound : n ≤ length{A}(xs)167  shows length{A}(listTake{A}(n, xs)) = n168proof169  induction xs generalizing n170  | List.nil =>171    intros n nNat bound172    rw length.nil at bound173    have shape := natural.zero_or_successor with *174    cases shape with zero | successor175    . rw [zero, listTake.nil, length.nil]176      rfl177    . obtain ⟨k, kNat, equal⟩ := successor178      rw equal at bound179      exfalso180      arith181  | List.cons(a, tail) using ih =>182    intros n nNat bound183    have element : a ∈ A by assumption184    have whole : List(A, a :: tail) by typecheck185    rw length.cons at bound186    have shape := natural.zero_or_successor with *187    cases shape with zero | successor188    . rw [zero, listTake.zero, length.nil]189      rfl190    . obtain ⟨k, kNat, equal⟩ := successor191      rw equal at bound192      have smaller : k ≤ length{A}(tail) by arith193      have inner := ih with k, kNat, smaller194      have taken := listTake.closed at A, tail, k with *195      rw [equal, listTake.succ_cons, length.cons, inner]196      rfl197198theorem listTake.all (A : Set) (xs : List(A)) (n : Nat)199  requires bound : length{A}(xs) ≤ n200  shows listTake{A}(n, xs) = xs201proof202  induction xs generalizing n203  | List.nil =>204    intros n nNat bound205    exact listTake.nil at A, n206  | List.cons(a, tail) using ih =>207    intros n nNat bound208    have element : a ∈ A by assumption209    have whole : List(A, a :: tail) by typecheck210    rw length.cons at bound211    have shape := natural.zero_or_successor with *212    cases shape with zero | successor213    . rw zero at bound214      exfalso215      arith216    . obtain ⟨k, kNat, equal⟩ := successor217      rw equal at bound218      have smaller : length{A}(tail) ≤ k by arith219      have inner := ih with k, kNat, smaller220      rw [equal, listTake.succ_cons, inner]221      rfl222223theorem listTake.self (A : Set) (xs : List(A))224  shows listTake{A}(length{A}(xs), xs) = xs225proof226  have reflexive := LessEqual.reflexive at length{A}(xs) with *227  exact listTake.all with reflexive228229theorem listDrop.all (A : Set) (xs : List(A)) (n : Nat)230  requires bound : length{A}(xs) ≤ n231  shows listDrop{A}(n, xs) = []232proof233  induction xs generalizing n234  | List.nil =>235    intros n nNat bound236    exact listDrop.nil at A, n237  | List.cons(a, tail) using ih =>238    intros n nNat bound239    have element : a ∈ A by assumption240    have whole : List(A, a :: tail) by typecheck241    rw length.cons at bound242    have shape := natural.zero_or_successor with *243    cases shape with zero | successor244    . rw zero at bound245      exfalso246      arith247    . obtain ⟨k, kNat, equal⟩ := successor248      rw equal at bound249      have smaller : length{A}(tail) ≤ k by arith250      have inner := ih with k, kNat, smaller251      rw [equal, listDrop.succ_cons, inner]252      rfl253254theorem listDrop.self (A : Set) (xs : List(A))255  shows listDrop{A}(length{A}(xs), xs) = []256proof257  have reflexive := LessEqual.reflexive at length{A}(xs) with *258  exact listDrop.all with reflexive259260theorem listDrop.length (A : Set) (xs : List(A)) (n : Nat)261  requires bound : n ≤ length{A}(xs)262  shows length{A}(listDrop{A}(n, xs)) + n = length{A}(xs)263proof264  have split := listTake.append_drop at A, xs, n with *265  have taken := listTake.closed at A, xs, n with *266  have dropped := listDrop.closed at A, xs, n with *267  have lengths := length.append at A, listDrop{A}(n, xs), listTake{A}(n, xs) with *268  rw [split, listTake.length] at lengths269  symm at lengths270  rwa add.commutative at lengths271272theorem listTake.eq_nil (A : Set) (xs : List(A)) (n : Nat)273  requires empty : listTake{A}(n, xs) = []274  shows n = 0 ∨ xs = []275proof276  have shape := natural.zero_or_successor with *277  cases shape with zero | successor278  . left279    exact zero280  . right281    obtain ⟨k, kNat, equal⟩ := successor282    have listShape := List.cases with *283    cases listShape with nil | cons284    . exact nil285    . obtain ⟨a, element, tail, tailList, equal2⟩ := cons286      rw [equal, equal2, listTake.succ_cons] at empty287      have taken := listTake.closed at A, tail, k with *288      exfalso289      have distinct := List.cons_ne_nil at A, a, listTake{A}(k, tail) with element290      exact distinct with empty291292theorem listTake.take (A : Set) (xs : List(A)) (m n : Nat)293  requires bound : m ≤ n294  shows listTake{A}(m, listTake{A}(n, xs)) = listTake{A}(m, xs)295proof296  induction xs generalizing m n297  | List.nil =>298    intros m n mNat nNat bound299    rw [listTake.nil, listTake.nil]300    rfl301  | List.cons(a, tail) using ih =>302    intros m n mNat nNat bound303    have element : a ∈ A by assumption304    have whole : List(A, a :: tail) by typecheck305    have outer := listTake.closed at A, a :: tail, n with *306    have shapeM := natural.zero_or_successor at m with mNat307    cases shapeM with zeroM | successorM308    . rw [zeroM, listTake.zero, listTake.zero]309      rfl310    . obtain ⟨j, jNat, equalM⟩ := successorM311      have shapeN := natural.zero_or_successor at n with nNat312      cases shapeN with zeroN | successorN313      . rw [equalM, zeroN] at bound314        exfalso315        arith316      . obtain ⟨k, kNat, equalN⟩ := successorN317        rw [equalM, equalN] at bound318        have smaller : j ≤ k by arith319        have inner := ih with j, k, jNat, kNat, smaller320        have taken := listTake.closed at A, tail, k with *321        rw [equalM, equalN, listTake.succ_cons, listTake.succ_cons, inner]322        rw listTake.succ_cons323        rfl324325theorem listTake.idempotent (A : Set) (xs : List(A)) (n : Nat)326  shows listTake{A}(n, listTake{A}(n, xs)) = listTake{A}(n, xs)327proof328  have reflexive := LessEqual.reflexive at n with *329  exact listTake.take with reflexive330331theorem listDrop.drop (A : Set) (xs : List(A)) (m n : Nat)332  shows listDrop{A}(m, listDrop{A}(n, xs)) = listDrop{A}(n + m, xs)333proof334  induction xs generalizing n335  | List.nil =>336    intros n nNat337    rw [listDrop.nil, listDrop.nil, listDrop.nil]338    rfl339  | List.cons(a, tail) using ih =>340    intros n nNat341    have element : a ∈ A by assumption342    have whole : List(A, a :: tail) by typecheck343    have shape := natural.zero_or_successor at n with nNat344    cases shape with zero | successor345    . rw [zero, listDrop.zero, add.left_unit]346      rfl347    . obtain ⟨k, kNat, equal⟩ := successor348      have inner := ih with k, kNat349      have shift : succ(k) + m = succ(k + m) by simp [add, add.succ_right]350      rw [equal, listDrop.succ_cons, inner, shift, listDrop.succ_cons]351      rfl352353theorem listDrop.succ (A : Set) (xs : List(A)) (n : Nat)354  shows listDrop{A}(succ(n), xs) = listTail{A}(listDrop{A}(n, xs))355proof356  induction xs generalizing n357  | List.nil =>358    intros n nNat359    rw [listDrop.nil, listDrop.nil, listTail.nil]360    rfl361  | List.cons(a, tail) using ih =>362    intros n nNat363    have element : a ∈ A by assumption364    have whole : List(A, a :: tail) by typecheck365    have shape := natural.zero_or_successor at n with nNat366    cases shape with zero | successor367    . rw [zero, listDrop.zero, listDrop.succ_cons, listDrop.zero, listTail.cons]368      rfl369    . obtain ⟨k, kNat, equal⟩ := successor370      have inner := ih with k, kNat371      rw [equal, listDrop.succ_cons, listDrop.succ_cons, inner]372      rfl373374theorem listDrop.one (A : Set) (xs : List(A))375  shows listDrop{A}(1, xs) = listTail{A}(xs)376proof377  have step := listDrop.succ at A, xs, 0 with *378  rw [listDrop.zero] at step379  exact step380381theorem listDrop.tail (A : Set) (xs : List(A)) (n : Nat)382  shows listDrop{A}(succ(n), xs) = listDrop{A}(n, listTail{A}(xs))383proof384  have shape := List.cases with *385  cases shape with nil | cons386  . rw [nil, listTail.nil, listDrop.nil, listDrop.nil]387    rfl388  . obtain ⟨a, element, tail, tailList, equal⟩ := cons389    rw [equal, listTail.cons, listDrop.succ_cons]390    rfl391392-- Take and drop across a concatenation.393theorem listTake.append_left (A : Set) (xs ys : List(A)) (n : Nat)394  requires bound : n ≤ length{A}(xs)395  shows listTake{A}(n, append(ys, xs)) = listTake{A}(n, xs)396proof397  induction xs generalizing n398  | List.nil =>399    intros n nNat bound400    rw length.nil at bound401    have ysList : List(A, ys) by typecheck402    rw append.nil403    have shape := natural.zero_or_successor with *404    cases shape with zero | successor405    . rw [zero, listTake.zero, listTake.nil]406      rfl407    . obtain ⟨k, kNat, equal⟩ := successor408      rw equal at bound409      exfalso410      arith411  | List.cons(a, tail) using ih =>412    intros n nNat bound413    have element : a ∈ A by assumption414    have whole : List(A, a :: tail) by typecheck415    rw length.cons at bound416    have appended := append.closed at A, tail, ys with *417    have appendedWhole : List(A, append(ys, a :: tail)) by typecheck418    have shape := natural.zero_or_successor with *419    cases shape with zero | successor420    . rw [zero, listTake.zero, listTake.zero]421      rfl422    . obtain ⟨k, kNat, equal⟩ := successor423      rw equal at bound424      have smaller : k ≤ length{A}(tail) by arith425      have inner := ih with k, kNat, smaller426      rw [equal, append.cons, listTake.succ_cons, listTake.succ_cons, inner]427      rfl428429theorem listDrop.append_left (A : Set) (xs ys : List(A)) (n : Nat)430  requires bound : n ≤ length{A}(xs)431  shows listDrop{A}(n, append(ys, xs)) = append(ys, listDrop{A}(n, xs))432proof433  induction xs generalizing n434  | List.nil =>435    intros n nNat bound436    rw length.nil at bound437    have ysList : List(A, ys) by typecheck438    rw append.nil439    have shape := natural.zero_or_successor with *440    cases shape with zero | successor441    . rw [zero, listDrop.zero, listDrop.nil, append.nil]442      rfl443    . obtain ⟨k, kNat, equal⟩ := successor444      rw equal at bound445      exfalso446      arith447  | List.cons(a, tail) using ih =>448    intros n nNat bound449    have element : a ∈ A by assumption450    have whole : List(A, a :: tail) by typecheck451    rw length.cons at bound452    have appended := append.closed at A, tail, ys with *453    have appendedWhole : List(A, append(ys, a :: tail)) by typecheck454    have shape := natural.zero_or_successor with *455    cases shape with zero | successor456    . rw [zero, listDrop.zero, listDrop.zero]457      rfl458    . obtain ⟨k, kNat, equal⟩ := successor459      rw equal at bound460      have smaller : k ≤ length{A}(tail) by arith461      have inner := ih with k, kNat, smaller462      rw [equal, append.cons, listDrop.succ_cons, listDrop.succ_cons, inner]463      rfl464465theorem listTake.append_right (A : Set) (xs ys : List(A)) (n : Nat)466  shows listTake{A}(length{A}(xs) + n, append(ys, xs)) =467    append(listTake{A}(n, ys), xs)468proof469  induction xs470  | List.nil =>471    have taken := listTake.closed at A, ys, n with *472    rw [length.nil, add.left_unit]473    simp [append]474  | List.cons(a, tail) using ih =>475    have element : a ∈ A by assumption476    have whole : List(A, a :: tail) by typecheck477    have appended := append.closed at A, tail, ys with *478    have taken := listTake.closed at A, ys, n with *479    have shift : succ(length{A}(tail)) + n = succ(length{A}(tail) + n)480      simp [add, add.succ_right]481    rw [length.cons, shift, append.cons, listTake.succ_cons, ih, append.cons]482    rfl483484theorem listDrop.append_right (A : Set) (xs ys : List(A)) (n : Nat)485  shows listDrop{A}(length{A}(xs) + n, append(ys, xs)) = listDrop{A}(n, ys)486proof487  induction xs488  | List.nil =>489    rw [length.nil, add.left_unit]490    simp [append]491  | List.cons(a, tail) using ih =>492    have element : a ∈ A by assumption493    have whole : List(A, a :: tail) by typecheck494    have appended := append.closed at A, tail, ys with *495    have shift : succ(length{A}(tail)) + n = succ(length{A}(tail) + n)496      simp [add, add.succ_right]497    rw [length.cons, shift, append.cons, listDrop.succ_cons, ih]498    rfl499500theorem listTake.append_self (A : Set) (xs ys : List(A))501  shows listTake{A}(length{A}(xs), append(ys, xs)) = xs502proof503  have reflexive := LessEqual.reflexive at length{A}(xs) with *504  have step := listTake.append_left at A, xs, ys, length{A}(xs) with reflexive505  rw [step, listTake.self]506  rfl507508theorem listDrop.append_self (A : Set) (xs ys : List(A))509  shows listDrop{A}(length{A}(xs), append(ys, xs)) = ys510proof511  have step := listDrop.append_right at A, xs, ys, 0 with *512  rw [add.right_unit, listDrop.zero] at step513  exact step514515-- Mapping commutes with take and drop.516theorem listTake.map (A B f : Set) (xs : List(A)) (n : Nat)517  requires function : f : A → B518  shows listMap{A}(f, listTake{A}(n, xs)) = listTake{B}(n, listMap{A}(f, xs))519proof520  induction xs generalizing n521  | List.nil =>522    intros n nNat523    rw [listTake.nil, listMap.nil, listTake.nil]524    rfl525  | List.cons(a, tail) using ih =>526    intros n nNat527    have element : a ∈ A by assumption528    have whole : List(A, a :: tail) by typecheck529    have image := FunctionBetween.apply_closed with function, element530    have mapped : List(B, listMap{A}(f, tail)) by exact listMap.closed with function531    have mappedWhole : List(B, f(a) :: listMap{A}(f, tail)) by typecheck532    have shape := natural.zero_or_successor with *533    cases shape with zero | successor534    . rw [zero, listTake.zero, listMap.nil, listMap.cons, listTake.zero]535      rfl536    . obtain ⟨k, kNat, equal⟩ := successor537      have inner := ih with k, kNat538      have taken := listTake.closed at A, tail, k with *539      rw [equal, listTake.succ_cons, listMap.cons, inner, listMap.cons]540      rw listTake.succ_cons541      rfl542543theorem listDrop.map (A B f : Set) (xs : List(A)) (n : Nat)544  requires function : f : A → B545  shows listMap{A}(f, listDrop{A}(n, xs)) = listDrop{B}(n, listMap{A}(f, xs))546proof547  induction xs generalizing n548  | List.nil =>549    intros n nNat550    rw [listDrop.nil, listMap.nil, listDrop.nil]551    rfl552  | List.cons(a, tail) using ih =>553    intros n nNat554    have element : a ∈ A by assumption555    have whole : List(A, a :: tail) by typecheck556    have image := FunctionBetween.apply_closed with function, element557    have mapped : List(B, listMap{A}(f, tail)) by exact listMap.closed with function558    have mappedWhole : List(B, f(a) :: listMap{A}(f, tail)) by typecheck559    have shape := natural.zero_or_successor with *560    cases shape with zero | successor561    . rw [zero, listDrop.zero, listMap.cons, listDrop.zero]562      rfl563    . obtain ⟨k, kNat, equal⟩ := successor564      have inner := ih with k, kNat565      rw [equal, listDrop.succ_cons, inner, listMap.cons, listDrop.succ_cons]566      rfl567568-- Take and drop of a constant list.569theorem listTake.replicate (A x : Set) (m k : Nat)570  requires element : x ∈ A571  shows listTake{A}(m, listReplicate(k + m, x)) = listReplicate(m, x)572proof573  induction m574  | zero =>575    have list := listReplicate.closed at A, x, k + 0 with element576    rw [listTake.zero, listReplicate.zero]577    rfl578  | succ(j) using ih =>579    have list := listReplicate.closed at A, x, k + j with element580    rw [add.succ_right, listReplicate.succ, listTake.succ_cons, ih]581    rw listReplicate.succ582    rfl583584theorem listDrop.replicate (A x : Set) (m k : Nat)585  requires element : x ∈ A586  shows listDrop{A}(m, listReplicate(k + m, x)) = listReplicate(k, x)587proof588  induction m589  | zero =>590    have list := listReplicate.closed at A, x, k with element591    rw [add.right_unit, listDrop.zero]592    rfl593  | succ(j) using ih =>594    have list := listReplicate.closed at A, x, k + j with element595    rw [add.succ_right, listReplicate.succ, listDrop.succ_cons, ih]596    rfl597598-- Supports of prefixes and suffixes.599theorem listTake.support_subset (A : Set) (xs : List(A)) (n : Nat)600  shows listSupport{A}(listTake{A}(n, xs)) ⊆ listSupport{A}(xs)601proof602  have split := listTake.append_drop at A, xs, n with *603  have taken := listTake.closed at A, xs, n with *604  have dropped := listDrop.closed at A, xs, n with *605  intros y hy606  have member := listSupport.mem_append_left at A, y, listTake{A}(n, xs), listDrop{A}(n, xs) with hy607  rwa split at member608609theorem listDrop.support_subset (A : Set) (xs : List(A)) (n : Nat)610  shows listSupport{A}(listDrop{A}(n, xs)) ⊆ listSupport{A}(xs)611proof612  have split := listTake.append_drop at A, xs, n with *613  have taken := listTake.closed at A, xs, n with *614  have dropped := listDrop.closed at A, xs, n with *615  intros y hy616  have member := listSupport.mem_append_right at A, y, listTake{A}(n, xs), listDrop{A}(n, xs) with hy617  rwa split at member618619theorem listSupport.take_union_drop (A : Set) (xs : List(A)) (n : Nat)620  shows listSupport{A}(xs) =621    listSupport{A}(listTake{A}(n, xs)) ∪ listSupport{A}(listDrop{A}(n, xs))622proof623  have split := listTake.append_drop at A, xs, n with *624  have taken := listTake.closed at A, xs, n with *625  have dropped := listDrop.closed at A, xs, n with *626  have union := listSupport.append at A, listDrop{A}(n, xs), listTake{A}(n, xs) with *627  rwa split at union628629-- Indexing into prefixes and suffixes.630theorem listTake.coefficient (A z : Set) (xs : List(A)) (n k : Nat)631  requires bound : k < n632  shows listCoefficient{A}(z, listTake{A}(n, xs), k) = listCoefficient{A}(z, xs, k)633proof634  induction xs generalizing n k635  | List.nil =>636    intros n k nNat kNat bound637    rw listTake.nil638    rfl639  | List.cons(a, tail) using ih =>640    intros n k nNat kNat bound641    have element : a ∈ A by assumption642    have whole : List(A, a :: tail) by typecheck643    have shapeN := natural.zero_or_successor at n with nNat644    cases shapeN with zeroN | successorN645    . rw zeroN at bound646      exfalso647      arith648    . obtain ⟨j, jNat, equalN⟩ := successorN649      have taken := listTake.closed at A, tail, j with *650      rw [equalN, listTake.succ_cons]651      have shapeK := natural.zero_or_successor at k with kNat652      cases shapeK with zeroK | successorK653      . rw [zeroK, listCoefficient.zero, listCoefficient.zero]654        rfl655      . obtain ⟨r, rNat, equalK⟩ := successorK656        rw [equalN, equalK] at bound657        have smaller : r < j by arith658        have inner := ih with j, r, jNat, rNat, smaller659        rw [equalK, listCoefficient.succ, listCoefficient.succ]660        exact inner661662theorem listDrop.coefficient (A z : Set) (xs : List(A)) (n k : Nat)663  shows listCoefficient{A}(z, listDrop{A}(n, xs), k) = listCoefficient{A}(z, xs, n + k)664proof665  induction xs generalizing n666  | List.nil =>667    intros n nNat668    rw [listDrop.nil, listCoefficient.nil, listCoefficient.nil]669    rfl670  | List.cons(a, tail) using ih =>671    intros n nNat672    have element : a ∈ A by assumption673    have whole : List(A, a :: tail) by typecheck674    have shape := natural.zero_or_successor at n with nNat675    cases shape with zero | successor676    . rw [zero, listDrop.zero, add.left_unit]677      rfl678    . obtain ⟨j, jNat, equal⟩ := successor679      have inner := ih with j, jNat680      have shift : succ(j) + k = succ(j + k) by simp [add, add.succ_right]681      rw [equal, listDrop.succ_cons, inner, shift, listCoefficient.succ]682      rfl683684theorem listCoefficient.head (A z : Set) (xs : List(A))685  shows listCoefficient{A}(z, xs, 0) = listHeadOr{A}(z, xs)686proof687  simp [listCoefficient]688689theorem listCoefficient.tail (A z : Set) (xs : List(A)) (n : Nat)690  shows listCoefficient{A}(z, listTail{A}(xs), n) = listCoefficient{A}(z, xs, succ(n))691proof692  simp [listCoefficient]693