Insert

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

Error message

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
- + Errors (1)
 `-- meow.idr line 20 col 14:
     When checking right hand side of insert_append with expected type
             Insert x
                    ((a :: as) ++ bs)
                    (rewrite__impl (\replaced => Vect replaced elem)
                                   (plusSuccRightSucc (S k) m)
                                   ((a :: as) ++ x :: bs))
     
     Type mismatch between
             Insert x
                    (a :: as ++ bs)
                    (a ::
                     (let _rewrite_rule = plusSuccRightSucc k m
                      in rewrite__impl (\replaced1 => Vect replaced1 elem)
                                       (plusSuccRightSucc k m)
                                       (as ++ x :: bs))) (Type of ILater IH)
     and
             Insert x
                    (a :: as ++ bs)
                    (rewrite__impl (\replaced => Vect replaced elem)
                                   (rewrite__impl (\replaced =>
                                                     S replaced = S (plus k (S m)))
                                                  (plusSuccRightSucc k m)
                                                  Refl)
                                   (a :: as ++ x :: bs)) (Expected type)
     
     Specifically:
             Type mismatch between
                     a ::
                     (let _rewrite_rule = plusSuccRightSucc k m
                      in rewrite__impl (\replaced1 => Vect replaced1 elem)
                                       (plusSuccRightSucc k m)
                                       (as ++ x :: bs))
             and
                     rewrite__impl (\replaced => Vect replaced elem)
                                   (rewrite__impl (\replaced =>
                                                     S replaced = S (plus k (S m)))
                                                  (plusSuccRightSucc k m)
                                                  Refl)
                                   (a :: as ++ x :: bs)