1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
 import Data.Vect
import Prelude.WellFounded
 A proof that by inserting 'x' somewhere into 'as', we get 'bs'.
 Example: 'Insert 1 [2,5,9,3] [2,5,9,1,3]' should hold, whereas 'Insert 9 [2,1,1,4] [2,1,5,1,4]' should not
data Insert : (x : elem) > (as : Vect n elem) > (bs : Vect (S n) elem) > Type where
 Consing counts as inserting
 Example: 'Insert 1 [2,5,5] [1,2,5,5]'
IHere : Insert x as (x :: as)
 Inserting into the tail implies inserting into the whole list
 Example: 'Insert 5 [2,3] [2,5,3] > Insert 5 [1,2,3] [1,2,5,3]'
ILater : Insert x as bs > Insert x (m :: as) (m :: bs)
 Inserting x in the middle of 'as' and 'bs' counts as inserting.
 Example: 'Insert 4 ([1,7] ++ [3,8]) ([1,7] ++ 4 :: [3, 8])', i.e. 'Insert 4 [1,7,3,8] [1,7,4,3,8]'
total
insert_append : (as : Vect n elem) > (x : elem) > (bs : Vect m elem) > Insert x (as ++ bs) (rewrite plusSuccRightSucc n m in as ++ x :: bs)
insert_append [] x bs = IHere
insert_append {n = S k} {m} (a :: as) x bs =
let IH = insert_append as x bs
in ILater {m = a} {x = x} {as = as ++ bs} {bs = rewrite plusSuccRightSucc k m in as ++ x :: bs} IH
