Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Mathematics.Fin public import Mathlib.Order.Lattice.Nat public import Mathlib.Data.List.TakeWhile import all Mathlib.Data.List.Sort

List lemmas

I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List Ih: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:P bhPa:P aList.takeWhile (fun b => decide (P b)) (a :: b :: l).tail = (match decide (P a) with | true => a :: match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => [] | false => []).tail All goals completed! 🐙 I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List Ih: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P bList.takeWhile (fun b => decide (P b)) (a :: b :: l).tail = (match decide (P a) with | true => a :: match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => [] | false => []).tail I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List Ih: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P b(match decide (P a) with | true => [a] | false => []).tail = [] I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List Ih: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = true[a].tail = []I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List Ih: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = false[].tail = [] I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List Ih: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = true[a].tail = []I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List Ih: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P bx✝:Boolheq✝:decide (P a) = false[].tail = [] All goals completed! 🐙 I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)List.takeWhile (fun b => decide (P b)) ((a :: b :: l).eraseIdx n.succ) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx n.succ I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)List.takeWhile (fun b => decide (P b)) ((a :: b :: l).eraseIdx n.succ) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx n.succ I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)List.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:P aList.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1)I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:¬P aList.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:P aList.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:P a(match decide (P a) with | true => a :: List.takeWhile (fun b => decide (P b)) ((b :: l).eraseIdx n) | false => []) = (match decide (P a) with | true => a :: match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => [] | false => []).eraseIdx (n + 1) I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:P aList.takeWhile (fun b => decide (P b)) ((b :: l).eraseIdx n) = (match decide (P b) with | true => b :: List.takeWhile (fun b => decide (P b)) l | false => []).eraseIdx n exact takeWile_eraseIdx P (b :: l) n fun i j hij hP => I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:P ai:Fin (b :: l).lengthj:Fin (b :: l).lengthhij:i < jhP:P ((b :: l).get j)P ((b :: l).get i) simpa using h i.succ j.succ (I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:P ai:Fin (b :: l).lengthj:Fin (b :: l).lengthhij:i < jhP:P ((b :: l).get j)i.succ < j.succ All goals completed! 🐙) (I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:P ai:Fin (b :: l).lengthj:Fin (b :: l).lengthhij:i < jhP:P ((b :: l).get j)P ((a :: b :: l).get j.succ) All goals completed! 🐙) I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPa:¬P aList.takeWhile (fun b => decide (P b)) (a :: (b :: l).eraseIdx n) = (List.takeWhile (fun b => decide (P b)) (a :: b :: l)).eraseIdx (n + 1) All goals completed! 🐙I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P bhPa:P a(match decide (P a) with | true => if (List.takeWhile (fun b => decide (P b)) (b :: l)).length n then (List.dropWhile (fun b => decide (P b)) (b :: l)).eraseIdx (n - (List.takeWhile (fun b => decide (P b)) (b :: l)).length) else List.dropWhile (fun b => decide (P b)) (b :: l) | false => a :: (b :: l).eraseIdx n) = if (match decide (P a) with | true => [a] | false => []).length n + 1 then (match decide (P a) with | true => b :: l | false => a :: b :: l).eraseIdx (n + 1 - (match decide (P a) with | true => [a] | false => []).length) else match decide (P a) with | true => b :: l | false => a :: b :: l All goals completed! 🐙 I:TypeP:I Propinst✝:DecidablePred Pa:Ib:Il:List In:h: (i j : Fin (a :: b :: l).length), i < j P ((a :: b :: l).get j) P ((a :: b :: l).get i)hPb:¬P bhPa:¬P a(match decide (P a) with | true => List.dropWhile (fun b => decide (P b)) ((b :: l).eraseIdx n) | false => a :: (b :: l).eraseIdx n) = if (match decide (P a) with | true => [a] | false => []).length n + 1 then (match decide (P a) with | true => b :: l | false => a :: b :: l).eraseIdx (n + 1 - (match decide (P a) with | true => [a] | false => []).length) else match decide (P a) with | true => b :: l | false => a :: b :: l All goals completed! 🐙lemma insertionSort_length {I : Type} (le1 : I I Prop) [DecidableRel le1] (l : List I) : (List.insertionSort le1 l).length = l.length := List.length_insertionSort le1 l

The position r0 ends up in r on adding it via List.orderedInsert _ r0 r.

n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(List.takeWhile (fun b => decide ¬le1 r0 b) r).length < r.length + 1 n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ih1:(List.takeWhile (fun b => decide ¬le1 r0 b) r).length r.length(List.takeWhile (fun b => decide ¬le1 r0 b) r).length < r.length + 1 All goals completed! 🐙
lemma orderedInsertPos_lt_length {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : orderedInsertPos le1 r r0 < (r0 :: r).length := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(orderedInsertPos le1 r r0) < (r0 :: r).length I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(List.takeWhile (fun b => decide ¬le1 r0 b) r).length < r.length + 1 All goals completed! 🐙@[simp] lemma orderedInsert_get_orderedInsertPos {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.orderedInsert le1 r0 r)[(orderedInsertPos le1 r r0).val] = r0 := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(List.orderedInsert le1 r0 r)[(orderedInsertPos le1 r r0)] = r0 All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:IList.takeWhile (fun b => decide ¬le1 r0 b) r ++ (r0 :: List.dropWhile (fun b => decide ¬le1 r0 b) r).eraseIdx ((orderedInsertPos le1 r r0) - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length) = rI:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(List.takeWhile (fun b => decide ¬le1 r0 b) r).length (orderedInsertPos le1 r r0) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:IList.takeWhile (fun b => decide ¬le1 r0 b) r ++ (r0 :: List.dropWhile (fun b => decide ¬le1 r0 b) r).eraseIdx ((orderedInsertPos le1 r r0) - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length) = r All goals completed! 🐙 I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(List.takeWhile (fun b => decide ¬le1 r0 b) r).length (orderedInsertPos le1 r r0) All goals completed! 🐙lemma orderedInsertPos_cons {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 r1 : I) : (orderedInsertPos le1 (r1 ::r) r0).val = if le1 r0 r1 then 0, n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ir1:I0 < (List.orderedInsert le1 r0 r).length + 1 All goals completed! 🐙 else (Fin.succ (orderedInsertPos le1 r r0)) := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ir1:I(orderedInsertPos le1 (r1 :: r) r0) = (if le1 r0 r1 then 0, else (orderedInsertPos le1 r r0).succ) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ir1:I(match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = (if le1 r0 r1 then 0 else (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:le1 r0 r1(match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = (if le1 r0 r1 then 0 else (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, )I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:¬le1 r0 r1(match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = (if le1 r0 r1 then 0 else (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:le1 r0 r1(match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = (if le1 r0 r1 then 0 else (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, )I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ir1:Ih:¬le1 r0 r1(match !decide (le1 r0 r1) with | true => r1 :: List.takeWhile (fun b => !decide (le1 r0 b)) r | false => []).length = (if le1 r0 r1 then 0 else (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1, ) All goals completed! 🐙lemma orderedInsertPos_sigma {I : Type} {f : I Type} (le1 : I I Prop) [DecidableRel le1] (l : List (Σ i, f i)) (k : I) (a : f k) : (orderedInsertPos (fun (i j : Σ i, f i) => le1 i.1 j.1) l k, a).1 = (orderedInsertPos le1 (List.map (fun (i : Σ i, f i) => i.1) l) k).1 := I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)k:Ia:f k(orderedInsertPos (fun i j => le1 i.fst j.fst) l k, a) = (orderedInsertPos le1 (List.map (fun i => i.fst) l) k) I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)k:Ia:f k(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).length induction l with I:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia:f k(List.takeWhile (fun b => !decide (le1 k b.fst)) []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) [])).length All goals completed! 🐙 I:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia✝:f ka:(i : I) × f il:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).length(List.takeWhile (fun b => !decide (le1 k b.fst)) (a :: l)).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (a :: l))).length I:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia✝:f ka:(i : I) × f il:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).length(match !decide (le1 k a.fst) with | true => a :: List.takeWhile (fun b => !decide (le1 k b.fst)) l | false => []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (a :: l))).length I:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fst(match !decide (le1 k fst, snd.fst) with | true => fst, snd :: List.takeWhile (fun b => !decide (le1 k b.fst)) l | false => []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (fst, snd :: l))).length I:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fst(match !decide (le1 k fst) with | true => fst, snd :: List.takeWhile (fun b => !decide (le1 k b.fst)) l | false => []).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (fst, snd :: l))).length I:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = true(fst, snd :: List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (fst, snd :: l))).lengthI:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = false[].length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (fst, snd :: l))).length I:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = true(fst, snd :: List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (fst, snd :: l))).lengthI:Typef:I Typele1:I I Propinst✝:DecidableRel le1k:Ia:f kl:List ((i : I) × f i)ih:(List.takeWhile (fun b => !decide (le1 k b.fst)) l).length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) l)).lengthfst:Isnd:f fstx✝:Boolheq✝:(!decide (le1 k fst)) = false[].length = (List.takeWhile (fun b => !decide (le1 k b)) (List.map (fun i => i.fst) (fst, snd :: l))).length All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi✝:i < (orderedInsertPos le1 r r0)hi:i < (List.takeWhile (fun b => !decide (le1 r0 b)) r).lengthList.takeWhile (fun b => !decide (le1 r0 b)) r <+: r All goals completed! 🐙lemma orderedInsertPos_take_orderedInsert {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.take (orderedInsertPos le1 r r0) (List.orderedInsert le1 r0 r)) = List.takeWhile (fun b => decide ¬le1 r0 b) r := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:IList.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r) = List.takeWhile (fun b => decide ¬le1 r0 b) r All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:h1:n < (List.take (↑(orderedInsertPos le1 r r0)) r).lengthh2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).lengthr[n] = r.get n, I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:h1:n < (List.take (↑(orderedInsertPos le1 r r0)) r).lengthh2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).lengthn < (orderedInsertPos le1 r r0) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:h1:n < (List.take (↑(orderedInsertPos le1 r r0)) r).lengthh2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).lengthn < (orderedInsertPos le1 r r0) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:h2:n < (List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)).lengthh1:n < (orderedInsertPos le1 r r0) n < r.lengthn < (orderedInsertPos le1 r r0) All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ihr:r = List.takeWhile (fun b => !decide (le1 r0 b)) r ++ List.dropWhile (fun b => !decide (le1 r0 b)) rList.drop (↑(orderedInsertPos le1 r r0)) (List.takeWhile (fun b => !decide (le1 r0 b)) r) ++ List.drop ((orderedInsertPos le1 r r0) - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) (List.dropWhile (fun b => !decide (le1 r0 b)) r) = List.dropWhile (fun b => !decide (le1 r0 b)) r All goals completed! 🐙All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:IList.drop (↑(orderedInsertPos le1 r r0).succ) (List.orderedInsert le1 r0 r) = List.dropWhile (fun b => decide ¬le1 r0 b) r All goals completed! 🐙lemma orderedInsertPos_succ_take_orderedInsert {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.take (orderedInsertPos le1 r r0).succ (List.orderedInsert le1 r0 r)) = List.takeWhile (fun b => decide ¬le1 r0 b) r ++ [r0] := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:IList.take (↑(orderedInsertPos le1 r r0).succ) (List.orderedInsert le1 r0 r) = List.takeWhile (fun b => decide ¬le1 r0 b) r ++ [r0] All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r0:Ir:List In:Fin r.lengthhn:n < (orderedInsertPos le1 r r0)htake:r.get n List.takeWhile (fun b => decide ¬le1 r0 b) r¬le1 r0 (r.get n) All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r0:Ir:List In:Fin (List.orderedInsert le1 r0 r).lengthhn:n < orderedInsertPos le1 r r0htake:(List.orderedInsert le1 r0 r).get n List.takeWhile (fun b => decide ¬le1 r0 b) r¬le1 r0 ((List.orderedInsert le1 r0 r).get n) All goals completed! 🐙I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1r0:Ir:List Ihs:List.Pairwise le1 rn:Fin r.lengthhn✝:¬n < (orderedInsertPos le1 r r0)hn:n - (orderedInsertPos le1 r r0) + (orderedInsertPos le1 r r0) < r.length (hm : n - (orderedInsertPos le1 r r0) + (orderedInsertPos le1 r r0) < r.length), r[(orderedInsertPos le1 r r0) + (n - (orderedInsertPos le1 r r0))] = r.get n I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1r0:Ir:List Ihs:List.Pairwise le1 rn:Fin r.lengthhn✝:¬n < (orderedInsertPos le1 r r0)hn:n - (orderedInsertPos le1 r r0) + (orderedInsertPos le1 r r0) < r.lengthr[(orderedInsertPos le1 r r0) + (n - (orderedInsertPos le1 r r0))] = r.get n I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1r0:Ir:List Ihs:List.Pairwise le1 rn:Fin r.lengthhn✝:¬n < (orderedInsertPos le1 r r0)hn:n - (orderedInsertPos le1 r r0) + (orderedInsertPos le1 r r0) < r.length(orderedInsertPos le1 r r0) + (n - (orderedInsertPos le1 r r0)) = n All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)hi:i < (List.takeWhile (fun b => !decide (le1 r0 b)) r).lengthhi':¬(List.takeWhile (fun b => !decide (le1 r0 b)) r).length ir0 :: List.dropWhile (fun b => decide ¬le1 r0 b) r = r0 :: if (List.takeWhile (fun b => decide ¬le1 r0 b) r).length i then (List.dropWhile (fun b => decide ¬le1 r0 b) r).eraseIdx (i - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length) else List.dropWhile (fun b => decide ¬le1 r0 b) rI:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi:i < (orderedInsertPos le1 r r0)hr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i) (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi:i < (orderedInsertPos le1 r r0)hr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i) (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i) All goals completed! 🐙 I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi:i < (orderedInsertPos le1 r r0)hr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)i < (List.takeWhile (fun b => decide ¬le1 r0 b) r).length All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi:(List.takeWhile (fun b => decide ¬le1 r0 b) r).length, ihr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)hn:i + 1 - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length = i - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length + 1(List.takeWhile (fun b => decide ¬le1 r0 b) r).length i All goals completed! 🐙 I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi:(orderedInsertPos le1 r r0) ihr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)hn:i + 1 - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length = i - (List.takeWhile (fun b => decide ¬le1 r0 b) r).length + 1 (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i) All goals completed! 🐙 I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi:(orderedInsertPos le1 r r0) ihr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)(List.takeWhile (fun b => decide ¬le1 r0 b) r).length i.succ I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ii:hi:(List.takeWhile (fun b => decide ¬le1 r0 b) r).length ihr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)(List.takeWhile (fun b => decide ¬le1 r0 b) r).length i.succ All goals completed! 🐙

The equivalence between Fin (r0 :: r).length and Fin (List.orderedInsert le1 r0 r).length according to where the elements map, i.e. 0 is taken to orderedInsertPos le1 r r0.

@[`@[expose]` has no effect outside a `module` fileexpose] def orderedInsertEquiv {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : Fin (r.length + 1) Fin (List.orderedInsert le1 r0 r).length := n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:IFin (r.length + 1) Fin (List.orderedInsert le1 r0 r).length n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ie2:Fin (List.orderedInsert le1 r0 r).length Fin (r0 :: r).length := (Fin.castOrderIso ).toEquivFin (r.length + 1) Fin (List.orderedInsert le1 r0 r).length n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ie2:Fin (List.orderedInsert le1 r0 r).length Fin (r0 :: r).length := (Fin.castOrderIso ).toEquive3:Fin (r0 :: r).length Fin 1 Fin r.length := finExtractOne 0Fin (r.length + 1) Fin (List.orderedInsert le1 r0 r).length n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ie2:Fin (List.orderedInsert le1 r0 r).length Fin (r0 :: r).length := (Fin.castOrderIso ).toEquive3:Fin (r0 :: r).length Fin 1 Fin r.length := finExtractOne 0e4:Fin (r0 :: r).length Fin 1 Fin r.length := finExtractOne (orderedInsertPos le1 r r0), Fin (r.length + 1) Fin (List.orderedInsert le1 r0 r).length All goals completed! 🐙
@[simp] lemma orderedInsertEquiv_zero {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : orderedInsertEquiv le1 r r0 0 = orderedInsertPos le1 r r0 := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(orderedInsertEquiv le1 r r0) 0 = orderedInsertPos le1 r r0 All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:In:r1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length(Fin.castOrderIso ).symm ((finExtractOne (orderedInsertPos le1 (r1 :: r) r0), ).symm (Sum.inr (predAboveI 0 n + 1, hn))) = Fin.cast ((orderedInsertPos le1 (r1 :: r) r0), .succAbove n, )I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:In:r1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length0 n + 1, hn I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:In:r1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length(Fin.castOrderIso ).symm ((List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, .succAbove (predAboveI 0 n + 1, hn)) = Fin.cast ((List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, .succAbove n, )I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:In:r1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length0 n + 1, hn I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:In:r1:Ir:List Ihn:n.succ < (r0 :: r1 :: r).length0 n + 1, hn All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length(Fin.castOrderIso ).symm ((finExtractOne (orderedInsertPos le1 (r1 :: r) r0), ).symm (Sum.inr (predAboveI 0 n.succ))) = Fin.cast ((orderedInsertPos le1 (r1 :: r) r0), .succAbove n)I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length0 n.succ I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length(Fin.castOrderIso ).symm ((List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, .succAbove (predAboveI 0 n.succ)) = Fin.cast ((List.takeWhile (fun b => !decide (le1 r0 b)) (r1 :: r)).length, .succAbove n)I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length0 n.succ I:Typele1:I I Propinst✝:DecidableRel le1r✝:List Ir0:Ir1:Ir:List In:Fin (r1 :: r).length0 n.succ All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:(Fin.cast ((orderedInsertPos le1 r r0), .succAbove n, )) < (Fin.cast ((orderedInsertPos le1 r r0), .succAbove m, ))n < m I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:(orderedInsertPos le1 r r0), .succAbove n < (orderedInsertPos le1 r r0), .succAbove mn < m rwa [I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:n < mn < mI:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthm:Fin r.lengthhx:n < mn < m at hxlemma orderedInsertEquiv_congr {α : Type} {r : α α Prop} [DecidableRel r] (a : α) (l l' : List α) (h : l = l') : orderedInsertEquiv r l a = (Fin.castOrderIso (n:α:Typer:α α Propinst✝:DecidableRel ra:αl:List αl':List αh:l = l'l.length + 1 = l'.length + 1 All goals completed! 🐙)).toEquiv.trans ((orderedInsertEquiv r l' a).trans (Fin.castOrderIso (n:α:Typer:α α Propinst✝:DecidableRel ra:αl:List αl':List αh:l = l'(List.orderedInsert r a l').length = (List.orderedInsert r a l).length All goals completed! 🐙)).toEquiv) := α:Typer:α α Propinst✝:DecidableRel ra:αl:List αl':List αh:l = l'orderedInsertEquiv r l a = (Fin.castOrderIso ).trans ((orderedInsertEquiv r l' a).trans (Fin.castOrderIso ).toEquiv) α:Typer:α α Propinst✝:DecidableRel ra:αl:List αorderedInsertEquiv r l a = (Fin.castOrderIso ).trans ((orderedInsertEquiv r l a).trans (Fin.castOrderIso ).toEquiv) All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ix:Fin (r0 :: r).lengthn:h:n.succ < (r0 :: r).lengthhn:¬n < (orderedInsertPos le1 r r0)hn':¬n + 1 < (List.takeWhile (fun b => !decide (le1 r0 b)) r).lengthhnn:n + 1 - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length = n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1hr:r.length = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + (List.dropWhile (fun b => !decide (le1 r0 b)) r).lengthn = r.length - (List.dropWhile (fun b => !decide (le1 r0 b)) r).length + (n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ix:Fin (r0 :: r).lengthn:h:n.succ < (r0 :: r).lengthhn:¬n < (orderedInsertPos le1 r r0)hn':¬n + 1 < (List.takeWhile (fun b => !decide (le1 r0 b)) r).lengthhnn:n + 1 - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length = n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + 1hr:r.length = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + (List.dropWhile (fun b => !decide (le1 r0 b)) r).lengthn = (List.takeWhile (fun b => !decide (le1 r0 b)) r).length + (n - (List.takeWhile (fun b => !decide (le1 r0 b)) r).length) All goals completed! 🐙lemma orderedInsertEquiv_get {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : (r0 :: r).get (orderedInsertEquiv le1 r r0).symm = (List.orderedInsert le1 r0 r).get := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(r0 :: r).get (orderedInsertEquiv le1 r r0).symm = (List.orderedInsert le1 r0 r).get I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:Ix:Fin (List.orderedInsert le1 r0 r).length((r0 :: r).get (orderedInsertEquiv le1 r r0).symm) x = (List.orderedInsert le1 r0 r).get x All goals completed! 🐙lemma orderedInsert_eraseIdx_orderedInsertEquiv_zero {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 0, n:I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I0 < r.length + 1 All goals completed! 🐙) = r := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:I(List.orderedInsert le1 r0 r).eraseIdx ((orderedInsertEquiv le1 r r0) 0, ) = r All goals completed! 🐙I:Typele1:I I Propinst✝:DecidableRel le1r0:In:r1:Ir:List Iih: (hn : n.succ < (r0 :: r).length), (∀ (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)) (List.orderedInsert le1 r0 r).eraseIdx ((orderedInsertEquiv le1 r r0) n.succ, hn) = List.orderedInsert le1 r0 (r.eraseIdx n)hn:n.succ < (r0 :: r1 :: r).lengthhr: (i j : Fin (r1 :: r).length), i < j ¬le1 r0 ((r1 :: r).get j) ¬le1 r0 ((r1 :: r).get i)hn':¬n < (orderedInsertPos le1 (r1 :: r) r0)(orderedInsertPos le1 (r1 :: r) r0) n All goals completed! 🐙lemma orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ {I : Type} (le1 : I I Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : Fin r.length) (hr : (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)) : (List.orderedInsert le1 r0 r).eraseIdx (orderedInsertEquiv le1 r r0 n.succ) = (List.orderedInsert le1 r0 (r.eraseIdx n)) := I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In:Fin r.lengthhr: (i j : Fin r.length), i < j ¬le1 r0 (r.get j) ¬le1 r0 (r.get i)(List.orderedInsert le1 r0 r).eraseIdx ((orderedInsertEquiv le1 r r0) n.succ) = List.orderedInsert le1 r0 (r.eraseIdx n) All goals completed! 🐙I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:h0:n.succ < l.length + 1(if n, .castSucc < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i), then n, .castSucc else n, .succ) = (if n, .castSucc < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i), then n, .castSucc else n, .succ) I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:h0:n.succ < l.length + 1(if n < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i) then n, else n + 1, ) = (if n < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i) then n, else n + 1, ) I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:h0:n.succ < l.length + 1h✝:n < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i)n, = n, I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:h0:n.succ < l.length + 1h✝:¬n < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i)n + 1, = n + 1, I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:h0:n.succ < l.length + 1h✝:n < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i)n, = n, I:Typef:I Typele1:I I Propinst✝:DecidableRel le1l:List ((i : I) × f i)i:Ia:f ix:Fin (l.length + 1)n:h0:n.succ < l.length + 1h✝:¬n < (orderedInsertPos le1 (List.map (fun i => i.fst) l) i)n + 1, = n + 1, All goals completed! 🐙set_option maxHeartbeats 350000I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':h0:n'.succ < r.length + 1h1:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (List.orderedInsert le1 r0 r).lengthh2:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) n'.succ, h0 = ((orderedInsertEquiv le1 r r0) n'.succ, h0), h1hr:((orderedInsertEquiv le1 r r0) n'.succ, h0) = (Fin.cast ((orderedInsertPos le1 r r0), .succAbove n', ))hx:((orderedInsertEquiv le1 r r0) n' + 1, h0), h2 = ((orderedInsertPos le1 r r0), .succAbove n', ), hn':¬n' < (orderedInsertPos le1 r r0)r[n'] = r[n' + 1 - 1]I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':h0:n'.succ < r.length + 1h1:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (List.orderedInsert le1 r0 r).lengthh2:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) n'.succ, h0 = ((orderedInsertEquiv le1 r r0) n'.succ, h0), h1hr:((orderedInsertEquiv le1 r r0) n'.succ, h0) = (Fin.cast ((orderedInsertPos le1 r r0), .succAbove n', ))hx:((orderedInsertEquiv le1 r r0) n' + 1, h0), h2 = ((orderedInsertPos le1 r r0), .succAbove n', ), hn':¬n' < (orderedInsertPos le1 r r0)(orderedInsertPos le1 r r0) < n' + 1 I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':h0:n'.succ < r.length + 1h1:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (List.orderedInsert le1 r0 r).lengthh2:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) n'.succ, h0 = ((orderedInsertEquiv le1 r r0) n'.succ, h0), h1hr:((orderedInsertEquiv le1 r r0) n'.succ, h0) = (Fin.cast ((orderedInsertPos le1 r r0), .succAbove n', ))hx:((orderedInsertEquiv le1 r r0) n' + 1, h0), h2 = ((orderedInsertPos le1 r r0), .succAbove n', ), hn':¬n' < (orderedInsertPos le1 r r0)r[n'] = r[n' + 1 - 1] All goals completed! 🐙 I:Typele1:I I Propinst✝:DecidableRel le1r:List Ir0:In'✝:Fin (r.length + 1)n':h0:n'.succ < r.length + 1h1:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (List.orderedInsert le1 r0 r).lengthh2:((orderedInsertEquiv le1 r r0) n'.succ, h0) < (r.insertIdx (↑(orderedInsertPos le1 r r0)) r0).lengthhn'✝:(orderedInsertEquiv le1 r r0) n'.succ, h0 = ((orderedInsertEquiv le1 r r0) n'.succ, h0), h1hr:((orderedInsertEquiv le1 r r0) n'.succ, h0) = (Fin.cast ((orderedInsertPos le1 r r0), .succAbove n', ))hx:((orderedInsertEquiv le1 r r0) n' + 1, h0), h2 = ((orderedInsertPos le1 r r0), .succAbove n', ), hn':¬n' < (orderedInsertPos le1 r r0)(orderedInsertPos le1 r r0) < n' + 1 All goals completed! 🐙

The equivalence between Fin l.length ≃ Fin (List.insertionSort r l).length induced by the sorting algorithm.

def insertionSortEquiv {α : Type} (r : α α Prop) [DecidableRel r] : (l : List α) Fin l.length Fin (List.insertionSort r l).length | [] => Equiv.refl _ | a :: l => (Fin.equivCons (insertionSortEquiv r l)).trans (orderedInsertEquiv r (List.insertionSort r l) a)
α:Typer:α α Propinst✝:DecidableRel ra:αl:List αhl:(a :: l).get (equivCons (insertionSortEquiv r l)).symm = (a :: List.insertionSort r l).get(List.orderedInsert r a (List.insertionSort r l)).get = (List.insertionSort r (a :: l)).get All goals completed! 🐙lemma insertionSortEquiv_congr {α : Type} {r : α α Prop} [DecidableRel r] (l l' : List α) (h : l = l') : insertionSortEquiv r l = (Fin.castOrderIso (n:α:Typer:α α Propinst✝:DecidableRel rl:List αl':List αh:l = l'l.length = l'.length All goals completed! 🐙)).toEquiv.trans ((insertionSortEquiv r l').trans (Fin.castOrderIso (n:α:Typer:α α Propinst✝:DecidableRel rl:List αl':List αh:l = l'(List.insertionSort r l').length = (List.insertionSort r l).length All goals completed! 🐙)).toEquiv) := α:Typer:α α Propinst✝:DecidableRel rl:List αl':List αh:l = l'insertionSortEquiv r l = (Fin.castOrderIso ).trans ((insertionSortEquiv r l').trans (Fin.castOrderIso ).toEquiv) α:Typer:α α Propinst✝:DecidableRel rl:List αinsertionSortEquiv r l = (Fin.castOrderIso ).trans ((insertionSortEquiv r l).trans (Fin.castOrderIso ).toEquiv) All goals completed! 🐙α:Typer:α α Propinst✝:DecidableRel rl:List αl':List αh:l = l'i:Fin l.length((Fin.castOrderIso ).trans ((insertionSortEquiv r l').trans (Fin.castOrderIso ).toEquiv)) i = Fin.cast ((insertionSortEquiv r l') (Fin.cast i)) All goals completed! 🐙lemma insertionSort_get_comp_insertionSortEquiv {α : Type} {r : α α Prop} [DecidableRel r] (l : List α) : (List.insertionSort r l).get (insertionSortEquiv r l) = l.get := α:Typer:α α Propinst✝:DecidableRel rl:List α(List.insertionSort r l).get (insertionSortEquiv r l) = l.get α:Typer:α α Propinst✝:DecidableRel rl:List αx:Fin l.length((List.insertionSort r l).get (insertionSortEquiv r l)) x = l.get x All goals completed! 🐙All goals completed! 🐙α:Typer:α α Propinst✝:DecidableRel ra:αas:List αhi:0 < (a :: as).lengthj:hj:j + 1 < (a :: as).lengthhij:0, hi < j + 1, hjhij':(insertionSortEquiv r (a :: as)) j + 1, hj < (orderedInsertEquiv r (List.insertionSort r as) a) 0as[j] = ((a :: as).get (insertionSortEquiv r (a :: as)).symm) ((insertionSortEquiv r (a :: as)) j + 1, hj) All goals completed! 🐙 α:Typer:α α Propinst✝:DecidableRel ra:αas:List αi:hi:i + 1 < (a :: as).lengthj:hj:j + 1 < (a :: as).lengthhij:i + 1, hi < j + 1, hjhij':(insertionSortEquiv r (a :: as)) j + 1, hj < (insertionSortEquiv r (a :: as)) i + 1, hi¬r (a :: as)[i + 1, hi] (a :: as)[j + 1, hj] α:Typer:α α Propinst✝:DecidableRel ra:αas:List αi:hi:i + 1 < (a :: as).lengthj:hj:j + 1 < (a :: as).lengthhij:i + 1, hi < j + 1, hjhij':(insertionSortEquiv r (a :: as)) j + 1, hj < (insertionSortEquiv r (a :: as)) i + 1, hi¬r (a :: as)[i + 1, hi] (a :: as)[j + 1, hj] α:Typer:α α Propinst✝:DecidableRel ra:αas:List αi:hi:i + 1 < (a :: as).lengthj:hj:j + 1 < (a :: as).lengthhij:i + 1, hi < j + 1, hjhij':(orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) j, ).succ < (orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) i, ).succ¬r (a :: as)[i + 1, hi] (a :: as)[j + 1, hj] simpa using insertionSortEquiv_order as i, Nat.succ_lt_succ_iff.mp hi j, Nat.succ_lt_succ_iff.mp hj (α:Typer:α α Propinst✝:DecidableRel ra:αas:List αi:hi:i + 1 < (a :: as).lengthj:hj:j + 1 < (a :: as).lengthhij:i + 1, hi < j + 1, hjhij':(orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) j, ).succ < (orderedInsertEquiv r (List.insertionSort r as) a) ((insertionSortEquiv r as) i, ).succi, < j, All goals completed! 🐙) (orderedInsertEquiv_monotone_fin_succ _ _ _ _ _ hij')

Optional erase of an element in a list. For none returns the list, for some i returns the list with the i'th element erased.

@[`@[expose]` has no effect outside a `module` fileexpose] def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I := match i with | none => l | some i => List.eraseIdx l i
lemma eraseIdx_length' {I : Type} (l : List I) (i : Fin l.length) : (List.eraseIdx l i).length = l.length - 1 := I:Typel:List Ii:Fin l.length(l.eraseIdx i).length = l.length - 1 All goals completed! 🐙lemma eraseIdx_length {I : Type} (l : List I) (i : Fin l.length) : (List.eraseIdx l i).length + 1 = l.length := List.length_eraseIdx_add_one i.isLtlemma eraseIdx_length_succ {I : Type} (l : List I) (i : Fin l.length) : (List.eraseIdx l i).length.succ = l.length := List.length_eraseIdx_add_one i.isLtlemma eraseIdx_cons_length {I : Type} (a : I) (l : List I) (i : Fin (a :: l).length) : (List.eraseIdx (a :: l) i).length= l.length := I:Typea:Il:List Ii:Fin (a :: l).length((a :: l).eraseIdx i).length = l.length All goals completed! 🐙I:Typel:List Ii:Fin l.lengthx:Fin (l.eraseIdx i).lengthhi✝:¬x.castSucc < Fin.cast ihi:i xhn:¬x < i(if h' : x < i then l[x] else l[x + 1]) = l[x + 1] All goals completed! 🐙I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ))(List.foldr (List.orderedInsert le1) [] (r0 :: r)).eraseIdx ((orderedInsertEquiv le1 (List.foldr (List.orderedInsert le1) [] r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.foldr (List.orderedInsert le1) [] ((r0 :: r).eraseIdx (n + 1)) erw [I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ))List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, )) = List.foldr (List.orderedInsert le1) [] ((r0 :: r).eraseIdx (n + 1))I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, )) (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ))List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, )) = List.foldr (List.orderedInsert le1) [] ((r0 :: r).eraseIdx (n + 1))I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, )) (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ))(List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ) = List.foldr (List.orderedInsert le1) [] (r.eraseIdx n)I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, )) (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, )) (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn✝:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ))i:Fin (List.insertionSort le1 r).lengthj:Fin (List.insertionSort le1 r).lengthhij:i < jhn:¬le1 r0 ((List.insertionSort le1 r).get j)¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn✝:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ))i:Fin (List.insertionSort le1 r).lengthj:Fin (List.insertionSort le1 r).lengthhij:i < jhn:¬le1 r0 ((List.insertionSort le1 r).get j)hx:le1 ((List.insertionSort le1 r).get i) ((List.insertionSort le1 r).get j)¬le1 r0 ((List.insertionSort le1 r).get i) I:Typele1:I I Propinst✝²:DecidableRel le1inst✝¹:Std.Total le1inst✝:IsTrans I le1n:r0:Ir:List Ihn✝:n.succ < (r0 :: r).lengthhOr:(∀ (i j : Fin (List.insertionSort le1 r).length), i < j ¬le1 r0 ((List.insertionSort le1 r).get j) ¬le1 r0 ((List.insertionSort le1 r).get i)) (List.orderedInsert le1 r0 (List.insertionSort le1 r)).eraseIdx ((orderedInsertEquiv le1 (List.insertionSort le1 r) r0) ((insertionSortEquiv le1 r) n, ).succ) = List.orderedInsert le1 r0 ((List.insertionSort le1 r).eraseIdx ((insertionSortEquiv le1 r) n, ))i:Fin (List.insertionSort le1 r).lengthj:Fin (List.insertionSort le1 r).lengthhij:i < jhn:¬le1 r0 ((List.insertionSort le1 r).get j)hx:le1 ((List.insertionSort le1 r).get i) ((List.insertionSort le1 r).get j)ht: (i j k : I), le1 i j ¬le1 k j ¬le1 k i¬le1 r0 ((List.insertionSort le1 r).get i) All goals completed! 🐙lemma eraseIdx_insertionSort_fin {I : Type} (le1 : I I Prop) [DecidableRel le1] [Std.Total le1] [IsTrans I le1] (r : List I) (n : Fin r.length) : (List.insertionSort le1 r).eraseIdx ((Physlib.List.insertionSortEquiv le1 r) n) = List.insertionSort le1 (r.eraseIdx n) := eraseIdx_insertionSort le1 n.val r (Fin.prop n)

Given a list i :: l the left-most minimal position a of i :: l wrt r. That is the first position of l such that for every element (i :: l)[b] before that position r ((i :: l)[b]) ((i :: l)[a]) is not true. The use of i :: l here rather then just l is to ensure that such a position exists. .

n:α:Typer:α α Propinst✝:DecidableRel ri:αl:List α0 < (i :: l).length All goals completed! 🐙

The element of i :: l at insertionSortMinPos.

@[`@[expose]` has no effect outside a `module` fileexpose] def insertionSortMin {α : Type} (r : α α Prop) [DecidableRel r] (i : α) (l : List α) : α := (i :: l).get (insertionSortMinPos r i l)
α:Typer:α α Propinst✝:DecidableRel ri:αl:List αinsertionSortMin r i l = ((i :: l).get (insertionSortEquiv r (i :: l)).symm) 0, All goals completed! 🐙 α:Typer:α α Propinst✝:DecidableRel ri:αl:List α(List.insertionSort r (i :: l)).get 0, = (List.insertionSort r (i :: l)).head All goals completed! 🐙

The list remaining after dropping the element at the position determined by insertionSortMinPos.

@[`@[expose]` has no effect outside a `module` fileexpose] def insertionSortDropMinPos {α : Type} (r : α α Prop) [DecidableRel r] (i : α) (l : List α) : List α := (i :: l).eraseIdx (insertionSortMinPos r i l)
α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ri:αl:List αList.foldr (List.orderedInsert r) [] (i :: l) = (List.insertionSort r (i :: l)).head :: (List.foldr (List.orderedInsert r) [] (i :: l)).tail All goals completed! 🐙

Optional erase of an element in a list, with addition for none. For none adds a to the front of the list, for some i removes the ith element of the list (does not add a). E.g. optionEraseZ [0, 1, 2] 4 none = [4, 0, 1, 2] and optionEraseZ [0, 1, 2] 4 (some 1) = [0, 2].

@[`@[expose]` has no effect outside a `module` fileexpose] def optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : List I := match i with | none => a :: l | some i => List.eraseIdx l i
@[simp] lemma optionEraseZ_some_length {I : Type} (l : List I) (a : I) (i : (Fin l.length)) : (optionEraseZ l a (some i)).length = l.length - 1 := I:Typel:List Ia:Ii:Fin l.length(optionEraseZ l a (some i)).length = l.length - 1 All goals completed! 🐙All goals completed! 🐙)) i = i') : optionEraseZ l a i = optionEraseZ l' a' i' := I:Typel:List Il':List Ia:Ia':Ii:Option (Fin l.length)i':Option (Fin l'.length)hl:l = l'ha:a = a'hi:Option.map (Fin.cast ) i = i'optionEraseZ l a i = optionEraseZ l' a' i' I:Typel:List Ia:Ia':Ii:Option (Fin l.length)ha:a = a'i':Option (Fin l.length)hi:Option.map (Fin.cast ) i = i'optionEraseZ l a i = optionEraseZ l a' i' I:Typel:List Ia:Ii:Option (Fin l.length)i':Option (Fin l.length)hi:Option.map (Fin.cast ) i = i'optionEraseZ l a i = optionEraseZ l a i' I:Typel:List Ia:Ii:Option (Fin l.length)optionEraseZ l a i = optionEraseZ l a (Option.map (Fin.cast ) i) I:Typel:List Ia:Ii:Option (Fin l.length)i = Option.map (Fin.cast ) i All goals completed! 🐙n:m:i:h:i + 1 < n + 1a:Fin nha:a < m a.succ = i + 1, hi < m n:m:i:h:i + 1 < n + 1a:Fin nha:a < m a = ii < m All goals completed! 🐙 n:m:i:h:i + 1 < n + 1i < m a List.take m (List.finRange n), a.succ = i + 1, h n:m:i:h:i + 1 < n + 1h1:i < m a List.take m (List.finRange n), a.succ = i + 1, h✝ n:m:i:h:i + 1 < n + 1h1:i < mi, List.take m (List.finRange n) i, .succ = i + 1, h n:m:i:h:i + 1 < n + 1h1:i < mi, List.take m (List.finRange n) rwa [n:m:i:h:i + 1 < n + 1h1:i < mi, < mn:m:i:h:i + 1 < n + 1h1:i < mi, < m