text:
------------------------------------------------------------------------------
-- Properties of the inequalities
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Inequalities.Properties where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.EliminationProperties
open import LTC-PCF.Data.Nat.Inequalities.ConversionRules public
open import LTC-PCF.Data.Nat.Properties
open import LTC-PCF.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- N.B. The elimination properties are in the module
-- LTC.Data.Nat.Inequalities.EliminationProperties.

------------------------------------------------------------------------------
-- Congruence properties

ltLeftCong : ∀ {m n o} → m ≡ n → lt m o ≡ lt n o
ltLeftCong refl = refl

ltRightCong : ∀ {m n o} → n ≡ o → lt m n ≡ lt m o
ltRightCong refl = refl

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

0≯x : ∀ {n} → N n → zero ≯ n
0≯x nzero          = lt-00
0≯x (nsucc {n} Nn) = lt-S0 n

x≮x : ∀ {n} → N n → n ≮ n
x≮x nzero          = lt-00
x≮x (nsucc {n} Nn) = trans (lt-SS n n) (x≮x Nn)

Sx≰0 : ∀ {n} → N n → succ₁ n ≰ zero
Sx≰0 nzero          = x≮x (nsucc nzero)
Sx≰0 (nsucc {n} Nn) = trans (lt-SS (succ₁ n) zero) (lt-S0 n)

x<Sx : ∀ {n} → N n → n < succ₁ n
x<Sx nzero          = lt-0S zero
x<Sx (nsucc {n} Nn) = trans (lt-SS n (succ₁ n)) (x<Sx Nn)

x<y→Sx<Sy : ∀ {m n} → m < n → succ₁ m < succ₁ n
x<y→Sx<Sy {m} {n} m<n = trans (lt-SS m n) m<n

Sx<Sy→x<y : ∀ {m n} → succ₁ m < succ₁ n → m < n
Sx<Sy→x<y {m} {n} Sm<Sn = trans (sym (lt-SS m n)) Sm<Sn

x≤x : ∀ {n} → N n → n ≤ n
x≤x nzero          = lt-0S zero
x≤x (nsucc {n} Nn) = trans (lt-SS n (succ₁ n)) (x≤x Nn)

x≤y→Sx≤Sy : ∀ {m n} → m ≤ n → succ₁ m ≤ succ₁ n
x≤y→Sx≤Sy {m} {n} m≤n = trans (lt-SS m (succ₁ n)) m≤n

Sx≤Sy→x≤y : ∀ {m n} → succ₁ m ≤ succ₁ n → m ≤ n
Sx≤Sy→x≤y {m} {n} Sm≤Sn = trans (sym (lt-SS m (succ₁ n))) Sm≤Sn

x≥y→x≮y : ∀ {m n} → N m → N n → m ≥ n → m ≮ n
x≥y→x≮y nzero          nzero          _     = x≮x nzero
x≥y→x≮y nzero          (nsucc Nn)     0≥Sn  = ⊥-elim (0≥S→⊥ Nn 0≥Sn)
x≥y→x≮y (nsucc {m} Nm) nzero          _     = lt-S0 m
x≥y→x≮y (nsucc {m} Nm) (nsucc {n} Nn) Sm≥Sn =
  trans (lt-SS m n) (x≥y→x≮y Nm Nn (trans (sym (lt-SS n (succ₁ m))) Sm≥Sn))

x≮y→x≥y : ∀ {m n} → N m → N n → m ≮ n → m ≥ n
x≮y→x≥y nzero nzero 0≮0 = x≤x nzero
x≮y→x≥y nzero (nsucc {n} Nn) 0≮Sn = ⊥-elim (t≢f (trans (sym (lt-0S n)) 0≮Sn))
x≮y→x≥y (nsucc {m} Nm) nzero Sm≮n = lt-0S (succ₁ m)
x≮y→x≥y (nsucc {m} Nm) (nsucc {n} Nn) Sm≮Sn =
  trans (lt-SS n (succ₁ m)) (x≮y→x≥y Nm Nn (trans (sym (lt-SS m n)) Sm≮Sn))

x>y∨x≤y : ∀ {m n} → N m → N n → m > n ∨ m ≤ n
x>y∨x≤y {n = n} nzero Nn = inj₂ (lt-0S n)
x>y∨x≤y (nsucc {m} Nm) nzero = inj₁ (lt-0S m)
x>y∨x≤y (nsucc {m} Nm) (nsucc {n} Nn) =
  case (λ m>n → inj₁ (trans (lt-SS n m) m>n))
       (λ m≤n → inj₂ (trans (lt-SS m (succ₁ n)) m≤n))
       (x>y∨x≤y Nm Nn)

x≤y→x≯y : ∀ {m n} → N m → N n → m ≤ n → m ≯ n
x≤y→x≯y nzero          Nn             _    = 0≯x Nn
x≤y→x≯y (nsucc Nm)     nzero          Sm≤0 = ⊥-elim (S≤0→⊥ Nm Sm≤0)
x≤y→x≯y (nsucc {m} Nm) (nsucc {n} Nn) Sm≤Sn =
  trans (lt-SS n m) (x≤y→x≯y Nm Nn (trans (sym (lt-SS m (succ₁ n))) Sm≤Sn))

x≯y→x≤y : ∀ {m n} → N m → N n → m ≯ n → m ≤ n
x≯y→x≤y {n = n} nzero Nn _ = lt-0S n
x≯y→x≤y (nsucc {m} Nm) nzero Sm≯0 = ⊥-elim (t≢f (trans (sym (lt-0S m)) Sm≯0))
x≯y→x≤y (nsucc {m} Nm) (nsucc {n} Nn) Sm≯Sn =
  trans (lt-SS m (succ₁ n)) (x≯y→x≤y Nm Nn (trans (sym (lt-SS n m)) Sm≯Sn))

x>y∨x≯y : ∀ {m n} → N m → N n → m > n ∨ m ≯ n
x>y∨x≯y nzero          Nn             = inj₂ (0≯x Nn)
x>y∨x≯y (nsucc {m} Nm) nzero          = inj₁ (lt-0S m)
x>y∨x≯y (nsucc {m} Nm) (nsucc {n} Nn) =
  case (λ h → inj₁ (trans (lt-SS n m) h))
       (λ h → inj₂ (trans (lt-SS n m) h))
       (x>y∨x≯y Nm Nn)

x<y∨x≥y : ∀ {m n} → N m → N n → m < n ∨ m ≥ n
x<y∨x≥y Nm Nn = x>y∨x≤y Nn Nm

x<y∨x≮y : ∀ {m n} → N m → N n → m < n ∨ m ≮ n
x<y∨x≮y Nm Nn = case (λ m<n → inj₁ m<n)
                     (λ m≥n → inj₂ (x≥y→x≮y Nm Nn m≥n))
                     (x<y∨x≥y Nm Nn)

x≡y→x≤y : ∀ {m n} → N m → N n → m ≡ n → m ≤ n
x≡y→x≤y Nm _ refl = x≤x Nm

x<y→x≤y : ∀ {m n} → N m → N n → m < n → m ≤ n
x<y→x≤y Nm             nzero          m<0   = ⊥-elim (x<0→⊥ Nm m<0)
x<y→x≤y nzero          (nsucc {n} Nn) _     = lt-0S (succ₁ n)
x<y→x≤y (nsucc {m} Nm) (nsucc {n} Nn) Sm<Sn =
  x≤y→Sx≤Sy (x<y→x≤y Nm Nn (Sx<Sy→x<y Sm<Sn))

x<Sy→x≤y : ∀ {m n} → N m → N n → m < succ₁ n → m ≤ n
x<Sy→x≤y {n = n} nzero      Nn 0<Sn  = lt-0S n
x<Sy→x≤y         (nsucc Nm) Nn Sm<Sn = Sm<Sn

x≤Sx : ∀ {m} → N m → m ≤ succ₁ m
x≤Sx Nm = x<y→x≤y Nm (nsucc Nm) (x<Sx Nm)

x<y→Sx≤y : ∀ {m n} → N m → N n → m < n → succ₁ m ≤ n
x<y→Sx≤y Nm             nzero          m<0   = ⊥-elim (x<0→⊥ Nm m<0)
x<y→Sx≤y nzero          (nsucc {n} Nn) _     = x≤y→Sx≤Sy (lt-0S n)
x<y→Sx≤y (nsucc {m} Nm) (nsucc {n} Nn) Sm<Sn =
  trans (lt-SS (succ₁ m) (succ₁ n)) Sm<Sn

Sx≤y→x<y : ∀ {m n} → N m → N n → succ₁ m ≤ n → m < n
Sx≤y→x<y Nm             nzero          Sm≤0   = ⊥-elim (S≤0→⊥ Nm Sm≤0)
Sx≤y→x<y nzero          (nsucc {n} Nn) _      = lt-0S n
Sx≤y→x<y (nsucc {m} Nm) (nsucc {n} Nn) SSm≤Sn =
  x<y→Sx<Sy (Sx≤y→x<y Nm Nn (Sx≤Sy→x≤y SSm≤Sn))

<-trans : ∀ {m n o} → N m → N n → N o → m < n → n < o → m < o
<-trans nzero          nzero           _             0<0   _    = ⊥-elim (0<0→⊥ 0<0)
<-trans nzero          (nsucc Nn)     nzero          _     Sn<0 = ⊥-elim (S<0→⊥ Sn<0)
<-trans nzero          (nsucc Nn)     (nsucc {o} No) _     _    = lt-0S o
<-trans (nsucc Nm)     Nn             nzero          _     n<0  = ⊥-elim (x<0→⊥ Nn n<0)
<-trans (nsucc Nm)     nzero          (nsucc No)     Sm<0  _    = ⊥-elim (S<0→⊥ Sm<0)
<-trans (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) Sm<Sn Sn<So =
  x<y→Sx<Sy (<-trans Nm Nn No (Sx<Sy→x<y Sm<Sn) (Sx<Sy→x<y Sn<So))

≤-trans : ∀ {m n o} → N m → N n → N o → m ≤ n → n ≤ o → m ≤ o
≤-trans {o = o} nzero Nn No _ _ = lt-0S o
≤-trans (nsucc Nm) nzero No Sm≤0 _ = ⊥-elim (S≤0→⊥ Nm Sm≤0)
≤-trans (nsucc Nm) (nsucc Nn) nzero _ Sn≤0 = ⊥-elim (S≤0→⊥ Nn Sn≤0)
≤-trans (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) Sm≤Sn Sn≤So =
  x≤y→Sx≤Sy (≤-trans Nm Nn No (Sx≤Sy→x≤y Sm≤Sn) (Sx≤Sy→x≤y Sn≤So))

x≤x+y : ∀ {m n} → N m → N n → m ≤ m + n
x≤x+y {n = n} nzero Nn = lt-0S (zero + n)
x≤x+y {n = n} (nsucc {m} Nm) Nn =
  lt (succ₁ m) (succ₁ (succ₁ m + n)) ≡⟨ lt-SS m (succ₁ m + n) ⟩
  lt m (succ₁ m + n)                 ≡⟨ ltRightCong (+-Sx m n) ⟩
  lt m (succ₁ (m + n))               ≡⟨ refl ⟩
  le m (m + n)                       ≡⟨ x≤x+y Nm Nn ⟩
  true                               ∎

x∸y<Sx : ∀ {m n} → N m → N n → m ∸ n < succ₁ m
x∸y<Sx {m} Nm nzero =
  lt (m ∸ zero) (succ₁ m) ≡⟨ ltLeftCong (∸-x0 m) ⟩
  lt m (succ₁ m)          ≡⟨ x<Sx Nm ⟩
  true                    ∎

x∸y<Sx nzero (nsucc {n} Nn) =
  lt (zero ∸ succ₁ n) [1] ≡⟨ ltLeftCong (0∸x (nsucc Nn)) ⟩
  lt zero [1]             ≡⟨ lt-0S zero ⟩
  true                    ∎

x∸y<Sx (nsucc {m} Nm) (nsucc {n} Nn) =
  lt (succ₁ m ∸ succ₁ n) (succ₁ (succ₁ m))
    ≡⟨ ltLeftCong (S∸S Nm Nn) ⟩
  lt (m ∸ n) (succ₁ (succ₁ m))
     ≡⟨ <-trans (∸-N Nm Nn) (nsucc Nm) (nsucc (nsucc Nm))
                (x∸y<Sx Nm Nn) (x<Sx (nsucc Nm))
     ⟩
  true ∎

Sx∸Sy<Sx : ∀ {m n} → N m → N n → succ₁ m ∸ succ₁ n < succ₁ m
Sx∸Sy<Sx {m} {n} Nm Nn =
  lt (succ₁ m ∸ succ₁ n) (succ₁ m) ≡⟨ ltLeftCong (S∸S Nm Nn) ⟩
  lt (m ∸ n) (succ₁ m)             ≡⟨ x∸y<Sx Nm Nn ⟩
  true                             ∎

x>y→x∸y+y≡x : ∀ {m n} → N m → N n → m > n → (m ∸ n) + n ≡ m
x>y→x∸y+y≡x nzero Nn 0>n = ⊥-elim (0>x→⊥ Nn 0>n)
x>y→x∸y+y≡x (nsucc {m} Nm) nzero Sm>0 =
  trans (+-rightIdentity (∸-N (nsucc Nm) nzero)) (∸-x0 (succ₁ m))
x>y→x∸y+y≡x (nsucc {m} Nm) (nsucc {n} Nn) Sm>Sn =
  (succ₁ m ∸ succ₁ n) + succ₁ n
    ≡⟨ +-leftCong (S∸S Nm Nn)  ⟩
  (m ∸ n) + succ₁ n
     ≡⟨ +-comm (∸-N Nm Nn) (nsucc Nn) ⟩
  succ₁ n + (m ∸ n)
    ≡⟨ +-Sx n (m ∸ n) ⟩
  succ₁ (n + (m ∸ n))
    ≡⟨ succCong (+-comm Nn (∸-N Nm Nn)) ⟩
  succ₁ ((m ∸ n) + n)
    ≡⟨ succCong (x>y→x∸y+y≡x Nm Nn (trans (sym (lt-SS n m)) Sm>Sn)) ⟩
  succ₁ m ∎

x≤y→y∸x+x≡y : ∀ {m n} → N m → N n → m ≤ n → (n ∸ m) + m ≡ n
x≤y→y∸x+x≡y {n = n} nzero Nn 0≤n =
  trans (+-rightIdentity (∸-N Nn nzero)) (∸-x0 n)
x≤y→y∸x+x≡y (nsucc Nm) nzero Sm≤0 = ⊥-elim (S≤0→⊥ Nm Sm≤0)
x≤y→y∸x+x≡y (nsucc {m} Nm) (nsucc {n} Nn) Sm≤Sn =
  (succ₁ n ∸ succ₁ m) + succ₁ m
    ≡⟨ +-leftCong (S∸S Nn Nm) ⟩
  (n ∸ m) + succ₁ m
     ≡⟨ +-comm (∸-N Nn Nm) (nsucc Nm) ⟩
  succ₁ m + (n ∸ m)
    ≡⟨ +-Sx m (n ∸ m) ⟩
  succ₁ (m + (n ∸ m))
    ≡⟨ succCong (+-comm Nm (∸-N Nn Nm)) ⟩
  succ₁ ((n ∸ m) + m)
    ≡⟨ succCong  (x≤y→y∸x+x≡y Nm Nn (trans (sym (lt-SS m (succ₁ n))) Sm≤Sn)) ⟩
  succ₁ n ∎

x<y→x<Sy : ∀ {m n} → N m → N n → m < n → m < succ₁ n
x<y→x<Sy Nm             nzero          m<0   = ⊥-elim (x<0→⊥ Nm m<0)
x<y→x<Sy nzero          (nsucc {n} Nn) 0<Sn  = lt-0S (succ₁ n)
x<y→x<Sy (nsucc {m} Nm) (nsucc {n} Nn) Sm<Sn =
  x<y→Sx<Sy (x<y→x<Sy Nm Nn (Sx<Sy→x<y Sm<Sn))

x<Sy→x<y∨x≡y : ∀ {m n} → N m → N n → m < succ₁ n → m < n ∨ m ≡ n
x<Sy→x<y∨x≡y nzero nzero 0<S0 = inj₂ refl
x<Sy→x<y∨x≡y nzero (nsucc {n} Nn) 0<SSn = inj₁ (lt-0S n)
x<Sy→x<y∨x≡y (nsucc {m} Nm) nzero Sm<S0 =
  ⊥-elim (x<0→⊥ Nm (trans (sym (lt-SS m zero)) Sm<S0))
x<Sy→x<y∨x≡y (nsucc {m} Nm) (nsucc {n} Nn) Sm<SSn =
  case (λ m<n → inj₁ (trans (lt-SS m n) m<n))
       (λ m≡n → inj₂ (succCong m≡n))
       m<n∨m≡n
  where
  m<n∨m≡n : m < n ∨ m ≡ n
  m<n∨m≡n = x<Sy→x<y∨x≡y Nm Nn (trans (sym (lt-SS m (succ₁ n))) Sm<SSn)

x≤y→x<y∨x≡y : ∀ {m n} → N m → N n → m ≤ n → m < n ∨ m ≡ n
x≤y→x<y∨x≡y = x<Sy→x<y∨x≡y

x<y→y≡z→x<z : ∀ {m n o} → m < n → n ≡ o → m < o
x<y→y≡z→x<z m<n refl = m<n

x≡y→y<z→x<z : ∀ {m n o} → m ≡ n → n < o → m < o
x≡y→y<z→x<z refl n<o = n<o

x≥y→y>0→x∸y<x : ∀ {m n} → N m → N n → m ≥ n → n > zero → m ∸ n < m
x≥y→y>0→x∸y<x Nm             nzero          _     0>0  = ⊥-elim (x>x→⊥ nzero 0>0)
x≥y→y>0→x∸y<x nzero          (nsucc Nn)     0≥Sn  _    = ⊥-elim (S≤0→⊥ Nn 0≥Sn)
x≥y→y>0→x∸y<x (nsucc {m} Nm) (nsucc {n} Nn) Sm≥Sn Sn>0 =
  lt (succ₁ m ∸ succ₁ n) (succ₁ m)
    ≡⟨ ltLeftCong (S∸S Nm Nn) ⟩
  lt (m ∸ n) (succ₁ m)
     ≡⟨ x∸y<Sx Nm Nn ⟩
  true ∎

------------------------------------------------------------------------------
-- Properties about LT₂

xy<00→⊥ : ∀ {m n} → N m → N n → ¬ (Lexi m n zero zero)
xy<00→⊥ Nm Nn mn<00 = case (λ m<0 → ⊥-elim (x<0→⊥ Nm m<0))
                           (λ m≡0∧n<0 → ⊥-elim (x<0→⊥ Nn (∧-proj₂ m≡0∧n<0)))
                           mn<00

0Sx<00→⊥ : ∀ {m} → ¬ (Lexi zero (succ₁ m) zero zero)
0Sx<00→⊥ 0Sm<00 = case 0<0→⊥
                       (λ 0≡0∧Sm<0 → S<0→⊥ (∧-proj₂ 0≡0∧Sm<0))
                       0Sm<00

Sxy<0y'→⊥ : ∀ {m n n'} → ¬ (Lexi (succ₁ m) n zero n')
Sxy<0y'→⊥ Smn<0n' =
  case S<0→⊥
       (λ Sm≡0∧n<n' → ⊥-elim (0≢S (sym (∧-proj₁ Sm≡0∧n<n'))))
       Smn<0n'

xy<x'0→x<x' : ∀ {m n} → N n → ∀ {m'} → Lexi m n m' zero → m < m'
xy<x'0→x<x' Nn mn<m'0 =
  case (λ m<n → m<n)
       (λ m≡n∧n<0 → ⊥-elim (x<0→⊥ Nn (∧-proj₂ m≡n∧n<0)))
       mn<m'0

xy<0y'→x≡0∧y<y' : ∀ {m} → N m → ∀ {n n'} → Lexi m n zero n' →
                  m ≡ zero ∧ n < n'
xy<0y'→x≡0∧y<y' Nm mn<0n' = case (λ m<0 → ⊥-elim (x<0→⊥ Nm m<0))
                                 (λ m≡0∧n<n' → m≡0∧n<n')
                                 mn<0n'

[Sx∸Sy,Sy]<[Sx,Sy] : ∀ {m n} → N m → N n →
                     Lexi (succ₁ m ∸ succ₁ n) (succ₁ n) (succ₁ m) (succ₁ n)
[Sx∸Sy,Sy]<[Sx,Sy] Nm Nn = inj₁ (Sx∸Sy<Sx Nm Nn)

[Sx,Sy∸Sx]<[Sx,Sy] : ∀ {m n} → N m → N n →
                     Lexi (succ₁ m) (succ₁ n ∸ succ₁ m) (succ₁ m) (succ₁ n)
[Sx,Sy∸Sx]<[Sx,Sy] Nm Nn = inj₂ (refl , Sx∸Sy<Sx Nn Nm)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import MLib.Prelude.FromStdlib
open import Relation.Binary using (Rel; _Respects₂_; IsStrictTotalOrder)
open FE using (Π)

module MLib.Prelude.DFS.ViaInjection
  {v v′ e}
  (V-setoid : Setoid v v′)
  (E : Rel (Setoid.Carrier V-setoid) e)
  (E-subst : E Respects₂ (Setoid._≈_ V-setoid))
  {i p} {I : Set i}
  {_<_ : I → I → Set p} (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  (injection : LeftInverse V-setoid (≡.setoid I))
  where

open import MLib.Prelude.Path
import MLib.Prelude.DFS as DFS
import Data.AVL isStrictTotalOrder as Tree
open Bool using (T)

module V = Setoid V-setoid
open V using (_≈_) renaming (Carrier to V)

open Π (LeftInverse.to injection) hiding (cong) renaming (_⟨$⟩_ to toIx)
open Π (LeftInverse.from injection) hiding (cong) renaming (_⟨$⟩_ to fromIx)
open LeftInverse using (left-inverse-of)

_⇒_ : I → I → Set e
i ⇒ j = E (fromIx i) (fromIx j)

module BaseDFS = DFS _⇒_ isStrictTotalOrder
open BaseDFS public using (Graph)
open Tree using (Tree)

convertPath : ∀ {i j} → Path _⇒_ i j → Path E (fromIx i) (fromIx j)
convertPath (edge e) = edge e
convertPath (connect p₁ p₂) = connect (convertPath p₁) (convertPath p₂)

PathE-subst : ∀ {x x′ y y′} → x ≈ x′ → y ≈ y′ → Path E x y → Path E x′ y′
PathE-subst x≈x′ y≈y′ (edge e) = edge (proj₂ E-subst x≈x′ (proj₁ E-subst y≈y′ e))
PathE-subst x≈x′ y≈y′ (connect p₁ p₂) = connect (PathE-subst x≈x′ V.refl p₁) (PathE-subst V.refl y≈y′ p₂)

mkGraph : List (∃₂ E) → Graph
mkGraph = List.foldr step Tree.empty
  where
  step : ∃₂ E → Graph → Graph
  step (x , y , e) =
    let e′ = proj₂ E-subst (V.sym (left-inverse-of injection x)) (proj₁ E-subst (V.sym (left-inverse-of injection y)) e)
    in Tree.insertWith (toIx x) ((toIx y , e′) ∷ []) List._++_

allTargetsFrom : Graph → (source : V) → List (∃ (Path E source))
allTargetsFrom graph source =
  let resI = BaseDFS.allTargetsFrom graph (toIx source)
  in List.map (uncurry (λ _ p → _ , PathE-subst (left-inverse-of injection _) V.refl (convertPath p))) resI

findDest : Graph → ∀ {dest} (isDest : ∀ i → Dec (i ≡ toIx dest)) (source : V) → Maybe (Path E source dest)
findDest graph {dest} isDest source =
  let resI = BaseDFS.findDest graph isDest (toIx source)
  in Maybe.map (PathE-subst (left-inverse-of injection _) (left-inverse-of injection _) ∘ convertPath) resI

findMatching : Graph → (matches : V → Bool) (source : V) → Maybe (∃ λ dest → Path E source dest × T (matches dest))
findMatching graph matches source =
  let resI = BaseDFS.findMatching graph (matches ∘ fromIx) (toIx source)
  in Maybe.map (λ {(_ , p , q) → _ , PathE-subst (left-inverse-of injection _) V.refl (convertPath p) , q}) resI

ext: agda


text:
open import FRP.JS.Behaviour using ( Beh ; map )
open import FRP.JS.DOM using ( DOM ; text ; element )
open import FRP.JS.RSet using ( ⟦_⟧ )
open import FRP.JS.Time using ( toUTCString ; every )
open import FRP.JS.Delay using ( _sec )

module FRP.JS.Demo.Clock where

main : ∀ {w} → ⟦ Beh (DOM w) ⟧
main = text (map toUTCString (every (1 sec)))

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
open import Type

module Graph.Walk {ℓ₁ ℓ₂} {V : Type{ℓ₁}} where

import      Lvl
open import Graph{ℓ₁}{ℓ₂}(V)
import      Structure.Relator.Names as Names

module _ (_⟶_ : Graph) where
  -- A path is matching directed edges connected to each other in a finite sequence.
  -- This is essentially a list of edges where the ends match.
  -- The terminology is that a walk is a sequence of connected edges and it visits all its vertices.
  -- Note: Walk is a generalized "List" for categories instead of the usual List which is for monoids.
  -- Note: Walk is equivalent to the reflexive-transitive closure.
  data Walk : V → V → Type{ℓ₁ Lvl.⊔ ℓ₂} where
    at      : Names.Reflexivity(Walk)
    prepend : ∀{a b c} → (a ⟶ b) → (Walk b c) → (Walk a c)

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:
open import Prelude

module Implicits.Substitutions where

import Implicits.Substitutions.Context as CtxSubst
open import Implicits.Substitutions.Term

module TypeSubst where
  open import Implicits.Substitutions.Type public

open import Implicits.Substitutions.MetaType public

open TypeSubst public using (_∙_; stp-weaken)
  renaming (_simple/_ to _stp/tp_; _/_ to _tp/tp_; _[/_] to _tp[/tp_]; weaken to tp-weaken)
open TermTypeSubst public using ()
  renaming (_/_ to _tm/tp_; _[/_] to _tm[/tp_]; weaken to tm-weaken)
open TermTermSubst public using ()
  renaming (_/_ to _tm/tm_; _/Var_ to _tm/Var_; _[/_] to _tm[/tm_]; weaken to tmtm-weaken)
open CtxSubst public using (ktx-map; ictx-weaken; ctx-weaken)
  renaming (_/_ to _ktx/_; _/Var_ to _ktx/Var_; weaken to ktx-weaken)


text:
module v01-02-induction where

import Relation.Binary.PropositionalEquality as Eq
open Eq             using (_≡_; refl; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
open import v01-01-basics

plus-n-O : ∀ (n : nat) → n ≡ n + 0
plus-n-O    O  = refl
plus-n-O (S n) rewrite sym (plus-n-O n) = refl

minus-n-n : ∀ (n : nat) → minus n n ≡ 0
minus-n-n    O  = refl
minus-n-n (S n) rewrite sym (minus-n-n n) = refl

mult-0-r : ∀ (n : nat) → n * 0 ≡ 0
mult-0-r    O  = refl
mult-0-r (S n) rewrite mult-0-r n = refl

plus-n-Sm : ∀ (n m : nat) → S (n + m) ≡ n + (S m)
plus-n-Sm    O  m = refl
plus-n-Sm (S n) m rewrite sym (plus-n-Sm n m) = refl

plus-comm : ∀ (n m : nat) → n + m ≡ m + n
plus-comm    n     O  rewrite sym (plus-n-O n) = refl
plus-comm    O  (S m) rewrite sym (plus-n-O m) = refl
plus-comm (S n) (S m)
  rewrite
    sym (plus-n-Sm n m)
  | sym (plus-n-Sm m n)
  | plus-comm n m
  = refl

plus-assoc : ∀ (n m p : nat) → n + (m + p) ≡ (n + m) + p
plus-assoc    O  m p = refl
plus-assoc (S n) m p        --         S n + (m + p) ≡ S n + m + p
  rewrite
    plus-comm (S n + m) p        -- S (plus n (plus m p)) ≡ plus p (S (plus n m))
  | sym (plus-n-Sm p (plus n m)) -- S (plus n (plus m p)) ≡ S (plus p (plus n m))
  | plus-comm p (plus n m)       -- S (plus n (plus m p)) ≡ S (plus (plus n m) p)
  | plus-assoc n m p             -- S (plus (plus n m) p) ≡ S (plus (plus n m) p)
  = refl

double : (n : nat) → nat
double    O  = O
double (S n) = S (S (double n))

double-plus : ∀ (n : nat) → double n ≡ n + n
double-plus    O  = refl
double-plus (S n)          --     double (S n) ≡ S n + S n
                           -- S (S (double n)) ≡ S n + S n
  rewrite
    double-plus n          -- S (S (plus n n)) ≡ S (plus n (S n))
  | plus-n-Sm n n          -- S (plus n (S n)) ≡ S (plus n (S n))
  = refl

{-
Inconvenient in evenb def: recursive call on n - 2.
Makes inductibe proofs about evenb harder since may need IH about n - 2.
Following lemma gives alternative characterization of evenb (S n) that works better with induction.
-}

evenb-S : ∀ (n : nat) → evenb (S n) ≡ negb (evenb n)
evenb-S    O  = refl
evenb-S (S n)                 -- evenb (S (S n)) ≡ negb (evenb (S n))
                              --         evenb n ≡ negb (evenb (S n))
  rewrite
    evenb-S n                 --         evenb n ≡ negb (negb (evenb n))
  | negb-involutive (evenb n) --         evenb n ≡ evenb n
  = refl

mult-0-plus' : ∀ (n m : nat) → (0 + n) * m ≡ n * m
mult-0-plus'    O  m = refl
mult-0-plus' (S n) m       --     (0 + S n) * m ≡ S n * m
  rewrite plus-O-n {n}     -- plus m (mult n m) ≡ plus m (mult n m)
  = refl

plus-rearrange : ∀ (n m p q : nat)
  → (n + m) + (p + q) ≡ (m + n) + (p + q)
plus-rearrange n m p q
  rewrite plus-comm n m
  = refl

plus-swap : ∀ (n m p : nat)
  → n + (m + p) ≡ m + (n + p)
plus-swap n m p
  rewrite
    plus-assoc n m p
  | plus-comm  n m
  | plus-assoc m n p
  = refl

mult-comm : ∀ (m n : nat)
  → m * n ≡ n * m
mult-comm    O  n
  rewrite
    mult-O-l {n}
  | *0 n
  = refl
mult-comm (S m) n       --           S m * n ≡ n * S m
  rewrite               -- plus n (mult m n) ≡ plus (mult n m) n
    sym (mult-n-Sm n m)
  | plus-comm n (mult m n)
  | mult-comm m n
  = refl

leb-refl : ∀ (n : nat) → true ≡ (n <=? n)
leb-refl    O  = refl
leb-refl (S n) = leb-refl n

zero-nbeq-S : ∀ (n : nat) → (0 =? (S n)) ≡ false
zero-nbeq-S n = refl

andb-false-r : ∀ (b : bool) → andb b false ≡ false
andb-false-r true  = refl
andb-false-r false = refl

plus-ble-compat-l : ∀ (n m p : nat)
  → (n <=? m) ≡ true
  → ((p + n) <=? (p + m)) ≡ true
plus-ble-compat-l _ _    O  n<=?m = n<=?m
plus-ble-compat-l n m (S p) n<=?m = plus-ble-compat-l n m p n<=?m

S-nbeq-0 : ∀ (n : nat) → ((S n) =? 0) ≡ false
S-nbeq-0 n = refl

mult-1-l : ∀ (n : nat) → 1 * n ≡ n
mult-1-l    O  = refl
mult-1-l (S n) rewrite mult-1-l n = refl

all3-spec : ∀ (b c : bool)
  → orb
      (andb b c)
      (orb (negb b)
               (negb c))
  ≡ true
all3-spec  true  true = refl
all3-spec  true false = refl
all3-spec false  true = refl
all3-spec false false = refl

mult-plus-distr-r : ∀ (n m p : nat)
  → (n + m) * p ≡ (n * p) + (m * p)
mult-plus-distr-r    O  m p = refl
mult-plus-distr-r (S n) m p      --   (S n     + m) * p
                                 -- ≡  S n * p + m  * p
  rewrite
    mult-comm (S n + m) p        --   mult p (S (plus n m))
                                 -- ≡ plus (plus p (mult n p)) (mult m p)
  | sym (mult-n-Sm p (plus n m)) --   plus (mult p (plus n m)) p
                                 -- ≡ plus (plus p (mult n p)) (mult m p)
  | mult-comm p (plus n m)       --   plus (mult (plus n m) p) p
                                 -- ≡ plus (plus p (mult n p)) (mult m p)
  | mult-plus-distr-r n m p      --   plus (plus (mult n p) (mult m p)) p
                                 -- ≡ plus (plus p (mult n p)) (mult m p)
  | plus-comm (plus (mult n p) (mult m p)) p
                                 --   plus p (plus (mult n p) (mult m p))
                                 -- ≡ plus (plus p (mult n p)) (mult m p)
  | plus-assoc p (mult n p) (mult m p)
                                 --   plus (plus p (mult n p)) (mult m p)
                                 -- ≡ plus (plus p (mult n p)) (mult m p)
  = refl

mult-assoc : ∀ (n m p : nat)
  → n * (m * p) ≡ (n * m) * p
mult-assoc    O  m p = refl
mult-assoc (S n) m p                 -- S n * (m * p) ≡ S n * m * p
  rewrite
    mult-plus-distr-r m (mult n m) p -- plus (mult m p) (mult n (mult m p)) ≡
                                     -- plus (mult m p) (mult (mult n m) p)
  | mult-assoc n m p                 -- plus (mult m p) (mult (mult n m) p) ≡
                                     -- plus (mult m p) (mult (mult n m) p)
  = refl

eqb-refl : ∀ (n : nat) → true ≡ (n =? n)
eqb-refl    O  = refl
eqb-refl (S n) = eqb-refl n

plus-swap' : ∀ (n m p : nat)
  → n + (m + p) ≡ m + (n + p)
plus-swap' n m p           -- n + (m + p) ≡ m + (n + p)
  rewrite
    plus-assoc n m p       -- plus (plus n m) p ≡ plus m (plus n p)
  | plus-comm n m          -- plus (plus m n) p ≡ plus m (plus n p)
  | sym (plus-assoc m n p) -- plus m (plus n p) ≡ plus m (plus n p)
  = refl

{-

Exercise: 3 stars, standard, especially useful (binary_commute)
Prove this diagram commutes:

                            incr
              bin ----------------------> bin
               |                           |
    bin_to_nat |                           |  bin_to_nat
               |                           |
               v                           v
              nat ----------------------> nat
                             S

incrementing a binary number and then converting it to a (unary) natural number
yields the same result as
first converting it to a natural number and then incrementing
-}

bin-to-nat' : bin → nat
bin-to-nat'     Z  = 0
bin-to-nat' (B₀ x) =      double (bin-to-nat' x)
bin-to-nat' (B₁ x) = 1 + (double (bin-to-nat' x))

_ : bin-to-nat'         (B₀ (B₁ Z))  ≡ 2
_ = refl
_ : bin-to-nat'       (incr (B₁ Z))  ≡ 1 + bin-to-nat' (B₁ Z)
_ = refl
_ : bin-to-nat' (incr (incr (B₁ Z))) ≡ 2 + bin-to-nat' (B₁ Z)
_ = refl

--         PREServes
bin-to-nat-pres-incr : (b : bin) (n : nat)
  → bin-to-nat'       b  ≡   n
  → bin-to-nat' (incr b) ≡ S n
bin-to-nat-pres-incr     Z  n b≡n --           bin-to-nat (incr Z) ≡ S n
                                  --                             1 ≡ S n ; b≡n : 0 ≡ n
  rewrite sym b≡n                 --                             1 ≡ 1
  = refl
bin-to-nat-pres-incr (B₀ b) n b≡n --     bin-to-nat' (incr (B₀ b)) ≡ S n
                                  --    1 + double (bin-to-nat' b) ≡ S n
  rewrite b≡n                     --                           S n ≡ S n
  = refl
bin-to-nat-pres-incr (B₁ b) n b≡n --     bin-to-nat' (incr (B₁ b)) ≡ S n
                                  -- double (bin-to-nat' (incr b)) ≡ S n
                                  -- b≡n : 1 + double (bin-to-nat' b) ≡ n
  rewrite
    sym b≡n                       -- double (bin-to-nat' (incr b)) ≡ S (S (double (bin-to-nat' b)))
--  | bin-to-nat-pres-incr b n b≡n
  = {!!}

nat-to-bin : (n : nat) → bin
nat-to-bin n = {!!}

{-

Prove for any nat, convert it to binary; convert it back, get same nat
HINT If def of nat_to_bin uses other functions,
might need to prove lemma showing how functions relate to nat_to_bin.)

Theorem nat_bin_nat : ∀ n, bin_to_nat (nat_to_bin n) = n.
Proof.
  (* FILL IN HERE *) Admitted.

(b) One might naturally expect that we should also prove the opposite direction -- that starting with a binary number, converting to a natural, and then back to binary should yield the same number we started with. However, this is not the case! Explain (in a comment) what the problem is.

(* FILL IN HERE *)

(c) Define a normalization function -- i.e., a function normalize going directly from bin to bin (i.e., not by converting to nat and back) such that, for any binary number b, converting b to a natural and then back to binary yields (normalize b). Prove it. (Warning: This part is a bit tricky -- you may end up defining several auxiliary lemmas. One good way to find out what you need is to start by trying to prove the main statement, see where you get stuck, and see if you can find a lemma -- perhaps requiring its own inductive proof -- that will allow the main proof to make progress.) Don't define this using nat_to_bin and bin_to_nat!

(* FILL IN HERE *)
-}

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

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

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


text:
{-# OPTIONS --exact-split #-}

open import Agda.Builtin.Nat

data IsZero : Nat → Set where
  isZero : IsZero 0

test : (n m : Nat) → IsZero n → IsZero m → Nat
test zero zero _ _ = zero
test (suc _) _ () _
test _ (suc _) _ ()

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bag and set equality
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.BagAndSetEquality where

open import Algebra using (CommutativeSemiring; CommutativeMonoid)
open import Algebra.FunctionProperties using (Idempotent)
open import Category.Monad using (RawMonad)
open import Data.Empty
open import Data.Fin
open import Data.List
open import Data.List.Categorical using (monad; module MonadProperties)
import Data.List.Properties as LP
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Binary.Subset.Propositional.Properties
  using (⊆-preorder)
open import Data.Product as Prod hiding (map)
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Sum as Sum hiding (map)
open import Data.Sum.Properties
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Data.Unit
open import Function
open import Function.Equality using (_⟨$⟩_)
import Function.Equivalence as FE
open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
open import Function.Related as Related
  using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→; K-refl; SK-sym)
open import Function.Related.TypeIsomorphisms
open import Level using (Lift)
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as EqR
import Relation.Binary.Reasoning.Preorder as PreorderReasoning
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; _≗_; refl)
open import Relation.Nullary
open import Data.List.Membership.Propositional.Properties

------------------------------------------------------------------------
-- Definitions

open Related public using (Kind; Symmetric-kind) renaming
  ( implication         to subset
  ; reverse-implication to superset
  ; equivalence         to set
  ; injection           to subbag
  ; reverse-injection   to superbag
  ; bijection           to bag
  )

[_]-Order : Kind → ∀ {a} → Set a → Preorder _ _ _
[ k ]-Order A = Related.InducedPreorder₂ k {A = A} _∈_

[_]-Equality : Symmetric-kind → ∀ {a} → Set a → Setoid _ _
[ k ]-Equality A = Related.InducedEquivalence₂ k {A = A} _∈_

infix 4 _∼[_]_

_∼[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _
_∼[_]_ {A = A} xs k ys = Preorder._∼_ ([ k ]-Order A) xs ys

private
  module Eq  {k a} {A : Set a} = Setoid ([ k ]-Equality A)
  module Ord {k a} {A : Set a} = Preorder ([ k ]-Order A)
  open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
  module MP = MonadProperties

------------------------------------------------------------------------
-- Bag equality implies the other relations.

bag-=⇒ : ∀ {k a} {A : Set a} {xs ys : List A} →
         xs ∼[ bag ] ys → xs ∼[ k ] ys
bag-=⇒ xs≈ys = ↔⇒ xs≈ys

------------------------------------------------------------------------
-- "Equational" reasoning for _⊆_ along with an additional relatedness

module ⊆-Reasoning where
  private
    module PreOrder {a} {A : Set a} = PreorderReasoning (⊆-preorder A)

    open PreOrder public
      hiding (_≈⟨_⟩_; _≈˘⟨_⟩_) renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)

  infixr 2 _∼⟨_⟩_
  infix  1 _∈⟨_⟩_

  _∈⟨_⟩_ : ∀ {a} {A : Set a} x {xs ys : List A} →
           x ∈ xs → xs IsRelatedTo ys → x ∈ ys
  x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

  _∼⟨_⟩_ : ∀ {k a} {A : Set a} xs {ys zs : List A} →
           xs ∼[ ⌊ k ⌋→ ] ys → ys IsRelatedTo zs → xs IsRelatedTo zs
  xs ∼⟨ xs≈ys ⟩ ys≈zs = xs ⊆⟨ ⇒→ xs≈ys ⟩ ys≈zs

------------------------------------------------------------------------
-- Congruence lemmas
------------------------------------------------------------------------
-- _∷_

module _ {a k} {A : Set a} {x y : A} {xs ys} where

  ∷-cong : x ≡ y → xs ∼[ k ] ys → x ∷ xs ∼[ k ] y ∷ ys
  ∷-cong refl xs≈ys {y} =
    y ∈ x ∷ xs        ↔⟨ SK-sym $ ∷↔ (y ≡_) ⟩
    (y ≡ x ⊎ y ∈ xs)  ∼⟨ (y ≡ x ∎) ⊎-cong xs≈ys ⟩
    (y ≡ x ⊎ y ∈ ys)  ↔⟨ ∷↔ (y ≡_) ⟩
    y ∈ x ∷ ys        ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- map

module _ {ℓ k} {A B : Set ℓ} {f g : A → B} {xs ys} where

  map-cong : f ≗ g → xs ∼[ k ] ys → map f xs ∼[ k ] map g ys
  map-cong f≗g xs≈ys {x} =
    x ∈ map f xs            ↔⟨ SK-sym $ map↔ ⟩
    Any (λ y → x ≡ f y) xs  ∼⟨ Any-cong (↔⇒ ∘ helper) xs≈ys ⟩
    Any (λ y → x ≡ g y) ys  ↔⟨ map↔ ⟩
    x ∈ map g ys            ∎
    where
    open Related.EquationalReasoning

    helper : ∀ y → x ≡ f y ↔ x ≡ g y
    helper y = record
      { to         = P.→-to-⟶ (λ x≡fy → P.trans x≡fy (        f≗g y))
      ; from       = P.→-to-⟶ (λ x≡gy → P.trans x≡gy (P.sym $ f≗g y))
      ; inverse-of = record
        { left-inverse-of  = λ { P.refl → P.trans-symʳ (f≗g y) }
        ; right-inverse-of = λ { P.refl → P.trans-symˡ (f≗g y) }
        }
      }

------------------------------------------------------------------------
-- _++_

module _ {a k} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} where

  ++-cong : xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
            xs₁ ++ ys₁ ∼[ k ] xs₂ ++ ys₂
  ++-cong xs₁≈xs₂ ys₁≈ys₂ {x} =
    x ∈ xs₁ ++ ys₁       ↔⟨ SK-sym $ ++↔ ⟩
    (x ∈ xs₁ ⊎ x ∈ ys₁)  ∼⟨ xs₁≈xs₂ ⊎-cong ys₁≈ys₂ ⟩
    (x ∈ xs₂ ⊎ x ∈ ys₂)  ↔⟨ ++↔ ⟩
    x ∈ xs₂ ++ ys₂       ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- concat

module _ {a k} {A : Set a} {xss yss : List (List A)} where

  concat-cong : xss ∼[ k ] yss → concat xss ∼[ k ] concat yss
  concat-cong xss≈yss {x} =
    x ∈ concat xss        ↔⟨ SK-sym concat↔ ⟩
    Any (Any (x ≡_)) xss  ∼⟨ Any-cong (λ _ → _ ∎) xss≈yss ⟩
    Any (Any (x ≡_)) yss  ↔⟨ concat↔ ⟩
    x ∈ concat yss         ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- _>>=_

module _ {ℓ k} {A B : Set ℓ} {xs ys} {f g : A → List B} where

  >>=-cong : xs ∼[ k ] ys → (∀ x → f x ∼[ k ] g x) →
             (xs >>= f) ∼[ k ] (ys >>= g)
  >>=-cong xs≈ys f≈g {x} =
    x ∈ (xs >>= f)          ↔⟨ SK-sym >>=↔ ⟩
    Any (λ y → x ∈ f y) xs  ∼⟨ Any-cong (λ x → f≈g x) xs≈ys ⟩
    Any (λ y → x ∈ g y) ys  ↔⟨ >>=↔ ⟩
    x ∈ (ys >>= g)          ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- _⊛_

module _ {ℓ k} {A B : Set ℓ} {fs gs : List (A → B)} {xs ys} where

  ⊛-cong : fs ∼[ k ] gs → xs ∼[ k ] ys → (fs ⊛ xs) ∼[ k ] (gs ⊛ ys)
  ⊛-cong fs≈gs xs≈ys =
    >>=-cong fs≈gs λ f →
    >>=-cong xs≈ys λ x →
    _ ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- _⊗_

module _ {ℓ k} {A B : Set ℓ} {xs₁ xs₂ : List A} {ys₁ ys₂ : List B} where

  ⊗-cong : xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
           (xs₁ ⊗ ys₁) ∼[ k ] (xs₂ ⊗ ys₂)
  ⊗-cong xs₁≈xs₂ ys₁≈ys₂ =
    ⊛-cong (⊛-cong (Ord.refl {x = [ _,_ ]}) xs₁≈xs₂) ys₁≈ys₂

------------------------------------------------------------------------
-- Other properties

-- _++_ and [] form a commutative monoid, with either bag or set
-- equality as the underlying equality.

commutativeMonoid : ∀ {a} → Symmetric-kind → Set a →
                    CommutativeMonoid _ _
commutativeMonoid {a} k A = record
  { Carrier             = List A
  ; _≈_                 = _∼[ ⌊ k ⌋ ]_
  ; _∙_                 = _++_
  ; ε                   = []
  ; isCommutativeMonoid = record
    { isSemigroup = record
      { isMagma = record
        { isEquivalence = Eq.isEquivalence
        ; ∙-cong        = ++-cong
        }
      ; assoc         = λ xs ys zs →
                          Eq.reflexive (LP.++-assoc xs ys zs)
      }
    ; identityˡ = λ xs {x} → x ∈ xs ∎
    ; comm      = λ xs ys {x} →
                    x ∈ xs ++ ys  ↔⟨ ++↔++ xs ys ⟩
                    x ∈ ys ++ xs  ∎
    }
  }
  where open Related.EquationalReasoning

-- The only list which is bag or set equal to the empty list (or a
-- subset or subbag of the list) is the empty list itself.

empty-unique : ∀ {k a} {A : Set a} {xs : List A} →
               xs ∼[ ⌊ k ⌋→ ] [] → xs ≡ []
empty-unique {xs = []}    _    = refl
empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here refl)
... | ()

-- _++_ is idempotent (under set equality).

++-idempotent : ∀ {a} {A : Set a} → Idempotent {A = List A} _∼[ set ]_ _++_
++-idempotent {a} xs {x} =
  x ∈ xs ++ xs  ∼⟨ FE.equivalence ([ id , id ]′ ∘ _⟨$⟩_ (Inverse.from $ ++↔))
                                  (_⟨$⟩_ (Inverse.to $ ++↔) ∘ inj₁) ⟩
  x ∈ xs        ∎
  where open Related.EquationalReasoning

-- The list monad's bind distributes from the left over _++_.

>>=-left-distributive :
  ∀ {ℓ} {A B : Set ℓ} (xs : List A) {f g : A → List B} →
  (xs >>= λ x → f x ++ g x) ∼[ bag ] (xs >>= f) ++ (xs >>= g)
>>=-left-distributive {ℓ} xs {f} {g} {y} =
  y ∈ (xs >>= λ x → f x ++ g x)                      ↔⟨ SK-sym $ >>=↔ ⟩
  Any (λ x → y ∈ f x ++ g x) xs                      ↔⟨ SK-sym (Any-cong (λ _ → ++↔) (_ ∎)) ⟩
  Any (λ x → y ∈ f x ⊎ y ∈ g x) xs                   ↔⟨ SK-sym $ ⊎↔ ⟩
  (Any (λ x → y ∈ f x) xs ⊎ Any (λ x → y ∈ g x) xs)  ↔⟨ >>=↔ ⟨ _⊎-cong_ ⟩ >>=↔ ⟩
  (y ∈ (xs >>= f) ⊎ y ∈ (xs >>= g))                  ↔⟨ ++↔ ⟩
  y ∈ (xs >>= f) ++ (xs >>= g)                       ∎
  where open Related.EquationalReasoning

-- The same applies to _⊛_.

⊛-left-distributive :
  ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) xs₁ xs₂ →
  (fs ⊛ (xs₁ ++ xs₂)) ∼[ bag ] (fs ⊛ xs₁) ++ (fs ⊛ xs₂)
⊛-left-distributive {B = B} fs xs₁ xs₂ = begin
  fs ⊛ (xs₁ ++ xs₂)                         ≡⟨⟩
  (fs >>= λ f → xs₁ ++ xs₂ >>= return ∘ f)  ≡⟨ (MP.cong (refl {x = fs}) λ f →
                                                MP.right-distributive xs₁ xs₂ (return ∘ f)) ⟩
  (fs >>= λ f → (xs₁ >>= return ∘ f) ++
                (xs₂ >>= return ∘ f))       ≈⟨ >>=-left-distributive fs ⟩

  (fs >>= λ f → xs₁ >>= return ∘ f) ++
  (fs >>= λ f → xs₂ >>= return ∘ f)         ≡⟨⟩

  (fs ⊛ xs₁) ++ (fs ⊛ xs₂)                  ∎
  where open EqR ([ bag ]-Equality B)

private

  -- If x ∷ xs is set equal to x ∷ ys, then xs and ys are not
  -- necessarily set equal.

  ¬-drop-cons : ∀ {a} {A : Set a} {x : A} →
    ¬ (∀ {xs ys} → x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys)
  ¬-drop-cons {x = x} drop-cons
    with FE.Equivalence.to x∼[] ⟨$⟩ here refl
    where
    x,x≈x :  (x ∷ x ∷ []) ∼[ set ] [ x ]
    x,x≈x = ++-idempotent [ x ]

    x∼[] : [ x ] ∼[ set ] []
    x∼[] = drop-cons x,x≈x
  ... | ()

-- However, the corresponding property does hold for bag equality.

drop-cons : ∀ {a} {A : Set a} {x : A} {xs ys} →
            x ∷ xs ∼[ bag ] x ∷ ys → xs ∼[ bag ] ys
drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys =
  ⊎-left-cancellative
    (∼→⊎↔⊎ x∷xs≈x∷ys)
    (lemma x∷xs≈x∷ys)
    (lemma (SK-sym x∷xs≈x∷ys))

  where

  -- TODO: Some of the code below could perhaps be exposed to users.

  -- Finds the element at the given position.

  index : ∀ {a} {A : Set a} (xs : List A) → Fin (length xs) → A
  index []       ()
  index (x ∷ xs) zero    = x
  index (x ∷ xs) (suc i) = index xs i

  -- List membership can be expressed as "there is an index which
  -- points to the element".

  ∈-index : ∀ {a} {A : Set a} {z}
            (xs : List A) → z ∈ xs ↔ ∃ λ i → z ≡ index xs i
  ∈-index {z = z} [] =
    z ∈ []                              ↔⟨ SK-sym ⊥↔Any[] ⟩
    ⊥                                   ↔⟨ SK-sym $ inverse (λ { (() , _) }) (λ ()) (λ { (() , _) }) (λ ()) ⟩
    (∃ λ (i : Fin 0) → z ≡ index [] i)  ∎
    where
    open Related.EquationalReasoning
  ∈-index {z = z} (x ∷ xs) =
    z ∈ x ∷ xs                        ↔⟨ SK-sym (∷↔ _) ⟩
    (z ≡ x ⊎ z ∈ xs)                  ↔⟨ K-refl ⊎-cong ∈-index xs ⟩
    (z ≡ x ⊎ ∃ λ i → z ≡ index xs i)  ↔⟨ SK-sym $ inverse (λ { (zero , p) → inj₁ p; (suc i , p) → inj₂ (i , p) })
                                                          (λ { (inj₁ p) → zero , p; (inj₂ (i , p)) → suc i , p })
                                                          (λ { (zero , _) → refl; (suc _ , _) → refl })
                                                          (λ { (inj₁ _) → refl; (inj₂ _) → refl }) ⟩
    (∃ λ i → z ≡ index (x ∷ xs) i)    ∎
    where
    open Related.EquationalReasoning

  -- The index which points to the element.

  index-of : ∀ {a} {A : Set a} {z} {xs : List A} →
             z ∈ xs → Fin (length xs)
  index-of = proj₁ ∘ (Inverse.to (∈-index _) ⟨$⟩_)

  -- The type ∃ λ z → z ∈ xs is isomorphic to Fin n, where n is the
  -- length of xs.
  --
  -- Thierry Coquand pointed out that (a variant of) this statement is
  -- a generalisation of the fact that singletons are contractible.

  Fin-length : ∀ {a} {A : Set a}
               (xs : List A) → (∃ λ z → z ∈ xs) ↔ Fin (length xs)
  Fin-length xs =
    (∃ λ z → z ∈ xs)                  ↔⟨ Σ.cong K-refl (∈-index xs) ⟩
    (∃ λ z → ∃ λ i → z ≡ index xs i)  ↔⟨ ∃∃↔∃∃ _ ⟩
    (∃ λ i → ∃ λ z → z ≡ index xs i)  ↔⟨ Σ.cong K-refl (inverse _ (λ _ → _ , refl) (λ { (_ , refl) → refl }) (λ _ → refl)) ⟩
    (Fin (length xs) × Lift _ ⊤)      ↔⟨ ×-identityʳ _ _ ⟩
    Fin (length xs)                   ∎
    where
    open Related.EquationalReasoning

  -- From this lemma we get that lists which are bag equivalent have
  -- related lengths.

  Fin-length-cong : ∀ {a} {A : Set a} {xs ys : List A} →
                    xs ∼[ bag ] ys → Fin (length xs) ↔ Fin (length ys)
  Fin-length-cong {xs = xs} {ys} xs≈ys =
    Fin (length xs)   ↔⟨ SK-sym $ Fin-length xs ⟩
    ∃ (λ z → z ∈ xs)  ↔⟨ Σ.cong K-refl xs≈ys ⟩
    ∃ (λ z → z ∈ ys)  ↔⟨ Fin-length ys ⟩
    Fin (length ys)   ∎
    where
    open Related.EquationalReasoning

  -- The index-of function commutes with applications of certain
  -- inverses.

  index-of-commutes :
    ∀ {a} {A : Set a} {z : A} {xs ys} →
    (xs≈ys : xs ∼[ bag ] ys) (p : z ∈ xs) →
    index-of (Inverse.to xs≈ys ⟨$⟩ p) ≡
    Inverse.to (Fin-length-cong xs≈ys) ⟨$⟩ index-of p
  index-of-commutes {z = z} {xs} {ys} xs≈ys p =
    index-of (to xs≈ys ⟨$⟩ p)                                        ≡⟨ lemma z p ⟩

    index-of (to xs≈ys ⟨$⟩ proj₂
      (from (Fin-length xs) ⟨$⟩ (to (Fin-length xs) ⟨$⟩ (z , p))))   ≡⟨⟩

    index-of (proj₂ (Prod.map id (to xs≈ys ⟨$⟩_)
      (from (Fin-length xs) ⟨$⟩ (to (Fin-length xs) ⟨$⟩ (z , p)))))  ≡⟨⟩

    to (Fin-length ys) ⟨$⟩ Prod.map id (to xs≈ys ⟨$⟩_)
      (from (Fin-length xs) ⟨$⟩ index-of p)                          ≡⟨⟩

    to (Fin-length-cong xs≈ys) ⟨$⟩ index-of p                        ∎
    where
    open P.≡-Reasoning
    open Inverse

    lemma :
      ∀ z p →
      index-of (to xs≈ys ⟨$⟩ p) ≡
      index-of (to xs≈ys ⟨$⟩ proj₂
        (from (Fin-length xs) ⟨$⟩ (to (Fin-length xs) ⟨$⟩ (z , p))))
    lemma z p with to (Fin-length xs) ⟨$⟩ (z , p)
                 | left-inverse-of (Fin-length xs) (z , p)
    lemma .(index xs i) .(from (∈-index xs) ⟨$⟩ (i , refl)) | i | refl =
      refl

  -- Bag equivalence isomorphisms preserve index equality. Note that
  -- this means that, even if the underlying equality is proof
  -- relevant, a bag equivalence isomorphism cannot map two distinct
  -- proofs, that point to the same position, to different positions.

  index-equality-preserved :
    ∀ {a} {A : Set a} {z : A} {xs ys} {p q : z ∈ xs}
    (xs≈ys : xs ∼[ bag ] ys) →
    index-of p ≡ index-of q →
    index-of (Inverse.to xs≈ys ⟨$⟩ p) ≡
    index-of (Inverse.to xs≈ys ⟨$⟩ q)
  index-equality-preserved {p = p} {q} xs≈ys eq =
    index-of (Inverse.to xs≈ys ⟨$⟩ p)                  ≡⟨ index-of-commutes xs≈ys p ⟩
    Inverse.to (Fin-length-cong xs≈ys) ⟨$⟩ index-of p  ≡⟨ P.cong (Inverse.to (Fin-length-cong xs≈ys) ⟨$⟩_) eq ⟩
    Inverse.to (Fin-length-cong xs≈ys) ⟨$⟩ index-of q  ≡⟨ P.sym $ index-of-commutes xs≈ys q ⟩
    index-of (Inverse.to xs≈ys ⟨$⟩ q)                  ∎
    where
    open P.≡-Reasoning

  -- The old inspect idiom.

  inspect : ∀ {a} {A : Set a} (x : A) → ∃ (x ≡_)
  inspect x = x , refl

  -- A function is "well-behaved" if any "left" element which is the
  -- image of a "right" element is in turn not mapped to another
  -- "left" element.

  Well-behaved : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
                 (A ⊎ B → A ⊎ C) → Set _
  Well-behaved f =
    ∀ {b a a′} → f (inj₂ b) ≡ inj₁ a → f (inj₁ a) ≢ inj₁ a′

  -- The type constructor _⊎_ is left cancellative for certain
  -- well-behaved inverses.

  ⊎-left-cancellative :
    ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
    (f : (A ⊎ B) ↔ (A ⊎ C)) →
    Well-behaved (Inverse.to   f ⟨$⟩_) →
    Well-behaved (Inverse.from f ⟨$⟩_) →
    B ↔ C
  ⊎-left-cancellative {A = A} = λ inv to-hyp from-hyp → inverse
    (g (to   inv ⟨$⟩_) to-hyp)
    (g (from inv ⟨$⟩_) from-hyp)
    (g∘g         inv  to-hyp from-hyp)
    (g∘g (SK-sym inv) from-hyp to-hyp)
    where
    open Inverse

    module _
      {a b c} {A : Set a} {B : Set b} {C : Set c}
      (f : A ⊎ B → A ⊎ C)
      (hyp : Well-behaved f)
      where

      mutual

        g : B → C
        g b = g′ (inspect (f (inj₂ b)))

        g′ : ∀ {b} → ∃ (f (inj₂ b) ≡_) → C
        g′ (inj₂ c , _)  = c
        g′ (inj₁ a , eq) = g″ eq (inspect (f (inj₁ a)))

        g″ : ∀ {a b} →
             f (inj₂ b) ≡ inj₁ a → ∃ (f (inj₁ a) ≡_) → C
        g″ _   (inj₂ c , _)   = c
        g″ eq₁ (inj₁ _ , eq₂) = ⊥-elim $ hyp eq₁ eq₂

    g∘g : ∀ {b c} {B : Set b} {C : Set c}
          (f : (A ⊎ B) ↔ (A ⊎ C)) →
          (to-hyp   : Well-behaved (to   f ⟨$⟩_)) →
          (from-hyp : Well-behaved (from f ⟨$⟩_)) →
          ∀ b → g (from f ⟨$⟩_) from-hyp (g (to f ⟨$⟩_) to-hyp b) ≡ b
    g∘g f to-hyp from-hyp b = g∘g′
      where
      open P.≡-Reasoning

      g∘g′ : g (from f ⟨$⟩_) from-hyp (g (to f ⟨$⟩_) to-hyp b) ≡ b
      g∘g′ with inspect (to f ⟨$⟩ inj₂ b)
      g∘g′ | inj₂ c , eq₁ with inspect (from f ⟨$⟩ inj₂ c)
      g∘g′ | inj₂ c , eq₁ | inj₂ b′ , eq₂ = inj₂-injective (
                                              inj₂ b′            ≡⟨ P.sym eq₂ ⟩
                                              from f ⟨$⟩ inj₂ c  ≡⟨ to-from f eq₁ ⟩
                                              inj₂ b             ∎)
      g∘g′ | inj₂ c , eq₁ | inj₁ a  , eq₂ with
        inj₁ a             ≡⟨ P.sym eq₂ ⟩
        from f ⟨$⟩ inj₂ c  ≡⟨ to-from f eq₁ ⟩
        inj₂ b             ∎
      ... | ()
      g∘g′ | inj₁ a , eq₁ with inspect (to f ⟨$⟩ inj₁ a)
      g∘g′ | inj₁ a , eq₁ | inj₁ a′ , eq₂ = ⊥-elim $ to-hyp eq₁ eq₂
      g∘g′ | inj₁ a , eq₁ | inj₂ c  , eq₂ with inspect (from f ⟨$⟩ inj₂ c)
      g∘g′ | inj₁ a , eq₁ | inj₂ c  , eq₂ | inj₂ b′ , eq₃ with
        inj₁ a             ≡⟨ P.sym $ to-from f eq₂ ⟩
        from f ⟨$⟩ inj₂ c  ≡⟨ eq₃ ⟩
        inj₂ b′            ∎
      ... | ()
      g∘g′ | inj₁ a , eq₁ | inj₂ c  , eq₂ | inj₁ a′ , eq₃ with inspect (from f ⟨$⟩ inj₁ a′)
      g∘g′ | inj₁ a , eq₁ | inj₂ c  , eq₂ | inj₁ a′ , eq₃ | inj₁ a″ , eq₄ = ⊥-elim $ from-hyp eq₃ eq₄
      g∘g′ | inj₁ a , eq₁ | inj₂ c  , eq₂ | inj₁ a′ , eq₃ | inj₂ b′ , eq₄ = inj₂-injective (
        let lemma =
              inj₁ a′            ≡⟨ P.sym eq₃ ⟩
              from f ⟨$⟩ inj₂ c  ≡⟨ to-from f eq₂ ⟩
              inj₁ a             ∎
        in
        inj₂ b′             ≡⟨ P.sym eq₄ ⟩
        from f ⟨$⟩ inj₁ a′  ≡⟨ P.cong ((from f ⟨$⟩_) ∘ inj₁) $ inj₁-injective lemma ⟩
        from f ⟨$⟩ inj₁ a   ≡⟨ to-from f eq₁ ⟩
        inj₂ b              ∎)

  -- Some final lemmas.

  ∼→⊎↔⊎ :
    ∀ {x : A} {xs ys} →
    x ∷ xs ∼[ bag ] x ∷ ys →
    ∀ {z} → (z ≡ x ⊎ z ∈ xs) ↔ (z ≡ x ⊎ z ∈ ys)
  ∼→⊎↔⊎ {x} {xs} {ys} x∷xs≈x∷ys {z} =
    (z ≡ x ⊎ z ∈ xs)  ↔⟨ ∷↔ _ ⟩
    z ∈ x ∷ xs        ↔⟨ x∷xs≈x∷ys ⟩
    z ∈ x ∷ ys        ↔⟨ SK-sym (∷↔ _) ⟩
    (z ≡ x ⊎ z ∈ ys)  ∎
    where
    open Related.EquationalReasoning

  lemma : ∀ {xs ys} (inv : x ∷ xs ∼[ bag ] x ∷ ys) {z} →
          Well-behaved (Inverse.to (∼→⊎↔⊎ inv {z}) ⟨$⟩_)
  lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ with
    zero                                                                  ≡⟨⟩
    index-of {xs = x ∷ xs} (here p)                                       ≡⟨⟩
    index-of {xs = x ∷ xs} (to (∷↔ _) ⟨$⟩ inj₁ p)                         ≡⟨ P.cong (index-of ∘ (to (∷↔ (_ ≡_)) ⟨$⟩_)) $ P.sym $
                                                                               to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟩
    index-of {xs = x ∷ xs} (to (∷↔ _) ⟨$⟩ (from (∼→⊎↔⊎ inv) ⟨$⟩ inj₁ q))  ≡⟨ P.cong index-of $
                                                                               right-inverse-of (∷↔ _) (from inv ⟨$⟩ here q) ⟩
    index-of {xs = x ∷ xs} (to (SK-sym inv) ⟨$⟩ here q)                   ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩
    index-of {xs = x ∷ xs} (to (SK-sym inv) ⟨$⟩ here p)                   ≡⟨ P.cong index-of $ P.sym $
                                                                               right-inverse-of (∷↔ _) (from inv ⟨$⟩ here p) ⟩
    index-of {xs = x ∷ xs} (to (∷↔ _) ⟨$⟩ (from (∼→⊎↔⊎ inv) ⟨$⟩ inj₁ p))  ≡⟨ P.cong (index-of ∘ (to (∷↔ (_ ≡_)) ⟨$⟩_)) $
                                                                               to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩
    index-of {xs = x ∷ xs} (to (∷↔ _) ⟨$⟩ inj₂ z∈xs)                      ≡⟨⟩
    index-of {xs = x ∷ xs} (there z∈xs)                                   ≡⟨⟩
    suc (index-of {xs = xs} z∈xs)                                         ∎
    where
    open Inverse
    open P.≡-Reasoning
  ... | ()


text:
open import Nat
open import Prelude
open import contexts

module core where
  -- types
  data htyp : Set where
    num   : htyp
    ⦇-⦈   : htyp
    _==>_ : htyp → htyp → htyp
    _⊕_   : htyp → htyp → htyp
    _⊠_   : htyp → htyp → htyp

  -- type constructors bind very tightly
  infixr 25  _==>_
  infixr 25 _⊕_
  infixr 25 _⊠_

  -- external expressions
  data hexp : Set where
    N        : Nat → hexp
    _·+_     : hexp → hexp → hexp
    _·:_     : hexp → htyp → hexp
    X        : Nat → hexp
    ·λ       : Nat → hexp → hexp
    ·λ_·[_]_ : Nat → htyp → hexp → hexp
    _∘_      : hexp → hexp → hexp
    inl      : hexp → hexp
    inr      : hexp → hexp
    case     : hexp → Nat → hexp → Nat → hexp → hexp
    ⟨_,_⟩    : hexp → hexp → hexp
    fst      : hexp → hexp
    snd      : hexp → hexp
    ⦇-⦈[_]   : Nat → hexp
    ⦇⌜_⌟⦈[_] : hexp → Nat → hexp

  -- the type of type contexts, i.e. Γs in the judgements below
  tctx : Set
  tctx = htyp ctx

  -- type consistency
  data _~_ : (t1 t2 : htyp) → Set where
    TCRefl  : {τ : htyp} → τ ~ τ
    TCHole1 : {τ : htyp} → τ ~ ⦇-⦈
    TCHole2 : {τ : htyp} → ⦇-⦈ ~ τ
    TCArr   : {τ1 τ2 τ1' τ2' : htyp} →
              τ1 ~ τ1' →
              τ2 ~ τ2' →
              τ1 ==> τ2 ~ τ1' ==> τ2'
    TCSum   : {τ1 τ2 τ1' τ2' : htyp} →
              τ1 ~ τ1' →
              τ2 ~ τ2' →
              τ1 ⊕ τ2 ~ τ1' ⊕ τ2'
    TCProd  : {τ1 τ2 τ1' τ2' : htyp} →
              τ1 ~ τ1' →
              τ2 ~ τ2' →
              τ1 ⊠ τ2 ~ τ1' ⊠ τ2'

  -- type inconsistency
  _~̸_ : htyp → htyp → Set
  t1 ~̸ t2 = (t1 ~ t2) → ⊥

  -- matching for arrows
  data _▸arr_ : htyp → htyp → Set where
    MAHole : ⦇-⦈ ▸arr ⦇-⦈ ==> ⦇-⦈
    MAArr  : {τ1 τ2 : htyp} → τ1 ==> τ2 ▸arr τ1 ==> τ2

  -- matching for sums
  data _▸sum_ : htyp → htyp → Set where
    MSHole : ⦇-⦈ ▸sum ⦇-⦈ ⊕ ⦇-⦈
    MSSum  : {τ1 τ2 : htyp} → τ1 ⊕ τ2 ▸sum τ1 ⊕ τ2

  -- matching for sums
  data _▸prod_ : htyp → htyp → Set where
    MPHole : ⦇-⦈ ▸prod ⦇-⦈ ⊠ ⦇-⦈
    MPProd : {τ1 τ2 : htyp} → τ1 ⊠ τ2 ▸prod τ1 ⊠ τ2

  -- the type of hole contexts, i.e. Δs in the judgements
  hctx : Set
  hctx = (htyp ctx × htyp) ctx

  -- bidirectional type checking judgements for hexp
  mutual
    -- synthesis
    data _⊢_=>_ : (Γ : tctx) (e : hexp) (τ : htyp) → Set where
      SNum    : {Γ : tctx} {n : Nat} →
                Γ ⊢ N n => num
      SPlus   : {Γ : tctx} {e1 e2 : hexp}  →
                Γ ⊢ e1 <= num →
                Γ ⊢ e2 <= num →
                Γ ⊢ (e1 ·+ e2) => num
      SAsc    : {Γ : tctx} {e : hexp} {τ : htyp} →
                Γ ⊢ e <= τ →
                Γ ⊢ (e ·: τ) => τ
      SVar    : {Γ : tctx} {τ : htyp} {x : Nat} →
                (x , τ) ∈ Γ →
                Γ ⊢ X x => τ
      SLam    : {Γ : tctx} {e : hexp} {τ1 τ2 : htyp} {x : Nat} →
                x # Γ →
                (Γ ,, (x , τ1)) ⊢ e => τ2 →
                Γ ⊢ ·λ x ·[ τ1 ] e => τ1 ==> τ2
      SAp     : {Γ : tctx} {e1 e2 : hexp} {τ τ1 τ2 : htyp} →
                Γ ⊢ e1 => τ1 →
                τ1 ▸arr τ2 ==> τ →
                Γ ⊢ e2 <= τ2 →
                Γ ⊢ (e1 ∘ e2) => τ
      SPair   : ∀{e1 e2 τ1 τ2 Γ} →
                Γ ⊢ e1 => τ1 →
                Γ ⊢ e2 => τ2 →
                Γ ⊢ ⟨ e1 , e2 ⟩ => τ1 ⊠ τ2
      SFst    : ∀{e τ τ1 τ2 Γ} →
                Γ ⊢ e => τ →
                τ ▸prod τ1 ⊠ τ2 →
                Γ ⊢ fst e => τ1
      SSnd    : ∀{e τ τ1 τ2 Γ} →
                Γ ⊢ e => τ →
                τ ▸prod τ1 ⊠ τ2 →
                Γ ⊢ snd e => τ2
      SEHole  : {Γ : tctx} {u : Nat} →
                Γ ⊢ ⦇-⦈[ u ] => ⦇-⦈
      SNEHole : {Γ : tctx} {e : hexp} {τ : htyp} {u : Nat} →
                Γ ⊢ e => τ →
                Γ ⊢ ⦇⌜ e ⌟⦈[ u ] => ⦇-⦈

    -- analysis
    data _⊢_<=_ : (Γ : htyp ctx) (e : hexp) (τ : htyp) → Set where
      ASubsume : {Γ : tctx} {e : hexp} {τ τ' : htyp} →
                 Γ ⊢ e => τ' →
                 τ ~ τ' →
                 Γ ⊢ e <= τ
      ALam     : {Γ : tctx} {e : hexp} {τ τ1 τ2 : htyp} {x : Nat} →
                 x # Γ →
                 τ ▸arr τ1 ==> τ2 →
                 (Γ ,, (x , τ1)) ⊢ e <= τ2 →
                 Γ ⊢ (·λ x e) <= τ
      AInl     : {Γ : tctx} {e : hexp} {τ+ τ1 τ2 : htyp} →
                 τ+ ▸sum (τ1 ⊕ τ2) →
                 Γ ⊢ e <= τ1 →
                 Γ ⊢ inl e <= τ+
      AInr     : {Γ : tctx} {e : hexp} {τ+ τ1 τ2 : htyp} →
                 τ+ ▸sum (τ1 ⊕ τ2) →
                 Γ ⊢ e <= τ2 →
                 Γ ⊢ inr e <= τ+
      ACase    : {Γ : tctx} {e e1 e2 : hexp} {τ τ+ τ1 τ2 : htyp} {x y : Nat} →
                 x # Γ →
                 y # Γ →
                 τ+ ▸sum (τ1 ⊕ τ2) →
                 Γ ⊢ e => τ+ →
                 (Γ ,, (x , τ1)) ⊢ e1 <= τ →
                 (Γ ,, (y , τ2)) ⊢ e2 <= τ →
                 Γ ⊢ case e x e1 y e2 <= τ

  -- those types without holes
  data _tcomplete : htyp → Set where
    TCNum  : num tcomplete
    TCArr  : ∀{τ1 τ2} → τ1 tcomplete → τ2 tcomplete → (τ1 ==> τ2) tcomplete
    TCSum  : ∀{τ1 τ2} → τ1 tcomplete → τ2 tcomplete → (τ1 ⊕ τ2) tcomplete
    TCProd : ∀{τ1 τ2} → τ1 tcomplete → τ2 tcomplete → (τ1 ⊠ τ2) tcomplete

  -- those external expressions without holes
  data _ecomplete : hexp → Set where
    ECNum  : ∀{n} →
             (N n) ecomplete
    ECPlus : ∀{e1 e2} →
             e1 ecomplete →
             e2 ecomplete →
             (e1 ·+ e2) ecomplete
    ECAsc  : ∀{τ e} →
             τ tcomplete →
             e ecomplete →
             (e ·: τ) ecomplete
    ECVar  : ∀{x} →
             (X x) ecomplete
    ECLam1 : ∀{x e} →
             e ecomplete →
             (·λ x e) ecomplete
    ECLam2 : ∀{x e τ} →
             e ecomplete →
             τ tcomplete →
             (·λ x ·[ τ ] e) ecomplete
    ECAp   : ∀{e1 e2} →
             e1 ecomplete →
             e2 ecomplete →
             (e1 ∘ e2) ecomplete
    ECInl  : ∀{e} →
             e ecomplete →
             (inl e) ecomplete
    ECInr  : ∀{e} →
             e ecomplete →
             (inr e) ecomplete
    ECCase : ∀{e x e1 y e2} →
             e ecomplete →
             e1 ecomplete →
             e2 ecomplete →
             (case e x e1 y e2) ecomplete
    ECPair : ∀{e1 e2} →
             e1 ecomplete →
             e2 ecomplete →
             ⟨ e1 , e2 ⟩ ecomplete
    ECFst  : ∀{e} →
             e ecomplete →
             (fst e) ecomplete
    ECSnd  : ∀{e} →
             e ecomplete →
             (snd e) ecomplete

  -- contexts that only produce complete types
  _gcomplete : tctx → Set
  Γ gcomplete = (x : Nat) (τ : htyp) → (x , τ) ∈ Γ → τ tcomplete

  -- ground types
  data _ground : htyp → Set where
    GNum      : num ground
    GArrHole  : ⦇-⦈ ==> ⦇-⦈ ground
    GSumHole  : ⦇-⦈ ⊕ ⦇-⦈ ground
    GProdHole : ⦇-⦈ ⊠ ⦇-⦈ ground

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Function.PointwiseStructure where

open import Functional using (_∘_) renaming (const to const₁)
open import Function.Equals
open import Function.Multi.Functions
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Setoid
open import Structure.Operator.Field
open import Structure.Operator.Group
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator.Vector
open import Structure.Operator
open import Structure.Relator.Properties
open import Type

private variable ℓ ℓₑ ℓₗ ℓₗₑ : Lvl.Level
private variable I S T : Type{ℓ}
private variable _+_ _⋅_ : S → S → S

-- TODO: Possible to generalize to functions with multiple arguments
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  private variable _▫_ _▫₁_ _▫₂_ : T → T → T
  private variable f inv : T → T
  private variable id : T

  -- A component-wise function is a function when its underlying function is a function.
  pointwiseFunction-function : ⦃ oper : Function(f) ⦄ → Function(pointwise(1)(1) {As = I} (f))
  Function.congruence (pointwiseFunction-function {f = f}) (intro p) = intro(congruence₁(f) p)

  -- A component-wise binary operator is a binary operator when its underlying binary operator is a binary operator.
  pointwiseFunction-binaryOperator : ⦃ oper : BinaryOperator(_▫_) ⦄ → BinaryOperator(pointwise(1)(2) {As = I} (_▫_))
  BinaryOperator.congruence (pointwiseFunction-binaryOperator {_▫_ = _▫_}) (intro p) (intro q) = intro(congruence₂(_▫_) p q)

  -- A component-wise operator is associative when its underlying operator is associative.
  pointwiseFunction-associativity : ⦃ assoc : Associativity(_▫_) ⦄ → Associativity(pointwise(1)(2) {As = I} (_▫_))
  pointwiseFunction-associativity {_▫_ = _▫_} = intro(intro(associativity(_▫_)))

  -- A component-wise operator is commutative when its underlying operator is commutative.
  pointwiseFunction-commutativity : ⦃ comm : Commutativity(_▫_) ⦄ → Commutativity(pointwise(1)(2) {As = I} (_▫_))
  pointwiseFunction-commutativity {_▫_ = _▫_} = intro(intro(commutativity(_▫_)))

  -- A component-wise operator have a left identity of repeated elements when its underlying operator have a left identity.
  pointwiseFunction-identityₗ : ⦃ identₗ : Identityₗ(_▫_)(id) ⦄ → Identityₗ(pointwise(1)(2) {As = I} (_▫_))(const₁ id)
  pointwiseFunction-identityₗ {_▫_ = _▫_} {id = id} = intro(intro(identityₗ(_▫_)(id)))

  -- A component-wise operator have a right identity of repeated elements when its underlying operator have a right identity.
  pointwiseFunction-identityᵣ : ⦃ identᵣ : Identityᵣ(_▫_)(id) ⦄ → Identityᵣ(pointwise(1)(2) {As = I} (_▫_))(const₁ id)
  pointwiseFunction-identityᵣ {_▫_ = _▫_} {id = id} = intro(intro(identityᵣ(_▫_)(id)))

  -- A component-wise operator have an identity of repeated elements when its underlying operator have an identity.
  pointwiseFunction-identity : ⦃ ident : Identity(_▫_)(id) ⦄ → Identity(pointwise(1)(2) {As = I} (_▫_))(const₁ id)
  Identity.left  pointwiseFunction-identity = pointwiseFunction-identityₗ
  Identity.right pointwiseFunction-identity = pointwiseFunction-identityᵣ

  pointwiseFunction-inverseFunctionₗ : ⦃ identₗ : Identityₗ(_▫_)(id) ⦄  ⦃ inverₗ : InverseFunctionₗ(_▫_) ⦃ [∃]-intro(id) ⦄ (inv) ⦄ → InverseFunctionₗ(pointwise(1)(2) {As = I} (_▫_)) ⦃ [∃]-intro _ ⦃ pointwiseFunction-identityₗ ⦄ ⦄ (pointwise(1)(1) {As = I} inv)
  pointwiseFunction-inverseFunctionₗ {_▫_ = _▫_} {id = id} {inv = inv} = intro(intro(inverseFunctionₗ(_▫_) ⦃ [∃]-intro id ⦄ (inv)))

  pointwiseFunction-inverseFunctionᵣ : ⦃ identᵣ : Identityᵣ(_▫_)(id) ⦄  ⦃ inverᵣ : InverseFunctionᵣ(_▫_) ⦃ [∃]-intro(id) ⦄ (inv) ⦄ → InverseFunctionᵣ(pointwise(1)(2) {As = I} (_▫_)) ⦃ [∃]-intro _ ⦃ pointwiseFunction-identityᵣ ⦄ ⦄ (pointwise(1)(1) {As = I} inv)
  pointwiseFunction-inverseFunctionᵣ {_▫_ = _▫_} {id = id} {inv = inv} = intro(intro(inverseFunctionᵣ(_▫_) ⦃ [∃]-intro id ⦄ (inv)))

  pointwiseFunction-inverseFunction : ⦃ ident : Identity(_▫_)(id) ⦄  ⦃ inver : InverseFunction(_▫_) ⦃ [∃]-intro(id) ⦄ (inv) ⦄ → InverseFunction(pointwise(1)(2) {As = I} (_▫_)) ⦃ [∃]-intro _ ⦃ pointwiseFunction-identity ⦄ ⦄ (pointwise(1)(1) {As = I} inv)
  InverseFunction.left  pointwiseFunction-inverseFunction = pointwiseFunction-inverseFunctionₗ
  InverseFunction.right pointwiseFunction-inverseFunction = pointwiseFunction-inverseFunctionᵣ

  -- A component-wise operator is left distributive over another component-wise operator when their underlying operators distribute.
  pointwiseFunction-distributivityₗ : ⦃ distₗ : Distributivityₗ(_▫₁_)(_▫₂_) ⦄ → Distributivityₗ(pointwise(1)(2) {As = I} (_▫₁_))(pointwise(1)(2) {As = I} (_▫₂_))
  pointwiseFunction-distributivityₗ = intro(intro(distributivityₗ _ _))

  -- A component-wise operator is right distributive over another component-wise operator when their underlying operators distribute.
  pointwiseFunction-distributivityᵣ : ⦃ distᵣ : Distributivityᵣ(_▫₁_)(_▫₂_) ⦄ → Distributivityᵣ(pointwise(1)(2) {As = I} (_▫₁_))(pointwise(1)(2) {As = I} (_▫₂_))
  pointwiseFunction-distributivityᵣ = intro(intro(distributivityᵣ _ _))

  pointwiseFunction-const-preserves : Preserving₂(const₁) (_▫_) (pointwise(1)(2) {As = I} (_▫_))
  pointwiseFunction-const-preserves = intro(intro(reflexivity(_≡_)))

  -- A component-wise operator is a monoid when its underlying operator is a monoid.
  pointwiseFunction-monoid : ⦃ monoid : Monoid(_▫_) ⦄ → Monoid(pointwise(1)(2) {As = I} (_▫_))
  Monoid.binary-operator    pointwiseFunction-monoid = pointwiseFunction-binaryOperator
  Monoid.associativity      pointwiseFunction-monoid = pointwiseFunction-associativity
  Monoid.identity-existence pointwiseFunction-monoid = [∃]-intro _ ⦃ pointwiseFunction-identity ⦄

  -- A component-wise operator is a group when its underlying operator is a group.
  pointwiseFunction-group : ⦃ group : Group(_▫_) ⦄ → Group(pointwise(1)(2) {As = I} (_▫_))
  Group.monoid            pointwiseFunction-group = pointwiseFunction-monoid
  Group.inverse-existence pointwiseFunction-group = [∃]-intro _ ⦃ pointwiseFunction-inverseFunction ⦄
  Group.inv-function      pointwiseFunction-group = pointwiseFunction-function

  -- A component-wise operator is a commutative group when its underlying operator is a commutative group.
  pointwiseFunction-commutativeGroup : ⦃ commutativeGroup : CommutativeGroup(_▫_) ⦄ → CommutativeGroup(pointwise(1)(2) {As = I} (_▫_))
  CommutativeGroup.group         pointwiseFunction-commutativeGroup = pointwiseFunction-group
  CommutativeGroup.commutativity pointwiseFunction-commutativeGroup = pointwiseFunction-commutativity

module _
  ⦃ equiv : Equiv{ℓₑ}(S) ⦄
  (field-structure : Field{T = S}(_+_)(_⋅_))
  where
  open Field(field-structure)

  -- Component-wise operators constructs a vector space from a field when using the fields as scalars and coordinate vectors as vectors.
  pointwiseFunction-vectorSpace : VectorSpace(pointwise(1)(2) {As = I} (_+_))(pointwise(1)(1) ∘ (_⋅_))(_+_)(_⋅_)
  VectorSpace.scalarField pointwiseFunction-vectorSpace = field-structure
  VectorSpace.vectorCommutativeGroup pointwiseFunction-vectorSpace = pointwiseFunction-commutativeGroup
  _⊜_.proof (BinaryOperator.congruence (VectorSpace.[⋅ₛᵥ]-binaryOperator pointwiseFunction-vectorSpace) p (intro q)) = congruence₂(_⋅_) p q
  _⊜_.proof (VectorSpace.[⋅ₛ][⋅ₛᵥ]-compatibility pointwiseFunction-vectorSpace) = associativity(_⋅_)
  _⊜_.proof (Identityₗ.proof (VectorSpace.[⋅ₛᵥ]-identity pointwiseFunction-vectorSpace)) = identityₗ(_⋅_)(𝟏)
  _⊜_.proof (Distributivityₗ.proof (VectorSpace.[⋅ₛᵥ][+ᵥ]-distributivityₗ pointwiseFunction-vectorSpace)) = distributivityₗ(_⋅_)(_+_)
  _⊜_.proof (VectorSpace.[⋅ₛᵥ][+ₛ][+ᵥ]-distributivityᵣ pointwiseFunction-vectorSpace) = distributivityᵣ(_⋅_)(_+_)


text:
open import Oscar.Prelude
open import Oscar.Class

module Oscar.Class.Leftstar where

module Leftstar
  {𝔞 𝔟 𝔣 𝔞̇ 𝔟̇}
  {𝔄 : Ø 𝔞}
  {𝔅 : Ø 𝔟}
  {𝔉 : Ø 𝔣}
  (𝔄̇ : 𝔄 → Ø 𝔞̇)
  (𝔅̇ : 𝔅 → Ø 𝔟̇)
  (_◂_ : 𝔉 → 𝔄 → 𝔅)
  = ℭLASS (_◂_ , 𝔅̇) (∀ {x} f → 𝔄̇ x → 𝔅̇ (f ◂ x))

module _
  {𝔞 𝔟 𝔣 𝔞̇ 𝔟̇}
  {𝔄 : Ø 𝔞}
  {𝔅 : Ø 𝔟}
  {𝔉 : Ø 𝔣}
  {𝔄̇ : 𝔄 → Ø 𝔞̇}
  {𝔅̇ : 𝔅 → Ø 𝔟̇}
  {_◂_ : 𝔉 → 𝔄 → 𝔅}
  where
  leftstar = Leftstar.method 𝔄̇ 𝔅̇ _◂_

open import Oscar.Class.Surjection
open import Oscar.Class.Smap

module Leftstar,smaparrow
  {𝔵₁ 𝔵₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  {𝔭₁ 𝔭₂} (𝔓₁ : 𝔛₂ → Ø 𝔭₁) (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭̇₁} (𝔓̇₁ : ∀ {a} → 𝔓₁ (surjection a) → Ø 𝔭̇₁)
  {𝔭̇₂} (𝔓̇₂ : ∀ {a} → 𝔓₂ (surjection a) → Ø 𝔭̇₂)
  (smaparrow : Smaparrow.type ℜ 𝔓₁ 𝔓₂ surjection surjection)
  where
  class = ∀ {a₁ a₂} → Leftstar.class (𝔓̇₁ {a₁}) (𝔓̇₂ {a₂}) smaparrow
  type = ∀ {a₁ a₂} → Leftstar.type (𝔓̇₁ {a₁}) (𝔓̇₂ {a₂}) smaparrow

module Leftstar,smaparrow!
  {𝔵₁ 𝔵₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  {𝔭₁ 𝔭₂} (𝔓₁ : 𝔛₂ → Ø 𝔭₁) (𝔓₂ : 𝔛₂ → Ø 𝔭₂)
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭̇₁} (𝔓̇₁ : ∀ {a} → 𝔓₁ (surjection a) → Ø 𝔭̇₁)
  {𝔭̇₂} (𝔓̇₂ : ∀ {a} → 𝔓₂ (surjection a) → Ø 𝔭̇₂)
  ⦃ _ : Smaparrow!.class ℜ 𝔓₁ 𝔓₂ ⦄
  = Leftstar,smaparrow surjection 𝔓₁ 𝔓₂ ℜ 𝔓̇₁ 𝔓̇₂ smaparrow

module Leftstar,smaphomarrow
  {𝔵₁ 𝔵₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  (surjection : Surjection.type 𝔛₁ 𝔛₂)
  {𝔭} (𝔓 : 𝔛₂ → Ø 𝔭)
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭̇} (𝔓̇ : ∀ {a} → 𝔓 (surjection a) → Ø 𝔭̇)
  (smaparrow : Smaphomarrow.type ℜ 𝔓 surjection)
  = Leftstar,smaparrow surjection 𝔓 𝔓 ℜ 𝔓̇ 𝔓̇ smaparrow

module Leftstar,smaphomarrow!
  {𝔵₁ 𝔵₂} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂}
  ⦃ _ : Surjection.class 𝔛₁ 𝔛₂ ⦄
  {𝔭} (𝔓 : 𝔛₂ → Ø 𝔭)
  {𝔯} (ℜ : 𝔛₁ → 𝔛₁ → Ø 𝔯)
  {𝔭̇} (𝔓̇ : ∀ {a} → 𝔓 (surjection a) → Ø 𝔭̇)
  ⦃ _ : Smaphomarrow!.class ℜ 𝔓 ⦄
  = Leftstar,smaphomarrow surjection 𝔓 ℜ 𝔓̇ smaparrow


text:
module _ where

data _==_ {A : Set} (a : A) : A → Set where
  refl : a == a

data ⊥ : Set where

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

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

f : (n : ℕ) ⦃ p : ⦃ _ : n == zero ⦄ → ⊥ ⦄ → ℕ
f n = n

g : (n : ℕ) ⦃ q : ⦃ _ : n == zero ⦄ → ⊥ ⦄ → ℕ
g n ⦃ q ⦄ = f n

h : (n : ℕ) ⦃ q : ⦃ _ : n == zero ⦄ → ⊥ ⦄ → ℕ
h n ⦃ q ⦄ = f n ⦃ it ⦄

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

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

module DistributiveLaws.TaskB-AllStepsATP where

open import DistributiveLaws.Base

open import Common.FOL.Relation.Binary.EqReasoning

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

-- We prove all the proof steps of DistributiveLaws.TaskB-I using the
-- ATPs.

prop₂ : ∀ u x y z →
        (x · y · (z · u)) · ((x · y · (z · u)) · (x · z · (y · u))) ≡
          x · z · (y · u)
prop₂ u x y z =
  xy·zu · (xy·zu · xz·yu)                                         ≡⟨ j₁ ⟩
  xy·zu · (x·zu · y·zu · xz·yu)                                   ≡⟨ j₂ ⟩
  xy·zu · (x·zu · xz·yu · (y·zu · xz·yu))                         ≡⟨ j₃ ⟩
  xy·zu · (xz·xu · xz·yu · (y·zu · xz·yu))                        ≡⟨ j₄ ⟩
  xy·zu · (xz · xu·yu · (y·zu · xz·yu))                           ≡⟨ j₅ ⟩
  xy·zu · (xz · xyu · (y·zu · xz·yu))                             ≡⟨ j₆ ⟩
  xy·zu · (xz · xyu · (yz·yu · xz·yu))                            ≡⟨ j₇ ⟩
  xy·zu · (xz · xyu · (yz·xz · yu))                               ≡⟨ j₈ ⟩
  xy·zu · (xz · xyu · (yxz · yu))                                 ≡⟨ j₉ ⟩
  xy·zu · (xz · xyu · (yx·yu · z·yu))                             ≡⟨ j₁₀ ⟩
  xy·zu · (xz · xyu · (y·xu · z·yu))                              ≡⟨ j₁₁ ⟩
  xyz · xyu · (xz · xyu · (y·xu · z·yu))                          ≡⟨ j₁₂ ⟩
  xz·yz · xyu · (xz · xyu · (y·xu · z·yu))                        ≡⟨ j₁₃ ⟩
  xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))              ≡⟨ j₁₄ ⟩
  xz · xyu · (yz · xyu · (y·xu · z·yu))                           ≡⟨ j₁₅ ⟩
  xz · xyu · (yz · xu·yu · (y·xu · z·yu))                         ≡⟨ j₁₆ ⟩
  xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu))            ≡⟨ j₁₇ ⟩
  xz · xyu ·
  (y · xu·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))       ≡⟨ j₁₈ ⟩
  xz · xyu ·
  (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))     ≡⟨ j₁₉ ⟩
  xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡⟨ j₂₀ ⟩
  xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu)))         ≡⟨ j₂₁ ⟩
  xz · xyu · (y·xu · y·zu · (z · xu·yu · (y·xu · z·yu)))          ≡⟨ j₂₂ ⟩
  xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))            ≡⟨ j₂₃ ⟩
  xz · xyu · (y · xu·zu · (z·xu · z·yu · (y·xu · z·yu)))          ≡⟨ j₂₄ ⟩
  (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))                 ≡⟨ j₂₅ ⟩
  xz · xyu · (y · xu·zu · (zy·xu · z·yu))                         ≡⟨ j₂₆ ⟩
  xz · xyu · (y · xu·zu · (zy·xu · zy·zu))                        ≡⟨ j₂₇ ⟩
  xz · xyu · (y · xu·zu · (zy · xu·zu))                           ≡⟨ j₂₈ ⟩
  xz · xyu · (y·zy · xu·zu)                                       ≡⟨ j₂₉ ⟩
  xz · xyu · (y·zy · xzu)                                         ≡⟨ j₃₀ ⟩
  xz·xy · xzu · (y·zy · xzu)                                      ≡⟨ j₃₁ ⟩
  x·zy · xzu · (y·zy · xzu)                                       ≡⟨ j₃₂ ⟩
  x·zy · y·zy · xzu                                               ≡⟨ j₃₃ ⟩
  xy·zy · xzu                                                     ≡⟨ j₃₄ ⟩
  xzy · xzu                                                       ≡⟨ j₃₅ ⟩
  xz·yu                                                           ∎
  where
  -- Two variables abbreviations

  xz = x · z
  yu = y · u
  yz = y · z
  zy = z · y
  {-# ATP definitions xz yu yz zy #-}

  -- Three variables abbreviations

  xyu = x · y · u
  xyz = x · y · z
  xzu = x · z · u
  xzy = x · z · y
  yxz = y · x · z
  {-# ATP definitions xyu xyz xzu xzy yxz #-}

  x·yu = x · (y · u)
  x·zu = x · (z · u)
  x·zy = x · (z · y)
  {-# ATP definitions x·yu x·zu x·zy #-}

  y·xu = y · (x · u)
  y·yu = y · (y · u)
  y·zu = y · (z · u)
  y·zy = y · (z · y)
  {-# ATP definitions y·xu y·yu y·zu y·zy #-}

  z·xu = z · (x · u)
  z·yu = z · (y · u)
  {-# ATP definitions z·xu z·yu #-}

  -- Four variables abbreviations

  xu·yu = x · u · (y · u)
  xu·zu = x · u · (z · u)
  {-# ATP definitions xu·yu xu·zu #-}

  xy·yz = x · y · (y · z)
  xy·zu = x · y · (z · u)
  xy·zy = x · y · (z · y)
  {-# ATP definitions xy·yz xy·zu xy·zy #-}

  xz·xu = x · z · (x · u)
  xz·xy = x · z · (x · y)
  xz·yu = x · z · (y · u)
  xz·yz = x · z · (y · z)
  {-# ATP definitions xz·xu xz·xy xz·yu xz·yz #-}

  yx·yu = y · x · (y · u)
  {-# ATP definition yx·yu #-}

  yz·xz = y · z · (x · z)
  yz·yu = y · z · (y · u)
  {-# ATP definitions yz·xz yz·yu #-}

  zy·xu = z · y · (x · u)
  zy·zu = z · y · (z · u)
  {-# ATP definitions zy·xu zy·zu #-}

  -- Steps justifications

  postulate j₁ : xy·zu · (xy·zu · xz·yu) ≡
                 xy·zu · (x·zu · y·zu · xz·yu)
  {-# ATP prove j₁ #-}

  postulate j₂ : xy·zu · (x·zu · y·zu · xz·yu) ≡
                 xy·zu · (x·zu · xz·yu · (y·zu · xz·yu))
  {-# ATP prove j₂ #-}

  postulate j₃ : xy·zu · (x·zu · xz·yu · (y·zu · xz·yu)) ≡
                 xy·zu · (xz·xu · xz·yu · (y·zu · xz·yu))
  {-# ATP prove j₃ #-}

  postulate j₄ : xy·zu · (xz·xu · xz·yu · (y·zu · xz·yu)) ≡
                 xy·zu · (xz · xu·yu · (y·zu · xz·yu))
  {-# ATP prove j₄ #-}

  postulate j₅ : xy·zu · (xz · xu·yu · (y·zu · xz·yu)) ≡
                 xy·zu · (xz · xyu · (y·zu · xz·yu))
  {-# ATP prove j₅ #-}

  postulate j₆ : xy·zu · (xz · xyu · (y·zu · xz·yu)) ≡
                 xy·zu · (xz · xyu · (yz·yu · xz·yu))
  {-# ATP prove j₆ #-}

  postulate j₇ : xy·zu · (xz · xyu · (yz·yu · xz·yu)) ≡
                 xy·zu · (xz · xyu · (yz·xz · yu))
  {-# ATP prove j₇ #-}

  postulate j₈ : xy·zu · (xz · xyu · (yz·xz · yu)) ≡
                 xy·zu · (xz · xyu · (yxz · yu))
  {-# ATP prove j₈ #-}

  postulate j₉ : xy·zu · (xz · xyu · (yxz · yu)) ≡
                 xy·zu · (xz · xyu · (yx·yu · z·yu))
  {-# ATP prove j₉ #-}

  postulate j₁₀ : xy·zu · (xz · xyu · (yx·yu · z·yu)) ≡
                  xy·zu · (xz · xyu · (y·xu · z·yu))
  {-# ATP prove j₁₀ #-}

  postulate j₁₁ : xy·zu · (xz · xyu · (y·xu · z·yu)) ≡
                  xyz · xyu · (xz · xyu · (y·xu · z·yu))
  {-# ATP prove j₁₁ #-}

  postulate j₁₂ : xyz · xyu · (xz · xyu · (y·xu · z·yu)) ≡
                  xz·yz · xyu · (xz · xyu · (y·xu · z·yu))
  {-# ATP prove j₁₂ #-}

  postulate j₁₃ : xz·yz · xyu · (xz · xyu · (y·xu · z·yu)) ≡
                  xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))
  {-# ATP prove j₁₃ #-}

  postulate j₁₄ : xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu)) ≡
                  xz · xyu · (yz · xyu · (y·xu · z·yu))
  {-# ATP prove j₁₄ #-}

  postulate j₁₅ : xz · xyu · (yz · xyu · (y·xu · z·yu)) ≡
                  xz · xyu · (yz · xu·yu · (y·xu · z·yu))
  {-# ATP prove j₁₅ #-}

  postulate j₁₆ : xz · xyu · (yz · xu·yu · (y·xu · z·yu)) ≡
                  xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu))
  {-# ATP prove j₁₆ #-}

  postulate
    j₁₇ : xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu)) ≡
          xz · xyu ·
          (y · xu·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₁₇ #-}

  postulate
    j₁₈ : xz · xyu ·
          (y · xu·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
          xz · xyu ·
          (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₁₈ #-}

  postulate
    j₁₉ : xz · xyu ·
          (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
          xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₁₉ #-}

  postulate
    j₂₀ : xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
          xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₂₀ #-}

  postulate j₂₁ : xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu))) ≡
                  xz · xyu · (y·xu · y·zu · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₂₁ #-}

  postulate j₂₂ : xz · xyu · (y·xu · y·zu · (z · xu·yu · (y·xu · z·yu))) ≡
                  xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₂₂ #-}

  postulate j₂₃ : xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu))) ≡
                  xz · xyu · (y · xu·zu · (z·xu · z·yu · (y·xu · z·yu)))
  {-# ATP prove j₂₃ #-}

  postulate j₂₄ : xz · xyu · (y · xu·zu · (z·xu · z·yu · (y·xu · z·yu))) ≡
                  (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))
  {-# ATP prove j₂₄ #-}

  postulate j₂₅ : (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu)) ≡
                  xz · xyu · (y · xu·zu · (zy·xu · z·yu))
  {-# ATP prove j₂₅ #-}

  postulate j₂₆ : xz · xyu · (y · xu·zu · (zy·xu · z·yu)) ≡
                  xz · xyu · (y · xu·zu · (zy·xu · zy·zu))
  {-# ATP prove j₂₆ #-}

  postulate j₂₇ : xz · xyu · (y · xu·zu · (zy·xu · zy·zu)) ≡
                  xz · xyu · (y · xu·zu · (zy · xu·zu))
  {-# ATP prove j₂₇ #-}

  postulate j₂₈ : xz · xyu · (y · xu·zu · (zy · xu·zu)) ≡
                  xz · xyu · (y·zy · xu·zu)
  {-# ATP prove j₂₈ #-}

  postulate j₂₉ : xz · xyu · (y·zy · xu·zu) ≡ xz · xyu · (y·zy · xzu)
  {-# ATP prove j₂₉ #-}

  postulate j₃₀ : xz · xyu · (y·zy · xzu) ≡ xz·xy · xzu · (y·zy · xzu)
  {-# ATP prove j₃₀ #-}

  postulate j₃₁ : xz·xy · xzu · (y·zy · xzu) ≡ x·zy · xzu · (y·zy · xzu)
  {-# ATP prove j₃₁ #-}

  postulate j₃₂ : x·zy · xzu · (y·zy · xzu) ≡ x·zy · y·zy · xzu
  {-# ATP prove j₃₂ #-}

  postulate j₃₃ : x·zy · y·zy · xzu ≡ xy·zy · xzu
  {-# ATP prove j₃₃ #-}

  postulate j₃₄ : xy·zy · xzu ≡ xzy · xzu
  {-# ATP prove j₃₄ #-}

  postulate j₃₅ : xzy · xzu ≡ xz·yu
  {-# ATP prove j₃₅ #-}


text:
-- Properties of quicksort

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

open import Relation.Binary

module Algorithms.List.Sort.Quick.Properties
  {c l₁ l₂} (DTO : DecTotalOrder c l₁ l₂)
  where

-- agda-stdlib
open import Level
open import Data.List
import      Data.List.Properties as Listₚ
import Data.List.Relation.Binary.Equality.Setoid as EqualitySetoid
import Data.List.Relation.Binary.Permutation.Setoid as PermutationSetoid
open import Data.Product
import      Data.Nat as ℕ
open import Data.Nat.Induction as Ind
open import Relation.Binary as B
open import Relation.Unary as U
import      Relation.Unary.Properties as Uₚ
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Function.Base
open import Induction.WellFounded

-- agda-misc
open import Algorithms.List.Sort.Common DTO
open import Algorithms.List.Sort.Quick

open DecTotalOrder DTO renaming (Carrier to A)
open Quicksort _≤?_
open PermutationSetoid Eq.setoid
open EqualitySetoid Eq.setoid
{-
sort-acc-cong : ∀ {xs ys rs₁ rs₂} → xs ≋ ys → sort-acc xs rs₁ ≋ sort-acc ys rs₂
sort-acc-cong {[]}     {[]}     {rs₁}     {rs₂}     xs≋ys = ≋-refl
sort-acc-cong {x ∷ xs} {y ∷ ys} {acc rs₁} {acc rs₂} (x≈y EqualitySetoid.∷ xs≋ys) =
  ++⁺ (sort-acc-cong {!   !}) (++⁺ (x≈y ∷ []) {!   !})
-}

{-
sort-acc-filter : ∀ x xs rs lt₁ lt₂ →
  sort-acc (x ∷ xs) (acc rs) ≡
  sort-acc (filter (_≤? x) xs) (rs _ lt₁) ++ [ x ] ++
  sort-acc (filter (Uₚ.∁? (_≤? x)) xs) (rs _ lt₂)
sort-acc-filter x xs rs lt₁ lt₂ = begin
  sort-acc (proj₁ (split x xs)) (rs _ _) ++ [ x ] ++
    sort-acc (proj₂ (split x xs)) (rs _ _)
    ≡⟨ ? ⟩
  sort-acc (filter (_≤? x) xs) (rs _ lt₁) ++ [ x ] ++
    sort-acc (filter (Uₚ.∁? (_≤? x)) xs) (rs _ lt₂) ∎

sort-acc-permutation : ∀ xs ac → sort-acc xs ac ↭ xs
sort-acc-permutation []       ac       = ↭-refl
sort-acc-permutation (x ∷ xs) (acc rs) = begin
  sort-acc (x ∷ xs) (acc rs) ≈⟨ {!   !} ⟩
  x ∷ xs ∎
  where open SetoidReasoning ↭-setoid
-}


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

-- In this module, we define the usual definition of D<: -- the one having typing and
-- subtyping mutually defined.
module DsubFull where

open import Data.List as List
open import Data.List.All as All
open import Data.Nat as ℕ
open import Data.Maybe as Maybe
open import Data.Product
open import Data.Sum
open import Data.Empty renaming (⊥ to False)
open import Data.Vec as Vec renaming (_∷_ to _‼_ ; [] to nil) hiding (_++_)
open import Function

open import Data.Maybe.Properties as Maybeₚ
open import Data.Nat.Properties as ℕₚ
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as ≡

open import DsubDef
open import Dsub renaming (_⊢_<:_ to _⊢′_<:_)
open import Utils

infix 4 _⊢_<:_ _⊢_∶_

mutual
  data _⊢_∶_ : Env → Trm → Typ → Set where
    var∶  : ∀ {Γ n T} →
      (T∈Γ : env-lookup Γ n ≡ just T) →
      Γ ⊢ var n ∶ T
    Π-I   : ∀ {Γ T t U} →
      Γ ‣ T ! ⊢ t ∶ U →
      Γ ⊢ val (Λ T ∙ t) ∶ Π T ∙ U
    Π-E   : ∀ {Γ n m S U} →
      Γ ⊢ var n ∶ Π S ∙ U →
      Γ ⊢ var m ∶ S →
      Γ ⊢ n $$ m ∶ U [ m / 0 ]
    ⟨A⟩-I : ∀ {Γ T} →
      Γ ⊢ val ⟨A= T ⟩ ∶ ⟨A: T ⋯ T ⟩
    ltinn : ∀ {Γ t u T U} →
      Γ ⊢ t ∶ T →
      Γ ‣ T ! ⊢ u ∶ U ↑ 0 →
      Γ ⊢ lt t inn u ∶ U
    <∶   : ∀ {Γ t S U} →
      Γ ⊢ t ∶ S →
      Γ ⊢ S <: U →
      Γ ⊢ t ∶ U

  data _⊢_<:_ : Env → Typ → Typ → Set where
    <:⊤   : ∀ {Γ T} →
      Γ ⊢ T <: ⊤
    ⊥<:   : ∀ {Γ T} →
      Γ ⊢ ⊥ <: T
    refl  : ∀ {Γ T} →
      Γ ⊢ T <: T
    tran : ∀ {Γ S U} T →
      (S<:T : Γ ⊢ S <: T) →
      (T<:U : Γ ⊢ T <: U) →
      Γ ⊢ S <: U
    bnd   : ∀ {Γ S U S′ U′} →
      (S′<:S : Γ ⊢ S′ <: S) →
      (U<:U′ : Γ ⊢ U <: U′) →
      Γ ⊢ ⟨A: S ⋯ U ⟩ <: ⟨A: S′ ⋯ U′ ⟩
    Π<:   : ∀ {Γ S U S′ U′} →
      (S′<:S : Γ ⊢ S′ <: S) →
      (U<:U′ : (S′ ∷ Γ) ⊢ U <: U′) →
      Γ ⊢ Π S ∙ U <: Π S′ ∙ U′
    sel₁  : ∀ {Γ n S U} →
      Γ ⊢ var n ∶ ⟨A: S ⋯ U ⟩ →
      Γ ⊢ S <: n ∙A
    sel₂  : ∀ {Γ n S U} →
      Γ ⊢ var n ∶ ⟨A: S ⋯ U ⟩ →
      Γ ⊢ n ∙A <: U

-- The following function shows that indeed the subtyping defined in Lemma 2 is
-- equivalent to the original subtyping.
mutual
  <:⇒<:′ : ∀ {Γ S U} → Γ ⊢ S <: U → Γ ⊢′ S <: U
  <:⇒<:′ <:⊤                = dtop
  <:⇒<:′ ⊥<:                = dbot
  <:⇒<:′ refl               = drefl
  <:⇒<:′ (tran T S<:T T<:U) = dtrans T (<:⇒<:′ S<:T) (<:⇒<:′ T<:U)
  <:⇒<:′ (bnd S′<:S U<:U′)  = dbnd (<:⇒<:′ S′<:S) (<:⇒<:′ U<:U′)
  <:⇒<:′ (Π<: S′<:S U<:U′)  = dall (<:⇒<:′ S′<:S) (<:⇒<:′ U<:U′)
  <:⇒<:′ (sel₁ n∶SU) with var∶⇒<: n∶SU
  ... | T′ , T′∈Γ , T′<:SU  = dsel₁ T′∈Γ (dtrans _ T′<:SU (dbnd drefl dtop))
  <:⇒<:′ (sel₂ n∶SU) with var∶⇒<: n∶SU
  ... | T′ , T′∈Γ , T′<:SU  = dsel₂ T′∈Γ (dtrans _ T′<:SU (dbnd dbot drefl))

  var∶⇒<: : ∀ {Γ x T} → Γ ⊢ var x ∶ T → ∃ λ T′ → env-lookup Γ x ≡ just T′ × Γ ⊢′ T′ <: T
  var∶⇒<: (var∶ T∈Γ)      = -, T∈Γ , drefl
  var∶⇒<: (<∶ x∶T T<:U) with var∶⇒<: x∶T
  ... | T′ , T′∈Γ , T′<:T = T′ , T′∈Γ , dtrans _ T′<:T (<:⇒<:′ T<:U)

<:′⇒<: : ∀ {Γ S U} → Γ ⊢′ S <: U → Γ ⊢ S <: U
<:′⇒<: dtop                 = <:⊤
<:′⇒<: dbot                 = ⊥<:
<:′⇒<: drefl                = refl
<:′⇒<: (dtrans T S<:T T<:U) = tran T (<:′⇒<: S<:T) (<:′⇒<: T<:U)
<:′⇒<: (dbnd S′<:S U<:U′)   = bnd (<:′⇒<: S′<:S) (<:′⇒<: U<:U′)
<:′⇒<: (dall S′<:S U<:U′)   = Π<: (<:′⇒<: S′<:S) (<:′⇒<: U<:U′)
<:′⇒<: (dsel₁ T∈Γ T<:SU)    = sel₁ (<∶ (var∶ T∈Γ) (<:′⇒<: T<:SU))
<:′⇒<: (dsel₂ T∈Γ T<:SU)    = sel₂ (<∶ (var∶ T∈Γ) (<:′⇒<: T<:SU))


text:
module Numeric.Nat where

open import Numeric.Nat.BinarySearch      public
open import Numeric.Nat.Divide.Properties public
open import Numeric.Nat.Divide            public
open import Numeric.Nat.DivMod            public
open import Numeric.Nat.GCD.Extended      public
open import Numeric.Nat.GCD.Properties    public
open import Numeric.Nat.GCD               public
open import Numeric.Nat.LCM.Properties    public
open import Numeric.Nat.LCM               public
open import Numeric.Nat.Modulo            public
open import Numeric.Nat.Pow               public
open import Numeric.Nat.Prime.Properties  public
open import Numeric.Nat.Prime             public
open import Numeric.Nat.Properties        public
open import Numeric.Nat.Sqrt              public

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
postulate
  A : Set

data B : Set where
  x : A → B

f : A → A
f = {!!} -- C-c C-c yields 'f x = ?', which fails to type check


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Data.Vec.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
------------------------------------------------------------------------

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

module Data.Vec.Membership.Propositional {a} {A : Set a} where

open import Data.Vec using (Vec)
open import Data.Vec.Relation.Unary.Any using (Any)
open import Relation.Binary.PropositionalEquality using (setoid; subst)

import Data.Vec.Membership.Setoid as SetoidMembership

------------------------------------------------------------------------
-- Re-export contents of setoid membership

open SetoidMembership (setoid A) public hiding (lose)

------------------------------------------------------------------------
-- Other operations

lose : ∀ {p} {P : A → Set p} {x n} {xs : Vec A n} → x ∈ xs → P x → Any P xs
lose = SetoidMembership.lose (setoid A) (subst _)


text:
module hello where

open import IO

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

max_stars_repo_name: nhutnamhcmus/code

max_issues_repo_name: nhutnamhcmus/code

max_forks_repo_name: nhutnamhcmus/code


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

open import HoTT

module stash.modalities.PushoutProduct {i j k l}
  {A : Type i} {B : Type j}
  {A' : Type k} {B' : Type l}
  where

□-span : (f : A → B) (g : A' → B') → Span
□-span f g = span (B × A') (A × B') (A × A')
  (λ { (a , a') → f a , a'})
  (λ { (a , a') → a , g a' })

module PshoutProd (f : A → B) (g : A' → B') =
  PushoutRec {d = □-span f g}
    (λ { (b , a') → b , g a' })
    (λ { (a , b') → f a , b' })
    (λ { (a , a') → idp })

_□_ : (f : A → B) (g : A' → B') → Pushout (□-span f g) → B × B'
f □ g = PshoutProd.f f g

□-glue-β : (f : A → B) (g : A' → B') (a : A) (a' : A') → ap (f □ g) (glue (a , a')) == idp
□-glue-β f g a a' = PshoutProd.glue-β f g (a , a')

module _ (f : A → B) (g : A' → B') where

  private
    abstract

      ↓-□=cst-out : ∀ {a a' b b'} {p p' : (f a , g a') == (b , b')}
        → p == p' [ (λ w → (f □ g) w == (b , b')) ↓ glue (a , a') ]
        → p == p'
      ↓-□=cst-out {p' = idp} q = ↓-app=cst-out' q ∙ □-glue-β f g _ _

      ↓-□=cst-in : ∀ {a a' b b'} {p p' : (f a , g a') == (b , b')}
        → p == p'
        → p == p' [ (λ w → (f □ g) w == (b , b')) ↓ glue (a , a') ]
      ↓-□=cst-in {p' = idp} q = ↓-app=cst-in' (q ∙ ! (□-glue-β f g _ _))

      ↓-□=cst-β : ∀ {a a' b b'} {p p' : (f a , g a') == (b , b')}
        (q : p == p')
        → ↓-□=cst-out (↓-□=cst-in q) == q
      ↓-□=cst-β {a} {a'} {p' = idp} idp = {!!}  ∙ !-inv-l (□-glue-β f g a a')

  □-hfiber-to : (b : B) (b' : B')
    → hfiber (f □ g) (b , b') → hfiber f b * hfiber g b'
  □-hfiber-to b b' = uncurry $ Pushout-elim
    (λ { (_ , a') → λ p → right (a' , snd×= p) })
    (λ { (a , _) → λ p → left (a , fst×= p) }) {!!}

  --
  -- Here is the main theorem
  --

  □-hfiber : (b : B) (b' : B')
    → hfiber (f □ g) (b , b') ≃ hfiber f b * hfiber g b'
  □-hfiber b b' = {!!}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module DivMod where

open import IO
open import Data.Nat
open import Data.Nat.DivMod
open import Coinduction
open import Data.String
open import Data.Fin

g : ℕ
g = 7 div 5

k : ℕ
k = toℕ (7 mod 5)

showNat : ℕ → String
showNat zero = "Z"
showNat (suc x) = "S (" ++ showNat x ++ ")"

main = run (♯ (putStrLn (showNat g)) >> ♯ (putStrLn (showNat k)))

max_stars_repo_name: andreasabel/agda-with-old-branches

max_issues_repo_name: andersk/agda

max_forks_repo_name: andersk/agda


text:
{-# OPTIONS --prop #-}

True : Prop
True = {P : Prop} → P → P

-- Current error (incomprehensible):
-- Set₁ != Set
-- when checking that the expression {P : Prop} → P → P has type Prop

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module README where

------------------------------------------------------------------------
-- The Agda standard library, version 0.9
--
-- Author: Nils Anders Danielsson, with contributions from Andreas
-- Abel, Stevan Andjelkovic, Jean-Philippe Bernardy, Peter Berry,
-- Joachim Breitner, Samuel Bronson, Daniel Brown, James Chapman,
-- Liang-Ting Chen, Dominique Devriese, Dan Doel, Érdi Gergő, Helmut
-- Grohne, Simon Foster, Liyang Hu, Patrik Jansson, Alan Jeffrey,
-- Pepijn Kokke, Evgeny Kotelnikov, Eric Mertens, Darin Morrison,
-- Guilhem Moulin, Shin-Cheng Mu, Ulf Norell, Noriyuki OHKAWA, Nicolas
-- Pouillard, Andrés Sicard-Ramírez and Noam Zeilberger.
------------------------------------------------------------------------

-- This version of the library has been tested using Agda 2.4.2.1.

-- Note that no guarantees are currently made about forwards or
-- backwards compatibility, the library is still at an experimental
-- stage.

-- To make use of the library, add the path to the library’s root
-- directory (src) to the Agda search path, either using the
-- --include-path flag or by customising the Emacs mode variable
-- agda2-include-dirs (M-x customize-group RET agda2 RET).

-- To compile the library using the MAlonzo compiler you first need to
-- install some supporting Haskell code, for instance as follows:
--
--   cd ffi
--   cabal install
--
-- Currently the library does not support the Epic or JavaScript
-- compiler backends.

-- Contributions to this library are welcome (but to avoid wasted work
-- it is suggested that you discuss large changes before implementing
-- them). Please send contributions in the form of git pull requests,
-- patch bundles or ask for commmit rights to the repository.  It is
-- appreciated if every patch contains a single, complete change, and
-- if the coding style used in the library is adhered to.

------------------------------------------------------------------------
-- Module hierarchy
------------------------------------------------------------------------

-- The top-level module names of the library are currently allocated
-- as follows:
--
-- • Algebra
--     Abstract algebra (monoids, groups, rings etc.), along with
--     properties needed to specify these structures (associativity,
--     commutativity, etc.), and operations on and proofs about the
--     structures.
-- • Category
--     Category theory-inspired idioms used to structure functional
--     programs (functors and monads, for instance).
-- • Coinduction
--     Support for coinduction.
-- • Data
--     Data types and properties about data types.
-- • Function
--     Combinators and properties related to functions.
-- • Foreign
--     Related to the foreign function interface.
-- • Induction
--     A general framework for induction (includes lexicographic and
--     well-founded induction).
-- • IO
--     Input/output-related functions.
-- • Irrelevance
--     Definitions related to (proscriptive) irrelevance.
-- • Level
--     Universe levels.
-- • Record
--     An encoding of record types with manifest fields and "with".
-- • Reflection
--     Support for reflection.
-- • Relation
--     Properties of and proofs about relations (mostly homogeneous
--     binary relations).
-- • Size
--     Sizes used by the sized types mechanism.
-- • Universe
--     A definition of universes.

------------------------------------------------------------------------
-- A selection of useful library modules
------------------------------------------------------------------------

-- Note that module names in source code are often hyperlinked to the
-- corresponding module. In the Emacs mode you can follow these
-- hyperlinks by typing M-. or clicking with the middle mouse button.

-- • Some data types

import Data.Bool     -- Booleans.
import Data.Char     -- Characters.
import Data.Empty    -- The empty type.
import Data.Fin      -- Finite sets.
import Data.List     -- Lists.
import Data.Maybe    -- The maybe type.
import Data.Nat      -- Natural numbers.
import Data.Product  -- Products.
import Data.Stream   -- Streams.
import Data.String   -- Strings.
import Data.Sum      -- Disjoint sums.
import Data.Unit     -- The unit type.
import Data.Vec      -- Fixed-length vectors.

-- • Some types used to structure computations

import Category.Functor      -- Functors.
import Category.Applicative  -- Applicative functors.
import Category.Monad        -- Monads.

-- • Equality

-- Propositional equality:
import Relation.Binary.PropositionalEquality

-- Convenient syntax for "equational reasoning" using a preorder:
import Relation.Binary.PreorderReasoning

-- Solver for commutative ring or semiring equalities:
import Algebra.RingSolver

-- • Properties of functions, sets and relations

-- Monoids, rings and similar algebraic structures:
import Algebra

-- Negation, decidability, and similar operations on sets:
import Relation.Nullary

-- Properties of homogeneous binary relations:
import Relation.Binary

-- • Induction

-- An abstraction of various forms of recursion/induction:
import Induction

-- Well-founded induction:
import Induction.WellFounded

-- Various forms of induction for natural numbers:
import Induction.Nat

-- • Support for coinduction

import Coinduction

-- • IO

import IO

------------------------------------------------------------------------
-- Record hierarchies
------------------------------------------------------------------------

-- When an abstract hierarchy of some sort (for instance semigroup →
-- monoid → group) is included in the library the basic approach is to
-- specify the properties of every concept in terms of a record
-- containing just properties, parameterised on the underlying
-- operations, sets etc.:
--
--   record IsSemigroup {A} (≈ : Rel A) (∙ : Op₂ A) : Set where
--     open FunctionProperties ≈
--     field
--       isEquivalence : IsEquivalence ≈
--       assoc         : Associative ∙
--       ∙-cong        : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
--
-- More specific concepts are then specified in terms of the simpler
-- ones:
--
--     record IsMonoid {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) : Set where
--       open FunctionProperties ≈
--       field
--         isSemigroup : IsSemigroup ≈ ∙
--         identity    : Identity ε ∙
--
--     open IsSemigroup isSemigroup public
--
-- Note here that open IsSemigroup isSemigroup public ensures that the
-- fields of the isSemigroup record can be accessed directly; this
-- technique enables the user of an IsMonoid record to use underlying
-- records without having to manually open an entire record hierarchy.
-- This is not always possible, though. Consider the following definition
-- of preorders:
--
--   record IsPreorder {A : Set}
--                     (_≈_ : Rel A) -- The underlying equality.
--                     (_∼_ : Rel A) -- The relation.
--                     : Set where
--     field
--       isEquivalence : IsEquivalence _≈_
--       -- Reflexivity is expressed in terms of an underlying equality:
--       reflexive     : _≈_ ⇒ _∼_
--       trans         : Transitive _∼_
--
--     module Eq = IsEquivalence isEquivalence
--
--     ...
--
-- The Eq module in IsPreorder is not opened publicly, because it
-- contains some fields which clash with fields or other definitions
-- in IsPreorder.

-- Records packing up properties with the corresponding operations,
-- sets, etc. are sometimes also defined:
--
--   record Semigroup : Set₁ where
--     infixl 7 _∙_
--     infix  4 _≈_
--     field
--       Carrier     : Set
--       _≈_         : Rel Carrier
--       _∙_         : Op₂ Carrier
--       isSemigroup : IsSemigroup _≈_ _∙_
--
--     open IsSemigroup isSemigroup public
--
--     setoid : Setoid
--     setoid = record { isEquivalence = isEquivalence }
--
--   record Monoid : Set₁ where
--     infixl 7 _∙_
--     infix  4 _≈_
--     field
--       Carrier  : Set
--       _≈_      : Rel Carrier
--       _∙_      : Op₂ Carrier
--       ε        : Carrier
--       isMonoid : IsMonoid _≈_ _∙_ ε
--
--     open IsMonoid isMonoid public
--
--     semigroup : Semigroup
--     semigroup = record { isSemigroup = isSemigroup }
--
--     open Semigroup semigroup public using (setoid)
--
-- Note that the Monoid record does not include a Semigroup field.
-- Instead the Monoid /module/ includes a "repackaging function"
-- semigroup which converts a Monoid to a Semigroup.

-- The above setup may seem a bit complicated, but we think it makes the
-- library quite easy to work with, while also providing enough
-- flexibility.

------------------------------------------------------------------------
-- More documentation
------------------------------------------------------------------------

-- Some examples showing where the natural numbers/integers and some
-- related operations and properties are defined, and how they can be
-- used:

import README.Nat
import README.Integer

-- Some examples showing how the AVL tree module can be used.

import README.AVL

-- An example showing how the Record module can be used.

import README.Record

-- An example showing how the case expression can be used.

import README.Case

------------------------------------------------------------------------
-- Core modules
------------------------------------------------------------------------

-- Some modules have names ending in ".Core". These modules are
-- internal, and have (mostly) been created to avoid mutual recursion
-- between modules. They should not be imported directly; their
-- contents are reexported by other modules.

------------------------------------------------------------------------
-- All library modules
------------------------------------------------------------------------

-- For short descriptions of every library module, see Everything:

import Everything

-- Note that the Everything module is generated automatically. If you
-- have downloaded the library from its Git repository and want to
-- type check README then you can (try to) construct Everything by
-- running "cabal install && GenerateEverything".

-- Note that all library sources are located under src or ffi. The
-- modules README, README.* and Everything are not really part of the
-- library, so these modules are located in the top-level directory
-- instead.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example use case for a fresh list: sorted list
------------------------------------------------------------------------

module README.Data.List.Fresh where

open import Data.Nat
open import Data.List.Base
open import Data.List.Fresh
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
open import Data.Product
open import Relation.Nary using (⌊_⌋; fromWitness)

-- A sorted list of natural numbers can be seen as a fresh list
-- where the notion of freshness is being smaller than all the
-- existing entries

SortedList : Set
SortedList = List# ℕ _<_

_ : SortedList
_ = cons 0 (cons 1 (cons 3 (cons 10 [] _)
      (s≤s (s≤s (s≤s (s≤s z≤n))) , _))
      (s≤s (s≤s z≤n) , s≤s (s≤s z≤n) , _))
      (s≤s z≤n , s≤s z≤n , s≤s z≤n , _)

-- Clearly, writing these by hand can pretty quickly become quite cumbersome
-- Luckily, if the notion of freshness we are using is decidable, we can
-- make most of the proofs inferrable by using the erasure of the relation
-- rather than the relation itself!

-- We call this new type *I*SortedList because all the proofs will be implicit.

ISortedList : Set
ISortedList = List# ℕ ⌊ _<?_ ⌋

-- The same example is now much shorter. It looks pretty much like a normal list
-- except that we know for sure that it is well ordered.

ins : ISortedList
ins = 0 ∷# 1 ∷# 3 ∷# 10 ∷# []

-- Indeed we can extract the support list together with a proof that it
-- is ordered thanks to the combined action of toList converting a fresh
-- list to a pair of a list and a proof and fromWitness which "unerases"
-- a proof.

ns : List ℕ
ns = proj₁ (toList ins)

sorted : AllPairs _<_ ns
sorted = AllPairs.map (fromWitness _<_ _<?_) (proj₂ (toList ins))

-- See the following module for an applied use-case of fresh lists
open import README.Data.Trie.NonDependent