text:
{-# OPTIONS --cubical #-}
module CubicalPrims where

open import Agda.Primitive renaming (_⊔_ to ℓ-max)
open import Agda.Primitive.Cubical renaming (primIMin to _∧_; primIMax to _∨_; primINeg to ~_; isOneEmpty to empty)
open import Agda.Builtin.Bool
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to ouc)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Id renaming (primIdJ to J)
open import Agda.Builtin.Cubical.Glue renaming (primGlue to Glue; prim^glue to glue; prim^unglue to unglue)
open import Agda.Builtin.Sigma
open import Agda.Builtin.List
open Helpers

module _ {ℓ} {A : Set ℓ} where
  trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  trans {x = x} p q i = primComp (λ _ → A) _ (λ { j (i = i0) → x
                                                ; j (i = i1) → q j }) (p i)

module _ {ℓ ℓ'} {A : Set ℓ} {x : A}
         (P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where
  pathJ : (y : A) → (p : x ≡ y) → P y p
  pathJ _ p = primTransp (λ i →  P (p i) (\ j → p (i ∧ j))) i0 d

module DerivedComp where
  forward : (la : I → Level) (A : ∀ i → Set (la i)) (r : I) → A r → A i1
  forward la A r x = primTransp (\ i → A (i ∨ r)) r x

  module _ (la : I → Level) (A : ∀ i → Set (la i)) (φ : I) (u : ∀ i → Partial φ (A i)) (u0 : A i0 [ φ ↦ u i0 ]) where
    comp : A i1
    comp = primHComp (\ i → \ { (φ = i1) → forward la A i (u i itIsOne) }) (forward la A i0 (ouc u0))

    comp-test : comp ≡ primComp A φ u (ouc u0)
    comp-test = refl

test-sym : ∀ {ℓ} {A : Set ℓ} → {x y : A} → (p : x ≡ y) → sym (sym p) ≡ p
test-sym p = refl

transpFill : ∀ {ℓ} {A' : Set ℓ} (φ : I)
               (A : (i : I) → Set ℓ [ φ ↦ (\ _ → A') ]) →
               (u0 : ouc (A i0)) →
               PathP (λ i → ouc (A i)) u0 (primTransp (λ i → ouc (A i)) φ u0)
transpFill φ A u0 i = primTransp (\ j → ouc (A (i ∧ j))) (~ i ∨ φ) u0

test-bool : (p : true ≡ false) → Bool
test-bool p = primComp (λ _ → Bool) i1 (λ j → λ _ → p j) true

-- cannot reduce to true, because it's already reducing to false.
test-bool-beta : ∀ p → test-bool p ≡ false
test-bool-beta p = refl

etaExpand : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → x ≡ y
etaExpand p = λ z → p z

etaEq : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → p ≡ etaExpand p
etaEq p = refl

module IntervalEquations where
  postulate
    P : I → Set
  test-0 : (P (~ i0) ≡ P i1)
  test-0 = refl
  test-1 : P (~ i1) ≡ P i0
  test-1 = refl
  test-2 : ∀ {i j} → P (~ (i ∧ j)) ≡ P (~ i ∨ ~ j)
  test-2 = refl
  test-3 : ∀ {i j} → P (~ (i ∨ j)) ≡ P (~ i ∧ ~ j)
  test-3 = refl
  test-4 : ∀ {i} → P (~ (~ i)) ≡ P i
  test-4 = refl

  test-5 : ∀ {i} → P (_∧_ i0 i) ≡ P i0
  test-5 = refl

  test-52 : ∀ {i} → P (_∧_ i i) ≡ P i
  test-52 = refl

  test-53 : ∀ {i j} → P (i ∧ j) ≡ P (j ∧ i)
  test-53 = refl

  test-n6 : ∀ {i} → P (i1 ∧ i) ≡ P i
  test-n6 = refl

  test-n7 : ∀ {i} → P (i ∧ i0) ≡ P i0
  test-n7 = refl

  test-n8 : ∀ {i} → P (i ∧ i1) ≡ P i
  test-n8 = refl

reflId : ∀ {l} {A : Set l} {x : A} → Id x x
reflId = conid i1 refl

J-comp : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} {P : ∀ y → Id x y → Set ℓ'} →
         (d : P x reflId) → J P d reflId ≡ d
J-comp _ = refl

outPartial : ∀ {ℓ} {A : Set ℓ} → Partial i1 A → A
outPartial = λ f → f itIsOne

inPartial : ∀ {ℓ} {A : Set ℓ} → A → Partial i1 A
inPartial a = λ _ → a

module _ {ℓ ℓ'} {A : I → Set ℓ} {B : ∀ i → A i → Set ℓ'}
         (let ℓ = _ ; C : I → Set ℓ ; C i = (x : A i) → B i x) where
  compPi : (φ : I) → (u : ∀ i → Partial φ (C i)) → (a : C i0 [ φ ↦ u i0 ]) → C i1
  compPi φ u a' x1 = primComp
      (λ i → B i (v i)) φ (λ i o → u i o (v i)) (a (v i0)) where
    a = ouc a'
    v : (i : I) → A i
    v i = primTransp (λ j → A (i ∨ (~ j))) i x1
    f : ∀ i → (a : A i) → Partial φ (B i a)
    f i a = λ { (φ = i1) → u i itIsOne a  }

  compPi' : (φ : I) → (u : ∀ i → Partial φ (C i)) → (a : C i0 [ φ ↦ u i0 ]) → C i1
  compPi' φ u a = primComp C φ u (ouc a)

  test-compPi : (φ : I) → (u : ∀ i → Partial φ (C i)) → (a : C i0 [ φ ↦ u i0 ]) →
                  compPi φ u a ≡ compPi' φ u a
  test-compPi = λ φ u u0 → refl

module HCompPathP {ℓ} {A : I → Set ℓ} (u : A i0) (v : A i1) (φ : I)
         (let C = PathP A u v) (p : ∀ i → Partial φ C) (p0 : C [ φ ↦ p i0 ]) where

  hcompPathP : C
  hcompPathP j = primHComp (\ { i (φ = i1) → p i itIsOne j
                              ; i (j = i0) → u
                              ; i (j = i1) → v })
                           (ouc p0 j)

  test-hcompPathP : hcompPathP ≡ primHComp p (ouc p0)
  test-hcompPathP = refl

module TranspPathP {ℓ} {A : I → I → Set ℓ} (u : ∀ i → A i i0)(v : ∀ i → A i i1)
                  (let C = λ (i : I) → PathP (A i) (u i) (v i))
                  (p0 : C i0) where
 φ = i0
 transpPathP : C i1
 transpPathP j = primComp (λ i → A i j) _
                          (\ { i (j = i0) → u i
                             ; i (j = i1) → v i })
                          (p0 j)

 test-compPathP : transpPathP ≡ primTransp C i0 p0
 test-compPathP = refl

module RecordComp where
  record R {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') (C : (x : A) → B x → Set ℓ)
     : Set (ℓ-max ℓ ℓ') where
   coinductive
   constructor _,_
   field
     fst : A
     snd : B fst
     trd : C fst snd
  open R

  hcompR : ∀ {ℓ ℓ'} {A : Set ℓ} {B : A → Set ℓ'}
                   {C : (x : A) → B x → Set ℓ} →
    (let ℓ = _ ; Z : Set ℓ ; Z = R(A)(B)(C))
    (φ : I) → (u : ∀ i → Partial φ Z) → Z [ φ ↦ u i0 ] → Z
  fst (hcompR {A = A} {B} φ w w0)
    = primComp (\ _ → A) φ (λ i →  (λ{ (φ = i1) → fst (w i itIsOne) }) ) (fst (ouc w0))
  snd (hcompR {A = A} {B} φ w w0)
    = primComp (λ i → B (a i)) φ (λ i → (λ { (φ = i1) → snd (w i itIsOne) })) (snd (ouc w0))
    where
      a = fill (λ z → A) (λ i → (λ { (φ = i1) → fst (w i itIsOne) }) ) (inc (fst (ouc w0)))
  trd (hcompR {A = A} {B} {C} φ w w0)
    = primComp (λ i → C (a i) (b i)) φ ((λ i → (λ { (φ = i1) → trd (w i itIsOne)}))) (trd (ouc w0))
    where
      a = fill (λ z → A) (λ i → (λ { (φ = i1) → fst (w i itIsOne) }) ) (inc (fst (ouc w0)))
      b = fill (λ i → B (a i)) (λ i → (λ { (φ = i1) → snd (w i itIsOne) }) ) (inc (snd (ouc w0)))

  module _ {ℓ ℓ'} {A : Set ℓ} {B : A → Set ℓ'}
                  {C : (x : A) → B x → Set ℓ}
                  (let ℓ = _ ; Z : Set ℓ ; Z = R(A)(B)(C))
                  (φ : I) (u : ∀ i → Partial φ (Z)) (a : Z [ φ ↦ u i0 ]) where
     test-compR-fst : hcompR {A = A} {B} {C} φ u a .fst ≡ primHComp u (ouc a) .fst
     test-compR-fst = refl

     test-compR-snd : hcompR {A = A} {B} {C} φ u a .snd ≡ primHComp u (ouc a) .snd
     test-compR-snd = refl

     test-compR-trd : hcompR {A = A} {B} {C} φ u a .trd ≡ primHComp u (ouc a) .trd
     test-compR-trd = refl

  module _ {ℓ ℓ'} {A : I → Set ℓ} {B : ∀ i → A i → Set ℓ'}
                   {C : ∀ i → (x : A i) → B i x → Set ℓ}
                   (let ℓ = _ ; Z : I → Set ℓ ; Z i = R(A i)(B i)(C i)) where

    φ = i0
    transpR : Z i0 → Z i1
    fst (transpR w0) =
      primTransp A φ (fst w0)
    snd (transpR w0) = primTransp (\ i → B i (a i)) φ (snd w0)
       where
         a = transpFill {A' = A i0} φ (λ i → inc (A i)) (fst w0)
    trd (transpR w0) = primTransp (\ i → C i (a i) (b i)) φ (trd w0)
       where
         a = transpFill {A' = A i0} φ (λ i → inc (A i)) (fst w0)
         b = transpFill {A' = B i0 (a i0)} φ (λ i → inc (B i (a i))) (snd w0)

  module _ {ℓ ℓ'} {A : I → Set ℓ} {B : ∀ i → A i → Set ℓ'}
                  {C : ∀ i → (x : A i) → B i x → Set ℓ}
                  (let ℓ = _ ; Z : I → Set ℓ ; Z i = R(A i)(B i)(C i))
                  (a : Z i0) where

    test-transpR-fst : fst (transpR {A = A} {B} {C} a) ≡ fst (primTransp Z i0 a)
    test-transpR-fst = refl

    test-transpR-snd : snd (transpR {A = A} {B} {C} a) ≡ snd (primTransp Z i0 a)
    test-transpR-snd = refl

    test-transpR-trd : trd (transpR {A = A} {B} {C} a) ≡ trd (primTransp Z i0 a)
    test-transpR-trd = refl

module _ {ℓ} {A : Set ℓ} {φ : I} {T : Partial φ (Set ℓ)}
             {e : PartialP φ (λ o → T o ≃ A)}
             where
  test-Glue-β : (t : PartialP φ T) (a : A [ φ ↦ (\ o → e o .fst (t o)) ]) →
    unglue {A = A} {φ = φ} {T = T} {e} (glue t (ouc a)) ≡ ouc a
  test-Glue-β _ _ = refl

  test-Glue-η : (b : Glue A T e) →
    (glue {φ = φ} (λ{ (φ = i1) → b }) (unglue {φ = φ} b)) ≡ b
  test-Glue-η b = refl

module _ {ℓ} {A : Set ℓ} (let φ = i1) {T : Partial φ (Set ℓ)}
             {e : PartialP φ (λ o → T o ≃ A)}
              where
  test-unglue-0 : (b : Glue A T e) →
    unglue {A = A} {φ = φ} {T = T} {e} b ≡ e itIsOne .fst b
  test-unglue-0 _ = refl

  test-unglue-2 : (t : PartialP φ T) (a : A [ φ ↦ (\ o → e o .fst (t o)) ]) →
    unglue {A = A} {φ = φ} {T = T} {e}
    (glue {A = A}{φ = φ}{T = T}{e} t (ouc a)) ≡ e itIsOne .fst (t itIsOne) -- = a
  test-unglue-2 _ _ = refl

  test-glue-0 : (t : PartialP φ T) (a : A [ φ ↦ (\ o → e o .fst (t o)) ]) →
    (glue {A = A} {T = T} {e} t (ouc a)) ≡ t itIsOne
  test-glue-0 _ _ = refl

eqToPath : ∀ {ℓ} {A B : Set ℓ} → A ≃ B → A ≡ B
eqToPath {ℓ} {A} {B} f = λ i → Glue B
  ([ ~ i ↦ (λ _ → A) , i ↦ (λ _ → B) ])
  ([ ~ i ↦ (λ{ (i = i0) → f }) , i ↦ (λ{ (i = i1) → pathToEquiv (λ _ → B) }) ])

univ = eqToPath

not : Bool → Bool
not true = false
not false = true

notnot : ∀ y → y ≡ not (not y)
notnot true = refl
notnot false = refl

nothelp : ∀ y (y₁ : Σ Bool \ x → (not x ≡ y)) → (not y , sym (notnot y)) ≡ y₁
nothelp y (true  , eq) = pathJ (λ y₁ eq' →
  (not y₁ , sym (notnot y₁)) ≡ (true  , eq')) refl _ eq
nothelp y (false , eq) = pathJ (λ y₁ eq' →
  (not y₁ , sym (notnot y₁)) ≡ (false , eq')) refl _ (eq)

notEquiv : Bool ≃ Bool
notEquiv = not , (λ { .equiv-proof y → (not y , sym (notnot y)) , nothelp y })

test : Bool
test = primComp (λ i → univ {A = Bool} {B = Bool} notEquiv i)
                i0 (λ _ → empty) true

test-test : test ≡ primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                  (primComp (λ i → Bool) i0 (λ _ _ → false)
                   false))))))))
test-test = refl

test-test2 : test ≡ false
test-test2 = refl

test2 : Bool
test2 = primComp (λ i → eqToPath {A = Bool} {B = Bool} notEquiv i)
                 i0
                 (λ _ → empty)
                 true

test2-test : test2 ≡ primComp (λ _ → Bool) i0 (λ _ _ → false)
                    (primComp (λ _ → Bool) i0 ((λ _ _ → false))
                    (primComp (λ _ → Bool) i0 ((λ _ _ → false))
                    (primComp (λ _ → Bool) i0 ((λ _ _ → false))
                     false)))
test2-test = refl

test3 : Bool
test3 = primComp (λ i → eqToPath {A = Bool} {B = Bool} notEquiv i)
                 i0
                 (λ _ → empty)
                 true

test3-test : test3 ≡ primComp (λ i → Bool) i0 (λ _ _ → false)
                    (primComp (λ _ → Bool) i0 (λ _ _ → false)
                    (primComp (λ i → Bool) i0 (λ _ _ → false)
                     false))
test3-test = refl

data D2 (A : Set) : Set where
   c1 : D2 A
   c2 : D2 A

test5-test : ∀ j →  primComp (λ i → D2 Bool) (j ∨ ~ j)
  (λ i → [ j ↦ (λ{ (j = i1) → c1 }) , ~ j ↦ (λ{ (j = i0) → c1 }) ]) c1 ≡ c1
test5-test j = refl

test6-test : (j : I → I) → primComp (λ i → D2 Bool) (j i0) (λ i o → c1) c1 ≡ c1
test6-test j = refl

test4-test : ∀ j → primComp (λ i → Bool) (j ∨ ~ j)
  (λ i → [ j ↦ (λ{ (j = i1) → false }) , ~ j ↦ (λ{ (j = i0) → false }) ] ) false ≡ false
test4-test j = refl

ListNot : List Bool ≡ List Bool
ListNot = λ i → List (univ {A = Bool} {B = Bool} notEquiv i)

trues : List Bool
trues = true ∷ true ∷ []

falses : List Bool
falses = primComp (λ i → ListNot i) i0 (λ _ → empty) trues

test-falses : falses ≡ (false ∷ false ∷ [])
test-falses = refl

trues2 : List Bool
trues2 = primComp (λ i → trans ListNot ListNot i) i0 (λ _ → empty) trues

test-trues2 : trues2 ≡ trues
test-trues2 = refl

trues3 : List Bool
trues3 = primComp (λ i → let p = trans ListNot ListNot in
                         trans p p i)
                  i0
                  (λ _ → empty)
                  trues

test-trues3 : trues3 ≡ trues
test-trues3 = refl

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
{-

Mayer-Vietoris cofiber sequence:

  Let X be a pointed type, and let a span B ←[f]- X -[g]→ C be given.
  Then the mapping cone of the canonical map (B ⋁ C) → B ⊔_X C is equivalent to Susp X.

The sequence Susp X → (B ⋁ C) → B ⊔_X C therefore induces a long exact sequence in cohomology.
Proof is adapted from Evan Cavallo's master's thesis.

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Homotopy.MayerVietorisCofiber where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Foundations.Pointed
open import Cubical.Data.Unit
open import Cubical.HITs.MappingCones
open import Cubical.HITs.Pushout
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge

module _ {ℓX ℓB ℓC} {X : Pointed ℓX} {B : Type ℓB} {C : Type ℓC} (f : X .fst → B) (g : X .fst → C)
  where

  private
    Y : Pointed _
    Y = (B , f (X .snd))

    Z : Pointed _
    Z = (C , g (X .snd))

  wedgeToPushout : Y ⋁ Z → Pushout f g
  wedgeToPushout (inl y) = inl y
  wedgeToPushout (inr z) = inr z
  wedgeToPushout (push _ i) = push (pt X) i

  pushoutToSusp : Pushout f g → Susp (X .fst)
  pushoutToSusp (inl y) = north
  pushoutToSusp (inr z) = south
  pushoutToSusp (push x i) = merid x i

  {-
    Coherence lemma:
    To construct a function f : (c : Cone wedgeToPushout) → D c, we can always
    adjust the definition of (f (spoke (inr z) i)) so that there is a canonical
    choice for (f (spoke (push tt j) i))
  -}
  module Helper {ℓD} {D : Cone wedgeToPushout → Type ℓD}
    (inj* : ∀ w → D (inj w))
    (hub* : D hub)
    (inl* : ∀ y → PathP (λ i → D (spoke (inl y) i)) hub* (inj* (inl y)))
    (inr* : ∀ z → PathP (λ i → D (spoke (inr z) i)) hub* (inj* (inr z)))
    where

    cap : (i j : I) → D (spoke (push tt j) i)
    cap i j =
      fill
        (λ i → D (spoke (push tt j) (~ i)))
        (λ i → λ
          { (j = i0) → inl* (Y .snd) (~ i)
          ; (j = i1) → inr* (Z .snd) (~ i)
          })
        (inS (inj* (push (X .snd) j)))
        (~ i)

    cap0 : (j : I) → D hub
    cap0 = cap i0

    face-i≡0 : (k j : I) → D hub
    face-i≡0 k j =
      hfill
        (λ j → λ
          { (k = i0) → cap0 j
          ; (k = i1) → hub*
          })
        (inS hub*)
        j

    inrFiller : ∀ z → (k i : I) → D (spoke (inr z) i)
    inrFiller z k i =
     hfill
       (λ k → λ
         { (i = i0) → face-i≡0 k i1
         ; (i = i1) → inj* (inr z)
         })
       (inS (inr* z i))
       k

    fun : ∀ c → D c
    fun (inj w) = inj* w
    fun hub = hub*
    fun (spoke (inl y) i) = inl* y i
    fun (spoke (inr z) i) = inrFiller z i1 i
    fun (spoke (push tt j) i) =
      hcomp
        (λ k → λ
          { (i = i0) → face-i≡0 k j
          ; (i = i1) → inj* (push (X .snd) j)
          ; (j = i0) → inl* (Y .snd) i
          })
        (cap i j)

  equiv : Cone wedgeToPushout ≃ Susp (X .fst)
  equiv = isoToEquiv (iso fwd bwd fwdBwd bwdFwd)
    where
    fwd : Cone wedgeToPushout → Susp (X .fst)
    fwd (inj w) = pushoutToSusp w
    fwd hub = north
    fwd (spoke (inl y) i) = north
    fwd (spoke (inr z) i) = merid (X .snd) i
    fwd (spoke (push tt j) i) = merid (X .snd) (i ∧ j)

    bwd : Susp (X .fst) → Cone wedgeToPushout
    bwd north = hub
    bwd south = hub
    bwd (merid x i) =
      hcomp
        (λ k → λ
          { (i = i0) → spoke (inl (f x)) (~ k)
          ; (i = i1) → spoke (inr (g x)) (~ k)
          })
        (inj (push x i))

    bwdPushout : (w : Pushout f g) → bwd (pushoutToSusp w) ≡ inj w
    bwdPushout (inl y) = spoke (inl y)
    bwdPushout (inr z) = spoke (inr z)
    bwdPushout (push x i) k =
      hfill
        (λ k → λ
          { (i = i0) → spoke (inl (f x)) (~ k)
          ; (i = i1) → spoke (inr (g x)) (~ k)
          })
        (inS (inj (push x i)))
        (~ k)

    bwdMeridPt : refl ≡ cong bwd (merid (X .snd))
    bwdMeridPt j i =
      hcomp
        (λ k → λ
          { (i = i0) → spoke (inl (Y .snd)) (~ k)
          ; (i = i1) → spoke (inr (Z .snd)) (~ k)
          ; (j = i0) → spoke (push _ i) (~ k)
          })
        (inj (push (X .snd) i))

    bwdFwd : (c : Cone wedgeToPushout) → bwd (fwd c) ≡ c
    bwdFwd =
      Helper.fun
        bwdPushout
        refl
        (λ y i k → spoke (inl y) (i ∧ k))
        (λ z i k →
          hcomp
            (λ l → λ
              { (i = i0) → hub
              ; (i = i1) → spoke (inr z) k
              ; (k = i0) → bwdMeridPt l i
              ; (k = i1) → spoke (inr z) i
              })
            (spoke (inr z) (i ∧ k)))

    fwdBwd : (s : Susp (X .fst)) → fwd (bwd s) ≡ s
    fwdBwd north = refl
    fwdBwd south = merid (X .snd)
    fwdBwd (merid a i) j =
      fill
        (λ _ → Susp (X .fst))
        (λ j → λ
          { (i = i0) → north
          ; (i = i1) → merid (X .snd) (~ j)
          })
        (inS (merid a i))
        (~ j)

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------------
-- Conversion rules for the greatest common divisor
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Total.ConversionRulesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Program.GCD.Total.GCD

------------------------------------------------------------------------------
private
  -- Before to prove some properties for the gcd it is convenient to
  -- descompose the behavior of the function step by step.

  -- Initially, we define the possible states (gcd-s₁, gcd-s₂,
  -- ...). Then we write down the proof for the execution step from
  -- the state p to the state q, e.g.
  --
  -- proof₂₋₃ : ∀ m n → gcd-s₂ m n → gcd-s₃ m n.

  -- The functions gcd-00, gcd-S0, gcd-0S, gcd-Sm>Sn and gcd-Sm≯Sn
  -- show the use of the states gcd-s₁, gcd-s₂, ..., and the proofs
  -- associated with the execution steps.

  ----------------------------------------------------------------------------
  -- The steps

  -- Initially, the equation gcd-eq is used.
  gcd-s₁ : D → D → D
  gcd-s₁ m n = if (iszero₁ n)
                 then m
                 else (if (iszero₁ m)
                         then n
                         else (if (gt m n)
                                 then gcd (m ∸ n) n
                                 else gcd m (n ∸ m)))

  -- First if_then_else_ (iszero₁ n).
  gcd-s₂ : D → D → D → D
  gcd-s₂ m n b = if b
                   then m
                   else (if (iszero₁ m)
                           then n
                           else (if (gt m n)
                                   then gcd (m ∸ n) n
                                   else gcd m (n ∸ m)))

  -- First if_then_else_ when iszero₁ n = true.
  gcd-s₃ : D → D
  gcd-s₃ m = m

  -- First if_then_else_ when iszero₁ n = false.
  gcd-s₄ : D → D → D
  gcd-s₄ m n = if (iszero₁ m)
                 then n
                 else (if (gt m n) then gcd (m ∸ n) n else gcd m (n ∸ m))

   -- Second if_then_else_ (iszero₁ m).
  gcd-s₈ : D → D → D → D
  gcd-s₈ m n b = if b
                   then n
                   else (if (gt m n) then gcd (m ∸ n) n else gcd m (n ∸ m))

  -- Second if_then_else_, when iszero₁ m = true.
  gcd-s₉ : D → D
  gcd-s₉ n = n

  -- Second if_then_else_, when iszero₁ m = false.
  gcd-s₁₀ : D → D → D
  gcd-s₁₀ m n = if (gt m n) then gcd (m ∸ n) n else gcd m (n ∸ m)

  -- Third if_then_else_ (gt m n).
  gcd-s₁₁ : D → D → D → D
  gcd-s₁₁ m n b = if b then gcd (m ∸ n) n else gcd m (n ∸ m)

  -- Third if_then_else_ when gt m n = true.
  gcd-s₁₂ : D → D → D
  gcd-s₁₂ m n = gcd (m ∸ n) n

  -- Fourth if_then_else_ when gt m n = false.
  gcd-s₁₃ : D → D → D
  gcd-s₁₃ m n = gcd m (n ∸ m)

  ----------------------------------------------------------------------------
  -- The execution steps

  {-

  To prove the execution steps, e.g.

  proof₃₋₄ : ∀ m n → gcd-s₃ m n → gcd_s₄ m n)

  we usually need to prove that

                         C [m] ≡ C [n] (1)

  given that
                             m ≡ n,    (2)

  where (2) is a conversion rule usually.
  We prove (1) using

  subst : ∀ {x y} (D : A → Set) → x ≡ y → P x → P y

  where
   • P is given by λ m → C [m ] ≡ C [n],
   • x ≡ y is given n ≡ m (actually, we use sym (m ≡ n)) and
   • P x is given by C [n] ≡ C [n] (i.e. refl).
  -}

  proof₀₋₁ : ∀ m n → gcd m n ≡ gcd-s₁ m n
  proof₀₋₁ = gcd-eq

  -- 25 April 2014. Failed with Andreas' --without-K.
  proof₁₋₂ : ∀ m n b → iszero₁ n ≡ b → gcd-s₁ m n ≡ gcd-s₂ m n b
  proof₁₋₂ m n .(iszero₁ n) refl = refl

  proof₂₋₃ : ∀ m n → gcd-s₂ m n true ≡ gcd-s₃ m
  proof₂₋₃ m _ = if-true (gcd-s₃ m)

  proof₂₋₄ : ∀ m n → gcd-s₂ m n false ≡ gcd-s₄ m n
  proof₂₋₄ m n = if-false (gcd-s₄ m n)

  proof₄₋₈ : ∀ m n b → iszero₁ m ≡ b → gcd-s₄ m n ≡ gcd-s₈ m n b
  proof₄₋₈ m n .(iszero₁ m) refl = refl

  proof₈₋₉ : ∀ m n → gcd-s₈ m n true ≡ gcd-s₉ n
  proof₈₋₉ _ n = if-true n

  proof₈₋₁₀ : ∀ m n → gcd-s₈ m n false ≡ gcd-s₁₀ m n
  proof₈₋₁₀ m n = if-false (gcd-s₁₀ m n)

  proof₁₀₋₁₁ : ∀ m n b → gt m n ≡ b → gcd-s₁₀ m n ≡ gcd-s₁₁ m n b
  proof₁₀₋₁₁ m n .(lt n m) refl = refl

  proof₁₁₋₁₂ : ∀ m n → gcd-s₁₁ m n true ≡ gcd-s₁₂ m n
  proof₁₁₋₁₂ m n = if-true (gcd (m ∸ n) n)

  proof₁₁₋₁₃ : ∀ m n → gcd-s₁₁ m n false ≡ gcd-s₁₃ m n
  proof₁₁₋₁₃ m n = if-false (gcd m (n ∸ m))

------------------------------------------------------------------------------
-- The five equations for gcd

-- First equation.
gcd-00 : gcd zero zero ≡ zero
gcd-00 =
  gcd zero zero         ≡⟨ proof₀₋₁ zero zero ⟩
  gcd-s₁ zero zero      ≡⟨ proof₁₋₂ zero zero true iszero-0 ⟩
  gcd-s₂ zero zero true ≡⟨ proof₂₋₃ zero zero ⟩
  zero                  ∎

-- Second equation.
gcd-S0 : ∀ n → gcd (succ₁ n) zero ≡ succ₁ n
gcd-S0 n =
  gcd (succ₁ n) zero         ≡⟨ proof₀₋₁ (succ₁ n) zero ⟩
  gcd-s₁ (succ₁ n) zero      ≡⟨ proof₁₋₂ (succ₁ n) zero true iszero-0 ⟩
  gcd-s₂ (succ₁ n) zero true ≡⟨ proof₂₋₃ (succ₁ n) zero ⟩
  succ₁ n                    ∎

-- Third equation.
gcd-0S : ∀ n → gcd zero (succ₁ n) ≡ succ₁ n
gcd-0S n =
  gcd zero (succ₁ n)          ≡⟨ proof₀₋₁ zero (succ₁ n) ⟩
  gcd-s₁ zero (succ₁ n)       ≡⟨ proof₁₋₂ zero (succ₁ n) false (iszero-S n) ⟩
  gcd-s₂ zero (succ₁ n) false ≡⟨ proof₂₋₄ zero (succ₁ n) ⟩
  gcd-s₄ zero (succ₁ n)       ≡⟨ proof₄₋₈ zero (succ₁ n) true iszero-0 ⟩
  gcd-s₈ zero (succ₁ n) true  ≡⟨ proof₈₋₉  zero (succ₁ n) ⟩
  succ₁ n                     ∎

-- Fourth equation.
gcd-S>S : ∀ m n → succ₁ m > succ₁ n →
          gcd (succ₁ m) (succ₁ n) ≡ gcd (succ₁ m ∸ succ₁ n) (succ₁ n)

gcd-S>S m n Sm>Sn =
  gcd (succ₁ m) (succ₁ n)           ≡⟨ proof₀₋₁ (succ₁ m) (succ₁ n) ⟩
  gcd-s₁ (succ₁ m) (succ₁ n)        ≡⟨ proof₁₋₂ (succ₁ m) (succ₁ n) false (iszero-S n) ⟩
  gcd-s₂ (succ₁ m) (succ₁ n) false  ≡⟨ proof₂₋₄ (succ₁ m) (succ₁ n) ⟩
  gcd-s₄ (succ₁ m) (succ₁ n)        ≡⟨ proof₄₋₈ (succ₁ m) (succ₁ n) false (iszero-S m) ⟩
  gcd-s₈ (succ₁ m) (succ₁ n) false  ≡⟨ proof₈₋₁₀ (succ₁ m) (succ₁ n) ⟩
  gcd-s₁₀ (succ₁ m) (succ₁ n)       ≡⟨ proof₁₀₋₁₁ (succ₁ m) (succ₁ n) true Sm>Sn ⟩
  gcd-s₁₁ (succ₁ m) (succ₁ n) true  ≡⟨ proof₁₁₋₁₂ (succ₁ m) (succ₁ n) ⟩
  gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∎

-- Fifth equation.
gcd-S≯S : ∀ m n → succ₁ m ≯ succ₁ n →
          gcd (succ₁ m) (succ₁ n) ≡ gcd (succ₁ m) (succ₁ n ∸ succ₁ m)
gcd-S≯S m n Sm≯Sn =
  gcd (succ₁ m) (succ₁ n)           ≡⟨ proof₀₋₁ (succ₁ m) (succ₁ n) ⟩
  gcd-s₁ (succ₁ m) (succ₁ n)        ≡⟨ proof₁₋₂ (succ₁ m) (succ₁ n) false (iszero-S n) ⟩
  gcd-s₂ (succ₁ m) (succ₁ n) false  ≡⟨ proof₂₋₄ (succ₁ m) (succ₁ n) ⟩
  gcd-s₄ (succ₁ m) (succ₁ n)        ≡⟨ proof₄₋₈ (succ₁ m) (succ₁ n) false (iszero-S m) ⟩
  gcd-s₈ (succ₁ m) (succ₁ n) false  ≡⟨ proof₈₋₁₀ (succ₁ m) (succ₁ n) ⟩
  gcd-s₁₀ (succ₁ m) (succ₁ n)       ≡⟨ proof₁₀₋₁₁ (succ₁ m) (succ₁ n) false Sm≯Sn ⟩
  gcd-s₁₁ (succ₁ m) (succ₁ n) false ≡⟨ proof₁₁₋₁₃ (succ₁ m) (succ₁ n) ⟩
  gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by Heyting Algebra
------------------------------------------------------------------------

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

open import Relation.Binary.Lattice

module Relation.Binary.Properties.HeytingAlgebra
  {c ℓ₁ ℓ₂} (L : HeytingAlgebra c ℓ₁ ℓ₂) where

open HeytingAlgebra L

open import Algebra.FunctionProperties _≈_
open import Data.Product using (_,_)
open import Function using (_$_; flip; _∘_)
open import Level using (_⊔_)
open import Relation.Binary
import Relation.Binary.Reasoning.PartialOrder as POR
open import Relation.Binary.Properties.MeetSemilattice meetSemilattice
open import Relation.Binary.Properties.JoinSemilattice joinSemilattice
import Relation.Binary.Properties.BoundedMeetSemilattice boundedMeetSemilattice as BM
open import Relation.Binary.Properties.Lattice lattice
open import Relation.Binary.Properties.BoundedLattice boundedLattice
import Relation.Binary.Reasoning.Setoid as EqReasoning

------------------------------------------------------------------------
-- Useful lemmas

⇨-eval : ∀ {x y} → (x ⇨ y) ∧ x ≤ y
⇨-eval {x} {y} = transpose-∧ refl

swap-transpose-⇨ : ∀ {x y w} → x ∧ w ≤ y → w ≤ x ⇨ y
swap-transpose-⇨ x∧w≤y = transpose-⇨ $ trans (reflexive $ ∧-comm _ _) x∧w≤y

------------------------------------------------------------------------
-- Properties of exponential

⇨-unit : ∀ {x} → x ⇨ x ≈ ⊤
⇨-unit = antisym (maximum _) (transpose-⇨ $ reflexive $ BM.identityˡ _)

y≤x⇨y : ∀ {x y} → y ≤ x ⇨ y
y≤x⇨y = transpose-⇨ (x∧y≤x _ _)

⇨-drop : ∀ {x y} → (x ⇨ y) ∧ y ≈ y
⇨-drop = antisym (x∧y≤y _ _) (∧-greatest y≤x⇨y refl)

⇨-app : ∀ {x y} → (x ⇨ y) ∧ x ≈ y ∧ x
⇨-app = antisym (∧-greatest ⇨-eval (x∧y≤y _ _)) (∧-monotonic y≤x⇨y refl)

⇨ʳ-covariant : ∀ {x} → (x ⇨_) Preserves _≤_ ⟶ _≤_
⇨ʳ-covariant y≤z = transpose-⇨ (trans ⇨-eval y≤z)

⇨ˡ-contravariant : ∀ {x} → (_⇨ x) Preserves (flip _≤_) ⟶ _≤_
⇨ˡ-contravariant z≤y = transpose-⇨ (trans (∧-monotonic refl z≤y) ⇨-eval)

⇨-relax : _⇨_ Preserves₂ (flip _≤_) ⟶ _≤_ ⟶ _≤_
⇨-relax {x} {y} {u} {v} y≤x u≤v = begin
  x ⇨ u ≤⟨ ⇨ʳ-covariant u≤v ⟩
  x ⇨ v ≤⟨ ⇨ˡ-contravariant y≤x ⟩
  y ⇨ v ∎
  where open POR poset

⇨-cong : _⇨_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
⇨-cong x≈y u≈v = antisym (⇨-relax (reflexive $ Eq.sym x≈y) (reflexive u≈v))
                         (⇨-relax (reflexive x≈y) (reflexive $ Eq.sym u≈v))

⇨-applyˡ : ∀ {w x y} → w ≤ x → (x ⇨ y) ∧ w ≤ y
⇨-applyˡ = transpose-∧ ∘ ⇨ˡ-contravariant

⇨-applyʳ : ∀ {w x y} → w ≤ x → w ∧ (x ⇨ y) ≤ y
⇨-applyʳ w≤x = trans (reflexive (∧-comm _ _)) (⇨-applyˡ w≤x)

⇨-curry : ∀ {x y z} → x ∧ y ⇨ z ≈ x ⇨ y ⇨ z
⇨-curry = antisym (transpose-⇨ $ transpose-⇨ $ trans (reflexive $ ∧-assoc _ _ _) ⇨-eval)
                  (transpose-⇨ $ trans (reflexive $ Eq.sym $ ∧-assoc _ _ _)
                                       (transpose-∧ $ ⇨-applyˡ refl))

------------------------------------------------------------------------
-- Various proofs of distributivity

∧-distribˡ-∨-≤ : ∀ x y z → x ∧ (y ∨ z) ≤ x ∧ y ∨ x ∧ z
∧-distribˡ-∨-≤ x y z = trans (reflexive $ ∧-comm _ _)
  (transpose-∧ $ ∨-least (swap-transpose-⇨ (x≤x∨y _ _)) $ swap-transpose-⇨ (y≤x∨y _ _))

∧-distribˡ-∨-≥ : ∀ x y z → x ∧ y ∨ x ∧ z ≤ x ∧ (y ∨ z)
∧-distribˡ-∨-≥ x y z = let
    x∧y≤x , x∧y≤y , _ = infimum x y
    x∧z≤x , x∧z≤z , _ = infimum x z
    y≤y∨z , z≤y∨z , _ = supremum y z
  in ∧-greatest (∨-least x∧y≤x x∧z≤x)
                (∨-least (trans x∧y≤y y≤y∨z) (trans x∧z≤z z≤y∨z))

∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
∧-distribˡ-∨ x y z = antisym (∧-distribˡ-∨-≤ x y z) (∧-distribˡ-∨-≥ x y z)

⇨-distribˡ-∧-≤ : ∀ x y z → x ⇨ y ∧ z ≤ (x ⇨ y) ∧ (x ⇨ z)
⇨-distribˡ-∧-≤ x y z = let
     y∧z≤y , y∧z≤z , _ = infimum y z
   in ∧-greatest (transpose-⇨ $ trans ⇨-eval y∧z≤y)
                 (transpose-⇨ $ trans ⇨-eval y∧z≤z)

⇨-distribˡ-∧-≥ : ∀ x y z → (x ⇨ y) ∧ (x ⇨ z) ≤ x ⇨ y ∧ z
⇨-distribˡ-∧-≥ x y z = transpose-⇨ (begin
  (((x ⇨ y) ∧ (x ⇨ z)) ∧ x)      ≈⟨ ∧-cong Eq.refl $ Eq.sym $ ∧-idempotent _ ⟩
  (((x ⇨ y) ∧ (x ⇨ z)) ∧ x  ∧ x) ≈⟨ Eq.sym $ ∧-assoc _ _ _ ⟩
  (((x ⇨ y) ∧ (x ⇨ z)) ∧ x) ∧ x  ≈⟨ ∧-cong (∧-assoc _ _ _) Eq.refl ⟩
  (((x ⇨ y) ∧ (x ⇨ z)  ∧ x) ∧ x) ≈⟨ ∧-cong (∧-cong Eq.refl $ ∧-comm _ _) Eq.refl ⟩
  (((x ⇨ y) ∧ x  ∧ (x ⇨ z)) ∧ x) ≈⟨ ∧-cong (Eq.sym $ ∧-assoc _ _ _) Eq.refl ⟩
  (((x ⇨ y) ∧ x) ∧ (x ⇨ z)) ∧ x  ≈⟨ ∧-assoc _ _ _ ⟩
  (((x ⇨ y) ∧ x) ∧ (x ⇨ z)  ∧ x) ≤⟨ ∧-monotonic ⇨-eval ⇨-eval ⟩
  y ∧ z                          ∎)
  where open POR poset

⇨-distribˡ-∧ : _⇨_ DistributesOverˡ _∧_
⇨-distribˡ-∧ x y z = antisym (⇨-distribˡ-∧-≤ x y z) (⇨-distribˡ-∧-≥ x y z)

⇨-distribˡ-∨-∧-≤ : ∀ x y z → x ∨ y ⇨ z ≤ (x ⇨ z) ∧ (y ⇨ z)
⇨-distribˡ-∨-∧-≤ x y z = let x≤x∨y , y≤x∨y , _ = supremum x y
   in ∧-greatest (transpose-⇨ $ trans (∧-monotonic refl x≤x∨y) ⇨-eval)
                 (transpose-⇨ $ trans (∧-monotonic refl y≤x∨y) ⇨-eval)

⇨-distribˡ-∨-∧-≥ : ∀ x y z → (x ⇨ z) ∧ (y ⇨ z) ≤ x ∨ y ⇨ z
⇨-distribˡ-∨-∧-≥ x y z = transpose-⇨ (trans (reflexive $ ∧-distribˡ-∨ _ _ _)
  (∨-least (trans (transpose-∧ (x∧y≤x _ _)) refl)
           (trans (transpose-∧ (x∧y≤y _ _)) refl)))

⇨-distribˡ-∨-∧ : ∀ x y z → x ∨ y ⇨ z ≈ (x ⇨ z) ∧ (y ⇨ z)
⇨-distribˡ-∨-∧ x y z = antisym (⇨-distribˡ-∨-∧-≤ x y z) (⇨-distribˡ-∨-∧-≥ x y z)

------------------------------------------------------------------------
-- Heyting algebras are distributive lattices

isDistributiveLattice : IsDistributiveLattice _≈_ _≤_ _∨_ _∧_
isDistributiveLattice = record
  { isLattice    = isLattice
  ; ∧-distribˡ-∨ = ∧-distribˡ-∨
  }

distributiveLattice : DistributiveLattice _ _ _
distributiveLattice = record
  { isDistributiveLattice = isDistributiveLattice
  }

------------------------------------------------------------------------
-- Heyting algebras can define pseudo-complement

infix 8 ¬_

¬_ : Op₁ Carrier
¬ x = x ⇨ ⊥

x≤¬¬x : ∀ x → x ≤ ¬ ¬ x
x≤¬¬x x = transpose-⇨ (trans (reflexive (∧-comm _ _)) ⇨-eval)

------------------------------------------------------------------------
-- De-Morgan laws

de-morgan₁ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y
de-morgan₁ x y = ⇨-distribˡ-∨-∧ _ _ _

de-morgan₂-≤ : ∀ x y → ¬ (x ∧ y) ≤ ¬ ¬ (¬ x ∨ ¬ y)
de-morgan₂-≤ x y = transpose-⇨ $ begin
  ¬ (x ∧ y) ∧ ¬ (¬ x ∨ ¬ y)     ≈⟨ ∧-cong ⇨-curry (de-morgan₁ _ _) ⟩
  (x ⇨ ¬ y) ∧ ¬ ¬ x ∧ ¬ ¬ y     ≈⟨ ∧-cong Eq.refl (∧-comm _ _) ⟩
  (x ⇨ ¬ y) ∧ ¬ ¬ y ∧ ¬ ¬ x     ≈⟨ Eq.sym $ ∧-assoc _ _ _ ⟩
  ((x ⇨ ¬ y) ∧ ¬ ¬ y) ∧ ¬ ¬ x   ≤⟨ ⇨-applyʳ $ transpose-⇨ $
    begin
      ((x ⇨ ¬ y) ∧ ¬ ¬ y) ∧ x   ≈⟨ ∧-cong (∧-comm _ _) Eq.refl ⟩
      ((¬ ¬ y) ∧ (x ⇨ ¬ y)) ∧ x ≈⟨ ∧-assoc _ _ _ ⟩
      (¬ ¬ y) ∧ (x ⇨ ¬ y) ∧ x   ≤⟨ ∧-monotonic refl ⇨-eval ⟩
      ¬ ¬ y ∧ ¬ y               ≤⟨ ⇨-eval ⟩
      ⊥                         ∎ ⟩
  ⊥                             ∎
  where open POR poset

de-morgan₂-≥ : ∀ x y → ¬ ¬ (¬ x ∨ ¬ y) ≤ ¬ (x ∧ y)
de-morgan₂-≥ x y = transpose-⇨ $ ⇨-applyˡ $ transpose-⇨ $ begin
  (x ∧ y) ∧ (¬ x ∨ ¬ y)         ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩
  (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≤⟨ ∨-monotonic (⇨-applyʳ (x∧y≤x _ _))
                                               (⇨-applyʳ (x∧y≤y _ _)) ⟩
  ⊥ ∨ ⊥                         ≈⟨ ∨-idempotent _ ⟩
  ⊥                             ∎
  where open POR poset

de-morgan₂ : ∀ x y → ¬ (x ∧ y) ≈ ¬ ¬ (¬ x ∨ ¬ y)
de-morgan₂ x y = antisym (de-morgan₂-≤ x y) (de-morgan₂-≥ x y)

weak-lem : ∀ {x} → ¬ ¬ (¬ x ∨ x) ≈ ⊤
weak-lem {x} = begin
  ¬ ¬ (¬ x ∨ x)   ≈⟨ ⇨-cong (de-morgan₁ _ _) Eq.refl ⟩
  ¬ (¬ ¬ x ∧ ¬ x) ≈⟨ ⇨-cong ⇨-app Eq.refl ⟩
  ⊥ ∧ (x ⇨ ⊥) ⇨ ⊥ ≈⟨ ⇨-cong (∧-zeroˡ _) Eq.refl ⟩
  ⊥ ⇨ ⊥           ≈⟨ ⇨-unit ⟩
  ⊤               ∎
  where open EqReasoning setoid


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Many properties which hold for _∼_ also hold for flip _∼_
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Flip where

open import Function
open import Data.Product

implies : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
          (≈ : REL A B ℓ₁) (∼ : REL A B ℓ₂) →
          ≈ ⇒ ∼ → flip ≈ ⇒ flip ∼
implies _ _ impl = impl

reflexive : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) →
            Reflexive ∼ → Reflexive (flip ∼)
reflexive _ refl = refl

irreflexive : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
              (≈ : REL A B ℓ₁) (∼ : REL A B ℓ₂) →
              Irreflexive ≈ ∼ → Irreflexive (flip ≈) (flip ∼)
irreflexive _ _ irrefl = irrefl

symmetric : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) →
            Symmetric ∼ → Symmetric (flip ∼)
symmetric _ sym = sym

transitive : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) →
             Transitive ∼ → Transitive (flip ∼)
transitive _ trans = flip trans

antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂) →
                Antisymmetric ≈ ≤ → Antisymmetric (flip ≈) (flip ≤)
antisymmetric _ _ antisym = antisym

asymmetric : ∀ {a ℓ} {A : Set a} (< : Rel A ℓ) →
             Asymmetric < → Asymmetric (flip <)
asymmetric _ asym = asym

respects : ∀ {a ℓ p} {A : Set a} (∼ : Rel A ℓ) (P : A → Set p) →
           Symmetric ∼ → P Respects ∼ → P Respects flip ∼
respects _ _ sym resp ∼ = resp (sym ∼)

respects₂ : ∀ {a ℓ₁ ℓ₂} {A : Set a} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) →
            Symmetric ∼₂ → ∼₁ Respects₂ ∼₂ → flip ∼₁ Respects₂ flip ∼₂
respects₂ _ _ sym (resp₁ , resp₂) =
  ((λ {_} {_} {_} ∼ → resp₂ (sym ∼)) , λ {_} {_} {_} ∼ → resp₁ (sym ∼))

decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} (∼ : REL A B ℓ) →
            Decidable ∼ → Decidable (flip ∼)
decidable _ dec x y = dec y x

total : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) →
        Total ∼ → Total (flip ∼)
total _ tot x y = tot y x

trichotomous : ∀ {a ℓ₁ ℓ₂} {A : Set a} (≈ : Rel A ℓ₁) (< : Rel A ℓ₂) →
               Trichotomous ≈ < → Trichotomous (flip ≈) (flip <)
trichotomous _ _ compare x y = compare y x

isEquivalence : ∀ {a ℓ} {A : Set a} {≈ : Rel A ℓ} →
                IsEquivalence ≈ → IsEquivalence (flip ≈)
isEquivalence {≈ = ≈} eq = record
  { refl  = reflexive  ≈ Eq.refl
  ; sym   = symmetric  ≈ Eq.sym
  ; trans = transitive ≈ Eq.trans
  }
  where module Eq = IsEquivalence eq

setoid : ∀ {s₁ s₂} → Setoid s₁ s₂ → Setoid s₁ s₂
setoid S = record
  { _≈_           = flip S._≈_
  ; isEquivalence = isEquivalence S.isEquivalence
  } where module S = Setoid S

isPreorder : ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} →
             IsPreorder ≈ ∼ → IsPreorder (flip ≈) (flip ∼)
isPreorder {≈ = ≈} {∼} pre = record
  { isEquivalence = isEquivalence Pre.isEquivalence
  ; reflexive     = implies ≈ ∼ Pre.reflexive
  ; trans         = transitive ∼ Pre.trans
  }
  where module Pre = IsPreorder pre

preorder : ∀ {p₁ p₂ p₃} → Preorder p₁ p₂ p₃ → Preorder p₁ p₂ p₃
preorder P = record
  { _∼_        = flip P._∼_
  ; _≈_        = flip P._≈_
  ; isPreorder = isPreorder P.isPreorder
  } where module P = Preorder P

isDecEquivalence : ∀ {a ℓ} {A : Set a} {≈ : Rel A ℓ} →
                   IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
isDecEquivalence {≈ = ≈} dec = record
  { isEquivalence = isEquivalence Dec.isEquivalence
  ; _≟_           = decidable ≈ Dec._≟_
  }
  where module Dec = IsDecEquivalence dec

decSetoid : ∀ {s₁ s₂} → DecSetoid s₁ s₂ → DecSetoid s₁ s₂
decSetoid S = record
  { _≈_              = flip S._≈_
  ; isDecEquivalence = isDecEquivalence S.isDecEquivalence
  } where module S = DecSetoid S

isPartialOrder : ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                 IsPartialOrder ≈ ≤ →
                 IsPartialOrder (flip ≈) (flip ≤)
isPartialOrder {≈ = ≈} {≤} po = record
  { isPreorder = isPreorder Po.isPreorder
  ; antisym    = antisymmetric ≈ ≤ Po.antisym
  }
  where module Po = IsPartialOrder po

poset : ∀ {p₁ p₂ p₃} → Poset p₁ p₂ p₃ → Poset p₁ p₂ p₃
poset O = record
  { _≈_            = flip O._≈_
  ; _≤_            = flip O._≤_
  ; isPartialOrder = isPartialOrder O.isPartialOrder
  } where module O = Poset O

isStrictPartialOrder :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
  IsStrictPartialOrder ≈ < → IsStrictPartialOrder (flip ≈) (flip <)
isStrictPartialOrder {≈ = ≈} {<} spo = record
  { isEquivalence = isEquivalence Spo.isEquivalence
  ; irrefl        = irreflexive ≈ < Spo.irrefl
  ; trans         = transitive < Spo.trans
  ; <-resp-≈      = respects₂ < ≈ Spo.Eq.sym Spo.<-resp-≈
  }
  where module Spo = IsStrictPartialOrder spo

strictPartialOrder :
  ∀ {s₁ s₂ s₃} →
  StrictPartialOrder s₁ s₂ s₃ → StrictPartialOrder s₁ s₂ s₃
strictPartialOrder O = record
  { _≈_                  = flip O._≈_
  ; _<_                  = flip O._<_
  ; isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
  } where module O = StrictPartialOrder O

isTotalOrder :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
  IsTotalOrder ≈ ≤ → IsTotalOrder (flip ≈) (flip ≤)
isTotalOrder {≈ = ≈} {≤} to = record
  { isPartialOrder = isPartialOrder To.isPartialOrder
  ; total          = total ≤ To.total
  }
  where module To = IsTotalOrder to

totalOrder : ∀ {t₁ t₂ t₃} → TotalOrder t₁ t₂ t₃ → TotalOrder t₁ t₂ t₃
totalOrder O = record
  { _≈_          = flip O._≈_
  ; _≤_          = flip O._≤_
  ; isTotalOrder = isTotalOrder O.isTotalOrder
  } where module O = TotalOrder O

isDecTotalOrder :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
  IsDecTotalOrder ≈ ≤ → IsDecTotalOrder (flip ≈) (flip ≤)
isDecTotalOrder {≈ = ≈} {≤} dec = record
  { isTotalOrder = isTotalOrder Dec.isTotalOrder
  ; _≟_          = decidable ≈ Dec._≟_
  ; _≤?_         = decidable ≤ Dec._≤?_
  }
  where module Dec = IsDecTotalOrder dec

decTotalOrder :
  ∀ {d₁ d₂ d₃} → DecTotalOrder d₁ d₂ d₃ → DecTotalOrder d₁ d₂ d₃
decTotalOrder O = record
  { _≈_             = flip O._≈_
  ; _≤_             = flip O._≤_
  ; isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
  } where module O = DecTotalOrder O

isStrictTotalOrder :
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
  IsStrictTotalOrder ≈ < → IsStrictTotalOrder (flip ≈) (flip <)
isStrictTotalOrder {≈ = ≈} {<} sto = record
  { isEquivalence = isEquivalence Sto.isEquivalence
  ; trans         = transitive < Sto.trans
  ; compare       = trichotomous ≈ < Sto.compare
  ; <-resp-≈      = respects₂ < ≈ Sto.Eq.sym Sto.<-resp-≈
  }
  where module Sto = IsStrictTotalOrder sto

strictTotalOrder :
  ∀ {s₁ s₂ s₃} → StrictTotalOrder s₁ s₂ s₃ → StrictTotalOrder s₁ s₂ s₃
strictTotalOrder O = record
  { _≈_                = flip O._≈_
  ; _<_                = flip O._<_
  ; isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
  } where module O = StrictTotalOrder O


text:
module Unsolved-meta-in-module-application where

module M (A : Set) where

open M _ public

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Closed monoid in the skew-closed category of families
module SOAS.Abstract.Monoid {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.ContextMaps.Combinators

open import SOAS.Construction.Structure as Structure

open import SOAS.Abstract.Hom {T}
open import SOAS.Abstract.Coalgebra using (module Sorted) ; open Sorted
open import SOAS.Families.Core {T}

open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)

open import SOAS.Coalgebraic.Map {T}
open import SOAS.Coalgebraic.Lift {T}

private
  variable
    Γ Δ Θ : Ctx
    α β γ : T

record Mon (𝒳 : Familyₛ) : Set where
  field
    η : ℐ ⇾̣ 𝒳
    μ : 𝒳 ⇾̣ 〖 𝒳 , 𝒳 〗

    lunit : {σ : Γ ~[ 𝒳 ]↝ Δ}{v : ℐ α Γ}
          → μ (η v) σ ≡ σ v
    runit : {t : 𝒳 α Γ} → μ t η ≡ t
    assoc : {σ : Γ ~[ 𝒳 ]↝ Δ}{ς : Δ ~[ 𝒳 ]↝ Θ} {t : 𝒳 α Γ}
          → μ (μ t σ) ς ≡ μ t (λ v → μ (σ v) ς)

  -- Congruence in both arguments of the multiplication
  μ≈₁ : {t₁ t₂ : 𝒳 α Γ}{σ : Γ ~[ 𝒳 ]↝ Δ}
      → t₁ ≡ t₂
      → μ t₁ σ ≡ μ t₂ σ
  μ≈₁ refl = refl

  μ≈₂ : {t : 𝒳 α Γ}{σ ς : Γ ~[ 𝒳 ]↝ Δ}
      → ({τ : T}{v : ℐ τ Γ} → σ v ≡ ς v)
      → μ t σ ≡ μ t ς
  μ≈₂ {t = t} p = cong (μ t) (dext′ p)

  -- Monoids are pointed coalgebras
  ᵇ : Coalg 𝒳
  ᵇ = record { r = λ t ρ →  μ t (η ∘ ρ) ; counit = runit
    ; comult = λ { {t = t} → sym (trans assoc (μ≈₂ lunit)) } }

  ᴮ : Coalgₚ 𝒳
  ᴮ = record { ᵇ = ᵇ ; η = η ; r∘η = lunit }

  -- Single-variable substitution
  [_/] : 𝒳 α Γ → 𝒳 β (α ∙ Γ) → 𝒳 β Γ
  [ s /] t = μ t (add 𝒳 s η)

  -- Substitution for second variable
  [_/]′ : 𝒳 α Γ → 𝒳 γ (β ∙ α ∙ Γ) → 𝒳 γ (β ∙ Γ)
  [ s /]′ t = μ t (lift₁ ᴮ (add 𝒳 s η))

  -- Substitution for top two variables
  [_,_/]₂ : 𝒳 α Γ → 𝒳 β Γ → 𝒳 γ (α ∙ β ∙ Γ) → 𝒳 γ Γ
  [ s₁ , s₂ /]₂ t = μ t (add 𝒳 s₁ (add 𝒳 s₂ η))

  open Coalgₚ ᴮ public using (r ; r∘η)

  -- Multiplication is coalgebraic map
  μᶜ : Coalgebraic ᴮ ᴮ ᴮ μ
  μᶜ = record { r∘f = assoc ; f∘r = trans assoc (μ≈₂ lunit) ; f∘η = lunit }

-- Monoid homomorphisms
record Mon⇒ {𝒳 𝒴 : Familyₛ}(𝒳ᵐ : Mon 𝒳)(𝒴ᵐ : Mon 𝒴)
               (f : 𝒳 ⇾̣ 𝒴) : Set where

  private module 𝒳 = Mon 𝒳ᵐ
  private module 𝒴 = Mon 𝒴ᵐ

  field
    ⟨η⟩ : {v : ℐ α Γ} → f (𝒳.η v) ≡ 𝒴.η v
    ⟨μ⟩ : {σ : Γ ~[ 𝒳 ]↝ Δ}{t : 𝒳 α Γ}
        → f (𝒳.μ t σ) ≡ 𝒴.μ (f t) (f ∘ σ)

  ᵇ⇒ : Coalg⇒ 𝒳.ᵇ 𝒴.ᵇ f
  ᵇ⇒ = record { ⟨r⟩ = trans ⟨μ⟩ (𝒴.μ≈₂ ⟨η⟩) }

  ᴮ⇒ : Coalgₚ⇒ 𝒳.ᴮ 𝒴.ᴮ f
  ᴮ⇒ = record { ᵇ⇒ = ᵇ⇒ ; ⟨η⟩ = ⟨η⟩ }

  -- Preservation of multiplication and unit implies the semantic substitution
  -- lemma for single- and double-variable substitution
  sub-lemma : (s : 𝒳 α Γ)(t : 𝒳 β (α ∙ Γ)) →
              f (𝒳.[ s /] t) ≡ 𝒴.[ f s /] (f t)
  sub-lemma s t = trans ⟨μ⟩ (cong (𝒴.μ (f t))
                        (dext λ{ new → refl ; (old y) → ⟨η⟩}))

  sub-lemma₂ : (s₁ : 𝒳 α Γ)(s₂ : 𝒳 β Γ)(t : 𝒳 γ (α ∙ β ∙ Γ)) →
               f (𝒳.[ s₁ , s₂ /]₂ t) ≡ 𝒴.[ f s₁ , f s₂ /]₂ (f t)
  sub-lemma₂ s₁ s₂ t = trans ⟨μ⟩ (cong (𝒴.μ (f t))
                             (dext λ{ new → refl ; (old new) → refl
                                    ; (old (old y)) → ⟨η⟩}))

module MonoidStructure = Structure 𝔽amiliesₛ Mon

-- Category of substitution monoids
𝕄onoids : Category 1ℓ 0ℓ 0ℓ
𝕄onoids = MonoidStructure.StructCat record
  { IsHomomorphism = Mon⇒
  ; id-hom = record { ⟨η⟩ = refl ; ⟨μ⟩ = refl }
  ; comp-hom = λ g f gᵐ⇒ fᵐ⇒ → record
    { ⟨η⟩ = trans (cong g (⟨η⟩ fᵐ⇒)) (⟨η⟩ gᵐ⇒)
    ; ⟨μ⟩ = trans (cong g (⟨μ⟩ fᵐ⇒)) (⟨μ⟩ gᵐ⇒)
    }
  } where open Mon⇒

module 𝕄on = Category 𝕄onoids

Monoid : Set₁
Monoid = 𝕄on.Obj

Monoid⇒ : Monoid → Monoid → Set
Monoid⇒ = 𝕄on._⇒_

module AsMonoid (ℳᵐ : Monoid) where
  open Object ℳᵐ renaming (𝐶 to ℳ; ˢ to ᵐ) public
  open Mon ᵐ public

module AsMonoid⇒ {ℳᵐ 𝒩ᵐ : Monoid} (fᵐ⇒ : Monoid⇒ ℳᵐ 𝒩ᵐ) where
  open Morphism fᵐ⇒ renaming (𝑓 to f ; ˢ⇒ to ᵐ⇒) public
  open Mon⇒ ᵐ⇒ public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module GUIgeneric.GUIFeaturesPart4 where

open import GUIgeneric.Prelude renaming (addButton to addButton')

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib
open import StateSizedIO.GUI.WxGraphicsLibLevel3 renaming (addButton to addButton')
open import GUIgeneric.GUIFeatures
open import GUIgeneric.GUIFeaturesPart2 hiding ( main )
open import GUIgeneric.GUIFeaturesPart3 hiding ( main )
open import GUIgeneric.GUIExample hiding (main )

open import Data.Product
open import Data.Fin

addStateFMachine  : {BaseState : Set}
                          (vm : FMachine BaseState)
                          (Snew : Set)
                          (newSM : (s : Snew) →
                            SMachineState (BaseState ⊎ vm .AddStateF ⊎ Snew) (inj₂ (inj₂ s)))
                         → FMachine BaseState
addStateFMachine {BaseState} vm Snew newSM .Features = vm .Features
addStateFMachine {BaseState} vm Snew newSM .AddStateF = vm .AddStateF ⊎ Snew
addStateFMachine {BaseState} vm Snew newSM .GUIF f (inj₁ s) =
                mapFMachineHandle (inj₁ s) (vm .GUIF f (inj₁ s))
addStateFMachine {BaseState} vm Snew newSM .GUIF f (inj₂ (inj₁ s)) =
                mapFMachineHandle (inj₂ s) (vm .GUIF f (inj₂ s))
addStateFMachine {BaseState} vm Snew newSM .GUIF f (inj₂ (inj₂ s)) .fSM = newSM s .fSM
addStateFMachine {BaseState} vm Snew newSM .GUIF f (inj₂ (inj₂ s)) .propSM = newSM s .propSM
addStateFMachine {BaseState} vm Snew newSM .GUIF f (inj₂ (inj₂ s)) .handlSM = newSM s .handlSM

addOneStateFMachine  : {BaseState : Set}
                          (vm : FMachine BaseState)
                          (newSM : SMachineState (BaseState ⊎ vm .AddStateF ⊎ ⊤) (inj₂ (inj₂ _)))
                         → FMachine BaseState
addOneStateFMachine vm newSM = addStateFMachine vm ⊤ λ _ → newSM

addDummyFeatures  : {BaseState : Set}
                                  (vm : FMachine BaseState)
                                  (FeatureNew : Set)
                                   → FMachine BaseState
addDummyFeatures vm FeatureNew .Features = vm .Features × FeatureNew
addDummyFeatures vm FeatureNew .AddStateF = vm .AddStateF
addDummyFeatures vm FeatureNew .GUIF (f , _) s = vm .GUIF f s

{- handler for the new state to be added to the cancel machine -}
cancelNewStateSM : (vm : FMachine StateV) →
                    SMachineState (StateV ⊎ vm .AddStateF ⊎ ⊤) (inj₂ (inj₂ tt))
cancelNewStateSM vm = simpleSMState "Intermediate" (inj₁ s0)

{- add the state to the old feature machine -}
cancelStateAdded : FMachine StateV → FMachine StateV
cancelStateAdded vm = addOneStateFMachine vm (cancelNewStateSM vm)

{- add a dummy feature "FeatureCancel" to the feature machine -}
cancelFeatureAdded : FMachine StateV → FMachine StateV
cancelFeatureAdded vm = addDummyFeatures
                         (cancelStateAdded vm)
                         FeatureCancel

{- redefine in the feature machine one button -}
Cancel' : FMachine StateV → FMachine StateV
Cancel' vm .Features = cancelFeatureAdded vm .Features
Cancel' vm .AddStateF  = cancelFeatureAdded vm .AddStateF
Cancel' vm .GUIF (f , yesCancel) (inj₁ s1) =
      addBtn2StateMachine (cancelFeatureAdded vm .GUIF (f , yesCancel) (inj₁ s1))
                          "Cancel" (inj₂ (inj₂ _))
Cancel' vm .GUIF f  s = cancelFeatureAdded vm .GUIF f s

main : NativeIO Unit
main = compileFeatureVM (Cancel' baseF) (_ , yesCancel) (inj₁ s0) --

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
module Nat where

open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality as Eq
open import Data.Empty
open import Level hiding (zero)

data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ

open Eq.≡-Reasoning

¬_ : { ℓ : Level} → Set ℓ → Set ℓ
¬ P = P → ⊥

≡-succ : (n m : ℕ) → succ n ≡ succ m → n ≡ m
≡-succ zero .zero refl = refl
≡-succ (succ n) .(succ n) refl = refl

sn≢0 : (n : ℕ) → ¬ (succ n ≡ zero)
sn≢0 _ ()

_+_ : ℕ → ℕ → ℕ
zero + m = m
succ n + m = succ (n + m)

_*_ : ℕ → ℕ → ℕ
zero * _ = zero
succ n * m = m + (n * m)

+-rUnit : (n : ℕ) → n + zero ≡ n
+-rUnit zero = refl
+-rUnit (succ n) = cong succ (+-rUnit n)

+-lUnit : (n : ℕ) → zero + n ≡ n
+-lUnit _ = refl

+-assoc : (n m l : ℕ) → n + (m + l) ≡ (n + m) + l
+-assoc zero m l = refl
+-assoc (succ n) m l = cong succ (+-assoc n m l)

+-right : (n m : ℕ) → n + succ m ≡ succ (n + m)
+-right zero m = refl
+-right (succ n) m = cong succ (+-right n m)

+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm zero n = sym (+-rUnit n)
+-comm (succ m) n = begin
        succ (m + n)
    ≡⟨ cong succ (+-comm m n) ⟩
        succ (n + m)
    ≡⟨ sym (+-right n m) ⟩
        n + succ m
    ∎

+-lCancel : (n m l : ℕ) → l + n ≡ l + m → n ≡ m
+-lCancel n m zero p = p
+-lCancel n m (succ l) p = +-lCancel n m l (≡-succ (l + n) (l + m) p)

+-rCancel : (n m l : ℕ) → n + l ≡ m + l → n ≡ m
+-rCancel n m zero p =
    begin
        n
    ≡⟨ sym (+-rUnit n) ⟩
        n + zero
    ≡⟨ p ⟩
        m + zero
    ≡⟨ +-rUnit m ⟩
        m
    ∎
+-rCancel n m (succ l) n+sl≡m+sl = +-rCancel n m l (≡-succ (n + l) (m + l)
    (begin
        succ (n + l)
    ≡⟨ sym (+-right n l) ⟩
        n + succ l
    ≡⟨ n+sl≡m+sl ⟩
        m + succ l
    ≡⟨ +-right m l ⟩
        succ (m + l)
    ∎))

*-rAbsorp : (n : ℕ) → n * zero ≡ zero
*-rAbsorp zero = refl
*-rAbsorp (succ n) = begin
        succ n * zero
    ≡⟨ refl ⟩
        zero + (n * zero)
    ≡⟨ cong (λ x → zero + x) (*-rAbsorp n) ⟩
        zero + zero
    ≡⟨ refl ⟩
        zero
    ∎

*-right : (m n : ℕ) → m * succ n ≡ (m * n) + m
*-right zero n = begin
        zero * succ n
    ≡⟨ refl ⟩
        zero
    ≡⟨ refl ⟩
        zero * n
    ≡⟨ +-rUnit (zero * n) ⟩
        (zero * n) + zero
    ∎
*-right (succ m) n = begin
        succ m * succ n
    ≡⟨ refl ⟩
        succ n + (m * succ n)
    ≡⟨ cong (λ x → succ n + x) (*-right m n) ⟩
        succ n + ((m * n) + m)
    ≡⟨ refl ⟩
        succ (n + ((m * n) + m))
    ≡⟨ cong succ (+-assoc n (m * n) m) ⟩
        succ ((n + (m * n)) + m)
    ≡⟨ sym (+-right (n + (m * n)) m) ⟩
        (succ m * n) + succ m
    ∎

+*-rDist : (m n l : ℕ) → (m + n) * l ≡ (m * l) + (n * l)
+*-rDist m n zero = begin
        (m + n) * zero
    ≡⟨ *-rAbsorp (m + n) ⟩
        zero
    ≡⟨ sym (*-rAbsorp m) ⟩
        m * zero
    ≡⟨ sym (+-rUnit (m * zero)) ⟩
        (m * zero) + zero
    ≡⟨ cong (λ x → (m * zero) + x) (sym (*-rAbsorp n)) ⟩
        (m * zero) + (n * zero)
    ∎
+*-rDist m n (succ l) = begin
        (m + n) * succ l
    ≡⟨ *-right (m + n) l ⟩
        ((m + n) * l) + (m + n)
    ≡⟨ cong (λ x → x + (m + n)) (+*-rDist m n l) ⟩
        ((m * l) + (n * l)) + (m + n)
    ≡⟨ +-assoc ((m * l) + (n * l)) m n ⟩
        (((m * l) + (n * l)) + m) + n
    ≡⟨ cong (λ x → x + n) (sym (+-assoc (m * l) (n * l) m)) ⟩
        ((m * l) + ((n * l) + m)) + n
    ≡⟨ cong (λ x → x + n) (cong (λ x → (m * l) + x) (+-comm (n * l) m)) ⟩
        ((m * l) + (m + (n * l))) + n
    ≡⟨ cong (λ x → x + n) (+-assoc (m * l) m (n * l)) ⟩
        (((m * l) + m) + (n * l)) + n
    ≡⟨ sym (+-assoc ((m * l) + m) (n * l) n) ⟩
        ((m * l) + m) + ((n * l) + n)
    ≡⟨ cong (λ x → x + ((n * l) + n)) (sym (*-right m l)) ⟩
        (m * succ l) + ((n * l) + n)
    ≡⟨ cong (λ x → (m * succ l) + x) (sym (*-right n l)) ⟩
        (m * succ l) + (n * succ l)
    ∎

*-assoc : (m n l : ℕ) → m * (n * l) ≡ (m * n) * l
*-assoc zero n l = refl
*-assoc (succ m) n l = begin
        succ m * (n * l)
    ≡⟨ refl ⟩
        (n * l) + (m * (n * l))
    ≡⟨ cong (λ x → (n * l) + x) (*-assoc m n l) ⟩
        (n * l) + ((m * n) * l)
    ≡⟨ sym (+*-rDist n (m * n) l) ⟩
        (n + (m * n)) * l
    ≡⟨ refl ⟩
        (succ m * n) * l
    ∎

*-comm : (m n : ℕ) → m * n ≡ n * m
*-comm zero n = sym (*-rAbsorp n)
*-comm (succ m) n = begin
        succ m * n
    ≡⟨ refl ⟩
        n + (m * n)
    ≡⟨ +-comm n (m * n) ⟩
        (m * n) + n
    ≡⟨ cong (λ x → x + n) (*-comm m n) ⟩
        (n * m) + n
    ≡⟨ sym (*-right n m) ⟩
        n * succ m
    ∎

_≤_ : ℕ → ℕ → Set
n ≤ m = Σ ℕ (λ l → n + l ≡ m)

≤-refl : (n : ℕ) → n ≤ n
≤-refl zero = zero , refl
≤-refl (succ n) = zero ,
    (begin
        (succ n + zero)
    ≡⟨ +-rUnit (succ n) ⟩
        (succ n)
    ∎)

0≤n : (n : ℕ) → zero ≤ n
0≤n zero = ≤-refl zero
0≤n (succ n) = succ n , refl

≤-trans : (n m l : ℕ) → n ≤ m → m ≤ l → n ≤ l
≤-trans zero m l p q = l , refl
≤-trans (succ n) m l (a , succn+a≡m) (b , m+b≡l)
    = (a + b) , (begin
        succ n + (a + b)
    ≡⟨ +-assoc (succ n) a b ⟩
        (succ n + a) + b
    ≡⟨ cong (λ x → x + b) succn+a≡m ⟩
        m + b
    ≡⟨ m+b≡l ⟩
        l
    ∎)

+-lZero : (n m : ℕ) → n + m ≡ zero → n ≡ zero
+-lZero zero m = λ _ → refl
+-lZero (succ n) m ()

≤-antisym : (n m : ℕ) → n ≤ m → m ≤ n → n ≡ m
≤-antisym n m (c , n+c≡m) (d , m+d≡n) = trans (sym n+c≡n) n+c≡m
    where
        c≡0 : c ≡ zero
        c≡0 = +-lZero c d (+-lCancel (c + d) zero n (
            begin
                n + (c + d)
            ≡⟨ +-assoc n c d ⟩
                (n + c) + d
            ≡⟨ cong (λ x → x + d) n+c≡m ⟩
                m + d
            ≡⟨ m+d≡n ⟩
                n
            ≡⟨ sym (+-rUnit n) ⟩
                n + zero
            ∎))
        n+c≡n : n + c ≡ n
        n+c≡n = begin
                n + c
            ≡⟨ cong (λ x → n + x) c≡0 ⟩
                n + zero
            ≡⟨ +-rUnit n ⟩
                n
            ∎

n+s0≡sn : (n : ℕ) → n + succ zero ≡ succ n
n+s0≡sn n = begin
        n + succ zero
    ≡⟨ +-right n zero ⟩
        succ (n + zero)
    ≡⟨ cong succ (+-rUnit n) ⟩
        succ n
    ∎

n≤sn : (n : ℕ) → n ≤ succ n
n≤sn n = succ zero , n+s0≡sn n

ℕ-ω : (n : ℕ) → n ≡ zero ⊎ Σ ℕ (λ c → n ≡ succ c)
ℕ-ω zero = inj₁ refl
ℕ-ω (succ n) = inj₂ (n , refl)

m+sn≡sm+n : (m n : ℕ) → m + succ n ≡ succ m + n
m+sn≡sm+n m zero = begin
        m + succ zero
    ≡⟨ n+s0≡sn m ⟩
        succ m
    ≡⟨ sym (+-rUnit (succ m)) ⟩
        succ m + zero
    ∎
m+sn≡sm+n m (succ n) = begin
        m + succ (succ n)
    ≡⟨ +-right m (succ n) ⟩
        succ (m + succ n)
    ≡⟨ cong succ (m+sn≡sm+n m n) ⟩
        succ (succ m + n)
    ≡⟨ sym (+-right (succ m) n) ⟩
        succ m + succ n
    ∎

sn≤m : (n m : ℕ) → n ≤ m → ¬ (n ≡ m) → succ n ≤ m
sn≤m n m (c , n+c≡m) q = lem (ℕ-ω c)
    where
        n+c≡n : c ≡ zero → n + c ≡ n
        n+c≡n p = begin
                n + c
            ≡⟨ cong (λ x → n + x) p ⟩
                n + zero
            ≡⟨ +-rUnit n ⟩
                n
            ∎
        lem : c ≡ zero ⊎ Σ ℕ (λ d → c ≡ succ d) → succ n ≤ m
        lem (inj₁ x) = ⊥-elim (q (trans (sym (n+c≡n x)) n+c≡m))
        lem (inj₂ (d , c≡sd)) = d , (begin
                succ n + d
            ≡⟨ sym (m+sn≡sm+n n d) ⟩
                n + succ d
            ≡⟨ sym (cong (λ x → n + x) c≡sd) ⟩
                n + c
            ≡⟨ n+c≡m ⟩
                m
            ∎)

≤-all : (m n : ℕ) → m ≤ n ⊎ n ≤ m
≤-all m zero = inj₂ (m , refl)
≤-all m (succ n) = lem (≤-all m n)
    where
        lem : m ≤ n ⊎ n ≤ m → m ≤ succ n ⊎ succ n ≤ m
        lem (inj₁ x) = inj₁ (≤-trans m n (succ n) x (n≤sn n))
        lem (inj₂ (zero , n+zero≡m)) = inj₁ (succ zero , (begin
                m + succ zero
            ≡⟨ +-right m zero ⟩
                succ (m + zero)
            ≡⟨ cong succ (+-rUnit m) ⟩
                succ m
            ≡⟨ cong succ (sym n+zero≡m) ⟩
                succ (n + zero)
            ≡⟨ cong succ (+-rUnit n) ⟩
                succ n
            ∎))
        lem (inj₂ (succ c , n+sc≡m)) = inj₂ (c , (begin
                succ n + c
            ≡⟨ refl ⟩
                succ (n + c)
            ≡⟨ sym (+-right n c) ⟩
                n + succ c
            ≡⟨ n+sc≡m ⟩
                m
            ∎))

+-mono : (m n l : ℕ) → m ≤ n → (m + l) ≤ (n + l)
+-mono m n zero (c , m+c≡n) = c , (begin
        (m + zero) + c
    ≡⟨ cong (λ x → x + c) (+-rUnit m) ⟩
        m + c
    ≡⟨ m+c≡n ⟩
        n
    ≡⟨ sym (+-rUnit n) ⟩
        n + zero
    ∎)
+-mono m n (succ l) (c , m+c≡n) = lem (+-mono m n l (c , m+c≡n))
    where
        lem : (m + l) ≤ (n + l) → (m + succ l) ≤ (n + succ l)
        lem (d , m+l+d≡n+l) = d , (begin
                (m + succ l) + d
            ≡⟨ cong (λ x → x + d) (+-right m l) ⟩
                succ (m + l) + d
            ≡⟨ refl ⟩
                succ ((m + l) + d)
            ≡⟨ cong succ m+l+d≡n+l ⟩
                succ (n + l)
            ≡⟨ sym (+-right n l) ⟩
                n + succ l
            ∎)

*-mono : (m n l : ℕ) → m ≤ n → (m * l) ≤ (n * l)
*-mono m n zero (c , m+c≡n) = zero , (begin
        (m * zero) + zero
    ≡⟨ +-rUnit (m * zero) ⟩
        m * zero
    ≡⟨ trans (*-rAbsorp m) (sym (*-rAbsorp n)) ⟩
        n * zero
    ∎)
*-mono m n (succ l) (c , m+c≡n) = lem (*-mono m n l (c , m+c≡n))
    where
        lem : (m * l) ≤ (n * l) → (m * succ l) ≤ (n * succ l)
        lem (d , m*l+d≡n*l) = (c * succ l) , sym (begin
                n * succ l
            ≡⟨ cong (λ x → x * succ l) (sym m+c≡n) ⟩
                (m + c) * succ l
            ≡⟨ +*-rDist m c (succ l) ⟩
                (m * succ l) + (c * succ l)
            ∎)

s≤s : (m n : ℕ) → m ≤ n → succ m ≤ succ n
s≤s zero n (c , c≡n) = n , refl
s≤s (succ m) n (c , sm+c≡n) = c , cong succ sm+c≡n

data _≲_ : ℕ → ℕ → Set where
    0≲n : {n : ℕ} → zero ≲ n
    s≲s : {n m : ℕ} → n ≲ m → succ n ≲ succ m

≤-≲ : (m n : ℕ) → m ≤ n → m ≲ n
≤-≲ zero _ _ = 0≲n
≤-≲ (succ m) zero (c , ())
≤-≲ (succ m) (succ n) (c , m+c≡n) = s≲s (≤-≲ m n (c , ≡-succ (m + c) n m+c≡n))

≲-≤ : (m n : ℕ) → m ≲ n → m ≤ n
≲-≤ .zero n 0≲n = n , refl
≲-≤ (succ m) (succ n) (s≲s p) = s≤s m n (≲-≤ m n p)

max_stars_repo_name: karrym/NatToReal

max_issues_repo_name: karrym/NatToReal

max_forks_repo_name: karrym/NatToReal


text:
-- mostly adapted from Agda stdlib

module level where

import Agda.Primitive

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

level = Level

lone : level
lone = lsuc lzero

record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

open Lift public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Issue327 where

open import Common.Prelude
open import Common.Reflect

_==_ : QName → QName → Bool
_==_ = primQNameEquality

postulate
  Dec : Bool → Set
  _≟_ : (x y : QName) → Dec (x == y)

Foo : Set₁
Foo with quote Foo ≟ quote Foo
... | _ = Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}
{-# OPTIONS --allow-unsolved-metas #-}

module Light.Implementation.Relation.Binary.Equality.Propositional.Decidable where

import Light.Implementation.Relation.Binary.Equality.Propositional as Propositional
open import Light.Library.Relation.Decidable using (Decidable ; yes ; no ; if_then_else_ ; from‐witness)
open import Light.Variable.Sets
open import Light.Library.Relation.Binary.Equality using (_≈_ ; SelfEquality ; wrap)
open import Light.Library.Relation.Binary
      using (SelfSymmetric ; SelfTransitive ; Reflexive ; Binary ; SelfBinary ; Symmetric ; Transitive ; CongruentFor ; Preserved ; reflexivity ; transitivity ; symmetry ; congruence)
import Light.Implementation.Relation.Decidable
open import Light.Variable.Sets
open import Light.Variable.Levels
open import Light.Library.Relation using (_∧_ ; _⇢_)
open import Light.Library.Data.Product using (first ; second ; both)
import Light.Implementation.Data.Product

module Base {𝕒 : Set aℓ} where
      instance relation : SelfBinary 𝕒
      relation = record { are = λ a b → Decidable (a ≈ b) }

      instance reflexive : Reflexive relation
      reflexive .Reflexive.reflexivity = {!!}

      instance symmetric : SelfSymmetric relation
      symmetric .Symmetric.symmetry a‐≈?‐b =
            if a‐≈?‐b
            then (λ ⦃ b‐≈‐a ⦄ → yes (symmetry b‐≈‐a))
            else (λ ⦃ f ⦄ → no λ b‐≈‐a → f (symmetry b‐≈‐a))

      instance transitive : SelfTransitive relation
      transitive .Transitive.transitivity a‐≈?‐b b‐≈?‐c =
            if a‐≈?‐b ∧ b‐≈?‐c
            then (λ ⦃ a‐≈‐c ⦄ → yes (transitivity (first a‐≈‐c) (second a‐≈‐c)))
            else (λ ⦃ f ⦄ → no λ a‐≈‐c → f (both {!!} {!!}))

      instance equals : SelfEquality 𝕒
      equals = wrap relation

instance base‐congruent : ∀ {f : 𝕒 → 𝕓} → CongruentFor f Base.relation Base.relation
base‐congruent .Preserved.preservation a‐≈?‐c =
      if a‐≈?‐c
      then (λ ⦃ a‐≈‐c ⦄ → yes (congruence a‐≈‐c))
      else λ ⦃ f ⦄ → no λ fa‐≈‐fc → f {!!}

module Main (_≈?_ : ∀ (a b : 𝕒) → Decidable (_≈_ ⦃ r = Propositional.equals ⦄ a b)) where
      instance relation : SelfBinary 𝕒
      relation = record { are = λ a b → a ≈? b }

      open import Agda.Builtin.Equality using (_≡_)

      instance reflexive : Reflexive relation
      reflexive .Reflexive.reflexivity {a = a} = from‐witness {a? = a ≈? a} ⦃ witness = reflexivity ⦄

      instance symmetric : SelfSymmetric relation
      symmetric .Symmetric.symmetry {a = a} {b = b} = from‐witness {a? = (a ≈? b) ⇢ (b ≈? a)} ⦃ witness = symmetry ⦄

      instance transitive : SelfTransitive relation
      transitive .Transitive.transitivity {a = a} {b = b} {c = c} = from‐witness {a? = (a ≈? b) ⇢ ((b ≈? c) ⇢ (a ≈? c))} ⦃ witness = transitivity ⦄

module _ (_≈a?_ : ∀ (a b : 𝕒) → Decidable (_≈_ ⦃ r = Propositional.equals ⦄ a b)) (_≈b?_ : ∀ (a b : 𝕓) → Decidable (_≈_ ⦃ r = Propositional.equals ⦄ a b)) where
      private module A = Main _≈a?_
      private module B = Main _≈b?_

      instance congruent : ∀ {f : 𝕒 → 𝕓} → CongruentFor f A.relation B.relation
      congruent {f = f} .Preserved.preservation {a = a} {c = c} = from‐witness {a? = (a ≈a? c) ⇢ (f a ≈b? f c)} ⦃ witness = congruence ⦄

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

module Categories.Category.Regular where

-- https://ncatlab.org/nlab/show/regular+category
-- https://en.wikipedia.org/wiki/Regular_category

open import Level

open import Categories.Category.Core
open import Categories.Category.Complete.Finitely using (FinitelyComplete)
open import Categories.Diagram.Coequalizer
open import Categories.Diagram.KernelPair
open import Categories.Diagram.Pullback
open import Categories.Morphism.Regular

record Regular {o ℓ e : Level} (𝒞 : Category o ℓ e) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Category 𝒞
  open Pullback

  field
    finitely-complete : FinitelyComplete 𝒞
    coeq-of-kernelpairs : {A B : Obj} (f : A ⇒ B) (kp : KernelPair 𝒞 f) → Coequalizer 𝒞 (p₁ kp) (p₂ kp)
    pullback-of-regularepi-is-regularepi : {A B C : Obj} (f : B ⇒ A) {g : C ⇒ A} → RegularEpi 𝒞 f → (p : Pullback 𝒞 f g) → RegularEpi 𝒞 (p₂ p)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Prelude

module Implicits.Resolution.Stack.Resolution where

open import Coinduction
open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Substitutions
open import Induction
open import Induction.Nat
open import Implicits.Resolution.Termination.Stack

infixl 5 _⊢ᵣ_
infixl 5 _&_⊢ᵣ_ _&_,_⊢_↓_

mutual

  -- Δ & s , r ⊢ a ↓ τ denotes:
  -- Under the context Δ, with stack of resolution goals s, the type a yields simple type τ.
  -- 'r' is used to keep track of the rule from the context that yielded 'a'
  -- ('a' is getting recursively refined)
  data _&_,_⊢_↓_ {ν} (Δ : ICtx ν) :
    ∀ {r} → Stack Δ → r List.∈ Δ → Type ν → SimpleType ν → Set where

    i-simp : ∀ {r s} {r∈Δ : r List.∈ Δ} a → Δ & s , r∈Δ ⊢ simpl a ↓ a
    i-iabs : ∀ {ρ₁ ρ₂ a r s} {r∈Δ : r List.∈ Δ} →
             ρ₁ for r∈Δ ⊬dom s → -- subproblems decrease when recursing
             Δ & (s push ρ₁ for r∈Δ) ⊢ᵣ ρ₁ → -- domain is resolvable
             Δ & s , r∈Δ ⊢ ρ₂ ↓ a → -- codomain matches
             Δ & s , r∈Δ ⊢ ρ₁ ⇒ ρ₂ ↓ a
    i-tabs : ∀ {ρ a r s} {r∈Δ : r List.∈ Δ} b →
             Δ & s , r∈Δ ⊢ ρ tp[/tp b ] ↓ a → Δ & s , r∈Δ ⊢ ∀' ρ ↓ a

  data _&_⊢ᵣ_ {ν} (Δ : ICtx ν) : Stack Δ → Type ν → Set where
    r-simp : ∀ {r τ s} → (r∈Δ : r List.∈ Δ) → Δ & s , r∈Δ ⊢ r ↓ τ → Δ & s ⊢ᵣ simpl τ
    r-iabs : ∀ {ρ₁ ρ₂} {s : Stack Δ} → ((ρ₁ List.∷ Δ) & (s prepend ρ₁) ⊢ᵣ ρ₂) →
             Δ & s ⊢ᵣ (ρ₁ ⇒ ρ₂)
    r-tabs : ∀ {ρ s} → ictx-weaken Δ & stack-weaken s ⊢ᵣ ρ → Δ & s ⊢ᵣ ∀' ρ

-- TODO: This doesn't hold.
-- e.g. we can unify (a → b) with the codomain of a rule (a → b → a) ⇒ (a → b)
-- so the subgoal is larger than the initial goal.
--
-- We instantiate the stack with types that act as 'infinity' on the goal.
-- Every possible 'subgoal' we encounter and push to the stack will certainly
-- be smaller than r
_⊢ᵣ_ : ∀ {ν} → ICtx ν → Type ν → Set
Δ ⊢ᵣ r = Δ & All.tabulate (const r) ⊢ᵣ r


text:
module Data.List where

import      Lvl
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

infixr 1000 _⊰_

-- A list is a container/collection of elements.
-- • The elements are in a linear order.
-- • The container allows multiples (non-uniqueness of elements in the container).
data List (T : Type{ℓ}) : Type{ℓ} where
  ∅   : List(T) -- An empty list
  _⊰_ : T → List(T) → List(T) -- Cons
{-# BUILTIN LIST List #-}

private variable l : List(T)
private variable P : List(T) → Type{ℓ}

elim : P(∅) → (∀(x : T)(l : List(T)) → P(l) → P(x ⊰ l)) → ((l : List(T)) → P(l))
elim base next ∅       = base
elim base next (x ⊰ l) = next(x)(l)(elim base next l)

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:
{-# OPTIONS --without-K --safe #-}

module Data.Fin.Indexed.Literals where

-- import Data.Nat as ℕ
-- import Data.Nat.Properties as ℕ
open import Data.Fin.Indexed.Base
open import Literals.Number
-- open import Relation.Nullary
open import Agda.Builtin.Nat renaming (_<_ to _<ᵇ_)
open import Data.Bool
open import Agda.Builtin.Nat using (_<_)

instance
  numberFin : ∀ {n} → Number (Fin n)
  numberFin {n} = record
    { Constraint = λ m → T (m <ᵇ n)
    ; fromNat    = λ m {{pr}} → FinFromℕ {n} m pr
    }

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2016-09-20 test whether --no-eta-equality is respected

{-# OPTIONS --no-eta-equality #-}

open import Common.Equality

data Wrap (A : Set) : Set where
  wrap : A → Wrap A

record R : Set where
  inductive
  constructor c
  field p : Wrap R
open R

test : ∀ (w : R) → w ≡ c (p w)
test w = refl  -- should fail


text:
{-# OPTIONS -v treeless.opt:20 #-}
-- Test that inlining a recursive function doesn't throw
-- the compiler into a loop.
module _ where

open import Common.Prelude

f : Nat → Nat
f zero = zero
f (suc n) = f n
{-# INLINE f #-}

main : IO Unit
main = printNat (f 4)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Testing a proof done using Hip (Haskell Inductive Prover)
------------------------------------------------------------------------------

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

module SK where

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Algebra.agda and Relation/Binary/Core.agda).
infixl 9 _·_
infix  7 _≡_

postulate
  D   : Set
  K S : D
  _·_ : D → D → D

-- The identity type.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

postulate
 K-eq : ∀ x y → K · x · y ≡ x
 S-eq : ∀ x y z → S · x · y · z ≡ x · z · (y · z)
{-# ATP axioms K-eq S-eq #-}

id : D → D
id x = x
{-# ATP definition id #-}

-- We don't use extensional equality, because _≡_ is not
-- polymorphic. See (Rosén 2012, p. 24).
postulate thm : ∀ x → S · K · K · x ≡ id x
{-# ATP prove thm #-}

------------------------------------------------------------------------------
-- References
--
-- Rosén, D. (2012). Proving Equational Haskell Properties Using
-- Automated Theorem Provers. MA thesis. University of Gothenburg.


text:
module list-merge-sort-test where

open import list
open import nat

open import list-merge-sort ℕ _<_

test-list = 3 :: 2 :: 5 :: 1 :: 1 :: 6 :: 8 :: 9 :: 4 :: []

sorted = merge-sort test-list


text:
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary.Decidable using (False; map)
open import Function.Equivalence as FE using ()

module AKS.Nat.Base where

open import Agda.Builtin.FromNat using (Number)
open import Data.Nat using (ℕ; _+_; _∸_; _*_; _≟_; _<ᵇ_; pred) public
open ℕ public
open import Data.Nat.Literals using (number)

instance
  ℕ-number : Number ℕ
  ℕ-number = number

data ℕ⁺ : Set where
  ℕ+ : ℕ → ℕ⁺

_+⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
ℕ+ n +⁺ ℕ+ m = ℕ+ (suc (n + m))

_*⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
ℕ+ n *⁺ ℕ+ m = ℕ+ (n + m * (suc n))

_≟⁺_ : Decidable {A = ℕ⁺} _≡_
ℕ+ n ≟⁺ ℕ+ m = map (FE.equivalence (λ { refl → refl }) (λ { refl → refl })) (n ≟ m)

⟅_⇑⟆ : ∀ n {≢0 : False (n ≟ zero)} → ℕ⁺
⟅ suc n ⇑⟆ = ℕ+ n

⟅_⇓⟆ : ℕ⁺ → ℕ
⟅ ℕ+ n ⇓⟆ = suc n

instance
  ℕ⁺-number : Number ℕ⁺
  ℕ⁺-number = record
    { Constraint = λ n → False (n ≟ zero)
    ; fromNat = λ n {{≢0}} → ⟅ n ⇑⟆ {≢0}
    }

infix 4 _≤_
record _≤_ (n : ℕ) (m : ℕ) : Set where
  constructor lte
  field
    k : ℕ
    ≤-proof : n + k ≡ m

infix 4 _≥_
_≥_ : ℕ → ℕ → Set
n ≥ m = m ≤ n

infix 4 _≰_
_≰_ : ℕ → ℕ → Set
n ≰ m = ¬ (n ≤ m)

infix 4 _≱_
_≱_ : ℕ → ℕ → Set
n ≱ m = ¬ (m ≤ n)

infix 4 _<_
_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

infix 4 _≮_
_≮_ : ℕ → ℕ → Set
n ≮ m = ¬ (n < m)

infix 4 _>_
_>_ : ℕ → ℕ → Set
n > m = m < n

infix 4 _≯_
_≯_ : ℕ → ℕ → Set
n ≯ m = m ≮ n

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
----------------------------------------------------------------------
-- Functional small-step semantics
----------------------------------------------------------------------

module SystemF.Reduction where

open import Codata.Musical.Notation
open import Category.Monad
open import Category.Monad.Partiality.All
open import Data.Maybe as Maybe using (Maybe; just; nothing; map)
open import Data.Maybe.Relation.Unary.All as MaybeAll using (nothing; just)
open import Data.Maybe.Relation.Unary.Any as MaybeAny using (just)
open import Data.Nat using (ℕ; _+_)
open import Data.Unit using (tt)
open import Data.Vec using ([])
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Relation.Nullary

open import PartialityAndFailure as PF
open PF.Equality hiding (fail)
open PF.Equivalence
private
  open module M {f} = RawMonad (PF.monad {f}) using (_>>=_; return)

open import SystemF.Type
open import SystemF.Term
open import SystemF.WtTerm
open import SystemF.Eval hiding (type-soundness)

open TypeSubst       using () renaming (_[/_]  to _[/tp_])
open TermTypeSubst   using () renaming (_[/_]  to _[/tmTp_])
open TermTermSubst   using () renaming (_[/_]  to _[/tmTm_])
open WtTermTypeSubst using () renaming (_[/_]′ to _[/⊢tmTp_])
open WtTermTermSubst using () renaming (_[/_]  to _[/⊢tmTm_])

----------------------------------------------------------------------
-- Functional call-by-value small-step semantics in the partiality
-- monad

-- The functional presentation of the small-step semantics below is
-- heavily inspired by Danielsson's ICFP'12 paper "Operational
-- Semantics Using the Partiality Monad".  Whereas the paper
-- illustrates the technique to give a functional abstract machine
-- semantics (i.e. the semantics of a "VM"), we skip the compilation
-- step and directly reduce terms, which results in a (functional)
-- structural operational semantics (SOS).  We adopt many of the
-- conventions used in the accompanying code, which can be found at
--
--   http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.tgz
--
-- As pointed out in Danielsson's paper, the functional presentation
-- of the semantics feels rather natural in that it follows the form
-- of an interpreter, and it has the added advantage of proving that
-- the semantics are deterministic and computable "for free".
--
-- For more information about Danielson's paper see
--
--   http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.html

----------------------------------------------------------------------
-- Small-step call-by-value reduction

-- Results of reduction steps
data Result (m n : ℕ) : Set where
  continue : (t : Term m n) → Result m n  -- further reducible term
  done     : (v : Val m n)  → Result m n  -- irreducible value

-- Take a single reduction step (if possible).
step : ∀ {m n} → Term m n → Maybe (Result m n)
step (var x)                 = nothing
step (Λ t)                   = just (done (Λ t))
step (λ' a t)                = just (done (λ' a t))
step (μ a t)                 = just (continue (t [/tmTm μ a t ]))
step (t [ a ])               with step t
... | just (continue t′)     = just (continue (t′ [ a ]))
... | just (done (Λ t′))     = just (continue (t′ [/tmTp a ]))
... | just (done _)          = nothing
... | nothing                = nothing
step {m} {n} (s · t)         with step s
... | just (continue s′)     = just (continue (s′ · t))
... | just (done v)          = nested v
  where -- Call-by-value: only reduce (s · t) if s is a value.
    nested : Val m n → Maybe (Result m n)
    nested v with step t
    nested v         | (just (continue t′)) = just (continue (⌜ v ⌝ · t′))
    nested (λ' _ s′) | (just (done v)) = just (continue (s′ [/tmTm ⌜ v ⌝ ]))
    nested _         | (just (done _)) = nothing
    nested _         | nothing         = nothing
... | nothing                = nothing
step (fold a t)              with step t
... | just (continue t′)     = just (continue (fold a t′))
... | just (done v)          = just (done (fold a v))
... | nothing                = nothing
step (unfold a t)            with step t
... | just (continue t′)     = just (continue (unfold a t′))
... | just (done (fold _ v)) = just (done v)
... | just (done _)          = nothing
... | nothing                = nothing

----------------------------------------------------------------------
-- Type soundness

infix 4 _⊢res_∈_ _⊢res?_∈_

-- Well-typedness lifted to results of reduction steps.
data _⊢res_∈_ {m n} (Γ : Ctx m n) : Result m n → Type n → Set where
  ⊢continue : ∀ {t a} → Γ ⊢    t ∈ a → Γ ⊢res continue t ∈ a
  ⊢done     : ∀ {v a} → Γ ⊢val v ∈ a → Γ ⊢res done v     ∈ a

-- Well-typedness lifted to possibly undefined reduction steps.
_⊢res?_∈_ : ∀ {m n} → Ctx m n → Maybe (Result m n) → Type n → Set
Γ ⊢res? r? ∈ a = MaybeAll.All (λ r → Γ ⊢res r ∈ a) r?

-- Preservation of well-typedness: a well-typed term reduces in one
-- step to a result of the same type or fails to reduce.
⊢step : ∀ {m n} {Γ : Ctx m n} {t a} → Γ ⊢ t ∈ a → Γ ⊢res? step t ∈ a
⊢step (var x)   = nothing
⊢step (Λ ⊢t)    = just (⊢done (Λ ⊢t))
⊢step (λ' a ⊢t) = just (⊢done (λ' a ⊢t))
⊢step (μ a ⊢t)  = just (⊢continue (⊢t [/⊢tmTm μ a ⊢t ]))
⊢step {t = t [ a ]} (⊢t [ .a ]) with step t | ⊢step ⊢t
... | just ._ | just (⊢continue ⊢t′) = just (⊢continue (⊢t′ [ a ]))
... | just ._ | just (⊢done (Λ ⊢t′)) = just (⊢continue (⊢t′ [/⊢tmTp a ]))
... | nothing | nothing              = nothing
⊢step {m} {n} {Γ} {s · t} {b} (⊢s · ⊢t) with step s | ⊢step ⊢s
... | just ._ | just (⊢continue ⊢s′) = just (⊢continue (⊢s′ · ⊢t))
... | just (done (λ' a s′)) | just (⊢done (λ' .a ⊢s′)) = nested
  where
    nested : Γ ⊢res? step ((λ' a s′) · t) ∈ b
    nested with step t | ⊢step ⊢t
    ... | just ._ | just (⊢continue ⊢t′) = just (⊢continue ((λ' a ⊢s′) · ⊢t′))
    ... | just ._ | just (⊢done v) = just (⊢continue (⊢s′ [/⊢tmTm ⊢⌜ v ⌝ ]))
    ... | nothing | nothing        = nothing
... | nothing | nothing = nothing
⊢step {t = fold a t} (fold .a ⊢t) with step t | ⊢step ⊢t
... | just ._ | just (⊢continue ⊢t′) = just (⊢continue (fold a ⊢t′))
... | just ._ | just (⊢done ⊢v)      = just (⊢done (fold a ⊢v))
... | nothing | nothing              = nothing
⊢step {t = unfold a t} (unfold .a ⊢t) with step t | ⊢step ⊢t
... | just ._ | just (⊢continue ⊢t′)      = just (⊢continue (unfold a ⊢t′))
... | just ._ | just (⊢done (fold .a ⊢v)) = just (⊢done ⊢v)
... | nothing | nothing                   = nothing

-- Progress: reduction of well-typed closed terms does not fail.
progress : ∀ {t} {a : Type 0} → [] ⊢ t ∈ a → Maybe.Is-just (step t)
progress (var ())
progress (Λ t) = just tt
progress (λ' a t) = just tt
progress (μ a t) = just tt
progress {t [ a ]} (⊢t [ .a ]) with step t | ⊢step ⊢t | progress ⊢t
... | just ._ | just (⊢continue _) | just tt = just tt
... | just ._ | just (⊢done (Λ _)) | just tt = just tt
progress {s · t} (⊢s · ⊢t) with step s | ⊢step ⊢s | progress ⊢s
... | just ._               | just (⊢continue _)     | just tt = just tt
... | just (done (λ' a s′)) | just (⊢done (λ' .a _)) | just tt = nested
  where
    nested : Maybe.Is-just (step ((λ' a s′) · t))
    nested with step t | ⊢step ⊢t | progress ⊢t
    ... | just ._ | just (⊢continue _) | just tt = just tt
    ... | just ._ | just (⊢done _)     | just tt = just tt
progress {fold a t} (fold .a ⊢t) with step t | ⊢step ⊢t | progress ⊢t
... | just ._ | just (⊢continue _) | just tt = just tt
... | just ._ | just (⊢done _)     | just tt = just tt
progress {unfold a t} (unfold .a ⊢t) with step t | ⊢step ⊢t | progress ⊢t
... | just ._ | just (⊢continue _)       | just tt = just tt
... | just ._ | just (⊢done (fold .a _)) | just tt = just tt

infix 7 _↓ ⊢_↓

-- Evaluation of untyped (open) terms in the partiality monad via
-- repeated reduction.
_↓ : ∀ {m n} → Term m n → Comp m n
t ↓ with step t
... | just (continue t′) = later (♯ (t′ ↓))
... | just (done v)      = return v
... | nothing            = fail

-- Evaluation of closed terms preserves well-typedness.
⊢_↓ : ∀ {t a} → [] ⊢ t ∈ a → [] ⊢comp t ↓ ∈ a
⊢_↓ {t} ⊢t with step t | ⊢step ⊢t | progress ⊢t
... | just (continue t′) | just (⊢continue ⊢t′) | just tt = later (♯ ⊢ ⊢t′ ↓)
... | just (done v)      | just (⊢done ⊢v)      | just tt = now (just ⊢v)
... | nothing            | _                    | ()

-- Type soundness: evaluation of well-typed terms does not fail.
type-soundness : ∀ {t a} → [] ⊢ t ∈ a → ¬ t ↓ ≈ fail
type-soundness ⊢t = does-not-fail ⊢ ⊢t ↓

----------------------------------------------------------------------
-- Strong bisimilarity of big-step and small-step semantics

open PF.AlternativeEquality
  renaming (return to returnP; fail to failP; _>>=_ to _>>=P_)

-- Lemma: values don't reduce.
step-val : ∀ {m n} (v : Val m n) → step ⌜ v ⌝ ≡ just (done v)
step-val (Λ a)      = P.refl
step-val (λ' a t)   = P.refl
step-val (fold a v) with step ⌜ v ⌝ | step-val v
... | just (continue t) | ()
... | just (done w) | w≡v = P.cong (map (lower a)) w≡v
  where lower : ∀ {m n} → Type (1 + n) → Result m n → Result m n
        lower a (done v)     = done (fold a v)
        lower a (continue t) = continue t
... | nothing | ()

-- Lemma: _↓ "preserves" values.
↓-val : ∀ {m n} (v : Val m n) → ⌜ v ⌝ ↓ ≡ return v
↓-val v with step ⌜ v ⌝ | step-val v
↓-val v | just (continue t) | ()
↓-val v | just (done w) | w≡v = P.cong toComp w≡v
  where toComp : ∀ {m n} → Maybe (Result m n) → Comp m n
        toComp (just (continue t′)) = later (♯ (t′ ↓))
        toComp (just (done v))      = return v
        toComp nothing              = fail
↓-val v | nothing | ()

mutual
  infix 7 _[_]⇓≅↓′ _·⇓≅↓′_

  -- A helper lemma relating reduction and evaluation of type
  -- application.
  _[_]⇓≅↓′ : ∀ {m n} (t : Term m n) (a : Type n) →
             (t ↓) [ a ]⇓ ≅P (t [ a ]) ↓
  t [ a ]⇓≅↓′ with step t
  ... | just (continue t′)     = later (♯ (t′ [ a ]⇓≅↓′))
  ... | just (done (Λ t′))     = later (♯ ⇓≅↓′ (t′ [/tmTp a ]) )
  ... | just (done (λ' _ _))   = failP
  ... | just (done (fold _ _)) = failP
  ... | nothing                = failP

  -- A helper lemma relating reduction and evaluation of term
  -- application.
  _·⇓≅↓′_ : ∀ {m n} (s : Term m n) (t : Term m n) →
            (s ↓) ·⇓ (t ↓) ≅P (s · t) ↓
  s ·⇓≅↓′ t with step s
  s ·⇓≅↓′ t | just (continue s′)     = later (♯ (s′ ·⇓≅↓′ t))
  s ·⇓≅↓′ t | just (done v)          with step t
  s ·⇓≅↓′ t | just (done v)          | just (continue t′) = later (♯ subst v)
    where
      subst : ∀ v → (return v) ·⇓ (t′ ↓) ≅P (⌜ v ⌝ · t′) ↓
      subst v with ⌜ v ⌝ ↓ | ↓-val v | ⌜ v ⌝ ·⇓≅↓′ t′
      subst v | now (just .v) | P.refl | v≅t′ = v≅t′
      subst _ | now nothing   | ()     | _
      subst _ | later x₁      | ()     | _
  s ·⇓≅↓′ t | just (done (Λ s′))     | just (done w) = failP
  s ·⇓≅↓′ t | just (done (λ' a s′))  | just (done w) =
    later (♯ ⇓≅↓′ (s′ [/tmTm ⌜ w ⌝ ]))
  s ·⇓≅↓′ t | just (done (fold x v)) | just (done w) = failP
  s ·⇓≅↓′ t | just (done v)          | nothing       = failP
  s ·⇓≅↓′ t | nothing                                = failP

  -- A helper lemma relating reduction and evaluation of recursive
  -- type folding.
  fold⇓≅↓′ : ∀ {m n} (a : Type (1 + n)) (t : Term m n) →
             fold⇓ a (t ↓) ≅P (fold a t) ↓
  fold⇓≅↓′ a t with step t
  ... | just (continue t′) = later (♯ fold⇓≅↓′ a t′)
  ... | just (done v)      = returnP P.refl
  ... | nothing            = failP

  -- A helper lemma relating reduction and evaluation of recursive
  -- type unfolding.
  unfold⇓≅↓′ : ∀ {m n} (a : Type (1 + n)) (t : Term m n) →
               unfold⇓ a (t ↓) ≅P (unfold a t) ↓
  unfold⇓≅↓′ a t with step t
  ... | just (continue t′) = later (♯ unfold⇓≅↓′ a t′)
  ... | just (done (Λ _))      = failP
  ... | just (done (λ' _ _))   = failP
  ... | just (done (fold _ v)) = returnP P.refl
  ... | nothing                = failP

  -- Big-step evaluation and small-step reduction are strongly bisimliar.
  ⇓≅↓′ : ∀ {m n} (t : Term m n) → t ⇓ ≅P t ↓
  ⇓≅↓′ (var x)        = failP
  ⇓≅↓′ (Λ t)          = returnP P.refl
  ⇓≅↓′ (λ' a t)       = returnP P.refl
  ⇓≅↓′ (μ a t)        = later (♯ ⇓≅↓′ (t [/tmTm μ a t ]))
  ⇓≅↓′ (t [ a ])      =
    (t [ a ]) ⇓       ≅⟨ complete ([]-comp t a) ⟩
    (t ⇓) [ a ]⇓      ≅⟨ (⇓≅↓′ t) >>=P (λ v → (_ ∎)) ⟩
    (t ↓) [ a ]⇓      ≅⟨ t [ a ]⇓≅↓′ ⟩
    (t [ a ]) ↓       ∎
  ⇓≅↓′ (s · t)        =
    (s · t) ⇓         ≅⟨ complete (·-comp s t) ⟩
    (s ⇓) ·⇓ (t ⇓)    ≅⟨ (⇓≅↓′ s >>=P λ v → ⇓≅↓′ t >>=P λ w → (_ ∎)) ⟩
    (s ↓) ·⇓ (t ↓)    ≅⟨ s ·⇓≅↓′ t ⟩
    (s · t) ↓         ∎
  ⇓≅↓′ (fold a t)     =
    (fold a t) ⇓      ≅⟨ complete (fold-comp a t) ⟩
    fold⇓ a (t ⇓)     ≅⟨ (⇓≅↓′ t) >>=P (λ v → (_ ∎)) ⟩
    fold⇓ a (t ↓)     ≅⟨ fold⇓≅↓′ a t ⟩
    (fold a t) ↓      ∎
  ⇓≅↓′ (unfold a t)   =
    (unfold a t) ⇓    ≅⟨ complete (unfold-comp a t) ⟩
    unfold⇓ a (t ⇓)   ≅⟨ (⇓≅↓′ t) >>=P (λ v → (_ ∎)) ⟩
    unfold⇓ a (t ↓)   ≅⟨ unfold⇓≅↓′ a t ⟩
    (unfold a t) ↓    ∎

-- Big-step evaluation and small-step reduction are strongly bisimliar.
⇓≅↓ : ∀ {m n} (t : Term m n) → t ⇓ ≅ t ↓
⇓≅↓ t = sound (⇓≅↓′ t)

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


text:
open import Data.Nat      using (ℕ; suc; zero; _<_; _≤_; z≤n; s≤s; _+_; _⊔_)
open import Data.Bool     using (Bool; true; false; not; _∧_)
open import Data.Sum      using (inj₁; inj₂; _⊎_; [_,_])
open import Data.Product  using (_×_; _,_; -,_; _-,-_; ∃; ∃-syntax; proj₂)
open import Data.String   using (String; _≟_; length)
open import Relation.Nullary           using (¬_; yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; trans; cong₂)
open import Data.Nat.Properties hiding (_≤?_; _≟_)

open import IMP

level = ℕ

sec : vname → level
-- We can also temporarily use "sec x" to avoid the
-- automatic expansion of the definition in error messages
sec x = length x

secₐ : aexp → level
secₐ (N n) = 0
secₐ (V x) = sec x
secₐ (Plus a b) = secₐ a ⊔ secₐ b

sec₆ : bexp → level
sec₆ (Bc x) = 0
sec₆ (Not b) = sec₆ b
sec₆ (And b₁ b₂) = sec₆ b₁ ⊔ sec₆ b₂
sec₆ (Less a b) = secₐ a ⊔ secₐ b

_≡_⦅≤_⦆ : state → state → level → Set
s₁ ≡ s₂ ⦅≤ l ⦆ = ∀ x → sec x ≤ l → s₁ x ≡ s₂ x

_≡_⦅<_⦆ : state → state → level → Set
s₁ ≡ s₂ ⦅< l ⦆ = ∀ x → sec x < l → s₁ x ≡ s₂ x

non-interference-aexp : ∀ a {s₁ s₂ l}
  → s₁ ≡ s₂ ⦅≤ l ⦆
  → secₐ a ≤ l
  → aval a s₁ ≡ aval a s₂
non-interference-aexp (N x) r e = refl
non-interference-aexp (V x) r e = r x e
non-interference-aexp (Plus a b) r e =
  cong₂ (_+_) (non-interference-aexp a r (m⊔n≤o⇒m≤o _ _ e))
              (non-interference-aexp b r (m⊔n≤o⇒n≤o _ _ e))

non-interference-bexp : ∀ a {s₁ s₂ l}
  → s₁ ≡ s₂ ⦅≤ l ⦆
  → sec₆ a ≤ l
  → bval a s₁ ≡ bval a s₂
non-interference-bexp (Bc x) r e = refl
non-interference-bexp (Not a) r e = cong not (non-interference-bexp a r e)
non-interference-bexp (And a b) r e =
  cong₂ (_∧_) (non-interference-bexp a r (m⊔n≤o⇒m≤o _ _ e))
              (non-interference-bexp b r (m⊔n≤o⇒n≤o _ _ e))
non-interference-bexp (Less a b) r e =
  cong₂ (_≤?_) (non-interference-aexp a r (m⊔n≤o⇒m≤o _ _ e))
               (non-interference-aexp b r (m⊔n≤o⇒n≤o _ _ e))

data _⊢_ : level → com → Set where
  SecSkip : ∀{l}
     → l ⊢ SKIP
  SecLoc : ∀{l a x}
     → secₐ a ≤ sec x
     → l ≤ sec x
     → l ⊢ (x ::= a)
  SecSeq : ∀{l c₁ c₂}
     → l ⊢ c₁
     → l ⊢ c₂
     → l ⊢ (c₁ :: c₂)
  SecIf : ∀{b l c₁ c₂}
     → (l ⊔ sec₆ b) ⊢ c₁
     → (l ⊔ sec₆ b) ⊢ c₂
     → l ⊢ (IF b THEN c₁ ELSE c₂)
  SecWhile : ∀{b l c}
     → (l ⊔ sec₆ b) ⊢ c
     → l ⊢ (WHILE b DO c)

anti-monotonicity : ∀{l l′ c}
  → l ⊢ c
  → l′ ≤ l
  → l′ ⊢ c
anti-monotonicity SecSkip s = SecSkip
anti-monotonicity (SecLoc x x₁) s = SecLoc x (≤-trans s x₁)
anti-monotonicity (SecSeq d d₁) s = SecSeq (anti-monotonicity d s) (anti-monotonicity d₁ s)
anti-monotonicity (SecIf d d₁) s = SecIf (anti-monotonicity d (⊔-monoˡ-≤ _ s)) (anti-monotonicity d₁ (⊔-monoˡ-≤ _ s))
anti-monotonicity (SecWhile d) s = SecWhile ((anti-monotonicity d (⊔-monoˡ-≤ _ s)))

data ⦅_,_⦆⇒_ : com → state → state → Set where
  Skip : ∀{s} → ⦅ SKIP , s ⦆⇒ s
  Loc : ∀{s x a}
         → ⦅ x ::= a , s ⦆⇒ (s [ x ::= aval a s ])
  Seq : ∀{c₁ c₂ s₁ s₂ s₃}
         → ⦅ c₁ , s₁ ⦆⇒ s₂
         → ⦅ c₂ , s₂ ⦆⇒ s₃
         → ⦅ c₁ :: c₂ , s₁ ⦆⇒ s₃
  IfTrue : ∀{c₁ c₂ b s t}
         → bval b s ≡ true
         → ⦅ c₁ , s ⦆⇒ t
         → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆⇒ t
  IfFalse : ∀{c₁ c₂ b s t}
         → bval b s ≡ false
         → ⦅ c₂ , s ⦆⇒ t
         → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆⇒ t
  WhileFalse : ∀{c b s}
         → bval b s ≡ false
         → ⦅ WHILE b DO c , s ⦆⇒ s
  WhileTrue : ∀{c b s₁ s₂ s₃}
         → bval b s₁ ≡ true
         → ⦅ c , s₁ ⦆⇒ s₂
         → ⦅ WHILE b DO c , s₂ ⦆⇒ s₃
         → ⦅ WHILE b DO c , s₁ ⦆⇒ s₃

confinement : ∀{c s t l}
  → ⦅ c , s ⦆⇒ t
  → l ⊢ c
  → s ≡ t ⦅< l ⦆
confinement Skip SecSkip x₂ x₃ = refl
confinement (Loc {x = x₂}) (SecLoc x x₁) e r with e ≟ x₂
... | yes refl = contradiction x₁ (<⇒≱ r)
... | no  _ = refl
confinement (Seq x x₄) (SecSeq x₁ x₅) x₂ x₃ =
  trans (confinement x x₁ x₂ x₃)
        (confinement x₄ x₅ x₂ x₃)
confinement (IfTrue x x₄) (SecIf x₁ x₅) x₂ x₃ = confinement x₄ x₁ x₂ (m<n⇒m<n⊔o _ x₃)
confinement (IfFalse x x₄) (SecIf x₁ x₅) x₂ x₃ = confinement x₄ x₅ x₂ (m<n⇒m<n⊔o _ x₃)
confinement (WhileFalse x) (SecWhile x₁) x₂ x₃ = refl
confinement {l = l} (WhileTrue x x₄ x₅) (SecWhile x₁) x₂ x₃ =
   trans (confinement x₄ (anti-monotonicity x₁ (m≤m⊔n _ _)) x₂ x₃)
         (confinement x₅ (SecWhile x₁) x₂ x₃)

true≢false : ¬ (true ≡ false)
true≢false = λ ()

reversal₁ : ∀{b c s₁ s₃}
  → ⦅ WHILE b DO c , s₁ ⦆⇒ s₃
  → bval b s₁ ≡ true
  → ∃[ s₂ ] ( ⦅ c , s₁ ⦆⇒ s₂ × ⦅ WHILE b DO c , s₂ ⦆⇒ s₃)
reversal₁ (WhileFalse x) v = contradiction (trans (sym v) x) true≢false
reversal₁ (WhileTrue x e e₁) v = -, e , e₁

reversal₂ : ∀{b c s₁ s₃}
  → ⦅ WHILE b DO c , s₁ ⦆⇒ s₃
  → bval b s₁ ≡ false
  → s₁ ≡ s₃
reversal₂ (WhileFalse x) v = refl
reversal₂ (WhileTrue x r r₁) v = contradiction (trans (sym x) v) true≢false

level-cong : ∀{l l′ c} → l ≡ l′ → l ⊢ c → l′ ⊢ c
level-cong refl x = x

≤⇒<suc : ∀{a b} → a ≤ b → a < suc b
≤⇒<suc z≤n = s≤s z≤n
≤⇒<suc (s≤s r) = s≤s (≤⇒<suc r)

non-interference : ∀{c s s′ t t′ l}
  → ⦅ c , s ⦆⇒ s′
  → ⦅ c , t ⦆⇒ t′
  → 0 ⊢ c
  → s  ≡ t  ⦅≤ l ⦆
  → s′ ≡ t′ ⦅≤ l ⦆
non-interference Skip Skip z e = e
non-interference (Loc {x = x₂} {a}) Loc (SecLoc x₃ z≤n) e x x₁ with x ≟ x₂
... | yes refl = non-interference-aexp a e (≤-trans x₃ x₁)
... | no _ = e x x₁
non-interference (Seq x cs) (Seq y ct) (SecSeq z z₁) e =
  non-interference cs ct z₁ (non-interference x y z e)
non-interference {l = l} (IfTrue {b = b} x cs) (IfTrue x₁ red) (SecIf w w₁) e r r₁ =
  non-interference cs red (anti-monotonicity w z≤n) e r r₁
non-interference {l = l} (IfTrue {b = b} x cs) (IfFalse x₁ red) (SecIf w w₁) e r r₁ =
  [ (λ secb≤l →
        let wr = non-interference-bexp b e secb≤l
         in contradiction (trans (sym x) (trans wr x₁)) true≢false)
  , (λ l<secb → let oo₁ = confinement cs w
                    oo₂ = confinement red w₁
                 in trans (sym (oo₁ r (<-transʳ r₁ l<secb)))
                   (trans (e r r₁)
                          (oo₂ r (<-transʳ r₁ l<secb))))
  ]  (≤-<-connex (sec₆ b) l)
non-interference {l = l} (IfFalse x₁ red) (IfTrue {b = b} x cs) (SecIf w w₁) e r r₁ =
  [ (λ secb≤l →
        let wr = non-interference-bexp b e secb≤l
         in contradiction (trans (sym x) (trans (sym wr) x₁)) true≢false)
  , (λ l<secb → let oo₁ = confinement cs w
                    oo₂ = confinement red w₁
                 in trans (sym (oo₂ r (<-transʳ r₁ l<secb)))
                   (trans (e r r₁)
                          (oo₁ r (<-transʳ r₁ l<secb))))
  ]  (≤-<-connex (sec₆ b) l)
non-interference (IfFalse x₁ red) (IfFalse x cs) (SecIf x₇ x₈) =
  non-interference red cs (anti-monotonicity x₈ z≤n)
non-interference (WhileFalse x) (WhileFalse x₁) (SecWhile z) e = e
non-interference {l = l} (WhileFalse {b = b} r) (WhileTrue c ct ct₁) (SecWhile z) e x x₁ =
  [ (λ secb≤l →
        let wr = non-interference-bexp b e secb≤l
         in contradiction (trans (sym c) (trans (sym wr) r)) true≢false)
  , (λ l<secb →
        let simp = confinement ct z
            simp2 = confinement ct₁ (SecWhile (level-cong (sym (m≤n⇒m⊔n≡n l<secb)) z))
         in trans (e x x₁) (trans (simp x (<-transʳ x₁ l<secb)) (simp2 x (≤⇒<suc x₁))))
  ]  (≤-<-connex (sec₆ b) l)
non-interference {l = l} (WhileTrue c ct ct₁) (WhileFalse {b = b} r) (SecWhile z) e x x₁ =
  [ (λ secb≤l →
        let wr = non-interference-bexp b e secb≤l
         in contradiction (trans (sym c) (trans wr r)) true≢false)
  , (λ l<secb →
        let simp = confinement ct z
            simp2 = confinement ct₁ (SecWhile (level-cong (sym (m≤n⇒m⊔n≡n l<secb)) z))
         in trans (trans (sym (simp2 x (≤⇒<suc x₁))) (sym (simp x ((<-transʳ x₁ l<secb))))) (e x x₁))
  ]  (≤-<-connex (sec₆ b) l)
non-interference {l = l} (WhileTrue {b = b} r cs cs₁) (WhileTrue c ct ct₁) (SecWhile z) e =
  let h₁ = non-interference cs ct (anti-monotonicity z z≤n) e
      h₂ = non-interference cs₁ ct₁ (SecWhile z) h₁
   in h₂

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of functions, such as associativity and
-- commutativity (only those that don't require any sort of setoid)
------------------------------------------------------------------------

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

module Algebra.FunctionProperties.Consequences.Core
  {a} {A : Set a} where

open import Algebra.FunctionProperties
open import Data.Sum
open import Relation.Binary

sel⇒idem : ∀ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) →
           Selective _≈_ _•_ → Idempotent _≈_ _•_
sel⇒idem _ sel x with sel x x
... | inj₁ x•x≈x = x•x≈x
... | inj₂ x•x≈x = x•x≈x


text:
------------------------------------------------------------------------------
-- We could not define the FOTC colists using the Agda machinery for
-- co-inductive types.
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Colist.TypeSL where

open import Codata.Musical.Notation

open import FOTC.Base
open import FOTC.Base.List

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

data Colist : D → Set where
  nilCL  : Colist []
  consCL : ∀ x xs → ∞ (Colist xs) → Colist (x ∷ xs)

-- Example (finite colist).
l₁ : Colist (zero ∷ true ∷ [])
l₁ = consCL zero (true ∷ []) (♯ (consCL true [] (♯ nilCL)))

-- Example (infinite colist).
-- zerosCL : Colist {!!}
-- zerosCL = consCL zero {!!} (♯ zerosCL)


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Float.Properties where

open import Agda.Builtin.Float
open import Agda.Builtin.Equality

primitive

  primFloatToWord64Injective : ∀ a b → primFloatToWord64 a ≡ primFloatToWord64 b → a ≡ b

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Interval where

open import Cubical.HITs.Interval.Base public

-- open import Cubical.HITs.Interval.Properties public

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Tarski-style semantics with context pairs as concrete worlds, and glueing for α, ▻, and □.
-- Hilbert-style syntax.

module BasicIS4.Semantics.TarskiOvergluedDyadicHilbert where

open import BasicIS4.Syntax.Common public
open import Common.Semantics public

-- Intuitionistic Tarski models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_ _[⊢]_
  field
    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_    : Cx² Ty Ty → Atom → Set
    mono²⊩ᵅ : ∀ {P Π Π′} → Π ⊆² Π′ → Π ⊩ᵅ P → Π′ ⊩ᵅ P

    -- Hilbert-style syntax representation; monotonic.
    _[⊢]_    : Cx² Ty Ty → Ty → Set
    mono²[⊢] : ∀ {A Π Π′}    → Π ⊆² Π′ → Π [⊢] A → Π′ [⊢] A
    [var]     : ∀ {A Γ Δ}     → A ∈ Γ → Γ ⁏ Δ [⊢] A
    [app]     : ∀ {A B Γ Δ}   → Γ ⁏ Δ [⊢] A ▻ B → Γ ⁏ Δ [⊢] A → Γ ⁏ Δ [⊢] B
    [ci]      : ∀ {A Γ Δ}     → Γ ⁏ Δ [⊢] A ▻ A
    [ck]      : ∀ {A B Γ Δ}   → Γ ⁏ Δ [⊢] A ▻ B ▻ A
    [cs]      : ∀ {A B C Γ Δ} → Γ ⁏ Δ [⊢] (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
    [mvar]    : ∀ {A Γ Δ}     → A ∈ Δ → Γ ⁏ Δ [⊢] A
    [box]     : ∀ {A Γ Δ}     → ∅ ⁏ Δ [⊢] A → Γ ⁏ Δ [⊢] □ A
    [cdist]   : ∀ {A B Γ Δ}   → Γ ⁏ Δ [⊢] □ (A ▻ B) ▻ □ A ▻ □ B
    [cup]     : ∀ {A Γ Δ}     → Γ ⁏ Δ [⊢] □ A ▻ □ □ A
    [cdown]   : ∀ {A Γ Δ}     → Γ ⁏ Δ [⊢] □ A ▻ A
    [cpair]   : ∀ {A B Γ Δ}   → Γ ⁏ Δ [⊢] A ▻ B ▻ A ∧ B
    [cfst]    : ∀ {A B Γ Δ}   → Γ ⁏ Δ [⊢] A ∧ B ▻ A
    [csnd]    : ∀ {A B Γ Δ}   → Γ ⁏ Δ [⊢] A ∧ B ▻ B
    [unit]    : ∀ {Γ Δ}       → Γ ⁏ Δ [⊢] ⊤

    -- NOTE: [mlam] is necessary for [mmulticut], which is necessary for eval.
    [mlam] : ∀ {A B Γ Δ} → Γ ⁏ Δ , A [⊢] B → Γ ⁏ Δ [⊢] □ A ▻ B

  infix 3 _[⊢]⋆_
  _[⊢]⋆_ : Cx² Ty Ty → Cx Ty → Set
  Π [⊢]⋆ ∅     = 𝟙
  Π [⊢]⋆ Ξ , A = Π [⊢]⋆ Ξ × Π [⊢] A

open Model {{…}} public

-- Forcing in a particular model.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : Cx² Ty Ty → Ty → Set
  Π ⊩ α P   = Glue (Π [⊢] α P) (Π ⊩ᵅ P)
  Π ⊩ A ▻ B = ∀ {Π′} → Π ⊆² Π′ → Glue (Π′ [⊢] A ▻ B) (Π′ ⊩ A → Π′ ⊩ B)
  Π ⊩ □ A   = ∀ {Π′} → Π ⊆² Π′ → Glue (Π′ [⊢] □ A) (Π′ ⊩ A)
  Π ⊩ A ∧ B = Π ⊩ A × Π ⊩ B
  Π ⊩ ⊤    = 𝟙

  infix 3 _⊩⋆_
  _⊩⋆_ : Cx² Ty Ty → Cx Ty → Set
  Π ⊩⋆ ∅     = 𝟙
  Π ⊩⋆ Ξ , A = Π ⊩⋆ Ξ × Π ⊩ A

-- Monotonicity with respect to context inclusion.

module _ {{_ : Model}} where
  mono²⊩ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊩ A → Π′ ⊩ A
  mono²⊩ {α P}   ψ s = mono²[⊢] ψ (syn s) ⅋ mono²⊩ᵅ ψ (sem s)
  mono²⊩ {A ▻ B} ψ s = λ ψ′ → s (trans⊆² ψ ψ′)
  mono²⊩ {□ A}   ψ s = λ ψ′ → s (trans⊆² ψ ψ′)
  mono²⊩ {A ∧ B} ψ s = mono²⊩ {A} ψ (π₁ s) , mono²⊩ {B} ψ (π₂ s)
  mono²⊩ {⊤}    ψ s = ∙

  mono²⊩⋆ : ∀ {Ξ Π Π′} → Π ⊆² Π′ → Π ⊩⋆ Ξ → Π′ ⊩⋆ Ξ
  mono²⊩⋆ {∅}     ψ ∙        = ∙
  mono²⊩⋆ {Ξ , A} ψ (ts , t) = mono²⊩⋆ ψ ts , mono²⊩ {A} ψ t

-- Extraction of syntax representation in a particular model.

module _ {{_ : Model}} where
  reifyʳ : ∀ {A Π} → Π ⊩ A → Π [⊢] A
  reifyʳ {α P}   s = syn s
  reifyʳ {A ▻ B} s = syn (s refl⊆²)
  reifyʳ {□ A}   s = syn (s refl⊆²)
  reifyʳ {A ∧ B} s = [app] ([app] [cpair] (reifyʳ {A} (π₁ s))) (reifyʳ {B} (π₂ s))
  reifyʳ {⊤}    s = [unit]

  reifyʳ⋆ : ∀ {Ξ Π} → Π ⊩⋆ Ξ → Π [⊢]⋆ Ξ
  reifyʳ⋆ {∅}     ∙        = ∙
  reifyʳ⋆ {Ξ , A} (ts , t) = reifyʳ⋆ ts , reifyʳ t

-- Useful theorems in functional form.

module _ {{_ : Model}} where
  [mmulticut] : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ [⊢]⋆ □⋆ Ξ → Γ ⁏ Ξ [⊢] A → Γ ⁏ Δ [⊢] A
  [mmulticut] {∅}     ∙        u = mono²[⊢] (refl⊆ , bot⊆) u
  [mmulticut] {Ξ , B} (ts , t) u = [app] ([mmulticut] ts ([mlam] u)) t

-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ : ∀ {A B Π} → Π ⊩ A ▻ B → Π ⊩ A → Π ⊩ B
  s ⟪$⟫ a = sem (s refl⊆²) a

  ⟪K⟫ : ∀ {A B Π} → Π ⊩ A → Π ⊩ B ▻ A
  ⟪K⟫ {A} a ψ = let a′ = mono²⊩ {A} ψ a
                in  [app] [ck] (reifyʳ a′) ⅋ K a′

  ⟪S⟫ : ∀ {A B C Π} → Π ⊩ A ▻ B ▻ C → Π ⊩ A ▻ B → Π ⊩ A → Π ⊩ C
  ⟪S⟫ s₁ s₂ a = (s₁ ⟪$⟫ a) ⟪$⟫ (s₂ ⟪$⟫ a)

  ⟪S⟫′ : ∀ {A B C Π} → Π ⊩ A ▻ B ▻ C → Π ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ ψ = let s₁′ = mono²⊩ {A ▻ B ▻ C} ψ s₁
                              t   = syn (s₁′ refl⊆²)
                          in  [app] [cs] t ⅋ λ s₂ ψ′ →
                              let s₁″ = mono²⊩ {A ▻ B ▻ C} (trans⊆² ψ ψ′) s₁
                                  s₂′ = mono²⊩ {A ▻ B} ψ′ s₂
                                  t′  = syn (s₁″ refl⊆²)
                                  u   = syn (s₂′ refl⊆²)
                              in  [app] ([app] [cs] t′) u ⅋ ⟪S⟫ s₁″ s₂′

  _⟪D⟫_ : ∀ {A B Π} → Π ⊩ □ (A ▻ B) → Π ⊩ □ A → Π ⊩ □ B
  (s₁ ⟪D⟫ s₂) ψ = let t ⅋ s₁′ = s₁ ψ
                      u ⅋ a   = s₂ ψ
                  in  [app] ([app] [cdist] t) u ⅋ s₁′ ⟪$⟫ a

  _⟪D⟫′_ : ∀ {A B Π} → Π ⊩ □ (A ▻ B) → Π ⊩ □ A ▻ □ B
  _⟪D⟫′_ {A} {B} s₁ ψ = let s₁′ = mono²⊩ {□ (A ▻ B)} ψ s₁
                        in  [app] [cdist] (reifyʳ (λ {_} ψ′ → s₁′ ψ′)) ⅋ _⟪D⟫_ s₁′

  ⟪↑⟫ : ∀ {A Π} → Π ⊩ □ A → Π ⊩ □ □ A
  ⟪↑⟫ {A} s ψ = [app] [cup] (syn (s ψ)) ⅋ λ ψ′ → s (trans⊆² ψ ψ′)

  ⟪↓⟫ : ∀ {A Π} → Π ⊩ □ A → Π ⊩ A
  ⟪↓⟫ s = sem (s refl⊆²)

  _⟪,⟫′_ : ∀ {A B Π} → Π ⊩ A → Π ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} a ψ = let a′ = mono²⊩ {A} ψ a
                   in  [app] [cpair] (reifyʳ a′) ⅋ _,_ a′

-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : Cx² Ty Ty → Cx² Ty Ty → Ty → Set
  Π ⊩ Γ ⁏ Δ ⇒ A = Π ⊩⋆ Γ → Π ⊩⋆ □⋆ Δ → Π ⊩ A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : Cx² Ty Ty → Cx² Ty Ty → Cx Ty → Set
  Π ⊩ Γ ⁏ Δ ⇒⋆ Ξ = Π ⊩⋆ Γ → Π ⊩⋆ □⋆ Δ → Π ⊩⋆ Ξ

-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx² Ty Ty → Ty → Set₁
Π ⊨ A = ∀ {{_ : Model}} {w : Cx² Ty Ty} → w ⊩ Π ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx² Ty Ty → Cx Ty → Set₁
Π ⊨⋆ Ξ = ∀ {{_ : Model}} {w : Cx² Ty Ty} → w ⊩ Π ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩⋆ Γ → w ⊩ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

  mlookup : ∀ {A Δ w} → A ∈ Δ → w ⊩⋆ □⋆ Δ → w ⊩ A
  mlookup top     (γ , s) = sem (s refl⊆²)
  mlookup (pop i) (γ , s) = mlookup i γ

  -- TODO: More equipment.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen