fabian/veribase-idr2 - Change BJGJCKMBY65UJSUP4DGEQVR2DZAXWDJKRVOGGTKQDQ4XAMBRLRZAC

Split Data.LinkedList

Created by fabian on June 19, 2021

BJGJCKMBY65UJSUP4DGEQVR2DZAXWDJKRVOGGTKQDQ4XAMBRLRZAC

Dependencies

In channels

main

Change contents

Insertion in veribase.ipkg at line 39 [5.6174]

[3.1314]

[4.2042]


	, Data.LinkedList.Applicative
	, Data.LinkedList.Basic
	, Data.LinkedList.Equivalence
	, Data.LinkedList.Functor
	, Data.LinkedList.Group
	, Data.LinkedList.Monad

Deletion in src/Data/LinkedList.idr at line 2 [4.17]

B:BD[4.41] → [4.41:57]

B:BD[4.57] → [6.445:482]

∅:D[6.482] → [4.57:58]

B:BD[4.57] → [4.57:58]

B:BD[7.823] → [7.823:854]

B:BD[7.854] → [8.448:483]

∅:D[8.483] → [7.854:883]

B:BD[7.854] → [7.854:883]

B:BD[7.883] → [6.483:511]

B:BD[6.511] → [8.484:515]

∅:D[6.511] → [7.883:911]

∅:D[8.515] → [7.883:911]

B:BD[7.883] → [7.883:911]

∅:D[9.22] → [4.108:201]

∅:D[6.543] → [4.108:201]

∅:D[7.911] → [4.108:201]

B:BD[4.108] → [4.108:201]

B:BD[4.201] → [10.0:222]

∅:D[10.222] → [4.372:441]

B:BD[4.372] → [4.372:441]

B:BD[4.441] → [10.223:284]

∅:D[10.284] → [4.497:512]

B:BD[4.497] → [4.497:512]

B:BD[4.512] → [10.285:362]

∅:D[10.362] → [4.561:659]

B:BD[4.561] → [4.561:659]

B:BD[4.659] → [10.363:440]

∅:D[10.440] → [4.708:806]

B:BD[4.708] → [4.708:806]

B:BD[4.806] → [10.441:584]

B:BD[4.963] → [10.585:641]


import Builtin
import Algebra.Relation.Equivalence
import Algebra.Control.Functor
import Algebra.Control.Applicative
import Algebra.Control.Monad
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
%default total
infixr 7 ::
public export
data LinkedList t = Nil | (::) t (LinkedList t)
data LinkedListEquiv : Equivalence t => (a, b : LinkedList t) -> Type where
  BothEmpty : (e : Equivalence t) => LinkedListEquiv @{e} Nil Nil
  EquivHeadAndTail : (e : Equivalence t) => {a, b : t} -> {x, y : LinkedList t}
                   -> (ok1: Equiv a b) -> (ok2: LinkedListEquiv x y)
                   -> LinkedListEquiv @{e} (a :: x) (b :: y)
public export
(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} Nil (h :: t)) where
  uninhabited BothEmpty impossible
  uninhabited (EquivHeadAndTail h t) impossible
public export
(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} (h :: t) Nil) where
  uninhabited BothEmpty impossible
  uninhabited (EquivHeadAndTail h t) impossible
public export
fromNotEquivHead : (e : Equivalence t) => {a, b : t} -> (ok: Not (Equiv a b))
                 -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))
fromNotEquivHead ctr (EquivHeadAndTail prf _) = ctr prf

Replacement in src/Data/LinkedList.idr at line 3 [4.17]

B:BD[4.1018] → [4.1018:1032]

B:BD[4.1032] → [10.642:786]

B:BD[4.1168] → [4.1168:1224]

public export
fromNotEquivTail : (e : Equivalence t) => (ok: Not (LinkedListEquiv @{e} x y))
                 -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))
fromNotEquivTail ctr (EquivHeadAndTail _ prf) = ctr prf

[4.1018]

[4.1315]

import public Data.LinkedList.Basic

Replacement in src/Data/LinkedList.idr at line 5 [4.17]

B:BD[4.1316] → [10.787:887]

B:BD[10.887] → [8.516:687]

∅:D[8.687] → [10.1087:1145]

B:BD[10.1087] → [10.1087:1145]

∅:D[10.1145] → [4.1505:1566]

B:BD[4.1505] → [4.1505:1566]

B:BD[4.1566] → [10.1146:1261]

decLinkedListEquiv : (e : Equivalence t) => (a, b : LinkedList t) -> Dec (LinkedListEquiv @{e} a b)
decLinkedListEquiv Nil Nil = Yes BothEmpty
decLinkedListEquiv Nil (_::_) = No absurd
decLinkedListEquiv (_::_) Nil = No absurd
decLinkedListEquiv @{e} (h1::t1) (h2::t2) =
  case (decEquiv @{e} h1 h2, decLinkedListEquiv t1 t2) of
    (Yes prf1, Yes prf2) => Yes $ EquivHeadAndTail prf1 prf2
    (Yes prf1, No ctra2) => No $ fromNotEquivTail @{e} ctra2
    (No ctra1, _) => No $ fromNotEquivHead @{e} ctra1

[4.1316]

[10.1261]

import public Data.LinkedList.Equivalence

Replacement in src/Data/LinkedList.idr at line 7 [4.17]

B:BD[10.1262] → [10.1262:1389]

B:BD[10.1389] → [9.23:149]

public export
(Equivalence t) => Equivalence (LinkedList t) where
  Equiv    = LinkedListEquiv
  decEquiv = decLinkedListEquiv
public export
concat : LinkedList t -> LinkedList t -> LinkedList t
concat Nil     y = y
concat (x::xs) y = x :: concat xs y

[10.1262]

[9.149]

import public Data.LinkedList.Group

Replacement in src/Data/LinkedList.idr at line 9 [4.17]

B:BD[9.150] → [9.150:389]

B:BD[9.389] → [2.1838:1949]

∅:D[9.506] → [4.1718:1733]

∅:D[10.1389] → [4.1718:1733]

∅:D[2.1949] → [4.1718:1733]

B:BD[4.1718] → [4.1718:1733]

B:BD[4.1733] → [9.507:582]

B:BD[9.582] → [11.22:96]

∅:D[11.96] → [9.649:686]

B:BD[9.649] → [9.649:686]

B:BD[9.686] → [11.97:173]

∅:D[11.173] → [9.755:770]

B:BD[9.755] → [9.755:770]

∅:D[9.770] → [4.1733:1758]

B:BD[4.1733] → [4.1733:1758]

B:BD[4.1758] → [8.688:738]

∅:D[8.738] → [4.1808:1836]

B:BD[4.1808] → [4.1808:1836]

B:BD[4.1836] → [8.739:838]

∅:D[8.838] → [4.1935:1936]

B:BD[4.1935] → [4.1935:1936]

B:BD[4.1936] → [8.839:947]

∅:D[8.947] → [12.28:121]

B:BD[4.2041] → [12.28:121]

B:BD[12.121] → [8.948:986]

∅:D[8.986] → [12.157:294]

B:BD[12.157] → [12.157:294]

B:BD[12.302] → [12.302:493]

B:BD[12.493] → [8.987:1032]

∅:D[8.1032] → [12.538:795]

B:BD[12.538] → [12.538:795]

B:BD[12.795] → [8.1033:1074]

∅:D[8.1074] → [12.836:892]

B:BD[12.836] → [12.836:892]

B:BD[12.892] → [8.1075:1116]

∅:D[8.1116] → [12.892:914]

B:BD[12.892] → [12.892:914]

B:BD[12.914] → [11.174:212]

B:BD[11.212] → [6.544:598]

∅:D[6.598] → [11.271:486]

B:BD[11.271] → [11.271:486]

B:BD[11.486] → [2.1950:2169]

public export
concatNil : (l : LinkedList t) -> concat l Nil = l
concatNil Nil = Refl
concatNil (x::xs) = rewrite concatNil xs in Refl
public export
Magma (LinkedList t) where
  (<>) = concat
public export
Semigroup (LinkedList t) where
  proofAssociative Nil     _ _ = Refl
  proofAssociative (x::xs) y z = rewrite proofAssociative xs y z in Refl
public export
Monoid (LinkedList t) where
  id = Nil
  proofLeftIdentity Nil     = Refl
  proofLeftIdentity (x::xs) = rewrite Monoid.proofLeftIdentity xs in Refl
  proofRightIdentity Nil     = Refl
  proofRightIdentity (y::ys) = rewrite Monoid.proofRightIdentity ys in Refl
public export
Functor LinkedList where
  _ <$> Nil = Nil
  f <$> (h::t) = f h :: f <$> t
  proofIdentity Nil = Refl
  proofIdentity (_::t) with (proofIdentity t)
    proofIdentity (_::_) | prf = rewrite prf in Refl
  proofComposition f g Nil    = Refl
  proofComposition f g (_::t) = rewrite proofComposition f g t in Refl
public export
app : LinkedList (a -> b) -> LinkedList a -> LinkedList b
app Nil     _ = Nil
app (f::fs) l = (f <$> l) <> app fs l
public export
appNil : (f : LinkedList (a -> b)) -> f `app` Nil = Nil
appNil Nil     = Refl
appNil (f::fs) = rewrite appNil fs in Refl
public export
Applicative LinkedList where
  pure x = [x]
  (<*>) = app
  proofIdentity Nil = Refl
  proofIdentity (_::xs) with (Functor.proofIdentity xs)
    proofIdentity (_::xs) | prf =
      rewrite concatNil (identity <$> xs) in
      rewrite prf in Refl
  proofHomomorphism f x = Refl
  proofInterchange Nil x = Refl
  proofInterchange (f::fs) x = rewrite proofInterchange fs x in Refl
  proofComposition Nil Nil _ = Refl
  proofComposition Nil (_::gs) _ =
    rewrite appNil gs in
    -- rewrite concatNil ((.) <$> gs) in
    ?holeComposition1
  proofComposition (f::fs) gs _ =
    -- rewrite concatNil ((.) <$> gs) in
    ?holeComposition2
public export
Monad LinkedList where
  Nil >>= _ = Nil
  (x::xs) >>= f = f x <> (xs >>= f)
  proofLeftIdentity x f = rewrite concatNil (f x) in Refl
  proofRightIdentity Nil = Refl
  proofRightIdentity (x::xs) with (Monad.proofRightIdentity xs)
    proofRightIdentity (_::_) | prf = rewrite prf in Refl
  proofAssociative Nil f g = Refl
  proofAssociative (x::xs) f g with (f x)
    proofAssociative (x::xs) f g | Nil = rewrite proofAssociative xs f g in Refl
    proofAssociative (x::xs) f g | (r::rs) = ?holeAssociative

[9.150]

import public Data.LinkedList.Functor
import public Data.LinkedList.Applicative
import public Data.LinkedList.Monad

File addition: LinkedList (d--x------)
[5.14]

File addition: Monad.idr (----------)

[0.413]

module Data.LinkedList.Monad
import Builtin
import Algebra.Control.Applicative
import Algebra.Control.Monad
import public Data.LinkedList.Basic
import public Data.LinkedList.Applicative
public export
Monad LinkedList where
  Nil >>= _ = Nil
  (x::xs) >>= f = f x `concat` (xs >>= f)
  proofLeftIdentity x f = rewrite proofConcatRightIdentity (f x) in Refl
  proofRightIdentity Nil = Refl
  proofRightIdentity (x::xs) with (Monad.proofRightIdentity xs)
    proofRightIdentity (_::_) | prf = rewrite prf in Refl
  proofAssociative Nil f g = Refl
  proofAssociative (x::xs) f g = case f x of
    Nil     => ?holeAssociative1
    (r::rs) => ?holeAssociative2

File addition: Group.idr (----------)

[0.413]

module Data.LinkedList.Group
import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
import public Data.LinkedList.Basic
%default total
public export
Magma (LinkedList t) where
  (<>) = concat
public export
Semigroup (LinkedList t) where
  proofAssociative Nil     _ _ = Refl
  proofAssociative (x::xs) y z = rewrite proofAssociative xs y z in Refl
public export
Monoid (LinkedList t) where
  id = Nil
  proofLeftIdentity Nil     = Refl
  proofLeftIdentity (x::xs) = rewrite Monoid.proofLeftIdentity xs in Refl
  proofRightIdentity Nil     = Refl
  proofRightIdentity (y::ys) = rewrite Monoid.proofRightIdentity ys in Refl

File addition: Functor.idr (----------)

[0.413]

module Data.LinkedList.Functor
import Builtin
import Algebra.Control.Functor
import public Data.LinkedList.Basic
public export
Functor LinkedList where
  _ <$> Nil = Nil
  f <$> (h::t) = f h :: f <$> t
  proofIdentity Nil = Refl
  proofIdentity (_::t) with (proofIdentity t)
    proofIdentity (_::_) | prf = rewrite prf in Refl
  proofComposition f g Nil    = Refl
  proofComposition f g (_::t) = rewrite proofComposition f g t in Refl

File addition: Equivalence.idr (----------)

[0.413]

module Data.LinkedList.Equivalence
import Builtin
import Algebra.Relation.Equivalence
import public Data.LinkedList.Basic
%default total
public export
data LinkedListEquiv : Equivalence t => (a, b : LinkedList t) -> Type where
  BothEmpty : (e : Equivalence t) => LinkedListEquiv @{e} Nil Nil
  EquivHeadAndTail : (e : Equivalence t) => {a, b : t} -> {x, y : LinkedList t}
                   -> (ok1: Equiv a b) -> (ok2: LinkedListEquiv x y)
                   -> LinkedListEquiv @{e} (a :: x) (b :: y)
public export
(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} Nil (h :: t)) where
  uninhabited BothEmpty impossible
  uninhabited (EquivHeadAndTail h t) impossible
public export
(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} (h :: t) Nil) where
  uninhabited BothEmpty impossible
  uninhabited (EquivHeadAndTail h t) impossible
public export
fromNotEquivHead : (e : Equivalence t) => {a, b : t} -> (ok: Not (Equiv a b))
                 -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))
fromNotEquivHead ctr (EquivHeadAndTail prf _) = ctr prf
public export
fromNotEquivTail : (e : Equivalence t) => (ok: Not (LinkedListEquiv @{e} x y))
                 -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))
fromNotEquivTail ctr (EquivHeadAndTail _ prf) = ctr prf
decLinkedListEquiv : (e : Equivalence t) => (a, b : LinkedList t)
                   -> Dec (LinkedListEquiv @{e} a b)
decLinkedListEquiv Nil Nil = Yes BothEmpty
decLinkedListEquiv Nil (_::_) = No absurd
decLinkedListEquiv (_::_) Nil = No absurd
decLinkedListEquiv @{e} (h1::t1) (h2::t2) =
  case (decEquiv @{e} h1 h2, decLinkedListEquiv t1 t2) of
    (Yes prf1, Yes prf2) => Yes $ EquivHeadAndTail prf1 prf2
    (Yes prf1, No ctra2) => No $ fromNotEquivTail @{e} ctra2
    (No ctra1, _) => No $ fromNotEquivHead @{e} ctra1
public export
(Equivalence t) => Equivalence (LinkedList t) where
  Equiv    = LinkedListEquiv
  decEquiv = decLinkedListEquiv

File addition: Basic.idr (----------)

[0.413]

module Data.LinkedList.Basic
import Builtin
%default total
infixr 7 ::
public export
data LinkedList t = Nil | (::) t (LinkedList t)
public export
concat : LinkedList t -> LinkedList t -> LinkedList t
concat Nil     y = y
concat (x::xs) y = x :: concat xs y
export
proofConcatRightIdentity : (l : LinkedList t) -> concat l Nil = l
proofConcatRightIdentity Nil = Refl
proofConcatRightIdentity (x::xs) = rewrite proofConcatRightIdentity xs in Refl

File addition: Applicative.idr (----------)

[0.413]

module Data.LinkedList.Applicative
import Builtin
import Algebra.Control.Functor
import Algebra.Control.Applicative
import public Data.LinkedList.Basic
import public Data.LinkedList.Functor
%default total
public export
app : LinkedList (a -> b) -> LinkedList a -> LinkedList b
app Nil     _ = Nil
app (f::fs) l = (f <$> l) `concat` app fs l
public export
appNil : (f : LinkedList (a -> b)) -> f `app` Nil = Nil
appNil Nil     = Refl
appNil (f::fs) = rewrite appNil fs in Refl
public export
Applicative LinkedList where
  pure x = [x]
  (<*>) = app
  proofIdentity Nil = Refl
  proofIdentity (_::xs) with (Functor.proofIdentity xs)
    proofIdentity (_::xs) | prf =
      rewrite proofConcatRightIdentity (identity <$> xs) in
      rewrite prf in Refl
  proofHomomorphism f x = Refl
  proofInterchange Nil x = Refl
  proofInterchange (f::fs) x = rewrite proofInterchange fs x in Refl
  proofComposition Nil Nil _ = Refl
  proofComposition Nil (_::gs) _ =
    rewrite appNil gs in
    -- rewrite proofConcatRightIdentity ((.) <$> gs) in
    ?holeComposition1
  proofComposition (f::fs) gs _ =
    -- rewrite proofConcatRightIdentity ((.) <$> gs) in
    ?holeComposition2

Split Data.LinkedList

Dependencies

In channels

Change contents

Insertion in veribase.ipkg at line 39 [5.6174]

Deletion in src/Data/LinkedList.idr at line 2 [4.17]

Replacement in src/Data/LinkedList.idr at line 3 [4.17]

Replacement in src/Data/LinkedList.idr at line 5 [4.17]

Replacement in src/Data/LinkedList.idr at line 7 [4.17]

Replacement in src/Data/LinkedList.idr at line 9 [4.17]

File addition: LinkedList (d--x------)

File addition: Monad.idr (----------)

File addition: Group.idr (----------)

File addition: Functor.idr (----------)

File addition: Equivalence.idr (----------)

File addition: Basic.idr (----------)

File addition: Applicative.idr (----------)