text:
module SimpleTT where

  data 𝟘 : Set where

  absurd : ∀ {ℓ} {A : Set ℓ} → 𝟘 → A
  absurd ()

  data _⁺ (A : Set) : Set where
     Z : A ⁺
     S : A → A ⁺

  record Signature : Set₁ where
    field
      ty-op : Set
      tm-op : Set
      ty-ty-arg : ty-op → Set
      -- ty-tm-arg : ty-op → Set
      -- tm-ty-arg : tm-op → Set
      tm-tm-arg : tm-op → Set

  open Signature

  data Theory : Set₁
  thy-signature : Theory → Signature
  data Ty (T : Theory) : Set
  data Tm (T : Theory) (A : Ty T) : Set

  data Theory where
    thy-empty : Theory
    th-type : ∀ (T : Theory) → (α : Set) → (α → Ty T) → Theory
    th-term : ∀ (T : Theory) → (α : Set) → (α → Ty T) → Ty T → Theory

  thy-signature thy-empty =
    record { ty-op = 𝟘
           ; tm-op = 𝟘
           ; ty-ty-arg = absurd
           ; tm-tm-arg = absurd
           }

  thy-signature (th-type T α x) =
    record { ty-op = (ty-op Σ) ⁺
           ; tm-op = tm-op Σ
           ; ty-ty-arg = t
           ; tm-tm-arg = tm-tm-arg Σ
           }
    where
      Σ = thy-signature T
      t : ∀ (f : (ty-op Σ) ⁺) → Set
      t Z = α
      t (S f) = ty-ty-arg (thy-signature T) f

  thy-signature (th-term T α ts t) =
    record { ty-op = ty-op Σ
           ; tm-op = (tm-op Σ) ⁺
           ; ty-ty-arg = ty-ty-arg Σ
           ; tm-tm-arg = tm
           }
    where
      Σ = thy-signature T
      tm : ∀ (f : (tm-op Σ) ⁺) → Set
      tm Z = {!!}
      tm (S x) = {!!}

  data Ty T where
    ty-expr : ∀ (f : ty-op (thy-signature T)) → (ty-ty-arg (thy-signature T) f → Ty T) → Ty T

  data Tm T A where

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Category.Category where

open import Algebra.Category.Semigroupoid
open import Core

-- A category is a semigroupoid with an identity morphism on every
-- object.

record Category {c h r} : Set (lsuc (c ⊔ h ⊔ r)) where
  field semigroupoid : Semigroupoid {c} {h} {r}
  open Semigroupoid semigroupoid public

  field
    id : ∀ {A} → Hom A A
    left-id  : ∀ {A B} (f : Hom A B) → id ∘ f ≈ f
    right-id : ∀ {A B} (f : Hom A B) → f ∘ id ≈ f

  -- The identity morphism is unique for each object.
  id-unique :
    ∀ {A} {id' : Hom A A}
    → id' ∘ id ≈ id
    → id' ≈ id
  id-unique {id' = id'} left-id' =
    begin
      id'      ≈[ sym (right-id _) ]
      id' ∘ id ≈[ left-id' ]
      id
    qed

  private
    ∘-monic :
      ∀ {A B C} {f : Hom B C} {g : Hom A B}
      → Monic f
      → Monic g
      → Monic (f ∘ g)
    ∘-monic {f = f} {g} pf pg {g1 = g1} {g2} p =
      pg $ pf $
      begin
        f ∘ (g ∘ g1)  ≈[ sym (assoc f g g1) ]
        f ∘ g ∘ g1    ≈[ p ]
        f ∘ g ∘ g2    ≈[ assoc f g g2 ]
        f ∘ (g ∘ g2)
      qed

  BimonicEq : Equiv Ob
  BimonicEq =
    record {
      _≈_ = _bimonic_;
      refl = record {
        to = id;
        from = id;
        to-monic = id-monic;
        from-monic = id-monic
      };
      sym = λ m →
        let module m = _bimonic_ m in
        record {
          to = m.from;
          from = m.to;
          to-monic = m.from-monic;
          from-monic = m.to-monic
        };
      trans = λ m1 m2 →
        let module m1 = _bimonic_ m1
            module m2 = _bimonic_ m2 in
        record {
          to = m2.to ∘ m1.to;
          from = m1.from ∘ m2.from;
          to-monic = ∘-monic m2.to-monic m1.to-monic;
          from-monic = ∘-monic m1.from-monic m2.from-monic
        }
    }

    where
    id-monic : ∀ {A} → Monic (id {A})
    id-monic {g1 = g1} {g2} p =
      begin
        g1       ≈[ sym (left-id g1) ]
        id ∘ g1  ≈[ p ]
        id ∘ g2  ≈[ left-id g2 ]
        g2
      qed

  module BimonicEq = Equiv BimonicEq

  -- Isomorphisms
  record Iso {A B} (f : Hom A B) : Set (h ⊔ r) where
    field
      inv : Hom B A
      left-inv  : inv ∘ f ≈ id
      right-inv : f ∘ inv ≈ id

    -- Inverses are unique for each morphism.
    inv-unique : ∀ g → f ∘ g ≈ id → g ≈ inv
    inv-unique g right-inv' =
      begin
        g              ≈[ sym (left-id g) ]
        id ∘ g         ≈[ ∘-cong (sym left-inv) refl ]
        (inv ∘ f) ∘ g  ≈[ assoc inv f g ]
        inv ∘ (f ∘ g)  ≈[ ∘-cong refl right-inv' ]
        inv ∘ id       ≈[ right-id inv ]
        inv
      qed

    inv-iso : Iso inv
    inv-iso =
      record {
        inv = f;
        left-inv = right-inv;
        right-inv = left-inv
      }

    inv-invol : ∀ g h → g ∘ f ≈ id → h ∘ g ≈ id → f ≈ h
    inv-invol g h g-left-inv h-left-inv =
      begin
        f            ≈[ sym (left-id f) ]
        id ∘ f       ≈[ ∘-cong (sym h-left-inv) refl ]
        (h ∘ g) ∘ f  ≈[ assoc h g f ]
        h ∘ (g ∘ f)  ≈[ ∘-cong refl g-left-inv ]
        h ∘ id       ≈[ right-id h ]
        h
      qed

  record _≃_ A B : Set (h ⊔ r) where
    field
      to : Hom A B
      iso : Iso to

    open Iso iso public

  IsoEq : Equiv Ob
  IsoEq =
    record {
      _≈_ = _≃_;
      refl = irefl;
      sym = isym;
      trans = itrans
    }

    where
    irefl : ∀ {A} → A ≃ A
    irefl =
      record {
        to = id;
        iso = record {
          inv = id;
          left-inv = left-id id;
          right-inv = left-id id
        }
      }

    isym : ∀ {A B} → A ≃ B → B ≃ A
    isym iso =
      record {
        to = iso.inv;
        iso = record {
          inv = iso.to;
          left-inv = iso.right-inv;
          right-inv = iso.left-inv
        }
      }

      where
      module iso = _≃_ iso

    itrans : ∀ {A B C} → A ≃ B → B ≃ C → A ≃ C
    itrans iso1 iso2 =
      record {
        to = iso2.to ∘ iso1.to;
        iso = record {
          inv = iso1.inv ∘ iso2.inv;
          left-inv =
            begin
              iso1.inv ∘ iso2.inv ∘ (iso2.to ∘ iso1.to)   ≈[ assoc iso1.inv iso2.inv (iso2.to ∘ iso1.to) ]
              iso1.inv ∘ (iso2.inv ∘ (iso2.to ∘ iso1.to)) ≈[ ∘-cong refl (sym (assoc iso2.inv iso2.to iso1.to)) ]
              iso1.inv ∘ (iso2.inv ∘ iso2.to ∘ iso1.to)   ≈[ ∘-cong refl (∘-cong iso2.left-inv refl) ]
              iso1.inv ∘ (id ∘ iso1.to)                   ≈[ ∘-cong refl (left-id iso1.to) ]
              iso1.inv ∘ iso1.to                          ≈[ iso1.left-inv ]
              id
            qed;
          right-inv =
            begin
              iso2.to ∘ iso1.to ∘ (iso1.inv ∘ iso2.inv)   ≈[ assoc iso2.to iso1.to (iso1.inv ∘ iso2.inv) ]
              iso2.to ∘ (iso1.to ∘ (iso1.inv ∘ iso2.inv)) ≈[ ∘-cong refl (sym (assoc iso1.to iso1.inv iso2.inv)) ]
              iso2.to ∘ (iso1.to ∘ iso1.inv ∘ iso2.inv)   ≈[ ∘-cong refl (∘-cong iso1.right-inv refl) ]
              iso2.to ∘ (id ∘ iso2.inv)                   ≈[ ∘-cong refl (left-id iso2.inv) ]
              iso2.to ∘ iso2.inv                          ≈[ iso2.right-inv ]
              id
            qed
        }
      }

      where
      module iso1 = _≃_ iso1
      module iso2 = _≃_ iso2

  Iso→Epic : ∀ {A B} {f : Hom A B} → Iso f → Epic f
  Iso→Epic {f = f} iso {g1 = g1} {g2} p =
    begin
      g1                  ≈[ sym (right-id g1) ]
      g1 ∘ id             ≈[ ∘-cong refl (sym iso.right-inv) ]
      g1 ∘ (f ∘ iso.inv)  ≈[ sym (assoc g1 f iso.inv) ]
      g1 ∘ f ∘ iso.inv    ≈[ ∘-cong p refl ]
      g2 ∘ f ∘ iso.inv    ≈[ assoc g2 f iso.inv ]
      g2 ∘ (f ∘ iso.inv)  ≈[ ∘-cong refl iso.right-inv ]
      g2 ∘ id             ≈[ right-id g2 ]
      g2
    qed

    where
    module iso = Iso iso

  Iso→Monic : ∀ {A B} {f : Hom A B} → Iso f → Monic f
  Iso→Monic {f = f} iso {g1 = g1} {g2} p =
    begin
      g1                 ≈[ sym (left-id g1) ]
      id ∘ g1            ≈[ ∘-cong (sym iso.left-inv) refl ]
      iso.inv ∘ f ∘ g1   ≈[ assoc iso.inv f g1 ]
      iso.inv ∘ (f ∘ g1) ≈[ ∘-cong refl p ]
      iso.inv ∘ (f ∘ g2) ≈[ sym (assoc iso.inv f g2) ]
      iso.inv ∘ f ∘ g2   ≈[ ∘-cong iso.left-inv refl ]
      id ∘ g2            ≈[ left-id g2 ]
      g2
    qed

    where
    module iso = Iso iso

  MonicOrd : PartialOrder Ob
  MonicOrd =
    record {
      Eq = BimonicEq;
      _≤_ = _≤_;
      antisym = antisym;
      refl' = refl';
      trans = mtrans
    }

    where
    _≤_ : Ob → Ob → Set _
    A ≤ B = ∃ (λ (f : Hom A B) → Monic f)

    antisym : ∀ {A B} → A ≤ B → B ≤ A → A bimonic B
    antisym A≤B B≤A =
      record {
        to = fst A≤B;
        from = fst B≤A;
        to-monic = snd A≤B;
        from-monic = snd B≤A
      }

    refl' : ∀ {A B} → A bimonic B → A ≤ B
    refl' bi = _bimonic_.to bi , _bimonic_.to-monic bi

    mtrans : ∀ {A B C} → A ≤ B → B ≤ C → A ≤ C
    mtrans (f , p) (g , q) = g ∘ f , ∘-monic q p

-- A functor is a structure-preserving mapping from one category to
-- another.

record Functor
           {cc ch cr dc dh dr}
           (C : Category {cc} {ch} {cr})
           (D : Category {dc} {dh} {dr})
           : Set (cc ⊔ ch ⊔ cr ⊔ dc ⊔ dh ⊔ dr)
       where

  private
    module C = Category C
    module D = Category D

  field semifunctor : Semifunctor C.semigroupoid D.semigroupoid
  open Semifunctor semifunctor public

  field
    id-preserving : ∀ {A} → map (C.id {A}) D.≈ D.id {F A}

  Iso-preserving : ∀ {A B} {f : C.Hom A B} → C.Iso f → D.Iso (map f)
  Iso-preserving {f = f} p =
    record {
      inv = map inv;
      left-inv =
        D.begin
          map inv D.∘ map f  D.≈[ D.sym (∘-preserving inv f) ]
          map (inv C.∘ f)    D.≈[ map-cong left-inv ]
          map C.id           D.≈[ id-preserving ]
          D.id
        D.qed;
      right-inv =
        D.begin
          map f D.∘ map inv  D.≈[ D.sym (∘-preserving f inv) ]
          map (f C.∘ inv)    D.≈[ map-cong right-inv ]
          map C.id           D.≈[ id-preserving ]
          D.id
        D.qed
    }

    where
    open Category.Iso p

-- Category of types and functions.

Sets : ∀ {r} → Category
Sets {r} =
  record {
    semigroupoid = record {
      Ob = Set r;
      Hom = λ A B → A → B;
      Eq = λ {A B} → FuncEq A B;
      _∘_ = _∘_;
      ∘-cong = ∘-cong;
      assoc = λ _ _ _ _ → PropEq.refl
    };
    id = λ x → x;
    left-id = λ _ _ → PropEq.refl;
    right-id = λ _ _ → PropEq.refl
  }

  where
  open module MyEquiv {A} {B} = Equiv (FuncEq A B)

  _∘_ : {A B C : Set r} (f : B → C) (g : A → B) → A → C
  (f ∘ g) x = f (g x)

  infixl 6 _∘_

  ∘-cong :
    ∀ {A B C}
      {f1 f2 : B → C} {g1 g2 : A → B}
    → f1 ≈ f2 → g1 ≈ g2 → f1 ∘ g1 ≈ f2 ∘ g2
  ∘-cong {f1 = f1} f1≈f2 g1≈g2 x =
    PropEq.trans (cong f1 (g1≈g2 _)) (f1≈f2 _)

module Sets {r} = Category (Sets {r})

injective→monic :
  ∀ {a} {A B : Set a}
    {f : A → B}
  → (∀ {x y} → f x ≡ f y → x ≡ y)
  → Sets.Monic f
injective→monic inj p x = inj (p x)

monic→injective :
  ∀ {a} {A B : Set a}
    {f : A → B}
  → Sets.Monic f
  → ∀ {x y} → f x ≡ f y → x ≡ y
monic→injective monic p = monic Sets.id p

surjective→epic :
  ∀ {a} {A B : Set a}
    {f : A → B}
  → (∀ y → ∃ (λ x → f x ≡ y))
  → Sets.Epic f
surjective→epic {f = f} surj {g1 = g1} {g2} p y with surj y
surjective→epic {f = f} surj {g1 = g1} {g2} p y | x , q =
  begin
    g1 y      ≈[ cong g1 (sym q) ]
    g1 (f x)  ≈[ p x ]
    g2 (f x)  ≈[ cong g2 q ]
    g2 y
  qed

  where
  open module MyEquiv {A} = Equiv (PropEq A)

ext: agda

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


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

Properties of nullary relations, i.e. structures on types.

Includes several results from [Notions of Anonymous Existence in Martin-Löf Type Theory](https://lmcs.episciences.org/3217)
by Altenkirch, Coquand, Escardo, Kraus.

-}
module Cubical.Relation.Nullary.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Fixpoint

open import Cubical.Data.Empty as ⊥

open import Cubical.Relation.Nullary.Base
open import Cubical.HITs.PropositionalTruncation.Base

private
  variable
    ℓ : Level
    A : Type ℓ

IsoPresDiscrete : ∀ {ℓ ℓ'}{A : Type ℓ} {B : Type ℓ'} → Iso A B
               → Discrete A → Discrete B
IsoPresDiscrete e dA x y with dA (Iso.inv e x) (Iso.inv e y)
... | yes p = subst Dec (λ i → Iso.rightInv e x i ≡ Iso.rightInv e y i)
                        (yes (cong (Iso.fun e) p))
... | no p = subst Dec (λ i → Iso.rightInv e x i ≡ Iso.rightInv e y i)
                   (no λ q → p (sym (Iso.leftInv e (Iso.inv e x))
                     ∙∙ cong (Iso.inv e) q
                     ∙∙ Iso.leftInv e (Iso.inv e y)))

EquivPresDiscrete : ∀ {ℓ ℓ'}{A : Type ℓ} {B : Type ℓ'} → A ≃ B
               → Discrete A → Discrete B
EquivPresDiscrete e = IsoPresDiscrete (equivToIso e)

isProp¬ : (A : Type ℓ) → isProp (¬ A)
isProp¬ A p q i x = isProp⊥ (p x) (q x) i

Stable¬ : Stable (¬ A)
Stable¬ ¬¬¬a a = ¬¬¬a ¬¬a
  where
  ¬¬a = λ ¬a → ¬a a

fromYes : A → Dec A → A
fromYes _ (yes a) = a
fromYes a (no _) = a

discreteDec : (Adis : Discrete A) → Discrete (Dec A)
discreteDec Adis (yes p) (yes p') = decideYes (Adis p p') -- TODO: monad would simply stuff
  where
    decideYes : Dec (p ≡ p') → Dec (yes p ≡ yes p')
    decideYes (yes eq) = yes (cong yes eq)
    decideYes (no ¬eq) = no λ eq → ¬eq (cong (fromYes p) eq)
discreteDec Adis (yes p) (no ¬p) = ⊥.rec (¬p p)
discreteDec Adis (no ¬p) (yes p) = ⊥.rec (¬p p)
discreteDec {A = A} Adis (no ¬p) (no ¬p') = yes (cong no (isProp¬ A ¬p ¬p'))

isPropDec : (Aprop : isProp A) → isProp (Dec A)
isPropDec Aprop (yes a) (yes a') = cong yes (Aprop a a')
isPropDec Aprop (yes a) (no ¬a) = ⊥.rec (¬a a)
isPropDec Aprop (no ¬a) (yes a) = ⊥.rec (¬a a)
isPropDec {A = A} Aprop (no ¬a) (no ¬a') = cong no (isProp¬ A ¬a ¬a')

mapDec : ∀ {B : Type ℓ} → (A → B) → (¬ A → ¬ B) → Dec A → Dec B
mapDec f _ (yes p) = yes (f p)
mapDec _ f (no ¬p) = no (f ¬p)

EquivPresDec : ∀ {ℓ ℓ'}{A : Type ℓ} {B : Type ℓ'} → A ≃ B
          → Dec A → Dec B
EquivPresDec p = mapDec (p .fst) (λ f → f ∘ invEq p)

¬→¬∥∥ : ¬ A → ¬ ∥ A ∥
¬→¬∥∥ ¬p ∣ a ∣ = ¬p a
¬→¬∥∥ ¬p (squash x y i) = isProp⊥ (¬→¬∥∥ ¬p x) (¬→¬∥∥ ¬p y) i

Dec∥∥ : Dec A → Dec ∥ A ∥
Dec∥∥ = mapDec ∣_∣ ¬→¬∥∥

-- we have the following implications
-- X ── ∣_∣ ─→ ∥ X ∥
-- ∥ X ∥ ── populatedBy ─→ ⟪ X ⟫
-- ⟪ X ⟫ ── notEmptyPopulated ─→ NonEmpty X

-- reexport propositional truncation for uniformity
open Cubical.HITs.PropositionalTruncation.Base
  using (∣_∣) public

populatedBy : ∥ A ∥ → ⟪ A ⟫
populatedBy {A = A} a (f , fIsConst) = h a where
  h : ∥ A ∥ → Fixpoint f
  h ∣ a ∣ = f a , fIsConst (f a) a
  h (squash a b i) = 2-Constant→isPropFixpoint f fIsConst (h a) (h b) i

notEmptyPopulated : ⟪ A ⟫ → NonEmpty A
notEmptyPopulated {A = A} pop u = u (fixpoint (pop (h , hIsConst))) where
  h : A → A
  h a = ⊥.elim (u a)
  hIsConst : ∀ x y → h x ≡ h y
  hIsConst x y i = ⊥.elim (isProp⊥ (u x) (u y) i)

-- these implications induce the following for different kinds of stability, gradually weakening the assumption
Dec→Stable : Dec A → Stable A
Dec→Stable (yes x) = λ _ → x
Dec→Stable (no x) = λ f → ⊥.elim (f x)

Stable→PStable : Stable A → PStable A
Stable→PStable st = st ∘ notEmptyPopulated

PStable→SplitSupport : PStable A → SplitSupport A
PStable→SplitSupport pst = pst ∘ populatedBy

-- Although SplitSupport and Collapsible are not properties, their path versions, HSeparated and Collapsible≡, are.
-- Nevertheless they are logically equivalent
SplitSupport→Collapsible : SplitSupport A → Collapsible A
SplitSupport→Collapsible {A = A} hst = h , hIsConst where
  h : A → A
  h p = hst ∣ p ∣
  hIsConst : 2-Constant h
  hIsConst p q i = hst (squash ∣ p ∣ ∣ q ∣ i)

Collapsible→SplitSupport : Collapsible A → SplitSupport A
Collapsible→SplitSupport f x = fixpoint (populatedBy x f)

HSeparated→Collapsible≡ : HSeparated A → Collapsible≡ A
HSeparated→Collapsible≡ hst x y = SplitSupport→Collapsible (hst x y)

Collapsible≡→HSeparated : Collapsible≡ A → HSeparated A
Collapsible≡→HSeparated col x y = Collapsible→SplitSupport (col x y)

-- stability of path space under truncation or path collapsability are necessary and sufficient properties
-- for a a type to be a set.
Collapsible≡→isSet : Collapsible≡ A → isSet A
Collapsible≡→isSet {A = A} col a b p q = p≡q where
  f : (x : A) → a ≡ x → a ≡ x
  f x = col a x .fst
  fIsConst : (x : A) → (p q : a ≡ x) → f x p ≡ f x q
  fIsConst x = col a x .snd
  rem : (p : a ≡ b) → PathP (λ i → a ≡ p i) (f a refl) (f b p)
  rem p j = f (p j) (λ i → p (i ∧ j))
  p≡q : p ≡ q
  p≡q j i = hcomp (λ k → λ { (i = i0) → f a refl k
                           ; (i = i1) → fIsConst b p q j k
                           ; (j = i0) → rem p i k
                           ; (j = i1) → rem q i k }) a

HSeparated→isSet : HSeparated A → isSet A
HSeparated→isSet = Collapsible≡→isSet ∘ HSeparated→Collapsible≡

isSet→HSeparated : isSet A → HSeparated A
isSet→HSeparated setA x y = extract where
  extract : ∥ x ≡ y ∥ → x ≡ y
  extract ∣ p ∣ = p
  extract (squash p q i) = setA x y (extract p) (extract q) i

-- by the above more sufficient conditions to inhibit isSet A are given
PStable≡→HSeparated : PStable≡ A → HSeparated A
PStable≡→HSeparated pst x y = PStable→SplitSupport (pst x y)

PStable≡→isSet : PStable≡ A → isSet A
PStable≡→isSet = HSeparated→isSet ∘ PStable≡→HSeparated

Separated→PStable≡ : Separated A → PStable≡ A
Separated→PStable≡ st x y = Stable→PStable (st x y)

Separated→isSet : Separated A → isSet A
Separated→isSet = PStable≡→isSet ∘ Separated→PStable≡

-- Proof of Hedberg's theorem: a type with decidable equality is an h-set
Discrete→Separated : Discrete A → Separated A
Discrete→Separated d x y = Dec→Stable (d x y)

Discrete→isSet : Discrete A → isSet A
Discrete→isSet = Separated→isSet ∘ Discrete→Separated

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


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

module Categories.Category.Instance.Properties.Setoids where

open import Categories.Category.Instance.Properties.Setoids.Complete
  using (Setoids-Complete)
  public

open import Categories.Category.Instance.Properties.Setoids.Cocomplete
  using (Setoids-Cocomplete)
  public

open import Categories.Category.Instance.Properties.Setoids.LCCC
  using (Setoids-LCCC)
  public


text:
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.ABox.Interp using ( _*_ ; ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _,_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; on-bnode ; bnodes ; ⊨a-resp-≲ ; ⊨a-resp-≡³ ; _,_ )
open import Web.Semantic.DL.Category.Object using
  ( Object ; IN ; iface )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; BN ; impl ; _≣_ ; _⊑_ ; _,_ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-right ; compose-resp-⊨a )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( ≲-refl )
open import Web.Semantic.Util using
  ( _∘_ ; _⊕_⊕_ ; False ; inode ; bnode ; enode ; left ; right )

module Web.Semantic.DL.Category.Properties.Composition.Assoc
  {Σ : Signature} {S T : TBox Σ} where

compose-assoc : ∀ {A B C D : Object S T} (F : A ⇒ B) (G : B ⇒ C) (H : C ⇒ D) →
  ((F ∙ G) ∙ H ≣ F ∙ (G ∙ H))
compose-assoc {A} {B} {C} {D} F G H = (LHS⊑RHS , RHS⊑LHS) where

  LHS⊑RHS : (F ∙ G) ∙ H ⊑ F ∙ (G ∙ H)
  LHS⊑RHS I I⊨STA I⊨LHS = (f , I⊨RHS) where

    f : (BN F ⊕ IN B ⊕ (BN G ⊕ IN C ⊕ BN H)) → Δ ⌊ I ⌋
    f (inode u) = ind I (bnode (inode (inode u)))
    f (bnode y) = ind I (bnode (inode (bnode y)))
    f (enode (inode v)) = ind I (bnode (inode (enode v)))
    f (enode (bnode z)) = ind I (bnode (bnode z))
    f (enode (enode w)) = ind I (bnode (enode w))

    I⊨F : left * bnodes I f ⊨a impl F
    I⊨F = ⊨a-resp-≡³ (left * left * I) (on-bnode f (ind I) ∘ left) refl
      (impl F) (compose-left F G (left * I) (compose-left (F ∙ G) H I I⊨LHS))

    I⊨G : left * right * bnodes I f ⊨a impl G
    I⊨G = ⊨a-resp-≡³ (right * left * I) (on-bnode f (ind I) ∘ right ∘ left) refl
      (impl G) (compose-right F G (left * I) (compose-left (F ∙ G) H I I⊨LHS))

    I⊨H : right * right * bnodes I f ⊨a impl H
    I⊨H = ⊨a-resp-≡³ (right * I) (on-bnode f (ind I) ∘ right ∘ right) refl
      (impl H) (compose-right (F ∙ G) H I I⊨LHS)

    I⊨RHS : bnodes I f ⊨a impl (F ∙ (G ∙ H))
    I⊨RHS = compose-resp-⊨a F (G ∙ H) (bnodes I f) I⊨F
      (compose-resp-⊨a G H (right * bnodes I f) I⊨G I⊨H)

  RHS⊑LHS : F ∙ (G ∙ H) ⊑ (F ∙ G) ∙ H
  RHS⊑LHS I I⊨STA I⊨RHS = (f , I⊨LHS) where

    f : ((BN F ⊕ IN B ⊕ BN G) ⊕ IN C ⊕ BN H) → Δ ⌊ I ⌋
    f (inode (inode u)) = ind I (bnode (inode u))
    f (inode (bnode y)) = ind I (bnode (bnode y))
    f (inode (enode v)) = ind I (bnode (enode (inode v)))
    f (bnode z) = ind I (bnode (enode (bnode z)))
    f (enode w) = ind I (bnode (enode (enode w)))

    I⊨F : left * left * bnodes I f ⊨a impl F
    I⊨F = ⊨a-resp-≡³ (left * I) (on-bnode f (ind I) ∘ left ∘ left) refl
      (impl F) (compose-left F (G ∙ H) I I⊨RHS)

    I⊨G : right * left * bnodes I f ⊨a impl G
    I⊨G = ⊨a-resp-≡³ (left * right * I) (on-bnode f (ind I) ∘ left ∘ right) refl
      (impl G) (compose-left G H (right * I) (compose-right F (G ∙ H) I I⊨RHS))

    I⊨H : right * bnodes I f ⊨a impl H
    I⊨H = ⊨a-resp-≡³ (right * right * I) (on-bnode f (ind I) ∘ right) refl
      (impl H) (compose-right G H (right * I) (compose-right F (G ∙ H) I I⊨RHS))

    I⊨LHS : bnodes I f ⊨a impl ((F ∙ G) ∙ H)
    I⊨LHS = compose-resp-⊨a (F ∙ G) H (bnodes I f)
      (compose-resp-⊨a F G (left * bnodes I f) I⊨F I⊨G) I⊨H

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module Esterel.Variable.Shared where

open import Data.Nat
  using (ℕ) renaming (_≟_ to _≟ℕ_)
open import Function
  using (_∘_)
open import Relation.Nullary
  using (Dec ; yes ; no ; ¬_)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; trans ; sym)

data SharedVar : Set where
  _ₛₕ : ℕ → SharedVar

unwrap : SharedVar → ℕ
unwrap (n ₛₕ) = n

unwrap-inverse : ∀ {s} → (unwrap s) ₛₕ ≡ s
unwrap-inverse {_ ₛₕ} = refl

unwrap-injective : ∀ {s t} → unwrap s ≡ unwrap t → s ≡ t
unwrap-injective s'≡t' = trans (sym unwrap-inverse) (trans (cong _ₛₕ s'≡t') unwrap-inverse)

-- for backward compatibility
unwrap-neq : ∀{k1 : SharedVar} → ∀{k2 : SharedVar} → ¬ k1 ≡ k2 → ¬ (unwrap k1) ≡ (unwrap k2)
unwrap-neq = (_∘ unwrap-injective)

wrap : ℕ → SharedVar
wrap = _ₛₕ

bijective : ∀{x} → unwrap (wrap x) ≡ x
bijective = refl

_≟_ : Decidable {A = SharedVar} _≡_
(s ₛₕ) ≟ (t ₛₕ) with s ≟ℕ t
... | yes p = yes (cong _ₛₕ p)
... | no ¬p = no (¬p ∘ cong unwrap)

data Status : Set where
  ready : Status
  new  : Status
  old : Status

_≟ₛₜ_ : Decidable {A = Status} _≡_
ready ≟ₛₜ ready = yes refl
ready ≟ₛₜ new   = no λ()
ready ≟ₛₜ old   = no λ()
new   ≟ₛₜ ready = no λ()
new   ≟ₛₜ new   = yes refl
new   ≟ₛₜ old   = no λ()
old   ≟ₛₜ ready = no λ()
old   ≟ₛₜ new   = no λ()
old   ≟ₛₜ old   = yes refl

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
open import Relation.Binary using (IsDecEquivalence)
open import Agda.Builtin.Equality

module UnifyMguL (A : Set) ⦃ isDecEquivalenceA : IsDecEquivalence (_≡_ {A = A}) ⦄ where

open import UnifyTermL A

open import Data.Product using (∃; _,_)
open import Data.Maybe using (Maybe; just; nothing)
open import Category.Monad using (RawMonad)
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

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

open IsDecEquivalence isDecEquivalenceA

amgu : ∀ {m} (s t : Term m) (acc : ∃ (AList m)) -> Maybe (∃ (AList m))
amgu (leaf l₁) (leaf l₂) acc with l₁ ≟ l₂
… | yes _ = just acc
… | no _ = nothing
amgu (leaf l) (s' fork t') acc = nothing
amgu (s' fork t') (leaf l) acc = nothing
amgu (s1 fork s2) (t1 fork t2) acc =
                  amgu s2 t2 =<< amgu s1 t1 acc
amgu (i x) (i y) (m , anil) = just (flexFlex x y)
amgu (i x) t     (m , anil) = flexRigid x t
amgu t     (i x) (m , anil) = flexRigid x t
amgu s     t  (n , σ asnoc r / z) =
         (λ σ -> σ ∃asnoc r / z) <$>
           amgu ((r for z) ◃ s) ((r for z) ◃ t) (n , σ)

mgu : ∀ {m} -> (s t : Term m) -> Maybe (∃ (AList m))
mgu {m} s t = amgu s t (m , anil)


text:
module Proof.Setup where

import LF
import IIRD
import IIRDr
import DefinitionalEquality
import Identity

open LF
open IIRD
open IIRDr
open DefinitionalEquality
open Identity

-- Given a code for a general IIRD we should give a code for a restricted IIRD.
ε : {I : Set}{D : I -> Set1} -> OPg I D -> OPr I D
ε {I}{D} (ι < j | e >') = \i -> σ (j == i) \p -> ι (subst₁ D p e)
ε        (σ A γ)        = \i -> σ A   \a -> ε (γ a) i
ε        (δ A j γ)      = \i -> δ A j \g -> ε (γ g) i

G→H : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
           (a : Gu γ U T) ->
           Hu (ε γ) U T (Gi γ U T a)
G→H (ι < i | e >') U T ★         = < refl | ★ >
G→H (σ A γ)        U T < a | b > = < a | G→H (γ a) U T b >
G→H (δ A i γ)      U T < g | b > = < g | G→H (γ (T « i × g »)) U T b >

H→G : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
    (i : I) -> Hu (ε γ) U T i -> Gu γ U T
H→G (ι < j | e >') U T i < p | ★ > = ★
H→G (σ A γ)        U T i < a | b > = < a | H→G (γ a) U T i b >
H→G (δ A j γ)      U T i < g | b > = < g | H→G (γ (T « j × g »)) U T i b >

-- We can turn an inductive argument of the general IIRD to an inductive
-- argument of the restricted version.

H→G∘G→H-identity : {I : Set}{D : I -> Set1}
                   (γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                   (a : Gu γ U T) ->
                   H→G γ U T (Gi γ U T a) (G→H γ U T a) ≡ a
H→G∘G→H-identity (ι < i | e >') U T ★         = refl-≡
H→G∘G→H-identity (σ A γ)        U T < a | b > = cong-≡ (\z -> < a | z >) (H→G∘G→H-identity (γ a) U T b)
H→G∘G→H-identity (δ A i γ)      U T < g | b > = cong-≡ (\z -> < g | z >)
                                                       (H→G∘G→H-identity (γ (T « i × g »)) U T b)
{-
Gi∘H→G-identity : {I : Set}{D : I -> Set1}
                  (γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                  (i : I)(b : Hu (ε γ) U T i) ->
                  Gi γ U T (H→G γ U T i b) == i
Gi∘H→G-identity (ι < j | e >') U T i < p | ★ > = p
Gi∘H→G-identity (σ A γ)        U T i < a | b > = Gi∘H→G-identity (γ a) U T i b
Gi∘H→G-identity (δ A j γ)      U T i < g | b > = Gi∘H→G-identity (γ (T « j × g »)) U T i b

Gt∘H→G-identity : {I : Set}{D : I -> Set1}
                  (γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                  (i : I)(b : Hu (ε γ) U T i) ->
                  Gt γ U T (H→G γ U T i b) ≡₁ Ht (ε γ) U T i b
Gt∘H→G-identity γ U T i b = ?

-- This one ain't true! p ≢ refl : x == y
G→H∘H→G-identity : {I : Set}{D : I -> Set1}
                   (γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                   (i : I)(b : Hu (ε γ) U T i) ->
                   G→H γ U T (H→G γ U T i b) ≡ b
G→H∘H→G-identity (ι < j | e >') U T i < p | ★ > = ?
G→H∘H→G-identity (σ A γ)        U T i < a | b > = ?
G→H∘H→G-identity (δ A j γ)      U T i < g | b > = ?
-}

-- Rather than proving equalities (which doesn't hold anyway) we provide
-- substitution rules.
G→H∘H→G-subst : {I : Set}{D : I -> Set1}
                (γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                (F : (i : I)(a : Hu (ε γ) U T i) -> Set1)
                (i : I)(a : Hu (ε γ) U T i)
                (h : F (Gi γ U T (H→G γ U T i a)) (G→H γ U T (H→G γ U T i a))) ->
                F i a
G→H∘H→G-subst (ι < j | e >') U T F i < p | ★ > h = elim==₁ j (\z q -> F z < q | ★ >) h i p
G→H∘H→G-subst (σ A γ)        U T F i < a | b > h =
  G→H∘H→G-subst (γ a) U T (\j c -> F j < a | c >) i b h
G→H∘H→G-subst (δ A j γ)      U T F i < g | b > h =
  G→H∘H→G-subst (γ (T « j × g »)) U T (\j c -> F j < g | c >) i b h

-- Q. When can we remove a G→H∘H→G-subst ?
-- A. When a = G→H γ U T i a'
G→H∘H→G-identity : {I : Set}{D : I -> Set1}
                   (γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                   (F : (i : I)(a : Hu (ε γ) U T i) -> Set1)
                   (a : Gu γ U T)
                   (h : F (Gi γ U T (H→G γ U T (Gi γ U T a) (G→H γ U T a)))
                          (G→H γ U T (H→G γ U T (Gi γ U T a) (G→H γ U T a)))
                   ) ->
                   G→H∘H→G-subst γ U T F (Gi γ U T a) (G→H γ U T a) h ≡₁ h
G→H∘H→G-identity (ι < i | e >') U T F ★ h = refl-≡₁
G→H∘H→G-identity (σ A γ) U T F < a | b > h =
  G→H∘H→G-identity (γ a) U T (\j  c -> F j < a | c >) b h
G→H∘H→G-identity (δ A i γ) U T F < g | b > h =
  G→H∘H→G-identity (γ (T « i × g »)) U T (\j c -> F j < g | c >) b h

εIArg : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
        (i : I)(a : Hu (ε γ) U T i) ->
        KIArg γ U T (H→G γ U T i a) -> KIArg (ε γ i) U T a
εIArg (ι < j | e >') U T i < h | ★ > ()
εIArg (σ A γ)        U T i < a | b > v       = εIArg (γ a) U T i b v
εIArg (δ A j γ)      U T i < g | b > (inl a) = inl a
εIArg (δ A j γ)      U T i < g | b > (inr v) = inr (εIArg (γ (T « j × g »)) U T i b v)

εIArg→I-identity : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                   (i : I)(a : Hu (ε γ) U T i)(v : KIArg γ U T (H→G γ U T i a)) ->
                   KIArg→I (ε γ i) U T a (εIArg γ U T i a v)
                   ≡ KIArg→I γ U T (H→G γ U T i a) v
εIArg→I-identity (ι < j | e >') U T i < p | ★ > ()
εIArg→I-identity (σ A γ)        U T i < a | b > v       = εIArg→I-identity (γ a) U T i b v
εIArg→I-identity (δ A j γ)      U T i < g | b > (inl a) = refl-≡
εIArg→I-identity (δ A j γ)      U T i < g | b > (inr v) = εIArg→I-identity (γ (T « j × g »)) U T i b v

εIArg→U-identity : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                   (i : I)(a : Hu (ε γ) U T i)(v : KIArg γ U T (H→G γ U T i a)) ->
                   KIArg→U (ε γ i) U T a (εIArg γ U T i a v)
                   ≡ KIArg→U γ U T (H→G γ U T i a) v
εIArg→U-identity (ι < j | e >') U T i < p | ★ > ()
εIArg→U-identity (σ A γ)        U T i < a | b > v       = εIArg→U-identity (γ a) U T i b v
εIArg→U-identity (δ A j γ)      U T i < g | b > (inl a) = refl-≡
εIArg→U-identity (δ A j γ)      U T i < g | b > (inr v) = εIArg→U-identity (γ (T « j × g »)) U T i b v

εIArg-subst : {I : Set}{D : I -> Set1}(γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
              (F : (i : I)(u : U i) -> Set1)
              (i : I)(a : Hu (ε γ) U T i)(v : KIArg γ U T (H→G γ U T i a)) ->
              F (KIArg→I (ε γ i) U T a (εIArg γ U T i a v))
                (KIArg→U (ε γ i) U T a (εIArg γ U T i a v)) ->
              F (KIArg→I γ U T (H→G γ U T i a) v)
                (KIArg→U γ U T (H→G γ U T i a) v)
εIArg-subst (ι < j | e >') U T F i < p | ★ > ()      h
εIArg-subst (σ A γ)        U T F i < a | b > v       h = εIArg-subst (γ a) U T F i b v h
εIArg-subst (δ A j γ)      U T F i < g | b > (inl a) h = h
εIArg-subst (δ A j γ)      U T F i < g | b > (inr v) h = εIArg-subst (γ (T « j × g »)) U T F i b v h

εIArg-identity : {I : Set}{D : I -> Set1}
                 (γ : OPg I D)(U : I -> Set)(T : (i : I) -> U i -> D i)
                 (F : (i : I)(u : U i) -> Set1)
                 (a : Gu γ U T)
                 (v : KIArg γ U T (H→G γ U T (Gi γ U T a) (G→H γ U T a)))
                 (h : F (KIArg→I (ε γ (Gi γ U T a)) U T (G→H γ U T a) (εIArg γ U T (Gi γ U T a) (G→H γ U T a) v))
                        (KIArg→U (ε γ (Gi γ U T a)) U T (G→H γ U T a) (εIArg γ U T (Gi γ U T a) (G→H γ U T a) v))
                 ) ->
                 εIArg-subst γ U T F (Gi γ U T a) (G→H γ U T a) v h ≡₁ h
εIArg-identity (ι < i | e >') U T F ★         ()      h
εIArg-identity (σ A γ)        U T F < a | b > v       h = εIArg-identity (γ a) U T F b v h
εIArg-identity (δ A i γ)      U T F < g | b > (inl a) h = refl-≡₁
εIArg-identity (δ A i γ)      U T F < g | b > (inr v) h = εIArg-identity (γ (T « i × g »)) U T F b v h

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- I decided that I wanted my Eq development to be separate from my HT one,
-- which means that I prove Kleene is reflexive through logical equivalence
-- being reflexive

module Eq.KleeneTheoryEarly where

open import Prelude
open import T
open import DynTheory
open import Eq.Defs

-- Theory about Kleene equality

kleene-sym : Symmetric KleeneEq
kleene-sym (kleeneq n val S1 S2) = kleeneq n val S2 S1

kleene-trans : Transitive KleeneEq
kleene-trans {z = e''} (kleeneq n val e-eval e'-eval) (kleeneq n' val' e'-eval2  e''-eval)
   with eval-deterministic e'-eval e'-eval2 val val'
... | eq = kleeneq _ val e-eval (ID.coe1 (λ x → e'' ~>* x) (symm eq) e''-eval)

kleene-converse-evaluation : ∀{e e' d : TNat} →
                             e ≃ e' → d ~>* e → d ≃ e'
kleene-converse-evaluation (kleeneq n val S1 S2) eval =
  kleeneq n val (eval-trans eval S1) S2

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
open import Functional hiding (Domain)
import      Structure.Logic.Classical.NaturalDeduction
import      Structure.Logic.Classical.SetTheory.ZFC

module Structure.Logic.Classical.SetTheory.ZFC.FunctionSet {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) ⦃ signature : _ ⦄ where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)
open Structure.Logic.Classical.SetTheory.ZFC.Signature {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic ⦄ {_∈_} (signature)

open import Structure.Logic.Classical.SetTheory.SetBoundedQuantification ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Classical.SetTheory.ZFC.BinaryRelatorSet     ⦃ classicLogic ⦄ (_∈_) ⦃ signature ⦄

-- The set s can be interpreted as a function.
FunctionSet : Domain → Formula
FunctionSet(s) = ∀ₗ(x ↦ Unique(y ↦ (x , y) ∈ s))
-- TODO: Maybe also define something that states ∀ₗ(x ↦ (x ∈ A) ↔ ∃ₗ(y ↦ (x , y) ∈ s)) so that a set representation of a function with domains becomes unique? But I think when (s ∈ (B ^ A)) is satisfied, this is implied? So try to prove that (FunctionSet(f) ∧ Total(A)(f) ∧ (the thing I mentioned earlier)) ↔ (f ∈ (B ^ A))

-- The set s can be interpreted as a function with a specified domain.
-- The following describes the relation to the standard notation of functions:
-- • ∀(x∊A)∀y. ((x,y) ∈ S) ⇔ (S(x) = y)
Total : Domain → Domain → Formula
Total(A)(s) = ∀ₛ(A)(x ↦ ∃ₗ(y ↦ (x , y) ∈ s))

Injective' : Domain → Formula
Injective'(f) = ∀ₗ(y ↦ Unique(x ↦ (x , y) ∈ f))

Surjective' : Domain → Domain → Formula
Surjective'(B)(f) = ∀ₛ(B)(y ↦ ∃ₗ(x ↦ (x , y) ∈ f))

Bijective' : Domain → Domain → Formula
Bijective'(B)(f) =
  Injective'(f)
  ∧ Surjective'(B)(f)

-- The set of total function sets. All sets which can be interpreted as a total function.
_^_ : Domain → Domain → Domain
B ^ A = filter(℘(A ⨯ B)) (f ↦ FunctionSet(f) ∧ Total(A)(f))

_→ₛₑₜ_ = swap _^_

⊷ : Domain → Domain
⊷ = lefts

⊶ : Domain → Domain
⊶ = rights

map' : Domain → Domain → Domain
map' = rightsOfMany

unmap' : Domain → Domain → Domain
unmap' = leftsOfMany

apply-set : Domain → Domain → Domain
apply-set = rightsOf

unapply-set : Domain → Domain → Domain
unapply-set = leftsOf

_∘'_ : Domain → Domain → Domain
_∘'_ f g = filter((⊷ f) ⨯ (⊶ g)) (a ↦ ∃ₗ(x ↦ ∃ₗ(y ↦ ∃ₗ(a₁ ↦ ((a₁ , y) ∈ f) ∧ ((x , a₁) ∈ g)) ∧ (a ≡ (x , y)))))

-- inv : Domain → Domain
-- inv f = filter(?) (yx ↦ ∃ₗ(x ↦ ∃ₗ(y ↦ ((x , y) ∈ f) ∧ (yx ≡ (y , x)))))

module Cardinality where
  -- Injection
  _≼_ : Domain → Domain → Formula
  _≼_ (a)(b) = ∃ₛ(a →ₛₑₜ b)(Injective')

  -- Surjection
  _≽_ : Domain → Domain → Formula
  _≽_ (a)(b) = ∃ₛ(a →ₛₑₜ b)(Surjective'(b))

  -- Bijection
  _≍_ : Domain → Domain → Formula
  _≍_ (a)(b) = ∃ₛ(a →ₛₑₜ b)(Bijective'(b))

  -- Strict injection
  _≺_ : Domain → Domain → Formula
  _≺_ A B = (A ≼ B) ∧ ¬(A ≍ B)

  -- Strict surjection
  _≻_ : Domain → Domain → Formula
  _≻_ A B = (A ≽ B) ∧ ¬(A ≍ B)

  -- TODO: Definition of a "cardinality object" requires ordinals, which requires axiom of choice
  -- # : Domain → Domain

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:
import AssocFree.STLambdaC.Typ
import AssocFree.STLambdaC.Exp

module AssocFree.STLambdaC.NF
  (TConst : Set)
  (Const : AssocFree.STLambdaC.Typ.Typ TConst → Set) where

open module Typ = AssocFree.STLambdaC.Typ TConst using
  ( Typ ; Ctxt ; const ; _⇝_ ; [_] ; [] ; _∷_ ; _++_ ; case ; singleton ; _≪_ )

open module Exp = AssocFree.STLambdaC.Exp TConst Const using
  ( Exp ; const ; abs ; app ; var ; var₀ ; weaken+ ; weaken* ; xweaken+ )

mutual

-- Normal forms

  data Atom {Γ : Ctxt} {T : Typ} : Exp Γ T → Set where
    const : ∀ c → Atom (const c)
    var : ∀ x → Atom (var x)
    app : ∀ {U M} {N : Exp Γ U} → Atom M → NF N → Atom (app M N)

  data NF {Γ : Ctxt} : ∀ {T} → Exp Γ T → Set where
    atom : ∀ {C} {M : Exp Γ (const C)} → Atom M → NF M
    abs : ∀ T {U} {M : Exp (T ∷ Γ) U} → NF M → NF (abs {Γ} T M)

-- Shorthand

atom₀ : ∀ {Γ T} → Atom (var₀ {Γ} {T})
atom₀ {Γ} {T} = var (singleton T ≪ Γ)

-- Weakening

mutual

  aweaken+ : ∀ B Γ Δ {T M} → Atom M → Atom (weaken+ B Γ Δ {T} M)
  aweaken+ B Γ Δ (const c) = const c
  aweaken+ B Γ Δ (app M N) = app (aweaken+ B Γ Δ M) (nweaken+ B Γ Δ N)
  aweaken+ B Γ Δ (var x)   = var (xweaken+ B Γ Δ x)

  nweaken+ : ∀ B Γ Δ {T M} → NF M → NF (weaken+ B Γ Δ {T} M)
  nweaken+ B Γ Δ (atom N)   = atom (aweaken+ B Γ Δ N)
  nweaken+ B Γ Δ (abs T N)  = abs T (nweaken+ (T ∷ B) Γ Δ N)

aweaken* : ∀ Γ {Δ T M} → Atom M → Atom (weaken* Γ {Δ} {T} M)
aweaken* Γ {Δ} = aweaken+ [] Γ Δ

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


text:
{-# OPTIONS --warning=error #-}

module Issue278 where

open import Agda.Builtin.Equality

abstract
  module A where
    Foo : Set₁
    Foo = Set
  module B where
    open A
    Foo≡Set : Foo ≡ Set
    Foo≡Set = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Nat using (Nat; zero; suc)
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

variable
  k l m n : Nat

postulate
  max : Nat → Nat → Nat
  max-0l : max 0 n ≡ n
  max-0r : max m 0 ≡ m
  max-diag : max m m ≡ m
  max-ss : max (suc m) (suc n) ≡ suc (max m n)
  max-diag-s : max (suc m) (suc m) ≡ suc m -- for global confluence
  max-assoc : max (max k l) m ≡ max k (max l m)

{-# REWRITE max-0l max-0r #-}
{-# REWRITE max-ss max-diag max-diag-s #-}
--{-# REWRITE max-assoc #-} -- not confluent!

postulate
  _+_ : Nat → Nat → Nat
  plus-0l : 0 + n ≡ n
  plus-0r : m + 0 ≡ m
  plus-00 : 0 + 0 ≡ 0  -- for global confluence
  plus-suc-l : (suc m) + n ≡ suc (m + n)
  plus-suc-0 : (suc m) + 0 ≡ suc m -- for global confluence
  plus-suc-r : m + (suc n) ≡ suc (m + n)
  plus-0-suc : 0 + (suc n) ≡ suc n
  plus-suc-suc : (suc m) + (suc n) ≡ suc (suc (m + n))
  plus-assoc : (k + l) + m ≡ k + (l + m) -- not accepted by global confluence check

{-# REWRITE plus-00 plus-0l plus-0r
            plus-suc-l plus-suc-0
            plus-suc-r plus-0-suc
            plus-suc-suc #-}

postulate
  _*_ : Nat → Nat → Nat
  mult-0l : 0 * n ≡ 0
  mult-0r : m * 0 ≡ 0
  mult-00 : 0 * 0 ≡ 0
  mult-suc-l : (suc m) * n ≡ n + (m * n)
  mult-suc-l-0 : (suc m) * 0 ≡ 0
  mult-suc-r : m * (suc n) ≡ (m * n) + m
  plus-mult-distr-l : k * (l + m) ≡ (k * l) + (k * m)
  plus-mult-distr-r : (k + l) * m ≡ (k * m) + (l * m)
  mult-assoc : (k * l) * m ≡ k * (l * m)

{-# REWRITE mult-0l mult-0r mult-00
            mult-suc-l mult-suc-l-0 #-}
--{-# REWRITE mult-suc-r #-} -- requires rule plus-assoc!
--{-# REWRITE plus-mult-distr-l #-}
--{-# REWRITE plus-mult-distr-r #-}
--{-# REWRITE mult-assoc #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Text.Greek.SBLGNT where

open import Data.List
open import Text.Greek.Bible
open import Text.Greek.SBLGNT.Matt
open import Text.Greek.SBLGNT.Mark
open import Text.Greek.SBLGNT.Luke
open import Text.Greek.SBLGNT.John
open import Text.Greek.SBLGNT.Acts
open import Text.Greek.SBLGNT.Rom
open import Text.Greek.SBLGNT.1Cor
open import Text.Greek.SBLGNT.2Cor
open import Text.Greek.SBLGNT.Gal
open import Text.Greek.SBLGNT.Eph
open import Text.Greek.SBLGNT.Phil
open import Text.Greek.SBLGNT.Col
open import Text.Greek.SBLGNT.1Thess
open import Text.Greek.SBLGNT.2Thess
open import Text.Greek.SBLGNT.1Tim
open import Text.Greek.SBLGNT.2Tim
open import Text.Greek.SBLGNT.Titus
open import Text.Greek.SBLGNT.Phlm
open import Text.Greek.SBLGNT.Heb
open import Text.Greek.SBLGNT.Jas
open import Text.Greek.SBLGNT.1Pet
open import Text.Greek.SBLGNT.2Pet
open import Text.Greek.SBLGNT.1John
open import Text.Greek.SBLGNT.2John
open import Text.Greek.SBLGNT.3John
open import Text.Greek.SBLGNT.Jude
open import Text.Greek.SBLGNT.Rev

books : List (List (Word))
books =
    ΚΑΤΑ-ΜΑΘΘΑΙΟΝ
  ∷ ΚΑΤΑ-ΜΑΡΚΟΝ
  ∷ ΚΑΤΑ-ΛΟΥΚΑΝ
  ∷ ΚΑΤΑ-ΙΩΑΝΝΗΝ
  ∷ ΠΡΑΞΕΙΣ-ΑΠΟΣΤΟΛΩΝ
  ∷ ΠΡΟΣ-ΡΩΜΑΙΟΥΣ
  ∷ ΠΡΟΣ-ΚΟΡΙΝΘΙΟΥΣ-Α
  ∷ ΠΡΟΣ-ΚΟΡΙΝΘΙΟΥΣ-Β
  ∷ ΠΡΟΣ-ΓΑΛΑΤΑΣ
  ∷ ΠΡΟΣ-ΕΦΕΣΙΟΥΣ
  ∷ ΠΡΟΣ-ΦΙΛΙΠΠΗΣΙΟΥΣ
  ∷ ΠΡΟΣ-ΚΟΛΟΣΣΑΕΙΣ
  ∷ ΠΡΟΣ-ΘΕΣΣΑΛΟΝΙΚΕΙΣ-Α
  ∷ ΠΡΟΣ-ΘΕΣΣΑΛΟΝΙΚΕΙΣ-Β
  ∷ ΠΡΟΣ-ΤΙΜΟΘΕΟΝ-Α
  ∷ ΠΡΟΣ-ΤΙΜΟΘΕΟΝ-Β
  ∷ ΠΡΟΣ-ΤΙΤΟΝ
  ∷ ΠΡΟΣ-ΦΙΛΗΜΟΝΑ
  ∷ ΠΡΟΣ-ΕΒΡΑΙΟΥΣ
  ∷ ΙΑΚΩΒΟΥ
  ∷ ΠΕΤΡΟΥ-Α
  ∷ ΠΕΤΡΟΥ-Β
  ∷ ΙΩΑΝΝΟΥ-Α
  ∷ ΙΩΑΝΝΟΥ-Β
  ∷ ΙΩΑΝΝΟΥ-Γ
  ∷ ΙΟΥΔΑ
  ∷ ΑΠΟΚΑΛΥΨΙΣ-ΙΩΑΝΝΟΥ
  ∷ []

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


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

open import Axiom.UniquenessOfIdentityProofs.WithK using (uip)

open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open ≡-Reasoning

open import Level using (Level)
open import Data.Nat using (ℕ)

open import Data.Vec using (Vec)

open import FLA.Axiom.Extensionality.Propositional
open import FLA.Algebra.Structures
open import FLA.Algebra.Properties.Field
open import FLA.Algebra.LinearMap
open import FLA.Algebra.LinearMap.Properties
open import FLA.Algebra.LinearAlgebra
open import FLA.Algebra.LinearAlgebra.Matrix

module FLA.Algebra.LinearAlgebra.Properties.Matrix where

private
  variable
    ℓ : Level
    A : Set ℓ
    m n p q : ℕ
    ⦃ F ⦄ : Field A

-------------------------------------------------------------------------------
--                   M without the inner product proof: Mat↓                   --
-------------------------------------------------------------------------------

private
  data Mat↓_∶_×_ (A : Set ℓ) ⦃ F : Field A ⦄ (m n : ℕ) : Set ℓ where
    ⟦_,_⟧ : (M : n ⊸ m ) → (Mᵀ : m ⊸ n ) → Mat↓ A ∶ m × n

  _·↓_ : ⦃ F : Field A ⦄ → Mat↓ A ∶ m × n → Vec A n → Vec A m
  ⟦ f , a ⟧ ·↓ x = f ·ˡᵐ x

  _ᵀ↓ : ⦃ F : Field A ⦄ → Mat↓ A ∶ m × n → Mat↓ A ∶ n × m
  ⟦ f , a ⟧ ᵀ↓ = ⟦ a , f ⟧

  infixr 20 _·↓_
  infixl 25 _ᵀ↓

  Mat→Mat↓ : ⦃ F : Field A ⦄ → Mat m × n → Mat↓ A ∶ m × n
  Mat→Mat↓ ⟦ M , Mᵀ , p ⟧ = ⟦ M , Mᵀ ⟧

  Mat↓→Mat : ⦃ F : Field A ⦄
        → (Mat↓ : Mat↓ A ∶ m × n)
        → (p : (x : Vec A m) → (y : Vec A n)
              → ⟨ x , Mat↓ ·↓ y ⟩ ≡ ⟨ y , Mat↓ ᵀ↓ ·↓ x ⟩ )
        → Mat m × n
  Mat↓→Mat ⟦ M , Mᵀ ⟧ p = ⟦ M , Mᵀ , p ⟧

  ⟨x,Ay⟩≡⟨y,Aᵀx⟩-UIP : {ℓ : Level} → {A : Set ℓ} → ⦃ F : Field A ⦄
                    → (C : n ⊸ m) → (Cᵀ : m ⊸ n)
                    → (p q : (x : Vec A m) (y : Vec A n)
                            → ⟨ x , C ·ˡᵐ y ⟩ ≡ ⟨ y , Cᵀ ·ˡᵐ x ⟩)
                    → p ≡ q
  ⟨x,Ay⟩≡⟨y,Aᵀx⟩-UIP {m} {n} {ℓ} {A} C Cᵀ p q =
    extensionality (λ x → extensionality (λ y → f C Cᵀ p q x y))
    where
      f : {m n : ℕ}
            → {A : Set ℓ}
            → ⦃ F : Field A ⦄
            → (C : n ⊸ m) → (Cᵀ : m ⊸ n)
            → (p q : (x : Vec A m) (y : Vec A n)
                    → ⟨ x , C ·ˡᵐ y ⟩ ≡ ⟨ y , Cᵀ ·ˡᵐ x ⟩)
            → (x : Vec A m) →  (y : Vec A n) → p x y ≡ q x y
      f C Cᵀ p q (x) (y) = uip (p x y) (q x y)

  Mat↓≡→Mat≡ : ⦃ F : Field A ⦄ → (C D : Mat m × n) → (Mat→Mat↓ C ≡ Mat→Mat↓ D) → C ≡ D
  Mat↓≡→Mat≡ ⟦ C , Cᵀ , p ⟧ ⟦ .C , .Cᵀ , q ⟧ refl rewrite
    ⟨x,Ay⟩≡⟨y,Aᵀx⟩-UIP C Cᵀ p q = refl

-------------------------------------------------------------------------------
--                                Proofs on M                                --
-------------------------------------------------------------------------------

module _ {ℓ : Level} {A : Set ℓ} ⦃ F : Field A ⦄ where
  open Field F

  ᵀᵀ : (B : Mat m × n) → B ᵀ ᵀ ≡ B
  ᵀᵀ B = Mat↓≡→Mat≡ (B ᵀ ᵀ) B (ᵀᵀ↓ B)
    where
      ᵀᵀ↓ : (B : Mat m × n) → Mat→Mat↓ (B ᵀ ᵀ) ≡ Mat→Mat↓ B
      ᵀᵀ↓ ⟦ M , Mᵀ , p ⟧ = refl

  ᵀ-distr-* : (L : Mat m × n) (R : Mat n × p)
            → (L *ᴹ R) ᵀ ≡ (R ᵀ *ᴹ L ᵀ)
  ᵀ-distr-* L R = Mat↓≡→Mat≡ ((L *ᴹ R) ᵀ) (R ᵀ *ᴹ L ᵀ) (ᵀ-distr-*↓ L R)
    where
      ᵀ-distr-*↓ : (L : Mat m × n) (R : Mat n × p)
                → Mat→Mat↓ ((L *ᴹ R) ᵀ) ≡ Mat→Mat↓ (R ᵀ *ᴹ L ᵀ)
      ᵀ-distr-*↓ ⟦ L , Lᵀ , p ⟧ ⟦ R , Rᵀ₁ , q ⟧ = refl

  ᵀ-distr-+ : (L R : Mat m × n) → (L +ᴹ R) ᵀ ≡ L ᵀ +ᴹ R ᵀ
  ᵀ-distr-+ L R = Mat↓≡→Mat≡ ((L +ᴹ R) ᵀ) (L ᵀ +ᴹ R ᵀ) (ᵀ-distr-+↓ L R)
    where
      ᵀ-distr-+↓ : (L R : Mat m × n)
                 → Mat→Mat↓ ((L +ᴹ R) ᵀ) ≡ Mat→Mat↓ (L ᵀ +ᴹ R ᵀ)
      ᵀ-distr-+↓ ⟦ L , Lᵀ , p ⟧ ⟦ R , Rᵀ , q ⟧ = refl

  *ᴹ-distr-+ᴹₗ : (X : Mat m × n) (Y Z : Mat n × p)
               → X *ᴹ (Y +ᴹ Z) ≡ X *ᴹ Y +ᴹ X *ᴹ Z
  *ᴹ-distr-+ᴹₗ X Y Z = Mat↓≡→Mat≡ (X *ᴹ (Y +ᴹ Z)) (X *ᴹ Y +ᴹ X *ᴹ Z)
                              (*ᴹ-distr-+ᴹ↓ₗ X Y Z)
    where
      *ᴹ-distr-+ᴹ↓ₗ : (X : Mat m × n) (Y Z : Mat n × p)
                    → Mat→Mat↓ (X *ᴹ (Y +ᴹ Z)) ≡ Mat→Mat↓ (X *ᴹ Y +ᴹ X *ᴹ Z)
      *ᴹ-distr-+ᴹ↓ₗ ⟦ X , Xᵀ , Xₚ ⟧ ⟦ Y , Yᵀ , Yₚ ⟧ ⟦ Z , Zᵀ , Zₚ ⟧ rewrite
          *ˡᵐ-distr-+ˡᵐₗ X Y Z
        | *ˡᵐ-distr-+ˡᵐᵣ Yᵀ Zᵀ Xᵀ
        = refl

  *ᴹ-distr-+ᴹᵣ : (X Y : Mat m × n) (Z : Mat n × p)
               → (X +ᴹ Y) *ᴹ Z ≡ X *ᴹ Z +ᴹ Y *ᴹ Z
  *ᴹ-distr-+ᴹᵣ X Y Z = Mat↓≡→Mat≡ ((X +ᴹ Y) *ᴹ Z) (X *ᴹ Z +ᴹ Y *ᴹ Z)
                              (*ᴹ-distr-+ᴹ↓ᵣ X Y Z)
    where
      *ᴹ-distr-+ᴹ↓ᵣ : (X Y : Mat m × n) (Z : Mat n × p)
                    → Mat→Mat↓ ((X +ᴹ Y) *ᴹ Z) ≡ Mat→Mat↓ (X *ᴹ Z +ᴹ Y *ᴹ Z)
      *ᴹ-distr-+ᴹ↓ᵣ ⟦ X , Xᵀ , Xₚ ⟧ ⟦ Y , Yᵀ , Yₚ ⟧ ⟦ Z , Zᵀ , Zₚ ⟧ rewrite
          *ˡᵐ-distr-+ˡᵐᵣ X Y Z
        | *ˡᵐ-distr-+ˡᵐₗ Zᵀ Xᵀ Yᵀ
        = refl

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Category.Monad.Monotone.Identity {i}(pre : Preorder i i i) where

open Preorder pre renaming (Carrier to I; _∼_ to _≤_; refl to ≤-refl)

open import Relation.Unary.PredicateTransformer using (Pt)
open import Category.Monad.Monotone pre
open RawMPMonad

Identity : Pt I i
Identity = λ P i → P i

instance
  id-monad : RawMPMonad Identity
  return id-monad px = px
  _≥=_ id-monad c f = f ≤-refl c


text:
-- A variant of LostTypeError.
module LostTypeError2 where

postulate
  Wrap   : (A : Set) → (A → Set) → A → Set
  wrap   : (A : Set) (P : A → Set) (x : A) → P x → Wrap A P x
  rewrap : (A : Set) (P : A → Set) (x : A) → Wrap A P x → Wrap A P x

postulate A : Set

data Box : Set where
  box : A → Box

data Dummy : Set where
  box : Dummy

postulate
  x y : A
  P   : Box → Set
  Px  : P (box x)

bad : Wrap Box P (box y)
bad =
  rewrap _ (λ a → P _) (box y)
   (wrap _ (λ a → P _) (box x) Px)


text:
module InstanceMetaType where

⟨⟩ : {A : Set} {{a : A}} → A
⟨⟩ {{a}} = a

postulate
  A : Set
  instance a : A
  f : (a : A) → Set

test₁ : Set
test₁ = f ⟨⟩

postulate
  B : Set
  b : B
  g : (b : B) → Set

instance
  b' : _
  b' = b

test₂ : Set
test₂ = g ⟨⟩


text:
{-# OPTIONS --safe --without-K #-}
open import Algebra.Bundles using (Group)

module Categories.Category.Construction.GroupAsCategory o {c ℓ} (G : Group c ℓ) where

open import Level

open import Categories.Category.Groupoid

open Group G

-- A group is a groupoid with a single object
open import Categories.Category.Construction.MonoidAsCategory o monoid
  renaming (MonoidAsCategory to GroupAsCategory) public

GroupIsGroupoid : IsGroupoid GroupAsCategory
GroupIsGroupoid = record
  { iso = record
    { isoˡ = inverseˡ _
    ; isoʳ = inverseʳ _
    }
  }

GroupAsGroupoid : Groupoid o c ℓ
GroupAsGroupoid = record { isGroupoid = GroupIsGroupoid }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit

postulate
  putStr : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

F : Set → Set
F A = A → A

data D : Set where
  c₀ : D
  c₁ : F D

f : D → String
f c₀     = "OK\n"
f (c₁ x) = f x

main = putStr (f (c₁ c₀))

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas, 2015-08-27, issue reported by Jesper Cockx

-- {-# OPTIONS -v tc.lhs:10 #-}
-- {-# OPTIONS -v tc:10 #-}
-- {-# OPTIONS -v tc.lhs.imp:100 #-}

data Bool : Set where true false : Bool

T : Set → Bool → Set
T A true = {x : A} → A
T A false = (x : A) → A

test : (A : Set) (b : Bool) → T A b
test A true {x} = x
test A false x = x


text:
module _ where

postulate
  A : Set

data Box : Set where
  box : A → Box

unbox : Box → A
unbox (box {x}) = x


text:
module rename where

open import cedille-types
open import constants
open import ctxt-types
open import free-vars
open import syntax-util
open import general-util

renamectxt : Set
renamectxt = stringset × trie string  {- the trie maps vars to their renamed versions,
                                         and the stringset stores all those renamed versions -}

empty-renamectxt : renamectxt
empty-renamectxt = empty-stringset , empty-trie

renamectxt-contains : renamectxt → string → 𝔹
renamectxt-contains (_ , r) s = trie-contains r s

renamectxt-insert : renamectxt → (s1 s2 : string) → renamectxt
renamectxt-insert (ranr , r) s x = stringset-insert ranr x , trie-insert r s x

renamectxt-single : var → var → renamectxt
renamectxt-single = renamectxt-insert empty-renamectxt

renamectxt-lookup : renamectxt → string → maybe string
renamectxt-lookup (ranr , r) s = trie-lookup r s

renamectxt-remove : renamectxt → string → renamectxt
renamectxt-remove (ranr , r) s with trie-lookup r s
renamectxt-remove (ranr , r) s | nothing = ranr , r
renamectxt-remove (ranr , r) s | just s' = stringset-remove ranr s' , trie-remove r s

renamectxt-in-range : renamectxt → string → 𝔹
renamectxt-in-range (ranr , r) s = stringset-contains ranr s

renamectxt-in-field : renamectxt → string → 𝔹
renamectxt-in-field m s = renamectxt-contains m s || renamectxt-in-range m s

renamectxt-rep : renamectxt → string → string
renamectxt-rep r x with renamectxt-lookup r x
renamectxt-rep r x | nothing = x
renamectxt-rep r x | just x' = x'

eq-var : renamectxt → string → string → 𝔹
eq-var r x y = renamectxt-rep r x =string renamectxt-rep r y

{-# NON_TERMINATING #-}
fresh' : (var → 𝔹) → ℕ → var → var
fresh' bound n base with base ^ ℕ-to-string n
...| x with bound x
...| tt = fresh' bound (suc n) base
...| ff = x

fresh-h : (var → 𝔹) → var → var
fresh-h bound ignored-var = ignored-var
fresh-h bound x =
  if ~ bound x'
    then x'
    else uncurry (fresh' bound) (fresh-split [] (reverse (string-to-𝕃char x')))
  where
  x' = unqual-local x

  to-num : 𝕃 char → ℕ
  to-num [] = 1
  to-num ns = string-to-ℕ0 (𝕃char-to-string ns)

  fresh-split : 𝕃 char → 𝕃 char → ℕ × var
  fresh-split ns [] = to-num ns , ""
  fresh-split ns (c :: cs) with is-digit c
  ...| tt = fresh-split (c :: ns) cs
  ...| ff = to-num ns , 𝕃char-to-string (reverse (c :: cs))

fresh-var : ctxt → var → var
fresh-var = fresh-h ∘' ctxt-binds-var

fresh-var-renamectxt : ctxt → renamectxt → var → var
fresh-var-renamectxt Γ ρ ignored-var = ignored-var
fresh-var-renamectxt Γ ρ x = fresh-h (λ x → ctxt-binds-var Γ x || renamectxt-in-field ρ x) x

fresh-var-new : ctxt → var → var
fresh-var-new Γ ignored-var = fresh-var Γ "x"
fresh-var-new Γ x = fresh-var Γ x

rename-var-if : {ed : exprd} → ctxt → renamectxt → var → ⟦ ed ⟧ → var
rename-var-if Γ ρ y t =
  if is-free-in y t || renamectxt-in-range ρ y then
    fresh-var-renamectxt Γ ρ y
  else
    y

renamectxt-insert* : renamectxt → 𝕃 (var × var) → renamectxt
renamectxt-insert* ρ [] = ρ
renamectxt-insert* ρ ((x , y) :: vs) = renamectxt-insert* (renamectxt-insert ρ x y) vs

max_stars_repo_name: mudathirmahgoub/cedille

max_issues_repo_name: mudathirmahgoub/cedille

max_forks_repo_name: mudathirmahgoub/cedille


text:
------------------------------------------------------------------------
-- Rice's theorem
------------------------------------------------------------------------

open import Equality.Propositional
open import Prelude hiding (const; Decidable)

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Coding         χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms

import Coding.Instances.Nat

-- The theorem is stated and proved under the assumption that a
-- correct self-interpreter can be implemented.

module Rices-theorem
  (eval : Exp)
  (cl-eval : Closed eval)
  (eval₁ : ∀ p v → Closed p → p ⇓ v → apply eval ⌜ p ⌝ ⇓ ⌜ v ⌝)
  (eval₂ : ∀ p v → Closed p → apply eval ⌜ p ⌝ ⇓ v →
           ∃ λ v′ → p ⇓ v′ × v ≡ ⌜ v′ ⌝)
  where

open import H-level.Truncation.Propositional as Trunc hiding (rec)
open import Logical-equivalence using (_⇔_)
open import Tactic.By.Propositional

open import Double-negation equality-with-J
open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Monad equality-with-J

open import Cancellation  χ-ℕ-atoms
open import Compatibility χ-ℕ-atoms
open import Computability χ-ℕ-atoms hiding (_∘_)
open import Constants     χ-ℕ-atoms
open import Deterministic χ-ℕ-atoms
open import Propositional χ-ℕ-atoms
open import Reasoning     χ-ℕ-atoms
open import Termination   χ-ℕ-atoms
open import Values        χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

open import Combinators as χ hiding (id; if_then_else_)
open import Halting-problem
open import Internal-coding

------------------------------------------------------------------------
-- The theorem

-- Definition of "pointwise semantically equivalent".

Pointwise-semantically-equivalent : Closed-exp → Closed-exp → Type
Pointwise-semantically-equivalent e₁ e₂ =
  ∀ e v → semantics [ apply-cl e₁ e ]= v ⇔
          semantics [ apply-cl e₂ e ]= v

-- This relation is symmetric.

symmetric :
  ∀ e₁ e₂ →
  Pointwise-semantically-equivalent e₁ e₂ →
  Pointwise-semantically-equivalent e₂ e₁
symmetric _ _ eq = λ e v → inverse (eq e v)

-- Rice's theorem.

module _
  (P : Closed-exp →Bool)
  (let P′ = proj₁ P)
  (e∈ : Closed-exp)
  (Pe∈ : P′ [ e∈ ]= true)
  (e∉ : Closed-exp)
  (¬Pe∉ : P′ [ e∉ ]= false)
  (resp : ∀ e₁ e₂ {b} →
          Pointwise-semantically-equivalent e₁ e₂ →
          P′ [ e₁ ]= b → P′ [ e₂ ]= b)
  where

  private

    module Helper
      (p : Exp) (cl-p : Closed p)
      (hyp : ∀ e b → P′ [ e ]= b → apply p ⌜ e ⌝ ⇓ ⌜ b ⌝)
      where

      arg : Closed-exp → Closed-exp → Closed-exp
      arg e p =
          lambda v-x
            (apply (lambda v-underscore (apply (proj₁ e) (var v-x)))
                   (apply eval (proj₁ p)))
        , (Closed′-closed-under-lambda $
           Closed′-closed-under-apply
             (Closed′-closed-under-lambda $
              Closed′-closed-under-apply
                (Closed→Closed′ $ proj₂ e)
                (Closed′-closed-under-var (inj₂ (inj₁ refl))))
             (Closed′-closed-under-apply
                (Closed→Closed′ cl-eval)
                (Closed→Closed′ (proj₂ p))))

      coded-arg : Closed-exp → Exp
      coded-arg e =
        const c-lambda (⌜ v-x ⌝ ∷
          const c-apply (
            ⌜ Exp.lambda v-underscore (apply (proj₁ e) (var v-x)) ⌝ ∷
            const c-apply (
              ⌜ eval ⌝ ∷
              apply internal-code (var v-p) ∷
              []) ∷ []) ∷ [])

      branches : List Br
      branches =
        branch c-false [] (apply p (coded-arg e∈)) ∷
        branch c-true  [] (χ.not (apply p (coded-arg e∉))) ∷
        []

      const-loop : Closed-exp
      const-loop =
          lambda v-underscore loop
        , (Closed′-closed-under-lambda $
           Closed→Closed′ loop-closed)

      ⌜const-loop⌝ : Closed-exp
      ⌜const-loop⌝ = ⌜ proj₁ const-loop ⌝

      halts : Exp
      halts =
        lambda v-p (case (apply p (proj₁ ⌜const-loop⌝)) branches)

      cl-coded-arg : ∀ e → Closed′ (v-p ∷ []) (coded-arg e)
      cl-coded-arg e =
        Closed′-closed-under-const λ where
          _ (inj₂ (inj₂ ()))
          _ (inj₁ refl) →
            Closed→Closed′ (rep-closed v-x)
          _ (inj₂ (inj₁ refl)) →
            Closed′-closed-under-const λ where
              _ (inj₂ (inj₂ ()))
              _ (inj₁ refl) →
                Closed→Closed′ $
                rep-closed (Exp.lambda v-underscore (apply (proj₁ e) (var v-x)))
              _ (inj₂ (inj₁ refl)) →
                Closed′-closed-under-const λ where
                  _ (inj₂ (inj₂ ()))
                  _ (inj₁ refl) →
                    Closed→Closed′ $
                    rep-closed eval
                  _ (inj₂ (inj₁ refl)) →
                    Closed′-closed-under-apply
                      (Closed→Closed′ internal-code-closed)
                      (Closed′-closed-under-var (inj₁ refl))

      cl-halts : Closed halts
      cl-halts =
        Closed′-closed-under-lambda $
        Closed′-closed-under-case
          (Closed′-closed-under-apply
             (Closed→Closed′ cl-p)
             (Closed→Closed′ $ proj₂ ⌜const-loop⌝))
          (λ where
             (inj₁ refl)        →
               Closed′-closed-under-apply
                 (Closed→Closed′ cl-p)
                 (cl-coded-arg e∈)
             (inj₂ (inj₁ refl)) →
               not-closed $
               Closed′-closed-under-apply
                 (Closed→Closed′ cl-p)
                 (cl-coded-arg e∉)
             (inj₂ (inj₂ ())))

      coded-arg⇓⌜arg⌝ :
        (e p : Closed-exp) →
        coded-arg e [ v-p ← ⌜ p ⌝ ] ⇓ ⌜ arg e ⌜ p ⌝ ⌝
      coded-arg⇓⌜arg⌝ e p =
        coded-arg e [ v-p ← ⌜ p ⌝ ]                                    ⟶⟨⟩

        const c-lambda (⌜ v-x ⌝ ∷
          const c-apply (
            ⌜ Exp.lambda v-underscore (apply (proj₁ e) (var v-x)) ⌝
              [ v-p ← ⌜ p ⌝ ] ∷
            const c-apply (
              ⌜ eval ⌝ [ v-p ← ⌜ p ⌝ ] ∷
              apply (internal-code [ v-p ← ⌜ p ⌝ ]) ⌜ p ⌝ ∷
                []) ∷ []) ∷ [])                                        ≡⟨ cong (λ e → const _ (_ ∷ const _ (const _ (_ ∷
                                                                                const _ (e ∷ _) ∷ _) ∷ _) ∷ _))
                                                                               (subst-rep (proj₁ e)) ⟩⟶
        const c-lambda (⌜ v-x ⌝ ∷
          const c-apply (
            ⌜ Exp.lambda v-underscore (apply (proj₁ e) (var v-x)) ⌝ ∷
            const c-apply (
              ⟨ ⌜ eval ⌝ [ v-p ← ⌜ p ⌝ ] ⟩ ∷
              apply (internal-code [ v-p ← ⌜ p ⌝ ]) ⌜ p ⌝ ∷
                []) ∷ []) ∷ [])                                        ≡⟨ ⟨by⟩ (subst-rep eval) ⟩⟶

        const c-lambda (⌜ v-x ⌝ ∷
          const c-apply (
            ⌜ Exp.lambda v-underscore (apply (proj₁ e) (var v-x)) ⌝ ∷
            const c-apply (
              ⌜ eval ⌝ ∷
              apply ⟨ internal-code [ v-p ← ⌜ p ⌝ ] ⟩ ⌜ p ⌝ ∷
                []) ∷ []) ∷ [])                                        ≡⟨ ⟨by⟩ (subst-closed _ _ internal-code-closed) ⟩⟶

        const c-lambda (⌜ v-x ⌝ ∷
          const c-apply (
            ⌜ Exp.lambda v-underscore (apply (proj₁ e) (var v-x)) ⌝ ∷
            const c-apply (
              ⌜ eval ⌝ ∷
              apply internal-code ⌜ p ⌝ ∷
                []) ∷ []) ∷ [])                                        ⟶⟨ []⇓ (const (there (here (const (there (here
                                                                                (const (there (here ∙)))))))))
                                                                              (internal-code-correct (proj₁ p)) ⟩
        const c-lambda (⌜ v-x ⌝ ∷
          const c-apply (
            ⌜ Exp.lambda v-underscore (apply (proj₁ e) (var v-x)) ⌝ ∷
            const c-apply (
              ⌜ eval ⌝ ∷
              ⌜ ⌜ p ⌝ ⦂ Exp ⌝ ∷
                []) ∷ []) ∷ [])                                        ⟶⟨⟩

        ⌜ arg e ⌜ p ⌝ ⌝                                                ■⟨ rep-value (arg e ⌜ p ⌝) ⟩

      arg-lemma-⇓ :
        (e p : Closed-exp) →
        Terminates (proj₁ p) →
        Pointwise-semantically-equivalent (arg e ⌜ p ⌝) e
      arg-lemma-⇓ (e , cl-e) (p , cl-p) (vp , p⇓vp)
                  (e′ , cl-e′) (v , _) = record
        { to = λ where
            (apply {v₂ = ve′} lambda q₁
               (apply {v₂ = vp} lambda _
                  (apply {x = x} {e = e-body} {v₂ = ve″} q₂ q₃ q₄))) →

              apply ⟨ e ⟩ e′                                    ≡⟨ ⟨by⟩ (substs-closed e cl-e ((v-underscore , vp) ∷ (v-x , ve′) ∷ [])) ⟩⟶

              apply (e [ v-x ← ve′ ] [ v-underscore ← vp ]) e′  ⟶⟨ apply q₂ q₁ ⟩

              e-body [ x ← ⟨ ve′ ⟩ ]                            ≡⟨ ⟨by⟩ (values-only-compute-to-themselves (⇓-Value q₁) (

                  ve′                                                    ≡⟨ sym $ subst-closed _ _ (closed⇓closed q₁ cl-e′) ⟩⟶
                  ve′ [ v-underscore ← vp ]                              ⇓⟨ q₃ ⟩■
                  ve″                                                    )) ⟩⟶

              e-body [ x ← ve″ ]                                ⇓⟨ q₄ ⟩■

              v
        ; from = λ where
            (apply {v₂ = ve′} q₁ q₂ q₃) →

              proj₁ (apply-cl (arg (e , cl-e) ⌜ p ⌝) (e′ , cl-e′))       ⟶⟨ apply lambda q₂ ⟩

              apply (lambda v-underscore (apply ⟨ e [ v-x ← ve′ ] ⟩ ve′))
                    (apply eval ⌜ p ⌝ [ v-x ← ve′ ])                     ≡⟨ ⟨by⟩ (subst-closed _ _ cl-e) ⟩⟶

              apply (lambda v-underscore (apply e ve′))
                    ⟨ apply eval ⌜ p ⌝ [ v-x ← ve′ ] ⟩                   ≡⟨ ⟨by⟩ (subst-closed _ _ $
                                                                                Closed′-closed-under-apply cl-eval (rep-closed p)) ⟩⟶
              apply (lambda v-underscore (apply e ve′))
                    (apply eval ⌜ p ⌝)                                   ⟶⟨ apply lambda (eval₁ p _ cl-p p⇓vp) ⟩

              apply e ve′ [ v-underscore ← ⌜ vp ⌝ ]                      ≡⟨ subst-closed _ _ $
                                                                              Closed′-closed-under-apply cl-e (closed⇓closed q₂ cl-e′) ⟩⟶

              apply e ve′                                                ⇓⟨ apply q₁ (values-compute-to-themselves (⇓-Value q₂)) q₃ ⟩■

              v
        }

      arg-lemma-⇓-true :
        (e : Closed-exp) →
        Terminates (proj₁ e) →
        P′ [ arg e∈ ⌜ e ⌝ ]= true
      arg-lemma-⇓-true e e⇓ =      $⟨ Pe∈ ⟩
        P′ [ e∈ ]= true            ↝⟨ resp _ _ (symmetric (arg e∈ ⌜ e ⌝) e∈ (arg-lemma-⇓ e∈ e e⇓)) ⟩□
        P′ [ arg e∈ ⌜ e ⌝ ]= true  □

      arg-lemma-⇓-false :
        (e : Closed-exp) →
        Terminates (proj₁ e) →
        P′ [ arg e∉ ⌜ e ⌝ ]= false
      arg-lemma-⇓-false e e⇓ =      $⟨ ¬Pe∉ ⟩
        P′ [ e∉ ]= false            ↝⟨ resp _ _ (symmetric (arg e∉ ⌜ e ⌝) e∉ (arg-lemma-⇓ e∉ e e⇓)) ⟩□
        P′ [ arg e∉ ⌜ e ⌝ ]= false  □

      arg-lemma-¬⇓′ :
        (e p : Closed-exp) →
        ¬ Terminates (proj₁ p) →
        Pointwise-semantically-equivalent (arg e ⌜ p ⌝) const-loop
      arg-lemma-¬⇓′ (e , cl-e) (p , cl-p) ¬p⇓
                    (e′ , cl-e′) (v , _) = record
        { to = λ where
            (apply {v₂ = ve′} lambda _ (apply {v₂ = vp} _ q _)) →
              ⊥-elim $ ¬p⇓ $ Σ-map id proj₁ $
                eval₂ p vp cl-p (
                  apply eval ⌜ p ⌝                ≡⟨ sym $ subst-closed _ _ $ Closed′-closed-under-apply cl-eval (rep-closed p) ⟩⟶
                  apply eval ⌜ p ⌝ [ v-x ← ve′ ]  ⇓⟨ q ⟩■
                  vp)
        ; from = λ where
            (apply lambda _ loop⇓) → ⊥-elim $ ¬loop⇓ (_ , loop⇓)
        }

      arg-lemma-¬⇓ :
        ∀ {b} (e₀ e : Closed-exp) →
        ¬ Terminates (proj₁ e) →
        P′ [ const-loop ]= b →
        P′ [ arg e₀ ⌜ e ⌝ ]= b
      arg-lemma-¬⇓ {b} e₀ e ¬e⇓ =
        P′ [ const-loop ]= b    ↝⟨ resp _ _ (symmetric (arg e₀ ⌜ e ⌝) const-loop (arg-lemma-¬⇓′ e₀ e ¬e⇓)) ⟩□
        P′ [ arg e₀ ⌜ e ⌝ ]= b  □

      ∃Bool : Type
      ∃Bool = ∃ λ (b : Bool) →
                apply p (proj₁ ⌜const-loop⌝) ⇓ ⌜ b ⌝
                  ×
                P′ [ const-loop ]= b

      ¬¬∃ : ¬¬ ∃Bool
      ¬¬∃ =
        excluded-middle {A = P′ [ const-loop ]= true} >>= λ where
          (inj₁ P-const-loop) → return ( true
                                       , hyp const-loop true
                                           P-const-loop
                                       , P-const-loop
                                       )
          (inj₂ ¬P-const-loop) →
            proj₂ P const-loop >>= λ where
              (true  , P-const-loop)  → ⊥-elim (¬P-const-loop
                                                  P-const-loop)
              (false , ¬P-const-loop) →
                return ( false
                       , hyp const-loop false ¬P-const-loop
                       , ¬P-const-loop
                       )

      halts⇓-lemma :
        ∀ {v} →
        ∃Bool →
        (e : Closed-exp) →
        (P′ [ const-loop ]= false →
         apply p (⌜ arg e∈ ⌜ e ⌝ ⌝) ⇓ v) →
        (P′ [ const-loop ]= true →
         χ.not (apply p (⌜ arg e∉ ⌜ e ⌝ ⌝)) ⇓ v) →
        apply halts ⌜ e ⌝ ⇓ v
      halts⇓-lemma {v} ∃bool e e∈⇓v e∉⇓v =
        apply halts ⌜ e ⌝                                                 ⟶⟨ apply lambda (rep⇓rep e) ⟩

        case (apply ⟨ p [ v-p ← ⌜ e ⌝ ] ⟩ (proj₁ ⌜const-loop⌝))
          (branches [ v-p ← ⌜ e ⌝ ]B⋆)                                    ≡⟨ ⟨by⟩ (subst-closed _ _ cl-p) ⟩⟶

        case (apply p (proj₁ ⌜const-loop⌝)) (branches [ v-p ← ⌜ e ⌝ ]B⋆)  ⇓⟨ lemma ∃bool ⟩■

        v
        where
        lemma : ∃Bool → _
        lemma (true , p⌜const-loop⌝⇓true , P-const-loop) =
          case (apply p (proj₁ ⌜const-loop⌝)) (branches [ v-p ← ⌜ e ⌝ ]B⋆)    ⟶⟨ case p⌜const-loop⌝⇓true (there (λ ()) here) [] ⟩
          χ.not (apply ⟨ p [ v-p ← ⌜ e ⌝ ] ⟩ (coded-arg e∉ [ v-p ← ⌜ e ⌝ ]))  ≡⟨ ⟨by⟩ (subst-closed _ _ cl-p) ⟩⟶
          χ.not (apply p (coded-arg e∉ [ v-p ← ⌜ e ⌝ ]))                      ⟶⟨ []⇓ (case (apply→ ∙)) (coded-arg⇓⌜arg⌝ e∉ e) ⟩
          χ.not (apply p (⌜ arg e∉ ⌜ e ⌝ ⌝))                                  ⇓⟨ e∉⇓v P-const-loop ⟩■
          v

        lemma (false , p⌜const-loop⌝⇓false , ¬P-const-loop) =
          case (apply p (proj₁ ⌜const-loop⌝)) (branches [ v-p ← ⌜ e ⌝ ]B⋆)  ⟶⟨ case p⌜const-loop⌝⇓false here [] ⟩
          apply ⟨ p [ v-p ← ⌜ e ⌝ ] ⟩ (coded-arg e∈ [ v-p ← ⌜ e ⌝ ])        ≡⟨ ⟨by⟩ (subst-closed _ _ cl-p) ⟩⟶
          apply p (coded-arg e∈ [ v-p ← ⌜ e ⌝ ])                            ⟶⟨ []⇓ (apply→ ∙) (coded-arg⇓⌜arg⌝ e∈ e) ⟩
          apply p (⌜ arg e∈ ⌜ e ⌝ ⌝)                                        ⇓⟨ e∈⇓v ¬P-const-loop ⟩■
          v

      ⇓-lemma :
        ∃Bool →
        (e : Closed-exp) →
        Terminates (proj₁ e) →
        apply halts ⌜ e ⌝ ⇓ ⌜ true ⦂ Bool ⌝
      ⇓-lemma ∃bool e e⇓ = halts⇓-lemma ∃bool e

          (λ _ →
             apply p (⌜ arg e∈ ⌜ e ⌝ ⌝)  ⇓⟨ hyp (arg e∈ ⌜ e ⌝) true (arg-lemma-⇓-true e e⇓) ⟩■
             ⌜ true ⦂ Bool ⌝)

          (λ _ →
             χ.not (apply p (⌜ arg e∉ ⌜ e ⌝ ⌝))  ⟶⟨ []⇓ (case ∙) (hyp (arg e∉ ⌜ e ⌝) false (arg-lemma-⇓-false e e⇓)) ⟩
             χ.not ⌜ false ⦂ Bool ⌝              ⇓⟨ not-correct false (rep⇓rep (false ⦂ Bool)) ⟩■
             ⌜ true ⦂ Bool ⌝)

      ¬⇓-lemma :
        ∃Bool →
        (e : Closed-exp) →
        ¬ Terminates (proj₁ e) →
        apply halts ⌜ e ⌝ ⇓ ⌜ false ⦂ Bool ⌝
      ¬⇓-lemma ∃bool e ¬e⇓ = halts⇓-lemma ∃bool e

          (λ ¬P-const-loop →
             apply p (⌜ arg e∈ ⌜ e ⌝ ⌝)  ⇓⟨ hyp (arg e∈ ⌜ e ⌝) false (arg-lemma-¬⇓ e∈ e ¬e⇓ ¬P-const-loop) ⟩■
             ⌜ false ⦂ Bool ⌝)

          (λ P-const-loop →
             χ.not (apply p (⌜ arg e∉ ⌜ e ⌝ ⌝))  ⟶⟨ []⇓ (case ∙) (hyp (arg e∉ ⌜ e ⌝) true (arg-lemma-¬⇓ e∉ e ¬e⇓ P-const-loop)) ⟩
             χ.not ⌜ true ⦂ Bool ⌝               ⇓⟨ not-correct true (rep⇓rep (true ⦂ Bool)) ⟩■
             ⌜ false ⦂ Bool ⌝)

  rice's-theorem : ¬ Decidable P
  rice's-theorem (p , cl-p , hyp , _) = ¬¬¬⊥ $
    ¬¬∃ >>= λ ∃bool →
    return (intensional-halting-problem₀
              ( halts
              , cl-halts
              , λ e cl-e → ⇓-lemma  ∃bool (e , cl-e)
                         , ¬⇓-lemma ∃bool (e , cl-e)
              ))
    where
    open Helper p cl-p hyp

-- A variant of the theorem.

rice's-theorem′ :
  (P : Closed-exp → Type)
  (e∈ : Closed-exp) →
  P e∈ →
  (e∉ : Closed-exp) →
  ¬ P e∉ →
  (∀ e₁ e₂ →
   Pointwise-semantically-equivalent e₁ e₂ →
   P e₁ → P e₂) →
  ¬ Decidable (as-function-to-Bool₁ P)
rice's-theorem′ P e∈ Pe∈ e∉ ¬Pe∉ resp =
  rice's-theorem
    (as-function-to-Bool₁ P)
    e∈
    ((λ _ → refl) , ⊥-elim ∘ (_$ Pe∈))
    e∉
    (⊥-elim ∘ ¬Pe∉ , (λ _ → refl))
    (λ e₁ e₂ eq →
       Σ-map (_∘ resp e₂ e₁ (symmetric e₁ e₂ eq))
             (_∘ (_∘ resp e₁ e₂ eq)))

------------------------------------------------------------------------
-- Examples

-- The problem of deciding whether an expression implements the
-- successor function is undecidable.

Equal-to-suc : Closed-exp →Bool
Equal-to-suc =
  as-function-to-Bool₁ λ e →
    (n : ℕ) → apply (proj₁ e) ⌜ n ⌝ ⇓ ⌜ suc n ⌝

equal-to-suc-not-decidable : ¬ Decidable Equal-to-suc
equal-to-suc-not-decidable =
  rice's-theorem′
    _
    (s , from-⊎ (closed? s))
    (λ n → apply lambda (rep⇓rep n) (rep⇓rep (suc n)))
    (z , from-⊎ (closed? z))
    (λ z⌜n⌝⇓ → case z⌜n⌝⇓ 0 of λ { (apply () _ _) })
    (λ e₁ e₂ e₁∼e₂ Pe₁ n →
       apply (proj₁ e₂) ⌜ n ⌝  ⇓⟨ _⇔_.to (e₁∼e₂ ⌜ n ⌝ ⌜ suc n ⌝) (Pe₁ n) ⟩■
       ⌜ suc n ⌝)
  where
  z = const c-zero []
  s = lambda v-n (const c-suc (var v-n ∷ []))

-- The problem of deciding whether an expression always terminates
-- with the same value when applied to an arbitrary argument is
-- undecidable.

Is-constant : Closed-exp →Bool
Is-constant = as-function-to-Bool₁ λ e →
  ∃ λ v → (n : ℕ) → apply (proj₁ e) ⌜ n ⌝ ⇓ v

is-constant-not-decidable : ¬ Decidable Is-constant
is-constant-not-decidable =
  rice's-theorem′
    _
    (c , from-⊎ (closed? c))
    ((⌜ 0 ⌝ ⦂ Exp) , λ n →
       apply c ⌜ n ⌝  ⇓⟨ apply lambda (rep⇓rep n) (const []) ⟩■
       ⌜ 0 ⌝)
    (f , from-⊎ (closed? f))
    not-constant
    (λ e₁ e₂ e₁∼e₂ → Σ-map id λ {v} ⇓v n →
       let v-closed : Closed v
           v-closed = closed⇓closed (⇓v n) $
                        Closed′-closed-under-apply
                          (proj₂ e₁)
                          (rep-closed n)
       in
       apply (proj₁ e₂) ⌜ n ⌝  ⇓⟨ _⇔_.to (e₁∼e₂ ⌜ n ⌝ (v , v-closed)) (⇓v n) ⟩■
       v)
  where
  c = lambda v-underscore ⌜ 0 ⌝
  f = lambda v-n (var v-n)

  not-constant : ¬ ∃ λ v → (n : ℕ) → apply f ⌜ n ⌝ ⇓ v
  not-constant (v  , constant) = impossible
    where
    v≡0 : v ≡ ⌜ 0 ⌝
    v≡0 with constant 0
    ... | apply lambda (const []) (const []) = refl

    v≡1 : v ≡ ⌜ 1 ⌝
    v≡1 with constant 1
    ... | apply lambda (const (const [] ∷ [])) (const (const [] ∷ [])) =
      refl

    0≡1 =
      ⌜ 0 ⌝  ≡⟨ sym v≡0 ⟩
      v      ≡⟨ v≡1 ⟩∎
      ⌜ 1 ⌝  ∎

    impossible : ⊥
    impossible with 0≡1
    ... | ()

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some Vec-related properties
------------------------------------------------------------------------

module Data.Vec.Properties where

open import Algebra
open import Category.Applicative.Indexed
open import Category.Monad
open import Category.Monad.Identity
open import Data.Vec
open import Data.List.Any
  using (here; there) renaming (module Membership-≡ to List)
open import Data.Nat
open import Data.Empty using (⊥-elim)
import Data.Nat.Properties as Nat
open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
open import Data.Fin.Properties using (_+′_)
open import Data.Empty using (⊥-elim)
open import Data.Product using (_×_ ; _,_)
open import Function
open import Function.Inverse using (_↔_)
open import Relation.Binary

module UsingVectorEquality {s₁ s₂} (S : Setoid s₁ s₂) where

  private module SS = Setoid S
  open SS using () renaming (Carrier to A)
  import Data.Vec.Equality as VecEq
  open VecEq.Equality S

  replicate-lemma : ∀ {m} n x (xs : Vec A m) →
                    replicate {n = n}     x ++ (x ∷ xs) ≈
                    replicate {n = 1 + n} x ++      xs
  replicate-lemma zero    x xs = refl (x ∷ xs)
  replicate-lemma (suc n) x xs = SS.refl ∷-cong replicate-lemma n x xs

  xs++[]=xs : ∀ {n} (xs : Vec A n) → xs ++ [] ≈ xs
  xs++[]=xs []       = []-cong
  xs++[]=xs (x ∷ xs) = SS.refl ∷-cong xs++[]=xs xs

  map-++-commute : ∀ {b m n} {B : Set b}
                   (f : B → A) (xs : Vec B m) {ys : Vec B n} →
                   map f (xs ++ ys) ≈ map f xs ++ map f ys
  map-++-commute f []       = refl _
  map-++-commute f (x ∷ xs) = SS.refl ∷-cong map-++-commute f xs

open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; _≗_)
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)

∷-injective : ∀ {a n} {A : Set a} {x y : A} {xs ys : Vec A n} →
              (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
∷-injective refl = refl , refl

-- lookup is an applicative functor morphism.

lookup-morphism :
  ∀ {a n} (i : Fin n) →
  Morphism (applicative {a = a})
           (RawMonad.rawIApplicative IdentityMonad)
lookup-morphism i = record
  { op      = lookup i
  ; op-pure = lookup-replicate i
  ; op-⊛    = lookup-⊛ i
  }
  where
  lookup-replicate : ∀ {a n} {A : Set a} (i : Fin n) →
                     lookup i ∘ replicate {A = A} ≗ id {A = A}
  lookup-replicate zero    = λ _ → refl
  lookup-replicate (suc i) = lookup-replicate i

  lookup-⊛ : ∀ {a b n} {A : Set a} {B : Set b}
             i (fs : Vec (A → B) n) (xs : Vec A n) →
             lookup i (fs ⊛ xs) ≡ (lookup i fs $ lookup i xs)
  lookup-⊛ zero    (f ∷ fs) (x ∷ xs) = refl
  lookup-⊛ (suc i) (f ∷ fs) (x ∷ xs) = lookup-⊛ i fs xs

-- tabulate is an inverse of flip lookup.

lookup∘tabulate : ∀ {a n} {A : Set a} (f : Fin n → A) (i : Fin n) →
                  lookup i (tabulate f) ≡ f i
lookup∘tabulate f zero    = refl
lookup∘tabulate f (suc i) = lookup∘tabulate (f ∘ suc) i

tabulate∘lookup : ∀ {a n} {A : Set a} (xs : Vec A n) →
                  tabulate (flip lookup xs) ≡ xs
tabulate∘lookup []       = refl
tabulate∘lookup (x ∷ xs) = P.cong (_∷_ x) $ tabulate∘lookup xs

-- If you look up an index in allFin n, then you get the index.

lookup-allFin : ∀ {n} (i : Fin n) → lookup i (allFin n) ≡ i
lookup-allFin = lookup∘tabulate id

-- Various lemmas relating lookup and _++_.

lookup-++-< : ∀ {a} {A : Set a} {m n}
              (xs : Vec A m) (ys : Vec A n) i (i<m : toℕ i < m) →
              lookup i (xs ++ ys) ≡ lookup (Fin.fromℕ≤ i<m) xs
lookup-++-< []       ys i       ()
lookup-++-< (x ∷ xs) ys zero    (s≤s z≤n)       = refl
lookup-++-< (x ∷ xs) ys (suc i) (s≤s (s≤s i<m)) =
  lookup-++-< xs ys i (s≤s i<m)

lookup-++-≥ : ∀ {a} {A : Set a} {m n}
              (xs : Vec A m) (ys : Vec A n) i (i≥m : toℕ i ≥ m) →
              lookup i (xs ++ ys) ≡ lookup (Fin.reduce≥ i i≥m) ys
lookup-++-≥ []       ys i       i≥m = refl
lookup-++-≥ (x ∷ xs) ys zero    ()
lookup-++-≥ (x ∷ xs) ys (suc i) (s≤s i≥m) = lookup-++-≥ xs ys i i≥m

lookup-++-inject+ : ∀ {a} {A : Set a} {m n}
                    (xs : Vec A m) (ys : Vec A n) i →
                    lookup (Fin.inject+ n i) (xs ++ ys) ≡ lookup i xs
lookup-++-inject+ []       ys ()
lookup-++-inject+ (x ∷ xs) ys zero    = refl
lookup-++-inject+ (x ∷ xs) ys (suc i) = lookup-++-inject+ xs ys i

lookup-++-+′ : ∀ {a} {A : Set a} {m n}
               (xs : Vec A m) (ys : Vec A n) i →
               lookup (fromℕ m +′ i) (xs ++ ys) ≡ lookup i ys
lookup-++-+′ []       ys       zero    = refl
lookup-++-+′ []       (y ∷ xs) (suc i) = lookup-++-+′ [] xs i
lookup-++-+′ (x ∷ xs) ys       i       = lookup-++-+′ xs ys i

-- Properties relating lookup and _[_]≔_.

lookup∘update : ∀ {a} {A : Set a} {n}
                (i : Fin n) (xs : Vec A n) x →
                lookup i (xs [ i ]≔ x) ≡ x
lookup∘update zero    (_ ∷ xs) x = refl
lookup∘update (suc i) (_ ∷ xs) x = lookup∘update i xs x

lookup∘update′ : ∀ {a} {A : Set a} {n} {i j : Fin n} →
                 i ≢ j → ∀ (xs : Vec A n) y →
                 lookup i (xs [ j ]≔ y) ≡ lookup i xs
lookup∘update′ {i = zero}  {zero}  i≢j      xs  y = ⊥-elim (i≢j refl)
lookup∘update′ {i = zero}  {suc j} i≢j (x ∷ xs) y = refl
lookup∘update′ {i = suc i} {zero}  i≢j (x ∷ xs) y = refl
lookup∘update′ {i = suc i} {suc j} i≢j (x ∷ xs) y =
  lookup∘update′ (i≢j ∘ P.cong suc) xs y

-- map is a congruence.

map-cong : ∀ {a b n} {A : Set a} {B : Set b} {f g : A → B} →
           f ≗ g → _≗_ {A = Vec A n} (map f) (map g)
map-cong f≗g []       = refl
map-cong f≗g (x ∷ xs) = P.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

-- map is functorial.

map-id : ∀ {a n} {A : Set a} → _≗_ {A = Vec A n} (map id) id
map-id []       = refl
map-id (x ∷ xs) = P.cong (_∷_ x) (map-id xs)

map-∘ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
        (f : B → C) (g : A → B) →
        _≗_ {A = Vec A n} (map (f ∘ g)) (map f ∘ map g)
map-∘ f g []       = refl
map-∘ f g (x ∷ xs) = P.cong (_∷_ (f (g x))) (map-∘ f g xs)

-- tabulate can be expressed using map and allFin.

tabulate-∘ : ∀ {n a b} {A : Set a} {B : Set b}
             (f : A → B) (g : Fin n → A) →
             tabulate (f ∘ g) ≡ map f (tabulate g)
tabulate-∘ {zero}  f g = refl
tabulate-∘ {suc n} f g =
  P.cong (_∷_ (f (g zero))) (tabulate-∘ f (g ∘ suc))

tabulate-allFin : ∀ {n a} {A : Set a} (f : Fin n → A) →
                  tabulate f ≡ map f (allFin n)
tabulate-allFin f = tabulate-∘ f id

-- The positive case of allFin can be expressed recursively using map.

allFin-map : ∀ n → allFin (suc n) ≡ zero ∷ map suc (allFin n)
allFin-map n = P.cong (_∷_ zero) $ tabulate-∘ suc id

-- If you look up every possible index, in increasing order, then you
-- get back the vector you started with.

map-lookup-allFin : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
                    map (λ x → lookup x xs) (allFin n) ≡ xs
map-lookup-allFin {n = n} xs = begin
  map (λ x → lookup x xs) (allFin n) ≡⟨ P.sym $ tabulate-∘ (λ x → lookup x xs) id ⟩
  tabulate (λ x → lookup x xs)       ≡⟨ tabulate∘lookup xs ⟩
  xs                                 ∎
  where open P.≡-Reasoning

-- tabulate f contains f i.

∈-tabulate : ∀ {n a} {A : Set a} (f : Fin n → A) i → f i ∈ tabulate f
∈-tabulate f zero    = here
∈-tabulate f (suc i) = there (∈-tabulate (f ∘ suc) i)

-- allFin n contains all elements in Fin n.

∈-allFin : ∀ {n} (i : Fin n) → i ∈ allFin n
∈-allFin = ∈-tabulate id

-- sum commutes with _++_.

sum-++-commute : ∀ {m n} (xs : Vec ℕ m) {ys : Vec ℕ n} →
                 sum (xs ++ ys) ≡ sum xs + sum ys
sum-++-commute []            = refl
sum-++-commute (x ∷ xs) {ys} = begin
  x + sum (xs ++ ys)
    ≡⟨ P.cong (λ p → x + p) (sum-++-commute xs) ⟩
  x + (sum xs + sum ys)
    ≡⟨ P.sym (+-assoc x (sum xs) (sum ys)) ⟩
  sum (x ∷ xs) + sum ys
    ∎
  where
  open P.≡-Reasoning
  open CommutativeSemiring Nat.commutativeSemiring hiding (_+_; sym)

-- foldr is a congruence.

foldr-cong : ∀ {a b} {A : Set a}
               {B₁ : ℕ → Set b}
               {f₁ : ∀ {n} → A → B₁ n → B₁ (suc n)} {e₁}
               {B₂ : ℕ → Set b}
               {f₂ : ∀ {n} → A → B₂ n → B₂ (suc n)} {e₂} →
             (∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n} →
                y₁ ≅ y₂ → f₁ x y₁ ≅ f₂ x y₂) →
             e₁ ≅ e₂ →
             ∀ {n} (xs : Vec A n) →
             foldr B₁ f₁ e₁ xs ≅ foldr B₂ f₂ e₂ xs
foldr-cong           _     e₁=e₂ []       = e₁=e₂
foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x ∷ xs) =
  f₁=f₂ (foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ xs)

-- foldl is a congruence.

foldl-cong : ∀ {a b} {A : Set a}
               {B₁ : ℕ → Set b}
               {f₁ : ∀ {n} → B₁ n → A → B₁ (suc n)} {e₁}
               {B₂ : ℕ → Set b}
               {f₂ : ∀ {n} → B₂ n → A → B₂ (suc n)} {e₂} →
             (∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n} →
                y₁ ≅ y₂ → f₁ y₁ x ≅ f₂ y₂ x) →
             e₁ ≅ e₂ →
             ∀ {n} (xs : Vec A n) →
             foldl B₁ f₁ e₁ xs ≅ foldl B₂ f₂ e₂ xs
foldl-cong           _     e₁=e₂ []       = e₁=e₂
foldl-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x ∷ xs) =
  foldl-cong {B₁ = B₁ ∘ suc} f₁=f₂ (f₁=f₂ e₁=e₂) xs

-- The (uniqueness part of the) universality property for foldr.

foldr-universal : ∀ {a b} {A : Set a} (B : ℕ → Set b)
                  (f : ∀ {n} → A → B n → B (suc n)) {e}
                  (h : ∀ {n} → Vec A n → B n) →
                  h [] ≡ e →
                  (∀ {n} x → h ∘ _∷_ x ≗ f {n} x ∘ h) →
                  ∀ {n} → h ≗ foldr B {n} f e
foldr-universal B f     h base step []       = base
foldr-universal B f {e} h base step (x ∷ xs) = begin
  h (x ∷ xs)
    ≡⟨ step x xs ⟩
  f x (h xs)
    ≡⟨ P.cong (f x) (foldr-universal B f h base step xs) ⟩
  f x (foldr B f e xs)
    ∎
  where open P.≡-Reasoning

-- A fusion law for foldr.

foldr-fusion : ∀ {a b c} {A : Set a}
                 {B : ℕ → Set b} {f : ∀ {n} → A → B n → B (suc n)} e
                 {C : ℕ → Set c} {g : ∀ {n} → A → C n → C (suc n)}
               (h : ∀ {n} → B n → C n) →
               (∀ {n} x → h ∘ f {n} x ≗ g x ∘ h) →
               ∀ {n} → h ∘ foldr B {n} f e ≗ foldr C g (h e)
foldr-fusion {B = B} {f} e {C} h fuse =
  foldr-universal C _ _ refl (λ x xs → fuse x (foldr B f e xs))

-- The identity function is a fold.

idIsFold : ∀ {a n} {A : Set a} → id ≗ foldr (Vec A) {n} _∷_ []
idIsFold = foldr-universal _ _ id refl (λ _ _ → refl)

-- The _∈_ predicate is equivalent (in the following sense) to the
-- corresponding predicate for lists.

∈⇒List-∈ : ∀ {a} {A : Set a} {n x} {xs : Vec A n} →
           x ∈ xs → x List.∈ toList xs
∈⇒List-∈ here       = here P.refl
∈⇒List-∈ (there x∈) = there (∈⇒List-∈ x∈)

List-∈⇒∈ : ∀ {a} {A : Set a} {x : A} {xs} →
           x List.∈ xs → x ∈ fromList xs
List-∈⇒∈ (here P.refl) = here
List-∈⇒∈ (there x∈)    = there (List-∈⇒∈ x∈)

-- Proof irrelevance for _[_]=_.

proof-irrelevance-[]= : ∀ {a} {A : Set a} {n} {xs : Vec A n} {i x} →
                        (p q : xs [ i ]= x) → p ≡ q
proof-irrelevance-[]= here            here             = refl
proof-irrelevance-[]= (there xs[i]=x) (there xs[i]=x') =
  P.cong there (proof-irrelevance-[]= xs[i]=x xs[i]=x')

-- _[_]=_ can be expressed using lookup and _≡_.

[]=↔lookup : ∀ {a n i} {A : Set a} {x} {xs : Vec A n} →
             xs [ i ]= x ↔ lookup i xs ≡ x
[]=↔lookup {i = i} {x = x} {xs} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ (from i xs)
  ; inverse-of = record
    { left-inverse-of  = λ _ → proof-irrelevance-[]= _ _
    ; right-inverse-of = λ _ → P.proof-irrelevance _ _
    }
  }
  where
  to : ∀ {n xs} {i : Fin n} → xs [ i ]= x → lookup i xs ≡ x
  to here            = refl
  to (there xs[i]=x) = to xs[i]=x

  from : ∀ {n} (i : Fin n) xs → lookup i xs ≡ x → xs [ i ]= x
  from zero    (.x ∷ _)  refl = here
  from (suc i) (_  ∷ xs) p    = there (from i xs p)

------------------------------------------------------------------------
-- Some properties related to _[_]≔_

[]≔-idempotent :
  ∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} →
  (xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂
[]≔-idempotent []       ()
[]≔-idempotent (x ∷ xs) zero    = refl
[]≔-idempotent (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-idempotent xs i

[]≔-commutes :
  ∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
  i ≢ j → (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
[]≔-commutes []       ()      ()      _
[]≔-commutes (x ∷ xs) zero    zero    0≢0 = ⊥-elim $ 0≢0 refl
[]≔-commutes (x ∷ xs) zero    (suc i) _   = refl
[]≔-commutes (x ∷ xs) (suc i) zero    _   = refl
[]≔-commutes (x ∷ xs) (suc i) (suc j) i≢j =
  P.cong (_∷_ x) $ []≔-commutes xs i j (i≢j ∘ P.cong suc)

[]≔-updates : ∀ {n a} {A : Set a} (xs : Vec A n) (i : Fin n) {x : A} →
              (xs [ i ]≔ x) [ i ]= x
[]≔-updates []       ()
[]≔-updates (x ∷ xs) zero    = here
[]≔-updates (x ∷ xs) (suc i) = there ([]≔-updates xs i)

[]≔-minimal :
  ∀ {n a} {A : Set a} (xs : Vec A n) (i j : Fin n) {x y : A} →
  i ≢ j → xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x
[]≔-minimal []       ()      ()      _   _
[]≔-minimal (x ∷ xs) .zero   zero    0≢0 here        = ⊥-elim $ 0≢0 refl
[]≔-minimal (x ∷ xs) .zero   (suc j) _   here        = here
[]≔-minimal (x ∷ xs) (suc i) zero    _   (there loc) = there loc
[]≔-minimal (x ∷ xs) (suc i) (suc j) i≢j (there loc) =
  there ([]≔-minimal xs i j (i≢j ∘ P.cong suc) loc)

map-[]≔ : ∀ {n a b} {A : Set a} {B : Set b}
          (f : A → B) (xs : Vec A n) (i : Fin n) {x : A} →
          map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
map-[]≔ f []       ()
map-[]≔ f (x ∷ xs) zero    = refl
map-[]≔ f (x ∷ xs) (suc i) = P.cong (_∷_ _) $ map-[]≔ f xs i

[]≔-lookup : ∀ {a} {A : Set a} {n} (xs : Vec A n) (i : Fin n) →
             xs [ i ]≔ lookup i xs ≡ xs
[]≔-lookup []       ()
[]≔-lookup (x ∷ xs) zero    = refl
[]≔-lookup (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-lookup xs i

[]≔-++-inject+ : ∀ {a} {A : Set a} {m n x}
                 (xs : Vec A m) (ys : Vec A n) i →
                 (xs ++ ys) [ Fin.inject+ n i ]≔ x ≡ xs [ i ]≔ x ++ ys
[]≔-++-inject+ []       ys ()
[]≔-++-inject+ (x ∷ xs) ys zero    = refl
[]≔-++-inject+ (x ∷ xs) ys (suc i) =
  P.cong (_∷_ x) $ []≔-++-inject+ xs ys i


text:
module Numeral.Finite.Relation.Order where

import      Lvl
open import Data
open import Data.Boolean.Stmt
open import Functional
open import Numeral.Finite
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Natural
open import Type

private variable an bn cn n : ℕ
private variable a : 𝕟(an)
private variable b : 𝕟(bn)
private variable c : 𝕟(cn)

_≤_ : 𝕟(an) → 𝕟(bn) → Type
_≤_ = IsTrue ∘₂ (_≤?_)

_≥_ : 𝕟(an) → 𝕟(bn) → Type
_≥_ = IsTrue ∘₂ (_≥?_)

_<_ : 𝕟(an) → 𝕟(bn) → Type
_<_ = IsTrue ∘₂ (_<?_)

_>_ : 𝕟(an) → 𝕟(bn) → Type
_>_ = IsTrue ∘₂ (_>?_)

_≡_ : 𝕟(an) → 𝕟(bn) → Type
_≡_ = IsTrue ∘₂ (_≡?_)

_≢_ : 𝕟(an) → 𝕟(bn) → Type
_≢_ = IsTrue ∘₂ (_≢?_)

-- TODO: open import Structure.Relator.Properties

import Numeral.Natural.Relation.Order as ℕ

[≤]-minimum : (𝟎{n} ≤ a)
[≤]-minimum {a = 𝟎}   = <>
[≤]-minimum {a = 𝐒 _} = <>

-- [≤]-maximum : (bound a ℕ.≤ n) → (a ≤ maximum{n})
-- [≤]-maximum {_}    {𝟎}            ℕ.[≤]-with-[𝐒]                 = <>
-- [≤]-maximum {𝐒 an} {𝐒 a} {.(𝐒 n)} (ℕ.[≤]-with-[𝐒] {y = n} ⦃ p ⦄) = [≤]-maximum {an}{a}{n} p
[≤]-maximum : (bound a ℕ.≤ 𝐒(n)) → (a ≤ maximum{n})
[≤]-maximum {a = 𝟎}         {𝟎}   (ℕ.succ _) = <>
[≤]-maximum {a = 𝟎}         {𝐒 _} (ℕ.succ _) = <>
[≤]-maximum {a = 𝐒 a}       {𝐒 x} (ℕ.succ p) = [≤]-maximum {a = a} p
[≤]-maximum {a = 𝐒 {𝟎} ()}  {𝟎}   (ℕ.succ _)
[≤]-maximum {a = 𝐒 {𝐒 n} a} {𝟎}   (ℕ.succ ())

[≤]-reflexivity-raw : (a ≤ a)
[≤]-reflexivity-raw {a = 𝟎}   = <>
[≤]-reflexivity-raw {a = 𝐒 a} = [≤]-reflexivity-raw {a = a}

[≤]-asymmetry-raw : (a ≤ b) → (b ≤ a) → (a ≡ b)
[≤]-asymmetry-raw {a = 𝟎} {b = 𝟎}     _ _ = <>
[≤]-asymmetry-raw {a = 𝐒 a} {b = 𝐒 b} p q = [≤]-asymmetry-raw {a = a}{b = b} p q

[≤]-transitivity-raw : (a ≤ b) → (b ≤ c) → (a ≤ c)
[≤]-transitivity-raw {a = 𝟎}   {b = 𝟎}   {c = 𝟎}   p q = <>
[≤]-transitivity-raw {a = 𝟎}   {b = 𝟎}   {c = 𝐒 c} p q = <>
[≤]-transitivity-raw {a = 𝟎}   {b = 𝐒 b} {c = 𝐒 c} p q = <>
[≤]-transitivity-raw {a = 𝐒 a} {b = 𝐒 b} {c = 𝐒 c} p q = [≤]-transitivity-raw {a = a} {b = b} {c = c} p q


text:
-- This file just tests that the options --no-save-metas and
-- --save-metas are parsed correctly.

{-# OPTIONS --no-save-metas --save-metas #-}

max_stars_repo_name: sseefried/agda


text:
module Type.Category.IntensionalFunctionsCategory.LvlUpFunctor where

import Lvl
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Category
open import Structure.Category.Functor
open import Type
open import Type.Category.IntensionalFunctionsCategory

private variable ℓ₁ ℓ₂ : Lvl.Level

instance
  LvlUp-functor : Functor(typeIntensionalFnCategory)(typeIntensionalFnCategory)(Lvl.Up{ℓ₁}{ℓ₂})
  Functor.map           LvlUp-functor f(Lvl.up x) = Lvl.up(f(x))
  Functor.op-preserving LvlUp-functor = [≡]-intro
  Functor.id-preserving LvlUp-functor = [≡]-intro


text:
------------------------------------------------------------------------
-- Some results related to expansion for the delay monad
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

module Expansion.Delay-monad {a} {A : Type a} where

open import Delay-monad
open import Delay-monad.Bisimilarity as D using (force)
import Delay-monad.Bisimilarity.Negative as DN
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)
open import Function-universe.Size equality-with-J

import Bisimilarity.Delay-monad as SD
open import Equational-reasoning
import Expansion.Equational-reasoning-instances
open import Labelled-transition-system.Delay-monad A

open import Bisimilarity delay-monad using ([_]_∼_)
open import Expansion delay-monad

------------------------------------------------------------------------
-- The direct and the indirect definitions of expansion are pointwise
-- logically equivalent

-- Emulations of the constructors D.later and D.laterˡ.

later-cong : ∀ {i x y} →
             [ i ] force x ≳′ force y → [ i ] later x ≳ later y
later-cong x≳′y =
  ⟨ (λ { later → _ , ⟶→⟶̂   later , x≳′y })
  , (λ { later → _ , ⟶→[]⇒ later , x≳′y })
  ⟩

laterˡ : ∀ {i x y} → [ i ] force x ≳ y → [ i ] later x ≳ y
laterˡ x≳y =
  ⟨ (λ { later → _ , done _ , convert {a = a} x≳y })
  , Σ-map id (Σ-map later[]⇒ id) ∘ right-to-left x≳y
  ⟩

-- The direct definition of expansion is contained in the one
-- obtained from the transition relation.

direct→indirect : ∀ {i x y} →
                  D.[ i ] x ≳ y → [ i ] x ≳ y
direct→indirect D.now        = reflexive
direct→indirect (D.later  p) = later-cong λ { .force →
                                 direct→indirect (force p) }
direct→indirect (D.laterˡ p) = laterˡ (direct→indirect p)

-- If x makes a sequence of zero or more silent transitions to y, then
-- x is an expansion of y.

⇒→≳ : ∀ {i x y} → x ⇒ y → D.[ i ] x ≳ y
⇒→≳ done               = D.reflexive _
⇒→≳ (step _  later tr) = D.laterˡ (⇒→≳ tr)
⇒→≳ (step () now   tr)

-- If x makes a non-silent transition with the label y, then x is an
-- expansion of now y.

[just]⟶→≳now : ∀ {i x x′ y} → x [ just y ]⟶ x′ → D.[ i ] x ≳ now y
[just]⟶→≳now now = D.reflexive _

[just]⇒→≳now : ∀ {i x x′ y} → x [ just y ]⇒ x′ → D.[ i ] x ≳ now y
[just]⇒→≳now (steps tr now _) = ⇒→≳ tr

[just]⇒̂→≳now : ∀ {i x x′ y} → x [ just y ]⇒̂ x′ → D.[ i ] x ≳ now y
[just]⇒̂→≳now (silent () _)
[just]⇒̂→≳now (non-silent _ tr) = [just]⇒→≳now tr

[just]⟶̂→≳now : ∀ {i x x′ y} → x [ just y ]⟶̂ x′ → D.[ i ] x ≳ now y
[just]⟶̂→≳now (done ())
[just]⟶̂→≳now (step tr) = [just]⇒̂→≳now (⟶→⇒̂ tr)

-- The definition of expansion obtained from the transition relation
-- is contained in the direct one.

indirect→direct : ∀ {i} x y → [ i ] x ≳ y → D.[ i ] x ≳ y
indirect→direct {i} (now x) y =
  ([ i ] now x ≳ y)                                ↝⟨ (λ p → left-to-right p now) ⟩
  (∃ λ y′ → y [ just x ]⟶̂ y′ × [ i ] now x ≳′ y′)  ↝⟨ sym ∘ [just]⟶̂→≡now ∘ proj₁ ∘ proj₂ ⟩
  now x ≡ y                                        ↝⟨ (λ { refl → D.reflexive _ }) ⟩□
  D.[ i ] now x ≳ y                                □

indirect→direct {i} x (now y) =
  [ i ] x ≳ now y                                  ↝⟨ (λ p → right-to-left p now) ⟩
  (∃ λ x′ → x [ just y ]⇒ x′ × [ i ] x′ ≳′ now y)  ↝⟨ [just]⇒→≳now ∘ proj₁ ∘ proj₂ ⟩□
  D.[ i ] x ≳ now y                                □

indirect→direct (later x) (later y) lx≳ly =
  case left-to-right lx≳ly later of λ where
    (_ , step later , x≳′y) → D.later λ { .force {j} →
                                indirect→direct _ _
                                  (force x≳′y {j = j}) }
    (_ , done _     , x≳′ly) →
      let x′ , lx⇒x′ , x′≳′y = right-to-left lx≳ly later
      in lemma x≳′ly ([]⇒→⇒ _ lx⇒x′) x′≳′y
  where
  indirect→direct′ : ∀ {i x x′ y} →
                     x ⇒ x′ → [ i ] x′ ≳ y → D.[ i ] x ≳ y
  indirect→direct′ done               p = indirect→direct _ _ p
  indirect→direct′ (step _  later tr) p = D.laterˡ
                                            (indirect→direct′ tr p)
  indirect→direct′ (step () now   _)

  lemma :
    ∀ {i x x′} →
    [ i ] force x ≳′ later y →
    later x ⇒ x′ → [ i ] x′ ≳′ force y →
    D.[ i ] later x ≳ later y
  lemma x≳′ly done lx≳′y =
    D.later λ { .force →
      D.laterˡʳ⁻¹
        (indirect→direct _ _ (force lx≳′y))
        (indirect→direct _ _ (force x≳′ly)) }
  lemma x≳′ly (step _ later x⇒x′) x′≳′y =
    D.later λ { .force →
      indirect→direct′ x⇒x′ (force x′≳′y) }

-- The direct definition of the expansion relation is logically
-- equivalent to the one obtained from the transition relation.
--
-- TODO: Are the two definitions isomorphic?

direct⇔indirect : ∀ {i x y} → D.[ i ] x ≳ y ⇔ [ i ] x ≳ y
direct⇔indirect = record
  { to   = direct→indirect
  ; from = indirect→direct _ _
  }

------------------------------------------------------------------------
-- Some non-existence results

Now≳later-now = ∀ x → now x ≳ later (record { force = now x })

now≳later-now⇔uninhabited : Now≳later-now ⇔ ¬ A
now≳later-now⇔uninhabited =
  Now≳later-now     ↝⟨ inverse $ ∀-cong _ (λ _ → direct⇔indirect) ⟩
  DN.Now≳later-now  ↝⟨ DN.now≳later-now⇔uninhabited ⟩□
  ¬ A               □

Laterˡ⁻¹ = ∀ {x y} → later x ≳ y → force x ≳ y

laterˡ⁻¹⇔uninhabited : Laterˡ⁻¹ ⇔ ¬ A
laterˡ⁻¹⇔uninhabited =
  Laterˡ⁻¹       ↝⟨ inverse $ implicit-∀-cong _ $ implicit-∀-cong _ $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DN.Laterˡ⁻¹-≳  ↝⟨ DN.laterˡ⁻¹-≳⇔uninhabited ⟩□
  ¬ A            □

Laterʳ⁻¹-∼≳ =
  ∀ {i x} →
  [ i ] never ∼ later (record { force = now x }) →
  [ i ] never ≳ now x

size-preserving-laterʳ⁻¹-∼≳⇔uninhabited : Laterʳ⁻¹-∼≳ ⇔ ¬ A
size-preserving-laterʳ⁻¹-∼≳⇔uninhabited =
  Laterʳ⁻¹-∼≳     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ →-cong _ SD.direct⇔indirect direct⇔indirect ⟩
  DN.Laterʳ⁻¹-∼≳  ↝⟨ DN.size-preserving-laterʳ⁻¹-∼≳⇔uninhabited ⟩□
  ¬ A             □

Laterʳ⁻¹ = ∀ {i x y} → [ i ] x ≳ later y → [ i ] x ≳ force y

size-preserving-laterʳ⁻¹⇔uninhabited : Laterʳ⁻¹ ⇔ ¬ A
size-preserving-laterʳ⁻¹⇔uninhabited =
  Laterʳ⁻¹       ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DN.Laterʳ⁻¹-≳  ↝⟨ DN.size-preserving-laterʳ⁻¹-≳⇔uninhabited ⟩□
  ¬ A            □

Transitivity-∼≳ˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ∼ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivity-∼≳ˡ⇔uninhabited : Transitivity-∼≳ˡ ⇔ ¬ A
size-preserving-transitivity-∼≳ˡ⇔uninhabited =
  Transitivity-∼≳ˡ     ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                          →-cong _ SD.direct⇔indirect (→-cong _ direct⇔indirect direct⇔indirect) ⟩
  DN.Transitivity-∼≳ˡ  ↝⟨ DN.size-preserving-transitivity-∼≳ˡ⇔uninhabited ⟩□
  ¬ A                  □

Transitivityˡ =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≳ y → y ≳ z → [ i ] x ≳ z

size-preserving-transitivityˡ⇔uninhabited : Transitivityˡ ⇔ ¬ A
size-preserving-transitivityˡ⇔uninhabited =
  Transitivityˡ       ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                         →-cong _ direct⇔indirect (→-cong _ direct⇔indirect direct⇔indirect) ⟩
  DN.Transitivity-≳ˡ  ↝⟨ DN.size-preserving-transitivity-≳ˡ⇔uninhabited ⟩□
  ¬ A                 □

Transitivity =
  ∀ {i} {x y z : Delay A ∞} →
  [ i ] x ≳ y → [ i ] y ≳ z → [ i ] x ≳ z

size-preserving-transitivity⇔uninhabited : Transitivity ⇔ ¬ A
size-preserving-transitivity⇔uninhabited =
  Transitivity       ↝⟨ inverse $ implicit-∀-size-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $ implicit-∀-cong _ $
                        →-cong _ direct⇔indirect $ →-cong _ direct⇔indirect direct⇔indirect ⟩
  DN.Transitivity-≳  ↝⟨ DN.size-preserving-transitivity-≳⇔uninhabited ⟩□
  ¬ A                □

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to