Need more list theorems

[treeowl]

I'm going to attempt some of these, but I figured I'd open a ticket to track.

1. Characterization of reverse
2. Cancellation laws for ++
3. init xs ++ [last xs] = xs
4. inits [] = [[]] and inits ys@(_:_) = inits (init ys) ++ [ys]
5. inits xs = reverse . tails . reverse $ xs, if it's worth the trouble
6. sort is actually a (stable) sort—this will have to wait for a proven-total version.
7. List and vector operations all correspond correctly through toList and fromList.
8. foldr and unfoldr laws
9. We can do induction backwards: I think that would look something like this (but I'm not yet familiar with how Idris handles rank-2 types).

back : {P : List a -> Type} ->
   P [] ->
   ({xs : List a, x : a} -> P xs -> P (xs ++ [x])) ->
   (ys : List a) -> P ys

Once 1 and 2 are complete, it should be safe to hide the choice of init implementation, which I think would probably be wise. Once 3 is complete, it should be safe to hide the choice of inits implementation, which I think would certainly be wise.

[david-christiansen]

Hiding implementations is a bit of a tradeoff. Because our type and term languages coincide, ordinary computation becomes visible in types, and things that are equal are just equal. If the implementation isn't available (eg if the function is abstract) then manual rewriting with equality proofs becomes necessary, which is quite tedious. In essence, treating functions that occur in types as black boxes makes type checking painful, while not treating them as black boxes is perhaps ugly software engineering.

[treeowl]

I don't understand all the details, but it seems pretty clear to me that exposing the implementation allows people to write all sorts of code that breaks as soon as the implementation changes! I'd much rather see black boxes, except for some functions exposed explicitly for this purpose. But I'd much rather get, say, a sorting function whose type explains what its result means than a sorting function whose code I need to dig into. On Apr 2, 2015 1:46 AM, "David Christiansen" notifications@github.com wrote:

Hiding implementations is a bit of a tradeoff. Because our type and term languages coincide, ordinary computation becomes visible in types, and things that are equal are just equal. If the implementation isn't available (eg if the function is abstract) then manual rewriting with equality proofs becomes necessary, which is quite tedious. In essence, treating functions that occur in types as black boxes makes type checking painful, while not treating them as black boxes is perhaps ugly software engineering.

— Reply to this email directly or view it on GitHub https://github.com/idris-lang/Idris-dev/issues/2099#issuecomment-88748123 .

[treeowl]

Note, for example, that the current inits implementation is asymptotically bad, so it needs to be replaced. There are several good ways to do it. Letting everyone depend on one particular one seems to limit future improvements. On Apr 2, 2015 1:58 AM, "David Feuer" david.feuer@gmail.com wrote:

I don't understand all the details, but it seems pretty clear to me that exposing the implementation allows people to write all sorts of code that breaks as soon as the implementation changes! I'd much rather see black boxes, except for some functions exposed explicitly for this purpose. But I'd much rather get, say, a sorting function whose type explains what its result means than a sorting function whose code I need to dig into. On Apr 2, 2015 1:46 AM, "David Christiansen" notifications@github.com wrote:

Hiding implementations is a bit of a tradeoff. Because our type and term languages coincide, ordinary computation becomes visible in types, and things that are equal are just equal. If the implementation isn't available (eg if the function is abstract) then manual rewriting with equality proofs becomes necessary, which is quite tedious. In essence, treating functions that occur in types as black boxes makes type checking painful, while not treating them as black boxes is perhaps ugly software engineering.

— Reply to this email directly or view it on GitHub https://github.com/idris-lang/Idris-dev/issues/2099#issuecomment-88748123 .

[david-christiansen]

This is one of the software engineering challenges of dependent types, that we don't yet have a good answer for.

I'm not saying we shouldn't do it in this case - just that it's not a generally applicable principle.

What we really need is a way to have run time and compile time versions of a function, one used in types and the other in programs, given proofs that they compute the same result for all inputs.

[treeowl]

Here are some basics I worked out (some badly) that would be very good to have in some form:

reverseOnto : List a -> List a -> List a
reverseOnto acc [] = acc
reverseOnto acc (x::xs) = reverseOnto (x::acc) xs

myreverse : List a -> List a
myreverse xs = reverseOnto [] xs

reverseOntoGenLem : (qs,rs, ps:List a) -> reverseOnto qs ps ++ rs = reverseOnto (qs ++ rs) ps
reverseOntoGenLem qs rs [] = Refl
reverseOntoGenLem qs rs (x :: xs) = reverseOntoGenLem (x::qs) rs xs

reverseOntoReversesOnto : (qs,ps:List a) -> reverseOnto qs ps = myreverse ps ++ qs
reverseOntoReversesOnto qs ps = sym $ reverseOntoGenLem [] qs ps

reverseDistributesOverAppend : (xs,ys : List a) -> myreverse (xs ++ ys) = myreverse ys ++ myreverse xs
reverseDistributesOverAppend [] ys =
  sym $ appendNilRightNeutral (myreverse ys)
reverseDistributesOverAppend (p :: ps) ys =
  let inductiveHypothesis = reverseDistributesOverAppend ps ys
  in ?reverseDistributesOverAppend_rhs_3

reverseSingletonIdentity : (x:a) -> myreverse [x] = [x]
reverseSingletonIdentity x = Refl

reverseSelfInverse : (xs : List a) -> myreverse (myreverse xs) = xs
reverseSelfInverse [] = Refl
reverseSelfInverse (x::xs) =
  let ind = reverseSelfInverse xs   -- myreverse (myreverse xs) = xs
      distr = reverseDistributesOverAppend [x] xs -- myreverse ([x]++xs) = myreverse xs ++ myreverse [x]
      distr2 = reverseDistributesOverAppend (myreverse xs) (myreverse [x])
  in ?reverseSelfInverse_rhs

tailsEq' : (x,y : a) -> (xs, ys : List a) -> (x::xs = y::ys) -> xs=ys
tailsEq' x x ys ys Refl = Refl

appendLeftCancel : (left : List a) -> (right : List a) -> (right' : List a) ->
                   (left ++ right = left ++ right') -> right = right'
appendLeftCancel [] right right' prf = prf
appendLeftCancel (x :: xs) right right' prf =
  let foo = tailsEq' x x (xs++right) (xs++right') prf
  in appendLeftCancel xs right right' foo

-- This part is reeeeeal ugly. Maybe someone will help me clean it up.
appendRightCancelL1 : (left : List a) -> (left' : List a) -> (right : List a) ->
                    (left ++ right = left' ++ right) -> myreverse (left++right) = myreverse (left' ++ right)
appendRightCancelL1 left left' right prf = cong {f = myreverse} prf

appendRightCancelL2 : (left : List a) -> (left' : List a) -> (right : List a) ->
                    (left ++ right = left' ++ right) -> myreverse right++myreverse left = myreverse right ++ myreverse left'
appendRightCancelL2 left left' right prf =
  rewrite sym $ reverseDistributesOverAppend left right
  in rewrite sym $ reverseDistributesOverAppend left' right
  in appendRightCancelL1 left left' right prf

appendRightCancelL3 : (left : List a) -> (left' : List a) -> (right : List a) ->
                    (left ++ right = left' ++ right) -> myreverse left = myreverse left'
appendRightCancelL3 left left' right prf =
  let first = appendRightCancelL2 left left' right prf
  in rewrite appendLeftCancel (myreverse right) (myreverse left) (myreverse left') first
  in Refl

appendRightCancel : (left : List a) -> (left' : List a) -> (right : List a) ->
                    (left ++ right = left' ++ right) -> left = left'
appendRightCancel left left' right prf =
  rewrite sym $ reverseSelfInverse left
  in rewrite sym $ reverseSelfInverse left'
  in cong {f = myreverse} (appendRightCancelL3 left left' right prf)

---------- Proofs ----------

reverseSelfInverse_rhs = proof
  compute
  intros
  rewrite sym distr
  rewrite sym distr2
  rewrite ind
  trivial

reverseDistributesOverAppend_rhs_3 = proof
  compute
  intros
  rewrite sym$ reverseOntoReversesOnto [p] ps
  rewrite sym $ appendAssociative (reverseOnto [] ys) (reverseOnto [] ps) [p]
  rewrite inductiveHypothesis 
  rewrite reverseOntoReversesOnto [p] (ps++ys)
  trivial

[JakobBruenker]

I changed a few things in ways that I personally find more aesthetically pleasing:

-- JB: added flag
%default total

reverseOnto : List a -> List a -> List a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x :: acc) xs

myreverse : List a -> List a
myreverse xs = reverseOnto [] xs

reverseOntoGenLem : (qs, rs, ps : List a) ->
                    reverseOnto qs ps ++ rs = reverseOnto (qs ++ rs) ps
reverseOntoGenLem qs rs [] = Refl
reverseOntoGenLem qs rs (x :: xs) = reverseOntoGenLem (x :: qs) rs xs

reverseOntoReversesOnto : (qs, ps : List a) ->
                          reverseOnto qs ps = myreverse ps ++ qs
reverseOntoReversesOnto qs ps = sym $ reverseOntoGenLem [] qs ps

-- JB: removed proof script
reverseDistributesOverAppend :
  (xs,ys : List a) ->
  myreverse (xs ++ ys) = myreverse ys ++ myreverse xs
reverseDistributesOverAppend [] ys =
  sym $ appendNilRightNeutral (myreverse ys)
reverseDistributesOverAppend (p :: ps) ys =
     rewrite reverseOntoReversesOnto [p] ps
  in rewrite appendAssociative (reverseOnto [] ys) (reverseOnto [] ps) [p]
  in rewrite sym $ reverseDistributesOverAppend ps ys
  in reverseOntoReversesOnto [p] (ps ++ ys)

reverseSingletonIdentity : (x : a) -> myreverse [x] = [x]
reverseSingletonIdentity x = Refl

-- JB: removed proof script
reverseSelfInverse : (xs : List a) -> myreverse (myreverse xs) = xs
reverseSelfInverse [] = Refl
reverseSelfInverse (x :: xs) = rewrite reverseDistributesOverAppend [x] xs
  in rewrite reverseDistributesOverAppend (myreverse xs) (myreverse [x])
  in rewrite reverseSelfInverse xs
  in Refl

tailsEq' : (x, y : a) -> (xs, ys : List a) -> (x :: xs = y :: ys) -> xs = ys
tailsEq' x x ys ys Refl = Refl

-- JB: removed let
appendLeftCancel : (left : List a) -> (right : List a) -> (right' : List a) ->
                   (left ++ right = left ++ right') -> right = right'
appendLeftCancel [] right right' prf = prf
appendLeftCancel (x :: xs) right right' prf = appendLeftCancel xs right right' $
  tailsEq' x x (xs ++ right) (xs ++ right') prf

-- This part is reeeeeal ugly. Maybe someone will help me clean it up.
-- JB: removed lemmas
appendRightCancel : (left : List a) -> (left' : List a) -> (right : List a) ->
                    (left ++ right = left' ++ right) -> left = left'
appendRightCancel left left' right prf =
     rewrite sym $ reverseSelfInverse left
  in rewrite sym $ reverseSelfInverse left'
  in cong {f = myreverse} $
      appendLeftCancel (myreverse right) (myreverse left) (myreverse left') $
           rewrite sym $ reverseDistributesOverAppend left  right
        in rewrite sym $ reverseDistributesOverAppend left' right
        in cong {f = myreverse} prf

[ahmadsalim]

I think that people should be more than welcome to add the current implementations to contrib if had not already done so