text:
------------------------------------------------------------------------------
-- Propositional equality without using pattern matching on refl
------------------------------------------------------------------------------

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

module
  FOT.Common.FOL.Relation.Binary.PropositionalEquality.NoPatternMatchingOnRefl
  where

open import Common.FOL.FOL using ( D )

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

------------------------------------------------------------------------------
-- The identity type on the universe of discourse.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

-- Elimination rule.
subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
subst A refl Ax = Ax

-- Identity properties

sym : ∀ {x y} → x ≡ y → y ≡ x
sym {x} h = subst (λ y' → y' ≡ x) h refl

trans : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
trans {x} h₁ h₂ = subst (_≡_ x) h₂ h₁

trans₂ : ∀ {w x y z} → w ≡ x → x ≡ y → y ≡ z → w ≡ z
trans₂ h₁ h₂ h₃ = trans (trans h₁ h₂) h₃

subst₂ : (A : D → D → Set) → ∀ {x₁ x₂ y₁ y₂} →
         x₁ ≡ y₁ → x₂ ≡ y₂ →
         A x₁ x₂ →
         A y₁ y₂
subst₂ A {x₁} {x₂} {y₁} {y₂} h₁ h₂ h₃ =
  subst (λ y₁' → A y₁' y₂) h₁ (subst (A x₁) h₂ h₃)

cong : (f : D → D) → ∀ {x y} → x ≡ y → f x ≡ f y
cong f {x} h = subst (λ x' → f x ≡ f x') h refl

cong₂ : (f : D → D → D) → ∀ {x₁ x₂ y₁ y₂} → x₁ ≡ y₁ → x₂ ≡ y₂ →
        f x₁ x₂ ≡ f y₁ y₂
cong₂ f {x₁} {x₂} {y₁} {y₂} h₁ h₂ =
  subst (λ x₁' → f x₁ x₂ ≡ f x₁' y₂)
        h₁
        (subst (λ x₂' → f x₁ x₂ ≡ f x₁ x₂') h₂ refl)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2015-11-17, issue reported by Martin Stone Davis

module _ where

module Sub (let open import oops) where

-- WAS: internal error

-- EXPECTED: Not a valid let-declaration
--   when scope checking the declaration
--     module Sub (let open import oops) where

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Equality over lists parameterised by some setoid
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid)

module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where

open import Data.List.Base using (List)
open import Level
open import Relation.Binary renaming (Rel to Rel₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)

open Setoid S renaming (Carrier to A)

------------------------------------------------------------------------
-- Definition of equality

infix 4 _≋_

_≋_ : Rel₂ (List A) (a ⊔ ℓ)
_≋_ = Pointwise _≈_

open Pointwise public using ([]; _∷_)

------------------------------------------------------------------------
-- Relational properties

≋-refl : Reflexive _≋_
≋-refl = PW.refl refl

≋-reflexive : _≡_ ⇒ _≋_
≋-reflexive P.refl = ≋-refl

≋-sym : Symmetric _≋_
≋-sym = PW.symmetric sym

≋-trans : Transitive _≋_
≋-trans = PW.transitive trans

≋-isEquivalence : IsEquivalence _≋_
≋-isEquivalence = PW.isEquivalence isEquivalence

≋-setoid : Setoid _ _
≋-setoid = PW.setoid S

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

open PW public using
  ( tabulate⁺
  ; tabulate⁻
  ; ++⁺
  ; concat⁺
  )


text:
module plfa.part1.Midterm where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
-- you can add any import definitions that you need
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; _>_; z≤n; s≤s; _≤?_; _<?_; _^_)
open import Data.Nat.Properties using (+-assoc; +-suc; +-comm; *-comm)
open import Relation.Nullary using (yes; no; Dec)

-- used for rewrite
simplify : ∀ {A : Set} (x : A) → x ≡ x
simplify x = refl

sum : ℕ → ℕ
sum 0 = 0
sum n@(suc sn) = sum sn + n

-- Problem 1
-- remove the "postulate" and prove this theorem, which is a version of
--   sum n ≡ n * (n - 1) / 2

--- my solution from Induction HW, copied here instead of importing for ease of grading
*-distrib-+ : ∀ (m n p : ℕ) →  (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p =
  begin
    (zero + n) * p
  ≡⟨⟩
   n * p
  ≡⟨⟩
   zero + n * p
  ≡⟨⟩
   zero * p + n * p
  ∎
*-distrib-+ (suc m) n p =
  begin
    (suc m + n) * p
  ≡⟨⟩
   (suc (m + n)) * p
  ≡⟨⟩
   p + ((m + n) * p)
  ≡⟨ cong (λ x -> p + x) (*-distrib-+ m n p) ⟩
   p + (m * p + n * p)
  ≡⟨ sym (+-assoc p (m * p) (n * p))⟩
   (p + m * p) + n * p
  ≡⟨⟩
   suc m * p + n * p
  ∎

1-suc : ∀ ( n : ℕ )
  → n + 1 ≡ suc n
1-suc (zero) = refl
1-suc (suc n) =
  begin
    suc n + 1
  ≡⟨ (+-comm (suc n) 1) ⟩
    1 + suc n
  ≡⟨⟩
    suc ( 1 + n)
  ≡⟨ cong suc (+-comm 1 n) ⟩
    suc ( n + 1)
  ≡⟨ cong suc (1-suc n) ⟩
    suc ( suc n )
  ∎

simple : ∀ (n : ℕ) → (sum n) * 2 ≡ (suc n) * n
simple zero = refl
simple (suc n) =
  begin
    (sum (suc n)) * 2
  ≡⟨⟩
    ((sum n) + (suc n)) * 2
  ≡⟨ cong (λ x -> x) (*-distrib-+ (sum n) (suc n) 2 )⟩
    (sum n) * 2 + (suc n) * 2
  ≡⟨ cong (λ x -> x + (suc n) * 2) (simple (n))⟩
    (suc n) * n + (suc n) * 2
  ≡⟨ cong (λ x → x + (suc n) * 2) (*-comm (suc n) n)⟩
    n * (suc n) + (suc n) * 2
  ≡⟨ cong (λ x → n * (suc n) + x) (*-comm (suc n) 2)⟩
    n * (suc n) + 2 * (suc n)
  ≡⟨ cong (λ x → x) (sym (*-distrib-+ n 2 (suc n)))⟩
    (n + 2) * (suc n)
  ≡⟨⟩
    (n + suc 1) * (suc n)
  ≡⟨ cong (λ x → x * (suc n)) (+-suc n 1)⟩
    (suc (n + 1)) * (suc n)
  ≡⟨ cong (λ x → (suc (x)) * (suc n)) (1-suc n)⟩
    (suc (suc n)) * (suc n)
  ∎

-- Problem 2
-- remove the postulate and implement this function, which gives an Natural
-- number approximation of square root

if_then_else_ : { A : Set }
  → Dec A
  → ℕ
  → ℕ
  → ℕ
if yes A then a else b = a
if no A then a else b = b

sqrt : ℕ → ℕ

rt_sub_ : ℕ → ℕ → ℕ
rt_sub_ n  sqrtn = if ((suc n) <? (((sqrtn) + 1) ^ 2)) then (sqrtn) else ((sqrtn) + 1)

sqrt 0 = 0
sqrt (suc n) = rt n sub (sqrt n)

-- you can run these test cases
_ : sqrt 0 ≡ 0
_ = refl
_ : sqrt 1 ≡ 1
_ = refl
_ : sqrt 2 ≡ 1
_ = refl
_ : sqrt 3 ≡ 1
_ = refl
_ : sqrt 4 ≡ 2
_ = refl
_ : sqrt 5 ≡ 2
_ = refl
_ : sqrt 6 ≡ 2
_ = refl
_ : sqrt 7 ≡ 2
_ = refl
_ : sqrt 8 ≡ 2
_ = refl
_ : sqrt 9 ≡ 3
_ = refl
_ : sqrt 10 ≡ 3
_ = refl
_ : sqrt 11 ≡ 3
_ = refl
_ : sqrt 12 ≡ 3
_ = refl
_ : sqrt 13 ≡ 3
_ = refl
_ : sqrt 14 ≡ 3
_ = refl
_ : sqrt 15 ≡ 3
_ = refl
_ : sqrt 16 ≡ 4
_ = refl
_ : sqrt 17 ≡ 4
_ = refl
_ : sqrt 18 ≡ 4
_ = refl
_ : sqrt 19 ≡ 4
_ = refl
_ : sqrt 20 ≡ 4
_ = refl
_ : sqrt 21 ≡ 4
_ = refl
_ : sqrt 22 ≡ 4
_ = refl
_ : sqrt 23 ≡ 4
_ = refl
_ : sqrt 24 ≡ 4
_ = refl
_ : sqrt 24 ≡ 4
_ = refl
_ : sqrt 24 ≡ 4
_ = refl
_ : sqrt 25 ≡ 5
_ = refl
_ : sqrt 26 ≡ 5
_ = refl
_ : sqrt 27 ≡ 5
_ = refl

_ : sqrt 100 ≡ 10
_ = refl
_ : sqrt 101 ≡ 10
_ = refl


text:
-- Andreas, 2016-12-30, issue #1886, reported by nad
--
-- Change of parameter names is an error.
-- Reason: the parameter names become names of hidden arguments
-- in the constructors.  There should be no ambiguity.

data D (X : Set) : Set

data D (Y : Set) where
  c : Y → D Y

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text: module Categories.Object.Zero where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Loop where

{-
data _=>_ (A, B : Set) : Set where
  lam : (A -> B) -> A => B

app : {A, B : Set} -> (A => B) -> A -> B
app (lam f) = f

delta = lam (\x -> app x x)

loop = app delta delta
-}

lam : (A, B : Set) -> (A -> B) -> A -> B
lam A B f = f

app : (A, B : Set) -> (A -> B) -> A -> B
app A B f = f

postulate Nat : Set
	  zero : Nat

wrap : (F : Nat -> Set) -> F zero -> F zero
wrap F x = x

delta : (Nat -> Nat) -> Nat
delta = \x -> x (wrap _ x)

loop : Nat
loop = delta (wrap _ delta)

-- delta : _ -> _
-- delta = \x -> app _ _ x x -- lam _ _ (\x -> app _ _ x x)
--
-- loop = app _ _ delta (wrap _ delta)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------------
-- Properties of the divisibility relation
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Divisibility.NotBy0.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.PropertiesATP
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Divisibility.NotBy0
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.PropertiesATP

------------------------------------------------------------------------------
-- Any positive number divides 0.
postulate S∣0 : ∀ n → succ₁ n ∣ zero
{-# ATP prove S∣0 #-}

-- 0 doesn't divide any number.
postulate 0∤x : ∀ {n} → ¬ (zero ∣ n)
{-# ATP prove 0∤x #-}

-- The divisibility relation is reflexive for positive numbers.
--
-- For the proof using the ATPs we added the helper hypothesis
--
-- N (succ zero).
postulate ∣-refl-S-ah : ∀ {n} → N n → N (succ₁ zero) → succ₁ n ∣ succ₁ n
{-# ATP prove ∣-refl-S-ah *-leftIdentity #-}

∣-refl-S : ∀ {n} → N n → succ₁ n ∣ succ₁ n
∣-refl-S Nn = ∣-refl-S-ah Nn (nsucc nzero)

-- If x divides y and z then x divides y ∸ z.
postulate
  x∣y→x∣z→x∣y∸z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                         n ≡ k * succ₁ m →
                         o ≡ k' * succ₁ m →
                         n ∸ o ≡ (k ∸ k') * succ₁ m
{-# ATP prove x∣y→x∣z→x∣y∸z-helper *∸-leftDistributive #-}

x∣y→x∣z→x∣y∸z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n ∸ o
x∣y→x∣z→x∣y∸z nzero _ _ (0≢0 , _) m∣o = ⊥-elim (0≢0 refl)
x∣y→x∣z→x∣y∸z (nsucc Nm) Nn No
              (_ , k , Nk , h₁)
              (_ , k' , Nk' , h₂) =
  (λ S≡0 → ⊥-elim (S≢0 S≡0))
  , k ∸ k' , ∸-N Nk Nk' , x∣y→x∣z→x∣y∸z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and z then x divides y + z.
postulate
  x∣y→x∣z→x∣y+z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                         n ≡ k * succ₁ m →
                         o ≡ k' * succ₁ m →
                         n + o ≡ (k + k') * succ₁ m
{-# ATP prove x∣y→x∣z→x∣y+z-helper *+-leftDistributive #-}

x∣y→x∣z→x∣y+z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n + o
x∣y→x∣z→x∣y+z nzero      _  _ (0≢0 , _) m∣o = ⊥-elim (0≢0 refl)
x∣y→x∣z→x∣y+z (nsucc Nm) Nn No
              (_ , k , Nk , h₁)
              (_ , k' , Nk' , h₂) =
  (λ S≡0 → ⊥-elim (S≢0 S≡0))
  , k + k' , +-N Nk Nk' , x∣y→x∣z→x∣y+z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and y is positive, then x ≤ y.
postulate x∣S→x≤S-ah₁ : ∀ {m n} → succ₁ n ≡ zero * succ₁ m → ⊥
{-# ATP prove x∣S→x≤S-ah₁ #-}

-- Nice proof by the ATP.
postulate x∣S→x≤S-ah₂ : ∀ {m n o} → N m → N n → N o →
                        succ₁ n ≡ succ₁ o * succ₁ m →
                        succ₁ m ≤ succ₁ n
{-# ATP prove x∣S→x≤S-ah₂ x≤x+y *-N #-}

x∣S→x≤S : ∀ {m n} → N m → N n → m ∣ (succ₁ n) → m ≤ succ₁ n
x∣S→x≤S  nzero Nn (0≢0 , _) = ⊥-elim (0≢0 refl)
x∣S→x≤S (nsucc Nm) Nn (_ , .zero , nzero , Sn≡0*Sm) = ⊥-elim (x∣S→x≤S-ah₁ Sn≡0*Sm)
x∣S→x≤S (nsucc {m} Nm) Nn (_ , .(succ₁ k) , nsucc {k} Nk , Sn≡Sk*Sm) =
  x∣S→x≤S-ah₂ Nm Nn Nk Sn≡Sk*Sm


text:
------------------------------------------------------------------------
-- Unary and binary relations
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

module Relation where

open import Equality.Propositional
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decision-procedures equality-with-J
import Equality.Groupoid equality-with-J as EG
open import Function-universe equality-with-J hiding (id; _∘_)
open import Groupoid equality-with-J

-- Unary relations.

Rel : ∀ {ℓ₁} ℓ₂ → Type ℓ₁ → Type (ℓ₁ ⊔ lsuc ℓ₂)
Rel ℓ A = A → Type ℓ

-- Homogeneous binary relations.

Rel₂ : ∀ {ℓ₁} ℓ₂ → Type ℓ₁ → Type (ℓ₁ ⊔ lsuc ℓ₂)
Rel₂ ℓ A = Rel ℓ (A × A)

-- One kind of unary relation transformer.

Trans : ∀ {a} ℓ → Type a → Type (a ⊔ lsuc ℓ)
Trans ℓ A = Rel ℓ A → Rel ℓ A

-- One kind of binary relation transformer.

Trans₂ : ∀ {a} ℓ → Type a → Type (a ⊔ lsuc ℓ)
Trans₂ ℓ A = Trans ℓ (A × A)

-- The converse of a binary relation.

infixr 10 _⁻¹

_⁻¹ : ∀ {a ℓ} {A : Type a} → Rel₂ ℓ A → Rel₂ ℓ A
R ⁻¹ = R ∘ swap

-- Composition of binary relations.

infixr 9 _⊙_

_⊙_ : ∀ {a ℓ₁ ℓ₂} {A : Type a} →
      Rel₂ ℓ₁ A → Rel₂ ℓ₂ A → Rel₂ (a ⊔ ℓ₁ ⊔ ℓ₂) A
(R ⊙ S) (x , z) = ∃ λ y → R (x , y) × S (y , z)

-- Composition of a relation with itself, with the base case as a
-- parameter.

composition : ∀ {a} {A : Type a} →
              Rel₂ a A → Rel₂ a A → ℕ → Rel₂ a A
composition R S zero    = R
composition R S (suc n) = S ⊙ composition R S n

-- Composition of a binary relation with itself, with the relation
-- itself as the base case.

infix 10 _^^[1+_]

_^^[1+_] : ∀ {a} {A : Type a} →
           Rel₂ a A → ℕ → Rel₂ a A
R ^^[1+ n ] = composition R R n

-- Composition of a binary relation with itself, with equality as the
-- base case.

infix 10 _^^_

_^^_ : ∀ {a} {A : Type a} →
       Rel₂ a A → ℕ → Rel₂ a A
R ^^ n = composition (uncurry _≡_) R n

-- Intersection of relations.

infixr 8 _∩_

_∩_ : ∀ {a ℓ₁ ℓ₂} {A : Type a} →
      Rel ℓ₁ A → Rel ℓ₂ A → Rel (ℓ₁ ⊔ ℓ₂) A
R ∩ S = λ x → R x × S x

-- Union of relations.

infixr 7 _∪_

_∪_ : ∀ {a ℓ₁ ℓ₂} {A : Type a} →
      Rel ℓ₁ A → Rel ℓ₂ A → Rel (ℓ₁ ⊔ ℓ₂) A
R ∪ S = λ x → R x ⊎ S x

-- Reflexive closure of binary relations.

_⁼ : ∀ {a ℓ} {A : Type a} →
     Rel₂ ℓ A → Rel₂ (a ⊔ ℓ) A
R ⁼ = R ∪ uncurry _≡_

-- Transitive closure of binary relations.

_⁺ : ∀ {a} {A : Type a} →
     Rel₂ a A → Rel₂ a A
(R ⁺) x = ∃ λ n → (R ^^[1+ n ]) x

-- Reflexive transitive closure of binary relations.

_* : ∀ {a} {A : Type a} →
     Rel₂ a A → Rel₂ a A
(R *) x = ∃ λ n → (R ^^ n) x

-- Repeated composition of a function with itself.

infix 10 _^[_]_

_^[_]_ : ∀ {a} {A : Type a} → (A → A) → ℕ → A → A
f ^[ zero  ] x = x
f ^[ suc n ] x = f (f ^[ n ] x)

-- Unions of families of relation transformers.

⋃ : ∀ {a b} ℓ {A : Type a} {B : Type b} →
    (A → Trans (a ⊔ ℓ) B) → Trans (a ⊔ ℓ) B
⋃ _ F R = λ b → ∃ λ a → F a R b

-- An analogue of ⋃ₙ Fⁿ.

infix 10 _^ω_

_^ω_ : ∀ {a ℓ} {A : Type a} → Trans ℓ A → Trans ℓ A
_^ω_ F = ⋃ _ (F ^[_]_)

-- Relation containment.

infix 4 _⊆_

_⊆_ : ∀ {a ℓ₁ ℓ₂} {A : Type a} →
      Rel ℓ₁ A → Rel ℓ₂ A → Type (a ⊔ ℓ₁ ⊔ ℓ₂)
R ⊆ S = ∀ {x} → R x → S x

-- "Equational" reasoning combinators.

infix  -1 finally-⊆
infixr -2 _⊆⟨_⟩_ _⊆⟨⟩_

_⊆⟨_⟩_ : ∀ {a p q r} {A : Type a}
         (P : Rel p A) {Q : Rel q A} {R : Rel r A} →
         P ⊆ Q → Q ⊆ R → P ⊆ R
_ ⊆⟨ P⊆Q ⟩ Q⊆R = Q⊆R ∘ P⊆Q

_⊆⟨⟩_ : ∀ {a p q} {A : Type a}
        (P : Rel p A) {Q : Rel q A} →
        P ⊆ Q → P ⊆ Q
_ ⊆⟨⟩ P⊆Q = P⊆Q

finally-⊆ : ∀ {a p q} {A : Type a}
            (P : Rel p A) (Q : Rel q A) →
            P ⊆ Q → P ⊆ Q
finally-⊆ _ _ P⊆Q = P⊆Q

syntax finally-⊆ P Q P⊆Q = P ⊆⟨ P⊆Q ⟩∎ Q ∎

-- Preservation lemmas for _⊆_.

infix 4 _⊆-cong-→_

⊆-cong :
  ∀ {k a r₁ r₂ s₁ s₂} {A : Type a}
    {R₁ : Rel r₁ A} {S₁ : Rel s₁ A}
    {R₂ : Rel r₂ A} {S₂ : Rel s₂ A} →
  Extensionality? ⌊ k ⌋-sym (a ⊔ r₁ ⊔ r₂) (r₁ ⊔ r₂ ⊔ s₁ ⊔ s₂) →
  (∀ {x} → R₁ x ↝[ ⌊ k ⌋-sym ] R₂ x) →
  (∀ {x} → S₁ x ↝[ ⌊ k ⌋-sym ] S₂ x) →
  R₁ ⊆ S₁ ↝[ ⌊ k ⌋-sym ] R₂ ⊆ S₂
⊆-cong {k} {a} {r₁} {r₂} ext R₁↝R₂ S₁↝S₂ =
  implicit-∀-cong
    (lower-extensionality? ⌊ k ⌋-sym (r₁ ⊔ r₂) lzero ext) $
  →-cong (lower-extensionality? ⌊ k ⌋-sym a (r₁ ⊔ r₂) ext)
         R₁↝R₂ S₁↝S₂

_⊆-cong-→_ :
  ∀ {a r₁ r₂ s₁ s₂} {A : Type a}
    {R₁ : Rel r₁ A} {S₁ : Rel s₁ A}
    {R₂ : Rel r₂ A} {S₂ : Rel s₂ A} →
  R₂ ⊆ R₁ → S₁ ⊆ S₂ → R₁ ⊆ S₁ → R₂ ⊆ S₂
R₂→R₁ ⊆-cong-→ S₁→S₂ = implicit-∀-cong _ $ →-cong-→ R₂→R₁ S₁→S₂

⊆-congʳ :
  ∀ {k a r s₁ s₂} {A : Type a}
    {R : Rel r A} {S₁ : Rel s₁ A} {S₂ : Rel s₂ A} →
  Extensionality? k (a ⊔ r) (r ⊔ s₁ ⊔ s₂) →
  (∀ {x} → S₁ x ↝[ k ] S₂ x) →
  R ⊆ S₁ ↝[ k ] R ⊆ S₂
⊆-congʳ {k} {a} {r} ext S₁↝S₂ =
  implicit-∀-cong (lower-extensionality? k r lzero ext) $
  ∀-cong (lower-extensionality? k a r ext) λ _ →
  S₁↝S₂

-- Relation containment (_⊆_) is not antisymmetric (with respect to
-- propositional equality) if the index type is inhabited.

⊆-not-antisymmetric :
  ∀ {ℓ x} {X : Type x} →
  X →
  ¬ ({R S : Rel ℓ X} → R ⊆ S → S ⊆ R → R ≡ S)
⊆-not-antisymmetric {ℓ} {X = X} x antisym = Bool.true≢false true≡false
  where
  R S : Rel ℓ X
  R = λ _ → ↑ _ ⊤
  S = λ _ → ↑ _ Bool

  R≡S : R ≡ S
  R≡S = antisym (λ _ → lift true) _

  ⊤≡Bool : ↑ _ ⊤ ≡ ↑ _ Bool
  ⊤≡Bool = cong (_$ x) R≡S

  ⊤↔Bool : ⊤ ↔ Bool
  ⊤↔Bool =
    ⊤         ↝⟨ inverse Bijection.↑↔ ⟩
    ↑ _ ⊤     ↝⟨ ≡⇒↝ _ ⊤≡Bool ⟩
    ↑ _ Bool  ↝⟨ Bijection.↑↔ ⟩□
    Bool      □

  true≡false : true ≡ false
  true≡false =
    true                                   ≡⟨ sym $ _↔_.right-inverse-of ⊤↔Bool _ ⟩
    _↔_.to ⊤↔Bool (_↔_.from ⊤↔Bool true)   ≡⟨⟩
    _↔_.to ⊤↔Bool tt                       ≡⟨⟩
    _↔_.to ⊤↔Bool (_↔_.from ⊤↔Bool false)  ≡⟨ _↔_.right-inverse-of ⊤↔Bool _ ⟩∎
    false                                  ∎

-- Monotonicity of relation transformers.

Monotone :
  ∀ {a ℓ} {A : Type a} →
  Trans ℓ A → Type (a ⊔ lsuc ℓ)
Monotone F = ∀ {R S} → R ⊆ S → F R ⊆ F S

-- A relation transformer is extensive if the input is always
-- contained in the output.

Extensive : ∀ {ℓ} {I : Type ℓ} → Trans ℓ I → Type (lsuc ℓ)
Extensive G = ∀ R → R ⊆ G R

-- A definition that turns into a notion of symmetry if the first
-- argument is instantiated with the swap function. In that case this
-- definition is similar to one of those given by Pous and Sangiorgi
-- in Section 6.3.4.1 of "Enhancements of the bisimulation proof
-- method".

Symmetric : ∀ {ℓ} {I : Type ℓ} → (I → I) → Trans ℓ I → Type (lsuc ℓ)
Symmetric f F = ∀ R → F (R ∘ f) ⊆ F R ∘ f

-- If f is an involution, then the inclusion in Symmetric f F holds
-- also in the other direction.

involution→other-symmetry :
  ∀ {ℓ} {I : Type ℓ} (F : Trans ℓ I) {f : I → I} →
  f ∘ f ≡ id → Symmetric f F → ∀ R → F R ∘ f ⊆ F (R ∘ f)
involution→other-symmetry F {f} inv symm R =
  F R ∘ f            ⊆⟨ (λ {x} → subst (λ g → F (R ∘ g) (f x)) (sym inv)) ⟩
  F (R ∘ f ∘ f) ∘ f  ⊆⟨ symm _ ⟩
  F (R ∘ f) ∘ f ∘ f  ⊆⟨ (λ {x} → subst (λ g → F (R ∘ f) (g x)) inv) ⟩∎
  F (R ∘ f)          ∎

-- Composition is associative.

⊙-assoc : ∀ {a ℓ₁ ℓ₂ ℓ₃} {A : Type a} →
          (R₁ : Rel₂ ℓ₁ A) {R₂ : Rel₂ ℓ₂ A} (R₃ : Rel₂ ℓ₃ A) →
          ∀ p → (R₁ ⊙ (R₂ ⊙ R₃)) p ↔ ((R₁ ⊙ R₂) ⊙ R₃) p
⊙-assoc R₁ {R₂} R₃ (a , d) =
  (∃ λ b → R₁ (a , b) × ∃ λ c → R₂ (b , c) × R₃ (c , d))    ↝⟨ ∃-cong (λ _ → ∃-comm) ⟩
  (∃ λ b → ∃ λ c → R₁ (a , b) × R₂ (b , c) × R₃ (c , d))    ↝⟨ ∃-comm ⟩
  (∃ λ c → ∃ λ b → R₁ (a , b) × R₂ (b , c) × R₃ (c , d))    ↝⟨ ∃-cong (λ _ → ∃-cong λ _ → Σ-assoc) ⟩
  (∃ λ c → ∃ λ b → (R₁ (a , b) × R₂ (b , c)) × R₃ (c , d))  ↝⟨ ∃-cong (λ _ → Σ-assoc) ⟩□
  (∃ λ c → (∃ λ b → R₁ (a , b) × R₂ (b , c)) × R₃ (c , d))  □

-- Several forms of composition preserve several kinds of functions.

⊙-cong :
  ∀ {k a r₁ r₂ s₁ s₂} {A : Type a} →
    {R₁ : Rel₂ r₁ A} {R₂ : Rel₂ r₂ A} →
    {S₁ : Rel₂ s₁ A} {S₂ : Rel₂ s₂ A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  (∀ p → S₁ p ↝[ k ] S₂ p) →
  ∀ p → (R₁ ⊙ S₁) p ↝[ k ] (R₂ ⊙ S₂) p
⊙-cong {R₁ = R₁} {R₂} {S₁} {S₂} R₁↝R₂ S₁↝S₂ (x , z) =
  (∃ λ y → R₁ (x , y) × S₁ (y , z))  ↝⟨ ∃-cong (λ _ → R₁↝R₂ _ ×-cong S₁↝S₂ _) ⟩□
  (∃ λ y → R₂ (x , y) × S₂ (y , z))  □

composition-cong :
  ∀ {k a} {A : Type a} {R₁ R₂ S₁ S₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  (∀ p → S₁ p ↝[ k ] S₂ p) →
  ∀ n p → composition R₁ S₁ n p ↝[ k ] composition R₂ S₂ n p
composition-cong R₁↝R₂ S₁↝S₂ = λ where
  zero    → R₁↝R₂
  (suc n) → ⊙-cong S₁↝S₂ (composition-cong R₁↝R₂ S₁↝S₂ n)

^^[1+]-cong :
  ∀ {k a} {A : Type a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ n p → (R₁ ^^[1+ n ]) p ↝[ k ] (R₂ ^^[1+ n ]) p
^^[1+]-cong R₁↝R₂ = composition-cong R₁↝R₂ R₁↝R₂

^^-cong :
  ∀ {k a} {A : Type a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ n p → (R₁ ^^ n) p ↝[ k ] (R₂ ^^ n) p
^^-cong R₁↝R₂ = composition-cong (λ _ → _ □) R₁↝R₂

⁺-cong :
  ∀ {k a} {A : Type a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ p → (R₁ ⁺) p ↝[ k ] (R₂ ⁺) p
⁺-cong R₁↝R₂ p = ∃-cong λ n → ^^[1+]-cong R₁↝R₂ n p

*-cong :
  ∀ {k a} {A : Type a} {R₁ R₂ : Rel₂ a A} →
  (∀ p → R₁ p ↝[ k ] R₂ p) →
  ∀ p → (R₁ *) p ↝[ k ] (R₂ *) p
*-cong R₁↝R₂ p = ∃-cong λ n → ^^-cong R₁↝R₂ n p

-- Two lemmas relating composition and _⊙_.

composition-⊙-comm :
  ∀ {k a} {A : Type a} {R S : Rel₂ a A} →
  (∀ p → (R ⊙ S) p ↝[ k ] (S ⊙ R) p) →
  ∀ n p → (composition R S n ⊙ S) p ↝[ k ] (S ⊙ composition R S n) p
composition-⊙-comm             hyp zero    = hyp
composition-⊙-comm {R = R} {S} hyp (suc n) = λ p →
  ((S ⊙ composition R S n) ⊙ S) p  ↔⟨ inverse $ ⊙-assoc S S _ ⟩
  (S ⊙ (composition R S n ⊙ S)) p  ↝⟨ ⊙-cong (λ p → S p □) (composition-⊙-comm hyp n) _ ⟩□
  (S ⊙ (S ⊙ composition R S n)) p  □

composition⊙composition :
  ∀ {k a} {A : Type a} {R S : Rel₂ a A} m n₁ {n₂} →
  (∀ p → (R ⊙ composition R S n₁) p ↝[ k ] composition R S n₂ p) →
  ∀ p → (composition R S m ⊙ composition R S n₁) p ↝[ k ]
        composition R S (m + n₂) p
composition⊙composition {R = R} {S} = λ where
  zero n₁ {n₂} hyp p →
    (R ⊙ composition R S n₁) p  ↝⟨ hyp _ ⟩
    composition R S n₂ p        □
  (suc m) n₁ {n₂} hyp p →
    ((S ⊙ composition R S m) ⊙ composition R S n₁) p  ↔⟨ inverse $ ⊙-assoc S (composition R S n₁) _ ⟩
    (S ⊙ (composition R S m ⊙ composition R S n₁)) p  ↝⟨ ⊙-cong (λ p → S p □) (composition⊙composition m n₁ hyp) _ ⟩□
    (S ⊙ composition R S (m + n₂)) p            □

-- The transitive closure is transitive.

⁺-trans : ∀ {a} {A : Type a} {R : Rel₂ a A} {x y z} →
          (R ⁺) (x , y) → (R ⁺) (y , z) → (R ⁺) (x , z)
⁺-trans (m , xR¹⁺ᵐy) (n , yR¹⁺ⁿz) =
    m + suc n
  , composition⊙composition m n (λ _ → id) _ (_ , xR¹⁺ᵐy , yR¹⁺ⁿz)

-- The reflexive transitive closure is transitive.

*-trans : ∀ {a} {A : Type a} {R : Rel₂ a A} {x y z} →
          (R *) (x , y) → (R *) (y , z) → (R *) (x , z)
*-trans {R = R} (m , xRᵐy) (n , yRⁿz) =
  m + n , composition⊙composition m n lemma _ (_ , xRᵐy , yRⁿz)
  where
  lemma : ∀ p → (uncurry _≡_ ⊙ (R ^^ n)) p → (R ^^ n) p
  lemma _ (_ , refl , r) = r

-- Lemmas relating different forms of composition and swap.

⊙-swap :
  ∀ {k a r s} {A : Type a} {R : Rel₂ r A} {S : Rel₂ s A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  (∀ p → S p ↝[ k ] S (swap p)) →
  ∀ p → (R ⊙ S) p ↝[ k ] (S ⊙ R) (swap p)
⊙-swap {R = R} {S} R↝ S↝ (x , z) =
  (∃ λ y → R (x , y) × S (y , z))  ↝⟨ ∃-cong (λ _ → R↝ _ ×-cong S↝ _) ⟩
  (∃ λ y → R (y , x) × S (z , y))  ↔⟨ ∃-cong (λ _ → ×-comm) ⟩□
  (∃ λ y → S (z , y) × R (y , x))  □

composition-swap :
  ∀ {k a} {A : Type a} {R S : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  (∀ p → S p ↝[ k ] S (swap p)) →
  (∀ p → (R ⊙ S) p ↝[ k ] (S ⊙ R) p) →
  ∀ n p → composition R S n p ↝[ k ] composition R S n (swap p)
composition-swap {R = R} {S} R↝ S↝ hyp = λ where
  zero    p → R p         ↝⟨ R↝ _ ⟩□
              R (swap p)  □
  (suc n) p → (S ⊙ composition R S n) p         ↝⟨ ⊙-swap S↝ (composition-swap R↝ S↝ hyp n) _ ⟩
              (composition R S n ⊙ S) (swap p)  ↝⟨ composition-⊙-comm hyp n _ ⟩□
              (S ⊙ composition R S n) (swap p)  □

^^[1+]-swap :
  ∀ {k a} {A : Type a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ n p → (R ^^[1+ n ]) p ↝[ k ] (R ^^[1+ n ]) (swap p)
^^[1+]-swap R↝ = composition-swap R↝ R↝ (λ _ → _ □)

^^-swap :
  ∀ {k a} {A : Type a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ n p → (R ^^ n) p ↝[ k ] (R ^^ n) (swap p)
^^-swap {R = R} R↝ = composition-swap lemma₁ R↝ lemma₂
  where
  lemma₁ = λ { (x , y) →
    x ≡ y  ↔⟨ Groupoid.⁻¹-bijection (EG.groupoid _) ⟩□
    y ≡ x  □ }

  lemma₂ = λ { (x , z) →
    (∃ λ y → x ≡ y × R (y , z))  ↔⟨ ∃-cong (λ _ → ×-comm) ⟩
    (∃ λ y → R (y , z) × x ≡ y)  ↝⟨ ∃-cong (λ _ → ∃-cong λ _ → lemma₁ _) ⟩
    (∃ λ y → R (y , z) × y ≡ x)  ↔⟨ inverse $ ∃-intro _ _ ⟩
    R (x , z)                    ↔⟨ ∃-intro _ _ ⟩□
    (∃ λ y → R (x , y) × y ≡ z)  □}

⁺-swap :
  ∀ {k a} {A : Type a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ p → (R ⁺) p ↝[ k ] (R ⁺) (swap p)
⁺-swap {R = R} R↝ p =
  (R ⁺) p                           ↔⟨⟩
  (∃ λ n → (R ^^[1+ n ]) p)         ↝⟨ ∃-cong (λ n → ^^[1+]-swap R↝ n _) ⟩
  (∃ λ n → (R ^^[1+ n ]) (swap p))  ↔⟨⟩
  (R ⁺) (swap p)                    □

*-swap :
  ∀ {k a} {A : Type a} {R : Rel₂ a A} →
  (∀ p → R p ↝[ k ] R (swap p)) →
  ∀ p → (R *) p ↝[ k ] (R *) (swap p)
*-swap {R = R} R↝ p =
  (R *) p                      ↔⟨⟩
  (∃ λ n → (R ^^ n) p)         ↝⟨ ∃-cong (λ n → ^^-swap R↝ n _) ⟩
  (∃ λ n → (R ^^ n) (swap p))  ↔⟨⟩
  (R *) (swap p)               □

-- ⋃ constructs least upper bounds.

⊆-⋃ : ∀ {a b ℓ} {A : Type a} {B : Type b}
      (F : A → Trans (a ⊔ ℓ) B) a →
      ∀ R → F a R ⊆ ⋃ ℓ F R
⊆-⋃ {ℓ = ℓ} F a R =
  F a R                    ⊆⟨ a ,_ ⟩
  (λ x → ∃ λ a → F a R x)  ⊆⟨ id ⟩∎
  ⋃ ℓ F R                  ∎

⋃-⊆ : ∀ {a b ℓ} {A : Type a} {B : Type b}
      (F : A → Trans (a ⊔ ℓ) B) (G : Trans (a ⊔ ℓ) B) →
      (∀ {a} R → F a R ⊆ G R) →
      ∀ R → ⋃ ℓ F R ⊆ G R
⋃-⊆ {ℓ = ℓ} F G hyp R =
  ⋃ ℓ F R                  ⊆⟨⟩
  (λ x → ∃ λ a → F a R x)  ⊆⟨ hyp _ ∘ proj₂ ⟩∎
  G R                      ∎

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
{-# OPTIONS --universe-polymorphism #-}

module LevelWithBug where

open import Common.Level

postulate
  take : ∀ a → Set a → Set
  a : Level
  A : Set a
  Goal : Set → Set
  goal : ∀ X → Goal X

-- The meta got solved by Level (Max [Plus 0 (NeutralLevel a)]) which
-- didn't match the argument in the with expression which is simply a.
-- Now the level noise should go away when it's not useful.
foo : Goal (take _ A)
foo with take a A
... | z = goal z

-- Here's another more complicated one.

data List {a}(A : Set a) : Set a where
  [] : List A
  _∷_ : A → List A → List A

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

-- Sums commute with Any (for a fixed list).

data Any {a p} {A : Set a}
         (P : A → Set p) : List A → Set (a ⊔ p) where
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

amap : ∀ {a p q} {A : Set a} {P : A → Set p} → {Q : A → Set q} →
      (∀ {x} → P x → Q x) → ∀ {xs} → Any P xs → Any Q xs
amap g (there pxs) = there (amap g pxs)

data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : (x : A) → A + B
  inr : (y : B) → A + B

smap : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
      (A → C) → (B → D) → (A + B → C + D)
smap f g (inl x) = inl (f x)
smap f g (inr y) = inr (g y)

postulate
  p q : Level
  P : A → Set p
  Q : A → Set q

to : ∀ xs → Any P xs + Any Q xs → Any (λ x → P x + Q x) xs
to xs (inl pxs) = amap inl pxs
to xs (inr pxs) = amap inr pxs

from : ∀ xs → Any (λ x → P x + Q x) xs → Any P xs + Any Q xs
from ._ (there p) = smap there there (from _ p)

-- Here the abstraction didn't work because a NeutralLevel was replaced
-- by an UnreducedLevel during abstraction.
fromto : ∀ xs (p : Any P xs + Any Q xs) → from xs (to xs p) ≡ p
fromto .(x ∷ xs) (inl (there {x}{xs} p)) rewrite fromto xs (inl p) = refl
fromto .(x ∷ xs) (inr (there {x}{xs} q)) rewrite fromto xs (inr q) = refl

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Structure.Operator.Ring.Rings where

import      Lvl
open import Structure.Operator.Ring
open import Structure.Setoid
open import Type
open import Type.Properties.Singleton

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

postulate trivialRing : ∀{_+_ _⋅_ : U → U → U} → ⦃ equiv : Equiv{ℓₑ}(U) ⦄ ⦃ singleton : IsUnit(U) ⦄ → Ring(_+_)(_⋅_)
{-Ring.[+]-commutative-group  trivialRing = {!!}
Ring.[⋅]-binary-operator    trivialRing = {!!}
Ring.[⋅]-associativity      trivialRing = {!!}
Ring.[⋅][+]-distributivityₗ trivialRing = {!!}
Ring.[⋅][+]-distributivityᵣ trivialRing = {!!}
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Bool.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Bool.Base
open import Cubical.Data.Empty

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

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

notIsEquiv : isEquiv not
notIsEquiv = isoToIsEquiv (iso not not notnot notnot)

notEquiv : Bool ≃ Bool
notEquiv = (not , notIsEquiv)

notEq : Bool ≡ Bool
notEq = ua notEquiv

private
  -- This computes to false as expected
  nfalse : Bool
  nfalse = transp (λ i → notEq i) i0 true

  -- Sanity check
  nfalsepath : nfalse ≡ false
  nfalsepath = refl

isSetBool : isSet Bool
isSetBool = Discrete→isSet _≟_

true≢false : ¬ true ≡ false
true≢false p = subst (λ b → if b then Bool else ⊥) p true

false≢true : ¬ false ≡ true
false≢true p = subst (λ b → if b then ⊥ else Bool) p true

not≢const : ∀ x → ¬ not x ≡ x
not≢const false = true≢false
not≢const true  = false≢true

zeroˡ : ∀ x → true or x ≡ true
zeroˡ false = refl
zeroˡ true  = refl

zeroʳ : ∀ x → x or true ≡ true
zeroʳ false = refl
zeroʳ true  = refl

or-identityˡ : ∀ x → false or x ≡ x
or-identityˡ false = refl
or-identityˡ true  = refl

or-identityʳ : ∀ x → x or false ≡ x
or-identityʳ false = refl
or-identityʳ true  = refl

or-comm      : ∀ x y → x or y ≡ y or x
or-comm false y =
  false or y ≡⟨ or-identityˡ y ⟩
  y          ≡⟨ sym (or-identityʳ y) ⟩
  y or false ∎
or-comm true y =
  true or y ≡⟨ zeroˡ y ⟩
  true      ≡⟨ sym (zeroʳ y) ⟩
  y or true ∎

or-assoc     : ∀ x y z → x or (y or z) ≡ (x or y) or z
or-assoc false y z =
  false or (y or z)   ≡⟨ or-identityˡ _ ⟩
  y or z              ≡[ i ]⟨ or-identityˡ y (~ i) or z ⟩
  ((false or y) or z) ∎
or-assoc true y z  =
 true or (y or z)  ≡⟨ zeroˡ _ ⟩
  true             ≡⟨ sym (zeroˡ _) ⟩
  true or z        ≡[ i ]⟨ zeroˡ y (~ i) or z ⟩
  (true or y) or z ∎

or-idem      : ∀ x → x or x ≡ x
or-idem false = refl
or-idem true  = refl

⊕-comm : ∀ x y → x ⊕ y ≡ y ⊕ x
⊕-comm false false = refl
⊕-comm false true  = refl
⊕-comm true  false = refl
⊕-comm true  true  = refl

⊕-assoc : ∀ x y z → x ⊕ (y ⊕ z) ≡ (x ⊕ y) ⊕ z
⊕-assoc false y z = refl
⊕-assoc true false z = refl
⊕-assoc true true z = notnot z

not-⊕ˡ : ∀ x y → not (x ⊕ y) ≡ not x ⊕ y
not-⊕ˡ false y = refl
not-⊕ˡ true  y = notnot y

⊕-invol : ∀ x y → x ⊕ (x ⊕ y) ≡ y
⊕-invol false x = refl
⊕-invol true  x = notnot x

isEquiv-⊕ : ∀ x → isEquiv (x ⊕_)
isEquiv-⊕ x = isoToIsEquiv (iso _ (x ⊕_) (⊕-invol x) (⊕-invol x))

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Theorems of ∧ connective.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Conjunction ( n : ℕ ) where

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

open import Data.PropFormula.Syntax n
open import Data.PropFormula.Theorems.Classical n

open import Function using ( _$_ ; _∘_  )

-------------------------------------------------------------------------- ∎

-- Theorem.
∧-assoc₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ∧ (ψ ∧ γ)
  → Γ ⊢ (φ ∧ ψ) ∧ γ

-- Proof.
∧-assoc₁ Γ⊢φ∧ψ∧γ =
  ∧-intro
    (∧-intro
      (∧-proj₁  Γ⊢φ∧ψ∧γ)
      ((∧-proj₁ ∘ ∧-proj₂) Γ⊢φ∧ψ∧γ))
    ((∧-proj₂ ∘ ∧-proj₂) Γ⊢φ∧ψ∧γ)

-------------------------------------------------------------------------- ∎

-- Theorem.
∧-assoc₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∧ ψ) ∧ γ
  → Γ ⊢ φ ∧ (ψ ∧ γ)

-- Proof.
∧-assoc₂ Γ⊢φ∧ψ∧γ =
  ∧-intro
    (∧-proj₁ (∧-proj₁ Γ⊢φ∧ψ∧γ))
    (∧-intro
      (∧-proj₂ (∧-proj₁ Γ⊢φ∧ψ∧γ))
      (∧-proj₂ Γ⊢φ∧ψ∧γ))
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-assoc
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∧ (ψ ∧ γ)) ⇔ ((φ ∧ ψ) ∧ γ)

-- Proof.
∧-assoc {Γ} {φ}{ψ}{γ} =
  ⇔-intro
    (∧-assoc₁ (assume (φ ∧ (ψ ∧ γ))))
    (∧-assoc₂ (assume (φ ∧ ψ ∧ γ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-comm
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ∧ ψ
  → Γ ⊢ ψ ∧ φ

-- Proof.
∧-comm Γ⊢φ∧ψ =
  ∧-intro
    (∧-proj₂ Γ⊢φ∧ψ)
    (∧-proj₁ Γ⊢φ∧ψ)
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-dist₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ∧ (ψ ∨ γ)
  → Γ ⊢ (φ ∧ ψ) ∨ (φ ∧ γ)

-- Proof.
∧-dist₁ {φ = φ}{ψ}{γ} Γ⊢φ∧ψ∨γ =
  ⊃-elim
    (⊃-intro $
      ∨-elim
        (∨-intro₁ (φ ∧ γ)
          (∧-intro
            (weaken ψ (∧-proj₁ Γ⊢φ∧ψ∨γ))
            (assume  ψ)))
        (∨-intro₂ (φ ∧ ψ)
          (∧-intro
            (weaken γ  (∧-proj₁ Γ⊢φ∧ψ∨γ))
            (assume  γ))))
    (∧-proj₂ Γ⊢φ∧ψ∨γ)
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-dist₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∧ ψ) ∨ (φ ∧ γ)
  → Γ ⊢ φ ∧ (ψ ∨ γ)

-- Proof.
∧-dist₂ {φ = φ}{ψ}{γ} =
  ⊃-elim
    (⊃-intro
      (∨-elim
        (∧-intro
          (∧-proj₁
            (assume (φ ∧ ψ)))
          (∨-intro₁ γ
            (∧-proj₂
              (assume (φ ∧ ψ)))))
        (∧-intro
          (∧-proj₁
            (assume (φ ∧ γ)))
          (∨-intro₂ ψ
            (∧-proj₂
              (assume (φ ∧ γ)))))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-dist
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ∧ (ψ ∨ γ) ⇔ (φ ∧ ψ) ∨ (φ ∧ γ)

-- Proof.
∧-dist {φ = φ}{ψ}{γ} =
  ⇔-intro
    (∧-dist₁ (assume (φ ∧ (ψ ∨ γ))))
    (∧-dist₂ (assume (φ ∧ ψ ∨ (φ ∧ γ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-dmorgan₁
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ (φ ∧ ψ)
  → Γ ⊢ ¬ φ ∨ ¬ ψ
¬∧-to-¬∨¬ = ∧-dmorgan₁

-- Proof.
∧-dmorgan₁ {Γ}{φ}{ψ} =
  ⊃-elim $
    ⊃-intro $
      RAA $
        ¬-elim
          (weaken (¬ (¬ φ ∨ ¬ ψ)) $
            assume $ ¬ (φ ∧ ψ))
          (∧-intro
            (RAA
              (¬-elim
                (weaken (¬ φ) $
                  assume {Γ = Γ , ¬ (φ ∧ ψ)} $ ¬ (¬ φ ∨ ¬ ψ))
                (∨-intro₁ (¬ ψ)
                  (assume {Γ = Γ , ¬ (φ ∧ ψ) , ¬ (¬ φ ∨ ¬ ψ)} $ ¬ φ))))
            (RAA
              (¬-elim {Γ = Γ , ¬ (φ ∧ ψ) , ¬ (¬ φ ∨ ¬ ψ) , ¬ ψ}
                (weaken (¬ ψ) $
                  assume {Γ = Γ , ¬ (φ ∧ ψ)} $ ¬ (¬ φ ∨ ¬ ψ))
                (∨-intro₂ (¬ φ)
                  (assume {Γ = Γ , ¬ (φ ∧ ψ) , ¬ (¬ φ ∨ ¬ ψ)} $ ¬ ψ )))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-dmorgan₂
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ φ ∨ ¬ ψ
  → Γ ⊢ ¬ (φ ∧ ψ)
¬∨¬-to-¬∧ = ∧-dmorgan₂

-- Proof.
∧-dmorgan₂ {Γ}{φ}{ψ} =
  ⊃-elim $
    ⊃-intro $
      ∨-elim {Γ = Γ}
        (¬-intro $
          ¬-elim
            (weaken (φ ∧ ψ) $
              assume (¬ φ))
            (∧-proj₁ $
              assume {Γ = Γ , ¬ φ} (φ ∧ ψ)))
        (¬-intro $
          ¬-elim
            (weaken (φ ∧ ψ) $ assume (¬ ψ))
          (∧-proj₂ $
            assume {Γ = Γ , ¬ ψ} (φ ∧ ψ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
∧-dmorgan
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ φ ∨ ¬ ψ ⇔ ¬ (φ ∧ ψ)
¬∨¬-⇔-¬∧ = ∧-dmorgan

-- Proof.
∧-dmorgan {Γ}{φ}{ψ} =
  ⇔-intro
    (∧-dmorgan₂
      (assume (¬ φ ∨ ¬ ψ)))
    (∧-dmorgan₁
      (assume (¬ (φ ∧ ψ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢∧₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ⊃ γ
  → Γ ⊢ φ ∧ ψ
  → Γ ⊢ γ ∧ ψ

-- Proof.
subst⊢∧₁ Γ⊢φ⊃ψ Γ⊢φ∧ψ =
  ∧-intro
    (⊃-elim (∧-proj₁ (∧-intro Γ⊢φ⊃ψ Γ⊢φ∧ψ)) (∧-proj₁ Γ⊢φ∧ψ))
    (∧-proj₂ Γ⊢φ∧ψ)
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢∧₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ ψ ⊃ γ
  → Γ ⊢ φ ∧ ψ
  → Γ ⊢ φ ∧ γ

-- Proof.
subst⊢∧₂ {Γ}{φ}{ψ} Γ⊢φ⊃ψ Γ⊢φ∧ψ =
  ∧-intro
    (∧-proj₁ Γ⊢φ∧ψ)
    (⊃-elim Γ⊢φ⊃ψ (∧-proj₂ Γ⊢φ∧ψ))
-------------------------------------------------------------------------- ∎

-- Theorem.
¬∧-to-⊥
  : ∀ {Γ} {φ}
  → Γ ⊢ ¬ φ ∧ φ
  → Γ ⊢ ⊥

-- Proof.
¬∧-to-⊥ {Γ}{φ} Γ⊢φ = ¬-elim (∧-proj₁ Γ⊢φ) (∧-proj₂ Γ⊢φ)
-------------------------------------------------------------------------- ∎

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
------------------------------------------------------------------------
-- Descending lists
--
-- Anders Mörtberg and Chuangjie Xu, October 2019
--
-- We define descending lists via simultaneous definitions and show
-- that they are isomorphic to finite multisets.  The conversion from
-- finite multisets to descending lists is exactly insertion sort.  We
-- obtain the concatenation operation on descending lists and its
-- properties by transporting those on finite multisets.
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Everything

open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.List using (List ; [] ; _∷_)

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

open import Cubical.HITs.FiniteMultiset hiding ([_])

module Cubical.Data.DescendingList.Properties
 (A : Type₀)
 (_≥_ : A → A → Type₀)
 where

open import Cubical.Data.DescendingList.Base A _≥_

toFMSet : DL → FMSet A
toFMSet []           = []
toFMSet (cons x u _) = x ∷ toFMSet u

toList : DL → List A
toList [] = []
toList (cons x u _) = x ∷ toList u

-- "x ≥ ALL the elements of u"
data _≥ᴬ_ (x : A) : List A → Type₀ where
 ≥ᴬ[]   : x ≥ᴬ []
 ≥ᴬcons : {y : A} {u : List A} → x ≥ y → x ≥ᴬ u → x ≥ᴬ (y ∷ u)

data descending : List A → Type₀ where
 []-descending   : descending []
 cons-descending : {x : A} {u : List A} → x ≥ᴬ u → descending u → descending (x ∷ u)

module DescendingDL
 (≥trans : {x y z : A} → x ≥ y → y ≥ z → x ≥ z)
 where

 ≥≥ᴴtrans : {x y : A} {u : DL}
          → x ≥ y → y ≥ᴴ u → x ≥ᴴ u
 ≥≥ᴴtrans _   ≥ᴴ[]         = ≥ᴴ[]
 ≥≥ᴴtrans x≥y (≥ᴴcons y≥z) = ≥ᴴcons (≥trans x≥y y≥z)

 ≥ᴴ→≥ᴬ : {x : A} {u : DL} → x ≥ᴴ u → x ≥ᴬ toList u
 ≥ᴴ→≥ᴬ ≥ᴴ[]                   = ≥ᴬ[]
 ≥ᴴ→≥ᴬ (≥ᴴcons {r = y≥u} x≥y) = ≥ᴬcons x≥y (≥ᴴ→≥ᴬ (≥≥ᴴtrans x≥y y≥u))

 descendingDL : (u : DL) → descending (toList u)
 descendingDL []             = []-descending
 descendingDL (cons x u x≥u) = cons-descending (≥ᴴ→≥ᴬ x≥u) (descendingDL u)

------------------------------------------------------------------------
-- Descending lists are a set.

head≡ : {x y : A} {u v : DL} {r : x ≥ᴴ u} {s : y ≥ᴴ v}
      → cons x u r ≡ cons y v s → x ≡ y
head≡ {x} = cong head
 where
  head : DL → A
  head []           = x
  head (cons z _ _) = z

tail≡ : {x y : A} {u v : DL} {r : x ≥ᴴ u} {s : y ≥ᴴ v}
      → cons x u r ≡ cons y v s → u ≡ v
tail≡ = cong tail
 where
  tail : DL → DL
  tail []           = []
  tail (cons _ u _) = u

caseDL : ∀ {ℓ} → {X : Type ℓ} → (x y : X) → DL → X
caseDL x y []           = x
caseDL x y (cons _ _ _) = y

[]≢cons : {x : A} {u : DL} {r : x ≥ᴴ u} → ¬ ([] ≡ cons x u r)
[]≢cons p = subst (caseDL Unit ⊥) p tt

cons≢[] : {x : A} {u : DL} {r : x ≥ᴴ u} → ¬ (cons x u r ≡ [])
cons≢[] p = subst (caseDL ⊥ Unit) p tt

module isSetDL
 (≥isPropValued : {x y : A} → isProp (x ≥ y))
 (discreteA : Discrete A)
 where

 ≥ᴴisPropValued : {x : A} {u : DL} → isProp (x ≥ᴴ u)
 ≥ᴴisPropValued ≥ᴴ[]         ≥ᴴ[]          = refl
 ≥ᴴisPropValued (≥ᴴcons x≥y) (≥ᴴcons x≥y') = cong ≥ᴴcons (≥isPropValued x≥y x≥y')

 cons≡ : {x y : A} {u v : DL} {r : x ≥ᴴ u} {s : y ≥ᴴ v}
       → x ≡ y → u ≡ v → cons x u r ≡ cons y v s
 cons≡ {x} p = subst P p d
  where
   P : A → Type₀
   P y = {u v : DL} {r : x ≥ᴴ u} {s : y ≥ᴴ v} → u ≡ v → cons x u r ≡ cons y v s
   d : P x
   d {u} q = subst Q q c
    where
     Q : (v : DL) → Type₀
     Q v = {r : x ≥ᴴ u} {s : x ≥ᴴ v} → cons x u r ≡ cons x v s
     c : Q u
     c = cong (cons x u) (≥ᴴisPropValued _ _)

 discreteDL : Discrete DL
 discreteDL []           []           = yes refl
 discreteDL []           (cons y v s) = no []≢cons
 discreteDL (cons x u r) []           = no cons≢[]
 discreteDL (cons x u r) (cons y v s) with discreteA x y
 discreteDL (cons x u r) (cons y v s) | yes x≡y with discreteDL u v
 discreteDL (cons x u r) (cons y v s) | yes x≡y | yes u≡v = yes (cons≡ x≡y u≡v)
 discreteDL (cons x u r) (cons y v s) | yes x≡y | no  u≢v = no (λ e → u≢v (tail≡ e))
 discreteDL (cons x u r) (cons y v s) | no  x≢y = no (λ e → x≢y (head≡ e))

 isSetDL : isSet DL
 isSetDL = Discrete→isSet discreteDL

------------------------------------------------------------------------
-- Descending lists are isomorphic to finite multisets.

module IsoToFMSet
 (discreteA : Discrete A)
 (≥dec : (x y : A) → Dec (x ≥ y))
 (≥isPropValued : {x y : A} → isProp (x ≥ y))
 (≥trans : {x y z : A} → x ≥ y → y ≥ z → x ≥ z)
 (≰→≥ : {x y : A} → ¬ (x ≥ y) → y ≥ x)
 (≤≥→≡ : {x y : A} → x ≥ y → y ≥ x → x ≡ y)
 where

 ------------------------------------------------------------------------
 -- The insert function
 --
 -- The type DL is defined simultaneously with the relation _≥ᴴ_.
 -- Hence the insert function has to be defined by simultaneously
 -- proving a property of _≥ᴴ_.

 insert : A → DL → DL
 ≥ᴴinsert : {x y : A} {u : DL}
          → y ≥ᴴ u → ¬ (x ≥ y) → y ≥ᴴ insert x u

 insert x  []          = [ x ]
 insert x (cons y u r) with ≥dec x y
 insert x (cons y u r) | yes x≥y = cons x (cons y u r) (≥ᴴcons x≥y)
 insert x (cons y u r) | no  x≱y = cons y (insert x u) (≥ᴴinsert r x≱y)

 ≥ᴴinsert ≥ᴴ[] x≱y = ≥ᴴcons (≰→≥ x≱y)
 ≥ᴴinsert {x} {y} {cons z u z≥u} (≥ᴴcons y≥z) x≱y with ≥dec x z
 ≥ᴴinsert {x} {y} {cons z u z≥u} (≥ᴴcons y≥z) x≱y | yes x≥z = ≥ᴴcons (≰→≥ x≱y)
 ≥ᴴinsert {x} {y} {cons z u z≥u} (≥ᴴcons y≥z) x≱y | no  x≱z = ≥ᴴcons y≥z

 open isSetDL ≥isPropValued discreteA

 insert-swap : (x y : A) (u : DL)
             → insert x (insert y u) ≡ insert y (insert x u)
 insert-swap x y [] with ≥dec x y
 insert-swap x y [] | yes x≥y with ≥dec y x
 insert-swap x y [] | yes x≥y | yes y≥x = cons≡ (≤≥→≡ x≥y y≥x) (cons≡ (≤≥→≡ y≥x x≥y) refl)
 insert-swap x y [] | yes x≥y | no  y≱x = cons≡ refl (cons≡ refl refl)
 insert-swap x y [] | no  x≱y with ≥dec y x
 insert-swap x y [] | no  x≱y | yes y≥x = cons≡ refl (cons≡ refl refl)
 insert-swap x y [] | no  x≱y | no  y≱x = ⊥-elim (x≱y (≰→≥ y≱x))
 insert-swap x y (cons z u z≥u) with ≥dec y z
 insert-swap x y (cons z u z≥u) | yes y≥z with ≥dec x y
 insert-swap x y (cons z u z≥u) | yes y≥z | yes x≥y with ≥dec x z
 insert-swap x y (cons z u z≥u) | yes y≥z | yes x≥y | yes x≥z with ≥dec y x
 insert-swap x y (cons z u z≥u) | yes y≥z | yes x≥y | yes x≥z | yes y≥x = cons≡ (≤≥→≡ x≥y y≥x) (cons≡ (≤≥→≡ y≥x x≥y) refl)
 insert-swap x y (cons z u z≥u) | yes y≥z | yes x≥y | yes x≥z | no  y≱x with ≥dec y z
 insert-swap x y (cons z u z≥u) | yes y≥z | yes x≥y | yes x≥z | no  y≱x | yes y≥z' = cons≡ refl (cons≡ refl refl)
 insert-swap x y (cons z u z≥u) | yes y≥z | yes x≥y | yes x≥z | no  y≱x | no  y≱z  = ⊥-elim (y≱z y≥z)
 insert-swap x y (cons z u z≥u) | yes y≥z | yes x≥y | no  x≱z = ⊥-elim (x≱z (≥trans x≥y y≥z))
 insert-swap x y (cons z u z≥u) | yes y≥z | no  x≱y with ≥dec x z
 insert-swap x y (cons z u z≥u) | yes y≥z | no  x≱y | yes x≥z with ≥dec y x
 insert-swap x y (cons z u z≥u) | yes y≥z | no  x≱y | yes x≥z | yes y≥x = cons≡ refl (cons≡ refl refl)
 insert-swap x y (cons z u z≥u) | yes y≥z | no  x≱y | yes x≥z | no  y≱x = ⊥-elim (x≱y (≰→≥ y≱x))
 insert-swap x y (cons z u z≥u) | yes y≥z | no  x≱y | no  x≱z with ≥dec y z
 insert-swap x y (cons z u z≥u) | yes y≥z | no  x≱y | no  x≱z | yes y≥z' = cons≡ refl (cons≡ refl refl)
 insert-swap x y (cons z u z≥u) | yes y≥z | no  x≱y | no  x≱z | no  y≱z  = ⊥-elim (y≱z y≥z)
 insert-swap x y (cons z u z≥u) | no  y≱z with ≥dec x z
 insert-swap x y (cons z u z≥u) | no  y≱z | yes x≥z with ≥dec y x
 insert-swap x y (cons z u z≥u) | no  y≱z | yes x≥z | yes y≥x = ⊥-elim (y≱z (≥trans y≥x x≥z))
 insert-swap x y (cons z u z≥u) | no  y≱z | yes x≥z | no  y≱x with ≥dec y z
 insert-swap x y (cons z u z≥u) | no  y≱z | yes x≥z | no  y≱x | yes y≥z  = ⊥-elim (y≱z y≥z)
 insert-swap x y (cons z u z≥u) | no  y≱z | yes x≥z | no  y≱x | no  y≱z' = cons≡ refl (cons≡ refl refl)
 insert-swap x y (cons z u z≥u) | no  y≱z | no  x≱z with ≥dec y z
 insert-swap x y (cons z u z≥u) | no  y≱z | no  x≱z | yes y≥z  = ⊥-elim (y≱z y≥z)
 insert-swap x y (cons z u z≥u) | no  y≱z | no  x≱z | no  y≱z' = cons≡ refl (insert-swap x y u)

 -- Insertion sort
 toDL : FMSet A → DL
 toDL = FMSetRec.f isSetDL [] insert insert-swap
 {-
 toDL []                  = []
 toDL (x ∷ u)             = insert x (toDL u)
 toDL (comm x y u i)      = insert-swap x y (toDL u) i
 toDL (trunc x y p q i j) = isSetDL (toDL x) (toDL y) (cong toDL p) (cong toDL q) i j
 -}

 insert-cons : (x : A) (u : DL) (r : x ≥ᴴ u)
             → insert x u ≡ cons x u r
 insert-cons x [] _ = cons≡ refl refl
 insert-cons x (cons y u _) _ with ≥dec x y
 insert-cons x (cons y u _) _            | yes x≥y = cons≡ refl refl
 insert-cons x (cons y u _) (≥ᴴcons x≥y) | no  x≱y = ⊥-elim (x≱y x≥y)

 toDL∘toFMSet≡id : (u : DL) → toDL (toFMSet u) ≡ u
 toDL∘toFMSet≡id [] = refl
 toDL∘toFMSet≡id (cons x u r) i =
   hcomp (λ j → λ { (i = i0) → insert x (toDL∘toFMSet≡id u (~ j))
                  ; (i = i1) → cons x u r })
         (insert-cons x u r i)

 insert-∷ : (x : A) (u : DL)
          → toFMSet (insert x u) ≡ x ∷ toFMSet u
 insert-∷ x [] = refl
 insert-∷ x (cons y u _) with ≥dec x y
 insert-∷ x (cons y u _) | yes x≥y = refl
 insert-∷ x (cons y u _) | no  x≱y = cong (λ z → y ∷ z) (insert-∷ x u) ∙ comm y x (toFMSet u)

 toFMSet∘toDL≡id : (u : FMSet A) → toFMSet (toDL u) ≡ u
 toFMSet∘toDL≡id = FMSetElimProp.f (trunc _ _)
                                   refl
                                   (λ x {u} p → insert-∷ x (toDL u) ∙ cong (λ z → x ∷ z) p)

 FMSet≡DL : FMSet A ≡ DL
 FMSet≡DL = isoToPath (iso toDL toFMSet toDL∘toFMSet≡id toFMSet∘toDL≡id)

 ------------------------------------------------------------------------
 -- Concatenation of sorted lists
 --
 -- Defined by transporting the one on finite multisets

 infixr 30 _++ᴰᴸ_

 _++ᴰᴸ_ : DL → DL → DL
 _++ᴰᴸ_ = transport (λ i → FMSet≡DL i → FMSet≡DL i → FMSet≡DL i) _++_

 []Path : PathP (λ i → FMSet≡DL i) [] []
 []Path i = transp (λ j → FMSet≡DL (i ∧ j)) (~ i) []

 ++Path : PathP (λ i → FMSet≡DL i → FMSet≡DL i → FMSet≡DL i) _++_ _++ᴰᴸ_
 ++Path i = transp (λ j → FMSet≡DL (i ∧ j) → FMSet≡DL (i ∧ j) → FMSet≡DL (i ∧ j)) (~ i) _++_

 unitl-++ᴰᴸ : ∀ u → [] ++ᴰᴸ u ≡ u
 unitl-++ᴰᴸ = transport (λ i → (u : FMSet≡DL i) → ++Path i ([]Path i) u ≡ u) unitl-++

 unitr-++ᴰᴸ : ∀ u → u ++ᴰᴸ [] ≡ u
 unitr-++ᴰᴸ = transport (λ i → (u : FMSet≡DL i) → ++Path i u ([]Path i) ≡ u) unitr-++

 assoc-++ᴰᴸ : ∀ u v w → u ++ᴰᴸ (v ++ᴰᴸ w) ≡ (u ++ᴰᴸ v) ++ᴰᴸ w
 assoc-++ᴰᴸ = transport (λ i → (u v w : FMSet≡DL i)
                             → ++Path i u (++Path i v w) ≡ ++Path i (++Path i u v) w)
                        assoc-++

 comm-++ᴰᴸ : ∀ u v → u ++ᴰᴸ v ≡ v ++ᴰᴸ u
 comm-++ᴰᴸ = transport (λ i → (u v : FMSet≡DL i) → ++Path i u v ≡ ++Path i v u) comm-++

 ------------------------------------------------------------------------
 -- Converting multisets to (descending) lists

 FMSet→List : FMSet A → List A
 FMSet→List u = toList (toDL u)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module main where

open import lib
import string-format
-- for parser for Cedille
open import cedille-types

-- for parser for options files
import options-types
import cedille-options

-- for parser for Cedille comments & whitespace
import cws-types

open import constants
open import general-util

createOptionsFile : (dot-ced-dir : string) → IO ⊤
createOptionsFile dot-ced-dir =
  let ops-fp = combineFileNames dot-ced-dir options-file-name in
  createDirectoryIfMissing ff (takeDirectory ops-fp) >>
  withFile ops-fp WriteMode (flip hPutRope (cedille-options.options-to-rope cedille-options.default-options))

str-bool-to-𝔹 : options-types.str-bool → 𝔹
str-bool-to-𝔹 options-types.StrBoolTrue = tt
str-bool-to-𝔹 options-types.StrBoolFalse = ff

opts-to-options : filepath → options-types.opts → IO cedille-options.options
opts-to-options ofp (options-types.OptsCons (options-types.Lib fps) ops) =
  opts-to-options ofp ops >>= λ ops → paths-to-stringset fps >>=r λ ip → record ops { include-path = ip }
  where paths-to-stringset : options-types.paths → IO (𝕃 string × stringset)
        paths-to-stringset (options-types.PathsCons fp fps) =
          let rfp = combineFileNames (takeDirectory (takeDirectory ofp)) fp in
          paths-to-stringset fps >>= λ ps →
          doesDirectoryExist rfp >>= λ rfpₑ →
          doesDirectoryExist fp >>= λ fpₑ →
          (if rfpₑ
            then (canonicalizePath rfp >>= λ rfp →
                  return (cedille-options.include-path-insert rfp ps))
            else return ps) >>= λ ps →
          if fpₑ
            then (canonicalizePath fp >>= λ fp →
                  return (cedille-options.include-path-insert fp ps))
            else return ps
        paths-to-stringset options-types.PathsNil = return ([] , empty-stringset)
opts-to-options ofp (options-types.OptsCons (options-types.UseCedeFiles b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { use-cede-files = str-bool-to-𝔹 b }
opts-to-options ofp (options-types.OptsCons (options-types.MakeRktFiles b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { make-rkt-files = str-bool-to-𝔹 b }
opts-to-options ofp (options-types.OptsCons (options-types.GenerateLogs b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { generate-logs = str-bool-to-𝔹 b }
opts-to-options ofp (options-types.OptsCons (options-types.ShowQualifiedVars b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { show-qualified-vars = str-bool-to-𝔹 b }
opts-to-options ofp (options-types.OptsCons (options-types.EraseTypes b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { erase-types = str-bool-to-𝔹 b }
opts-to-options ofp options-types.OptsNil = return cedille-options.default-options

-- helper function to try to parse the options file
processOptions : filepath → string → IO (string ⊎ cedille-options.options)
processOptions filename s with options-types.scanOptions s
...| options-types.Left cs = return (inj₁ ("Parse error in file " ^ filename ^ " " ^ cs ^ "."))
...| options-types.Right (options-types.File oo) =
  opts-to-options filename oo
  >>= λ opts → if cedille-options.options.make-rkt-files opts
    then return ∘ inj₁ $ "Racket compilation disabled, please set to false in " ^ filename ^ "."
  else (return ∘ inj₂ $ opts)

getOptionsFile : (filepath : string) → string
getOptionsFile fp = combineFileNames (dot-cedille-directory fp) options-file-name

findOptionsFile : (filepath : string) → IO (maybe string)
findOptionsFile fp = h fp (pred (length (splitPath fp))) where
  h : string → ℕ → IO (maybe string)
  h fp 0 = return nothing
  h fp (suc n) =
    let fpc = getOptionsFile fp in
    doesFileExist fpc >>= λ where
      ff → h (takeDirectory fp) n
      tt → return (just fpc)

readOptions : IO (string × cedille-options.options)
readOptions =
  getCurrentDirectory >>=
  canonicalizePath >>=
  findOptionsFile >>= λ where
    nothing →
      getHomeDirectory >>=
      canonicalizePath >>= λ home →
      createOptionsFile (dot-cedille-directory home) >>r
      dot-cedille-directory home , cedille-options.default-options
    (just fp) → readFiniteFile fp >>= λ fc →
      processOptions fp fc >>= λ where
        (inj₁ err) →
          putStrLn (global-error-string err) >>r
          fp , cedille-options.default-options
        (inj₂ ops) → return (fp , ops)

module main-with-options
  (compileTime : UTC)
  (options-filepath : filepath)
  (options : cedille-options.options) where

  open import ctxt
  open import monad-instances
  open import process-cmd options {IO}
  open import parser
  open import spans options {IO}
  open import syntax-util
  open import to-string options
  open import toplevel-state options {IO}
  import interactive-cmds
  open import rkt options
  open import elaboration options

  logFilepath : IO filepath
  logFilepath = getHomeDirectory >>=r λ home →
                combineFileNames (dot-cedille-directory home) "log"

  maybeClearLogFile : IO ⊤
  maybeClearLogFile = if cedille-options.options.generate-logs options then
      logFilepath >>= clearFile
    else
      return triv

  logRope : rope → IO ⊤
  logRope s with cedille-options.options.generate-logs options
  ...| ff = return triv
  ...| tt = getCurrentTime >>= λ time →
            logFilepath >>= λ fn →
            withFile fn AppendMode λ hdl →
              hPutRope hdl ([[ "([" ^ utcToString time ^ "] " ]] ⊹⊹ s ⊹⊹ [[ ")\n" ]])

  logMsg : (message : string) → IO ⊤
  logMsg msg = logRope [[ msg ]]

  sendProgressUpdate : string → IO ⊤
  sendProgressUpdate msg = putStr "progress: " >> putStr msg >> putStr "\n"

  progressUpdate : (filename : string) → (do-check : 𝔹) → IO ⊤
  progressUpdate filename do-check =
    sendProgressUpdate ((if do-check then "Checking " else "Skipping ") ^ filename)

  fileBaseName : filepath → string
  fileBaseName fn = base-filename (takeFileName fn)

  {-------------------------------------------------------------------------------
    .cede support
  -------------------------------------------------------------------------------}

  cede-suffix = ".cede"
  rkt-suffix = ".rkt"

  ced-aux-filename : (suffix ced-path : filepath) → filepath
  ced-aux-filename sfx ced-path =
    let dir = takeDirectory ced-path in
      combineFileNames (dot-cedille-directory dir) (fileBaseName ced-path ^ sfx)

  cede-filename = ced-aux-filename cede-suffix
  rkt-filename = ced-aux-filename rkt-suffix

  maybe-write-aux-file : include-elt → (create-dot-ced-if-missing : IO ⊤) → (filename file-suffix : filepath) → (cedille-options.options → 𝔹) → (include-elt → 𝔹) → rope → IO ⊤
  maybe-write-aux-file ie mk-dot-ced fn sfx f f' r with f options && ~ f' ie
  ...| ff = return triv
  ...| tt = mk-dot-ced >>
            logMsg ("Starting writing " ^ sfx ^ " file " ^ fn) >>
            writeRopeToFile fn r >>
            logMsg ("Finished writing " ^ sfx ^ " file " ^ fn)

  write-aux-files : toplevel-state → filepath → IO ⊤
  write-aux-files s filename with get-include-elt-if s filename
  ...| nothing = return triv
  ...| just ie =
    let dot-ced = createDirectoryIfMissing ff (dot-cedille-directory (takeDirectory filename)) in
    maybe-write-aux-file ie dot-ced (cede-filename filename) cede-suffix
      cedille-options.options.use-cede-files
      include-elt.cede-up-to-date
      ((if include-elt.err ie then [[ "e" ]] else [[]]) ⊹⊹ include-elt-spans-to-rope ie) >>
    maybe-write-aux-file ie dot-ced (rkt-filename filename) rkt-suffix
      cedille-options.options.make-rkt-files
      include-elt.rkt-up-to-date
      (to-rkt-file filename (toplevel-state.Γ s) ie rkt-filename)

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

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

  -- Allows you to say "import FOO.BAR.BAZ" rather than "import FOO/BAR/BAZ"
  replace-dots : filepath → filepath
  replace-dots s = 𝕃char-to-string (h (string-to-𝕃char s)) where
    h : 𝕃 char → 𝕃 char
    h ('.' :: '.' :: cs) = '.' :: '.' :: h cs
    h ('.' :: cs) = pathSeparator :: h cs
    h (c :: cs) = c :: h cs
    h [] = []

  find-imported-file : (dirs : 𝕃 filepath) → (unit-name : string) → IO (maybe filepath)
  find-imported-file [] unit-name = return nothing
  find-imported-file (dir :: dirs) unit-name =
      let e = combineFileNames dir (add-cedille-extension unit-name) in
      doesFileExist e >>= λ where
        ff → find-imported-file dirs unit-name
        tt → canonicalizePath e >>=r just

  find-imported-files : (dirs : 𝕃 filepath) → (imports : 𝕃 string) → IO (𝕃 (string × filepath))
  find-imported-files dirs (u :: us) =
    find-imported-file dirs (replace-dots u) >>= λ where
      nothing → logMsg ("Error finding file: " ^ replace-dots u) >> find-imported-files dirs us
      (just fp) → logMsg ("Found import: " ^ fp) >> find-imported-files dirs us >>=r (u , fp) ::_
  find-imported-files dirs [] = return []

  {- new parser test integration -}
  reparse : toplevel-state → filepath → IO toplevel-state
  reparse st filename =
     doesFileExist filename >>= λ b →
       (if b then
           (readFiniteFile filename >>= λ s → getCurrentTime >>= λ time → processText s >>=r λ ie → set-last-parse-time-include-elt ie time)
        else return (error-include-elt ("The file " ^ filename ^ " could not be opened for reading.")))
       >>=r set-include-elt st filename
    where processText : string → IO include-elt
          processText x with parseStart x
          processText x | Left (Left cs)  = return (error-span-include-elt ("Error in file " ^ filename ^ ".") "Lexical error." cs)
          processText x | Left (Right cs) = return (error-span-include-elt ("Error in file " ^ filename ^ ".") "Parsing error." cs)
          processText x | Right t  with cws-types.scanComments x
          processText x | Right t | t2 = find-imported-files (fst (cedille-options.include-path-insert (takeDirectory filename) (toplevel-state.include-path st)))
                                                             (get-imports t) >>= λ deps →
                                         logMsg ("deps for file " ^ filename ^ ": " ^ 𝕃-to-string (λ {(a , b) → "short: " ^ a ^ ", long: " ^ b}) ", " deps) >>r
                                         new-include-elt filename deps t t2 nothing

  reparse-file : filepath → toplevel-state → IO toplevel-state
  reparse-file filename s =
    reparse s filename >>=r λ s →
    set-include-elt s filename
      (set-cede-file-up-to-date-include-elt
        (set-do-type-check-include-elt
          (get-include-elt s filename) tt) ff)

  infixl 1 _&&>>_
  _&&>>_ : IO 𝔹 → IO 𝔹 → IO 𝔹
  (a &&>> b) = a >>= λ a → if a then b else return ff

  aux-up-to-date : filepath → toplevel-state → IO toplevel-state
  aux-up-to-date filename s =
    let rkt = rkt-filename filename in
    doesFileExist rkt &&>> fileIsOlder filename rkt >>=r
    (set-include-elt s filename ∘  (set-rkt-file-up-to-date-include-elt (get-include-elt s filename)))

  ie-up-to-date : filepath → include-elt → IO 𝔹
  ie-up-to-date filename ie =
    getModificationTime filename >>=r λ mt →
    maybe-else ff (λ lpt → lpt utc-after mt) (include-elt.last-parse-time ie)

  import-changed : toplevel-state → filepath → (import-file : string) → IO 𝔹
  import-changed s filename import-file =
    let dtc = include-elt.do-type-check (get-include-elt s import-file)
        cede = cede-filename filename
        cede' = cede-filename import-file in
    case cedille-options.options.use-cede-files options of λ where
      ff → return dtc
      tt → doesFileExist cede &&>> doesFileExist cede' >>= λ where
        ff → return ff
        tt → fileIsOlder cede cede' >>=r λ fio → dtc || fio

  any-imports-changed : toplevel-state → filepath → (imports : 𝕃 string) → IO 𝔹
  any-imports-changed s filename [] = return ff
  any-imports-changed s filename (h :: t) =
    import-changed s filename h >>= λ where
      tt → return tt
      ff → any-imports-changed s filename t

  file-after-compile : filepath → IO 𝔹
  file-after-compile fn =
    getModificationTime fn >>= λ mt →
    case mt utc-after compileTime of λ where
      tt → doesFileExist options-filepath &&>> fileIsOlder options-filepath fn
      ff → return ff

  ensure-ast-depsh : filepath → toplevel-state → IO toplevel-state
  ensure-ast-depsh filename s with get-include-elt-if s filename
  ...| just ie = ie-up-to-date filename ie >>= λ where
    ff → reparse-file filename s
    tt → return s
  ...| nothing =
      let cede = cede-filename filename in
      return (cedille-options.options.use-cede-files options) &&>>
      doesFileExist cede &&>>
      fileIsOlder filename cede &&>>
      file-after-compile cede >>= λ where
         ff → reparse-file filename s
         tt → reparse s filename >>= λ s →
              read-cede-file filename >>= λ where
                (err , ss) → return
                  (set-include-elt s filename
                  (set-do-type-check-include-elt
                  (set-need-to-add-symbols-to-context-include-elt
                  (set-spans-string-include-elt
                  (get-include-elt s filename) err ss) tt) ff))

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

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

  log-files-to-check : toplevel-state → IO ⊤
  log-files-to-check s = logRope ([[ "\n" ]] ⊹⊹ (h (trie-mappings (toplevel-state.is s)))) where
    h : 𝕃 (string × include-elt) → rope
    h [] = [[]]
    h ((fn , ie) :: t) = [[ "file: " ]] ⊹⊹ [[ fn ]] ⊹⊹ [[ "\nadd-symbols: " ]] ⊹⊹ [[ 𝔹-to-string (include-elt.need-to-add-symbols-to-context ie) ]] ⊹⊹ [[ "\ndo-type-check: " ]] ⊹⊹ [[ 𝔹-to-string (include-elt.do-type-check ie) ]] ⊹⊹ [[ "\n\n" ]] ⊹⊹ h t

  {- this function checks the given file (if necessary), updates .cede and .rkt files (again, if necessary), and replies on stdout if appropriate -}
  checkFile : toplevel-state → filepath → (should-print-spans : 𝔹) → IO toplevel-state
  checkFile s filename should-print-spans =
    update-asts s filename >>= λ s →
    log-files-to-check s >>
    logMsg (𝕃-to-string (λ {(im , fn) → "im: " ^ im ^ ", fn: " ^ fn}) "; " (trie-mappings (include-elt.import-to-dep (get-include-elt s filename)))) >>
    process-file progressUpdate s filename (fileBaseName filename) >>= finish
    where
          reply : toplevel-state → IO ⊤
          reply s with get-include-elt-if s filename
          reply s | nothing = putStrLn (global-error-string ("Internal error looking up information for file " ^ filename ^ "."))
          reply s | just ie =
             if should-print-spans then
               putRopeLn (include-elt-spans-to-rope ie)
             else return triv
          finish : toplevel-state × mod-info → IO toplevel-state
          finish (s @ (mk-toplevel-state ip mod is Γ) , ret-mod) =
            logMsg ("Started reply for file " ^ filename) >> -- Lazy, so checking has not been calculated yet?
            reply s >>
            logMsg ("Finished reply for file " ^ filename) >>
            logMsg ("Files with updated spans:\n" ^ 𝕃-to-string (λ x → x) "\n" mod) >>
            let Γ = ctxt-set-current-mod Γ ret-mod in
            writeo mod >>r -- Should process-file now always add files to the list of modified ones because now the cede-/rkt-up-to-date fields take care of whether to rewrite them?
            mk-toplevel-state ip mod is Γ
              where
                writeo : 𝕃 string → IO ⊤
                writeo [] = return triv
                writeo (f :: us) =
                  writeo us >>
                  -- let ie = get-include-elt s f in
                  write-aux-files s f
                  --  (if cedille-options.options.make-rkt-files options && ~ include-elt.rkt-up-to-date ie then (write-rkt-file f (toplevel-state.Γ s) ie rkt-filename) else return triv)

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

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

              debugCommand : toplevel-state → IO ⊤
              debugCommand s = putStrLn (escape-string (toplevel-state-to-string s))

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

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

              handleCommands : 𝕃 string → toplevel-state → IO toplevel-state
              handleCommands ("progress stub" :: xs) = return
              handleCommands ("status ping" :: xs) s = putStrLn "idle" >> return s
              handleCommands ("check" :: xs) s = checkCommand xs s
              handleCommands ("debug" :: []) s = debugCommand s >>r s
              handleCommands ("elaborate" :: x :: x' :: []) s = elab-all s x x' >>r s
              handleCommands ("interactive" :: xs) s = interactive-cmds.interactive-cmd options xs s >>r s
  --            handleCommands ("find" :: xs) s = findCommand xs s
              handleCommands xs s = errorCommand xs s >>r s

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

  -- this is the case for when we are called with a single command-line argument, the name of the file to process
  processArgs (input-filename :: []) =
    canonicalizePath input-filename >>= λ input-filename →
    checkFile (new-toplevel-state (cedille-options.include-path-insert (takeDirectory input-filename) (cedille-options.options.include-path options)))
      input-filename ff {- should-print-spans -} >>= finish input-filename
    where finish : string → toplevel-state → IO ⊤
          finish input-filename s = return triv
{-            let ie = get-include-elt s input-filename in
            if include-elt.err ie then (putRopeLn (include-elt-spans-to-rope ie)) else return triv
-}
  -- this is the case where we will go into a loop reading commands from stdin, from the fronted
  processArgs [] = readCommandsFromFrontend (new-toplevel-state (cedille-options.options.include-path options))

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

  main' : IO ⊤
  main' =
    maybeClearLogFile >>
    logMsg ("Started Cedille process (compiled at: " ^ utcToString compileTime ^ ")") >>
    getArgs >>=
    processArgs

postulate
  initializeStdinToUTF8 : IO ⊤
  setStdinNewlineMode : IO ⊤
  compileTime : UTC
  templatesDir : filepath

{-# FOREIGN GHC {-# LANGUAGE TemplateHaskell #-} #-}
{-# FOREIGN GHC import qualified System.IO #-}
{-# FOREIGN GHC import qualified Data.Time.Clock #-}
{-# FOREIGN GHC import qualified Data.Time.Format #-}
{-# FOREIGN GHC import qualified Data.Time.Clock.POSIX #-}
{-# FOREIGN GHC import qualified Language.Haskell.TH.Syntax #-}
{-# COMPILE GHC initializeStdinToUTF8 = System.IO.hSetEncoding System.IO.stdin System.IO.utf8 #-}
{-# COMPILE GHC setStdinNewlineMode = System.IO.hSetNewlineMode System.IO.stdin System.IO.universalNewlineMode #-}
{-# COMPILE GHC compileTime =
  maybe (Data.Time.Clock.POSIX.posixSecondsToUTCTime (fromIntegral 0)) id
  (Data.Time.Format.parseTimeM True Data.Time.Format.defaultTimeLocale "%s"
    $(Language.Haskell.TH.Syntax.runIO
      (Data.Time.Clock.getCurrentTime >>= \ t ->
       return (Language.Haskell.TH.Syntax.LitE
         (Language.Haskell.TH.Syntax.StringL
           (Data.Time.Format.formatTime Data.Time.Format.defaultTimeLocale "%s" t)))))
    :: Maybe Data.Time.Clock.UTCTime) #-}

-- main entrypoint for the backend
main : IO ⊤
main = initializeStdoutToUTF8 >>
       initializeStdinToUTF8 >>
       setStdoutNewlineMode >>
       setStdinNewlineMode >>
       setToLineBuffering >>
       readOptions >>=
       uncurry (main-with-options.main' compileTime)

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

module Story where

{--

PiCat level 0:
  Objects:     Finite sets viewed as discrete-groupoids
  Morphisms:   Permutations between finite sets viewed as permutation-groupoids
  Equivalence: Strong Equivalence of categories

Discrete-Groupoids:
  Objects:     Parameterized
  Morphisms:   Only id
  Equivalence: ≡

Permutation-Groupoids: each permutation is a 1-1 function
  Objects:     Finite Sets (or Enumerations)
  Morphisms:   A morphism represents a swap of two elements by the permutation
  Equivalence: ≡

------

PiCat level 1:
  Objects:     Finite sets viewed as discrete-groupoids
  Morphisms:   Permutations between finite sets viewed as permutation-groupoids
  Equivalence: Equivalence-of-Permutations-groupoids

Discrete-Groupoids:
  Objects:     Parameterized
  Morphisms:   Only id
  Equivalence: ≡

Permutation-Groupoids: each permutation is a 1-1 function
  Objects:     Finite Sets (or Enumerations)
  Morphisms:   A morphism represents a swap of two elements by the permutation
  Equivalence: ≡

Equivalance-of-Permutations-Groupoids:
  Objects:     Permutation-Groupoids
  Morphisms:   ??
  Equivalence: Strong Equivalence of categories

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------------
-- Testing the existential quantifier
------------------------------------------------------------------------------

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

module Existential where

postulate
  D : Set
  A : D → Set
  ∃ : (A : D → Set) → Set

postulate foo : (∃ λ x → A x) → (∃ λ x → A x)
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --without-K #-}
module Homotopy where

open import GroupoidStructure
open import PathOperations
open import Types

infix  1 _∼_

_∼_ : ∀ {a b} {A : Set a} {B : Set b}
  (f g : A → B) → Set _
f ∼ g = ∀ x → f x ≡ g x

naturality : ∀ {a b} {A : Set a} {B : Set b} {x y : A}
  (f g : A → B) (H : f ∼ g) (p : x ≡ y) →
  H x · ap g p ≡ ap f p · H y
naturality f g H = J
  (λ x y p → H x · ap g p ≡ ap f p · H y)
  (λ _ → p·id _) _ _

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

open import lib.Basics
open import lib.Equivalence2
open import lib.Relation2
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.TLevel

module lib.NType2 where

module _ {i} {A : Type i} where
  abstract
    has-dec-onesided-eq-is-prop : {x : A} → is-prop (has-dec-onesided-eq x)
    has-dec-onesided-eq-is-prop {x = x} = inhab-to-prop-is-prop λ dec →
      Π-level λ y → Dec-level (dec-onesided-eq-is-prop x dec y)

    has-dec-eq-is-prop : is-prop (has-dec-eq A)
    has-dec-eq-is-prop = Π-level (λ _ → has-dec-onesided-eq-is-prop)

module _ {i j} {A : Type i} {B : A → Type j} where
  abstract
    ↓-level : {a b : A} {p : a == b} {u : B a} {v : B b} {n : ℕ₋₂}
      → has-level (S n) (B b) → has-level n (u == v [ B ↓ p ])
    ↓-level {p = idp} k = has-level-apply k _ _

    ↓-preserves-level : {a b : A} {p : a == b} {u : B a} {v : B b} {n : ℕ₋₂}
      → has-level n (B b) → has-level n (u == v [ B ↓ p ])
    ↓-preserves-level {p = idp} = =-preserves-level

    prop-has-all-paths-↓ : {x y : A} {p : x == y} {u : B x} {v : B y}
      {{_ : is-prop (B y)}} → u == v [ B ↓ p ]
    prop-has-all-paths-↓ {p = idp} = prop-has-all-paths _ _

    set-↓-has-all-paths-↓ : ∀ {k} {C : Type k}
      {x y : C → A} {p : (t : C) → x t == y t} {u : (t : C) → B (x t)} {v : (t : C) → B (y t)}
      {a b : C} {q : a == b} {α : u a == v a [ B ↓ p a ]} {β : u b == v b [ B ↓ p b ]}
      {{_ : is-set (B (y a))}} → α == β [ (λ t → u t == v t [ B ↓ p t ]) ↓ q ]
    set-↓-has-all-paths-↓ {q = idp} {{p}} = lemma _ p
      where
        lemma : {x y : A} (p : x == y) {u : B x} {v : B y} {α β : u == v [ B ↓ p ]}
          → is-set (B y) → α == β
        lemma idp k = contr-center (has-level-apply (has-level-apply k _ _) _ _)

abstract
  -- Every map between contractible types is an equivalence
  contr-to-contr-is-equiv : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
    → (is-contr A → is-contr B → is-equiv f)
  contr-to-contr-is-equiv f cA cB =
    is-eq f (λ _ → contr-center cA) (λ b → ! (contr-path cB _) ∙ contr-path cB b) (contr-path cA)

  is-contr-is-prop : ∀ {i} {A : Type i} → is-prop (is-contr A)
  is-contr-is-prop {A = A} = all-paths-is-prop is-contr-is-prop-aux
          where

    lemma : (x : is-contr A) (b a : A) (p : b == a)
      → contr-path x a == contr-path x b ∙' p
    lemma x b ._ idp = idp

    is-contr-is-prop-aux : (x y : is-contr A) → x == y
    is-contr-is-prop-aux x y =
      ap has-level-in
        (pair= (contr-path x (contr-center y))
               (↓-Π-cst-app-in (λ a → ↓-idf=cst-in' (lemma x (contr-center y) a (contr-path y a)))))

  has-level-is-prop : ∀ {i} {n : ℕ₋₂} {A : Type i}
    → is-prop (has-level n A)
  has-level-is-prop {n = ⟨-2⟩} = is-contr-is-prop
  has-level-is-prop {n = S n} {A} = equiv-preserves-level e {{has-level-aux-prop}} where

    has-level-aux-prop : is-prop (has-level-aux (S n) A)
    has-level-aux-prop = Π-level (λ x → Π-level (λ y → has-level-is-prop))

    e : has-level-aux (S n) A ≃ has-level (S n) A
    fst e = has-level-in
    is-equiv.g (snd e) = has-level-apply
    is-equiv.f-g (snd e) = λ _ → idp
    is-equiv.g-f (snd e) = λ _ → idp
    is-equiv.adj (snd e) = λ _ → idp

  instance
    has-level-level : ∀ {i} {n m : ℕ₋₂} {A : Type i}
      → has-level (S m) (has-level n A)
    has-level-level {m = ⟨-2⟩} = has-level-is-prop
    has-level-level {m = S m} = raise-level _ has-level-level

{- Subtypes. -}

module _ {i j} {A : Type i} (P : SubtypeProp A j) where
  private
    module P = SubtypeProp P

  instance
    Subtype-level : ∀ {n : ℕ₋₂}
      {{_ : has-level (S n) A}}
      → has-level (S n) (Subtype P)
    Subtype-level = Σ-level ⟨⟩ (λ x → prop-has-level-S (P.level x))

  Subtype= : (x y : Subtype P) → Type i
  Subtype= x y = fst x == fst y

  Subtype=-out : ∀ {x y : Subtype P} → Subtype= x y → x == y
  Subtype=-out p = pair= p (prop-has-all-paths-↓ {{P.level _}})

  Subtype=-β : {x y : Subtype P} (p : Subtype= x y)
    → fst= (Subtype=-out {x = x} {y = y} p) == p
  Subtype=-β idp = fst=-β idp _

  Subtype=-η : {x y : Subtype P} (p : x == y)
    → Subtype=-out (fst= p) == p
  Subtype=-η idp = ap (pair= idp)
    (contr-has-all-paths {{has-level-apply (P.level _) _ _}} _ _)

  Subtype=-econv : (x y : Subtype P) → (Subtype= x y) ≃ (x == y)
  Subtype=-econv x y = equiv Subtype=-out fst= Subtype=-η Subtype=-β

  abstract
    Subtype-∙ : ∀ {x y z : Subtype P}
      (p : Subtype= x y) (q : Subtype= y z)
      → (Subtype=-out {x} {y} p ∙ Subtype=-out {y} {z} q)
      == Subtype=-out {x} {z} (p ∙ q)
    Subtype-∙ {x} {y} {z} p q =
      Subtype=-out p ∙ Subtype=-out q
        =⟨ Σ-∙ {p = p} {p' = q} (prop-has-all-paths-↓ {{P.level (fst y)}}) (prop-has-all-paths-↓ {{P.level (fst z)}}) ⟩
      pair= (p ∙ q) (prop-has-all-paths-↓ {p = p} {{P.level (fst y)}} ∙ᵈ prop-has-all-paths-↓ {{P.level (fst z)}})
        =⟨ contr-has-all-paths {{↓-level (P.level (fst z))}} _ (prop-has-all-paths-↓ {{P.level (fst z)}})
          |in-ctx pair= (p ∙ q) ⟩
      Subtype=-out (p ∙ q)
        =∎

-- Groupoids

is-gpd : {i : ULevel} → Type i → Type i
is-gpd = has-level 1

-- Type of all n-truncated types

-- TODO: redefine it like that, so that instance arguments can work

-- record _-Type_ (n : ℕ₋₂) (i : ULevel) : Type (lsucc i) where
--   constructor _,_
--   field
--     El : Type i
--     {{El-level}} : has-level n El
-- open _-Type_ public

has-level-prop : ∀ {i} → ℕ₋₂ → SubtypeProp (Type i) i
has-level-prop n = has-level n , λ _ → has-level-is-prop

_-Type_ : (n : ℕ₋₂) (i : ULevel) → Type (lsucc i)
n -Type i = Subtype (has-level-prop {i} n)

hProp : (i : ULevel) → Type (lsucc i)
hProp i = -1 -Type i

hSet : (i : ULevel) → Type (lsucc i)
hSet i = 0 -Type i

_-Type₀ : (n : ℕ₋₂) → Type₁
n -Type₀ = n -Type lzero

hProp₀ = hProp lzero
hSet₀ = hSet lzero

-- [n -Type] is an (n+1)-type

abstract
  ≃-contr : ∀ {i j} {A : Type i} {B : Type j}
      → is-contr A → is-contr B → is-contr (A ≃ B)
  ≃-contr pA pB = has-level-in
      ((cst (contr-center pB) , contr-to-contr-is-equiv _ pA pB)
      , (λ e → pair= (λ= (λ _ → contr-path pB _))
                     (from-transp is-equiv _ (prop-path is-equiv-is-prop _ _))))

instance
  ≃-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j}
    → (has-level n A → has-level n B → has-level n (A ≃ B))
  ≃-level {n = ⟨-2⟩} = ≃-contr
  ≃-level {n = S n} pA pB = Σ-level ⟨⟩ ⟨⟩ where instance _ = pA; _ = pB

  universe-=-level : ∀ {i} {n : ℕ₋₂} {A B : Type i}
    → (has-level n A → has-level n B → has-level n (A == B))
  universe-=-level pA pB = equiv-preserves-level ua-equiv where instance _ = pA; _ = pB

module _ {i} {n} where
  private
    prop : SubtypeProp {lsucc i} (Type i) i
    prop = has-level-prop n

  nType= : (A B : n -Type i) → Type (lsucc i)
  nType= = Subtype= prop

  nType=-out : {A B : n -Type i} → nType= A B → A == B
  nType=-out = Subtype=-out prop

  abstract
    nType=-β : {A B : n -Type i} (p : nType= A B)
      → fst= (nType=-out {A = A} {B = B} p) == p
    nType=-β = Subtype=-β prop

    nType=-η : {A B : n -Type i} (p : A == B)
      → nType=-out (fst= p) == p
    nType=-η = Subtype=-η prop

    nType=-econv : (A B : n -Type i) → (nType= A B) ≃ (A == B)
    nType=-econv = Subtype=-econv prop

    nType-∙ : {A B C : n -Type i}
      (p : nType= A B) (q : nType= B C)
      → (nType=-out {A = A} p ∙ nType=-out {A = B} q)
      == nType=-out {A = A} {B = C} (p ∙ q)
    nType-∙ = Subtype-∙ prop

abstract
 instance
  _-Type-level_ : (n : ℕ₋₂) (i : ULevel)
    → has-level (S n) (n -Type i)
  (n -Type-level i) = has-level-in (λ { (A , pA) (B , pB) → aux A B pA pB}) where

    aux : (A B : Type i) (pA : has-level n A) (pB : has-level n B) → has-level n ((A , pA) == (B , pB))
    aux A B pA pB = equiv-preserves-level (nType=-econv (A , ⟨⟩) (B , ⟨⟩)) where instance _ = pA; _ = pB

hProp-is-set : (i : ULevel) → is-set (hProp i)
hProp-is-set i = -1 -Type-level i

hSet-level : (i : ULevel) → has-level 1 (hSet i)
hSet-level i = 0 -Type-level i

{- The following two lemmas are in NType2 instead of NType because of cyclic
   dependencies -}

module _ {i} {A : Type i} where
  abstract
    raise-level-<T : {m n : ℕ₋₂} → (m <T n) → has-level m A → has-level n A
    raise-level-<T ltS = raise-level _
    raise-level-<T (ltSR lt) = raise-level _ ∘ raise-level-<T lt

    raise-level-≤T : {m n : ℕ₋₂} → (m ≤T n) → has-level m A → has-level n A
    raise-level-≤T (inl p) = transport (λ t → has-level t A) p
    raise-level-≤T (inr lt) = raise-level-<T lt

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda