text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe which includes several kinds of "relatedness" for sets,
-- such as equivalences, surjections and bijections
------------------------------------------------------------------------

module Function.Related where

open import Level
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq      using (Equivalence)
open import Function.Injection   as Inj     using (Injection; _↣_)
open import Function.Inverse     as Inv     using (Inverse; _↔_)
open import Function.LeftInverse as LeftInv using (LeftInverse)
open import Function.Surjection  as Surj    using (Surjection)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Wrapper types

-- Synonyms which are used to make _∼[_]_ below "constructor-headed"
-- (which implies that Agda can deduce the universe code from an
-- expression matching any of the right-hand sides).

record _←_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor lam
  field app-← : B → A

open _←_ public

record _↢_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor lam
  field app-↢ : B ↣ A

open _↢_ public

------------------------------------------------------------------------
-- Relatedness

-- There are several kinds of "relatedness".

-- The idea to include kinds other than equivalence and bijection came
-- from Simon Thompson and Bengt Nordström. /NAD

data Kind : Set where
  implication reverse-implication
    equivalence
    injection reverse-injection
    left-inverse surjection
    bijection
    : Kind

-- Interpretation of the codes above. The code "bijection" is
-- interpreted as Inverse rather than Bijection; the two types are
-- equivalent.

infix 4 _∼[_]_

_∼[_]_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Kind → Set ℓ₂ → Set _
A ∼[ implication         ] B = A → B
A ∼[ reverse-implication ] B = A ← B
A ∼[ equivalence         ] B = Equivalence (P.setoid A) (P.setoid B)
A ∼[ injection           ] B = Injection   (P.setoid A) (P.setoid B)
A ∼[ reverse-injection   ] B = A ↢ B
A ∼[ left-inverse        ] B = LeftInverse (P.setoid A) (P.setoid B)
A ∼[ surjection          ] B = Surjection  (P.setoid A) (P.setoid B)
A ∼[ bijection           ] B = Inverse     (P.setoid A) (P.setoid B)

-- A non-infix synonym.

Related : Kind → ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
Related k A B = A ∼[ k ] B

-- The bijective equality implies any kind of relatedness.

↔⇒ : ∀ {k x y} {X : Set x} {Y : Set y} →
     X ∼[ bijection ] Y → X ∼[ k ] Y
↔⇒ {implication}         = _⟨$⟩_ ∘ Inverse.to
↔⇒ {reverse-implication} = lam ∘′ _⟨$⟩_ ∘ Inverse.from
↔⇒ {equivalence}         = Inverse.equivalence
↔⇒ {injection}           = Inverse.injection
↔⇒ {reverse-injection}   = lam ∘′ Inverse.injection ∘ Inv.sym
↔⇒ {left-inverse}        = Inverse.left-inverse
↔⇒ {surjection}          = Inverse.surjection
↔⇒ {bijection}           = id

-- Actual equality also implies any kind of relatedness.

≡⇒ : ∀ {k ℓ} {X Y : Set ℓ} → X ≡ Y → X ∼[ k ] Y
≡⇒ P.refl = ↔⇒ Inv.id

------------------------------------------------------------------------
-- Special kinds of kinds

-- Kinds whose interpretation is symmetric.

data Symmetric-kind : Set where
  equivalence bijection : Symmetric-kind

-- Forgetful map.

⌊_⌋ : Symmetric-kind → Kind
⌊ equivalence ⌋ = equivalence
⌊ bijection   ⌋ = bijection

-- The proof of symmetry can be found below.

-- Kinds whose interpretation include a function which "goes in the
-- forward direction".

data Forward-kind : Set where
  implication equivalence injection
    left-inverse surjection bijection : Forward-kind

-- Forgetful map.

⌊_⌋→ : Forward-kind → Kind
⌊ implication  ⌋→ = implication
⌊ equivalence  ⌋→ = equivalence
⌊ injection    ⌋→ = injection
⌊ left-inverse ⌋→ = left-inverse
⌊ surjection   ⌋→ = surjection
⌊ bijection    ⌋→ = bijection

-- The function.

⇒→ : ∀ {k x y} {X : Set x} {Y : Set y} → X ∼[ ⌊ k ⌋→ ] Y → X → Y
⇒→ {implication}  = id
⇒→ {equivalence}  = _⟨$⟩_ ∘ Equivalence.to
⇒→ {injection}    = _⟨$⟩_ ∘ Injection.to
⇒→ {left-inverse} = _⟨$⟩_ ∘ LeftInverse.to
⇒→ {surjection}   = _⟨$⟩_ ∘ Surjection.to
⇒→ {bijection}    = _⟨$⟩_ ∘ Inverse.to

-- Kinds whose interpretation include a function which "goes backwards".

data Backward-kind : Set where
  reverse-implication equivalence reverse-injection
    left-inverse surjection bijection : Backward-kind

-- Forgetful map.

⌊_⌋← : Backward-kind → Kind
⌊ reverse-implication ⌋← = reverse-implication
⌊ equivalence         ⌋← = equivalence
⌊ reverse-injection   ⌋← = reverse-injection
⌊ left-inverse        ⌋← = left-inverse
⌊ surjection          ⌋← = surjection
⌊ bijection           ⌋← = bijection

-- The function.

⇒← : ∀ {k x y} {X : Set x} {Y : Set y} → X ∼[ ⌊ k ⌋← ] Y → Y → X
⇒← {reverse-implication} = app-←
⇒← {equivalence}         = _⟨$⟩_ ∘ Equivalence.from
⇒← {reverse-injection}   = _⟨$⟩_ ∘ Injection.to ∘ app-↢
⇒← {left-inverse}        = _⟨$⟩_ ∘ LeftInverse.from
⇒← {surjection}          = _⟨$⟩_ ∘ Surjection.from
⇒← {bijection}           = _⟨$⟩_ ∘ Inverse.from

-- Kinds whose interpretation include functions going in both
-- directions.

data Equivalence-kind : Set where
    equivalence left-inverse surjection bijection : Equivalence-kind

-- Forgetful map.

⌊_⌋⇔ : Equivalence-kind → Kind
⌊ equivalence  ⌋⇔ = equivalence
⌊ left-inverse ⌋⇔ = left-inverse
⌊ surjection   ⌋⇔ = surjection
⌊ bijection    ⌋⇔ = bijection

-- The functions.

⇒⇔ : ∀ {k x y} {X : Set x} {Y : Set y} →
     X ∼[ ⌊ k ⌋⇔ ] Y → X ∼[ equivalence ] Y
⇒⇔ {equivalence}  = id
⇒⇔ {left-inverse} = LeftInverse.equivalence
⇒⇔ {surjection}   = Surjection.equivalence
⇒⇔ {bijection}    = Inverse.equivalence

-- Conversions between special kinds.

⇔⌊_⌋ : Symmetric-kind → Equivalence-kind
⇔⌊ equivalence ⌋ = equivalence
⇔⌊ bijection   ⌋ = bijection

→⌊_⌋ : Equivalence-kind → Forward-kind
→⌊ equivalence  ⌋ = equivalence
→⌊ left-inverse ⌋ = left-inverse
→⌊ surjection   ⌋ = surjection
→⌊ bijection    ⌋ = bijection

←⌊_⌋ : Equivalence-kind → Backward-kind
←⌊ equivalence  ⌋ = equivalence
←⌊ left-inverse ⌋ = left-inverse
←⌊ surjection   ⌋ = surjection
←⌊ bijection    ⌋ = bijection

------------------------------------------------------------------------
-- Opposites

-- For every kind there is an opposite kind.

_op : Kind → Kind
implication         op = reverse-implication
reverse-implication op = implication
equivalence         op = equivalence
injection           op = reverse-injection
reverse-injection   op = injection
left-inverse        op = surjection
surjection          op = left-inverse
bijection           op = bijection

-- For every morphism there is a corresponding reverse morphism of the
-- opposite kind.

reverse : ∀ {k a b} {A : Set a} {B : Set b} →
          A ∼[ k ] B → B ∼[ k op ] A
reverse {implication}         = lam
reverse {reverse-implication} = app-←
reverse {equivalence}         = Eq.sym
reverse {injection}           = lam
reverse {reverse-injection}   = app-↢
reverse {left-inverse}        = Surj.fromRightInverse
reverse {surjection}          = Surjection.right-inverse
reverse {bijection}           = Inv.sym

------------------------------------------------------------------------
-- Equational reasoning

-- Equational reasoning for related things.

module EquationalReasoning where

  private

    refl : ∀ {k ℓ} → Reflexive (Related k {ℓ})
    refl {implication}         = id
    refl {reverse-implication} = lam id
    refl {equivalence}         = Eq.id
    refl {injection}           = Inj.id
    refl {reverse-injection}   = lam Inj.id
    refl {left-inverse}        = LeftInv.id
    refl {surjection}          = Surj.id
    refl {bijection}           = Inv.id

    trans : ∀ {k ℓ₁ ℓ₂ ℓ₃} →
            Trans (Related k {ℓ₁} {ℓ₂})
                  (Related k {ℓ₂} {ℓ₃})
                  (Related k {ℓ₁} {ℓ₃})
    trans {implication}         = flip _∘′_
    trans {reverse-implication} = λ f g → lam (app-← f ∘ app-← g)
    trans {equivalence}         = flip Eq._∘_
    trans {injection}           = flip Inj._∘_
    trans {reverse-injection}   = λ f g → lam (Inj._∘_ (app-↢ f) (app-↢ g))
    trans {left-inverse}        = flip LeftInv._∘_
    trans {surjection}          = flip Surj._∘_
    trans {bijection}           = flip Inv._∘_

  sym : ∀ {k ℓ₁ ℓ₂} →
        Sym (Related ⌊ k ⌋ {ℓ₁} {ℓ₂})
            (Related ⌊ k ⌋ {ℓ₂} {ℓ₁})
  sym {equivalence} = Eq.sym
  sym {bijection}   = Inv.sym

  infix  2 _∎
  infixr 2 _∼⟨_⟩_ _↔⟨_⟩_ _↔⟨⟩_ _≡⟨_⟩_

  _∼⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
           X ∼[ k ] Y → Y ∼[ k ] Z → X ∼[ k ] Z
  _ ∼⟨ X↝Y ⟩ Y↝Z = trans X↝Y Y↝Z

  -- Isomorphisms can be combined with any other kind of relatedness.

  _↔⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
           X ↔ Y → Y ∼[ k ] Z → X ∼[ k ] Z
  X ↔⟨ X↔Y ⟩ Y⇔Z = X ∼⟨ ↔⇒ X↔Y ⟩ Y⇔Z

  _↔⟨⟩_ : ∀ {k x y} (X : Set x) {Y : Set y} →
          X ∼[ k ] Y → X ∼[ k ] Y
  X ↔⟨⟩ X⇔Y = X⇔Y

  _≡⟨_⟩_ : ∀ {k ℓ z} (X : Set ℓ) {Y : Set ℓ} {Z : Set z} →
           X ≡ Y → Y ∼[ k ] Z → X ∼[ k ] Z
  X ≡⟨ X≡Y ⟩ Y⇔Z = X ∼⟨ ≡⇒ X≡Y ⟩ Y⇔Z

  _∎ : ∀ {k x} (X : Set x) → X ∼[ k ] X
  X ∎ = refl

-- For a symmetric kind and a fixed universe level we can construct a
-- setoid.

setoid : Symmetric-kind → (ℓ : Level) → Setoid _ _
setoid k ℓ = record
  { Carrier       = Set ℓ
  ; _≈_           = Related ⌊ k ⌋
  ; isEquivalence =
      record {refl = _ ∎; sym = sym; trans = _∼⟨_⟩_ _}
  } where open EquationalReasoning

-- For an arbitrary kind and a fixed universe level we can construct a
-- preorder.

preorder : Kind → (ℓ : Level) → Preorder _ _ _
preorder k ℓ = record
  { Carrier    = Set ℓ
  ; _≈_        = _↔_
  ; _∼_        = Related k
  ; isPreorder = record
    { isEquivalence = Setoid.isEquivalence (setoid bijection ℓ)
    ; reflexive     = ↔⇒
    ; trans         = _∼⟨_⟩_ _
    }
  } where open EquationalReasoning

------------------------------------------------------------------------
-- Some induced relations

-- Every unary relation induces a preorder and, for symmetric kinds,
-- an equivalence. (No claim is made that these relations are unique.)

InducedRelation₁ : Kind → ∀ {a s} {A : Set a} →
                   (A → Set s) → A → A → Set _
InducedRelation₁ k S = λ x y → S x ∼[ k ] S y

InducedPreorder₁ : Kind → ∀ {a s} {A : Set a} →
                   (A → Set s) → Preorder _ _ _
InducedPreorder₁ k S = record
  { _≈_        = P._≡_
  ; _∼_        = InducedRelation₁ k S
  ; isPreorder = record
    { isEquivalence = P.isEquivalence
    ; reflexive     = reflexive ∘
                      Setoid.reflexive (setoid bijection _) ∘
                      P.cong S
    ; trans         = trans
    }
  } where open Preorder (preorder _ _)

InducedEquivalence₁ : Symmetric-kind → ∀ {a s} {A : Set a} →
                      (A → Set s) → Setoid _ _
InducedEquivalence₁ k S = record
  { _≈_           = InducedRelation₁ ⌊ k ⌋ S
  ; isEquivalence = record {refl = refl; sym = sym; trans = trans}
  } where open Setoid (setoid _ _)

-- Every binary relation induces a preorder and, for symmetric kinds,
-- an equivalence. (No claim is made that these relations are unique.)

InducedRelation₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
                   (A → B → Set s) → B → B → Set _
InducedRelation₂ k _S_ = λ x y → ∀ {z} → (z S x) ∼[ k ] (z S y)

InducedPreorder₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
                   (A → B → Set s) → Preorder _ _ _
InducedPreorder₂ k _S_ = record
  { _≈_        = P._≡_
  ; _∼_        = InducedRelation₂ k _S_
  ; isPreorder = record
    { isEquivalence = P.isEquivalence
    ; reflexive     = λ x≡y {z} →
                        reflexive $
                        Setoid.reflexive (setoid bijection _) $
                        P.cong (_S_ z) x≡y

    ; trans         = λ i↝j j↝k → trans i↝j j↝k
    }
  } where open Preorder (preorder _ _)

InducedEquivalence₂ : Symmetric-kind →
                      ∀ {a b s} {A : Set a} {B : Set b} →
                      (A → B → Set s) → Setoid _ _
InducedEquivalence₂ k _S_ = record
  { _≈_           = InducedRelation₂ ⌊ k ⌋ _S_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = λ i↝j → sym i↝j
    ; trans = λ i↝j j↝k → trans i↝j j↝k
    }
  } where open Setoid (setoid _ _)


text:
{-# OPTIONS --cubical --no-sized-types --guardedness --safe #-}

module Issue3564 where
record Stream (A : Set) : Set where
  coinductive
  field head : A
  field tail : Stream A
open Stream

data A : Set where a : A

someA : Stream A
head someA = a
tail someA = someA

-- WAS: termination check failed
-- NOW: OK

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------------
-- The gcd is a common divisor
------------------------------------------------------------------------------

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

module LTC-PCF.Program.GCD.Partial.CommonDivisor where

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Divisibility.NotBy0
open import LTC-PCF.Data.Nat.Divisibility.NotBy0.Properties
open import LTC-PCF.Data.Nat.Induction.NonAcc.Lexicographic
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.EliminationProperties
open import LTC-PCF.Data.Nat.Inequalities.Properties
open import LTC-PCF.Data.Nat.Properties
open import LTC-PCF.Program.GCD.Partial.ConversionRules
open import LTC-PCF.Program.GCD.Partial.Definitions
open import LTC-PCF.Program.GCD.Partial.GCD
open import LTC-PCF.Program.GCD.Partial.Totality

------------------------------------------------------------------------------
-- Some cases of the gcd-∣₁.

-- We don't prove that
--
-- gcd-∣₁ : ... → (gcd m n) ∣ m

-- because this proof should be defined mutually recursive with the
-- proof
--
-- gcd-∣₂ : ... → (gcd m n) ∣ n.
--
-- Therefore, instead of proving
--
-- gcdCD : ... → CD m n (gcd m n)
--
-- using these proofs (i.e. the conjunction of them), we proved it
-- using well-founded induction.

-- gcd 0 (succ n) ∣ 0.
gcd-0S-∣₁ : ∀ {n} → N n → gcd zero (succ₁ n) ∣ zero
gcd-0S-∣₁ {n} Nn = subst (λ x → x ∣ zero)
                         (sym (gcd-0S n))
                         (S∣0 Nn)

-- gcd (succ₁ m) 0 ∣ succ₁ m.
gcd-S0-∣₁ : ∀ {m} → N m → gcd (succ₁ m) zero ∣ succ₁ m
gcd-S0-∣₁ {m} Nm = subst (λ x → x ∣ succ₁ m)
                         (sym (gcd-S0 m))
                         (∣-refl-S Nm)

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ m, when succ₁ m ≯ succ₁ n.
gcd-S≯S-∣₁ :
  ∀ {m n} → N m → N n →
  (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ succ₁ m) →
  succ₁ m ≯ succ₁ n →
  gcd (succ₁ m) (succ₁ n) ∣ succ₁ m
gcd-S≯S-∣₁ {m} {n} Nm Nn ih Sm≯Sn =
  subst (λ x → x ∣ succ₁ m)
        (sym (gcd-S≯S m n Sm≯Sn))
        ih

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ m when succ₁ m > succ₁ n.
-- We use gcd-∣₂.
-- We apply the theorem that if m∣n and m∣o then m∣(n+o).
gcd-S>S-∣₁ :
  ∀ {m n} → N m → N n →
  (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ (succ₁ m ∸ succ₁ n)) →
  (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ succ₁ n) →
  succ₁ m > succ₁ n →
  gcd (succ₁ m) (succ₁ n) ∣ succ₁ m

{- Proof:
1. gcd (Sm ∸ Sn) Sn | (Sm ∸ Sn)        IH
2. gcd (Sm ∸ Sn) Sn | Sn               gcd-∣₂
3. gcd (Sm ∸ Sn) Sn | (Sm ∸ Sn) + Sn   m∣n→m∣o→m∣n+o 1,2
4. Sm > Sn                             Hip
5. gcd (Sm ∸ Sn) Sn | Sm               arith-gcd-m>n₂ 3,4
6. gcd Sm Sn = gcd (Sm ∸ Sn) Sn        gcd eq. 4
7. gcd Sm Sn | Sm                      subst 5,6
-}

gcd-S>S-∣₁ {m} {n} Nm Nn ih gcd-∣₂ Sm>Sn =
  -- The first substitution is based on
  -- gcd (succ₁ m) (succ₁ n) = gcd (succ₁ m ∸ succ₁ n) (succ₁ n).
  subst (λ x → x ∣ succ₁ m)
        (sym (gcd-S>S m n Sm>Sn))
        -- The second substitution is based on
        -- m = (m ∸ n) + n.
        (subst (λ y → gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ y)
               (x>y→x∸y+y≡x (nsucc Nm) (nsucc Nn) Sm>Sn)
               (x∣y→x∣z→x∣y+z
                 {gcd (succ₁ m ∸ succ₁ n) (succ₁ n)}
                 {succ₁ m ∸ succ₁ n}
                 {succ₁ n}
                 (gcd-N Sm-Sn-N (nsucc Nn) (λ p → ⊥-elim (S≢0 (∧-proj₂ p))))
                 Sm-Sn-N
                 (nsucc Nn)
                 ih
                 gcd-∣₂
               )
       )
  where
  Sm-Sn-N : N (succ₁ m ∸ succ₁ n)
  Sm-Sn-N = ∸-N (nsucc Nm) (nsucc Nn)

------------------------------------------------------------------------------
-- Some case of the gcd-∣₂
-- We don't prove that gcd-∣₂ : ... → gcd m n ∣ n. The reason is
-- the same to don't prove gcd-∣₁ : ... → gcd m n ∣ m.

-- gcd 0 (succ₁ n) ∣₂ succ₁ n.
gcd-0S-∣₂ : ∀ {n} → N n → gcd zero (succ₁ n) ∣ succ₁ n
gcd-0S-∣₂ {n} Nn = subst (λ x → x ∣ succ₁ n)
                         (sym (gcd-0S n))
                         (∣-refl-S Nn)

-- gcd (succ₁ m) 0 ∣ 0.
gcd-S0-∣₂ : ∀ {m} → N m → gcd (succ₁ m) zero ∣ zero
gcd-S0-∣₂  {m} Nm = subst (λ x → x ∣ zero)
                          (sym (gcd-S0 m))
                          (S∣0 Nm)

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ n when succ₁ m > succ₁ n.
gcd-S>S-∣₂ :
  ∀ {m n} → N m → N n →
  (gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ succ₁ n) →
  succ₁ m > succ₁ n →
  gcd (succ₁ m) (succ₁ n) ∣ succ₁ n

gcd-S>S-∣₂ {m} {n} Nm Nn ih Sm>Sn =
  subst (λ x → x ∣ succ₁ n)
        (sym (gcd-S>S m n Sm>Sn))
        ih

-- gcd (succ₁ m) (succ₁ n) ∣ succ₁ n when succ₁ m ≯ succ₁ n.
-- We use gcd-∣₁.
-- We apply the theorem that if m∣n and m∣o then m∣(n+o).
gcd-S≯S-∣₂ :
  ∀ {m n} → N m → N n →
  (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ (succ₁ n ∸ succ₁ m)) →
  (gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ succ₁ m) →
  succ₁ m ≯ succ₁ n  →
  gcd (succ₁ m) (succ₁ n) ∣ succ₁ n

{- Proof:
1. gcd Sm (Sn ∸ Sm) | (Sn ∸ Sm)        IH
2  gcd Sm (Sn ∸ Sm) | Sm               gcd-∣₁
3. gcd Sm (Sn ∸ Sm) | (Sn ∸ Sm) + Sm   m∣n→m∣o→m∣n+o 1,2
4. Sm ≯ Sn                             Hip
5. gcd (Sm ∸ Sn) Sn | Sm               arith-gcd-m≤n₂ 3,4
6. gcd Sm Sn = gcd Sm (Sn ∸ Sm)        gcd eq. 4
7. gcd Sm Sn | Sn                      subst 5,6
-}

gcd-S≯S-∣₂ {m} {n} Nm Nn ih gcd-∣₁ Sm≯Sn =
  -- The first substitution is based on gcd m n = gcd m (n ∸ m).
  subst (λ x → x ∣ succ₁ n)
        (sym (gcd-S≯S m n Sm≯Sn))
         -- The second substitution is based on
         -- n = (n ∸ m) + m.
        (subst (λ y → gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ y)
               (x≤y→y∸x+x≡y (nsucc Nm) (nsucc Nn) (x≯y→x≤y (nsucc Nm) (nsucc Nn) Sm≯Sn))
               (x∣y→x∣z→x∣y+z
                 {gcd (succ₁ m) (succ₁ n ∸ succ₁ m)}
                 {succ₁ n ∸ succ₁ m}
                 {succ₁ m}
                 (gcd-N (nsucc Nm) Sn-Sm-N (λ p → ⊥-elim (S≢0 (∧-proj₁ p))))
                 Sn-Sm-N
                 (nsucc Nm)
                 ih
                 gcd-∣₁
               )
        )

  where
  Sn-Sm-N : N (succ₁ n ∸ succ₁ m)
  Sn-Sm-N = ∸-N (nsucc Nn) (nsucc Nm)

------------------------------------------------------------------------------
-- The gcd is CD.
-- We will prove that gcdCD : ... → CD m n (gcd m n).

-- The gcd 0 (succ₁ n) is CD.
gcd-0S-CD : ∀ {n} → N n → CD zero (succ₁ n) (gcd zero (succ₁ n))
gcd-0S-CD Nn = (gcd-0S-∣₁ Nn , gcd-0S-∣₂ Nn)

-- The gcd (succ₁ m) 0 is CD.
gcd-S0-CD : ∀ {m} → N m → CD (succ₁ m) zero (gcd (succ₁ m) zero)
gcd-S0-CD Nm = (gcd-S0-∣₁ Nm , gcd-S0-∣₂ Nm)

-- The gcd (succ₁ m) (succ₁ n) when succ₁ m > succ₁ n is CD.
gcd-S>S-CD :
  ∀ {m n} → N m → N n →
  (CD (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))) →
  succ₁ m > succ₁ n →
  CD (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S>S-CD {m} {n} Nm Nn acc Sm>Sn =
   (gcd-S>S-∣₁ Nm Nn acc-∣₁ acc-∣₂ Sm>Sn , gcd-S>S-∣₂ Nm Nn acc-∣₂ Sm>Sn)
  where
  acc-∣₁ : gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ (succ₁ m ∸ succ₁ n)
  acc-∣₁ = ∧-proj₁ acc

  acc-∣₂ : gcd (succ₁ m ∸ succ₁ n) (succ₁ n) ∣ succ₁ n
  acc-∣₂ = ∧-proj₂ acc

-- The gcd (succ₁ m) (succ₁ n) when succ₁ m ≯ succ₁ n is CD.
gcd-S≯S-CD :
  ∀ {m n} → N m → N n →
  (CD (succ₁ m) (succ₁ n ∸ succ₁ m) (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))) →
  succ₁ m ≯ succ₁ n →
  CD (succ₁ m) (succ₁ n) (gcd (succ₁ m) (succ₁ n))
gcd-S≯S-CD {m} {n} Nm Nn acc Sm≯Sn =
  (gcd-S≯S-∣₁ Nm Nn acc-∣₁ Sm≯Sn , gcd-S≯S-∣₂ Nm Nn acc-∣₂ acc-∣₁ Sm≯Sn)
  where
  acc-∣₁ : gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ succ₁ m
  acc-∣₁ = ∧-proj₁ acc

  acc-∣₂ : gcd (succ₁ m) (succ₁ n ∸ succ₁ m) ∣ (succ₁ n ∸ succ₁ m)
  acc-∣₂ = ∧-proj₂ acc

-- The gcd m n when m > n is CD.
gcd-x>y-CD :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → x≢0≢y o p → CD o p (gcd o p)) →
  m > n →
  x≢0≢y m n →
  CD m n (gcd m n)
gcd-x>y-CD nzero          Nn             _  0>n   _ = ⊥-elim (0>x→⊥ Nn 0>n)
gcd-x>y-CD (nsucc Nm)     nzero          _  _     _ = gcd-S0-CD Nm
gcd-x>y-CD (nsucc {m} Nm) (nsucc {n} Nn) ah Sm>Sn _ =
  gcd-S>S-CD Nm Nn ih Sm>Sn
  where
  -- Inductive hypothesis.
  ih : CD (succ₁ m ∸ succ₁ n) (succ₁ n) (gcd (succ₁ m ∸ succ₁ n) (succ₁ n))
  ih  = ah {succ₁ m ∸ succ₁ n}
           {succ₁ n}
           (∸-N (nsucc Nm) (nsucc Nn))
           (nsucc Nn)
           ([Sx∸Sy,Sy]<[Sx,Sy] Nm Nn)
           (λ p → ⊥-elim (S≢0 (∧-proj₂ p)))

-- The gcd m n when m ≯ n is CD.
gcd-x≯y-CD :
  ∀ {m n} → N m → N n →
  (∀ {o p} → N o → N p → Lexi o p m n → x≢0≢y o p → CD o p (gcd o p)) →
  m ≯ n →
  x≢0≢y m n →
  CD m n (gcd m n)
gcd-x≯y-CD nzero          nzero          _  _     h = ⊥-elim (h (refl , refl))
gcd-x≯y-CD nzero          (nsucc Nn)     _  _     _ = gcd-0S-CD Nn
gcd-x≯y-CD (nsucc _)      nzero          _  Sm≯0  _ = ⊥-elim (S≯0→⊥ Sm≯0)
gcd-x≯y-CD (nsucc {m} Nm) (nsucc {n} Nn) ah Sm≯Sn _ = gcd-S≯S-CD Nm Nn ih Sm≯Sn
  where
  -- Inductive hypothesis.
  ih : CD (succ₁ m) (succ₁ n ∸ succ₁ m)  (gcd (succ₁ m) (succ₁ n ∸ succ₁ m))
  ih = ah {succ₁ m}
          {succ₁ n ∸ succ₁ m}
          (nsucc Nm)
          (∸-N (nsucc Nn) (nsucc Nm))
          ([Sx,Sy∸Sx]<[Sx,Sy] Nm Nn)
          (λ p → ⊥-elim (S≢0 (∧-proj₁ p)))

-- The gcd is CD.
gcdCD : ∀ {m n} → N m → N n → x≢0≢y m n → CD m n (gcd m n)
gcdCD = Lexi-wfind A h
  where
  A : D → D → Set
  A i j = x≢0≢y i j → CD i j (gcd i j)

  h : ∀ {i j} → N i → N j → (∀ {k l} → N k → N l → Lexi k l i j → A k l) →
      A i j
  h Ni Nj ah = case (gcd-x>y-CD Ni Nj ah) (gcd-x≯y-CD Ni Nj ah) (x>y∨x≯y Ni Nj)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Numeral.Natural.Function.GreatestCommonDivisor.Extended where

import Lvl
open import Data
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Logic.Propositional
open import Numeral.Integer as ℤ
open import Numeral.Integer.Oper
open import Numeral.Integer.Proofs hiding (_≤_)
open import Numeral.Natural as ℕ
open import Numeral.Natural.Function.GreatestCommonDivisor
import      Numeral.Natural.Oper as ℕ
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Classical
open import Syntax.Number
open import Type

-- TODO: Does the same algorithm work in the naturals? https://math.stackexchange.com/questions/237372/finding-positive-b%C3%A9zout-coefficients https://math.stackexchange.com/questions/1230224/positive-solutions-of-893x-2432y-19?rq=1
gcdExt : ℕ → ℕ → (ℕ ⨯ ℤ ⨯ ℤ)
gcdExt a b = gcdFold(\{a (𝐒 b) _ (succ min) _ (x , y) → (y , (x − ((+ₙ(a ⌊/⌋ ℕ.𝐒(b))) ⋅ y)))}) (\_ _ _ _ _ → Tuple.swap) (1 , 0) a b

open import Logic.IntroInstances
open import Logic.Predicate
open import Numeral.Natural.Inductions
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.DivMod.Proofs
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Syntax.Function
open import Syntax.Transitivity

private variable a b d : ℕ

gcd-gcdExt-equal : (gcd a b ≡ Tuple.left(gcdExt a b))
gcd-gcdExt-equal {a}{b} = Gcd-unique {a}{b} Gcd-gcd Gcd-gcdFold

-- Also called: Bézout's identity, extended Euclid's algorithm.
gcd-linearCombination-existence : ∃{Obj = ℤ ⨯ ℤ}(\{(x , y) → (((+ₙ a) ⋅ x) + ((+ₙ b) ⋅ y) ≡ +ₙ(gcd a b))})
gcd-linearCombination-existence {a}{b} = [ℕ]-strong-induction {φ = b ↦ ∀{a} → ∃{Obj = ℤ ⨯ ℤ}(\{(x , y) → (((+ₙ a) ⋅ x) + ((+ₙ b) ⋅ y) ≡ +ₙ(gcd a b))})} base step {b}{a} where
  base : ∀{a} → ∃{Obj = ℤ ⨯ ℤ}(\{(x , y) → (((+ₙ a) ⋅ x) + (0 ⋅ y) ≡ +ₙ(gcd a 0))})
  ∃.witness (base {a})     = (1 , 0)
  ∃.proof   (base {ℕ.𝟎})   = [≡]-intro
  ∃.proof   (base {ℕ.𝐒 a}) = [≡]-intro

  step : ∀{i} → (∀{j} → (j ≤ i) → ∀{a} → ∃{Obj = ℤ ⨯ ℤ}(\{(x , y) → (((+ₙ a) ⋅ x) + ((+ₙ j) ⋅ y) ≡ +ₙ(gcd a j))})) → ∀{a} → ∃{Obj = ℤ ⨯ ℤ}(\{(x , y) → (((+ₙ a) ⋅ x) + ((+𝐒ₙ i) ⋅ y) ≡ +ₙ(gcd a (ℕ.𝐒(i))))})
  ∃.witness (step {i} prev {a}) with [≥]-or-[<] {a}{ℕ.𝐒(i)}
  ... | [∨]-introₗ ia with [∃]-intro (x , y) ← prev{a mod ℕ.𝐒(i)} ([≤]-without-[𝐒] (mod-maxᵣ {a = a})) {ℕ.𝐒(i)} = (y , ((x − ((+ₙ(a ⌊/⌋ ℕ.𝐒(i))) ⋅ y))))
  ... | [∨]-introᵣ (succ ai) with [∃]-intro (x , y) ← prev{a} ai {ℕ.𝐒(i)} = (y , x)
  ∃.proof (step {i} prev {a}) with [≥]-or-[<] {a}{ℕ.𝐒(i)}
  ... | [∨]-introₗ ia with [∃]-intro (x , y) ⦃ p ⦄ ← prev{a mod ℕ.𝐒(i)} ([≤]-without-[𝐒] (mod-maxᵣ {a = a})) {ℕ.𝐒(i)} =
    ((+ₙ a) ⋅ y) + ((+𝐒ₙ i) ⋅ (x − ((+ₙ(a ⌊/⌋ ℕ.𝐒(i))) ⋅ y)))             🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)((+ₙ a) ⋅ y) (distributivityₗ(_⋅_)(_−_) {+𝐒ₙ i}{x}{(+ₙ(a ⌊/⌋ ℕ.𝐒(i))) ⋅ y}) ]
    ((+ₙ a) ⋅ y) + (((+𝐒ₙ i) ⋅ x) − ((+𝐒ₙ i) ⋅ ((+ₙ(a ⌊/⌋ ℕ.𝐒(i))) ⋅ y))) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)((+ₙ a) ⋅ y) (congruence₂ᵣ(_−_)((+𝐒ₙ i) ⋅ x) p1) ]
    ((+ₙ a) ⋅ y) + (((+𝐒ₙ i) ⋅ x) − ((+ₙ(a ℕ.−₀ (a mod ℕ.𝐒(i)))) ⋅ y))    🝖[ _≡_ ]-[ One.commuteₗ-assocᵣ{a = (+ₙ a) ⋅ y}{b = (+𝐒ₙ i) ⋅ x} ]
    ((+𝐒ₙ i) ⋅ x) + (((+ₙ a) ⋅ y) − ((+ₙ(a ℕ.−₀ (a mod ℕ.𝐒(i)))) ⋅ y))    🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)((+𝐒ₙ i) ⋅ x) (distributivityᵣ(_⋅_)(_−_) {+ₙ a}{_}{y}) ]-sym
    ((+𝐒ₙ i) ⋅ x) + (((+ₙ a) − (+ₙ(a ℕ.−₀ (a mod ℕ.𝐒(i))))) ⋅ y)          🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)((+𝐒ₙ i) ⋅ x) (congruence₂ₗ(_⋅_)(y) p2) ]
    ((+𝐒ₙ i) ⋅ x) + ((+ₙ(a mod ℕ.𝐒(i))) ⋅ y)                              🝖[ _≡_ ]-[ p ]
    +ₙ(gcd (ℕ.𝐒(i)) (a mod ℕ.𝐒(i)))                                       🝖-end
    where
      p0 =
        (ℕ.𝐒 i) ℕ.⋅ (a ⌊/⌋ ℕ.𝐒(i)) 🝖[ _≡_ ]-[ commutativity(ℕ._⋅_) {ℕ.𝐒 i}{a ⌊/⌋ ℕ.𝐒(i)} ]
        (a ⌊/⌋ ℕ.𝐒(i)) ℕ.⋅ (ℕ.𝐒 i) 🝖[ _≡_ ]-[ OneTypeTwoOp.moveᵣ-to-invOp {b = a mod ℕ.𝐒(i)}{c = a} (([⌊/⌋][mod]-is-division-with-remainder {y = i})) ]
        a ℕ.−₀ (a mod ℕ.𝐒(i))      🝖-end

      p1 =
        (+𝐒ₙ i) ⋅ ((+ₙ(a ⌊/⌋ ℕ.𝐒(i))) ⋅ y)     🝖[ _≡_ ]-[ associativity(_⋅_) {+𝐒ₙ i} ]-sym
        ((+𝐒ₙ i) ⋅ (+ₙ(a ⌊/⌋ ℕ.𝐒(i)))) ⋅ y     🝖[ _≡_ ]-[]
        ((+ₙ(ℕ.𝐒 i)) ⋅ (+ₙ(a ⌊/⌋ ℕ.𝐒(i)))) ⋅ y 🝖[ _≡_ ]-[ congruence₂ₗ(_⋅_)(y) (preserving₂(+ₙ_)(ℕ._⋅_)(_⋅_) {ℕ.𝐒 i}) ]-sym
        (+ₙ((ℕ.𝐒 i) ℕ.⋅ (a ⌊/⌋ ℕ.𝐒(i)))) ⋅ y   🝖[ _≡_ ]-[ congruence₂ₗ(_⋅_)(y) (congruence₁(+ₙ_) p0) ]
        (+ₙ(a ℕ.−₀ (a mod ℕ.𝐒(i)))) ⋅ y        🝖-end

      p2 =
        (+ₙ a) − (+ₙ(a ℕ.−₀ (a mod ℕ.𝐒(i))))          🝖[ _≡_ ]-[ congruence₂ᵣ(_−_)(+ₙ a) ([+ₙ][−₀][−]-preserving (mod-maxₗ {a}{ℕ.𝐒(i)})) ]
        (+ₙ a) − ((+ₙ a) − (+ₙ(a mod ℕ.𝐒(i))))        🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(+ₙ a) (preserving₂(−_)(_+_)(_+_) {+ₙ a}{−(+ₙ(a mod ℕ.𝐒(i)))}) ]
        (+ₙ a) + ((−(+ₙ a)) − (−(+ₙ(a mod ℕ.𝐒(i)))))  🝖[ _≡_ ]-[ associativity(_+_) {+ₙ a}{−(+ₙ a)} ]-sym
        ((+ₙ a) − (+ₙ a)) − (−(+ₙ(a mod ℕ.𝐒(i))))     🝖[ _≡_ ]-[ congruence₂(_+_) (inverseFunctionᵣ(_+_)(−_) {+ₙ a}) (involution(−_)) ]
        0 + (+ₙ(a mod ℕ.𝐒(i)))                        🝖[ _≡_ ]-[ identityₗ(_+_)(0) ]
        +ₙ(a mod ℕ.𝐒(i))                              🝖[ _≡_ ]-end
  ... | [∨]-introᵣ (succ ai) with [∃]-intro (x , y) ⦃ p ⦄ ← prev{a} ai {ℕ.𝐒(i)} = commutativity(_+_) {(+ₙ a) ⋅ y}{(+ₙ ℕ.𝐒(i)) ⋅ x} 🝖 p

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Issue2229Reexport2 where

open import Issue2229Base public


text:
module View where

open import Data.Unit
open import Data.Char
open import Data.Maybe
open import Data.Container.Indexed

open import Signature
open import Model
open import IO.Primitive

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

postulate
  view : Model → IO ⊤

data VtyEvent : Set where
  key   : Char → VtyEvent
  enter : VtyEvent

vtyToCmd : VtyEvent → (m : Mode) → Maybe (Command Hårss m)
vtyToCmd (key 'j')  cmd            = just (moveP down)
vtyToCmd (key 'k')  cmd            = just (moveP up)
vtyToCmd (key 'a')  cmd            = just (promptP addFeed)
vtyToCmd (key '\t') cmd            = just (promptP search)
vtyToCmd (key 'R')  cmd            = just fetchP
vtyToCmd _          cmd            = nothing
vtyToCmd enter      (input p)      = just doneP
vtyToCmd (key '\t') (input search) = just searchNextP
vtyToCmd (key c)    (input p)      = just (putCharP c)

max_stars_repo_name: stevana/haarss

max_issues_repo_name: stevana/haarss

max_forks_repo_name: stevana/haarss


text:
{- Basic combinators, basic permutations, and their relation -}
module CombPerm where

import Data.Fin as F
--
open import Data.Unit
open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _>_ )
open import Data.Sum using (inj₁ ; inj₂ ; _⊎_)
open import Data.Vec
open import Function using ( id ) renaming (_∘_ to _○_)
open import Relation.Binary  -- to make certain goals look nicer
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong ; trans ; subst ; module ≡-Reasoning )
open ≡-Reasoning

-- start re-splitting things up, as this is getting out of hand
open import FT -- Finite Types
open import VecHelpers
open import NatSimple
open import Eval
open import Permutations

-- This should really go elsewhere!
finToVal : {n : ℕ} → F.Fin n → ⟦ fromℕ n ⟧
finToVal F.zero = inj₁ tt
finToVal (F.suc n) = inj₂ (finToVal n)

valToFin : {n : ℕ} → ⟦ fromℕ n ⟧ → F.Fin n
valToFin {zero} ()
valToFin {suc n} (inj₁ tt) = F.zero
valToFin {suc n} (inj₂ v) = F.suc (valToFin v)

finToValToFin : {n : ℕ} → (v : ⟦ fromℕ n ⟧) → finToVal (valToFin v) ≡ v
finToValToFin {zero} ()
finToValToFin {suc n} (inj₁ tt)  = refl -- (inj₁ tt)
finToValToFin {suc n} (inj₂ v) = cong inj₂ (finToValToFin v)

valToFinToVal : {n : ℕ} → (i : F.Fin n) → valToFin (finToVal i) ≡ i
valToFinToVal F.zero = refl -- F.zero
valToFinToVal (F.suc i) = cong F.suc (valToFinToVal i)

-- construct a combinator which represents the swapping of the i-th and
-- (i+1)-th 'bit' of a finite type.
-- Best to think of this as an 'elementary permutation', in the same way
-- we have 'elementary matrices' (which turn out to be permutations when they
-- are unitary).
swapi : {n : ℕ} → F.Fin n → (fromℕ (suc n)) ⇛ (fromℕ (suc n))
swapi {zero}  ()
swapi {suc n} F.zero    = assocl₊⇛ ◎ (swap₊⇛ ⊕ id⇛) ◎ assocr₊⇛
swapi {suc n} (F.suc i) = id⇛ ⊕ swapi {n} i

swapiPerm : {n : ℕ} → F.Fin n → Permutation (suc n)
swapiPerm {zero} ()
swapiPerm {suc n} F.zero = F.suc F.zero ∷ idP
swapiPerm {suc n} (F.suc i) = F.zero ∷ swapiPerm {n} i

swapiAct : {n : ℕ} {A : Set} → (i : F.Fin n) → (v : Vec A (suc n)) →
    permute (swapiPerm i) v ≡ insert (remove (F.inject₁ i) v) (F.suc i) (v !! (F.inject₁ i))
swapiAct {zero} () v
swapiAct {suc n} F.zero (x ∷ y ∷ v) = cong (λ z → y ∷ x ∷ z) (idP-id v)
swapiAct {suc n} (F.suc i) (x ∷ v) = cong (_∷_ x) (swapiAct i v)

-- swapUpTo i permutes the combinator left by one up to i
-- if possible values are X a b c Y d e, swapUpTo 3's possible outputs
-- are a b c X Y d e
swapUpTo : {n : ℕ} → F.Fin n → (fromℕ (suc n)) ⇛ (fromℕ (suc n))
swapUpTo F.zero    = id⇛
swapUpTo (F.suc i) = (id⇛ ⊕ swapUpTo i) ◎ swapi F.zero

-- 1 i times, 0 for the rest
1iP : {n : ℕ} → F.Fin n → Permutation (suc n)
1iP F.zero = idP
1iP (F.suc i) = (F.suc F.zero) ∷ 1iP i

-- The permutation we need:
-- [i, 0, 0, 0, 0, ...]
swapUpToPerm : {n : ℕ} → F.Fin n → Permutation (suc n)
swapUpToPerm F.zero    = idP
swapUpToPerm (F.suc j) = (F.inject₁ (F.suc j)) ∷ idP

-- swapDownFrom i permutes the combinator right by one up to i (the reverse
-- of swapUpTo)
swapDownFrom : {n : ℕ} → F.Fin n → (fromℕ (suc n)) ⇛ (fromℕ (suc n))
swapDownFrom F.zero    = id⇛
swapDownFrom (F.suc i) = swapi F.zero ◎ (id⇛ ⊕ swapDownFrom i)

-- The permutation we need:
-- [1, 1, 1, ..., 1, 0, 0, 0, ...]
-- |--i-1 times---|
swapDownFromPerm : {n : ℕ} → F.Fin n → Permutation (suc n)
swapDownFromPerm = 1iP
-- swapDownFromPerm F.zero = idP
-- swapDownFromPerm (F.suc i) = (F.suc F.zero) ∷ swapDownFromPerm i

-- swapm i returns a combinator that swaps 0 and i
swapm : {n : ℕ} → F.Fin n → (fromℕ n) ⇛ (fromℕ n)
swapm F.zero = id⇛
swapm (F.suc i) = swapDownFrom i ◎ swapi i ◎ swapUpTo i

swapOne : {n : ℕ} → (i : F.Fin n) → Permutation n
swapOne F.zero = idP
swapOne {suc zero} (F.suc ())
swapOne {suc (suc n)} (F.suc i) = (F.suc F.zero) ∷ swapOne i

-- which should correspond to this permutation!!
swapmPerm : {n : ℕ} → F.Fin n → Permutation n
swapmPerm F.zero = idP
swapmPerm {suc n} (F.suc i) = F.suc i ∷ swapOne i

permToComb : {n : ℕ} → Permutation n → (fromℕ n ⇛ fromℕ n)
permToComb [] = id⇛
permToComb (F.zero ∷ p) = id⇛ ⊕ permToComb p
permToComb (F.suc n ∷ p) = swapm (F.suc n) ◎ (id⇛ ⊕ permToComb p)

swap01 : (n : ℕ) → Permutation n
swap01 zero = []
swap01 (suc zero) = F.zero ∷ []
swap01 (suc (suc n)) = F.suc (F.zero) ∷ idP

vmap-insert : {n : ℕ} {A B : Set} {x : A} → (v : Vec A n) → (f : A → B) → (i : F.Fin (suc n)) → vmap f (insert v i x) ≡ insert (vmap f v) i (f x)
vmap-insert {zero} [] f F.zero = refl
vmap-insert {zero} [] f (F.suc ())
vmap-insert {suc n} v f F.zero = refl
vmap-insert {suc n} {x = x} (y ∷ v) f (F.suc i) = cong (_∷_ (f y)) (vmap-insert v f i)

vmap-permute : {n : ℕ} {A B : Set} → (p : Permutation n) → (v : Vec A n) → (f : A → B) → vmap f (permute p v) ≡ permute p (vmap f v)
vmap-permute {zero} [] [] f = refl
vmap-permute {suc n} (i ∷ p) (x ∷ v) f = trans (vmap-insert (permute p v) f i) (cong (λ y → insert y i (f x)) (vmap-permute p v f))

evalPerm : {n : ℕ} → Permutation n → F.Fin n → F.Fin n
evalPerm {zero} _ ()
evalPerm {suc n} p k = lookup k (permute p (allFin (suc n)))

testP5 : Vec (F.Fin five) five
testP5 = permute (swapmPerm (F.inject (F.fromℕ three))) (allFin five)

push-f-through : {n : ℕ} {A B : Set} → (f : A → B) → (j : F.Fin n) → (p : Permutation n) → (g : F.Fin n → A) → f (lookup j (permute p (tabulate g))) ≡ lookup j (permute p (tabulate (f ○ g)))
push-f-through {zero} f () p g
push-f-through {suc n} f j p g = begin
   f (lookup j (permute p (tabulate g)))            ≡⟨ sym (map!! f (permute p (tabulate g)) j) ⟩
   lookup j (vmap f (permute p (tabulate g)))       ≡⟨ cong (lookup j) (vmap-permute p (tabulate g) f) ⟩
   lookup j (permute p (vmap f (tabulate g)))       ≡⟨ cong (λ x → lookup j (permute p x)) (mapTab f g) ⟩
   lookup j (permute p (tabulate (f ○ g))) ∎

-- Just to make a lot of the proofs look nicer
vId : {n : ℕ} → Vec (F.Fin n) n
vId = tabulate id

vS : {n : ℕ} → Vec (F.Fin (suc n)) n
vS = tabulate F.suc

vSS : {n : ℕ} → Vec (F.Fin (suc (suc n))) n
vSS = tabulate (F.suc ○ F.suc)

swapiCorrect : {n : ℕ} → (i : F.Fin n) → (j : F.Fin (1 + n)) → evalComb (swapi i) (finToVal j) ≡ finToVal (evalPerm (swapiPerm i) j)
swapiCorrect {zero} () _
swapiCorrect {suc n} F.zero F.zero = refl
swapiCorrect {suc zero} F.zero (F.suc F.zero) = refl
swapiCorrect {suc zero} F.zero (F.suc (F.suc ()))
swapiCorrect {suc zero} (F.suc ()) j
swapiCorrect {suc (suc n)} (F.suc i) F.zero = refl
swapiCorrect {suc (suc n)} F.zero (F.suc F.zero) = refl
swapiCorrect {suc (suc n)} F.zero (F.suc (F.suc j)) = cong finToVal
  let F2 = F.suc ○ F.suc in
  begin
    F2 j
                                 ≡⟨ cong F2 (sym (lookupTab {f = id} j)) ⟩
    F2 (lookup j (tabulate id))
                                 ≡⟨ cong (λ x → F2 (lookup j x)) (sym (idP-id (tabulate id))) ⟩
    F2 (lookup j (permute idP (tabulate id)))
                                 ≡⟨ push-f-through F2 j idP id ⟩
    lookup j (permute idP (tabulate F2)) ∎
swapiCorrect {suc (suc n)} (F.suc i) (F.suc j) =
  begin
   evalComb (swapi (F.suc i)) (finToVal (F.suc j))
                                   ≡⟨ refl ⟩
   inj₂ (evalComb (swapi i) (finToVal j))
                                   ≡⟨ cong inj₂ (swapiCorrect {suc n} i j) ⟩
   inj₂ (finToVal (evalPerm (swapiPerm i) j))
                                   ≡⟨ refl ⟩
   inj₂ (finToVal (lookup j (permute (swapiPerm i) (tabulate id))))
                                   ≡⟨ refl ⟩
   finToVal (F.suc (lookup j (permute (swapiPerm i) (tabulate id))))
                                   ≡⟨ cong finToVal (push-f-through F.suc j (swapiPerm i) id) ⟩
   finToVal (lookup j (permute (swapiPerm i) (tabulate F.suc))) ∎

-- JC: Need seriously better names for the next 3 lemmas!!
lookup-insert : {n : ℕ} {A : Set} → (v : Vec A (suc n)) → {i : F.Fin (suc n)} → {a : A} →
    lookup F.zero (insert v (F.suc i) a) ≡ lookup F.zero v
lookup-insert (x ∷ v) = refl

lookup-insert′ : {n : ℕ} {A : Set} (i : F.Fin (suc n)) {a : A} → (v : Vec A n) →
    lookup i (insert v i a) ≡ a
lookup-insert′ F.zero [] = refl
lookup-insert′ (F.suc ()) []
lookup-insert′ F.zero (x ∷ v) = refl
lookup-insert′ (F.suc i) (x ∷ v) = lookup-insert′ i v

-- this is what is needed in swapDownCorrect, but would be true for any j < i instead of F.suc F.zero < F.suc i
lookup-insert′′ : {n : ℕ} {A : Set} {a : A} → (i : F.Fin n) → (v : Vec A (suc n)) →
    lookup (F.suc i) v ≡ lookup (F.suc (F.suc i)) (insert v (F.suc F.zero) a)
lookup-insert′′ {zero} () v
lookup-insert′′ {suc n} i (x ∷ v) = refl

-- this should be unified with the previous
lookup-insert3 : {n : ℕ} {A : Set} {a : A} → (i : F.Fin n) → (v : Vec A n) →
    lookup i v ≡ lookup (F.suc i) (insert v (F.inject₁ i) a)
lookup-insert3 {zero} () v
lookup-insert3 {suc n} F.zero (x ∷ v) = refl
lookup-insert3 {suc n} (F.suc i) (x ∷ v) = lookup-insert3 i v

lookup+1-insert-remove : {n : ℕ} {A : Set} {a : A} → (i : F.Fin n) → (v : Vec A (suc n)) →
  lookup (F.inject₁ i) (insert (remove (F.inject₁ i) v) (F.suc i) a) ≡ lookup (F.suc i) v
lookup+1-insert-remove {zero} () _
lookup+1-insert-remove {suc n} F.zero (x ∷ x₁ ∷ v) = refl
lookup+1-insert-remove {suc n} (F.suc i) (x ∷ v) = lookup+1-insert-remove i v

-- insert (remove (F.inject₁ (F.suc i)) (tabulate id)) (F.suc (F.suc i)) (F.inject₁ (F.suc i)) !! (F.inject₁ (F.suc i))

lookup-idP-id : {n : ℕ} → (i : F.Fin n) → lookup i (permute idP vId) ≡ i
lookup-idP-id i = trans (cong (lookup i) (idP-id vId)) (lookupTab i)

swapUpToAct : {n : ℕ} {A : Set} → (i : F.Fin n) → (v : Vec A (suc n)) →
    permute (swapUpToPerm i) v ≡ insert (remove F.zero v) (F.inject₁ i) (v !! F.zero)
swapUpToAct F.zero v = trans (idP-id v) (remove0 v)
swapUpToAct (F.suc i) (x ∷ v) = cong (λ z → insert z (F.suc (F.inject₁ i)) x) (idP-id v)

swapDownFromVec : {n : ℕ} {A : Set} → (i : F.Fin (suc n)) → Vec A (suc n) →
                  Vec A (suc n)
swapDownFromVec i v = (v !! i) ∷ remove i v

swapDownFromAct : {n : ℕ} → {A : Set} → (i : F.Fin n) → (v : Vec A (suc n)) →
                  permute (swapDownFromPerm i) v ≡
                    swapDownFromVec (F.inject₁ i) v
swapDownFromAct {zero} () _
swapDownFromAct {suc n} F.zero (x ∷ v) =
  begin
    permute (swapDownFromPerm F.zero) (x ∷ v)
      ≡⟨ refl ⟩
    permute idP (x ∷ v)
      ≡⟨ idP-id (x ∷ v) ⟩
    swapDownFromVec F.zero (x ∷ v) ∎
swapDownFromAct {suc zero} (F.suc ()) _
swapDownFromAct {suc (suc n)} (F.suc i) (x ∷ y ∷ v) =
  begin
    permute (swapDownFromPerm (F.suc i)) (x ∷ y ∷ v)
      ≡⟨ refl ⟩
    permute (F.suc F.zero ∷ 1iP i) (x ∷ y ∷ v)
      ≡⟨ refl ⟩
    insert (permute (swapDownFromPerm i) (y ∷ v)) (F.suc F.zero) x
      ≡⟨ cong (λ q → insert q (F.suc F.zero) x) (swapDownFromAct i (y ∷ v)) ⟩
    insert (swapDownFromVec (F.inject₁ i) (y ∷ v)) (F.suc F.zero) x
      ≡⟨ refl ⟩
    ((y ∷ v) !! (F.inject₁ i)) ∷ x ∷ remove (F.inject₁ i) (y ∷ v)
      ≡⟨ refl ⟩
    swapDownFromVec (F.inject₁ (F.suc i)) (x ∷ y ∷ v) ∎

swapmVec : {n : ℕ} {A : Set} → F.Fin n → Vec A n → Vec A n
swapmVec {zero} () _
swapmVec {suc n} F.zero v = v
swapmVec {suc zero} (F.suc ()) _
swapmVec {suc (suc n)} (F.suc i) (x ∷ v) =
  (v !! i) ∷ (insert (remove i v) i x)

swapOneVec : {n : ℕ} {A : Set} → F.Fin n → Vec A n → Vec A n
swapOneVec {zero} () _
swapOneVec {suc n} F.zero v = v
swapOneVec {suc n} (F.suc i) v = (v !! (F.suc i)) ∷ (remove (F.suc i) v)

swapOneAct : {n : ℕ} {A : Set} → (i : F.Fin n) → (v : Vec A n) →
           permute (swapOne i) v ≡ swapOneVec i v
swapOneAct {zero} () _
swapOneAct {suc n} F.zero (x ∷ v) = cong (_∷_ x) (idP-id v)
swapOneAct {suc zero} (F.suc ()) v
swapOneAct {suc (suc n)} (F.suc F.zero) (x ∷ y ∷ v) = cong (λ z → y ∷ x ∷ z) (idP-id v)
swapOneAct {suc (suc n)} (F.suc (F.suc i)) (x ∷ v) =
  begin
    permute (swapOne (F.suc (F.suc i))) (x ∷ v)
        ≡⟨ refl ⟩
    insert (permute (swapOne (F.suc i)) v) (F.suc F.zero) x
        ≡⟨ cong (λ y → insert y (F.suc F.zero) x) (swapOneAct (F.suc i) v) ⟩
    insert (swapOneVec (F.suc i) v) (F.suc F.zero) x
        ≡⟨ refl ⟩ -- lots of β reduction
    ((x ∷ v) !! (F.suc (F.suc i))) ∷ (remove (F.suc (F.suc i)) (x ∷ v))
        ≡⟨ refl ⟩
    swapOneVec (F.suc (F.suc i)) (x ∷ v)
  ∎

swapmAct : {n : ℕ} {A : Set} → (i : F.Fin n) → (v : Vec A n) →
           permute (swapmPerm i) v ≡ swapmVec i v
swapmAct {zero} () _
swapmAct {suc n} F.zero (x ∷ v) =
  begin
    permute (swapmPerm F.zero) (x ∷ v)
      ≡⟨ idP-id (x ∷ v) ⟩
    swapmVec F.zero (x ∷ v) ∎
swapmAct {suc zero} (F.suc ()) _
swapmAct {suc (suc n)} (F.suc F.zero) (x ∷ y ∷ v) = cong (λ z → y ∷ x ∷ z) (idP-id v)
swapmAct {suc (suc n)} (F.suc (F.suc i)) (x ∷ y ∷ v) =
  begin
    permute (swapmPerm (F.suc (F.suc i))) (x ∷ y ∷ v)
      ≡⟨ refl ⟩
    permute (F.suc (F.suc i) ∷ swapOne (F.suc i)) (x ∷ y ∷ v)
      ≡⟨ refl ⟩
    insert (permute (swapOne (F.suc i)) (y ∷ v)) (F.suc (F.suc i)) x
      ≡⟨ cong (λ z → insert z (F.suc (F.suc i)) x) (swapOneAct (F.suc i) (y ∷ v)) ⟩
    insert (swapOneVec (F.suc i) (y ∷ v)) (F.suc (F.suc i)) x
      ≡⟨ refl ⟩  -- by lots of beta on both sides
    ((y ∷ v) !! (F.suc i)) ∷ (insert (remove (F.suc i) (y ∷ v)) (F.suc i) x)
      ≡⟨ refl ⟩
    swapmVec (F.suc (F.suc i)) (x ∷ y ∷ v) ∎

swapi≡swap01 : {n : ℕ} → (j : F.Fin (suc (suc n))) →  evalComb (assocl₊⇛ ◎ (swap₊⇛ ⊕ id⇛) ◎ assocr₊⇛) (finToVal j) ≡ finToVal (evalPerm (swap01 (suc (suc n))) j)
swapi≡swap01 F.zero = refl
swapi≡swap01 (F.suc F.zero) = refl
swapi≡swap01 (F.suc (F.suc j)) = sym (trans
    (cong (λ x → finToVal (x !! j)) (idP-id _))
    (cong finToVal (lookupTab j)))

-- this is the raw swap01 vector
swap01vec : {n : ℕ} → Vec (F.Fin (2 + n)) (2 + n)
swap01vec = F.suc F.zero ∷ F.zero ∷ vSS

-- this is the one we 'naturally' get via permutation
swap01vec′ : (n : ℕ) → Vec (F.Fin (2 + n)) (2 + n)
swap01vec′ n = permute (swap01 (suc (suc n))) vId

-- but they are the same!
swap01Correct : (n : ℕ) → swap01vec′ n ≡ swap01vec {n}
swap01Correct zero = refl
swap01Correct (suc n) = cong (λ x → F.suc F.zero ∷ F.zero ∷ x) (idP-id _)

newlemma6 : {m n : ℕ} → (i : F.Fin n) → (v : Vec (F.Fin m) n) →
            (vmap F.suc (insert (vmap F.suc v) (F.inject₁ i) F.zero)) ∘̬′ swap01vec
          ≡ insert (vmap F.suc (vmap F.suc v)) (F.inject₁ i) F.zero
newlemma6 F.zero (x ∷ v) =
  let suc2v = vmap F.suc (vmap F.suc v) in
  begin
  vmap F.suc (insert (vmap F.suc (x ∷ v)) F.zero F.zero) ∘̬′ swap01vec
    ≡⟨ refl ⟩
  (F.suc F.zero ∷ F.suc (F.suc x) ∷ suc2v) ∘̬′ swap01vec
    ≡⟨ refl ⟩
  F.zero ∷ ((F.suc (F.suc x) ∷ suc2v) ∘̬′ swap01vec)
    ≡⟨ refl ⟩
  F.zero ∷ (vSS !! x) ∷ (suc2v ∘̬′ swap01vec)
    ≡⟨ cong (λ x → F.zero ∷ x ∷ suc2v ∘̬′ swap01vec) (lookupTab x) ⟩
  F.zero ∷ F.suc (F.suc x) ∷ (suc2v ∘̬′ swap01vec)
    ≡⟨ cong (λ q → F.zero ∷ F.suc (F.suc x) ∷ q) (map2+id v) ⟩
  F.zero ∷ F.suc (F.suc x) ∷ suc2v
    ≡⟨ refl ⟩
  insert (vmap F.suc (vmap F.suc (x ∷ v))) F.zero F.zero ∎
newlemma6 (F.suc i) (x ∷ v) =
  let v′ = insert (vmap F.suc v) (F.inject₁ i) F.zero in
  begin
  vmap F.suc (insert (vmap F.suc (x ∷ v)) (F.inject₁ (F.suc i)) F.zero) ∘̬′ swap01vec
    ≡⟨ refl ⟩
  (tabulate (F.suc ○ F.suc) !! x) ∷ ((vmap F.suc v′) ∘̬′ swap01vec)
    ≡⟨ cong (λ q → q ∷ ((vmap F.suc v′) ∘̬′ swap01vec)) (lookupTab x) ⟩
  F.suc (F.suc x) ∷ ((vmap F.suc v′) ∘̬′ swap01vec)
    ≡⟨ cong (_∷_ (F.suc (F.suc x))) (newlemma6 i v) ⟩
  F.suc (F.suc x) ∷ insert (vmap F.suc (vmap F.suc v)) (F.inject₁ i) F.zero
    ≡⟨ refl ⟩
  insert (vmap F.suc (vmap F.suc (x ∷ v))) (F.inject₁ (F.suc i)) F.zero ∎

---
--- testing

tests01 : Vec (F.Fin five) five
tests01 = permute (swap01 five) (allFin five)

tests02 : (fromℕ five ⇛ fromℕ five)
tests02 = permToComb (swap01 five)

tests03 : Vec ⟦ PLUS ONE (PLUS ONE (PLUS ONE (PLUS ONE (PLUS ONE ZERO)))) ⟧ five
tests03 = tabulate (λ i → evalComb tests02 (finToVal i))

l6test1 : _
l6test1 = (vmap F.suc (insert (tabulate {4} F.suc) (F.suc (F.suc F.zero)) F.zero)) ∘̬ (F.suc F.zero ∷ F.zero ∷ tabulate (F.suc ○ F.suc))

l6test1b : _
l6test1b = permute (swapUpToPerm {5} (F.suc (F.suc (F.suc F.zero)))) (tabulate id)

test1a : Vec _ 5 -- Vec (F.Fin 5) 5
--test1a = (insert (tabulate {4} F.suc) (F.suc F.zero) F.zero)
test1a = (vmap F.suc (insert (tabulate {4} F.suc) (F.suc F.zero) F.zero))
       ∘̬ (F.suc F.zero ∷ F.zero ∷ tabulate (λ x → F.suc (F.suc x)))

test1b : Vec _ 5
test1b = insert (tabulate (F.suc ○ F.suc)) (F.suc F.zero) F.zero

aPerm : Permutation six
aPerm = (F.suc (F.suc (F.suc F.zero))) ∷ (F.suc F.zero) ∷ (F.suc F.zero) ∷ F.zero ∷ F.zero ∷ F.zero ∷ []

test5 : Vec (F.Fin six) six
test5 = permute aPerm (tabulate id)

combToVec : {n : ℕ} → (fromℕ n) ⇛ (fromℕ n) → Vec (F.Fin n) n
combToVec c = tabulate (valToFin ○ (evalComb c) ○ finToVal)

test6a : Vec (F.Fin six) six
test6a = combToVec (swapUpTo (F.suc F.zero))

test6b : Vec (F.Fin six) six
test6b = permute (swapUpToPerm (F.suc F.zero)) (tabulate id)

test7a : Vec (F.Fin six) six
test7a = combToVec (swapUpTo (F.zero))

test7b : Vec (F.Fin six) six
test7b = permute (swapUpToPerm (F.zero)) (tabulate id)

test8a : Vec (F.Fin six) six
test8a = combToVec (swapUpTo (F.suc (F.suc (F.suc (F.zero)))))

test8b : Vec (F.Fin six) six
test8b = permute (swapUpToPerm (F.suc (F.suc (F.suc F.zero)))) (tabulate id)

test9 : Vec (F.Fin six) six
test9 = permute (swapOne (F.suc (F.suc (F.suc F.zero)))) (tabulate id)

test10 : Vec (F.Fin six) six
test10 = permute (swapmPerm (F.suc (F.suc (F.suc F.zero)))) (tabulate id)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Container.List.Isomorphism where

open import Prelude
open import Container
open import Container.List
open import Data.Fin
open import Data.List using (tabulate; length ; _!_) renaming (_∷_ to _L∷_; [] to L[]; List to 𝕃)
open import Data.List.Properties

ℒ→𝕃 : List A → 𝕃 A
ℒ→𝕃 = uncurry tabulate

𝕃→ℒ : 𝕃 A → List A
𝕃→ℒ xs .fst = length xs
𝕃→ℒ xs .snd i = xs ! i

ℒ→𝕃→ℒ : ∀ n (xs : Fin n → A) → 𝕃→ℒ (ℒ→𝕃 (n , xs)) ≡ (n , xs)
ℒ→𝕃→ℒ n xs i .fst = tab-length n xs i
ℒ→𝕃→ℒ n xs i .snd = tab-id n xs i

𝕃→ℒ→𝕃 : ∀ (xs : 𝕃 A) → ℒ→𝕃 (𝕃→ℒ xs) ≡ xs
𝕃→ℒ→𝕃 L[] _ = L[]
𝕃→ℒ→𝕃 (x L∷ xs) i = x L∷ 𝕃→ℒ→𝕃 xs i

𝕃⇔ℒ : 𝕃 A ⇔ List A
𝕃⇔ℒ .fun = 𝕃→ℒ
𝕃⇔ℒ .inv = ℒ→𝕃
𝕃⇔ℒ .rightInv  = uncurry ℒ→𝕃→ℒ
𝕃⇔ℒ .leftInv = 𝕃→ℒ→𝕃

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Andreas, 2018-07-21, issue #3161
-- Insert space before brace if preceeded by `-`.
-- (Symmetric case was already fixed in #269).

data Pol : Set where
  + - : Pol

f : {x : Pol} → Set
f {x} = {!x!}  -- Split on x here

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Relation.Nullary.DecidablePropositions where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)

open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary.Base
open import Cubical.Relation.Nullary.Properties

private
  variable
    ℓ ℓ'  : Level

DecProp : (ℓ : Level) → Type (ℓ-suc ℓ)
DecProp ℓ = Σ[ P ∈ hProp ℓ ] Dec (P .fst)

isSetDecProp : isSet (DecProp ℓ)
isSetDecProp = isOfHLevelΣ 2 isSetHProp (λ P → isProp→isSet (isPropDec (P .snd)))

-- the following is an alternative formulation of decidable propositions
-- it separates the boolean value from more proof-relevant part
-- so it performs better when doing computation

isDecProp : Type ℓ → Type ℓ
isDecProp P = Σ[ t ∈ Bool ] P ≃ Bool→Type t

DecProp' : (ℓ : Level) → Type (ℓ-suc ℓ)
DecProp' ℓ = Σ[ P ∈ Type ℓ ] isDecProp P

-- properties of the alternative formulation

isDecProp→isProp : {P : Type ℓ} → isDecProp P → isProp P
isDecProp→isProp h = isOfHLevelRespectEquiv 1 (invEquiv (h .snd)) isPropBool→Type

isDecProp→Dec : {P : Type ℓ} → isDecProp P → Dec P
isDecProp→Dec h = EquivPresDec (invEquiv (h .snd)) DecBool→Type

isPropIsDecProp : {P : Type ℓ} → isProp (isDecProp P)
isPropIsDecProp p q =
  Σ≡PropEquiv (λ _ → isOfHLevel⁺≃ᵣ 0 isPropBool→Type) .fst
    (Bool→TypeInj _ _ (invEquiv (p .snd) ⋆ q .snd))

isDecPropRespectEquiv : {P : Type ℓ} {Q : Type ℓ'}
  → P ≃ Q → isDecProp Q → isDecProp P
isDecPropRespectEquiv e (t , e') = t , e ⋆ e'

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2011-09-21, reported by Nisse
-- {-# OPTIONS -v tc.lhs.unify:25 #-}
module Issue292-23 where

data ⊤ : Set where
  tt : ⊤

data D : (A : Set) → A → Set₁ where
  d : (A : Set) (x : A) → D A x

data P : (x : ⊤) → D ⊤ x → Set₁ where
  p : (x : ⊤) → P x (d ⊤ x)

Foo : P tt (d ⊤ tt) → Set₁
Foo (p .tt) = Set
-- should work
-- bug was caused by a use of ureduce instead of reduce

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Everything where

import Basic
import Category
import Functor
import Nat
import Yoneda
import Adjoint
import Monad
import TAlgebra

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
-- Andreas, 2016-07-29, issue #1720 reported by Mietek Bak

postulate
  A B : Set
  a0 : A
  b0 : B

record R (a1 : A) (b1 : B) : Set where

  field fa : A

  a : A
  a = {!!}

  field fb : B

  b : B
  b = {!!}

  field f : A

-- Problem:
-- Interaction points are doubled.


text:
module L.Base.Unit.Core where

-- Import the unit type and its only element tt : ⊤
open import Agda.Builtin.Unit renaming (tt to ⋆) public

⊤-elim : ∀{c} (C : ⊤ → Set c) → C ⋆ → (a : ⊤) → C a
⊤-elim = λ C c a → c

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
-- {-# OPTIONS -v tc.cc:12 -v tc.cover.splittree:10 #-}
-- {-# OPTIONS -v tc.cover.strategy:100 -v tc.cover.precomputed:100 #-}
-- {-# OPTIONS -v tc.cover.split.con:20 #-}
module CoverStrategy where

import Common.Level
open import Common.Prelude renaming (Nat to ℕ)

data _∼_ : ℕ → ℕ → Set where
  pr : ∀ {n} → suc n ∼ n
  eq : ∀ {n} →     n ∼ n

max : ∀ {m n} → m ∼ n → ℕ
max (pr {n}) = suc n
max (eq {n}) =     n

data Tree : ℕ → Set where
  node : ∀ {hˡ hʳ} (bal : hˡ ∼ hʳ) → Tree (max bal)

-- 'test' only passes if we split first on 'Tree hˡ' and then on 'hˡ ∼ hʳ'
-- This refutes a split strategy that prefers all-constructor columns
-- over those with catch-alls.
test : ∀ {hˡ hʳ} → Tree hˡ → hˡ ∼ hʳ → Set
test (node pr) pr = ℕ
test (node eq) pr = ℕ
test x         eq = ℕ

{- We cannot split on 'Tree hˡ' if we have already split on 'hˡ ∼ hʳ'
bla : ∀ {hˡ hʳ} → Tree hˡ → hˡ ∼ hʳ → Set
bla nod pr = {!nod!}
bla nod eq = {!!}
-}

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

-- 'Traditionally', meaning in nLab and in
-- "Lectures on n-Categories and Cohomology" by Baez and Shulman
-- https://arxiv.org/abs/math/0608420
-- (-2)-Categories are defined to be just a single value, with trivial Hom

-- But that's hardly a definition of a class of things, it's a definition of
-- a single structure!  What we want is the definition of a class which turns
-- out to be (essentially) unique. Rather like the reals are (essentially) the
-- only ordered complete archimedean field.

-- So we will take a -2-Category to be a full-fledge Category, but where
-- 1. |Obj| is (Categorically) contractible
-- 2. |Hom| is connected (all arrows are equal)
-- Note that we don't need to say anything at all about ≈

module Categories.Minus2-Category where

open import Level
open import Categories.Category
open import Data.Product using (Σ)
import Categories.Morphism as M

private
  variable
    o ℓ e : Level

record -2-Category : Set (suc (o ⊔ ℓ ⊔ e)) where
   field
     cat : Category o ℓ e
   open Category cat public
   open M cat using (_≅_)

   field
     Obj-Contr : Σ Obj (λ x → (y : Obj) → x ≅ y)
     Hom-Conn  : {x y : Obj} {f g : x ⇒ y} → f ≈ g

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:
{-# OPTIONS --cumulativity #-}

open import Agda.Primitive

postulate
  X     : Set
  P     : (A : Set) → A → Set
  id    : ∀ a (A : Set a) → A → A
  works : P (X → X) (id (lsuc lzero) X)
  fails : P _ (id (lsuc lzero) X)


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Interval.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

data Interval : Type₀ where
  zero : Interval
  one  : Interval
  seg  : zero ≡ one

isContrInterval : isContr Interval
isContrInterval = (zero , (λ x → rem x))
  where
  rem : (x : Interval) → zero ≡ x
  rem zero      = refl
  rem one       = seg
  rem (seg i) j = seg (i ∧ j)

funExtInterval : ∀ {ℓ} (A B : Type ℓ) (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g
funExtInterval A B f g p = λ i x → hmtpy x (seg i)
  where
  hmtpy : A → Interval → B
  hmtpy x zero    = f x
  hmtpy x one     = g x
  hmtpy x (seg i) = p x i

intervalElim : (A : Interval → Type₀) (x : A zero) (y : A one)
               (p : PathP (λ i → A (seg i)) x y) → (x : Interval) → A x
intervalElim A x y p zero    = x
intervalElim A x y p one     = y
intervalElim A x y p (seg i) = p i

-- Note that this is not definitional (it is not proved by refl)
intervalEta : ∀ {A : Type₀} (f : Interval → A) → intervalElim _ (f zero) (f one) (λ i → f (seg i)) ≡ f
intervalEta f i zero    = f zero
intervalEta f i one     = f one
intervalEta f i (seg j) = f (seg j)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- Andreas, 2012-05-14, issue reported by Nisse
-- {-# OPTIONS -v term:20 #-}
module Issue636 where

open import Common.Coinduction

data ⊥ : Set where

data D : Set where
  c : ∞ D → D

d : D
d = c (♯ d)

not-d : D → ⊥
not-d (c x) = not-d (♭ x)

bad : ⊥
bad = not-d d

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module xxx where

open import Agda.Builtin.Unit using (⊤)
open import IO                as IO hiding (_>>=_; _>>_)
import      IO.Primitive      as Primitive
open import hcio              as HCIO

main : Primitive.IO ⊤
main = run do
  IO.putStrLn "enter file name:"
  f ← HCIO.getLine

  IO.putStrLn "enter file contents"
  c ← HCIO.getLine

  IO.writeFile f c
  c' ← IO.readFiniteFile f
  IO.putStrLn c'

  std ← IO.readFiniteFile "spacetrack-data-2021-05-31.txt"
  IO.putStrLn std

  IO.putStrLn "Bye"

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

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

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


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

module GPerm where

-- Definition of a general permutation, and some combinators.
-- This is the 'abstract' view, in terms of functions.  Contrast with the
-- concrete view in term of vectors (and restricted to Enumerable sets)

-- In some sense, even better would be to consider 'weak' permutations
-- as exactly _≃_.  Having both side be syntactically equal is weird, as we
-- are exactly trying to liberate ourselves from that!

-- In other words, we won't actually use GPerm anywhere.

open import Level using (_⊔_)
open import Data.Sum using (_⊎_)
open import Data.Product using (_×_)

open import Equiv
open import TypeEquiv

GPerm : Set → Set
GPerm A = A ≃ A

-- composition.  Stick to Set₀.
_⊙_ : {A : Set} → GPerm A → GPerm A → GPerm A
_⊙_ = trans≃

-- parallel composition.
_⊕_ : {A C : Set} → GPerm A → GPerm C → GPerm (A ⊎ C)
_⊕_ = path⊎

-- tensor product
_⊗_ :  {A B : Set} → GPerm A → GPerm B → GPerm (A × B)
_⊗_ = path×