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

open import lib.Basics

module lib.types.Sigma where

-- pointed [Σ]
⊙Σ : ∀ {i j} (X : Ptd i) → (de⊙ X → Ptd j) → Ptd (lmax i j)
⊙Σ ⊙[ A , a₀ ] Y = ⊙[ Σ A (de⊙ ∘ Y) , (a₀ , pt (Y a₀)) ]

-- Cartesian product
_×_ : ∀ {i j} (A : Type i) (B : Type j) → Type (lmax i j)
A × B = Σ A (λ _ → B)

_⊙×_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
X ⊙× Y = ⊙Σ X (λ _ → Y)

infixr 80 _×_ _⊙×_

-- XXX Do we really need two versions of [⊙fst]?
⊙fstᵈ : ∀ {i j} {X : Ptd i} (Y : de⊙ X → Ptd j) → ⊙Σ X Y ⊙→ X
⊙fstᵈ Y = fst , idp

⊙fst : ∀ {i j} {X : Ptd i} {Y : Ptd j} → X ⊙× Y ⊙→ X
⊙fst = ⊙fstᵈ _

⊙snd : ∀ {i j} {X : Ptd i} {Y : Ptd j} → X ⊙× Y ⊙→ Y
⊙snd = (snd , idp)

fanout : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  → (A → B) → (A → C) → (A → B × C)
fanout f g x = f x , g x

⊙fanout-pt : ∀ {i j} {A : Type i} {B : Type j}
  {a₀ a₁ : A} (p : a₀ == a₁) {b₀ b₁ : B} (q : b₀ == b₁)
  → (a₀ , b₀) == (a₁ , b₁) :> A × B
⊙fanout-pt = pair×=

⊙fanout : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → X ⊙→ Y → X ⊙→ Z → X ⊙→ Y ⊙× Z
⊙fanout (f , fpt) (g , gpt) = fanout f g , ⊙fanout-pt fpt gpt

diag : ∀ {i} {A : Type i} → (A → A × A)
diag a = a , a

⊙diag : ∀ {i} {X : Ptd i} → X ⊙→ X ⊙× X
⊙diag = ((λ x → (x , x)) , idp)

⊙×-inl : ∀ {i j} (X : Ptd i) (Y : Ptd j) → X ⊙→ X ⊙× Y
⊙×-inl X Y = (λ x → x , pt Y) , idp

⊙×-inr : ∀ {i j} (X : Ptd i) (Y : Ptd j) → Y ⊙→ X ⊙× Y
⊙×-inr X Y = (λ y → pt X , y) , idp

⊙fst-fanout : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (f : X ⊙→ Y) (g : X ⊙→ Z)
  → ⊙fst ⊙∘ ⊙fanout f g == f
⊙fst-fanout (f , idp) (g , idp) = idp

⊙snd-fanout : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (f : X ⊙→ Y) (g : X ⊙→ Z)
  → ⊙snd ⊙∘ ⊙fanout f g == g
⊙snd-fanout (f , idp) (g , idp) = idp

⊙fanout-pre∘ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (f : Y ⊙→ Z) (g : Y ⊙→ W) (h : X ⊙→ Y)
  → ⊙fanout f g ⊙∘ h == ⊙fanout (f ⊙∘ h) (g ⊙∘ h)
⊙fanout-pre∘ (f , idp) (g , idp) (h , idp) = idp

module _ {i j} {A : Type i} {B : A → Type j} where

  pair : (a : A) (b : B a) → Σ A B
  pair a b = (a , b)

  -- pair= has already been defined

  fst= : {ab a'b' : Σ A B} (p : ab == a'b') → (fst ab == fst a'b')
  fst= = ap fst

  snd= : {ab a'b' : Σ A B} (p : ab == a'b')
    → (snd ab == snd a'b' [ B ↓ fst= p ])
  snd= {._} {_} idp = idp

  fst=-β : {a a' : A} (p : a == a')
    {b : B a} {b' : B a'} (q : b == b' [ B ↓ p ])
    → fst= (pair= p q) == p
  fst=-β idp idp = idp

  snd=-β : {a a' : A} (p : a == a')
    {b : B a} {b' : B a'} (q : b == b' [ B ↓ p ])
    → snd= (pair= p q) == q [ (λ v → b == b' [ B ↓ v ]) ↓ fst=-β p q ]
  snd=-β idp idp = idp

  pair=-η : {ab a'b' : Σ A B} (p : ab == a'b')
    → p == pair= (fst= p) (snd= p)
  pair=-η {._} {_} idp = idp

  pair== : {a a' : A} {p p' : a == a'} (α : p == p')
           {b : B a} {b' : B a'} {q : b == b' [ B ↓ p ]} {q' : b == b' [ B ↓ p' ]}
           (β : q == q' [ (λ u → b == b' [ B ↓ u ]) ↓ α ])
    → pair= p q == pair= p' q'
  pair== idp idp = idp

module _ {i j} {A : Type i} {B : Type j} where

  fst×= : {ab a'b' : A × B} (p : ab == a'b') → (fst ab == fst a'b')
  fst×= = ap fst

  snd×= : {ab a'b' : A × B} (p : ab == a'b')
    → (snd ab == snd a'b')
  snd×= = ap snd

  fst×=-β : {a a' : A} (p : a == a')
    {b b' : B} (q : b == b')
    → fst×= (pair×= p q) == p
  fst×=-β idp idp = idp

  snd×=-β : {a a' : A} (p : a == a')
    {b b' : B} (q : b == b')
    → snd×= (pair×= p q) == q
  snd×=-β idp idp = idp

  pair×=-η : {ab a'b' : A × B} (p : ab == a'b')
    → p == pair×= (fst×= p) (snd×= p)
  pair×=-η {._} {_} idp = idp

module _ {i j} {A : Type i} {B : A → Type j} where

  =Σ : (x y : Σ A B) → Type (lmax i j)
  =Σ (a , b) (a' , b') = Σ (a == a') (λ p → b == b' [ B ↓ p ])

  =Σ-econv : (x y : Σ A B) →  (=Σ x y) ≃ (x == y)
  =Σ-econv x y =
    equiv (λ pq → pair= (fst pq) (snd pq)) (λ p → fst= p , snd= p)
          (λ p → ! (pair=-η p))
          (λ pq → pair= (fst=-β (fst pq) (snd pq)) (snd=-β (fst pq) (snd pq)))

  =Σ-conv : (x y : Σ A B) → (=Σ x y) == (x == y)
  =Σ-conv x y = ua (=Σ-econv x y)

Σ= : ∀ {i j} {A A' : Type i} (p : A == A') {B : A → Type j} {B' : A' → Type j}
  (q : B == B' [ (λ X → (X → Type j)) ↓ p ]) → Σ A B == Σ A' B'
Σ= idp idp = idp

instance
  Σ-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {P : A → Type j}
    → has-level n A → ((x : A) → has-level n (P x))
      → has-level n (Σ A P)
  Σ-level {n = ⟨-2⟩} p q = has-level-in ((contr-center p , (contr-center (q (contr-center p)))) , lemma)
    where abstract lemma = λ y → pair= (contr-path p _) (from-transp! _ _ (contr-path (q _) _))
  Σ-level {n = S n} p q = has-level-in lemma where
    abstract
      lemma = λ x y → equiv-preserves-level (=Σ-econv x y)
        {{Σ-level (has-level-apply p _ _) (λ _ →
          equiv-preserves-level ((to-transp-equiv _ _)⁻¹) {{has-level-apply (q _) _ _}})}}

×-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j}
  → (has-level n A → has-level n B → has-level n (A × B))
×-level pA pB = Σ-level pA (λ x → pB)

-- Equivalences in a Σ-type

Σ-fmap-l : ∀ {i j k} {A : Type i} {B : Type j} (P : B → Type k)
  → (f : A → B) → (Σ A (P ∘ f) → Σ B P)
Σ-fmap-l P f (a , r) = (f a , r)

×-fmap-l : ∀ {i₀ i₁ j} {A₀ : Type i₀} {A₁ : Type i₁} (B : Type j)
  → (f : A₀ → A₁) → (A₀ × B → A₁ × B)
×-fmap-l B = Σ-fmap-l (λ _ → B)

Σ-isemap-l : ∀ {i j k} {A : Type i} {B : Type j} (P : B → Type k) {h : A → B}
  → is-equiv h → is-equiv (Σ-fmap-l P h)
Σ-isemap-l {A = A} {B = B} P {h} e = is-eq _ g f-g g-f
  where f = Σ-fmap-l P h

        g : Σ B P → Σ A (P ∘ h)
        g (b , s) = (is-equiv.g e b , transport P (! (is-equiv.f-g e b)) s)

        f-g : ∀ y → f (g y) == y
        f-g (b , s) = pair= (is-equiv.f-g e b) (transp-↓ P (is-equiv.f-g e b) s)

        g-f : ∀ x → g (f x) == x
        g-f (a , r) =
          pair= (is-equiv.g-f e a)
                (transport (λ q → transport P (! q) r == r [ P ∘ h ↓ is-equiv.g-f e a ])
                           (is-equiv.adj e a)
                           (transp-ap-↓ P h (is-equiv.g-f e a) r))

×-isemap-l : ∀ {i₀ i₁ j} {A₀ : Type i₀} {A₁ : Type i₁} (B : Type j) {h : A₀ → A₁}
  → is-equiv h → is-equiv (×-fmap-l B h)
×-isemap-l B = Σ-isemap-l (λ _ → B)

Σ-emap-l : ∀ {i j k} {A : Type i} {B : Type j} (P : B → Type k)
  → (e : A ≃ B) → (Σ A (P ∘ –> e) ≃ Σ B P)
Σ-emap-l P (f , e) = _ , Σ-isemap-l P e

×-emap-l : ∀ {i₀ i₁ j} {A₀ : Type i₀} {A₁ : Type i₁} (B : Type j)
  → (e : A₀ ≃ A₁) → (A₀ × B ≃ A₁ × B)
×-emap-l B = Σ-emap-l (λ _ → B)

Σ-fmap-r : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  → (∀ x → B x → C x) → (Σ A B → Σ A C)
Σ-fmap-r h (a , b) = (a , h a b)

×-fmap-r : ∀ {i j₀ j₁} (A : Type i) {B₀ : Type j₀} {B₁ : Type j₁}
  → (h : B₀ → B₁) → (A × B₀ → A × B₁)
×-fmap-r A h = Σ-fmap-r (λ _ → h)

Σ-isemap-r : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  {h : ∀ x → B x → C x} → (∀ x → is-equiv (h x)) → is-equiv (Σ-fmap-r h)
Σ-isemap-r {A = A} {B = B} {C = C} {h} k = is-eq _ g f-g g-f
  where f = Σ-fmap-r h

        g : Σ A C → Σ A B
        g (a , c) = (a , is-equiv.g (k a) c)

        f-g : ∀ p → f (g p) == p
        f-g (a , c) = pair= idp (is-equiv.f-g (k a) c)

        g-f : ∀ p → g (f p) == p
        g-f (a , b) = pair= idp (is-equiv.g-f (k a) b)

×-isemap-r : ∀ {i j₀ j₁} (A : Type i) {B₀ : Type j₀} {B₁ : Type j₁}
  → {h : B₀ → B₁} → is-equiv h → is-equiv (×-fmap-r A h)
×-isemap-r A e = Σ-isemap-r (λ _ → e)

Σ-emap-r : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  → (∀ x → B x ≃ C x) → (Σ A B ≃ Σ A C)
Σ-emap-r k = _ , Σ-isemap-r (λ x → snd (k x))

×-emap-r : ∀ {i j₀ j₁} (A : Type i) {B₀ : Type j₀} {B₁ : Type j₁}
  → (e : B₀ ≃ B₁) → (A × B₀ ≃ A × B₁)
×-emap-r A e = Σ-emap-r (λ _ → e)

hfiber-Σ-fmap-r : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  → (h : ∀ x → B x → C x) → {a : A} → (c : C a)
  → hfiber (Σ-fmap-r h) (a , c) ≃ hfiber (h a) c
hfiber-Σ-fmap-r h {a} c = equiv to from to-from from-to

  where to : hfiber (Σ-fmap-r h) (a , c) → hfiber (h a) c
        to ((_ , b) , idp) = b , idp

        from : hfiber (h a) c → hfiber (Σ-fmap-r h) (a , c)
        from (b , idp) = (a , b) , idp

        abstract
          to-from : (x : hfiber (h a) c) → to (from x) == x
          to-from (b , idp) = idp

          from-to : (x : hfiber (Σ-fmap-r h) (a , c)) → from (to x) == x
          from-to ((_ , b) , idp) = idp

{-
-- 2016/08/20 favonia: no one is using the following two functions.

-- Two ways of simultaneously applying equivalences in each component.
module _ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁}
         {B₀ : A₀ → Type j₀} {B₁ : A₁ → Type j₁} where
  Σ-emap : (u : A₀ ≃ A₁) (v : ∀ a → B₀ (<– u a) ≃ B₁ a) → Σ A₀ B₀ ≃ Σ A₁ B₁
  Σ-emap u v = Σ A₀ B₀           ≃⟨ Σ-emap-l _ (u ⁻¹) ⁻¹ ⟩
               Σ A₁ (B₀ ∘ <– u)  ≃⟨ Σ-emap-r v ⟩
               Σ A₁ B₁           ≃∎

  Σ-emap' : (u : A₀ ≃ A₁) (v : ∀ a → B₀ a ≃ B₁ (–> u a)) → Σ A₀ B₀ ≃ Σ A₁ B₁
  Σ-emap' u v = Σ A₀ B₀           ≃⟨ Σ-emap-r v ⟩
                Σ A₀ (B₁ ∘ –> u)  ≃⟨ Σ-emap-l _ u ⟩
                Σ A₁ B₁           ≃∎
-}

×-fmap : ∀ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  → (h : A₀ → A₁) (k : B₀ → B₁) → (A₀ × B₀ → A₁ × B₁)
×-fmap u v = ×-fmap-r _ v ∘ ×-fmap-l _ u

⊙×-fmap : ∀ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'}
  → X ⊙→ X' → Y ⊙→ Y' → X ⊙× Y ⊙→ X' ⊙× Y'
⊙×-fmap (f , fpt) (g , gpt) = ×-fmap f g , pair×= fpt gpt

×-isemap : ∀ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  {h : A₀ → A₁} {k : B₀ → B₁} → is-equiv h → is-equiv k → is-equiv (×-fmap h k)
×-isemap eh ek = ×-isemap-r _ ek ∘ise ×-isemap-l _ eh

×-emap : ∀ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  → (u : A₀ ≃ A₁) (v : B₀ ≃ B₁) → (A₀ × B₀ ≃ A₁ × B₁)
×-emap u v = ×-emap-r _ v ∘e ×-emap-l _ u

⊙×-emap : ∀ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'}
  → X ⊙≃ X' → Y ⊙≃ Y' → X ⊙× Y ⊙≃ X' ⊙× Y'
⊙×-emap (F , F-ise) (G , G-ise) = ⊙×-fmap F G , ×-isemap F-ise G-ise

-- Implementation of [_∙'_] on Σ
Σ-∙' : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
  → (pair= p q ∙' pair= p' r) == pair= (p ∙' p') (q ∙'ᵈ r)
Σ-∙' {p = idp} {p' = idp} q idp = idp

-- Implementation of [_∙_] on Σ
Σ-∙ : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
  → (pair= p q ∙ pair= p' r) == pair= (p ∙ p') (q ∙ᵈ r)
Σ-∙ {p = idp} {p' = idp} idp r = idp

-- Implementation of [!] on Σ
Σ-! : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y : A} {p : x == y}
  {u : B x} {v : B y}
  (q : u == v [ B ↓ p ])
  → ! (pair= p q) == pair= (! p) (!ᵈ q)
Σ-! {p = idp} idp = idp

-- Implementation of [_∙'_] on ×
×-∙' : ∀ {i j} {A : Type i} {B : Type j}
  {x y z : A} (p : x == y) (p' : y == z)
  {u v w : B} (q : u == v) (q' : v == w)
  → (pair×= p q ∙' pair×= p' q') == pair×= (p ∙' p') (q ∙' q')
×-∙' idp idp q idp = idp

-- Implementation of [_∙_] on ×
×-∙ : ∀ {i j} {A : Type i} {B : Type j}
  {x y z : A} (p : x == y) (p' : y == z)
  {u v w : B} (q : u == v) (q' : v == w)
  → (pair×= p q ∙ pair×= p' q') == pair×= (p ∙ p') (q ∙ q')
×-∙ idp idp idp r = idp

-- Implementation of [!] on ×
×-! : ∀ {i j} {A : Type i} {B : Type j}
  {x y : A} (p : x == y) {u v : B} (q : u == v)
  → ! (pair×= p q) == pair×= (! p) (! q)
×-! idp idp = idp

-- Special case of [ap-,]
ap-cst,id : ∀ {i j} {A : Type i} (B : A → Type j)
  {a : A} {x y : B a} (p : x == y)
  → ap (λ x → _,_ {B = B} a x) p == pair= idp p
ap-cst,id B idp = idp

-- hfiber fst == B
module _ {i j} {A : Type i} {B : A → Type j} where

  private
    to : ∀ a → hfiber (fst :> (Σ A B → A)) a → B a
    to a ((.a , b) , idp) = b

    from : ∀ (a : A) → B a → hfiber (fst :> (Σ A B → A)) a
    from a b = (a , b) , idp

    to-from : ∀ (a : A) (b : B a) → to a (from a b) == b
    to-from a b = idp

    from-to : ∀ a b′ → from a (to a b′) == b′
    from-to a ((.a , b) , idp) = idp

  hfiber-fst : ∀ a → hfiber (fst :> (Σ A B → A)) a ≃ B a
  hfiber-fst a = to a , is-eq (to a) (from a) (to-from a) (from-to a)

{- Dependent paths in a Σ-type -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k}
  where

  ↓-Σ-in : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (q : r == r' [ B ↓ p ])
    → s == s' [ uncurry C ↓ pair= p q ]
    → (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ]
  ↓-Σ-in {p = idp} idp t = pair= idp t

  ↓-Σ-fst : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    → (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ]
    → r == r' [ B ↓ p ]
  ↓-Σ-fst {p = idp} u = fst= u

  ↓-Σ-snd : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    → (u : (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ])
    → s == s' [ uncurry C ↓ pair= p (↓-Σ-fst u) ]
  ↓-Σ-snd {p = idp} idp = idp

  ↓-Σ-β-fst : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (q : r == r' [ B ↓ p ])
    (t : s == s' [ uncurry C ↓ pair= p q ])
    → ↓-Σ-fst (↓-Σ-in q t) == q
  ↓-Σ-β-fst {p = idp} idp idp = idp

  ↓-Σ-β-snd : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (q : r == r' [ B ↓ p ])
    (t : s == s' [ uncurry C ↓ pair= p q ])
    → ↓-Σ-snd (↓-Σ-in q t) == t
      [ (λ q' → s == s' [ uncurry C ↓ pair= p q' ]) ↓ ↓-Σ-β-fst q t ]
  ↓-Σ-β-snd {p = idp} idp idp = idp

  ↓-Σ-η : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x r} {s' : C x' r'}
    (u : (r , s) == (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ])
    → ↓-Σ-in (↓-Σ-fst u) (↓-Σ-snd u) == u
  ↓-Σ-η {p = idp} idp = idp

{- Dependent paths in a ×-type -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  where

  ↓-×-in : {x x' : A} {p : x == x'} {r : B x} {r' : B x'}
    {s : C x} {s' : C x'}
    → r == r' [ B ↓ p ]
    → s == s' [ C ↓ p ]
    → (r , s) == (r' , s') [ (λ x → B x × C x) ↓ p ]
  ↓-×-in {p = idp} q t = pair×= q t

{- Dependent paths over a ×-type -}
module _ {i j k} {A : Type i} {B : Type j} (C : A → B → Type k)
  where

  ↓-over-×-in : {x x' : A} {p : x == x'} {y y' : B} {q : y == y'}
    {u : C x y} {v : C x' y} {w : C x' y'}
    → u == v [ (λ a → C a y) ↓ p ]
    → v == w [ (λ b → C x' b) ↓ q ]
    → u == w [ uncurry C ↓ pair×= p q ]
  ↓-over-×-in {p = idp} {q = idp} idp idp = idp

  ↓-over-×-in' : {x x' : A} {p : x == x'} {y y' : B} {q : y == y'}
    {u : C x y} {v : C x y'} {w : C x' y'}
    → u == v [ (λ b → C x b) ↓ q ]
    → v == w [ (λ a → C a y') ↓ p ]
    → u == w [ uncurry C ↓ pair×= p q ]
  ↓-over-×-in' {p = idp} {q = idp} idp idp = idp

module _ where
  -- An orphan lemma.
  ↓-cst×app-in : ∀ {i j k} {A : Type i}
    {B : Type j} {C : A → B → Type k}
    {a₁ a₂ : A} (p : a₁ == a₂)
    {b₁ b₂ : B} (q : b₁ == b₂)
    {c₁ : C a₁ b₁}{c₂ : C a₂ b₂}
    → c₁ == c₂ [ uncurry C ↓ pair×= p q ]
    → (b₁ , c₁) == (b₂ , c₂) [ (λ x → Σ B (C x)) ↓ p ]
  ↓-cst×app-in idp idp idp = idp

{- pair= and pair×= where one argument is reflexivity -}
pair=-idp-l : ∀ {i j} {A : Type i} {B : A → Type j} (a : A) {b₁ b₂ : B a}
  (q : b₁ == b₂) → pair= {B = B} idp q == ap (λ y → (a , y)) q
pair=-idp-l _ idp = idp

pair×=-idp-l : ∀ {i j} {A : Type i} {B : Type j} (a : A) {b₁ b₂ : B}
  (q : b₁ == b₂) → pair×= idp q == ap (λ y → (a , y)) q
pair×=-idp-l _ idp = idp

pair×=-idp-r : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} (p : a₁ == a₂)
  (b : B) → pair×= p idp == ap (λ x → (x , b)) p
pair×=-idp-r idp _ = idp

pair×=-split-l : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} (p : a₁ == a₂)
  {b₁ b₂ : B} (q : b₁ == b₂)
  → pair×= p q == ap (λ a → (a , b₁)) p ∙ ap (λ b → (a₂ , b)) q
pair×=-split-l idp idp = idp

pair×=-split-r : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} (p : a₁ == a₂)
  {b₁ b₂ : B} (q : b₁ == b₂)
  → pair×= p q == ap (λ b → (a₁ , b)) q ∙ ap (λ a → (a , b₂)) p
pair×=-split-r idp idp = idp

-- Commutativity of products and derivatives.
module _ {i j} {A : Type i} {B : Type j} where
  ×-comm : Σ A (λ _ → B) ≃ Σ B (λ _ → A)
  ×-comm = equiv (λ {(a , b) → (b , a)}) (λ {(b , a) → (a , b)}) (λ _ → idp) (λ _ → idp)

module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} where
  Σ₂-×-comm : Σ (Σ A B) (λ ab → C (fst ab)) ≃ Σ (Σ A C) (λ ac → B (fst ac))
  Σ₂-×-comm = Σ-assoc ⁻¹ ∘e Σ-emap-r (λ a → ×-comm) ∘e Σ-assoc

module _ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k} where
  Σ₁-×-comm : Σ A (λ a → Σ B (λ b → C a b)) ≃ Σ B (λ b → Σ A (λ a → C a b))
  Σ₁-×-comm = Σ-assoc ∘e Σ-emap-l _ ×-comm ∘e Σ-assoc ⁻¹

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

-- The basic CBPV metalanguage, extended with parallelism.

open import Calf.CostMonoid

module Calf.ParMetalanguage (parCostMonoid : ParCostMonoid) where

open ParCostMonoid parCostMonoid

open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.Step costMonoid

open import Calf.Types.Eq
open import Calf.Types.Bounded costMonoid

open import Data.Product
open import Relation.Binary.PropositionalEquality

postulate
  _&_ : {A₁ A₂ : tp pos} → cmp (F A₁) → cmp (F A₂) → cmp (F (Σ++ A₁ (λ _ → A₂)))

  &/join : ∀ {A₁ A₂} {v₁ v₂ p₁ p₂} →
    step (F A₁) p₁ (ret v₁) & step (F A₂) p₂ (ret v₂) ≡ step (F (Σ++ A₁ λ _ → A₂)) (p₁ ⊗ p₂) (ret (v₁ , v₂))
  {-# REWRITE &/join #-}

&/join/𝟘 : ∀ {A₁ A₂} {v₁ v₂} →
  ret v₁ & ret v₂ ≡ step (F (Σ++ A₁ λ _ → A₂)) (𝟘 ⊗ 𝟘) (ret (v₁ , v₂))
&/join/𝟘 = &/join {p₁ = 𝟘} {p₂ = 𝟘}
{-# REWRITE &/join/𝟘 #-}

bind/& : ∀ {A₁ A₂} {X} {v₁ v₂ f} (p₁ p₂ : ℂ) →
  bind {Σ++ A₁ λ _ → A₂} X (step (F A₁) p₁ (ret v₁) & step (F A₂) p₂ (ret v₂)) f ≡ step X (p₁ ⊗ p₂) (f (v₁ , v₂))
bind/& _ _ = refl

bound/par : {A₁ A₂ : tp pos} {e₁ : cmp (F A₁)} {e₂ : cmp (F A₂)} {c₁ c₂ : ℂ} →
  IsBounded A₁ e₁ c₁ →
  IsBounded A₂ e₂ c₂ →
  IsBounded (Σ++ A₁ λ _ → A₂) (e₁ & e₂) (c₁ ⊗ c₂)
bound/par (⇓ a₁ withCost p₁' [ h-bounded₁ , h-≡₁ ]) (⇓ a₂ withCost p₂' [ h-bounded₂ , h-≡₂ ]) with eq/ref h-≡₁ | eq/ref h-≡₂
... | refl | refl = ⇓ (a₁ , a₂) withCost (p₁' ⊗ p₂') [ (λ u → ⊗-mono-≤ (h-bounded₁ u) (h-bounded₂ u)) , (ret (eq/intro refl)) ]

ext: agda

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae
open import Lists.Lists
open import Numbers.BinaryNaturals.Definition
open import Maybe
open import Numbers.BinaryNaturals.SubtractionGo

module Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalRight where

goPreservesCanonicalRightZero : (a b : BinNat) → mapMaybe canonical (go zero a b) ≡ mapMaybe canonical (go zero a (canonical b))
goPreservesCanonicalRightOne : (a b : BinNat) → mapMaybe canonical (go one a b) ≡ mapMaybe canonical (go one a (canonical b))

goPreservesCanonicalRightZero [] [] = refl
goPreservesCanonicalRightZero [] (zero :: b) with inspect (go zero [] b)
goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr with inspect (canonical b)
goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | [] with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (goPreservesCanonicalRightZero [] b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero [] i)) pr2) refl))))
goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | (x :: y) with≡ pr2 with inspect (go zero [] (x :: y))
goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | (x :: y) with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = refl
goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | (x :: y) with≡ pr2 | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (goPreservesCanonicalRightZero [] b) (applyEquality (mapMaybe canonical) pr3))))
goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr with inspect (canonical b)
goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | [] with≡ pr2 rewrite pr | pr2 = applyEquality yes (goZeroEmpty' b pr)
goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | (x :: xs) with≡ pr2 with inspect (go zero [] (x :: xs))
goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | (x :: xs) with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (noNotYes (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero [] i)) (equalityCommutative pr2)) (equalityCommutative (goPreservesCanonicalRightZero [] b)))) (applyEquality (mapMaybe canonical) pr)))
goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | (x :: xs) with≡ pr2 | yes x₁ with≡ pr3 rewrite pr | pr2 | pr3 = transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (transitivity (goPreservesCanonicalRightZero [] b) (applyEquality (λ i → mapMaybe canonical (go zero [] i)) pr2)) (applyEquality (mapMaybe canonical) pr3))
goPreservesCanonicalRightZero [] (one :: b) = refl
goPreservesCanonicalRightZero (zero :: a) [] = refl
goPreservesCanonicalRightZero (one :: a) [] = refl
goPreservesCanonicalRightZero (zero :: a) (zero :: b) with inspect (canonical b)
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | [] with≡ pr1 with inspect (go zero a b)
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | [] with≡ pr1 | no with≡ pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1) (applyEquality (mapMaybe canonical) (goEmpty a))))))
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | [] with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
  where
    t : canonical y ≡ canonical a
    t = yesInjective (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1) (applyEquality (mapMaybe canonical) (goEmpty a)))))
    v : canonical (zero :: y) ≡ canonical (zero :: a)
    v with inspect (canonical y)
    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 with inspect (go zero a b)
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 with inspect (go zero a (r :: rs))
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1)) (applyEquality (mapMaybe canonical) pr3))))
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | yes y with≡ pr2 with inspect (go zero a (r :: rs))
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | yes y with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) (equalityCommutative pr1)) (equalityCommutative (goPreservesCanonicalRightZero a b))) (applyEquality (mapMaybe canonical) pr2))))
goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | yes y with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality yes v
  where
    t : canonical y ≡ canonical z
    t = yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1) (applyEquality (mapMaybe canonical) pr3))))
    v : canonical (zero :: y) ≡ canonical (zero :: z)
    v with inspect (canonical y)
    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
goPreservesCanonicalRightZero (zero :: a) (one :: b) with inspect (go one a b)
goPreservesCanonicalRightZero (zero :: a) (one :: b) | no with≡ x with inspect (go one a (canonical b))
goPreservesCanonicalRightZero (zero :: a) (one :: b) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
goPreservesCanonicalRightZero (zero :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
goPreservesCanonicalRightZero (zero :: a) (one :: b) | yes r with≡ pr1 with inspect (go one a (canonical b))
goPreservesCanonicalRightZero (zero :: a) (one :: b) | yes r with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1))))
goPreservesCanonicalRightZero (zero :: a) (one :: b) | yes r with≡ pr1 | yes s with≡ pr2 rewrite pr1 | pr2 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
goPreservesCanonicalRightZero (one :: a) (zero :: b) with inspect (go zero a b)
goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 with inspect (canonical b)
goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a))))))
goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 with inspect (go zero a (x :: y))
goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) pr3)))))
goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 with inspect (canonical b)
goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a))))))
goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go zero a (r :: rs))
goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) (equalityCommutative pr2)) (equalityCommutative (goPreservesCanonicalRightZero a b))) (applyEquality (mapMaybe canonical) pr1))))
goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | (r :: rs) with≡ pr2 | yes y with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
goPreservesCanonicalRightZero (one :: a) (one :: b) with inspect (go zero a b)
goPreservesCanonicalRightZero (one :: a) (one :: b) | no with≡ pr1 with inspect (go zero a (canonical b))
goPreservesCanonicalRightZero (one :: a) (one :: b) | no with≡ pr1 | no with≡ x rewrite pr1 | x = refl
goPreservesCanonicalRightZero (one :: a) (one :: b) | no with≡ pr1 | yes x₁ with≡ x rewrite pr1 | x = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (mapMaybe canonical) x))))
goPreservesCanonicalRightZero (one :: a) (one :: b) | yes x with≡ pr1 with inspect (go zero a (canonical b))
goPreservesCanonicalRightZero (one :: a) (one :: b) | yes x with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightZero a b)) (applyEquality (mapMaybe canonical) pr1))))
goPreservesCanonicalRightZero (one :: a) (one :: b) | yes x with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
  where
    t : canonical x ≡ canonical y
    t = yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (goPreservesCanonicalRightZero a b)) (applyEquality (mapMaybe canonical) pr2))
    v : canonical (zero :: x) ≡ canonical (zero :: y)
    v with inspect (canonical x)
    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl

goPreservesCanonicalRightOne a [] = refl
goPreservesCanonicalRightOne [] (zero :: b) rewrite goOneEmpty' (canonical (zero :: b)) = refl
goPreservesCanonicalRightOne (zero :: a) (zero :: b) with inspect (go one a b)
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 with inspect (canonical b)
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 with inspect (go one a [])
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 | yes y with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightOne a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2) refl)) (applyEquality (mapMaybe canonical) pr3))))
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 with inspect (go one a (x :: y))
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2))) (applyEquality (mapMaybe canonical) pr3)))
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 with inspect (canonical b)
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 with inspect (go one a [])
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (applyEquality (λ i → mapMaybe canonical (go one a i)) (equalityCommutative pr2)) (equalityCommutative (goPreservesCanonicalRightOne a b)))) (applyEquality (mapMaybe canonical) pr1)))
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go one a (r :: rs))
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (applyEquality (λ i → mapMaybe canonical (go one a i)) (equalityCommutative pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1)))))
goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
goPreservesCanonicalRightOne (one :: a) (zero :: b) with inspect (go zero a b)
goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 with inspect (canonical b)
goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a))))))
goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go zero a (r :: rs))
goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | (r :: rs) with≡ pr2 | yes y with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 with inspect (canonical b)
goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
  where
    t : canonical y ≡ canonical a
    t = yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a)))))
    v : canonical (zero :: y) ≡ canonical (zero :: a)
    v with inspect (canonical y)
    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go zero a (r :: rs))
goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))) (applyEquality (mapMaybe canonical) pr1)))
goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality yes v
  where
    t : canonical y ≡ canonical z
    t = yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) pr3))))
    v : canonical (zero :: y) ≡ canonical (zero :: z)
    v with inspect (canonical y)
    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
goPreservesCanonicalRightOne [] (one :: b) = refl
goPreservesCanonicalRightOne (zero :: a) (one :: b) with inspect (go one a b)
goPreservesCanonicalRightOne (zero :: a) (one :: b) | no with≡ pr1 with inspect (go one a (canonical b))
goPreservesCanonicalRightOne (zero :: a) (one :: b) | no with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = refl
goPreservesCanonicalRightOne (zero :: a) (one :: b) | no with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
goPreservesCanonicalRightOne (zero :: a) (one :: b) | yes y with≡ pr1 with inspect (go one a (canonical b))
goPreservesCanonicalRightOne (zero :: a) (one :: b) | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1))))
goPreservesCanonicalRightOne (zero :: a) (one :: b) | yes y with≡ pr1 | yes z with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
  where
    t : canonical y ≡ canonical z
    t = yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr2))
    v : canonical (zero :: y) ≡ canonical (zero :: z)
    v with inspect (canonical y)
    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
goPreservesCanonicalRightOne (one :: a) (one :: b) with inspect (go one a b)
goPreservesCanonicalRightOne (one :: a) (one :: b) | no with≡ pr1 with inspect (go one a (canonical b))
goPreservesCanonicalRightOne (one :: a) (one :: b) | no with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = refl
goPreservesCanonicalRightOne (one :: a) (one :: b) | no with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
goPreservesCanonicalRightOne (one :: a) (one :: b) | yes y with≡ pr1 with inspect (go one a (canonical b))
goPreservesCanonicalRightOne (one :: a) (one :: b) | yes y with≡ pr1 | yes z with≡ pr2 rewrite pr1 | pr2 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (goPreservesCanonicalRightOne a b) ) (applyEquality (mapMaybe canonical) pr2)))
goPreservesCanonicalRightOne (one :: a) (one :: b) | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1))))

goPreservesCanonicalRight : (state : Bit) → (a b : BinNat) → mapMaybe canonical (go state a b) ≡ mapMaybe canonical (go state a (canonical b))
goPreservesCanonicalRight zero = goPreservesCanonicalRightZero
goPreservesCanonicalRight one = goPreservesCanonicalRightOne


text:
open import Nat
open import Prelude
open import core
open import contexts

module htype-decidable where
  lemma-l : ∀{t1 t2 t4} → t1 ==> t2 == t1 ==> t4 → t2 == t4
  lemma-l refl = refl

  lemma-r : ∀{t1 t2 t3} → t1 ==> t2 == t3 ==> t2 → t1 == t3
  lemma-r refl = refl

  lemma-b : ∀{t1 t2 t3 t4} → t1 ==> t2 == t3 ==> t4 → t1 == t3
  lemma-b refl = refl

  htype-dec : (t1 t2 : htyp) → t1 == t2 + (t1 == t2 → ⊥)
  htype-dec b b = Inl refl
  htype-dec b ⦇-⦈ = Inr (λ ())
  htype-dec b (t2 ==> t3) = Inr (λ ())
  htype-dec ⦇-⦈ b = Inr (λ ())
  htype-dec ⦇-⦈ ⦇-⦈ = Inl refl
  htype-dec ⦇-⦈ (t2 ==> t3) = Inr (λ ())
  htype-dec (t1 ==> t2) b = Inr (λ ())
  htype-dec (t1 ==> t2) ⦇-⦈ = Inr (λ ())
  htype-dec (t1 ==> t2) (t3 ==> t4) with htype-dec t1 t3 | htype-dec t2 t4
  htype-dec (t1 ==> t2) (.t1 ==> .t2) | Inl refl | Inl refl = Inl refl
  htype-dec (t1 ==> t2) (.t1 ==> t4)  | Inl refl | Inr x₁   = Inr (λ x → x₁ (lemma-l x))
  htype-dec (t1 ==> t2) (t3 ==> .t2)  | Inr x    | Inl refl = Inr (λ x₁ → x (lemma-r x₁))
  htype-dec (t1 ==> t2) (t3 ==> t4)   | Inr x    | Inr x₁   = Inr (λ x₂ → x (lemma-b x₂))

  -- if an arrow is disequal, it disagrees in the first or second argument
  ne-factor : ∀{τ1 τ2 τ3 τ4} → (τ1 ==> τ2) ≠ (τ3 ==> τ4) → (τ1 ≠ τ3) + (τ2 ≠ τ4)
  ne-factor {τ1} {τ2} {τ3} {τ4} ne with htype-dec τ1 τ3 | htype-dec τ2 τ4
  ne-factor ne | Inl refl | Inl refl = Inl (λ x → ne refl)
  ne-factor ne | Inl x | Inr x₁ = Inr x₁
  ne-factor ne | Inr x | Inl x₁ = Inl x
  ne-factor ne | Inr x | Inr x₁ = Inl x

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
open import Agda.Builtin.Nat

-- Matching against negative numbers

lit : Nat → Nat
lit -20 = 0  -- Error thrown here
lit _   = 1

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The two coinductive definitions of weak bisimilarity are pointwise
-- logically equivalent
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Weak.Equivalent {ℓ} {lts : LTS ℓ} where

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

import Bisimilarity.Weak lts as Std
import Bisimilarity.Weak.Alternative lts as Alt
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning

open LTS lts

mutual

  -- The alternative definition of weak bisimilarity can be converted
  -- to the standard one, in a size-preserving way.

  alternative⇒ : ∀ {i p q} → Alt.[ i ] p ≈ q → Std.[ i ] p ≈ q
  alternative⇒ {i} p≈q =
    Std.⟨ lr p≈q
        , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p≈q)
        ⟩
    where
    lr : ∀ {p p′ q μ} →
         Alt.[ i ] p ≈ q → p [ μ ]⟶ p′ →
         ∃ λ q′ → q [ μ ]⇒̂ q′ × Std.[ i ] p′ ≈′ q′
    lr p≈q p⟶p′ =
      Σ-map id (Σ-map id alternative⇒′)
        (Alt.left-to-right p≈q (⟶→⇒̂ p⟶p′))

  alternative⇒′ : ∀ {i p q} → Alt.[ i ] p ≈′ q → Std.[ i ] p ≈′ q
  Std.force (alternative⇒′ p≈′q) = alternative⇒ (Alt.force p≈′q)

mutual

  -- One can also convert in the other direction. Note that this
  -- conversion is not guaranteed to be size-preserving. For at least
  -- one LTS it cannot (in general) be size-preserving, see
  -- Bisimilarity.Weak.Delay-monad.size-preserving-⇒alternative⇔uninhabited.

  ⇒alternative : ∀ {i p q} → p Std.≈ q → Alt.[ i ] p ≈ q
  ⇒alternative {i} p≈q =
    Alt.⟨ lr p≈q
        , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p≈q)
        ⟩
    where
    lr : ∀ {p p′ q μ} →
         p Std.≈ q → p [ μ ]⇒̂ p′ →
         ∃ λ q′ → q [ μ ]⇒̂ q′ × Alt.[ i ] p′ ≈′ q′
    lr p≈q p⇒̂p′ =
      Σ-map id (Σ-map id ⇒alternative′) (Std.weak-is-weak⇒̂ p≈q p⇒̂p′)

  ⇒alternative′ : ∀ {i p q} → p Std.≈ q → Alt.[ i ] p ≈′ q
  Alt.force (⇒alternative′ p≈q) = ⇒alternative p≈q

-- The two definitions of weak bisimilarity are logically equivalent.

alternative⇔ : ∀ {p q} → p Alt.≈ q ⇔ p Std.≈ q
alternative⇔ = record
  { to   = alternative⇒
  ; from = ⇒alternative
  }

-- TODO: I don't know if the two definitions of weak bisimilarity are
-- isomorphic.

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
------------------------------------------------------------------------
-- Monads
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

module Category.Monad where

open import Data.Function
open import Category.Monad.Indexed
open import Data.Unit

RawMonad : (Set → Set) → Set₁
RawMonad M = RawIMonad {⊤} (λ _ _ → M)

RawMonadZero : (Set → Set) → Set₁
RawMonadZero M = RawIMonadZero {⊤} (λ _ _ → M)

RawMonadPlus : (Set → Set) → Set₁
RawMonadPlus M = RawIMonadPlus {⊤} (λ _ _ → M)

module RawMonad {M : Set → Set} (Mon : RawMonad M) where
  open RawIMonad Mon public

module RawMonadZero {M : Set → Set} (Mon : RawMonadZero M) where
  open RawIMonadZero Mon public

module RawMonadPlus {M : Set → Set} (Mon : RawMonadPlus M) where
  open RawIMonadPlus Mon public

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v interaction.give:20 -v tc.cc:60 -v reify.clause:60 -v tc.section.check:10 -v tc:90 #-}
-- {-# OPTIONS -v tc.lhs:20 #-}

module Issue937 where

open import Common.Equality

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

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁
open Σ public

data _≤_ : Nat → Nat → Set  where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

_<_ : Nat → Nat → Set
m < n = suc m ≤ n

ex : Σ Nat (λ n → zero < n)
proj₁ ex = suc zero
proj₂ ex = s≤s z≤n

module _ (A : Set) where

  ex'' : Σ Nat (λ n → zero < n)
  proj₁ ex'' = suc zero
  proj₂ ex'' = s≤s z≤n

test : ex'' Nat ≡ (suc zero , s≤s z≤n)
test = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.Equiv-Polyn-nPoly where

open import Cubical.Foundations.Everything

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Univariate.Base
open import Cubical.Algebra.CommRing.Instances.UnivariatePoly

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open import Cubical.Algebra.Polynomials.Multivariate.Equiv.Poly0-A
open import Cubical.Algebra.Polynomials.Multivariate.Equiv.Poly1-Poly
open import Cubical.Algebra.Polynomials.Multivariate.Equiv.Comp-Poly
open import Cubical.Algebra.Polynomials.Multivariate.Equiv.Induced-Poly

open Nth-Poly-structure
open CommRingEquivs renaming (compCommRingEquiv to _∘-ecr_ ; invCommRingEquiv to inv-ecr)

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Definition

nPoly : (A' : CommRing ℓ) → (n : ℕ) → CommRing ℓ
nPoly A' zero = A'
nPoly A' (suc n) = UnivariatePoly (nPoly A' n)

Equiv-Polyn-nPoly : (A' : CommRing ℓ) → (n : ℕ) → CommRingEquiv (PolyCommRing A' n) (nPoly A' n)
Equiv-Polyn-nPoly A' zero = CRE-Poly0-A A'
Equiv-Polyn-nPoly A' (suc n) = inv-ecr _ _ (CRE-PolyN∘M-PolyN+M A' 1 n)
                               ∘-ecr (lift-equiv-poly _ _ (Equiv-Polyn-nPoly A' n) 1
                               ∘-ecr CRE-Poly1-Poly: (nPoly A' n))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
import cedille-options
open import general-util

module toplevel-state (options : cedille-options.options) {mF : Set → Set} {{_ : monad mF}} where

open import lib

open import cedille-types
open import classify options {mF}
open import ctxt
open import constants
open import conversion
open import rename
open import spans options {mF}
open import syntax-util
open import to-string options
open import string-format
open import subst

import cws-types

record include-elt : Set where
  field ast : maybe start
        cwst : maybe cws-types.start
        deps : 𝕃 string {- dependencies -}
        import-to-dep : trie string {- map import strings in the file to their full paths -}
        ss : spans ⊎ string {- spans in string form (read from disk) -}
        err : 𝔹 -- is ss reporting an error
        need-to-add-symbols-to-context : 𝔹
        do-type-check : 𝔹
        inv : do-type-check imp need-to-add-symbols-to-context ≡ tt
        last-parse-time : maybe UTC
        cede-up-to-date : 𝔹
        rkt-up-to-date : 𝔹

blank-include-elt : include-elt
blank-include-elt = record { ast = nothing ; cwst = nothing; deps = [] ;
                             import-to-dep = empty-trie ; ss = inj₂ "" ; err = ff ; need-to-add-symbols-to-context = tt ;
                             do-type-check = tt ; inv = refl ; last-parse-time = nothing; cede-up-to-date = ff ; rkt-up-to-date = ff }

-- the dependencies should pair import strings found in the file with the full paths to those imported files
new-include-elt : filepath → (dependencies : 𝕃 (string × string)) → (ast : start) →
                  cws-types.start → maybe UTC → include-elt
new-include-elt filename deps x y time =
  record { ast = just x ; cwst = just y ; deps = map snd deps ; import-to-dep = trie-fill empty-trie deps ; ss = inj₂ "" ; err = ff ;
           need-to-add-symbols-to-context = tt ;
           do-type-check = tt ; inv = refl ; last-parse-time = time ; cede-up-to-date = ff ; rkt-up-to-date = ff }

error-include-elt : string → include-elt
error-include-elt err = record blank-include-elt { ss = inj₂ (global-error-string err) ; err = tt }

error-span-include-elt : string → string → posinfo → include-elt
error-span-include-elt err errSpan pos = record blank-include-elt { ss = inj₁ (add-span (span.mk-span err pos (posinfo-plus pos 1) [] (just errSpan) ) empty-spans ) ; err = tt }

set-do-type-check-include-elt : include-elt → 𝔹 → include-elt
set-do-type-check-include-elt ie b =
 record ie { need-to-add-symbols-to-context = (b || include-elt.need-to-add-symbols-to-context ie) ;
             do-type-check = b ;
             inv = lem b }
 where lem : (b : 𝔹) → b imp (b || include-elt.need-to-add-symbols-to-context ie) ≡ tt
       lem tt = refl
       lem ff = refl

set-need-to-add-symbols-to-context-include-elt : include-elt → 𝔹 → include-elt
set-need-to-add-symbols-to-context-include-elt ie b =
 record ie { need-to-add-symbols-to-context = b ;
             do-type-check = b && include-elt.do-type-check ie ;
             inv = lem b }
 where lem : ∀(b : 𝔹){b' : 𝔹} → b && b' imp b ≡ tt
       lem tt {tt} = refl
       lem tt {ff} = refl
       lem ff {tt} = refl
       lem ff {ff} = refl

set-spans-include-elt : include-elt → spans → include-elt
set-spans-include-elt ie ss =
 record ie { ss = inj₁ ss ;
             err = spans-have-error ss  }

set-last-parse-time-include-elt : include-elt → UTC → include-elt
set-last-parse-time-include-elt ie time =
  record ie { last-parse-time = just time }

set-cede-file-up-to-date-include-elt : include-elt → 𝔹 → include-elt
set-cede-file-up-to-date-include-elt ie up-to-date = record ie { cede-up-to-date = up-to-date }
set-rkt-file-up-to-date-include-elt : include-elt → 𝔹 → include-elt
set-rkt-file-up-to-date-include-elt ie up-to-date = record ie { rkt-up-to-date = up-to-date }

set-spans-string-include-elt : include-elt → (err : 𝔹) → string → include-elt
set-spans-string-include-elt ie err ss = record ie { ss = inj₂ ss ; err = err  }

record toplevel-state : Set where
  constructor mk-toplevel-state
  field include-path : 𝕃 string × stringset
        files-with-updated-spans : 𝕃 string
        is : trie include-elt {- keeps track of files we have parsed and/or processed -}
        Γ : ctxt

new-toplevel-state : (include-path : 𝕃 string × stringset) → toplevel-state
new-toplevel-state ip = record { include-path = ip ;
                                                                             files-with-updated-spans = [] ; is = empty-trie ; Γ = new-ctxt "[nofile]" "[nomod]" }

toplevel-state-lookup-occurrences : var → toplevel-state → 𝕃 (var × posinfo × string)
toplevel-state-lookup-occurrences symb (mk-toplevel-state _ _ _ Γ) = ctxt-lookup-occurrences Γ symb

get-include-elt-if : toplevel-state → filepath → maybe include-elt
get-include-elt-if s filename = trie-lookup (toplevel-state.is s) filename

-- get an include-elt assuming it will be there
get-include-elt : toplevel-state → filepath → include-elt
get-include-elt s filename with get-include-elt-if s filename
get-include-elt s filename | nothing = blank-include-elt {- should not happen -}
get-include-elt s filename | just ie = ie

set-include-elt : toplevel-state → filepath → include-elt → toplevel-state
set-include-elt s f ie = record s { is = trie-insert (toplevel-state.is s) f ie }

set-include-path : toplevel-state → 𝕃 string × stringset → toplevel-state
set-include-path s ip = record s { include-path = ip }

get-do-type-check : toplevel-state → string → 𝔹
get-do-type-check s filename = include-elt.do-type-check (get-include-elt s filename)

include-elt-spans-to-rope : include-elt → rope
include-elt-spans-to-rope ie with (include-elt.ss ie)
include-elt-spans-to-rope ie | inj₁ ss = spans-to-rope ss
include-elt-spans-to-rope ie | inj₂ ss = [[ ss ]]

include-elt-to-string : include-elt → string
include-elt-to-string ie =
    " deps:  " ^ (𝕃-to-string (λ x → x) "," (include-elt.deps ie)) ^
    -- ast
    ", ast:  " ^ maybe-else "not parsed" (λ ast → "parsed") (include-elt.ast ie) ^ ", " ^
    " import-to-dep:  " ^ (trie-to-string "," (format "filename: %s") (include-elt.import-to-dep ie)) ^
    -- spans
    " err:  " ^ (𝔹-to-string (include-elt.err ie)) ^
    ", need-to-add-symbols-to-context:  " ^ (𝔹-to-string (include-elt.need-to-add-symbols-to-context ie)) ^
    ", do-type-check:  " ^ (𝔹-to-string (include-elt.do-type-check ie)) ^
    ", last-parse-time: " ^ (maybe-else "" utcToString (include-elt.last-parse-time ie))

params-to-string'' : params → string
params-to-string'' ParamsNil = ""
-- TODO print erased vs non-erased?
params-to-string'' (ParamsCons (Decl pi pi' me v t-k pi'') pms) = "{var: " ^ v ^ ", tk: " ^ rope-to-string (tk-to-string empty-ctxt t-k) ^ "}" ^ ", " ^ (params-to-string'' pms)

defParams-to-string : defParams → string
defParams-to-string (just pms) = params-to-string'' pms
defParams-to-string nothing = ""

-- TODO also print modname?
syms-to-string : trie (string × 𝕃 string) → string
syms-to-string = trie-to-string ", " (λ l → "{" ^ (𝕃-to-string (λ s → s) ", " (snd l)) ^ "}")

ctxt-info-to-string : ctxt-info → string
ctxt-info-to-string (term-decl tp) = "term-decl: {type: " ^ rope-to-string (to-string empty-ctxt tp) ^ "}"
ctxt-info-to-string (term-def dp opac t tp) = "term-def: {defParams: {" ^ (defParams-to-string dp) ^ "}, opacity: " ^ (opacity-to-string opac) ^ ", term: " ^ rope-to-string (to-string empty-ctxt t) ^ ", type: " ^ rope-to-string (to-string empty-ctxt tp) ^ "}"
ctxt-info-to-string (term-udef dp opac t) = "term-udef: {defParams: {" ^ (defParams-to-string dp) ^ "}, opacity: " ^ (opacity-to-string opac) ^ ", term: " ^ rope-to-string (to-string empty-ctxt t) ^ "}"
ctxt-info-to-string (type-decl k) = "type-decl: {kind: " ^ rope-to-string (to-string empty-ctxt k) ^ "}"
ctxt-info-to-string (type-def dp opac tp k) = "type-def: {defParams: {" ^ (defParams-to-string dp) ^ "}, opacity: " ^ (opacity-to-string opac) ^ ", tp: " ^ rope-to-string (to-string empty-ctxt tp) ^ ", kind: " ^ rope-to-string (to-string empty-ctxt k) ^ "}"
ctxt-info-to-string (kind-def pms k) = "kind-def: {pms: " ^ (params-to-string'' pms) ^ "kind: " ^ rope-to-string (to-string empty-ctxt k) ^ "}"
ctxt-info-to-string (rename-def v) = "rename-def: {var: " ^ v ^ "}"
ctxt-info-to-string (var-decl) = "var-decl"
ctxt-info-to-string (const-def _) = "const-def"
ctxt-info-to-string (datatype-def _ _) = "datatype-def"

sym-info-to-string : sym-info → string
sym-info-to-string (ci , (fn , pi)) = "{ctxt-info: " ^ (ctxt-info-to-string ci) ^ ", location: {filename: " ^ fn ^ ", posinfo: " ^ pi ^ "}}"

sym-infos-to-string : trie sym-info → string
sym-infos-to-string = trie-to-string ", " sym-info-to-string

occ-to-string : var × posinfo × string → string
occ-to-string (v , pi , s) = "var: " ^ v ^ ", posinfo: " ^ pi ^ ", string: " ^ s

sym-occs-to-string : trie (𝕃 (var × posinfo × string)) → string
sym-occs-to-string = trie-to-string ", " (λ l → "{" ^ (𝕃-to-string occ-to-string ", " l) ^ "}")

qualif-to-string : qualif-info → string
qualif-to-string (x , as) = x ^ rope-to-string (fst (args-to-string as {TERM} [[]] 0 [] (new-ctxt "" "") nothing neither))

mod-info-to-string : mod-info → string
mod-info-to-string (fn , mn , pms , q) = "filename: " ^ fn ^ ", modname: " ^ mn ^ ", pms: {" ^ (params-to-string'' pms) ^ "}" ^ ", qualif: {" ^ (trie-to-string ", " qualif-to-string q) ^ "}"

ctxt-to-string : ctxt → string
ctxt-to-string (mk-ctxt mi (ss , mn-fn) is os d) = "mod-info: {" ^ (mod-info-to-string mi) ^ "}, syms: {" ^ (syms-to-string ss) ^ "}, i: {" ^ (sym-infos-to-string is) ^ "}, sym-occs: {" ^ (sym-occs-to-string os) ^ "}"

toplevel-state-to-string : toplevel-state → string
toplevel-state-to-string (mk-toplevel-state include-path files is context) =
    "\ninclude-path: {\n" ^ (𝕃-to-string (λ x → x) "\n" (fst include-path)) ^
    "\n}\nis: {" ^ (trie-to-string "\n" include-elt-to-string is) ^
    "\n}\nΓ: {" ^ (ctxt-to-string context) ^ "}"

-- check if a variable is being redefined, and if so return the first given state; otherwise the second (in the monad)
check-redefined : posinfo → var → toplevel-state → spanM toplevel-state → spanM toplevel-state
check-redefined pi x s c =
  get-ctxt (λ Γ →
    if ctxt-binds-var Γ x then
      (spanM-add (redefined-var-span Γ pi x) ≫span spanMr s)
    else c)

import-as : var → optAs → var
import-as v NoOptAs = v
import-as v (SomeOptAs pi pfx) = pfx # v

error-in-import-string = "There is an error in the imported file"

-- Traverse all imports, returning an error if we encounter the same file twice
{-# TERMINATING #-}
check-cyclic-imports : (original current : filepath) → stringset → (path : 𝕃 string) → toplevel-state → err-m
check-cyclic-imports fnₒ fn fs path s with stringset-contains fs fn
...| ff = foldr (λ fnᵢ x → x maybe-or check-cyclic-imports fnₒ fnᵢ (stringset-insert fs fn) (fn :: path) s)
            nothing (include-elt.deps (get-include-elt s fn))
...| tt with fnₒ =string fn
...| tt = just (foldr (λ fnᵢ x → x ^ " → " ^ fnᵢ) ("Cyclic dependencies (" ^ fn) path ^ " → " ^ fn ^ ")")
...| ff = just error-in-import-string

scope-t : Set → Set
scope-t X = filepath → string → optAs → params → args → X → toplevel-state → toplevel-state × err-m

infixl 0 _≫=scope_
_≫=scope_ : toplevel-state × err-m → (toplevel-state → toplevel-state × err-m) → toplevel-state × err-m
_≫=scope_ (ts , err) f with f ts
...| ts' , err' = ts' , err maybe-or err'

{-# TERMINATING #-}
scope-file : toplevel-state → (original imported : filepath) → optAs → args → toplevel-state × err-m
scope-file' : scope-t ⊤
scope-cmds : scope-t cmds
scope-cmd : scope-t cmd
scope-var : scope-t var

scope-file ts fnₒ fnᵢ oa as with check-cyclic-imports fnₒ fnᵢ (trie-single fnₒ triv) [] ts
...| just e = ts , just e
...| nothing = scope-file' fnₒ fnᵢ oa ParamsNil as triv ts

scope-file' fnₒ fn oa psₒ as triv s with get-include-elt s fn
...| ie with include-elt.err ie | include-elt.ast ie
...| e | nothing = s , (maybe-if e) ≫maybe just error-in-import-string
...| e | just (File pi0 is pi1 pi2 mn ps cs pi3) =
  (s , (maybe-if e) ≫maybe just error-in-import-string) ≫=scope
  scope-cmds fn mn oa ps as (imps-to-cmds is) ≫=scope
  scope-cmds fn mn oa ps as cs

scope-cmds fn mn oa ps as (CmdsNext c cs) s =
  scope-cmd fn mn oa ps as c s ≫=scope scope-cmds fn mn oa ps as cs
scope-cmds fn mn oa ps as CmdsStart s = s , nothing

scope-cmd fn mn oa ps as (ImportCmd (Import pi NotPublic pi' ifn oa' as' pi'')) s = s , nothing
scope-cmd fn mn oa psₒ asₒ (ImportCmd (Import pi IsPublic pi' ifn oa' asᵢ' pi'')) s =
  let ifn' = trie-lookup-else ifn (include-elt.import-to-dep (get-include-elt s fn)) ifn in
  scope-file' fn ifn' oa psₒ asᵢ triv s
  -- ^ oa' should be NoOptAs, so we can use oa ^
  where

  merged : trie (maybe arg) → params → args → trie (maybe arg)
  merged σ (ParamsCons (Decl _ _ me x atk _) ps) (ArgsCons a as) =
    merged (trie-insert σ x $ just a) ps as
  merged σ (ParamsCons (Decl _ _ me x atk _) ps) ArgsNil =
    merged (trie-insert σ x nothing) ps ArgsNil
  merged σ _ _ = σ

  arg-var : arg → maybe var
  arg-var (TermArg me (Var pi x)) = just x
  arg-var (TypeArg (TpVar pi x)) = just x
  arg-var _ = nothing

  σ = merged empty-trie psₒ asₒ

  reorder : args → args
  reorder (ArgsCons a as) =
    maybe-else' (arg-var a ≫=maybe trie-lookup σ) (ArgsCons a $ reorder as) λ ma →
    maybe-else' ma ArgsNil λ a → ArgsCons a $ reorder as
  reorder ArgsNil = ArgsNil

  asᵢ = reorder $ qualif-args (toplevel-state.Γ s) asᵢ'

scope-cmd fn mn oa ps as (DefKind _ v _ _ _) = scope-var fn mn oa ps as v
scope-cmd fn mn oa ps as (DefTermOrType _ (DefTerm _ v _ _) _) = scope-var fn mn oa ps as v
scope-cmd fn mn oa ps as (DefTermOrType _ (DefType _ v _ _) _) = scope-var fn mn oa ps as v
scope-cmd fn mn oa ps as (DefDatatype (Datatype _ _ v _ _ _ _) _) = scope-var fn mn oa ps as v

scope-var _ mn oa ps as v s with import-as v oa | s
...| v' | mk-toplevel-state ip fns is (mk-ctxt (mn' , fn , pms , q) ss sis os d) =
  mk-toplevel-state ip fns is (mk-ctxt (mn' , fn , pms , trie-insert q v' (mn # v , as)) ss sis os d) ,
  flip maybe-map (trie-lookup q v') (uncurry λ v'' as' →
    "Multiple definitions of variable " ^ v' ^ " as " ^ v'' ^ " and " ^ (mn # v) ^
    (if (mn # v =string v'') then " (perhaps it was already imported?)" else ""))

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module nodcap.NF.Typing where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺ using (ℕ⁺; suc; _+_)
open import Data.Environment
open import Data.List as L using (List; []; _∷_; _++_)
open import Data.List.Any as LA using (Any; here; there)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import nodcap.Base
open import nodcap.Typing as FF using (⊢_)

-- Typing Rules.

infix 1 ⊢ⁿᶠ_

data ⊢ⁿᶠ_ : Environment → Set where

  send : {Γ Δ : Environment} {A B : Type} →

       ⊢ⁿᶠ A ∷ Γ → ⊢ⁿᶠ B ∷ Δ →
       -------------------
       ⊢ⁿᶠ A ⊗ B ∷ Γ ++ Δ

  recv : {Γ : Environment} {A B : Type} →

       ⊢ⁿᶠ A ∷ B ∷ Γ →
       -------------
       ⊢ⁿᶠ A ⅋ B ∷ Γ

  sel₁ : {Γ : Environment} {A B : Type} →

       ⊢ⁿᶠ A ∷ Γ →
       -----------
       ⊢ⁿᶠ A ⊕ B ∷ Γ

  sel₂ : {Γ : Environment} {A B : Type} →

       ⊢ⁿᶠ B ∷ Γ →
       -----------
       ⊢ⁿᶠ A ⊕ B ∷ Γ

  case : {Γ : Environment} {A B : Type} →

       ⊢ⁿᶠ A ∷ Γ → ⊢ⁿᶠ B ∷ Γ →
       -------------------
       ⊢ⁿᶠ A & B ∷ Γ

  halt :

       --------
       ⊢ⁿᶠ 𝟏 ∷ []

  wait : {Γ : Environment} →

       ⊢ⁿᶠ Γ →
       -------
       ⊢ⁿᶠ ⊥ ∷ Γ

  loop : {Γ : Environment} →

       -------
       ⊢ⁿᶠ ⊤ ∷ Γ

  mk?₁ : {Γ : Environment} {A : Type} →

       ⊢ⁿᶠ A ∷ Γ →
       ---------------------
       ⊢ⁿᶠ ?[ 1 ] A ∷ Γ

  mk!₁ : {Γ : Environment} {A : Type} →

       ⊢ⁿᶠ A ∷ Γ →
       ---------------------
       ⊢ⁿᶠ ![ 1 ] A ∷ Γ

  cont : {Γ : Environment} {A : Type} {m n : ℕ⁺} →

       ⊢ⁿᶠ ?[ m ] A ∷ ?[ n ] A ∷ Γ →
       ------------------------------
       ⊢ⁿᶠ ?[ m + n ] A ∷ Γ

  pool : {Γ Δ : Environment} {A : Type} {m n : ℕ⁺} →

       ⊢ⁿᶠ ![ m ] A ∷ Γ → ⊢ⁿᶠ ![ n ] A ∷ Δ →
       -------------------------------------
       ⊢ⁿᶠ ![ m + n ] A ∷ Γ ++ Δ

  exch : {Γ Δ : Environment} →

       Γ ∼[ bag ] Δ → ⊢ⁿᶠ Γ →
       --------------------
       ⊢ⁿᶠ Δ

fromNF : {Γ : Environment} → ⊢ⁿᶠ Γ → ⊢ Γ
fromNF (send x y) = FF.send (fromNF x) (fromNF y)
fromNF (recv x)   = FF.recv (fromNF x)
fromNF (sel₁ x)   = FF.sel₁ (fromNF x)
fromNF (sel₂ x)   = FF.sel₂ (fromNF x)
fromNF (case x y) = FF.case (fromNF x) (fromNF y)
fromNF  halt      = FF.halt
fromNF (wait x)   = FF.wait (fromNF x)
fromNF  loop      = FF.loop
fromNF (mk?₁ x)   = FF.mk?₁ (fromNF x)
fromNF (mk!₁ x)   = FF.mk!₁ (fromNF x)
fromNF (cont x)   = FF.cont (fromNF x)
fromNF (pool x y) = FF.pool (fromNF x) (fromNF y)
fromNF (exch x y) = FF.exch x (fromNF y)

-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
-- {-# OPTIONS -v tc.check.app:70 #-}
-- {-# OPTIONS -v tc.proj.amb:30 #-}

record S : Set₁ where
  field X : Set

record T : Set₁ where
  field X : Set

open S
open T

ok : S → Set
ok s = X s

test : S → Set
test s = s .X

-- Error WAS:
-- Cannot resolve overloaded projection X because it is not applied to
-- a visible argument
-- when inferring the type of .X

-- Should succeed.


text:
open import Data.Nat
open import Data.Vec using ( Vec ; [] ; _∷_ )
module OpenTheory2 where

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

data _∈_ {A : Set} : A → {n : ℕ} → Vec A n → Set where
  here  : {n : ℕ} {x : A} {xs : Vec A n} → x ∈ (x ∷ xs)
  there : {n : ℕ} {x y : A} {xs : Vec A n} (p : x ∈ xs) → x ∈ (y ∷ xs)

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

max_stars_repo_name: larrytheliquid/generic-elim

max_issues_repo_name: larrytheliquid/generic-elim

max_forks_repo_name: larrytheliquid/generic-elim


text:
------------------------------------------------------------------------------
-- Properties of the inequalities
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Inequalities.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP
open import FOTC.Data.Nat.PropertiesATP

------------------------------------------------------------------------------
-- N.B. The elimination properties are in the module
-- FOTC.Data.Nat.Inequalities.EliminationProperties.

0≯x : ∀ {n} → N n → zero ≯ n
0≯x nzero = prf
  where postulate prf : zero ≯ zero
        {-# ATP prove prf #-}
0≯x (nsucc {n} Nn) = prf
  where postulate prf : zero ≯ succ₁ n
        {-# ATP prove prf #-}

0≮x→x≡0 : ∀ {n} → N n → zero ≮ n → n ≡ zero
0≮x→x≡0 nzero h = refl
0≮x→x≡0 (nsucc {n} Nn) h = prf
  where postulate prf : succ₁ n ≡ zero
        {-# ATP prove prf #-}

x≮x : ∀ {n} → N n → n ≮ n
x≮x nzero = prf
  where postulate prf : zero ≮ zero
        {-# ATP prove prf #-}
x≮x (nsucc {n} Nn) = prf (x≮x Nn)
  where postulate prf : n ≮ n → succ₁ n ≮ succ₁ n
        {-# ATP prove prf #-}

Sx≰0 : ∀ {n} → N n → succ₁ n ≰ zero
Sx≰0 nzero = prf
  where postulate prf : succ₁ zero ≰ zero
        {-# ATP prove prf #-}
Sx≰0 (nsucc {n} Nn) = prf
  where postulate prf : succ₁ (succ₁ n) ≰ zero
        {-# ATP prove prf #-}

x<Sx : ∀ {n} → N n → n < succ₁ n
x<Sx nzero = lt-0S zero
x<Sx (nsucc {n} Nn) = prf (x<Sx Nn)
  where postulate prf : n < succ₁ n → succ₁ n < succ₁ (succ₁ n)
        {-# ATP prove prf #-}

postulate x<y→Sx<Sy : ∀ {m n} → m < n → succ₁ m < succ₁ n
{-# ATP prove x<y→Sx<Sy #-}

postulate Sx<Sy→x<y : ∀ {m n} → succ₁ m < succ₁ n → m < n
{-# ATP prove Sx<Sy→x<y #-}

x<y→x<Sy : ∀ {m n} → N m → N n → m < n → m < succ₁ n
x<y→x<Sy {m} Nm nzero h = prf
  where postulate prf : m < succ₁ zero
        {-# ATP prove prf x<0→⊥ #-}
x<y→x<Sy nzero (nsucc {n} Nn) _ = lt-0S (succ₁ n)
x<y→x<Sy (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x<y→x<Sy Nm Nn m<n)
  where
  postulate m<n : m < n
  {-# ATP prove m<n #-}

  postulate prf : m < succ₁ n → succ₁ m < succ₁ (succ₁ n)
  {-# ATP prove prf #-}

x≤x : ∀ {n} → N n → n ≤ n
x≤x nzero = lt-0S zero
x≤x (nsucc {n} Nn) = prf (x≤x Nn)
  where postulate prf : n ≤ n → succ₁ n ≤ succ₁ n
        {-# ATP prove prf #-}

postulate 2*SSx≥2 : ∀ {n} → N n →
                    succ₁ (succ₁ zero) * succ₁ (succ₁ n) ≥ succ₁ (succ₁ zero)
{-# ATP prove 2*SSx≥2 #-}

postulate x≤y→Sx≤Sy : ∀ {m n} → m ≤ n → succ₁ m ≤ succ₁ n
{-# ATP prove x≤y→Sx≤Sy #-}

postulate Sx≤Sy→x≤y : ∀ {m n} → succ₁ m ≤ succ₁ n → m ≤ n
{-# ATP prove Sx≤Sy→x≤y #-}

postulate Sx≤y→x≤y : ∀ {m n} → N m → N n → succ₁ m ≤ n → m ≤ n
{-# ATP prove Sx≤y→x≤y x<y→x<Sy #-}

postulate x≰y→Sx≰Sy : ∀ m n → m ≰ n → succ₁ m ≰ succ₁ n
{-# ATP prove x≰y→Sx≰Sy #-}

x>y→y<x : ∀ {m n} → N m → N n → m > n → n < m
x>y→y<x {n = n} nzero Nn h = prf
  where postulate prf : n < zero
        {-# ATP prove prf #-}
x>y→y<x (nsucc {m} Nm) nzero _ = lt-0S m
x>y→y<x (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x>y→y<x Nm Nn m>n)
  where
  postulate m>n : m > n
  {-# ATP prove m>n #-}

  postulate prf : n < m → succ₁ n < succ₁ m
  {-# ATP prove prf #-}

x≥y→x≮y : ∀ {m n} → N m → N n → m ≥ n → m ≮ n
x≥y→x≮y nzero nzero h = prf
  where postulate prf : zero ≮ zero
        {-# ATP prove prf #-}
x≥y→x≮y nzero (nsucc {n} Nn) h = prf
  where postulate prf : zero ≮ succ₁ n
        {-# ATP prove prf 0≥S→⊥ #-}
x≥y→x≮y (nsucc {m} Nm) nzero _ = lt-S0 m
x≥y→x≮y (nsucc {m} Nm) (nsucc {n} Nn) h =
  prf (x≥y→x≮y Nm Nn m≥n)
  where
  postulate m≥n : m ≥ n
  {-# ATP prove m≥n #-}

  postulate prf : m ≮ n → succ₁ m ≮ succ₁ n
  {-# ATP prove prf #-}

x≮y→x≥y : ∀ {m n} → N m → N n → m ≮ n → m ≥ n
x≮y→x≥y nzero nzero h = prf
  where postulate prf : zero ≥ zero
        {-# ATP prove prf #-}
x≮y→x≥y nzero (nsucc {n} Nn) h = prf
   where postulate prf : zero ≥ succ₁ n
         {-# ATP prove prf #-}
x≮y→x≥y (nsucc {m} Nm) nzero _ = lt-0S (succ₁ m)
x≮y→x≥y (nsucc {m} Nm) (nsucc {n} Nn) h =
  prf (x≮y→x≥y Nm Nn m≮n)
  where
  postulate m≮n : m ≮ n
  {-# ATP prove m≮n #-}
  postulate prf : m ≥ n → succ₁ m ≥ succ₁ n
  {-# ATP prove prf #-}

x>y→x≰y : ∀ {m n} → N m → N n → m > n → m ≰ n
x>y→x≰y {n = n} nzero Nn h = prf
  where postulate prf : zero ≰ n
        {-# ATP prove prf 0>x→⊥ #-}
x>y→x≰y (nsucc {m} Nm) nzero h = prf
  where postulate prf : succ₁ m ≰ zero
        {-# ATP prove prf Sx≰0 #-}
x>y→x≰y (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x>y→x≰y Nm Nn m>n)
  where
  postulate m>n : m > n
  {-# ATP prove m>n #-}

  postulate prf : m ≰ n → succ₁ m ≰ succ₁ n
  {-# ATP prove prf #-}

x>y∨x≤y : ∀ {m n} → N m → N n → m > n ∨ m ≤ n
x>y∨x≤y {n = n} nzero Nn = prf
  where postulate prf : zero > n ∨ zero ≤ n
        {-# ATP prove prf #-}
x>y∨x≤y (nsucc {m} Nm) nzero = prf
  where postulate prf : succ₁ m > zero ∨ succ₁ m  ≤ zero
        {-# ATP prove prf #-}
x>y∨x≤y (nsucc {m} Nm) (nsucc {n} Nn) = prf (x>y∨x≤y Nm Nn)
  where postulate prf : m > n ∨ m ≤ n → succ₁ m > succ₁ n ∨ succ₁ m ≤ succ₁ n
        {-# ATP prove prf #-}

x<y∨x≥y : ∀ {m n} → N m → N n → m < n ∨ m ≥ n
x<y∨x≥y Nm Nn = x>y∨x≤y Nn Nm

x<y∨x≮y : ∀ {m n} → N m → N n → m < n ∨ m ≮ n
x<y∨x≮y nzero nzero = prf
  where postulate prf : zero < zero ∨ zero ≮ zero
        {-# ATP prove prf #-}
x<y∨x≮y nzero (nsucc {n} Nn) = prf
  where postulate prf : zero < succ₁ n ∨ zero ≮ succ₁ n
        {-# ATP prove prf #-}
x<y∨x≮y (nsucc {m} Nm) nzero = prf
  where postulate prf : succ₁ m < zero ∨ succ₁ m ≮ zero
        {-# ATP prove prf #-}
x<y∨x≮y (nsucc {m} Nm) (nsucc {n} Nn) = prf (x<y∨x≮y Nm Nn)
  where postulate prf : m < n ∨ m ≮ n → succ₁ m < succ₁ n ∨ succ₁ m ≮ succ₁ n
        {-# ATP prove prf #-}

x≤y∨x≰y : ∀ {m n} → N m → N n → m ≤ n ∨ m ≰ n
x≤y∨x≰y {n = n} nzero Nn = prf
  where postulate prf : zero ≤ n ∨ zero ≰ n
        {-# ATP prove prf #-}
x≤y∨x≰y (nsucc {m} Nm) nzero = prf
  where postulate prf : succ₁ m ≤ zero ∨ succ₁ m ≰ zero
        {-# ATP prove prf Sx≰0 #-}
x≤y∨x≰y (nsucc {m} Nm) (nsucc {n} Nn) = prf (x≤y∨x≰y Nm Nn)
  where postulate prf : m ≤ n ∨ m ≰ n → succ₁ m ≤ succ₁ n ∨ succ₁ m ≰ succ₁ n
        {-# ATP prove prf #-}

postulate x≡y→x≤y : ∀ {m n} → N m → N n → m ≡ n → m ≤ n
{-# ATP prove x≡y→x≤y x≤x #-}

x<y→x≤y : ∀ {m n} → N m → N n → m < n → m ≤ n
x<y→x≤y {m} Nm nzero h = prf
  where postulate prf : m ≤ zero
        {-# ATP prove prf x<0→⊥ #-}
x<y→x≤y nzero  (nsucc {n} Nn) _ = lt-0S (succ₁ n)
x<y→x≤y (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x<y→x≤y Nm Nn m<n)
  where
  postulate m<n : m < n
  {-# ATP prove m<n #-}

  postulate prf : m ≤ n → succ₁ m ≤ succ₁ n
  {-# ATP prove prf #-}

x<Sy→x≤y : ∀ {m n} → N m → N n → m < succ₁ n → m ≤ n
x<Sy→x≤y {n = n} nzero      Nn _     = lt-0S n
x<Sy→x≤y         (nsucc Nm) Nn Sm<Sn = Sm<Sn

x≤y→x<Sy : ∀ {m n} → N m → N n → m ≤ n → m  < succ₁ n
x≤y→x<Sy {n = n} nzero      Nn _    = lt-0S n
x≤y→x<Sy         (nsucc Nm) Nn Sm≤n = Sm≤n

x≤Sx : ∀ {m} → N m → m ≤ succ₁ m
x≤Sx nzero = lt-0S (succ₁ zero)
x≤Sx (nsucc {m} Nm) = prf (x≤Sx Nm)
  where postulate prf : m ≤ succ₁ m → succ₁ m ≤ succ₁ (succ₁ m)
        {-# ATP prove prf #-}

x<y→Sx≤y : ∀ {m n} → N m → N n → m < n → succ₁ m ≤ n
x<y→Sx≤y {m} Nm nzero h = prf
  where postulate prf : succ₁ m ≤ zero
        {-# ATP prove prf x<0→⊥ #-}
x<y→Sx≤y nzero (nsucc {n} Nn) h = prf
  where postulate prf : succ₁ zero ≤ succ₁ n
        {-# ATP prove prf x<0→⊥ #-}
x<y→Sx≤y (nsucc {m} Nm) (nsucc {n} Nn) h = prf
  where postulate prf : succ₁ (succ₁ m) ≤ succ₁ n
        {-# ATP prove prf #-}

Sx≤y→x<y : ∀ {m n} → N m → N n → succ₁ m ≤ n → m < n
Sx≤y→x<y {m} Nm nzero h = prf
  where postulate prf : m < zero
        {-# ATP prove prf S≤0→⊥ #-}
Sx≤y→x<y nzero (nsucc {n} Nn) _  = lt-0S n
Sx≤y→x<y (nsucc {m} Nm) (nsucc {n} Nn) h = prf (Sx≤y→x<y Nm Nn Sm≤n)
  where
  postulate Sm≤n : succ₁ m ≤ n
  {-# ATP prove Sm≤n  #-}

  postulate prf : m < n → succ₁ m < succ₁ n
  {-# ATP prove prf  #-}

x≤y→x≯y : ∀ {m n} → N m → N n → m ≤ n → m ≯ n
x≤y→x≯y nzero nzero h = prf
  where postulate prf : zero ≯ zero
        {-# ATP prove prf #-}
x≤y→x≯y nzero (nsucc {n} Nn) h = prf
  where postulate prf : zero ≯ succ₁ n
        {-# ATP prove prf #-}
x≤y→x≯y (nsucc {m} Nm) nzero h = prf
  where postulate prf : succ₁ m ≯ zero
        {-# ATP prove prf S≤0→⊥ #-}
x≤y→x≯y (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x≤y→x≯y Nm Nn m≤n)
  where
  postulate m≤n : m ≤ n
  {-# ATP prove m≤n #-}

  postulate prf : m ≯ n → succ₁ m ≯ succ₁ n
  {-# ATP prove prf #-}

x≯y→x≤y : ∀ {m n} → N m → N n → m ≯ n → m ≤ n
x≯y→x≤y {n = n} nzero Nn _ = lt-0S n
x≯y→x≤y (nsucc {m} Nm) nzero h = prf
  where postulate prf : succ₁ m ≤ zero
        {-# ATP prove prf #-}
x≯y→x≤y (nsucc {m} Nm) (nsucc {n} Nn) h =
  prf (x≯y→x≤y Nm Nn m≯n)
  where
  postulate m≯n : m ≯ n
  {-# ATP prove m≯n #-}

  postulate prf : m ≤ n → succ₁ m ≤ succ₁ n
  {-# ATP prove prf #-}

Sx≯y→x≯y : ∀ {m n} → N m → N n → succ₁ m ≯ n → m ≯ n
Sx≯y→x≯y nzero nzero h = prf
  where postulate prf : zero ≯ zero
        {-# ATP prove prf #-}
Sx≯y→x≯y nzero (nsucc {n} Nn) h = prf
  where postulate prf : zero ≯ succ₁ n
        {-# ATP prove prf #-}
Sx≯y→x≯y (nsucc {m} Nm) nzero h = prf
  where postulate prf : succ₁ m ≯ zero
        {-# ATP prove prf #-}
Sx≯y→x≯y (nsucc {m} Nm) (nsucc {n} Nn) h = prf (Sx≯y→x≯y Nm Nn Sm≯n)
  where
  postulate Sm≯n : succ₁ m ≯ n
  {-# ATP prove Sm≯n #-}
  postulate prf : m ≯ n → succ₁ m ≯ succ₁ n
  {-# ATP prove prf #-}

x>y∨x≯y : ∀ {m n} → N m → N n → m > n ∨ m ≯ n
x>y∨x≯y {n = n} nzero Nn = prf
  where postulate prf : zero > n ∨ zero ≯ n
        {-# ATP prove prf 0≯x #-}
x>y∨x≯y (nsucc {m} Nm) nzero = prf
  where postulate prf : succ₁ m > zero ∨ succ₁ m ≯ zero
        {-# ATP prove prf #-}
x>y∨x≯y (nsucc {m} Nm) (nsucc {n} Nn) = prf (x>y∨x≯y Nm Nn)
  where postulate prf : m > n ∨ m ≯ n →
                        succ₁ m > succ₁ n ∨ succ₁ m ≯ succ₁ n
        {-# ATP prove prf #-}

<-trans : ∀ {m n o} → N m → N n → N o → m < n → n < o → m < o
<-trans {o = o} nzero nzero No h₁ h₂ = prf
  where postulate prf : zero < o
        {-# ATP prove prf #-}
<-trans nzero (nsucc Nn) nzero h₁ h₂ = prf
  where postulate prf : zero < zero
        {-# ATP prove prf #-}
<-trans nzero (nsucc Nn) (nsucc {o} No) _ _ = lt-0S o
<-trans (nsucc {m} Nm) Nn nzero h₁ h₂ = prf
  where postulate prf : succ₁ m < zero
        {-# ATP prove prf x<0→⊥ #-}
<-trans (nsucc {m} Nm) nzero (nsucc {o} No) h₁ h₂ = prf
  where postulate prf : succ₁ m < succ₁ o
        {-# ATP prove prf #-}
<-trans (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) h₁ h₂ =
  prf (<-trans Nm Nn No m<n n<o)
  where
  postulate m<n : m < n
  {-# ATP prove m<n #-}

  postulate n<o : n < o
  {-# ATP prove n<o #-}

  postulate prf : m < o → succ₁ m < succ₁ o
  {-# ATP prove prf #-}

≤-trans : ∀ {m n o} → N m → N n → N o → m ≤ n → n ≤ o → m ≤ o
≤-trans {o = o} nzero Nn No _ _ = lt-0S o
≤-trans {o = o} (nsucc {m} Nm) nzero No h₁ h₂ = prf
  where postulate prf : succ₁ m ≤ o
        {-# ATP prove prf S≤0→⊥ #-}
≤-trans (nsucc {m} Nm) (nsucc Nn) nzero h₁ h₂ = prf
  where postulate prf : succ₁ m ≤ zero
        {-# ATP prove prf S≤0→⊥ #-}
≤-trans (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) h₁ h₂ =
  prf (≤-trans Nm Nn No m≤n n≤o)
  where
  postulate m≤n : m ≤ n
  {-# ATP prove m≤n #-}

  postulate n≤o : n ≤ o
  {-# ATP prove n≤o #-}

  postulate prf : m ≤ o → succ₁ m ≤ succ₁ o
  {-# ATP prove prf #-}

pred-≤ : ∀ {n} → N n → pred₁ n ≤ n
pred-≤ nzero = prf
  where postulate prf : pred₁ zero ≤ zero
        {-# ATP prove prf #-}
pred-≤ (nsucc {n} Nn) = prf
  where postulate prf : pred₁ (succ₁ n) ≤ succ₁ n
        {-# ATP prove prf <-trans x<Sx #-}

x≤x+y : ∀ {m n} → N m → N n → m ≤ m + n
x≤x+y {n = n} nzero          Nn = lt-0S (zero + n)
x≤x+y {n = n} (nsucc {m} Nm) Nn = prf (x≤x+y Nm Nn)
  where postulate prf : m ≤ m + n → succ₁ m ≤ succ₁ m + n
        {-# ATP prove prf #-}

x<x+Sy : ∀ {m n} → N m → N n → m < m + succ₁ n
x<x+Sy {n = n} nzero Nn = prf0
  where postulate prf0 : zero < zero + succ₁ n
        {-# ATP prove prf0 #-}
x<x+Sy {n = n} (nsucc {m} Nm) Nn = prfS (x<x+Sy Nm Nn)
  where postulate prfS : m < m + succ₁ n → succ₁ m < succ₁ m + succ₁ n
        {-# ATP prove prfS #-}

k+x<k+y→x<y : ∀ {m n k} → N m → N n → N k → k + m < k + n → m < n
k+x<k+y→x<y {m} {n} Nm Nn nzero h = prf0
  where postulate prf0 : m < n
        {-# ATP prove prf0 #-}
k+x<k+y→x<y {m} {n} Nm Nn (nsucc {k} Nk) h = k+x<k+y→x<y Nm Nn Nk prfS
  where postulate prfS : k + m < k + n
        {-# ATP prove prfS #-}

postulate x+k<y+k→x<y : ∀ {m n k} → N m → N n → N k →
                        m + k < n + k → m < n
{-# ATP prove x+k<y+k→x<y k+x<k+y→x<y +-comm #-}

x≤y→k+x≤k+y : ∀ {m n k} → N m → N n → N k → m ≤ n → k + m ≤ k + n
x≤y→k+x≤k+y {m} {n} Nm Nn nzero h = prf0
  where postulate prf0 : zero + m ≤ zero + n
        {-# ATP prove prf0 #-}
x≤y→k+x≤k+y {m} {n} Nm Nn (nsucc {k} Nk) h = prfS (x≤y→k+x≤k+y Nm Nn Nk h)
  where postulate prfS : k + m ≤ k + n → succ₁ k + m ≤ succ₁ k + n
        {-# ATP prove prfS #-}

postulate x≤y→x+k≤y+k : ∀ {m n k} → N m → N n → N k → m ≤ n → m + k ≤ n + k
{-# ATP prove x≤y→x+k≤y+k x≤y→k+x≤k+y +-comm #-}

x<y→Sx∸y≡0 : ∀ {m n} → N m → N n → m < n → succ₁ m ∸ n ≡ zero
x<y→Sx∸y≡0 {m} Nm nzero h = prfx0
  where postulate prfx0 : succ₁ m ∸ zero ≡ zero
        {-# ATP prove prfx0 x<0→⊥ #-}
x<y→Sx∸y≡0 nzero (nsucc {n} Nn) h = prf0S
  where postulate prf0S : succ₁ zero ∸ succ₁ n ≡ zero
        {-# ATP prove prf0S S∸S 0∸x #-}
x<y→Sx∸y≡0 (nsucc {m} Nm) (nsucc {n} Nn) h = prfSS (x<y→Sx∸y≡0 Nm Nn m<n)
  where
  postulate m<n : m < n
  {-# ATP prove m<n #-}

  postulate prfSS : succ₁ m ∸ n ≡ zero → succ₁ (succ₁ m) ∸ succ₁ n ≡ zero
  {-# ATP prove prfSS S∸S #-}

postulate x≤y→x∸y≡0 : ∀ {m n} → N m → N n → m ≤ n → m ∸ n ≡ zero
{-# ATP prove x≤y→x∸y≡0 x<y→Sx∸y≡0 S∸S #-}

x<y→0<y∸x : ∀ {m n} → N m → N n → m < n → zero < n ∸ m
x<y→0<y∸x {m} Nm nzero h = prfx0
  where postulate prfx0 : zero < zero ∸ m
        {-# ATP prove prfx0 x<0→⊥ #-}
x<y→0<y∸x nzero (nsucc {n} Nn) h = prf0S
  where postulate prf0S : zero < succ₁ n ∸ zero
        {-# ATP prove prf0S #-}
x<y→0<y∸x (nsucc {m} Nm) (nsucc {n} Nn) h = prfSS (x<y→0<y∸x Nm Nn m<n)
  where
  postulate m<n : m < n
  {-# ATP prove m<n #-}

  postulate prfSS : zero < n ∸ m → zero < succ₁ n ∸ succ₁ m
  {-# ATP prove prfSS S∸S #-}

0<x∸y→0<Sx∸y : ∀ {m n} → N m → N n → zero < m ∸ n → zero < succ₁ m ∸ n
0<x∸y→0<Sx∸y {m} Nm nzero h = prfx0
  where postulate prfx0 : zero < succ₁ m ∸ zero
        {-# ATP prove prfx0 #-}
0<x∸y→0<Sx∸y nzero (nsucc {n} Nn) h = prf0S
  where postulate prf0S : zero < succ₁ zero ∸ succ₁ n
        {-# ATP prove prf0S 0∸x x<0→⊥ #-}
0<x∸y→0<Sx∸y (nsucc {m} Nm) (nsucc {n} Nn) h = prfSS (0<x∸y→0<Sx∸y Nm Nn 0<m-n)
  where
  postulate 0<m-n : zero < m ∸ n
  {-# ATP prove 0<m-n S∸S #-}

  postulate prfSS : zero < succ₁ m ∸ n → zero < succ₁ (succ₁ m) ∸ succ₁ n
  {-# ATP prove prfSS <-trans S∸S #-}

x∸y<Sx : ∀ {m n} → N m → N n → m ∸ n < succ₁ m
x∸y<Sx {m} Nm nzero = prf
  where postulate prf : m ∸ zero < succ₁ m
        {-# ATP prove prf x<Sx #-}
x∸y<Sx nzero (nsucc {n} Nn) = prf
  where postulate prf : zero ∸ succ₁ n < succ₁ zero
        {-# ATP prove prf 0∸x #-}
x∸y<Sx (nsucc {m} Nm) (nsucc {n} Nn) = prf (x∸y<Sx Nm Nn)
  where postulate prf : m ∸ n < succ₁ m → succ₁ m ∸ succ₁ n < succ₁ (succ₁ m)
        {-# ATP prove prf <-trans ∸-N x<Sx S∸S #-}

postulate Sx∸Sy<Sx : ∀ {m n} → N m → N n → succ₁ m ∸ succ₁ n < succ₁ m
{-# ATP prove Sx∸Sy<Sx x∸y<Sx S∸S #-}

x<x∸y→⊥ : ∀ {m n} → N m → N n → ¬ (m < m ∸ n)
x<x∸y→⊥ {m} Nm nzero h = prf
  where postulate prf : ⊥
        {-# ATP prove prf x<x→⊥ #-}
x<x∸y→⊥ nzero (nsucc Nn) h = prf
 where postulate prf : ⊥
       {-# ATP prove prf x<x→⊥ 0∸x #-}
x<x∸y→⊥ (nsucc Nm) (nsucc Nn) h = prf
  where postulate prf : ⊥
        {-# ATP prove prf ∸-N x<y→y<x→⊥ x∸y<Sx S∸S #-}

postulate x∸Sy≤x∸y : ∀ {m n} → N m → N n → m ∸ succ₁ n ≤ m ∸ n
{-# ATP prove x∸Sy≤x∸y pred-≤ ∸-N #-}

x>y→x∸y+y≡x : ∀ {m n} → N m → N n → m > n → (m ∸ n) + n ≡ m
x>y→x∸y+y≡x {n = n} nzero Nn h = prf
  where postulate prf : zero ∸ n + n ≡ zero
        {-# ATP prove prf 0>x→⊥ #-}
x>y→x∸y+y≡x (nsucc {m} Nm) nzero h = prf
  where postulate prf : (succ₁ m ∸ zero) + zero ≡ succ₁ m
        {-# ATP prove prf +-rightIdentity ∸-N #-}
x>y→x∸y+y≡x (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x>y→x∸y+y≡x Nm Nn m>n)
  where
  postulate m>n : m > n
  {-# ATP prove m>n #-}

  postulate prf : (m ∸ n) + n ≡ m → (succ₁ m ∸ succ₁ n) + succ₁ n ≡ succ₁ m
  {-# ATP prove prf +-comm ∸-N S∸S #-}

x≤y→y∸x+x≡y : ∀ {m n} → N m → N n → m ≤ n → (n ∸ m) + m ≡ n
x≤y→y∸x+x≡y {n = n} nzero Nn h = prf
  where postulate prf : (n ∸ zero) + zero ≡ n
        {-# ATP prove prf +-rightIdentity ∸-N #-}
x≤y→y∸x+x≡y (nsucc {m} Nm) nzero h = prf
  where postulate prf : (zero ∸ succ₁ m) + succ₁ m ≡ zero
        {-# ATP prove prf S≤0→⊥ #-}
x≤y→y∸x+x≡y (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x≤y→y∸x+x≡y Nm Nn m≤n)
  where
  postulate m≤n : m ≤ n
  {-# ATP prove m≤n #-}

  postulate prf : (n ∸ m) + m ≡ n → (succ₁ n ∸ succ₁ m) + succ₁ m ≡ succ₁ n
  {-# ATP prove prf +-comm ∸-N S∸S #-}

x<Sy→x<y∨x≡y : ∀ {m n} → N m → N n → m < succ₁ n → m < n ∨ m ≡ n
x<Sy→x<y∨x≡y nzero nzero h = inj₂ refl
x<Sy→x<y∨x≡y nzero (nsucc {n} Nn) h = inj₁ (lt-0S n)
x<Sy→x<y∨x≡y (nsucc {m} Nm) nzero h = prf
  where postulate prf : succ₁ m < zero ∨ succ₁ m ≡ zero
        {-# ATP prove prf x<0→⊥ #-}
x<Sy→x<y∨x≡y (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x<Sy→x<y∨x≡y Nm Nn m<Sn)
  where
    postulate m<Sn : m < succ₁ n
    {-# ATP prove m<Sn #-}

    postulate prf : m < n ∨ m ≡ n → succ₁ m < succ₁ n ∨ succ₁ m ≡ succ₁ n
    {-# ATP prove prf #-}

x≤y→x<y∨x≡y : ∀ {m n} → N m → N n → m ≤ n → m < n ∨ m ≡ n
x≤y→x<y∨x≡y = x<Sy→x<y∨x≡y

postulate x<y→y≡z→x<z : ∀ {m n o} → m < n → n ≡ o → m < o
{-# ATP prove x<y→y≡z→x<z #-}

postulate x≡y→y<z→x<z : ∀ {m n o} → m ≡ n → n < o → m < o
{-# ATP prove x≡y→y<z→x<z #-}

x≯Sy→x≯y∨x≡Sy : ∀ {m n} → N m → N n → m ≯ succ₁ n → m ≯ n ∨ m ≡ succ₁ n
x≯Sy→x≯y∨x≡Sy nzero nzero h = prf
  where postulate prf : zero ≯ zero ∨ zero ≡ succ₁ zero
        {-# ATP prove prf #-}
x≯Sy→x≯y∨x≡Sy nzero (nsucc {n} Nn) h = prf
  where postulate prf : zero ≯ succ₁ n ∨ zero ≡ succ₁ (succ₁ n)
        {-# ATP prove prf #-}
x≯Sy→x≯y∨x≡Sy (nsucc {m} Nm) nzero h = prf
  where postulate prf : succ₁ m ≯ zero ∨ succ₁ m ≡ succ₁ zero
        {-# ATP prove prf 0≮x→x≡0 #-}
x≯Sy→x≯y∨x≡Sy (nsucc {m} Nm) (nsucc {n} Nn) h = prf (x≯Sy→x≯y∨x≡Sy Nm Nn m≯Sn)
  where
  postulate m≯Sn : m ≯ succ₁ n
  {-# ATP prove m≯Sn #-}

  postulate prf : m ≯ n ∨ m ≡ succ₁ n →
                  succ₁ m ≯ succ₁ n ∨ succ₁ m ≡ succ₁ (succ₁ n)
  {-# ATP prove prf #-}

x≥y→y>0→x∸y<x : ∀ {m n} → N m → N n → m ≥ n → n > zero → m ∸ n < m
x≥y→y>0→x∸y<x {m} Nm nzero h₁ h₂ = prf
  where postulate prf : m ∸ zero < m
        {-# ATP prove prf x∸y<Sx 0∸x S∸S #-}
x≥y→y>0→x∸y<x nzero (nsucc {n} Nn) h₁ h₂ = prf
  where postulate prf : zero ∸ succ₁ n < zero
        {-# ATP prove prf 0∸x S≤0→⊥ #-}
x≥y→y>0→x∸y<x (nsucc {m} Nm) (nsucc {n} Nn) h₁ h₂ = prf
  where postulate prf : succ₁ m ∸ succ₁ n < succ₁ m
        {-# ATP prove prf x∸y<Sx 0∸x S∸S #-}

x<y→y≤z→x<z : ∀ {m n o} → N m → N n → N o → m < n → n ≤ o → m < o
x<y→y≤z→x<z {o = o} nzero nzero No h₁ h₂ = prf
  where postulate prf : zero < o
        {-# ATP prove prf 0<0→⊥ #-}
x<y→y≤z→x<z nzero (nsucc Nn) nzero h₁ h₂ = prf
  where postulate prf : zero < zero
        {-# ATP prove prf S≤0→⊥ #-}
x<y→y≤z→x<z nzero (nsucc Nn) (nsucc {o} No) h₁ h₂ = prf
  where postulate prf : zero < succ₁ o
        {-# ATP prove prf #-}
x<y→y≤z→x<z {o = o} (nsucc {m} Nm) nzero No h₁ h₂ = prf
  where postulate prf : succ₁ m < o
        {-# ATP prove prf #-}
x<y→y≤z→x<z (nsucc {m} Nm) (nsucc Nn) nzero h₁ h₂ = prf
  where postulate prf : succ₁ m < zero
        {-# ATP prove prf S≤0→⊥ #-}
x<y→y≤z→x<z (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) h₁ h₂ =
  prf (x<y→y≤z→x<z Nm Nn No m<n n≤o)
  where
  postulate m<n : m < n
  {-# ATP prove m<n #-}

  postulate n≤o : n ≤ o
  {-# ATP prove n≤o #-}

  postulate prf : m < o → succ₁ m < succ₁ o
  {-# ATP prove prf #-}

x≤y+x∸y : ∀ {m n} → N m → N n → m ≤ n + (m ∸ n)
x≤y+x∸y {n = n} nzero Nn = prf0
  where postulate prf0 : zero ≤ n + (zero ∸ n)
        {-# ATP prove prf0 +-N #-}
x≤y+x∸y (nsucc {m} Nm) nzero = prfx0
  where postulate prfx0 : succ₁ m ≤ zero + (succ₁ m ∸ zero)
        {-# ATP prove prfx0 x<Sx #-}
x≤y+x∸y (nsucc {m} Nm) (nsucc {n} Nn) = prfSS (x≤y+x∸y Nm Nn)
  where postulate prfSS : m ≤ n + (m ∸ n) →
                          succ₁ m ≤ succ₁ n + (succ₁ m ∸ succ₁ n)
        {-# ATP prove prfSS x≤y→Sx≤Sy ≤-trans +-N ∸-N S∸S #-}

x∸y<x∸z→Sx∸y<Sx∸z : ∀ {m n o} → N m → N n → N o →
                    m ∸ n < m ∸ o → succ₁ m ∸ n < succ₁ m ∸ o
x∸y<x∸z→Sx∸y<Sx∸z {n = n} {o} nzero Nn No h = prf
  where postulate prf : succ₁ zero ∸ n < succ₁ zero ∸ o
        {-# ATP prove prf 0∸x #-}
x∸y<x∸z→Sx∸y<Sx∸z {o = o} (nsucc {m} Nm) nzero No h = prf
  where postulate prf : succ₁ (succ₁ m) ∸ zero < succ₁ (succ₁ m) ∸ o
        {-# ATP prove prf x<x∸y→⊥ #-}
x∸y<x∸z→Sx∸y<Sx∸z (nsucc {m} Nm) (nsucc {n} Nn) nzero h = prf
  where postulate prf : succ₁ (succ₁ m) ∸ succ₁ n < succ₁ (succ₁ m) ∸ zero
        {-# ATP prove prf Sx∸Sy<Sx #-}
x∸y<x∸z→Sx∸y<Sx∸z (nsucc {m} Nm) (nsucc {n} Nn) (nsucc {o} No) h =
  prf (x∸y<x∸z→Sx∸y<Sx∸z Nm Nn No)
  where
  postulate prf : (m ∸ n < m ∸ o → succ₁ m ∸ n < succ₁ m ∸ o) →
                  succ₁ (succ₁ m) ∸ succ₁ n < succ₁ (succ₁ m) ∸ succ₁ o
  {-# ATP prove prf S∸S #-}

------------------------------------------------------------------------------
-- Properties about the lexicographical order

postulate xy<00→⊥ : ∀ {m n} → N m → N n → ¬ (Lexi m n zero zero)
{-# ATP prove xy<00→⊥ x<0→⊥ #-}

postulate 0Sx<00→⊥ : ∀ {m} → ¬ (Lexi zero (succ₁ m) zero zero)
{-# ATP prove 0Sx<00→⊥ #-}

postulate Sxy₁<0y₂→⊥ : ∀ {m n₁ n₂} → ¬ (Lexi (succ₁ m) n₁ zero n₂)
{-# ATP prove Sxy₁<0y₂→⊥ #-}

postulate x₁y<x₂0→x₁<x₂ : ∀ {m₁ n} → N n → ∀ {m₂} → Lexi m₁ n m₂ zero → m₁ < m₂
{-# ATP prove x₁y<x₂0→x₁<x₂ x<0→⊥ #-}

postulate xy₁<0y₂→x≡0∧y₁<y₂ : ∀ {m} → N m → ∀ {n₁ n₂} → Lexi m n₁ zero n₂ →
                              m ≡ zero ∧ n₁ < n₂
{-# ATP prove xy₁<0y₂→x≡0∧y₁<y₂ x<0→⊥ #-}

[Sx∸Sy,Sy]<[Sx,Sy] : ∀ {m n} → N m → N n →
                     Lexi (succ₁ m ∸ succ₁ n) (succ₁ n) (succ₁ m) (succ₁ n)
[Sx∸Sy,Sy]<[Sx,Sy] {m} {n} Nm Nn = prf
  where postulate prf : Lexi (succ₁ m ∸ succ₁ n) (succ₁ n) (succ₁ m) (succ₁ n)
        {-# ATP prove prf x∸y<Sx S∸S #-}

[Sx,Sy∸Sx]<[Sx,Sy] : ∀ {m n} → N m → N n →
                     Lexi (succ₁ m) (succ₁ n ∸ succ₁ m) (succ₁ m) (succ₁ n)
[Sx,Sy∸Sx]<[Sx,Sy] {m} {n} Nm Nn = prf
  where postulate prf : Lexi (succ₁ m) (succ₁ n ∸ succ₁ m) (succ₁ m) (succ₁ n)
        {-# ATP prove prf x∸y<Sx S∸S #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Like Leftovers.Examples, but more meant to stress-test the library
-- than to be clear/readable
module Leftovers.Tests where

open import Leftovers.Leftovers
open import Leftovers.ByRefl

open import Level
open import Reflection
open import Data.Nat
open import Relation.Binary.PropositionalEquality

open import Data.Unit
open import Data.List

--Make sure findLeftovers works with

data Foo : Set(Level.suc Level.zero) where
  Bar : Set → ℕ → ((n : ℕ) → n ≡ n + 0) → Foo

makePair : Term → TC ⊤
makePair = λ goal →
    do
      hole1 <- newMeta (quoteTerm Set)
      hole2 <- newMeta (quoteTerm ℕ)
      hole3 <- newMeta (quoteTerm ((n : ℕ) → n ≡ n + 0))
      body <- extendContext (vArg (quoteTerm ℕ)) do
        tyHole ← newMeta (quoteTerm Set)
        newHole ← newMeta tyHole
        return (def (quote sym) (vArg newHole ∷ []))
      unify hole3 (lam visible (abs "arg" body))
      unify hole2 (quoteTerm 4)
      unify goal (con (quote Bar) (vArg hole1 ∷ vArg hole2 ∷ vArg hole3 ∷ []))

p0 : ∀ n → n + 0 ≡ n
p0 zero = refl
p0 (suc n) rewrite p0 n = refl

f : Foo
f =
  by
    makePair
  andAlso
    p0
    ℕ

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


text:
module std-reduction.Base where

open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open EvaluationContext1
open import Esterel.Lang
open import Esterel.Environment as Env
  using (Env)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)
open import Esterel.Lang.CanFunction
  using (Canₛ ; Canₛₕ)

open import Data.List
  using (List; _∷_ ; [] ; mapMaybe)
open import Data.List.Any
  using (any)
open import blocked
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Data.Product using (_×_ ; proj₁ ; proj₂ ; _,_ ; ∃-syntax; Σ-syntax)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; sym)
open _≡_
import Data.Nat as Nat
open import Relation.Nullary using (yes ; no ; ¬_)
open import Function using (_∘_ ; id ; _$_)
open import Data.Maybe
  using (Maybe)
open Maybe
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Data.Bool
  using (if_then_else_)

blocked-or-done : Env → Ctrl → Term → Set
blocked-or-done θ A p = (done p) ⊎ (blocked θ A p)

mutual
  set-all-absent : (θ : Env) → (List (∃[ S ] Env.isSig∈ S θ)) → Env
  set-all-absent θ [] = θ
  set-all-absent θ ((S , S∈) ∷ Ss)
    = Env.set-sig{S} (set-all-absent θ Ss) (set-all-absent∈ θ S Ss S∈) Signal.absent

  set-all-absent∈ : ∀ θ S Ss → Env.isSig∈ S θ → Env.isSig∈ S (set-all-absent θ Ss)
  set-all-absent∈ θ S [] S∈ = S∈
  set-all-absent∈ θ S (x ∷ Ss) S∈
    = Env.sig-set-mono'{S = S}{S' = (proj₁ x)}{θ = set-all-absent θ Ss}{S'∈ = S'∈2} S∈2
   where
     S∈2 = (set-all-absent∈ θ S Ss S∈)
     S'∈2 = (set-all-absent∈ θ (proj₁ x) Ss (proj₂ x))

mutual
  set-all-ready : (θ : Env) → (List (∃[ s ] Env.isShr∈ s θ)) → Env
  set-all-ready θ [] = θ
  set-all-ready θ ((s , s∈) ∷ ss)
    = Env.set-shr {s} θ2 s∈2 SharedVar.ready (Env.shr-vals{s} θ s∈)
      where
        s∈2 = (set-all-ready∈ θ s ss s∈)
        θ2 = (set-all-ready θ ss)

  set-all-ready∈ : ∀ θ s ss → Env.isShr∈ s θ → Env.isShr∈ s (set-all-ready θ ss)
  set-all-ready∈ θ s [] s∈ = s∈
  set-all-ready∈ θ s (x ∷ ss) s∈
    = Env.shr-set-mono' {s = s} {s' = proj₁ x} {θ = set-all-ready θ ss}
        {s'∈ = set-all-ready∈ θ (proj₁ x) ss (proj₂ x)} (set-all-ready∈ θ s ss s∈)

shr-val-same-after-all-ready : ∀ s θ ss →
                               (s∈  : Env.isShr∈ s θ) →
                               (s∈2  : Env.isShr∈ s (set-all-ready θ ss)) →
                               (Env.shr-vals {s} θ s∈) ≡ (Env.shr-vals {s} (set-all-ready θ ss) s∈2)
shr-val-same-after-all-ready s θ [] s∈ s∈2 =  Env.shr-vals-∈-irr{s}{θ} s∈ s∈2
shr-val-same-after-all-ready s θ ((s' , s'∈) ∷ ss) s∈ s∈2 with (SharedVar._≟_ s' s)
... | yes p rewrite p | Env.shr∈-eq{s}{θ} s∈ s'∈
   = sym (proj₂ (Env.shr-putget{s}{(set-all-ready θ ss)}{SharedVar.ready}{(Env.shr-vals {s} θ s'∈)} (set-all-ready∈ θ s ss s∈) s∈2))
... | no ¬s'≡s
  = sym
     (proj₂
       (Env.shr-putputget{θ = (set-all-ready θ ss)}{v1l = Env.shr-stats{s} (set-all-ready θ ss) ((set-all-ready∈ θ s ss s∈))}
                         (¬s'≡s ∘ sym)
                         (set-all-ready∈ θ s ss s∈)
                         (set-all-ready∈ θ s' ss s'∈)
                         s∈2
                         refl
                         (sym (shr-val-same-after-all-ready s θ ss s∈ (set-all-ready∈ θ s ss s∈))) ))
--

can-set-absent' : (θ : Env) → Term →
                  List (∃[ S ] (Σ[ S∈ ∈ (Env.isSig∈ S θ) ] (Env.sig-stats{S} θ S∈ ≡ Signal.unknown)))
can-set-absent' θ p = mapMaybe id $ Env.SigDomMap θ get-res
  where
    get-res : (S : Signal) → Env.isSig∈ S θ → Maybe (∃[ S ] (Σ[ S∈ ∈ (Env.isSig∈ S θ) ] (Env.sig-stats{S} θ S∈ ≡ Signal.unknown)))
    get-res S S∈ with any (Nat._≟_ (Signal.unwrap S)) (Canₛ p θ) | Signal._≟ₛₜ_ (Env.sig-stats{S} θ S∈) Signal.unknown
    ... | no _ | yes eq = just $ S , (S∈ , eq)
    ... | _ | _ = nothing

can-set-absent : (θ : Env) → Term → List (∃[ S ] Env.isSig∈ S θ)
can-set-absent θ p
   = Data.List.map (λ x → proj₁ x , proj₁ (proj₂ x))
                   (can-set-absent' θ p)

CanSetToReady : Env → Set
CanSetToReady θ = (∃[ s ] (Σ[ S∈ ∈ (Env.isShr∈ s θ) ] (Env.shr-stats{s} θ S∈ ≡ SharedVar.old ⊎ Env.shr-stats{s} θ S∈ ≡ SharedVar.new)))

can-set-ready' : (θ : Env) → Term → List (CanSetToReady θ)
can-set-ready' θ p = mapMaybe id $ Env.ShrDomMap θ get-res
  where
    get-res : (s : SharedVar) → Env.isShr∈ s θ → Maybe (CanSetToReady θ)
    get-res s s∈ with any (Nat._≟_ (SharedVar.unwrap s)) (Canₛₕ p θ)
                    | SharedVar._≟ₛₜ_ (Env.shr-stats{s} θ s∈) SharedVar.old
                    | SharedVar._≟ₛₜ_ (Env.shr-stats{s} θ s∈) SharedVar.new
    ... | no _ | yes eq |  _   = just $ s , (s∈ , inj₁ eq)
    ... | no _ | no _ | yes eq = just $ s , (s∈ , inj₂ eq)
    ... | _ | yes _ | yes _ = nothing
    ... | _ | yes _ | no _ = nothing
    ... | _ | no _ | yes _ = nothing
    ... | _ | no _ | no _ = nothing

can-set-ready :  (θ : Env) → Term → List (∃[ s ] Env.isShr∈ s θ)
can-set-ready θ p = Data.List.map (λ x → proj₁ x , proj₁ (proj₂ x)) (can-set-ready' θ p)

data left-most : Env → EvaluationContext → Set where
  lhole : ∀{θ} → left-most θ []
  lseq : ∀{θ E q} → left-most θ E → left-most θ ((eseq q) ∷ E)
  lloopˢ : ∀{θ E q} → left-most θ E → left-most θ ((eloopˢ q) ∷ E)
  lparl : ∀{θ E q} → left-most θ E → left-most θ ((epar₁ q) ∷ E)
  lparrdone : ∀{θ E p} → done p → left-most θ E → left-most θ ((epar₂ p) ∷ E)
  lparrblocked : ∀{θ A E p} → blocked θ A p → left-most θ E → left-most θ ((epar₂ p) ∷ E)
  lsuspend : ∀{θ E S} → left-most θ E → left-most θ ((esuspend S) ∷ E)
  ltrap : ∀{θ E} → left-most θ E → left-most θ (etrap ∷ E)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus