text:
module Section3 where

open import Section1 public

-- 3. The calculus of proof trees
-- ==============================
--
-- We define the set of proof trees of implicational logic in the ordinary style à la Church,
-- except that we use explicit substitutions.

-- 3.1. Definition of types
-- ------------------------
--
-- The types we have are base type and function types.  The set of types `𝒯 : Set` is introduced
-- by:

infixr 7 _⊃_
data 𝒯 : Set where
  •   : 𝒯
  _⊃_ : 𝒯 → 𝒯 → 𝒯

-- Types are denoted by `A`, `B`.  (…)
--
-- We write `•` for the base type and `A ⊃ B` for the function type.

module _ where
  inj₁⊃ : ∀ {A A′ B B′} → A ⊃ B ≡ A′ ⊃ B′ → A ≡ A′
  inj₁⊃ refl = refl

  inj₂⊃ : ∀ {A A′ B B′} → A ⊃ B ≡ A′ ⊃ B′ → B ≡ B′
  inj₂⊃ refl = refl

  _≟𝒯_ : (A A′ : 𝒯) → Dec (A ≡ A′)
  •       ≟𝒯 •         = yes refl
  •       ≟𝒯 (A′ ⊃ B′) = no λ ()
  (A ⊃ B) ≟𝒯 •         = no λ ()
  (A ⊃ B) ≟𝒯 (A′ ⊃ B′) with A ≟𝒯 A′ | B ≟𝒯 B′
  …                   | yes refl | yes refl = yes refl
  …                   | yes refl | no B≢B′  = no (λ p → inj₂⊃ p ↯ B≢B′)
  …                   | no A≢A′  | _        = no (λ p → inj₁⊃ p ↯ A≢A′)

-- 3.2. Definition of contexts
-- ---------------------------
--
-- Suppose a countably infinite set, `Name`, with names together with a decidable equality on it.
-- The set of contexts `𝒞` is mutually defined with a boolean-valued function `fresh` which describes
-- when a name is fresh in a context.  (…)
--
-- Ordinarily, the freshness condition is written as a side-condition, but since we are to
-- formalise the proof trees, this information must be represented, too.
--
-- We write `[]` for the empty context and `[ Γ , x ∷ A ]` for adding an element to a context,
-- hence when we write `[ Γ , x ∷ A ]`
-- it is implicit that we also have a proof that `x` is fresh in `Γ` (when `[ Γ , x ∷ A ]` occurs in the
-- conclusion of a statement, then it is implicit that `T (fresh x Γ)` is an assumption.)  The
-- function `fresh` is defined by induction on the context as:

mutual
  data 𝒞 : Set where
    []      : 𝒞
    [_,_∷_] : (Γ : 𝒞) (x : Name) {{_ : T (fresh x Γ)}} → 𝒯 → 𝒞

  fresh : Name → 𝒞 → Bool
  fresh x []            = true
  fresh x [ Γ , y ∷ A ] = and (x ≠ y) (fresh x Γ)

-- We use `Γ`, `Δ` and `Θ` for contexts.
--
-- The predicate `Γ ∋ x ∷ A` is true when a name with its type occurs in a context.
--
-- The introduction rules are:

data _∋_∷_ : 𝒞 → Name → 𝒯 → Set where
  zero : ∀ {Γ A x} {{_ : T (fresh x Γ)}} →
           [ Γ , x ∷ A ] ∋ x ∷ A
  suc  : ∀ {Γ A B x y} {{_ : T (fresh y Γ)}} →
           Γ ∋ x ∷ A →
           [ Γ , y ∷ B ] ∋ x ∷ A

module _ where
  injsuc : ∀ {Γ A B x y} {{_ : T (fresh y Γ)}} {i i′ : Γ ∋ x ∷ A} →
             suc {B = B} {y = y} i ≡ suc i′ → i ≡ i′
  injsuc refl = refl

  _≟∋_ : ∀ {Γ A x} → (i i′ : Γ ∋ x ∷ A) → Dec (i ≡ i′)
  zero  ≟∋ zero   = yes refl
  zero  ≟∋ suc i′ = no (λ ())
  suc i ≟∋ zero   = no (λ ())
  suc i ≟∋ suc i′ with i ≟∋ i′
  …              | yes refl = yes refl
  …              | no i≢i′  = no (λ p → injsuc p ↯ i≢i′)

module _ where
  _∌_∷_ : 𝒞 → Name → 𝒯 → Set
  Γ ∌ x ∷ A = ¬ (Γ ∋ x ∷ A)

  fresh→∌ : ∀ {x Γ A} {{_ : T (fresh x Γ)}} → Γ ∌ x ∷ A
  fresh→∌ {x} {{φ}}  zero             with x ≟ x
  fresh→∌ {x} {{()}} zero             | yes refl
  fresh→∌ {x} {{φ}}  zero             | no x≢x   = refl ↯ x≢x
  fresh→∌ {x} {{φ}}  (suc {y = y}  i) with x ≟ y
  fresh→∌ {x} {{()}} (suc {y = .x} i) | yes refl
  fresh→∌ {x} {{φ}}  (suc {y = y}  i) | no x≢y   = i ↯ fresh→∌

  freshlem₁ : ∀ {b′} → (x : Name) → ¬ (T (and (x ≠ x) b′))
  freshlem₁ x p with x ≟ x
  …            | yes refl = p
  …            | no x≢x   = refl ↯ x≢x

  freshlem₂ : ∀ {b′} → (x {y} : Name) → T (and (x ≠ y) b′) → T b′
  freshlem₂ x {y} p with x ≟ y
  …              | yes refl = elim⊥ p
  …              | no x≢y   = p

-- We also define the relation that describes when a context contains another.
--
-- We use the notational convention `Γ ⊇ Δ` for `Γ` being greater than `Δ`.
-- The set `_⊇_` has the constructors:

infix 3 _⊇_
data _⊇_ : 𝒞 → 𝒞 → Set where
  done : ∀ {Γ} →
           Γ ⊇ []
  step : ∀ {Γ Δ A x} {{_ : T (fresh x Δ)}} →
           Γ ⊇ Δ → Γ ∋ x ∷ A →
           Γ ⊇ [ Δ , x ∷ A ]

module _ where
  inj₁step : ∀ {Γ Δ A x} {{_ : T (fresh x Δ)}} {c c′ : Γ ⊇ Δ} {i i′ : Γ ∋ x ∷ A} →
               step c i ≡ step c′ i′ → c ≡ c′
  inj₁step refl = refl

  inj₂step : ∀ {Γ Δ A x} {{_ : T (fresh x Δ)}} {c c′ : Γ ⊇ Δ} {i i′ : Γ ∋ x ∷ A} →
               step c i ≡ step c′ i′ → i ≡ i′
  inj₂step refl = refl

  _≟⊇_ : ∀ {Γ Δ} → (c c′ : Γ ⊇ Δ) → Dec (c ≡ c′)
  done     ≟⊇ done       = yes refl
  step c i ≟⊇ step c′ i′ with c ≟⊇ c′ | i ≟∋ i′
  …                     | yes refl | yes refl = yes refl
  …                     | yes refl | no i≢i′  = no (λ p → inj₂step p ↯ i≢i′)
  …                     | no c≢c′  | _        = no (λ p → inj₁step p ↯ c≢c′)

-- The following lemmas are easy to prove:

-- Lemma 1.
ext⊇ : ∀ {Δ Γ} → (∀ {A x} → Δ ∋ x ∷ A → Γ ∋ x ∷ A) → Γ ⊇ Δ
ext⊇ {[]}            f = done
ext⊇ {[ Δ , x ∷ A ]} f = step (ext⊇ (λ i → f (suc i))) (f zero)

-- Lemma 2.
module _ where
  ↑⟨_⟩∋ : ∀ {Γ Δ A x} → Δ ⊇ Γ → Γ ∋ x ∷ A → Δ ∋ x ∷ A
  ↑⟨ done ⟩∋     ()
  ↑⟨ step c i ⟩∋ zero    = i
  ↑⟨ step c i ⟩∋ (suc j) = ↑⟨ c ⟩∋ j

  instance
    raise∋ : ∀ {A x} → Raiseable (_∋ x ∷ A)
    raise∋ = record { ↑⟨_⟩ = ↑⟨_⟩∋ }

-- Lemma 3.
refl⊇ : ∀ {Γ} → Γ ⊇ Γ
refl⊇ = ext⊇ id

-- Lemma 4.
module _ where
  _○_ : ∀ {Γ Δ Θ} → Γ ⊇ Δ → Θ ⊇ Γ → Θ ⊇ Δ
  c ○ c′ = ext⊇ (λ i → ↑⟨ c′ ⟩ (↑⟨ c ⟩ i))

  trans⊇ : ∀ {Γ Δ Θ} → Θ ⊇ Γ → Γ ⊇ Δ → Θ ⊇ Δ
  trans⊇ = flip _○_

-- Lemma 5.
weak⊇ : ∀ {Γ A x} {{_ : T (fresh x Γ)}} → [ Γ , x ∷ A ] ⊇ Γ
weak⊇ = ext⊇ suc

-- Lemma 6.
uniq∋ : ∀ {Γ A x} → (i i′ : Γ ∋ x ∷ A) → i ≡ i′
uniq∋ zero    zero     = refl
uniq∋ zero    (suc i′) = i′ ↯ fresh→∌
uniq∋ (suc i) zero     = i ↯ fresh→∌
uniq∋ (suc i) (suc i′) = cong suc (uniq∋ i i′)

-- Lemma 7.
uniq⊇ : ∀ {Γ Δ} → (c c′ : Γ ⊇ Δ) → c ≡ c′
uniq⊇ done       done         = refl
uniq⊇ (step c i) (step c′ i′) = cong² step (uniq⊇ c c′) (uniq∋ i i′)

-- `ext⊇`, `↑⟨_⟩∋` and `uniq⊇` are proven by induction on `Δ` and `uniq∋` is proven by
-- induction on `Γ`.  `refl⊇` and `weak⊇` are direct consequences of `ext⊇` and for `trans⊇`
-- we also use `↑⟨_⟩∋`.  (…)
--
-- The last two lemmas may seem slightly strange: they are used for guaranteeing independence
-- of the proofs of `_∋_∷_` and `_⊇_`.  For example, `uniq∋` says that if it can be shown that
-- `x ∷ A` occurs in a context `Γ`, then there is a unique proof of this fact.  The need to prove
-- independence of proofs might point to a problem in using type theory for formalising proofs.  On
-- the other hand, as we shall see, proof objects can also be useful: the present formalisation
-- heavily uses the possibilities to perform case analysis on proof objects, which reduces the
-- number of cases to consider.

module _ where
  id₁○ : ∀ {Γ Δ} → (c : Γ ⊇ Γ) (c′ : Δ ⊇ Γ) → c ○ c′ ≡ c′
  id₁○ c c′ = uniq⊇ (c ○ c′) c′

  id₂○ : ∀ {Γ Δ} → (c : Δ ⊇ Γ) (c′ : Δ ⊇ Δ) → c ○ c′ ≡ c
  id₂○ c c′ = uniq⊇ (c ○ c′) c

  assoc○ : ∀ {Γ Δ Θ Ω} → (c : Δ ⊇ Γ) (c′ : Θ ⊇ Δ) (c″ : Ω ⊇ Θ) →
             c ○ (c′ ○ c″) ≡ (c ○ c′) ○ c″
  assoc○ c c′ c″ = uniq⊇ (c ○ (c′ ○ c″)) ((c ○ c′) ○ c″)

  comp○ : ∀ {Γ Δ Θ} → (c : Δ ⊇ Γ) (c′ : Θ ⊇ Δ) (c″ : Θ ⊇ Γ) →
            c ○ c′ ≡ c″
  comp○ c c′ c″ = uniq⊇ (c ○ c′) c″

-- 3.3. Definition of proof trees
-- ------------------------------
--
-- Proof trees and substitutions are mutually inductively defined.  (…)
--
-- We use the notational convention `Γ ⊢ A` and `Δ ⋙ Γ` for a proof of `A` in context `Γ` and
-- a substitution of `Γ` by `Δ`, respectively.
--
-- A substitution of type `Δ ⋙ Γ` intuitively is a list that associates to each `x ∷ A` in `Γ` a unique
-- proof tree of type `Δ ⊢ A`.
--
-- The proof trees are defined by the following rules.
--
-- We recall that hidden assumptions in the definition above are implicitly universally defined
-- and that the notation `[ Γ , x ∷ A ]` implies that `x` is fresh in `Γ`.  (…)
--
-- In the definition of variables we can see that a proof of occurrence is part of the proof
-- tree.  The advantage is that we can do case-analysis on this proof to find out where in the
-- context `x ∷ A` occurs.  The disadvantage is that we need to prove that two variables are the
-- same even if they have two possibly different proofs of occurrence of `x ∷ A` (by Lemma 6 we
-- know that the proofs are the same).

mutual
  infix 3 _⊢_
  data _⊢_ : 𝒞 → 𝒯 → Set where
    ν   : ∀ {Γ A} →
            (x : Name) → Γ ∋ x ∷ A →
            Γ ⊢ A
    ƛ   : ∀ {Γ A B} →
            (x : Name) {{_ : T (fresh x Γ)}} → [ Γ , x ∷ A ] ⊢ B →
            Γ ⊢ A ⊃ B
    _∙_ : ∀ {Γ A B} →
            Γ ⊢ A ⊃ B → Γ ⊢ A →
            Γ ⊢ B
    _▶_ : ∀ {Γ Δ A} →
            Γ ⊢ A → Δ ⋙ Γ →
            Δ ⊢ A

  infix 3 _⋙_
  data _⋙_ : 𝒞 → 𝒞 → Set where
    π⟨_⟩    : ∀ {Γ Δ} →
                Δ ⊇ Γ →
                Δ ⋙ Γ
    _●_     : ∀ {Γ Δ Θ} →
                Γ ⋙ Δ → Θ ⋙ Γ →
                Θ ⋙ Δ
    [_,_≔_] : ∀ {Γ Δ A} →
                Δ ⋙ Γ → (x : Name) {{_ : T (fresh x Γ)}} → Δ ⊢ A →
                Δ ⋙ [ Γ , x ∷ A ]

-- Explicit substitutions are built from a projection map, update and composition (see below
-- for a discussion on the projection map).
--
-- We use the following notational conventions:
--
-- -   `ν x`           for referencing the occurrence `x`, where `x : Γ ∋ x ∷ A`
-- -   `M ▶ γ`         for applying the substitution `γ` to the term `M`
-- -   `ƛ x M`         for abstracting the occurrence `x` from the term `M`, where `M : [ Γ , x ∷ A ] ⊢ B`
-- -   `M ∙ N`         for applying the term `M` to the term `N`
-- -   `π⟨ c ⟩`        for projecting the inclusion `c` as a substitution
-- -   `[ γ , x ≔ M ]` for updating the substitution `γ` with the term `M` for the occurrence `x`
-- -   `γ ● δ`         for composing the substitution `δ` with the substitution `γ`
--
-- Proof trees and substitutions are named `M, N` and `γ, δ, θ` respectively.
--
-- The substitution `π⟨_⟩` is not a standard primitive for explicit substitutions.  Often one rather
-- has an identity substitution (in `Γ ⋙ Γ`) [1, 13] or the empty substitution (in `Γ ⋙ []`) [5].
-- Instead we have taken `π⟨_⟩` as primitive.  If `c : Γ ⊇ Γ`, then `π⟨ c ⟩` is the identity substitution and
-- if `c : Γ ⊇ []`, then `π⟨ c ⟩` is the empty substitution.  Abadi et al. [1] use a substitution `↑` that
-- corresponds to a shift on substitutions; the same substitution is here defined as `π⟨ c ⟩` where
-- `c : [ Γ , x ∷ A ] ⊇ Γ`.  In Martin-Löf’s substitution calculus [13, 20] we have as primitives also
-- thinning rules (i.e., if a term is well-typed in a given context, then it is also well-typed in a
-- larger context and likewise for substitutions.)  Here, thinning is achieved using `π⟨_⟩`, since if,
-- for example, `M : Γ ⊢ A` and `c : Δ ⊇ Γ`, then `M ▶ π⟨ c ⟩ : Δ ⊢ A`.
--
-- The first version of our work used combinators for the thinning rules, since we wanted it to
-- be a start for a complete mechanical analysis of Martin-Löf’s substitution calculus [13, 20].
-- The set of conversion rules we obtained using these combinators suggested the use of `π⟨_⟩`,
-- which gives fewer conversion rules.  There might be other advantages in using `π⟨_⟩`: if a proof
-- tree is of the form `M ▶ π⟨_⟩` we know which are the possible free variables of the term `M`,
-- information that might be used in a computation.

module _ where
  ↑⟨_⟩⊢ : ∀ {Γ Δ A} → Δ ⊇ Γ → Γ ⊢ A → Δ ⊢ A
  ↑⟨ c ⟩⊢ M = M ▶ π⟨ c ⟩

  ↑⟨_⟩⋙ : ∀ {Γ Δ Θ} → Δ ⊇ Γ → Γ ⋙ Θ → Δ ⋙ Θ
  ↑⟨ c ⟩⋙ δ = δ ● π⟨ c ⟩

  ↓⟨_⟩⋙ : ∀ {Γ Δ Θ} → Δ ⊇ Γ → Θ ⋙ Δ → Θ ⋙ Γ
  ↓⟨ c ⟩⋙ δ = π⟨ c ⟩ ● δ

  refl⋙ : ∀ {Γ} → Γ ⋙ Γ
  refl⋙ = π⟨ refl⊇ ⟩

  trans⋙ : ∀ {Γ Δ Θ} → Θ ⋙ Γ → Γ ⋙ Δ → Θ ⋙ Δ
  trans⋙ = flip _●_

  weak⋙ : ∀ {Γ A x} {{_ : T (fresh x Γ)}} → [ Γ , x ∷ A ] ⋙ Γ
  weak⋙ = π⟨ weak⊇ ⟩

  instance
    raise⊢ : ∀ {A} → Raiseable (_⊢ A)
    raise⊢ = record { ↑⟨_⟩ = ↑⟨_⟩⊢ }

    raise⋙ : ∀ {Γ} → Raiseable (_⋙ Γ)
    raise⋙ = record { ↑⟨_⟩ = ↑⟨_⟩⋙ }

    lower⋙ : ∀ {Δ} → Lowerable (Δ ⋙_)
    lower⋙ = record { ↓⟨_⟩ = ↓⟨_⟩⋙ }

-- 3.4. Convertibility of proof trees
-- ----------------------------------
--
-- The rules for conversion between proof trees and substitutions are inductively defined.
--
-- We use the notational convention `M ≅ N` and `γ ≅ₛ δ` for convertibility on proof trees and
-- on substitutions respectively.  (…)
--
-- The conversion rules for proof trees are the reflexivity, symmetry, transitivity, congruence
-- rules and the following rules:

mutual
  infix 3 _≅_
  data _≅_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
    refl≅  : ∀ {Γ A} {M : Γ ⊢ A} →
               M ≅ M
    sym≅   : ∀ {Γ A} {M M′ : Γ ⊢ A} →
               M ≅ M′ →
               M′ ≅ M
    trans≅ : ∀ {Γ A} {M M′ M″ : Γ ⊢ A} →
               M ≅ M′ → M′ ≅ M″ →
               M ≅ M″

    congƛ≅ : ∀ {Γ A B x} {{_ : T (fresh x Γ)}} {M M′ : [ Γ , x ∷ A ] ⊢ B} →
               M ≅ M′ →
               ƛ x M ≅ ƛ x M′
    cong∙≅ : ∀ {Γ A B} {M M′ : Γ ⊢ A ⊃ B} {N N′ : Γ ⊢ A} →
               M ≅ M′ → N ≅ N′ →
               M ∙ N ≅ M′ ∙ N′
    cong▶≅ : ∀ {Γ Δ A} {M M′ : Γ ⊢ A} {γ γ′ : Δ ⋙ Γ} →
               M ≅ M′ → γ ≅ₛ γ′ →
               M ▶ γ ≅ M′ ▶ γ′

    conv₁≅ : ∀ {Γ Δ A B x} {{_ : T (fresh x Γ)}} →
               (M : [ Γ , x ∷ A ] ⊢ B) (N : Δ ⊢ A) (γ : Δ ⋙ Γ) →
               (ƛ x M ▶ γ) ∙ N ≅ M ▶ [ γ , x ≔ N ]
    conv₂≅ : ∀ {Γ A B x} {{_ : T (fresh x Γ)}} →
               (c : [ Γ , x ∷ A ] ⊇ Γ) (M : Γ ⊢ A ⊃ B) →
               M ≅ ƛ x ((M ▶ π⟨ c ⟩) ∙ ν x zero)
    conv₃≅ : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}} →
               (M : Δ ⊢ A) (γ : Δ ⋙ Γ) →
               ν x zero ▶ [ γ , x ≔ M ] ≅ M
    conv₄≅ : ∀ {Γ Δ A x} →
               (c : Δ ⊇ Γ) (i : Γ ∋ x ∷ A) (j : Δ ∋ x ∷ A) →
               ν x i ▶ π⟨ c ⟩ ≅ ν x j
    conv₅≅ : ∀ {Γ A} →
               (c : Γ ⊇ Γ) (M : Γ ⊢ A) →
               M ▶ π⟨ c ⟩ ≅ M
    conv₆≅ : ∀ {Γ Δ A B} →
               (M : Γ ⊢ A ⊃ B) (N : Γ ⊢ A) (γ : Δ ⋙ Γ) →
               (M ∙ N) ▶ γ ≅ (M ▶ γ) ∙ (N ▶ γ)
    conv₇≅ : ∀ {Γ Δ Θ A} →
               (M : Γ ⊢ A) (γ : Δ ⋙ Γ) (δ : Θ ⋙ Δ) →
               (M ▶ γ) ▶ δ ≅ M ▶ (γ ● δ)

  infix 3 _≅ₛ_
  data _≅ₛ_ : ∀ {Γ Δ} → Δ ⋙ Γ → Δ ⋙ Γ → Set where
    refl≅ₛ  : ∀ {Γ Δ} {γ : Δ ⋙ Γ} →
                γ ≅ₛ γ
    sym≅ₛ   : ∀ {Γ Δ} {γ γ′ : Δ ⋙ Γ} →
                γ ≅ₛ γ′ →
                γ′ ≅ₛ γ
    trans≅ₛ : ∀ {Γ Δ} {γ γ′ γ″ : Δ ⋙ Γ} →
                γ ≅ₛ γ′ → γ′ ≅ₛ γ″ →
                γ ≅ₛ γ″

    cong●≅ₛ : ∀ {Γ Δ Θ} {γ γ′ : Δ ⋙ Γ} {δ δ′ : Θ ⋙ Δ} →
                γ ≅ₛ γ′ → δ ≅ₛ δ′ →
                γ ● δ ≅ₛ γ′ ● δ′
    cong≔≅ₛ : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}} {γ γ′ : Δ ⋙ Γ} {M M′ : Δ ⊢ A} →
                γ ≅ₛ γ′ → M ≅ M′ →
                [ γ , x ≔ M ] ≅ₛ [ γ′ , x ≔ M′ ]

    conv₁≅ₛ : ∀ {Γ Δ Θ Ω} →
                (γ : Δ ⋙ Γ) (δ : Θ ⋙ Δ) (θ : Ω ⋙ Θ) →
                (γ ● δ) ● θ ≅ₛ γ ● (δ ● θ)
    conv₂≅ₛ : ∀ {Γ Δ Θ A x} {{_ : T (fresh x Γ)}} →
                (M : Δ ⊢ A) (γ : Δ ⋙ Γ) (δ : Θ ⋙ Δ) →
                [ γ , x ≔ M ] ● δ ≅ₛ [ γ ● δ , x ≔ M ▶ δ ]
    conv₃≅ₛ : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}} →
                (c : [ Γ , x ∷ A ] ⊇ Γ) (M : Δ ⊢ A) (γ : Δ ⋙ Γ) →
                π⟨ c ⟩ ● [ γ , x ≔ M ] ≅ₛ γ
    conv₄≅ₛ : ∀ {Γ Δ Θ} →
                (c : Θ ⊇ Γ) (c′ : Δ ⊇ Γ) (c″ : Θ ⊇ Δ) →
                π⟨ c′ ⟩ ● π⟨ c″ ⟩ ≅ₛ π⟨ c ⟩
    conv₅≅ₛ : ∀ {Γ Δ} →
                (c : Δ ⊇ Δ) (γ : Δ ⋙ Γ) →
                γ ● π⟨ c ⟩ ≅ₛ γ
    conv₆≅ₛ : ∀ {Γ} →
                (c : Γ ⊇ []) (γ : Γ ⋙ []) →
                γ ≅ₛ π⟨ c ⟩
    conv₇≅ₛ : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}} →
                (c : [ Γ , x ∷ A ] ⊇ Γ) (γ : Δ ⋙ [ Γ , x ∷ A ]) (i : [ Γ , x ∷ A ] ∋ x ∷ A) →
                γ ≅ₛ [ π⟨ c ⟩ ● γ , x ≔ ν x i ▶ γ ]

-- The first two `conv≅` rules correspond to the ordinary β- and η-rules, the next three define the effect
-- of substitutions and the last two rules can be seen as the correspondence of the η-rule for
-- substitutions.  The remaining `conv≅ₛ` rules define how the substitutions distribute.

module _ where
  ≡→≅ : ∀ {Γ A} {M M′ : Γ ⊢ A} → M ≡ M′ → M ≅ M′
  ≡→≅ refl = refl≅

  module ≅-Reasoning where
    infix 1 begin_
    begin_ : ∀ {Γ A} {M M′ : Γ ⊢ A} → M ≅ M′ → M ≅ M′
    begin p = p

    infixr 2 _≅⟨⟩_
    _≅⟨⟩_ : ∀ {Γ A} (M {M′} : Γ ⊢ A) → M ≅ M′ → M ≅ M′
    M ≅⟨⟩ p = p

    infixr 2 _≅⟨_⟩_
    _≅⟨_⟩_ : ∀ {Γ A} (M {M′ M″} : Γ ⊢ A) → M ≅ M′ → M′ ≅ M″ → M ≅ M″
    M ≅⟨ p ⟩ p′ = trans≅ p p′

    infixr 2 _≡⟨⟩_
    _≡⟨⟩_ : ∀ {Γ A} (M {M′} : Γ ⊢ A) → M ≅ M′ → M ≅ M′
    M ≡⟨⟩ p = p

    infixr 2 _≡⟨_⟩_
    _≡⟨_⟩_ : ∀ {Γ A} (M {M′ M″} : Γ ⊢ A) → M ≡ M′ → M′ ≅ M″ → M ≅ M″
    M ≡⟨ p ⟩ p′ = trans≅ (≡→≅ p) p′

    infix 3 _∎
    _∎ : ∀ {Γ A} (M : Γ ⊢ A) → M ≅ M
    M ∎ = refl≅

  ≡→≅ₛ : ∀ {Γ Δ} {γ γ′ : Δ ⋙ Γ} → γ ≡ γ′ → γ ≅ₛ γ′
  ≡→≅ₛ refl = refl≅ₛ

  module ≅ₛ-Reasoning where
    infix 1 begin_
    begin_ : ∀ {Γ Δ} {γ γ′ : Δ ⋙ Γ} → γ ≅ₛ γ′ → γ ≅ₛ γ′
    begin p = p

    infixr 2 _≅ₛ⟨⟩_
    _≅ₛ⟨⟩_ : ∀ {Γ Δ} (γ {γ′} : Δ ⋙ Γ) → γ ≅ₛ γ′ → γ ≅ₛ γ′
    γ ≅ₛ⟨⟩ p = p

    infixr 2 _≅ₛ⟨_⟩_
    _≅ₛ⟨_⟩_ : ∀ {Γ Δ} (γ {γ′ γ″} : Δ ⋙ Γ) → γ ≅ₛ γ′ → γ′ ≅ₛ γ″ → γ ≅ₛ γ″
    γ ≅ₛ⟨ p ⟩ p′ = trans≅ₛ p p′

    infixr 2 _≡⟨⟩_
    _≡⟨⟩_ : ∀ {Γ Δ} (γ {γ′} : Δ ⋙ Γ) → γ ≅ₛ γ′ → γ ≅ₛ γ′
    γ ≡⟨⟩ p = p

    infixr 2 _≡⟨_⟩_
    _≡⟨_⟩_ : ∀ {Γ Δ} (γ {γ′ γ″} : Δ ⋙ Γ) → γ ≡ γ′ → γ′ ≅ₛ γ″ → γ ≅ₛ γ″
    γ ≡⟨ p ⟩ p′ = trans≅ₛ (≡→≅ₛ p) p′

    infix 3 _∎
    _∎ : ∀ {Γ Δ} (γ : Δ ⋙ Γ) → γ ≅ₛ γ
    γ ∎ = refl≅ₛ

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
-- Andreas, 2015-07-07 Let _ pattern be instantiable by an inaccessible pattern

module _ where

open import Common.Equality

-- These used to work and should still work:

transV1 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
transV1 _ ._ ._ refl refl = refl

transV2 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
transV2 ._ _ ._ refl refl = refl

transV3 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
transV3 ._ ._ _ refl refl = refl

transH : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
transH refl refl = refl

transH1 : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
transH1 {a = _}{b = ._}{c = ._} refl refl = refl

transH1' : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
transH1' {a = _} refl refl = refl

-- NEW: the following should also work:

transVNew : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
transVNew _ _ _ refl refl = refl

transHNew : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
transHNew {a = _}{b = _}{c = _} refl refl = refl

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module PatternShadowsConstructor2 where

module A where

  data A (X : Set) : Set where
    c : A X → A X
    x : A X

open A using (A; c)

f : ∀ {X} → A X → A X → A X
f (c y) x = x
f A.x   _ = A.x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- All library modules, along with short descriptions
------------------------------------------------------------------------

-- Note that core modules are not included.

module Everything where

-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
import Algebra

-- Properties of functions, such as associativity and commutativity
import Algebra.FunctionProperties

-- Morphisms between algebraic structures
import Algebra.Morphism

-- Some defined operations (multiplication by natural number and
-- exponentiation)
import Algebra.Operations

-- Some derivable properties
import Algebra.Props.AbelianGroup

-- Some derivable properties
import Algebra.Props.BooleanAlgebra

-- Some derivable properties
import Algebra.Props.DistributiveLattice

-- Some derivable properties
import Algebra.Props.Group

-- Some derivable properties
import Algebra.Props.Lattice

-- Some derivable properties
import Algebra.Props.Ring

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

-- Commutative semirings with some additional structure ("almost"
-- commutative rings), used by the ring solver
import Algebra.RingSolver.AlmostCommutativeRing

-- Some boring lemmas used by the ring solver
import Algebra.RingSolver.Lemmas

-- Instantiates the ring solver with two copies of the same ring
import Algebra.RingSolver.Simple

-- Some algebraic structures (not packed up with sets, operations,
-- etc.)
import Algebra.Structures

-- Applicative functors
import Category.Applicative

-- Indexed applicative functors
import Category.Applicative.Indexed

-- Functors
import Category.Functor

-- Monads
import Category.Monad

-- A delimited continuation monad
import Category.Monad.Continuation

-- The identity monad
import Category.Monad.Identity

-- Indexed monads
import Category.Monad.Indexed

-- The partiality monad
import Category.Monad.Partiality

-- The state monad
import Category.Monad.State

-- Types used to make recursive arguments coinductive
import Coinduction

-- AVL trees
import Data.AVL

-- Finite maps with indexed keys and values, based on AVL trees
import Data.AVL.IndexedMap

-- Finite sets, based on AVL trees
import Data.AVL.Sets

-- A binary representation of natural numbers
import Data.Bin

-- Booleans
import Data.Bool

-- A bunch of properties
import Data.Bool.Properties

-- Showing booleans
import Data.Bool.Show

-- Bounded vectors
import Data.BoundedVec

-- Bounded vectors (inefficient, concrete implementation)
import Data.BoundedVec.Inefficient

-- Characters
import Data.Char

-- "Finite" sets indexed on coinductive "natural" numbers
import Data.Cofin

-- Coinductive lists
import Data.Colist

-- Coinductive "natural" numbers
import Data.Conat

-- Coinductive vectors
import Data.Covec

-- Lists with fast append
import Data.DifferenceList

-- Natural numbers with fast addition (for use together with
-- DifferenceVec)
import Data.DifferenceNat

-- Vectors with fast append
import Data.DifferenceVec

-- Digits and digit expansions
import Data.Digit

-- Empty type
import Data.Empty

-- Empty type (in Set₁)
import Data.Empty1

-- Finite sets
import Data.Fin

-- Decision procedures for finite sets and subsets of finite sets
import Data.Fin.Dec

-- Properties related to Fin, and operations making use of these
-- properties (or other properties not available in Data.Fin)
import Data.Fin.Props

-- Subsets of finite sets
import Data.Fin.Subset

-- Some properties about subsets
import Data.Fin.Subset.Props

-- Substitutions
import Data.Fin.Substitution

-- An example of how Data.Fin.Substitution can be used: a definition
-- of substitution for the untyped λ-calculus, along with some lemmas
import Data.Fin.Substitution.Example

-- Substitution lemmas
import Data.Fin.Substitution.Lemmas

-- Application of substitutions to lists, along with various lemmas
import Data.Fin.Substitution.List

-- Simple combinators working solely on and with functions
import Data.Function

-- Directed acyclic multigraphs
import Data.Graph.Acyclic

-- Integers
import Data.Integer

-- Divisibility and coprimality
import Data.Integer.Divisibility

-- Some properties about integers
import Data.Integer.Properties

-- Lists
import Data.List

-- Lists where all elements satisfy a given property
import Data.List.All

-- Properties relating All to various list functions
import Data.List.All.Properties

-- Lists where at least one element satisfies a given property
import Data.List.Any

-- Properties relating Any to various list functions
import Data.List.Any.Properties

-- A data structure which keeps track of an upper bound on the number
-- of elements /not/ in a given list
import Data.List.Countdown

-- List equality
import Data.List.Equality

-- Non-empty lists
import Data.List.NonEmpty

-- Properties of non-empty lists
import Data.List.NonEmpty.Properties

-- List-related properties
import Data.List.Properties

-- Lists parameterised on things in Set₁
import Data.List1

-- Finite maps, i.e. lookup tables (currently only some type
-- signatures)
import Data.Map

-- The Maybe type
import Data.Maybe

-- Natural numbers
import Data.Nat

-- Coprimality
import Data.Nat.Coprimality

-- Integer division
import Data.Nat.DivMod

-- Divisibility
import Data.Nat.Divisibility

-- Greatest common divisor
import Data.Nat.GCD

-- Boring lemmas used in Data.Nat.GCD and Data.Nat.Coprimality
import Data.Nat.GCD.Lemmas

-- Least common multiple
import Data.Nat.LCM

-- A bunch of properties about natural number operations
import Data.Nat.Properties

-- Showing natural numbers
import Data.Nat.Show

-- Products
import Data.Product

-- Products implemented using records
import Data.Product.Record

-- Products (variants for Set₁)
import Data.Product1

-- Rational numbers
import Data.Rational

-- Finite sets (currently only some type signatures)
import Data.Sets

-- Signs
import Data.Sign

-- Some properties about signs
import Data.Sign.Properties

-- The reflexive transitive closures of McBride, Norell and Jansson
import Data.Star

-- Bounded vectors (inefficient implementation)
import Data.Star.BoundedVec

-- Decorated star-lists
import Data.Star.Decoration

-- Environments (heterogeneous collections)
import Data.Star.Environment

-- Finite sets defined in terms of Data.Star
import Data.Star.Fin

-- Lists defined in terms of Data.Star
import Data.Star.List

-- Natural numbers defined in terms of Data.Star
import Data.Star.Nat

-- Pointers into star-lists
import Data.Star.Pointer

-- Some properties related to Data.Star
import Data.Star.Properties

-- Vectors defined in terms of Data.Star
import Data.Star.Vec

-- Streams
import Data.Stream

-- Strings
import Data.String

-- Sums (disjoint unions)
import Data.Sum

-- The unit type
import Data.Unit

-- The unit type (in Set₁)
import Data.Unit1

-- Vectors
import Data.Vec

-- Semi-heterogeneous vector equality
import Data.Vec.Equality

-- Code for converting Vec n A → B to and from n-ary functions
import Data.Vec.N-ary

-- Code for converting Vec₁ n A → B to and from n-ary functions
import Data.Vec.N-ary1

-- Some Vec-related properties
import Data.Vec.Properties

-- Vectors parameterised on types in Set₁
import Data.Vec1

-- Types used (only) when calling out to Haskell via the FFI
import Foreign.Haskell

-- IO
import IO

-- Primitive IO: simple bindings to Haskell types and functions
import IO.Primitive

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

-- Lexicographic induction
import Induction.Lexicographic

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

-- Well-founded induction
import Induction.WellFounded

-- A variant of Induction for Set₁
import Induction1

-- One form of induction for natural numbers
import Induction1.Nat

-- Well-founded induction
import Induction1.WellFounded

-- Properties of homogeneous binary relations
import Relation.Binary

-- Some properties imply others
import Relation.Binary.Consequences

-- Convenient syntax for equational reasoning
import Relation.Binary.EqReasoning

-- Many properties which hold for _∼_ also hold for flip₁ _∼_
import Relation.Binary.Flip

-- Function setoids and related constructions
import Relation.Binary.FunctionSetoid

-- Heterogeneous equality
import Relation.Binary.HeterogeneousEquality

-- Conversion of ≤ to <, along with a number of properties
import Relation.Binary.NonStrictToStrict

-- Many properties which hold for _∼_ also hold for _∼_ on₁ f
import Relation.Binary.On

-- Order morphisms
import Relation.Binary.OrderMorphism

-- Convenient syntax for "equational reasoning" using a partial order
import Relation.Binary.PartialOrderReasoning

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

-- Lexicographic products of binary relations
import Relation.Binary.Product.NonStrictLex

-- Pointwise products of binary relations
import Relation.Binary.Product.Pointwise

-- Lexicographic products of binary relations
import Relation.Binary.Product.StrictLex

-- Propositional (intensional) equality
import Relation.Binary.PropositionalEquality

-- Propositional equality
import Relation.Binary.PropositionalEquality1

-- Properties satisfied by decidable total orders
import Relation.Binary.Props.DecTotalOrder

-- Properties satisfied by posets
import Relation.Binary.Props.Poset

-- Properties satisfied by strict partial orders
import Relation.Binary.Props.StrictPartialOrder

-- Properties satisfied by strict partial orders
import Relation.Binary.Props.StrictTotalOrder

-- Properties satisfied by total orders
import Relation.Binary.Props.TotalOrder

-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
import Relation.Binary.Reflection

-- Some simple binary relations
import Relation.Binary.Simple

-- Convenient syntax for "equational reasoning" using a strict partial
-- order
import Relation.Binary.StrictPartialOrderReasoning

-- Conversion of < to ≤, along with a number of properties
import Relation.Binary.StrictToNonStrict

-- Sums of binary relations
import Relation.Binary.Sum

-- Operations on nullary relations (like negation and decidability)
import Relation.Nullary

-- Operations on and properties of decidable relations
import Relation.Nullary.Decidable

-- Properties related to negation
import Relation.Nullary.Negation

-- Products of nullary relations
import Relation.Nullary.Product

-- Sums of nullary relations
import Relation.Nullary.Sum

-- A universe of proposition functors, along with some properties
import Relation.Nullary.Universe

-- Unary relations
import Relation.Unary

-- Unary relations (variant for Set₁)
import Relation.Unary1

-- Sizes for Agda's sized types
import Size

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --sized-types #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Size

mutual

  data D (i : Size) : Set where
    c : D′ i → D i

  record D′ (i : Size) : Set where
    coinductive
    field
      force : (j : Size< i) → D j

data R (i : Size) : D ∞ → D ∞ → Set where
  c₁ : ∀ x y → R i (c x) (c y)
  c₂ : ∀ x y → R i (c x) y

postulate
  F : (x : D ∞) (x′ : D′ ∞) → x ≡ c x′ → Set₁

G : Size → Set₁
G i = Set
  where
  G′ :
    (x′ y′ : D ∞) (x y : D′ ∞) →
    R i (c x) y′ →
    R i x′ (c y) →
    x .D′.force _ {- ∞ -} ≡ x′ →
    Set₁
  G′ _ _ _ _ (c₁ x _) (c₂ u _) eq   = F _ {- x .D′.force ∞ -} u eq
  G′ _ _ _ _ (c₂ _ _) _        refl = Set
  G′ _ _ _ _ _        _        _    = Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

-- Andreas, 2014-05-17 reported by Fabien Renaud

open import Common.Equality

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

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

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

foldr : ∀{a b}{A : Set a}{B : Set b} → (A → B → B) → B → List A → B
foldr c n [] = n
foldr c n (x ∷ xs) = c x (foldr c n xs)

length-cons : ∀{b} {B : Set b} (L : List B) x → length (x ∷ L) ≡ suc (length L)
length-cons []      _ = refl
length-cons (x ∷ L) _ = refl

suc-foldr-eq : ∀{b} {c} {B : Set b} {C : Set c} (LL : List B) (LA : List C)

  → suc (foldr (λ _ → suc) 0 LL) ≡
    suc (foldr (λ _ → suc) 0 LA)

  → length LL ≡
    length LA

suc-foldr-eq [] [] Eq = refl
suc-foldr-eq [] (x ∷ LA) ()
suc-foldr-eq (x ∷ LL) [] ()
suc-foldr-eq (x ∷ LL) (y ∷ LA) Eq rewrite length-cons LL x = {!!}

-- WAS:
-- Failed to infer the value of dotted pattern
-- when checking that the pattern ._ has type Nat

-- NOW: unsolved meta


text:
module _ (A : Set) where

data A where


text:
------------------------------------------------------------------------
-- The classical definition of (strong) bisimilarity
------------------------------------------------------------------------

-- This module is largely based on "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi.

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

open import Labelled-transition-system

module Bisimilarity.Classical {ℓ} (lts : LTS ℓ) where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

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

open LTS lts

open import Bisimilarity.Step lts _[_]⟶_ _[_]⟶_ as S hiding (⟨_,_⟩)
open import Indexed-container
  hiding (⟨_⟩; Bisimilarity; larger⇔smallest)
open import Relation

------------------------------------------------------------------------
-- Progressions, bisimulations and bisimilarity

-- Progressions.

Progression : ∀ {r s} → Rel₂ r Proc → Rel₂ s Proc → Type (ℓ ⊔ r ⊔ s)
Progression R S = R ⊆ Step S

module Progression
        {r s} {R : Rel₂ r Proc} {S : Rel₂ s Proc}
        (P : Progression R S)
        where

  -- Some "projections".

  left-to-right :
    ∀ {p p′ q μ} →
    R (p , q) → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]⟶ q′ × S (p′ , q′)
  left-to-right pRq = Step.left-to-right (P pRq)

  right-to-left :
    ∀ {p q q′ μ} →
    R (p , q) → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]⟶ p′ × S (p′ , q′)
  right-to-left pRq = Step.right-to-left (P pRq)

open Progression public

-- A "constructor" for Progression.

⟪_,_⟫ :
  ∀ {r s} {R : Rel₂ r Proc} {S : Rel₂ s Proc} →
  (∀ {p p′ q μ} →
   R (p , q) → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]⟶ q′ × S (p′ , q′)) →
  (∀ {p q q′ μ} →
   R (p , q) → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]⟶ p′ × S (p′ , q′)) →
  Progression R S
⟪ lr , rl ⟫ = λ pRq → S.⟨ lr pRq , rl pRq ⟩

-- Bisimulations.

Bisimulation : ∀ {r} → Rel₂ r Proc → Type (ℓ ⊔ r)
Bisimulation R = Progression R R

-- Bisimilarity with a level argument.

Bisimilarity′ : ∀ ℓ′ → Rel₂ (lsuc (ℓ ⊔ ℓ′)) Proc
Bisimilarity′ ℓ′ = gfp ℓ′ StepC

-- Bisimilarity′ ℓ′ is pointwise logically equivalent to
-- Bisimilarity′ lzero.
--
-- For this reason the code below is mostly restricted to
-- Bisimilarity′ lzero.

larger⇔smallest :
  ∀ ℓ′ {p} → Bisimilarity′ ℓ′ p ⇔ Bisimilarity′ lzero p
larger⇔smallest ℓ′ = Indexed-container.larger⇔smallest ℓ′

-- Bisimilarity.

Bisimilarity : Rel₂ (lsuc ℓ) Proc
Bisimilarity = Bisimilarity′ lzero

infix 4 _∼_

_∼_ : Proc → Proc → Type (lsuc ℓ)
p ∼ q = ∃ λ R → R ⊆ ⟦ StepC ⟧ R × R (p , q)

private

  -- The definition of _∼_ could also have been given more indirectly.

  indirect-∼ : _∼_ ≡ curry Bisimilarity
  indirect-∼ = refl

-- An unfolding lemma for Bisimilarity′.

Bisimilarity′↔ :
  ∀ {k} ℓ′ {pq} →
  Extensionality? k (ℓ ⊔ ℓ′) (ℓ ⊔ ℓ′) →

  Bisimilarity′ ℓ′ pq
    ↝[ k ]
  ∃ λ (R : Rel₂ (ℓ ⊔ ℓ′) Proc) → Bisimulation R × R pq

Bisimilarity′↔ {k} ℓ′ {pq} ext =
  Bisimilarity′ ℓ′ pq                                      ↔⟨⟩
  gfp ℓ′ StepC pq                                          ↔⟨⟩
  (∃ λ (R : Rel₂ (ℓ ⊔ ℓ′) Proc) → R ⊆ ⟦ StepC ⟧ R × R pq)  ↝⟨ (∃-cong λ _ → ×-cong₁ λ _ → ⊆-congʳ ext $
                                                               inverse-ext? Step↔StepC (lower-extensionality? k ℓ′ lzero ext)) ⟩□
  (∃ λ (R : Rel₂ (ℓ ⊔ ℓ′) Proc) → Bisimulation R × R pq)   □

-- An unfolding lemma for Bisimilarity.

Bisimilarity↔ :
  ∀ {k pq} →
  Extensionality? k ℓ ℓ →

  Bisimilarity pq
    ↝[ k ]
  ∃ λ (R : Rel₂ ℓ Proc) → Bisimulation R × R pq

Bisimilarity↔ = Bisimilarity′↔ lzero

-- A "constructor".

⟨_,_,_⟩ :
  ∀ {p q} →
  (R : Rel₂ ℓ Proc) → Bisimulation R → R (p , q) → p ∼ q
⟨ R , bisim , pRq ⟩ = _⇔_.from (Bisimilarity↔ _) (R , bisim , pRq)

------------------------------------------------------------------------
-- Bisimilarity is an equivalence relation

-- Reflexivity, proved generally for Bisimilarity′.

reflexive-∼′ : ∀ ℓ {p} → Bisimilarity′ ℓ (p , p)
reflexive-∼′ ℓ = _⇔_.from (Bisimilarity′↔ ℓ _)
  ( ↑ ℓ ∘ uncurry _≡_
  ,  ⟪ (λ p≡q p⟶p′ →
          _ , subst (_[ _ ]⟶ _)       (lower p≡q) p⟶p′ , lift refl)
     , (λ p≡q q⟶q′ →
          _ , subst (_[ _ ]⟶ _) (sym $ lower p≡q) q⟶q′ , lift refl)
     ⟫
  , lift refl
  )

-- Reflexivity.

reflexive-∼ : ∀ {p} → p ∼ p
reflexive-∼ = reflexive-∼′ lzero

-- Symmetry.

symmetric-∼ : ∀ {p q} → p ∼ q → q ∼ p
symmetric-∼ p∼q with _⇔_.to (Bisimilarity↔ _) p∼q
... | R , R-is-a-bisimulation , pRq =
  ⟨ R ⁻¹
  , ⟪ right-to-left R-is-a-bisimulation
    , left-to-right R-is-a-bisimulation
    ⟫
  , pRq
  ⟩

-- Transitivity.

transitive-∼ : ∀ {p q r} → p ∼ q → q ∼ r → p ∼ r
transitive-∼ p∼q q∼r with _⇔_.to (Bisimilarity↔ _) p∼q
                        | _⇔_.to (Bisimilarity↔ _) q∼r
... | R₁ , R-is₁ , pR₁q | R₂ , R-is₂ , qR₂r =
  ⟨ R₁ ⊙ R₂
  , ⟪_,_⟫ {R = _ ⊙ _}
      (λ { (q , pR₁q , qR₂r) p⟶p′ →
           let q′ , q⟶q′ , p′R₁q′ = left-to-right R-is₁ pR₁q p⟶p′
               r′ , r⟶r′ , q′R₂r′ = left-to-right R-is₂ qR₂r q⟶q′
           in r′ , r⟶r′ , (q′ , p′R₁q′ , q′R₂r′) })
      (λ { (q , pR₁q , qR₂r) r⟶r′ →
         let q′ , q⟶q′ , q′R₂r′ = right-to-left R-is₂ qR₂r r⟶r′
             p′ , p⟶p′ , p′R₁q′ = right-to-left R-is₁ pR₁q q⟶q′
         in p′ , p⟶p′ , (q′ , p′R₁q′ , q′R₂r′) })
  , (_ , pR₁q , qR₂r)
  ⟩

-- A function that can be used to aid the instance resolution
-- mechanism.

infix -2 ∼:_

∼:_ : ∀ {p q} → p ∼ q → p ∼ q
∼:_ = id

------------------------------------------------------------------------
-- Lemmas relating bisimulations and bisimilarity

-- Bisimilarity is a bisimulation.

bisimilarity-is-a-bisimulation : Bisimulation Bisimilarity
bisimilarity-is-a-bisimulation =
  Bisimilarity            ⊆⟨ gfp-out ℓ ⟩
  ⟦ StepC ⟧ Bisimilarity  ⊆⟨ _⇔_.from (Step↔StepC _) ⟩∎
  Step Bisimilarity       ∎

-- Bisimilarity is larger than every bisimulation.

bisimulation⊆∼ :
  ∀ {r} {R : Rel₂ r Proc} →
  Bisimulation R → R ⊆ Bisimilarity
bisimulation⊆∼ {r} {R} R-is-a-bisimulation =
  R                ⊆⟨ gfp-unfold lzero (

      R                 ⊆⟨ R-is-a-bisimulation ⟩
      Step R            ⊆⟨ Step↔StepC _ ⟩∎
      ⟦ StepC ⟧ R       ∎) ⟩

  Bisimilarity′ r  ⊆⟨ _⇔_.to (larger⇔smallest r) ⟩∎

  Bisimilarity     ∎

------------------------------------------------------------------------
-- Bisimulations up to bisimilarity

-- Bisimulations up to bisimilarity.

Bisimulation-up-to-bisimilarity :
  ∀ {r} → Rel₂ r Proc → Type (lsuc ℓ ⊔ r)
Bisimulation-up-to-bisimilarity R =
  Progression R (Bisimilarity ⊙ R ⊙ Bisimilarity)

-- If R is a bisimulation up to bisimilarity, then ∼R∼ is a
-- bisimulation.

bisimulation-up-to-∼⇒bisimulation :
  ∀ {r} {R : Rel₂ r Proc} →
  Bisimulation-up-to-bisimilarity R →
  Bisimulation (Bisimilarity ⊙ R ⊙ Bisimilarity)
bisimulation-up-to-∼⇒bisimulation R-is =
  ⟪_,_⟫ {R = _ ⊙ _ ⊙ _}
    (λ { (q , p∼q , r , qRr , r∼s) p⟶p′ →
       let q′ , q⟶q′ , p′∼q′ =
             left-to-right bisimilarity-is-a-bisimulation p∼q p⟶p′
           r′ , r⟶r′ , (q″ , q′∼q″ , r″ , q″Rr″ , r″∼r′) =
             left-to-right R-is qRr q⟶q′
           s′ , s⟶s′ , r′∼s′ =
             left-to-right bisimilarity-is-a-bisimulation r∼s r⟶r′
       in
         s′ , s⟶s′ , q″
       , transitive-∼ p′∼q′ q′∼q″
       , r″ , q″Rr″
       , transitive-∼ r″∼r′ r′∼s′ })
    (λ { (q , p∼q , r , qRr , r∼s) s⟶s′ →
       let r′ , r⟶r′ , r′∼s′ =
             right-to-left bisimilarity-is-a-bisimulation r∼s s⟶s′
           q′ , q⟶q′ , (q″ , q′∼q″ , r″ , q″Rr″ , r″∼r′) =
             right-to-left R-is qRr r⟶r′
           p′ , p⟶p′ , p′∼q′ =
             right-to-left bisimilarity-is-a-bisimulation p∼q q⟶q′
       in
         p′ , p⟶p′ , q″
       , transitive-∼ p′∼q′ q′∼q″
       , r″ , q″Rr″
       , transitive-∼ r″∼r′ r′∼s′ })

-- If R is a bisimulation up to bisimilarity, then R is contained in
-- bisimilarity.

bisimulation-up-to-∼⊆∼ :
  ∀ {r} {R : Rel₂ r Proc} →
  Bisimulation-up-to-bisimilarity R →
  R ⊆ Bisimilarity
bisimulation-up-to-∼⊆∼ {R = R} R-is =
  R                                ⊆⟨ (λ { {p , q} pRq → p , reflexive-∼ , q , pRq , reflexive-∼ }) ⟩
  Bisimilarity ⊙ R ⊙ Bisimilarity  ⊆⟨ bisimulation⊆∼ (bisimulation-up-to-∼⇒bisimulation R-is) ⟩∎
  Bisimilarity                     ∎

------------------------------------------------------------------------
-- Bisimulations up to union

-- Bisimulations up to ∪.

Bisimulation-up-to-∪ : ∀ {r} → Rel₂ r Proc → Type (lsuc ℓ ⊔ r)
Bisimulation-up-to-∪ R = Progression R (R ∪ Bisimilarity)

-- If _R_ is a bisimulation up to ∪, then _R_ ∪ _∼_ is a bisimulation.

bisimulation-up-to-∪⇒bisimulation :
  ∀ {r} {R : Rel₂ r Proc} →
  Bisimulation-up-to-∪ R →
  Bisimulation (R ∪ Bisimilarity)
bisimulation-up-to-∪⇒bisimulation R-is =
  ⟪ [ left-to-right R-is
    , (λ p∼q → Σ-map id (Σ-map id inj₂) ∘
               left-to-right bisimilarity-is-a-bisimulation p∼q)
    ]
  , [ right-to-left R-is
    , (λ p∼q → Σ-map id (Σ-map id inj₂) ∘
               right-to-left bisimilarity-is-a-bisimulation p∼q)
    ]
  ⟫

-- If R is a bisimulation up to ∪, then R is contained in
-- bisimilarity.

bisimulation-up-to-∪⊆∼ :
  ∀ {r} {R : Rel₂ r Proc} →
  Bisimulation-up-to-∪ R →
  R ⊆ Bisimilarity
bisimulation-up-to-∪⊆∼ {R = R} R-is =
  R                 ⊆⟨ inj₁ ⟩
  R ∪ Bisimilarity  ⊆⟨ bisimulation⊆∼ (bisimulation-up-to-∪⇒bisimulation R-is) ⟩∎
  Bisimilarity      ∎

------------------------------------------------------------------------
-- Bisimulations up to reflexive transitive closure

-- Bisimulations up to reflexive transitive closure.

Bisimulation-up-to-* : Rel₂ ℓ Proc → Type ℓ
Bisimulation-up-to-* R = Progression R (R *)

-- If R is a bisimulation up to reflexive transitive closure, then R *
-- is a bisimulation.

bisimulation-up-to-*⇒bisimulation :
  ∀ {R} → Bisimulation-up-to-* R → Bisimulation (R *)
bisimulation-up-to-*⇒bisimulation {R} R-is = ⟪ lr , rl ⟫
  where
  lr : ∀ {p p′ q μ} →
       (R *) (p , q) → p [ μ ]⟶ p′ →
       ∃ λ q′ → q [ μ ]⟶ q′ × (R *) (p′ , q′)
  lr (zero  , refl)           q⟶p′ = _ , q⟶p′ , zero , refl
  lr (suc n , r , pRr , rRⁿq) p⟶p′ =
    let r′ , r⟶r′ , p′R*r′ = left-to-right R-is pRr p⟶p′
        q′ , q⟶q′ , r′R*q′ = lr (n , rRⁿq) r⟶r′
    in q′ , q⟶q′ , *-trans p′R*r′ r′R*q′

  rl : ∀ {p q q′ μ} →
       (R *) (p , q) → q [ μ ]⟶ q′ →
       ∃ λ p′ → p [ μ ]⟶ p′ × (R *) (p′ , q′)
  rl (zero  , refl)           p⟶q′ = _ , p⟶q′ , zero , refl
  rl (suc n , r , pRr , rRⁿq) q⟶q′ =
    let r′ , r⟶r′ , r′R*q′ = rl (n , rRⁿq) q⟶q′
        p′ , p⟶p′ , p′R*r′ = right-to-left R-is pRr r⟶r′
    in p′ , p⟶p′ , *-trans p′R*r′ r′R*q′

-- If R is a bisimulation up to reflexive transitive closure, then R
-- is contained in bisimilarity.

bisimulation-up-to-*⊆∼ :
  ∀ {R} → Bisimulation-up-to-* R → R ⊆ Bisimilarity
bisimulation-up-to-*⊆∼ {R} R-is =
  R             ⊆⟨ (λ pRq → 1 , _ , pRq , refl) ⟩
  (R *)         ⊆⟨ bisimulation⊆∼ (bisimulation-up-to-*⇒bisimulation R-is) ⟩∎
  Bisimilarity  ∎

------------------------------------------------------------------------
-- Some preservation results

-- These results are not taken from "Enhancements of the bisimulation
-- proof method".

-- Equal processes are bisimilar.

≡⇒∼ : ∀ {p q} → p ≡ q → p ∼ q
≡⇒∼ refl = reflexive-∼

-- Precomposition with the lifting operator preserves the "is a
-- bisimulation" relation.

↑-preserves-bisimulations :
  ∀ {ℓ r} {R : Rel₂ r Proc} →
  Bisimulation R → Bisimulation (↑ ℓ ∘ R)
↑-preserves-bisimulations R-is =
  ⟪ (λ pRq → Σ-map id (Σ-map id lift) ∘ left-to-right R-is (lower pRq))
  , (λ pRq → Σ-map id (Σ-map id lift) ∘ right-to-left R-is (lower pRq))
  ⟫

-- The "times two" operator preserves the "is a bisimulation"
-- relation.

×2-preserves-bisimulations :
  ∀ {r} {R : Rel₂ r Proc} →
  Bisimulation R →
  Bisimulation (R ∪ R)
×2-preserves-bisimulations R-is =
  ⟪ (let f = λ pRq p⟶p′ →
               Σ-map id (Σ-map id inj₁) (left-to-right R-is pRq p⟶p′) in
     [ f , f ])
  , (let f = λ pRq q⟶q′ →
               Σ-map id (Σ-map id inj₁) (right-to-left R-is pRq q⟶q′) in
     [ f , f ])
  ⟫

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

module Data.Binary.Definitions where

open import Function
open import Data.Binary.Bits public
open import Data.List using (_∷_) renaming ([] to 1ᵇ) public
open import Data.Maybe
open import Data.Product

𝔹⁺ : Set
𝔹⁺ = Data.List.List Bit

𝔹 : Set
𝔹 = Maybe 𝔹⁺

infixr 5 0<_
pattern 0ᵇ = nothing
pattern 0<_ x = just x

𝔹± : Set
𝔹± = Maybe (Bit × 𝔹⁺)

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
------------------------------------------------------------------------
-- The delay monad quotiented by weak bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

module Partiality-monad.Coinductive where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)
open import Prelude.Size

open import H-level.Truncation.Propositional equality-with-paths
open import Quotient equality-with-paths

open import Delay-monad
open import Delay-monad.Bisimilarity

-- The partiality monad, defined as the delay monad quotiented by
-- (propositionally truncated) weak bisimilarity.

_⊥ : ∀ {a} → Type a → Type a
A ⊥ = Delay A ∞ / λ x y → ∥ x ≈ y ∥

-- The partiality monad is a set.

⊥-is-set : ∀ {a} {A : Type a} → Is-set (A ⊥)
⊥-is-set = /-is-set

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module _ where

record R : Set₁ where
  constructor c

open R {{...}}


text:
-- Andreas, 2019-10-01, continuing issue #3855 (erasure modality @0)
-- Test case by Nisse at https://github.com/agda/agda/issues/3855#issuecomment-527164352

-- Occurs check needs to take erasure status of definitions
-- (here: postulates) into account.

postulate
  P    : Set → Set
  p    : (A : Set) → P A
  @0 A : Set

-- fails : P A
-- fails = p A

test : P A
test = p _

-- Should fail with error like:
--
-- Cannot instantiate the metavariable _2 to solution A
-- since (part of) the solution was created in an erased context
-- when checking that the expression p _ has type P A


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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)
module Loop.Structures
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where

open import Algebra.Core
open import Level using (_⊔_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Algebra.Definitions _≈_
open import Loop.Definitions _≈_
open import Algebra.Structures _≈_

record IsLeftBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isLoop  : IsLoop ∙ \\ //  ε
    leftBol : LeftBol ∙

  open IsLoop isLoop public

record IsRightBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isLoop   : IsLoop ∙ \\ //  ε
    rightBol : RightBol ∙

  open IsLoop isLoop public

record IsMoufangLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isLoop           : IsLoop ∙ \\ // ε
    moufangIdentity  : MoufangIdentity₁ ∙
    moufangIdentity₂ : MoufangIdentity₂ ∙
    moufangIdentity₃ : MoufangIdentity₃ ∙
    moufangIdentity₄ : MoufangIdentity₄ ∙

  open IsLoop isLoop public


text:
-- Andreas, 2015-07-21 Issue 1612
-- Error "D is not strictly positive" should appear immediately.
-- (There was a performance problem due to the use of Utils.Graph.....allPaths).

{-# NON_TERMINATING #-}

mutual

  data D : Set where
    c0 : A0 → D
    c1 : A1 → D
    c2 : A2 → D
    c3 : A3 → D
    c4 : A4 → D
    c5 : A5 → D
    c6 : A6 → D
    c7 : A7 → D
    c8 : A8 → D
    c9 : A9 → D

  A0 : Set
  A0 = B0

  B0 : Set
  B0 = A0 → D

  A1 : Set
  A1 = B1

  B1 : Set
  B1 = A1 → D

  A2 : Set
  A2 = B2

  B2 : Set
  B2 = A2 → D

  A3 : Set
  A3 = B3

  B3 : Set
  B3 = A3 → D

  A4 : Set
  A4 = B4

  B4 : Set
  B4 = A4 → D

  A5 : Set
  A5 = B5

  B5 : Set
  B5 = A5 → D

  A6 : Set
  A6 = B6

  B6 : Set
  B6 = A6 → D

  A7 : Set
  A7 = B7

  B7 : Set
  B7 = A7 → D

  A8 : Set
  A8 = B8

  B8 : Set
  B8 = A8 → D

  A9 : Set
  A9 = B9

  B9 : Set
  B9 = A9 → D


text:
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (from-yes)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Tri)
open Tri
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; trans)

open import Data.Empty using (⊥)
open import Data.Sum using (inj₁; inj₂)

module AKS.Primality.Properties where

open import AKS.Nat using (ℕ; _+_; _≟_; _<_; _>_; _<?_; _≤_)
open import AKS.Nat using (<-cmp; <-irrefl; <-trans; 0<1+n; ≤-antisym; 0≤n; suc-injective-≤; <⇒≤; ≢⇒¬≟; <⇒≱; n≤m⇒n<m⊎n≡m; ≤-refl; n<1+n)
open import AKS.Nat using (Acc; acc; <-well-founded; _⊂_; Interval; [_,_∣_]; ⊂-well-founded; upward)
open import AKS.Nat.GCD
  using (_∣_; _∤_; _∣?_; gcd; bézout; lemma; Identity; gcd[a,b]∣a; gcd[a,b]∣b; 0∣n⇒n≈0; ∣-respˡ; ∣⇒≤; ∣-trans)
  renaming (_⊥_ to _coprime_)

open import AKS.Primality.Base

prime≢0 : ∀ {p} → IsPrime p → p ≢ 0
prime≢0 (IsPrime✓ 1<p _) p≡0 = <-irrefl (sym p≡0) (<-trans 0<1+n 1<p)

¬prime<2 : ∀ p → p < 2 → ¬ (IsPrime p)
¬prime<2 p p<2 (IsPrime✓ 1<p ∀i∣p[i≡p]) = contradiction 1<p (<⇒≱ p<2)

exclusive : ∀ {n} → IsPrime n → IsComposite n → ⊥
exclusive {n} (IsPrime✓ 1<n ∀i∣n[i≡n]) (IsComposite✓ p p<n (IsPrime✓ 1<p _) p∣n)
  = contradiction p<n (<-irrefl (∀i∣n[i≡n] 1<p p∣n))

n<1⇒n≡0 : ∀ {n} → n < 1 → n ≡ 0
n<1⇒n≡0 {n} n<1 = ≤-antisym (suc-injective-≤ n<1) 0≤n

n⊥prime : ∀ {p} n {n≢0 : n ≢ 0} → n < p → IsPrime p → n coprime p
n⊥prime {p} n {n≢0} n<p (IsPrime✓ 1<p ∀i∣p[i≡p]) with <-cmp 1 (gcd n p)
... | tri> _ _ 1>gcd[n,p] = contradiction (0∣n⇒n≈0 (∣-respˡ (n<1⇒n≡0 1>gcd[n,p]) (gcd[a,b]∣a n p))) n≢0
... | tri≈ _ 1≡gcd[n,p] _ = sym 1≡gcd[n,p]
... | tri< 1<gcd[n,p] _ _ = contradiction p≤n (<⇒≱ n<p)
  where
  gcd[n,p]≡p : gcd n p ≡ p
  gcd[n,p]≡p = ∀i∣p[i≡p] 1<gcd[n,p] (gcd[a,b]∣b n p)
  p∣n : p ∣ n
  p∣n = ∣-respˡ gcd[n,p]≡p (gcd[a,b]∣a n p)
  p≤n : p ≤ n
  p≤n = ∣⇒≤ {n≢0 = ≢⇒¬≟ n≢0} p∣n

bézout-prime : ∀ x p → x ≢ 0 → x < p → IsPrime p → Identity 1 x p
bézout-prime x p x≢0 x<p p-isPrime with bézout x p | n⊥prime x {x≢0} x<p p-isPrime
bézout-prime x p x≢0 x<p p-isPrime | lemma d gcd[x,p]≡d ident | gcd[x,p]≡1 with trans (sym gcd[x,p]≡d) gcd[x,p]≡1
bézout-prime x p x≢0 x<p p-isPrime | lemma .1 gcd[x,p]≡d ident | gcd[x,p]≡1 | refl = ident

compositionalityⁱ : ∀ n → 1 < n → Acc _<_ n → Compositionality n
primalityⁱ : ∀ n → 1 < n → Acc _<_ n → Primality n

compositionalityⁱ n 1<n (acc downward)
  = loop 2 (from-yes (1 <? 2)) 1<n ⊂-well-founded ¬p<2[p∤n]
  where
  ¬p<2[p∤n] : ∀ {p} → p < 2 → IsPrime p → p ∤ n
  ¬p<2[p∤n] {p} p<2 p-isPrime _ = contradiction p-isPrime (¬prime<2 p p<2)
  cons
    : ∀ {x}
    → (IsPrime x → x ∤ n)
    → (∀ {p} → p < x → IsPrime p → p ∤ n)
    → (∀ {p} → p < 1 + x → IsPrime p → p ∤ n)
  cons {x} x-isPrime⇒x∤n ∀p<x[p∤n] {p} p<1+x p-isPrime p∣n with <-cmp p x
  ... | tri< p<x _ _ = contradiction p∣n (∀p<x[p∤n] p<x p-isPrime)
  ... | tri≈ _ refl _ = contradiction p∣n (x-isPrime⇒x∤n p-isPrime)
  ... | tri> _ _ x<p = contradiction (suc-injective-≤ p<1+x) (<⇒≱ x<p)
  loop
    : ∀ x → 1 < x → (x≤n : x ≤ n) → Acc _⊂_ [ x , n ∣ x≤n ]
    → (∀ {p} → p < x → IsPrime p → p ∤ n)
    → Compositionality n
  loop x 1<x x≤n (acc next) ∀p<x⇒p∤n with n≤m⇒n<m⊎n≡m x≤n
  ... | inj₂ refl = Prime✓ ∀p<x⇒p∤n
  ... | inj₁ x<n with primalityⁱ x 1<x (downward x<n)
  ...   | Composite✓ x-isComposite = loop (1 + x) (<-trans 1<x n<1+n) x<n (next [1+x,n]⊂[x,n]) ∀p<1+x⇒p∤n
          where
          [1+x,n]⊂[x,n] : [ 1 + x , n ∣ x<n ] ⊂ [ x , n ∣ x≤n ]
          [1+x,n]⊂[x,n] = upward n<1+n ≤-refl
          ∀p<1+x⇒p∤n = cons (λ x-isPrime _ → exclusive x-isPrime x-isComposite) ∀p<x⇒p∤n
  ...   | Prime✓ x-isPrime with x ∣? n
  ...     | yes x∣n = Composite✓ (IsComposite✓ x x<n x-isPrime x∣n)
  ...     | no ¬x∣n = loop (1 + x) (<-trans 1<x n<1+n) x<n (next [1+x,n]⊂[x,n]) ∀p<1+x[p∤n]
          where
          [1+x,n]⊂[x,n] : [ 1 + x , n ∣ x<n ] ⊂ [ x , n ∣ x≤n ]
          [1+x,n]⊂[x,n] = upward n<1+n ≤-refl
          ∀p<1+x[p∤n] = cons (λ _ x∣n → ¬x∣n x∣n) ∀p<x⇒p∤n

primalityⁱ n 1<n wf@(acc downward) with compositionalityⁱ n 1<n wf
... | Composite✓ isComposite = Composite✓ isComposite
  -- n is a composite so just return the proof of compositionality
... | Prime✓ ∀p<n[p∤n] = Prime✓ (IsPrime✓ 1<n ∀i∣n[i≡n])
  -- All prime divisors less then n do not divide n therefore n is prime (#1)
  where
  n≢0 : n ≢ 0
  n≢0 n≡0 = <-irrefl (sym n≡0) (<-trans 0<1+n 1<n)
  ∀i∣n[i≡n] : ∀ {i} → 1 < i → i ∣ n → i ≡ n
  ∀i∣n[i≡n] {i} 1<i i∣n with <-cmp i n
  ... | tri> _ _ n<i = contradiction (∣⇒≤ {n≢0 = ≢⇒¬≟ n≢0} i∣n) (<⇒≱ n<i)
      -- i is larger than n so i divides n so i is less then or equal to n ⇒⇐
  ... | tri≈ _ i≡n _ = i≡n
  ... | tri< i<n _ _ with primalityⁱ i 1<i (downward i<n)
  ...   | Prime✓ i-isPrime
        = contradiction i∣n (∀p<n[p∤n] i<n i-isPrime)
        -- i is a prime divisor of n (#1) ⇒⇐
  ...   | Composite✓ (IsComposite✓ p p<i p-isPrime p∣i)
        = contradiction (∣-trans p∣i i∣n) (∀p<n[p∤n] (<-trans p<i i<n) p-isPrime)
        -- i is a composite number with a prime divisor therefore there exists a prime divisor of n (#1) ⇒⇐

primality : ∀ n → 1 < n → Primality n
primality n 1<n = primalityⁱ n 1<n <-well-founded

prime? : ∀ n → Dec (IsPrime n)
prime? n with 1 <? n
... | no ¬1<n = no λ { (IsPrime✓ 1<n _) → ¬1<n 1<n }
... | yes 1<n with primality n 1<n
... | Prime✓ isPrime = yes isPrime
... | Composite✓ isComposite = no λ { isPrime → exclusive isPrime isComposite }

composite? : ∀ n → Dec (IsComposite n)
composite? n with 1 <? n
... | no ¬1<n = no λ { (IsComposite✓ p p<n (IsPrime✓ 1<p _) _) → ¬1<n (<-trans 1<p p<n) }
... | yes 1<n with primality n 1<n
... | Prime✓ isPrime = no λ { isComposite → exclusive isPrime isComposite }
... | Composite✓ isComposite = yes isComposite

-- 13-isPrime : IsPrime 13
-- 13-isPrime = from-yes (prime? 13)

-- 24-isComposite : IsComposite 24
-- 24-isComposite = from-yes (composite? 24)

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Common syntax.

module BasicIS4.Syntax.Common where

open import Common.ContextPair public

-- Types, or propositions.

infixr 10 □_
infixl 9 _∧_
infixr 7 _▻_
data Ty : Set where
  α_  : Atom → Ty
  _▻_ : Ty → Ty → Ty
  □_  : Ty → Ty
  _∧_ : Ty → Ty → Ty
  ⊤  : Ty

-- Additional useful types.

infix 7 _▻◅_
_▻◅_ : Ty → Ty → Ty
A ▻◅ B = (A ▻ B) ∧ (B ▻ A)

infixr 7 _▻⋯▻_
_▻⋯▻_ : Cx Ty → Ty → Ty
∅       ▻⋯▻ B = B
(Ξ , A) ▻⋯▻ B = Ξ ▻⋯▻ (A ▻ B)

infixr 10 □⋆_
□⋆_ : Cx Ty → Cx Ty
□⋆ ∅       = ∅
□⋆ (Ξ , A) = □⋆ Ξ , □ A

dist□⋆₁ : ∀ Ξ Ξ′ → □⋆ (Ξ ⧺ Ξ′) ≡ (□⋆ Ξ) ⧺ (□⋆ Ξ′)
dist□⋆₁ Ξ ∅        = refl
dist□⋆₁ Ξ (Ξ′ , A) = cong² _,_ (dist□⋆₁ Ξ Ξ′) refl

lift⊆ : ∀ {Δ Δ′} → Δ ⊆ Δ′ → □⋆ Δ ⊆ □⋆ Δ′
lift⊆ done     = done
lift⊆ (skip θ) = skip (lift⊆ θ)
lift⊆ (keep θ) = keep (lift⊆ θ)

-- Inversion principles.

invα : ∀ {P P′} → α P ≡ α P′ → P ≡ P′
invα refl = refl

inv▻₁ : ∀ {A A′ B B′} → A ▻ B ≡ A′ ▻ B′ → A ≡ A′
inv▻₁ refl = refl

inv▻₂ : ∀ {A A′ B B′} → A ▻ B ≡ A′ ▻ B′ → B ≡ B′
inv▻₂ refl = refl

inv□ : ∀ {A A′} → □ A ≡ □ A′ → A ≡ A′
inv□ refl = refl

inv∧₁ : ∀ {A A′ B B′} → A ∧ B ≡ A′ ∧ B′ → A ≡ A′
inv∧₁ refl = refl

inv∧₂ : ∀ {A A′ B B′} → A ∧ B ≡ A′ ∧ B′ → B ≡ B′
inv∧₂ refl = refl

-- Decidable equality on types.

_≟ᵀ_ : (A A′ : Ty) → Dec (A ≡ A′)
(α P)   ≟ᵀ (α P′)    with P ≟ᵅ P′
(α P)   ≟ᵀ (α .P)    | yes refl = yes refl
(α P)   ≟ᵀ (α P′)    | no  P≢P′ = no (P≢P′ ∘ invα)
(α P)   ≟ᵀ (A′ ▻ B′) = no λ ()
(α P)   ≟ᵀ (□ A′)    = no λ ()
(α P)   ≟ᵀ (A′ ∧ B′) = no λ ()
(α P)   ≟ᵀ ⊤        = no λ ()
(A ▻ B) ≟ᵀ (α P′)    = no λ ()
(A ▻ B) ≟ᵀ (A′ ▻ B′) with A ≟ᵀ A′ | B ≟ᵀ B′
(A ▻ B) ≟ᵀ (.A ▻ .B) | yes refl | yes refl = yes refl
(A ▻ B) ≟ᵀ (A′ ▻ B′) | no  A≢A′ | _        = no (A≢A′ ∘ inv▻₁)
(A ▻ B) ≟ᵀ (A′ ▻ B′) | _        | no  B≢B′ = no (B≢B′ ∘ inv▻₂)
(A ▻ B) ≟ᵀ (□ A′)    = no λ ()
(A ▻ B) ≟ᵀ (A′ ∧ B′) = no λ ()
(A ▻ B) ≟ᵀ ⊤        = no λ ()
(□ A)   ≟ᵀ (α P′)    = no λ ()
(□ A)   ≟ᵀ (A′ ▻ B′) = no λ ()
(□ A)   ≟ᵀ (□ A′)    with A ≟ᵀ A′
(□ A)   ≟ᵀ (□ .A)    | yes refl = yes refl
(□ A)   ≟ᵀ (□ A′)    | no  A≢A′ = no (A≢A′ ∘ inv□)
(□ A)   ≟ᵀ (A′ ∧ B′) = no λ ()
(□ A)   ≟ᵀ ⊤        = no λ ()
(A ∧ B) ≟ᵀ (α P′)    = no λ ()
(A ∧ B) ≟ᵀ (A′ ▻ B′) = no λ ()
(A ∧ B) ≟ᵀ (□ A′)    = no λ ()
(A ∧ B) ≟ᵀ (A′ ∧ B′) with A ≟ᵀ A′ | B ≟ᵀ B′
(A ∧ B) ≟ᵀ (.A ∧ .B) | yes refl | yes refl = yes refl
(A ∧ B) ≟ᵀ (A′ ∧ B′) | no  A≢A′ | _        = no (A≢A′ ∘ inv∧₁)
(A ∧ B) ≟ᵀ (A′ ∧ B′) | _        | no  B≢B′ = no (B≢B′ ∘ inv∧₂)
(A ∧ B) ≟ᵀ ⊤        = no λ ()
⊤      ≟ᵀ (α P′)    = no λ ()
⊤      ≟ᵀ (A′ ▻ B′) = no λ ()
⊤      ≟ᵀ (□ A′)    = no λ ()
⊤      ≟ᵀ (A′ ∧ B′) = no λ ()
⊤      ≟ᵀ ⊤        = yes refl

open ContextEquality (_≟ᵀ_) public

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
-- 2011-09-15 posted by Nisse
-- {-# OPTIONS --show-implicit -v tc.lhs.unify:15 #-}
module Issue292-16 where

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

postulate
  A : Set
  f : A → A

data C : A → Set where
  c : ∀ x → C (f x)

record Box : Set where
  constructor box
  field
    a : A
    b : C a

test : ∀ {x₁ x₂} → box (f x₁) (c x₁) ≡ box (f x₂) (c x₂) → x₁ ≡ x₂
test refl = refl

-- this failed before because we tried
--
--   c x₁ : C (f x₁) =?= c₂ x₂ : C (f x₂)
--
-- and did not recognize that
--
--   x₁ : A =?= x₂ : A
--
-- is homogeneous

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --without-K --safe --overlapping-instances #-}
module Interpreter where

open import Data.Char hiding (_≤_)
open import Data.Bool hiding (_≤_)
open import Data.Nat hiding (_≤_)
open import Data.Unit
import Data.Nat as N
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality as PropEq
open import Relation.Nullary
import Data.String as Str
open import Data.Nat.Show
import Data.List as List
open import Data.Empty

infix 3 _:::_,_
infix 2 _∈_

infix 1 _⊢_

data `Set : Set where
  `ℕ    : `Set
  `Bool : `Set
  _`⇨_  : `Set → `Set → `Set
  `⊤    : `Set
  _`×_  : `Set → `Set → `Set
  _`+_  : `Set → `Set → `Set
infixr 2 _`⇨_

data Var : Set where
  x' : Var
  y' : Var
  z' : Var

-- Inequality proofs on variables
data _≠_ : Var → Var → Set where
  x≠y : x' ≠ y'
  x≠z : x' ≠ z'
  y≠x : y' ≠ x'
  y≠z : y' ≠ z'
  z≠x : z' ≠ x'
  z≠y : z' ≠ y'

⟦_⟧ : `Set → Set
⟦ `ℕ ⟧ = ℕ
⟦ `Bool ⟧ = Bool
⟦ (t `⇨ s) ⟧ =  ⟦ t ⟧ → ⟦ s ⟧
⟦ `⊤ ⟧ = ⊤
⟦ (t `× s) ⟧ = ⟦ t ⟧ × ⟦ s ⟧
⟦ (t `+ s) ⟧ = ⟦ t ⟧ ⊎ ⟦ s ⟧

data Γ : Set where
  ·         : Γ
  _:::_,_   : Var → `Set → Γ → Γ

data _∈_ :  Var → Γ → Set where
  H  : ∀ {x Δ t } → x ∈ x ::: t , Δ
  TH : ∀ {x y Δ t } → ⦃ prf : x ∈ Δ ⦄ → ⦃ neprf : x ≠ y ⦄ → x ∈ y ::: t , Δ

!Γ_[_] : ∀ {x} → (Δ : Γ) → x ∈ Δ → `Set
!Γ_[_] · ()
!Γ _ ::: t , Δ [ H ]     = t
!Γ _ ::: _ , Δ [ TH ⦃ prf = i ⦄ ]  = !Γ Δ [ i ]

infix 30 `v_
infix 30 `n_
infix 30 `¬_

infix 26 _`+_
infix 27 _`*_
infix 27 _`∧_
infix 26 _`∨_
infix 24 _`≤_
infix 24 _`,_
infixl 22 _`₋_

data _⊢_ : Γ → `Set → Set where
  `false           : ∀ {Δ} → Δ ⊢ `Bool
  `true            : ∀ {Δ} → Δ ⊢ `Bool
  `n_              : ∀ {Δ} → ℕ → Δ ⊢ `ℕ
  `v_              : ∀ {Δ} → (x : Var) → ⦃ i : x ∈ Δ ⦄ → Δ ⊢ !Γ Δ [ i ]
  _`₋_             : ∀ {Δ t s} → Δ ⊢ t `⇨ s → Δ ⊢ t → Δ ⊢ s --application
  `λ_`:_⇨_         : ∀ {Δ tr} → (x : Var) → (tx : `Set)
                        → x ::: tx , Δ ⊢ tr → Δ ⊢ tx `⇨ tr
  _`+_             : ∀ {Δ} → Δ ⊢ `ℕ → Δ ⊢ `ℕ → Δ ⊢ `ℕ
  _`*_             : ∀ {Δ} → Δ ⊢ `ℕ →  Δ ⊢ `ℕ → Δ ⊢ `ℕ
  _`∧_             : ∀ {Δ} → Δ ⊢ `Bool → Δ ⊢ `Bool → Δ ⊢ `Bool
  _`∨_             : ∀ {Δ} → Δ ⊢ `Bool →  Δ ⊢ `Bool → Δ ⊢ `Bool
  _`≤_             : ∀ {Δ} → Δ ⊢ `ℕ → Δ ⊢ `ℕ →  Δ ⊢ `Bool
  `¬_              : ∀ {Δ} → Δ ⊢ `Bool →  Δ ⊢ `Bool
  _`,_             : ∀ {Δ t s} → Δ ⊢ t →  Δ ⊢ s →  Δ ⊢ t `× s
  `fst             : ∀ {Δ t s} → Δ ⊢ t `× s → Δ ⊢ t
  `snd             : ∀ {Δ t s} → Δ ⊢ t `× s → Δ ⊢ s
  `left            : ∀ {Δ t s} → Δ ⊢ t → Δ ⊢ t `+ s
  `right           : ∀ {Δ t s} → Δ ⊢ s → Δ ⊢ t `+ s
  `case_`of_||_    : ∀ {Δ t s u} → Δ ⊢ t `+ s
                        → Δ ⊢ t `⇨ u → Δ ⊢ s `⇨ u → Δ ⊢ u
  `tt              : ∀ {Δ} → Δ ⊢ `⊤
  `let_`=_`in_     : ∀ {Δ th tb} → (x : Var)
                       → Δ ⊢ th → x ::: th , Δ ⊢ tb → Δ ⊢ tb
  `if_`then_`else_ : ∀ {Δ t} → Δ ⊢ `Bool → Δ ⊢ t → Δ ⊢ t → Δ ⊢ t

data ⟨_⟩ : Γ → Set₁ where
  []   : ⟨ · ⟩
  _∷_  : ∀ {x t Δ} → ⟦ t ⟧ → ⟨ Δ ⟩ → ⟨ x ::: t , Δ ⟩

!_[_] : ∀ {x Δ} → ⟨ Δ ⟩ → (i : x ∈ Δ) → ⟦ !Γ Δ [ i ] ⟧
!_[_] [] ()
!_[_] (val ∷ env) H      = val
!_[_] (val ∷ env) (TH ⦃ prf = i ⦄) = ! env [ i ]

interpret : ∀ {t} → · ⊢ t → ⟦ t ⟧
interpret = interpret' []
  where interpret' : ∀ {Δ t} → ⟨ Δ ⟩ → Δ ⊢ t → ⟦ t ⟧
        interpret' env `true = true
        interpret' env `false = false
        interpret' env `tt = tt
        interpret' env (`n n) = n
        interpret' env ((`v x) ⦃ i = idx ⦄) = ! env [ idx ]
        interpret' env (f `₋ x) = (interpret' env f) (interpret' env x)
        interpret' env (`λ _ `: tx ⇨ body) = λ (x : ⟦ tx ⟧) → interpret' (x ∷ env) body
        interpret' env (l `+ r) = interpret' env l + interpret' env r
        interpret' env (l `* r) = interpret' env l * interpret' env r
        interpret' env (l `∧ r) = interpret' env l ∧ interpret' env r
        interpret' env (l `∨ r) = interpret' env l ∨ interpret' env r
        interpret' env (l `≤ r) with interpret' env l N.≤? interpret' env r
        ...                             | yes  p = true
        ...                             | no ¬p = false
        interpret' env (`¬ x) = not (interpret' env x)
        interpret' env (f `, s) = interpret' env f ,′ interpret' env s
        interpret' env (`fst p) with interpret' env p
        interpret' env (`fst p) | f , s = f
        interpret' env (`snd p) with interpret' env p
        interpret' env (`snd p) | f , s = s
        interpret' env (`left v) = inj₁ (interpret' env v)
        interpret' env (`right v) = inj₂ (interpret' env v)
        interpret' env (`case s `of le || re) with interpret' env s
        interpret' env (`case s `of le || re) | inj₁ l = (interpret' env le) l
        interpret' env (`case s `of le || re) | inj₂ r = (interpret' env re) r
        interpret' env (`let _ `= h `in b) = let hval = interpret' env h in interpret' (hval ∷ env) b
        interpret' env (`if b `then et `else ef) with interpret' env b
        interpret' env (`if b `then et `else ef) | true = interpret' env et
        interpret' env (`if b `then et `else ef) | false = interpret' env ef

instance
  v_type₁ : ∀ {x Δ t} → x ∈ x ::: t , Δ
  v_type₁ = H

  v_type₂ : ∀ {x y Δ t} → ⦃ prf : x ∈ Δ ⦄ → ⦃ x ≠ y ⦄ → x ∈ y ::: t , Δ
  v_type₂ = TH

instance
  xy : x' ≠ y'
  xy = x≠y

  xz : x' ≠ z'
  xz = x≠z

  yx : y' ≠ x'
  yx = y≠x

  yz : y' ≠ z'
  yz = y≠z

  zx : z' ≠ x'
  zx = z≠x

  zy : z' ≠ y'
  zy = z≠y

max_stars_repo_name: sseefried/well-typed-agda-interpreter

max_issues_repo_name: sseefried/well-typed-agda-interpreter

max_forks_repo_name: sseefried/well-typed-agda-interpreter


text:
-- Andreas, 2016-10-23 issue #2280:
-- Solver throws away meta arguments.
-- (Issue discovered by code review.)

open import Common.Equality
open import Common.Product

data Bool : Set where
  true false : Bool

postulate
  not : Bool → Bool

data D (f : Bool → Bool) : Set where
  c : ∀ x → x ≡ not (f true) → D f

test : D {!!}
test = c {!!} refl

-- C-c C-= says
-- ?1 := not (?0 true)

-- But C-c C-s solves
-- ?1 := not ?

-- Ulf says this is fine, since we create a new interaction meta.
-- I must agree.

data E (p : Bool × Bool) : Set where
  c : ∀ x → x ≡ not (proj₁ p) → E p

test2 : E {!!}
test2 = c {!!} refl

-- Consequently, C-c C-s should solve the last meta as
-- ?3 := not ?


text:
module Lib.Prelude where

infixr 90 _∘_
infixr 1 _,_

id : {A : Set} -> A -> A
id x = x

_∘_ : {A : Set}{B : A -> Set}{C : {x : A} -> B x -> Set}
      (f : {x : A}(y : B x) -> C y)(g : (x : A) -> B x)(x : A) ->
      C (g x)
(f ∘ g) x = f (g x)

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}

postulate String : Set

{-# BUILTIN STRING String #-}

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

{-# COMPILED_DATA _×_ (,) (,) #-}

fst : {A B : Set} -> A × B -> A
fst (x , y) = x

snd : {A B : Set} -> A × B -> B
snd (x , y) = y


text:
------------------------------------------------------------------------
-- Up-to techniques for the delay monad and the alternative
-- coinductive definition of weak bisimilarity
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.Weak.Alternative.Up-to.Delay-monad
         {a} {A : Type a} where

open import Delay-monad
import Delay-monad.Bisimilarity as B
import Delay-monad.Partial-order as P
open import Equality.Propositional as Eq
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Excluded-middle equality-with-J
open import Function-universe equality-with-J hiding (id)
open import H-level equality-with-J

import Bisimilarity.Weak.Alternative.Equational-reasoning-instances
import Bisimilarity.Weak.Delay-monad as W′
open import Bisimilarity.Weak.Equivalent
open import Equational-reasoning
open import Labelled-transition-system
open import Labelled-transition-system.Delay-monad A
open import Relation

open import Bisimilarity.Step (weak delay-monad) _[_]⇒̂_ _[_]⇒̂_
open import Bisimilarity.Up-to (weak delay-monad)
import Bisimilarity.Weak delay-monad as BW
open import Bisimilarity.Weak.Alternative delay-monad

-- Everything is an up-to technique for the alternative coinductive
-- definition of weak bisimilarity for the delay monad (if A is a set,
-- and assuming excluded middle and extensionality).

everything-up-to :
  Excluded-middle a →
  Eq.Extensionality a a →
  Is-set A →
  (F : Trans₂ a (Delay A ∞)) →
  Up-to-technique F
everything-up-to em ext A-set F {R = R} R-prog {x = x , y} =
  everything-up-to′ x y
  where
  lemma :
    ∀ {x y} {P : Rel₂ a (Delay A ∞)} →
    (∀ {x′ z} → x [ just z ]⇒̂ x′ →
     ∃ λ y′ → y [ just z ]⇒̂ y′ × P (x′ , y′)) →
    (∃ λ z → now z B.≈ x) →
    x ≈ y
  lemma {x} {y} hyp = uncurry λ z →
    now z B.≈ x                              ↝⟨ _⇔_.to W′.direct⇔alternative ⟩
    now z ≈ x                                ↝⟨ (λ nz≈x → Σ-map id proj₁ $ left-to-right nz≈x (⟶→⇒̂ now)) ⟩
    ∃ (x [ just z ]⇒̂_)                       ↝⟨ (λ x⇒̂ → x⇒̂ , Σ-map id proj₁ (hyp (proj₂ x⇒̂))) ⟩
    ∃ (x [ just z ]⇒̂_) × ∃ (y [ just z ]⇒̂_)  ↝⟨ (uncurry λ x⇒̂ y⇒̂ → W′.⇒̂-with-equal-labels→≈ id (proj₂ x⇒̂) (proj₂ y⇒̂)) ⟩
    x BW.≈ y                                 ↝⟨ ⇒alternative ⟩□
    x ≈ y                                    □

  everything-up-to′ : ∀ x y → R (x , y) → x ≈ y
  everything-up-to′ x y Rxy =
    case P.⇑⊎⇓ em ext A-set x ,′ P.⇑⊎⇓ em ext A-set y of λ where
      (inj₂ x⇓ , _)       → lemma (StepC.left-to-right (R-prog Rxy)) x⇓
      (_       , inj₂ y⇓) → symmetric
                              (lemma (StepC.right-to-left (R-prog Rxy))
                                     y⇓)
      (inj₁ x⇑ , inj₁ y⇑) →
        x      ∼⟨ symmetric (_⇔_.to W′.direct⇔alternative x⇑) ⟩
        never  ∼⟨ _⇔_.to W′.direct⇔alternative y⇑ ⟩■
        y


text:
-- TODO
-- Gentzen-style formalisation of syntax.
-- Simple terms.

module BasicT.Syntax.Gentzen where

open import BasicT.Syntax.Common public

-- Derivations.

infix 3 _⊢_
data _⊢_ (Γ : Cx Ty) : Ty → Set where
  var   : ∀ {A}   → A ∈ Γ → Γ ⊢ A
  lam   : ∀ {A B} → Γ , A ⊢ B → Γ ⊢ A ▻ B
  app   : ∀ {A B} → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
  pair  : ∀ {A B} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
  fst   : ∀ {A B} → Γ ⊢ A ∧ B → Γ ⊢ A
  snd   : ∀ {A B} → Γ ⊢ A ∧ B → Γ ⊢ B
  unit  : Γ ⊢ ⊤
  true  : Γ ⊢ BOOL
  false : Γ ⊢ BOOL
  if    : ∀ {C}   → Γ ⊢ BOOL → Γ ⊢ C → Γ ⊢ C → Γ ⊢ C
  zero  : Γ ⊢ NAT
  suc   : Γ ⊢ NAT → Γ ⊢ NAT
  it    : ∀ {C}   → Γ ⊢ NAT → Γ ⊢ C ▻ C → Γ ⊢ C → Γ ⊢ C
  rec   : ∀ {C}   → Γ ⊢ NAT → Γ ⊢ NAT ▻ C ▻ C → Γ ⊢ C → Γ ⊢ C

infix 3 _⊢⋆_
_⊢⋆_ : Cx Ty → Cx Ty → Set
Γ ⊢⋆ ∅     = 𝟙
Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ η (var i)     = var (mono∈ η i)
mono⊢ η (lam t)     = lam (mono⊢ (keep η) t)
mono⊢ η (app t u)   = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η (pair t u)  = pair (mono⊢ η t) (mono⊢ η u)
mono⊢ η (fst t)     = fst (mono⊢ η t)
mono⊢ η (snd t)     = snd (mono⊢ η t)
mono⊢ η unit        = unit
mono⊢ η true        = true
mono⊢ η false       = false
mono⊢ η (if t u v)  = if (mono⊢ η t) (mono⊢ η u) (mono⊢ η v)
mono⊢ η zero        = zero
mono⊢ η (suc t)     = suc (mono⊢ η t)
mono⊢ η (it t u v)  = it (mono⊢ η t) (mono⊢ η u) (mono⊢ η v)
mono⊢ η (rec t u v) = rec (mono⊢ η t) (mono⊢ η u) (mono⊢ η v)

mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
mono⊢⋆ {∅}     η ∙        = ∙
mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Shorthand for variables.

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → Γ , A , B ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ} → Γ , A , B , C ⊢ A
v₂ = var i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem is built-in.

lam⋆ : ∀ {Ξ Γ A} → Γ ⧺ Ξ ⊢ A → Γ ⊢ Ξ ▻⋯▻ A
lam⋆ {∅}     = I
lam⋆ {Ξ , B} = lam⋆ {Ξ} ∘ lam

lam⋆₀ : ∀ {Γ A} → Γ ⊢ A → ∅ ⊢ Γ ▻⋯▻ A
lam⋆₀ {∅}     = I
lam⋆₀ {Γ , B} = lam⋆₀ ∘ lam

-- Detachment theorem.

det : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ , A ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

det⋆ : ∀ {Ξ Γ A} → Γ ⊢ Ξ ▻⋯▻ A → Γ ⧺ Ξ ⊢ A
det⋆ {∅}     = I
det⋆ {Ξ , B} = det ∘ det⋆ {Ξ}

det⋆₀ : ∀ {Γ A} → ∅ ⊢ Γ ▻⋯▻ A → Γ ⊢ A
det⋆₀ {∅}     = I
det⋆₀ {Γ , B} = det ∘ det⋆₀

-- Cut and multicut.

cut : ∀ {A B Γ} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut t u = app (lam u) t

multicut : ∀ {Ξ A Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

ccont : ∀ {A B Γ} → Γ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ} → Γ , A , A ⊢ B → Γ , A ⊢ B
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ} → Γ , A , B ⊢ C → Γ , B , A ⊢ C
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ} → Γ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ} → Γ , B ⊢ C → Γ , A ⊢ B → Γ , A ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in combinatory form.

ci : ∀ {A Γ} → Γ ⊢ A ▻ A
ci = lam v₀

ck : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A
ck = lam (lam v₁)

cs : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

cpair : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A ∧ B
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ A
cfst = lam (fst v₀)

csnd : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ B
csnd = lam (snd v₀)

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ → Γ , A ⊢ B → Γ′ ⊢ A → Γ ⧺ Γ′ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

-- Substitution.

[_≔_]_ : ∀ {A B Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢ B → Γ ∖ i ⊢ B
[ i ≔ s ] var j     with i ≟∈ j
[ i ≔ s ] var .i    | same   = s
[ i ≔ s ] var ._    | diff j = var j
[ i ≔ s ] lam t     = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
[ i ≔ s ] app t u   = app ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] pair t u  = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] fst t     = fst ([ i ≔ s ] t)
[ i ≔ s ] snd t     = snd ([ i ≔ s ] t)
[ i ≔ s ] unit      = unit
[ i ≔ s ] true      = true
[ i ≔ s ] false     = false
[ i ≔ s ] if t u v  = if ([ i ≔ s ] t) ([ i ≔ s ] u) ([ i ≔ s ] v)
[ i ≔ s ] zero      = zero
[ i ≔ s ] suc t     = suc ([ i ≔ s ] t)
[ i ≔ s ] it t u v  = it ([ i ≔ s ] t) ([ i ≔ s ] u) ([ i ≔ s ] v)
[ i ≔ s ] rec t u v = rec ([ i ≔ s ] t) ([ i ≔ s ] u) ([ i ≔ s ] v)

[_≔_]⋆_ : ∀ {Ξ A Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢⋆ Ξ → Γ ∖ i ⊢⋆ Ξ
[_≔_]⋆_ {∅}     i s ∙        = ∙
[_≔_]⋆_ {Ξ , B} i s (ts , t) = [ i ≔ s ]⋆ ts , [ i ≔ s ] t

-- Convertibility.

data _⋙_ {Γ : Cx Ty} : ∀ {A} → Γ ⊢ A → Γ ⊢ A → Set where
  refl⋙        : ∀ {A} → {t : Γ ⊢ A}
                        → t ⋙ t

  trans⋙       : ∀ {A} → {t t′ t″ : Γ ⊢ A}
                        → t ⋙ t′ → t′ ⋙ t″
                        → t ⋙ t″

  sym⋙         : ∀ {A} → {t t′ : Γ ⊢ A}
                        → t ⋙ t′
                        → t′ ⋙ t

  conglam⋙     : ∀ {A B} → {t t′ : Γ , A ⊢ B}
                          → t ⋙ t′
                          → lam t ⋙ lam t′

  congapp⋙     : ∀ {A B} → {t t′ : Γ ⊢ A ▻ B} → {u u′ : Γ ⊢ A}
                          → t ⋙ t′ → u ⋙ u′
                          → app t u ⋙ app t′ u′

  congpair⋙    : ∀ {A B} → {t t′ : Γ ⊢ A} → {u u′ : Γ ⊢ B}
                          → t ⋙ t′ → u ⋙ u′
                          → pair t u ⋙ pair t′ u′

  congfst⋙     : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                          → t ⋙ t′
                          → fst t ⋙ fst t′

  congsnd⋙     : ∀ {A B} → {t t′ : Γ ⊢ A ∧ B}
                          → t ⋙ t′
                          → snd t ⋙ snd t′

  congsuc⋙     : ∀ {t t′ : Γ ⊢ NAT} → t ⋙ t′
                                      → suc t ⋙ suc t′

  congif⋙      : ∀ {C} → {t t′ : Γ ⊢ BOOL} → {u u′ : Γ ⊢ C} → {v v′ : Γ ⊢ C}
                        → t ⋙ t′
                        → if t u v ⋙ if t′ u′ v′

  congit⋙      : ∀ {C} → {t t′ : Γ ⊢ NAT} → {u u′ : Γ ⊢ C ▻ C} → {v v′ : Γ ⊢ C}
                        → t ⋙ t′
                        → it t u v ⋙ it t′ u′ v′

  congrec⋙     : ∀ {C} → {t t′ : Γ ⊢ NAT} → {u u′ : Γ ⊢ NAT ▻ C ▻ C} → {v v′ : Γ ⊢ C}
                        → t ⋙ t′
                        → rec t u v ⋙ rec t′ u′ v′

  beta▻⋙       : ∀ {A B} → {t : Γ , A ⊢ B} → {u : Γ ⊢ A}
                          → app (lam t) u ⋙ ([ top ≔ u ] t)

  eta▻⋙        : ∀ {A B} → {t : Γ ⊢ A ▻ B}
                          → t ⋙ lam (app (mono⊢ weak⊆ t) v₀)

  beta∧₁⋙      : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                          → fst (pair t u) ⋙ t

  beta∧₂⋙      : ∀ {A B} → {t : Γ ⊢ A} → {u : Γ ⊢ B}
                          → snd (pair t u) ⋙ u

  eta∧⋙        : ∀ {A B} → {t : Γ ⊢ A ∧ B}
                          → t ⋙ pair (fst t) (snd t)

  eta⊤⋙       : ∀ {t : Γ ⊢ ⊤} → t ⋙ unit

  betaBOOL₁⋙   : ∀ {C} → {u v : Γ ⊢ C}
                        → if true u v ⋙ u

  betaBOOL₂⋙   : ∀ {C} → {u v : Γ ⊢ C}
                        → if false u v ⋙ v

  betaNATit₁⋙  : ∀ {C} → {u : Γ ⊢ C ▻ C} → {v : Γ ⊢ C}
                        → it zero u v ⋙ v

  -- TODO: Verify this.
  betaNATit₂⋙  : ∀ {C} → {t : Γ ⊢ NAT} → {u : Γ ⊢ C ▻ C} → {v : Γ ⊢ C}
                        → it (suc t) u v ⋙ app u (it t u v)

  betaNATrec₁⋙ : ∀ {C} → {u : Γ ⊢ NAT ▻ C ▻ C} → {v : Γ ⊢ C}
                        → rec zero u v ⋙ v

  -- TODO: Verify this.
  betaNATrec₂⋙ : ∀ {C} → {t : Γ ⊢ NAT} → {u : Γ ⊢ NAT ▻ C ▻ C} → {v : Γ ⊢ C}
                        → rec (suc t) u v ⋙ app (app u t) (rec t u v)

  -- TODO: What about eta for BOOL and NAT?


text:
-- Andreas, 2015-05-01
-- With clauses for functions with flexible arity.

-- {-# OPTIONS -v tc.with:40 #-}

open import Common.Prelude
open import Common.Equality

mutual
  even : Nat → Bool
  even 0       = true
  even (suc n) = odd n

  odd  : Nat → Bool
  odd 0 = false
  odd (suc n) = even n

NPred : Nat → Set
NPred 0       = Bool
NPred (suc n) = Nat → NPred n

const : Bool → ∀{n} → NPred n
const b {0}       = b
const b {suc n} m = const b {n}

allOdd : ∀ n → NPred n
allOdd 0 = true
allOdd (suc n) m with even m
... | true  = const false
... | false = allOdd n

test : allOdd 4 1 3 5 7 ≡ true
test = refl


text:
module par-swap.dpg where

open import par-swap
open import par-swap.properties
open import par-swap.confluent
open import par-swap.dpg-pot
open import par-swap.dpg-e-view
open import noetherian using (noetherian ; ∥_∥s)
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.Binding
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Bool
open import Data.Empty
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Data.Sum
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; subst ; cong ; trans ;
         module ≡-Reasoning ; cong₂ ; subst₂ ; inspect)
open import sn-calculus
open import context-properties -- get view, E-views

DPG₁ : ∀ {p q r} ->
   (p ∥ q) sn⟶₁ r ->
   ∃ \ {(d , d₁) -> (q ∥ p) sn⟶ d₁ × d₁ sn⟶* d × r ∥R* d}
DPG₁{p} {q} {r} (rpar-done-right haltedp doneq) =
    (r , r) ,
    fixup-valuemax₁ doneq haltedp (rcontext [] dchole (rpar-done-left doneq haltedp)) ,
    rrefl , ∥R0 where
 fixup-valuemax₁ : ∀ {p q}  ->
   (doneq : done q) ->
   (haltedp : halted p) ->
   q ∥ p sn⟶ value-max doneq (dhalted haltedp) (inj₂ haltedp) ->
   q ∥ p sn⟶ value-max (dhalted haltedp) doneq (inj₁ haltedp)
 fixup-valuemax₁ donep haltedq rewrite value-max-sym donep haltedq = λ z → z

DPG₁{p}{q}{r} (rpar-done-left donep haltedq) =
    (r , r) ,
    fixup-valuemax₂ donep haltedq (rcontext [] dchole (rpar-done-right haltedq donep)) ,
    rrefl , ∥R0 where
 fixup-valuemax₂ : ∀ {p q} ->
  (donep : done p) ->
  (haltedq : halted q) ->
  q ∥ p sn⟶ value-max (dhalted haltedq) donep (inj₁ haltedq) ->
  q ∥ p sn⟶ value-max donep (dhalted haltedq) (inj₂ haltedq)
 fixup-valuemax₂ donep haltedq rewrite sym (value-max-sym donep haltedq) = λ z → z

par-not-halted : ∀ {p C q₁ q₂} -> halted p -> p ≐ C ⟦ q₁ ∥ q₂ ⟧c -> ⊥
par-not-halted hnothin ()
par-not-halted (hexit n) ()

swap-paused-is-paused :
  ∀ {p C q₁ q₂} ->
    paused p ->
    p ≐ C ⟦ q₁ ∥ q₂ ⟧c ->
    paused (C ⟦ q₂ ∥ q₁ ⟧c)
swap-paused-is-paused ppause ()
swap-paused-is-paused (pseq pausedp) (dcseq₁ dc)
 = pseq (swap-paused-is-paused pausedp dc)
swap-paused-is-paused (pseq pausedp) (dcseq₂ dc)
 = pseq pausedp
swap-paused-is-paused (ploopˢ pausedp) (dcloopˢ₁ dc)
 = ploopˢ (swap-paused-is-paused pausedp dc)
swap-paused-is-paused (ploopˢ pausedp) (dcloopˢ₂ dc)
 = ploopˢ pausedp
swap-paused-is-paused (ppar pausedp pausedp₁) dchole
 = ppar pausedp₁ pausedp
swap-paused-is-paused (ppar pausedp pausedp₁) (dcpar₁ dc)
 = ppar (swap-paused-is-paused pausedp dc) pausedp₁
swap-paused-is-paused (ppar pausedp pausedp₁) (dcpar₂ dc)
 = ppar pausedp (swap-paused-is-paused pausedp₁ dc)
swap-paused-is-paused (psuspend pausedp) (dcsuspend dc)
 = psuspend (swap-paused-is-paused pausedp dc)
swap-paused-is-paused (ptrap pausedp) (dctrap dc)
 = ptrap (swap-paused-is-paused pausedp dc)

DPG : ∀ {a b c} ->
      a ∥R b ->
      a sn⟶ c ->
      Σ (Term × Term) λ {(d , d₁) -> b sn⟶ d₁ × d₁ sn⟶* d × c ∥R* d}

DPG (∥Rstep dchole) (rcontext _ dchole psn⟶₁p')
  = DPG₁ psn⟶₁p'

DPG (∥Rstep dchole) (rcontext _ (dcpar₁ dcsn⟶) psn⟶₁p')
  =  _ ,  rcontext _ (dcpar₂ dcsn⟶) psn⟶₁p'  , rrefl , ∥Rn (∥Rstep dchole) ∥R0

DPG (∥Rstep dchole) (rcontext _ (dcpar₂ dcsn⟶) psn⟶₁p')
  = _ ,  rcontext _ (dcpar₁ dcsn⟶) psn⟶₁p'  , rrefl , ∥Rn (∥Rstep dchole) ∥R0

DPG (∥Rstep (dcpar₁ dc∥R)) (rcontext .[] dchole (rpar-done-right haltedp doneq))
 = ⊥-elim (par-not-halted haltedp dc∥R)

DPG (∥Rstep (dcpar₁ dc∥R)) (rcontext .[] dchole (rpar-done-left (dhalted p/halted) haltedq))
  = ⊥-elim (par-not-halted p/halted dc∥R)

DPG (∥Rstep (dcpar₁ dc∥R)) (rcontext .[] dchole (rpar-done-left (dpaused p/paused) hnothin))
  = _ ,
    rcontext [] dchole (rpar-done-left (dpaused (swap-paused-is-paused p/paused dc∥R)) hnothin) ,
    rrefl ,
    ∥Rn (∥Rstep dc∥R) ∥R0

DPG (∥Rstep (dcpar₁ dc∥R)) (rcontext .[] dchole (rpar-done-left (dpaused p/paused) (hexit n)))
  = _ ,
    rcontext [] dchole (rpar-done-left (dpaused (swap-paused-is-paused p/paused dc∥R)) (hexit n)) ,
    rrefl ,
    ∥R0

DPG (∥Rstep (dcpar₁ dc∥R)) (rcontext (ceval (epar₁ _) ∷ C) (dcpar₁ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ (ceval (epar₁ _)) sn⟶step ,
   Context1-sn⟶* (ceval (epar₁ _)) sn⟶*step ,
   Context1-∥R* (ceval (epar₁ _)) ∥R*step

DPG (∥Rstep (dcpar₁ dc∥R)) (rcontext _ (dcpar₂ dcsn⟶) psn⟶₁p')
 = _ ,
  rcontext _ (dcpar₂ dcsn⟶) psn⟶₁p' ,
  rrefl ,
  ∥Rn (∥Rstep (dcpar₁ dc∥R)) ∥R0

DPG (∥Rstep (dcpar₂ dc∥R)) (rcontext .[] dchole (rpar-done-right haltedp (dhalted p/halted)))
 = ⊥-elim (par-not-halted p/halted dc∥R)

DPG (∥Rstep (dcpar₂ dc∥R)) (rcontext .[] dchole (rpar-done-right hnothin (dpaused p/paused)))
 = _ ,
   rcontext [] dchole (rpar-done-right hnothin (dpaused (swap-paused-is-paused p/paused dc∥R))) ,
   rrefl ,
   ∥Rn (∥Rstep dc∥R) ∥R0

DPG (∥Rstep (dcpar₂ dc∥R)) (rcontext .[] dchole (rpar-done-right (hexit n) (dpaused p/paused)))
 =  _ ,
    rcontext [] dchole (rpar-done-right (hexit n) (dpaused (swap-paused-is-paused p/paused dc∥R))) ,
    rrefl ,
    ∥R0

DPG (∥Rstep (dcpar₂ dc∥R)) (rcontext .[] dchole (rpar-done-left donep haltedq))
 = ⊥-elim (par-not-halted haltedq dc∥R)

DPG (∥Rstep (dcpar₂ dc∥R)) (rcontext _ (dcpar₁ dcsn⟶) psn⟶₁p')
 = _ ,
   (rcontext _ (dcpar₁ dcsn⟶) psn⟶₁p') ,
   rrefl ,
   ∥Rn (∥Rstep (dcpar₂ dc∥R)) ∥R0

DPG (∥Rstep (dcpar₂ dc∥R)) (rcontext (c ∷ C) (dcpar₂ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcseq₁ ())) (rcontext .[] dchole rseq-done)

DPG (∥Rstep (dcseq₁ ())) (rcontext .[] dchole rseq-exit)

DPG (∥Rstep (dcseq₁ dc∥R)) (rcontext (c ∷ C) (dcseq₁ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcseq₁ dc∥R)) (rcontext _ (dcseq₂ dcsn⟶) psn⟶₁p')
 = _ ,
   rcontext _ (dcseq₂ dcsn⟶) psn⟶₁p' ,
   rrefl ,
   ∥Rn (∥Rstep (dcseq₁ dc∥R)) ∥R0

DPG (∥Rstep (dcseq₂ dc∥R)) (rcontext .[] dchole rseq-done)
 = _ , rcontext [] dchole rseq-done , rrefl , ∥Rn (∥Rstep dc∥R) ∥R0

DPG (∥Rstep (dcseq₂ dc∥R)) (rcontext .[] dchole rseq-exit)
 = _ , rcontext [] dchole rseq-exit , rrefl , ∥R0

DPG (∥Rstep (dcseq₂ dc∥R)) (rcontext _ (dcseq₁ dcsn⟶) psn⟶₁p')
 = _ ,
   rcontext _ (dcseq₁ dcsn⟶) psn⟶₁p' ,
   rrefl ,
   ∥Rn (∥Rstep (dcseq₂ dc∥R)) ∥R0

DPG (∥Rstep (dcseq₂ dc∥R)) (rcontext (c ∷ C) (dcseq₂ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcsuspend dc∥R)) (rcontext .[] dchole (rsuspend-done haltedp))
  = ⊥-elim (par-not-halted haltedp dc∥R)

DPG (∥Rstep (dcsuspend dc∥R)) (rcontext (c ∷ C) (dcsuspend dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dctrap dc∥R)) (rcontext .[] dchole (rtrap-done haltedp))
  = ⊥-elim (par-not-halted haltedp dc∥R)

DPG (∥Rstep (dctrap dc∥R)) (rcontext (c ∷ C) (dctrap dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcsignl dc∥R)) (rcontext .[] dchole rraise-signal)
 = _ ,
   (rcontext [] dchole rraise-signal) ,
   rrefl ,
   (∥Rn (∥Rstep (dcenv dc∥R)) ∥R0)

DPG (∥Rstep (dcsignl dc∥R)) (rcontext (c ∷ C) (dcsignl dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcpresent₁ dc∥R)) (rcontext .[] dchole ())

DPG (∥Rstep (dcpresent₁ dc∥R)) (rcontext (c ∷ C) (dcpresent₁ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcpresent₁ dc∥R)) (rcontext _ (dcpresent₂ dcsn⟶) psn⟶₁p')
  = _ ,
    rcontext _ (dcpresent₂ dcsn⟶) psn⟶₁p' ,
    rrefl ,
    ∥Rn (∥Rstep (dcpresent₁ dc∥R)) ∥R0

DPG (∥Rstep (dcpresent₂ dc∥R)) (rcontext .[] dchole ())

DPG (∥Rstep (dcpresent₂ dc∥R)) (rcontext _ (dcpresent₁ dcsn⟶) psn⟶₁p')
  = _ ,
    rcontext _ (dcpresent₁ dcsn⟶) psn⟶₁p' ,
    rrefl ,
    ∥Rn (∥Rstep (dcpresent₂ dc∥R)) ∥R0

DPG (∥Rstep (dcpresent₂ dc∥R)) (rcontext (c ∷ C) (dcpresent₂ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcloop dc∥R)) (rcontext .[] dchole rloop-unroll)
 = _ ,
   (rcontext [] dchole rloop-unroll) ,
   rrefl ,
   ∥Rn (∥Rstep (dcloopˢ₁ dc∥R)) (∥Rn (∥Rstep (dcloopˢ₂ dc∥R)) ∥R0)

DPG (∥Rstep (dcloop dc∥R)) (rcontext (c ∷ C) (dcloop dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcloopˢ₁ ())) (rcontext .[] dchole rloopˢ-exit)

DPG (∥Rstep (dcloopˢ₁ dc∥R)) (rcontext (c ∷ C) (dcloopˢ₁ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcloopˢ₁ dc∥R)) (rcontext _ (dcloopˢ₂ dcsn⟶) psn⟶₁p')
 = _ ,
   rcontext _ (dcloopˢ₂ dcsn⟶) psn⟶₁p' ,
   rrefl ,
   ∥Rn (∥Rstep (dcloopˢ₁ dc∥R)) ∥R0

DPG (∥Rstep (dcloopˢ₂ dc∥R)) (rcontext .[] dchole rloopˢ-exit)
 = _ ,
   (rcontext [] dchole rloopˢ-exit) ,
   rrefl ,
   ∥R0

DPG (∥Rstep (dcloopˢ₂ dc∥R)) (rcontext _ (dcloopˢ₁ dcsn⟶) psn⟶₁p')
 = _ ,
   rcontext _ (dcloopˢ₁ dcsn⟶) psn⟶₁p' ,
   rrefl ,
   ∥Rn (∥Rstep (dcloopˢ₂ dc∥R)) ∥R0

DPG (∥Rstep (dcloopˢ₂ dc∥R)) (rcontext (c ∷ C) (dcloopˢ₂ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcshared dc∥R)) (rcontext .[] dchole ())

DPG (∥Rstep (dcshared dc∥R)) (rcontext (c ∷ C) (dcshared dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcvar dc∥R)) (rcontext .[] dchole ())

DPG (∥Rstep (dcvar dc∥R)) (rcontext (c ∷ C) (dcvar dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcif₁ dc∥R)) (rcontext .[] dchole ())

DPG (∥Rstep (dcif₁ dc∥R)) (rcontext (c ∷ C) (dcif₁ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcif₁ dc∥R)) (rcontext _ (dcif₂ dcsn⟶) psn⟶₁p')
 = _ ,
   rcontext _ (dcif₂ dcsn⟶) psn⟶₁p' ,
   rrefl ,
   ∥Rn (∥Rstep (dcif₁ dc∥R)) ∥R0

DPG (∥Rstep (dcif₂ dc∥R)) (rcontext .[] dchole ())

DPG (∥Rstep (dcif₂ dc∥R)) (rcontext _ (dcif₁ dcsn⟶) psn⟶₁p')
 = _ ,
   rcontext _ (dcif₁ dcsn⟶) psn⟶₁p' ,
   rrefl ,
   ∥Rn (∥Rstep (dcif₂ dc∥R)) ∥R0

DPG (∥Rstep (dcif₂ dc∥R)) (rcontext (c ∷ C) (dcif₂ dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

DPG (∥Rstep (dcenv dc∥R)) (rcontext{p' = p'} .[] dchole psn⟶₁p')
  with ρ-stays-ρ-sn⟶₁ psn⟶₁p'
... | θ' , q , A' , refl
  with get-view psn⟶₁p'
... | inj₂ (eq , eq2 , pot-view) = DPG-pot-view dc∥R psn⟶₁p' eq eq2 pot-view
... | inj₁ (E , pin , qin , peq , qeq , E-view) with
   DPG-E-view peq qeq dc∥R psn⟶₁p' E-view
... | (d , sn⟶step , ∥R*-step , _ )
  = _ ,
    rcontext [] dchole sn⟶step ,
    rrefl ,
    Context1-∥R* (cenv θ' _) ∥R*-step

DPG (∥Rstep (dcenv dc∥R)) (rcontext (c ∷ C) (dcenv dcsn⟶) psn⟶₁p')
 with DPG (∥Rstep dc∥R) (rcontext C dcsn⟶ psn⟶₁p')
... | _ , sn⟶step , sn⟶*step , ∥R*step
 = _ ,
   Context1-sn⟶ c sn⟶step ,
   Context1-sn⟶* c sn⟶*step ,
   Context1-∥R* c ∥R*step

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module UnSizedIO.Console where

open import NativeIO
open import UnSizedIO.Base hiding (main)

data ConsoleCommand : Set where
  putStrLn : String → ConsoleCommand
  getLine  : ConsoleCommand

ConsoleResponse : ConsoleCommand → Set
ConsoleResponse (putStrLn s) = Unit
ConsoleResponse  getLine     = String

ConsoleInterface : IOInterface
Command  ConsoleInterface = ConsoleCommand
Response ConsoleInterface = ConsoleResponse

IOConsole : Set → Set
IOConsole = IO ConsoleInterface

IOConsole+ : Set → Set
IOConsole+ = IO+ ConsoleInterface

translateIOConsoleLocal : (c : ConsoleCommand) → NativeIO (ConsoleResponse c)
translateIOConsoleLocal (putStrLn s) = nativePutStrLn s
translateIOConsoleLocal getLine      = nativeGetLine

translateIOConsole : {A : Set} → IOConsole A → NativeIO A
translateIOConsole = translateIO translateIOConsoleLocal

main : NativeIO Unit
main = nativePutStrLn "Console"

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Base.Free.Instance.Maybe.Properties where

open import Relation.Binary.PropositionalEquality using (refl; cong)

open import Base.Free                             using (Free; pure; impure; _>>=_)
open import Base.Free.Instance.Maybe              using (Just; Nothing)             renaming (Maybe to MaybeF)

open import Base.Isomorphism                      using (_≃_)
open        _≃_
open import Base.Extensionality                   using (ext)

open import Data.Unit                             using (tt)
import      Relation.Binary.PropositionalEquality as Eq
open        Eq                                    using (_≡_; refl; cong)

-- The usual `Maybe` monad representation an the free version are isomorphic.
data Maybe (A : Set) : Set where
  just : A → Maybe A
  nothing : Maybe A

Maybe≃MaybeF : ∀ {A} → Maybe A ≃ MaybeF A
to Maybe≃MaybeF (just x) = Just x
to Maybe≃MaybeF nothing  = Nothing
from Maybe≃MaybeF (pure x)      = just x
from Maybe≃MaybeF (impure tt _) = nothing
from∘to Maybe≃MaybeF (just x) = refl
from∘to Maybe≃MaybeF nothing  = refl
to∘from Maybe≃MaybeF (pure x)      = refl
to∘from Maybe≃MaybeF (impure tt x) = cong (impure tt) (ext λ())

Nothing>>=k≡Nothing : ∀ {A B} → (k : A → MaybeF B) → (Nothing >>= k) ≡ Nothing
Nothing>>=k≡Nothing k = cong (impure tt) (ext  (λ ()))

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Empty
open import Data.Product
open import Data.List using ([]; _∷_; _∷ʳ_)

open import Relation.Unary using (_∈_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Relation.Binary.HeterogeneousEquality as Het

open import Common

module Transitions {ℙ : Set} (message : Message ℙ)
  where

open import SessionType message
open import Trace message

data Transition : SessionType -> Action -> SessionType -> Set where
  inp : ∀{f x}                 -> Transition (inp f) (I x) (f x .force)
  out : ∀{f x} (!x : x ∈ dom f) -> Transition (out f) (O x) (f x .force)

data Transitions : SessionType -> Trace -> SessionType -> Set where
  refl : ∀{T} -> Transitions T [] T
  step : ∀{T α T' φ T''} (t : Transition T α T') (tr : Transitions T' φ T'') -> Transitions T (α ∷ φ) T''

transition->defined : ∀{T a S} -> Transition T a S -> Defined T
transition->defined inp     = inp
transition->defined (out _) = out

output-transition->defined : ∀{T x S} -> Transition T (O x) S -> Defined S
output-transition->defined (out !x) = !x

output-transitions->defined : ∀{T φ x S} -> Transitions T (φ ∷ʳ O x) S -> Defined S
output-transitions->defined {_} {[]} (step (out fx) refl) = fx
output-transitions->defined {_} {_ ∷ _} (step _ tr) = output-transitions->defined tr

unsnoc-transitions : ∀{T φ α S} -> Transitions T (φ ∷ʳ α) S -> ∃[ R ] (Transitions T φ R × Transition R α S)
unsnoc-transitions {_} {[]} (step t refl) = _ , refl , t
unsnoc-transitions {_} {x ∷ φ} (step t tr) with unsnoc-transitions tr
... | _ , sr , s = _ , step t sr , s

transitions+defined->defined : ∀{T as S} -> Transitions T as S -> Defined S -> Defined T
transitions+defined->defined refl def = def
transitions+defined->defined (step t _) _ = transition->defined t

transitions-eq : ∀{T T' T'' φ} (tr : Transitions T φ T') (sr : Transitions T φ T'') ->
  T' ≡ T'' × tr Het.≅ sr
transitions-eq refl refl = refl , Het.refl
transitions-eq (step inp tr) (step inp sr) with transitions-eq tr sr
... | refl , Het.refl = refl , Het.refl
transitions-eq (step (out fx) tr) (step (out gx) sr) with Defined-eq fx gx | transitions-eq tr sr
... | refl | refl , Het.refl = refl , Het.refl

win-reduces-⊥ : ∀{S S' α} → Win S → Transition S α S' → ⊥
win-reduces-⊥ (out e) (out !x) = e _ !x

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
{-# OPTIONS --sized-types --show-implicit #-}

module WrongSizeAssignment where

postulate
  Size : Set
  _^   : Size -> Size
  ∞    : Size

{-# BUILTIN SIZE Size  #-}
{-# BUILTIN SIZESUC _^ #-}
{-# BUILTIN SIZEINF ∞  #-}

data Empty : Set where

data N : {_ : Size} -> Set where
  zero : N {∞}
  suc  : forall {i} -> N {i ^} -> N {i}

lift : forall {i} -> N {i} -> N {i ^}
lift zero    = zero
lift (suc x) = suc (lift x)

f : forall {i} -> N {i ^} -> Empty
f x = f (suc (lift x))


text:
{-# OPTIONS --cubical --no-import-sorts  #-}

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Function.Base using (_∋_; _$_)
import Cubical.Algebra.Monoid as Std
open import MorePropAlgebra.Bundles

module MorePropAlgebra.Properties.Monoid {ℓ} (assumptions : Monoid {ℓ}) where
open Monoid assumptions renaming (Carrier to F)

import MorePropAlgebra.Properties.Semigroup
module Semigroup'Properties = MorePropAlgebra.Properties.Semigroup   (record { Monoid assumptions })
module Semigroup'           =                            Semigroup   (record { Monoid assumptions })
(      Semigroup')          =                            Semigroup ∋ (record { Monoid assumptions })

stdIsMonoid : Std.IsMonoid ε _·_
stdIsMonoid  .Std.IsMonoid.isSemigroup = Semigroup'Properties.stdIsSemigroup
stdIsMonoid  .Std.IsMonoid.identity    = is-identity

stdMonoid : Std.Monoid {ℓ}
stdMonoid = record { Monoid assumptions ; isMonoid = stdIsMonoid }

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module _ (C Dummy : Set) where

data Maybe : Set where
  nothing : Maybe

IfJust : Maybe → Set → Set
IfJust nothing P = P

postulate
  qCtx     : C
  inferRes : Maybe

                             -- v-- Implicit is important here
inferResBest : IfJust inferRes ({G : Maybe} → C)
inferResBest with inferRes
inferResBest | nothing = qCtx    -- Error: Dummy != C when checking qCtx : C

-- Test also with an existing implicit argument
inferResBest₁ : {A : Set} → IfJust inferRes ({G : Maybe} → C)
inferResBest₁ with inferRes
inferResBest₁ | nothing = qCtx    -- Error: Dummy != C when checking qCtx : C

-- Make sure it does break down on underapplied clauses
underapplied : Maybe → C
underapplied with inferRes
underapplied | nothing = λ _ → qCtx


text:
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --no-double-check #-}

-- {-# OPTIONS -v impossible:70 #-}
-- {-# OPTIONS -v tc.interaction:30 #-}
-- {-# OPTIONS -v tc.check.internal:20 #-}

open import Agda.Builtin.Sigma

record R1 (A : Set) : Set where

instance
  prodR1 : {A : Set} {B : A → Set} → ⦃ {a : A} → R1 (B a) ⦄ → R1 (Σ A B)
  prodR1 = record {}

record R2 (A : Set) ⦃ aR1 : R1 A ⦄ : Set₁ where
  field
    f : A → Set
open R2 ⦃...⦄ public

record R3 (A : Set) (B : A → Set) : Set₁ where
  instance
    bR1 : {a : A} → R1 (B a)
    bR1 = {!!} -- record {}
  field
    ⦃ r2 ⦄ : R2 (Σ A B)
    fab : ∀ {a} {b : B a} → f (a , b)