text:
module container.w.core where

open import level
open import sum
open import equality
open import function.extensionality
open import function.isomorphism
open import function.isomorphism.properties
open import function.overloading
open import sets.empty
open import sets.nat.core using (suc)
open import sets.unit
open import hott.level
open import container.core
open import container.fixpoint
open import container.equality

private
  module Definition {li la lb} (c : Container li la lb) where
    open Container c

    -- definition of indexed W-types using a type family
    data W (i : I) : Set (la ⊔ lb) where
      sup : (a : A i) → ((b : B a) → W (r b)) → W i

    -- initial F-algebra
    inW : F W →ⁱ W
    inW i (a , f) = sup a f

    module Elim {lx} {X : I → Set lx}
                (α : F X →ⁱ X) where
      -- catamorphisms
      fold : W →ⁱ X
      fold i (sup a f) = α i (a , λ b → fold _ (f b))

      -- computational rule for catamorphisms
      -- this holds definitionally
      fold-β : ∀ {i} (x : F W i) → fold i (inW i x) ≡ α i (imap fold i x)
      fold-β x = refl

      -- η-rule, this is only propositional
      fold-η : (h : W →ⁱ X)
             → (∀ {i} (x : F W i) → h i (inW i x) ≡ α i (imap h i x))
             → ∀ {i} (x : W i) → h i x ≡ fold i x
      fold-η h p {i} (sup a f) = p (a , λ b → f b) · lem
        where
          lem : α i (a , (λ b → h _ (f b)))
              ≡ α i (a , (λ b → fold _ (f b)))
          lem = ap (λ z → α i (a , z))
                     (funext λ b → fold-η h p (f b))
    open Elim public

    head : ∀ {i} → W i → A i
    head (sup a f) = a

    tail : ∀ {i} (x : W i)(b : B (head x)) → W (r b)
    tail (sup a f) = f

    fixpoint : (i : I) → W i ≅ F W i
    fixpoint _ = iso f g H K
      where
        f : {i : I} → W i → F W i
        f (sup a f) = a , f

        g : {i : I} → F W i → W i
        g (a , f) = sup a f

        H : {i : I}(w : W i) → g (f w) ≡ w
        H (sup a f) = refl

        K : {i : I}(w : F W i) → f (g w) ≡ w
        K (a , f) = refl

private
  module Properties {li la lb}{c : Container li la lb} where
    open Container c
    open Definition c

    open Equality c (fix W fixpoint)
    open Container equality
      using ()
      renaming (F to F-≡')
    open Definition equality
      using ()
      renaming ( W to W-≡
               ; fixpoint to fixpoint-≡ )

    F-≡ : ∀ {lx}
        → (∀ {i} → W i → W i → Set lx)
        → (∀ {i} → W i → W i → Set _)
    F-≡ X  u v = F-≡' (λ {(i , u , v) → X {i} u v}) (_ , u , v)

    _≡W_ : ∀ {i} → W i → W i → Set _
    _≡W_ {i} u v = W-≡ (i , u , v)

    fixpoint-W : ∀ {i}{u v : W i} → (u ≡ v) ≅ F-≡ _≡_ u v
    fixpoint-W {i}{sup a f}{sup a' f'} = begin
        (sup a f ≡ sup a' f')
      ≅⟨ iso≡ (fixpoint i) ⟩
        (apply (fixpoint i) (sup a f) ≡ apply (fixpoint i) (sup a' f'))
      ≅⟨ sym≅ Σ-split-iso ⟩
        (Σ (a ≡ a') λ p → subst (λ a → (b : B a) → W (r b)) p f ≡ f')
      ≅⟨ Σ-ap-iso refl≅ (substX-β f f') ⟩
        (Σ (a ≡ a') λ p → ∀ b → f b ≡ substX p b (f' (subst B p b)))
      ∎
      where open ≅-Reasoning

    str-iso : ∀ {i}{u v : W i} → (u ≡ v) ≅ (u ≡W v)
    str-iso {i}{sup a f}{sup a' f'} = begin
        (sup a f ≡ sup a' f')
      ≅⟨ fixpoint-W ⟩
        (Σ (a ≡ a') λ p → ∀ b → f b ≡ substX p b (f' (subst B p b)))
      ≅⟨ Σ-ap-iso refl≅ (λ a → Π-ap-iso refl≅ λ b → str-iso) ⟩
        (Σ (a ≡ a') λ p → ∀ b → f b ≡W substX p b (f' (subst B p b)))
      ≅⟨ sym≅ (fixpoint-≡ _) ⟩
        (sup a f ≡W sup a' f')
      ∎
      where open ≅-Reasoning

--    w-level : ∀ {n} → ((i : I) → h (suc n) (A i)) → (i : I) → h (suc n) (W i)
--    w-level hA i (sup a f) (sup a' f') = iso-level (sym≅ lem)
--      (Σ-level (hA i a a') (λ p → Π-level λ b → w-level hA _ _ _))
--      where
--        lem : ∀ {i}{a a' : A i}
--              {f : (b : B a) → W (r b)}
--              {f' : (b : B a') → W (r b)}
--            → (sup a f ≡ sup a' f')
--            ≅ Σ (a ≡ a') λ p → ∀ b → f b ≡ substX p b (f' (subst B p b))
--        lem = fixpoint-W

open Definition public
-- open Properties public using (w-level)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


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

-- This module defines D<: normal form, proves its transitivity and shows its
-- equivalence to the original D<:. It turns out that D<: normal form can be used to
-- prove undecidability.
module DsubEquivSimpler where

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

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

open import Induction.Nat

open import DsubDef
open import Dsub
open import Utils

-- D<: Normal Form
--
-- The following judgment defines D<: normal form as in Figure 4.
infix 4 _⊢″_<:_
data _⊢″_<:_ : Env → Typ → Typ → Set where
  <:⊤  : ∀ {Γ T} → Γ ⊢″ T <: ⊤
  ⊥<:  : ∀ {Γ T} → Γ ⊢″ ⊥ <: T
  refl : ∀ {Γ T} → Γ ⊢″ T <: T
  bnd  : ∀ {Γ S U S′ U′} →
           Γ ⊢″ S′ <: S →
           Γ ⊢″ U <: U′ →
           Γ ⊢″ ⟨A: S ⋯ U ⟩ <: ⟨A: S′ ⋯ U′ ⟩
  Π<:  : ∀ {Γ S U S′ U′} →
           Γ ⊢″ S′ <: S →
           Γ ‣ S′ ! ⊢″ U <: U′ →
           Γ ⊢″ Π S ∙ U <: Π S′ ∙ U′
  sel₁ : ∀ {Γ n T S} →
           env-lookup Γ n ≡ just T →
           Γ ⊢″ T <: ⟨A: S ⋯ ⊤ ⟩ →
           Γ ⊢″ S <: n ∙A
  sel₂ : ∀ {Γ n T U} →
           env-lookup Γ n ≡ just T →
           Γ ⊢″ T <: ⟨A: ⊥ ⋯ U ⟩ →
           Γ ⊢″ n ∙A <: U
  <:>  : ∀ {Γ n T S U} →
           env-lookup Γ n ≡ just T →
           Γ ⊢″ T <: ⟨A: S ⋯ ⊤ ⟩ →
           Γ ⊢″ T <: ⟨A: ⊥ ⋯ U ⟩ →
           Γ ⊢″ S <: U

-- First we show that D<: normal form admits weakening.
<:″-weakening-gen : ∀ {Γ S U} →
                      Γ ⊢″ S <: U →
                    ∀ Γ₁ Γ₂ T →
                      Γ ≡ Γ₁ ‣ Γ₂ →
                      Γ₁ ‣ T ! ‣ Γ₂ ⇑ ⊢″ S ↑ length Γ₂ <: U ↑ length Γ₂
<:″-weakening-gen <:⊤ Γ₁ Γ₂ T eqΓ               = <:⊤
<:″-weakening-gen ⊥<: Γ₁ Γ₂ T eqΓ               = ⊥<:
<:″-weakening-gen refl Γ₁ Γ₂ T eqΓ              = refl
<:″-weakening-gen (bnd S′<:S U<:U′) Γ₁ Γ₂ T eqΓ = bnd (<:″-weakening-gen S′<:S Γ₁ Γ₂ T eqΓ)
                                                      (<:″-weakening-gen U<:U′ Γ₁ Γ₂ T eqΓ)
<:″-weakening-gen (Π<: S′<:S U<:U′) Γ₁ Γ₂ T eqΓ = Π<: (<:″-weakening-gen S′<:S Γ₁ Γ₂ T eqΓ)
                                                      (<:″-weakening-gen U<:U′ Γ₁ (_ ∷ Γ₂) T (cong (_ ∷_) eqΓ))
<:″-weakening-gen (sel₁ {_} {n} T∈Γ T<:B) Γ₁ Γ₂ T eqΓ
  rewrite ↑-var n (length Γ₂)                   = sel₁ (↦∈-weaken′ T∈Γ Γ₁ Γ₂ T eqΓ)
                                                       (<:″-weakening-gen T<:B Γ₁ Γ₂ T eqΓ)
<:″-weakening-gen (sel₂ {_} {n} T∈Γ T<:B) Γ₁ Γ₂ T eqΓ
  rewrite ↑-var n (length Γ₂)                   = sel₂ (↦∈-weaken′ T∈Γ Γ₁ Γ₂ T eqΓ)
                                                       (<:″-weakening-gen T<:B Γ₁ Γ₂ T eqΓ)
<:″-weakening-gen (<:> {_} {n} T∈Γ T<:B T<:B′) Γ₁ Γ₂ T eqΓ
  rewrite ↑-var n (length Γ₂)                   = <:> (↦∈-weaken′ T∈Γ Γ₁ Γ₂ T eqΓ)
                                                      (<:″-weakening-gen T<:B Γ₁ Γ₂ T eqΓ)
                                                      (<:″-weakening-gen T<:B′ Γ₁ Γ₂ T eqΓ)

<:″-weakening : ∀ {Γ₁ Γ₂ S U} T →
                  Γ₁ ‣ Γ₂ ⊢″ S <: U →
                  Γ₁ ‣ T ! ‣ Γ₂ ⇑ ⊢″ S ↑ length Γ₂ <: U ↑ length Γ₂
<:″-weakening T S<:U = <:″-weakening-gen S<:U _ _ T refl

<:″-weakening-hd : ∀ {Γ S U} T →
                     Γ ⊢″ S <: U →
                     Γ ‣ T ! ⊢″ S ↑ 0 <: U ↑ 0
<:″-weakening-hd T = <:″-weakening {Γ₂ = []} T

-- Then we work on transitivity.
module SimplerTransitivity where
  -- This predicate asserts that the first context replaces _one_ type in the second
  -- context with its subtype. That is, the first context is more "precise" than the
  -- second context.
  infix 4 _≺:[_]_
  data _≺:[_]_ : Env → ℕ → Env → Set where
    ≺[_,_] : ∀ {Γ U} S → Γ ⊢″ S <: U → Γ ‣ S ! ≺:[ 0 ] Γ ‣ U !
    _∷_    : ∀ {Γ₁ n Γ₂} T → Γ₁ ≺:[ n ] Γ₂ → Γ₁ ‣ T ! ≺:[ suc n ] Γ₂ ‣ T !

  <:∈-find : ∀ {x T Γ Γ′ n} →
               x ↦ T ∈ Γ →
               Γ′ ≺:[ n ] Γ →
               x ≡ n × (∃ λ T′ → n ↦ T′ ∈ Γ′ × Γ′ ⊢″ T′ <: T) ⊎ x ≢ n × x ↦ T ∈ Γ′
  <:∈-find hd ≺[ T′ , T′<:T ]           = inj₁ (refl , T′ ↑ 0 , hd , <:″-weakening-hd T′ T′<:T)
  <:∈-find hd (T ∷ Γ′≺:Γ)               = inj₂ ((λ ()) , hd)
  <:∈-find (tl T∈Γ) ≺[ T′ , T′<:T ]     = inj₂ ((λ ()) , tl T∈Γ)
  <:∈-find (tl T∈Γ) (S ∷ Γ′≺:Γ) with <:∈-find T∈Γ Γ′≺:Γ
  ... | inj₁ (x≡n , T′ , T′∈Γ′ , T′<:T) = inj₁ (cong suc x≡n , T′ ↑ 0 , tl T′∈Γ′ , <:″-weakening-hd S T′<:T)
  ... | inj₂ (x≢n , T∈Γ′)               = inj₂ (x≢n ∘ suc-injective , tl T∈Γ′)

  <:∈-find′ : ∀ {x T Γ Γ′ n} →
                env-lookup Γ x ≡ just T →
                Γ′ ≺:[ n ] Γ →
                x ≡ n × (∃ λ T′ → env-lookup Γ′ n ≡ just T′ × Γ′ ⊢″ T′ <: T) ⊎ x ≢ n × env-lookup Γ′ x ≡ just T
  <:∈-find′ T∈Γ Γ′≺Γ with <:∈-find (lookup⇒↦∈ T∈Γ) Γ′≺Γ
  ... | inj₁ (x≡n , T′ , T′∈Γ′ , T′<:T) = inj₁ (x≡n , T′ , ↦∈⇒lookup T′∈Γ′ , T′<:T)
  ... | inj₂ (x≢n , T∈Γ′)               = inj₂ (x≢n , ↦∈⇒lookup T∈Γ′)

  private
    trans-on : Typ → Set
    trans-on T = ∀ {Γ S U} → Γ ⊢″ S <: T → Γ ⊢″ T <: U → Γ ⊢″ S <: U

    narrow-on : Typ → Set
    narrow-on T = ∀ {Γ Γ′ n S U} →
                    Γ ⊢″ S <: U →
                    Γ′ ≺:[ n ] Γ →
                    env-lookup Γ n ≡ just T →
                    Γ′ ⊢″ S <: U

  -- Per Definition 11, this defines type declaration hierarchy.
  ⟨A:⟩-layer : Typ → List Typ → Typ
  ⟨A:⟩-layer T []      = T
  ⟨A:⟩-layer T (S ∷ l) = ⟨A: S ⋯ ⟨A:⟩-layer T l ⟩

  -- Now we start proving transitivity and narrowing via a mutual induction.  This
  -- mutual induction begins exactly as presented in the paper: an induction of
  -- lexicographical order of the triple (T, 𝒟₁, 𝒟₂). Notice that this is
  -- automatically handled by Agda's termination checker, which makes the problem very
  -- nice to work with.
  --
  -- If one loads this file from Emacs, one shall see that some cases below are
  -- highlighted. The reason is that those cases are not defined
  -- _definitionally_. More details can be found in:
  -- https://agda.readthedocs.io/en/v2.5.4.2/language/function-definitions.html#case-trees.
  --
  -- In fact, those non-definitional cases hides many cases away, as they expand to
  -- numerous definitional cases, which is necessarily the case in Coq. The fact that
  -- Agda's termination checking is permissive and Agda allows non-definitional cases
  -- has significantly improved productivity of showing transitivity. In Coq, this
  -- would have required significant amount of technical setup which can easily wipe
  -- away the main idea of the proof and might not be finished within a reasonable
  -- time interval.
  mutual
    <:′-trans-rec : ∀ T → (∀ T′ → Typ-measure T′ < Typ-measure T → trans-on T′ × narrow-on T′) → trans-on T
    <:′-trans-rec (n ∙A) rec (sel₁ T∈Γ T<:B) (sel₂ T′∈Γ T<:B′)
      with ≡.trans (≡.sym T∈Γ) T′∈Γ
    ... | refl                                                           = <:> T′∈Γ T<:B T<:B′
    <:′-trans-rec ⟨A: S′ ⋯ U′ ⟩ rec (bnd S′<:S U<:U′) (bnd S″<:S U′<:U″) = bnd (<:′-trans-rec S′ (λ T′ T′<S′ → rec T′ (≤-step (≤-stepsʳ _ T′<S′))) S″<:S S′<:S)
                                                                               (<:′-trans-rec U′ (λ T′ T′<U′ → rec T′ (≤-step (≤-stepsˡ _ T′<U′))) U<:U′ U′<:U″)

    <:′-trans-rec (Π S′ ∙ U′) rec (Π<: S′<:S″ U″<:U′) (Π<: S‴<:S′ U′<:U‴)
      = Π<: (<:′-trans-rec S′ (λ T′ T′<S′ → rec T′ (≤-step (≤-stepsʳ _ T′<S′))) S‴<:S′ S′<:S″)
            (<:′-trans-rec U′ (λ T′ T′<U′ → rec T′ (≤-step (≤-stepsˡ _ T′<U′)))
                           (proj₂ (rec (S′ ↑ 0) (s≤s $ ≤-stepsʳ _ $ ≤-reflexive (Typ-measure-↑ S′ 0)))
                                  U″<:U′
                                  ≺[ _ , S‴<:S′ ]
                                  refl)
                           U′<:U‴)

    <:′-trans-rec T rec ⊥<: T<:U                     = ⊥<:
    <:′-trans-rec T rec refl T<:U                    = T<:U
    <:′-trans-rec T rec S<:T <:⊤                     = <:⊤
    <:′-trans-rec T rec S<:T refl                    = S<:T
    <:′-trans-rec T rec (sel₂ T′∈Γ T′<:B) T<:U       = sel₂ T′∈Γ (⟨A<:⟩-traverseʳ T rec T<:U T′<:B _ refl)
    <:′-trans-rec T rec (<:> T′∈Γ T′<:B T′<:B′) T<:U = <:> T′∈Γ T′<:B (⟨A<:⟩-traverseʳ T rec T<:U T′<:B′ _ refl)
    <:′-trans-rec T rec S<:T (sel₁ T′∈Γ T′<:B)       = sel₁ T′∈Γ (⟨A<:⟩-traverseˡ T rec S<:T T′<:B [] refl)
    <:′-trans-rec T rec S<:T (<:> T′∈Γ T′<:B T′<:B′) = <:> T′∈Γ (⟨A<:⟩-traverseˡ T rec S<:T T′<:B [] refl) T′<:B′

    ⟨A<:⟩-traverseʳ : ∀ T →
                        (∀ T′ → Typ-measure T′ < Typ-measure T → trans-on T′ × narrow-on T′) →
                      ∀ {Γ U} →
                        Γ ⊢″ T <: U →
                      ∀ {S S′ T′} →
                        Γ ⊢″ S <: ⟨A: S′ ⋯ T′ ⟩ →
                      ∀ l →
                        T′ ≡ ⟨A:⟩-layer T l →
                        Γ ⊢″ S <: ⟨A: S′ ⋯ ⟨A:⟩-layer U l ⟩
    ⟨A<:⟩-traverseʳ T rec T<:U ⊥<: l eqT′                        = ⊥<:
    ⟨A<:⟩-traverseʳ T rec T<:U refl [] refl                      = bnd refl T<:U
    ⟨A<:⟩-traverseʳ T rec T<:U refl (S′ ∷ l) refl                = bnd refl (⟨A<:⟩-traverseʳ T rec T<:U refl l refl)
    ⟨A<:⟩-traverseʳ T rec T<:U (bnd S₂<:S₁ U₁<:T) [] refl        = bnd S₂<:S₁ (<:′-trans-rec T rec U₁<:T T<:U)
    ⟨A<:⟩-traverseʳ T rec T<:U (bnd S₂<:S₁ U₁<:U₂) (S′ ∷ l) refl = bnd S₂<:S₁ (⟨A<:⟩-traverseʳ T rec T<:U U₁<:U₂ l refl)
    ⟨A<:⟩-traverseʳ T rec T<:U (sel₂ T′∈Γ T′<:B) l refl          = sel₂ T′∈Γ (⟨A<:⟩-traverseʳ T rec T<:U T′<:B (_ ∷ l) refl)
    ⟨A<:⟩-traverseʳ T rec T<:U (<:> T′∈Γ T′<:B T′<:B′) l refl    = <:> T′∈Γ T′<:B (⟨A<:⟩-traverseʳ T rec T<:U T′<:B′ (_ ∷ l) refl)

    ⟨A<:⟩-traverseˡ : ∀ T →
                        (∀ T′ → Typ-measure T′ < Typ-measure T → trans-on T′ × narrow-on T′) →
                      ∀ {Γ S} →
                        Γ ⊢″ S <: T →
                      ∀ {S′ T′} →
                        Γ ⊢″ S′ <: T′ →
                      ∀ {U} l →
                        T′ ≡ ⟨A:⟩-layer ⟨A: T ⋯ U ⟩ l →
                        Γ ⊢″ S′ <: ⟨A:⟩-layer ⟨A: S ⋯ U ⟩ l
    ⟨A<:⟩-traverseˡ T rec S<:T <:⊤ [] ()
    ⟨A<:⟩-traverseˡ T rec S<:T <:⊤ (_ ∷ l) ()
    ⟨A<:⟩-traverseˡ T rec S<:T ⊥<: l eqT′                        = ⊥<:
    ⟨A<:⟩-traverseˡ T rec S<:T refl [] refl                      = bnd S<:T refl
    ⟨A<:⟩-traverseˡ T rec S<:T refl (S′ ∷ l) refl                = bnd refl (⟨A<:⟩-traverseˡ T rec S<:T refl l refl)
    ⟨A<:⟩-traverseˡ T rec S<:T (bnd T<:S₁ U₁<:U₂) [] refl        = bnd (<:′-trans-rec T rec S<:T T<:S₁) U₁<:U₂
    ⟨A<:⟩-traverseˡ T rec S<:T (bnd S₂<:S₁ U₁<:U₂) (S′ ∷ l) refl = bnd S₂<:S₁ (⟨A<:⟩-traverseˡ T rec S<:T U₁<:U₂ l refl)
    ⟨A<:⟩-traverseˡ T rec S<:T (Π<: S₂<:S₁ U₁<:U₂) [] ()
    ⟨A<:⟩-traverseˡ T rec S<:T (Π<: S₂<:S₁ U₁<:U₂) (_ ∷ l) ()
    ⟨A<:⟩-traverseˡ T rec S<:T (sel₁ T′∈Γ T′<:B) [] ()
    ⟨A<:⟩-traverseˡ T rec S<:T (sel₁ T′∈Γ T′<:B) (_ ∷ l) ()
    ⟨A<:⟩-traverseˡ T rec S<:T (sel₂ T′∈Γ T′<:B) {U} l refl      = sel₂ T′∈Γ (⟨A<:⟩-traverseˡ T rec S<:T T′<:B {U} (_ ∷ l) refl)
    ⟨A<:⟩-traverseˡ T rec S<:T (<:> T′∈Γ T′<:B T′<:B′) l refl    = <:> T′∈Γ T′<:B (⟨A<:⟩-traverseˡ T rec S<:T T′<:B′ (_ ∷ l) refl)

  <:″-narrow-on : ∀ T → (∀ T′ → Typ-measure T′ ≡ Typ-measure T → trans-on T′) → narrow-on T
  <:″-narrow-on T trans <:⊤ Γ′≺Γ T∈Γ               = <:⊤
  <:″-narrow-on T trans ⊥<: Γ′≺Γ T∈Γ               = ⊥<:
  <:″-narrow-on T trans refl Γ′≺Γ T∈Γ              = refl
  <:″-narrow-on T trans (bnd S′<:S U<:U′) Γ′≺Γ T∈Γ = bnd (<:″-narrow-on T trans S′<:S Γ′≺Γ T∈Γ)
                                                         (<:″-narrow-on T trans U<:U′ Γ′≺Γ T∈Γ)
  <:″-narrow-on T trans {Γ} {Γ′} {n} (Π<: {S′ = S′} S′<:S U<:U′) Γ′≺Γ T∈Γ
    = Π<: (<:″-narrow-on T trans S′<:S Γ′≺Γ T∈Γ)
          (<:″-narrow-on (T ↑ 0)
                         (λ T′ eq → trans T′ (≡.trans eq (Typ-measure-↑ T 0)))
                         U<:U′ (_ ∷ Γ′≺Γ)
                         (↦∈⇒lookup (tl {n} {T′ = S′} {Γ} (lookup⇒↦∈ T∈Γ))))

  <:″-narrow-on T trans (sel₁ T′∈Γ T′<:B) Γ′≺Γ T∈Γ
    with <:∈-find′ T′∈Γ Γ′≺Γ
  ...  | inj₁ (refl , T″ , T″∈Γ′ , T″<:T)
    rewrite just-injective (≡.trans (≡.sym T′∈Γ) T∈Γ) = sel₁ T″∈Γ′ (trans T refl T″<:T (<:″-narrow-on T trans T′<:B Γ′≺Γ T∈Γ))
  ... | inj₂ (x≢n , T′∈Γ′)                            = sel₁ T′∈Γ′ (<:″-narrow-on T trans T′<:B Γ′≺Γ T∈Γ)
  <:″-narrow-on T trans (sel₂ T′∈Γ T′<:B) Γ′≺Γ T∈Γ
    with <:∈-find′ T′∈Γ Γ′≺Γ
  ...  | inj₁ (refl , T″ , T″∈Γ′ , T″<:T)
    rewrite just-injective (≡.trans (≡.sym T′∈Γ) T∈Γ) = sel₂ T″∈Γ′ (trans T refl T″<:T (<:″-narrow-on T trans T′<:B Γ′≺Γ T∈Γ))
  ... | inj₂ (x≢n , T′∈Γ′)                            = sel₂ T′∈Γ′ (<:″-narrow-on T trans T′<:B Γ′≺Γ T∈Γ)
  <:″-narrow-on T trans (<:> T′∈Γ T′<:B T′<:B′) Γ′≺Γ T∈Γ
    with <:∈-find′ T′∈Γ Γ′≺Γ
  ...  | inj₁ (refl , T″ , T″∈Γ′ , T″<:T)
    rewrite just-injective (≡.trans (≡.sym T′∈Γ) T∈Γ) = <:> T″∈Γ′
                                                            (trans T refl T″<:T (<:″-narrow-on T trans T′<:B Γ′≺Γ T∈Γ))
                                                            (trans T refl T″<:T (<:″-narrow-on T trans T′<:B′ Γ′≺Γ T∈Γ))
  ... | inj₂ (x≢n , T′∈Γ′)                            = <:> T′∈Γ′
                                                            (<:″-narrow-on T trans T′<:B Γ′≺Γ T∈Γ)
                                                            (<:″-narrow-on T trans T′<:B′ Γ′≺Γ T∈Γ)

  -- The previous functions achieve the inductive hypotheses of the well-founded
  -- induction on the size of the type T, and the following function combines those
  -- inductive hypotheses and conclude transitivity and narrowing.
  <:″-trans-narrow : ∀ T → trans-on T × narrow-on T
  <:″-trans-narrow = wfRec _ aux
    where open Measure <-wellFounded Typ-measure
          aux : ∀ T → (∀ T′ → Typ-measure T′ < Typ-measure T → trans-on T′ × narrow-on T′) → trans-on T × narrow-on T
          aux T rec = <:′-trans-rec T rec
                    , <:″-narrow-on T (λ T′ T′≡T →
                                         <:′-trans-rec T′ λ T″ T″<T′ → rec T″ (≤-trans T″<T′ (≤-reflexive T′≡T)))

  <:″-trans : ∀ {T} → trans-on T
  <:″-trans {T} = proj₁ (<:″-trans-narrow T)

  <:″-narrow : ∀ {T} → narrow-on T
  <:″-narrow {T} = proj₂ (<:″-trans-narrow T)

open SimplerTransitivity using (<:″-trans ; <:″-narrow) public

-- the following two functions show that the original D<: and D<: normal form are
-- equivalent.
<:⇒<:″ : ∀ {Γ S U} → Γ ⊢ S <: U → Γ ⊢″ S <: U
<:⇒<:″ dtop                 = <:⊤
<:⇒<:″ dbot                 = ⊥<:
<:⇒<:″ drefl                = refl
<:⇒<:″ (dtrans T S<:T T<:U) = <:″-trans (<:⇒<:″ S<:T) (<:⇒<:″ T<:U)
<:⇒<:″ (dbnd S′<:S U<:U′)   = bnd (<:⇒<:″ S′<:S) (<:⇒<:″ U<:U′)
<:⇒<:″ (dall S′<:S U<:U′)   = Π<: (<:⇒<:″ S′<:S) (<:⇒<:″ U<:U′)
<:⇒<:″ (dsel₁ T∈Γ T<:B)     = sel₁ T∈Γ (<:⇒<:″ T<:B)
<:⇒<:″ (dsel₂ T∈Γ T<:B)     = sel₂ T∈Γ (<:⇒<:″ T<:B)

<:″⇒<: : ∀ {Γ S U} → Γ ⊢″ S <: U → Γ ⊢ S <: U
<:″⇒<: <:⊤                  = dtop
<:″⇒<: ⊥<:                  = dbot
<:″⇒<: refl                 = drefl
<:″⇒<: (bnd S′<:S U<:U′)    = dbnd (<:″⇒<: S′<:S) (<:″⇒<: U<:U′)
<:″⇒<: (Π<: S′<:S U<:U′)    = dall (<:″⇒<: S′<:S) (<:″⇒<: U<:U′)
<:″⇒<: (sel₁ T∈Γ T<:B)      = dsel₁ T∈Γ (<:″⇒<: T<:B)
<:″⇒<: (sel₂ T∈Γ T<:B)      = dsel₂ T∈Γ (<:″⇒<: T<:B)
<:″⇒<: (<:> T∈Γ T<:B S<:B′) = dtrans _ (dsel₁ T∈Γ (dtrans _ (<:″⇒<: T<:B) (dbnd drefl dtop)))
                                       (dsel₂ T∈Γ (dtrans _ (<:″⇒<: S<:B′) (dbnd dbot drefl)))
-- D<: subtyping is undecidable.
module Undecidability′ where
  open import DsubReduced
  open FsubMinusToDsubR using (⟦_⟧ ; ⟪_⟫ ; D<:ᵣ⇒F<: ; F<:⇒D<:ᵣ ; ⟪⟫-contraEnv ; ⟦⟧-covar)
  open DsubInvProperties contraInvertible
  open import FsubMinus

  <:″⇒<:ᵣ : ∀ {Γ S U} →
              Γ ⊢″ S <: U →
              ContraEnv Γ → Covar S → Covar U →
              Γ ⊢ᵣ S <: U
  <:″⇒<:ᵣ <:⊤ cΓ cS cU                                           = drtop cS
  <:″⇒<:ᵣ ⊥<: cΓ () cU
  <:″⇒<:ᵣ refl cΓ cS cU                                          = drrefl cU
  <:″⇒<:ᵣ (bnd S′<:S U<:U′) cΓ cS ()
  <:″⇒<:ᵣ (Π<: <:⊤ U<:U′) cΓ () cU
  <:″⇒<:ᵣ (Π<: ⊥<: U<:U′) cΓ cS ()
  <:″⇒<:ᵣ (Π<: refl U<:U′) cΓ (cvΠ cS cU) (cvΠ cS′ cU′)          = drall cS′ cU cS′ cU′
                                                                         (drrefl cS′)
                                                                         (<:″⇒<:ᵣ U<:U′ (ctt cS′ ∷ cΓ) cU cU′)
  <:″⇒<:ᵣ (Π<: (bnd _ S′<:S) U<:U′) cΓ (cvΠ cS cU) (cvΠ cS′ cU′) = drall cS cU cS′ cU′
                                                                         (<:″⇒<:ᵣ S′<:S cΓ cS′ cS)
                                                                         (<:″⇒<:ᵣ U<:U′ (ctt cS′ ∷ cΓ) cU cU′)
  <:″⇒<:ᵣ (Π<: (Π<: S′<:S S′<:S₁) U<:U′) cΓ () cU
  <:″⇒<:ᵣ (Π<: (sel₁ x S′<:S) U<:U′) cΓ () cU
  <:″⇒<:ᵣ (Π<: (sel₂ x S′<:S) U<:U′) cΓ cS ()
  <:″⇒<:ᵣ (Π<: (<:> T∈Γ T<:B T<:B′) U<:U′) cΓ (cvΠ _ _) (cvΠ _ _)
    with lookupContraEnv T∈Γ cΓ
  ... | ctt _                                                    = case ⟨A:⟩<:⟨A:⟩′ (<:″⇒<: T<:B) cΓ of λ ()
  <:″⇒<:ᵣ (sel₁ T∈Γ T<:B) cΓ cS cU
    with lookupContraEnv T∈Γ cΓ
  ... | ctt _  rewrite ⟨A:⟩<:⟨A:⟩′ (<:″⇒<: T<:B) cΓ              = case cS of λ ()
  <:″⇒<:ᵣ (sel₂ T∈Γ T<:B) cΓ cS cU
    with lookupContraEnv T∈Γ cΓ
  ... | ctt cT                                                   = drsel T∈Γ cT (aux T<:B cΓ cT cU)
    where aux : ∀ {Γ T S U} → Γ ⊢″ ⟨A: ⊥ ⋯ T ⟩ <: ⟨A: S ⋯ U ⟩ → ContraEnv Γ → Covar T → Covar U → Γ ⊢ᵣ T <: U
          aux refl cΓ cT cU                                      = drrefl cU
          aux (bnd _ T<:U) cΓ cT cU                              = <:″⇒<:ᵣ T<:U cΓ cT cU
          aux (<:> T′∈Γ T′<:B _) cΓ cT cU
            with lookupContraEnv T′∈Γ cΓ
          ... | ctt _                                            = case ⟨A:⟩<:⟨A:⟩′ (<:″⇒<: T′<:B) cΓ of λ ()
  <:″⇒<:ᵣ (<:> T∈Γ T<:B T<:B′) cΓ cS cU
    with lookupContraEnv T∈Γ cΓ
  ... | ctt _  rewrite ⟨A:⟩<:⟨A:⟩′ (<:″⇒<: T<:B) cΓ              = case cS of λ ()

  <:ᵣ⇒<: : ∀ {Γ S U} → Γ ⊢ᵣ S <: U → Γ ⊢ S <: U
  <:ᵣ⇒<: (drtop _)                   = dtop
  <:ᵣ⇒<: (drrefl _)                  = drefl
  <:ᵣ⇒<: (drall _ _ _ _ S′<:S U<:U′) = dall (dbnd dbot (<:ᵣ⇒<: S′<:S)) (<:ᵣ⇒<: U<:U′)
  <:ᵣ⇒<: (drsel T∈Γ _ T<:B)          = dtrans _ (dsel₂ T∈Γ drefl) (<:ᵣ⇒<: T<:B)

  open FsubMinus.FsubMinus

  F<:⇒D<: : ∀ {Γ S U} → Γ ⊢F S <: U → ⟪ Γ ⟫ ⊢ ⟦ S ⟧ <: ⟦ U ⟧
  F<:⇒D<: = <:ᵣ⇒<: ∘ F<:⇒D<:ᵣ

  D<:⇒F<: : ∀ {Γ S U} → ⟪ Γ ⟫ ⊢ ⟦ S ⟧ <: ⟦ U ⟧ → Γ ⊢F S <: U
  D<:⇒F<: S<:U = D<:ᵣ⇒F<: (<:″⇒<:ᵣ (<:⇒<:″ S<:U) (⟪⟫-contraEnv _) (⟦⟧-covar _) (⟦⟧-covar _))
                          refl refl refl

ext: agda


text:
module imper-nouni where

--
-- TO-DOs
--
-- * change use of =string
-- * prove that =string can't be both tt and ff
-- * prove reverse theorems for passes/fails/chck
-- * prove semantic equivalence for execs and execsTo
--    + this would be s-thm and s-det

open import lib
open import eq-reas-nouni

_=nat_ = _=ℕ_

_-nat_ = _∸_

cross = _×_

equiv = _≡_

bottom = ⊥

bottom-elim = ⊥-elim

--
-- inspect/with-eq idiom
--

data Singleton {a} {A : Set a} (x : A) : Set a where
  _with-eq_ : (y : A) → equiv x y → Singleton x

inspect : forall {a} {A : Set a} (x : A) -> Singleton x
inspect x = x with-eq refl

--
-- variable identifiers
--
Id : Set
Id = string

_=Id_ : Id -> Id -> bool
_=Id_ = _=string_

--
-- values (just natural numbers here)
--

Val : Set
Val = nat

--
-- value and variable expressions
--
data Expn : Set where
  val : Val -> Expn
  var : Id -> Expn
  plus : Expn -> Expn -> Expn
  minus : Expn -> Expn -> Expn
  scaleBy : Expn -> Val -> Expn

--
-- conditions on values and variables
--
data Cond : Set where
  true : Cond
  false : Cond
  and : Cond -> Cond -> Cond
  or : Cond -> Cond -> Cond
  not : Cond -> Cond
  less : Expn -> Expn -> Cond
  equal : Expn -> Expn -> Cond

--
-- stack frames containing variable bindings
--
Frm : Set
Frm = list (cross Id Val)

--
-- program statements that transform a frame
--
data Stmt : Set where
  skip : Stmt
  assign : Id -> Expn -> Stmt
  seq : Stmt -> Stmt -> Stmt
  ifThenElse : Cond -> Stmt -> Stmt -> Stmt
  repeatBy : Id -> Stmt -> Stmt
  returns : Expn -> Stmt

--
-- functional SEMANTICS of frames
--

lkup : Id -> Frm -> Val
lkup x [] = 0
lkup x ((y , w) :: F) = if (x =Id y) then w else (lkup x F)

update : Id -> Val -> Frm -> Frm
update x v [] = (x , v) :: []
update x v ((y , w) :: F)
          = if (x =Id y)
              then (y , v) :: F
              else (y , w) :: (update x v F)
--
-- functional SEMANTICS of expressions
--
eval : Expn -> Frm -> Val
eval (val v) F = v
eval (var x) F = lkup x F
eval (plus e1 e2) F = (eval e1 F) + (eval e2 F)
eval (minus e1 e2) F = (eval e1 F) -nat (eval e2 F)
eval (scaleBy e1 v2) F = (eval e1 F) * v2

--
-- functional SEMANTICS of conditions
--
chck : Cond -> Frm -> bool
chck true F = tt
chck false F = ff
chck (and c1 c2) F = (chck c1 F) && (chck c2 F)
chck (or c1 c2) F = (chck c1 F) || (chck c2 F)
chck (not c) F = ~ (chck c F)
chck (less e1 e2) F = (eval e1 F) < (eval e2 F)
chck (equal e1 e2) F = (eval e1 F) =nat (eval e2 F)

--
-- functional SEMANTICS of program execution
--
exec : Stmt -> Frm -> Frm
repeatedly : Stmt -> Id -> nat -> Frm -> Frm
repeatedly s x 0 F = F
repeatedly s x (suc n) F = repeatedly s x n (update x n (exec s F))
exec skip F = F
exec (seq s1 s2) F = (exec s2 (exec s1 F))
exec (assign x e) F = (update x (eval e F) F)
exec (ifThenElse c s1 s2) F = if (chck c F) then (exec s1 F) else (exec s2 F)
exec (repeatBy x s) F = repeatedly s x (lkup x F) F
exec (returns e) F = (update "retval" (eval e F) F)

--
-- SEMANTICS of stack bindings as a relation
--
data mapsTo : Frm -> Id -> Val -> Set where

  var-undef : forall {x : Id}
              ----------------
              -> (mapsTo [] x 0)

  var-match : forall {x y : Id} {F : Frm} {v : Val}
              -> (equiv (x =string y) tt)
              ---------------------------
              -> (mapsTo ((y , v) :: F) x v)

  var-mismatch : forall {x y : Id} {F : Frm} {v w : Val}
                 -> (equiv (x =string y) ff)
                 -> (mapsTo F x v)
                 ----------------------------
                 -> (mapsTo ((y , w) :: F) x v)

--
-- THEOREM: mapsTo agrees with lookup
--
var-thm : forall (x : Id) (F : Frm) -> mapsTo F x (lkup x F)
var-thm x [] = var-undef
var-thm x ((y , w) :: F)
     with (inspect (x =string y))
...     | tt with-eq match =
            let lkup-is-w : (equiv (lkup x ((y , w) :: F)) w)
                lkup-is-w = cong3 if_then_else_ match refl refl
             in cong-pred (mapsTo ((y , w) :: F) x) (sym lkup-is-w) (var-match match)
...     | ff with-eq mismatch =
            let lkup-is-lkup : (equiv (lkup x ((y , w) :: F)) (lkup x F))
                lkup-is-lkup = cong3 if_then_else_ mismatch refl refl
             in cong-pred (mapsTo ((y , w) :: F) x) (sym lkup-is-lkup) (var-mismatch mismatch (var-thm x F))

postulate
  =Id-det : ∀ {x y : Id} -> (equiv (x =string y) tt) -> (equiv (x =string y) ff) -> bottom

var-det : forall{x : Id}{F : Frm}{u1 u2 : Val}
    -> mapsTo F x u1 -> mapsTo F x u2 -> equiv u1 u2
var-det{x}{[]}{u1}{u2} var-undef var-undef =
  refl
var-det{x}{(y , w) :: F}{u1}{u2} (var-match _) (var-match _) =
  refl
var-det{x}{(y , w) :: F}{u1}{u2} (var-mismatch _ lkup-is-u1) (var-mismatch _ lkup-is-u2) =
  var-det lkup-is-u1 lkup-is-u2
var-det{x}{(y , w) :: F}{u1}{u2} (var-match{.x}{.y}{.F}{.u1} same) (var-mismatch{.x}{.y}{.F}{.u2} diff _) =
  bottom-elim (=Id-det{x}{y} same diff)
var-det{x}{(y , w) :: F}{u1}{u2} (var-mismatch{.x}{.y}{.F}{.u1} diff _) (var-match{.x}{.y}{.F}{.u2} same) =
  bottom-elim (=Id-det{x}{y} same diff)

--
-- SEMANTICS of expression evaluation as a relation
--

data evalsTo : Frm -> Expn -> Val -> Set where

  e-val : forall {v : Val} {F : Frm}
            ------------------------
            -> (evalsTo F (val v) v)

  e-var : forall {x : Id} {F : Frm} {v : Val}
          -> (mapsTo F x v)
          ------------------------
          -> (evalsTo F (var x) v)

  e-add : forall {e1 e2 : Expn} {F : Frm} {v1 v2 : Val}
          -> (evalsTo F e1 v1)
          -> (evalsTo F e2 v2)
          -------------------------------------
          -> (evalsTo F (plus e1 e2) (v1 + v2))

  e-sub : forall {e1 e2 : Expn} {F : Frm} {v1 v2 : Val}
          -> (evalsTo F e1 v1)
          -> (evalsTo F e2 v2)
          -----------------------------------------
          -> (evalsTo F (minus e1 e2) (v1 -nat v2))

  e-scale : forall {e1 : Expn} {F : Frm} {v1 v2 : Val}
          -> (evalsTo F e1 v1)
          ----------------------------------------
          -> (evalsTo F (scaleBy e1 v2) (v1 * v2))

e-thm : forall (e : Expn) -> (F : Frm) -> (evalsTo F e (eval e F))
e-thm (val e) F = e-val
e-thm (var x) F = e-var (var-thm x F)
e-thm (plus e1 e2) F = (e-add (e-thm e1 F) (e-thm e2 F))
e-thm (minus e1 e2) F = (e-sub (e-thm e1 F) (e-thm e2 F))
e-thm (scaleBy e1 v2) F = (e-scale (e-thm e1 F))

e-det : forall {e : Expn}{F : Frm}{u w : Val}
  -> (evalsTo F e u) -> (evalsTo F e w) -> (equiv u w)
e-det{val v}{F}{u}{w} e-val e-val =  refl
e-det{var x}{F}{u}{w} (e-var var-lkup-u) (e-var var-lkup-v) =
  var-det var-lkup-u var-lkup-v
e-det{plus e1 e2}{F}{u}{w} (e-add e-u1 e-u2) (e-add e-w1 e-w2) =
  cong2 _+_ (e-det e-u1 e-w1) (e-det e-u2 e-w2)
e-det{minus e1 e2}{F}{u}{w} (e-sub e-u1 e-u2) (e-sub e-w1 e-w2) =
  cong2 _-nat_ (e-det e-u1 e-w1) (e-det e-u2 e-w2)
e-det{scaleBy e1 v2}{F}{u}{w} (e-scale e-u1) (e-scale e-w1) =
  cong2 _*_ (e-det e-u1 e-w1) refl

e-thm-fwd : forall {e : Expn}{F : Frm}{v : Val}
  -> (evalsTo F e v) -> (equiv v (eval e F))
e-thm-fwd{e}{F}{v} ev =
  let
      p1 : evalsTo F e (eval e F)
      p1 = e-thm e F
   in e-det ev p1

e-thm-rev : forall {e : Expn}{F : Frm}{v : Val}
  -> (equiv v (eval e F)) -> (evalsTo F e v)
e-thm-rev{e}{F}{v} v-is = cong-pred (evalsTo F e) (sym v-is) (e-thm e F)

--
-- SEMANTICS of conditions as a decidable relation
--

data  passes : Frm -> Cond -> Set
data fails : Frm -> Cond -> Set

data passes where

  c-tt :  forall {F : Frm}
          ----------------
          -> passes F true

  c-and : forall {c1 c2 : Cond} {F : Frm}
          -> passes F c1
          -> passes F c2
          -----------------------
          -> passes F (and c1 c2)

  c-or1 : forall {c1 c2 : Cond} {F : Frm}
          -> passes F c1
          ----------------------
          -> passes F (or c1 c2)

  c-or2 : forall {c1 c2 : Cond} {F : Frm}
          -> passes F c2
          ----------------------
          -> passes F (or c1 c2)

  c-less : forall {e1 e2 : Expn} {F : Frm} {v1 v2 : Val}
           -> equiv (v1 < v2) tt
           -> evalsTo F e1 v1
           -> evalsTo F e2 v2
           -------------------------
           -> passes F (less e1 e2)

  c-eq : forall {e1 e2 : Expn} {F : Frm} {v1 v2 : Val}
           -> equiv (v1 =nat v2) tt
           -> evalsTo F e1 v1
           -> evalsTo F e2 v2
           --------------------------
           -> passes F (equal e1 e2)

  c-not : forall {c : Cond} {F : Frm}
          -> fails F c
          -------------------
          -> passes F (not c)

data fails where

  ~c-ff :  forall {F : Frm}
          ----------------
          -> fails F false

  ~c-or : forall {c1 c2 : Cond} {F : Frm}
          -> fails F c1
          -> fails F c2
          -----------------------
          -> fails F (or c1 c2)

  ~c-and1 : forall {c1 c2 : Cond} {F : Frm}
          -> fails F c1
          ----------------------
          -> fails F (and c1 c2)

  ~c-and2 : forall {c1 c2 : Cond} {F : Frm}
          -> fails F c2
          ----------------------
          -> fails F (and c1 c2)

  ~c-less : forall {e1 e2 : Expn} {F : Frm} {v1 v2 : Val}
           -> equiv (v1 < v2) ff
           -> evalsTo F e1 v1
           -> evalsTo F e2 v2
           -------------------------
           -> fails F (less e1 e2)

  ~c-eq : forall {e1 e2 : Expn} {F : Frm} {v1 v2 : Val}
           -> equiv (v1 =nat v2) ff
           -> evalsTo F e1 v1
           -> evalsTo F e2 v2
           --------------------------
           -> fails F (equal e1 e2)

  ~c-not : forall {c : Cond} {F : Frm}
          -> passes F c
          -------------------
          -> fails F (not c)

c-thm-fwd : forall {c : Cond}{F : Frm} -> (passes F c) -> (equiv (chck c F) tt)
~c-thm-fwd : forall {c : Cond}{F : Frm} -> (fails F c) -> (equiv (chck c F) ff)

c-thm-fwd (c-tt{F}) = refl
c-thm-fwd (c-and{c1}{c2}{F} passes-c1 passes-c2) =
  cong2 _&&_ (c-thm-fwd passes-c1) (c-thm-fwd passes-c2)
c-thm-fwd (c-or1{c1}{c2}{F} passes-c1) =
  cong2 _||_ (c-thm-fwd passes-c1) refl
c-thm-fwd (c-or2{c1}{c2}{F} passes-c2) =
  trans (cong2 _||_ refl (c-thm-fwd passes-c2)) (||-tt (chck c1 F))
c-thm-fwd (c-less{e1}{e2}{F}{v1}{v2} v1-less-v2 evalsTo-e1-v1 evalsTo-e2-v2) =
  let
    eval-e1-is-v1 : (equiv (eval e1 F) v1)
    eval-e1-is-v1 = sym (e-thm-fwd evalsTo-e1-v1)
    eval-e2-is-v2 : (equiv (eval e2 F) v2)
    eval-e2-is-v2 = sym (e-thm-fwd evalsTo-e2-v2)
  in
    begin
      chck (less e1 e2) F
    equiv[ refl ]
      (eval e1 F) < (eval e2 F)
    equiv[ cong2 _<_ eval-e1-is-v1 eval-e2-is-v2 ]
      v1 < v2
    equiv[ v1-less-v2 ]
      tt
    qed
c-thm-fwd (c-eq{e1}{e2}{F}{v1}{v2} v1-equals-v2 evalsTo-e1-v1 evalsTo-e2-v2) =
  let
    eval-e1-is-v1 : (equiv (eval e1 F) v1)
    eval-e1-is-v1 = sym (e-thm-fwd evalsTo-e1-v1)
    eval-e2-is-v2 : (equiv (eval e2 F) v2)
    eval-e2-is-v2 = sym (e-thm-fwd evalsTo-e2-v2)
  in
    begin
      chck (equal e1 e2) F
    equiv[ refl ]
      (eval e1 F) =nat (eval e2 F)
    equiv[ cong2 _=nat_ eval-e1-is-v1 eval-e2-is-v2 ]
      v1 =nat v2
    equiv[ v1-equals-v2 ]
      tt
    qed
c-thm-fwd (c-not{c}{F} c-fails) = cong ~_ (~c-thm-fwd c-fails)

~c-thm-fwd (~c-ff{F}) =
  refl
~c-thm-fwd (~c-or{c1}{c2}{F} fails-c1 fails-c2) =
  cong2 _||_ (~c-thm-fwd fails-c1) (~c-thm-fwd fails-c2)
~c-thm-fwd (~c-and1{c1}{c2}{F} fails-c1) =
  cong2 _&&_ (~c-thm-fwd fails-c1) refl
~c-thm-fwd (~c-and2{c1}{c2}{F} fails-c2) =
  trans (cong2 _&&_ refl (~c-thm-fwd fails-c2)) (&&-ff (chck c1 F))
~c-thm-fwd (~c-less{e1}{e2}{F}{v1}{v2} v1-not-less-v2 evalsTo-e1-v1 evalsTo-e2-v2) =
  let
    eval-e1-is-v1 : (equiv (eval e1 F) v1)
    eval-e1-is-v1 = sym (e-thm-fwd evalsTo-e1-v1)
    eval-e2-is-v2 : (equiv (eval e2 F) v2)
    eval-e2-is-v2 = sym (e-thm-fwd  evalsTo-e2-v2)
  in begin
    chck (less e1 e2) F
  equiv[ refl ]
    (eval e1 F) < (eval e2 F)
  equiv[ cong2 _<_ eval-e1-is-v1 eval-e2-is-v2 ]
    v1 < v2
  equiv[ v1-not-less-v2 ]
    ff
  qed
~c-thm-fwd (~c-eq{e1}{e2}{F}{v1}{v2} v1-not-equals-v2 evalsTo-e1-v1 evalsTo-e2-v2) =
  let
    eval-e1-is-v1 : (equiv (eval e1 F) v1)
    eval-e1-is-v1 = sym (e-thm-fwd evalsTo-e1-v1)
    eval-e2-is-v2 : (equiv (eval e2 F) v2)
    eval-e2-is-v2 = sym (e-thm-fwd evalsTo-e2-v2)
  in
    begin
      chck (equal e1 e2) F
    equiv[ refl ]
      (eval e1 F) =nat (eval e2 F)
    equiv[ cong2 _=nat_ eval-e1-is-v1 eval-e2-is-v2 ]
      v1 =nat v2
    equiv[ v1-not-equals-v2 ]
      ff
    qed
~c-thm-fwd (~c-not{c}{F} c-passes) =
  cong ~_ (c-thm-fwd c-passes)

-- These can probably be shown just by using
-- the contrapositives of ~c-thm-fwd and ~~c-thm-fwd
postulate
  c-thm-rev : forall {c : Cond}{F : Frm} -> (equiv (chck c F) tt) -> (passes F c)
  ~c-thm-rev : forall {c : Cond}{F : Frm} -> (equiv (chck c F) ff) -> (fails F c)

--
-- SEMANTICS of program statements
-- as a state transformation relation
--

data execsTo : Frm -> Stmt -> Frm -> Set where

  s-skip : forall {F : Frm}
    -------------------
    -> execsTo F skip F

  s-assign : forall {x : Id} {e : Expn} {F : Frm}  {v : Val}
    -> evalsTo F e v
    ----------------------------------------
    -> execsTo F (assign x e) (update x v F)

  s-seq : forall {s1 s2 : Stmt} {F0 F1 F2 : Frm}
    -> (execsTo F0 s1 F1)
    -> (execsTo F1 s2 F2)
    ------------------------------
    -> (execsTo F0 (seq s1 s2) F2)

  s-if-then : forall {c : Cond} {s1 s2 : Stmt} {F F' : Frm}
    -> (passes F c)
    -> (execsTo F s1 F')
    --------------------------------------
    -> (execsTo F (ifThenElse c s1 s2) F')

  s-if-else : forall {c : Cond} {s1 s2 : Stmt} {F F' : Frm}
    -> (fails F c)
    -> (execsTo F s2 F')
    --------------------------------------
    -> (execsTo F (ifThenElse c s1 s2) F')

  s-repeat-0 : forall {s : Stmt} {x : Id} {F : Frm}
     -> (mapsTo F x 0)
     -------------------------------
     -> (execsTo F (repeatBy x s) F)

  s-repeat-suc : forall {n : nat} {s : Stmt} {x : Id} {F F' : Frm}
    -> (mapsTo F x (suc n))
    -> (execsTo F (seq (seq s (assign x (val n))) (repeatBy x s)) F')
    -----------------------------------------------------------------
    -> (execsTo F (repeatBy x s) F')

  --
  -- A lil cheat: "returns" is just assign; doesn't exit

  s-return : forall {e : Expn} {F : Frm}  {rv : Val}
    -> (evalsTo F e rv)
    -------------------------------------------------
    -> (execsTo F (returns e) (update "retval" rv F))

postulate
  frm-compare : Frm -> Frm -> bool
  frm-iso : Frm -> Frm -> Set
  frm-not-iso  : Frm -> Frm -> Set

postulate
  s-thm : forall {s : Stmt}{F Ff Fr : Frm}
    -> execsTo F s Fr
    -> equiv (exec s F) Ff
    ----------------------
    -> frm-iso Ff Fr

max_stars_repo_name: JimFixGroupResearch/imper-ial

max_issues_repo_name: JimFixGroupResearch/imper-ial

max_forks_repo_name: JimFixGroupResearch/imper-ial


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

postulate
 I : Set
 P : I → Set

record ∃ (P : I → Set) : Set where
 constructor _,_
 field
   fst : I
   snd : P fst

open ∃

data S : ∃ P → Set where
 s : (i : I) (x : P i) → S (i , x)

Foo : (p : ∃ P) → S p → Set
Foo p (s .(fst p) .(snd p)) = I

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module hello-world where

open import IO
open import Level

main = run {0ℓ} (putStrLn "Hello, World!")

max_stars_repo_name: supeterlau/bedev

max_issues_repo_name: supeterlau/bedev

max_forks_repo_name: supeterlau/bedev


text:
-- Andreas, 2011-05-10
-- {-# OPTIONS -v tc.term.con:20 -v tc.meta:20 #-}
module Issue380 where

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

record Sigma (A : Set)(B : A -> Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Sigma public

testProj : {A : Set}{B : A -> Set}(y z : Sigma A B) ->
  let X : Sigma A B
      X = _
  in fst X == fst y -> snd X == snd z
testProj y z = refl , refl
{-  OLD BEHAVIOR: Error message about telescope comparison unreadable
This ill-typed term produces a weird error message:
(z' : fst (fst z , _283 y z) == fst y) !=<
when checking that the expression refl , refl has type
fst (fst z , _283 y z) == fst y → snd (fst z , _283 y z) == snd z
-}
{- FIXED.  Now it should complain that
Sigma (_47 y z == _47 y z) (_45 y z) !=<
fst (fst z , _43 y z) == fst y → snd (fst z , _43 y z) == snd z
when checking that the expression refl , refl has type
fst (fst z , _43 y z) == fst y → snd (fst z , _43 y z) == snd z
-}


text:
module _ where

open import Common.Bool

private
  unused = true
  used = true

private
 module Private where
  not-in-scope = true

in-scope = used


text:
record R : Set₁ where
  field
    ⟨_+_⟩ : Set

open R

-- Name parts coming from projections can not be used as part of the
-- defined name.

+ : Set → Set
+ A = A


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

open import HoTT
open import homotopy.elims.Lemmas
open import homotopy.elims.CofPushoutSection

module homotopy.elims.SuspSmash {i j k} {X : Ptd i} {Y : Ptd j}
  {P : Suspension (X ∧ Y) → Type k}
  (north* : P north) (south* : P south)
  (cod* : (s : fst X × fst Y) → north* == south* [ P ↓ merid (cfcod s) ])
  where

private
  base* = transport (λ κ → north* == south* [ P ↓ merid κ ])
    (! (cfglue (winl (snd X))))
    (cod* (snd X , snd Y))

  coh* : (s : X ∧ Y) → north* == south* [ P ↓ merid s ]
  coh* = CofPushoutSection.elim (λ _ → tt) (λ _ → idp)
    base*
    (λ {(x , y) →
      (fst (fillX x) ∙ fst (fillY y)) ◃ fst fill0 ◃ cod* (x , y)})
    (↓↓-from-squareover ∘ λ x →
      snd (fillX x) ↓⊡h∙
      ap (λ p → p ◃ fst fill0 ◃ cod* (x , snd Y))
         (! (ap (λ q → fst (fillX x) ∙ q) fillY-lemma ∙ ∙-unit-r _)))
    (↓↓-from-squareover ∘ λ y →
      snd (fillY y) ↓⊡h∙
      ap (λ p → p ◃ fst fill0 ◃ cod* (snd X , y))
         (! (ap (λ q → q ∙ fst (fillY y)) fillX-lemma)))
    where
    fill-lemma : (w : X ∨ Y)
      (α : north* == south* [ P ↓ merid (cfcod (∨-in-× X Y w)) ])
      → Σ (north* == north*)
          (λ p → SquareOver P (natural-square merid (cfglue w))
                   base*
                   (↓-ap-in _ _ (apd (λ _ → north*) (cfglue w)))
                   (↓-ap-in _ _ (apd (λ _ → south*) (cfglue w)))
                   (p ◃ α))
    fill-lemma w α = fill-upper-right _ _ _ _ _

    fill0 = fill-lemma (winl (snd X)) (cod* (snd X , snd Y))
    fillX = λ x → fill-lemma (winl x) (fst fill0 ◃ cod* (x , snd Y))
    fillY = λ y → fill-lemma (winr y) (fst fill0 ◃ cod* (snd X , y))

    fillX-lemma : fst (fillX (snd X)) == idp
    fillX-lemma = ! $
      fill-upper-right-unique _ _ _ _ _ idp (snd fill0 ↓⊡h∙ ! (idp◃ _))

    fillY-lemma : fst (fillY (snd Y)) == idp
    fillY-lemma = ! $
      fill-upper-right-unique _ _ _ _ _ idp (snd fill0 ↓⊡h∙ ! (idp◃ _))
      ∙ ap (λ w → fst (fill-lemma w (fst fill0 ◃ cod* (∨-in-× X Y w))))
           wglue

susp-smash-elim : Π (Suspension (X ∧ Y)) P
susp-smash-elim = Suspension-elim north* south* coh*

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- {-# OPTIONS -v term:20 #-}
module Issue787 where

data ⊥ : Set where

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

data Rat' {X : Set} : List (List X) → List X → Set where
  cons : ∀{ss x xs} → Rat' ((x ∷ xs) ∷ ss) xs → Rat' ss (x ∷ xs)

bad : {X : Set} (xs : List X) (acc : List (List X)) (p : Rat' acc xs) → ⊥
bad .(x ∷ xs) acc (cons {ss = .acc} {x = x} {xs = xs} p) =
 bad (x ∷ xs) acc (cons {ss = acc} {x = x} {xs = xs} p)

-- Andreas, 2013-02-18
-- This should give a termination error.
-- It did pass up to today because of the idempotency check
-- excluded bad calls with embedded sub-matrices.
-- Disabling matrix-shaped orders, which do not have a formal semantics
-- anyway, bring the termination problem to Agda's attention.


text:
module Warshall
  (X   : Set)
  ((≤) : X -> X -> Prop)
  -- and axioms...
  where

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

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

-- Natural numbers --------------------------------------------------------

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

(+) : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

-- Finite sets ------------------------------------------------------------

data Zero : Set where

data Suc (A:Set) : Set where
  fzero_ : Suc A
  fsuc_  : A -> Suc A

mutual

  data Fin (n:Nat) : Set where
    finI : Fin_ n -> Fin n

  Fin_ : Nat -> Set
  Fin_  zero   = Zero
  Fin_ (suc n) = Suc (Fin n)

fzero : {n:Nat} -> Fin (suc n)
fzero = finI fzero_

fsuc : {n:Nat} -> Fin n -> Fin (suc n)
fsuc i = finI (fsuc_ i)

finE : {n:Nat} -> Fin n -> Fin_ n
finE (finI i) = i

infixr 15 ::

-- Vectors ----------------------------------------------------------------

data Nil : Set where
  nil_ : Nil

data Cons (Xs:Set) : Set where
  cons_ : X -> Xs -> Cons Xs

mutual

  data Vec (n:Nat) : Set where
    vecI : Vec_ n -> Vec n

  Vec_ : Nat -> Set
  Vec_  zero   = Nil
  Vec_ (suc n) = Cons (Vec n)

nil : Vec zero
nil = vecI nil_

(::) : {n:Nat} -> X -> Vec n -> Vec (suc n)
x :: xs = vecI (cons_ x xs)

vecE : {n:Nat} -> Vec n -> Vec_ n
vecE (vecI xs) = xs

vec : (n:Nat) -> X -> Vec n
vec  zero   _ = nil
vec (suc n) x = x :: vec n x

map : {n:Nat} -> (X -> X) -> Vec n -> Vec n
map {zero}  f (vecI nil_)	  = nil
map {suc n} f (vecI (cons_ x xs)) = f x :: map f xs

(!) : {n:Nat} -> Vec n -> Fin n -> X
(!) {suc n} (vecI (cons_ x _ )) (finI fzero_)    = x
(!) {suc n} (vecI (cons_ _ xs)) (finI (fsuc_ i)) = xs ! i

upd : {n:Nat} -> Fin n -> X -> Vec n -> Vec n
upd {suc n} (finI fzero_)    x (vecI (cons_ _ xs)) = x :: xs
upd {suc n} (finI (fsuc_ i)) x (vecI (cons_ y xs)) = y :: upd i x xs

tabulate : {n:Nat} -> (Fin n -> X) -> Vec n
tabulate {zero}  f = nil
tabulate {suc n} f = f fzero :: tabulate (\x -> f (fsuc x))

postulate
  (===) : {n:Nat} -> Vec n -> Vec n -> Prop

module Proof
    (F : {n:Nat} -> Vec n -> Vec n)
    -- and axioms...
    where

  stepF : {n:Nat} -> Fin n -> Vec n -> Vec n
  stepF i xs = upd i (F xs ! i) xs

  unsafeF' : {n:Nat} -> Nat -> Vec (suc n) -> Vec (suc n)
  unsafeF' zero    = id
  unsafeF' (suc m) = unsafeF' m ∘ stepF fzero

  unsafeF : {n:Nat} -> Vec n -> Vec n
  unsafeF {zero}  = id
  unsafeF {suc n} = unsafeF' (suc n)

  thm : {n:Nat} -> (xs:Vec n) -> F xs === unsafeF xs
  thm = ?

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module BTA4 where
-- specialize two-level typed terms to untyped lambda calculus

open import Data.Nat hiding (_<_)
open import Data.Bool
open import Data.Fin hiding (_≤_ ; pred; _+_)
open import Data.List
open import Data.Product

open import Function
open import Algebra.FunctionProperties using (Commutative; Identity; RightIdentity)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning
open import Data.Nat.Properties

open import Relation.Nullary

-- Binding times
data BT : Set where
  S : BT
  D : BT

-- defining a data type [BT],where two members are
-- [S] standing for "static" and [D] standing for dynamic.

-- ``subsumption'' binding times; static can be treated as dynamic,
-- but not vice versa
_≼_ : BT → BT → Bool
_≼_ D S  = false
_≼_ _ _  = true

record True : Set where
data False : Set where

isTrue : Bool → Set
isTrue true  = True
isTrue false = False

-- an inductive type describing bt subsumption
data _⊑_ : BT → BT → Set where
  bt-leq-refl : ∀ {bt} → bt ⊑ bt
  bt-leq-dyn  : ∀ {bt} → bt ⊑ D

bt-reify : ∀ bt1 bt2 → isTrue (bt1 ≼ bt2) → bt1 ⊑ bt2
bt-reify S S p = bt-leq-refl
bt-reify S D p = bt-leq-dyn
bt-reify D S ()
bt-reify D D p = bt-leq-refl

bt-reflect : ∀ bt1 bt2 → bt1 ⊑ bt2 → isTrue (bt1 ≼ bt2)
bt-reflect S S p = _
bt-reflect S D p = _
bt-reflect D S ()
bt-reflect D D p = _

-- More general purpose definitions (should also be in standard library)
-- list membership
infix 4 _∈_
data _∈_ {A : Set} : A → List A → Set where
  hd : ∀ {x xs} → x ∈ (x ∷ xs)
  tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

-- Types of the calculus
mutual
  -- s ^ BT
  data AType : Set where
    Ann : BT → SType → AType

  -- int | t -> t
  data SType : Set where
    SInt  : SType
    SFun  : AType → AType → SType

-- aux definitions
ATInt : BT → AType
ATInt bt = Ann bt SInt
ATFun  : BT → AType → AType → AType
ATFun  bt at1 at2 = Ann bt (SFun at1 at2)

-- projection: get the BT from a type
btof : AType → BT
btof (Ann bt _) = bt

-- an alternative: have only wf types from the start
data AType' : BT → Set where
  AInt : (bt : BT) → AType' bt
  AFun : (bt : BT) → ∀ {bt1 bt2} → AType' bt1 → AType' bt2 → bt ⊑ bt1 → bt ⊑ bt2 → AType' bt

forget-wft : ∀ {bt} → AType' bt → AType
forget-wft {bt} (AInt .bt) = ATInt bt
forget-wft {bt} (AFun .bt at at₁ x x₁) = ATFun bt (forget-wft at) (forget-wft at₁)

data LEQ-Problem : Set where
  LEQ-not-D⊑S : LEQ-Problem

data WF-Problem : Set where
  WF-LEQ-right : LEQ-Problem → WF-Problem
  WF-LEQ-left : LEQ-Problem → WF-Problem
  WF-WF-left : WF-Problem → WF-Problem
  WF-WF-right : WF-Problem → WF-Problem

data Inferred (E A : Set) : Set where
  Ok : A → Inferred E A
  Error : E → Inferred E A

infer-bt-leq : ∀ bt1 bt2 → Inferred LEQ-Problem (bt1 ⊑ bt2)
infer-bt-leq S S = Ok bt-leq-refl
infer-bt-leq S D = Ok bt-leq-dyn
infer-bt-leq D S = Error LEQ-not-D⊑S
infer-bt-leq D D = Ok bt-leq-refl

-- insufficiently constrained ...
infer-wft' : (α : AType) → Inferred WF-Problem (AType' (btof α))
infer-wft' (Ann x SInt) = Ok (AInt x)
infer-wft' (Ann x (SFun x₁ x₂)) with infer-wft' x₁ | infer-wft' x₂ | infer-bt-leq x (btof x₁) | infer-bt-leq x (btof x₂)
infer-wft' (Ann x₄ (SFun x₁ x₂)) | Ok x | Ok x₃ | Ok x₅ | Ok x₆ = Ok (AFun x₄ x x₃ x₅ x₆)
infer-wft' (Ann x₄ (SFun x₁ x₂)) | Ok x | Ok x₃ | Ok x₅ | Error x₆ = Error (WF-LEQ-right x₆)
infer-wft' (Ann x₄ (SFun x₁ x₂)) | Ok x | Ok x₃ | Error x₅ | okbt2 = Error (WF-LEQ-left x₅)
infer-wft' (Ann x₄ (SFun x₁ x₂)) | Ok x | Error x₃ | _ | _ = Error (WF-WF-right x₃)
infer-wft' (Ann x₃ (SFun x₁ x₂)) | Error x | r2 | _ | _ = Error (WF-WF-left x)

-- might be easier to infer a Σ type
check-wft : (α : AType) → Inferred WF-Problem (∃ λ α' → α ≡ forget-wft {btof α} α')
check-wft (Ann x SInt) = Ok (AInt x , refl)
check-wft (Ann x (SFun x₁ x₂)) with check-wft x₁ | check-wft x₂ | infer-bt-leq x (btof x₁) | infer-bt-leq x (btof x₂)
... | Ok (α₁ , pr₁) | Ok (α₂ , pr₂) | Ok leq₁ | Ok leq₂ = Ok (AFun x α₁ α₂ leq₁ leq₂ , cong₂ (λ x₃ x₄ → Ann x (SFun x₃ x₄)) pr₁ pr₂)
... | Ok p₁ | Ok p₂ | Ok leq₁ | Error e₄ = Error (WF-LEQ-right e₄)
... | Ok p₁ | Ok p₂ | Error e₃ | _ = Error (WF-LEQ-left e₃)
... | Ok p₁ | Error e₂ | _ | _ = Error (WF-WF-right e₂)
... | Error e₁ | _ | _ | _ = Error (WF-WF-left e₁)

unfold-forget : ∀ bt {bt₁} {bt₂} at₁ at₂ x₅ x₆ →
  forget-wft (AFun bt  {bt₁} {bt₂} at₁ at₂ x₅ x₆) ≡ ATFun bt (forget-wft at₁) (forget-wft at₂)
unfold-forget bt at₁ at₂ x₅ x₆ = refl

-- well-formedness
data wft : AType → Set where
  wf-int  : ∀ {bt} → wft (Ann bt SInt)
  wf-fun  : ∀ {bt at1 at2} → wft at1 → wft at2
          → isTrue (bt ≼ btof at1) → isTrue (bt ≼ btof at2) → wft (Ann bt (SFun at1 at2))

infer-lemma-fun-left : ∀ σ₁ α₂ → ¬ wft (Ann D (SFun (Ann S σ₁) α₂))
infer-lemma-fun-left σ₁ α₂ (wf-fun v v₁ () x₁)

infer-lemma-fun-right : ∀ α σ → ¬ wft (Ann D (SFun α (Ann S σ)))
infer-lemma-fun-right α σ (wf-fun v v₁ x ())

infer-yes-yes : ∀ bt α₁ α₂ → (wf1 : wft α₁) (wf2 : wft α₂) → Dec (wft (Ann bt (SFun α₁ α₂)))
infer-yes-yes S (Ann bt1 σ₁) (Ann bt2 σ₂) wf1 wf2 = yes (wf-fun wf1 wf2 _ _)
infer-yes-yes D (Ann D σ₁) (Ann D σ₂) wf1 wf2     = yes (wf-fun wf1 wf2 _ _)
infer-yes-yes D (Ann S σ₁) (Ann bt2 σ₂) wf1 wf2   = no (infer-lemma-fun-left σ₁ (Ann bt2 σ₂))
infer-yes-yes D (Ann bt1 σ₁) (Ann S σ₂) wf1 wf2   = no (infer-lemma-fun-right (Ann bt1 σ₁) σ₂)

infer-lemma-arg-left : ∀ bt α₁ α₂ → ¬ wft α₁ → ¬ wft (Ann bt (SFun α₁ α₂))
infer-lemma-arg-left bt α₁ α₂ ¬wft1 (wf-fun v v₁ x x₁) = ¬wft1 v

infer-lemma-arg-right : ∀ bt α₁ α₂ → ¬ wft α₂ → ¬ wft (Ann bt (SFun α₁ α₂))
infer-lemma-arg-right bt α₁ α₂ ¬wft2 (wf-fun v v₁ x x₁) = ¬wft2 v₁

infer-wft : (α : AType) → Dec (wft α)
infer-wft (Ann bt SInt) = yes wf-int
infer-wft (Ann bt (SFun α₁ α₂))
  with infer-wft α₁ | infer-wft α₂
... | yes wf1 | yes wf2 = infer-yes-yes bt α₁ α₂ wf1 wf2
... | yes wf1 | no ¬wf2 = no (infer-lemma-arg-right bt α₁ α₂ ¬wf2)
... | no ¬wf1 | yes wf2 = no (infer-lemma-arg-left bt α₁ α₂ ¬wf1)
... | no ¬wf1 | no ¬wf2 = no (infer-lemma-arg-left bt α₁ α₂ ¬wf1)

----------------------------------------------------------------------
-- step 0
-- Untyped expressions, incorrect results
data Exp : Set where
  EVar : ℕ → Exp
  EInt : ℕ → Exp
  EAdd : Exp → Exp → Exp
  ELam : Exp → Exp
  EApp : Exp → Exp → Exp

-- mapping from annotated type to implementation type
ImpTA : AType → Set
ImpTA (Ann S SInt) = ℕ
ImpTA (Ann S (SFun α β)) = ImpTA α → ImpTA β
ImpTA (Ann D σ) = Exp

-- test for dynamic by wellformedness
data IsDynamic : AType → Set where
  is-dyn : ∀ σ → IsDynamic (Ann D σ)

lem-IsDynamic-by-wf : ∀ α → isTrue (D ≼ btof α) → IsDynamic α
lem-IsDynamic-by-wf (Ann S σ) ()
lem-IsDynamic-by-wf (Ann D σ) _ = is-dyn σ

-- typed annotated expressions
ACtx = List AType

data AExp (Δ : ACtx) : AType → Set where
  AVar : ∀ {α} → α ∈ Δ → AExp Δ α
  AInt : (bt : BT) → ℕ → AExp Δ (ATInt bt)
  AAdd : (bt : BT) → AExp Δ (ATInt bt) → AExp Δ (ATInt bt) → AExp Δ (ATInt bt)
  ALam : ∀ {α₁ α₂} (bt : BT) → wft (ATFun bt α₂ α₁) → AExp (α₂ ∷ Δ) α₁ → AExp Δ (ATFun bt α₂ α₁)
  AApp : ∀ {α₁ α₂} (bt : BT) → wft (ATFun bt α₂ α₁) → AExp Δ (ATFun bt α₂ α₁) → AExp Δ α₂ → AExp Δ α₁

-- TODO: replace wellformedness of types in AApp with lemma
-- the lemma does not require wft in AApp
data wft-context : ACtx → Set where
  wft-[] : wft-context []
  wft-:: : ∀ {α Δ} → wft α → wft-context Δ → wft-context (α ∷ Δ)

lemma-wft-var : ∀ {α Δ} → wft-context Δ → α ∈ Δ → wft α
lemma-wft-var (wft-:: x wc) hd = x
lemma-wft-var (wft-:: x wc) (tl pf) = lemma-wft-var wc pf

lemma-wft : ∀ {α Δ} → wft-context Δ → AExp Δ α → wft α
lemma-wft wc (AVar x) = lemma-wft-var wc x
lemma-wft wc (AInt bt x) = wf-int
lemma-wft wc (AAdd bt ae₁ ae₂) = wf-int
lemma-wft wc (ALam bt x ae) = x
lemma-wft wc (AApp bt _ ae ae₁)
  with lemma-wft wc ae
... | (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) = w₂

data AEnv0 (F : AType → Set) : ACtx -> Set where
  AE[] : AEnv0 F []
  AE∷  : ∀ {Δ} α → F α → AEnv0 F Δ → AEnv0 F (α ∷ Δ)

AEnv = AEnv0 ImpTA

aelength : ∀ {F Δ} → AEnv0 F Δ → ℕ
aelength AE[] = 0
aelength (AE∷ α x ae) = suc( aelength ae)

lookup : ∀ {F Δ α} → AEnv0 F Δ → (o : α ∈ Δ ) → F α
lookup (AE∷ α x env) hd = x
lookup (AE∷ α x env) (tl o) = lookup env o

-- partial evaluation
peval : ∀ {α Δ } → AExp Δ α → AEnv Δ → ImpTA α
peval (AVar x) env = lookup env x
peval (AInt S x) env = x
peval (AInt D x) env = EInt x
peval (AAdd S e₁ e₂) env = peval e₁ env + peval e₂ env
peval (AAdd D e₁ e₂) env = EAdd (peval e₁ env) (peval e₂ env)
peval (ALam {α₂} {α₁} S w e) env = λ y → peval e (AE∷ α₁ y env)
peval (ALam {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
peval (ALam {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun _ _ d≤bt₁ d≤bt₂) e) env
  | is-dyn σ₁ | is-dyn σ₂ = ELam (peval e (AE∷ (Ann D σ₁) (EVar (aelength env)) env))
peval (AApp S w e e₁) env = peval e env (peval e₁ env)
peval (AApp {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e e₁) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
peval (AApp {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun _ _ d≤bt₁ d≤bt₂) e e₁) env
  | is-dyn σ₁ | is-dyn σ₂ = EApp (peval e env) (peval e₁ env)

----------------------------------------------------------------------
-- step 1
-- Untyped expression, but correctly scoped
data Exp' : ℕ → Set where
  EVar : ∀ {n} → Fin n → Exp' n
  EInt : ∀ {n} → ℕ → Exp' n
  EAdd : ∀ {n} → Exp' n → Exp' n → Exp' n
  ELam : ∀ {n} → Exp' (suc n) → Exp' n
  EApp : ∀ {n} → Exp' n → Exp' n → Exp' n

---

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero    n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

n+0≡n : ∀ n → n + 0 ≡ n
n+0≡n zero    = refl
n+0≡n (suc n) = cong suc $ n+0≡n n

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

≤-refl : ∀ {n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀ {a b c} → a ≤ b → b ≤ c → a ≤ c
≤-trans z≤n q = z≤n
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

≤-suc-right : ∀ {m n} → m ≤ n → m ≤ suc n
≤-suc-right z≤n = z≤n
≤-suc-right (s≤s p) = s≤s (≤-suc-right p)

≤-suc-left : ∀ {m n} → suc m ≤ n → m ≤ n
≤-suc-left (s≤s p) = ≤-suc-right p

xlate : ∀ {m} {n} → Exp' (m + suc n) → Exp' (suc (n + m))
xlate {m} {n} e rewrite m+1+n≡1+m+n m n | +-comm m n = e

shifter1 : ∀ {n} m → Exp' (suc n) → Exp' (suc (n + m))
shifter1 {n} m (EVar x) = xlate {m} (EVar (raise m x))
shifter1 m (EInt x) = EInt x
shifter1 m (EAdd e₁ e₂) = EAdd (shifter1 m e₁) (shifter1 m e₂)
shifter1 m (ELam e) = ELam (shifter1 m e)
shifter1 m (EApp e e₁) = EApp (shifter1 m e) (shifter1 m e₁)

shifter0 : ∀ m → Exp' zero → Exp' m
shifter0 m (EVar ())
shifter0 m (EInt x) = EInt x
shifter0 m (EAdd e₁ e₂) = EAdd (shifter0 m e₁) (shifter0 m e₂)
shifter0 m (ELam e) = ELam (shifter1 m e)
shifter0 m (EApp e e₁) = EApp (shifter0 m e) (shifter0 m e₁)

shifter : ∀ m d → Exp' m → Exp' (m + d)
shifter zero d e = shifter0 d e
shifter (suc m) d e = shifter1 d e

-- m+n∸m≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
-- m+n∸m≡n p

helper : ∀ {m n} → n ≤ m → Exp' (n + (m ∸ n)) → Exp' m
helper p e rewrite m+n∸m≡n p = e

-- index m = nesting level of dynamic definitions
Imp : (m : ℕ) → AType → Set
Imp m (Ann S SInt) = ℕ
Imp m (Ann S (SFun α₁ α₂)) = ∀ n → m ≤ n → (Imp n α₁ → Imp n α₂)
Imp m (Ann D σ) = Exp' m

-- index = nesting level of dynamic definitions
data AEnv1 : ℕ → ACtx → Set where
  [] : AEnv1 0 []
  consS : ∀ {m Δ o} → m ≤ o → (α : AType) → Imp o α → AEnv1 m Δ → AEnv1 o (α ∷ Δ)
  consD : ∀ {m Δ} → (α : AType) → isTrue (D ≼ btof α) → Imp (suc m) α → AEnv1 m Δ → AEnv1 (suc m) (α ∷ Δ)

lift1 : ∀ {m n} α → m ≤ n → Imp m α → Imp n α
lift1 (Ann S SInt) p v = v
lift1 (Ann S (SFun x x₁)) p v = λ k n≤k → v k (≤-trans p n≤k)
lift1 {m} {n} (Ann D σ) p v = helper p (shifter m (n ∸ m) v)

lookup1 : ∀ {α Δ m n} → m  ≤ n → AEnv1 m Δ → α ∈ Δ → Imp n α
lookup1 {α} p (consS _ .α x env) hd = lift1 α p x
lookup1 {α} p (consD .α x x₁ env) hd = lift1 α p x₁
lookup1 p (consS p' .y x env) (tl {_} {y} x₁) = lookup1 (≤-trans p' p) env x₁
lookup1 p (consD .y x x₁ env) (tl {_} {y} x₂) = lookup1 (≤-suc-left p) env x₂

pe1 : ∀ {α Δ} m → AExp Δ α → AEnv1 m Δ → Imp m α
pe1 m (AVar x) env = lookup1 ≤-refl env x
pe1 m (AInt S x) env = x
pe1 m (AInt D x) env = EInt x
pe1 m (AAdd S e₁ e₂) env = pe1 m e₁ env + pe1 m e₂ env
pe1 m (AAdd D e₁ e₂) env = EAdd (pe1 m e₁ env) (pe1 m e₂ env)
pe1 m (ALam S x e) env = λ o p → λ v → pe1 o e (consS p _ v env)
pe1 m (ALam {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
pe1 m (ALam {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun _ _ d≤bt₁ d≤bt₂) e) env
  | is-dyn σ₁ | is-dyn σ₂ = ELam (pe1 (suc m) e (consD (Ann D σ₁) d≤bt₁ (EVar zero) env))
pe1 m (AApp S x e e₁) env = (pe1 m e env) m ≤-refl (pe1 m e₁ env)
pe1 m (AApp {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e e₁) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
pe1 m (AApp {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e e₁) env
  | is-dyn σ₁ | is-dyn σ₂ = EApp (pe1 m e env) (pe1 m e₁ env)

term1 : AExp [] (ATInt D)
term1 = AInt D 42

term2 : AExp [] (ATFun D (ATInt D) (ATInt D))
term2 = ALam D (wf-fun wf-int wf-int _ _) (AVar hd)
-- Dλ y → let f = λ x → x D+ y in Dλ z → f z
-- Dλ y → let f = λ x → (Dλ w → x D+ y) in Dλ z → f z
-- Dλ y → (λ f → Dλ z → f z) (λ x → (Dλ w → x D+ y))
-- :: DInt D→ (DT  D→ DInt)
-- y : DInt, f : DInt → (DT  D→ DInt)

term3-0 : AExp (Ann D SInt ∷ Ann D SInt ∷ Ann D SInt ∷ []) (Ann D SInt)
term3-0 = AAdd D (AVar (tl (tl hd))) (AVar (tl hd))

term3-1 : AExp (Ann D SInt ∷ Ann D SInt ∷ []) (Ann D (SFun (Ann D SInt) (Ann D SInt)))
term3-1 = ALam D (wf-fun wf-int wf-int _ _) term3-0

term3-2 : AExp (Ann D SInt ∷ []) (Ann S (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))))
term3-2 = ALam S (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) term3-1

term3-3 : AExp (Ann D SInt ∷ Ann S (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))) ∷ Ann D SInt ∷ [])
               (Ann D (SFun (Ann D SInt) (Ann D SInt)))
term3-3 = AApp S (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) (AVar (tl hd)) (AVar hd)

term3-4 : AExp (Ann S (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))) ∷ Ann D SInt ∷ [])
               (Ann D (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))))
term3-4 = ALam D (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) term3-3

term3-5 : AExp (Ann D SInt ∷ [])
               (Ann S (SFun (Ann S (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))))
                            (Ann D (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))))))
term3-5 = ALam S (wf-fun (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) _ _) term3-4

term3-6 : AExp (Ann D SInt ∷ [])
               (Ann D (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))))
term3-6 = AApp S (wf-fun (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) _ _) term3-5 term3-2

term3 : AExp [] (Ann D (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D (SFun (Ann D SInt) (Ann D SInt)))))))
term3 = ALam D (wf-fun wf-int (wf-fun wf-int (wf-fun wf-int wf-int _ _) _ _) _ _) term3-6

-- conclusion: you want type inference ...

-------------------------------------------------------------------------------
-- step 2
-- now let's do everything typed

data Type : Set where
  Int : Type
  Fun : Type → Type → Type

Ctx = List Type

data _↝_ : Ctx → Ctx → Set where
  ↝-refl   : ∀ {Γ}      → Γ ↝ Γ
  ↝-extend : ∀ {Γ Γ' τ} → Γ ↝ Γ' → Γ ↝ (τ ∷ Γ')

↝-≤ : ∀ Γ Γ' → Γ ↝ Γ' → length Γ ≤ length Γ'
↝-≤ .Γ' Γ' ↝-refl = ≤-refl
↝-≤ Γ .(τ ∷ Γ') (↝-extend {.Γ} {Γ'} {τ} Γ↝Γ') = ≤-suc-right (↝-≤ Γ Γ' Γ↝Γ')

↝-no-left : ∀ Γ τ → ¬ (τ ∷ Γ) ↝ Γ
↝-no-left Γ τ p = 1+n≰n (↝-≤ (τ ∷ Γ) Γ p)

↝-trans : ∀ {Γ Γ' Γ''} → Γ ↝ Γ' → Γ' ↝ Γ'' → Γ ↝ Γ''
↝-trans Γ↝Γ' ↝-refl = Γ↝Γ'
↝-trans Γ↝Γ' (↝-extend Γ'↝Γ'') = ↝-extend (↝-trans Γ↝Γ' Γ'↝Γ'')

lem : ∀ x y xs xs' → (x ∷ xs) ↝ xs' → xs ↝ (y ∷ xs')
lem x y xs .(x ∷ xs) ↝-refl = ↝-extend (↝-extend ↝-refl)
lem x y xs .(x' ∷ xs') (↝-extend {.(x ∷ xs)} {xs'} {x'} p) = ↝-extend (lem x x' xs xs' p)

data _↝_↝_ : Ctx → Ctx → Ctx → Set where
  ↝↝-base   : ∀ {Γ Γ''} → Γ ↝ Γ'' → Γ ↝ [] ↝ Γ''
  ↝↝-extend : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → (τ ∷ Γ) ↝ (τ ∷ Γ') ↝ (τ ∷ Γ'')

-- Typed residula expressions
data Exp'' (Γ : Ctx) : Type → Set where
  EVar : ∀ {τ} → τ ∈ Γ → Exp'' Γ τ
  EInt : ℕ → Exp'' Γ Int
  EAdd : Exp'' Γ Int → Exp'' Γ Int -> Exp'' Γ Int
  ELam : ∀ {τ τ'} → Exp'' (τ ∷ Γ) τ' → Exp'' Γ (Fun τ τ')
  EApp : ∀ {τ τ'} → Exp'' Γ (Fun τ τ')  → Exp'' Γ τ → Exp'' Γ τ'

-- erase annotations
erase : AType → Type
erase (Ann x SInt) = Int
erase (Ann x (SFun x₁ x₂)) = Fun (erase x₁) (erase x₂)

-- index Γ = nesting level of dynamic definitions / dynamic environment
Imp'' : Ctx → AType → Set
Imp'' Γ (Ann S SInt) = ℕ
Imp'' Γ (Ann S (SFun α₁ α₂)) = ∀ Γ' → Γ ↝ Γ' → (Imp'' Γ' α₁ → Imp'' Γ' α₂)
Imp'' Γ (Ann D σ) = Exp'' Γ (erase (Ann D σ))

-- index = nesting level of dynamic definitions
data AEnv2 : Ctx → ACtx → Set where
  [] : AEnv2 [] []
  consS : ∀ {Γ Δ Γ'} → Γ ↝ Γ' → (α : AType) → Imp'' Γ' α → AEnv2 Γ Δ → AEnv2 Γ' (α ∷ Δ)
  consD : ∀ {Γ Δ} → (α : AType) → isTrue (D ≼ btof α) → Imp'' (erase α ∷ Γ) α → AEnv2 Γ Δ → AEnv2 (erase α ∷ Γ) (α ∷ Δ)

elevate-var : ∀ {Γ Γ' τ} → Γ ↝ Γ' → τ ∈ Γ → τ ∈ Γ'
elevate-var ↝-refl x = x
elevate-var (↝-extend Γ↝Γ') x = tl (elevate-var Γ↝Γ' x)

elevate-var2 : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → τ ∈ Γ → τ ∈ Γ''
elevate-var2 (↝↝-base x) x₁ = elevate-var x x₁
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') hd = hd
elevate-var2 (↝↝-extend Γ↝Γ'↝Γ'') (tl x) = tl (elevate-var2 Γ↝Γ'↝Γ'' x)

elevate : ∀ {Γ Γ' Γ'' τ} → Γ ↝ Γ' ↝ Γ'' → Exp'' Γ τ → Exp'' Γ'' τ
elevate Γ↝Γ'↝Γ'' (EVar x) = EVar (elevate-var2 Γ↝Γ'↝Γ'' x)
elevate Γ↝Γ'↝Γ'' (EInt x) = EInt x
elevate Γ↝Γ'↝Γ'' (EAdd e e₁) = EAdd (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)
elevate Γ↝Γ'↝Γ'' (ELam e) = ELam (elevate (↝↝-extend Γ↝Γ'↝Γ'') e)
elevate Γ↝Γ'↝Γ'' (EApp e e₁) = EApp (elevate Γ↝Γ'↝Γ'' e) (elevate Γ↝Γ'↝Γ'' e₁)

lift2 : ∀ {Γ Γ'} α → Γ ↝ Γ' → Imp'' Γ α → Imp'' Γ' α
lift2 (Ann S SInt) p v = v
lift2 (Ann S (SFun x x₁)) Γ↝Γ' v = λ Γ'' Γ'↝Γ'' → v Γ'' (↝-trans Γ↝Γ' Γ'↝Γ'')
lift2 (Ann D x₁) Γ↝Γ' v = elevate (↝↝-base Γ↝Γ') v

lookup2 : ∀ {α Δ Γ Γ'} → Γ ↝ Γ' → AEnv2 Γ Δ → α ∈ Δ → Imp'' Γ' α
lookup2 Γ↝Γ' (consS p α v env) hd = lift2 α Γ↝Γ' v
lookup2 Γ↝Γ' (consS p α₁ v env) (tl x) = lookup2 (↝-trans p Γ↝Γ') env x
lookup2 Γ↝Γ' (consD α D≼α v env) hd = lift2 α Γ↝Γ' v
lookup2 ↝-refl (consD α₁ D≼α v env) (tl x) = lookup2 (↝-extend ↝-refl) env x
lookup2 (↝-extend Γ↝Γ') (consD α₁ D≼α v env) (tl x) = lookup2 (lem (erase α₁) _ _ _ Γ↝Γ') env x

pe2 : ∀ {α Δ} Γ → AExp Δ α → AEnv2 Γ Δ → Imp'' Γ α
pe2 Γ (AVar x) env = lookup2 ↝-refl env x
pe2 Γ (AInt S x) env = x
pe2 Γ (AInt D x) env = EInt x
pe2 Γ (AAdd S e₁ e₂) env = pe2 Γ e₁ env + pe2 Γ e₂ env
pe2 Γ (AAdd D e₁ e₂) env = EAdd (pe2 Γ e₁ env) (pe2 Γ e₂ env)
pe2 {Ann S (SFun α₂ α₁)} Γ (ALam .S w e) env = λ Γ' Γ↝Γ' → λ y → pe2 {α₁} Γ' e (consS Γ↝Γ' α₂ y env)
pe2 Γ (ALam {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
pe2 Γ (ALam {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun _ _ d≤bt₁ d≤bt₂) e) env
  | is-dyn σ₁ | is-dyn σ₂ = ELam (pe2 (erase (Ann D σ₁) ∷ Γ) e (consD (Ann D σ₁) d≤bt₁ (EVar hd) env))
pe2 Γ (AApp S w e₁ e₂) env = pe2 Γ e₁ env Γ ↝-refl (pe2 Γ e₂ env)
pe2 Γ (AApp {α₂} {α₁} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e e₁) env
  with lem-IsDynamic-by-wf α₁ d≤bt₁ | lem-IsDynamic-by-wf α₂ d≤bt₂
pe2 Γ (AApp {.(Ann D σ₂)} {.(Ann D σ₁)} D (wf-fun w₁ w₂ d≤bt₁ d≤bt₂) e e₁) env
  | is-dyn σ₁ | is-dyn σ₂ = EApp (pe2 Γ e env) (pe2 Γ e₁ env)

pe2-term1 = pe2 [] term1 []
pe2-term2 = pe2 [] term2 []
pe2-term3 = pe2 [] term3 []

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some defined operations (multiplication by natural number and
-- exponentiation)
------------------------------------------------------------------------

open import Algebra

module Algebra.Operations {s₁ s₂} (S : Semiring s₁ s₂) where

open Semiring S renaming (zero to *-zero)
open import Data.Nat
  using (zero; suc; ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Product using (module Σ)
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
import Relation.Binary.EqReasoning as EqR
open EqR setoid

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

-- Multiplication by natural number.

infixr 7 _×_

_×_ : ℕ → Carrier → Carrier
0     × x = 0#
suc n × x = x + n × x

-- A variant that includes a "redundant" case which ensures that 1 × y
-- is definitionally equal to y.

_×′_ : ℕ → Carrier → Carrier
0     ×′ x = 0#
1     ×′ x = x
suc n ×′ x = x + n ×′ x

-- Exponentiation.

infixr 8 _^_

_^_ : Carrier → ℕ → Carrier
x ^ zero  = 1#
x ^ suc n = x * x ^ n

------------------------------------------------------------------------
-- Some properties

-- Unfolding lemma for _×′_.

1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x
1+×′ 0 x = begin
  x       ≈⟨ sym $ Σ.proj₂ +-identity x ⟩
  x + 0#  ∎
1+×′ (suc n) x = begin
  x + suc n ×′ x  ≡⟨⟩
  x + suc n ×′ x  ∎

-- _×_ and _×′_ are extensionally equal (up to the setoid
-- equivalence).

×≈×′ : ∀ n x → n × x ≈ n ×′ x
×≈×′ 0       x = begin 0# ∎
×≈×′ (suc n) x = begin
  x + n × x   ≈⟨ +-cong refl (×≈×′ n x) ⟩
  x + n ×′ x  ≈⟨ sym $ 1+×′ n x ⟩
  suc n ×′ x  ∎

-- _×_ is homomorphic with respect to _ℕ+_/_+_.

×-homo-+ : ∀ c m n → (m ℕ+ n) × c ≈ m × c + n × c
×-homo-+ c 0 n = begin
  n × c       ≈⟨ sym $ Σ.proj₁ +-identity (n × c) ⟩
  0# + n × c  ∎
×-homo-+ c (suc m) n = begin
  c + (m ℕ+ n) × c     ≈⟨ +-cong refl (×-homo-+ c m n) ⟩
  c + (m × c + n × c)  ≈⟨ sym $ +-assoc c (m × c) (n × c) ⟩
  c + m × c + n × c    ∎

-- _×′_ is homomorphic with respect to _ℕ+_/_+_.

×′-homo-+ : ∀ c m n → (m ℕ+ n) ×′ c ≈ m ×′ c + n ×′ c
×′-homo-+ c m n = begin
  (m ℕ+ n) ×′ c    ≈⟨ sym $ ×≈×′ (m ℕ+ n) c ⟩
  (m ℕ+ n) ×  c    ≈⟨ ×-homo-+ c m n ⟩
  m ×  c + n ×  c  ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩
  m ×′ c + n ×′ c  ∎

-- _× 1# is homomorphic with respect to _ℕ*_/_*_.

×1-homo-* : ∀ m n → (m ℕ* n) × 1# ≈ (m × 1#) * (n × 1#)
×1-homo-* 0 n = begin
  0#             ≈⟨ sym $ Σ.proj₁ *-zero (n × 1#) ⟩
  0# * (n × 1#)  ∎
×1-homo-* (suc m) n = begin
  (n ℕ+ m ℕ* n) × 1#                   ≈⟨ ×-homo-+ 1# n (m ℕ* n) ⟩
  n × 1# + (m ℕ* n) × 1#               ≈⟨ +-cong refl (×1-homo-* m n) ⟩
  n × 1# + (m × 1#) * (n × 1#)         ≈⟨ sym $ +-cong (Σ.proj₁ *-identity (n × 1#)) refl ⟩
  1# * (n × 1#) + (m × 1#) * (n × 1#)  ≈⟨ sym $ Σ.proj₂ distrib (n × 1#) 1# (m × 1#) ⟩
  (1# + m × 1#) * (n × 1#)             ∎

-- _×′ 1# is homomorphic with respect to _ℕ*_/_*_.

×′1-homo-* : ∀ m n → (m ℕ* n) ×′ 1# ≈ (m ×′ 1#) * (n ×′ 1#)
×′1-homo-* m n = begin
  (m ℕ* n) ×′ 1#         ≈⟨ sym $ ×≈×′ (m ℕ* n) 1# ⟩
  (m ℕ* n) ×  1#         ≈⟨ ×1-homo-* m n ⟩
  (m ×  1#) * (n ×  1#)  ≈⟨ *-cong (×≈×′ m 1#) (×≈×′ n 1#) ⟩
  (m ×′ 1#) * (n ×′ 1#)  ∎

-- _×_ preserves equality.

×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
×-cong {n} {n′} {x} {x′} n≡n′ x≈x′ = begin
  n  × x   ≈⟨ reflexive $ PropEq.cong (λ n → n × x) n≡n′ ⟩
  n′ × x   ≈⟨ ×-congʳ n′ x≈x′ ⟩
  n′ × x′  ∎
  where
  ×-congʳ : ∀ n → (_×_ n) Preserves _≈_ ⟶ _≈_
  ×-congʳ 0       x≈x′ = refl
  ×-congʳ (suc n) x≈x′ = x≈x′ ⟨ +-cong ⟩ ×-congʳ n x≈x′

-- _×′_ preserves equality.

×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
×′-cong {n} {n′} {x} {x′} n≡n′ x≈x′ = begin
  n  ×′ x   ≈⟨ sym $ ×≈×′ n x ⟩
  n  ×  x   ≈⟨ ×-cong n≡n′ x≈x′ ⟩
  n′ ×  x′  ≈⟨ ×≈×′ n′ x′ ⟩
  n′ ×′ x′  ∎

-- _^_ preserves equality.

^-cong : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
^-cong {x} {x'} {n} {n'} x≈x' n≡n' = begin
  x  ^ n   ≈⟨ reflexive $ PropEq.cong (_^_ x) n≡n' ⟩
  x  ^ n'  ≈⟨ ^-congˡ n' x≈x' ⟩
  x' ^ n'  ∎
  where
  ^-congˡ : ∀ n → (λ x → x ^ n) Preserves _≈_ ⟶ _≈_
  ^-congˡ zero    x≈x' = refl
  ^-congˡ (suc n) x≈x' = x≈x' ⟨ *-cong ⟩ ^-congˡ n x≈x'


text:
module New.Types where

open import Data.Integer public
open import Data.Product public hiding (map)
open import Data.Sum public hiding (map)
infixr 5 _⇒_

data Type : Set where
  _⇒_ : (σ τ : Type) → Type
  int : Type
  pair : (σ τ : Type) → Type
  sum : (σ τ : Type) → Type

⟦_⟧Type : Type → Set
⟦ σ ⇒ τ ⟧Type = ⟦ σ ⟧Type → ⟦ τ ⟧Type
⟦ int ⟧Type = ℤ
⟦ pair σ τ ⟧Type = ⟦ σ ⟧Type × ⟦ τ ⟧Type
⟦ sum σ τ ⟧Type = ⟦ σ ⟧Type ⊎ ⟦ τ ⟧Type

Δt : Type → Type
Δt (σ ⇒ τ) = σ ⇒ Δt σ ⇒ Δt τ
Δt int = int
Δt (pair σ τ) = pair (Δt σ) (Δt τ)
Δt (sum σ τ) = sum (sum (Δt σ) (Δt τ)) (sum σ τ)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.CommRingAsAlmostRing where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.CommRing.Base
open import Cubical.Algebra.RingSolver.AlmostRing
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring.Base
open import Cubical.Algebra.Ring.Properties

private
  variable
    ℓ : Level

open Cubical.Algebra.Ring.Properties.Theory

CommRingAsAlmostRing : CommRing {ℓ} → AlmostRing {ℓ}
CommRingAsAlmostRing {ℓ}
  (R , commringstr _ _ _ _ _
         (iscommring (isring
                       (isabgroup (isgroup +-isMonoid inverse) +-comm)
                       ·-isMonoid dist)
                     ·-comm)) =
  let
    R' : CommRing {ℓ}
    R' = (R , commringstr _ _ _ _ _
         (iscommring (isring
                       (isabgroup (isgroup +-isMonoid inverse) +-comm) ·-isMonoid dist)
                     ·-comm))
    R″ = CommRing→Ring R'
  in almostring R _ _ _ _ _
     (isalmostring
       +-isMonoid
       ·-isMonoid
       +-comm
       ·-comm
       (λ x y z → fst (dist x y z))
       (λ x y z → snd (dist x y z))
       (λ x y → sym (-DistL· R″ x y))
       (λ x y → sym (-Dist R″ x y))
       (λ x → 0LeftAnnihilates R″ x)
       λ x → 0RightAnnihilates R″ x)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Yamanote where

open import Data.Fin
open import Data.List using (List; map) renaming (_∷_ to _L∷_; _++_ to _L++_; [] to L[])
open import Data.Maybe using (fromMaybe)
open import Data.Nat
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Function using (_∘_)
open import Data.Vec using (Vec; []; _∷_; zip; toList) renaming (map to vmap)

open import Relation.Binary.PropositionalEquality using (refl)

open import Counterpoint
open import Note
open import Music
open import MidiEvent
open import Pitch
open import Interval
-- open import ScaleDegree
open import Util

-- Yamanoto melody transposed down an octave and with an additional d6 at the end.
cantusFirmus : Vec Pitch 40
cantusFirmus =
        g 4  ∷ a 4 ∷ g 4 ∷ c 5 ∷ g 4 ∷ e 5 ∷ g 4 ∷
  g 5 ∷ g 4  ∷ a 4 ∷ g 4 ∷ c 5 ∷ g 4 ∷ e 5 ∷ g 4 ∷
  g 5 ∷ g 4  ∷ a 4 ∷ g 4 ∷ b 4 ∷ g 4 ∷ d 5 ∷ g 4 ∷
  g 5 ∷ g 4  ∷ a 4 ∷ g 4 ∷ b 4 ∷ g 4 ∷ d 5 ∷ g 4 ∷
  g 4 ∷ e 4  ∷ g 4 ∷ c 5 ∷ c 5 ∷ c 5 ∷ e 5 ∷ g 5 ∷
  d 6 ∷ []

-- Counterpoint (composed on Aug 2, 2019)
counterpoint : Vec Upi 40
counterpoint =
         maj6 ∷ min6 ∷ per8 ∷ maj3 ∷ per8 ∷ min3 ∷ maj6 ∷
  maj6 ∷ maj6 ∷ min3 ∷ per5 ∷ maj3 ∷ maj6 ∷ min3 ∷ per8 ∷
  maj3 ∷ maj10 ∷ per8 ∷ maj10 ∷ min6 ∷ per8 ∷ maj6 ∷ maj10 ∷
  maj3 ∷ maj3 ∷ min3 ∷ per5 ∷ min6 ∷ maj6 ∷ min3 ∷ per8 ∷
  maj6 ∷ min10 ∷ per8 ∷ maj10 ∷ per8 ∷ maj10 ∷ min10 ∷ per8 ∷
  maj6 ∷ []

-- Counterpoint (composed on March 18, 2019)
counterpoint0 : Vec Upi 40
counterpoint0 =
         maj6 ∷ min6 ∷ per8 ∷ maj3 ∷ per8 ∷ min3 ∷ maj6 ∷
  maj6 ∷ maj6 ∷ min3 ∷ per5 ∷ maj3 ∷ maj6 ∷ min3 ∷ per8 ∷
  maj3 ∷ maj10 ∷ per8 ∷ maj10 ∷ min6 ∷ per8 ∷ maj6 ∷ maj10 ∷
  maj3 ∷ maj10 ∷ min6 ∷ per8 ∷ min3 ∷ per8 ∷ min3 ∷ per8 ∷
  maj6 ∷ min10 ∷ per8 ∷ maj10 ∷ per8 ∷ maj10 ∷ min10 ∷ per8 ∷
  maj6 ∷ []

yamanote-cfcp : Vec PitchInterval 40
yamanote-cfcp = zip cantusFirmus counterpoint

fs : FirstSpecies
fs = firstSpecies (g 5 , per8) (toList yamanote-cfcp) (c 6 , per8) refl refl refl refl

yamanote counterp : List Note
yamanote =
  tone 8th (g 5) L∷
  map (tone 8th ∘ proj₁ ∘ pitchIntervalToPitchPair) (FirstSpecies.middleBars fs) L++
  tone 8th (g 5) L∷
  L[]

counterp =
  tone 8th (g 6) L∷
  map (tone 8th ∘ proj₂ ∘ pitchIntervalToPitchPair) (FirstSpecies.middleBars fs) L++
  tone 8th (c 7) L∷
  L[]

----

piano marimba : InstrumentNumber-1
piano   = # 0
marimba = # 12

channel1 channel2 : Channel-1
channel1 = # 0
channel2 = # 1

tempo : ℕ
tempo = 120

yVelocity cVelocity : Velocity
yVelocity = # 60
cVelocity = # 30

yamanoteTrack : MidiTrack
yamanoteTrack = track "Cantus Firmus" piano channel1 tempo (notes→events yVelocity yamanote)

cpTrack : MidiTrack
cpTrack = track "Counterpoint" marimba channel2 tempo (notes→events cVelocity counterp)

ycpTracks : List MidiTrack
ycpTracks = cpTrack L∷ yamanoteTrack L∷ L[]

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module Examples.InfiniteBind where

open import ActorMonad
open import Prelude

Box : InboxShape
Box = []

binder : ∀ {i} → ∞ActorM i Box ⊤₁ [] (λ _ → [])
binder .force = binder ∞>> binder

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


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

module Miscellaneous.LimNatural where

import      Lvl
open import Numeral.Natural as ℕ using (ℕ)
open import Numeral.Sign as Sign using (−|+ ; −|0|+ ; ➖ ; ➕)
open import Type.Cubical
open import Type.Cubical.Path.Equality
open import Type

data ℕ∞ : Type{Lvl.𝟎} where
  𝟎 : ℕ∞
  𝐒 : ℕ∞ → ℕ∞
  ∞ : ℕ∞
  𝐒-fixpoint : (𝐒(∞) ≡ ∞)

𝐏₀ : ℕ∞ → ℕ∞
𝐏₀(𝟎)    = 𝟎
𝐏₀(𝐒(n)) = n
𝐏₀(∞)    = ∞
𝐏₀(𝐒-fixpoint i) = ∞

_+_ : ℕ∞ → ℕ∞ → ℕ∞
x + 𝟎    = x
x + 𝐒(y) = 𝐒(x + y)
_ + ∞    = ∞
x + 𝐒-fixpoint i = 𝐒-fixpoint i

_⋅_ : ℕ∞ → ℕ∞ → ℕ∞
x ⋅ 𝟎    = 𝟎
x ⋅ 𝐒(y) = x + (x ⋅ y)
x ⋅ ∞    = ∞
x ⋅ 𝐒-fixpoint i = ∞

infixl 10010 _+_
infixl 10020 _⋅_

open import Structure.Function.Domain
open import Structure.Function
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type.Cubical.Path.Proofs

private variable x y z : ℕ∞

𝐒-∞-involutive : (𝐒(𝐒(∞)) ≡ ∞)
𝐒-∞-involutive = congruence₁(𝐒) 𝐒-fixpoint 🝖 𝐒-fixpoint

instance
  𝐒-injectivity : Injective(𝐒)
  Injective.proof 𝐒-injectivity = congruence₁(𝐏₀)

[+]-baseₗ : (𝟎 + x ≡ x)
[+]-baseₗ {𝟎}   = reflexivity(_≡_)
[+]-baseₗ {𝐒 x} = congruence₁(𝐒) ([+]-baseₗ {x})
[+]-baseₗ {∞}   = reflexivity(_≡_)
[+]-baseₗ {𝐒-fixpoint i} = reflexivity(_≡_) {𝐒-fixpoint i}

[+]-stepₗ : (𝐒(x) + y ≡ 𝐒(x + y))
[+]-stepₗ {x} {𝟎}   = reflexivity(_≡_)
[+]-stepₗ {x} {𝐒 y} = congruence₁(𝐒) ([+]-stepₗ {x}{y})
[+]-stepₗ {x} {∞}   = symmetry(_≡_) 𝐒-fixpoint
[+]-stepₗ {x} {𝐒-fixpoint i} = symmetry(_≡_) (Interval.hComp diagram {!!}) where
  diagram : Interval → Interval.Partial(Interval.farBound i) _
  diagram _ (i = Interval.𝟎) = congruence₁(𝐒) 𝐒-fixpoint
  diagram _ (i = Interval.𝟏) = 𝐒-fixpoint
  {-
  i0 j0 𝐒∞
  i0 j1 𝐒𝐒∞
  i1 j0 ∞
  i1 j1 𝐒∞
  -}
  -- test : ∀{i} → (𝐒(𝐒-fixpoint i) ≡ 𝐒-fixpoint i)
  -- test {i} j = {!!}
  {-
  i0 j0 𝐒𝐒∞
  i0 j1 𝐒∞
  i1 j0 𝐒∞
  i1 j1 ∞
  -}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Id

reflPath : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≡ x
reflPath {x = x} = λ i → x

reflId : ∀ {ℓ} {A : Set ℓ} {x : A} → Id x x
reflId {x = x} = conid i1 reflPath

Id-comp-Id : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ')
           → (b : P x reflId) → Id (primIdJ P b reflId) b
Id-comp-Id P b = reflId

Id-comp-Path : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ')
             → (b : P x reflId) → (primIdJ P b reflId) ≡ b
Id-comp-Path P b = λ i → b


text:
module Issue246 where

module James where

  data Nat : Set where
    zero  : Nat
    suc   : Nat -> Nat

  data Zero : Set where

  data One : Set where
    void : One

  propLEQ : Nat -> Nat -> Set
  propLEQ zero    _       = One
  propLEQ (suc n) (suc m) = propLEQ n m
  propLEQ (suc n) zero    = Zero

  data Fin : Nat -> Set where
    fzero : {n : Nat} -> Fin (suc n)
    fsuc  : {n : Nat} -> Fin n -> Fin (suc n)

  toFin : {n : Nat} -> (i : Nat) -> (propLEQ (suc i) n) -> Fin n
  toFin {zero}  zero      ()
  toFin {zero}  (suc _)   ()
  toFin {suc n} zero    k  = fzero
  toFin {suc n} (suc i) k  = fsuc (toFin i k)

  one : Nat
  one = suc zero

  two : Nat
  two = suc one

  three : Nat
  three = suc two

  null : Fin three
  null = toFin zero void

module Conor where

  data Nat : Set where
   ze : Nat
   su : Nat -> Nat

  data Bool : Set where
   tt ff : Bool

  record One : Set where
  data Zero : Set where

  So : Bool -> Set
  So tt = One
  So ff = Zero

  _<_ : Nat -> Nat -> Bool
  _ < ze = ff
  ze < su n = tt
  su m < su n = m < n

  data Lt (m n : Nat) : Set where
   lt : So (m < n) -> Lt m n

  boo : {m n : Nat} -> So (m < n) -> Lt (su m) (su n)
  boo p = lt p

module Alan where

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

  {-# BUILTIN NATURAL ℕ #-}
  {-# BUILTIN ZERO zero #-}
  {-# BUILTIN SUC suc #-}

  data Bool : Set where
    true false : Bool

  infixr 5 _∷_

  _lt_ : ℕ → ℕ → Bool
  _     lt zero  = false
  zero  lt suc _ = true
  suc x lt suc y = x lt y

  data List<? (X : ℕ → Set) (n : ℕ) : Bool → Set where
    [] : List<? X n true
    _∷_ : {m : ℕ} → (x : X m) → (List<? X m true) → (List<? X n (m lt n))

  List< : (ℕ → Set) → ℕ → Set
  List< X n = List<? X n true

  data A : ℕ → Set where
    a1 : A 1
    a2 : A 2

  as : List< A 3
  as = a2 ∷ a1 ∷ ([] {A})

  as' : List< A 3
  as' = a2 ∷ a1 ∷ []

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

module FOT.FOTC.Data.Conat.PropertiesI where

open import FOTC.Base
open import FOTC.Data.Conat
open import FOTC.Data.Conat.PropertiesI
open import FOTC.Data.Nat

------------------------------------------------------------------------------
-- 25 April 2014, Failed with --without-K.
--
{-# TERMINATING #-}
Conat→N : ∀ {n} → Conat n → N n
Conat→N Cn with Conat-out Cn
... | inj₁ prf               = subst N (sym prf) nzero
... | inj₂ (n' , refl , Cn') = nsucc (Conat→N Cn')

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --warning=ignore #-}
module Issue2596 where

{-# REWRITE #-}


text:
module Pi-.NoRepeat where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Data.List as L
open import Function using (_∘_)
open import Pi-.Syntax
open import Pi-.Opsem
open import Pi-.AuxLemmas
import RevNoRepeat

-- Forward deterministic
deterministic : ∀ {st st₁ st₂} → st ↦ st₁ → st ↦ st₂ → st₁ ≡ st₂
deterministic (↦⃗₁ {b = b₁}) (↦⃗₁ {b = b₂}) with base-is-prop _ b₁ b₂
... | refl = refl
deterministic ↦⃗₂ ↦⃗₂ = refl
deterministic ↦⃗₃ ↦⃗₃ = refl
deterministic ↦⃗₄ ↦⃗₄ = refl
deterministic ↦⃗₅ ↦⃗₅ = refl
deterministic ↦⃗₆ ↦⃗₆ = refl
deterministic ↦⃗₇ ↦⃗₇ = refl
deterministic ↦⃗₈ ↦⃗₈ = refl
deterministic ↦⃗₉ ↦⃗₉ = refl
deterministic ↦⃗₁₀ ↦⃗₁₀ = refl
deterministic ↦⃗₁₁ ↦⃗₁₁ = refl
deterministic ↦⃗₁₂ ↦⃗₁₂ = refl
deterministic {［ c ∣ _ ∣ κ ］◁} {⟨ _ ∣ v ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］▷} ↦⃖₁ r with Lemma₅ r
... | refl , refl with Lemma₆ r
... | refl , refl with Lemma₇ r
... | refl with v
... | ()
deterministic {［ c ∣ _ ∣ _ ］◁} {⟨ _ ∣ v ∣ _ ⟩◁} {⟨ _ ∣ v' ∣ _ ⟩◁} ↦⃖₁ r with Lemma₁ r
... | refl , refl with Lemma₂ r
deterministic {［ unite₊l  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ y        ∣ κ ⟩◁} {⟨ _ ∣ inj₂ y        ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ uniti₊l  ∣ _ ∣ κ ］◁} {⟨ _ ∣ v             ∣ κ ⟩◁} {⟨ _ ∣ v             ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ swap₊    ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₁ x        ∣ κ ⟩◁} {⟨ _ ∣ inj₁ x        ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ swap₊    ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ y        ∣ κ ⟩◁} {⟨ _ ∣ inj₂ y        ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocl₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₁ x        ∣ κ ⟩◁} {⟨ _ ∣ inj₁ x        ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocl₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₁ x        ∣ κ ⟩◁} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩◁} ↦⃖₁ (() ) | refl , refl | refl , refl
deterministic {［ assocl₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₁ x        ∣ κ ⟩◁} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩◁} ↦⃖₁ (() ) | refl , refl | refl , refl
deterministic {［ assocl₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩◁} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocl₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩◁} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocr₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩◁} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocr₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩◁} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocr₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ z        ∣ κ ⟩◁} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩◁} ↦⃖₁ (() ) | refl , refl | refl , refl
deterministic {［ assocr₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ z        ∣ κ ⟩◁} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩◁} ↦⃖₁ (() ) | refl , refl | refl , refl
deterministic {［ assocr₊  ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ z        ∣ κ ⟩◁} {⟨ _ ∣ inj₂ z        ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ unite⋆l  ∣ _ ∣ κ ］◁} {⟨ _ ∣ (tt , v)      ∣ κ ⟩◁} {⟨ _ ∣ (tt , v)      ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ uniti⋆l  ∣ _ ∣ κ ］◁} {⟨ _ ∣ v             ∣ κ ⟩◁} {⟨ _ ∣ v             ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ swap⋆    ∣ _ ∣ κ ］◁} {⟨ _ ∣ (x , y)       ∣ κ ⟩◁} {⟨ _ ∣ (x , y)       ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocl⋆  ∣ _ ∣ κ ］◁} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩◁} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ assocr⋆  ∣ _ ∣ κ ］◁} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩◁} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ dist     ∣ _ ∣ κ ］◁} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩◁} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ dist     ∣ _ ∣ κ ］◁} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩◁} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ factor   ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩◁} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ factor   ∣ _ ∣ κ ］◁} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩◁} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩◁} ↦⃖₁ ↦⃖₁ | refl , refl | refl , refl = refl
deterministic {［ unite₊l ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ uniti₊l ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ swap₊   ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ assocl₊ ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ assocr₊ ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ unite⋆l ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ uniti⋆l ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ swap⋆   ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ assocl⋆ ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ assocr⋆ ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ dist    ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ factor  ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁ ()
deterministic {［ id↔     ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} (↦⃖₁ {b = ()})
deterministic {［ _ ⨾ _   ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} (↦⃖₁ {b = ()})
deterministic {［ _ ⊕ _   ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} (↦⃖₁ {b = ()})
deterministic {［ _ ⊗ _   ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} (↦⃖₁ {b = ()})
deterministic {［ η₊      ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} (↦⃖₁ {b = ()})
deterministic {［ ε₊      ∣ _ ∣ _ ］◁} {⟨ _ ∣ _ ∣ _ ⟩◁} {［ _ ∣ _ ∣ _ ］◁} (↦⃖₁ {b = ()})
deterministic ↦⃖₂ ↦⃖₂ = refl
deterministic ↦⃖₃ ↦⃖₃ = refl
deterministic ↦⃖₄ ↦⃖₄ = refl
deterministic ↦⃖₅ ↦⃖₅ = refl
deterministic ↦⃖₆ ↦⃖₆ = refl
deterministic ↦⃖₇ ↦⃖₇ = refl
deterministic ↦⃖₈ ↦⃖₈ = refl
deterministic ↦⃖₉ ↦⃖₉ = refl
deterministic ↦⃖₁₀ ↦⃖₁₀ = refl
deterministic {［ c₁ ⊕ c₂ ∣ inj₁ v ∣ κ ］◁} {［ c₁ ∣ v ∣ ☐⊕ c₂ • κ ］◁} {⟨ _ ∣ x ∣ _ ⟩◁} ↦⃖₁₁ r with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with Lemma₃ r
... | inj₂ refl with Lemma₄ r
... | inj₁ ()
... | inj₂ ()
deterministic {［ c₁ ⊕ c₂ ∣ _ ∣ _ ］◁} {［ _ ∣ _ ∣ _ ］◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁₁ ↦⃖₁₁ = refl
deterministic {［ c₁ ⊕ c₂ ∣ inj₂ v ∣ _ ］◁} {［ _ ∣ _ ∣ _ ］◁} {⟨ _ ∣ x ∣ _ ⟩◁} ↦⃖₁₂ r with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with Lemma₃ r
... | inj₂ refl with Lemma₄ r
... | inj₁ ()
... | inj₂ ()
deterministic {［ c₁ ⊕ c₂ ∣ _ ∣ _ ］◁} {［ _ ∣ _ ∣ _ ］◁} {［ _ ∣ _ ∣ _ ］◁} ↦⃖₁₂ ↦⃖₁₂ = refl
deterministic {［ η₊ ∣ inj₁ v ∣ _ ］◁} {［ η₊ ∣ _ ∣ _ ］▷} {［ _ ∣ _ ∣ _ ］▷} ↦η₁ ↦η₁ = refl
deterministic {［ η₊ ∣ inj₁ v ∣ _ ］◁} {［ η₊ ∣ _ ∣ _ ］▷} {⟨ η₊ ∣ v' ∣ _ ⟩◁} ↦η₁ r with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with v'
... | ()
deterministic {［ η₊ ∣ inj₂ (- v) ∣ _ ］◁} {［ η₊ ∣ _ ∣ _ ］▷} {［ _ ∣ _ ∣ _ ］▷} ↦η₂ ↦η₂ = refl
deterministic {［ η₊ ∣ inj₂ (- v) ∣ _ ］◁} {［ η₊ ∣ _ ∣ _ ］▷} {⟨ η₊ ∣ v' ∣ _ ⟩◁} ↦η₂ r with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with v'
... | ()
deterministic ↦ε₁ ↦ε₁ = refl
deterministic ↦ε₂ ↦ε₂ = refl

-- Backward deterministic
deterministicᵣₑᵥ : ∀ {st st₁ st₂} → st₁ ↦ st → st₂ ↦ st → st₁ ≡ st₂
deterministicᵣₑᵥ {［ c ∣ _ ∣ κ ］▷} {⟨ c ∣ v ∣ κ ⟩▷} {⟨ c' ∣ v' ∣ κ' ⟩▷} ↦⃗₁ r with Lemma₈ r
... | refl , refl with Lemma₉ r
deterministicᵣₑᵥ {［ unite₊l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ y        ∣ κ ⟩▷} {⟨ _ ∣ inj₂ y        ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ uniti₊l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v             ∣ κ ⟩▷} {⟨ _ ∣ v             ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₁ x        ∣ κ ⟩▷} {⟨ _ ∣ inj₁ x        ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ y        ∣ κ ⟩▷} {⟨ _ ∣ inj₂ y        ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₁ x        ∣ κ ⟩▷} {⟨ _ ∣ inj₁ x        ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₁ x        ∣ κ ⟩▷} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩▷} ↦⃗₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₁ x        ∣ κ ⟩▷} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩▷} ↦⃗₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩▷} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩▷} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩▷} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩▷} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ z        ∣ κ ⟩▷} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩▷} ↦⃗₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ z        ∣ κ ⟩▷} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩▷} ↦⃗₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ z        ∣ κ ⟩▷} {⟨ _ ∣ inj₂ z        ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ unite⋆l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ (tt , v)      ∣ κ ⟩▷} {⟨ _ ∣ (tt , v)      ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ uniti⋆l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v             ∣ κ ⟩▷} {⟨ _ ∣ v             ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap⋆    ∣ _ ∣ κ ］▷} {⟨ _ ∣ (x , y)       ∣ κ ⟩▷} {⟨ _ ∣ (x , y)       ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl⋆  ∣ _ ∣ κ ］▷} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩▷} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr⋆  ∣ _ ∣ κ ］▷} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩▷} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］▷} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩▷} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］▷} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩▷} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩▷} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］▷} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩▷} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩▷} ↦⃗₁ ↦⃗₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ unite₊l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ uniti₊l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ unite⋆l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ uniti⋆l  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ swap⋆    ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ assocl⋆  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ assocr⋆  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} ↦⃗₁ ()
deterministicᵣₑᵥ {［ id↔      ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} (↦⃗₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⨾ c₂  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} (↦⃗₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⊕ c₂  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} (↦⃗₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⊗ c₂  ∣ _ ∣ κ ］▷} {⟨ _ ∣ v  ∣ κ ⟩▷} {［ c' ∣ v' ∣ κ' ］▷} (↦⃗₁ {b = ()})
deterministicᵣₑᵥ {［ c ∣ _ ∣ κ ］▷} {⟨ c ∣ v ∣ κ ⟩▷} {［ _ ∣ _ ∣ _ ］◁} ↦⃗₁ r with Lemma₅ r
... | refl , refl with Lemma₆ r
... | refl , refl with Lemma₇ r
... | refl with v
... | ()
deterministicᵣₑᵥ ↦⃗₂ ↦⃗₂ = refl
deterministicᵣₑᵥ ↦⃗₃ ↦⃗₃ = refl
deterministicᵣₑᵥ ↦⃗₄ ↦⃗₄ = refl
deterministicᵣₑᵥ ↦⃗₅ ↦⃗₅ = refl
deterministicᵣₑᵥ ↦⃗₆ ↦⃗₆ = refl
deterministicᵣₑᵥ ↦⃗₇ ↦⃗₇ = refl
deterministicᵣₑᵥ ↦⃗₈ ↦⃗₈ = refl
deterministicᵣₑᵥ ↦⃗₉ ↦⃗₉ = refl
deterministicᵣₑᵥ ↦⃗₁₀ ↦⃗₁₀ = refl
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₁ v ∣ κ ］▷} {_} {⟨ _ ∣ _ ∣ _ ⟩▷} ↦⃗₁₁ r with Lemma₈ r
... | refl , refl with Lemma₉ r
... | refl , refl with Lemma₁₀ r
... | inj₂ refl with Lemma₁₁ r
... | inj₁ ()
... | inj₂ ()
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₁ v ∣ κ ］▷} {_} {［ _ ∣ _ ∣ _ ］▷} ↦⃗₁₁ ↦⃗₁₁ = refl
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₂ v ∣ κ ］▷} {_} {⟨ _ ∣ _ ∣ _ ⟩▷} ↦⃗₁₂ r with Lemma₈ r
... | refl , refl with Lemma₉ r
... | refl , refl with Lemma₁₀ r
... | inj₂ refl with Lemma₁₁ r
... | inj₁ ()
... | inj₂ ()
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₂ v ∣ κ ］▷} {_} {［ _ ∣ _ ∣ _ ］▷} ↦⃗₁₂ ↦⃗₁₂ = refl
deterministicᵣₑᵥ (↦⃖₁ {b = b₁}) (↦⃖₁ {b = b₂})  with base-is-prop _ b₁ b₂
... | refl = refl
deterministicᵣₑᵥ ↦⃖₂ ↦⃖₂ = refl
deterministicᵣₑᵥ ↦⃖₃ ↦⃖₃ = refl
deterministicᵣₑᵥ ↦⃖₄ ↦⃖₄ = refl
deterministicᵣₑᵥ ↦⃖₅ ↦⃖₅ = refl
deterministicᵣₑᵥ ↦⃖₆ ↦⃖₆ = refl
deterministicᵣₑᵥ ↦⃖₇ ↦⃖₇ = refl
deterministicᵣₑᵥ ↦⃖₈ ↦⃖₈ = refl
deterministicᵣₑᵥ ↦⃖₉ ↦⃖₉ = refl
deterministicᵣₑᵥ ↦⃖₁₀ ↦⃖₁₀ = refl
deterministicᵣₑᵥ ↦⃖₁₁ ↦⃖₁₁ = refl
deterministicᵣₑᵥ ↦⃖₁₂ ↦⃖₁₂ = refl
deterministicᵣₑᵥ {_} {［ η₊ ∣ inj₁ _ ∣ _ ］◁} {⟨ _ ∣ v ∣ _ ⟩▷} ↦η₁ r with Lemma₈ r
... | refl , refl with Lemma₉ r
... | refl , refl with Lemma₁₀ r
... | inj₁ ()
... | inj₂ ()
deterministicᵣₑᵥ {_} {［ η₊ ∣ inj₁ v ∣ _ ］◁} {［ _ ∣ _ ∣ _ ］◁} ↦η₁ ↦η₁ = refl
deterministicᵣₑᵥ {_} {［ η₊ ∣ inj₂ (- v) ∣ _ ］◁} {⟨ c ∣ x ∣ x₁ ⟩▷} ↦η₂ r with Lemma₈ r
... | refl , refl with Lemma₉ r
... | refl , refl with Lemma₁₀ r
... | inj₁ ()
... | inj₂ ()
deterministicᵣₑᵥ {_} {［ η₊ ∣ inj₂ (- v) ∣ _ ］◁} {［ _ ∣ _ ∣ _ ］◁} ↦η₂ ↦η₂ = refl
deterministicᵣₑᵥ ↦ε₁ ↦ε₁ = refl
deterministicᵣₑᵥ ↦ε₂ ↦ε₂ = refl

-- Non-repeating Lemma
open RevNoRepeat (record { State = State
                         ; _↦_ = _↦_
                         ; deterministic = deterministic
                         ; deterministicᵣₑᵥ = deterministicᵣₑᵥ }) public

NoRepeatPi- : ∀ {A B stₙ stₘ n m} (c : A ↔ B) (v : ⟦ A ⟧)
            → n < m
            → ⟨ c ∣ v ∣ ☐ ⟩▷ ↦[ n ] stₙ
            → ⟨ c ∣ v ∣ ☐ ⟩▷ ↦[ m ] stₘ
            → stₙ ≢ stₘ
NoRepeatPi- c v n<m st₀↦stₙ st₀↦stₘ = NoRepeat (λ ()) n<m st₀↦stₙ st₀↦stₘ