text:
module Data.Buffer

import System.Directory
import System.File
import System.FFI

import Data.List

%default total

-- Reading and writing binary buffers. Note that this primitives are unsafe,
-- in that they don't check that buffer locations are within bounds.
-- We really need a safe wrapper!
-- They are used in the Idris compiler itself for reading/writing checked
-- files.

-- This is known to the compiler, so maybe ought to be moved to Builtin
export
data Buffer : Type where [external]

bufferClass : String
bufferClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer"

stringsClass : String
stringsClass = "io/github/mmhelloworld/idrisjvm/runtime/Strings"

%foreign "scheme:blodwen-buffer-size"
         "RefC:getBufferSize"
         "node:lambda:b => BigInt(b.length)"
         jvm bufferClass "size"
prim__bufferSize : Buffer -> Int

export %inline
rawSize : HasIO io => Buffer -> io Int
rawSize buf = pure (prim__bufferSize buf)

%foreign "scheme:blodwen-new-buffer"
         "RefC:newBuffer"
         "node:lambda:s=>Buffer.alloc(Number(s))"
         jvm bufferClass "create"
prim__newBuffer : Int -> PrimIO Buffer

export
newBuffer : HasIO io => Int -> io (Maybe Buffer)
newBuffer size
    = if size >= 0
            then do buf <- primIO (prim__newBuffer size)
                    pure $ Just buf
                 else pure Nothing
--          if prim__nullAnyPtr buf /= 0
--             then pure Nothing
--             else pure $ Just $ MkBuffer buf size 0

%foreign "scheme:blodwen-buffer-setbyte"
         "RefC:setBufferByte"
         "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))"
         jvm bufferClass "setByte"
prim__setByte : Buffer -> Int -> Int -> PrimIO ()

%foreign "scheme:blodwen-buffer-setbyte"
         "RefC:setBufferByte"
         "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))"
         jvm bufferClass "setByte"
prim__setBits8 : Buffer -> Int -> Bits8 -> PrimIO ()

-- Assumes val is in the range 0-255
export %inline
setByte : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setByte buf loc val
    = primIO (prim__setByte buf loc val)

export %inline
setBits8 : HasIO io => Buffer -> (loc : Int) -> (val : Bits8) -> io ()
setBits8 buf loc val
    = primIO (prim__setBits8 buf loc val)

%foreign "scheme:blodwen-buffer-getbyte"
         "RefC:getBufferByte"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))"
         jvm bufferClass "getByte"
prim__getByte : Buffer -> Int -> PrimIO Int

%foreign "scheme:blodwen-buffer-getbyte"
         "RefC:getBufferByte"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))"
         jvm bufferClass "getByte"
prim__getBits8 : Buffer -> Int -> PrimIO Bits8

export %inline
getByte : HasIO io => Buffer -> (loc : Int) -> io Int
getByte buf loc
    = primIO (prim__getByte buf loc)

export %inline
getBits8 : HasIO io => Buffer -> (loc : Int) -> io Bits8
getBits8 buf loc
    = primIO (prim__getBits8 buf loc)

%foreign "scheme:blodwen-buffer-setbits16"
         "node:lambda:(buf,offset,value)=>buf.writeUInt16LE(Number(value), Number(offset))"
         jvm bufferClass "setShort"
prim__setBits16 : Buffer -> Int -> Bits16 -> PrimIO ()

export %inline
setBits16 : HasIO io => Buffer -> (loc : Int) -> (val : Bits16) -> io ()
setBits16 buf loc val
    = primIO (prim__setBits16 buf loc val)

%foreign "scheme:blodwen-buffer-getbits16"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt16LE(Number(offset)))"
         jvm bufferClass "getShort"
prim__getBits16 : Buffer -> Int -> PrimIO Bits16

export %inline
getBits16 : HasIO io => Buffer -> (loc : Int) -> io Bits16
getBits16 buf loc
    = primIO (prim__getBits16 buf loc)

%foreign "scheme:blodwen-buffer-setbits32"
         "node:lambda:(buf,offset,value)=>buf.writeUInt32LE(Number(value), Number(offset))"
         jvm bufferClass "setInt"
prim__setBits32 : Buffer -> Int -> Bits32 -> PrimIO ()

export %inline
setBits32 : HasIO io => Buffer -> (loc : Int) -> (val : Bits32) -> io ()
setBits32 buf loc val
    = primIO (prim__setBits32 buf loc val)

%foreign "scheme:blodwen-buffer-getbits32"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt32LE(Number(offset)))"
         jvm bufferClass "getInt"
prim__getBits32 : Buffer -> Int -> PrimIO Bits32

export %inline
getBits32 : HasIO io => Buffer -> (loc : Int) -> io Bits32
getBits32 buf loc
    = primIO (prim__getBits32 buf loc)

%foreign "scheme:blodwen-buffer-setbits64"
         jvm bufferClass "setLong"
prim__setBits64 : Buffer -> Int -> Bits64 -> PrimIO ()

export %inline
setBits64 : HasIO io => Buffer -> (loc : Int) -> (val : Bits64) -> io ()
setBits64 buf loc val
    = primIO (prim__setBits64 buf loc val)

%foreign "scheme:blodwen-buffer-getbits64"
         jvm bufferClass "getLong"
prim__getBits64 : Buffer -> Int -> PrimIO Bits64

export %inline
getBits64 : HasIO io => Buffer -> (loc : Int) -> io Bits64
getBits64 buf loc
    = primIO (prim__getBits64 buf loc)

%foreign "scheme:blodwen-buffer-setint32"
         "node:lambda:(buf,offset,value)=>buf.writeInt32LE(Number(value), Number(offset))"
         jvm bufferClass "setInt"
prim__setInt32 : Buffer -> Int -> Int -> PrimIO ()

export %inline
setInt32 : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt32 buf loc val
    = primIO (prim__setInt32 buf loc val)

%foreign "scheme:blodwen-buffer-getint32"
         "node:lambda:(buf,offset)=>BigInt(buf.readInt32LE(Number(offset)))"
         jvm bufferClass "getInt"
prim__getInt32 : Buffer -> Int -> PrimIO Int

export %inline
getInt32 : HasIO io => Buffer -> (loc : Int) -> io Int
getInt32 buf loc
    = primIO (prim__getInt32 buf loc)

%foreign "scheme:blodwen-buffer-setint"
         "RefC:setBufferInt"
         "node:lambda:(buf,offset,value)=>buf.writeInt64(Number(value), Number(offset))"
         jvm bufferClass "setInt"
prim__setInt : Buffer -> Int -> Int -> PrimIO ()

export %inline
setInt : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt buf loc val
    = primIO (prim__setInt buf loc val)

%foreign "scheme:blodwen-buffer-getint"
         "RefC:getBufferInt"
         "node:lambda:(buf,offset)=>BigInt(buf.readInt64(Number(offset)))"
         jvm bufferClass "getInt"
prim__getInt : Buffer -> Int -> PrimIO Int

export %inline
getInt : HasIO io => Buffer -> (loc : Int) -> io Int
getInt buf loc
    = primIO (prim__getInt buf loc)

%foreign "scheme:blodwen-buffer-setdouble"
         "RefC:setBufferDouble"
         "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, Number(offset))"
         jvm bufferClass "setDouble"
prim__setDouble : Buffer -> Int -> Double -> PrimIO ()

export %inline
setDouble : HasIO io => Buffer -> (loc : Int) -> (val : Double) -> io ()
setDouble buf loc val
    = primIO (prim__setDouble buf loc val)

%foreign "scheme:blodwen-buffer-getdouble"
         "RefC:getBufferDouble"
         "node:lambda:(buf,offset)=>buf.readDoubleLE(Number(offset))"
         jvm bufferClass "getDouble"
prim__getDouble : Buffer -> Int -> PrimIO Double

export %inline
getDouble : HasIO io => Buffer -> (loc : Int) -> io Double
getDouble buf loc
    = primIO (prim__getDouble buf loc)

-- Get the length of a string in bytes, rather than characters
export
%foreign
    "C:strlen,libc 6"
    jvm stringsClass "bytesLengthUtf8"
stringByteLength : String -> Int

%foreign "scheme:blodwen-buffer-setstring"
         "RefC:setBufferString"
         "node:lambda:(buf,offset,value)=>buf.write(value, Number(offset),buf.length - Number(offset), 'utf-8')"
         jvm bufferClass "setString"
prim__setString : Buffer -> Int -> String -> PrimIO ()

export %inline
setString : HasIO io => Buffer -> (loc : Int) -> (val : String) -> io ()
setString buf loc val
    = primIO (prim__setString buf loc val)

%foreign "scheme:blodwen-buffer-getstring"
         "RefC:getBufferString"
         "node:lambda:(buf,offset,len)=>buf.slice(Number(offset), Number(offset+len)).toString('utf-8')"
         jvm bufferClass "getString"
prim__getString : Buffer -> Int -> Int -> PrimIO String

export %inline
getString : HasIO io => Buffer -> (loc : Int) -> (len : Int) -> io String
getString buf loc len
    = primIO (prim__getString buf loc len)

export
covering
bufferData : HasIO io => Buffer -> io (List Int)
bufferData buf
    = do len <- rawSize buf
         unpackTo [] len
  where
    covering
    unpackTo : List Int -> Int -> io (List Int)
    unpackTo acc 0 = pure acc
    unpackTo acc loc
        = do val <- getByte buf (loc - 1)
             unpackTo (val :: acc) (loc - 1)

%foreign "scheme:blodwen-buffer-copydata"
         "RefC:copyBuffer"
         "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,Number(o2), Number(o1), Number(o1+length))"
         jvm bufferClass "copy"
prim__copyData : Buffer -> Int -> Int -> Buffer -> Int -> PrimIO ()

export
copyData : HasIO io => (src : Buffer) -> (start, len : Int) ->
           (dest : Buffer) -> (loc : Int) -> io ()
copyData src start len dest loc
    = primIO (prim__copyData src start len dest loc)

%foreign "C:idris2_readBufferData, libidris2_support, idris_file.h"
         "RefC:readBufferData"
         "node:lambda:(f,b,l,m) => BigInt(require('fs').readSync(f.fd,b,Number(l), Number(m)))"
         "jvm:readFromFile(java/nio/channels/ReadableByteChannel io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer int int int),io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer"
prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int

%foreign "C:idris2_writeBufferData, libidris2_support, idris_file.h"
         "RefC:writeBufferData"
         "node:lambda:(f,b,l,m) => BigInt(require('fs').writeSync(f.fd,b,Number(l), Number(m)))"
         "jvm:writeToFile(java/nio/channels/WritableByteChannel io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer int int int),io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer"
prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int

export
readBufferData : HasIO io => File -> Buffer ->
                 (loc : Int) -> -- position in buffer to start adding
                 (maxbytes : Int) -> -- maximums size to read, which must not
                                     -- exceed buffer length
                 io (Either FileError ())
readBufferData (FHandle h) buf loc max
    = do read <- primIO (prim__readBufferData h buf loc max)
         if read >= 0
            then pure (Right ())
            else pure (Left FileReadError)

export
writeBufferData : HasIO io => File -> Buffer ->
                  (loc : Int) -> -- position in buffer to write from
                  (maxbytes : Int) -> -- maximums size to write, which must not
                                      -- exceed buffer length
                  io (Either FileError ())
writeBufferData (FHandle h) buf loc max
    = do written <- primIO (prim__writeBufferData h buf loc max)
         if written >= 0
            then pure (Right ())
            else pure (Left FileWriteError)

export
writeBufferToFile : HasIO io => String -> Buffer -> Int -> io (Either FileError ())
writeBufferToFile fn buf max
    = do Right f <- openFile fn WriteTruncate
             | Left err => pure (Left err)
         Right ok <- writeBufferData f buf 0 max
             | Left err => pure (Left err)
         closeFile f
         pure (Right ok)

export
createBufferFromFile : HasIO io => String -> io (Either FileError Buffer)
createBufferFromFile fn
    = do Right f <- openFile fn Read
             | Left err => pure (Left err)
         Right size <- fileSize f
             | Left err => pure (Left err)
         Just buf <- newBuffer size
             | Nothing => pure (Left FileReadError)
         Right ok <- readBufferData f buf 0 size
             | Left err => pure (Left err)
         closeFile f
         pure (Right buf)

export
resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
resizeBuffer old newsize
    = do Just buf <- newBuffer newsize
              | Nothing => pure Nothing
         -- If the new buffer is smaller than the old one, just copy what
         -- fits
         oldsize <- rawSize old
         let len = if newsize < oldsize then newsize else oldsize
         copyData old 0 len buf 0
         pure (Just buf)

||| Create a buffer containing the concatenated content from a
||| list of buffers.
export
concatBuffers : HasIO io => List Buffer -> io (Maybe Buffer)
concatBuffers xs
    = do let sizes = map prim__bufferSize xs
         let (totalSize, revCumulative) = foldl scanSize (0,[]) sizes
         let cumulative = reverse revCumulative
         Just buf <- newBuffer totalSize
              | Nothing => pure Nothing
         traverse_ (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative)
         pure (Just buf)
    where
        scanSize : (Int, List Int) -> Int -> (Int, List Int)
        scanSize (s, cs) x  = (s+x, s::cs)

||| Split a buffer into two at a position.
export
splitBuffer : HasIO io => Buffer -> Int -> io (Maybe (Buffer, Buffer))
splitBuffer buf pos = do size <- rawSize buf
                         if pos > 0 && pos < size
                             then do Just first <- newBuffer pos
                                        | Nothing => pure Nothing
                                     Just second <- newBuffer (size - pos)
                                        | Nothing => pure Nothing
                                     copyData buf 0 pos first 0
                                     copyData buf pos (size-pos) second 0
                                     pure $ Just (first, second)
                             else pure Nothing

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Web.Internal.FetchTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace RequestDestination

  public export
  data RequestDestination = Empty
                          | Audio
                          | Audioworklet
                          | Document
                          | Embed
                          | Font
                          | Frame
                          | Iframe
                          | Image
                          | Manifest
                          | Object
                          | Paintworklet
                          | Report
                          | Script
                          | Sharedworker
                          | Style
                          | Track
                          | Video
                          | Worker
                          | Xslt

  public export
  Show RequestDestination where
    show Empty = ""
    show Audio = "audio"
    show Audioworklet = "audioworklet"
    show Document = "document"
    show Embed = "embed"
    show Font = "font"
    show Frame = "frame"
    show Iframe = "iframe"
    show Image = "image"
    show Manifest = "manifest"
    show Object = "object"
    show Paintworklet = "paintworklet"
    show Report = "report"
    show Script = "script"
    show Sharedworker = "sharedworker"
    show Style = "style"
    show Track = "track"
    show Video = "video"
    show Worker = "worker"
    show Xslt = "xslt"

  public export
  Eq RequestDestination where
    (==) = (==) `on` show

  public export
  Ord RequestDestination where
    compare = compare `on` show

  public export
  read : String -> Maybe RequestDestination
  read "" = Just Empty
  read "audio" = Just Audio
  read "audioworklet" = Just Audioworklet
  read "document" = Just Document
  read "embed" = Just Embed
  read "font" = Just Font
  read "frame" = Just Frame
  read "iframe" = Just Iframe
  read "image" = Just Image
  read "manifest" = Just Manifest
  read "object" = Just Object
  read "paintworklet" = Just Paintworklet
  read "report" = Just Report
  read "script" = Just Script
  read "sharedworker" = Just Sharedworker
  read "style" = Just Style
  read "track" = Just Track
  read "video" = Just Video
  read "worker" = Just Worker
  read "xslt" = Just Xslt
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (RequestDestination.read s)}
             -> RequestDestination
  fromString s = fromJust $ read s

  export
  ToFFI RequestDestination String where
    toFFI = show

  export
  FromFFI RequestDestination String where
    fromFFI = read

namespace RequestMode

  public export
  data RequestMode = Navigate | SameOrigin | NoCors | Cors

  public export
  Show RequestMode where
    show Navigate = "navigate"
    show SameOrigin = "same-origin"
    show NoCors = "no-cors"
    show Cors = "cors"

  public export
  Eq RequestMode where
    (==) = (==) `on` show

  public export
  Ord RequestMode where
    compare = compare `on` show

  public export
  read : String -> Maybe RequestMode
  read "navigate" = Just Navigate
  read "same-origin" = Just SameOrigin
  read "no-cors" = Just NoCors
  read "cors" = Just Cors
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (RequestMode.read s)}
             -> RequestMode
  fromString s = fromJust $ read s

  export
  ToFFI RequestMode String where
    toFFI = show

  export
  FromFFI RequestMode String where
    fromFFI = read

namespace RequestCredentials

  public export
  data RequestCredentials = Omit | SameOrigin | Include

  public export
  Show RequestCredentials where
    show Omit = "omit"
    show SameOrigin = "same-origin"
    show Include = "include"

  public export
  Eq RequestCredentials where
    (==) = (==) `on` show

  public export
  Ord RequestCredentials where
    compare = compare `on` show

  public export
  read : String -> Maybe RequestCredentials
  read "omit" = Just Omit
  read "same-origin" = Just SameOrigin
  read "include" = Just Include
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (RequestCredentials.read s)}
             -> RequestCredentials
  fromString s = fromJust $ read s

  export
  ToFFI RequestCredentials String where
    toFFI = show

  export
  FromFFI RequestCredentials String where
    fromFFI = read

namespace RequestCache

  public export
  data RequestCache = Default
                    | NoStore
                    | Reload
                    | NoCache
                    | ForceCache
                    | OnlyIfCached

  public export
  Show RequestCache where
    show Default = "default"
    show NoStore = "no-store"
    show Reload = "reload"
    show NoCache = "no-cache"
    show ForceCache = "force-cache"
    show OnlyIfCached = "only-if-cached"

  public export
  Eq RequestCache where
    (==) = (==) `on` show

  public export
  Ord RequestCache where
    compare = compare `on` show

  public export
  read : String -> Maybe RequestCache
  read "default" = Just Default
  read "no-store" = Just NoStore
  read "reload" = Just Reload
  read "no-cache" = Just NoCache
  read "force-cache" = Just ForceCache
  read "only-if-cached" = Just OnlyIfCached
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (RequestCache.read s)}
             -> RequestCache
  fromString s = fromJust $ read s

  export
  ToFFI RequestCache String where
    toFFI = show

  export
  FromFFI RequestCache String where
    fromFFI = read

namespace RequestRedirect

  public export
  data RequestRedirect = Follow | Error | Manual

  public export
  Show RequestRedirect where
    show Follow = "follow"
    show Error = "error"
    show Manual = "manual"

  public export
  Eq RequestRedirect where
    (==) = (==) `on` show

  public export
  Ord RequestRedirect where
    compare = compare `on` show

  public export
  read : String -> Maybe RequestRedirect
  read "follow" = Just Follow
  read "error" = Just Error
  read "manual" = Just Manual
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (RequestRedirect.read s)}
             -> RequestRedirect
  fromString s = fromJust $ read s

  export
  ToFFI RequestRedirect String where
    toFFI = show

  export
  FromFFI RequestRedirect String where
    fromFFI = read

namespace ResponseType

  public export
  data ResponseType = Basic | Cors | Default | Error | Opaque | Opaqueredirect

  public export
  Show ResponseType where
    show Basic = "basic"
    show Cors = "cors"
    show Default = "default"
    show Error = "error"
    show Opaque = "opaque"
    show Opaqueredirect = "opaqueredirect"

  public export
  Eq ResponseType where
    (==) = (==) `on` show

  public export
  Ord ResponseType where
    compare = compare `on` show

  public export
  read : String -> Maybe ResponseType
  read "basic" = Just Basic
  read "cors" = Just Cors
  read "default" = Just Default
  read "error" = Just Error
  read "opaque" = Just Opaque
  read "opaqueredirect" = Just Opaqueredirect
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ResponseType.read s)}
             -> ResponseType
  fromString s = fromJust $ read s

  export
  ToFFI ResponseType String where
    toFFI = show

  export
  FromFFI ResponseType String where
    fromFFI = read

namespace ReferrerPolicy

  public export
  data ReferrerPolicy = Empty
                      | NoReferrer
                      | NoReferrerWhenDowngrade
                      | SameOrigin
                      | Origin
                      | StrictOrigin
                      | OriginWhenCrossOrigin
                      | StrictOriginWhenCrossOrigin
                      | UnsafeUrl

  public export
  Show ReferrerPolicy where
    show Empty = ""
    show NoReferrer = "no-referrer"
    show NoReferrerWhenDowngrade = "no-referrer-when-downgrade"
    show SameOrigin = "same-origin"
    show Origin = "origin"
    show StrictOrigin = "strict-origin"
    show OriginWhenCrossOrigin = "origin-when-cross-origin"
    show StrictOriginWhenCrossOrigin = "strict-origin-when-cross-origin"
    show UnsafeUrl = "unsafe-url"

  public export
  Eq ReferrerPolicy where
    (==) = (==) `on` show

  public export
  Ord ReferrerPolicy where
    compare = compare `on` show

  public export
  read : String -> Maybe ReferrerPolicy
  read "" = Just Empty
  read "no-referrer" = Just NoReferrer
  read "no-referrer-when-downgrade" = Just NoReferrerWhenDowngrade
  read "same-origin" = Just SameOrigin
  read "origin" = Just Origin
  read "strict-origin" = Just StrictOrigin
  read "origin-when-cross-origin" = Just OriginWhenCrossOrigin
  read "strict-origin-when-cross-origin" = Just StrictOriginWhenCrossOrigin
  read "unsafe-url" = Just UnsafeUrl
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ReferrerPolicy.read s)}
             -> ReferrerPolicy
  fromString s = fromJust $ read s

  export
  ToFFI ReferrerPolicy String where
    toFFI = show

  export
  FromFFI ReferrerPolicy String where
    fromFFI = read

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data Headers : Type where [external]

export
ToFFI Headers Headers where toFFI = id

export
FromFFI Headers Headers where fromFFI = Just

export
SafeCast Headers where
  safeCast = unsafeCastOnPrototypeName "Headers"

export data Request : Type where [external]

export
ToFFI Request Request where toFFI = id

export
FromFFI Request Request where fromFFI = Just

export
SafeCast Request where
  safeCast = unsafeCastOnPrototypeName "Request"

export data Response : Type where [external]

export
ToFFI Response Response where toFFI = id

export
FromFFI Response Response where fromFFI = Just

export
SafeCast Response where
  safeCast = unsafeCastOnPrototypeName "Response"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data RequestInit : Type where [external]

export
ToFFI RequestInit RequestInit where toFFI = id

export
FromFFI RequestInit RequestInit where fromFFI = Just

export data ResponseInit : Type where [external]

export
ToFFI ResponseInit ResponseInit where toFFI = id

export
FromFFI ResponseInit ResponseInit where fromFFI = Just

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

export data Body : Type where [external]

export
ToFFI Body Body where toFFI = id

export
FromFFI Body Body where fromFFI = Just

ext: idr


text:
= Tactics : More Basic Tactics

This chapter introduces several additional proof strategies and tactics that
allow us to begin proving more interesting properties of functional programs. We
will see:

  - how to use auxiliary lemmas in both "forward-style" and "backward-style"
    proofs;

  - how to reason about data constructors (in particular, how to use the fact
    that they are injective and disjoint);

  - how to strengthen an induction hypothesis (and when such strengthening is
    required); and

  - more details on how to reason by case analysis.

> module Tactics
>
> import Basics
> import Induction

> import Pruviloj
>
> %access public export
>
> %default total
>
> %language ElabReflection
>

== The \idr{exact} Tactic

We often encounter situations where the goal to be proved is _exactly_ the same
as some hypothesis in the context or some previously proved lemma.

> silly1 : (n, m, o, p : Nat) -> (n = m) -> [n,o] = [n,p] -> [n,o] = [m,p]

Here, we could prove this with rewrites:

> silly1 n m o p eq1 eq2 = rewrite eq2 in
>                          rewrite eq1 in Refl

or the dependent pattern matching:

```idris
silly1 n n o o Refl Refl = Refl
```

\todo[inline]{Write more about dependent pattern matching techinque. Maybe move
to an earlier chapter?}

as we have done several times before. We can achieve the same effect by a series
of tactic applications, using \idr{exact} instead of the
\idr{rewrite}+\idr{Refl} combination:

\todo[inline]{Explain \idr{intros} (move text from `Basics`?), \idr{Var} and
\idr{rewriteWith}. Explain the "backwards" order.}

\todo[inline]{\idr{| _ => fail []} is needed for totality}

> silly1' : (n, m, o, p : Nat) -> (n = m) -> [n,o] = [n,p] -> [n,o] = [m,p]
> silly1' = %runElab silly1_tac
> where
>   silly1_tac : Elab ()
>   silly1_tac = do
>     [n,m,o,p,eq1,eq2] <- intros
>       | _ => fail []
>     rewriteWith $ Var eq1
>     exact $ Var eq2

(This tactic is called `apply` in Coq.)

\todo[inline]{The following doesn't seem to hold in Idris, you have to manually
apply things with \idr{RApp} for \idr{exact} to work. Maybe there's another
tactic?}

The \idr{exact} tactic also works with _conditional_ hypotheses and lemmas: if the
statement being applied is an implication, then the premises of this implication
will be added to the list of subgoals needing to be proved.

> silly2 : (n, m, o, p : Nat) -> (n = m) ->
>          ((q, r : Nat) -> q = r -> [q,o] = [r,p]) ->
>          [n,o] = [m,p]
> silly2 = %runElab silly2_tac
> where
>   silly2_tac : Elab ()
>   silly2_tac = do
>     [n,m,o,p,eq1,eq2] <- intros
>       | _ => fail []
>     exact $ (((Var eq2) `RApp` (Var n)) `RApp` (Var m)) `RApp` (Var eq1)

You may find it instructive to experiment with this proof and see if there is a
way to complete it using just \idr{rewrite} instead of \idr{exact}.

\todo[inline]{Edit}

Typically, when we use \idr{exact h}, the statement \idr{h} will begin with a
`(...)` that binds some _universal variables_. When Idris matches the current
goal against the conclusion of \idr{h}, it will try to find appropriate values
for these variables. For example, when we do \idr{exact $ Var eq2} in the
following proof, the universal variable \idr{q} in \idr{eq2} gets instantiated
with \idr{n} and \idr{r} gets instantiated with \idr{m}.

> silly2a : (n, m : Nat) -> (n,n) = (m,m) ->
>           ((q, r : Nat) -> (q,q) = (r,r) -> [q] = [r]) ->
>           [n] = [m]
> silly2a = %runElab silly2a_tac
> where
>   silly2a_tac : Elab ()
>   silly2a_tac = do
>     [n,m,eq1,eq2] <- intros
>       | _ => fail []
>     exact $ (((Var eq2) `RApp` (Var n)) `RApp` (Var m)) `RApp` (Var eq1)

==== Exercise: 2 stars, optional (silly_ex)

Complete the following proof without using `simpl`.

> silly_ex : ((n : Nat) -> evenb n = True -> oddb (S n) = True)
>            -> evenb 3 = True -> oddb 4 = True
> silly_ex = ?remove_me -- %runElab silly_ex_tac
> where
>   silly_ex_tac : Elab ()
>   silly_ex_tac = ?silly_ex_tac_rhs

$\square$

To use the \idr{exact} tactic, the (conclusion of the) fact being applied must
match the goal exactly -- for example, \idr{exact} will not work if the left and
right sides of the equality are swapped.

> silly3_firsttry : (n : Nat) -> True = n == 5 ->
>                   (S (S n)) == 7 = True
> silly3_firsttry = %runElab silly3_firsttry_tac
> where
>   silly3_firsttry_tac : Elab ()
>   silly3_firsttry_tac = do
>    [_,h] <- intros
>       | _ => fail []

Here we cannot use \idr{exact} directly, but we can use the \idr{symmetry}
tactic, which switches the left and right sides of an equality in the goal.

>    symmetry
>    exact $ Var h

==== Exercise: 3 stars (apply_exercise1)

(_Hint_: You can use \idr{exact} with previously defined lemmas, not just
hypotheses in the context. Remember that `:search` is your friend.)

> rev : (l : List x) -> List x
> rev [] = []
> rev (h::t) = (rev t) ++ [h]

> rev_exercise1 : (l, l' : List Nat) -> l = rev l' -> l' = rev l
> rev_exercise1 = ?remove_me1 -- %runElab rev_exercise1_tac
> where
>   rev_exercise1_tac : Elab ()
>   rev_exercise1_tac = ?rev_exercise1_tac_rhs

$\square$

==== Exercise: 1 star, optional (apply_rewrite)

Briefly explain the difference between the tactics \idr{exact} and
\idr{rewriteWith}. What are the situations where both can usefully be applied?

> -- FILL IN HERE

$\square$

== The \idr{apply} Tactic

The following silly example uses two rewrites in a row to get from `[a,b]` to
`[e,f]`.

> trans_eq_example : (a, b, c, d, e, f : Nat) ->
>                    [a,b] = [c,d] -> [c,d] = [e,f] -> [a,b] = [e,f]
> trans_eq_example a b c d e f eq1 eq2 = rewrite eq1 in
>                                        rewrite eq2 in Refl

Note that this can also be proven with dependent pattern matching:

```idris
trans_eq_example a b a b a b Refl Refl = Refl
```

Since this is a common pattern, we might like to pull it out as a lemma
recording, once and for all, the fact that equality is transitive.

> trans_eq : (n, m, o : x) -> n = m -> m = o -> n = o
> trans_eq n n n Refl Refl = Refl

(This lemma already exists in Idris' stdlib under the name of \idr{trans}.)

Now, we should be able to use \idr{trans_eq} to prove the above example.
However, to do this we need a slight refinement of the \idr{exact} tactic.

> trans_eq_example' : (a, b, c, d, e, f : Nat) ->
>                     [a,b] = [c,d] -> [c,d] = [e,f] -> [a,b] = [e,f]
> trans_eq_example' = %runElab trans_eq_example_tac
> where
>   trans_eq_example_tac : Elab ()
>   trans_eq_example_tac = do
>    [a,b,c,d,e,f,eq1,eq2] <- intros
>      | _ => fail []

\todo[inline]{Edit: Idris apparently can figure things out itself via
\idr{solve}. Explain the quotation syntax.}

If we simply tell Idris \idr{apply (Var `{trans_eq}) ..} at this point, it can
tell (by matching the goal against the conclusion of the lemma) that it should
instantiate \idr{x} with \idr{[Nat]}, \idr{n} with \idr{[a,b]}, and \idr{o} with
\idr{[e,f]}. However, the matching process doesn't determine an instantiation
for \idr{m}: we have to supply one explicitly by adding with (m:=[c,d]) to the
invocation of \idr{apply}.

>    [_,_,_,_,_,_] <- apply (Var `{trans_eq})
>                     [True, True, True, True, False, False]
>      | _ => fail []
>    solve
>    exact $ Var eq1
>    exact $ Var eq2

==== Exercise: 3 stars, optional (apply_with_exercise)

> trans_eq_exercise : (n, m, o, p : Nat) ->
>                     m = (minusTwo o) ->
>                     (n + p) = m ->
>                     (n + p) = (minusTwo o)
> trans_eq_exercise = ?remove_me2 -- %runElab trans_eq_exercise_tac
> where
>   trans_eq_exercise_tac : Elab ()
>   trans_eq_exercise_tac = ?trans_eq_exercise_rhs

$\square$

== The \idr{inversion} Tactic

Recall the definition of natural numbers:

```idris
  data Nat : Type where
         Z : Nat
         S : Nat -> Nat
```

It is obvious from this definition that every number has one of two forms:
either it is the constructor \idr{Z} or it is built by applying the constructor
\idr{S} to another number. But there is more here than meets the eye: implicit
in the definition (and in our informal understanding of how datatype
declarations work in other programming languages) are two more facts:

  - The constructor \idr{S} is _injective_. That is, if \idr{S n = S m}, it must
    be the case that \idr{n = m}.

  - The constructors \idr{Z} and \idr{S} are _disjoint_. That is, \idr{Z} is not
    equal to \idr{S n} for any \idr{n}.

Similar principles apply to all inductively defined types: all constructors are
injective, and the values built from distinct constructors are never equal. For
lists, the \idr{(::)} constructor is injective and \idr{Nil} is different from
every non-empty list. For booleans, \idr{True} and \idr{False} are different.
(Since neither \idr{True} nor \idr{False} take any arguments, their injectivity
is not interesting.) And so on.

Idris provides a tactic called \idr{injective} that allows us to exploit these
principles in proofs. To see how to use it, let's show explicitly that the
\idr{S} constructor is injective:

> S_injective : (n, m : Nat) -> S n = S m -> n = m
> S_injective = %runElab S_injective_tac
> where
>   covering
>   S_injective_tac : Elab ()
>   S_injective_tac = do
>     [n, m, h] <- intros
>       | _ => fail []

By writing \idr{injective (Var h) res} at this point, we are asking Idris to
generate all equations that it can infer from \idr{h} as additional hypotheses,
replacing variables in the goal as it goes. In the present example, this amounts
to adding a new hypothesis \idr{h1 : n = m} and replacing \idr{n} by \idr{m} in
the goal.

\todo[inline]{Explain \idr{gensym}, \idr{unproduct} and \idr{hypothesis}}

>     res <- gensym "sInj"
>     injective (Var h) res
>     unproduct (Var res)
>     hypothesis

Here's a more interesting example that shows how multiple equations can be
derived at once.

\todo[inline]{Works quite fast in Elab shell but hangs the compiler}

> -- inversion_ex1 : (n, m, o : Nat) -> [n, m] = [o, o] -> [n] = [m]
> -- inversion_ex1 = %runElab inversion_ex1_tac
> -- where
> --   inversion_ex1_tac : Elab ()
> --   inversion_ex1_tac = do
> --     [n, m, o, eq] <- intros
> --       | _ => fail []
> --     eqinj <- gensym "eqinj"
> --     injective (Var eq) eqinj
> --
> --     eqinj2 <- gensym "eqinj2"                    -- manual destructuring
> --     both (Var eqinj) !(gensym "natnat") eqinj2
> --     neqo <- gensym "neqo"
> --     eqinj3 <- gensym "eqinj3"
> --     both (Var eqinj2) no eqinj3
> --     meqos <- gensym "meqos"
> --     both (Var eqinj3) mos !(gensym "uu")
> --
> --     oeqn <- gensym "oeqn"
> --     symmetryAs (Var neqo) oeqn
> --     symmetry
> --     rewriteWith $ Var oeqn
> --     exact $ Var meqos
> --     solve

Note that we need to pass the parameter \idr{eqinj} which will be bound to
equations that \idr{injective} generates.

\todo[inline]{Remove when a release with
https://github.com/idris-lang/Idris-dev/pull/3925 happens}

==== Exercise: 1 star (inversion_ex3)

> inversion_ex3 : (x, y, z : a) -> (l, j : List a) ->
>                 x :: y :: l = z :: j ->
>                 y :: l = x :: j ->
>                 x = y
> inversion_ex3 = ?remove_me3 -- %runElab inversion_ex3_tac
> where
>   inversion_ex3_tac : Elab ()
>   inversion_ex3_tac = ?inversion_ex3_tac_rhs

$\square$

\todo[inline]{Edit}

When used on a hypothesis involving an equality between _different_ constructors
(e.g., \idr{S n = Z}), \idr{injective} solves the goal immediately. Consider the
following proof:

> beq_nat_0_l : Z == n = True -> n = Z

We can proceed by case analysis on n. The first case is trivial.

> beq_nat_0_l {n=Z} _ = Refl

However, the second one doesn't look so simple: assuming \idr{0 == S n' = True},
we must show \idr{S n' = 0}, but the latter clearly contradictory! The way
forward lies in the assumption. After simplifying the goal state, we see that
\idr{0 == S n' = True} has become \idr{False = True}:

\todo[inline]{How to show impossible cases from Elab?}

> beq_nat_0_l {n=(S _)} prf = absurd prf

If we use \idr{absurd} on this hypothesis, Idris allows us to safely infer any
conclusion from it, in this case our goal of \idr{n = 0}.

This is an instance of a logical principle known as the principle of explosion,
which asserts that a contradictory hypothesis entails anything, even false
things!

> inversion_ex4 : (n : Nat) -> S n = Z -> 2 + 2 = 5
> -- we need "sym" because Prelude.Nat only disproves "Z = S n" for us
> inversion_ex4 n prf = absurd $ sym prf

In simple cases like this, we could've also solved this with matching on
\idr{prf}:

```idris
inversion_ex4 _ Refl impossible
```

> inversion_ex5 : (n, m : Nat) -> False = True -> [n] = [m]
> inversion_ex5 n m prf = absurd prf

Again, here we can also write

```idris
inversion_ex5 _ _ Refl impossible
```

If you find the principle of explosion confusing, remember that these proofs are
not actually showing that the conclusion of the statement holds. Rather, they
are arguing that, if the nonsensical situation described by the premise did
somehow arise, then the nonsensical conclusion would follow. We'll explore the
principle of explosion of more detail in the next chapter.

==== Exercise: 1 star (inversion_ex6)

> inversion_ex6 : (x, y, z : a) -> (l, j : List a) ->
>                 x :: y :: l = [] ->
>                 y :: l = z :: j ->
>                 x = z
> inversion_ex6 x y z l j prf prf1 = ?inversion_ex6_rhs

$\square$

To summarize this discussion, suppose \idr{h} is a hypothesis in the context
or a previously proven lemma of the form

        \idr{c a1 a2 ... an = d b1 b2 ... bm}

\todo[inline]{Edit, especially the \idr{disjoint} part}

for some constructors \idr{c} and \idr{d} and arguments \idr{a1 ... an} and
\idr{b1 ... bm}. Then \idr{injective h} and \idr{disjoint h} have the following
effects:

  - If \idr{c} and \idr{d} are the same constructor, then, by the injectivity of
    this constructor, we know that \idr{a1 = b1}, \idr{a2 = b2}, etc. The
    \idr{injective h} adds these facts to the context and tries to use them to
    rewrite the goal.

  - If \idr{c} and \idr{d} are different constructors, then the hypothesis
    \idr{h} is contradictory, and the current goal doesn't have to be considered
    at all. In this case, \idr{disjoint h} marks the current goal as completed
    and pops it off the goal stack.

The injectivity of constructors allows us to reason that \idr{(n, m : Nat) -> S
n = S m -> n = m}. The converse of this implication is an instance of a more
general fact about both constructors and functions, which we will find useful in
a few places below:

> f_equal : (f : a -> b) -> (x, y : a) -> x = y -> f x = f y
> f_equal f x x Refl = Refl

(This is called \idr{cong} in Idris' stdlib.)

== Using Tactics on Hypotheses

\todo[inline]{Edit, Idris runs \idr{compute} on hypotheses automatically}

By default, most tactics work on the goal formula and leave the context
unchanged. However, most tactics also have a variant that performs a similar
operation on a statement in the context. For example, the tactic \idr{compute}
in H performs simplification in the hypothesis named \idr{h} in the context.

> S_inj : (n, m : Nat) -> (b : Bool) ->
>         S n == S m = b -> n == m = b
> S_inj = %runElab S_inj_tac
> where
>   S_inj_tac : Elab ()
>   S_inj_tac = do
>     [n, m, b, eq] <- intros
>       | _ => fail []
>     exact $ Var eq

\todo[inline]{Edit}

Similarly, \idr{applyIn l h} matches some conditional statement \idr{l} (of the
form \idr{l1 -> l2}, say) against a hypothesis \idr{h} in the context. However,
unlike ordinary \idr{exact} (which rewrites a goal matching \idr{l2} into a
subgoal \idr{l1}), \idr{applyIn l h n} matches \idr{h} against \idr{l1} and, if
successful, binds the result \idr{l2} to \idr{n}.

In other words, \idr{applyIn l h} gives us a form of "forward reasoning": from
\idr{l1 -> l2} and a hypothesis matching \idr{l1}, it produces a hypothesis
matching \idr{l2}. By contrast, \idr{exact l} is "backward reasoning": it says
that if we know \idr{l1->l2} and we are trying to prove \idr{l2}, it suffices to
prove \idr{l1}.

Here is a variant of a proof from above, using forward reasoning throughout
instead of backward reasoning.

> silly3' : (n, m : Nat) -> (n == 5 = True -> m == 7 = True) ->
>          True = n == 5 -> True = m == 7
> silly3' = %runElab silly3_tac
> where
>   silly3_tac : Elab ()
>   silly3_tac = do
>     [n,m,eq,h] <- intros
>       | _ => fail []
>     hsym <- symmetryAs (Var h) "hsym"
>     happ <- applyAs (Var eq) (Var hsym) "happ"
>     happsym <- symmetryAs (Var happ) "happsym"
>     exact $ Var happsym

Forward reasoning starts from what is _given_ (premises, previously proven
theorems) and iteratively draws conclusions from them until the goal is reached.
Backward reasoning starts from the _goal_, and iteratively reasons about what
would imply the goal, until premises or previously proven theorems are reached.
If you've seen informal proofs before (for example, in a math or computer
science class), they probably used forward reasoning. In general, idiomatic use
of Idris elab scripts tends to favor backward reasoning, but in some situations
the forward style can be easier to think about.

==== Exercise: 3 stars, recommended (plus_n_n_injective)

Practice using "in" variants in this exercise. (Hint: use \idr{plus_n_Sm}.)

> plus_n_n_injective : n + n = m + m -> n = m
> plus_n_n_injective = ?plus_n_n_injective_rhs

$\square$

== Varying the Induction Hypothesis

Sometimes it is important to control the exact form of the induction hypothesis
when carrying out inductive proofs in Idris elab script. In particular, we need
to be careful about which of the assumptions we move (using \idr{intros}) from
the goal to the context before invoking the \idr{induction} tactic. For example,
suppose we want to show that the \idr{double} function is injective -- i.e., that
it maps different arguments to different results:

> double_injective : double n = double m -> n = m
> double_injective {n=Z} {m=Z} _ = Refl
> double_injective {n=Z} {m=(S _)} Refl impossible
> double_injective {n=(S _)} {m=Z} Refl impossible
> double_injective {n=(S n')} {m=(S m')} eq =
>   let eqss = succInjective _ _ $ succInjective _ _ eq
>   in rewrite double_injective {n=n'} {m=m'} eqss in Refl

\todo[inline]{Edit the rest of the section to use \idr{induction}?}

The way we _start_ this proof is a bit delicate: if we begin with

      intros n. induction n.

all is well. But if we begin it with

      intros n m. induction n.

we get stuck in the middle of the inductive case...

Theorem double_injective_FAILED : ∀n m,
     double n = double m -> n = m.
Proof.
  intros n m. induction n as [| n']. - (* n = Z *) simpl. intros eq. destruct m
  as [| m'].
    + (* m = Z *) reflexivity. + (* m = S m' *) inversion eq.
  - (* n = S n' *) intros eq. destruct m as [| m'].
    + (* m = Z *) inversion eq. + (* m = S m' *) apply f_equal.

At this point, the induction hypothesis, IHn', does not give us n' = m' -- there
is an extra S in the way -- so the goal is not provable.

      Abort.

What went wrong?

The problem is that, at the point we invoke the induction hypothesis, we have
already introduced m into the context -- intuitively, we have told Coq, "Let's
consider some particular n and m..." and we now have to prove that, if double n
= double m for these particular n and m, then n = m.

The next tactic, induction n says to Coq: We are going to show the goal by
induction on n. That is, we are going to prove, for all n, that the proposition

  - P n = "if double n = double m, then n = m"

holds, by showing

  - P Z
    (i.e., "if double Z = double m then Z = m") and

  - P n -> P (S n)
    (i.e., "if double n = double m then n = m" implies "if double (S n) = double
    m then S n = m").

If we look closely at the second statement, it is saying something rather
strange: it says that, for a particular m, if we know

  - "if double n = double m then n = m"

then we can prove

  - "if double (S n) = double m then S n = m".

To see why this is strange, let's think of a particular m -- say, 5. The
statement is then saying that, if we know

  - Q = "if double n = 10 then n = 5"

then we can prove

  - R = "if double (S n) = 10 then S n = 5".

But knowing Q doesn't give us any help at all with proving R! (If we tried to
prove R from Q, we would start with something like "Suppose double (S n) =
10..." but then we'd be stuck: knowing that double (S n) is 10 tells us nothing
about whether double n is 10, so Q is useless.)

Trying to carry out this proof by induction on n when m is already in the
context doesn't work because we are then trying to prove a relation involving
every n but just a single m.

The successful proof of double_injective leaves m in the goal statement at the
point where the induction tactic is invoked on n:

Theorem double_injective : ∀n m,
     double n = double m -> n = m.
Proof.
  intros n. induction n as [| n']. - (* n = Z *) simpl. intros m eq. destruct m
  as [| m'].
    + (* m = Z *) reflexivity. + (* m = S m' *) inversion eq.

  - (* n = S n' *) simpl.

Notice that both the goal and the induction hypothesis are different this time:
the goal asks us to prove something more general (i.e., to prove the statement
for every m), but the IH is correspondingly more flexible, allowing us to choose
any m we like when we apply the IH.

    intros m eq.

Now we've chosen a particular m and introduced the assumption that double n =
double m. Since we are doing a case analysis on n, we also need a case analysis
on m to keep the two "in sync."

    destruct m as [| m']. + (* m = Z *) simpl.

The 0 case is trivial:

      inversion eq.

    + (* m = S m' *)
      apply f_equal.

At this point, since we are in the second branch of the destruct m, the m'
mentioned in the context is the predecessor of the m we started out talking
about. Since we are also in the S branch of the induction, this is perfect: if
we instantiate the generic m in the IH with the current m' (this instantiation
is performed automatically by the apply in the next step), then IHn' gives us
exactly what we need to finish the proof.

      apply IHn'. inversion eq. reflexivity. Qed.

What you should take away from all this is that we need to be careful about
using induction to try to prove something too specific: To prove a property of n
and m by induction on n, it is sometimes important to leave m generic.

The following exercise requires the same pattern.

==== Exercise: 2 stars (beq_nat_true)

\ \todo[inline]{We explicitly write out implicits as having type \idr{Nat} since
\idr{(==)} is polymorphic}

> beq_nat_true : {n, m : Nat} -> n == m = True -> n = m
> beq_nat_true prf = ?beq_nat_true_rhs

$\square$

==== Exercise: 2 stars, advanced (beq_nat_true_informal)

Give a careful informal proof of \idr{beq_nat_true}, being as explicit as possible
about quantifiers.

> -- FILL IN HERE

$\square$

\todo[inline]{What to do with the rest of this?}

The strategy of doing fewer intros before an induction to obtain a more general
IH doesn't always work by itself; sometimes some rearrangement of quantified
variables is needed. Suppose, for example, that we wanted to prove
double_injective by induction on m instead of n.

Theorem double_injective_take2_FAILED : ∀n m,
     double n = double m -> n = m.
Proof.
  intros n m. induction m as [| m']. - (* m = Z *) simpl. intros eq. destruct n
  as [| n'].
    + (* n = Z *) reflexivity. + (* n = S n' *) inversion eq.
  - (* m = S m' *) intros eq. destruct n as [| n'].
    + (* n = Z *) inversion eq. + (* n = S n' *) apply f_equal.
        (* Stuck again here, just like before. *)
Abort.

The problem is that, to do induction on m, we must first introduce n. (If we
simply say induction m without introducing anything first, Coq will
automatically introduce n for us!)

What can we do about this? One possibility is to rewrite the statement of the
lemma so that m is quantified before n. This works, but it's not nice: We don't
want to have to twist the statements of lemmas to fit the needs of a particular
strategy for proving them! Rather we want to state them in the clearest and most
natural way.

What we can do instead is to first introduce all the quantified variables and
then re-generalize one or more of them, selectively taking variables out of the
context and putting them back at the beginning of the goal. The generalize
dependent tactic does this.

Theorem double_injective_take2 : ∀n m,
     double n = double m -> n = m.
Proof.
  intros n m. (* n and m are both in the context *) generalize dependent n. (*
  Now n is back in the goal and we can do induction on
     m and get a sufficiently general IH. *)
  induction m as [| m']. - (* m = Z *) simpl. intros n eq. destruct n as [| n'].
    + (* n = Z *) reflexivity. + (* n = S n' *) inversion eq.
  - (* m = S m' *) intros n eq. destruct n as [| n'].
    + (* n = Z *) inversion eq. + (* n = S n' *) apply f_equal.
      apply IHm'. inversion eq. reflexivity. Qed.

Let's look at an informal proof of this theorem. Note that the proposition we
prove by induction leaves n quantified, corresponding to the use of generalize
dependent in our formal proof.

_Theorem_: For any nats n and m, if double n = double m, then n = m.

_Proof_: Let m be a Nat. We prove by induction on m that, for any n, if double n
= double m then n = m.

  - First, suppose m = 0, and suppose n is a number such that double n = double
    m. We must show that n = 0.

    Since m = 0, by the definition of double we have double n = 0. There are two
    cases to consider for n. If n = 0 we are done, since m = 0 = n, as required.
    Otherwise, if n = S n' for some n', we derive a contradiction: by the
    definition of double, we can calculate double n = S (S (double n')), but
    this contradicts the assumption that double n = 0.

  - Second, suppose m = S m' and that n is again a number such that double n =
    double m. We must show that n = S m', with the induction hypothesis that for
    every number s, if double s = double m' then s = m'.

    By the fact that m = S m' and the definition of double, we have double n = S
    (S (double m')). There are two cases to consider for n.

    If n = 0, then by definition double n = 0, a contradiction.

    Thus, we may assume that n = S n' for some n', and again by the definition
    of double we have S (S (double n')) = S (S (double m')), which implies by
    inversion that double n' = double m'. Instantiating the induction hypothesis
    with n' thus allows us to conclude that n' = m', and it follows immediately
    that S n' = S m'. Since S n' = n and S m' = m, this is just what we wanted
    to show. $\square$

Before we close this section and move on to some exercises, let's digress
briefly and use \idr{beq_nat_true} to prove a similar property of identifiers
that we'll need in later chapters:

> data Id : Type where
>   MkId : Nat -> Id

> beq_id : (x1, x2 : Id) -> Bool
> beq_id (MkId n1) (MkId n2) = n1 == n2

> beq_id_true : beq_id x y = True -> x = y
> beq_id_true {x=MkId x'} {y=MkId y'} prf =
>   rewrite beq_nat_true {n=x'} {m=y'} prf in Refl

=== Exercise: 3 stars, recommended (gen_dep_practice)

Prove this by induction on \idr{l}.

> data Option : (x : Type) -> Type where
>  Some : x -> Option x
>  None : Option x

> nth_error : (l : List x) -> (n : Nat) -> Option x
> nth_error [] n = None
> nth_error (a::l') n = if n == 0
>                         then Some a
>                         else nth_error l' (Nat.pred n)

> nth_error_after_last: (n : Nat) -> (l : List x) ->
>                       length l = n -> nth_error l n = None

$\square$

== Unfolding Definitions

\todo[inline]{Edit}

It sometimes happens that we need to manually unfold a definition so that we can
manipulate its right-hand side. For example, if we define...

> square : Nat -> Nat
> square n = n * n

... and try to prove a simple fact about square...

> square_mult : (n, m : Nat) -> square (n * m) = square n * square m
> square_mult n m = rewrite multAssociative (n*m) n m in
>                   rewrite multCommutative (n*m) n in
>                   rewrite multAssociative (n*n) m m in
>                   rewrite multAssociative n n m in Refl

... we succeed because Idris unfolds everything for us automatically.

\todo[inline]{Remove the next part?}

... we get stuck: simpl doesn't simplify anything at this point, and since we
haven't proved any other facts about square, there is nothing we can apply or
rewrite with.

To make progress, we can manually unfold the definition of square:

  unfold square.

Now we have plenty to work with: both sides of the equality are expressions
involving multiplication, and we have lots of facts about multiplication at our
disposal. In particular, we know that it is commutative and associative, and
from these facts it is not hard to finish the proof.

  rewrite mult_assoc. assert (H : n * m * n = n * n * m). { rewrite mult_comm.
  apply mult_assoc. } rewrite H. rewrite mult_assoc. reflexivity.
Qed.

At this point, a deeper discussion of unfolding and simplification is in order.

You may already have observed that \idr{Refl} will often unfold the definitions
of functions automatically when this allows them to make progress. For example,
if we define \idr{foo m} to be the constant \idr{5}...

> foo : Nat -> Nat
> foo x = 5

then \idr{Refl} in the following proof will unfold \idr{foo m} to \idr{(\x => 5)
m} and then further simplify this expression to just \idr{5}.

> silly_fact_1 : foo m + 1 = foo (m + 1) + 1
> silly_fact_1 = Refl

However, this automatic unfolding is rather conservative. For example, if we
define a slightly more complicated function involving a pattern match...

> bar : Nat -> Nat
> bar Z = 5
> bar (S _) = 5

...then the analogous proof will get stuck:

```idris
silly_fact_2_FAILED : bar m + 1 = bar (m + 1) + 1
silly_fact_2_FAILED = Refl
```

The reason that \idr{Refl} doesn't make progress here is that it notices that,
after tentatively unfolding \idr{bar m}, it is left with a match whose
scrutinee, \idr{m}, is a variable, so the match cannot be simplified further.
(It is not smart enough to notice that the two branches of the match are
identical.) So it gives up on unfolding \idr{bar m} and leaves it alone.
Similarly, tentatively unfolding \idr{bar (m+1)} leaves a match whose scrutinee
is a function application (that, itself, cannot be simplified, even after
unfolding the definition of \idr{+}), so \idr{Refl} leaves it alone.

At this point, there are two ways to make progress. One is to match on implicit
parameter \idr{m} to break the proof into two cases, each focusing on a more
concrete choice of \idr{m} (\idr{Z} vs \idr{S _}). In each case, the match
inside of \idr{bar} can now make progress, and the proof is easy to complete.

> silly_fact_2 : bar m + 1 = bar (m + 1) + 1
> silly_fact_2 {m=Z} = Refl
> silly_fact_2 {m=(S _)} = Refl

\todo[inline]{Edit}

This approach works, but it depends on our recognizing that the match hidden
inside bar is what was preventing us from making progress. A more
straightforward way to make progress is to explicitly tell Idris to unfold bar.

\todo[inline]{Can we destruct in Elab script? Maybe with \idr{deriveElim}?}

Fact silly_fact_2' : ∀m, bar m + 1 = bar (m + 1) + 1. Proof.
  intros m. unfold bar.

Now it is apparent that we are stuck on the match expressions on both sides of
the =, and we can use destruct to finish the proof without thinking too hard.

  destruct m.
  - reflexivity.
  - reflexivity.
Qed.

== Using \idr{destruct} on Compound Expressions

\todo[inline]{Edit. Explain \idr{with}}

We have seen many examples where destruct is used to perform case analysis of
the value of some variable. But sometimes we need to reason by cases on the
result of some _expression_. We can also do this with destruct.

Here are some examples:

> sillyfun : Nat -> Bool
> sillyfun n = if n == 3
>                 then False
>                 else if n == 5
>                         then False
>                         else False

> sillyfun_false : (n : Nat) -> sillyfun n = False
> sillyfun_false n with (n == 3)
>   sillyfun_false n | True = Refl
>   sillyfun_false n | False with (n == 5)
>     sillyfun_false n | False | True = Refl
>     sillyfun_false n | False | False = Refl

After unfolding \idr{sillyfun} in the above proof, we find that we are stuck on
\idr{if (n == 3) then ... else ...}. But either \idr{n} is equal to \idr{3} or
it isn't, so we can use \idr{with (n == 3)} to let us reason about the two
cases.

\todo[inline]{Edit}

In general, the destruct tactic can be used to perform case analysis of the
results of arbitrary computations. If e is an expression whose type is some
inductively defined type T, then, for each constructor c of T, destruct e
generates a subgoal in which all occurrences of e (in the goal and in the
context) are replaced by c.

==== Exercise: 3 stars, optional (combine_split)

> combine_split : (l : List (x,y)) -> (l1 : List x) -> (l2 : List y) ->
>                 unzip l = (l1, l2) -> zip l1 l2 = l
> combine_split l l1 l2 prf = ?combine_split_rhs

$\square$

However, destructing compound expressions requires a bit of care, as
such destructs can sometimes erase information we need to complete a proof. For
example, suppose we define a function \idr{sillyfun1} like this:

> sillyfun1 : Nat -> Bool
> sillyfun1 n = if n == 3
>                  then True
>                  else if n == 5
>                          then True
>                          else False

Now suppose that we want to convince Idris of the (rather obvious) fact that
\idr{sillyfun1 n} yields \idr{True} only when \idr{n} is odd. By analogy with
the proofs we did with \idr{sillyfun} above, it is natural to start the proof
like this:

> sillyfun1_odd : (n : Nat) -> sillyfun1 n = True -> oddb n = True
> sillyfun1_odd n prf with (n == 3) proof eq3
>   sillyfun1_odd n Refl | True =
>     rewrite beq_nat_true (sym eq3) {n} {m=3} in Refl
>   sillyfun1_odd n prf | False with (n == 5) proof eq5
>     sillyfun1_odd n Refl | False | True =
>       rewrite beq_nat_true (sym eq5) {n} {m=5} in Refl
>     sillyfun1_odd n prf | False | False = absurd prf

\todo[inline]{Edit the following, since \idr{with} works fine here as well}

We get stuck at this point because the context does not contain enough
information to prove the goal! The problem is that the substitution performed by
destruct is too brutal -- it threw away every occurrence of n == 3, but we need
to keep some memory of this expression and how it was destructed, because we
need to be able to reason that, since n == 3 = True in this branch of the case
analysis, it must be that n = 3, from which it follows that n is odd.

What we would really like is to substitute away all existing occurences of n ==
3, but at the same time add an equation to the context that records which case
we are in. The eqn: qualifier allows us to introduce such an equation, giving it
a name that we choose.

Theorem sillyfun1_odd : ∀(n : Nat),
     sillyfun1 n = True -> oddb n = True.
Proof.
  intros n eq. unfold sillyfun1 in eq. destruct (beq_nat n 3) eqn:Heqe3.
  (* Now
  we have the same state as at the point where we got
     stuck above, except that the context contains an extra equality assumption,
     which is exactly what we need to make progress. *) - (* e3 = True *) apply
     beq_nat_true in Heqe3. rewrite -> Heqe3. reflexivity. - (* e3 = False *) (*
     When we come to the second equality test in the body
        of the function we are reasoning about, we can use eqn: again in the
        same way, allow us to finish the proof. *)
      destruct (beq_nat n 5) eqn:Heqe5.
        + (* e5 = True *)
          apply beq_nat_true in Heqe5. rewrite -> Heqe5. reflexivity.
        + (* e5 = False *) inversion eq. Qed.

==== Exercise: 2 stars (destruct_eqn_practice)

> bool_fn_applied_thrice : (f : Bool -> Bool) -> (b : Bool) -> f (f (f b)) = f b
> bool_fn_applied_thrice f b = ?bool_fn_applied_thrice_rhs

$\square$

== Review

We've now seen many of Idris's most fundamental tactics. We'll introduce a few
more in the coming chapters, and later on we'll see some more powerful
automation tactics that make Idris help us with low-level details. But basically
we've got what we need to get work done.

Here are the ones we've seen:

\todo[inline]{Edit}

  - \idr{intros}: move hypotheses/variables from goal to context

  - \idr{reflexivity}: finish the proof (when the goal looks like \idr{e = e})

  - \idr{exact}: prove goal using a hypothesis, lemma, or constructor

  - \idr{apply... in H}: apply a hypothesis, lemma, or constructor to a
    hypothesis in the context (forward reasoning)

  - \idr{apply... with...}: explicitly specify values for variables that cannot
    be determined by pattern matching

  - \idr{compute}: simplify computations in the goal

  - \idr{simpl in H}: ... or a hypothesis

  - \idr{rewriteWith}: use an equality hypothesis (or lemma) to rewrite the goal

  - \idr{rewrite ... in H}: ... or a hypothesis

  - \idr{symmetry}: changes a goal of the form \idr{t=u} into \idr{u=t}

  - \idr{symmetryAs h}: changes a hypothesis of the form \idr{t=u} into
    \idr{u=t}

  - \idr{unfold}: replace a defined constant by its right-hand side in the goal

  - \idr{unfold... in H}: ... or a hypothesis

  - \idr{destruct... as...}: case analysis on values of inductively defined
    types

  - \idr{destruct... eqn:...}: specify the name of an equation to be added to
    the context, recording the result of the case analysis

  - \idr{induction... as...}: induction on values of inductively defined types

  - \idr{injective}: reason by injectivity of constructors

  - \idr{disjoint}: reason by distinctness of constructors

  - \idr{assert (H: e)} (or \idr{assert (e) as H}): introduce a "local lemma"
    \idr{e} and call it \idr{H}

  - \idr{generalize dependent x}: move the variable \idr{x} (and anything else
    that depends on it) from the context back to an explicit hypothesis in the goal formula

== Additional Exercises

==== Exercise: 3 stars (beq_nat_sym)

> beq_nat_sym : (n, m : Nat) -> n == m = m == n
> beq_nat_sym n m = ?beq_nat_sym_rhs

$\square$

==== Exercise: 3 stars, advancedM? (beq_nat_sym_informal)

Give an informal proof of this lemma that corresponds to your formal proof
above:

Theorem: For any \idr{Nat}s \idr{n}, idr{m}, \idr{n == m = m == n}

Proof:

> --FILL IN HERE

$\square$

==== Exercise: 3 stars, optional (beq_nat_trans)

> beq_nat_trans : {n, m, p : Nat} -> n == m = True -> m == p = True ->
>                                    n == p = True
> beq_nat_trans prf prf1 = ?beq_nat_trans_rhs

$\square$

==== Exercise: 3 stars, advanced (split_combine)

We proved, in an exercise above, that for all lists of pairs, \idr{zip} is the
inverse of \idr{unzip}. How would you formalize the statement that \idr{unzip}
is the inverse of \idr{zip}? When is this property true?

Complete the definition of \idr{split_combine} below with a property that states
that \idr{unzip} is the inverse of \idr{zip}. Then, prove that the property
holds. (Be sure to leave your induction hypothesis general by not doing
\idr{intros} on more things than necessary. Hint: what property do you need of
\idr{l1} and \idr{l2} for \idr{unzip (zip l1 l2) = (l1,l2)} to be true?)

> split_combine : ?split_combine

$\square$

==== Exercise: 3 stars, advanced (filter_exercise)

This one is a bit challenging. Pay attention to the form of your induction
hypothesis.

> filter_exercise : (test : a -> Bool) -> (x : a) -> (l, lf : List a) ->
>                   filter test l = x :: lf ->
>                   test x = True
> filter_exercise test x l lf prf = ?filter_exercise_rhs

$\square$

==== Exercise: 4 stars, advanced, recommended (forall_exists_challenge)

Define two recursive functions, \idr{forallb} and \idr{existsb}. The first
checks whether every element in a list satisfies a given predicate:

      \idr{forallb oddb [1,3,5,7,9] = True}

      \idr{forallb not [False,False] = True}

      \idr{forallb evenb [0,2,4,5] = False}

      \idr{forallb (== 5) [] = True}

The second checks whether there exists an element in the list that satisfies a
given predicate:

      \idr{existsb (== 5) [0,2,3,6] = False}

      \idr{existsb ((&&) True) [True,True,False] = True}

      \idr{existsb oddb [1,0,0,0,0,3] = True}

      \idr{existsb evenb [] = False}

Next, define a _nonrecursive_ version of \idr{existsb} -- call it \idr{existsb'}
-- using \idr{forallb} and \idr{not}.

Finally, prove a theorem \idr{existsb_existsb'} stating that \idr{existsb'} and
\idr{existsb} have the same behavior.

> -- FILL IN HERE

$\square$

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
module Text.CSS.Rule

import Data.String
import Text.CSS.Declaration
import Text.CSS.Render
import Text.CSS.Selector

%default total

public export
data Rule : (n : Nat) -> Type where
  MkRule :  (selector : Selector selDepth hasPseudoClass hasPseudoElem)
         -> (decls    : List Declaration)
         -> Rule n

  Media :   (query : String)
         -> (rules : List $ Rule 0)
         -> Rule 1

infix 2 !!

export %inline
(!!) : Selector n b1 b1 -> List Declaration -> Rule k
(!!) = MkRule

export
Render (Rule n) where
  render (MkRule s ds) = "\{render s}{\{fastConcat $ map render ds}}"
  render (Media q rs)  = "@media (\{q}){\{fastUnlines $ map render rs}}"


text:
> module Fraction.BasicOperations

> import Fraction.Fraction
> import PNat.PNat
> import PNat.Operations
> import Nat.Positive

> %default total
> %access public export

> ||| The numerator of a fraction
> num : Fraction -> Nat
> num = fst

> ||| The denominator of a fraction
> den : Fraction -> Nat
> den = toNat . snd

> ||| Every natural number is a fraction
> fromNat : Nat -> Fraction
> fromNat n = (n, Element (S Z) MkPositive)

> ||| Fraction addition
> plus : Fraction -> Fraction -> Fraction
> plus (n1, d1) (n2, d2) = (n1 * (toNat d2) + n2 * (toNat d1), d1 * d2)

> ||| Fraction multiplication
> mult : Fraction -> Fraction -> Fraction
> mult (n1, d1) (n2, d2) = (n1 * n2, d1 * d2)

> ||| Fraction upscaling
> upscale : Fraction -> PNat -> Fraction
> upscale (m, d) e = (m * (toNat e), d * e)

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Lens.Reversible

import Data.Maybe
import Lens
import Lens.Uninhabited
import Lens.Util
import Map

%default total

make_reversible : (k : Kind) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (Make k) s = Just s' -> transform_schema (reverse_lens (Make k)) s' = Just s
make_reversible KNull SNull _ Refl impossible
make_reversible KNull SBoolean _ Refl impossible
make_reversible KNull SNumber _ Refl impossible
make_reversible KNull SText _ Refl impossible
make_reversible KNull (SArray _ _) _ Refl impossible
make_reversible KNull (SObject _) _ Refl impossible
make_reversible (KPrimitive KBoolean) SNull SBoolean Refl = Refl
make_reversible (KPrimitive KBoolean) SBoolean _ Refl impossible
make_reversible (KPrimitive KBoolean) SNumber _ Refl impossible
make_reversible (KPrimitive KBoolean) SText _ Refl impossible
make_reversible (KPrimitive KBoolean) (SArray _ _) _ Refl impossible
make_reversible (KPrimitive KBoolean) (SObject _) _ Refl impossible
make_reversible (KPrimitive KNumber) SNull SNumber Refl = Refl
make_reversible (KPrimitive KNumber) SBoolean _ Refl impossible
make_reversible (KPrimitive KNumber) SNumber _ Refl impossible
make_reversible (KPrimitive KNumber) SText _ Refl impossible
make_reversible (KPrimitive KNumber) (SArray _ _) _ Refl impossible
make_reversible (KPrimitive KNumber) (SObject _) _ Refl impossible
make_reversible (KPrimitive KText) SNull SText Refl = Refl
make_reversible (KPrimitive KText) SBoolean _ Refl impossible
make_reversible (KPrimitive KText) SNumber _ Refl impossible
make_reversible (KPrimitive KText) SText _ Refl impossible
make_reversible (KPrimitive KText) (SArray _ _) _ Refl impossible
make_reversible (KPrimitive KText) (SObject _) _ Refl impossible
make_reversible KArray SNull (SArray True SNull) Refl = Refl
make_reversible KArray SBoolean _ Refl impossible
make_reversible KArray SNumber _ Refl impossible
make_reversible KArray SText _ Refl impossible
make_reversible KArray (SArray _ _) _ Refl impossible
make_reversible KArray (SObject _) _ Refl impossible
make_reversible KObject SNull (SObject Empty) Refl = Refl
make_reversible KObject SBoolean _ Refl impossible
make_reversible KObject SNumber _ Refl impossible
make_reversible KObject SText _ Refl impossible
make_reversible KObject (SArray _ _) _ Refl impossible
make_reversible KObject (SObject _) _ Refl impossible

destroy_reversible : (k : Kind) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (Destroy k) s = Just s' -> transform_schema (reverse_lens (Destroy k)) s' = Just s
destroy_reversible KNull SNull _ Refl impossible
destroy_reversible KNull SBoolean _ Refl impossible
destroy_reversible KNull SNumber _ Refl impossible
destroy_reversible KNull SText _ Refl impossible
destroy_reversible KNull (SArray _ _) _ Refl impossible
destroy_reversible KNull (SObject _) _ Refl impossible
destroy_reversible (KPrimitive KBoolean) SNull _ Refl impossible
destroy_reversible (KPrimitive KBoolean) SBoolean SNull Refl = Refl
destroy_reversible (KPrimitive KBoolean) SNumber _ Refl impossible
destroy_reversible (KPrimitive KBoolean) SText _ Refl impossible
destroy_reversible (KPrimitive KBoolean) (SArray _ _) _ Refl impossible
destroy_reversible (KPrimitive KBoolean) (SObject _) _ Refl impossible
destroy_reversible (KPrimitive KNumber) SNull _ Refl impossible
destroy_reversible (KPrimitive KNumber) SBoolean _ Refl impossible
destroy_reversible (KPrimitive KNumber) SNumber SNull Refl = Refl
destroy_reversible (KPrimitive KNumber) SText _ Refl impossible
destroy_reversible (KPrimitive KNumber) (SArray _ _) _ Refl impossible
destroy_reversible (KPrimitive KNumber) (SObject _) _ Refl impossible
destroy_reversible (KPrimitive KText) SNull _ Refl impossible
destroy_reversible (KPrimitive KText) SBoolean _ Refl impossible
destroy_reversible (KPrimitive KText) SNumber _ Refl impossible
destroy_reversible (KPrimitive KText) SText SNull Refl = Refl
destroy_reversible (KPrimitive KText) (SArray _ _) _ Refl impossible
destroy_reversible (KPrimitive KText) (SObject _) _ Refl impossible
destroy_reversible KArray SNull _ Refl impossible
destroy_reversible KArray SBoolean _ Refl impossible
destroy_reversible KArray SNumber _ Refl impossible
destroy_reversible KArray SText _ Refl impossible
destroy_reversible KArray (SArray False _) _ Refl impossible
destroy_reversible KArray (SArray True SNull) SNull Refl = Refl
destroy_reversible KArray (SArray True SBoolean) _ Refl impossible
destroy_reversible KArray (SArray True SNumber) _ Refl impossible
destroy_reversible KArray (SArray True SText) _ Refl impossible
destroy_reversible KArray (SArray True (SArray _ _)) _ Refl impossible
destroy_reversible KArray (SArray True (SObject _)) _ Refl impossible
destroy_reversible KArray (SObject _) _ Refl impossible
destroy_reversible KObject SNull _ Refl impossible
destroy_reversible KObject SBoolean _ Refl impossible
destroy_reversible KObject SNumber _ Refl impossible
destroy_reversible KObject SText _ Refl impossible
destroy_reversible KObject (SArray _ _) _ Refl impossible
destroy_reversible KObject (SObject (Update _ _ _)) _ Refl impossible
destroy_reversible KObject (SObject Empty) s' prf =
    rewrite sym $ justInjective prf in Refl

add_property_reversible : (k : Key) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (AddProperty k) s = Just s' -> transform_schema (reverse_lens (AddProperty k)) s' = Just s
add_property_reversible _ SNull _ Refl impossible
add_property_reversible _ SBoolean _ Refl impossible
add_property_reversible _ SNumber _ Refl impossible
add_property_reversible _ SText _ Refl impossible
add_property_reversible _ (SArray _ _) _ Refl impossible
add_property_reversible k (SObject m) s' prf with (get k m) proof prf1
    add_property_reversible k (SObject _) _ prf | (Just _) = absurd $ prf
    add_property_reversible k (SObject m) s' prf | Nothing =
        rewrite sym $ justInjective prf in
        rewrite update_eq m k (Just SNull) in
        rewrite update_shadow m k (Just SNull) Nothing in
        rewrite update_same m k Nothing prf1 in Refl

remove_property_reversible : (k : Key) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (RemoveProperty k) s = Just s' -> transform_schema (reverse_lens (RemoveProperty k)) s' = Just s
remove_property_reversible _ SNull _ Refl impossible
remove_property_reversible _ SBoolean _ Refl impossible
remove_property_reversible _ SNumber _ Refl impossible
remove_property_reversible _ SText _ Refl impossible
remove_property_reversible _ (SArray _ _) _ Refl impossible
remove_property_reversible k (SObject m) s' prf with (get k m) proof prf1
    remove_property_reversible _ (SObject _) _ prf | Nothing = absurd $ prf
    remove_property_reversible _ (SObject _) _ prf | (Just SBoolean) = absurd $ prf
    remove_property_reversible _ (SObject _) _ prf | (Just SNumber) = absurd $ prf
    remove_property_reversible _ (SObject _) _ prf | (Just SText) = absurd $ prf
    remove_property_reversible _ (SObject _) _ prf | (Just (SArray _ _)) = absurd $ prf
    remove_property_reversible _ (SObject _) _ prf | (Just (SObject _)) = absurd $ prf
    remove_property_reversible k (SObject m) s' prf | (Just SNull) =
        rewrite sym $ justInjective prf in
        rewrite update_eq m k Nothing in
        rewrite update_shadow m k Nothing (Just SNull) in
        rewrite update_same m k (Just SNull) prf1 in Refl

rename_property_reversible : (k, k' : Key) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (RenameProperty k k') s = Just s' -> transform_schema (reverse_lens (RenameProperty k k')) s' = Just s
rename_property_reversible _ _ SNull _ Refl impossible
rename_property_reversible _ _ SBoolean _ Refl impossible
rename_property_reversible _ _ SNumber _ Refl impossible
rename_property_reversible _ _ SText _ Refl impossible
rename_property_reversible _ _ (SArray _ _) _ Refl impossible
rename_property_reversible k k' (SObject m) s' prf with (get k m, get k' m) proof prf1
    rename_property_reversible _ _ (SObject _) _ prf | (Nothing, _) = absurd $ prf
    rename_property_reversible _ _ (SObject _) _ prf | (Just _, Just _) = absurd $ prf
    rename_property_reversible k k' (SObject m) s' prf | ((Just x), Nothing) =
        rewrite sym $ justInjective prf in
        rewrite update_eq (update k Nothing m) k' (Just x) in
        let va = cong fst prf1
            vb = cong snd prf1
            not_a_eq_b = get_neq $ tuple_eq prf1 uninhabited
            not_b_eq_a = \p => not_a_eq_b $ sym p in
        rewrite update_permute m k' k (Just x) Nothing not_b_eq_a in
        rewrite ne_key k k' not_a_eq_b in
        rewrite beq_key k in
        rewrite update_permute m k k' Nothing (Just x) not_a_eq_b in
        rewrite update_shadow (update k Nothing m) k' (Just x) Nothing in
        rewrite update_permute m k' k Nothing Nothing not_b_eq_a in
        rewrite update_same m k' Nothing vb in
        rewrite update_shadow m k Nothing (Just x) in
        rewrite update_same m k (Just x) va in Refl

hoist_property_reversible : (h, t : Key) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (HoistProperty h t) s = Just s' -> transform_schema (reverse_lens (HoistProperty h t)) s' = Just s
hoist_property_reversible _ _ SNull _ Refl impossible
hoist_property_reversible _ _ SBoolean _ Refl impossible
hoist_property_reversible _ _ SNumber _ Refl impossible
hoist_property_reversible _ _ SText _ Refl impossible
hoist_property_reversible _ _ (SArray _ _) _ Refl impossible
hoist_property_reversible h t (SObject m) s' prf with (get h m, get t m) proof prf1
    hoist_property_reversible _ _ (SObject _) _ prf | (Nothing, _) = absurd $ prf
    hoist_property_reversible _ _ (SObject _) _ prf | (Just SNull, _) = absurd $ prf
    hoist_property_reversible _ _ (SObject _) _ prf | (Just SBoolean, _) = absurd $ prf
    hoist_property_reversible _ _ (SObject _) _ prf | (Just SNumber, _) = absurd $ prf
    hoist_property_reversible _ _ (SObject _) _ prf | (Just SText, _) = absurd $ prf
    hoist_property_reversible _ _ (SObject _) _ prf | (Just (SArray _ _), _) = absurd $ prf
    hoist_property_reversible _ _ (SObject _) _ prf | (Just (SObject _), Just _) = absurd $ prf
    hoist_property_reversible h t (SObject m) s' prf | (Just (SObject hm), Nothing) with (get t hm) proof prf2
        hoist_property_reversible _ _ (SObject _) _ prf | (Just (SObject _), Nothing) | Nothing = absurd $ prf
        hoist_property_reversible h t (SObject m) s' prf | (Just (SObject hm), Nothing) | Just x =
            rewrite sym $ justInjective prf in
            let neq_ht = get_neq (tuple_eq prf1 uninhabited)
                neq_th = \p => neq_ht (sym p) in
            rewrite update_permute m h t (Just (SObject (update t Nothing hm))) (Just x) neq_ht in
            rewrite ne_key t h neq_th in
            rewrite beq_key t in
            rewrite beq_key h in
            rewrite beq_key t in
            rewrite update_permute m t h (Just x) (Just (SObject (update t Nothing hm))) neq_th in
            rewrite update_shadow hm t Nothing (Just x) in
            rewrite update_permute (update t (Just x) m) t h Nothing (Just (SObject (update t Nothing hm))) neq_th in
            rewrite update_shadow m t (Just x) Nothing in
            rewrite update_shadow (update t Nothing m) h
                (Just (SObject (update t Nothing hm)))
                (Just (SObject (update t (Just x) hm))) in
            rewrite update_same m t Nothing (cong snd prf1) in
            rewrite update_same hm t (Just x) prf2 in
            rewrite update_same m h (Just (SObject hm)) (cong fst prf1) in Refl

plunge_property_reversible : (h, t : Key) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (PlungeProperty h t) s = Just s' -> transform_schema (reverse_lens (PlungeProperty h t)) s' = Just s
plunge_property_reversible _ _ SNull _ Refl impossible
plunge_property_reversible _ _ SBoolean _ Refl impossible
plunge_property_reversible _ _ SNumber _ Refl impossible
plunge_property_reversible _ _ SText _ Refl impossible
plunge_property_reversible _ _ (SArray _ _) _ Refl impossible
plunge_property_reversible h t (SObject m) s' prf with (get t m, get h m, t == h) proof prf1
    plunge_property_reversible _ _ (SObject _) _ prf | (Nothing, _, _) = absurd $ prf
    plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Nothing, _) = absurd $ prf
    plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Just SNull, _) = absurd $ prf
    plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Just SBoolean, _) = absurd $ prf
    plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Just SNumber, _) = absurd $ prf
    plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Just SText, _) = absurd $ prf
    plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Just (SArray _ _), _) = absurd $ prf
    plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Just (SObject _), True) = absurd $ prf
    plunge_property_reversible h t (SObject m) s' prf | (Just tv, Just (SObject hm), False) with (get t hm) proof prf2
        plunge_property_reversible _ _ (SObject _) _ prf | (Just _, Just (SObject _), False) | Just _ = absurd $ prf
        plunge_property_reversible h t (SObject m) s' prf | (Just tv, Just (SObject hm), False) | Nothing =
            rewrite sym $ justInjective prf in
            let neq_th = bne_key t h $ cong snd $ cong snd $ prf1
                neq_ht = \p => neq_th $ sym p in
            rewrite update_eq (update t Nothing m) h (Just (SObject (update t (Just tv) hm))) in
            rewrite update_permute m h t (Just (SObject (update t (Just tv) hm))) Nothing neq_ht in
            rewrite ne_key t h neq_th in
            rewrite beq_key t in
            rewrite beq_key t in
            rewrite update_shadow hm t (Just tv) Nothing in
            rewrite update_shadow (update h (Just (SObject (update t (Just tv) hm))) m) t Nothing (Just tv) in
            rewrite update_permute m t h (Just tv) (Just (SObject (update t (Just tv) hm))) neq_th in
            rewrite update_same m t (Just tv) (cong fst prf1) in
            rewrite update_shadow m h (Just (SObject (update t (Just tv) hm))) (Just (SObject (update t Nothing hm))) in
            rewrite update_same hm t Nothing prf2 in
            rewrite update_same m h (Just (SObject hm)) (cong fst $ cong snd prf1) in Refl

wrap_reversible :
    (s : Schema) -> (s' : Schema) ->
    transform_schema Wrap s = Just s' -> transform_schema (reverse_lens Wrap) s' = Just s
wrap_reversible SNull _ prf = rewrite sym $ justInjective prf in Refl
wrap_reversible SBoolean _ prf = rewrite sym $ justInjective prf in Refl
wrap_reversible SNumber _ prf = rewrite sym $ justInjective prf in Refl
wrap_reversible SText _ prf = rewrite sym $ justInjective prf in Refl
wrap_reversible (SArray _ _) _ prf = rewrite sym $ justInjective prf in Refl
wrap_reversible (SObject _) _ prf = rewrite sym $ justInjective prf in Refl

head_reversible :
    (s : Schema) -> (s' : Schema) ->
    transform_schema Head s = Just s' -> transform_schema (reverse_lens Head) s' = Just s
head_reversible SNull _ Refl impossible
head_reversible SBoolean _ Refl impossible
head_reversible SNumber _ Refl impossible
head_reversible SText _ Refl impossible
head_reversible (SArray False _) _ prf = rewrite sym $ justInjective prf in Refl
head_reversible (SArray True _) _ Refl impossible
head_reversible (SObject _) _ Refl impossible

convert_reversible : (k, k' : PrimitiveKind) -> (m : List (PrimitiveValue, PrimitiveValue)) ->
    (s : Schema) -> (s' : Schema) ->
    transform_schema (Convert k k' m) s = Just s' -> transform_schema (reverse_lens (Convert k k' m)) s' = Just s
convert_reversible k k' m s s' prf with (validate_map k k' m) proof prf1
    convert_reversible KBoolean KBoolean _ _ _ prf | False = absurd $ prf
    convert_reversible KBoolean KNumber _ _ _ prf | False = absurd $ prf
    convert_reversible KBoolean KText _ _ _ prf | False = absurd $ prf
    convert_reversible KNumber KBoolean _ _ _ prf | False = absurd $ prf
    convert_reversible KNumber KNumber _ _ _ prf | False = absurd $ prf
    convert_reversible KNumber KText _ _ _ prf | False = absurd $ prf
    convert_reversible KText KBoolean _ _ _ prf | False = absurd $ prf
    convert_reversible KText KNumber _ _ _ prf | False = absurd $ prf
    convert_reversible KText KText _ _ _ prf | False = absurd $ prf
    convert_reversible KBoolean KBoolean _ SNull _ prf | True = absurd $ prf
    convert_reversible KBoolean KBoolean _ SBoolean SNull prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KBoolean m SBoolean SBoolean prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KBoolean KBoolean m prf1 in Refl
    convert_reversible KBoolean KBoolean _ SBoolean SNumber prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KBoolean _ SBoolean SText prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KBoolean _ SBoolean (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KBoolean _ SBoolean (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KBoolean _ SNumber _ prf | True = absurd $ prf
    convert_reversible KBoolean KBoolean _ SText _ prf | True = absurd $ prf
    convert_reversible KBoolean KBoolean _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KBoolean KBoolean _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KBoolean KNumber _ SNull _ prf | True = absurd $ prf
    convert_reversible KBoolean KNumber _ SBoolean SNull prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KNumber _ SBoolean SBoolean prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KNumber m SBoolean SNumber prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KBoolean KNumber m prf1 in Refl
    convert_reversible KBoolean KNumber _ SBoolean SText prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KNumber _ SBoolean (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KNumber _ SBoolean (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KNumber _ SNumber _ prf | True = absurd $ prf
    convert_reversible KBoolean KNumber _ SText _ prf | True = absurd $ prf
    convert_reversible KBoolean KNumber _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KBoolean KNumber _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KBoolean KText _ SNull _ prf | True = absurd $ prf
    convert_reversible KBoolean KText _ SBoolean SNull prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KText _ SBoolean SBoolean prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KText _ SBoolean SNumber prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KText m SBoolean SText prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KBoolean KText m prf1 in Refl
    convert_reversible KBoolean KText _ SBoolean (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KText _ SBoolean (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KBoolean KText _ SNumber _ prf | True = absurd $ prf
    convert_reversible KBoolean KText _ SText _ prf | True = absurd $ prf
    convert_reversible KBoolean KText _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KBoolean KText _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KNumber KBoolean _ SNull _ prf | True = absurd $ prf
    convert_reversible KNumber KBoolean _ SBoolean _ prf | True = absurd $ prf
    convert_reversible KNumber KBoolean _ SNumber SNull prf | True = absurd $ justInjective prf
    convert_reversible KNumber KBoolean m SNumber SBoolean prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KNumber KBoolean m prf1 in Refl
    convert_reversible KNumber KBoolean _ SNumber SNumber prf | True = absurd $ justInjective prf
    convert_reversible KNumber KBoolean _ SNumber SText prf | True = absurd $ justInjective prf
    convert_reversible KNumber KBoolean _ SNumber (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KNumber KBoolean _ SNumber (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KNumber KBoolean _ SText _ prf | True = absurd $ prf
    convert_reversible KNumber KBoolean _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KNumber KBoolean _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KNumber KNumber _ SNull _ prf | True = absurd $ prf
    convert_reversible KNumber KNumber _ SBoolean _ prf | True = absurd $ prf
    convert_reversible KNumber KNumber _ SNumber SNull prf | True = absurd $ justInjective prf
    convert_reversible KNumber KNumber _ SNumber SBoolean prf | True = absurd $ justInjective prf
    convert_reversible KNumber KNumber m SNumber SNumber prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KNumber KNumber m prf1 in Refl
    convert_reversible KNumber KNumber _ SNumber SText prf | True = absurd $ justInjective prf
    convert_reversible KNumber KNumber _ SNumber (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KNumber KNumber _ SNumber (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KNumber KNumber _ SText _ prf | True = absurd $ prf
    convert_reversible KNumber KNumber _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KNumber KNumber _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KNumber KText _ SNull _ prf | True = absurd $ prf
    convert_reversible KNumber KText _ SBoolean _ prf | True = absurd $ prf
    convert_reversible KNumber KText _ SNumber SNull prf | True = absurd $ justInjective prf
    convert_reversible KNumber KText _ SNumber SBoolean prf | True = absurd $ justInjective prf
    convert_reversible KNumber KText _ SNumber SNumber prf | True = absurd $ justInjective prf
    convert_reversible KNumber KText m SNumber SText prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KNumber KText m prf1 in Refl
    convert_reversible KNumber KText _ SNumber (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KNumber KText _ SNumber (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KNumber KText _ SText _ prf | True = absurd $ prf
    convert_reversible KNumber KText _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KNumber KText _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KText KBoolean _ SNull _ prf | True = absurd $ prf
    convert_reversible KText KBoolean _ SBoolean _ prf | True = absurd $ prf
    convert_reversible KText KBoolean _ SNumber _ prf | True = absurd $ prf
    convert_reversible KText KBoolean _ SText SNull prf | True = absurd $ justInjective prf
    convert_reversible KText KBoolean m SText SBoolean prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KText KBoolean m prf1 in Refl
    convert_reversible KText KBoolean _ SText SNumber prf | True = absurd $ justInjective prf
    convert_reversible KText KBoolean _ SText SText prf | True = absurd $ justInjective prf
    convert_reversible KText KBoolean _ SText (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KText KBoolean _ SText (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KText KBoolean _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KText KBoolean _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KText KNumber _ SNull _ prf | True = absurd $ prf
    convert_reversible KText KNumber _ SBoolean _ prf | True = absurd $ prf
    convert_reversible KText KNumber _ SNumber _ prf | True = absurd $ prf
    convert_reversible KText KNumber _ SText SNull prf | True = absurd $ justInjective prf
    convert_reversible KText KNumber _ SText SBoolean prf | True = absurd $ justInjective prf
    convert_reversible KText KNumber m SText SNumber prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KText KNumber m prf1 in Refl
    convert_reversible KText KNumber _ SText SText prf | True = absurd $ justInjective prf
    convert_reversible KText KNumber _ SText (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KText KNumber _ SText (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KText KNumber _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KText KNumber _ (SObject _) _ prf | True = absurd $ prf
    convert_reversible KText KText _ SNull _ prf | True = absurd $ prf
    convert_reversible KText KText _ SBoolean _ prf | True = absurd $ prf
    convert_reversible KText KText _ SNumber _ prf | True = absurd $ prf
    convert_reversible KText KText _ SText SNull prf | True = absurd $ justInjective prf
    convert_reversible KText KText _ SText SBoolean prf | True = absurd $ justInjective prf
    convert_reversible KText KText _ SText SNumber prf | True = absurd $ justInjective prf
    convert_reversible KText KText m SText SText prf | True =
        rewrite sym $ justInjective prf in
        rewrite flip_map_preserves_validity KText KText m prf1 in Refl
    convert_reversible KText KText _ SText (SArray _ _) prf | True = absurd $ justInjective prf
    convert_reversible KText KText _ SText (SObject _) prf | True = absurd $ justInjective prf
    convert_reversible KText KText _ (SArray _ _) _ prf | True = absurd $ prf
    convert_reversible KText KText _ (SObject _) _ prf | True = absurd $ prf

||| Forwards and backwards compatibility requires schema transformations to be reversible
lens_reversible : (l : Lens) -> (s : Schema) -> (s' : Schema) ->
    transform_schema l s = Just s' -> transform_schema (reverse_lens l) s' = Just s
lens_reversible (Make k) s s' prf = make_reversible k s s' prf
lens_reversible (Destroy k) s s' prf = destroy_reversible k s s' prf
lens_reversible (AddProperty k) s s' prf = add_property_reversible k s s' prf
lens_reversible (RemoveProperty k) s s' prf = remove_property_reversible k s s' prf
lens_reversible (RenameProperty k k') s s' prf = rename_property_reversible k k' s s' prf
lens_reversible (HoistProperty h t) s s' prf = hoist_property_reversible h t s s' prf
lens_reversible (PlungeProperty h t) s s' prf = plunge_property_reversible h t s s' prf
lens_reversible Wrap s s' prf = wrap_reversible s s' prf
lens_reversible Head s s' prf = head_reversible s s' prf
lens_reversible (LensIn _ _) SNull _ Refl impossible
lens_reversible (LensIn _ _) SBoolean _ Refl impossible
lens_reversible (LensIn _ _) SNumber _ Refl impossible
lens_reversible (LensIn _ _) SText _ Refl impossible
lens_reversible (LensIn _ _) (SArray _ _) _ Refl impossible
lens_reversible (LensIn k l) (SObject m) s' prf with (get k m) proof prf1
    lens_reversible (LensIn k l) (SObject m) s' prf | Nothing = absurd $ prf
    lens_reversible (LensIn k l) (SObject m) s' prf | (Just s2) with (transform_schema l s2) proof prf2
        lens_reversible (LensIn k l) (SObject m) s' prf | (Just s2) | Nothing = absurd $ prf
        lens_reversible (LensIn k l) (SObject m) s' prf | (Just s2) | (Just s2') =
            rewrite sym $ justInjective prf in
            rewrite update_eq m k (Just s2') in
            rewrite lens_reversible l s2 s2' prf2 in
            rewrite update_shadow m k (Just s2') (Just s2) in
            rewrite update_same m k (Just s2) prf1 in Refl
lens_reversible (LensMap _) SNull _ Refl impossible
lens_reversible (LensMap _) SBoolean _ Refl impossible
lens_reversible (LensMap _) SNumber _ Refl impossible
lens_reversible (LensMap _) SText _ Refl impossible
lens_reversible (LensMap l) (SArray e s2) s' prf with (transform_schema l s2) proof prf1
    lens_reversible (LensMap l) (SArray e s2) s' prf | Nothing = absurd $ prf
    lens_reversible (LensMap l) (SArray e s2) s' prf | (Just s2') =
        rewrite sym $ justInjective prf in
        rewrite lens_reversible l s2 s2' prf1 in Refl
lens_reversible (LensMap _) (SObject _) _ Refl impossible
lens_reversible (Convert k k' m) s s' prf = convert_reversible k k' m s s' prf

max_stars_repo_name: Actyx/cambria

max_issues_repo_name: Actyx/cambria

max_forks_repo_name: Actyx/cambria