text:
open import Prelude
open import Nat
open import core
open import contexts
open import disjointness

-- this module contains lemmas and properties about the holes-disjoint
-- judgement that double check that it acts as we would expect

module holes-disjoint-checks where
  -- these lemmas are all structurally recursive and quite
  -- mechanical. morally, they establish the properties about reduction
  -- that would be obvious / baked into Agda if holes-disjoint was defined
  -- as a function rather than a judgement (datatype), or if we had defined
  -- all the O(n^2) cases rather than relying on a little indirection to
  -- only have O(n) cases. that work has to go somewhwere, and we prefer
  -- that it goes here.
  ds-lem-asc : ∀{e1 e2 τ} → holes-disjoint e2 e1 → holes-disjoint e2 (e1 ·: τ)
  ds-lem-asc HDConst = HDConst
  ds-lem-asc (HDAsc hd) = HDAsc (ds-lem-asc hd)
  ds-lem-asc HDVar = HDVar
  ds-lem-asc (HDLam1 hd) = HDLam1 (ds-lem-asc hd)
  ds-lem-asc (HDLam2 hd) = HDLam2 (ds-lem-asc hd)
  ds-lem-asc (HDHole x) = HDHole (HNAsc x)
  ds-lem-asc (HDNEHole x hd) = HDNEHole (HNAsc x) (ds-lem-asc hd)
  ds-lem-asc (HDAp hd hd₁) = HDAp (ds-lem-asc hd) (ds-lem-asc hd₁)

  ds-lem-lam1 : ∀{e1 e2 x} → holes-disjoint e2 e1 → holes-disjoint e2 (·λ x e1)
  ds-lem-lam1 HDConst = HDConst
  ds-lem-lam1 (HDAsc hd) = HDAsc (ds-lem-lam1 hd)
  ds-lem-lam1 HDVar = HDVar
  ds-lem-lam1 (HDLam1 hd) = HDLam1 (ds-lem-lam1 hd)
  ds-lem-lam1 (HDLam2 hd) = HDLam2 (ds-lem-lam1 hd)
  ds-lem-lam1 (HDHole x₁) = HDHole (HNLam1 x₁)
  ds-lem-lam1 (HDNEHole x₁ hd) = HDNEHole (HNLam1 x₁) (ds-lem-lam1 hd)
  ds-lem-lam1 (HDAp hd hd₁) = HDAp (ds-lem-lam1 hd) (ds-lem-lam1 hd₁)

  ds-lem-lam2 : ∀{e1 e2 x τ} → holes-disjoint e2 e1 → holes-disjoint e2 (·λ x [ τ ] e1)
  ds-lem-lam2 HDConst = HDConst
  ds-lem-lam2 (HDAsc hd) = HDAsc (ds-lem-lam2 hd)
  ds-lem-lam2 HDVar = HDVar
  ds-lem-lam2 (HDLam1 hd) = HDLam1 (ds-lem-lam2 hd)
  ds-lem-lam2 (HDLam2 hd) = HDLam2 (ds-lem-lam2 hd)
  ds-lem-lam2 (HDHole x₁) = HDHole (HNLam2 x₁)
  ds-lem-lam2 (HDNEHole x₁ hd) = HDNEHole (HNLam2 x₁) (ds-lem-lam2 hd)
  ds-lem-lam2 (HDAp hd hd₁) = HDAp (ds-lem-lam2 hd) (ds-lem-lam2 hd₁)

  ds-lem-nehole : ∀{e e1 u} → holes-disjoint e e1 → hole-name-new e u → holes-disjoint e ⦇⌜ e1 ⌟⦈[ u ]
  ds-lem-nehole HDConst ν = HDConst
  ds-lem-nehole (HDAsc hd) (HNAsc ν) = HDAsc (ds-lem-nehole hd ν)
  ds-lem-nehole HDVar ν = HDVar
  ds-lem-nehole (HDLam1 hd) (HNLam1 ν) = HDLam1 (ds-lem-nehole hd ν)
  ds-lem-nehole (HDLam2 hd) (HNLam2 ν) = HDLam2 (ds-lem-nehole hd ν)
  ds-lem-nehole (HDHole x) (HNHole x₁) = HDHole (HNNEHole (flip x₁) x)
  ds-lem-nehole (HDNEHole x hd) (HNNEHole x₁ ν) = HDNEHole (HNNEHole (flip x₁) x) (ds-lem-nehole hd ν)
  ds-lem-nehole (HDAp hd hd₁) (HNAp ν ν₁) = HDAp (ds-lem-nehole hd ν) (ds-lem-nehole hd₁ ν₁)

  ds-lem-ap : ∀{e1 e2 e3} → holes-disjoint e3 e1 → holes-disjoint e3 e2 → holes-disjoint e3 (e1 ∘ e2)
  ds-lem-ap HDConst hd2 = HDConst
  ds-lem-ap (HDAsc hd1) (HDAsc hd2) = HDAsc (ds-lem-ap hd1 hd2)
  ds-lem-ap HDVar hd2 = HDVar
  ds-lem-ap (HDLam1 hd1) (HDLam1 hd2) = HDLam1 (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDLam2 hd1) (HDLam2 hd2) = HDLam2 (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDHole x) (HDHole x₁) = HDHole (HNAp x x₁)
  ds-lem-ap (HDNEHole x hd1) (HDNEHole x₁ hd2) = HDNEHole (HNAp x x₁) (ds-lem-ap hd1 hd2)
  ds-lem-ap (HDAp hd1 hd2) (HDAp hd3 hd4) = HDAp (ds-lem-ap hd1 hd3) (ds-lem-ap hd2 hd4)

  -- holes-disjoint is symmetric
  disjoint-sym : (e1 e2 : hexp) → holes-disjoint e1 e2 → holes-disjoint e2 e1
  disjoint-sym .c c HDConst = HDConst
  disjoint-sym .c (e2 ·: x) HDConst = HDAsc (disjoint-sym _ _ HDConst)
  disjoint-sym .c (X x) HDConst = HDVar
  disjoint-sym .c (·λ x e2) HDConst = HDLam1 (disjoint-sym c e2 HDConst)
  disjoint-sym .c (·λ x [ x₁ ] e2) HDConst = HDLam2 (disjoint-sym c e2 HDConst)
  disjoint-sym .c ⦇-⦈[ x ] HDConst = HDHole HNConst
  disjoint-sym .c ⦇⌜ e2 ⌟⦈[ x ] HDConst = HDNEHole HNConst (disjoint-sym c e2 HDConst)
  disjoint-sym .c (e2 ∘ e3) HDConst = HDAp (disjoint-sym c e2 HDConst) (disjoint-sym c e3 HDConst)

  disjoint-sym _ c (HDAsc hd) = HDConst
  disjoint-sym _ (e2 ·: x) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x) (HDAsc hd) | HDAsc ih = HDAsc (ds-lem-asc ih)
  disjoint-sym _ (X x) (HDAsc hd) = HDVar
  disjoint-sym _ (·λ x e2) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x e2) (HDAsc hd) | HDLam1 ih = HDLam1 (ds-lem-asc ih)
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDAsc hd) | HDLam2 ih = HDLam2 (ds-lem-asc ih)
  disjoint-sym _ ⦇-⦈[ x ] (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇-⦈[ x ] (HDAsc hd) | HDHole x₁ = HDHole (HNAsc x₁)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDAsc hd) | HDNEHole x₁ ih = HDNEHole (HNAsc x₁) (ds-lem-asc ih)
  disjoint-sym _ (e2 ∘ e3) (HDAsc hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDAsc hd) | HDAp ih ih₁ = HDAp (ds-lem-asc ih) (ds-lem-asc ih₁)

  disjoint-sym _ c HDVar = HDConst
  disjoint-sym _ (e2 ·: x₁) HDVar = HDAsc (disjoint-sym _ e2 HDVar)
  disjoint-sym _ (X x₁) HDVar = HDVar
  disjoint-sym _ (·λ x₁ e2) HDVar = HDLam1 (disjoint-sym _ e2 HDVar)
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) HDVar = HDLam2 (disjoint-sym _ e2 HDVar)
  disjoint-sym _ ⦇-⦈[ x₁ ] HDVar = HDHole HNVar
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] HDVar = HDNEHole HNVar (disjoint-sym _ e2 HDVar)
  disjoint-sym _ (e2 ∘ e3) HDVar = HDAp (disjoint-sym _ e2 HDVar) (disjoint-sym _ e3 HDVar)

  disjoint-sym _ c (HDLam1 hd) = HDConst
  disjoint-sym _ (e2 ·: x₁) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x₁) (HDLam1 hd) | HDAsc ih = HDAsc (ds-lem-lam1 ih)
  disjoint-sym _ (X x₁) (HDLam1 hd) = HDVar
  disjoint-sym _ (·λ x₁ e2) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ e2) (HDLam1 hd) | HDLam1 ih = HDLam1 (ds-lem-lam1 ih)
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam1 hd) | HDLam2 ih = HDLam2 (ds-lem-lam1 ih)
  disjoint-sym _ ⦇-⦈[ x₁ ] (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇-⦈[ x₁ ] (HDLam1 hd) | HDHole x = HDHole (HNLam1 x)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam1 hd) | HDNEHole x ih = HDNEHole (HNLam1 x) (ds-lem-lam1 ih)
  disjoint-sym _ (e2 ∘ e3) (HDLam1 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDLam1 hd) | HDAp ih ih₁ = HDAp (ds-lem-lam1 ih) (ds-lem-lam1 ih₁)

  disjoint-sym _ c (HDLam2 hd) = HDConst
  disjoint-sym _ (e2 ·: x₁) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ·: x₁) (HDLam2 hd) | HDAsc ih = HDAsc (ds-lem-lam2 ih)
  disjoint-sym _ (X x₁) (HDLam2 hd) = HDVar
  disjoint-sym _ (·λ x₁ e2) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ e2) (HDLam2 hd) | HDLam1 ih = HDLam1 (ds-lem-lam2 ih)
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x₁ [ x₂ ] e2) (HDLam2 hd) | HDLam2 ih = HDLam2 (ds-lem-lam2 ih)
  disjoint-sym _ ⦇-⦈[ x₁ ] (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇-⦈[ x₁ ] (HDLam2 hd) | HDHole x = HDHole (HNLam2 x)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x₁ ] (HDLam2 hd) | HDNEHole x ih = HDNEHole (HNLam2 x) (ds-lem-lam2 ih)
  disjoint-sym _ (e2 ∘ e3) (HDLam2 hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e2 ∘ e3) (HDLam2 hd) | HDAp ih ih₁ = HDAp (ds-lem-lam2 ih) (ds-lem-lam2 ih₁)

  disjoint-sym _ c (HDHole x) = HDConst
  disjoint-sym _ (e2 ·: x) (HDHole (HNAsc x₁)) = HDAsc (disjoint-sym ⦇-⦈[ _ ] e2 (HDHole x₁))
  disjoint-sym _ (X x) (HDHole x₁) = HDVar
  disjoint-sym _ (·λ x e2) (HDHole (HNLam1 x₁)) = HDLam1 (disjoint-sym ⦇-⦈[ _ ] e2 (HDHole x₁))
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDHole (HNLam2 x₂)) = HDLam2 (disjoint-sym ⦇-⦈[ _ ] e2 (HDHole x₂))
  disjoint-sym _ ⦇-⦈[ x ] (HDHole (HNHole x₁)) =  HDHole (HNHole (flip x₁))
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ u' ] (HDHole (HNNEHole x x₁)) = HDNEHole (HNHole (flip x)) (disjoint-sym ⦇-⦈[ _ ] e2 (HDHole x₁))
  disjoint-sym _ (e2 ∘ e3) (HDHole (HNAp x x₁)) = HDAp (disjoint-sym ⦇-⦈[ _ ] e2 (HDHole x))
                                                    (disjoint-sym ⦇-⦈[ _ ] e3 (HDHole x₁))

  disjoint-sym _ c (HDNEHole x hd) = HDConst
  disjoint-sym _ (e2 ·: x) (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e ·: x) (HDNEHole (HNAsc x₁) hd) | HDAsc ih = HDAsc (ds-lem-nehole ih x₁)
  disjoint-sym _ (X x) (HDNEHole x₁ hd) = HDVar
  disjoint-sym _ (·λ x e2) (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x e2) (HDNEHole (HNLam1 x₁) hd) | HDLam1 ih = HDLam1 (ds-lem-nehole ih x₁)
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDNEHole x₂ hd) with disjoint-sym _ _ hd
  disjoint-sym _ (·λ x [ x₁ ] e2) (HDNEHole (HNLam2 x₂) hd) | HDLam2 ih = HDLam2 (ds-lem-nehole ih x₂)
  disjoint-sym _ ⦇-⦈[ x ] (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇-⦈[ x ] (HDNEHole (HNHole x₂) hd) | HDHole x₁ = HDHole (HNNEHole (flip x₂) x₁)
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDNEHole x₁ hd) with disjoint-sym _ _ hd
  disjoint-sym _ ⦇⌜ e2 ⌟⦈[ x ] (HDNEHole (HNNEHole x₂ x₃) hd) | HDNEHole x₁ ih = HDNEHole (HNNEHole (flip x₂) x₁) (ds-lem-nehole ih x₃)
  disjoint-sym _ (e2 ∘ e3) (HDNEHole x hd) with disjoint-sym _ _ hd
  disjoint-sym _ (e1 ∘ e3) (HDNEHole (HNAp x x₁) hd) | HDAp ih ih₁ = HDAp (ds-lem-nehole ih x) (ds-lem-nehole ih₁ x₁)

  disjoint-sym _ c (HDAp hd hd₁) = HDConst
  disjoint-sym _ (e3 ·: x) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (e3 ·: x) (HDAp hd hd₁) | HDAsc ih | HDAsc ih1 = HDAsc (ds-lem-ap ih ih1)
  disjoint-sym _ (X x) (HDAp hd hd₁) = HDVar
  disjoint-sym _ (·λ x e3) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (·λ x e3) (HDAp hd hd₁) | HDLam1 ih | HDLam1 ih1 = HDLam1 (ds-lem-ap ih ih1)
  disjoint-sym _ (·λ x [ x₁ ] e3) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (·λ x [ x₁ ] e3) (HDAp hd hd₁) | HDLam2 ih | HDLam2 ih1 = HDLam2 (ds-lem-ap ih ih1)
  disjoint-sym _ ⦇-⦈[ x ] (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⦇-⦈[ x ] (HDAp hd hd₁) | HDHole x₁ | HDHole x₂ = HDHole (HNAp x₁ x₂)
  disjoint-sym _ ⦇⌜ e3 ⌟⦈[ x ] (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ ⦇⌜ e3 ⌟⦈[ x ] (HDAp hd hd₁) | HDNEHole x₁ ih | HDNEHole x₂ ih1 = HDNEHole (HNAp x₁ x₂) (ds-lem-ap ih ih1)
  disjoint-sym _ (e3 ∘ e4) (HDAp hd hd₁) with disjoint-sym _ _ hd | disjoint-sym _ _ hd₁
  disjoint-sym _ (e3 ∘ e4) (HDAp hd hd₁) | HDAp ih ih₁ | HDAp ih1 ih2 = HDAp (ds-lem-ap ih ih1) (ds-lem-ap ih₁ ih2)

  -- note that this is false, so holes-disjoint isn't transitive
  -- disjoint-new : ∀{e1 e2 u} → holes-disjoint e1 e2 → hole-name-new e1 u → hole-name-new e2 u

  -- it's also not reflexive, because ⦇-⦈[ u ] isn't hole-disjoint with
  -- itself since refl : u == u; it's also not anti-reflexive, because the
  -- expression c *is* hole-disjoint with itself (albeit vacuously)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


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

module Dodo.Binary.Disjoint where

-- Stdlib imports
open import Level using (Level; _⊔_) renaming (suc to ℓsuc)
open import Data.Empty using (⊥)
open import Data.Product using (_,_)
open import Relation.Unary using (Pred)
open import Relation.Binary using (REL)
open import Data.List using (List; _∷_; []; all; map)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Relation.Nullary using (¬_)
-- Local imports
open import Dodo.Binary.Empty
open import Dodo.Binary.Equality
open import Dodo.Binary.Intersection

-- # Definitions

-- | Predicate stating two binary relations are never inhabited for the same elements.
Disjoint₂ : ∀ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  → REL A B ℓ₁ → REL A B ℓ₂ → Set _
Disjoint₂ P Q = Empty₂ (P ∩₂ Q)

-- | Given a predicate `P`, `Any₂ P xs` states that /at least two/ elements in
-- `xs` satisfy `P`.
data Any₂ {a ℓ : Level} {A : Set a} (P : Pred A ℓ) : Pred (List A) (a ⊔ ℓ) where
  here  : ∀ {x xs} (px : P x) → Any P xs → Any₂ P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any₂ P xs) → Any₂ P (x ∷ xs)

-- | A predicate stating any two predicates in the list cannot be inhabitated for the same elements.
PairwiseDisjoint₁ : {a ℓ : Level} {A : Set a} → List (Pred A ℓ) → Set (a ⊔ ℓsuc ℓ)
PairwiseDisjoint₁ Ps = ∀ {x} → Any₂ (λ{P → P x}) Ps → ⊥

-- | A predicate stating any two binary relations in the list cannot be inhabitated for the same elements.
PairwiseDisjoint₂ : {a b ℓ : Level} {A : Set a} {B : Set b} → List (REL A B ℓ) → Set (a ⊔ b ⊔ ℓsuc ℓ)
PairwiseDisjoint₂ Rs = ∀ {x y} → Any₂ (λ{R → R x y}) Rs → ⊥

-- # Properties

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  -- | If P is disjoint with Q, then Q is surely also disjoint with P.
  disjoint₂-sym : Disjoint₂ P Q → Disjoint₂ Q P
  disjoint₂-sym disjointPQ x y [Q∩P]xy =
    let [P∩Q]xy = ⇔₂-apply-⊆₂ (∩₂-comm {P = Q} {Q = P}) [Q∩P]xy
    in disjointPQ x y [P∩Q]xy

module _ {a b ℓ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ} where

  -- | Every relation is disjoint with its negation.
  disjoint₂-neg : Disjoint₂ P (¬₂ P)
  disjoint₂-neg x y (Pxy , ¬Pxy) = ¬Pxy Pxy

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {P : REL A B ℓ₁} {Q : REL A B ℓ₂} {R : REL A B ℓ₃} where

  -- | If two relations P and Q are disjoint, then any subset R of P is also disjoint with Q.
  disjoint₂-⊆ˡ : R ⊆₂ P → Disjoint₂ P Q → Disjoint₂ R Q
  disjoint₂-⊆ˡ R⊆P disjointPQ x y [R∩Q]xy = disjointPQ x y (⊆₂-apply (∩₂-substˡ-⊆₂ {R = Q} R⊆P) [R∩Q]xy)

  -- | If two relations P and Q are disjoint, then any subset R of Q is also disjoint with P.
  disjoint₂-⊆ʳ : R ⊆₂ Q → Disjoint₂ P Q → Disjoint₂ P R
  disjoint₂-⊆ʳ R⊆Q disjointPQ x y [P∩R]xy = disjointPQ x y (⊆₂-apply (∩₂-substʳ-⊆₂ {R = P} R⊆Q) [P∩R]xy)

ext: agda

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Instances.Pointwise where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Algebra.CommRing.Base
open import Cubical.Algebra.CommRing.Instances.Pointwise
open import Cubical.Algebra.CommAlgebra.Base

private
  variable
    ℓ : Level

pointwiseAlgebra :  {R : CommRing ℓ} (X : Type ℓ) (A : CommAlgebra R ℓ) → CommAlgebra R ℓ
pointwiseAlgebra {R = R} X A =
  let open CommAlgebraStr (snd A)
      isSetX→A = isOfHLevelΠ 2 (λ (x : X) → isSetCommRing (CommAlgebra→CommRing A))
  in commAlgebraFromCommRing
       (pointwiseRing X (CommAlgebra→CommRing A))
       (λ r f → (λ x → r ⋆ (f x)))
       (λ r s f i x → ⋆Assoc r s (f x) i)
       (λ r f g i x → ⋆DistR+ r (f x) (g x) i)
       (λ r s f i x → ⋆DistL+ r s (f x) i)
       (λ f i x → ⋆IdL (f x) i)
       λ r f g i x → ⋆AssocL r (f x) (g x) i

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Experiments.Brunerie where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence

open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Data.Int

open import Cubical.HITs.S1 hiding (encode)
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.Join
open import Cubical.HITs.SetTruncation as SetTrunc
open import Cubical.HITs.GroupoidTruncation as GroupoidTrunc
open import Cubical.HITs.2GroupoidTruncation as 2GroupoidTrunc
open import Cubical.HITs.Truncation as Trunc
open import Cubical.HITs.Susp renaming (toSusp to σ)

open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Hopf
open S¹Hopf

-- This code is adapted from examples/brunerie3.ctt on the pi4s3_nobug branch of cubicaltt

Bool∙ S¹∙ S³∙ : Pointed₀
Bool∙ = (Bool , true)
S¹∙ = (S¹ , base)
S³∙ = (S³ , base)

∥_∥₃∙ ∥_∥₄∙ : Pointed₀ → Pointed₀
∥ A , a ∥₃∙ = ∥ A ∥₃ , ∣ a ∣₃
∥ A , a ∥₄∙ = ∥ A ∥₄ , ∣ a ∣₄

join∙ : Pointed₀ → Type₀ → Pointed₀
join∙ (A , a) B = join A B , inl a

Ω² Ω³ : Pointed₀ → Pointed₀
Ω² = Ω^ 2
Ω³ = Ω^ 3

mapΩrefl : {A : Pointed₀} {B : Type₀} (f : A .fst → B) → Ω A .fst → Ω (B , f (pt A)) .fst
mapΩrefl f p i = f (p i)

mapΩ²refl : {A : Pointed₀} {B : Type₀} (f : A .fst → B) → Ω² A .fst → Ω² (B , f (pt A)) .fst
mapΩ²refl f p i j = f (p i j)

mapΩ³refl : {A : Pointed₀} {B : Type₀} (f : A .fst → B) → Ω³ A .fst → Ω³ (B , f (pt A)) .fst
mapΩ³refl f p i j k = f (p i j k)

meridS² : S¹ → Path S² base base
meridS² base _ = base
meridS² (loop i) j = surf i j

alpha : join S¹ S¹ → S²
alpha (inl x) = base
alpha (inr y) = base
alpha (push x y i) = (meridS² y ∙ meridS² x) i

connectionBoth : {A : Type₀} {a : A} (p : Path A a a) → PathP (λ i → Path A (p i) (p i)) p p
connectionBoth {a = a} p i j =
  hcomp
    (λ k → λ
      { (i = i0) → p (j ∨ ~ k)
      ; (i = i1) → p (j ∧ k)
      ; (j = i0) → p (i ∨ ~ k)
      ; (j = i1) → p (i ∧ k)
      })
    a

data PostTotalHopf : Type₀ where
  base : S¹ → PostTotalHopf
  loop : (x : S¹) → PathP (λ i → Path PostTotalHopf (base x) (base (rotLoop x (~ i)))) refl refl

tee12 : (x : S²) → HopfS² x → PostTotalHopf
tee12 base y = base y
tee12 (surf i j) y =
  hcomp
    (λ k → λ
      { (i = i0) → base y
      ; (i = i1) → base y
      ; (j = i0) → base y
      ; (j = i1) → base (rotLoopInv y (~ i) k)
      })
    (loop (unglue (i ∨ ~ i ∨ j ∨ ~ j) y) i j)

tee34 : PostTotalHopf → join S¹ S¹
tee34 (base x) = inl x
tee34 (loop x i j) =
  hcomp
    (λ k → λ
      { (i = i0) → push x x (j ∧ ~ k)
      ; (i = i1) → push x x (j ∧ ~ k)
      ; (j = i0) → inl x
      ; (j = i1) → push (rotLoop x (~ i)) x (~ k)
      })
    (push x x j)

tee : (x : S²) → HopfS² x → join S¹ S¹
tee x y = tee34 (tee12 x y)

fibΩ : {B : Pointed₀} (P : B .fst → Type₀) → P (pt B) → Ω B .fst → Type₀
fibΩ P f p = PathP (λ i → P (p i)) f f

fibΩ² : {B : Pointed₀} (P : B .fst → Type₀) → P (pt B) → Ω² B .fst → Type₀
fibΩ² P f = fibΩ (fibΩ P f) refl

fibΩ³ : {B : Pointed₀} (P : B .fst → Type₀) → P (pt B) → Ω³ B .fst → Type₀
fibΩ³ P f = fibΩ² (fibΩ P f) refl

Ω³Hopf : Ω³ S²∙ .fst → Type₀
Ω³Hopf = fibΩ³ HopfS² base

fibContrΩ³Hopf : ∀ p → Ω³Hopf p
fibContrΩ³Hopf p i j k =
  hcomp
    (λ m → λ
      { (i = i0) → base
      ; (i = i1) → base
      ; (j = i0) → base
      ; (j = i1) → base
      ; (k = i0) → base
      ; (k = i1) →
        isSetΩS¹ refl refl
          (λ i j → transp (λ n → HopfS² (p i j n)) (i ∨ ~ i ∨ j ∨ ~ j) base)
          (λ _ _ → base)
          m i j
      })
    (transp (λ n → HopfS² (p i j (k ∧ n))) (i ∨ ~ i ∨ j ∨ ~ j ∨ ~ k) base)

h : Ω³ S²∙ .fst → Ω³ (join∙ S¹∙ S¹) .fst
h p i j k = tee (p i j k) (fibContrΩ³Hopf p i j k)

multTwoAux : (x : S²) → Path (Path ∥ S² ∥₄ ∣ x ∣₄ ∣ x ∣₄) refl refl
multTwoAux base i j = ∣ surf i j ∣₄
multTwoAux (surf k l) i j =
  hcomp
    (λ m → λ
      { (i = i0) → ∣ surf k l ∣₄
      ; (i = i1) → ∣ surf k l ∣₄
      ; (j = i0) → ∣ surf k l ∣₄
      ; (j = i1) → ∣ surf k l ∣₄
      ; (k = i0) → ∣ surf i j ∣₄
      ; (k = i1) → ∣ surf i j ∣₄
      ; (l = i0) → ∣ surf i j ∣₄
      ; (l = i1) → squash₄ _ _ _ _ _ _ (λ k i j → step₁ k i j) refl m k i j
      })
    (step₁ k i j)

  where
  step₁ : I → I → I → ∥ S² ∥₄
  step₁ k i j =
    hcomp {A = ∥ S² ∥₄}
      (λ m → λ
        { (i = i0) → ∣ surf k (l ∧ m) ∣₄
        ; (i = i1) → ∣ surf k (l ∧ m) ∣₄
        ; (j = i0) → ∣ surf k (l ∧ m) ∣₄
        ; (j = i1) → ∣ surf k (l ∧ m) ∣₄
        ; (k = i0) → ∣ surf i j ∣₄
        ; (k = i1) → ∣ surf i j ∣₄
        ; (l = i0) → ∣ surf i j ∣₄
        })
     ∣ surf i j ∣₄

multTwoTildeAux : (t : ∥ S² ∥₄) → Path (Path ∥ S² ∥₄ t t) refl refl
multTwoTildeAux ∣ x ∣₄ = multTwoAux x
multTwoTildeAux (squash₄ _ _ _ _ _ _ t u k l m n) i j =
  squash₄ _ _ _ _ _ _
    (λ k l m → multTwoTildeAux (t k l m) i j)
    (λ k l m → multTwoTildeAux (u k l m) i j)
    k l m n

multTwoEquivAux : Path (Path (∥ S² ∥₄ ≃ ∥ S² ∥₄) (idEquiv _) (idEquiv _)) refl refl
multTwoEquivAux i j =
  ( f i j
  , hcomp
      (λ l → λ
        { (i = i0) → isPropIsEquiv _ (idIsEquiv _) (idIsEquiv _) l
        ; (i = i1) → isPropIsEquiv _ (idIsEquiv _) (idIsEquiv _) l
        ; (j = i0) → isPropIsEquiv _ (idIsEquiv _) (idIsEquiv _) l
        ; (j = i1) →
          isPropIsEquiv _
            (transp (λ k → isEquiv (f i k)) (i ∨ ~ i) (idIsEquiv _))
            (idIsEquiv _)
            l
        })
      (transp (λ k → isEquiv (f i (j ∧ k))) (i ∨ ~ i ∨ ~ j) (idIsEquiv _))
  )
  where
  f : I → I → ∥ S² ∥₄ → ∥ S² ∥₄
  f i j t = multTwoTildeAux t i j

tHopf³ : S³ → Type₀
tHopf³ base = ∥ S² ∥₄
tHopf³ (surf i j k) =
  Glue ∥ S² ∥₄
    (λ { (i = i0) → (∥ S² ∥₄ , idEquiv _)
       ; (i = i1) → (∥ S² ∥₄ , idEquiv _)
       ; (j = i0) → (∥ S² ∥₄ , idEquiv _)
       ; (j = i1) → (∥ S² ∥₄ , idEquiv _)
       ; (k = i0) → (∥ S² ∥₄ , multTwoEquivAux i j)
       ; (k = i1) → (∥ S² ∥₄ , idEquiv _)
       })

π₃S³ : Ω³ S³∙ .fst → Ω² ∥ S²∙ ∥₄∙ .fst
π₃S³ p i j = transp (λ k → tHopf³ (p j k i)) i0 ∣ base ∣₄

codeS² : S² → hGroupoid _
codeS² s = ∥ HopfS² s ∥₃ , squash₃

codeTruncS² : ∥ S² ∥₄ → hGroupoid _
codeTruncS² = 2GroupoidTrunc.rec (isOfHLevelTypeOfHLevel 3) codeS²

encodeTruncS² : Ω ∥ S²∙ ∥₄∙ .fst → ∥ S¹ ∥₃
encodeTruncS² p = transp (λ i → codeTruncS² (p i) .fst) i0 ∣ base ∣₃

codeS¹ : S¹ → hSet _
codeS¹ s = ∥ helix s ∥₂ , squash₂

codeTruncS¹ : ∥ S¹ ∥₃ → hSet _
codeTruncS¹ = GroupoidTrunc.rec (isOfHLevelTypeOfHLevel 2) codeS¹

encodeTruncS¹ : Ω ∥ S¹∙ ∥₃∙ .fst → ∥ ℤ ∥₂
encodeTruncS¹ p = transp (λ i → codeTruncS¹ (p i) .fst) i0 ∣ pos zero ∣₂

-- THE BIG GAME

f3 : Ω³ S³∙ .fst → Ω³ (join∙ S¹∙ S¹) .fst
f3 = mapΩ³refl S³→joinS¹S¹

f4 : Ω³ (join∙ S¹∙ S¹) .fst → Ω³ S²∙ .fst
f4 = mapΩ³refl alpha

f5 : Ω³ S²∙ .fst → Ω³ (join∙ S¹∙ S¹) .fst
f5 = h

f6 : Ω³ (join∙ S¹∙ S¹) .fst → Ω³ S³∙ .fst
f6 = mapΩ³refl joinS¹S¹→S³

f7 : Ω³ S³∙ .fst → Ω² ∥ S²∙ ∥₄∙ .fst
f7 = π₃S³

g8 : Ω² ∥ S²∙ ∥₄∙ .fst → Ω ∥ S¹∙ ∥₃∙ .fst
g8 = mapΩrefl encodeTruncS²

g9 : Ω ∥ S¹∙ ∥₃∙ .fst → ∥ ℤ ∥₂
g9 = encodeTruncS¹

g10 : ∥ ℤ ∥₂ → ℤ
g10 = SetTrunc.rec isSetℤ (idfun ℤ)

-- don't run me
brunerie : ℤ
brunerie = g10 (g9 (g8 (f7 (f6 (f5 (f4 (f3 (λ i j k → surf i j k))))))))

-- simpler tests

test63 : ℕ → ℤ
test63 n = g10 (g9 (g8 (f7 (63n n))))
  where
  63n : ℕ → Ω³ S³∙ .fst
  63n zero i j k = surf i j k
  63n (suc n) = f6 (f3 (63n n))

foo : Ω³ S²∙ .fst
foo i j k =
  hcomp
    (λ l → λ
      { (i = i0) → surf l l
      ; (i = i1) → surf l l
      ; (j = i0) → surf l l
      ; (j = i1) → surf l l
      ; (k = i0) → surf l l
      ; (k = i1) → surf l l
      })
    base

sorghum : Ω³ S²∙ .fst
sorghum i j k =
  hcomp
    (λ l → λ
      { (i = i0) → surf j l
      ; (i = i1) → surf k (~ l)
      ; (j = i0) → surf k (i ∧ ~ l)
      ; (j = i1) → surf k (i ∧ ~ l)
      ; (k = i0) → surf j (i ∨ l)
      ; (k = i1) → surf j (i ∨ l)
      })
    (hcomp
      (λ l → λ
        { (i = i0) → base
        ; (i = i1) → surf j l
        ; (j = i0) → surf k i
        ; (j = i1) → surf k i
        ; (k = i0) → surf j (i ∧ l)
        ; (k = i1) → surf j (i ∧ l)
        })
      (surf k i))

goo : Ω³ S²∙ .fst → ℤ
goo x = g10 (g9 (g8 (f7 (f6 (f5 x)))))

{- Computation of an alternative definition of the Brunerie number
based on https://github.com/agda/cubical/pull/741. One should note
that this computation by no means is comparable to the one of the term
"brunerie" defined above. This computation starts in π₃S³ rather than
π₃S². -}

-- The brunerie element can be shown to correspond to the following map
η₃ : (join S¹ S¹ , inl base) →∙ (Susp S² , north)
fst η₃ (inl x) = north
fst η₃ (inr x) = north
fst η₃ (push a b i) =
  (σ (S² , base) (S¹×S¹→S² a b) ∙ σ (S² , base) (S¹×S¹→S² a b)) i
  where
  S¹×S¹→S² : S¹ → S¹ → S²
  S¹×S¹→S² base y = base
  S¹×S¹→S² (loop i) base = base
  S¹×S¹→S² (loop i) (loop j) = surf i j
snd η₃ = refl

K₂ = ∥ S² ∥₄
-- We will need a map Ω (Susp S²) → K₂. It turns out that the
-- following map is fast. It need a bit of work, however. It's
-- esentially the same map as you find in ZCohomology from ΩKₙ₊₁ to
-- Kₙ. This gives another definition of f7 which appears to work better.

module f7stuff where
  _+₂_ : K₂ → K₂ → K₂
  _+₂_ = 2GroupoidTrunc.elim (λ _ → isOfHLevelΠ 4 λ _ → squash₄)
          λ { base x → x
          ; (surf i j) x → surfc x i j}
    where
    surfc : (x : K₂) → typ ((Ω^ 2) (K₂ , x))
    surfc =
      2GroupoidTrunc.elim
        (λ _ → isOfHLevelPath 4 (isOfHLevelPath 4 squash₄ _ _) _ _)
        (S²ToSetElim (λ _ → squash₄ _ _ _ _) λ i j → ∣ surf i j ∣₄)

  K₂≃K₂ : (x : S²) → K₂ ≃ K₂
  fst (K₂≃K₂ x) y = ∣ x ∣₄ +₂ y
  snd (K₂≃K₂ x) = help x
    where
    help : (x : _) → isEquiv (λ y → ∣ x ∣₄ +₂ y)
    help = S²ToSetElim (λ _ → isProp→isSet (isPropIsEquiv _))
                       (idEquiv _ .snd)

  Code : Susp S² → Type ℓ-zero
  Code north = K₂
  Code south = K₂
  Code (merid a i) = ua (K₂≃K₂ a) i

  encode : (x : Susp S²) →  north ≡ x → Code x
  encode x = J (λ x p → Code x) ∣ base ∣₄

-- We now get an alternative definition of f7
f7' : typ (Ω (Susp∙ S²)) → K₂
f7' = f7stuff.encode north

-- We can define the Brunerie number by
brunerie' : ℤ
brunerie' = g10 (g9 (g8 λ i j → f7' λ k → η₃ .fst (push (loop i) (loop j) k)))

-- Computing it takes ~1s
brunerie'≡-2 : brunerie' ≡ -2
brunerie'≡-2 = refl

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


text:
module StalinSort where

  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl)
  open import Data.Nat using (ℕ; _≤_; _≤?_)
  open import Data.List using (List; _∷_; [])
  open import Relation.Nullary using (Dec; yes; no)

  -- Implementation of Stalin Sort
  stalinSort : List ℕ → List ℕ
  stalinSort [] = []
  stalinSort (x ∷ []) = x ∷ []
  stalinSort (x ∷ y ∷ zs) with x ≤? y
  ...| yes m≤n = x ∷ stalinSort (y ∷ zs)
  ...| no m≰n  = stalinSort (x ∷ zs)

  -- Example Test
  _ : stalinSort (2 ∷ 3 ∷ 5 ∷ 4 ∷ 6 ∷ []) ≡ (2 ∷ 3 ∷ 5 ∷ 6 ∷ [])
  _ = refl

  -------------------- Correctness of Stalin Sort -------------------------
  {-
     This section is only interesting for Logic and Formal Verification
     enthusiasts. Although I tried to sketch the formal proof that
     Stalin Sort always returns a Sorted List, there is a point in the proof
     that I couldn't solve yet. I declared it as a postulate, so somebody can
     try improving it by giving an lemma that remove the postulate and
     finish the proof =D
  -}

  -- A proof that x is less than all values in xs (thanks to Twan van Laarhoven)
  data _≤*_ (x : ℕ) : List ℕ → Set where
    []  : x ≤* []
    _∷_ : ∀ {y ys} → (x ≤ y) → y ≤* ys → x ≤* (y ∷ ys)

  -- Proof that a list is sorted (thanks to Twan van Laarhoven)
  data SortedList : List ℕ → Set where
    []  : SortedList []
    _∷_ : ∀ {x xs} → x ≤* xs → SortedList xs → SortedList (x ∷ xs)

  -- This is necessary to prove the correctness, I can't find a way yet ...
  postulate
    less-stalin : ∀ (x y : ℕ) (zs : List ℕ) → x ≤ y → x ≤* stalinSort (y ∷ zs)

  -- Proof that Stalin Sort returns a sorted list
  stalinSort-correctness : ∀ (xs : List ℕ) → SortedList (stalinSort xs)
  stalinSort-correctness [] = []
  stalinSort-correctness (x ∷ []) = [] ∷ []
  stalinSort-correctness (x ∷ y ∷ zs) with x ≤? y
  ...| yes m≤n = less-stalin x y zs m≤n ∷ (stalinSort-correctness (y ∷ zs))
  ...| no m≰n  = stalinSort-correctness (x ∷ zs)

max_stars_repo_name: bluoxy/stalin-sort

max_issues_repo_name: bluoxy/stalin-sort

max_forks_repo_name: bluoxy/stalin-sort


text:
module Data.Bin.Utils where

  open import Data.Digit
  open import Data.Bin hiding (suc)
  open import Data.Fin
  open import Data.List

  _%2 : Bin → Bin
  0# %2 = 0#
  ([] 1#) %2 = [] 1#
  ((zero ∷ _) 1#) %2 = 0#
  ((suc zero ∷ _) 1#) %2 = [] 1#
  ((suc (suc ()) ∷ _) 1#) %2

  bitToBin : Bit → Bin
  bitToBin zero = 0#
  bitToBin (suc zero) = [] 1#
  bitToBin (suc (suc ()))

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
module Properties where

open import Data.Bool
open import Data.Empty
open import Data.Maybe hiding (Any ; All)
open import Data.Nat
open import Data.List
open import Data.List.All
open import Data.List.Any
open import Data.Product
open import Data.Sum
open import Data.Unit

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session
open import Schedule

open import ProcessSyntax
open import ProcessRun

-- adequacy
open import Properties.Base

import Properties.StepBeta
import Properties.StepPair
import Properties.StepFork
import Properties.StepNew
import Properties.StepCloseWait

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


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

open import Categories.Category

--  obtain free properties from duality
module Categories.Diagram.Pushout.Properties {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Data.Product using (∃; _,_)

open import Categories.Category.Cocartesian C
open import Categories.Morphism C
open import Categories.Morphism.Properties C
open import Categories.Morphism.Duality C
open import Categories.Object.Initial C
open import Categories.Object.Terminal op
open import Categories.Object.Coproduct C
open import Categories.Object.Duality C
open import Categories.Diagram.Coequalizer C
open import Categories.Diagram.Pushout C
open import Categories.Diagram.Duality C
open import Categories.Diagram.Pullback op as P′ using (Pullback)
open import Categories.Diagram.Pullback.Properties op

private
  variable
    A B X Y : Obj
    f g h i : A ⇒ B

module _ (p : Pushout f g) where
  open Pushout p

  private
    pullback : Pullback f g
    pullback = Pushout⇒coPullback p

  open Pullback pullback
    using (unique′; id-unique; unique-diagram)
    public

  swap : Pushout g f
  swap = coPullback⇒Pushout (P′.swap pullback)

  glue : Pushout h i₁ → Pushout (h ∘ f) g
  glue p = coPullback⇒Pushout (P′.glue pullback (Pushout⇒coPullback p))

  unglue : Pushout (h ∘ f) g → Pushout h i₁
  unglue p = coPullback⇒Pushout (P′.unglue pullback (Pushout⇒coPullback p))

  Pushout-resp-Epi : Epi g → Epi i₁
  Pushout-resp-Epi epi = P′.Pullback-resp-Mono pullback epi

  Pushout-resp-Iso : Iso g h → ∃ λ j → Iso i₁ j
  Pushout-resp-Iso iso with P′.Pullback-resp-Iso pullback (Iso⇒op-Iso (Iso-swap iso))
  ... | j , record { isoˡ = isoˡ ; isoʳ = isoʳ } = j , record { isoˡ = isoʳ ; isoʳ = isoˡ }

Coproduct×Coequalizer⇒Pushout : (cp : Coproduct A B) →
                                Coequalizer (Coproduct.i₁ cp ∘ f) (Coproduct.i₂ cp ∘ g) →
                                Pushout f g
Coproduct×Coequalizer⇒Pushout cp coe =
  coPullback⇒Pushout (P′.Product×Equalizer⇒Pullback (coproduct→product cp)
                                                    (Coequalizer⇒coEqualizer coe))

Coproduct×Pushout⇒Coequalizer : (cp : Coproduct A B) →
                                Pushout f g →
                                Coequalizer (Coproduct.i₁ cp ∘ f) (Coproduct.i₂ cp ∘ g)
Coproduct×Pushout⇒Coequalizer cp p =
  coEqualizer⇒Coequalizer (P′.Product×Pullback⇒Equalizer (coproduct→product cp)
                                                         (Pushout⇒coPullback p))

module _ (i : Initial) where
  open Initial i
  private
    t : Terminal
    t = ⊥⇒op⊤ i

  pushout-⊥⇒coproduct : Pushout (! {X}) (! {Y}) → Coproduct X Y
  pushout-⊥⇒coproduct p = product→coproduct (pullback-⊤⇒product t (Pushout⇒coPullback p))

  coproduct⇒pushout-⊥ : Coproduct X Y → Pushout (! {X}) (! {Y})
  coproduct⇒pushout-⊥ c = coPullback⇒Pushout (product⇒pullback-⊤ t (coproduct→product c))

pushout-resp-≈ : Pushout f g → f ≈ h → g ≈ i → Pushout h i
pushout-resp-≈ p eq eq′ = coPullback⇒Pushout (pullback-resp-≈ (Pushout⇒coPullback p) eq eq′)

module _ (pushouts : ∀ {X Y Z} (f : X ⇒ Y) (g : X ⇒ Z) → Pushout f g)
         (cocartesian : Cocartesian) where
  open Cocartesian cocartesian
  open Dual

  pushout×cocartesian⇒coequalizer : Coequalizer f g
  pushout×cocartesian⇒coequalizer = coEqualizer⇒Coequalizer
    (pullback×cartesian⇒equalizer (λ f g → Pushout⇒coPullback (pushouts f g)) op-cartesian)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text: module Categories.Monad.Algebras where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module x02induction where

-- prove properties of inductive naturals and operations on them via induction

import      Relation.Binary.PropositionalEquality as Eq
open        Eq             using (_≡_; refl; cong; sym)
open        Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat       using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

{-
------------------------------------------------------------------------------
## Properties of operators : identity, associativity, commutativity, distributivity

* _Identity_.   left/right/both; sometimes called _unit_

* _Associativity_.   e.g., `(m + n) + p ≡ m + (n + p)`

* _Commutativity_.   e.g., `m + n ≡ n + m`

* _Distributivity_.  e.g., from the left  `(m + n) * p ≡ (m * p) + (n * p)`
                           from the right `m * (p + q) ≡ (m * p) + (m * q)`

#### Exercise `operators` (practice) {name=operators} TODO : ops with different properties - no proofs

pair of operators
- have an identity
- are associative, commutative, and distribute over one another
(do not prove)

operator
- has identity
- is associative
- not commutative
(do not prove)
-}

{-
HC not associative; right identity
-}
_ =
  begin
    (3 ∸ 1) ∸ 1 ∸ 0 ≡⟨⟩
     2      ∸ 1 ∸ 0 ≡⟨⟩
     1          ∸ 0 ≡⟨⟩
     1          ∸ 0
  ∎
{-
------------------------------------------------------------------------------
## ASSOCIATIVITY of ADDITION : (m + n) + p ≡ m + (n + p)
-}

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 +  4) + 5  ≡⟨⟩
     7       + 5  ≡⟨⟩
    12            ≡⟨⟩
     3 +  9       ≡⟨⟩
     3 + (4  + 5)
  ∎

{-
useful to read chains like above
- from top down  until reaching simplest term (i.e., `12`)
- from bottom up until reaching the same term

Why should `7 + 5` be the same as `3 + 9`?
Perhaps gather more evidence, testing the proposition by choosing other numbers.
But infinite naturals so testing can never be complete.

## PROOF BY INDUCTION

natural definition has
- base case
- inductive case

inductive proof follows structure of definition: prove two cases
- _base case_ : show property holds for `zero`
- _inductive case_ :
  - assume property holds for an arbitrary natural `m` (the _inductive hypothesis_)
  - then show that the property holds for `suc m`

    ------
    P  zero

    P      m
    ---------
    P (suc m)

- initially, no properties are known.
- base case : `P zero` holds : add it to set of known properties
    -- On the first day, one property is known.
    P zero
- inductive case tells us that if `P m` holds
    -- On the second day, two properties are known.
    P zero
    P (suc zero)
  then `P (suc m)` also holds

    -- On the third day, three properties are known.
    P zero
    P (suc zero)
    P (suc (suc zero))

    -- On the fourth day, four properties are known.
    P zero
    P (suc zero)
    P (suc (suc zero))
    P (suc (suc (suc zero)))

the process continues: property `P n` first appears on day _n+1_

------------------------------------------------------------------------------
## PROVE ASSOCIATIVITY of ADDITION

take `P m` to be the property:

    (m + n) + p ≡ m + (n + p)

`n` and `p` are arbitrary natural numbers

show the equation holds for all `m` it will also hold for all `n` and `p`

    -------------------------------
     (zero + n) + p ≡  zero + (n + p)

        (m + n) + p ≡     m + (n + p)
    ---------------------------------
    (suc m + n) + p ≡ suc m + (n + p)

demonstrate both of above, then associativity of addition follows by induction
-}

-- signature says providing evidence for proposition
+-assoc : ∀ (m n p : ℕ)
        → (m +  n) + p
        ≡  m + (n  + p)

-- Evidence is a function that
-- - takes three natural numbers, binds them to `m`, `n`, and `p`
-- - returns evidence for the corresponding instance of the equation

-- base case : show: (zero +  n) + p
--                  ≡ zero + (n  + p)
+-assoc zero n p =
  begin
  (zero +  n) + p ≡⟨⟩ -- _+_ base case
           n  + p ≡⟨⟩
   zero + (n  + p)
  ∎

-- inductive case : show: (suc m +  n) + p
--                       ≡ suc m + (n  + p)
+-assoc (suc m) n p =
  begin
  (suc   m +  n) + p   ≡⟨⟩ -- _+_ inductive case (left to right)
   suc  (m +  n) + p   ≡⟨⟩
   suc ((m +  n) + p)  ≡⟨ cong suc (+-assoc m n p) ⟩
                           -- simplifying both sides : suc ((m + n) + p) ≡ suc (m + (n + p))
                           -- follows by prefacing `suc` to both sides of the induction hypothesis:
                           --                               (m + n) + p  ≡      m + (n + p)
   suc  (m + (n  + p)) ≡⟨⟩ -- _+_ inductive case (right to left)
   suc   m + (n  + p)
  ∎

-- HC minimal version

+-assoc' : ∀ (m n p : ℕ)
        → (m +  n) + p
        ≡  m + (n  + p)
+-assoc'   zero  n p = refl
+-assoc' (suc m) n p = cong suc (+-assoc m n p)

{-
identifiers can have any characters NOT including spaces or the characters @.(){};_

the "middle" equation, does not follow from applying _+_ (i.e., "simplification") alone
- `_≡⟨_⟩_` : called "chain reasoning"
- justification for equation given in angle brackets:
  - empty means "simplification", or
  - something more, e.g.,:

    ⟨ cong suc (+-assoc m n p) ⟩

recursive invocation `+-assoc m n p`
- has type of the induction hypothesis
- `cong suc` prefaces `suc` to each side of inductive hypothesis

A relation is a CONGRUENCE for a given function
if the relation is preserved by applying the function.

if `e` is evidence that `x ≡ y`, then `cong f e` is evidence `f x ≡ f y`, for any `f`

here the inductive hypothesis is not assumed

instead, proved by recursive invocation of the function being defined, `+-assoc m n p`

WELL FOUNDED : associativity of larger numbers is proved in of associativity of smaller numbers.

e.g., `assoc (suc m) n p` is proved using `assoc m n p`.

------------------------------------------------------------------------------
## Induction as recursion

Concrete example of how induction corresponds to recursion : instantiate `m` to `2`
-}

+-assoc-2 : ∀ (n p : ℕ)
          → (2 +  n) + p
          ≡  2 + (n  + p)
+-assoc-2 n p =
  begin
         (2 +  n) + p   ≡⟨⟩
    suc  (1 +  n) + p   ≡⟨⟩
    suc ((1 +  n) + p)  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc  (1 + (n  + p)) ≡⟨⟩
          2 + (n  + p)
  ∎
 where
  +-assoc-1 : ∀ (n p : ℕ) → (1 + n) + p ≡ 1 + (n + p)
  +-assoc-1 n p =
    begin
           (1 +  n) + p   ≡⟨⟩
      suc  (0 +  n) + p   ≡⟨⟩
      suc ((0 +  n) + p)  ≡⟨ cong suc (+-assoc-0 n p) ⟩
      suc  (0 + (n  + p)) ≡⟨⟩
            1 + (n  + p)
    ∎
   where
    +-assoc-0 : ∀ (n p : ℕ) → (0 + n) + p ≡ 0 + (n + p)
    +-assoc-0 n p =
      begin
        (0 + n) + p  ≡⟨⟩
             n  + p  ≡⟨⟩
        0 + (n  + p)
      ∎
{-
------------------------------------------------------------------------------
## Terminology and notation

Evidence for a universal quantifier is a function.  The notations

    +-assoc : ∀ (m n p : ℕ)
            → (m +  n) + p
            ≡  m + (n  + p)

and

    +-assoc : ∀ (m : ℕ)
            → ∀ (n : ℕ)
            → ∀ (p : ℕ)
            → (m +  n) + p
            ≡  m + (n  + p)

are equivalent.

differ from function type such as `ℕ → ℕ → ℕ`
- variables are associated with each argument type
- the result type may mention (or depend upon) these variables
- hence called _DEPENDENT functions_

------------------------------------------------------------------------------
## COMMUTATIVITY of ADDITION : m + n ≡ n + m

two lemmas used in proof

### first lemma

The base case of the definition of addition states that zero is a left-identity:

    zero + n ≡ n

First lemma states that zero is also a right-identity:
-}

-- proof by induction on `m`
+-identityʳ : ∀ (m : ℕ)
            → m + zero
            ≡ m

-- base case : show:
--    zero + zero
--  ≡ zero
+-identityʳ zero =
  begin
    zero + zero ≡⟨⟩ -- _+_ base
    zero
  ∎

-- inductive case : show:
--     (suc m) + zero
--    = suc m
+-identityʳ (suc m) =
  begin
    suc  m + zero  ≡⟨⟩ -- _+_ inductive
    suc (m + zero) ≡⟨ cong suc (+-identityʳ m) ⟩
                       -- recursive invocation `+-identityʳ m`
                       -- has type of induction hypothesis
                       --      m + zero  ≡     m
                       -- `cong suc` prefaces `suc` to each side of that type, yielding
                       -- suc (m + zero) ≡ suc m
    suc  m
  ∎
{-
### second lemma

inductive case of _+_ pushes `suc` on 1st arg to the outside:

    suc m + n ≡ suc (m + n)

second lemma does same for `suc` on 2nd arg:

    m + suc n ≡ suc (m + n)
-}

-- signature states defining `+-suc` which provides evidence for the proposition/type
+-suc : ∀ (m n : ℕ)
      →      m + suc n
      ≡ suc (m +     n)

-- evidence is fun that takes two nats, binds to `m` and `n`
-- returns evidence for the corresponding instance of the equation
-- proof is by induction on `m`

-- base case
+-suc zero n =
  begin
         zero + suc n  ≡⟨⟩ -- _+_ base
                suc n  ≡⟨⟩ -- _+_ base
    suc (zero +     n)
  ∎
-- inductive case : show:      suc m + suc n
--                      ≡ suc (suc m +     n)
+-suc (suc m) n =
  begin
    suc       m + suc n   ≡⟨⟩                       -- _+_ inductive
    suc      (m + suc n)  ≡⟨ cong suc (+-suc m n) ⟩ -- induction
    suc (suc (m +     n)) ≡⟨⟩                       -- _+_ inductive
    suc (suc  m +     n)
  ∎

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

+-comm : ∀ (m n : ℕ)
       → m + n
       ≡ n + m
+-comm m zero =
  begin
           m + zero ≡⟨ +-identityʳ m ⟩
           m        ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
         m + suc n  ≡⟨ +-suc m n ⟩
    suc (m +     n) ≡⟨ cong suc (+-comm m n) ⟩ -- congruence and induction hypothesis
    suc (n +     m) ≡⟨⟩                        -- _+_ inductive
    suc  n +     m
  ∎

{-
definition required BEFORE using them

------------------------------------------------------------------------------
## COROLLARY: REARRANGING : apply associativity to rearrange parentheses (SYM; sections)
-}

+-rearrange : ∀ (m n p q : ℕ)
            → (m +  n) + (p  + q)
            ≡  m + (n  +  p) + q
+-rearrange m n p q =
  begin
    (m +   n) + (p   + q)  ≡⟨                   +-assoc m n   (p + q) ⟩
     m +  (n  + (p   + q)) ≡⟨ cong (m +_) (sym (+-assoc n p        q)) ⟩
     m + ((n  +  p)  + q)  ≡⟨              sym (+-assoc m (n + p)  q) ⟩
    (m +  (n  +  p)) + q   ≡⟨⟩
     m +  (n  +  p)  + q
  ∎

{-
no induction is required

NOTE:

addition is left associative : m + (n + p)  + q
                            = (m + (n + p)) + q

SYM : interchange sides of an equation, e.g.,
- `+-assoc n p q` shifts parens right to left:

    (n + p) + q ≡ n + (p + q)

`sym (+-assoc n p q)`: to shift them left-to-right

    n + (p + q) ≡ (n + p) + q

general
- if `e` provides evidence for `x ≡ y`
- then `sym e` provides evidence for `y ≡ x`

SECTION NOTATION (introduced by Richard Bird) : `(x +_)`    `(_+ x)`

------------------------------------------------------------------------------
## Creation, one last time

base case : `(zero + n) + p ≡ zero + (n + p)`

inductive case :
- if `(m + n) + p ≡     m + (n + p)` then
 `(suc m + n) + p ≡ suc m + (n + p)`

using base case, associativity of zero on left:
    (0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
using inductive case
    (1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
    (2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...
    (3 + 0) + 0 ≡ 3 + (0 + 0)   ...   (3 + 4) + 5 ≡ 3 + (4 + 5)   ...
    ...

there is a finite approach to generating the same equations (following exercise)

------------------------------------------------------------------------------
#### Exercise `finite-|-assoc` (stretch) {name=finite-plus-assoc} TODO - first four days of creation - description, not proof

Write out what is known about associativity of addition on each of the
first four days using a finite story of creation, as
[earlier](/Naturals/#finite-creation).

------------------------------------------------------------------------------
## proof of ASSOCIATIVITY using `rewrite` (rather than chains of equations)

avoids chains of equations and the need to invoke `cong`
-}

+-assoc′ : ∀ (m n p : ℕ)
         → (m +  n) + p
         ≡  m + (n  + p)

-- base
-- show: (zero + n) + p ≡ zero + (n + p)
-- _+_ base applied "invisibly", then terms equal/refl
+-assoc′ zero    n p                         = refl

-- inductive
-- show: (suc m + n) + p ≡ suc m + (n + p)
-- _+_ inductive applied "invisibly" giving: suc ((m + n) + p) ≡ suc (m + (n + p))
-- rewrite with the inductive hypothesis
-- then terms are equal/refl
+-assoc′ (suc m) n p  rewrite +-assoc′ m n p = refl

{-
rewriting by a given equation
- indicated by keyword `rewrite`
- followed by a proof of that equation

------------------------------------------------------------------------------
## COMMUTATIVITY with rewrite
-}

+-suc′ : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc′ zero n = refl
+-suc′ (suc m) n rewrite +-suc′ m n = refl

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identityʳ m = refl
-- rewriting with two equations indicated by separating the two proofs
-- of the relevant equations by a vertical bar
-- left rewrite performed before right
+-comm′ m (suc n)  -- m + suc n ≡ suc  n + m
                   -- m + suc n ≡ suc (n + m) -- def/eq
  rewrite
    +-suc′  m n    -- suc (m + n) ≡ suc (n + m)
  | +-comm′ m n    -- suc (n + m) ≡ suc (n + m)
  = refl

+-comm′′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′′ m   zero rewrite +-identityʳ m = refl
+-comm′′ m (suc n) =
  begin
    m +  suc n  ≡⟨ +-suc′  m n ⟩
    suc (m + n) ≡⟨ cong suc (+-comm′′ m n) ⟩
    suc (n + m) ≡⟨⟩ -- def/eq
    suc  n + m
  ∎

{-
------------------------------------------------------------------------------
HC
-}

*0 : ∀ (m : ℕ) → m * 0 ≡ 0
*0 zero    = refl
*0 (suc m) = *0 m

0* : ∀ (m : ℕ) → 0 * m ≡ 0
0* m = refl

*1 : ∀ (n : ℕ) → n * 1 ≡ n
*1 zero = refl
*1 (suc n) rewrite *1 n = refl

1* : ∀ (n : ℕ) → 1 * n ≡ n
1* zero = refl
1* (suc n) rewrite 1* n = refl

{-
------------------------------------------------------------------------------
## Building proofs interactively

    +-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
    +-assoc′ m n p = ?

C-c C-l

    +-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
    +-assoc′ m n p = { }0

new window at the bottom:

    ?0 : ((m + n) + p) ≡ (m + (n + p))

indicates hole 0 needs to be filled with a proof of the stated judgment

to prove the proposition by induction on `m`
move cursor into hole
C-c C-c
prompt: pattern variables to case (empty for split on result):

type `m` to case split on that variable

    +-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
    +-assoc′ zero n p = { }0
    +-assoc′ (suc m) n p = { }1

There are now two holes, and the window at the bottom tells you what
each is required to prove:

    ?0 : ((zero + n) + p) ≡ (zero + (n + p))
    ?1 : ((suc m + n) + p) ≡ (suc m + (n + p))

goto hole 0
C-c C-,

    Goal: (n + p) ≡ (n + p)
    ————————————————————————————————————————————————————————————
    p : ℕ
    n : ℕ

indicates that after simplification the goal for hole 0 is as stated,
 and that variables `p` and `n` of the stated types are available to use in the proof.

the proof of the given goal is simple
goto goal
C-c C-r
fills in with refl
C-c C-l renumbers remaining hole to 0:

    +-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
    +-assoc′ zero n p = refl
    +-assoc′ (suc m) n p = { }0

goto hole 0
C-c C-,

    Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
    ————————————————————————————————————————————————————————————
    p : ℕ
    n : ℕ
    m : ℕ

gives simplified goal and available variables

need to rewrite by the induction hypothesis

    +-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
    +-assoc′ zero n p = refl
    +-assoc′ (suc m) n p rewrite +-assoc′ m n p = { }0

goto hole
C-c C-,

    Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
    ————————————————————————————————————————————————————————————
    p : ℕ
    n : ℕ
    m : ℕ

goto goal
C-c C-r
fills in, completing proof

    +-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
    +-assoc′ zero n p = refl
    +-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

------------------------------------------------------------------------------
#### Exercise `+-swap` (recommended) {name=plus-swap}

Show

    m + (n + p) ≡ n + (m + p)

for all naturals `m`, `n`, and `p`
- no induction
- use associativity and commutativity of addtion
-}

+-swap : ∀ (m n p : ℕ)
       → m + (n + p)
       ≡ n + (m + p)
+-swap m n p =
  begin
     m + (n  + p) ≡⟨ sym (+-assoc m n p) ⟩
    (m +  n) + p  ≡⟨ cong (_+ p) (sym (+-comm n m)) ⟩
    (n +  m) + p  ≡⟨ +-assoc n m p ⟩
     n + (m  + p)
  ∎

{-
------------------------------------------------------------------------------
#### Exercise `*-distrib-+` (recommended) {name=times-distrib-plus} (m + n) * p ≡ m * p + n * p
-}

*-distrib-+r : ∀ (m n p : ℕ)
             → (m     + n) * p
             ≡  m * p + n  * p
*-distrib-+r  zero   y z = refl
*-distrib-+r (suc x) y z            -- (suc x     + y) * z  ≡ suc x * z + y * z
                                    -- z + (x     + y) * z  ≡ z + x * z + y * z
  rewrite
    *-distrib-+r x y z              -- z + (x * z + y  * z) ≡ z + x * z + y * z
  | sym (+-assoc z (x * z) (y * z)) -- z +  x * z + y  * z  ≡ z + x * z + y * z
  = refl

{- TODO: agda loops on this : *-distrib-+r done with chain reasoning
*-distrib-+r' : ∀ (m n p : ℕ)
             → (m     + n) * p
             ≡  m * p + n  * p
*-distrib-+r'  zero   y z = refl
*-distrib-+r' (suc x) y z
  begin
    (suc x     + y) * z  ≡⟨⟩
    z + (x     + y) * z  ≡⟨ *-distrib-+r' x y z ⟩
    z + (x * z + y  * z) ≡⟨ sym (+-assoc z (x * z) (y * z)) ⟩
    z +  x * z + y  * z  ≡⟨⟩
     suc x * z + y  * z
  ∎
-}
{-
------------------------------------------------------------------------------
#### Exercise `*-assoc` (recommended) {name=times-assoc} (m * n) * p ≡ m * (n * p)
-}

*-assoc : ∀ (m n p : ℕ)
        → (m *  n) * p
        ≡  m * (n  * p)
-- base case : show: (zero *  n) * p
--                  ≡ zero * (n  * p)
*-assoc zero n p = refl      -- zero * n * p        ≡ zero * (n * p)
                             -- zero                ≡ zero -- def/eq
-- inductive case : show: (suc m *  n) * p
--                       ≡ suc m * (n  * p)
*-assoc (suc m) n p          --     suc m * n  * p  ≡     suc m * (n * p)
                             --    (n + m * n) * p  ≡ n * p + m * (n * p)
  rewrite
    *-distrib-+r n (m * n) p -- n * p + m *  n * p  ≡ n * p + m * (n * p)
  | *-assoc m n p            -- n * p + m * (n * p) ≡ n * p + m * (n * p)
  = refl

{-
------------------------------------------------------------------------------
#### Exercise `*-comm` (practice) {name=times-comm} MULTIPLICATION is COMMUTATIVE : m * n ≡ n * m
-}

*-suc : ∀ (x y : ℕ) → x * (suc y) ≡ x + (x * y)
*-suc zero y = refl
*-suc (suc x) y               --       suc x * suc y  ≡ suc  x +  suc  x * y
                              -- suc (y  + x * suc y) ≡ suc (x + (y +  x * y))
  rewrite
    +-comm y (x * suc y)      -- suc (x  * suc y + y) ≡ suc (x + (y +  x * y))
  | *-suc x y                 -- suc (x + x  * y + y) ≡ suc (x + (y +  x * y))
  | +-comm y (x * y)          -- suc (x + x  * y + y) ≡ suc (x + (x *  y + y))
  | sym (+-assoc x (x * y) y) -- suc (x + x  * y + y) ≡ suc (x +  x *  y + y)
  = refl

*-comm : ∀ (m n : ℕ) → m * n  ≡ n * m
*-comm m zero rewrite *0 m = refl
*-comm m (suc n) -- m * suc n ≡ suc n * m
                 -- m * suc n ≡ m + n * m
  rewrite
    *-suc m n    -- m + m * n ≡ m + n * m
  | *-comm m n   -- m + n * m ≡ m + n * m
  = refl

{-
------------------------------------------------------------------------------
#### Exercise `0∸n≡0` (practice) {name=zero-monus} : Show zero ∸ n ≡ zero

for all naturals `n`. Did your proof require induction?
-}

0∸n≡0 : ∀ (n : ℕ) → 0 ∸ n ≡ 0
0∸n≡0  zero   = refl
0∸n≡0 (suc n) = refl

{-
------------------------------------------------------------------------------
#### Exercise `∸-|-assoc` (practice) {name=monus-plus-assoc} : m ∸ n ∸ p ≡ m ∸ (n + p)

show that monus associates with addition
-}

∸-|-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-|-assoc      m       n   zero   --     m ∸     n ∸ zero   ≡     m ∸     (n + zero)
                                  --     m ∸     n          ≡     m ∸     (n + zero)
  rewrite +-identityʳ n = refl    --     m ∸     n          ≡     m ∸      n
∸-|-assoc      m   zero   (suc p) --     m ∸  zero ∸ suc p  ≡     m ∸  (zero + suc p)
  = refl                          --     m ∸         suc p  ≡     m ∸          suc p
∸-|-assoc  zero   (suc n) (suc p) --  zero ∸ suc n ∸ suc p  ≡  zero ∸ (suc n + suc p)
  = refl                          --  zero                  ≡  zero
∸-|-assoc (suc m) (suc n) (suc p) -- suc m ∸ suc n ∸ suc p  ≡ suc m ∸ (suc n + suc p)
                                  --     m ∸     n ∸ suc p  ≡     m ∸     (n + suc p)
  rewrite
    ∸-|-assoc m n (suc p)         --     m ∸    (n + suc p) ≡     m ∸     (n + suc p)
  = refl

{-
------------------------------------------------------------------------------
#### Exercise `+*^` (stretch)

     m ^ (n  + p) ≡ (m ^  n) * (m ^ p)  (^-distribˡ-|-*)
     (m * n) ^ p  ≡ (m ^  p) * (n ^ p)  (^-distribʳ-*)
     (m ^ n) ^ p  ≡  m ^ (n  *  p)      (^-*-assoc)
-}

-------------------------
-- this can be shortened
^-distribˡ-|-* : ∀ (m n p : ℕ)
               →  m ^ (n  +      p)
               ≡ (m ^  n) * (m ^ p)
^-distribˡ-|-* m n zero              -- (m ^ (n + zero))        ≡ (m ^ n) * (m ^ zero)
                                     -- (m ^ (n + zero))        ≡ (m ^ n) * 1
  rewrite
    +-identityʳ n                    -- (m ^  n)                ≡ (m ^ n) * 1
  | *1 (m ^ n)                       -- (m ^  n)                ≡ (m ^ n)
  = refl
^-distribˡ-|-* m n (suc p)           -- (m ^ (n + suc p))       ≡ (m ^ n) *      (m ^ suc p)
                                     -- (m ^ (n + suc p))       ≡ (m ^ n) * (m * (m ^     p))
  rewrite
    *-comm m (m ^ p)                 -- (m ^ (n + suc p))       ≡ (m ^ n) *     ((m ^     p) * m)
  | sym (*-assoc (m ^ n) (m ^ p) m)  -- (m ^ (n + suc p))       ≡ (m ^ n) *      (m ^     p) * m
  | +-comm n (suc p)                 -- (m ^ suc (p + n))       ≡ (m ^ n) *      (m ^     p) * m
                                     -- m * (m ^ (p + n))       ≡ (m ^ n) *      (m ^     p) * m
  | *-comm ((m ^ n) * (m ^     p)) m -- m * (m ^ (p + n))       ≡  m * ((m ^ n) * (m ^ p))
  | sym (*-assoc m (m ^ n) (m ^ p))  -- m * (m ^ (p + n))       ≡  m *  (m ^ n) * (m ^ p)
  | ^-distribˡ-|-* m p n             -- m * ((m ^ p) * (m ^ n)) ≡  m *  (m ^ n) * (m ^ p)
  | sym (*-comm (m ^ n) (m ^ p))     -- m * ((m ^ n) * (m ^ p)) ≡  m *  (m ^ n) * (m ^ p)
  | *-assoc m (m ^ n) (m ^ p)        -- m * ((m ^ n) * (m ^ p)) ≡  m * ((m ^ n) * (m ^ p))
  = refl

-------------------------
^-distribʳ-* : ∀ (m n p : ℕ)
             → (m * n) ^ p
             ≡ (m ^ p) * (n ^ p)
^-distribʳ-* m n zero = refl
^-distribʳ-* m n (suc p)            --      ((m * n) ^ suc p)      ≡(m ^ suc p) * (n ^ suc p)
                                    -- m * n * ((m      *  n) ^ p) ≡ m * (m ^ p) * (n * (n ^ p))
  rewrite
    ^-distribʳ-* m n p              -- m * n * ((m ^ p) * (n ^ p)) ≡ m * (m ^ p) * (n * (n ^ p))
  | *-comm (m * (m ^ p)) (n * (n ^ p))
                                    -- m * n * ((m ^ p) * (n ^ p)) ≡ n * (n ^ p) * (m * (m ^ p))
  | *-assoc m n ((m ^ p) * (n ^ p)) -- m *(n * ((m ^ p) * (n ^ p)))≡ n * (n ^ p) * (m * (m ^ p))
  | *-comm m (n * ((m ^ p) * (n ^ p)))
                                    -- n *((m ^ p) * (n ^ p))* m  ≡ n * (n ^ p) * (m * (m ^ p))
  | *-comm (m ^ p) (n ^ p)          -- n *((n ^ p) * (m ^ p))* m  ≡ n * (n ^ p) * (m * (m ^ p))
  | sym (*-assoc n (n ^ p) (m ^ p)) -- n * (n ^ p) * (m ^ p) * m  ≡ n * (n ^ p) * (m * (m ^ p))
  | *-assoc n (n ^ p) (m * (m ^ p)) -- n * (n ^ p) * (m ^ p) * m  ≡ n *((n ^ p) * (m * (m ^ p)))
  | *-comm m (m ^ p)                -- n * (n ^ p) * (m ^ p) * m  ≡ n *((n ^ p) * ((m ^ p) * m))
  | *-assoc n (n ^ p) (m ^ p)       -- n *((n ^ p) * (m ^ p))* m  ≡ n *((n ^ p) * ((m ^ p) * m))
  | *-assoc n ((n ^ p) * (m ^ p)) m -- n *((n ^ p) * (m ^ p) * m) ≡ n *((n ^ p) * ((m ^ p) * m))
  | *-assoc (n ^ p) (m ^ p) m       -- n *((n ^ p) *((m ^ p) * m))≡ n *((n ^ p) * ((m ^ p) * m))
  = refl

-------------------------
^-*-assoc : ∀ (m n p : ℕ)
          → (m ^  n) ^ p
          ≡  m ^ (n  * p)
^-*-assoc m n  zero                 --        ((m ^ n) ^ zero) ≡ (m ^ (n * zero))
                                    --                      1  ≡ (m ^ (n * zero))
  rewrite *0 n                      --                      1  ≡ (m ^ 0)
                                    --                      1  ≡ 1
  = refl
^-*-assoc m n (suc p)               --       ((m ^ n) ^ suc p) ≡ (m ^ (n * suc p))
                                    -- (m ^ n) * ((m ^ n) ^ p) ≡ (m ^ (n * suc p))
  rewrite
    *-suc n p                       -- (m ^ n) * ((m ^ n) ^ p) ≡ (m ^ (n + n * p))
  | ^-distribˡ-|-* m n (n * p)      -- (m ^ n) * ((m ^ n) ^ p) ≡ (m ^ n) * (m ^ (n * p))
  | sym (^-*-assoc m n p)           -- (m ^ n) * ((m ^ n) ^ p) ≡ (m ^ n) * ((m ^ n) ^ p)
  = refl

{-
------------------------------------------------------------------------------
#### Exercise `Bin-laws` (stretch) {name=Bin-laws}

Recall that
Exercise [Bin](/Naturals/#Bin)
defines a datatype `Bin` of bitstrings representing natural numbers,
and asks you to define functions
-}

-- begin duplicated from x01 (can't import because of "duplicate" pragma)

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc  ⟨⟩    = ⟨⟩      I
inc (b  O) =      b  I
inc (b  I) = (inc b) O

_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
_ = refl

-- end duplicated

dbl : ℕ → ℕ
dbl   zero  = zero
dbl (suc m) = suc (suc (dbl m))

to : ℕ → Bin
to   zero  = ⟨⟩ O
to (suc m) = inc (to m)

-- THIS IS THE CRITICAL STEP : defining in terms of 'dbl'
-- Got hint from : https://cs.uwaterloo.ca/~plragde/842/
from : Bin → ℕ
from     ⟨⟩ = 0
from (b  O) =      dbl (from b)
from (b  I) = suc (dbl (from b))

_ : to 6 ≡ ⟨⟩ I I O
_ = refl

_ : from (⟨⟩ I I O) ≡ 6
_ = refl

{-
Consider the following laws, where `n` ranges over naturals and `b`
over bitstrings:

    from (inc b) ≡ suc (from b)
    to (from b) ≡ b
    from (to n) ≡ n

For each law: if it holds, prove; if not, give a counterexample.
-}

-------------------------
-- fromInc≡sucFrom

+1 : ∀ (x : ℕ) → x + 1 ≡ suc x
+1 zero = refl
+1 (suc n) rewrite +1 n = refl

fromInc≡sucFrom : ∀ (b : Bin)
                → from (inc b) ≡ suc (from b)
fromInc≡sucFrom ⟨⟩       --       from (inc ⟨⟩)      ≡ suc (from ⟨⟩)
                         --                        1 ≡ 1
  = refl
fromInc≡sucFrom (⟨⟩ I)   --       from (inc (⟨⟩ I))  ≡ suc (from (⟨⟩ I))
                         --                        2 ≡ 2
  = refl
fromInc≡sucFrom (b O)    --       from (inc (b O))   ≡ suc (from (b O))
                         --       dbl (from b) + 1   ≡ suc (dbl (from b))
  rewrite
    +1 (dbl (from b))    --       suc (dbl (from b)) ≡ suc (dbl (from b))
  = refl
fromInc≡sucFrom (b I)    --       from (inc (b I))   ≡ suc (from (b I))
                         --       dbl (from (inc b)) ≡ suc (dbl (from b) + 1)
  rewrite
    +1 (dbl (from b))    --       dbl (from (inc b)) ≡ suc (suc (dbl (from b)))
  | fromInc≡sucFrom b    --       dbl (suc (from b)) ≡ suc (suc (dbl (from b)))
                         -- suc (suc (dbl (from b))) ≡ suc (suc (dbl (from b)))
  = refl

-------------------------
-- to-from≡b -- cannot be proved because there are TWO representations of ZERO

-- NOT USED
xx : ∀ (b : Bin)
   → (dbl (from b)) ≡ from (b O)
xx ⟨⟩        -- dbl (from ⟨⟩) ≡ from (⟨⟩ O)
             -- zero ≡ zero
  = refl
xx (b O)     -- dbl (from (b O)) ≡ from ((b O) O)
             -- dbl (dbl (from b)) ≡ dbl (dbl (from b))
  = refl
xx (b I)     -- dbl (from (b I)) ≡ from ((b I) O)
             -- suc (suc (dbl (dbl (from b)))) ≡ suc (suc (dbl (dbl (from b))))
  = refl

-- CANNOT BE PROVED BECAUSE TWO REPRESENTATIONS OF ZERO : (⟨⟩) and (⟨⟩ O)
yy : ∀ (b : Bin)
   → to (dbl (from b)) ≡ (b O)
yy ⟨⟩        --                  to (dbl (from ⟨⟩)) ≡ (⟨⟩ O)
             --                              (⟨⟩ O) ≡ (⟨⟩ O)
  = refl
yy (b O)     --           to (dbl (from (b O)))     ≡ ((b O) O)
             --           to (dbl (dbl (from b)))   ≡ ((b O) O)
  rewrite
    yy b
  = {!!}
yy (b I)     --           to (dbl (from (b I)))     ≡ ((b I) O)
             -- inc (inc (to (dbl (dbl (from b))))) ≡ ((b I) O)
  = {!!}

to-from : ∀ (b : Bin)
       → to (from b) ≡ b
to-from ⟨⟩       --       to (from ⟨⟩)      ≡ ⟨⟩
                 --               (⟨⟩ O)    ≡ ⟨⟩ -- *****
  = {!!}
to-from (⟨⟩ I)   --       to (from (⟨⟩ I))  ≡ (⟨⟩ I)
                 --       (⟨⟩ I)            ≡ (⟨⟩ I)
  = refl
to-from (b O)    --       to (from (b O))   ≡ (b O)
                 --       to (dbl (from b)) ≡ (b O)
  rewrite
    yy b         --                   (b O) ≡ (b O)
  = refl
to-from (b I)    --         to (from (b I)) ≡ (b I)
                 -- inc (to (dbl (from b))) ≡ (b I)
  rewrite
    yy b         --                   (b I) ≡ (b I)
  = refl

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

-- https://github.com/billyang98/plfa/blob/master/plfa/Induction.agda

from-inc≡suc-from : ∀ x → from (inc x) ≡ suc (from x)
from-inc≡suc-from ⟨⟩    = refl
from-inc≡suc-from (x O) = refl
from-inc≡suc-from (x I)  --         from (inc (x I)) ≡ suc           (from (x I))
                         --    dbl (from (inc  x))   ≡ suc (suc (dbl (from  x)))
  rewrite
    from-inc≡suc-from x  -- suc (suc (dbl (from x))) ≡ suc (suc (dbl (from x)))
  = refl

from-to : ∀ n → from (to n) ≡ n
from-to zero = refl
from-to (suc n)              -- from (to (suc n)) ≡ suc n
                             -- from (inc (to n)) ≡ suc n
  rewrite
    from-inc≡suc-from (to n) -- suc (from (to n)) ≡ suc n
  | cong suc (from-to n)     -- suc           n   ≡ suc n
  = refl

{-
------------------------------------------------------------------------------
## Standard library

Definitions similar to those in this chapter can be found in the standard library:
```
import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)
```

------------------------------------------------------------------------------
## Unicode

This chapter uses the following unicode:

    ∀  U+2200  FOR ALL (\forall, \all)
    ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
    ′  U+2032  PRIME (\')
    ″  U+2033  DOUBLE PRIME (\')
    ‴  U+2034  TRIPLE PRIME (\')
    ⁗  U+2057  QUADRUPLE PRIME (\')

Similar to `\r`, the command `\^r` gives access to a variety of
superscript rightward arrows, and also a superscript letter `r`.
The command `\'` gives access to a range of primes (`′ ″ ‴ ⁗`).
-}

-- ============================================================================

-- this is here to ensure the Bin/in/from/to does not get broken if changed above

_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
_ = refl

_ : inc (⟨⟩     O) ≡ ⟨⟩     I
_ = refl
_ : inc (⟨⟩     I) ≡ ⟨⟩   I O
_ = refl
_ : inc (⟨⟩   I O) ≡ ⟨⟩   I I
_ = refl
_ : inc (⟨⟩   I I) ≡ ⟨⟩ I O O
_ = refl
_ : inc (⟨⟩ I O O) ≡ ⟨⟩ I O I
_ = refl

_ : from (⟨⟩     O) ≡ 0
_ = refl
_ : from (⟨⟩     I) ≡ 1
_ = refl
_ : from (⟨⟩   I O) ≡ 2
_ = refl
_ : from (⟨⟩   I I) ≡ 3
_ = refl
_ : from (⟨⟩ I O O) ≡ 4
_ = refl

_ : to 0 ≡ (⟨⟩     O)
_ = refl
_ : to 1 ≡ (⟨⟩     I)
_ = refl
_ : to 2 ≡ (⟨⟩   I O)
_ = refl
_ : to 3 ≡ (⟨⟩   I I)
_ = refl
_ : to 4 ≡ (⟨⟩ I O O)
_ = refl

_ : from (to 12) ≡ 12
_ = refl

_ : to (from (⟨⟩ I I O O)) ≡ ⟨⟩ I I O O
_ = refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
-- Helper operations to construct and build signatures
module SOAS.Syntax.Build (T : Set) where

open import SOAS.Common
open import SOAS.Families.Build {T}
open import SOAS.Context {T}
open import Data.List.Base

open import SOAS.Syntax.Signature T

-- Syntactic sugar to construct arity - sort mappings
⟼₀_ : T → List (Ctx × T) × T
⟼₀_ τ = [] , τ

_⟼₁_ : (Ctx × T) → T → List (Ctx × T) × T
a ⟼₁ τ = [ a ] , τ

_,_⟼₂_ : (a₁ a₂ : Ctx × T) → T → List (Ctx × T) × T
a₁ , a₂ ⟼₂ τ = (a₁ ∷ [ a₂ ]) , τ

_,_,_⟼₃_ : (a₁ a₂ a₃ : Ctx × T) → T → List (Ctx × T) × T
a₁ , a₂ , a₃ ⟼₃ τ = (a₁ ∷ a₂ ∷ [ a₃ ]) , τ

_,_,_,_⟼₄_ : (a₁ a₂ a₃ a₄ : Ctx × T) → T → List (Ctx × T) × T
a₁ , a₂ , a₃ , a₄ ⟼₄ τ = (a₁ ∷ a₂ ∷ a₃ ∷ [ a₄ ]) , τ

_⟼ₙ_ : List (Ctx × T) → T → List (Ctx × T) × T
_⟼ₙ_ = _,_

-- Syntactic sugar to costruct arguments
⊢₀_ : T → Ctx × T
⊢₀ α = ∅ , α

_⊢₁_ : T → T → Ctx × T
τ ⊢₁ α = ⌊ τ ⌋ , α

_,_⊢₂_ : (τ₁ τ₂ : T) → T → Ctx × T
τ₁ , τ₂ ⊢₂ α = ⌊ τ₁ ∙ τ₂ ⌋ , α

_,_,_⊢₃_ : (τ₁ τ₂ τ₃ : T) → T → Ctx × T
τ₁ , τ₂ , τ₃ ⊢₃ α = ⌊ τ₁ ∙ τ₂ ∙ τ₃ ⌋ , α

_⊢ₙ_ : Ctx → T → Ctx × T
Π ⊢ₙ τ = Π , τ

infix 2 ⟼₀_
infix 2 _⟼₁_
infix 2 _,_⟼₂_
infix 2 _,_,_⟼₃_
infix 2 _⟼ₙ_

infix 10 ⊢₀_
infix 10 _⊢₁_
infix 10 _,_⊢₂_
infix 10 _⊢ₙ_

-- Sum of two signatures
_+ˢ_ : {O₁ O₂ : Set} → Signature O₁ → Signature O₂ → Signature (+₂ O₁ O₂)
S1 +ˢ S2 = sig (₂| ∣ S1 ∣ ∣ S2 ∣)
  where open Signature

-- Sums of signatures
Σ₂ : {O₁ O₂ : Set} → Signature O₁ → Signature O₂ → Signature (+₂ O₁ O₂)
Σ₂ S₁ S₂ = sig (₂| (∣ S₁ ∣) (∣ S₂ ∣))
  where open Signature

Σ₃ : {O₁ O₂ O₃ : Set} → Signature O₁ → Signature O₂ → Signature O₃ → Signature (+₃ O₁ O₂ O₃)
Σ₃ S₁ S₂ S₃ = sig (₃| (∣ S₁ ∣) (∣ S₂ ∣) (∣ S₃ ∣))
  where open Signature

Σ₄ : {O₁ O₂ O₃ O₄ : Set} → Signature O₁ → Signature O₂ → Signature O₃ → Signature O₄ → Signature (+₄ O₁ O₂ O₃ O₄)
Σ₄ S₁ S₂ S₃ S₄ = sig (₄| (∣ S₁ ∣) (∣ S₂ ∣) (∣ S₃ ∣) (∣ S₄ ∣))
  where open Signature

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module ANF  where

open import Data.Nat
open import Data.Vec
open import Data.Fin
open import Data.String
open import Data.Rational
open import Data.Sum
open import Data.Unit

open import Binders.Var

record DataConApp (universe a : Set) : Set  where
         constructor _#_◂_
         -- theres probably room for a better notation :)))

         field
--            universe : Set
           arity : ℕ
           schema : Vec universe arity
           app  : Vec a arity

mutual
    data term (a : Set ) : Set where
      v : a -> term a -- variables return only appears in "tail" position
      app : ∀ (n : ℕ ) ->  Callish a n   -> term a
      letCall : ∀ (n : ℕ ) -> Callish a n    -> term (Var (Fin n) a)  -> term a
      letAlloc :  Allocish a 1 -> term (Var (Fin 1) a) -> term a
    -- for now we only model direct allocations have having a single return value ...

    data Allocish (a : Set) : ℕ  -> Set  where
      lam : ∀ (n : ℕ ) ->  term (Var (Fin n) (term a)) -> Allocish  a 1
      delay : term a -> Allocish  a 1
      dataConstr : DataConApp ⊤ {- for now using unit as the universe -} a -> Allocish a 1

    data Callish  (a : Set) : ℕ ->  Set where
      force : a -> Callish a 0
      call : ∀ {n } ->  a -> Vec a n -> Callish a n
      primCall : ∀ {n } ->  String ->  Vec a n -> Callish a n


text:
{-# OPTIONS --postfix-projections #-}

module StateSized.cellStateDependent where

open import Data.Product
open import Data.String.Base

{-
open import SizedIO.Object
open import SizedIO.ConsoleObject
-}

open import SizedIO.Console hiding (main)

open import SizedIO.Base

open import NativeIO

open import StateSizedIO.Object
open import StateSizedIO.IOObject

open import Size
open import StateSizedIO.cellStateDependent

{- I moved most into src/StateSizedIO/cellStateDependent.agda

now the code doesn't work
-}

-- Program is another program
program : IOConsole ∞ Unit
program =
  let c₀ = cellPempty ∞  in
  exec getLine            λ str →
  method c₀ (put str)    >>= λ{ (_ , c₁) →        -- empty
  method c₁ get          >>= λ{ (str₁ , c₂) →     -- full
  exec (putStrLn ("we got " ++ str₁))    λ _ →
  exec (putStrLn ("Second Round"))    λ _ →
  exec getLine            λ str₂ →
  method c₂ (put str₂)    >>= λ{ (_ , c₃) →
  method c₃ get          >>= λ{ (str₃ , c₄) →
  exec (putStrLn ("we got " ++ str₃)  ) λ _ →
  return unit
  }}}}

main : NativeIO Unit
main = translateIOConsole program

-- cellP is constructor for the consoleObject for interface (cellI String)
{-
cellPˢ : ∀{i} → CellCˢ i
force (method cellPˢ (put x)) = {!!}
-}

{-
cellP : ∀{i} (s : String) → CellC i
force (method (cellP s) get) =
  exec' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  return (s , cellP s)
force (method (cellP s) (put x)) =
  exec' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
  return (_ , (cellP x))
-}

{-
-- cellI is the interface of the object of a simple cell
cellI : (A : Set) → Interfaceˢ
Method  (cellI A)    =  CellMethodˢ A
Result  (cellI A) m  =  CellResultˢ m

-- cellC is the type of consoleObjects with interface (cellI String)
CellC : (i : Size) → Set
CellC i = ConsoleObject i (cellI String)
-}
{-
-- cellO is a program for a simple cell which
-- when get is called writes "getting s" for the string s of the object
-- and when putting s writes "putting s" for the string

-- cellP is constructor for the consoleObject for interface (cellI String)
cellP : ∀{i} (s : String) → CellC i
force (method (cellP s) get) =
  exec' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  return (s , cellP s)
force (method (cellP s) (put x)) =
  exec' (putStrLn ("putting (" ++ x ++ ")")) λ _ →
  return (_ , (cellP x))

-- Program is another program
program : String → IOConsole ∞ Unit
program arg =
  let c₀ = cellP "Start" in
  method c₀ get       >>= λ{ (s , c₁) →
  exec1 (putStrLn s)         >>
  method c₁ (put arg) >>= λ{ (_ , c₂) →
  method c₂ get       >>= λ{ (s' , c₃) →
  exec1 (putStrLn s')        }}}

main : NativeIO Unit
main = translateIOConsole (program "hello")
-}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Logic.Propositional.Xor where

open import Logic.Propositional
open import Logic
import      Lvl

-- TODO: Is it possible write a general construction for arbitrary number of xors? Probably by using rotate₃Fn₃Op₂?
data _⊕₃_⊕₃_ {ℓ₁ ℓ₂ ℓ₃} (P : Stmt{ℓ₁}) (Q : Stmt{ℓ₂}) (R : Stmt{ℓ₃}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
  [⊕₃]-intro₁ : P     → (¬ Q) → (¬ R) → (P ⊕₃ Q ⊕₃ R)
  [⊕₃]-intro₂ : (¬ P) → Q     → (¬ R) → (P ⊕₃ Q ⊕₃ R)
  [⊕₃]-intro₃ : (¬ P) → (¬ Q) → R     → (P ⊕₃ Q ⊕₃ R)

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:
module _ where

open import Agda.Builtin.Bool

postulate Eq : Set → Set

it : {A : Set} → ⦃ A ⦄ → A
it ⦃ x ⦄ = x

module M1 (A : Set) ⦃ eqA : Eq A ⦄ where
  postulate B : Set
  variable  n : B
  postulate P : B → Set

module M2 (A : Set) ⦃ eqA : Eq A ⦄ where
  open M1 A
  postulate
    p₁ : P n
    p₂ : P ⦃ it ⦄ n
    p₃ : P ⦃ eqA ⦄ n
    p₄ : M1.P A n

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
record R : Set₁ where
  field
    A : Set

module _ (r : R) where

  open R r

  data D : Set where
    c : A → D

  data P : D → Set where
    d : (x : A) → P (c x)

  postulate
    f : D → A

  g : (x : D) → P x → D
  g x (d y) with Set
  g x (d y) | _ = x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
postulate
  A : Set
  f : A → A → A → A → A → A → A → A → A → A → A

test : A
test = {!f!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

open import Level
open import Categories.Category using (Category; _[_,_])

-- Various conclusions that can be drawn from Yoneda
-- over a particular Category C
module Categories.Yoneda.Properties {o ℓ e : Level} (C : Category o ℓ e) where

open import Function using (_$_; Inverse) -- else there's a conflict with the import below
open import Function.Equality using (Π; _⟨$⟩_; cong)
open import Relation.Binary using (module Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR
open import Data.Product using (_,_; Σ)

open import Categories.Category.Product
open import Categories.Category.Construction.Presheaves
open import Categories.Category.Construction.Functors
open import Categories.Category.Instance.Setoids
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Hom using (module Hom; Hom[_][-,_]; Hom[_][-,-])
open import Categories.Functor.Bifunctor
open import Categories.Functor.Presheaf
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Yoneda

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.NaturalTransformation.Hom as NT-Hom

open Category C
open HomReasoning
open NaturalTransformation
open Yoneda C
private
  module CE = Category.Equiv C
  module C = Category C

YoFull : Full embed
YoFull {X} {Y} = record
  { from             = record { _⟨$⟩_ = λ ε → η ε X ⟨$⟩ id ; cong = λ i≈j → i≈j CE.refl }
  ; right-inverse-of = λ ε {x} {z} {y} z≈y →
    begin
      (η ε X ⟨$⟩ id) ∘ z      ≈˘⟨ identityˡ ⟩
      id ∘ (η ε X ⟨$⟩ id) ∘ z ≈˘⟨ commute ε z CE.refl ⟩
      η ε x ⟨$⟩ id ∘ id ∘ z   ≈⟨ cong (η ε x) (identityˡ ○ identityˡ ○ z≈y) ⟩
      η ε x ⟨$⟩ y             ∎
  }

YoFaithful : Faithful embed
YoFaithful _ _ pres-≈ = ⟺ identityʳ ○ pres-≈ {_} {id} CE.refl ○ identityʳ

YoFullyFaithful : FullyFaithful embed
YoFullyFaithful = YoFull , YoFaithful

open Mor C

yoneda-iso : ∀ {A B : Obj} → NaturalIsomorphism Hom[ C ][-, A ] Hom[ C ][-, B ] → A ≅ B
yoneda-iso {A} {B} niso = record
  { from = ⇒.η A ⟨$⟩ id
  ; to   = ⇐.η B ⟨$⟩ id
  ; iso  = record
    { isoˡ = begin
      (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
      id ∘ (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id) ≈⟨  B⇒A.inverseʳ F⇐G refl  ⟩
      ⇐.η A ⟨$⟩ (⇒.η A ⟨$⟩ id)             ≈⟨ isoX.isoˡ refl ⟩
      id                                   ∎
    ; isoʳ = begin
      (⇒.η A ⟨$⟩ id) ∘ (⇐.η B ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
      id ∘ (⇒.η A ⟨$⟩ id) ∘ (⇐.η B ⟨$⟩ id) ≈⟨  A⇒B.inverseʳ F⇒G refl  ⟩
      ⇒.η B ⟨$⟩ (⇐.η B ⟨$⟩ id)             ≈⟨ isoX.isoʳ refl ⟩
      id                                   ∎
    }
  }
  where open NaturalIsomorphism niso
        A⇒B = yoneda-inverse A (Functor.F₀ embed B)
        B⇒A = yoneda-inverse B (Functor.F₀ embed A)
        module A⇒B = Inverse A⇒B
        module B⇒A = Inverse B⇒A
        module isoX {X} = Mor.Iso (iso X)

module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where
  private
    module D = Category D

    module _ {F G : Functor D C} where
      private
        module F = Functor F
        module G = Functor G
        Hom[-,F-] : Bifunctor C.op D (Setoids ℓ e)
        Hom[-,F-] = Hom[ C ][-,-] ∘F (idF ⁂ F)

        Hom[-,G-] : Bifunctor C.op D (Setoids ℓ e)
        Hom[-,G-] = Hom[ C ][-,-] ∘F (idF ⁂ G)

      nat-appʳ : ∀ X → NaturalTransformation Hom[-,F-] Hom[-,G-] →
                       NaturalTransformation Hom[ C ][-, F.F₀ X ] Hom[ C ][-, G.F₀ X ]
      nat-appʳ X α = ntHelper record
        { η       = λ Y → η α (Y , X)
        ; commute = λ {_ Y} f eq → cong (η α (Y , X)) (∘-resp-≈ˡ (⟺ F.identity)) ○ commute α (f , D.id) eq ○ ∘-resp-≈ˡ G.identity
        }

      transform : NaturalTransformation Hom[-,F-] Hom[-,G-] → NaturalTransformation F G
      transform α = ntHelper record
        { η       = λ X → η α (F.F₀ X , X) ⟨$⟩ id
        ; commute = λ {X Y} f → begin
          (η α (F.F₀ Y , Y) ⟨$⟩ id) ∘ F.F₁ f      ≈˘⟨ identityˡ ⟩
          id ∘ (η α (F.F₀ Y , Y) ⟨$⟩ id) ∘ F.F₁ f ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, G.F₀ Y ] , _} (idN , F.F₁ f) {nat-appʳ Y α} {nat-appʳ Y α} (cong (η α _))) ⟩
          η α (F.F₀ X , Y) ⟨$⟩ F.F₁ f ∘ id        ≈⟨ cong (η α (F.F₀ X , Y)) (∘-resp-≈ʳ (⟺ identityˡ)) ⟩
          η α (F.F₀ X , Y) ⟨$⟩ F.F₁ f ∘ id ∘ id   ≈⟨ commute α (id , f) refl ⟩
          G.F₁ f ∘ (η α (F.F₀ X , X) ⟨$⟩ id) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
          G.F₁ f ∘ (η α (F.F₀ X , X) ⟨$⟩ id)      ∎
        }

  module _ (F G : Functor D C) where
    private
      module F = Functor F
      module G = Functor G
      Hom[-,F-] : Bifunctor C.op D (Setoids ℓ e)
      Hom[-,F-] = Hom[ C ][-,-] ∘F (idF ⁂ F)

      Hom[-,G-] : Bifunctor C.op D (Setoids ℓ e)
      Hom[-,G-] = Hom[ C ][-,-] ∘F (idF ⁂ G)

    yoneda-NI : NaturalIsomorphism Hom[-,F-] Hom[-,G-] → NaturalIsomorphism F G
    yoneda-NI ni = record
      { F⇒G = transform F⇒G
      ; F⇐G = transform F⇐G
      ; iso = λ X → record
        { isoˡ = begin
          (⇐.η (G.F₀ X , X) ⟨$⟩ id) ∘ (⇒.η (F.F₀ X , X) ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
          id ∘ (⇐.η (G.F₀ X , X) ⟨$⟩ id) ∘ (⇒.η (F.F₀ X , X) ⟨$⟩ id) ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, F.F₀ X ] , _} (idN , (⇒.η (F.F₀ X , X) ⟨$⟩ C.id))
                                                                                {nat-appʳ X F⇐G} {nat-appʳ X F⇐G} (cong (⇐.η _))) ⟩
          ⇐.η (F.F₀ X , X) ⟨$⟩ (⇒.η (F.F₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ cong (⇐.η _) identityʳ ⟩
          ⇐.η (F.F₀ X , X) ⟨$⟩ (⇒.η (F.F₀ X , X) ⟨$⟩ id)             ≈⟨ iso.isoˡ _ refl ⟩
          id                                                         ∎
        ; isoʳ = begin
          (⇒.η (F.F₀ X , X) ⟨$⟩ id) ∘ (⇐.η (G.F₀ X , X) ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
          id ∘ (⇒.η (F.F₀ X , X) ⟨$⟩ id) ∘ (⇐.η (G.F₀ X , X) ⟨$⟩ id) ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, G.F₀ X ] , _} (idN , (⇐.η (G.F₀ X , X) ⟨$⟩ C.id))
                                                                                {nat-appʳ X F⇒G} {nat-appʳ X F⇒G} (cong (⇒.η _))) ⟩
          ⇒.η (G.F₀ X , X) ⟨$⟩ (⇐.η (G.F₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ cong (⇒.η _) identityʳ ⟩
          ⇒.η (G.F₀ X , X) ⟨$⟩ (⇐.η (G.F₀ X , X) ⟨$⟩ id)             ≈⟨ iso.isoʳ _ refl ⟩
          id                                                         ∎
        }
      }
      where open NaturalIsomorphism ni


text:
------------------------------------------------------------------------
-- A virtual machine
------------------------------------------------------------------------

open import Prelude

import Lambda.Virtual-machine.Instructions

module Lambda.Virtual-machine
  {Name : Type}
  (open Lambda.Virtual-machine.Instructions Name)
  (def : Name → Code 1)
  where

open import Equality.Propositional

open import Colist equality-with-J as Colist using (Colist)
open import List equality-with-J using (_++_; length)
open import Monad equality-with-J
open import Vec.Data equality-with-J

open import Lambda.Delay-crash using (Delay-crash)
open import Lambda.Delay-crash-trace
open import Lambda.Syntax Name

open Closure Code

-- A single step of the computation.

step : State → Result
step ⟨ var x     ∷ c ,                           s  , ρ  ⟩ = continue ⟨ c       , val (index ρ x) ∷ s ,     ρ  ⟩
step ⟨ clo c′    ∷ c ,                           s  , ρ  ⟩ = continue ⟨ c       , val (lam c′ ρ)  ∷ s ,     ρ  ⟩
step ⟨ app       ∷ c , val v ∷ val (lam c′ ρ′) ∷ s  , ρ  ⟩ = continue ⟨ c′      , ret c ρ         ∷ s , v ∷ ρ′ ⟩
step ⟨ ret       ∷ c , val v ∷       ret c′ ρ′ ∷ s  , ρ  ⟩ = continue ⟨ c′      , val v           ∷ s ,     ρ′ ⟩
step ⟨ cal f     ∷ c ,                   val v ∷ s  , ρ  ⟩ = continue ⟨ def f   , ret c ρ         ∷ s , v ∷ [] ⟩
step ⟨ tcl f     ∷ c ,                   val v ∷ s  , ρ  ⟩ = continue ⟨ def f   ,                   s , v ∷ [] ⟩
step ⟨ con b     ∷ c ,                           s  , ρ  ⟩ = continue ⟨ c       , val (con b)     ∷ s ,     ρ  ⟩
step ⟨ bra c₁ c₂ ∷ c ,         val (con true)  ∷ s  , ρ  ⟩ = continue ⟨ c₁ ++ c ,                   s ,     ρ  ⟩
step ⟨ bra c₁ c₂ ∷ c ,         val (con false) ∷ s  , ρ  ⟩ = continue ⟨ c₂ ++ c ,                   s ,     ρ  ⟩
step ⟨ []            ,                   val v ∷ [] , [] ⟩ = done v
step _                                                     = crash

-- A functional semantics for the VM. The result includes a trace of
-- all the encountered states.

mutual

  exec⁺ : ∀ {i} → State → Delay-crash-trace State Value i
  exec⁺ s = later s λ { .force → exec⁺′ (step s) }

  exec⁺′ : ∀ {i} → Result → Delay-crash-trace State Value i
  exec⁺′ (continue s) = exec⁺ s
  exec⁺′ (done v)     = now v
  exec⁺′ crash        = crash

-- The semantics without the trace of states.

exec : ∀ {i} → State → Delay-crash Value i
exec = delay-crash ∘ exec⁺

-- The stack sizes of all the encountered states.

stack-sizes : ∀ {i} → State → Colist ℕ i
stack-sizes =
  Colist.map (λ { ⟨ _ , s , _ ⟩ → length s }) ∘ trace ∘ exec⁺

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
module Rewrite where

open import Common.Equality

data _≈_ {A : Set}(x : A) : A → Set where
  refl : ∀ {y} → x ≈ y

lem : ∀ {A} (x y : A) → x ≈ y
lem x y = refl

thm : {A : Set}(P : A → Set)(x y : A) → P x → P y
thm P x y px rewrite lem x y = {!!}

max_forks_repo_name: Agda-zh/agda


text: module Issue3818.M where


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[Am[X]]-Anm[X] where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Univariate.Base

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly

private variable
  ℓ ℓ' : Level

module Comp-Poly-nm (A' : CommRing ℓ) (n m : ℕ) where
  private
    A = fst A'
  open CommRingStr (snd A')

  module Mr  = Nth-Poly-structure A' m
  module N+Mr = Nth-Poly-structure A' (n +n m)
  module N∘Mr  = Nth-Poly-structure (PolyCommRing A' m) n

-----------------------------------------------------------------------------
-- direct sens

  N∘M→N+M-b : (v : Vec ℕ n) → Poly A' m → Poly A' (n +n m)
  N∘M→N+M-b v = Poly-Rec-Set.f A' m (Poly A' (n +n m)) trunc
                0P
                (λ v' a → base (v ++ v') a)
                _poly+_
                poly+Assoc
                poly+IdR
                poly+Comm
                (λ v' → base-0P (v ++ v'))
                (λ v' a b → base-poly+ (v ++ v') a b)

  N∘M→N+M : Poly (PolyCommRing A' m) n → Poly A' (n +n m)
  N∘M→N+M = Poly-Rec-Set.f (PolyCommRing A' m) n (Poly A' (n +n m)) trunc
           0P
           N∘M→N+M-b
           _poly+_
           poly+Assoc
           poly+IdR
           poly+Comm
           (λ _ → refl)
           (λ v a b → refl)

-- -----------------------------------------------------------------------------
-- -- Converse sens

  N+M→N∘M : Poly A' (n +n m) → Poly (PolyCommRing A' m) n
  N+M→N∘M = Poly-Rec-Set.f A' (n +n m) (Poly (PolyCommRing A' m) n) trunc
            0P
            (λ v a → let v , v'  = sep-vec n m v in
                      base v (base v' a))
            _poly+_
            poly+Assoc
            poly+IdR
            poly+Comm
            (λ v → (cong (base (fst (sep-vec n m v))) (base-0P (snd (sep-vec n m v)))) ∙ (base-0P (fst (sep-vec n m v))))
            λ v a b → base-poly+ (fst (sep-vec n m v)) (base (snd (sep-vec n m v)) a) (base (snd (sep-vec n m v)) b)
                       ∙ cong (base (fst (sep-vec n m v))) (base-poly+ (snd (sep-vec n m v)) a b)

-----------------------------------------------------------------------------
-- Section

  e-sect : (P : Poly A' (n +n m)) → N∘M→N+M (N+M→N∘M P) ≡ P
  e-sect = Poly-Ind-Prop.f A' (n +n m)
           (λ P → N∘M→N+M (N+M→N∘M P) ≡ P)
           (λ _ → trunc _ _)
           refl
           (λ v a → cong (λ X → base X a) (sep-vec-id n m v))
           (λ {U V} ind-U ind-V → cong₂ _poly+_ ind-U ind-V)

-----------------------------------------------------------------------------
-- Retraction

  e-retr : (P : Poly (PolyCommRing A' m) n) → N+M→N∘M (N∘M→N+M P) ≡ P
  e-retr = Poly-Ind-Prop.f (PolyCommRing A' m) n
           (λ P → N+M→N∘M (N∘M→N+M P) ≡ P)
           (λ _ → trunc _ _)
           refl
           (λ v → Poly-Ind-Prop.f A' m
                   (λ P → N+M→N∘M (N∘M→N+M (base v P)) ≡ base v P)
                   (λ _ → trunc _ _)
                   (sym (base-0P v))
                   (λ v' a → cong₂ base (sep-vec-fst n m v v') (cong (λ X → base X a) (sep-vec-snd n m v v')))
                   (λ {U V} ind-U ind-V → (cong₂ _poly+_ ind-U ind-V) ∙ (base-poly+ v U V)))
           (λ {U V} ind-U ind-V → cong₂ _poly+_ ind-U ind-V )

-----------------------------------------------------------------------------
-- Morphism of ring

  map-0P : N∘M→N+M (0P) ≡ 0P
  map-0P = refl

  N∘M→N+M-gmorph : (P Q : Poly (PolyCommRing A' m) n) → N∘M→N+M ( P poly+ Q) ≡ N∘M→N+M P poly+ N∘M→N+M Q
  N∘M→N+M-gmorph = λ P Q → refl

  map-1P : N∘M→N+M (N∘Mr.1P) ≡ N+Mr.1P
  map-1P = cong (λ X → base X 1r) (rep-concat n m 0 )

  N∘M→N+M-rmorph : (P Q : Poly (PolyCommRing A' m) n) → N∘M→N+M ( P N∘Mr.poly* Q) ≡ N∘M→N+M P N+Mr.poly* N∘M→N+M Q
  N∘M→N+M-rmorph =
    -- Ind P
    Poly-Ind-Prop.f (PolyCommRing A' m) n
    (λ P → (Q : Poly (PolyCommRing A' m) n) → N∘M→N+M (P N∘Mr.poly* Q) ≡ (N∘M→N+M P N+Mr.poly* N∘M→N+M Q))
    (λ P p q i Q j → trunc _ _ (p Q) (q Q) i j)
    (λ Q → refl)
    (λ v → -- Ind Base P
           Poly-Ind-Prop.f A' m
           (λ P → (Q : Poly (PolyCommRing A' m) n) → N∘M→N+M (base v P N∘Mr.poly* Q) ≡ (N∘M→N+M (base v P) N+Mr.poly* N∘M→N+M Q))
           (λ P p q i Q j → trunc _ _ (p Q) (q Q) i j)
           (λ Q → cong (λ X → N∘M→N+M (X N∘Mr.poly* Q)) (base-0P v))
           (λ v' a → -- Ind Q
                      Poly-Ind-Prop.f (PolyCommRing A' m) n
                      (λ Q → N∘M→N+M (base v (base v' a) N∘Mr.poly* Q) ≡ (N∘M→N+M (base v (base v' a)) N+Mr.poly* N∘M→N+M Q))
                      (λ _ → trunc _ _)
                      (sym (N+Mr.poly*AnnihilR (N∘M→N+M (base v (base v' a)))))
                      (λ w → -- Ind base Q
                              Poly-Ind-Prop.f A' m
                              _
                              (λ _ → trunc _ _)
                              (sym (N+Mr.poly*AnnihilR (N∘M→N+M (base v (base v' a)))))
                              (λ w' b → cong (λ X → base X (a · b)) (+n-vec-concat n m v w v' w'))
                              λ {U V} ind-U ind-V → cong (λ X → N∘M→N+M (base v (base v' a) N∘Mr.poly* X)) (sym (base-poly+ w U V))
                                                     ∙ cong₂ (_poly+_ ) ind-U ind-V
                                                     ∙ sym (cong (λ X → N∘M→N+M (base v (base v' a)) N+Mr.poly* N∘M→N+M X) (base-poly+ w U V)) )
                              -- End Ind base Q
                      λ {U V} ind-U ind-V → cong₂ _poly+_ ind-U ind-V)
                      -- End Ind Q
           λ {U V} ind-U ind-V Q → cong (λ X → N∘M→N+M (X N∘Mr.poly* Q)) (sym (base-poly+ v U V))
                                    ∙ cong₂ _poly+_ (ind-U Q) (ind-V Q)
                                    ∙ sym (cong (λ X → (N∘M→N+M X) N+Mr.poly* (N∘M→N+M Q)) (sym (base-poly+ v U V)) ))
           -- End Ind base P
     λ {U V} ind-U ind-V Q → cong₂ _poly+_ (ind-U Q) (ind-V Q)
     -- End Ind P

-----------------------------------------------------------------------------
-- Ring Equivalence

module _ (A' : CommRing ℓ) (n m : ℕ) where

  open Comp-Poly-nm A' n m

  CRE-PolyN∘M-PolyN+M : CommRingEquiv (PolyCommRing (PolyCommRing A' m) n) (PolyCommRing A' (n +n m))
  fst CRE-PolyN∘M-PolyN+M = isoToEquiv is
    where
    is : Iso _ _
    Iso.fun is = N∘M→N+M
    Iso.inv is = N+M→N∘M
    Iso.rightInv is = e-sect
    Iso.leftInv is = e-retr

  snd CRE-PolyN∘M-PolyN+M = makeIsRingHom map-1P N∘M→N+M-gmorph N∘M→N+M-rmorph

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some defined operations (multiplication by natural number and
-- exponentiation)
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Operations.Semiring {s₁ s₂} (S : Semiring s₁ s₂) where

import Algebra.Operations.CommutativeMonoid as MonoidOperations
open import Data.Nat.Base
  using (zero; suc; ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Product using (module Σ)
open import Function using (_$_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Semiring S renaming (zero to *-zero)
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Operations

-- Re-export all monoid operations and proofs
open MonoidOperations +-commutativeMonoid public

-- Exponentiation.
infixr 9 _^_
_^_ : Carrier → ℕ → Carrier
x ^ zero  = 1#
x ^ suc n = x * x ^ n

------------------------------------------------------------------------
-- Properties of _×_

-- _× 1# is homomorphic with respect to _ℕ*_/_*_.

×1-homo-* : ∀ m n → (m ℕ* n) × 1# ≈ (m × 1#) * (n × 1#)
×1-homo-* 0 n = begin
  0#             ≈⟨ sym (Σ.proj₁ *-zero (n × 1#)) ⟩
  0# * (n × 1#)  ∎
×1-homo-* (suc m) n = begin
  (n ℕ+ m ℕ* n) × 1#                  ≈⟨ ×-homo-+ 1# n (m ℕ* n) ⟩
  n × 1# + (m ℕ* n) × 1#              ≈⟨ +-cong refl (×1-homo-* m n) ⟩
  n × 1# + (m × 1#) * (n × 1#)         ≈⟨ sym (+-cong (*-identityˡ _) refl) ⟩
  1# * (n × 1#) + (m × 1#) * (n × 1#)  ≈⟨ sym (distribʳ (n × 1#) 1# (m × 1#)) ⟩
  (1# + m × 1#) * (n × 1#)             ∎

------------------------------------------------------------------------
-- Properties of _×′_

-- _×′ 1# is homomorphic with respect to _ℕ*_/_*_.

×′1-homo-* : ∀ m n → (m ℕ* n) ×′ 1# ≈ (m ×′ 1#) * (n ×′ 1#)
×′1-homo-* m n = begin
  (m ℕ* n) ×′ 1#         ≈⟨ sym $ ×≈×′ (m ℕ* n) 1# ⟩
  (m ℕ* n) ×  1#         ≈⟨ ×1-homo-* m n ⟩
  (m ×  1#) * (n ×  1#)  ≈⟨ *-cong (×≈×′ m 1#) (×≈×′ n 1#) ⟩
  (m ×′ 1#) * (n ×′ 1#)  ∎

------------------------------------------------------------------------
-- Properties of _^_

-- _^_ preserves equality.

^-congˡ : ∀ n → (_^ n) Preserves _≈_ ⟶ _≈_
^-congˡ zero    x≈y = refl
^-congˡ (suc n) x≈y = *-cong x≈y (^-congˡ n x≈y)

^-cong : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
^-cong {v = n} x≈y P.refl = ^-congˡ n x≈y