text:
module main-old where

import parse
import run
open import lib
open import cedille-types

-- for parser for Cedille source files
import cedille
module parsem = parse cedille.gratr2-nt ptr
open parsem.pnoderiv cedille.rrs cedille.cedille-rtn

module pr = run ptr
open pr.noderiv {- from run.agda -}

-- for parser for options files
import options
import options-types
module parsem2 = parse options.gratr2-nt options-types.ptr
module options-parse = parsem2.pnoderiv options.rrs options.options-rtn
module pr2 = run options-types.ptr
module options-run = pr2.noderiv

-- for parser for Cedille comments & whitespace
import cws
import cws-types
module parsem3 = parse cws.gratr2-nt cws-types.ptr
module cws-parse = parsem3.pnoderiv cws.rrs cws.cws-rtn
module pr3 = run cws.ptr
module cws-run = pr3.noderiv

--open import cedille-find
--open import classify
open import ctxt
open import constants
--open import conversion
open import general-util
open import process-cmd
open import spans
open import syntax-util
open import to-string
open import toplevel-state
import interactive-cmds

open import rkt

opts : Set
opts = options-types.opts

{-------------------------------------------------------------------------------
  .cede support
-------------------------------------------------------------------------------}
dot-cedille-directory : string → string
dot-cedille-directory dir = combineFileNames dir ".cedille"

cede-filename : (ced-path : string) → string
cede-filename ced-path =
  let dir = takeDirectory ced-path in
  let unit-name = base-filename (takeFileName ced-path) in
    combineFileNames (dot-cedille-directory dir) (unit-name ^ ".cede")

-- .cede files are just a dump of the spans, prefixed by 'e' if there is an error
write-cede-file : (ced-path : string) → (ie : include-elt) → IO ⊤
write-cede-file ced-path ie =
--  putStrLn ("write-cede-file " ^ ced-path ^ " : " ^ contents) >>
  let dir = takeDirectory ced-path in
    createDirectoryIfMissing ff (dot-cedille-directory dir) >>
    writeFile (cede-filename ced-path)
      ((if (include-elt.err ie) then "e" else "") ^
        (include-elt-spans-to-string ie))

-- we assume the cede file is known to exist at this point
read-cede-file : (ced-path : string) → IO (𝔹 × string)
read-cede-file ced-path =
  get-file-contents (cede-filename ced-path) >>= λ c → finish c
  where finish : maybe string → IO (𝔹 × string)
        finish nothing = return (tt , global-error-string ("Could not read the file " ^ cede-filename ced-path ^ "."))
        finish (just ss) with string-to-𝕃char ss
        finish (just ss)  | ('e' :: ss') = forceFileRead ss >> return (tt , 𝕃char-to-string ss')
        finish (just ss) | _ = forceFileRead ss >> return (ff , ss)

add-cedille-extension : string → string
add-cedille-extension x = x ^ "." ^ cedille-extension

find-imported-file : (dirs : 𝕃 string) → (unit-name : string) → IO string
find-imported-file [] unit-name = return (add-cedille-extension unit-name) -- assume the current directory if the unit is not found
find-imported-file (dir :: dirs) unit-name =
  let e = combineFileNames dir (add-cedille-extension unit-name) in

    doesFileExist e >>= λ b →
    if b then
      return e
    else
      find-imported-file dirs unit-name

-- return a list of pairs (i,p) where i is the import string in the file, and p is the full path for that imported file
find-imported-files : (dirs : 𝕃 string) → (imports : 𝕃 string) → IO (𝕃 (string × string))
find-imported-files dirs (u :: us) =
  find-imported-file dirs u >>= λ p →
  find-imported-files dirs us >>= λ ps →
    return ((u , p) :: ps)
find-imported-files dirs [] = return []

ced-file-up-to-date : (ced-path : string) → IO 𝔹
ced-file-up-to-date ced-path =
  let e = cede-filename ced-path in
    doesFileExist e >>= λ b →
    if b then
      fileIsOlder ced-path e
    else
      return ff

paths-to-𝕃string : options-types.paths → 𝕃 string
paths-to-𝕃string options-types.PathsNil = []
paths-to-𝕃string (options-types.PathsCons p ps) = p :: paths-to-𝕃string ps

opts-get-include-path : opts → 𝕃 string
opts-get-include-path options-types.OptsNil = []
opts-get-include-path (options-types.OptsCons (options-types.Lib ps) oo) = (paths-to-𝕃string ps) ++ opts-get-include-path oo
opts-get-include-path (options-types.OptsCons options-types.NoCedeFiles oo) = opts-get-include-path oo
opts-get-include-path (options-types.OptsCons options-types.NoRktFiles oo) = opts-get-include-path oo
--opts-get-include-path (options-types.OptsCons _ oo) = opts-get-include-path oo

{- see if "no-cede-files" is turned on in the options file -}
opts-get-no-cede-files : opts → 𝔹
opts-get-no-cede-files options-types.OptsNil = ff
opts-get-no-cede-files (options-types.OptsCons options-types.NoCedeFiles oo) = tt
opts-get-no-cede-files (options-types.OptsCons options-types.NoRktFiles oo) = opts-get-no-cede-files oo
opts-get-no-cede-files (options-types.OptsCons (options-types.Lib _) oo) = opts-get-no-cede-files oo

{- see if "no-rkt-files" is turned on in the options file -}
opts-get-no-rkt-files : opts → 𝔹
opts-get-no-rkt-files options-types.OptsNil = ff
opts-get-no-rkt-files (options-types.OptsCons options-types.NoCedeFiles oo) = opts-get-no-rkt-files oo
opts-get-no-rkt-files (options-types.OptsCons options-types.NoRktFiles oo) = tt
opts-get-no-rkt-files (options-types.OptsCons (options-types.Lib _) oo) = opts-get-no-rkt-files oo

{- reparse the given file, and update its include-elt in the toplevel-state appropriately -}
reparse : toplevel-state → (filename : string) → IO toplevel-state
reparse st filename =
--   putStrLn ("reparsing " ^ filename) >>
   doesFileExist filename >>= λ b →
     (if b then
         (readFiniteFile filename >>= processText)
      else return (error-include-elt ("The file " ^ filename ^ " could not be opened for reading."))) >>= λ ie →
        return (set-include-elt st filename ie)
  where processText : string → IO include-elt
        processText x with string-to-𝕃char x
        processText x | s with runRtn s
        processText x | s | inj₁ cs = return (error-include-elt ("Parse error in file " ^ filename ^ " at position " ^ (ℕ-to-string (length s ∸ length cs)) ^ "."))
        processText x | s | inj₂ r with rewriteRun r
        processText x | s | inj₂ r | ParseTree (parsed-start t) :: [] with cws-parse.runRtn s
        processText x | s | inj₂ r | ParseTree (parsed-start t) :: [] | inj₁ cs = return (error-include-elt ("This shouldn't happen in " ^ filename ^ " at position "
                                                                                ^ (ℕ-to-string (length s ∸ length cs)) ^ "."))
        processText x | s | inj₂ r | ParseTree (parsed-start t) :: [] | inj₂ r2 with cws-parse.rewriteRun r2
        processText x | s | inj₂ r | ParseTree (parsed-start t) :: [] | inj₂ r2 | cws-run.ParseTree (cws-types.parsed-start t2) :: [] = find-imported-files (toplevel-state.include-path st)
                                                                                (get-imports t) >>= λ deps → return
                                                                                (new-include-elt filename deps t t2)
        processText x | s | inj₂ r | ParseTree (parsed-start t) :: [] | inj₂ r2 | _ = return (error-include-elt ("Parse error in file " ^ filename ^ "."))
        processText x | s | inj₂ r | _ = return (error-include-elt ("Parse error in file " ^ filename ^ "."))

add-spans-if-up-to-date : (up-to-date : 𝔹) → (use-cede-files : 𝔹) → (filename : string) → include-elt → IO include-elt
add-spans-if-up-to-date up-to-date use-cede-files filename ie =
  if up-to-date && use-cede-files then
    (read-cede-file filename >>= finish)
  else
    return ie
  where finish : 𝔹 × string → IO include-elt
        finish (err , ss) = return (set-do-type-check-include-elt (set-spans-string-include-elt ie err ss) ff)

{- make sure that the current ast and dependencies are stored in the
   toplevel-state, updating the state as needed. -}
ensure-ast-deps : toplevel-state → (filename : string) → IO toplevel-state
ensure-ast-deps s filename with get-include-elt-if s filename
ensure-ast-deps s filename | nothing =
  let ucf = (toplevel-state.use-cede-files s) in
    reparse s filename >>= λ s →
    ced-file-up-to-date filename >>= λ up-to-date →
    add-spans-if-up-to-date up-to-date ucf filename (get-include-elt s filename) >>= λ ie →
    return (set-include-elt s filename ie)
ensure-ast-deps s filename | just ie =
  let ucf = (toplevel-state.use-cede-files s) in
    ced-file-up-to-date filename >>= λ up-to-date →
      if up-to-date then
        (add-spans-if-up-to-date up-to-date (toplevel-state.use-cede-files s) filename (get-include-elt s filename) >>= λ ie →
         return (set-include-elt s filename ie))
      else reparse s filename

{- helper function for update-asts, which keeps track of the files we have seen so
   we avoid importing the same file twice, and also avoid following cycles in the import
   graph. -}
{-# TERMINATING #-}
update-astsh : stringset {- seen already -} → toplevel-state → (filename : string) →
               IO (stringset {- seen already -} × toplevel-state)
update-astsh seen s filename =
--  putStrLn ("update-astsh [filename = " ^ filename ^ "]") >>
  if stringset-contains seen filename then return (seen , s)
  else (ensure-ast-deps s filename >>= cont (stringset-insert seen filename))
  where cont : stringset → toplevel-state → IO (stringset × toplevel-state)
        cont seen s with get-include-elt s filename
        cont seen s | ie with include-elt.deps ie
        cont seen s | ie | ds =
          proc seen s ds
          where proc : stringset → toplevel-state → 𝕃 string → IO (stringset × toplevel-state)
                proc seen s [] =
                  if (list-any (get-do-type-check s) ds)
                  then return (seen , set-include-elt s filename (set-do-type-check-include-elt ie tt))
                  else return (seen , s)
                proc seen s (d :: ds) = update-astsh seen s d >>= λ p →
                                        proc (fst p) (snd p) ds

{- this function updates the ast associated with the given filename in the toplevel state.
   So if we do not have an up-to-date .cede file (i.e., there is no such file at all,
   or it is older than the given file), reparse the file.  We do this recursively for all
   dependencies (i.e., imports) of the file. -}
update-asts : toplevel-state → (filename : string) → IO toplevel-state
update-asts s filename = update-astsh empty-stringset s filename >>= λ p →
  return (snd p)

{- this function checks the given file (if necessary), updates .cede and .rkt files (again, if necessary), and replies on stdout if appropriate -}
checkFile : toplevel-state → (filename : string) → (should-print-spans : 𝔹) → IO toplevel-state
checkFile s filename should-print-spans =
--  putStrLn ("checkFile " ^ filename) >>
  update-asts s filename >>= λ s →
  finish (process-file s filename) -- ignore-errors s filename)

  where reply : toplevel-state → IO ⊤
        reply s with get-include-elt-if s filename
        reply s | nothing = putStrLn (global-error-string ("Internal error looking up information for file " ^ filename ^ "."))
        reply s | just ie =
           if should-print-spans then
             putStrLn (include-elt-spans-to-string ie)
           else return triv
        finish : toplevel-state × mod-info → IO toplevel-state
        finish (s , m) with s
        finish (s , m) | mk-toplevel-state use-cede make-rkt ip mod is Γ =
          writeo mod >>
          reply s >>
          return (mk-toplevel-state use-cede make-rkt ip [] is (ctxt-set-current-mod Γ m))
            where
              writeo : 𝕃 string → IO ⊤
              writeo [] = return triv
              writeo (f :: us) =
                let ie = get-include-elt s f in
                  (if use-cede then (write-cede-file f ie) else (return triv)) >>
                  (if make-rkt then (write-rkt-file f (toplevel-state.Γ s) ie) else (return triv)) >>
                  writeo us

remove-dup-include-paths : 𝕃 string → 𝕃 string
remove-dup-include-paths l = stringset-strings (stringset-insert* empty-stringset l)

-- this is the function that handles requests (from the frontend) on standard input
{-# TERMINATING #-}
readCommandsFromFrontend : toplevel-state → IO ⊤
readCommandsFromFrontend s =
    getLine >>= λ input →
    let input-list : 𝕃 string
        input-list = (string-split (undo-escape-string input) delimiter)
            in (handleCommands input-list s) >>= λ s →
        readCommandsFromFrontend s
        where
            delimiter : char
            delimiter = '§'

            errorCommand : 𝕃 string → toplevel-state → IO toplevel-state
            errorCommand ls s = putStrLn (global-error-string "Invalid command sequence \"" ^ (𝕃-to-string (λ x → x) ", " ls) ^ "\".") >>= λ x → return s

            debugCommand : toplevel-state → IO toplevel-state
            debugCommand s = putStrLn (escape-string (toplevel-state-to-string s)) >>= λ x → return s

            checkCommand : 𝕃 string → toplevel-state → IO toplevel-state
            checkCommand (input :: []) s = canonicalizePath input >>= λ input-filename →
                        checkFile (set-include-path s (remove-dup-include-paths (takeDirectory input-filename :: toplevel-state.include-path s)))
                        input-filename tt {- should-print-spans -}
            checkCommand ls s = errorCommand ls s

            interactiveCommand : 𝕃 string → toplevel-state → IO toplevel-state
            interactiveCommand xs s = interactive-cmds.interactive-cmd xs s

  {-          findCommand : 𝕃 string → toplevel-state → IO toplevel-state
            findCommand (symbol :: []) s = putStrLn (find-symbols-to-JSON symbol (toplevel-state-lookup-occurrences symbol s)) >>= λ x → return s
            findCommand _ s = errorCommand s -}

            handleCommands : 𝕃 string → toplevel-state → IO toplevel-state
            handleCommands ("check" :: xs) s = checkCommand xs s
            handleCommands ("debug" :: []) s = debugCommand s
            handleCommands ("interactive" :: xs) s = interactiveCommand xs s
--            handleCommands ("find" :: xs) s = findCommand xs s
            handleCommands ls s = errorCommand ls s

-- function to process command-line arguments
processArgs : opts → 𝕃 string → IO ⊤

-- this is the case for when we are called with a single command-line argument, the name of the file to process
processArgs oo (input-filename :: []) =
  canonicalizePath input-filename >>= λ input-filename →
  checkFile (new-toplevel-state (takeDirectory input-filename :: opts-get-include-path oo) (~ (opts-get-no-cede-files oo)) (~ (opts-get-no-rkt-files oo)) )
    input-filename ff {- should-print-spans -} >>= finish input-filename
  where finish : string → toplevel-state → IO ⊤
        finish input-filename s =
          let ie = get-include-elt s input-filename in
          if include-elt.err ie then (putStrLn (include-elt-spans-to-string ie)) else return triv

-- this is the case where we will go into a loop reading commands from stdin, from the fronted
processArgs oo [] = readCommandsFromFrontend (new-toplevel-state (opts-get-include-path oo) (~ (opts-get-no-cede-files oo)) (~ (opts-get-no-rkt-files oo)))

-- all other cases are errors
processArgs oo xs = putStrLn ("Run with the name of one file to process, or run with no command-line arguments and enter the\n"
                         ^ "names of files one at a time followed by newlines (this is for the emacs mode).")

-- helper function to try to parse the options file
processOptions : string → string → (string ⊎ options-types.opts)
processOptions filename s with string-to-𝕃char s
...                       | i with options-parse.runRtn i
...                           | inj₁ cs =
                                     inj₁ ("Parse error in file " ^ filename ^ " at position " ^ (ℕ-to-string (length i ∸ length cs)) ^ ".")
...                           | inj₂ r with options-parse.rewriteRun r
...                                    | options-run.ParseTree (options-types.parsed-start (options-types.File oo)) :: [] = inj₂ oo
...                                    | _ =  inj₁ ("Parse error in file " ^ filename ^ ". ")

-- read the ~/.cedille/options file
readOptions : IO (string ⊎ options-types.opts)
readOptions =
  getHomeDirectory >>= λ homedir →
    let homecedir = dot-cedille-directory homedir in
    let optsfile = combineFileNames homecedir options-file-name in
      createDirectoryIfMissing ff homecedir >>
      doesFileExist optsfile >>= λ b →
       if b then
         (readFiniteFile optsfile >>= λ f → return (processOptions optsfile f))
       else
         (return (inj₂ options-types.OptsNil))

postulate
  initializeStdinToUTF8 : IO ⊤
  setStdinNewlineMode : IO ⊤
{-# COMPILED initializeStdinToUTF8  System.IO.hSetEncoding System.IO.stdin System.IO.utf8 #-}
{-# COMPILED setStdinNewlineMode System.IO.hSetNewlineMode System.IO.stdin System.IO.universalNewlineMode #-}

-- main entrypoint for the backend
main : IO ⊤
main = initializeStdoutToUTF8 >>
       initializeStdinToUTF8 >>
       setStdoutNewlineMode >>
       setStdinNewlineMode >>
       readOptions >>=
       next
  where next : string ⊎ options-types.opts → IO ⊤
        next (inj₁ s) = putStrLn (global-error-string s)
        next (inj₂ oo) = getArgs >>= processArgs oo

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module Utils.HaskellFunctions where

open import bool
open import maybe

open import Utils.HaskellTypes

postulate _str-eq_ : String → String → 𝔹
{-# COMPILED _str-eq_ (==) #-}

infixr 20 _++s_
postulate _++s_ : String → String → String
{-# COMPILED _++s_ Data.Text.append #-}

fst : {A B : Set} → Prod A B → A
fst (x , y) = x

snd : {A B : Set} → Prod A B → B
snd (x , y) = y

fstT : {A B C : Set} → Triple A B C → A
fstT (triple x y z) = x

sndT : {A B C : Set} → Triple A B C → B
sndT (triple x y z) = y

trdT : {A B C : Set} → Triple A B C → C
trdT (triple x y z) = z

fstMapT : {A₁ A₂ B C : Set} → (A₁ → A₂) → Triple A₁ B C → Triple A₂ B C
fstMapT f (triple x y z) = triple (f x) y z

_++_ : {A : Set} → List A → List A → List A
[] ++ l₂ = l₂
(x :: l₁) ++ l₂ = x :: (l₁ ++ l₂)

map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x :: xs) = f x :: map f xs

list-member : {A : Set}(eq : A → A → 𝔹)(a : A)(l : List A) → 𝔹
list-member eq a [] = ff
list-member eq a (x :: xs) with eq a x
... | tt = tt
... | ff = list-member eq a xs

foldr : {A : Set}{B : Set} → (A → B → B) → B → List A → B
foldr f b [] = b
foldr f b (a :: as) = f a (foldr f b as)

foldl : {A : Set}{B : Set} → (B → A → B) → B → List A → B
foldl f b [] = b
foldl f b (x :: xs) = foldl f (f b x) xs

lookup : ∀{A B} → (A → A → 𝔹) → A → List (Prod A B) → maybe B
lookup _eq_ x [] = nothing
lookup _eq_ x ((y , b) :: l) with x eq y
... | tt = just b
... | ff = lookup _eq_ x l

disjoint : {A : Set} → (A → A → 𝔹) → List A → List A → 𝔹
disjoint _eq_ (x :: l₁) (y :: l₂) with x eq y
... | tt = ff
... | ff = disjoint _eq_ l₁ l₂
disjoint _ [] _ = tt
disjoint _ _ [] = tt

ext: agda

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
module Coirc.Network where
open import Function
open import Coinduction
open import Data.Unit
open import Data.String
open import Data.Maybe
open import IO
open import Coirc
open import Coirc.Parser
import Coirc.Network.Primitive as Prim

private
  Handle = Prim.Handle

  hConnect : String → IO Handle
  hConnect s = lift (Prim.hConnect s)

  hGetLine : Handle → IO String
  hGetLine h =
    ♯ lift (Prim.hGetLine h) >>= λ s →
    ♯ (♯ putStrLn s >>
       ♯ return (s ++ "\n"))

  hPutStr : Handle → String → IO ⊤
  hPutStr h s = ♯ lift (Prim.hPutStr h s) >> ♯ return tt

  hSend : Handle → String → IO ⊤
  hSend h s =
    ♯ putStrLn ("> " ++ s) >>
    ♯ hPutStr h (s ++ "\r\n")

  getEvent : Handle → IO (Maybe Event)
  getEvent h = ♯ hGetLine h >>= (λ x → ♯ f x) where
    f : String → IO (Maybe Event)
    f = return ∘ parse-Event ∘ toList

  runAction : Handle → Action → IO ⊤
  runAction h (print text) =
    putStrLn text
  runAction h (nick name) =
    hSend h ("NICK " ++ name)
  runAction h (user name real) =
    hSend h ("USER " ++ name ++ " 0 * :" ++ real)
  runAction h (pong name) =
    hSend h ("PONG " ++ name)
  runAction h (join channel) =
    hSend h ("JOIN " ++ channel)
  runAction h (part channel) =
    hSend h ("PART " ++ channel)
  runAction h (privmsg target text) =
    hSend h ("PRIVMSG " ++ target ++ " :" ++ text)
  runAction h (quit text) =
    hSend h ("QUIT :" ++ text)

  runSP : Handle → Bot → IO ⊤
  runSP h (get f) =
    ♯ getEvent h >>= λ e? →
    ♯ g e?
    where
    g : Maybe Event → IO ⊤
    g nothing =
      ♯ putStrLn "<disconnect>" >>
      ♯ return tt
    g (just e) = runSP h (f e)
  runSP h (put a sp) =
    ♯ runAction h a >>
    ♯ runSP h (♭ sp)

runBot : Bot → String → IO ⊤
runBot bot server =
  ♯ hConnect server >>= λ h →
  ♯ runSP h bot

max_stars_repo_name: larrytheliquid/coirc

max_issues_repo_name: larrytheliquid/coirc

max_forks_repo_name: larrytheliquid/coirc


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation: Task B
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module DistributiveLaws.TaskB.UnprovedATP where

open import DistributiveLaws.Base

------------------------------------------------------------------------------
-- 2018-06-28: The ATPs could not prove the theorem (300 sec).
postulate
  prop₂ : ∀ u x y z →
          (x · y · (z · u)) · ((x · y · (z · u)) · (x · z · (y · u))) ≡
            x · z · (y · u)
{-# ATP prove prop₂ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module DynTheory where

open import Prelude
open import T

---- Some theory about the dynamic semantics

module DynTheory where

  -- prove some obvious theorems about iterated stepping
  -- transitivity (which makes sense, given that it is the transitive closure)
  eval-trans : ∀{A} {e e' e'' : TCExp A} →
                e ~>* e' → e' ~>* e'' → e ~>* e''
  eval-trans eval-refl E2 = E2
  eval-trans (eval-cons S1 E1') E2 = eval-cons S1 (eval-trans E1' E2)

  -- prove that we can life any compatibility rule from steps to eval
  eval-compat : ∀{A B} {P : TCExp A -> TCExp B} →
                 (∀{e e'} → (e ~> e' → P e ~> P e')) →
                 {e e' : TCExp A} → e ~>* e' → P e ~>* P e'
  eval-compat f eval-refl = eval-refl
  eval-compat f (eval-cons S1 D) = eval-cons (f S1) (eval-compat f D)

  -- Lemma we need to prove determism
  not-val-and-step : ∀{C : Set} {A : TTp} {e e' : TCExp A} →
                     TVal e → e ~> e' →
                     C
  not-val-and-step val-zero ()
  not-val-and-step val-lam ()
  not-val-and-step (val-suc v) (step-suc S1) = not-val-and-step v S1

  -- Show that the dynamic semantics are a function
  step-deterministic : ∀{A} → (e : TCExp A) → {e' e'' : TCExp A} →
                       e ~> e' → e ~> e'' ->
                       e' ≡ e''
  -- Trivial contradictory cases
  step-deterministic (var x) () S2
  step-deterministic (Λ e) () S2
  step-deterministic zero () S2
  step-deterministic (Λ e $ e') step-beta (step-app-l ())
  step-deterministic (Λ e $ e') (step-app-l ()) step-beta
  step-deterministic (rec .zero e'' e₂) (step-rec ()) step-rec-z
  step-deterministic (rec zero e₀ es) step-rec-z (step-rec ())

  -- Nontrival contradictory cases
  step-deterministic (rec (suc e) e₁ e₂) (step-rec (step-suc S1)) (step-rec-s v) = not-val-and-step v S1
  step-deterministic (rec (suc e) e₁ e₂) (step-rec-s v) (step-rec (step-suc S2)) = not-val-and-step v S2

  -- Normal cases
  step-deterministic (e $ e') (step-app-l S1) (step-app-l S2) =
                   resp (λ x → x $ e') (step-deterministic e S1 S2)
  step-deterministic (Λ e $ e') step-beta step-beta = Refl
  step-deterministic (suc e) (step-suc S1) (step-suc S2) = resp suc (step-deterministic e S1 S2)
  step-deterministic (rec e e₁ e₂) (step-rec S1) (step-rec S2) =
                    resp (λ x → rec x e₁ e₂) (step-deterministic e S1 S2)
  step-deterministic (rec zero _ _) step-rec-z step-rec-z = Refl
  step-deterministic (rec (suc e) e₁ e₂) (step-rec-s x) (step-rec-s x₁) = Refl

  -- Prove that if we evaluate to two expressions, and one is a value,
  -- then the other evaluates to it.
  eval-finish : ∀{A} → {e : TCExp A} → {e' e'' : TCExp A} →
                e ~>* e' → e ~>* e'' →
                TVal e'' →
                e' ~>* e''
  eval-finish eval-refl E2 v = E2
  eval-finish (eval-cons S1 E1) eval-refl v = not-val-and-step v S1
  eval-finish (eval-cons S1 E1) (eval-cons S2 E2) v with step-deterministic _ S1 S2
  ... | Refl = eval-finish E1 E2 v

  -- Prove that if we evaluate to two values, they are the same
  eval-deterministic : ∀{A} → {e : TCExp A} → {e' e'' : TCExp A} →
                       e ~>* e' → e ~>* e'' →
                       TVal e' → TVal e'' →
                       e' ≡ e''
  eval-deterministic E1 E2 v1 v2 with eval-finish E1 E2 v2
  ... | eval-refl = Refl
  ... | eval-cons S1 _ = not-val-and-step v1 S1

open DynTheory public

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Nat.Mod where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order

-- Defining x mod 0 to be 0. This way all the theorems below are true
-- for n : ℕ instead of n : ℕ₊₁.

------ Preliminary definitions ------
modInd : (n : ℕ) → ℕ → ℕ
modInd n = +induction n (λ _ → ℕ) (λ x _ → x) λ _ x → x

modIndBase : (n m : ℕ) → m < suc n → modInd n m ≡ m
modIndBase n = +inductionBase n (λ _ → ℕ) (λ x _ → x) (λ _ x → x)

modIndStep : (n m : ℕ) → modInd n (suc n + m) ≡ modInd n m
modIndStep n = +inductionStep n (λ _ → ℕ) (λ x _ → x) (λ _ x → x)
-------------------------------------

_mod_ : (x n : ℕ) → ℕ
x mod zero = 0
x mod (suc n) = modInd n x

mod< : (n x : ℕ) → x mod (suc n) < (suc n)
mod< n =
  +induction n
    (λ x → x mod (suc n) < suc n)
    (λ x base → fst base
               , (cong (λ x → fst base + suc x)
                       (modIndBase n x base)
                ∙ snd base))
     λ x ind → fst ind
              , cong (λ x → fst ind + suc x)
                     (modIndStep n x) ∙ snd ind

mod-rUnit : (n x : ℕ) → x mod n ≡ ((x + n) mod n)
mod-rUnit zero x = refl
mod-rUnit (suc n) x =
    sym (modIndStep n x)
  ∙ cong (modInd n) (+-comm (suc n) x)

mod-lUnit : (n x : ℕ) → x mod n ≡ ((n + x) mod n)
mod-lUnit zero _ = refl
mod-lUnit (suc n) x = sym (modIndStep n x)

mod+mod≡mod : (n x y : ℕ)
  → (x + y) mod n ≡ (((x mod n) + (y mod n)) mod n)
mod+mod≡mod zero _ _ = refl
mod+mod≡mod (suc n) =
  +induction n
    (λ z → (x : ℕ)
         → ((z + x) mod (suc n))
         ≡ (((z mod (suc n)) + (x mod (suc n))) mod (suc n)))
    (λ x p →
      +induction n _
        (λ y q → cong (modInd n)
                       (sym (cong₂  _+_ (modIndBase n x p)
                       (modIndBase n y q))))
        λ y ind → cong (modInd n)
                        (cong (x +_) (+-comm (suc n) y)
                                   ∙ (+-assoc x y (suc n)))
                     ∙∙ sym (mod-rUnit (suc n) (x + y))
                     ∙∙ ind
                      ∙ cong (λ z → modInd n
                                    ((modInd n x + z)))
                             (mod-rUnit (suc n) y
                             ∙ cong (modInd n) (+-comm y (suc n))))
    λ x p y →
      cong (modInd n) (cong suc (sym (+-assoc n x y)))
        ∙∙ sym (mod-lUnit (suc n) (x + y))
        ∙∙ p y
         ∙ sym (cong (modInd n)
                (cong (_+ modInd n y)
                 (cong (modInd n)
                  (+-comm (suc n) x) ∙ sym (mod-rUnit (suc n) x))))

mod-idempotent : {n : ℕ} (x : ℕ) → (x mod n) mod n ≡ x mod n
mod-idempotent {n = zero} _ = refl
mod-idempotent {n = suc n} =
  +induction n (λ x → (x mod suc n) mod (suc n) ≡ x mod (suc n))
             (λ x p → cong (_mod (suc n))
                            (modIndBase n x p))
              λ x p → cong (_mod (suc n))
                            (modIndStep n x)
                          ∙∙ p
                          ∙∙ mod-rUnit (suc n) x
                           ∙ (cong (_mod (suc n)) (+-comm x (suc n)))

mod-rCancel : (n x y : ℕ) → (x + y) mod n ≡ (x + y mod n) mod n
mod-rCancel zero x y = refl
mod-rCancel (suc n) x =
  +induction n _
    (λ y p → cong (λ z → (x + z) mod (suc n))
                   (sym (modIndBase n y p)))
     λ y p → cong (_mod suc n) (+-assoc x (suc n) y
                             ∙∙ (cong (_+ y) (+-comm x (suc n)))
                             ∙∙ sym (+-assoc (suc n) x y))
          ∙∙ sym (mod-lUnit (suc n) (x + y))
          ∙∙ (p ∙ cong (λ z → (x + z) mod suc n) (mod-lUnit (suc n) y))

mod-lCancel : (n x y : ℕ) → (x + y) mod n ≡ (x mod n + y) mod n
mod-lCancel n x y =
     cong (_mod n) (+-comm x y)
  ∙∙ mod-rCancel n y x
  ∙∙ cong (_mod n) (+-comm y (x mod n))

zero-charac : (n : ℕ) → n mod n ≡ 0
zero-charac zero = refl
zero-charac (suc n) = cong (_mod suc n) (+-comm 0 (suc n))
                  ∙∙ modIndStep n 0
                  ∙∙ modIndBase n 0 (n , (+-comm n 1))

-- remainder and quotient after division by n
-- Again, allowing for 0-division to get nicer syntax
remainder_/_ : (x n : ℕ) → ℕ
remainder x / zero = x
remainder x / suc n = x mod (suc n)

quotient_/_ : (x n : ℕ) → ℕ
quotient x / zero = 0
quotient x / suc n =
  +induction n (λ _ → ℕ) (λ _ _ → 0) (λ _ → suc) x

≡remainder+quotient : (n x : ℕ)
  → (remainder x / n) + n · (quotient x / n) ≡ x
≡remainder+quotient zero x = +-comm x 0
≡remainder+quotient (suc n) =
  +induction n
    (λ x → (remainder x / (suc n)) + (suc n)
          · (quotient x / (suc n)) ≡ x)
    (λ x base → cong₂ _+_ (modIndBase n x base)
                           (cong ((suc n) ·_)
                           (+inductionBase n _ _ _ x base))
              ∙∙ cong (x +_) (·-comm n 0)
              ∙∙ +-comm x 0)
     λ x ind → cong₂ _+_ (modIndStep n x)
                        (cong ((suc n) ·_) (+inductionStep n _ _ _ x))
          ∙∙ cong (modInd n x +_)
                  (·-suc (suc n) (+induction n _ _ _ x))
          ∙∙ cong (modInd n x +_)
                  (+-comm (suc n) ((suc n) · (+induction n _ _ _ x)))
          ∙∙ +-assoc (modInd n x) ((suc n) · +induction n _ _ _ x) (suc n)
          ∙∙ cong (_+ suc n) ind
           ∙ +-comm x (suc n)

private
  test₀ : 100 mod 81 ≡ 19
  test₀ = refl

  test₁ : ((11 + (10 mod 3)) mod 3) ≡ 0
  test₁ = refl

max_stars_repo_name: FernandoLarrain/cubical

max_issues_repo_name: FernandoLarrain/cubical

max_forks_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Group.MorphismProperties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Functions.Embedding
open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.NAryOp
open import Cubical.Structures.Pointed
open import Cubical.Structures.Semigroup hiding (⟨_⟩)
open import Cubical.Structures.Monoid hiding (⟨_⟩)

open import Cubical.Structures.Group.Base
open import Cubical.Structures.Group.Properties
open import Cubical.Structures.Group.Morphism

open Iso

private
  variable
    ℓ ℓ' ℓ'' : Level

isPropIsGroupHom : (G : Group {ℓ}) (H : Group {ℓ'}) {f : ⟨ G ⟩ → ⟨ H ⟩} → isProp (isGroupHom G H f)
isPropIsGroupHom G H {f} = isPropΠ2 λ a b → Group.is-set H _ _

isSetGroupHom : {G : Group {ℓ}} {H : Group {ℓ'}} → isSet (GroupHom G H)
isSetGroupHom {G = G} {H = H} = isOfHLevelRespectEquiv 2 equiv (isSetΣ (isSetΠ λ _ → is-set H) λ _ → isProp→isSet (isPropIsGroupHom G H)) where
  open Group
  equiv : (Σ[ g ∈ (Carrier G → Carrier H) ] (isGroupHom G H g)) ≃ GroupHom G H
  equiv = isoToEquiv (iso (λ (g , m) → grouphom g m) (λ (grouphom g m) → g , m) (λ _ → refl) λ _ → refl)

-- Morphism composition
isGroupHomComp : {F : Group {ℓ}} {G : Group {ℓ'}} {H : Group {ℓ''}} →
  (f : GroupHom F G) → (g : GroupHom G H) → isGroupHom F H (GroupHom.fun g ∘ GroupHom.fun f)
isGroupHomComp (grouphom f morph-f) (grouphom g morph-g) x y =
  cong g (morph-f _ _) ∙ morph-g _ _

compGroupHom : {F : Group {ℓ}} {G : Group {ℓ'}} {H : Group {ℓ''}} → GroupHom F G → GroupHom G H → GroupHom F H
compGroupHom {F = F} {G = G} {H = H} f g = grouphom _ (isGroupHomComp f g)

compGroupEquiv : {F : Group {ℓ}} {G : Group {ℓ'}} {H : Group {ℓ''}} → GroupEquiv F G → GroupEquiv G H → GroupEquiv F H
compGroupEquiv {F = F} {G = G} {H = H} f g =
  groupequiv (compEquiv f.eq g.eq) (isGroupHomComp f.hom g.hom) where
  module f = GroupEquiv f
  module g = GroupEquiv g

idGroupEquiv : (G : Group {ℓ}) → GroupEquiv G G
idGroupEquiv G = groupequiv (idEquiv (Group.Carrier G)) (λ _ _ → refl)

-- Isomorphism inversion
isGroupHomInv : {G : Group {ℓ}} {H : Group {ℓ'}} (f : GroupEquiv G H) → isGroupHom H G (invEq (GroupEquiv.eq f))
isGroupHomInv {G = G} {H = H}  (groupequiv (f , eq) morph) h h' = isInj-f _ _ (
  f (g (h ⋆² h') )
    ≡⟨ retEq (f , eq) _ ⟩
  h ⋆² h'
    ≡⟨ sym (λ i → retEq (f , eq) h i ⋆² retEq (f , eq) h' i) ⟩
  f (g h) ⋆² f (g h')
    ≡⟨ sym (morph _ _) ⟩
  f (g h ⋆¹ g h') ∎)
  where
  _⋆¹_ = Group._+_ G
  _⋆²_ = Group._+_ H
  g = invEq (f , eq)
  isEmbedding-f : isEmbedding f
  isEmbedding-f = isEquiv→isEmbedding eq
  isInj-f : (x y : ⟨ G ⟩) → f x ≡ f y → x ≡ y
  isInj-f x y = invEq (_ , isEquiv→isEmbedding eq x y)

invGroupEquiv : {G : Group {ℓ}} {H : Group {ℓ'}} → GroupEquiv G H → GroupEquiv H G
invGroupEquiv {G = G} {H = H} f = groupequiv (invEquiv (eq f)) (isGroupHomInv f) where open GroupEquiv

groupHomEq : {G : Group {ℓ}} {H : Group {ℓ'}} {f g : GroupHom G H} → (GroupHom.fun f ≡ GroupHom.fun g) → f ≡ g
groupHomEq {G = G} {H = H} {grouphom f fm} {grouphom g gm} p i = grouphom (p i) (p-hom i) where
  p-hom : PathP (λ i → isGroupHom G H (p i)) fm gm
  p-hom = toPathP (isPropIsGroupHom G H _ _)

groupEquivEq : {G : Group {ℓ}} {H : Group {ℓ'}} {f g : GroupEquiv G H} → (GroupEquiv.eq f ≡ GroupEquiv.eq g) → f ≡ g
groupEquivEq {G = G} {H = H} {groupequiv f fm} {groupequiv g gm} p i = groupequiv (p i) (p-hom i) where
  p-hom : PathP (λ i → isGroupHom G H (p i .fst)) fm gm
  p-hom = toPathP (isPropIsGroupHom G H _ _)

module GroupΣTheory {ℓ} where

  RawGroupStructure : Type ℓ → Type ℓ
  RawGroupStructure = SemigroupΣTheory.RawSemigroupStructure

  rawGroupUnivalentStr : UnivalentStr RawGroupStructure _
  rawGroupUnivalentStr = SemigroupΣTheory.rawSemigroupUnivalentStr

  -- The neutral element and the inverse function will be derived from the
  -- axioms, instead of being defined in the RawGroupStructure in order
  -- to have that group equivalences are equivalences that preserves
  -- multiplication (so we don't have to show that they also preserve inversion
  -- and neutral element, although they will preserve them).
  GroupAxioms : (G : Type ℓ) → RawGroupStructure G → Type ℓ
  GroupAxioms G _·_ =
      IsSemigroup _·_
    × (Σ[ e ∈ G ] ((x : G) → (x · e ≡ x) × (e · x ≡ x))
                × ((x : G) → Σ[ x' ∈ G ] (x · x' ≡ e) × (x' · x ≡ e)))

  GroupStructure : Type ℓ → Type ℓ
  GroupStructure = AxiomsStructure RawGroupStructure GroupAxioms

  GroupΣ : Type (ℓ-suc ℓ)
  GroupΣ = TypeWithStr ℓ GroupStructure

  -- Structured equivalences for groups are those for monoids (but different axioms)
  GroupEquivStr : StrEquiv GroupStructure ℓ
  GroupEquivStr = AxiomsEquivStr (BinaryFunEquivStr PointedEquivStr) GroupAxioms

  open MonoidTheory

  isPropGroupAxioms : (G : Type ℓ)
                      → (s : RawGroupStructure G)
                      → isProp (GroupAxioms G s)
  isPropGroupAxioms G _+_ = isPropΣ (isPropIsSemigroup _) γ
    where
    γ : (h : IsSemigroup _+_) →
        isProp (Σ[ e ∈ G ] ((x : G) → (x + e ≡ x) × (e + x ≡ x))
                         × ((x : G) → Σ[ x' ∈ G ] (x + x' ≡ e) × (x' + x ≡ e)))
    γ h (e , P , _) (e' , Q , _) =
      Σ≡Prop (λ x → isPropΣ (isPropΠ λ _ → isProp× (isSetG _ _) (isSetG _ _)) (β x))
             (sym (fst (Q e)) ∙ snd (P e'))
      where
      isSetG : isSet G
      isSetG = IsSemigroup.is-set h

      β : (e : G) → ((x : G) → (x + e ≡ x) × (e + x ≡ x))
        → isProp ((x : G) → Σ[ x' ∈ G ] (x + x' ≡ e) × (x' + x ≡ e))
      β e He =
        isPropΠ λ { x (x' , _ , P) (x'' , Q , _) →
                Σ≡Prop (λ _ → isProp× (isSetG _ _) (isSetG _ _))
                       (inv-lemma ℳ x x' x'' P Q) }
        where
        ℳ : Monoid
        ℳ = makeMonoid e _+_ isSetG (IsSemigroup.assoc h) (λ x → He x .fst) (λ x → He x .snd)

  Group→GroupΣ : Group → GroupΣ
  Group→GroupΣ (group _ _ _ -_ isGroup) =
   _ , _ , IsMonoid.isSemigroup (IsGroup.isMonoid isGroup) ,
   _ , IsMonoid.identity (IsGroup.isMonoid isGroup) ,
   λ x → (- x) , IsGroup.inverse isGroup x

  GroupΣ→Group : GroupΣ → Group
  GroupΣ→Group (_ , _ , SG , _ , H0g , w ) =
     group _ _ _ (λ x → w x .fst) (isgroup (ismonoid SG H0g) λ x → w x .snd)

  GroupIsoGroupΣ : Iso Group GroupΣ
  GroupIsoGroupΣ = iso Group→GroupΣ GroupΣ→Group (λ _ → refl) (λ _ → refl)

  groupUnivalentStr : UnivalentStr GroupStructure GroupEquivStr
  groupUnivalentStr = axiomsUnivalentStr _ isPropGroupAxioms rawGroupUnivalentStr

  GroupΣPath : (G H : GroupΣ) → (G ≃[ GroupEquivStr ] H) ≃ (G ≡ H)
  GroupΣPath = SIP groupUnivalentStr

  GroupEquivΣ : (G H : Group) → Type ℓ
  GroupEquivΣ G H = Group→GroupΣ G ≃[ GroupEquivStr ] Group→GroupΣ H

  GroupIsoΣPath : {G H : Group} → Iso (GroupEquiv G H) (GroupEquivΣ G H)
  fun GroupIsoΣPath (groupequiv e h) = (e , h)
  inv GroupIsoΣPath (e , h)        = groupequiv e h
  rightInv GroupIsoΣPath _         = refl
  leftInv GroupIsoΣPath _          = refl

  GroupPath : (G H : Group) → (GroupEquiv G H) ≃ (G ≡ H)
  GroupPath G H =
    GroupEquiv G H                    ≃⟨ isoToEquiv GroupIsoΣPath ⟩
    GroupEquivΣ G H                   ≃⟨ GroupΣPath _ _ ⟩
    Group→GroupΣ G ≡ Group→GroupΣ H ≃⟨ isoToEquiv (invIso (congIso GroupIsoGroupΣ)) ⟩
    G ≡ H ■

-- Extract the characterization of equality of groups
GroupPath : (G H : Group {ℓ}) → (GroupEquiv G H) ≃ (G ≡ H)
GroupPath = GroupΣTheory.GroupPath

uaGroup : {G H : Group {ℓ}} → GroupEquiv G H → G ≡ H
uaGroup {G = G} {H = H} = equivFun (GroupPath G H)

carac-uaGroup : {G H : Group {ℓ}} (f : GroupEquiv G H) → cong Group.Carrier (uaGroup f) ≡ ua (GroupEquiv.eq f)
carac-uaGroup (groupequiv f m) =
  (refl ∙∙ ua f ∙∙ refl)
    ≡⟨ sym (rUnit (ua f)) ⟩
  ua f ∎

-- Group-ua functoriality
open Group

Group≡ : (G H : Group {ℓ}) → (
  Σ[ p ∈ Carrier G ≡ Carrier H ]
  Σ[ q ∈ PathP (λ i → p i) (0g G) (0g H) ]
  Σ[ r ∈ PathP (λ i → p i → p i → p i) (_+_ G) (_+_ H) ]
  Σ[ s ∈ PathP (λ i → p i → p i) (-_ G) (-_ H) ]
  PathP (λ i → IsGroup (q i) (r i) (s i)) (isGroup G) (isGroup H))
  ≃ (G ≡ H)
Group≡ G H = isoToEquiv (iso
  (λ (p , q , r , s , t) i → group (p i) (q i) (r i) (s i) (t i))
  (λ p → cong Carrier p , cong 0g p , cong _+_ p , cong -_ p , cong isGroup p)
  (λ _ → refl) (λ _ → refl))

caracGroup≡ : {G H : Group {ℓ}} (p q : G ≡ H) → cong Group.Carrier p ≡ cong Group.Carrier q → p ≡ q
caracGroup≡ {G = G} {H = H} p q t = cong (fst (Group≡ G H)) (Σ≡Prop (λ t →
  isPropΣ
    (isOfHLevelPathP' 1 (is-set H) _ _) λ t₁ → isPropΣ
    (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set H) _ _) λ t₂ → isPropΣ
    (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set H) _ _) λ t₃ →
    isOfHLevelPathP 1 (isPropIsGroup _ _ _) _ _)
  t)

uaGroupId : (G : Group {ℓ}) → uaGroup (idGroupEquiv G) ≡ refl
uaGroupId G = caracGroup≡ _ _ (carac-uaGroup (idGroupEquiv G) ∙ uaIdEquiv)

uaCompGroupEquiv : {F G H : Group {ℓ}} (f : GroupEquiv F G) (g : GroupEquiv G H) → uaGroup (compGroupEquiv f g) ≡ uaGroup f ∙ uaGroup g
uaCompGroupEquiv f g = caracGroup≡ _ _ (
  cong Carrier (uaGroup (compGroupEquiv f g))
    ≡⟨ carac-uaGroup (compGroupEquiv f g) ⟩
  ua (eq (compGroupEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  ua (eq f) ∙ ua (eq g)
    ≡⟨ cong (_∙ ua (eq g)) (sym (carac-uaGroup f)) ⟩
  cong Carrier (uaGroup f) ∙ ua (eq g)
    ≡⟨ cong (cong Carrier (uaGroup f) ∙_) (sym (carac-uaGroup g)) ⟩
  cong Carrier (uaGroup f) ∙ cong Carrier (uaGroup g)
    ≡⟨ sym (cong-∙ Carrier (uaGroup f) (uaGroup g)) ⟩
  cong Carrier (uaGroup f ∙ uaGroup g) ∎) where
  open GroupEquiv

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Inference.Prenexer(x : X) where
  import OutsideIn.Constraints as C
  import OutsideIn.Expressions as E
  open E(x)
  open C(x)
  open X(x)
  private module PlusN-m n        = Monad (PlusN-is-monad {n})
          module PlusN-f n        = Functor (Monad.is-functor (PlusN-is-monad {n}))
          module Constraint-f {s} = Functor (constraint-is-functor {s})
          module QC-f             = Functor (qconstraint-is-functor)

  data _prenex:_,_ {n : Set} : Constraint n Extended → (m : ℕ) → Constraint (n ⨁ m) Flat → Set where
    PN-QC : ∀ {x} → QC x prenex: 0 , QC x
    PN-∧  : ∀ {a b}{na nb}{a′}{b′} → a prenex: na , a′ → b prenex: nb , b′
          → (a ∧′ b) prenex: (na + nb) ,
                                               (Constraint-f.map ((subst id (sym (PlusN-collect {n}{na}{nb}))) ∘ PlusN-m.unit nb) a′
                                             ∧′ Constraint-f.map ((subst id (sym (PlusN-collect {n}{na}{nb})))  ∘ PlusN-f.map nb (PlusN-m.unit na)) b′)
    PN-Imp : ∀ {q}{c}{m}{c′}
           → c prenex: m , c′
           → Imp′ q c prenex: 0 , Imp (∃ m · q ⊃ c′)
    PN-Ext  : ∀ {x}{n}{x′} → x prenex: n , x′ → (Ⅎ_ x) prenex: suc n , x′

  prenex : ∀ {n} → (C : Constraint n Extended) → ∃ (λ m → ∃ (λ C′ → C prenex: m , C′))
  prenex (QC x) = _ , _ , PN-QC
  prenex {n} (a ∧′ b) with prenex a | prenex b
  ... | na , a′ , p₁ | nb , b′ , p₂ = _ , _ , PN-∧ p₁ p₂
  prenex {n} (Imp′ q c) with prenex c
  ... | m , c′ , p = _ , _ , PN-Imp p
  prenex (Ⅎ_ x) with prenex x
  ... | n , x′ , p = _ , _ , PN-Ext  p

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
module Class.Monad.Except where

open import Class.Monad
open import Class.Monoid
open import Data.Maybe
open import Level

private
  variable
    a : Level
    A : Set a

record MonadExcept (M : Set a → Set a) {{_ : Monad M}} (E : Set a) : Set (suc a) where
  field
    throwError : E → M A
    catchError : M A → (E → M A) → M A

  appendIfError : {{_ : Monoid E}} → M A → E → M A
  appendIfError x s = catchError x λ e → throwError (e + s)

  maybeToError : Maybe A → E → M A
  maybeToError (just x) e = return x
  maybeToError nothing e = throwError e

  tryElse : M A → M A → M A
  tryElse x y = catchError x λ _ → y

open MonadExcept {{...}} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
-- Andreas, 2016-10-11, AIM XXIV, issue #2250

{-# OPTIONS --injective-type-constructors #-}

open import Common.Prelude
open import Common.Equality

abstract
  f : Bool → Bool
  f x = true

  same : f true ≡ f false
  same = refl

-- f should not be treated as injective here,
-- even though f true and f false do not reduce.

not-same : f true ≡ f false → ⊥
not-same () -- should be yellow

absurd : ⊥
absurd = not-same same

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Prelude renaming (_++_ to _++-List_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ; suc; zero; _+_; _≤_; z≤n; s≤s; _≤?_) renaming (decTotalOrder to decTotalOrder-ℕ)
open import Data.Nat.Properties as ℕ-Props
open import Data.Nat.Properties.Simple using (+-suc; +-comm)
open import Data.Fin using (Fin; toℕ; fromℕ≤) renaming (inject+ to finject; raise to fraise; zero to fzero; suc to fsuc)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; cong; sym)
open import Algebra using (module CommutativeSemiring; module DistributiveLattice)
open import Relation.Binary using (module DecTotalOrder)

open import RW.Language.RTerm
open import RW.Language.RTermUtils using (typeArity; typeResult)

-- Utility Module to handle (RTerm (Fin n)), or,
-- finite-scope terms.
--
-- Adapted from "Auto In Agda", by Pepijn Kokke and Wouter Swierstra.
--  https://github.com/pepijnkokke/AutoInAgda
--
module RW.Language.FinTerm where

  -----------------------------------------
  -- Unification/Instantiation
  --   by Structural Recursion
  --
  --  We have to bypass some problems with the termination checker;
  --  The trick is to represent variables using a finite datatype,
  --  this way we can prove that the index of the variables to be
  --  replaced decreases.
  --
  --  To work with FinTerms, as we'll call them:
  FinTerm : ℕ → Set
  FinTerm = RTerm ∘ Fin

  --  We're going to need a lot of machinery to inject and raise
  --  FinTerms in loads of different contexts.
  --
  --  The beginning of this module is reserved for that boilerplate.
  --
  --------------------------------------------
  -- Fin Boilerplate

  record Inject (T : ℕ → Set) : Set where
    constructor inj
    field
      inject : ∀ {m} n → T m → T (m + n)

    inject≤ : ∀ {m n} → m ≤ n → T m → T n
    inject≤ {m} {n} p t = P.subst T (sym (Δ-correct p)) (inject (Δ p) t)

  open Inject {{...}} using (inject; inject≤)

  record Raise (T : ℕ → Set) : Set where
    constructor rai
    field
      raise : ∀ {m} n → T m → T (n + m)

    raise≤ : ∀ {m n} → m ≤ n → T m → T n
    raise≤ {m} {n} p t = P.subst T (sym (P.trans (Δ-correct p) (+-comm m (Δ p)))) (raise (Δ p) t)

  open Raise {{...}} using (raise; raise≤)

  instance
    InjectFin : Inject Fin
    InjectFin = inj finject

    RaiseFin : Raise Fin
    RaiseFin = rai fraise

    InjectRTerm : Inject FinTerm
    InjectRTerm = inj (λ n → replace-A (ovar ∘ inject n))

    RaiseRTerm : Raise FinTerm
    RaiseRTerm = rai (λ n → replace-A (ovar ∘ raise n))

    InjectRTerms : Inject (List ∘ FinTerm)
    InjectRTerms = inj (λ n → map (inject n))

    RaiseRTerms : Raise (List ∘ FinTerm)
    RaiseRTerms = rai (λ n → map (raise n))

  open DistributiveLattice ℕ-Props.distributiveLattice
    using (_∧_; ∧-comm) public
  open DecTotalOrder decTotalOrder-ℕ
    using (total) public

  private
    supremumLemma : ∀{m n} → m ≤ n → m ∧ n ≡ n
    supremumLemma z≤n     = refl
    supremumLemma (s≤s p) = cong suc (supremumLemma p)

  -- Match indexes of injectable types.
  match : ∀{m n} {I J} ⦃ i : Inject I ⦄ ⦃ j : Inject J ⦄
        → I m → J n → I (m ∧ n) × J (m ∧ n)
  match {m} {n} i j with total m n
  ...| i1 m≤n rewrite supremumLemma m≤n = inject≤ m≤n i , j
  ...| i2 n≤m rewrite ∧-comm m n
                      | supremumLemma n≤m = i , inject≤ n≤m j

  -- Conversion of regular terms to finite terms.

  mutual
    R2FinTerm : RTerm ℕ → ∃ FinTerm
    R2FinTerm (ovar x) = suc x , ovar (fromℕ x)
    R2FinTerm (ivar n) = 0 , ivar n
    R2FinTerm (rlit l) = 0 , rlit l
    R2FinTerm (rlam t) with R2FinTerm t
    ...| (n , t') = n , rlam t'
    R2FinTerm (rapp n ts) with R2FinTerm* ts
    ...| (k , l) = k , rapp n l

    R2FinTerm* : List (RTerm ℕ) → ∃ (List ∘ FinTerm)
    R2FinTerm* [] = 0 , []
    R2FinTerm* (x ∷ xs) with R2FinTerm x | R2FinTerm* xs
    ...| kx , x' | kxs , xs' with match x' xs'
    ...| rx , rxs = kx ∧ kxs , rx ∷ rxs

  Fin2RTerm : ∀{n} → FinTerm n → RTerm ℕ
  Fin2RTerm = replace-A (ovar ∘ toℕ)

  R2FinType : RTerm ℕ → ∃ FinTerm
  R2FinType t with typeArity t
  ...| ar = ar , replace-A fix-ovars t
    where
      fix-ovars : ℕ → FinTerm ar
      fix-ovars fn with suc fn ≤? ar
      ...| yes prf = ovar (fromℕ≤ prf)
      ...| no  _   = ivar fn

  Fin2RTerm⊥ : FinTerm zero → RTerm ⊥
  Fin2RTerm⊥ = replace-A (λ ())

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
{-# OPTIONS --without-K #-}

open import M-types.Base.Core
open import M-types.Base.Sum
open import M-types.Base.Prod
open import M-types.Base.Eq
open import M-types.Base.Equi
open import M-types.Base.Axiom

module M-types.Base.Rel where
    SpanRel : Ty ℓ → Ty (ℓ-suc ℓ)
    SpanRel {ℓ} X = ∑[ ty ∈ Ty ℓ ] (ty → X) × (ty → X)

    ρ₀ : {X : Ty ℓ₀} {Y Z : X → Ty ℓ₁} →
        ∏[ s ∈ ∑[ x ∈ X ] (Y x × Z x) ] Y (pr₀ s)
    ρ₀ = pr₀ ∘ pr₁

    ρ₁ : {X : Ty ℓ₀} {Y Z : X → Ty ℓ₁} →
        ∏[ s ∈ ∑[ x ∈ X ] (Y x × Z x) ] Z (pr₀ s)
    ρ₁ = pr₁ ∘ pr₁

    SpanRel-syntax : {X : Ty ℓ} →
        ∏[ ∼ ∈ SpanRel X ] ∏[ x₀ ∈ X ] ∏[ x₁ ∈ X ] Ty ℓ
    SpanRel-syntax ∼ x₀ x₁ = ∑[ s ∈ (ty ∼) ] ((ρ₀ ∼ s ≡ x₀) × (ρ₁ ∼ s ≡ x₁))
    syntax SpanRel-syntax ∼ x₀ x₁ = x₀ ⟨ ∼ ⟩ x₁

    ≡-spanRel : {X : Ty ℓ} →
        SpanRel X
    ≡-spanRel {_} {X} = (X , id , id)

    SpanRelMor : {X : Ty ℓ} →
        SpanRel X → SpanRel X → Ty ℓ
    SpanRelMor {_} {X} ∼ ≈ =
        ∑[ fun ∈ (ty ∼ → ty ≈) ]
        (ρ₀ ≈ ∘ fun ≡ ρ₀ ∼) × (ρ₁ ≈ ∘ fun ≡ ρ₁ ∼)

    com₀ : {X : Ty ℓ₀} {Y Z : X → Ty ℓ₁} →
        ∏[ s ∈ ∑[ x ∈ X ] (Y x × Z x) ] Y (pr₀ s)
    com₀ = pr₀ ∘ pr₁

    com₁ : {X : Ty ℓ₀} {Y Z : X → Ty ℓ₁} →
        ∏[ s ∈ ∑[ x ∈ X ] (Y x × Z x) ] Z (pr₀ s)
    com₁ = pr₁ ∘ pr₁

    id-spanRel : {X : Ty ℓ} {∼ : SpanRel X} →
        SpanRelMor ∼ ∼
    id-spanRel {_} {X} {∼} = (id , refl , refl)

    infixr 9 _∘-spanRel_
    _∘-spanRel_ : {X : Ty ℓ} {∼₀ ∼₁ ∼₂ : SpanRel X} →
        SpanRelMor ∼₁ ∼₂ → SpanRelMor ∼₀ ∼₁ → SpanRelMor ∼₀ ∼₂
    g ∘-spanRel f =
        (
            fun g ∘ fun f ,
            ap (λ k → k ∘ fun f) (com₀ g) · com₀ f ,
            ap (λ k → k ∘ fun f) (com₁ g) · com₁ f
        )

    DepRel : Ty ℓ → Ty (ℓ-suc ℓ)
    DepRel {ℓ} X = X → X → Ty ℓ

    DepRel-syntax : {X : Ty ℓ} →
        ∏[ ∼ ∈ DepRel X ] ∏[ x₀ ∈ X ] ∏[ x₁ ∈ X ] Ty ℓ
    DepRel-syntax ∼ x₀ x₁ = ∼ x₀ x₁
    syntax DepRel-syntax ∼ x₀ x₁ = x₀ [ ∼ ] x₁

    ≡-depRel : {X : Ty ℓ} →
        DepRel X
    ≡-depRel = λ x₀ → λ x₁ → x₀ ≡ x₁

    DepRelMor : {X : Ty ℓ} →
        DepRel X → DepRel X → Ty ℓ
    DepRelMor {_} {X} ∼ ≈ =
        ∏[ x₀ ∈ X ] ∏[ x₁ ∈ X ]
        (x₀ [ ∼ ] x₁ → x₀ [ ≈ ] x₁)

    id-depRel : {X : Ty ℓ} {∼ : DepRel X} →
        DepRelMor ∼ ∼
    id-depRel {_} {X} {∼} = λ x₀ → λ x₁ → id

    infixr 9 _∘-depRel_
    _∘-depRel_ : {X : Ty ℓ} {∼₀ ∼₁ ∼₂ : DepRel X} →
        DepRelMor ∼₁ ∼₂ → DepRelMor ∼₀ ∼₁ → DepRelMor ∼₀ ∼₂
    g ∘-depRel f = λ x₀ → λ x₁ → g x₀ x₁ ∘ f x₀ x₁

    SpanRel→DepRel : {X : Ty ℓ} →
        SpanRel X → DepRel X
    SpanRel→DepRel {_} {X} ∼ = λ x₀ → λ x₁ → x₀ ⟨ ∼ ⟩ x₁

    DepRel→SpanRel : {X : Ty ℓ} →
        DepRel X → SpanRel X
    DepRel→SpanRel {_} {X} ∼ =
        (
            (∑[ x₀ ∈ X ] ∑[ x₁ ∈ X ] x₀ [ ∼ ] x₁) ,
            pr₀ ,
            pr₀ ∘ pr₁
        )

    SpanRel→DepRel-pres : {X : Ty ℓ} →
        ∏[ ∼ ∈ SpanRel X ] ∏[ x₀ ∈ X ] ∏[ x₁ ∈ X ]
        (x₀ [ SpanRel→DepRel ∼ ] x₁) ≡ (x₀ ⟨ ∼ ⟩ x₁)
    SpanRel→DepRel-pres ∼ x₀ x₁ = refl

    DepRel→SpanRel-pres : {X : Ty ℓ} →
        ∏[ ∼ ∈ DepRel X ] ∏[ x₀ ∈ X ] ∏[ x₁ ∈ X ]
        (x₀ ⟨ DepRel→SpanRel ∼ ⟩ x₁) ≃ (x₀ [ ∼ ] x₁)
    DepRel→SpanRel-pres ∼ x₀ x₁ =
        (
            (λ ((y₀ , y₁ , s) , p₀ , p₁) →
                tra (λ x → x [ ∼ ] x₁) p₀ (tra (λ y → y₀ [ ∼ ] y) p₁ s)
            ) ,
            Qinv→IsEqui (
                (λ s → ((x₀ , x₁ , s) , refl , refl)) ,
                (λ {((x₀ , x₁ , s) , refl , refl) → refl}) ,
                (λ s → refl)
            )
        )

    SpanRel→SpanRel-mor : {X : Ty ℓ} →
        ∏[ ∼ ∈ SpanRel X ] SpanRelMor ∼ (DepRel→SpanRel (SpanRel→DepRel ∼))
    SpanRel→SpanRel-mor ∼ =
        (
            (λ s → (ρ₀ ∼ s , ρ₁ ∼ s , (s , refl , refl))) ,
            refl ,
            refl
        )

    DepRel→DepRel-mor : {X : Ty ℓ} →
        ∏[ ∼ ∈ DepRel X ] DepRelMor ∼ (SpanRel→DepRel (DepRel→SpanRel ∼))
    DepRel→DepRel-mor ∼ = λ x₀ → λ x₁ → λ s → ((x₀ , x₁ , s) , refl , refl)

    ≡-SpanRel→DepRel-mor : {X : Ty ℓ} →
        DepRelMor {ℓ} {X} (SpanRel→DepRel ≡-spanRel) ≡-depRel
    ≡-SpanRel→DepRel-mor = λ x₀ → λ x₁ → λ(s , p₀ , p₁) → p₀ ⁻¹ · p₁

    ≡-DepRel→SpanRel-mor : {X : Ty ℓ} →
        SpanRelMor {ℓ} {X} (DepRel→SpanRel ≡-depRel) ≡-spanRel
    ≡-DepRel→SpanRel-mor =
        (
            (λ (x₀ , x₁ , p) → x₀) ,
            refl ,
            funext (λ (x₀ , x₁ , p) → p)
        )

    SpanRelMor→DepRelMor : {X : Ty ℓ} {∼ ≈ : SpanRel X} →
        SpanRelMor ∼ ≈ → DepRelMor (SpanRel→DepRel ∼) (SpanRel→DepRel ≈)
    SpanRelMor→DepRelMor (fun , refl , refl) x₀ x₁ (s , refl , refl) =
        (
            fun s ,
            refl ,
            refl
        )

    DepRelMor→SpanRelMor : {X : Ty ℓ} {∼ ≈ : DepRel X} →
        DepRelMor ∼ ≈ → SpanRelMor (DepRel→SpanRel ∼) (DepRel→SpanRel ≈)
    DepRelMor→SpanRelMor f =
        (
            (λ (x₀ , x₁ , s) → (x₀ , x₁ , f x₀ x₁ s)) ,
            refl {_} {_} {pr₀}  ,
            refl
        )

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
module Data.Tree.Base where

open import Class.Monoid
open import Class.Show
open import Data.List using (List; sum; map; replicate; intersperse)
open import Data.Nat using (ℕ; suc)
open import Data.Nat.Instance
open import Data.String using (String)
open import Data.String.Instance
open import Function

data Tree (A : Set) : Set where
  Node : A -> List (Tree A) -> Tree A

{-# TERMINATING #-}
lengthTree : ∀ {A} -> Tree A -> ℕ
lengthTree (Node x x₁) = 1 + sum (map lengthTree x₁)

-- show tree that is compatible with org mode
{-# TERMINATING #-}
showTreeOrg : ∀ {A} {{_ : Show A}} -> Tree A -> String
showTreeOrg = helper 1
  where
    helper : ∀ {A} {{_ : Show A}} -> ℕ -> Tree A -> String
    helper level (Node x x₁) =
      (concat $ replicate level "*") + " " + show x + "\n" +
      (concat $ intersperse "\n" $ map (helper (suc level)) x₁) + "\n"


text:
{-# OPTIONS --without-K --safe #-}

module Dodo.Binary where

open import Dodo.Binary.Acyclic public
open import Dodo.Binary.Composition public
open import Dodo.Binary.Cycle public
open import Dodo.Binary.Dec public
open import Dodo.Binary.Disjoint public
open import Dodo.Binary.Domain public
open import Dodo.Binary.Empty public
open import Dodo.Binary.Equality public
open import Dodo.Binary.Filter public
open import Dodo.Binary.Flip public
open import Dodo.Binary.Functional public
open import Dodo.Binary.Identity public
open import Dodo.Binary.Immediate public
open import Dodo.Binary.Intersection public
open import Dodo.Binary.Irreflexive public
open import Dodo.Binary.Maximal public
open import Dodo.Binary.Precedes public
open import Dodo.Binary.Product public
open import Dodo.Binary.SplittableOrder public
open import Dodo.Binary.Subtraction public
open import Dodo.Binary.Transitive public
open import Dodo.Binary.Trichotomous public
open import Dodo.Binary.Union public

open ⊆₂-Reasoning public
open ⇔₂-Reasoning public

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
-- Andreas, 2014-04-12, Order of declaration mattered in the presence
-- of meta variables involving sizes
-- {-# OPTIONS -v tc.meta:10 -v tc.meta.assign:10 #-}

-- Error persists without option sized-types
{-# OPTIONS --sized-types #-}
module _ where

open import Common.Size
-- different error if we do not use the built-ins (Size vs Size<)

module Works where
  mutual

    data Colist' i : Set where
      inn  : (xs : Colist i) → Colist' i

    record Colist i : Set where
      coinductive
      field out : ∀ {j : Size< i} → Colist' j

module Fails where
  mutual

    record Colist i : Set where
      coinductive
      field out : ∀ {j : Size< i} → Colist' j

    data Colist' i : Set where
      inn  : (xs : Colist i) → Colist' i

-- Error: Issue1087.agda:21,45-46
-- Cannot instantiate the metavariable _20 to solution (Size< i) since
-- it contains the variable i which is not in scope of the
-- metavariable or irrelevant in the metavariable but relevant in the
-- solution
-- when checking that the expression j has type _20

-- Works now.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Luau.OpSem where

open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (just)
open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup; function_⟨_⟩_end)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
open import Luau.Value using (addr; val)

data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set

data _⊢_⟶ᴱ_⊣_  where

  nil : ∀ {H} →

    -------------------
    H ⊢ nil ⟶ᴱ nil ⊣ H

  function : ∀ {H H′ a x B} →

    H′ ≡ H ⊕ a ↦ (function "anon" ⟨ x ⟩ B end) →
    -------------------------------------------
    H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′

  app : ∀ {H H′ M M′ N} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    -----------------------------
    H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′

  beta : ∀ {H M a f x B} →

    (lookup H a) ≡ just(function f ⟨ x ⟩ B end) →
    -----------------------------------------------------
    H ⊢ (addr a $ M) ⟶ᴱ (block f is local x ← M ∙ B end) ⊣ H

  block : ∀ {H H′ B B′ b} →

    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
    ----------------------------------------------------
    H ⊢ (block b is B end) ⟶ᴱ (block b is B′ end) ⊣ H′

  return : ∀ {H V B b} →

    --------------------------------------------------------
    H ⊢ (block b is return (val V) ∙ B end) ⟶ᴱ (val V) ⊣ H

  done : ∀ {H b} →

    ---------------------------------
    H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H

data _⊢_⟶ᴮ_⊣_  where

  local : ∀ {H H′ x M M′ B} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    -------------------------------------------------
    H ⊢ (local x ← M ∙ B) ⟶ᴮ (local x ← M′ ∙ B) ⊣ H′

  subst : ∀ {H x v B} →

    -------------------------------------------------
    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H

  function : ∀ {H H′ a f x B C} →

    H′ ≡ H ⊕ a ↦ (function f ⟨ x ⟩ C end) →
    --------------------------------------------------------------
    H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′

  return : ∀ {H H′ M M′ B} →

    H ⊢ M ⟶ᴱ M′ ⊣ H′ →
    --------------------------------------------
    H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′

data _⊢_⟶*_⊣_ : Heap → Block → Block → Heap → Set where

  refl : ∀ {H B} →

    ----------------
    H ⊢ B ⟶* B ⊣ H

  step : ∀ {H H′ H″ B B′ B″} →
    H ⊢ B ⟶ᴮ B′ ⊣ H′ →
    H′ ⊢ B′ ⟶* B″ ⊣ H″ →
    ------------------
    H ⊢ B ⟶* B″ ⊣ H″

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Orders.Total.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.EuclideanDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open import Rings.Divisible.Definition R
open Setoid S
open Equivalence eq
open Ring R
open Group additiveGroup

record DivisionAlgorithmResult (norm : {a : A} → ((a ∼ 0R) → False) → ℕ) {x y : A} (x!=0 : (x ∼ 0R) → False) (y!=0 : (y ∼ 0R) → False) : Set (a ⊔ b) where
  field
    quotient : A
    rem : A
    remSmall : (rem ∼ 0R) || Sg ((rem ∼ 0R) → False) (λ rem!=0 → (norm rem!=0) <N (norm y!=0))
    divAlg : x ∼ ((quotient * y) + rem)

record DivisionAlgorithmResult' (norm : (a : A) → ℕ) (x y : A) : Set (a ⊔ b) where
  field
    quotient : A
    rem : A
    remSmall : (rem ∼ 0R) || ((norm rem) <N (norm y))
    divAlg : x ∼ ((quotient * y) + rem)

record EuclideanDomain : Set (a ⊔ lsuc b) where
  field
    isIntegralDomain : IntegralDomain R
    norm : {a : A} → ((a ∼ 0R) → False) → ℕ
    normSize : {a b : A} → (a!=0 : (a ∼ 0R) → False) → (b!=0 : (b ∼ 0R) → False) → (c : A) → b ∼ (a * c) → (norm a!=0) ≤N (norm b!=0)
    divisionAlg : {a b : A} → (a!=0 : (a ∼ 0R) → False) → (b!=0 : (b ∼ 0R) → False) → DivisionAlgorithmResult norm a!=0 b!=0
  normWellDefined : {a : A} → (p1 p2 : (a ∼ 0R) → False) → norm p1 ≡ norm p2
  normWellDefined {a} p1 p2 with normSize p1 p2 1R (symmetric (transitive *Commutative identIsIdent))
  normWellDefined {a} p1 p2 | inl n1<n2 with normSize p2 p1 1R (symmetric (transitive *Commutative identIsIdent))
  normWellDefined {a} p1 p2 | inl n1<n2 | inl n2<n1 = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder n1<n2 n2<n1))
  normWellDefined {a} p1 p2 | inl n1<n2 | inr n2=n1 = equalityCommutative n2=n1
  normWellDefined {a} p1 p2 | inr n1=n2 = n1=n2
  normWellDefined' : {a b : A} → (a ∼ b) → (a!=0 : (a ∼ 0R) → False) → (b!=0 : (b ∼ 0R) → False) → norm a!=0 ≡ norm b!=0
  normWellDefined' a=b a!=0 b!=0 with normSize a!=0 b!=0 1R (symmetric (transitive *Commutative (transitive identIsIdent a=b)))
  normWellDefined' a=b a!=0 b!=0 | inl a<b with normSize b!=0 a!=0 1R (symmetric (transitive *Commutative (transitive identIsIdent (symmetric a=b))))
  normWellDefined' a=b a!=0 b!=0 | inl a<b | inl b<a = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder a<b b<a))
  normWellDefined' a=b a!=0 b!=0 | inl a<b | inr n= = equalityCommutative n=
  normWellDefined' a=b a!=0 b!=0 | inr n= = n=

record EuclideanDomain' : Set (a ⊔ lsuc b) where
  field
    isIntegralDomain : IntegralDomain R
    norm : A → ℕ
    normWellDefined : {a b : A} → (a ∼ b) → norm a ≡ norm b
    normSize : (a b : A) → (a ∣ b) → ((b ∼ 0R) → False) → norm a ≤N (norm b)
    divisionAlg : (a b : A) → ((b ∼ 0R) → False) → DivisionAlgorithmResult' norm a b

normEquiv : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) → A → ℕ
normEquiv e decidableZero a with decidableZero a
... | inl a=0 = 0
... | inr a!=0 = EuclideanDomain.norm e a!=0

normSizeEquiv : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) (a b : A) → (a ∣ b) → ((b ∼ 0R) → False) → normEquiv e decidableZero a ≤N normEquiv e decidableZero b
normSizeEquiv e decidableZero a b (c , ac=b) b!=0 = ans
  where
    abstract
      a!=0 : (a ∼ 0R) → False
      a!=0 a=0 = b!=0 (transitive (symmetric ac=b) (transitive (*WellDefined a=0 reflexive) (transitive *Commutative timesZero)))
    normIs : normEquiv e decidableZero a ≡ EuclideanDomain.norm e a!=0
    normIs with decidableZero a
    normIs | inl a=0 = exFalso (a!=0 a=0)
    normIs | inr a!=0' = EuclideanDomain.normWellDefined e a!=0' a!=0
    normIs' : normEquiv e decidableZero b ≡ EuclideanDomain.norm e b!=0
    normIs' with decidableZero b
    normIs' | inl b=0 = exFalso (b!=0 b=0)
    normIs' | inr b!=0' = EuclideanDomain.normWellDefined e b!=0' b!=0
    ans : (normEquiv e decidableZero a) ≤N (normEquiv e decidableZero b)
    ans with EuclideanDomain.normSize e a!=0 b!=0 c (symmetric ac=b)
    ans | inl n<Nn = inl (identityOfIndiscernablesLeft _<N_ (identityOfIndiscernablesRight _<N_ n<Nn (equalityCommutative normIs')) (equalityCommutative normIs))
    ans | inr n=n = inr (transitivity normIs (transitivity n=n (equalityCommutative normIs')))

divisionAlgEquiv : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) → (a b : A) → ((b ∼ 0R) → False) → DivisionAlgorithmResult' (normEquiv e decidableZero) a b
divisionAlgEquiv e decidableZero a b b!=0 with decidableZero a
divisionAlgEquiv e decidableZero a b b!=0 | inl a=0 = record { quotient = 0R ; rem = 0R ; remSmall = inl reflexive ; divAlg = transitive a=0 (transitive (symmetric identLeft) (+WellDefined (symmetric (transitive *Commutative timesZero)) reflexive)) }
divisionAlgEquiv e decidableZero a b b!=0 | inr a!=0 with EuclideanDomain.divisionAlg e a!=0 b!=0
divisionAlgEquiv e decidableZero a b b!=0 | inr a!=0 | record { quotient = quotient ; rem = rem ; remSmall = inl x ; divAlg = divAlg } = record { quotient = quotient ; rem = rem ; remSmall = inl x ; divAlg = divAlg }
divisionAlgEquiv e decidableZero a b b!=0 | inr a!=0 | record { quotient = quotient ; rem = rem ; remSmall = inr (rem!=0 , pr) ; divAlg = divAlg } = record { quotient = quotient ; rem = rem ; remSmall = inr (identityOfIndiscernablesLeft _<N_ (identityOfIndiscernablesRight _<N_ pr (equalityCommutative normIs')) (equalityCommutative normIs)) ; divAlg = divAlg }
  where
    normIs : normEquiv e decidableZero rem ≡ EuclideanDomain.norm e rem!=0
    normIs with decidableZero rem
    normIs | inl rem=0 = exFalso (rem!=0 rem=0)
    normIs | inr rem!=0' = EuclideanDomain.normWellDefined e rem!=0' rem!=0
    normIs' : normEquiv e decidableZero b ≡ EuclideanDomain.norm e b!=0
    normIs' with decidableZero b
    normIs' | inl b=0 = exFalso (b!=0 b=0)
    normIs' | inr b!=0' = EuclideanDomain.normWellDefined e b!=0' b!=0

normWellDefined : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) {a b : A} (a=b : a ∼ b) → normEquiv e decidableZero a ≡ normEquiv e decidableZero b
normWellDefined e decidableZero {a} {b} a=b with decidableZero a
normWellDefined e decidableZero {a} {b} a=b | inl a=0 with decidableZero b
normWellDefined e decidableZero {a} {b} a=b | inl a=0 | inl b=0 = refl
normWellDefined e decidableZero {a} {b} a=b | inl a=0 | inr b!=0 = exFalso (b!=0 (transitive (symmetric a=b) a=0))
normWellDefined e decidableZero {a} {b} a=b | inr a!=0 with decidableZero b
normWellDefined e decidableZero {a} {b} a=b | inr a!=0 | inl b=0 = exFalso (a!=0 (transitive a=b b=0))
normWellDefined e decidableZero {a} {b} a=b | inr a!=0 | inr b!=0 = EuclideanDomain.normWellDefined' e a=b a!=0 b!=0

eucDomsEquiv : (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) → EuclideanDomain → EuclideanDomain'
eucDomsEquiv decidableZero e = record { isIntegralDomain = EuclideanDomain.isIntegralDomain e ; norm = normEquiv e decidableZero ; normSize = normSizeEquiv e decidableZero ; divisionAlg = divisionAlgEquiv e decidableZero ; normWellDefined = normWellDefined e decidableZero }


text:
module Logic.Classical.Propositional where

open import Boolean
open import Data
open import Functional
import      Lvl

-- Propositional logic. Working with propositions and their truth (whether they are true or false).

module ProofSystems {ℓ₁} {ℓ₂} {Proposition : Set(ℓ₁)} {Formula : Set(ℓ₁) → Set(ℓ₂)} (symbols : Syntax.Symbols Proposition Formula) where
  open Syntax.Symbols(symbols)

  module TruthTables where

  -- The "proofs" that results by these postulates are very much alike the classical notation of natural deduction proofs in written as trees.
  -- A function that has the type (Node(A) → Node(B)) is a proof of (A ⊢ B) (A is the assumption, B is the single conclusion)
  -- A function that has the type (Node(A₁) → Node(A₂) → Node(A₃) →  .. → Node(B)) is a proof of ({A₁,A₂,A₃,..} ⊢ B) (Aᵢ is the assumptions, B is the single result)
  -- A function's function body is the "tree proof"
  -- • The inner most (deepest) expression is at the top of a normal tree
  -- • The outer most (shallow) expression is at the bottom of a normal tree that should result in a construction of the conclusion
  -- One difference is that one cannot introduce assumptions however one wants. There are however rules that allows one to to this by using a function, and can be written as a lambda abstraction if one want it to look similar to the tree proofs.
  module NaturalDeduction where
    -- Intro rules are like constructors of formulas
    -- Elimination rules are like deconstructors of formulas
    record Rules : Set(Lvl.𝐒(ℓ₁ Lvl.⊔ ℓ₂)) where
      field
        {Node} : Formula(Proposition) → Set(ℓ₁ Lvl.⊔ ℓ₂)

      field
        [⊤]-intro : Node(⊤)

        [⊥]-intro : ∀{φ : Formula(Proposition)} → Node(φ) → Node(¬ φ) → Node(⊥)

        [¬]-intro : ∀{φ : Formula(Proposition)} → (Node(φ) → Node(⊥)) → Node(¬ φ)
        [¬]-elim  : ∀{φ : Formula(Proposition)} → (Node(¬ φ) → Node(⊥)) → Node(φ)

        [∧]-intro : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁) → Node(φ₂) → Node(φ₁ ∧ φ₂)
        [∧]-elimₗ  : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁ ∧ φ₂) → Node(φ₁)
        [∧]-elimᵣ  : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁ ∧ φ₂) → Node(φ₂)

        [∨]-introₗ : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁) → Node(φ₁ ∨ φ₂)
        [∨]-introᵣ : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₂) → Node(φ₁ ∨ φ₂)
        [∨]-elim  : ∀{φ₁ φ₂ φ₃ : Formula(Proposition)} → (Node(φ₁) → Node(φ₃)) → (Node(φ₂) → Node(φ₃)) → Node(φ₁ ∨ φ₂) → Node(φ₃)

        [⇒]-intro : ∀{φ₁ φ₂ : Formula(Proposition)} → (Node(φ₁) → Node(φ₂)) → Node(φ₁ ⇒ φ₂)
        [⇒]-elim  : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁ ⇒ φ₂) → Node(φ₁) → Node(φ₂)

        [⇐]-intro : ∀{φ₁ φ₂ : Formula(Proposition)} → (Node(φ₂) → Node(φ₁)) → Node(φ₁ ⇐ φ₂)
        [⇐]-elim : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁ ⇐ φ₂) → Node(φ₂) → Node(φ₁)

        [⇔]-intro : ∀{φ₁ φ₂ : Formula(Proposition)} → (Node(φ₂) → Node(φ₁)) → (Node(φ₁) → Node(φ₂)) → Node(φ₁ ⇔ φ₂)
        [⇔]-elimₗ : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁ ⇔ φ₂) → Node(φ₂) → Node(φ₁)
        [⇔]-elimᵣ : ∀{φ₁ φ₂ : Formula(Proposition)} → Node(φ₁ ⇔ φ₂) → Node(φ₁) → Node(φ₂)

      -- Double negated proposition is positive
      [¬¬]-elim : ∀{φ : Formula(Proposition)} → Node(¬ (¬ φ)) → Node(φ)
      [¬¬]-elim nna = [¬]-elim(na ↦ [⊥]-intro na nna)

      [⊥]-elim : ∀{φ : Formula(Proposition)} → Node(⊥) → Node(φ)
      [⊥]-elim bottom = [¬]-elim(_ ↦ bottom)

    module Meta(rules : Rules) (meta-symbols : Syntax.Symbols (Set(ℓ₁ Lvl.⊔ ℓ₂)) id) where
      open import Data.List
      open        Rules(rules)
      open        Syntax.Symbols(meta-symbols)
        renaming (
          •_ to ◦_ ;
          ⊤   to ⊤ₘ ;
          ⊥   to ⊥ₘ ;
          ¬_  to ¬ₘ_ ;
          _∧_ to _∧ₘ_ ;
          _∨_ to _∨ₘ_ ;
          _⇒_ to _⇒ₘ_ )

      module Theorems where
        open import Data.List.Proofs{ℓ₁}{ℓ₂}
        import      List.Theorems
        open        Data.List.Relation.Membership
        open        Data.List.Relation.Membership.Relators
        open import Relator.Equals{ℓ₁}{ℓ₂}
open import Relator.Equals.Proofs{ℓ₁}{ℓ₂}

        -- [⊢]-subset : (Γ₁ ⊆ Γ₂) → (Γ₁ ⊢ φ) → (Γ₂ ⊢ φ)
        -- [⊢]-subset proof =
        -- [⊢]-subset : ∀{T}{L₁ L₂ : List(Stmt)} → (L₁ ⊆ L₂) → ∀{X} → (f(L₁) → X) → (f(L₂) → X)

        [⊢]-id : ∀{φ} → ([ φ ] ⊢ φ)
        [⊢]-id = id

        -- [⊢]-lhs-commutativity : ∀{Γ₁ Γ₂}{φ} → ((Γ₁ ++ Γ₂) ⊢ φ) → ((Γ₂ ++ Γ₁) ⊢ φ)
        -- [⊢]-lhs-commutativity = id

        -- [⊢]-test : ∀{φ₁ φ₂ φ₃} → ([ φ₁ ⊰ φ₂ ⊰ φ₃ ] ⊢ φ₁) → (Node(φ₁) ⨯ (Node(φ₂) ⨯ Node(φ₃)) → Node(φ₁))
        -- [⊢]-test = id

        [⊢]-weakening : ∀{Γ}{φ₁} → (Γ ⊢ φ₁) → ∀{φ₂} → ((φ₂ ⊰ Γ) ⊢ φ₁)
        [⊢]-weakening {∅}     (⊢φ₁) (φ₂)      = (⊢φ₁)
        [⊢]-weakening {_ ⊰ _} (Γ⊢φ₁) (φ₂ , Γ) = (Γ⊢φ₁) (Γ)

        -- [⊢]-weakening₂ : ∀{Γ₁}{φ₁} → (Γ₁ ⊢ φ₁) → ∀{Γ₂} → ((Γ₁ ++ Γ₂) ⊢ φ₁)
        -- [⊢]-weakening₂ {Γ₁}{φ₁} (Γ⊢φ₁)  {∅}       = [≡]-elimᵣ {_}{_}{_} [++]-identityₗ {expr ↦ (expr ⊢ φ₁)} Γ⊢φ₁
        -- [⊢]-weakening₂ {Γ₁}{φ₁} (Γ₁⊢φ₁) {φ₂ ⊰ Γ₂} = [⊢]-weakening₂ {Γ₁}{φ₁} ([⊢]-weakening{Γ₁}{φ₁} (Γ₁⊢φ₁) {φ₂}) {Γ₂}

        [⊢]-compose : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₁) → ([ φ₁ ] ⊢ φ₂) → (Γ ⊢ φ₂)
        [⊢]-compose {∅}     (φ₁)   (φ₁⊢φ₂)      = (φ₁⊢φ₂) (φ₁)
        [⊢]-compose {_ ⊰ _} (Γ⊢φ₁) (φ₁⊢φ₂) (Γ) = (φ₁⊢φ₂) ((Γ⊢φ₁) (Γ))

        [⊢]-compose₂ : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₁) → ((φ₁ ⊰ Γ) ⊢ φ₂) → (Γ ⊢ φ₂)
        [⊢]-compose₂ {∅}     (φ₁)   (φ₁⊢φ₂)      = (φ₁⊢φ₂)(φ₁)
        [⊢]-compose₂ {_ ⊰ _} (Γ⊢φ₁) (φ₁Γ⊢φ₂) (Γ) = (φ₁Γ⊢φ₂) ((Γ⊢φ₁) (Γ) , (Γ))
        -- [⊢]-test : ∀{φ₁ φ₂ γ₁ γ₂} → ([ γ₁ ⊰ γ₂ ] ⊢ φ₁) → ([ φ₁ ⊰ γ₁ ⊰ γ₂ ] ⊢ φ₂) → ([ γ₁ ⊰ γ₂ ] ⊢ φ₂)
        -- [⊢]-test (Γ⊢φ₁) (φ₁Γ⊢φ₂) (Γ) = (φ₁Γ⊢φ₂) ((Γ⊢φ₁) (Γ) , (Γ))

        -- [⊢]-compose₃ : ∀{Γ₁ Γ₂}{φ₁ φ₂} → (Γ₁ ⊢ φ₁) → ((φ₁ ⊰ Γ₂) ⊢ φ₂) → ((Γ₁ ++ Γ₂) ⊢ φ₂)
        -- [⊢]-compose₃ {∅}    {∅} (φ₁) (φ₁⊢φ₂) = (φ₁⊢φ₂) (φ₁)
        -- [⊢]-compose₃ {_ ⊰ _}{∅} = [⊢]-compose
        -- [⊢]-compose₃ {∅}{∅} (φ₁)   (φ₁⊢φ₂)      = (φ₁⊢φ₂) (φ₁)
        -- [⊢]-compose₃ {Γ}{∅} = [≡]-elimᵣ [++]-identityₗ [⊢]-compose{Γ}
        -- [⊢]-compose₃ {∅}{Γ}  = [⊢]-compose₂{Γ}
        -- [⊢]-compose₃ {_ ⊰ _}{_ ⊰ _}  = [⊢]-compose₂

        -- olt-9-17 : ∀{Γ}{φ} → (Γ ⊢ φ) → ((φ ⊰ Γ) ⊢ ⊥) → (inconsistent Γ)
        -- olt-9-17 Γ⊢φ Γφ⊢⊥ = (Γ ↦ [⊥]-intro (Γ⊢φ Γ) ([⊥]-elim(Γφ⊢⊥ Γ)))

    module Theorems(rules : Rules) where
      open Rules(rules)

      -- Ensures that a certain proof is a certain proposition
      -- (Like type ascription, ensures that a certain expression has a certain type)
      -- Example:
      --   (A :with: a) where a : Node(A)
      --   ((A ∧ B) :with: [∧]-intro a b) where a : Node(A), b : Node(B)
      _:with:_ : ∀(φ : Formula(Proposition)) → Node(φ) → Node(φ)
      _:with:_ _ x = x
      infixl 100 _:with:_

      -- The ability to derive anything from a contradiction
      ex-falso-quodlibet : ∀{A : Formula(Proposition)} → Node(⊥) → Node(A)
      ex-falso-quodlibet = [⊥]-elim

      [∧]-symmetry : ∀{A B : Formula(Proposition)} → Node(A ∧ B) → Node(B ∧ A)
      [∧]-symmetry {A} {B} A∧B =
        ((B ∧ A) :with: [∧]-intro
          (B :with: [∧]-elimᵣ(A∧B))
          (A :with: [∧]-elimₗ(A∧B))
        )

      [∨]-symmetry : ∀{A B : Formula(Proposition)} → Node(A ∨ B) → Node(B ∨ A)
      [∨]-symmetry {A} {B} A∨B =
        ((B ∨ A) :with: [∨]-elim
          [∨]-introᵣ
          [∨]-introₗ
          A∨B
        )

      contrapositive : ∀{A B : Formula(Proposition)} → Node(A ⇒ B) → Node((¬ B) ⇒ (¬ A))
      contrapositive {A} {B} A→B =
        ((¬ B) ⇒ (¬ A)) :with: [⇒]-intro(nb ↦
          (¬ A) :with: [¬]-intro(a ↦
            ⊥ :with: [⊥]-intro
              (B     :with: [⇒]-elim (A→B) a)
              ((¬ B) :with: nb)
          )
        )

      [⇒]-syllogism : ∀{A B C : Formula(Proposition)} → Node(A ⇒ B) → Node(B ⇒ C) → Node(A ⇒ C)
      [⇒]-syllogism {A} {B} {C} A→B B→C =
        ([⇒]-intro(a ↦
          ([⇒]-elim
            B→C
            ([⇒]-elim A→B a)
          )
        ))

      [∨]-syllogism : ∀{A B : Formula(Proposition)} → Node(A ∨ B) → Node((¬ A) ⇒ B)
      [∨]-syllogism {A} {B} A∨B =
        ([∨]-elim
          (a ↦ ((¬ A) ⇒ B) :with: [⇒]-syllogism
            (((¬ A) ⇒ (¬ (¬ B))) :with: contrapositive
              (((¬ B) ⇒ A) :with: [⇒]-intro(_ ↦ a))
            )
            (((¬ (¬ B)) ⇒ B) :with: [⇒]-intro [¬¬]-elim)
          )
          (b ↦ ((¬ A) ⇒ B) :with: [⇒]-intro(_ ↦ b))
          A∨B
        )

      -- Currying
      [∧]→[⇒]-in-assumption : {X Y Z : Formula(Proposition)} → Node((X ∧ Y) ⇒ Z) → Node(X ⇒ (Y ⇒ Z))
      [∧]→[⇒]-in-assumption x∧y→z =
        ([⇒]-intro(x ↦
          ([⇒]-intro(y ↦
            ([⇒]-elim
              (x∧y→z)
              ([∧]-intro x y)
            )
          ))
        ))

      -- Uncurrying
      [∧]←[⇒]-in-assumption : {X Y Z : Formula(Proposition)} → Node(X ⇒ (Y ⇒ Z)) → Node((X ∧ Y) ⇒ Z)
      [∧]←[⇒]-in-assumption x→y→z =
        ([⇒]-intro(x∧y ↦
          ([⇒]-elim
            ([⇒]-elim
              (x→y→z)
              ([∧]-elimₗ x∧y)
            )
            ([∧]-elimᵣ x∧y)
          )
        ))

      -- It is either that a proposition is true or its negation is true.
      -- A proposition is either true or false.
      -- There is no other truth values than true and false.
      excluded-middle : ∀{A : Formula(Proposition)} → Node(A ∨ (¬ A))
      excluded-middle {A} =
        ([¬]-elim(¬[a∨¬a] ↦
          (⊥ :with: [⊥]-intro
            ((A ∨ (¬ A)) :with: [∨]-introᵣ
              ((¬ A) :with: [¬]-intro(a ↦
                (⊥ :with: [⊥]-intro
                  ((A ∨ (¬ A))    :with: [∨]-introₗ(a))
                  ((¬(A ∨ (¬ A))) :with: ¬[a∨¬a])
                )
              ))
            )
            (¬[a∨¬a])
          )
        ))

      -- It cannot be that a proposition is true and its negation is true at the same time.
      -- A proposition cannot be true and false at the same time.
      non-contradiction : ∀{A : Formula(Proposition)} → Node(¬ (A ∧ (¬ A)))
      non-contradiction {A} =
        ([¬]-intro(a∧¬a ↦
          (⊥ :with: [⊥]-intro
            (A     :with: [∧]-elimₗ a∧¬a)
            ((¬ A) :with: [∧]-elimᵣ a∧¬a)
          )
        ))

      -- TODO: Mix of excluded middle and non-contradiction: (A ⊕ (¬ A))

      -- The standard proof technic: Assume the opposite of the conclusion and prove that it leads to a contradiction
      proof-by-contradiction : ∀{A B : Formula(Proposition)} → (Node(¬ A) → Node(B)) → (Node(¬ A) → Node(¬ B)) → Node(A)
      proof-by-contradiction {A} {B} ¬a→b ¬a→¬b =
        (A :with: [¬]-elim(¬a ↦
          (⊥ :with: [⊥]-intro
            (B     :with: ¬a→b(¬a))
            ((¬ B) :with: ¬a→¬b(¬a))
          )
        ))

      peirce : ∀{A B : Formula(Proposition)} → Node((A ⇒ B) ⇒ A) → Node(A)
      peirce {A} {B} [A→B]→A =
        (A :with: [¬]-elim(¬a ↦
          ([⊥]-intro
            (A :with: [⇒]-elim
              [A→B]→A
              ((A ⇒ B) :with: [⇒]-intro(a ↦
                (B :with: [⊥]-elim
                  ([⊥]-intro
                    a
                    ¬a
                  )
                )
              ))
            )
            ((¬ A) :with: ¬a)
          )
        ))

      skip-[⇒]-assumption : ∀{A B : Formula(Proposition)} → (Node(A ⇒ B) → Node(A)) → Node(A)
      skip-[⇒]-assumption A⇒B→A =
        (peirce
          ([⇒]-intro
            (A⇒B→A)
          )
        )

{-
data □ : Formula(Proposition) → Set where
  Initial   : ∀{φ} → □(φ)
  [∧]-intro : ∀{φ₁ φ₂} → □(φ₁) → □(φ₂) → □(φ₁ ∧ φ₂)
  [∧]-elimₗ  : ∀{φ₁ φ₂} → □(φ₁ ∧ φ₂) → □(φ₁)
  [∧]-elimᵣ  : ∀{φ₁ φ₂} → □(φ₁ ∧ φ₂) → □(φ₂)
  [∨]-introₗ : ∀{φ₁ φ₂} → □(φ₁) → □(φ₁ ∨ φ₂)
  [∨]-introᵣ : ∀{φ₁ φ₂} → □(φ₁) → □(φ₁ ∨ φ₂)
  [∨]-elim  : ∀{φ₁ φ₂ φ₃} → (□(φ₁) → □(φ₃)) → (□(φ₂) → □(φ₃)) → □(φ₃)
  [⇒]-intro : ∀{φ₁ φ₂} → (□(φ₁) → □(φ₂)) → □(φ₁ ⇒ φ₂)
  [⇒]-elim  : ∀{φ₁ φ₂} → □(φ₁ ⇒ φ₂) → □(φ₁) → □(φ₂)
  [¬]-intro : ∀{φ} → (□(φ) → □(⊥)) → □(¬ φ)
  [¬]-elim  : ∀{φ} → (□(¬ φ) → □(⊥)) → □(φ)

data □ : Formula(Proposition) → Set where
  Initial   : ∀{φ} → □(φ)
  [∧]-intro : ∀{φ₁ φ₂} → □(φ₁) → □(φ₂) → □(φ₁ ∧ φ₂)
  [∧]-elimₗ  : ∀{φ₁ φ₂} → □(φ₁ ∧ φ₂) → □(φ₁)
  [∧]-elimᵣ  : ∀{φ₁ φ₂} → □(φ₁ ∧ φ₂) → □(φ₂)
  [∨]-introₗ : ∀{φ₁ φ₂} → □(φ₁) → □(φ₁ ∨ φ₂)
  [∨]-introᵣ : ∀{φ₁ φ₂} → □(φ₁) → □(φ₁ ∨ φ₂)
  [∨]-elim  : ∀{φ₁ φ₂ φ₃} → (□(φ₁) → □(φ₃)) → (□(φ₂) → □(φ₃)) → □(φ₃)
  [⇒]-intro : ∀{φ₁ φ₂} → (□(φ₁) → □(φ₂)) → □(φ₁ ⇒ φ₂)
  [⇒]-elim  : ∀{φ₁ φ₂} → □(φ₁ ⇒ φ₂) → □(φ₁) → □(φ₂)
  [¬]-intro : ∀{φ} → (□(φ) → □(⊥)) → □(¬ φ)
  [¬¬]-elim  : ∀{φ} → □(¬(¬ φ)) → □(φ)
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coprimality
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

-- Disabled to prevent warnings from deprecated names
{-# OPTIONS --warn=noUserWarning #-}

module Data.Nat.Coprimality where

open import Data.Empty
open import Data.Fin.Base using (toℕ; fromℕ<)
open import Data.Fin.Properties using (toℕ-fromℕ<)
open import Data.Nat.Base
open import Data.Nat.Divisibility
open import Data.Nat.GCD
open import Data.Nat.GCD.Lemmas
open import Data.Nat.Primality
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Data.Product as Prod
open import Function
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; cong; subst; module ≡-Reasoning)
open import Relation.Nullary
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary

open ≤-Reasoning

------------------------------------------------------------------------
-- Definition
--
-- Coprime m n is inhabited iff m and n are coprime (relatively
-- prime), i.e. if their only common divisor is 1.

Coprime : Rel ℕ 0ℓ
Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1

------------------------------------------------------------------------
-- Relationship between GCD and coprimality

coprime⇒GCD≡1 : ∀ {m n} → Coprime m n → GCD m n 1
coprime⇒GCD≡1 {m} {n} c = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ c)

GCD≡1⇒coprime : ∀ {m n} → GCD m n 1 → Coprime m n
GCD≡1⇒coprime g cd with GCD.greatest g cd
... | divides q eq = m*n≡1⇒n≡1 q _ (P.sym eq)

coprime⇒gcd≡1 : ∀ {m n} → Coprime m n → gcd m n ≡ 1
coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime)

gcd≡1⇒coprime : ∀ {m n} → gcd m n ≡ 1 → Coprime m n
gcd≡1⇒coprime gcd≡1 = GCD≡1⇒coprime (subst (GCD _ _) gcd≡1 (gcd-GCD _ _))

coprime-/gcd : ∀ m n {gcd≢0} →
               Coprime ((m / gcd m n) {gcd≢0}) ((n / gcd m n) {gcd≢0})
coprime-/gcd m n {gcd≢0} = GCD≡1⇒coprime (GCD-/gcd m n {gcd≢0})

------------------------------------------------------------------------
-- Relational properties of Coprime

sym : Symmetric Coprime
sym c = c ∘ swap

private
  0≢1 : 0 ≢ 1
  0≢1 ()

  2+≢1 : ∀ {n} → suc (suc n) ≢ 1
  2+≢1 ()

coprime? : Decidable Coprime
coprime? i j with mkGCD i j
... | (0           , g) = no  (0≢1  ∘ GCD.unique g ∘ coprime⇒GCD≡1)
... | (1           , g) = yes (GCD≡1⇒coprime g)
... | (suc (suc d) , g) = no  (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1)

------------------------------------------------------------------------
-- Other basic properties

-- Everything is coprime to 1.

1-coprimeTo : ∀ m → Coprime 1 m
1-coprimeTo m = ∣1⇒≡1 ∘ proj₁

-- Nothing except for 1 is coprime to 0.

0-coprimeTo-m⇒m≡1 : ∀ {m} → Coprime 0 m → m ≡ 1
0-coprimeTo-m⇒m≡1 {m} c = c (m ∣0 , ∣-refl)

-- If m and n are coprime, then n + m and n are also coprime.

coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n
coprime-+ c (d₁ , d₂) = c (∣m+n∣m⇒∣n d₁ d₂ , d₂)

------------------------------------------------------------------------
-- Relationship with Bezout's lemma

-- If the "gcd" in Bézout's identity is non-zero, then the "other"
-- divisors are coprime.

Bézout-coprime : ∀ {i j d} →
                 Bézout.Identity (suc d) (i * suc d) (j * suc d) →
                 Coprime i j
Bézout-coprime (Bézout.+- x y eq) (divides q₁ refl , divides q₂ refl) =
  lem₁₀ y q₂ x q₁ eq
Bézout-coprime (Bézout.-+ x y eq) (divides q₁ refl , divides q₂ refl) =
  lem₁₀ x q₁ y q₂ eq

-- Coprime numbers satisfy Bézout's identity.

coprime-Bézout : ∀ {i j} → Coprime i j → Bézout.Identity 1 i j
coprime-Bézout = Bézout.identity ∘ coprime⇒GCD≡1

-- If i divides jk and is coprime to j, then it divides k.

coprime-divisor : ∀ {k i j} → Coprime i j → i ∣ j * k → i ∣ k
coprime-divisor {k} c (divides q eq′) with coprime-Bézout c
... | Bézout.+- x y eq = divides (x * k ∸ y * q) (lem₈ x y eq eq′)
... | Bézout.-+ x y eq = divides (y * q ∸ x * k) (lem₉ x y eq eq′)

-- If d is a common divisor of mk and nk, and m and n are coprime,
-- then d divides k.

coprime-factors : ∀ {d m n k} →
                  Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k
coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout c
... | Bézout.+- x y eq = divides (x * q₁ ∸ y * q₂) (lem₁₁ x y eq eq₁ eq₂)
... | Bézout.-+ x y eq = divides (y * q₂ ∸ x * q₁) (lem₁₁ y x eq eq₂ eq₁)

------------------------------------------------------------------------
-- Primality implies coprimality.

prime⇒coprime : ∀ m → Prime m →
                ∀ n → 0 < n → n < m → Coprime m n
prime⇒coprime (suc (suc m)) _  _ _  _ {1} _                       = refl
prime⇒coprime (suc (suc m)) p  _ _  _ {0} (divides q 2+m≡q*0 , _) =
  ⊥-elim $ m+1+n≢m 0 (begin-equality
    2 + m  ≡⟨ 2+m≡q*0 ⟩
    q * 0  ≡⟨ *-zeroʳ q ⟩
    0      ∎)
prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
              (2+i∣2+m , 2+i∣1+n) =
  ⊥-elim (p _ 2+i′∣2+m)
  where
  i<m : i < m
  i<m = +-cancelˡ-< 2 (begin-strict
    2 + i ≤⟨ ∣⇒≤ 2+i∣1+n ⟩
    1 + n <⟨ 1+n<2+m ⟩
    2 + m ∎)

  2+i′∣2+m : 2 + toℕ (fromℕ< i<m) ∣ 2 + m
  2+i′∣2+m = subst (_∣ 2 + m)
    (P.sym (cong (2 +_) (toℕ-fromℕ< i<m)))
    2+i∣2+m

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use GCD from `Data.Nat.GCD` as continued support for the
-- proofs below is not guaranteed.

-- Version 1.1.

data GCD′ : ℕ → ℕ → ℕ → Set where
  gcd-* : ∀ {d} q₁ q₂ (c : Coprime q₁ q₂) →
          GCD′ (q₁ * d) (q₂ * d) d
{-# WARNING_ON_USAGE GCD′
"Warning: GCD′ was deprecated in v1.1."
#-}
gcd-gcd′ : ∀ {d m n} → GCD m n d → GCD′ m n d
gcd-gcd′         g with GCD.commonDivisor g
gcd-gcd′ {zero}  g | (divides q₁ refl , divides q₂ refl)
  with q₁ * 0 | *-comm 0 q₁ | q₂ * 0 | *-comm 0 q₂
... | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
gcd-gcd′ {suc d} g | (divides q₁ refl , divides q₂ refl) =
  gcd-* q₁ q₂ (Bézout-coprime (Bézout.identity g))
{-# WARNING_ON_USAGE gcd-gcd′
"Warning: gcd-gcd′ was deprecated in v1.1."
#-}
gcd′-gcd : ∀ {m n d} → GCD′ m n d → GCD m n d
gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (n∣m*n q₁ , n∣m*n q₂) (coprime-factors c)
{-# WARNING_ON_USAGE gcd′-gcd
"Warning: gcd′-gcd was deprecated in v1.1."
#-}
mkGCD′ : ∀ m n → ∃ λ d → GCD′ m n d
mkGCD′ m n = Prod.map id gcd-gcd′ (mkGCD m n)
{-# WARNING_ON_USAGE mkGCD′
"Warning: mkGCD′ was deprecated in v1.1."
#-}

-- Version 1.2

coprime-gcd = coprime⇒GCD≡1
{-# WARNING_ON_USAGE coprime-gcd
"Warning: coprime-gcd was deprecated in v1.2.
Please use coprime⇒GCD≡1 instead."
#-}
gcd-coprime = GCD≡1⇒coprime
{-# WARNING_ON_USAGE gcd-coprime
"Warning: gcd-coprime was deprecated in v1.2.
Please use GCD≡1⇒coprime instead."
#-}


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.KVMap
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude
open import Yasm.Base

open        EpochConfig

-- In this module, we define two "implementation obligations"
-- (ImplObligationᵢ for i ∈ {1 , 2}), which are predicates over
-- reachable states of a system defined by
-- 'LibraBFT.Concrete.System.Parameters'.  These two properties relate
-- votes sent by the same sender, ensuring that if they are for the
-- same epoch and round, then they vote for the same blockID; the
-- first relates a vote output by the handler to a vote sent
-- previously, and the second relates two votes both sent by the
-- handler.
--
-- We then prove that, if an implementation satisfies these two
-- semantic obligations, along with a structural one about messages
-- sent by honest peers in the implementation, then the implemenation
-- satisfies the LibraBFT.Abstract.Properties.VotesOnce invariant.

-- It is not actually necessary to provide an EpochConfig to define
-- these implementation obligations, but it is needed below to state
-- the goal of the proof (voo).  In contrast, the PreferredRound rule
-- requires and EpochConfig to state the obligations, because they
-- are defined in terms of abstract Records, which are defined for an
-- EpochConfig.  We introduce the EpochConfig at the top of this
-- module for consistency with the PreferredRound rule so that the
-- order of parameters to invoke the respective proofs is consistent.
module LibraBFT.Concrete.Properties.VotesOnce (iiah : SystemInitAndHandlers ℓ-RoundManager ConcSysParms) (𝓔 : EpochConfig) where
 open        SystemTypeParameters ConcSysParms
 open        SystemInitAndHandlers iiah
 open        ParamsWithInitAndHandlers iiah
 open import LibraBFT.Concrete.Properties.Common iiah 𝓔
 open import LibraBFT.ImplShared.Util.HashCollisions iiah
 open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms iiah PeerCanSignForPK PeerCanSignForPK-stable

 -- TODO-3: This may not be the best way to state the implementation obligation.  Why not reduce
 -- this as much as possible before giving the obligation to the implementation?  For example, this
 -- will still require the implementation to deal with hash collisons (v and v' could be different,
 -- but yield the same bytestring and therefore same signature).  Also, avoid the need for the
 -- implementation to reason about messages sent by step-cheat, or give it something to make this
 -- case easy to eliminate.

 ImplObligation₂ : Set (ℓ+1 ℓ-RoundManager)
 ImplObligation₂ =
   ∀{pid s' outs pk}{pre : SystemState}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → ∀{v m v' m'}
   → Meta-Honest-PK pk
   -- For every vote v represented in a message output by the call
   → v  ⊂Msg m  → send m ∈ outs
   → (sig : WithVerSig pk v) → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig))
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre))
   → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v pid pk
   -- And if there exists another v' that is also new and valid
   → v' ⊂Msg m'  → send m' ∈ outs
   → (sig' : WithVerSig pk v') → ¬ (∈BootstrapInfo bootstrapInfo (ver-signature sig'))
   → ¬ (MsgWithSig∈ pk (ver-signature sig') (msgPool pre))
   → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v' pid pk
   -- If v and v' share the same epoch and round
   → v ^∙ vEpoch ≡ v' ^∙ vEpoch
   → v ^∙ vRound ≡ v' ^∙ vRound
   ----------------------------------------------------------
   -- Then, an honest implemenation promises v and v' vote for the same blockId.
   → v ^∙ vProposedId ≡ v' ^∙ vProposedId

 -- Next, we prove that, given the necessary obligations,
 module Proof
   (sps-corr   : StepPeerState-AllValidParts)
   (Impl-bsvc  : ImplObl-bootstrapVotesConsistent)
   (Impl-bsvr  : ImplObl-bootstrapVotesRound≡0)
   (Impl-nvr≢0 : ImplObl-NewVoteRound≢0)
   (Impl-∈BI?  : (sig : Signature) → Dec (∈BootstrapInfo bootstrapInfo sig))
   (Impl-IRO   : IncreasingRoundObligation)
   (Impl-VO2   : ImplObligation₂)
   where

  -- Any reachable state satisfies the VO rule for any epoch in the system.
  module _ {st : SystemState}(r : ReachableSystemState st) where

   open Structural sps-corr
   -- Bring in intSystemState
   open PerEpoch 𝓔
   open PerState st
   open PerReachableState r
   open ConcreteCommonProperties st r sps-corr Impl-bsvr Impl-nvr≢0
   open WithEC

   open import LibraBFT.Concrete.Obligations.VotesOnce 𝓔 (ConcreteVoteEvidence 𝓔) as VO

   -- The VO proof is done by induction on the execution trace leading to 'st'. In
   -- Agda, this is 'r : RechableSystemState st' above.

   private

    -- From this point onwards, it might be easier to read this proof starting at 'voo'
    -- at the end of the file. Next, we provide an overview the proof.
    --
    -- We wish to prove that, for any two votes v and v' cast by an honest α in the message
    -- pool of a state st, if v and v' have equal rounds and epochs, then they vote for the
    -- same block.
    --
    -- The base case and the case for a new epoch in the system are trivial. For the base case
    -- we get to a contradiction because it's not possible to have any message in the msgpool.
    --
    -- Regarding the PeerStep case. The induction hypothesis tells us that the property holds
    -- in the pre-state.  Next, we reason about the post-state.  We start by analyzing whether
    -- v and v' have been sent as outputs of the PeerStep under scrutiny or were already in
    -- the pool before.
    --
    -- There are four possibilities:
    --
    --   i) v and v' were aleady present in the msgPool before: use induction hypothesis.
    --  ii) v and v' are both in the output produced by the PeerStep under scrutiny.
    -- iii) v was present before, but v' is new.
    --  iv) v' was present before, but v is new.
    --
    -- In order to obtain this four possiblities we invoke newMsg⊎msgSent4 lemma, which
    -- receives proof that some vote is in a message that is in the msgPool of the post state
    -- and returns evidence that either the vote is new or that some message with the same
    -- signature was sent before.
    --
    -- Case (i) is trivial; cases (iii) and (iv) are symmetric and reduce to an implementation
    -- obligation (Impl-VO1) and case (ii) reduces to a different implementation obligation
    -- (Impl-VO2).

    VotesOnceProof :
       ∀ {pk round epoch blockId₁ blockId₂} {st : SystemState}
       → ReachableSystemState st
       → Meta-Honest-PK pk
       → (m₁ : VoteForRound∈ pk round epoch blockId₁ (msgPool st))
       → (m₂ : VoteForRound∈ pk round epoch blockId₂ (msgPool st))
       → blockId₁ ≡ blockId₂
    VotesOnceProof step-0 _ m₁ = ⊥-elim (¬Any[] (msg∈pool m₁))
    VotesOnceProof step@(step-s r theStep) pkH m₁ m₂
       with msgRound≡ m₁ | msgEpoch≡ m₁ | msgBId≡ m₁
          | msgRound≡ m₂ | msgEpoch≡ m₂ | msgBId≡ m₂
    ...| refl | refl | refl | refl | refl | refl
       with Impl-∈BI? (_vSignature (msgVote m₁)) | Impl-∈BI? (_vSignature (msgVote m₂))
    ...| yes init₁  | yes init₂  = Impl-bsvc (msgVote m₁) (msgVote m₂) init₁ init₂
    ...| yes init₁  | no  ¬init₂ = ⊥-elim (NewVoteRound≢0 step pkH m₂ ¬init₂ (Impl-bsvr (msgSigned m₁) init₁))
    ...| no  ¬init₁ | yes init₂  = ⊥-elim (NewVoteRound≢0 step pkH m₁ ¬init₁ (Impl-bsvr (msgSigned m₂) init₂))
    ...| no  ¬init₁ | no ¬init₂
       with theStep
    ...| step-peer cheat@(step-cheat c)
         = let m₁sb4 = ¬cheatForgeNewSig r cheat unit pkH (msgSigned m₁) (msg⊆ m₁) (msg∈pool m₁) ¬init₁
               m₂sb4 = ¬cheatForgeNewSig r cheat unit pkH (msgSigned m₂) (msg⊆ m₂) (msg∈pool m₂) ¬init₂
               v₁sb4 = msgSentB4⇒VoteRound∈ (msgSigned m₁) m₁sb4
               v₂sb4 = msgSentB4⇒VoteRound∈ (msgSigned m₂) m₂sb4
           in VotesOnceProof r pkH (proj₁ v₁sb4) (proj₁ v₂sb4)
    ...| step-peer (step-honest stP)
       with ⊎-map₂ (msgSentB4⇒VoteRound∈ (msgSigned m₁))
                   (newMsg⊎msgSentB4 r stP pkH (msgSigned m₁) ¬init₁  (msg⊆ m₁) (msg∈pool m₁))
          | ⊎-map₂ (msgSentB4⇒VoteRound∈ (msgSigned m₂))
                   (newMsg⊎msgSentB4 r stP pkH (msgSigned m₂) ¬init₂ (msg⊆ m₂) (msg∈pool m₂))
    ...| inj₂ (v₁sb4 , refl)           | inj₂ (v₂sb4 , refl)
         = VotesOnceProof r pkH v₁sb4 v₂sb4
    ...| inj₁ (m₁∈outs , v₁pk , v₁New) | inj₁ (m₂∈outs , v₂pk , v₂New)
         = Impl-VO2 r stP pkH (msg⊆ m₁) m₁∈outs (msgSigned m₁) ¬init₁ v₁New v₁pk
                    (msg⊆ m₂) m₂∈outs (msgSigned m₂) ¬init₂ v₂New v₂pk refl refl
    ...| inj₁ (m₁∈outs , v₁pk , v₁New) | inj₂ (v₂sb4 , refl)
         = let round≡ = trans (msgRound≡ v₂sb4) (msgRound≡ m₂)
               ¬bootstrapV₂ = ¬Bootstrap∧Round≡⇒¬Bootstrap step pkH m₂ ¬init₂ (msgSigned v₂sb4) round≡
               epoch≡ = sym (msgEpoch≡ v₂sb4)
           in either (λ v₂<v₁ → ⊥-elim (<⇒≢ v₂<v₁ (msgRound≡ v₂sb4)))
                     (λ v₁sb4 → VotesOnceProof r pkH v₁sb4 v₂sb4)
                     (Impl-IRO r stP pkH (msg⊆ m₁) m₁∈outs (msgSigned m₁) ¬init₁ v₁New v₁pk
                               (msg⊆ v₂sb4) (msg∈pool v₂sb4) (msgSigned v₂sb4) ¬bootstrapV₂ epoch≡)
    ...| inj₂ (v₁sb4 , refl)           | inj₁ (m₂∈outs , v₂pk , v₂New)
         = let round≡ = trans (msgRound≡ v₁sb4) (msgRound≡ m₁)
               ¬bootstrapV₁ = ¬Bootstrap∧Round≡⇒¬Bootstrap step pkH m₁ ¬init₁ (msgSigned v₁sb4) round≡
           in either (λ v₁<v₂ → ⊥-elim (<⇒≢ v₁<v₂ (msgRound≡ v₁sb4)))
                     (λ v₂sb4 → VotesOnceProof r pkH v₁sb4 v₂sb4)
                     (Impl-IRO r stP pkH (msg⊆ m₂) m₂∈outs (msgSigned m₂) ¬init₂ v₂New v₂pk
                               (msg⊆ v₁sb4) (msg∈pool v₁sb4) (msgSigned v₁sb4) ¬bootstrapV₁
                               (sym (msgEpoch≡ v₁sb4)))

   voo : VO.Type intSystemState
   voo hpk refl sv refl sv' refl
      with vmsg≈v (vmFor sv) | vmsg≈v (vmFor sv')
   ...| refl | refl
      with vmsgEpoch (vmFor sv) | vmsgEpoch (vmFor sv')
   ...| refl | refl
       = let vfr  = mkVoteForRound∈ (nm (vmFor sv)) (cv ((vmFor sv))) (cv∈nm (vmFor sv))
                                    (vmSender sv) (nmSentByAuth sv) (vmsgSigned (vmFor sv))
                                    (vmsgEpoch (vmFor sv)) refl refl
             vfr' = mkVoteForRound∈ (nm (vmFor sv')) (cv (vmFor sv')) (cv∈nm (vmFor sv'))
                                    (vmSender sv') (nmSentByAuth sv') (vmsgSigned (vmFor sv'))
                                    (vmsgEpoch (vmFor sv')) refl refl
         in VotesOnceProof r hpk vfr vfr'


text:
open import Data.Product using ( _×_ ; _,_ )
open import Data.Sum using ( _⊎_ )
open import Relation.Unary using ( _∈_ ; _∉_ )
open import Web.Semantic.DL.FOL using  ( Formula ; true ; false ; _∧_ ; _∈₁_ ; _∈₁_⇒_ ; _∈₂_ ; _∈₂_⇒_ ; _∼_ ; _∼_⇒_ ; ∀₁ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using ( Interp ; Δ ; _⊨_≈_ ; con ; rol )
open import Web.Semantic.Util using ( True ; False )

module Web.Semantic.DL.FOL.Model {Σ : Signature} where

_⊨f_ : (I : Interp Σ) → Formula Σ (Δ I) → Set
I ⊨f true = True
I ⊨f false = False
I ⊨f (F ∧ G) = (I ⊨f F) × (I ⊨f G)
I ⊨f (x ∈₁ c) = x ∈ (con I c)
I ⊨f (x ∈₁ c ⇒ F) = (x ∈ (con I c)) → (I ⊨f F)
I ⊨f ((x , y) ∈₂ r) = (x , y) ∈ (rol I r)
I ⊨f ((x , y) ∈₂ r ⇒ F) = ((x , y) ∈ (rol I r)) → (I ⊨f F)
I ⊨f (x ∼ y) = I ⊨ x ≈ y
I ⊨f (x ∼ y ⇒ F) = (I ⊨ x ≈ y) → (I ⊨f F)
I ⊨f ∀₁ F = ∀ x → (I ⊨f F x)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
data Cx (U : Set) : Set where
  ∅   : Cx U
  _,_ : Cx U → U → Cx U

data _∈_ {U : Set} (A : U) : Cx U → Set where
  top : ∀ {Γ} → A ∈ (Γ , A)
  pop : ∀ {B Γ} → A ∈ Γ → A ∈ (Γ , B)

infixr 3 _⇒_
data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty
  □_  : Ty → Ty

infix 1 _⊢_
data _⊢_ : Cx Ty → Ty → Set where
  var  : ∀ {Γ A}     → A ∈ Γ → Γ ⊢ A
  app  : ∀ {Γ A B}   → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
  nec  : ∀ {A}       → ∅ ⊢ A → ∅ ⊢ □ A
  kcom : ∀ {Γ A B}   → Γ ⊢ A ⇒ B ⇒ A
  scom : ∀ {Γ A B C} → Γ ⊢ (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
  dist : ∀ {Γ A B}   → Γ ⊢ □ (A ⇒ B) ⇒ □ A ⇒ □ B
  down : ∀ {Γ A}     → Γ ⊢ □ A ⇒ A
  up   : ∀ {Γ A}     → Γ ⊢ □ A ⇒ □ □ A

icom : ∀ {A Γ} → Γ ⊢ A ⇒ A
icom {A} = app (app (scom {A = A} {B = A ⇒ A} {C = A}) kcom) kcom

ded : ∀ {A B Γ} → Γ , A ⊢ B → Γ ⊢ A ⇒ B
ded (var top)     = icom
ded (var (pop i)) = app kcom (var i)
ded (app t u)     = app (app scom (ded t)) (ded u)
ded (nec t)       = ?
ded kcom          = app kcom kcom
ded scom          = app kcom scom
ded dist          = app kcom dist
ded down          = app kcom down
ded up            = app kcom up