text:
module FOLdisplay where

open import Data.String using (String)

open import Data.Empty

open import Data.Nat

open import Data.Product
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; subst)
open import Relation.Nullary

open import Data.String using (String; _++_)

-- open import Data.Fin
-- open import Data.Fin.Subset
open import Data.List.Base as List using (List; []; _∷_; [_])
-- open import Data.Bool using () renaming (_∨_ to _∨B_)

Name : Set
Name = String

insert : ℕ → List ℕ → List ℕ
insert n List.[] = n ∷ []
insert n (x ∷ l) with n ≟ x
insert n (.n ∷ l) | yes refl = n ∷ l
insert n (x ∷ l) | no n≠x with n ≤? x
insert n (x ∷ l) | no n≠x | yes n<x = n ∷ x ∷ l
insert n (x ∷ l) | no n≠x | no n>x = x ∷ insert n l

sortRemDups : List ℕ → List ℕ
sortRemDups [] = []
sortRemDups (x ∷ xs) = insert x (sortRemDups xs)

union : List ℕ → List ℕ → List ℕ
union [] ys = ys
union (x ∷ xs) ys = insert x (union xs ys)

remove : ℕ → List ℕ → List ℕ
remove n [] = []
remove n (x ∷ xs) with n Data.Nat.≟ x
remove n (.n ∷ xs) | yes refl = xs
remove n (x ∷ xs) | no _ = x ∷ remove n xs

remove-rewrite : ∀ x {xs} -> remove x (x ∷ xs) ≡ xs
remove-rewrite x with x ≟ x
remove-rewrite x | yes refl = refl
remove-rewrite x | no x≠x = ⊥-elim (x≠x refl)

-- xs \\ ys
diff : List ℕ → List ℕ → List ℕ
diff xs [] = xs
diff xs (x ∷ ys) = diff (remove x xs) ys

--
-- mutual
--   data TermT : List ℕ -> Set where
--     VarT : (n : ℕ) → TermT [ n ]
--     ConstT : Name → TermT []
--     FunT : ∀ {xs} -> Name → (TermList xs) → TermT xs
--   -- [[[_]]]T_ : List (Term × ℕ) → Term → Term
--   data TermList : List ℕ -> Set where
--     []T : TermList []
--     _∷T_ : ∀ {xs ys} (t : TermT xs) (ts : TermT ys) -> TermList (union xs ys)
--
--   data SubstList : List ℕ -> Set where
--     []S : SubstList []
--     _/_∷S_ : ∀ {xs ys} (t : TermT xs) (x : ℕ) (ts : TermT ys) -> SubstList (union xs (remove x ys))

data Term : Set where
  Var : ℕ → Term
  Const : Name → Term
  Fun : Name → List Term → Term
  -- [[_/_]]_ : Term → ℕ → Term → Term
  [[[_]]]_ : List (Term × ℕ) → Term → Term

mutual
  data _⊢≡_ : Term → Term → Set where
    atom : ∀ {n} → Var n ⊢≡ Var n
    atomC : ∀ {n} → Const n ⊢≡ Const n
    funEq : ∀ {n arg1 arg2} → arg1 ≡ₗ arg2 → Fun n arg1 ⊢≡ Fun n arg2
    -- subMon : ∀ {substs X Y} → X ⊢≡ Y → ([[[ substs ]]] X) ⊢≡ ([[[ substs ]]] Y) -- this rule is derivable
    sub[]R : ∀ {X Y} → X ⊢≡ Y → X ⊢≡ ([[[ [] ]]] Y)
    sub[]L : ∀ {X Y} → X ⊢≡ Y → ([[[ [] ]]] X) ⊢≡ Y
    subAtomEqR : ∀ {x t lst X} → X ⊢≡ ([[[ lst ]]] t) → X ⊢≡ ([[[ (t , x) ∷ lst ]]] (Var x))
    subAtomEqL : ∀ {x t lst Y} → ([[[ lst ]]] t) ⊢≡ Y → ([[[ (t , x) ∷ lst ]]] (Var x)) ⊢≡ Y

    subAtomNeqR : ∀ {x y t lst X} → X ⊢≡ ([[[ lst ]]] (Var x)) → x ≢ y → X ⊢≡ ([[[ (t , y) ∷ lst ]]] (Var x))
    subAtomNeqL : ∀ {x y t lst Y} → ([[[ lst ]]] (Var x)) ⊢≡ Y → x ≢ y → ([[[ (t , y) ∷ lst ]]] (Var x)) ⊢≡ Y

    subAtomCR : ∀ {n lst X} → X ⊢≡ (Const n) → X ⊢≡ ([[[ lst ]]] (Const n))
    subAtomCL : ∀ {n lst Y} → (Const n) ⊢≡ Y → ([[[ lst ]]] (Const n)) ⊢≡ Y

    subFunR : ∀ {n arg lst X} → X ⊢≡ (Fun n (List.map ([[[_]]]_ lst) arg)) → X ⊢≡ ([[[ lst ]]] (Fun n arg))
    subFunL : ∀ {n arg lst Y} → (Fun n (List.map ([[[_]]]_ lst) arg)) ⊢≡ Y → ([[[ lst ]]] (Fun n arg)) ⊢≡ Y

    subConsR : ∀ {lst lst' X Y} → X ⊢≡ ([[[ lst List.++ lst' ]]] Y) → X ⊢≡ ([[[ lst' ]]] ([[[ lst ]]] Y))
    subConsL : ∀ {lst lst' X Y} → ([[[ lst List.++ lst' ]]] X) ⊢≡ Y → ([[[ lst' ]]] ([[[ lst ]]] X)) ⊢≡ Y

  data _≡ₗ_ : List Term → List Term → Set where
    []≡ : [] ≡ₗ []
    _∷≡_ : {xs : List Term} {ys : List Term} {t1 t2 : Term} → t1 ⊢≡ t2 → xs ≡ₗ ys → (t1 ∷ xs) ≡ₗ (t2 ∷ ys)

-- open import Data.Maybe using (Maybe; just; nothing; monad)
--
-- open import Category.Monad using (RawMonad)
-- open import Agda.Primitive as P
--
-- open RawMonad (monad {P.lzero}) using (_>>=_;return)
-- open Category.Monad.rawMonad
open import Data.String using () renaming (_≟_ to _≟S_)

data Term' : Set where
  Var' : ℕ → Term'
  Const' : Name → Term'
  Fun' : Name → List Term' → Term'

mutual
  data TTerm : List ℕ -> Set where
    TVar : (n : ℕ) → TTerm [ n ]
    TConst : Name → TTerm []
    TFun : ∀ {xs} -> Name → TTermList xs → TTerm xs

  data TTermList : List ℕ -> Set where
    []T : TTermList []
    _∷T_ : ∀ {xs ys} (t : TTerm xs) (ts : TTermList ys) -> TTermList (union xs ys)

open import Relation.Nullary.Decidable
open import Relation.Binary.Core

open import Data.List.Any as LAny
open LAny.Membership-≡

∈-∷-elim : ∀ {A : Set} {x : A} (y : A) xs -> ¬(x ≡ y) -> y ∈ x ∷ xs -> y ∈ xs
∈-∷-elim x [] x≠y (here refl) = ⊥-elim (x≠y refl)
∈-∷-elim y [] _ (there ())
∈-∷-elim x (x₁ ∷ xs) x≠y (here refl) = ⊥-elim (x≠y refl)
∈-∷-elim y (x₁ ∷ xs) _ (there y∈x∷xs) = y∈x∷xs

_∈ℕ?_ : Decidable {A = ℕ} (_∈_)
x ∈ℕ? [] = no (λ ())
x ∈ℕ? (x' ∷ xs) with x ≟ x'
x ∈ℕ? (.x ∷ xs) | yes refl = yes (here refl)
x ∈ℕ? (x' ∷ xs) | no x≠x' with x ∈ℕ? xs
x ∈ℕ? (x' ∷ xs) | no x≠x' | yes x∈xs = yes (there x∈xs)
x ∈ℕ? (x' ∷ xs) | no x≠x' | no x∉xs = no (λ x∈x'∷xs → x∉xs (∈-∷-elim x xs (λ x'≡x → x≠x' (sym x'≡x)) x∈x'∷xs))

-- subTaux : List ℕ -> ℕ -> List ℕ -> List ℕ
-- subTaux xs x ys with x ∈ℕ? ys
-- subTaux xs x ys | yes _ = union xs (remove x ys)
-- subTaux xs x ys | no _ = ys

-- mutual
--   subT : ∀ {ts ys} → TTerm ts → (x : ℕ) -> TTerm ys → TTerm (subTaux ts x ys)
--   subT t x (TVar x') with x ≟ x'
--   subT t .x' (TVar x') | yes refl rewrite remove-rewrite x' {[]} = {! t'  !}
--   ... | no _ = (TVar x')
--   subT _ _ (TConst n) = TConst n
--   subT t x (TFun n args) = TFun n (subTList t x args)
--
--   subTList : ∀ {ts ys} → TTerm ts → (x : ℕ) -> TTermList ys → TTermList (subTaux ts x ys)
--   subTList _ _ []T = []T
--   subTList {ts} t x (_∷T_ {xs} {ys} a args) = rec
--     where
--       a' : TTerm (subTaux ts x xs)
--       a' = subT t x a
--
--       args' : TTermList (subTaux ts x ys)
--       args' = subTList t x args
--
--       ≡-subTaux : ∀ x xs ys -> subTaux ts x (union xs ys) ≡ union (subTaux ts x xs) (subTaux ts x ys)
--       ≡-subTaux _ [] _ = refl
--       ≡-subTaux x (x' ∷ xs) ys = {!   !}
--
--       rec : TTermList (subTaux ts x (union xs ys))
--       rec rewrite ≡-subTaux x xs ys = a' ∷T args'
--
--     --subT x t' t ∷T subTList x t' l
--

TTerm→Term : ∀ {xs} -> TTerm xs -> Term
TTerm→Term (TVar n) = Var n
TTerm→Term (TConst c) = Const c
TTerm→Term (TFun n args) = Fun n (TTermList→ListTerm args)
  where
    TTermList→ListTerm : ∀ {xs} -> TTermList xs -> List Term
    TTermList→ListTerm []T = []
    TTermList→ListTerm (_∷T_ {_} {ys} t ts) = (TTerm→Term t) ∷ (TTermList→ListTerm {ys} ts)

mutual
  sub : ℕ → Term' → Term' → Term'
  sub x t' (Var' x') with x ≟ x'
  ... | yes _ = t'
  ... | no _ = (Var' x')
  sub x t' (Const' n) = Const' n
  sub x t' (Fun' n args) = Fun' n (subList x t' args)

  subList : ℕ → Term' → List Term' → List Term'
  subList x t' [] = []
  subList x t' (t ∷ l) = sub x t' t ∷ subList x t' l

mutual
  Term→Term' : Term → Term'
  Term→Term' (Var x) = Var' x
  Term→Term' (Const c) = Const' c
  Term→Term' (Fun n args) = Fun' n (LTerm→LTerm' args)
  Term→Term' ([[[ lst ]]] t) = STerm lst (Term→Term' t)

  LTerm→LTerm' : List Term → List Term'
  LTerm→LTerm' [] = []
  LTerm→LTerm' (x ∷ l) = Term→Term' x ∷ LTerm→LTerm' l

  STerm : List (Term × ℕ) → Term' → Term'
  STerm [] t = t
  STerm ((t' , x) ∷ lst) t = STerm lst (sub x (Term→Term' t') t)

mutual
  ⊢≡symm : ∀ {t1 t2 : Term} → t1 ⊢≡ t2 → t2 ⊢≡ t1
  ⊢≡symm atom = atom
  ⊢≡symm atomC = atomC
  ⊢≡symm (funEq x) = funEq (≡ₗsymm x)
  ⊢≡symm (sub[]R {Y = Y} t1⊢≡t2) = sub[]L (⊢≡symm t1⊢≡t2)
  ⊢≡symm (sub[]L {X = X} t1⊢≡t2) = sub[]R (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subAtomEqR {t = t} {lst} t1⊢≡t2) = subAtomEqL (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subAtomEqL {t = t} {lst} t1⊢≡t2) = subAtomEqR (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subAtomNeqR {x = x} t1⊢≡t2 x₁) = subAtomNeqL (⊢≡symm t1⊢≡t2) x₁
  ⊢≡symm (subAtomNeqL {x = x} t1⊢≡t2 x₁) = subAtomNeqR (⊢≡symm t1⊢≡t2) x₁
  ⊢≡symm (subAtomCR {n = n} t1⊢≡t2) = subAtomCL (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subAtomCL t1⊢≡t2) = subAtomCR (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subFunR t1⊢≡t2) = subFunL (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subFunL t1⊢≡t2) = subFunR (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subConsR t1⊢≡t2) = subConsL (⊢≡symm t1⊢≡t2)
  ⊢≡symm (subConsL t1⊢≡t2) = subConsR (⊢≡symm t1⊢≡t2)

  ≡ₗsymm : ∀ {arg1 arg2} → arg1 ≡ₗ arg2 → arg2 ≡ₗ arg1
  ≡ₗsymm []≡ = []≡
  ≡ₗsymm (x ∷≡ arg1≡ₗarg2) = (⊢≡symm x) ∷≡ (≡ₗsymm arg1≡ₗarg2)

≡-Fun-nm : ∀ {n n' args args'} → Fun' n args ≡ Fun' n' args' → n ≡ n'
≡-Fun-nm refl = refl

≡-Fun-args : ∀ {n args args'} → Fun' n args ≡ Fun' n args' → args ≡ args'
≡-Fun-args refl = refl

Fun-args-≡ : ∀ {n args args'} → args ≡ args' → Fun' n args ≡ Fun' n args'
Fun-args-≡ refl = refl

substFun≡aux : ∀ {n} lst args → STerm lst (Fun' n args) ≡ Fun' n (List.map (STerm lst) args)
substFun≡aux [] args = Fun-args-≡ (aux args)
  where
    aux : ∀ args → args ≡ List.map (STerm []) args
    aux [] = refl
    aux (a ∷ args) = cong (_∷_ a) (aux args)
substFun≡aux {n} ((t , x) ∷ lst) args = PropEq.trans (substFun≡aux {n} lst (subList x (Term→Term' t) args)) (Fun-args-≡ (aux lst x t args))
  where
    aux : ∀ lst x t args → List.map (STerm lst) (subList x (Term→Term' t) args) ≡ List.map (STerm ((t , x) ∷ lst)) args
    aux lst x t [] = refl
    aux lst x t (x' ∷ args) = cong (_∷_ (STerm lst (sub x (Term→Term' t) x'))) (aux lst x t args)

substFun≡ : ∀ {n} args lst → Term→Term' ([[[ lst ]]] Fun n args) ≡ Fun' n (LTerm→LTerm' (List.map ([[[_]]]_ lst) args))
substFun≡ [] [] = refl
substFun≡ [] (s ∷ lst) = substFun≡ [] lst
substFun≡ (a ∷ args) [] = Fun-args-≡ (cong (_∷_ (Term→Term' a)) (LTerm[]Subst args))
  where
    LTerm[]Subst : ∀ args → LTerm→LTerm' args ≡ LTerm→LTerm' (List.map ([[[_]]]_ []) args)
    LTerm[]Subst [] = refl
    LTerm[]Subst (a ∷ args) = cong (_∷_ (Term→Term' a)) (LTerm[]Subst args)
substFun≡ (a ∷ args) ((t , x) ∷ lst) = PropEq.trans
  (substFun≡aux lst (subList x (Term→Term' t) (LTerm→LTerm' (a ∷ args))))
  (Fun-args-≡ (aux (a ∷ args)))
  where
    aux : ∀ args {lst x t} → List.map (STerm lst) (subList x (Term→Term' t) (LTerm→LTerm' args)) ≡ LTerm→LTerm' (List.map ([[[_]]]_ ((t , x) ∷ lst)) args)
    aux [] = refl
    aux (a ∷ args) {lst} {x} {t} = cong (_∷_ (STerm lst (sub x (Term→Term' t) (Term→Term' a)))) (aux args)

++[]-id : ∀ {a} {A : Set a} (lst : List A) → lst List.++ [] ≡ lst
++[]-id [] = refl
++[]-id (x ∷ xs) = cong (_∷_ x) (++[]-id xs)

substSubst≡ : ∀ {lst lst' t} → Term→Term' ([[[ lst ]]] ([[[ lst' ]]] t)) ≡ Term→Term' ([[[ lst' List.++ lst ]]] t)
substSubst≡ {[]} {lst'} rewrite ++[]-id lst' = refl
substSubst≡ {(t , x₂) ∷ lst} {[]} = refl
substSubst≡ {(t , x) ∷ lst} {(t' , x') ∷ lst'} {t''} = substSubst≡ {(t , x) ∷ lst} {lst'} {[[[ [ (t' , x') ]  ]]] t''}

subsConst≡ : ∀ {lst c} → Term→Term' ([[[ lst ]]] (Const c)) ≡ Const' c
subsConst≡ {[]} = refl
subsConst≡ {_ ∷ lst} {c} = subsConst≡ {lst} {c}

open import Data.List.Properties

substTac : (t1 : Term) → (t2 : Term) → {_ : Term→Term' t1 ≡ Term→Term' t2} → t1 ⊢≡ t2
{-# TERMINATING #-}
substTac (Var x) (Var .x) {refl} = atom
substTac (Var _) (Const _) {()}
substTac (Var _) (Fun _ _) {()}

substTac (Const _) (Var _) {()}
substTac (Const c) (Const .c) {refl} = atomC
substTac (Const _) (Fun _ _) {()}

substTac (Fun _ _) (Var _) {()}
substTac (Fun _ _) (Const _) {()}
substTac (Fun n args) (Fun n' args') with n ≟S n'
substTac (Fun n []) (Fun .n []) | yes refl = funEq []≡
substTac (Fun n []) (Fun .n (_ ∷ _)) {()} | yes refl
substTac (Fun n (x ∷ args)) (Fun .n []) {()} | yes refl
substTac (Fun n (t ∷ args)) (Fun .n (t' ∷ args')) {eq} | yes refl with
  substTac t t' {proj₁ (∷-injective (≡-Fun-args eq))} |
  substTac (Fun n args) (Fun n args') {Fun-args-≡ (proj₂ (∷-injective (≡-Fun-args eq)))}
substTac (Fun n (t ∷ args)) (Fun .n (t' ∷ args')) | yes refl | t⊢≡t' | funEq args≡ₗargs' = funEq (t⊢≡t' ∷≡ args≡ₗargs')
substTac (Fun n args) (Fun n' args') {eq} | no ¬p = ⊥-elim (¬p (≡-Fun-nm eq))

substTac t1 ([[[ [] ]]] t2) {eq} = sub[]R (substTac t1 t2 {eq})
substTac t1 ([[[ (t , x') ∷ lst ]]] Var x) with x ≟ x'
substTac t1 ([[[ (t , x') ∷ lst ]]] Var .x') {eq} | yes refl =
  subAtomEqR (substTac t1 ([[[ lst ]]] t) {eq' {x'} {Term→Term' t1} {t} {lst} eq}) -- agda doesnt like this call because it doesnt get structurally smaller, but its fine...
  where
    eq' : ∀ {x t t' lst} → t ≡ Term→Term' (([[[ (t' , x) ∷ lst ]]] Var x)) → t ≡ Term→Term' ([[[ lst ]]] t')
    eq' {x} refl with x ≟ x
    eq' {x} refl | yes _ = refl
    eq' {x} refl | no ¬p = ⊥-elim (¬p refl)
substTac t1 ([[[ (t , x') ∷ lst ]]] Var x) {eq} | no ¬p = subAtomNeqR (substTac t1 ([[[ lst ]]] (Var x)) {eq' {x} {x'} {Term→Term' t1} {t} {lst} eq ¬p}) ¬p
  where
    eq' : ∀ {x x' t t' lst} → t ≡ Term→Term' (([[[ (t' , x') ∷ lst ]]] Var x)) → x ≢ x' → t ≡ Term→Term' ([[[ lst ]]] Var x)
    eq' {x} {x'} refl x≠x' with x' ≟ x
    eq' {x} {.x} refl x≠x' | yes refl = ⊥-elim (x≠x' refl)
    eq' {x} {x'} refl x≠x' | no ¬p = refl
substTac t1 ([[[ x ∷ lst ]]] Const c) {eq} = subAtomCR (substTac t1 (Const c) {PropEq.trans eq (subsConst≡ {x ∷ lst} {c})})
substTac t1 ([[[ x ∷ lst ]]] Fun n args) {eq} = subFunR (substTac t1 (Fun n (List.map ([[[_]]]_ (x ∷ lst)) args)) {PropEq.trans eq (substFun≡ args (x ∷ lst))})

substTac t1 ([[[ x ∷ lst ]]] ([[[ lst' ]]] t2)) {eq} =
  subConsR (substTac t1 ([[[ lst' List.++ x ∷ lst ]]] t2) {PropEq.trans eq (substSubst≡ {x ∷ lst} {lst'} {t2})})

substTac ([[[ lst ]]] t1) t2 {eq} = ⊢≡symm (substTac t2 ([[[ lst ]]] t1) {sym eq}) -- adga doesn't like this, but it should be fine...

⊢≡-≡ : ∀ {X Y} → X ⊢≡ Y → Term→Term' X ≡ Term→Term' Y
⊢≡-≡ atom = refl
⊢≡-≡ atomC = refl
⊢≡-≡ (funEq x) = Fun-args-≡ (≡ₗ→≡ x)
  where
    ∷-≡ : ∀ {a} {A : Set a} {x y : A} {xs ys} → x ≡ y → xs ≡ ys → x ∷ xs ≡ y ∷ ys
    ∷-≡ refl refl = refl

    ≡ₗ→≡ : ∀ {arg1 arg2} → arg1 ≡ₗ arg2 → (LTerm→LTerm' arg1) ≡ (LTerm→LTerm' arg2)
    ≡ₗ→≡ []≡ = refl
    ≡ₗ→≡ (t1⊢≡t2 ∷≡ ≡ₗ) = ∷-≡ (⊢≡-≡ t1⊢≡t2) (≡ₗ→≡ ≡ₗ)
⊢≡-≡ (sub[]R X⊢≡Y) = ⊢≡-≡ X⊢≡Y
⊢≡-≡ (sub[]L X⊢≡Y) = ⊢≡-≡ X⊢≡Y
⊢≡-≡ (subAtomEqR {x} X⊢≡Y) with x ≟ x
⊢≡-≡ (subAtomEqR {x} X⊢≡Y) | yes p = ⊢≡-≡ X⊢≡Y
⊢≡-≡ (subAtomEqR {x} X⊢≡Y) | no ¬p = ⊥-elim (¬p refl)
⊢≡-≡ (subAtomEqL {x} X⊢≡Y) with x ≟ x
⊢≡-≡ (subAtomEqL {x} X⊢≡Y) | yes p = ⊢≡-≡ X⊢≡Y
⊢≡-≡ (subAtomEqL {x} X⊢≡Y) | no ¬p = ⊥-elim (¬p refl)
⊢≡-≡ (subAtomNeqR {x} {y} X⊢≡Y x₁) with y ≟ x
⊢≡-≡ (subAtomNeqR {x} {.x} X⊢≡Y x₁) | yes refl = ⊥-elim (x₁ refl)
⊢≡-≡ (subAtomNeqR {x} {y} X⊢≡Y x₁) | no ¬p = ⊢≡-≡ X⊢≡Y
⊢≡-≡ (subAtomNeqL {x} {y} X⊢≡Y x₁) with y ≟ x
⊢≡-≡ (subAtomNeqL {x} {.x} X⊢≡Y x₁) | yes refl = ⊥-elim (x₁ refl)
⊢≡-≡ (subAtomNeqL {x} {y} X⊢≡Y x₁) | no ¬p = ⊢≡-≡ X⊢≡Y
⊢≡-≡ (subAtomCR {c} {lst} X⊢≡Y) = PropEq.trans (⊢≡-≡ X⊢≡Y) (sym (subsConst≡ {lst} {c}))
⊢≡-≡ (subAtomCL {c} {lst} X⊢≡Y) = PropEq.trans (subsConst≡ {lst} {c}) (⊢≡-≡ X⊢≡Y)
⊢≡-≡ (subFunR {n} {args} {lst} X⊢≡Y) = PropEq.trans (⊢≡-≡ X⊢≡Y) (sym (substFun≡ {n} args lst))
⊢≡-≡ (subFunL {n} {args} {lst} X⊢≡Y) = PropEq.trans (substFun≡ {n} args lst) (⊢≡-≡ X⊢≡Y)
⊢≡-≡ (subConsR {lst} {lst'} {_} {Y} X⊢≡Y) = PropEq.trans (⊢≡-≡ X⊢≡Y) (sym (substSubst≡ {lst'} {lst} {Y}))
⊢≡-≡ (subConsL {lst} {lst'} {X} X⊢≡Y) = PropEq.trans (substSubst≡ {lst'} {lst} {X}) (⊢≡-≡ X⊢≡Y)

mutual
  ⊢≡atom : ∀ {t} → t ⊢≡ t
  ⊢≡atom {Var x} = atom
  ⊢≡atom {Const x} = atomC
  ⊢≡atom {Fun x x₁} = funEq ≡ₗatom
    where
      ≡ₗatom : ∀ {xs} → xs ≡ₗ xs
      ≡ₗatom {[]} = []≡
      ≡ₗatom {x ∷ xs} = ⊢≡atom ∷≡ ≡ₗatom
  ⊢≡atom {[[[ x ]]] t} = ⊢≡subMon ⊢≡atom

  ⊢≡subMon : ∀ {sub X Y} → X ⊢≡ Y → ([[[ sub ]]] X) ⊢≡ ([[[ sub ]]] Y)
  ⊢≡subMon {sub} {X} {Y} X⊢≡Y = substTac ([[[ sub ]]] X) ([[[ sub ]]] Y) {mon {sub} {Term→Term' X} {Term→Term' Y} (⊢≡-≡ X⊢≡Y)}
    where
      mon : ∀ {sub X Y} → X ≡ Y → STerm sub X ≡ STerm sub Y
      mon refl = refl

-- data _∈_ : ℕ → List ℕ → Set where
--   here : ∀ {x xs} → x ∈ (x ∷ xs)
--   there : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)
--
-- data _⊆_ : List ℕ → List ℕ → Set where
--   nil : ∀ {xs} → [] ⊆ xs
--   cons : ∀ {x xs ys} → x ∈ ys → xs ⊆ ys → (x ∷ xs) ⊆ ys
--
-- _∉_ : ℕ → List ℕ → Set
-- n ∉ ns = ¬ (n ∈ ns)
--
-- _⊈_ : List ℕ → List ℕ → Set
-- xs ⊈ ys = ¬ (xs ⊆ ys)

mutual
  FV : Term' → List ℕ
  FV (Var' x) = [ x ]
  FV (Const' _) = []
  FV (Fun' _ args) = FVs args

  FVs : List Term' → List ℕ
  FVs [] = []
  FVs (t ∷ ts) = union (FV t) (FVs ts)

data Formula : List ℕ → Set where
  _⟨_⟩ : Name → ∀ {xs} (ts : TTermList xs) → Formula xs
  _∧_ : ∀ {ns} → Formula ns → Formula ns → Formula ns
  _∨_ : ∀ {ns} → Formula ns → Formula ns → Formula ns
  _⟶_ : ∀ {ns} → Formula ns → Formula ns → Formula ns
  ∘ : ∀ {ns} v → Formula ns → {v∉ : v ∉ ns} → Formula (insert v ns)
  -- [_/_] : ∀ {y ns} → Term → (x : ℕ) → {x∈ : x ∈ ns} → {y⊆ : y ⊆ ns} → {x≠y : [ x ] ≢ y} → Formula ns → Formula (remove x ns)
  -- [_//_] : ∀ {y ns} → Term y → (x : ℕ) → {x⊆ : x ∈ ns} → {y⊈ : y ⊈ ns} → {x≠y : [ x ] ≢ y} → Formula ns → Formula (union y (remove x ns))
  All : ∀ {ns} v → Formula ns → Formula (remove v ns)
  Ex : ∀ {ns} v → Formula ns → Formula (remove v ns)

data Structure : List ℕ → Set where
  ∣_∣ : ∀ {n} → Formula n → Structure n
  _,_ : ∀ {n m} → Structure n → Structure m → {n≡m : n ≡ m} -> Structure n
  _>>_ : ∀ {n m} → Structure n → Structure m → {n≡m : n ≡ m} → Structure n
  _<<_ : ∀ {n m} → Structure n → Structure m → {n≡m : n ≡ m} → Structure n
  I : ∀ {n} → Structure n
  ○ : ∀ {n} v → Structure n → {v∉ : v ∉ n} → Structure (insert v n)
  Q : ∀ {n} v → Structure n → Structure (remove v n)

data _⊢_ : ∀ {n} → Structure n → Structure n → Set where
  atom : ∀ {n xs} {ts us : TTermList xs} →
    ∣ n ⟨ ts ⟩ ∣ ⊢ ∣ n ⟨ us ⟩ ∣
  allR : ∀ {x n X Y} →
    Y ⊢ Q {n} x ∣ X ∣ →
    -------------------
    Y ⊢ ∣ All {n} x X ∣
  allL : ∀ {x n X Y} →
            ∣ Y ∣ ⊢ ∣ X ∣ →
    -------------------------------
    ∣ All {n} x Y ∣ ⊢ Q {n} x ∣ X ∣

open import Data.Unit as Unit using (⊤)
open import Data.Nat.Properties as Propℕ

_≤'?_ : Decidable _≤′_
x ≤'? y with x ≤? y
x ≤'? y | yes p = yes (≤⇒≤′ p)
x ≤'? y | no ¬p = no (λ x₁ → ¬p (≤′⇒≤ x₁))

-- mutual
--   data OList : Set where
--     []O : OList
--     _∷O_ : (x : ℕ) -> (xs : OList) -> {x< : isLess x xs} -> OList
--
--   isLess : ℕ -> OList -> Set
--   isLess x []O = ⊤
--   isLess x (y ∷O ol) with x ≤'? y
--   isLess x (.x ∷O ol) | yes ≤′-refl = ⊥
--   isLess x (.(suc _) ∷O ol) | yes (≤′-step _) = ⊤
--   isLess x (y ∷O ol) | no _ = ⊥
--
--
--
-- mutual
--   data IsLess : ℕ -> OList -> Set where
--     nil : ∀ {x} -> IsLess x []O
--     cons : ∀ {x x' xs} -> x < x' -> (x'<xs : IsLess x' xs) -> IsLess x ((x' ∷O xs) {IsLess→isLess x'<xs})
--
--   IsLess→isLess : ∀ {x xs} -> IsLess x xs -> isLess x xs
--   IsLess→isLess nil = ⊤.tt
--   IsLess→isLess {x} (cons {x' = x'} x<x' x<xs) with x ≤'? x'
--   IsLess→isLess {x} (cons {_} {.x} x<x' x<xs) | yes ≤′-refl = contr x<x'
--     where
--       contr : ∀ {x} -> suc x ≤ x -> ⊥
--       contr {zero} ()
--       contr {suc x} (s≤s sx≤x) = contr sx≤x
--   IsLess→isLess {x} (cons {_} {.(suc _)} x<x' x<xs) | yes (≤′-step p) = ⊤.tt
--   IsLess→isLess {x} (cons {_} {x'} x<x' x<xs) | no ¬x≤′x' = ¬x≤′x' (≤⇒≤′ (sucx≤y→x≤y x<x'))
--     where
--       sucx≤y→x≤y : ∀ {x y} -> suc x ≤ y -> x ≤ y
--       sucx≤y→x≤y {zero} sx≤y = z≤n
--       sucx≤y→x≤y {suc x} (s≤s sx≤y) = s≤s (sucx≤y→x≤y sx≤y)
--
-- open import Data.Sum
--
--
-- isLess→IsLess : ∀ {x xs} -> isLess x xs -> IsLess x xs
-- isLess→IsLess {x} {[]O} ⊤.tt = nil
-- isLess→IsLess {x} {x' ∷O xs} x< with x ≤'? x'
-- isLess→IsLess {.x'} {x' ∷O xs} () | yes ≤′-refl
-- isLess→IsLess {x} {(.(suc _) ∷O xs) {sn<}} ⊤.tt | yes (≤′-step {n = n} x≤′n) = {!sn<   !}
--   where
--     aux : x < suc n
--     aux = {! sn<  !}
--
--     rec : IsLess (suc n) xs
--     rec = isLess→IsLess sn<
--   --
--     aux₂ : IsLess x ((suc n ∷O xs) {sn<})
--     aux₂ = cons aux rec
--
-- isLess→IsLess {x} {x' ∷O xs} x< | no ¬p = {!   !}

mutual
  data OList : Set where
    []O : OList
    _∷O_ : (x : ℕ) -> (xs : OList) -> {x< : IsLess x xs} -> OList

  data IsLess : ℕ -> OList -> Set where
    base : ∀ {x} -> IsLess x []O
    step : ∀ {x x' xs} -> x < x' -> (x'<xs : IsLess x' xs) -> IsLess x ((x' ∷O xs) {x'<xs})

IsLess→< : ∀ {x x' xs x'<} -> IsLess x ((x' ∷O xs) {x'<}) -> x < x'
IsLess→< (step x<x' _) = x<x'

mutual
  insertO : ℕ -> OList -> OList
  insertO x []O = (x ∷O []O) {base}
  insertO x (x' ∷O xs) with x ≤'? x'
  insertO x ((.x ∷O xs) {x<}) | yes ≤′-refl = (x ∷O xs) {x<}
  insertO x ((.(suc _) ∷O xs) {x<}) | yes (≤′-step {n = x'} p) = (x ∷O (((suc x') ∷O xs) {x<})) {step (s≤s (≤′⇒≤ p)) x<}
  insertO x ((x' ∷O xs) {x'<}) | no x'<x = (x' ∷O insertO x xs) {insertO-lemma xs x'< x'<x}

  insertO-lemma : ∀ {x x'} xs -> IsLess x' xs -> ¬ x ≤′ x' -> IsLess x' (insertO x xs)
  insertO-lemma []O base ¬x≤′x' = step (≰⇒> (λ x≤x' → ¬x≤′x' (≤⇒≤′ x≤x'))) base
  insertO-lemma {x} {x'} (x'' ∷O xs) x'<xs x'<x with x ≤'? x''
  insertO-lemma {.x''} {x'} ((x'' ∷O xs) {x''<}) x'<xs _ | yes ≤′-refl = step (IsLess→< x'<xs) x''<
  insertO-lemma {x} {x'} ((.(suc _) ∷O xs) {sn<xs}) x'<xs ¬x≤′x' | yes (≤′-step x≤′n) =
    step (≰⇒> (λ x≤x' → ¬x≤′x' (≤⇒≤′ x≤x'))) (step (s≤s (≤′⇒≤ x≤′n)) sn<xs)
  insertO-lemma {x} {x'} ((x'' ∷O xs) {x''<xs}) x'<xs _ | no x''<x = step (IsLess→< x'<xs) (insertO-lemma {x} {x''} xs x''<xs x''<x)

data _∈O_ : ℕ -> OList -> Set where
  here : ∀ {x xs x<xs} -> x ∈O ((x ∷O xs) {x<xs})
  there : ∀ {x y xs y<xs} -> x ∈O xs -> x ∈O ((y ∷O xs) {y<xs})

_∉O_ : ℕ -> OList -> Set
x ∉O xs = ¬ (x ∈O xs)

IsLess-remove : ∀ {x x'} xs {x'<xs} -> IsLess x ((x' ∷O xs) {x'<xs}) -> IsLess x xs
IsLess-remove []O x<x∷xs = base
IsLess-remove ((x'' ∷O xs) {x''<xs}) (step x<x' x'<x''∷xs) = step (<-trans x<x' (IsLess→< x'<x''∷xs)) x''<xs

mutual
  removeO : ℕ -> OList -> OList
  removeO x []O = []O
  removeO x (x' ∷O xs) with x ≟ x'
  removeO x (.x ∷O xs) | yes refl = xs
  removeO x ((x' ∷O xs) {x'<xs}) | no ¬p = (x' ∷O removeO x xs) {removeO-lemma {x} {x'} xs x'<xs}

  removeO-lemma : ∀ {x x'} xs -> IsLess x' xs -> IsLess x' (removeO x xs)
  removeO-lemma []O x'<xs = base
  removeO-lemma {x} {x'} (x'' ∷O xs) x'<xs with x ≟ x''
  removeO-lemma {.x''} {x'} (x'' ∷O xs) x<xs | yes refl = IsLess-remove xs x<xs
  removeO-lemma {x} {x'} ((x'' ∷O xs) {x''<xs}) x'<xs | no ¬p = step (IsLess→< x'<xs) (removeO-lemma {x} {x''} xs x''<xs)

-- isLess : ℕ -> OList -> Set
-- isLess x []O = ⊤
-- isLess x (y ∷O ol) with x ≤'? y
-- isLess x (.x ∷O ol) | yes ≤′-refl = ⊥
-- isLess x (.(suc _) ∷O ol) | yes (≤′-step _) = ⊤
-- isLess x (y ∷O ol) | no _ = ⊥
--

-- smart constructor for OList
_∷O'_ : (x : ℕ) -> (xs : OList) -> OList
x ∷O' xs = insertO x xs

testOList : OList
testOList = 2 ∷O' (1 ∷O' (2 ∷O' []O))

data Formula' : OList → Set where
  -- _⟨_⟩ : Name → ∀ {xs} (ts : TTermList xs) → Formula xs
  _∧_ : ∀ {ns} → Formula' ns → Formula' ns → Formula' ns
  _∨_ : ∀ {ns} → Formula' ns → Formula' ns → Formula' ns
  _⟶_ : ∀ {ns} → Formula' ns → Formula' ns → Formula' ns
  ∘ : ∀ {ns} v → Formula' ns → {v∉ : v ∉O ns} → Formula' (insertO v ns)
  -- [_/_] : ∀ {y ns} → Term → (x : ℕ) → {x∈ : x ∈ ns} → {y⊆ : y ⊆ ns} → {x≠y : [ x ] ≢ y} → Formula ns → Formula (remove x ns)
  -- [_//_] : ∀ {y ns} → Term y → (x : ℕ) → {x⊆ : x ∈ ns} → {y⊈ : y ⊈ ns} → {x≠y : [ x ] ≢ y} → Formula ns → Formula (union y (remove x ns))
  All : ∀ {ns} v → Formula' ns → Formula' (removeO v ns)
  Ex : ∀ {ns} v → Formula' ns → Formula' (removeO v ns)

-- insert-reomve-id : ∀ {x n m} -> n ≡ m -> n ≡ insertO x (removeO x m)
-- insert-reomve-id {x} {xs} refl = {! xs  !}

rem-inj : ∀ {n m} x -> n ≡ m -> remove x n ≡ remove x m
rem-inj _ refl = refl

data _⊢⟨_⟩_ : ∀ {n m} → Structure n → n ≡ m -> Structure m → Set where
  atom : ∀ {n xs n≡m} {ts us : TTermList xs} →
    ∣ n ⟨ ts ⟩ ∣ ⊢⟨ n≡m ⟩ ∣ n ⟨ us ⟩ ∣
  allR : ∀ {x n m n≡m X} {Y : Structure m} →
    Y ⊢⟨ n≡m ⟩ Q {n} x ∣ X ∣ →
    -------------------
    Y ⊢⟨ n≡m ⟩ ∣ All {n} x X ∣
  allL : ∀ {x n m n≡m X} {Y : Formula m} →
            ∣ X ∣ ⊢⟨ n≡m ⟩ ∣ Y ∣ →
    -------------------------------
    ∣ All {n} x X ∣ ⊢⟨ rem-inj x n≡m ⟩ Q {m} x ∣ Y ∣
  IL : ∀ {n m n≡m} {X : Structure n} {Y : Structure m} →
       X ⊢⟨ n≡m ⟩ Y →
    -------------------
    (I , X) {refl} ⊢⟨ n≡m ⟩ Y
  IL2 : ∀ {n m n≡m} {X : Structure n} {Y : Structure m} →
    (I , X) {refl} ⊢⟨ n≡m ⟩ Y →
    -------------------
       X ⊢⟨ n≡m ⟩ Y
  IR : ∀ {n m n≡m} {X : Structure n} {Y : Structure m} →
      X ⊢⟨ n≡m ⟩ Y →
   -----------------
   X ⊢⟨ n≡m ⟩ (Y , I) {refl}
  IR2 : ∀ {n m n≡m} {X : Structure n} {Y : Structure m} →
    X ⊢⟨ n≡m ⟩ (Y , I) {refl} →
    -----------------
    X ⊢⟨ n≡m ⟩ Y

  ,>>disp : ∀ {n m n≡m} {Z : Structure n} {X Y : Structure m} →
    Z ⊢⟨ n≡m ⟩ (X , Y) {refl} →
    -----------------
    (X >> Z) {sym n≡m} ⊢⟨ refl ⟩ Y
  ,>>disp2 : ∀ {n m n≡m} {Z : Structure n} {X Y : Structure m} →
    (X >> Z) {sym n≡m} ⊢⟨ refl ⟩ Y →
    -----------------
    Z ⊢⟨ n≡m ⟩ (X , Y) {refl}
  ○IR : ∀ {x n m n≡m x∉m} {X : Structure n} →
    X ⊢⟨ n≡m ⟩ (I {insert x m}) →
    -----------------
    X ⊢⟨ n≡m ⟩ ○ x (I {m}) {x∉m}
  ○IR2 : ∀ {x n m n≡m x∉m} {X : Structure n} →
    X ⊢⟨ n≡m ⟩ ○ x (I {m}) {x∉m}  →
    -----------------
    X ⊢⟨ n≡m ⟩ (I {insert x m})
  -- ,<<disp : ∀ {n m n≡m} {X : Structure n} {Y Z : Structure m} →
  --   X ⊢⟨ n≡m ⟩ (Y , Z) {refl} →
  --   -----------------
  --   (X >> Z) {n≡m} ⊢⟨ n≡m ⟩ Y
  -- ,<<disp2 : ∀ {n m n≡m} {X : Structure n} {Y Z : Structure m} →
  --   (X >> Z) {n≡m} ⊢⟨ n≡m ⟩ Y →
  --   -----------------
  --   X ⊢⟨ n≡m ⟩ (Y , Z) {refl}
rem-union-id : ∀ x -> remove x (union [ x ] []) ≡ []
rem-union-id x rewrite remove-rewrite x {[]} = refl

test : ∀ x y {n} -> ∣ All x (n ⟨ (TVar x) ∷T []T ⟩) ∣ ⊢⟨ PropEq.trans (rem-union-id x) (sym (rem-union-id y)) ⟩ ∣ All y (n ⟨ (TVar y) ∷T []T ⟩) ∣
test x y = allR ?

data Map : List ℕ → Set where
  nil : Map []
  _/_:::_ : ∀ {xs} (x : ℕ) → String → Map xs → Map (x ∷ xs)

_!!_ : List (ℕ × String) → ℕ → String
[] !! _ = "not found"
((x , s) ∷ m) !! y with x ≟ y
... | yes _ = s
... | no _ = m !! y

Term→Str : List (ℕ × String) → Term → String
Term→Str m (Var x) = "\\textit{" ++ (m !! x) ++ "}"
Term→Str m (Const s) = "\\textbf{" ++ s ++ "}"
Term→Str m (Fun n args) = "" --"\\textbf{" ++ s ++ "}"
-- Term→Str m ([[_/_]]_ _ _ _) = "" --"\\textbf{" ++ s ++ "}"
Term→Str m ([[[_]]]_ _ _) = ""

Formula→Str : ∀ {xs} → List (ℕ × String) → Formula xs → String
Formula→Str m (n ⟨ args ⟩) = n ++ "(" ++ ")" --aux args ++ ")"
  -- where
  -- aux : List Term → String
  -- aux [] = ""
  -- aux (x ∷ []) = Term→Str m x
  -- aux (x ∷ (y ∷ args)) = Term→Str m x ++ ", " ++ aux (y ∷ args)
Formula→Str m (f ∧ f₁) = Formula→Str m f ++ " \\land " ++ Formula→Str m f₁
Formula→Str m (f ∨ f₁) = Formula→Str m f ++ " \\lor " ++ Formula→Str m f₁
Formula→Str m (f ⟶ f₁) = Formula→Str m f ++ " \\leftarrow " ++ Formula→Str m f₁
Formula→Str m (∘ v f) = "\\circ_" ++ (m !! v) ++ Formula→Str m f
-- Formula→Str m ([ y / x ] f) = "(" ++ Term→Str m y ++ "/" ++ (m !! x) ++ ") " ++ Formula→Str m f
-- Formula→Str m ([ y // x ] f) = "(" ++ Term→Str m y ++ "//" ++ (m !! x) ++ ") " ++ Formula→Str m f
Formula→Str m (All v f) = "\\forall " ++ (m !! v) ++ Formula→Str m f
Formula→Str m (Ex v f) = "\\exists " ++ (m !! v) ++ Formula→Str m f

Structure→Str : ∀ {xs} → List (ℕ × String) → Structure xs → String
Structure→Str m ∣ x ∣ = Formula→Str m x
Structure→Str m (s , s₁) = Structure→Str m s ++ " , " ++ Structure→Str m s₁
Structure→Str m (s >> s₁) = Structure→Str m s ++ " >> " ++ Structure→Str m s₁
Structure→Str m (s << s₁) = Structure→Str m s ++ " << " ++ Structure→Str m s₁
Structure→Str m I = "I"
Structure→Str m (○ v s) = "\\bigcirc_" ++ (m !! v) ++ Structure→Str m s
Structure→Str m (Q v s) = "Q " ++ (m !! v) ++ Structure→Str m s

⊢concl : ∀ {n} {xs ys : Structure n} → xs ⊢ ys → (Structure n × Structure n)
⊢concl {_} {xs} {ys} _ = xs , ys

data ⊢List : Set where
  ⊢nil : ⊢List
  _⊢::_ : ∀ {n} {xs ys : Structure n} → xs ⊢ ys → ⊢List → ⊢List

⊢prems : ∀ {n} {xs ys : Structure n} → xs ⊢ ys → ⊢List
⊢prems atom = ⊢nil
⊢prems (allR xs⊢ys) = xs⊢ys ⊢:: ⊢nil
⊢prems (allL xs⊢ys) = xs⊢ys ⊢:: ⊢nil

-- proof1 : ∀ {n} P (args : TList n) → ∣ P ⟨ args ⟩ ∣ ⊢ ∣ P ⟨ args ⟩ ∣
-- proof1 P args = atom
--
-- proof : ∣ "P" ⟨ Var 0 ::: nil ⟩ ∣ ⊢ ∣ "P" ⟨ Var 0 ::: nil ⟩ ∣
-- proof = let (x , y) = ⊢concl (proof1 "P"  (Var 0 ::: nil)) in {!Structure→Str [ (0 , "x") ] x  !}

⊢→Str' : ∀ {n} {xs ys : Structure n} → List (ℕ × String) → xs ⊢ ys → String
⊢→Str' m xs⊢ys with ⊢concl xs⊢ys | ⊢prems xs⊢ys
⊢→Str' m xs⊢ys | xs , ys | prems = Structure→Str m xs ++ " \\vdash " ++ Structure→Str m ys
  where
    prems→Str : ⊢List → String
    prems→Str ⊢nil = ""
    prems→Str (x ⊢:: lst) = {!   !}

open import IO

main = run (putStrLn "Hello, world!")

max_stars_repo_name: goodlyrottenapple/FOLdisplay

max_issues_repo_name: goodlyrottenapple/FOLdisplay

max_forks_repo_name: goodlyrottenapple/FOLdisplay


text:
import Algebra
import Algebra.Structures
import Function.Equality
import Function.Equivalence
import Function.Bijection
import Level
import Relation.Binary
import Algebra.FunctionProperties
import Relation.Binary.EqReasoning

open Level renaming (zero to ₀)
open Relation.Binary using (Setoid; module Setoid)
open Function.Bijection

module Algebra.Lifting
  (S₁ S₂ : Setoid ₀ ₀)
  (f : Bijection S₁ S₂) where

  open Algebra.FunctionProperties using (Op₂; LeftIdentity)
  open Algebra.Structures

  open Setoid S₁ using () renaming (Carrier to A₁; _≈_ to _≈₁_; sym to sym₁; refl to refl₁; trans to trans₁)
  open Setoid S₂ using (sym; trans) renaming (Carrier to A₂; _≈_ to _≈₂_; isEquivalence to isEquivalence₂)
  open Bijection f
  open Function.Equality using (_⟨$⟩_; cong)
  module WithOp₂
   (_+₁_ : Op₂ A₁)
   (_+₂_ : Op₂ A₂)
   (+-same : ∀ x y → from ⟨$⟩ (x +₂ y) ≈₁ (from ⟨$⟩ x) +₁ (from ⟨$⟩ y)) where

   open Relation.Binary.EqReasoning S₁ renaming (begin_ to begin₁_; _∎ to _∎₁; _≈⟨_⟩_ to _≈₁⟨_⟩_)
   open Relation.Binary.EqReasoning S₂ renaming (begin_ to begin₂_; _∎ to _∎₂; _≈⟨_⟩_ to _≈₂⟨_⟩_)

   open import Function using (_⟨_⟩_)

   from-inj : ∀ {x y} → from ⟨$⟩ x ≈₁ from ⟨$⟩ y → x ≈₂ y
   from-inj {x} {y} eq = (sym (right-inverse-of x)) ⟨ trans ⟩ cong to eq ⟨ trans ⟩ (right-inverse-of y)

   lift-comm : (∀ x y → (x +₁ y) ≈₁ (y +₁ x)) → (∀ x y → (x +₂ y) ≈₂ (y +₂ x))
   lift-comm comm₁ x y = from-inj (
       begin₁
          from ⟨$⟩ x +₂ y
           ≈₁⟨ +-same x y ⟩
          (from ⟨$⟩ x) +₁ (from ⟨$⟩ y)
           ≈₁⟨ comm₁ (from ⟨$⟩ x) (from ⟨$⟩ y) ⟩
          (from ⟨$⟩ y) +₁ (from ⟨$⟩ x)
           ≈₁⟨ sym₁ (+-same y x) ⟩
          from ⟨$⟩ y +₂ x
       ∎₁
      )

   using-+-same : ∀ {a b c d}
                  → (from ⟨$⟩ a) +₁ (from ⟨$⟩ b) ≈₁ (from ⟨$⟩ c) +₁ (from ⟨$⟩ d)
                  → from ⟨$⟩ a +₂ b ≈₁ from ⟨$⟩ c +₂ d
   using-+-same {a} {b} {c} {d} eq =
    begin₁
     from ⟨$⟩ a +₂ b
      ≈₁⟨ +-same a b ⟩
     (from ⟨$⟩ a) +₁ (from ⟨$⟩ b)
      ≈₁⟨ eq ⟩
     (from ⟨$⟩ c) +₁ (from ⟨$⟩ d)
      ≈₁⟨ sym₁ (+-same c d) ⟩
     from ⟨$⟩ c +₂ d
    ∎₁

   lift-comm' : (∀ x y → (x +₁ y) ≈₁ (y +₁ x)) → (∀ x y → (x +₂ y) ≈₂ (y +₂ x))
   lift-comm' comm₁ x y = from-inj (using-+-same (comm₁ (from ⟨$⟩ x) (from ⟨$⟩ y)))

   lift-assoc : (∀ x y z → (x +₁ y) +₁ z ≈₁ x +₁ (y +₁ z))
              → (∀ {a b c d} → a ≈₁ b → c ≈₁ d → a +₁ c ≈₁ b +₁ d)
              → (∀ x y z → (x +₂ y) +₂ z ≈₂ x +₂ (y +₂ z))
   lift-assoc assoc₁ +₁-cong x y z = from-inj (using-+-same (
    begin₁
      (from ⟨$⟩ x +₂ y) +₁ fz
       ≈₁⟨ +₁-cong (+-same x y) refl₁ ⟩
      (fx +₁ fy) +₁ fz
       ≈₁⟨ assoc₁ fx fy fz ⟩
      fx +₁ (fy +₁ fz)
       ≈₁⟨ +₁-cong  refl₁ (sym₁ (+-same y z)) ⟩
      fx +₁ (from ⟨$⟩ y +₂ z)
    ∎₁)) where
     fx = from ⟨$⟩ x
     fy = from ⟨$⟩ y
     fz = from ⟨$⟩ z

   +Cong₁ = (∀ {a b c d} → a ≈₁ b → c ≈₁ d → a +₁ c ≈₁ b +₁ d)
   +Cong₂ = (∀ {a b c d} → a ≈₂ b → c ≈₂ d → a +₂ c ≈₂ b +₂ d)

   lift-cong : +Cong₁ → +Cong₂
   lift-cong cong₁ a≈₂b c≈₂d = from-inj (using-+-same (cong₁ (cong from  a≈₂b) (cong from  c≈₂d)))

   lift-isSemigroup : IsSemigroup _≈₁_ _+₁_ → IsSemigroup _≈₂_ _+₂_
   lift-isSemigroup isSemigroup = record
     { isEquivalence = isEquivalence₂
     ; assoc = lift-assoc assoc ∙-cong
     ; ∙-cong = lift-cong ∙-cong
     } where
    open IsSemigroup isSemigroup

   lift-LeftIdentity : ∀ ε → +Cong₁ → LeftIdentity _≈₁_ ε _+₁_ → LeftIdentity _≈₂_ (to ⟨$⟩ ε) _+₂_
   lift-LeftIdentity ε +-cong₁ identityˡ x = from-inj (
    begin₁
     from ⟨$⟩ (to ⟨$⟩ ε) +₂ x
      ≈₁⟨ +-same (to ⟨$⟩ ε) x ⟩
     (from ⟨$⟩ (to ⟨$⟩ ε)) +₁ (from ⟨$⟩ x)
      ≈₁⟨ +-cong₁ (left-inverse-of ε) refl₁ ⟩
     ε +₁ (from ⟨$⟩ x)
      ≈₁⟨ identityˡ (from ⟨$⟩ x) ⟩
     from ⟨$⟩ x
    ∎₁)

   lift-isCommutativeMonoid : ∀ ε → IsCommutativeMonoid _≈₁_ _+₁_ ε → IsCommutativeMonoid _≈₂_ _+₂_ (to ⟨$⟩ ε)
   lift-isCommutativeMonoid ε isCommMonoid = record
     { isSemigroup = lift-isSemigroup isSemigroup
     ; identityˡ = lift-LeftIdentity ε ∙-cong identityˡ
     ; comm = lift-comm comm
     } where
    open IsCommutativeMonoid isCommMonoid

ext: agda

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
{-# OPTIONS --erased-cubical #-}

module Main where

open import Data.List using (map)
open import Data.Unit using (⊤)

open import Midi      using (IO; _>>=_; getArgs; putStrLn; exportTracks; track→htrack)

open import FarmCanon using (canonTracks)
open import FarmFugue using (fugueTracks)

-- TODO: Remove
open import Data.List using (List; []; _∷_)
open import Data.String using (String)
open import Function using (_∘_)
open import Midi using (readNat)
open import Pitch using (toPC; showPC)
open import Agda.Builtin.Nat using (zero; suc)
process : List String → String
process []       = ""
process (x ∷ xs) with readNat x
... | zero  = ""
... | suc n = (showPC ∘ toPC) n

main : IO ⊤
main = do
  args ← getArgs
  (putStrLn ∘ process) args

main' : IO ⊤
main' =
  let ticksPerBeat = 4 -- (1 = quarter notes; 4 = 16th notes)
      file         = "/Users/leo/Music/MusicTools/test.mid"
      song         = fugueTracks
  in exportTracks file ticksPerBeat (map track→htrack song)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module MoreLogic.Reasoning where -- hProp logic

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)

-- "implicational" reaoning

-- infix  3 _◼ᵖ
-- infixr 2 _⇒ᵖ⟨_⟩_
--
-- _⇒ᵖ⟨_⟩_ : ∀{ℓ ℓ' ℓ''} {Q : hProp ℓ'} {R : hProp ℓ''} → (P : hProp ℓ) → [ P ⇒ Q ] → [ Q ⇒ R ] → [ P ⇒ R ]
-- _ ⇒ᵖ⟨ pq ⟩ qr = qr ∘ pq
--
-- _◼ᵖ : ∀{ℓ} (A : hProp ℓ) → [ A ] → [ A ]
-- _ ◼ᵖ = λ x → x

infix  3 _◼
infixr 2 _⇒⟨_⟩_

infix  3 _◼ᵖ
infixr 2 ⇒ᵖ⟨⟩-syntax -- _⇒ᵖ⟨_⟩_

infix  3 _∎ᵖ
infixr 2 ⇔⟨⟩-syntax -- _⇔⟨_⟩_

⇔⟨⟩-syntax : ∀{ℓ ℓ' ℓ''} → (P : hProp ℓ'') → (((Q , R) , _) : Σ[ (Q , R) ∈ hProp ℓ' × hProp ℓ ] [ Q ⇔ R ]) → [ P ⇔ Q ] → Σ[ (P , R) ∈ hProp ℓ'' × hProp ℓ ] [ P ⇔ R ]
⇔⟨⟩-syntax P ((Q , R) , q⇔r) p⇔q .fst = P , R -- x⇔y ∙ y⇔z
⇔⟨⟩-syntax P ((Q , R) , q⇔r) p⇔q .snd .fst = fst q⇔r ∘ fst p⇔q
⇔⟨⟩-syntax P ((Q , R) , q⇔r) p⇔q .snd .snd = snd p⇔q ∘ snd q⇔r

syntax ⇔⟨⟩-syntax P QRq⇔r p⇔q = P ⇔⟨ p⇔q ⟩ QRq⇔r

_∎ᵖ : ∀{ℓ} → (P : hProp ℓ) → Σ[ (Q , R) ∈ hProp ℓ × hProp ℓ ] [ Q ⇔ R ]
_∎ᵖ P .fst        = P , P
_∎ᵖ P .snd .fst x = x
_∎ᵖ P .snd .snd x = x

⇒ᵖ⟨⟩-syntax : ∀{ℓ ℓ' ℓ''} → (P : hProp ℓ'') → (((Q , R) , _) : Σ[ (Q , R) ∈ hProp ℓ' × hProp ℓ ] [ Q ⇒ R ]) → [ P ⇒ Q ] → Σ[ (P , R) ∈ hProp ℓ'' × hProp ℓ ] [ P ⇒ R ]
⇒ᵖ⟨⟩-syntax P ((Q , R) , q⇔r) p⇔q .fst = P , R -- x⇔y ∙ y⇔z
⇒ᵖ⟨⟩-syntax P ((Q , R) , q⇒r) p⇒q .snd = q⇒r ∘ p⇒q

_◼ᵖ : ∀{ℓ} → (P : hProp ℓ) → Σ[ (Q , R) ∈ hProp ℓ × hProp ℓ ] [ Q ⇒ R ]
_◼ᵖ P .fst   = P , P
_◼ᵖ P .snd x = x

syntax ⇒ᵖ⟨⟩-syntax P QRq⇒r p⇒q = P ⇒ᵖ⟨ p⇒q ⟩ QRq⇒r

_⇒⟨_⟩_ : ∀{ℓ ℓ' ℓ''} {Q : Type ℓ'} {R : Type ℓ''} → (P : Type ℓ) → (P → Q) → (Q → R) → (P → R)
_ ⇒⟨ p⇒q ⟩ q⇒r = q⇒r ∘ p⇒q

_◼ : ∀{ℓ} (A : Type ℓ) → A → A
_ ◼ = λ x → x

-- ⊎⇒⊔ : ∀ {ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ') → [ P ] ⊎ [ Q ] → [ P ⊔ Q ]
-- ⊎⇒⊔ P Q (inl x) = inlᵖ x
-- ⊎⇒⊔ P Q (inr x) = inrᵖ x
--
-- case[_⊔_]_return_of_ : ∀ {ℓ ℓ'} (P : hProp ℓ) (Q : hProp ℓ')
--                   → (z : [ P ⊔ Q ])
--                   → (R : [ P ⊔ Q ] → hProp ℓ'')
--                   → (S : (x : [ P ] ⊎ [ Q ]) → [ R (⊎⇒⊔ P Q x) ] )
--                   → [ R z ]
-- case[_⊔_]_return_of_ P Q z R S = ⊔-elim P Q R (λ p → S (inl p)) (λ q → S (inr q)) z

{- NOTE: in the CHANGELOG.md of the v1.3 non-cubical standard library, it is explained:

* Previously all equational reasoning combinators (e.g. `_≈⟨_⟩_`, `_≡⟨_⟩_`, `_≤⟨_⟩_`)
  were defined in the following style:
  ```agda
  infixr 2 _≡⟨_⟩_

  _≡⟨_⟩_ : ∀ x {y z : A} → x ≡ y → y ≡ z → x ≡ z
  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
  ```
  The type checker therefore infers the RHS of the equational step from the LHS + the
  type of the proof. For example for `x ≈⟨ x≈y ⟩ y ∎` it is inferred that `y ∎`
  must have type `y IsRelatedTo y` from `x : A` and `x≈y : x ≈ y`.

* There are two problems with this. Firstly, it means that the reasoning combinators are
  not compatible with macros (i.e. tactics) that attempt to automatically generate proofs
  for `x≈y`. This is because the reflection machinary does not have access to the type of RHS
  as it cannot be inferred. In practice this meant that the new reflective solvers
  `Tactic.RingSolver` and `Tactic.MonoidSolver` could not be used inside the equational
  reasoning. Secondly the inference procedure itself is slower as described in this
  [exchange](https://lists.chalmers.se/pipermail/agda/2016/009090.html)
  on the Agda mailing list.

* Therefore, as suggested on the mailing list, the order of arguments to the combinators
  have been reversed so that instead the type of the proof is inferred from the LHS + RHS.
  ```agda
  infixr -2 step-≡

  step-≡ : ∀ x {y z : A} → y ≡ z → x ≡ y → x ≡ z
  step-≡ y≡z x≡y = trans x≡y y≡z

  syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
  ```
  where the `syntax` declaration is then used to recover the original order of the arguments.
  This change enables the use of macros and anecdotally speeds up type checking by a
  factor of 5.

-} -- TODO: that might be "correct" the way to implement these reasoning operators

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
-- Mixing CatchAll branches with varying arity can be tricky.
--
-- If the number of arguments a catch all branch expects to be already abstracted over is smaller
-- than the number of arguments present in the failing clause/branch, we need to apply
-- the catch-all branch to the surplus arguments already abstracted over.

module CatchAllVarArity where

open import Common.Nat
open import Common.IO
open import Common.Unit

f : Nat → Nat → Nat
f zero = λ y → y
f (suc zero) (suc y) = suc y
f x y = (suc y)

case_of_ : ∀{A B : Set} → A → (A → B) → B
case a of f = f a

-- case tree variant of f
g : Nat → Nat → Nat
g = λ x →
    case x of
     λ{ zero     → λ y → y
      ; (suc x') →
        case x' of
         λ{ zero  → λ y →
            case y of
             λ{ (suc y') → suc y'
              ; _        → fallback (suc x') y
              }
          ; _ → λ y → fallback x y
          }
      }
  where
    fallback = λ x y → suc y

--expected:
-- 10
-- 21
-- 1
-- 0
-- 4
-- 1
main = printNat (f 0 10) ,,
  putStrLn "" ,,
  printNat (f 10 20) ,,
  putStrLn "" ,,
  printNat (f 10 0) ,,
  putStrLn "" ,,
  printNat (f 0 0) ,,
  putStrLn "" ,,
  printNat (f 1 4) ,,
  putStrLn "" ,,
  printNat (f 1 0) ,,
  putStrLn ""

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module NF.Nat where

open import NF
open import Relation.Binary.PropositionalEquality
open import Data.Nat

instance
  nf0 : NF 0
  Sing.unpack (NF.!! nf0) = 0
  Sing.eq (NF.!! nf0) = refl

  {-# INLINE nf0 #-}

  nfSuc : {n : ℕ}{{nfn : NF n}} -> NF (suc n)
  Sing.unpack (NF.!! (nfSuc {n})) = suc (nf n)
  Sing.eq (NF.!! (nfSuc {{nfn}})) = cong suc nf≡

  {-# INLINE nfSuc #-}

max_stars_repo_name: yanok/normalize-via-instances

max_issues_repo_name: yanok/normalize-via-instances

max_forks_repo_name: yanok/normalize-via-instances


text:
module STLC.Coquand.Renaming where

open import STLC.Syntax public
open import Category

--------------------------------------------------------------------------------

-- Renamings
infix 4 _∋⋆_
data _∋⋆_ : 𝒞 → 𝒞 → Set
  where
    ∅   : ∀ {Γ} → Γ ∋⋆ ∅

    _,_ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ) (i : Γ′ ∋ A)
                     → Γ′ ∋⋆ Γ , A

putᵣ : ∀ {Γ Γ′} → (∀ {A} → Γ ∋ A → Γ′ ∋ A) → Γ′ ∋⋆ Γ
putᵣ {∅}     f = ∅
putᵣ {Γ , A} f = putᵣ (λ i → f (suc i)) , f 0

getᵣ : ∀ {Γ Γ′ A} → Γ′ ∋⋆ Γ → Γ ∋ A → Γ′ ∋ A
getᵣ (η , i) zero    = i
getᵣ (η , i) (suc j) = getᵣ η j

wkᵣ : ∀ {A Γ Γ′} → Γ′ ∋⋆ Γ → Γ′ , A ∋⋆ Γ
wkᵣ ∅       = ∅
wkᵣ (η , i) = wkᵣ η , suc i

liftᵣ : ∀ {A Γ Γ′} → Γ′ ∋⋆ Γ → Γ′ , A ∋⋆ Γ , A
liftᵣ η = wkᵣ η , 0

idᵣ : ∀ {Γ} → Γ ∋⋆ Γ
idᵣ {∅}     = ∅
idᵣ {Γ , A} = liftᵣ idᵣ

ren : ∀ {Γ Γ′ A} → Γ′ ∋⋆ Γ → Γ ⊢ A → Γ′ ⊢ A
ren η (𝓋 i)   = 𝓋 (getᵣ η i)
ren η (ƛ M)   = ƛ (ren (liftᵣ η) M)
ren η (M ∙ N) = ren η M ∙ ren η N

wk : ∀ {B Γ A} → Γ ⊢ A → Γ , B ⊢ A
wk M = ren (wkᵣ idᵣ) M

-- NOTE: _○_ = getᵣ⋆
_○_ : ∀ {Γ Γ′ Γ″} → Γ″ ∋⋆ Γ′ → Γ′ ∋⋆ Γ → Γ″ ∋⋆ Γ
η₁ ○ ∅        = ∅
η₁ ○ (η₂ , i) = η₁ ○ η₂ , getᵣ η₁ i

--------------------------------------------------------------------------------

-- (wkgetᵣ)
natgetᵣ : ∀ {Γ Γ′ A B} → (η : Γ′ ∋⋆ Γ) (i : Γ ∋ A)
                       → getᵣ (wkᵣ {B} η) i ≡ (suc ∘ getᵣ η) i
natgetᵣ (η , j) zero    = refl
natgetᵣ (η , j) (suc i) = natgetᵣ η i

idgetᵣ : ∀ {Γ A} → (i : Γ ∋ A)
                 → getᵣ idᵣ i ≡ i
idgetᵣ zero    = refl
idgetᵣ (suc i) = natgetᵣ idᵣ i
               ⦙ suc & idgetᵣ i

idren : ∀ {Γ A} → (M : Γ ⊢ A)
                → ren idᵣ M ≡ M
idren (𝓋 i)   = 𝓋 & idgetᵣ i
idren (ƛ M)   = ƛ & idren M
idren (M ∙ N) = _∙_ & idren M
                    ⊗ idren N

--------------------------------------------------------------------------------

zap○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ) (i : Γ″ ∋ A)
                     → (η₁ , i) ○ wkᵣ η₂ ≡ η₁ ○ η₂
zap○ η₁ ∅        i = refl
zap○ η₁ (η₂ , j) i = (_, getᵣ η₁ j) & zap○ η₁ η₂ i

lid○ : ∀ {Γ Γ′} → (η : Γ′ ∋⋆ Γ)
                → idᵣ ○ η ≡ η
lid○ ∅       = refl
lid○ (η , i) = _,_ & lid○ η
                   ⊗ idgetᵣ i

rid○ : ∀ {Γ Γ′} → (η : Γ′ ∋⋆ Γ)
                → η ○ idᵣ ≡ η
rid○ {∅}     ∅       = refl
rid○ {Γ , A} (η , i) = (_, i) & ( zap○ η idᵣ i
                                ⦙ rid○ η
                                )

--------------------------------------------------------------------------------

get○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ) (i : Γ ∋ A)
                     → getᵣ (η₁ ○ η₂) i ≡ (getᵣ η₁ ∘ getᵣ η₂) i
get○ η₁ (η₂ , j) zero    = refl
get○ η₁ (η₂ , j) (suc i) = get○ η₁ η₂ i

wk○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ)
                    → wkᵣ {A} (η₁ ○ η₂) ≡ wkᵣ η₁ ○ η₂
wk○ η₁ ∅        = refl
wk○ η₁ (η₂ , i) = _,_ & wk○ η₁ η₂
                      ⊗ (natgetᵣ η₁ i ⁻¹)

lift○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ)
                      → liftᵣ {A} (η₁ ○ η₂) ≡ liftᵣ η₁ ○ liftᵣ η₂
lift○ η₁ η₂ = (_, 0) & ( wk○ η₁ η₂
                          ⦙ (zap○ (wkᵣ η₁) η₂ 0 ⁻¹)
                          )

wklid○ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ)
                    → wkᵣ {A} idᵣ ○ η ≡ wkᵣ η
wklid○ η = wk○ idᵣ η ⁻¹
         ⦙ wkᵣ & lid○ η

wkrid○ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ)
                    → wkᵣ {A} η ○ idᵣ ≡ wkᵣ η
wkrid○ η = wk○ η idᵣ ⁻¹
         ⦙ wkᵣ & rid○ η

liftwkrid○ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ)
                        → liftᵣ {A} η ○ wkᵣ idᵣ ≡ wkᵣ η
liftwkrid○ η = zap○ (wkᵣ η) idᵣ 0 ⦙ wkrid○ η

mutual
  ren○ : ∀ {Γ Γ′ Γ″ A} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ) (M : Γ ⊢ A)
                       → ren (η₁ ○ η₂) M ≡ (ren η₁ ∘ ren η₂) M
  ren○ η₁ η₂ (𝓋 i)   = 𝓋 & get○ η₁ η₂ i
  ren○ η₁ η₂ (ƛ M)   = ƛ & renlift○ η₁ η₂ M
  ren○ η₁ η₂ (M ∙ N) = _∙_ & ren○ η₁ η₂ M
                           ⊗ ren○ η₁ η₂ N

  renlift○ : ∀ {Γ Γ′ Γ″ A B} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ) (M : Γ , B ⊢ A)
                             → ren (liftᵣ {B} (η₁ ○ η₂)) M ≡
                                (ren (liftᵣ η₁) ∘ ren (liftᵣ η₂)) M
  renlift○ η₁ η₂ M = (λ η′ → ren η′ M) & lift○ η₁ η₂
                   ⦙ ren○ (liftᵣ η₁) (liftᵣ η₂) M

renwk○ : ∀ {Γ Γ′ Γ″ A B} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ) (M : Γ ⊢ A)
                         → ren (wkᵣ {B} (η₁ ○ η₂)) M ≡
                            (ren (wkᵣ η₁) ∘ ren η₂) M
renwk○ η₁ η₂ M = (λ η′ → ren η′ M) & wk○ η₁ η₂
               ⦙ ren○ (wkᵣ η₁) η₂ M

renliftwk○ : ∀ {Γ Γ′ Γ″ A B} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ) (M : Γ ⊢ A)
                             → ren (wkᵣ {B} (η₁ ○ η₂)) M ≡
                                (ren (liftᵣ η₁) ∘ ren (wkᵣ η₂)) M
renliftwk○ η₁ η₂ M = (λ η′ → ren η′ M) & ( wk○ η₁ η₂
                                          ⦙ zap○ (wkᵣ η₁) η₂ 0 ⁻¹
                                          )
                   ⦙ ren○ (liftᵣ η₁) (wkᵣ η₂) M

--------------------------------------------------------------------------------

assoc○ : ∀ {Γ Γ′ Γ″ Γ‴} → (η₁ : Γ‴ ∋⋆ Γ″) (η₂ : Γ″ ∋⋆ Γ′) (η₃ : Γ′ ∋⋆ Γ)
                        → η₁ ○ (η₂ ○ η₃) ≡ (η₁ ○ η₂) ○ η₃
assoc○ η₁ η₂ ∅        = refl
assoc○ η₁ η₂ (η₃ , i) = _,_ & assoc○ η₁ η₂ η₃
                            ⊗ (get○ η₁ η₂ i ⁻¹)

--------------------------------------------------------------------------------

𝗥𝗲𝗻 : Category 𝒞 _∋⋆_
𝗥𝗲𝗻 =
  record
    { idₓ    = idᵣ
    ; _⋄_    = flip _○_
    ; lid⋄   = rid○
    ; rid⋄   = lid○
    ; assoc⋄ = assoc○
    }

getᵣPsh : 𝒯 → Presheaf₀ 𝗥𝗲𝗻
getᵣPsh A =
  record
    { Fₓ  = _∋ A
    ; F   = getᵣ
    ; idF = fext! idgetᵣ
    ; F⋄  = λ η₂ η₁ → fext! (get○ η₁ η₂)
    }

renPsh : 𝒯 → Presheaf₀ 𝗥𝗲𝗻
renPsh A =
  record
    { Fₓ  = _⊢ A
    ; F   = ren
    ; idF = fext! idren
    ; F⋄  = λ η₂ η₁ → fext! (ren○ η₁ η₂)
    }

--------------------------------------------------------------------------------

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
------------------------------------------------------------------------
-- An investigation of nested fixpoints of the form μX.νY.… in Agda
------------------------------------------------------------------------

module MuNu where

open import Codata.Musical.Notation
import Codata.Musical.Colist as Colist
open import Codata.Musical.Stream
open import Data.Digit
open import Data.Empty
open import Data.List using (List; _∷_; [])
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)

-- Christophe Raffalli discusses (essentially) the type μO. νZ. Z + O
-- in his thesis. If Z is read as zero and O as one, then this type
-- contains bit sequences of the form (0^⋆1)^⋆0^ω.

-- It is interesting to note that currently it is not possible to
-- encode this type directly in Agda. One might believe that the
-- following definition should work. First we define the inner
-- greatest fixpoint:

data Z (O : Set) : Set where
  [0] : ∞ (Z O) → Z O
  [1] :    O    → Z O

-- Then we define the outer least fixpoint:

data O : Set where
  ↓ : Z O → O

-- However, it is still possible to define values of the form (01)^ω:

01^ω : O
01^ω = ↓ ([0] (♯ [1] 01^ω))

-- The reason is the way the termination/productivity checker works:
-- it accepts definitions by guarded corecursion as long as the guard
-- contains at least one occurrence of ♯_, no matter how the types
-- involved are defined. In effect ∞ has global reach. The mistake
-- done above was believing that O is defined to be a least fixpoint.
-- The type O really corresponds to νZ. μO. Z + O, i.e. (1^⋆0)^ω:

data O′ : Set where
  [0] : ∞ O′ → O′
  [1] :   O′ → O′

mutual

  O→O′ : O → O′
  O→O′ (↓ z) = ZO→O′ z

  ZO→O′ : Z O → O′
  ZO→O′ ([0] z) = [0] (♯ ZO→O′ (♭ z))
  ZO→O′ ([1] o) = [1] (O→O′ o)

mutual

  O′→O : O′ → O
  O′→O o = ↓ (O′→ZO o)

  O′→ZO : O′ → Z O
  O′→ZO ([0] o) = [0] (♯ O′→ZO (♭ o))
  O′→ZO ([1] o) = [1] (O′→O o)

-- If O had actually encoded the type μO. νZ. Z + O, then we could
-- have proved the following theorem:

mutual

  ⟦_⟧O : O → Stream Bit
  ⟦ ↓ z ⟧O = ⟦ z ⟧Z

  ⟦_⟧Z : Z O → Stream Bit
  ⟦ [0] z ⟧Z = 0b ∷ ♯ ⟦ ♭ z ⟧Z
  ⟦ [1] o ⟧Z = 1b ∷ ♯ ⟦   o ⟧O

Theorem : Set
Theorem = ∀ o → ¬ (head ⟦ o ⟧O ≡ 0b × head (tail ⟦ o ⟧O) ≡ 1b ×
                                      tail (tail ⟦ o ⟧O) ≈ ⟦ o ⟧O)

-- This would have been unfortunate, though:

inconsistency : Theorem → ⊥
inconsistency theorem = theorem 01^ω (refl , refl , proof)
  where
  proof : tail (tail ⟦ 01^ω ⟧O) ≈ ⟦ 01^ω ⟧O
  proof = refl ∷ ♯ (refl ∷ ♯ proof)

-- Using the following elimination principle we can prove the theorem:

data ⇑ {O} (P : O → Set) : Z O → Set where
  [0] : ∀ {z} → ∞ (⇑ P (♭ z)) → ⇑ P ([0] z)
  [1] : ∀ {o} → P o           → ⇑ P ([1] o)

O-Elim : Set₁
O-Elim = (P : O → Set) → (∀ {z} → ⇑ P z → P (↓ z)) → (o : O) → P o

theorem : O-Elim → Theorem
theorem O-elim = O-elim P helper
  where
  P : O → Set
  P o = ¬ (head ⟦ o ⟧O ≡ 0b × head (tail ⟦ o ⟧O) ≡ 1b ×
                              tail (tail ⟦ o ⟧O) ≈ ⟦ o ⟧O)

  helper : ∀ {z} → ⇑ P z → P (↓ z)
  helper ([1] p) (()   , eq₂ , eq₃)
  helper ([0] p) (refl , eq₂ , eq₃) =
    hlp _ eq₂ (head-cong eq₃) (tail-cong eq₃) (♭ p)
    where
    hlp : ∀ z → head ⟦ z ⟧Z ≡ 1b →
                head (tail ⟦ z ⟧Z) ≡ 0b →
                tail (tail ⟦ z ⟧Z) ≈ ⟦ z ⟧Z →
                ⇑ P z → ⊥
    hlp .([0] _) ()  eq₂ eq₃ ([0] p)
    hlp .([1] _) eq₁ eq₂ eq₃ ([1] p) =
      p (eq₂ , head-cong eq₃ , tail-cong eq₃)

-- Fortunately it appears as if we cannot prove this elimination
-- principle. The following code is not accepted by the termination
-- checker:

{-
mutual

  O-elim : O-Elim
  O-elim P hyp (↓ z) = hyp (Z-elim P hyp z)

  Z-elim : (P : O → Set) →
           (∀ {z} → ⇑ P z → P (↓ z)) →
           (z : Z O) → ⇑ P z
  Z-elim P hyp ([0] z) = [0] (♯ Z-elim P hyp (♭ z))
  Z-elim P hyp ([1] o) = [1] (O-elim P hyp o)
-}

-- If hyp were known to be contractive, then the code above would be
-- correct (if not accepted by the termination checker). This is not
-- the case in theorem above.

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
open import Preliminaries

module Preorder where

  record PreorderStructure (A : Set) : Set1 where
    constructor preorder-structure
    field
      _≤_ : A → A → Set
      refl : ∀ x → x ≤ x
      trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z

  record Preorder A : Set1 where
    constructor preorder
    field
      preorder-struct : PreorderStructure A

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import Categories.Category
open import Categories.Functor hiding (id)

module Categories.Diagram.Colimit.DualProperties
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} where

open import Function.Equality renaming (id to idFun)

open import Categories.Category.Instance.Setoids
open import Categories.Diagram.Duality C
open import Categories.Functor.Hom
open import Categories.Category.Construction.Cocones as Coc
open import Categories.Diagram.Limit as Lim
open import Categories.Diagram.Limit.Properties
open import Categories.Diagram.Colimit as Col
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.Morphism C
open import Categories.Morphism.Duality C

private
    module C = Category C
    module J = Category J
    open C
    open Hom C
    open HomReasoning

-- contravariant hom functor sends colimit of F to its limit.
module _ (W : Obj) {F : Functor J C} (col : Colimit F) where
  private
    module F = Functor F

    HomF : Functor J.op (Setoids ℓ e)
    HomF = Hom[-, W ] ∘F F.op

  hom-colimit⇒limit : Limit HomF
  hom-colimit⇒limit = ≃-resp-lim (Hom≃ ⓘʳ F.op) (hom-resp-limit W (Colimit⇒coLimit col))
    where Hom≃ : Hom[ op ][ W ,-] ≃ Hom[-, W ]
          Hom≃ = record
            { F⇒G = ntHelper record
              { η       = λ _ → idFun
              ; commute = λ _ eq → C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq) ○ C.assoc
              }
            ; F⇐G = ntHelper record
              { η       = λ _ → idFun
              ; commute = λ _ eq → C.sym-assoc ○ C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq)
              }
            ; iso = λ _ → record
              { isoˡ = λ eq → eq
              ; isoʳ = λ eq → eq
              }
            }

-- natural isomorphisms respects limits
module _ {F G : Functor J C} (F≃G : F ≃ G) where
  private
    module F  = Functor F
    module G  = Functor G
    open NaturalIsomorphism F≃G

  ≃-resp-colim : Colimit F → Colimit G
  ≃-resp-colim Cf = coLimit⇒Colimit (≃-resp-lim op′ (Colimit⇒coLimit Cf))

  ≃⇒Cocone⇒ : ∀ (Cf : Colimit F) (Cg : Colimit G) → Cocones G [ Colimit.colimit Cg , Colimit.colimit (≃-resp-colim Cf) ]
  ≃⇒Cocone⇒ Cf Cg = coCone⇒⇒Cocone⇒ (≃⇒Cone⇒ op′ (Colimit⇒coLimit Cf) (Colimit⇒coLimit Cg))

≃⇒colim≅ : ∀ {F G : Functor J C} (F≃G : F ≃ G) (Cf : Colimit F) (Cg : Colimit G) → Colimit.coapex Cf ≅ Colimit.coapex Cg
≃⇒colim≅ F≃G Cf Cg = op-≅⇒≅ (≃⇒lim≅ (NaturalIsomorphism.op′ F≃G) (Colimit⇒coLimit Cf) (Colimit⇒coLimit Cg))

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Setoids.Facts.Initial where

open import Level
open import Relation.Binary using (Setoid)

open import Cats.Category
open import Cats.Category.Setoids using (Setoids ; ≈-intro)

import Data.Empty as Empty

⊥ : ∀ {l l′} → Setoid l l′
⊥ = record
  { Carrier = Lift _ Empty.⊥
  ; _≈_ = λ()
  ; isEquivalence = record
      { refl = λ{}
      ; sym = λ{}
      ; trans = λ{}
      }
  }

instance
  hasInitial : ∀ {l l≈} → HasInitial (Setoids l l≈)
  hasInitial = record
    { ⊥ = ⊥
    ; isInitial = λ X → record
      { arr = record { arr = λ() ; resp = λ{} }
      ; unique = λ _ → ≈-intro λ{}
      }
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Class.IsEquivalence
open import Oscar.Class.Setoid
open import Oscar.Data.Proposequality

module Oscar.Property.Setoid.Proposextensequality where

module _ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} where

  instance

    𝓡eflexivityProposextensequality : Reflexivity.class Proposextensequality⟦ 𝔓 ⟧
    𝓡eflexivityProposextensequality .⋆ _ = ∅

    𝓢ymmetryProposextensequality : Symmetry.class Proposextensequality⟦ 𝔓 ⟧
    𝓢ymmetryProposextensequality .⋆ f₁≡̇f₂ x rewrite f₁≡̇f₂ x = ∅

    𝓣ransitivityProposextensequality : Transitivity.class Proposextensequality⟦ 𝔓 ⟧
    𝓣ransitivityProposextensequality .⋆ f₁≡̇f₂ f₂≡̇f₃ x rewrite f₁≡̇f₂ x = f₂≡̇f₃ x

    IsEquivalenceProposextensequality : IsEquivalence Proposextensequality⟦ 𝔓 ⟧
    IsEquivalenceProposextensequality = ∁

module _ {𝔬} {𝔒 : Ø 𝔬} {𝔭} (𝔓 : 𝔒 → Ø 𝔭) where

  SetoidProposextensequality : Setoid _ _
  SetoidProposextensequality = ∁ Proposextensequality⟦ 𝔓 ⟧


text:
{-# OPTIONS --allow-unsolved-metas #-}

latex : Set
latex = {!test!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some algebraic structures defined over some other structure
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)

module Algebra.Module.Structures where

open import Algebra.Bundles
open import Algebra.Core
import Algebra.Definitions as Defs
open import Algebra.Module.Definitions
open import Algebra.Structures
open import Data.Product using (_,_; proj₁; proj₂)
open import Level using (Level; _⊔_)

private
  variable
    m ℓm r ℓr s ℓs : Level
    M : Set m

module _ (semiring : Semiring r ℓr) (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
  where

  open Semiring semiring renaming (Carrier to R)

  record IsPreleftSemimodule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open LeftDefs R ≈ᴹ
    field
      *ₗ-cong : Congruent _≈_ *ₗ
      *ₗ-zeroˡ : LeftZero 0# 0ᴹ *ₗ
      *ₗ-distribʳ : *ₗ DistributesOverʳ _+_ ⟶ +ᴹ
      *ₗ-identityˡ : LeftIdentity 1# *ₗ
      *ₗ-assoc : Associative _*_ *ₗ
      *ₗ-zeroʳ : RightZero 0ᴹ *ₗ
      *ₗ-distribˡ : *ₗ DistributesOverˡ +ᴹ

  record IsLeftSemimodule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open LeftDefs R ≈ᴹ
    field
      +ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
      isPreleftSemimodule : IsPreleftSemimodule *ₗ

    open IsPreleftSemimodule isPreleftSemimodule public

    open IsCommutativeMonoid +ᴹ-isCommutativeMonoid public
      using () renaming
      ( assoc                to +ᴹ-assoc
      ; comm                 to +ᴹ-comm
      ; identity             to +ᴹ-identity
      ; identityʳ            to +ᴹ-identityʳ
      ; identityˡ            to +ᴹ-identityˡ
      ; isEquivalence        to ≈ᴹ-isEquivalence
      ; isMagma              to +ᴹ-isMagma
      ; isMonoid             to +ᴹ-isMonoid
      ; isPartialEquivalence to ≈ᴹ-isPartialEquivalence
      ; isSemigroup          to +ᴹ-isSemigroup
      ; refl                 to ≈ᴹ-refl
      ; reflexive            to ≈ᴹ-reflexive
      ; setoid               to ≈ᴹ-setoid
      ; sym                  to ≈ᴹ-sym
      ; trans                to ≈ᴹ-trans
      ; ∙-cong               to +ᴹ-cong
      ; ∙-congʳ              to +ᴹ-congʳ
      ; ∙-congˡ              to +ᴹ-congˡ
      )

    *ₗ-congˡ : LeftCongruent *ₗ
    *ₗ-congˡ mm = *ₗ-cong refl mm

    *ₗ-congʳ : RightCongruent _≈_ *ₗ
    *ₗ-congʳ xx = *ₗ-cong xx ≈ᴹ-refl

  record IsPrerightSemimodule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open RightDefs R ≈ᴹ
    field
      *ᵣ-cong : Congruent _≈_ *ᵣ
      *ᵣ-zeroʳ : RightZero 0# 0ᴹ *ᵣ
      *ᵣ-distribˡ : *ᵣ DistributesOverˡ _+_ ⟶ +ᴹ
      *ᵣ-identityʳ : RightIdentity 1# *ᵣ
      *ᵣ-assoc : Associative _*_ *ᵣ
      *ᵣ-zeroˡ : LeftZero 0ᴹ *ᵣ
      *ᵣ-distribʳ : *ᵣ DistributesOverʳ +ᴹ

  record IsRightSemimodule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open RightDefs R ≈ᴹ
    field
      +ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
      isPrerightSemimodule : IsPrerightSemimodule *ᵣ

    open IsPrerightSemimodule isPrerightSemimodule public

    open IsCommutativeMonoid +ᴹ-isCommutativeMonoid public
      using () renaming
      ( assoc                to +ᴹ-assoc
      ; comm                 to +ᴹ-comm
      ; identity             to +ᴹ-identity
      ; identityʳ            to +ᴹ-identityʳ
      ; identityˡ            to +ᴹ-identityˡ
      ; isEquivalence        to ≈ᴹ-isEquivalence
      ; isMagma              to +ᴹ-isMagma
      ; isMonoid             to +ᴹ-isMonoid
      ; isPartialEquivalence to ≈ᴹ-isPartialEquivalence
      ; isSemigroup          to +ᴹ-isSemigroup
      ; refl                 to ≈ᴹ-refl
      ; reflexive            to ≈ᴹ-reflexive
      ; setoid               to ≈ᴹ-setoid
      ; sym                  to ≈ᴹ-sym
      ; trans                to ≈ᴹ-trans
      ; ∙-cong               to +ᴹ-cong
      ; ∙-congʳ              to +ᴹ-congʳ
      ; ∙-congˡ              to +ᴹ-congˡ
      )

    *ᵣ-congˡ : LeftCongruent _≈_ *ᵣ
    *ᵣ-congˡ xx = *ᵣ-cong ≈ᴹ-refl xx

    *ᵣ-congʳ : RightCongruent *ᵣ
    *ᵣ-congʳ mm = *ᵣ-cong mm refl

module _ (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs)
         (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
  where

  open Semiring R-semiring using () renaming (Carrier to R)
  open Semiring S-semiring using () renaming (Carrier to S)

  record IsBisemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ S M)
                        : Set (r ⊔ s ⊔ m ⊔ ℓr ⊔ ℓs ⊔ ℓm) where
    open BiDefs R S ≈ᴹ
    field
      +ᴹ-isCommutativeMonoid : IsCommutativeMonoid ≈ᴹ +ᴹ 0ᴹ
      isPreleftSemimodule : IsPreleftSemimodule R-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
      isPrerightSemimodule : IsPrerightSemimodule S-semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
      *ₗ-*ᵣ-assoc : Associative *ₗ *ᵣ

    isLeftSemimodule : IsLeftSemimodule R-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
    isLeftSemimodule = record
      { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
      ; isPreleftSemimodule = isPreleftSemimodule
      }

    isRightSemimodule : IsRightSemimodule S-semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
    isRightSemimodule = record
      { +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid
      ; isPrerightSemimodule = isPrerightSemimodule
      }

    open IsLeftSemimodule isLeftSemimodule public
      hiding (+ᴹ-isCommutativeMonoid; isPreleftSemimodule)
    open IsPrerightSemimodule isPrerightSemimodule public
    open IsRightSemimodule isRightSemimodule public
      using (*ᵣ-congˡ; *ᵣ-congʳ)

module _ (commutativeSemiring : CommutativeSemiring r ℓr)
         (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M)
  where

  open CommutativeSemiring commutativeSemiring renaming (Carrier to R)

  -- An R-semimodule is an R-R-bisemimodule where R is commutative.
  -- This means that *ₗ and *ᵣ coincide up to mathematical equality, though it
  -- may be that they do not coincide up to definitional equality.

  record IsSemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M)
                      : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    field
      isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ

    open IsBisemimodule isBisemimodule public

module _ (ring : Ring r ℓr)
         (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
  where

  open Ring ring renaming (Carrier to R)

  record IsLeftModule (*ₗ : Opₗ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open Defs ≈ᴹ
    field
      isLeftSemimodule : IsLeftSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ₗ
      -ᴹ‿cong : Congruent₁ -ᴹ
      -ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ

    open IsLeftSemimodule isLeftSemimodule public

    +ᴹ-isAbelianGroup : IsAbelianGroup ≈ᴹ +ᴹ 0ᴹ -ᴹ
    +ᴹ-isAbelianGroup = record
      { isGroup = record
        { isMonoid = +ᴹ-isMonoid
        ; inverse = -ᴹ‿inverse
        ; ⁻¹-cong = -ᴹ‿cong
        }
      ; comm = +ᴹ-comm
      }

    open IsAbelianGroup +ᴹ-isAbelianGroup public
      using () renaming
      ( isGroup    to +ᴹ-isGroup
      ; inverseˡ   to -ᴹ‿inverseˡ
      ; inverseʳ   to -ᴹ‿inverseʳ
      ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
      ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
      )

  record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    open Defs ≈ᴹ
    field
      isRightSemimodule : IsRightSemimodule semiring ≈ᴹ +ᴹ 0ᴹ *ᵣ
      -ᴹ‿cong : Congruent₁ -ᴹ
      -ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ

    open IsRightSemimodule isRightSemimodule public

    +ᴹ-isAbelianGroup : IsAbelianGroup ≈ᴹ +ᴹ 0ᴹ -ᴹ
    +ᴹ-isAbelianGroup = record
      { isGroup = record
        { isMonoid = +ᴹ-isMonoid
        ; inverse = -ᴹ‿inverse
        ; ⁻¹-cong = -ᴹ‿cong
        }
      ; comm = +ᴹ-comm
      }

    open IsAbelianGroup +ᴹ-isAbelianGroup public
      using () renaming
      ( isGroup    to +ᴹ-isGroup
      ; inverseˡ   to -ᴹ‿inverseˡ
      ; inverseʳ   to -ᴹ‿inverseʳ
      ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
      ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
      )

module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs)
         (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
  where

  open Ring R-ring renaming (Carrier to R; semiring to R-semiring)
  open Ring S-ring renaming (Carrier to S; semiring to S-semiring)

  record IsBimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ S M)
                    : Set (r ⊔ s ⊔ m ⊔ ℓr ⊔ ℓs ⊔ ℓm) where
    open Defs ≈ᴹ
    field
      isBisemimodule : IsBisemimodule R-semiring S-semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
      -ᴹ‿cong : Congruent₁ -ᴹ
      -ᴹ‿inverse : Inverse 0ᴹ -ᴹ +ᴹ

    open IsBisemimodule isBisemimodule public

    isLeftModule : IsLeftModule R-ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ
    isLeftModule = record
      { isLeftSemimodule = isLeftSemimodule
      ; -ᴹ‿cong = -ᴹ‿cong
      ; -ᴹ‿inverse = -ᴹ‿inverse
      }

    open IsLeftModule isLeftModule public
      using ( +ᴹ-isAbelianGroup; +ᴹ-isGroup; -ᴹ‿inverseˡ; -ᴹ‿inverseʳ
            ; uniqueˡ‿-ᴹ; uniqueʳ‿-ᴹ)

    isRightModule : IsRightModule S-ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ᵣ
    isRightModule = record
      { isRightSemimodule = isRightSemimodule
      ; -ᴹ‿cong = -ᴹ‿cong
      ; -ᴹ‿inverse = -ᴹ‿inverse
      }

module _ (commutativeRing : CommutativeRing r ℓr)
         (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
  where

  open CommutativeRing commutativeRing renaming (Carrier to R)

  -- An R-module is an R-R-bimodule where R is commutative.
  -- This means that *ₗ and *ᵣ coincide up to mathematical equality, though it
  -- may be that they do not coincide up to definitional equality.

  record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
    field
      isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ

    open IsBimodule isBimodule public

    isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
    isSemimodule = record { isBisemimodule = isBisemimodule }


text:
------------------------------------------------------------------------
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.BooleanAlgebra (b : BooleanAlgebra) where

open BooleanAlgebra b
import Algebra.Props.DistributiveLattice as DL
open DL distributiveLattice public
open import Algebra.Structures
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Relation.Binary
open import Data.Function
open import Data.Product

------------------------------------------------------------------------
-- Some simple generalisations

∨-complement : Inverse ⊤ ¬_ _∨_
∨-complement = ∨-complementˡ , ∨-complementʳ
  where
  ∨-complementˡ : LeftInverse ⊤ ¬_ _∨_
  ∨-complementˡ x = begin
    ¬ x ∨ x    ≈⟨ ∨-comm _ _ ⟩
    x   ∨ ¬ x  ≈⟨ ∨-complementʳ _ ⟩
    ⊤          ∎

∧-complement : Inverse ⊥ ¬_ _∧_
∧-complement = ∧-complementˡ , ∧-complementʳ
  where
  ∧-complementˡ : LeftInverse ⊥ ¬_ _∧_
  ∧-complementˡ x = begin
    ¬ x ∧ x    ≈⟨ ∧-comm _ _ ⟩
    x   ∧ ¬ x  ≈⟨ ∧-complementʳ _ ⟩
    ⊥          ∎

------------------------------------------------------------------------
-- The dual construction is also a boolean algebra

∧-∨-isBooleanAlgebra : IsBooleanAlgebra _≈_ _∧_ _∨_ ¬_ ⊥ ⊤
∧-∨-isBooleanAlgebra = record
  { isDistributiveLattice = ∧-∨-isDistributiveLattice
  ; ∨-complementʳ         = proj₂ ∧-complement
  ; ∧-complementʳ         = proj₂ ∨-complement
  ; ¬-pres-≈              = ¬-pres-≈
  }

∧-∨-booleanAlgebra : BooleanAlgebra
∧-∨-booleanAlgebra = record
  { _∧_              = _∨_
  ; _∨_              = _∧_
  ; ⊤                = ⊥
  ; ⊥                = ⊤
  ; isBooleanAlgebra = ∧-∨-isBooleanAlgebra
  }

------------------------------------------------------------------------
-- (∨, ∧, ⊥, ⊤) is a commutative semiring

private

  ∧-identity : Identity ⊤ _∧_
  ∧-identity = (λ _ → ∧-comm _ _ ⟨ trans ⟩ x∧⊤=x _) , x∧⊤=x
    where
    x∧⊤=x : ∀ x → x ∧ ⊤ ≈ x
    x∧⊤=x x = begin
      x ∧ ⊤          ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∨-complement _) ⟩
      x ∧ (x ∨ ¬ x)  ≈⟨ proj₂ absorptive _ _ ⟩
      x              ∎

  ∨-identity : Identity ⊥ _∨_
  ∨-identity = (λ _ → ∨-comm _ _ ⟨ trans ⟩ x∨⊥=x _) , x∨⊥=x
    where
    x∨⊥=x : ∀ x → x ∨ ⊥ ≈ x
    x∨⊥=x x = begin
      x ∨ ⊥          ≈⟨ refl ⟨ ∨-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩
      x ∨ x ∧ ¬ x    ≈⟨ proj₁ absorptive _ _ ⟩
      x              ∎

  ∧-zero : Zero ⊥ _∧_
  ∧-zero = (λ _ → ∧-comm _ _ ⟨ trans ⟩ x∧⊥=⊥ _) , x∧⊥=⊥
    where
    x∧⊥=⊥ : ∀ x → x ∧ ⊥ ≈ ⊥
    x∧⊥=⊥ x = begin
      x ∧ ⊥          ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩
      x ∧  x  ∧ ¬ x  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
      (x ∧ x) ∧ ¬ x  ≈⟨ ∧-idempotent _ ⟨ ∧-pres-≈ ⟩ refl ⟩
      x       ∧ ¬ x  ≈⟨ proj₂ ∧-complement _ ⟩
      ⊥              ∎

∨-∧-isCommutativeSemiring : IsCommutativeSemiring _≈_ _∨_ _∧_ ⊥ ⊤
∨-∧-isCommutativeSemiring = record
  { isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = record
        { isMonoid = record
          { isSemigroup = record
            { isEquivalence = isEquivalence
            ; assoc         = ∨-assoc
            ; ∙-pres-≈      = ∨-pres-≈
            }
          ; identity  = ∨-identity
          }
        ; comm  = ∨-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∧-assoc
          ; ∙-pres-≈      = ∧-pres-≈
          }
        ; identity = ∧-identity
        }
      ; distrib = ∧-∨-distrib
      }
    ; zero = ∧-zero
    }
  ; *-comm = ∧-comm
  }

∨-∧-commutativeSemiring : CommutativeSemiring
∨-∧-commutativeSemiring = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = ⊥
  ; 1#                    = ⊤
  ; isCommutativeSemiring = ∨-∧-isCommutativeSemiring
  }

------------------------------------------------------------------------
-- (∧, ∨, ⊤, ⊥) is a commutative semiring

private

  ∨-zero : Zero ⊤ _∨_
  ∨-zero = (λ _ → ∨-comm _ _ ⟨ trans ⟩ x∨⊤=⊤ _) , x∨⊤=⊤
    where
    x∨⊤=⊤ : ∀ x → x ∨ ⊤ ≈ ⊤
    x∨⊤=⊤ x = begin
      x ∨ ⊤          ≈⟨ refl ⟨ ∨-pres-≈ ⟩ sym (proj₂ ∨-complement _) ⟩
      x ∨  x  ∨ ¬ x  ≈⟨ sym $ ∨-assoc _ _ _ ⟩
      (x ∨ x) ∨ ¬ x  ≈⟨ ∨-idempotent _ ⟨ ∨-pres-≈ ⟩ refl ⟩
      x       ∨ ¬ x  ≈⟨ proj₂ ∨-complement _ ⟩
      ⊤              ∎

∧-∨-isCommutativeSemiring : IsCommutativeSemiring _≈_ _∧_ _∨_ ⊤ ⊥
∧-∨-isCommutativeSemiring = record
  { isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = record
        { isMonoid = record
          { isSemigroup = record
            { isEquivalence = isEquivalence
            ; assoc         = ∧-assoc
            ; ∙-pres-≈      = ∧-pres-≈
            }
          ; identity  = ∧-identity
          }
        ; comm  = ∧-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∨-assoc
          ; ∙-pres-≈      = ∨-pres-≈
          }
        ; identity = ∨-identity
        }
      ; distrib = ∨-∧-distrib
      }
    ; zero = ∨-zero
    }
  ; *-comm = ∨-comm
  }

∧-∨-commutativeSemiring : CommutativeSemiring
∧-∨-commutativeSemiring =
  record { isCommutativeSemiring = ∧-∨-isCommutativeSemiring }

------------------------------------------------------------------------
-- Some other properties

-- I took the statement of this lemma (called Uniqueness of
-- Complements) from some course notes, "Boolean Algebra", written
-- by Gert Smolka.

private
  lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y
  lemma x y x∧y=⊥ x∨y=⊤ = begin
    ¬ x                ≈⟨ sym $ proj₂ ∧-identity _ ⟩
    ¬ x ∧ ⊤            ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym x∨y=⊤ ⟩
    ¬ x ∧ (x ∨ y)      ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
    ¬ x ∧ x ∨ ¬ x ∧ y  ≈⟨ proj₁ ∧-complement _ ⟨ ∨-pres-≈ ⟩ refl ⟩
    ⊥ ∨ ¬ x ∧ y        ≈⟨ sym x∧y=⊥ ⟨ ∨-pres-≈ ⟩ refl ⟩
    x ∧ y ∨ ¬ x ∧ y    ≈⟨ sym $ proj₂ ∧-∨-distrib _ _ _ ⟩
    (x ∨ ¬ x) ∧ y      ≈⟨ proj₂ ∨-complement _ ⟨ ∧-pres-≈ ⟩ refl ⟩
    ⊤ ∧ y              ≈⟨ proj₁ ∧-identity _ ⟩
    y                  ∎

¬⊥=⊤ : ¬ ⊥ ≈ ⊤
¬⊥=⊤ = lemma ⊥ ⊤ (proj₂ ∧-identity _) (proj₂ ∨-zero _)

¬⊤=⊥ : ¬ ⊤ ≈ ⊥
¬⊤=⊥ = lemma ⊤ ⊥ (proj₂ ∧-zero _) (proj₂ ∨-identity _)

¬-involutive : Involutive ¬_
¬-involutive x = lemma (¬ x) x (proj₁ ∧-complement _) (proj₁ ∨-complement _)

deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y
deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂
  where
  lem₁ = begin
    (x ∧ y) ∧ (¬ x ∨ ¬ y)          ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
    (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ (∧-comm _ _ ⟨ ∧-pres-≈ ⟩ refl) ⟨ ∨-pres-≈ ⟩ refl ⟩
    (y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∧-assoc _ _ _ ⟨ ∨-pres-≈ ⟩ ∧-assoc _ _ _ ⟩
    y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y)  ≈⟨ (refl ⟨ ∧-pres-≈ ⟩ proj₂ ∧-complement _) ⟨ ∨-pres-≈ ⟩
                                      (refl ⟨ ∧-pres-≈ ⟩ proj₂ ∧-complement _) ⟩
    (y ∧ ⊥) ∨ (x ∧ ⊥)              ≈⟨ proj₂ ∧-zero _ ⟨ ∨-pres-≈ ⟩ proj₂ ∧-zero _ ⟩
    ⊥ ∨ ⊥                          ≈⟨ proj₂ ∨-identity _ ⟩
    ⊥                              ∎

  lem₃ = begin
    (x ∧ y) ∨ ¬ x          ≈⟨ proj₂ ∨-∧-distrib _ _ _ ⟩
    (x ∨ ¬ x) ∧ (y ∨ ¬ x)  ≈⟨ proj₂ ∨-complement _ ⟨ ∧-pres-≈ ⟩ refl ⟩
    ⊤ ∧ (y ∨ ¬ x)          ≈⟨ proj₁ ∧-identity _ ⟩
    y ∨ ¬ x                ≈⟨ ∨-comm _ _ ⟩
    ¬ x ∨ y                ∎

  lem₂ = begin
    (x ∧ y) ∨ (¬ x ∨ ¬ y)  ≈⟨ sym $ ∨-assoc _ _ _ ⟩
    ((x ∧ y) ∨ ¬ x) ∨ ¬ y  ≈⟨ lem₃ ⟨ ∨-pres-≈ ⟩ refl ⟩
    (¬ x ∨ y) ∨ ¬ y        ≈⟨ ∨-assoc _ _ _ ⟩
    ¬ x ∨ (y ∨ ¬ y)        ≈⟨ refl ⟨ ∨-pres-≈ ⟩ proj₂ ∨-complement _ ⟩
    ¬ x ∨ ⊤                ≈⟨ proj₂ ∨-zero _ ⟩
    ⊤                      ∎

deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y
deMorgan₂ x y = begin
  ¬ (x ∨ y)          ≈⟨ ¬-pres-≈ $ sym (¬-involutive _) ⟨ ∨-pres-≈ ⟩
                                   sym (¬-involutive _) ⟩
  ¬ (¬ ¬ x ∨ ¬ ¬ y)  ≈⟨ ¬-pres-≈ $ sym $ deMorgan₁ _ _ ⟩
  ¬ ¬ (¬ x ∧ ¬ y)    ≈⟨ ¬-involutive _ ⟩
  ¬ x ∧ ¬ y          ∎

------------------------------------------------------------------------
-- (⊕, ∧, id, ⊥, ⊤) is a commutative ring

-- This construction is parameterised over the definition of xor.

module XorRing
  (xor : Op₂ carrier)
  (⊕-def : ∀ x y → xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y))
  where

  private
    infixl 6 _⊕_

    _⊕_ : Op₂ carrier
    _⊕_ = xor

  private
    helper : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ ¬ u ≈ y ∧ ¬ v
    helper x≈y u≈v = x≈y ⟨ ∧-pres-≈ ⟩ ¬-pres-≈ u≈v

  ⊕-¬-distribˡ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y
  ⊕-¬-distribˡ x y = begin
    ¬ (x ⊕ y)                              ≈⟨ ¬-pres-≈ $ ⊕-def _ _ ⟩
    ¬ ((x ∨ y) ∧ (¬ (x ∧ y)))              ≈⟨ ¬-pres-≈ (proj₂ ∧-∨-distrib _ _ _) ⟩
    ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y)))  ≈⟨ ¬-pres-≈ $
                                                refl ⟨ ∨-pres-≈ ⟩
                                                  (refl ⟨ ∧-pres-≈ ⟩
                                                     ¬-pres-≈ (∧-comm _ _)) ⟩
    ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x)))  ≈⟨ ¬-pres-≈ $ lem _ _ ⟨ ∨-pres-≈ ⟩ lem _ _ ⟩
    ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x))              ≈⟨ deMorgan₂ _ _ ⟩
    ¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x)              ≈⟨ deMorgan₁ _ _ ⟨ ∧-pres-≈ ⟩ refl ⟩
    (¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x)          ≈⟨ helper (refl ⟨ ∨-pres-≈ ⟩ ¬-involutive _)
                                                     (∧-comm _ _) ⟩
    (¬ x ∨ y) ∧ ¬ (¬ x ∧ y)                ≈⟨ sym $ ⊕-def _ _ ⟩
    ¬ x ⊕ y                                ∎
    where
    lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y
    lem x y = begin
      x ∧ ¬ (x ∧ y)          ≈⟨ refl ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _ ⟩
      x ∧ (¬ x ∨ ¬ y)        ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩
      (x ∧ ¬ x) ∨ (x ∧ ¬ y)  ≈⟨ proj₂ ∧-complement _ ⟨ ∨-pres-≈ ⟩ refl ⟩
      ⊥ ∨ (x ∧ ¬ y)          ≈⟨ proj₁ ∨-identity _ ⟩
      x ∧ ¬ y                ∎

  private
    ⊕-comm : Commutative _⊕_
    ⊕-comm x y = begin
      x ⊕ y                ≈⟨ ⊕-def _ _ ⟩
      (x ∨ y) ∧ ¬ (x ∧ y)  ≈⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩
      (y ∨ x) ∧ ¬ (y ∧ x)  ≈⟨ sym $ ⊕-def _ _ ⟩
      y ⊕ x                ∎

  ⊕-¬-distribʳ : ∀ x y → ¬ (x ⊕ y) ≈ x ⊕ ¬ y
  ⊕-¬-distribʳ x y = begin
    ¬ (x ⊕ y)  ≈⟨ ¬-pres-≈ $ ⊕-comm _ _ ⟩
    ¬ (y ⊕ x)  ≈⟨ ⊕-¬-distribˡ _ _ ⟩
    ¬ y ⊕ x    ≈⟨ ⊕-comm _ _ ⟩
    x ⊕ ¬ y    ∎

  ⊕-annihilates-¬ : ∀ x y → x ⊕ y ≈ ¬ x ⊕ ¬ y
  ⊕-annihilates-¬ x y = begin
    x ⊕ y        ≈⟨ sym $ ¬-involutive _ ⟩
    ¬ ¬ (x ⊕ y)  ≈⟨ ¬-pres-≈ $ ⊕-¬-distribˡ _ _ ⟩
    ¬ (¬ x ⊕ y)  ≈⟨ ⊕-¬-distribʳ _ _ ⟩
    ¬ x ⊕ ¬ y    ∎

  private
    ⊕-pres : _⊕_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
    ⊕-pres {x} {y} {u} {v} x≈y u≈v = begin
      x ⊕ u                ≈⟨ ⊕-def _ _ ⟩
      (x ∨ u) ∧ ¬ (x ∧ u)  ≈⟨ helper (x≈y ⟨ ∨-pres-≈ ⟩ u≈v)
                                     (x≈y ⟨ ∧-pres-≈ ⟩ u≈v) ⟩
      (y ∨ v) ∧ ¬ (y ∧ v)  ≈⟨ sym $ ⊕-def _ _ ⟩
      y ⊕ v                ∎

    ⊕-identity : Identity ⊥ _⊕_
    ⊕-identity = ⊥⊕x=x , (λ _ → ⊕-comm _ _ ⟨ trans ⟩ ⊥⊕x=x _)
      where
      ⊥⊕x=x : ∀ x → ⊥ ⊕ x ≈ x
      ⊥⊕x=x x = begin
        ⊥ ⊕ x                ≈⟨ ⊕-def _ _ ⟩
        (⊥ ∨ x) ∧ ¬ (⊥ ∧ x)  ≈⟨ helper (proj₁ ∨-identity _)
                                       (proj₁ ∧-zero _) ⟩
        x ∧ ¬ ⊥              ≈⟨ refl ⟨ ∧-pres-≈ ⟩ ¬⊥=⊤ ⟩
        x ∧ ⊤                ≈⟨ proj₂ ∧-identity _ ⟩
        x                    ∎

    ⊕-inverse : Inverse ⊥ id _⊕_
    ⊕-inverse = x⊕x=⊥ , (λ _ → ⊕-comm _ _ ⟨ trans ⟩ x⊕x=⊥ _)
      where
      x⊕x=⊥ : ∀ x → x ⊕ x ≈ ⊥
      x⊕x=⊥ x = begin
        x ⊕ x                ≈⟨ ⊕-def _ _ ⟩
        (x ∨ x) ∧ ¬ (x ∧ x)  ≈⟨ helper (∨-idempotent _)
                                       (∧-idempotent _) ⟩
        x ∧ ¬ x              ≈⟨ proj₂ ∧-complement _ ⟩
        ⊥                    ∎

    distrib-∧-⊕ : _∧_ DistributesOver _⊕_
    distrib-∧-⊕ = distˡ , distʳ
      where
      distˡ : _∧_ DistributesOverˡ _⊕_
      distˡ x y z = begin
        x ∧ (y ⊕ z)                ≈⟨ refl ⟨ ∧-pres-≈ ⟩ ⊕-def _ _ ⟩
        x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
        (x ∧ (y ∨ z)) ∧ ¬ (y ∧ z)  ≈⟨ refl ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _ ⟩
        (x ∧ (y ∨ z)) ∧
        (¬ y ∨ ¬ z)                ≈⟨ sym $ proj₁ ∨-identity _ ⟩
        ⊥ ∨
        ((x ∧ (y ∨ z)) ∧
         (¬ y ∨ ¬ z))              ≈⟨ lem₃ ⟨ ∨-pres-≈ ⟩ refl ⟩
        ((x ∧ (y ∨ z)) ∧ ¬ x) ∨
        ((x ∧ (y ∨ z)) ∧
         (¬ y ∨ ¬ z))              ≈⟨ sym $ proj₁ ∧-∨-distrib _ _ _ ⟩
        (x ∧ (y ∨ z)) ∧
        (¬ x ∨ (¬ y ∨ ¬ z))        ≈⟨  refl ⟨ ∧-pres-≈ ⟩
                                      (refl ⟨ ∨-pres-≈ ⟩ sym (deMorgan₁ _ _)) ⟩
        (x ∧ (y ∨ z)) ∧
        (¬ x ∨ ¬ (y ∧ z))          ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym (deMorgan₁ _ _) ⟩
          (x ∧ (y ∨ z)) ∧
        ¬ (x ∧ (y ∧ z))            ≈⟨ helper refl lem₁ ⟩
          (x ∧ (y ∨ z)) ∧
        ¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟨ ∧-pres-≈ ⟩
                                      refl ⟩
          ((x ∧ y) ∨ (x ∧ z)) ∧
        ¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ sym $ ⊕-def _ _ ⟩
        (x ∧ y) ⊕ (x ∧ z)          ∎
        where
        lem₂ = begin
          x ∧ (y ∧ z)  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
          (x ∧ y) ∧ z  ≈⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ refl ⟩
          (y ∧ x) ∧ z  ≈⟨ ∧-assoc _ _ _ ⟩
          y ∧ (x ∧ z)  ∎

        lem₁ = begin
          x ∧ (y ∧ z)        ≈⟨ sym (∧-idempotent _) ⟨ ∧-pres-≈ ⟩ refl ⟩
          (x ∧ x) ∧ (y ∧ z)  ≈⟨ ∧-assoc _ _ _ ⟩
          x ∧ (x ∧ (y ∧ z))  ≈⟨ refl ⟨ ∧-pres-≈ ⟩ lem₂ ⟩
          x ∧ (y ∧ (x ∧ z))  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
          (x ∧ y) ∧ (x ∧ z)  ∎

        lem₃ = begin
          ⊥                      ≈⟨ sym $ proj₂ ∧-zero _ ⟩
          (y ∨ z) ∧ ⊥            ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩
          (y ∨ z) ∧ (x ∧ ¬ x)    ≈⟨ sym $ ∧-assoc _ _ _ ⟩
          ((y ∨ z) ∧ x) ∧ ¬ x    ≈⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ refl  ⟩
          (x ∧ (y ∨ z)) ∧ ¬ x    ∎

      distʳ : _∧_ DistributesOverʳ _⊕_
      distʳ x y z = begin
        (y ⊕ z) ∧ x        ≈⟨ ∧-comm _ _ ⟩
        x ∧ (y ⊕ z)        ≈⟨ distˡ _ _ _ ⟩
        (x ∧ y) ⊕ (x ∧ z)  ≈⟨ ∧-comm _ _ ⟨ ⊕-pres ⟩ ∧-comm _ _ ⟩
        (y ∧ x) ⊕ (z ∧ x)  ∎

    lemma₂ : ∀ x y u v →
             (x ∧ y) ∨ (u ∧ v) ≈
             ((x ∨ u) ∧ (y ∨ u)) ∧
             ((x ∨ v) ∧ (y ∨ v))
    lemma₂ x y u v = begin
        (x ∧ y) ∨ (u ∧ v)              ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
        ((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v)  ≈⟨ proj₂ ∨-∧-distrib _ _ _
                                            ⟨ ∧-pres-≈ ⟩
                                          proj₂ ∨-∧-distrib _ _ _ ⟩
        ((x ∨ u) ∧ (y ∨ u)) ∧
        ((x ∨ v) ∧ (y ∨ v))            ∎

    ⊕-assoc : Associative _⊕_
    ⊕-assoc x y z = sym $ begin
      x ⊕ (y ⊕ z)                                ≈⟨ refl ⟨ ⊕-pres ⟩ ⊕-def _ _ ⟩
      x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z))                  ≈⟨ ⊕-def _ _ ⟩
        (x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))) ∧
      ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))              ≈⟨ lem₃ ⟨ ∧-pres-≈ ⟩ lem₄ ⟩
      (((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
      (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ ∧-assoc _ _ _ ⟩
      ((x ∨ y) ∨ z) ∧
      (((x ∨ ¬ y) ∨ ¬ z) ∧
       (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ refl ⟨ ∧-pres-≈ ⟩ lem₅ ⟩
      ((x ∨ y) ∨ z) ∧
      (((¬ x ∨ ¬ y) ∨ z) ∧
       (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ sym $ ∧-assoc _ _ _ ⟩
      (((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
      (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ lem₁ ⟨ ∧-pres-≈ ⟩ lem₂ ⟩
        (((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z) ∧
      ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)              ≈⟨ sym $ ⊕-def _ _ ⟩
      ((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z                  ≈⟨ sym $ ⊕-def _ _ ⟨ ⊕-pres ⟩ refl ⟩
      (x ⊕ y) ⊕ z                                ∎
      where
      lem₁ = begin
        ((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)  ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩
        ((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z        ≈⟨ (refl ⟨ ∧-pres-≈ ⟩ sym (deMorgan₁ _ _))
                                                    ⟨ ∨-pres-≈ ⟩ refl ⟩
        ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z          ∎

      lem₂' = begin
        (x ∨ ¬ y) ∧ (¬ x ∨ y)              ≈⟨ sym $
                                                proj₁ ∧-identity _
                                                  ⟨ ∧-pres-≈ ⟩
                                                proj₂ ∧-identity _ ⟩
        (⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤)  ≈⟨ sym $
                                                (proj₁ ∨-complement _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _)
                                                  ⟨ ∧-pres-≈ ⟩
                                                (refl ⟨ ∧-pres-≈ ⟩ proj₁ ∨-complement _) ⟩
        ((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧
        ((¬ x ∨ y) ∧ (¬ y ∨ y))            ≈⟨ sym $ lemma₂ _ _ _ _ ⟩
        (¬ x ∧ ¬ y) ∨ (x ∧ y)              ≈⟨ sym $ deMorgan₂ _ _ ⟨ ∨-pres-≈ ⟩ ¬-involutive _ ⟩
        ¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y)            ≈⟨ sym (deMorgan₁ _ _) ⟩
        ¬ ((x ∨ y) ∧ ¬ (x ∧ y))            ∎

      lem₂ = begin
        ((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)  ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩
        ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z          ≈⟨ lem₂' ⟨ ∨-pres-≈ ⟩ refl ⟩
        ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z          ≈⟨ sym $ deMorgan₁ _ _ ⟩
        ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)          ∎

      lem₃ = begin
        x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))          ≈⟨ refl ⟨ ∨-pres-≈ ⟩
                                                (refl ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _) ⟩
        x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z))        ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
        (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z))  ≈⟨ sym (∨-assoc _ _ _) ⟨ ∧-pres-≈ ⟩
                                              sym (∨-assoc _ _ _) ⟩
        ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)  ∎

      lem₄' = begin
        ¬ ((y ∨ z) ∧ ¬ (y ∧ z))    ≈⟨ deMorgan₁ _ _ ⟩
        ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z)    ≈⟨ deMorgan₂ _ _ ⟨ ∨-pres-≈ ⟩ ¬-involutive _ ⟩
        (¬ y ∧ ¬ z) ∨ (y ∧ z)      ≈⟨ lemma₂ _ _ _ _ ⟩
        ((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧
        ((¬ y ∨ z) ∧ (¬ z ∨ z))    ≈⟨ (proj₁ ∨-complement _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _)
                                        ⟨ ∧-pres-≈ ⟩
                                      (refl ⟨ ∧-pres-≈ ⟩ proj₁ ∨-complement _) ⟩
        (⊤ ∧ (y ∨ ¬ z)) ∧
        ((¬ y ∨ z) ∧ ⊤)            ≈⟨ proj₁ ∧-identity _ ⟨ ∧-pres-≈ ⟩
                                      proj₂ ∧-identity _ ⟩
        (y ∨ ¬ z) ∧ (¬ y ∨ z)      ∎

      lem₄ = begin
        ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))  ≈⟨ deMorgan₁ _ _ ⟩
        ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ refl ⟨ ∨-pres-≈ ⟩ lem₄' ⟩
        ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩
        (¬ x ∨ (y     ∨ ¬ z)) ∧
        (¬ x ∨ (¬ y ∨ z))              ≈⟨ sym (∨-assoc _ _ _) ⟨ ∧-pres-≈ ⟩
                                          sym (∨-assoc _ _ _) ⟩
        ((¬ x ∨ y)     ∨ ¬ z) ∧
        ((¬ x ∨ ¬ y) ∨ z)              ≈⟨ ∧-comm _ _ ⟩
        ((¬ x ∨ ¬ y) ∨ z) ∧
        ((¬ x ∨ y)     ∨ ¬ z)          ∎

      lem₅ = begin
        ((x ∨ ¬ y) ∨ ¬ z) ∧
        (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ sym $ ∧-assoc _ _ _ ⟩
        (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
        ((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ refl ⟩
        (((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
        ((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-assoc _ _ _ ⟩
        ((¬ x ∨ ¬ y) ∨ z) ∧
        (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ∎

  isCommutativeRing : IsCommutativeRing _≈_ _⊕_ _∧_ id ⊥ ⊤
  isCommutativeRing = record
    { isRing = record
      { +-isAbelianGroup = record
        { isGroup = record
          { isMonoid = record
            { isSemigroup = record
              { isEquivalence = isEquivalence
              ; assoc         = ⊕-assoc
              ; ∙-pres-≈      = ⊕-pres
              }
            ; identity = ⊕-identity
            }
          ; inverse   = ⊕-inverse
          ; ⁻¹-pres-≈ = id
          }
        ; comm = ⊕-comm
        }
      ; *-isMonoid = record
        { isSemigroup = record
          { isEquivalence = isEquivalence
          ; assoc         = ∧-assoc
          ; ∙-pres-≈      = ∧-pres-≈
          }
        ; identity = ∧-identity
        }
      ; distrib = distrib-∧-⊕
      }
    ; *-comm = ∧-comm
    }

  commutativeRing : CommutativeRing
  commutativeRing = record
    { _+_               = _⊕_
    ; _*_               = _∧_
    ; -_                = id
    ; 0#                = ⊥
    ; 1#                = ⊤
    ; isCommutativeRing = isCommutativeRing
    }

infixl 6 _⊕_

_⊕_ : Op₂ carrier
x ⊕ y = (x ∨ y) ∧ ¬ (x ∧ y)

module DefaultXorRing = XorRing _⊕_ (λ _ _ → refl)

max_issues_repo_name: larrytheliquid/Lemmachine