text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Homotopy.Connected where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Univalence
open import Cubical.Functions.Fibration
open import Cubical.Data.Nat
open import Cubical.Data.Prod hiding (map)
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.HITs.Nullification
open import Cubical.HITs.Susp
open import Cubical.HITs.SmashProduct
open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec)
open import Cubical.Homotopy.Loopspace
open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.S1
open import Cubical.Data.Bool
open import Cubical.Data.Unit

-- Note that relative to most sources, this notation is off by +2
isConnected : ∀ {ℓ} (n : HLevel) (A : Type ℓ) → Type ℓ
isConnected n A = isContr (hLevelTrunc n A)

isConnectedFun : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ-max ℓ ℓ')
isConnectedFun n f = ∀ b → isConnected n (fiber f b)

isTruncatedFun : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ-max ℓ ℓ')
isTruncatedFun n f = ∀ b → isOfHLevel n (fiber f b)

isConnectedSubtr : ∀ {ℓ} {A : Type ℓ} (n m : HLevel)
                → isConnected (m + n) A
                → isConnected n A
isConnectedSubtr {A = A} n m iscon =
  isOfHLevelRetractFromIso 0 (truncOfTruncIso n m) (helper n iscon)
  where
  helper : (n : ℕ) → isConnected (m + n) A → isContr (hLevelTrunc n (hLevelTrunc (m + n) A))
  helper zero iscon = isContrUnit*
  helper (suc n) iscon = ∣ iscon .fst ∣ , (Trunc.elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ a → cong ∣_∣ (iscon .snd a))

isConnectedFunSubtr : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : HLevel) (f : A → B)
                → isConnectedFun (m + n) f
                → isConnectedFun n f
isConnectedFunSubtr n m f iscon b = isConnectedSubtr n m (iscon b)

private
  typeToFiberIso : ∀ {ℓ} (A : Type ℓ) → Iso A (fiber (λ (x : A) → tt) tt)
  Iso.fun (typeToFiberIso A) x = x , refl
  Iso.inv (typeToFiberIso A) = fst
  Iso.rightInv (typeToFiberIso A) b i = fst b , (isOfHLevelSuc 1 (isPropUnit) tt tt (snd b) refl) i
  Iso.leftInv (typeToFiberIso A) a = refl

  typeToFiber : ∀ {ℓ} (A : Type ℓ) → A ≡ fiber (λ (x : A) → tt) tt
  typeToFiber A = isoToPath (typeToFiberIso A)

module elim {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where
  private
    inv : ∀ {ℓ'''} (n : HLevel) (P : B → TypeOfHLevel ℓ''' (suc n))
        → ((a : A) → P (f a) .fst)
        → (b : B)
        → hLevelTrunc (suc n) (fiber f b) → P b .fst
    inv n P t b =
      Trunc.rec
        (P b .snd)
        (λ {(a , p) → subst (fst ∘ P) p (t a)})

  isIsoPrecompose : ∀ {ℓ'''} (n : ℕ) (P : B → TypeOfHLevel ℓ''' n)
                   → isConnectedFun n f
                   → Iso ((b : B) → P b .fst) ((a : A) → P (f a) .fst)
  isIsoPrecompose zero P fConn = isContr→Iso (isOfHLevelΠ _ (λ b → P b .snd)) (isOfHLevelΠ _ λ a → P (f a) .snd)
  Iso.fun (isIsoPrecompose (suc n) P fConn) = _∘ f
  Iso.inv (isIsoPrecompose (suc n) P fConn) t b = inv n P t b (fConn b .fst)
  Iso.rightInv (isIsoPrecompose (suc n) P fConn) t =
    funExt λ a → cong (inv n P t (f a)) (fConn (f a) .snd ∣ a , refl ∣)
               ∙ substRefl {B = fst ∘ P} (t a)
  Iso.leftInv (isIsoPrecompose (suc n) P fConn) s =
    funExt λ b →
          Trunc.elim
            {B = λ d → inv n P (s ∘ f) b d ≡ s b}
            (λ _ → isOfHLevelPath (suc n) (P b .snd) _ _)
            (λ {(a , p) i → transp (λ j → P (p (j ∨ i)) .fst) i (s (p i))})
            (fConn b .fst)

  isEquivPrecompose : ∀ {ℓ'''} (n : ℕ) (P : B → TypeOfHLevel ℓ''' n)
                   → isConnectedFun n f
                   → isEquiv (λ(s : (b : B) → P b .fst) → s ∘ f)
  isEquivPrecompose zero P fConn = isoToIsEquiv theIso
    where
    theIso : Iso ((b : B) → P b .fst) ((a : A) → P (f a) .fst)
    Iso.fun theIso = λ(s : (b : B) → P b .fst) → s ∘ f
    Iso.inv theIso = λ _ b → P b .snd .fst
    Iso.rightInv theIso g = funExt λ x → P (f x) .snd .snd (g x)
    Iso.leftInv theIso g = funExt λ x → P x .snd .snd (g x)
  isEquivPrecompose (suc n) P fConn = isoToIsEquiv (isIsoPrecompose (suc n) P fConn)

  isConnectedPrecompose : (n : ℕ) → ((P : B → TypeOfHLevel (ℓ-max ℓ ℓ') n)
                                    → hasSection (λ(s : (b : B) → P b .fst) → s ∘ f))
                       → isConnectedFun n f
  isConnectedPrecompose zero P→sect b = isContrUnit*
  isConnectedPrecompose (suc n) P→sect b = c n P→sect b , λ y →  sym (fun n P→sect b y)
    where
    P : (n : HLevel) → ((P : B → TypeOfHLevel ℓ (suc n))
     → hasSection (λ(s : (b : B) → P b .fst) → s ∘ f))
     → B → Type _
    P n s b = hLevelTrunc (suc n) (fiber f b)

    c : (n : HLevel) → ((P : B → TypeOfHLevel (ℓ-max ℓ ℓ') (suc n))
     → hasSection (λ(s : (b : B) → P b .fst) → s ∘ f)) → (b : B)
     → hLevelTrunc (suc n) (fiber f b)
    c n s = (s λ b → (hLevelTrunc (suc n) (fiber f b) , isOfHLevelTrunc _)) .fst
              λ a → ∣ a , refl ∣

    fun : (n : HLevel) (P→sect : ((P : B → TypeOfHLevel (ℓ-max ℓ ℓ') (suc n))
                     → hasSection λ(s : (b : B) → P b .fst) → s ∘ f))
      → (b : B) (w : (hLevelTrunc (suc n) (fiber f b)))
      → w ≡ c n P→sect b
    fun n P→sect b = Trunc.elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc _) _ _)
                                       λ a → J (λ b p → ∣ (fst a) , p ∣ ≡ c n P→sect b)
                                               (c* (fst a))
                                               (snd a)
        where
        c* : ((a : A) → ∣ (a , refl {x = f a}) ∣ ≡ c n P→sect (f a))
        c* a = sym (cong (λ x → x a) (P→sect (λ b → hLevelTrunc (suc n) (fiber f b) , isOfHLevelTrunc _) .snd λ a → ∣ a , refl ∣))

isOfHLevelPrecomposeConnected : ∀ {ℓ ℓ' ℓ''} (k : HLevel) (n : HLevel)
  {A : Type ℓ} {B : Type ℓ'} (P : B → TypeOfHLevel ℓ'' (k + n)) (f : A → B)
  → isConnectedFun n f
  → isOfHLevelFun k (λ(s : (b : B) → P b .fst) → s ∘ f)
isOfHLevelPrecomposeConnected zero n P f fConn =
  elim.isEquivPrecompose f n P fConn .equiv-proof
isOfHLevelPrecomposeConnected (suc k) n P f fConn t =
  isOfHLevelPath'⁻ k
    λ {(s₀ , p₀) (s₁ , p₁) →
      isOfHLevelRetractFromIso k (invIso ΣPathIsoPathΣ)
         (subst (isOfHLevel k)
           (sym (fiberPath (s₀ , p₀) (s₁ , p₁)))
           (isOfHLevelRetract k
            (λ {(q , α) → (funExt⁻ q) , (cong funExt⁻ α)})
            (λ {(h , β) → (funExt h) , (cong funExt β)})
            (λ _ → refl)
            (isOfHLevelPrecomposeConnected k n
              (λ b → (s₀ b ≡ s₁ b) , isOfHLevelPath' (k + n) (P b .snd) _ _)
              f fConn
              (funExt⁻ (p₀ ∙∙ refl ∙∙ sym p₁)))))}

indMapEquiv→conType : ∀ {ℓ} {A : Type ℓ} (n : HLevel)
                   → ((B : TypeOfHLevel ℓ n)
                      → isEquiv (λ (b : (fst B)) → λ (a : A) → b))
                   → isConnected n A
indMapEquiv→conType {A = A} zero BEq = isContrUnit*
indMapEquiv→conType {A = A} (suc n) BEq =
  isOfHLevelRetractFromIso 0 (mapCompIso {n = (suc n)} (typeToFiberIso A))
    (elim.isConnectedPrecompose (λ _ → tt) (suc n)
                                (λ P → ((λ a _ → a) ∘ invIsEq (BEq (P tt)))
                               , λ a → equiv-proof (BEq (P tt)) a .fst .snd)
                                tt)

isConnectedPath : ∀ {ℓ} (n : HLevel) {A : Type ℓ}
  → isConnected (suc n) A
  → (a₀ a₁ : A) → isConnected n (a₀ ≡ a₁)
isConnectedPath zero connA a₀ a₁ = isContrUnit*
isConnectedPath (suc n) connA a₀ a₁ =
  isOfHLevelRetractFromIso 0
    (invIso (PathIdTruncIso (suc n)))
    (isContr→isContrPath connA _ _)

isConnectedPathP : ∀ {ℓ} (n : HLevel) {A : I → Type ℓ}
  → isConnected (suc n) (A i1)
  → (a₀ : A i0) (a₁ : A i1) → isConnected n (PathP A a₀ a₁)
isConnectedPathP n con a₀ a₁ =
  subst (isConnected n) (sym (PathP≡Path _ _ _))
        (isConnectedPath n con _ _)

isConnectedRetract : ∀ {ℓ ℓ'} (n : HLevel)
  {A : Type ℓ} {B : Type ℓ'}
  (f : A → B) (g : B → A)
  (h : (x : A) → g (f x) ≡ x)
  → isConnected n B → isConnected n A
isConnectedRetract zero _ _ _ _ = isContrUnit*
isConnectedRetract (suc n) f g h =
  isContrRetract
    (Trunc.map f)
    (Trunc.map g)
    (Trunc.elim
      (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
      (λ a → cong ∣_∣ (h a)))

isConnectedRetractFromIso :  ∀ {ℓ ℓ'} (n : HLevel)
    {A : Type ℓ} {B : Type ℓ'}
  → Iso A B
  → isConnected n B → isConnected n A
isConnectedRetractFromIso n e =
  isConnectedRetract n
    (Iso.fun e)
    (Iso.inv e)
    (Iso.leftInv e)

isConnectedPoint : ∀ {ℓ} (n : HLevel) {A : Type ℓ}
  → isConnected (suc n) A
  → (a : A) → isConnectedFun n (λ(_ : Unit) → a)
isConnectedPoint n connA a₀ a =
  isConnectedRetract n
    snd (_ ,_) (λ _ → refl)
    (isConnectedPath n connA a₀ a)

isConnectedPoint2 : ∀ {ℓ} (n : HLevel) {A : Type ℓ} (a : A)
   → isConnectedFun n (λ(_ : Unit) → a)
   → isConnected (suc n) A
isConnectedPoint2 n {A = A} a connMap = indMapEquiv→conType _ λ B → isoToIsEquiv (theIso B)
  where
  module _  {ℓ' : Level} (B : TypeOfHLevel ℓ' (suc n))
    where
    helper : (f : A → fst B) → (a2 : A) → f a2 ≡ f a
    helper f = equiv-proof (elim.isEquivPrecompose (λ _ → a) n (λ a2 → (f a2 ≡ f a) ,
                             isOfHLevelPath' n (snd B) (f a2) (f a)) connMap) (λ _ → refl) .fst .fst

    theIso : Iso (fst B) (A → fst B)
    Iso.fun theIso b a = b
    Iso.inv theIso f = f a
    Iso.rightInv theIso f = funExt λ y → sym (helper f y)
    Iso.leftInv theIso _ = refl

connectedTruncIso : ∀ {ℓ} {A B : Type ℓ} (n : HLevel) (f : A → B)
                   → isConnectedFun n f
                   → Iso (hLevelTrunc n A) (hLevelTrunc n B)
connectedTruncIso {A = A} {B = B} zero f con = isContr→Iso isContrUnit* isContrUnit*
connectedTruncIso {A = A} {B = B} (suc n) f con = g
  where
  back : B → hLevelTrunc (suc n) A
  back y = map fst ((con y) .fst)

  backSection :  (b : B) → Path (hLevelTrunc (suc n) B)
                                (Trunc.rec (isOfHLevelTrunc (suc n))
                                           (λ a → ∣ f a ∣)
                                           (Trunc.rec {n = n}
                                                      {B = hLevelTrunc (suc n) A} (isOfHLevelTrunc (suc n))
                                                      back ∣ b ∣))
                               ∣ b ∣
  backSection b = helper (λ p → map f p ≡ ∣ b ∣)
                         (λ x → (isOfHLevelSuc (suc n) (isOfHLevelTrunc (suc n)))
                                   (map f (map fst x)) ∣ b ∣)
                         (λ a p → cong ∣_∣ p)
                         (fst (con b))
    where
    helper : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} (P : hLevelTrunc (suc n) A → Type ℓ'')
           → ((x : hLevelTrunc (suc n) (Σ A B)) → isOfHLevel (suc n) (P (map fst x)))
           → ((a : A) (b : B a) → P ∣ a ∣)
           → (p : hLevelTrunc (suc n) (Σ A B))
           →  P (map fst p)
    helper P hlev pf = Trunc.elim hlev λ pair → pf (fst pair) (snd pair)

  g : Iso (hLevelTrunc (suc n) A) (hLevelTrunc (suc n) B)
  Iso.fun g = map f
  Iso.inv g = Trunc.rec (isOfHLevelTrunc _) back
  Iso.leftInv g = Trunc.elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc _) _ _)
                               λ a → cong (map fst) (con (f a) .snd  ∣ a , refl ∣)
  Iso.rightInv g = Trunc.elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc _) _ _)
                              backSection

connectedTruncIso2 : ∀ {ℓ} {A B : Type ℓ} (n m : HLevel) (f : A → B)
                   → Σ[ x ∈ ℕ ] x + n ≡ m
                   → isConnectedFun m f
                   → Iso (hLevelTrunc n A) (hLevelTrunc n B)
connectedTruncIso2 {A = A} {B = B} n m f (x , pf) con =
  connectedTruncIso n f (isConnectedFunSubtr n x f (transport (λ i → isConnectedFun (pf (~ i)) f) con))

connectedTruncEquiv : ∀ {ℓ} {A B : Type ℓ} (n : HLevel) (f : A → B)
                   → isConnectedFun n f
                   → hLevelTrunc n A ≃ hLevelTrunc n B
connectedTruncEquiv {A = A} {B = B} n f con = isoToEquiv (connectedTruncIso n f con)

-- TODO : Reorganise the following proofs.

inrConnected : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} (n : HLevel)
            → (f : C → A) (g : C → B)
            → isConnectedFun n f
            → isConnectedFun n {A = B} {B = Pushout f g} inr
inrConnected {A = A} {B = B} {C = C} n f g iscon =
  elim.isConnectedPrecompose inr n λ P → (k P) , λ b → refl
  where
  module _ {ℓ : Level} (P : (Pushout f g) → TypeOfHLevel ℓ n)
                   (h : (b : B) → typ (P (inr b)))
    where
    Q : A → TypeOfHLevel _ n
    Q a = (P (inl a))

    fun : (c : C) → typ (Q (f c))
    fun c = transport (λ i → typ (P (push c (~ i)))) (h (g c))

    k : (d : Pushout f g) → typ (P d)
    k (inl x) = equiv-proof (elim.isEquivPrecompose f n Q iscon) fun .fst .fst x
    k (inr x) = h x
    k (push a i) =
      hcomp (λ k → λ { (i = i0) → equiv-proof (elim.isEquivPrecompose f n Q iscon) fun .fst .snd i0 a
                     ; (i = i1) → transportTransport⁻ (λ j → typ (P (push a j))) (h (g a)) k })
            (transp (λ j → typ (P (push a (i ∧ j))))
                    (~ i)
                    (equiv-proof (elim.isEquivPrecompose f n Q iscon)
                                 fun .fst .snd i a))

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
module Data.Num.Core where

open import Data.Num.Digit public

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra
open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤; toℕ; zero; suc; #_)
open import Data.Fin.Properties as FinProps using (bounded; toℕ-fromℕ≤)

open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Function.Equality using (_⟶_)

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

------------------------------------------------------------------------
-- Numbers
------------------------------------------------------------------------

infixr 5 _∷_

data Numeral : ℕ → ℕ → ℕ → Set where
    _∙  : ∀ {b d o} → Digit d → Numeral b d o
    _∷_ : ∀ {b d o} → Digit d → Numeral b d o → Numeral b d o

MMXVI : Numeral 10 10 0
MMXVI = # 6 ∷ # 1 ∷ # 0 ∷ (# 2) ∙

------------------------------------------------------------------------
-- Converting from Numeral to ℕ
------------------------------------------------------------------------

⟦_⟧ : ∀ {b d o} → (xs : Numeral b d o) → ℕ
⟦_⟧ {_} {_} {o} (x ∙)    = Digit-toℕ x o
⟦_⟧ {b} {_} {o} (x ∷ xs) = Digit-toℕ x o + ⟦ xs ⟧ * b

Num-lower-bound : ∀ {b d o}
    → (xs : Numeral b (suc d) o)
    → ⟦ xs ⟧ ≥ o
Num-lower-bound {_} {_} {o} (x ∙) = Digit-lower-bound o x
Num-lower-bound {b} {d} {o} (x ∷ xs) =
    start
        o
    ≤⟨ m≤m+n o (⟦ xs ⟧ * b) ⟩
        o + ⟦ xs ⟧ * b
    ≤⟨ +n-mono (⟦ xs ⟧ * b) (Digit-lower-bound o x) ⟩
        Digit-toℕ x o + ⟦ xs ⟧ * b
    □

-- the least significant digit
lsd : ∀ {b d o} → (xs : Numeral b d o) → Digit d
lsd (x ∙   ) = x
lsd (x ∷ xs) = x

lsd-toℕ : ∀ {b d o} → (xs : Numeral b d o) → Digit-toℕ (lsd xs) o ≤ ⟦ xs ⟧
lsd-toℕ (x ∙) = ≤-refl
lsd-toℕ {b} {d} {o} (x ∷ xs) = m≤m+n (Digit-toℕ x o) (⟦ xs ⟧ * b)

------------------------------------------------------------------------
-- View of Num
------------------------------------------------------------------------

data NumView : ℕ → ℕ → ℕ → Set where
    NullBase    : ∀   d o                            → NumView 0       (suc d) o
    NoDigits    : ∀ b o                              → NumView b       0       o
    AllZeros    : ∀ b                                → NumView (suc b) 1       0
    Proper      : ∀ b d o → (proper : suc d + o ≥ 2) → NumView (suc b) (suc d) o

numView : ∀ b d o → NumView b d o
numView b       zero          o       = NoDigits b o
numView zero    (suc d)       o       = NullBase d o
numView (suc b) (suc zero)    zero    = AllZeros b
numView (suc b) (suc zero)    (suc o) = Proper b zero (suc o) (s≤s (s≤s z≤n))
numView (suc b) (suc (suc d)) o       = Proper b (suc d) o (s≤s (s≤s z≤n))

------------------------------------------------------------------------
-- Properties of Num
------------------------------------------------------------------------

NoDigits-explode : ∀ {b o a} {Whatever : Set a}
    → (xs : Numeral b 0 o)
    → Whatever
NoDigits-explode (() ∙   )
NoDigits-explode (() ∷ xs)

toℕ-NullBase : ∀ {d o}
    → (x : Digit d)
    → (xs : Numeral 0 d o)
    → ⟦ x ∷ xs ⟧ ≡ Digit-toℕ x o
toℕ-NullBase {d} {o} x xs =
    begin
        Digit-toℕ x o + ⟦ xs ⟧ * 0
    ≡⟨ cong (λ w → Digit-toℕ x o + w) (*-right-zero ⟦ xs ⟧) ⟩
        Digit-toℕ x o + 0
    ≡⟨ +-right-identity (Digit-toℕ x o) ⟩
        Digit-toℕ x o
    ∎

toℕ-AllZeros : ∀ {b} → (xs : Numeral b 1 0) → ⟦ xs ⟧ ≡ 0
toℕ-AllZeros     (zero   ∙   ) = refl
toℕ-AllZeros     (suc () ∙   )
toℕ-AllZeros {b} (zero   ∷ xs) = cong (λ w → w * b) (toℕ-AllZeros xs)
toℕ-AllZeros     (suc () ∷ xs)

n∷-mono-strict : ∀ {b d o}
    → (x : Fin d) (xs : Numeral (suc b) d o)
    → (y : Fin d) (ys : Numeral (suc b) d o)
    → Digit-toℕ x o ≡ Digit-toℕ y o
    → ⟦ xs ⟧ < ⟦ ys ⟧
    → ⟦ x ∷ xs ⟧ < ⟦ y ∷ ys ⟧
n∷-mono-strict {b} {d} {o} x xs y ys ⟦x⟧≡⟦y⟧ ⟦xs⟧<⟦ys⟧ =
    start
        suc (Digit-toℕ x o) + ⟦ xs ⟧ * suc b
    ≈⟨ sym (+-suc (Digit-toℕ x o) (⟦ xs ⟧ * suc b)) ⟩
        Digit-toℕ x o + suc (⟦ xs ⟧ * suc b)
    ≤⟨ n+-mono (Digit-toℕ x o) (s≤s (n≤m+n b (⟦ xs ⟧ * suc b))) ⟩
        Digit-toℕ x o + (suc ⟦ xs ⟧) * suc b
    ≤⟨ (reflexive ⟦x⟧≡⟦y⟧) +-mono (*n-mono (suc b) ⟦xs⟧<⟦ys⟧) ⟩
        Digit-toℕ y o + ⟦ ys ⟧ * suc b
    □

∷ns-mono-strict : ∀ {b d o}
    → (x : Fin d) (xs : Numeral b d o)
    → (y : Fin d) (ys : Numeral b d o)
    → ⟦ xs ⟧ ≡ ⟦ ys ⟧
    → Digit-toℕ x o < Digit-toℕ y o
    → ⟦ x ∷ xs ⟧ < ⟦ y ∷ ys ⟧
∷ns-mono-strict {b} {d} {o} x xs y ys ⟦xs⟧≡⟦ys⟧ ⟦x⟧<⟦y⟧ =
    start
        suc ⟦ x ∷ xs ⟧
    ≤⟨ ⟦x⟧<⟦y⟧ +-mono *n-mono b (reflexive ⟦xs⟧≡⟦ys⟧) ⟩
        ⟦ y ∷ ys ⟧
    □

tail-mono-strict : ∀ {b d o}
    → (x : Fin d) (xs : Numeral b d o)
    → (y : Fin d) (ys : Numeral b d o)
    → Greatest x
    → ⟦ x ∷ xs ⟧ < ⟦ y ∷ ys ⟧
    → ⟦ xs ⟧ < ⟦ ys ⟧
tail-mono-strict {b} {_} {o} x xs y ys greatest p
    = *n-mono-strict-inverse b ⟦∷xs⟧<⟦∷ys⟧
    where
        ⟦x⟧≥⟦y⟧ : Digit-toℕ x o ≥ Digit-toℕ y o
        ⟦x⟧≥⟦y⟧ = greatest-of-all o x y greatest
        ⟦∷xs⟧<⟦∷ys⟧ : ⟦ xs ⟧ * b < ⟦ ys ⟧ * b
        ⟦∷xs⟧<⟦∷ys⟧ = +-mono-contra ⟦x⟧≥⟦y⟧ p

tail-mono-strict-Null : ∀ {b d o}
    → (x : Fin d)
    → (y : Fin d) (ys : Numeral b d o)
    → Greatest x
    → ⟦ _∙ {b} {d} {o} x ⟧ < ⟦ y ∷ ys ⟧
    → 0 < ⟦ ys ⟧
tail-mono-strict-Null {b} {_} {o} x y ys greatest p
    = *n-mono-strict-inverse b ⟦∷∙⟧<⟦∷ys⟧
    where
        ⟦x⟧≥⟦y⟧ : Digit-toℕ x o ≥ Digit-toℕ y o
        ⟦x⟧≥⟦y⟧ = greatest-of-all o x y greatest
        ⟦∷∙⟧<⟦∷ys⟧ : 0 < ⟦ ys ⟧ * b
        ⟦∷∙⟧<⟦∷ys⟧ = +-mono-contra ⟦x⟧≥⟦y⟧ $
            start
                suc (Digit-toℕ x o) + 0
            ≈⟨ +-right-identity (suc (Digit-toℕ x o)) ⟩
                suc (Digit-toℕ x o)
            ≤⟨ p ⟩
                ⟦ y ∷ ys ⟧
            □

ext: agda

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


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

open import Functions.Definition
open import Rings.Homomorphisms.Definition
open import Groups.Homomorphisms.Definition
open import Setoids.Setoids
open import Rings.Definition
open import Sets.EquivalenceRelations
open import Groups.QuotientGroup.Definition

module Rings.Quotients.Definition {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ _*A_ : A → A → A} {_+B_ _*B_ : B → B → B} (R : Ring S _+A_ _*A_) (R2 : Ring T _+B_ _*B_) {underf : A → B} (f : RingHom R R2 underf) where

open import Groups.QuotientGroup.Lemmas (Ring.additiveGroup R) (Ring.additiveGroup R2) (RingHom.groupHom f)

quotientByRingHom : Ring (quotientGroupSetoid (Ring.additiveGroup R) (RingHom.groupHom f)) _+A_ _*A_
Ring.additiveGroup quotientByRingHom = quotientGroupByHom (Ring.additiveGroup R) (RingHom.groupHom f)
Ring.*WellDefined quotientByRingHom fr=ft fs=fu = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (transitive (RingHom.ringHom f) (transitive (Ring.*WellDefined R2 (quotientGroupLemma' (Ring.additiveGroup R) (RingHom.groupHom f) fr=ft) (quotientGroupLemma' (Ring.additiveGroup R) (RingHom.groupHom f) fs=fu)) (symmetric (RingHom.ringHom f))))
  where
    open Setoid T
    open Equivalence eq
Ring.1R quotientByRingHom = Ring.1R R
Ring.groupIsAbelian quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.groupIsAbelian R))
Ring.*Associative quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*Associative R))
Ring.*Commutative quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*Commutative R))
Ring.*DistributesOver+ quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.*DistributesOver+ R))
Ring.identIsIdent quotientByRingHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (GroupHom.wellDefined (RingHom.groupHom f) (Ring.identIsIdent R))

projectionMapIsHom : RingHom R quotientByRingHom id
RingHom.preserves1 projectionMapIsHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (Equivalence.reflexive (Setoid.eq T))
RingHom.ringHom projectionMapIsHom = quotientGroupLemma (Ring.additiveGroup R) (RingHom.groupHom f) (Equivalence.reflexive (Setoid.eq T))
RingHom.groupHom projectionMapIsHom = projectionMapIsGroupHom


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Int.MoreInts.DiffInt.Properties where

open import Cubical.Foundations.HLevels

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

open import Cubical.Data.Int.MoreInts.DiffInt.Base
open import Cubical.Data.Nat as ℕ renaming (_+_ to _+ℕ_ ; _·_ to _*ℕ_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Nullary

open import Cubical.HITs.SetQuotients as SetQuotients
open import Cubical.HITs.PropositionalTruncation as PropositionalTruncation
open import Cubical.Foundations.Isomorphism

open BinaryRelation

relIsEquiv : isEquivRel rel
relIsEquiv = equivRel {A = ℕ × ℕ} relIsRefl relIsSym relIsTrans
  where
    relIsRefl : isRefl rel
    relIsRefl (a0 , a1) = refl

    relIsSym : isSym rel
    relIsSym (a0 , a1) (b0 , b1) p = sym p

    relIsTrans : isTrans rel
    relIsTrans (a0 , a1) (b0 , b1) (c0 , c1) p0 p1 =
      inj-m+ {m = (b0 +ℕ b1)} ((b0 +ℕ b1) +ℕ (a0 +ℕ c1) ≡⟨ ℕ.+-assoc (b0 +ℕ b1) a0 c1  ⟩
            ((b0 +ℕ b1) +ℕ a0) +ℕ c1 ≡[ i ]⟨ ℕ.+-comm b0 b1 i +ℕ a0   +ℕ c1 ⟩
            ((b1 +ℕ b0) +ℕ a0) +ℕ c1 ≡[ i ]⟨ ℕ.+-comm (b1 +ℕ b0) a0 i +ℕ c1 ⟩
            (a0 +ℕ (b1 +ℕ b0)) +ℕ c1 ≡[ i ]⟨ ℕ.+-assoc a0 b1 b0 i    +ℕ c1 ⟩
            (a0 +ℕ b1) +ℕ b0 +ℕ c1 ≡⟨ sym (ℕ.+-assoc (a0 +ℕ b1) b0 c1) ⟩
            (a0 +ℕ b1) +ℕ (b0 +ℕ c1) ≡⟨ cong (λ p → p . fst +ℕ p .snd) (transport ΣPath≡PathΣ (p0 , p1))⟩
            (b0 +ℕ a1) +ℕ (c0 +ℕ b1) ≡⟨ sym (ℕ.+-assoc b0 a1 (c0 +ℕ b1))⟩
            b0 +ℕ (a1 +ℕ (c0 +ℕ b1)) ≡[ i ]⟨ b0 +ℕ (a1 +ℕ ℕ.+-comm c0 b1 i) ⟩
            b0 +ℕ (a1 +ℕ (b1 +ℕ c0)) ≡[ i ]⟨ b0 +ℕ ℕ.+-comm a1 (b1 +ℕ c0) i ⟩
            b0 +ℕ ((b1 +ℕ c0) +ℕ a1) ≡[ i ]⟨ b0 +ℕ ℕ.+-assoc b1 c0 a1 (~ i) ⟩
            b0 +ℕ (b1 +ℕ (c0 +ℕ a1)) ≡⟨ ℕ.+-assoc b0 b1 (c0 +ℕ a1)⟩
            (b0 +ℕ b1) +ℕ (c0 +ℕ a1) ∎ )

relIsProp : BinaryRelation.isPropValued rel
relIsProp a b x y = isSetℕ _ _ _ _

discreteℤ : Discrete ℤ
discreteℤ = discreteSetQuotients (discreteΣ discreteℕ λ _ → discreteℕ) relIsProp relIsEquiv (λ _ _ → discreteℕ _ _)

private
  _ : Dec→Bool (discreteℤ [ (3 , 5) ] [ (4 , 6) ]) ≡ true
  _ = refl

  _ : Dec→Bool (discreteℤ [ (3 , 5) ] [ (4 , 7) ]) ≡ false
  _ = refl

  _+ℕ'_ : (ℕ × ℕ) → (ℕ × ℕ) → (ℕ × ℕ)
  (n₁ , n₂) +ℕ' (m₁ , m₂) = (n₁ +ℕ m₁ , n₂ +ℕ m₂)

  [_-ℕ'_] : ℕ → ℕ → ℤ
  [ x -ℕ' y ] = [ x , y ]

  ℤ-cancelˡ : ∀ {a b} (c : ℕ) → [ (c ℕ.+ a) -ℕ' (c +ℕ b) ] ≡ [ a -ℕ' b ]
  ℤ-cancelˡ {a} {b} c = eq/ _ _ (tmp a b c)
    where tmp : ∀ a b c → rel (c +ℕ a , c +ℕ b) (a , b)
          tmp a b c =
            c +ℕ a +ℕ b
              ≡⟨ cong (λ x → x +ℕ b) (ℕ.+-comm c a) ⟩
            a +ℕ c +ℕ b
              ≡⟨ sym(ℕ.+-assoc a c b) ⟩
            a +ℕ (c +ℕ b) ∎

  ℤ-cancelʳ : ∀ {a b} (c : ℕ) → [ a +ℕ c -ℕ' b +ℕ c ] ≡ [ a -ℕ' b ]
  ℤ-cancelʳ {a} {b} c = eq/ _ _ (tmp a b c)
    where tmp : ∀ a b c → rel (a +ℕ c , b +ℕ c) (a , b)
          tmp a b c =
            a +ℕ c +ℕ b
              ≡⟨ sym(ℕ.+-assoc a c b) ⟩
            a +ℕ (c +ℕ b)
              ≡⟨ cong (λ x → a +ℕ x) (ℕ.+-comm c b) ⟩
            a +ℕ (b +ℕ c) ∎

  -- right congruence
  +-right-congruence : ∀ x y z → rel y z → rel (x +ℕ' y) (x +ℕ' z)
  +-right-congruence x y z  p =
    (fst x +ℕ fst y) +ℕ (snd x +ℕ snd z)
      ≡⟨ cong (λ x' → (fst x +ℕ fst y) +ℕ x') (ℕ.+-comm (snd x) (snd z)) ⟩
    (fst x +ℕ fst y) +ℕ (snd z +ℕ snd x)
      ≡⟨ ℕ.+-assoc (fst x +ℕ fst y) (snd z) (snd x) ⟩
    fst x +ℕ fst y +ℕ snd z +ℕ snd x
      ≡⟨ cong (λ x' → x' +ℕ snd x) (sym (ℕ.+-assoc (fst x) (fst y) (snd z))) ⟩
    fst x +ℕ (fst y +ℕ snd z) +ℕ snd x
      ≡⟨ cong (λ x' → fst x +ℕ x' +ℕ snd x) p ⟩
    fst x +ℕ (fst z +ℕ snd y) +ℕ snd x
      ≡⟨ cong (λ x' → x' +ℕ snd x) (ℕ.+-assoc (fst x) (fst z) (snd y)) ⟩
    fst x +ℕ fst z +ℕ snd y +ℕ snd x
      ≡⟨ sym (ℕ.+-assoc (fst x +ℕ fst z) (snd y) (snd x)) ⟩
    fst x +ℕ fst z +ℕ (snd y +ℕ snd x)
      ≡⟨ cong (λ x' → fst x +ℕ fst z +ℕ x') (ℕ.+-comm (snd y) (snd x)) ⟩
    fst x +ℕ fst z +ℕ (snd x +ℕ snd y) ∎

  +-left-congruence : ∀ x y z → rel x y → rel (x +ℕ' z) (y +ℕ' z)
  +-left-congruence x y z p =
    (fst x +ℕ fst z) +ℕ (snd y +ℕ snd z)
      ≡⟨ cong (λ x' → x' +ℕ (snd y +ℕ snd z)) (ℕ.+-comm (fst x) (fst z)) ⟩
    (fst z +ℕ fst x) +ℕ (snd y +ℕ snd z)
      ≡⟨ ℕ.+-assoc (fst z +ℕ fst x) (snd y) (snd z) ⟩
    fst z +ℕ fst x +ℕ snd y +ℕ snd z
      ≡⟨ cong (λ x' → x' +ℕ snd z) (sym (ℕ.+-assoc (fst z) (fst x) (snd y))) ⟩
    fst z +ℕ (fst x +ℕ snd y) +ℕ snd z
      ≡⟨ cong (λ x' → fst z +ℕ x' +ℕ snd z) p ⟩
    fst z +ℕ (fst y +ℕ snd x) +ℕ snd z
      ≡⟨ cong (λ x' → x' +ℕ snd z) (ℕ.+-assoc (fst z) (fst y) (snd x)) ⟩
    fst z +ℕ fst y +ℕ snd x +ℕ snd z
      ≡⟨ sym (ℕ.+-assoc (fst z +ℕ fst y) (snd x) (snd z)) ⟩
    fst z +ℕ fst y +ℕ (snd x +ℕ snd z)
      ≡⟨ cong (λ x' → x' +ℕ (snd x +ℕ snd z)) (ℕ.+-comm (fst z) (fst y)) ⟩
    fst y +ℕ fst z +ℕ (snd x +ℕ snd z) ∎

ℤ-isSet : isSet ℤ
ℤ-isSet m n p q = squash/ m n p q

_+_ : ℤ → ℤ → ℤ
_+_ = SetQuotients.rec2 ℤ-isSet (λ x y → [ x +ℕ' y ]) feql feqr
    where
      feql : (a b c : ℕ × ℕ) (r : rel a b) → [ a +ℕ' c ] ≡ [ b +ℕ' c ]
      feql a b c r = eq/ (a +ℕ' c) (b +ℕ' c) (+-left-congruence a b c r)
      feqr : (a b c : ℕ × ℕ) (r : rel b c) → [ a +ℕ' b ] ≡ [ a +ℕ' c ]
      feqr a b c r = eq/ (a +ℕ' b) (a +ℕ' c) (+-right-congruence a b c r)

private
  zero-identityˡ-lem : (a : ℕ)(b : ℤ) → (Σ (ℕ × ℕ) ( λ (c , d) → [ (c , d) ]  ≡ b )) → [ a , a ] + b ≡ b
  zero-identityˡ-lem a b ( (c , d) , p ) =
    [ a , a ] + b           ≡⟨ cong (λ x → [ a , a ] + x) (sym p) ⟩
    [ a , a ] + [ c , d ]   ≡⟨ ℤ-cancelˡ a ⟩
    [ c , d ]               ≡⟨ p ⟩
    b ∎

  zero-identityʳ-lem : (a : ℕ)(b : ℤ) → (Σ (ℕ × ℕ) ( λ (c , d) → [ (c , d) ]  ≡ b )) → b + [ a , a ] ≡ b
  zero-identityʳ-lem a b ( (c , d) , p ) =
    b + [ a , a ]           ≡⟨ cong (λ x → x + [ a , a ]) (sym(p)) ⟩
    [ c , d ] + [ a , a ]   ≡⟨ ℤ-cancelʳ a ⟩
    [ c , d ]               ≡⟨ p ⟩
    b ∎

zero-identityˡ : (a : ℕ) (b : ℤ) → [ a , a ] + b ≡ b
zero-identityˡ a b = PropositionalTruncation.rec (lem2 a b) (zero-identityˡ-lem a b) ([]surjective b)
                     where
                       lem2 : (a : ℕ) (b : ℤ) → isProp ([ a , a ] + b ≡ b)
                       lem2 a b = ℤ-isSet ([ a , a ] + b) b

zero-identityʳ : (a : ℕ)(b : ℤ) → b + [ a , a ] ≡ b
zero-identityʳ a b = PropositionalTruncation.rec (lem2 a b) (zero-identityʳ-lem a b) ([]surjective b)
                     where
                       lem2 : (a : ℕ) (b : ℤ) → isProp (b + [ a , a ] ≡ b)
                       lem2 a b = ℤ-isSet (b + [ a , a ]) b

-ℤ_  : ℤ → ℤ
-ℤ [ a ] = [ snd a , fst a ]
-ℤ eq/ a b r i = eq/ (snd a , fst a) (snd b , fst b) (tmp a b r) i
                  where
                    tmp : ∀ a b → fst a +ℕ snd b ≡ fst b +ℕ snd a → snd a +ℕ fst b ≡ snd b +ℕ fst a
                    tmp a b r =
                      snd a +ℕ fst b ≡⟨ ℕ.+-comm (snd a) (fst b) ⟩
                      fst b +ℕ snd a ≡⟨ sym r ⟩
                      fst a +ℕ snd b ≡⟨ ℕ.+-comm (fst a) (snd b) ⟩
                      snd b +ℕ fst a ∎
-ℤ squash/ a a₁ p q i i₁ = squash/ (-ℤ a) (-ℤ a₁) (cong (λ x → -ℤ x) p) (cong (λ x → -ℤ x) q) i i₁

private
  -ℤ-invʳ-lem : (b : ℤ) → (Σ (ℕ × ℕ) ( λ (c , d) → [ (c , d) ]  ≡ b )) → b + (-ℤ b) ≡ [ 0 , 0 ]
  -ℤ-invʳ-lem b ( (c , d) , p ) =
    b + (-ℤ b)
      ≡⟨ cong (λ x → x + (-ℤ b)) (sym p) ⟩
    [ c , d ] + (-ℤ b)
      ≡⟨ cong (λ x → [ c , d ] + (-ℤ x)) (sym p) ⟩
    [ c +ℕ d , d +ℕ c ]
      ≡⟨ cong (λ x → [ c +ℕ d , x ]) (ℕ.+-comm d c) ⟩
    [ c +ℕ d , c +ℕ d ]
      ≡⟨ ℤ-cancelˡ c ⟩
    [ d -ℕ' d ]
      ≡⟨ sym(ℤ-cancelʳ 0) ⟩
    [ d +ℕ 0 -ℕ' d +ℕ 0 ]
      ≡⟨ ℤ-cancelˡ d ⟩
    [ 0 , 0 ] ∎

  -ℤ-invˡ-lem : (b : ℤ) → (Σ (ℕ × ℕ) ( λ (c , d) → [ (c , d) ]  ≡ b )) → (-ℤ b) + b ≡ [ 0 , 0 ]
  -ℤ-invˡ-lem b ( (c , d) , p ) =
    (-ℤ b) + b
      ≡⟨ cong (λ x → (-ℤ b) + x) (sym p) ⟩
    (-ℤ b) + [ c , d ]
      ≡⟨ cong (λ x → (-ℤ x) + [ c , d ]) (sym p) ⟩
    [ d +ℕ c , c +ℕ d ]
      ≡⟨ cong (λ x → [ x , c +ℕ d ]) (ℕ.+-comm d c) ⟩
    [ c +ℕ d , c +ℕ d ]
      ≡⟨ ℤ-cancelˡ c ⟩
    [ d -ℕ' d ]
      ≡⟨ sym(ℤ-cancelʳ 0) ⟩
    [ d +ℕ 0 -ℕ' d +ℕ 0 ]
      ≡⟨ ℤ-cancelˡ d ⟩
    [ 0 , 0 ] ∎

_-_ : ℤ → ℤ → ℤ
a - b = a + (-ℤ b)

-ℤ-invʳ : (b : ℤ) → b + (-ℤ b) ≡ [ 0 , 0 ]
-ℤ-invʳ b = PropositionalTruncation.rec (lem2 b) (-ℤ-invʳ-lem b) ([]surjective b)
             where
               lem2 : (b : ℤ) → isProp (b + (-ℤ b) ≡ [ 0 , 0 ])
               lem2 b = ℤ-isSet (b + (-ℤ b)) [ 0 , 0 ]

-ℤ-invˡ : (b : ℤ) → (-ℤ b) + b ≡ [ 0 , 0 ]
-ℤ-invˡ b = PropositionalTruncation.rec (lem2 b) (-ℤ-invˡ-lem b) ([]surjective b)
             where
               lem2 : (b : ℤ) → isProp ((-ℤ b) + b ≡ [ 0 , 0 ])
               lem2 b = ℤ-isSet ((-ℤ b) + b) [ 0 , 0 ]

+ℤ-assoc : ∀ x y z → x + (y + z) ≡ (x + y) + z
+ℤ-assoc = elimProp3 (λ _ _ _ → ℤ-isSet _ _)
    (λ { (a , b) (c , d) (e , f) i → [ ℕ.+-assoc a c e i -ℕ' ℕ.+-assoc b d f i ] })

+ℤ-comm : ∀ x y → x + y ≡ y + x
+ℤ-comm = elimProp2 (λ _ _ → ℤ-isSet _ _)
         λ ( a , b ) ( c , d ) i → [ ℕ.+-comm a c i -ℕ'  ℕ.+-comm b d i ]

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------------
-- Main properties of the McCarthy 91 function
------------------------------------------------------------------------------

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

-- The main properties proved of the McCarthy 91 function (called
-- f₉₁) are

-- 1. The function always terminates.
-- 2. For all n, n < f₉₁ n + 11.
-- 3. For all n > 100, then f₉₁ n = n - 10.
-- 4. For all n <= 100, then f₉₁ n = 91.

-- N.B This module does not contain combined proofs, but it imports
-- modules which contain combined proofs.

module FOTC.Program.McCarthy91.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP
  using ( x>y→x≤y→⊥ )
open import FOTC.Data.Nat.Inequalities.PropertiesATP
  using ( x>y∨x≯y
        ; x≯y→x≤y
        ; x≯Sy→x≯y∨x≡Sy
        ; x+k<y+k→x<y
        ; <-trans
        )
open import FOTC.Data.Nat.PropertiesATP
  using ( ∸-N
        ; +-N
        )
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.Inequalities.PropertiesATP
  using ( x<x+11 )
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP
  using ( 10-N
        ; 11-N
        ; 89-N
        ; 90-N
        ; 91-N
        ; 92-N
        ; 93-N
        ; 94-N
        ; 95-N
        ; 96-N
        ; 97-N
        ; 98-N
        ; 99-N
        ; 100-N
        )
open import FOTC.Program.McCarthy91.ArithmeticATP
open import FOTC.Program.McCarthy91.AuxiliaryPropertiesATP
open import FOTC.Program.McCarthy91.McCarthy91
open import FOTC.Program.McCarthy91.WF-Relation
open import FOTC.Program.McCarthy91.WF-Relation.LT2WF-RelationATP
open import FOTC.Program.McCarthy91.WF-Relation.Induction.Acc.WF-ATP

------------------------------------------------------------------------------
-- For all n > 100, then f₉₁ n = n - 10.
postulate f₉₁-x>100 : ∀ n → n > 100' → f₉₁ n ≡ n ∸ 10'
{-# ATP prove f₉₁-x>100 #-}

-- For all n <= 100, then f₉₁ n = 91.
f₉₁-x≯100 : ∀ {n} → N n → n ≯ 100' → f₉₁ n ≡ 91'
f₉₁-x≯100 = ◁-wfind A h
  where
  A : D → Set
  A d = d ≯ 100' → f₉₁ d ≡ 91'

  h : ∀ {m} → N m → (∀ {k} → N k → k ◁ m → A k) → A m
  h {m} Nm f with x>y∨x≯y Nm 100-N
  ... | inj₁ m>100 = λ m≯100 →
                     ⊥-elim (x>y→x≤y→⊥ Nm 100-N m>100 (x≯y→x≤y Nm 100-N m≯100))
  ... | inj₂ m≯100 with x≯Sy→x≯y∨x≡Sy Nm 99-N m≯100
  ... | inj₂ m≡100 = λ _ → f₉₁-x≡y f₉₁-100 m≡100
  ... | inj₁ m≯99 with x≯Sy→x≯y∨x≡Sy Nm 98-N m≯99
  ... | inj₂ m≡99 = λ _ → f₉₁-x≡y f₉₁-99 m≡99
  ... | inj₁ m≯98 with x≯Sy→x≯y∨x≡Sy Nm 97-N m≯98
  ... | inj₂ m≡98 = λ _ → f₉₁-x≡y f₉₁-98 m≡98
  ... | inj₁ m≯97 with x≯Sy→x≯y∨x≡Sy Nm 96-N m≯97
  ... | inj₂ m≡97 = λ _ → f₉₁-x≡y f₉₁-97 m≡97
  ... | inj₁ m≯96 with x≯Sy→x≯y∨x≡Sy Nm 95-N m≯96
  ... | inj₂ m≡96 = λ _ → f₉₁-x≡y f₉₁-96 m≡96
  ... | inj₁ m≯95 with x≯Sy→x≯y∨x≡Sy Nm 94-N m≯95
  ... | inj₂ m≡95 = λ _ → f₉₁-x≡y f₉₁-95 m≡95
  ... | inj₁ m≯94 with x≯Sy→x≯y∨x≡Sy Nm 93-N m≯94
  ... | inj₂ m≡94 = λ _ → f₉₁-x≡y f₉₁-94 m≡94
  ... | inj₁ m≯93 with x≯Sy→x≯y∨x≡Sy Nm 92-N m≯93
  ... | inj₂ m≡93 = λ _ → f₉₁-x≡y f₉₁-93 m≡93
  ... | inj₁ m≯92 with x≯Sy→x≯y∨x≡Sy Nm 91-N m≯92
  ... | inj₂ m≡92 = λ _ → f₉₁-x≡y f₉₁-92 m≡92
  ... | inj₁ m≯91 with x≯Sy→x≯y∨x≡Sy Nm 90-N m≯91
  ... | inj₂ m≡91 = λ _ → f₉₁-x≡y f₉₁-91 m≡91
  ... | inj₁ m≯90 with x≯Sy→x≯y∨x≡Sy Nm 89-N m≯90
  ... | inj₂ m≡90 = λ _ → f₉₁-x≡y f₉₁-90 m≡90
  ... | inj₁ m≯89 = λ _ → f₉₁-m≯89
    where
    m≤89 : m ≤ 89'
    m≤89 = x≯y→x≤y Nm 89-N m≯89

    f₉₁-m+11 : m + 11' ≯ 100' → f₉₁ (m + 11') ≡ 91'
    f₉₁-m+11 = f (x+11-N Nm) (<→◁ (x+11-N Nm) Nm m≯100 (x<x+11 Nm))

    f₉₁-m≯89 : f₉₁ m ≡ 91'
    f₉₁-m≯89 = f₉₁-x≯100-helper m 91' m≯100
                                (f₉₁-m+11 (x≤89→x+11≯100 Nm m≤89))
                                f₉₁-91

-- The function always terminates.
f₉₁-N : ∀ {n} → N n → N (f₉₁ n)
f₉₁-N {n} Nn = case prf₁ prf₂ (x>y∨x≯y Nn 100-N)
  where
  prf₁ : n > 100' → N (f₉₁ n)
  prf₁ n>100 = subst N (sym (f₉₁-x>100 n n>100)) (∸-N Nn 10-N)

  prf₂ : n ≯ 100' → N (f₉₁ n)
  prf₂ n≯100 = subst N (sym (f₉₁-x≯100 Nn n≯100)) 91-N

-- The function always terminates (using Agda with constructor).
f₉₁-N' : ∀ {n} → N n → N (f₉₁ n)
f₉₁-N' {n} Nn with x>y∨x≯y Nn 100-N
... | inj₁ n>100 = subst N (sym (f₉₁-x>100 n n>100)) (∸-N Nn 10-N)
... | inj₂ n≯100 = subst N (sym (f₉₁-x≯100 Nn n≯100)) 91-N

-- For all n, n < f₉₁ n + 11.
f₉₁-ineq : ∀ {n} → N n → n < f₉₁ n + 11'
f₉₁-ineq = ◁-wfind A h
  where
  A : D → Set
  A d = d < f₉₁ d + 11'

  h : ∀ {m} → N m → (∀ {k} → N k → k ◁ m → A k) → A m
  h {m} Nm f with x>y∨x≯y Nm 100-N
  ... | inj₁ m>100 = x>100→x<f₉₁-x+11 Nm m>100
  ... | inj₂ m≯100 =
    let f₉₁-m+11-N : N (f₉₁ (m + 11'))
        f₉₁-m+11-N = f₉₁-N (+-N Nm 11-N)

        h₁ : A (m + 11')
        h₁ = f (x+11-N Nm) (<→◁ (x+11-N Nm) Nm m≯100 (x<x+11 Nm))

        m<f₉₁m+11 : m < f₉₁ (m + 11')
        m<f₉₁m+11 = x+k<y+k→x<y Nm f₉₁-m+11-N 11-N h₁

        h₂ : A (f₉₁ (m + 11'))
        h₂ = f f₉₁-m+11-N (<→◁ f₉₁-m+11-N Nm m≯100 m<f₉₁m+11)

    in (<-trans Nm f₉₁-m+11-N (x+11-N (f₉₁-N Nm))
                m<f₉₁m+11
                (f₉₁x+11<f₉₁x+11 m m≯100 h₂))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import CS410-Prelude

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

data Vec (X : Set) : Nat -> Set where
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)

infixr 4 _,-_

------------------------------------------------------------------------------
-- Heads and Tails
------------------------------------------------------------------------------

vHead : {X : Set}{n : Nat} -> Vec X (suc n) -> X
vHead (x ,- xs) = x

vTail : {X : Set}{n : Nat} -> Vec X (suc n) -> Vec X n
vTail (x ,- xs) = xs

vHeadTailFact : {X : Set}{n : Nat}(xs : Vec X (suc n)) -> (vHead xs ,- vTail xs) == xs
vHeadTailFact (x ,- xs) = refl (x ,- xs)

------------------------------------------------------------------------------
-- Concatenation and its Inverse
------------------------------------------------------------------------------

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V ys        = ys
(x ,- xs) +V ys = x ,- xs +V ys

infixr 4 _+V_

vChop : {X : Set}(m : Nat){n : Nat} -> Vec X (m +N n) -> Vec X m * Vec X n
vChop zero xs = [] , xs
vChop (suc m) (x ,- xs) with vChop m xs
vChop (suc m) (x ,- xs) | xf , xb = (x ,- xf) , xb

vChopAppendFact : {X : Set}{m n : Nat}(xs : Vec X m)(ys : Vec X n) -> vChop m (xs +V ys) == (xs , ys)
vChopAppendFact [] ys = refl ([] , ys)
vChopAppendFact (x ,- xs) ys rewrite vChopAppendFact xs ys = refl ((x ,- xs) , ys)

------------------------------------------------------------------------------
-- Map, take I
------------------------------------------------------------------------------

-- Implement the higher-order function that takes an operation on
-- elements and does it to each element of a vector. Use recursion
-- on the vector.
-- Note that the type tells you the size remains the same.

-- Show that if the elementwise function "does nothing", neither does
-- its vMap. "map of identity is identity"

-- Show that two vMaps in a row can be collapsed to just one, or
-- "composition of maps is map of compositions"

vMap : {X Y : Set} -> (X -> Y) -> {n : Nat} -> Vec X n -> Vec Y n
vMap f []        = []
vMap f (x ,- xs) = f x ,- vMap f xs

vMapIdFact : {X : Set}{f : X -> X}(feq : (x : X) -> f x == x) ->
             {n : Nat}(xs : Vec X n) ->
             vMap f xs == xs
vMapIdFact feq [] = refl []
vMapIdFact feq (x ,- xs) rewrite vMapIdFact feq xs | feq x
  = refl (x ,- xs)

vMapCpFact : {X Y Z : Set}{f : Y -> Z}{g : X -> Y}{h : X -> Z}(heq : (x : X) -> f (g x) == h x) ->
             {n : Nat}(xs : Vec X n) ->
             vMap f (vMap g xs) == vMap h xs
vMapCpFact heq [] = refl []
vMapCpFact {f = f}{g = g}{h = h} heq (x ,- xs) rewrite vMapCpFact {f = f}{g = g}{h = h} heq xs | heq x
  = refl (h x ,- vMap h xs)

------------------------------------------------------------------------------
-- vMap and +V
------------------------------------------------------------------------------

-- Show that if you've got two vectors of Xs and a function from X to Y,
-- and you want to concatenate and map, it doesn't matter which you do
-- first.

vMap+VFact : {X Y : Set}(f : X -> Y) ->
             {m n : Nat}(xs : Vec X m)(xs' : Vec X n) ->
             vMap f (xs +V xs') == (vMap f xs +V vMap f xs')
vMap+VFact f [] xs' = refl (vMap f xs')
vMap+VFact f (x ,- xs) xs' rewrite vMap+VFact f xs xs' = refl (f x ,- vMap f xs +V vMap f xs')

------------------------------------------------------------------------------
-- Applicative Structure (giving mapping and zipping cheaply)
------------------------------------------------------------------------------

-- HINT: you will need to override the default invisibility of n to do this.
vPure : {X : Set} -> X -> {n : Nat} -> Vec X n
vPure x {zero}  = []
vPure x {suc n} =  x ,- vPure x

_$V_ : {X Y : Set}{n : Nat} -> Vec (X -> Y) n -> Vec X n -> Vec Y n
[] $V []           = []
f ,- fs $V x ,- xs =  f x ,- (fs $V xs)

infixl 3 _$V_

-- Pattern matching and recursion are forbidden for the next two tasks.

-- implement vMap again, but as a one-liner
vec : {X Y : Set} -> (X -> Y) -> {n : Nat} -> Vec X n -> Vec Y n
vec f xs = vPure f $V xs

-- implement the operation which pairs up corresponding elements
vZip : {X Y : Set}{n : Nat} -> Vec X n -> Vec Y n -> Vec (X * Y) n
vZip xs ys = vPure _,_ $V xs $V ys

------------------------------------------------------------------------------
-- Applicative Laws
------------------------------------------------------------------------------

-- According to "Applicative programming with effects" by
--   Conor McBride and Ross Paterson
-- some laws should hold for applicative functors.
-- Check that this is the case.

vIdentity : {X : Set}{f : X -> X}(feq : (x : X) -> f x == x) ->
            {n : Nat}(xs : Vec X n) -> (vPure f $V xs) == xs
vIdentity feq [] = refl []
vIdentity feq (x ,- xs) rewrite vIdentity feq xs | feq x = refl (x ,- xs)

vHomomorphism : {X Y : Set}(f : X -> Y)(x : X) -> {n : Nat} ->
                   (vPure f $V vPure x) == vPure (f x) {n}
vHomomorphism f x {zero} = refl []
vHomomorphism f x {suc n} rewrite vHomomorphism f x {n} = refl (f x ,- vPure (f x))

vInterchange : {X Y : Set}{n : Nat}(fs : Vec (X -> Y) n)(x : X) ->
                 (fs $V vPure x) == (vPure (_$ x) $V fs)
vInterchange [] x = refl []
vInterchange (f ,- fs) x rewrite vInterchange fs x = refl (f x ,- (vPure (\ f → f x) $V fs))

vComposition : {X Y Z : Set}{n : Nat}(fs : Vec (Y -> Z) n)(gs : Vec (X -> Y) n)(xs : Vec X n) ->
                  (vPure _<<_ $V fs $V gs $V xs) == (fs $V (gs $V xs))
vComposition [] [] [] = refl []
vComposition (f ,- fs) (g ,- gs) (x ,- xs) rewrite vComposition fs gs xs = refl (f (g x) ,- (fs $V (gs $V xs)))

------------------------------------------------------------------------------
-- Order-Preserving Embeddings (also known in the business as "thinnings")
------------------------------------------------------------------------------

-- What have these to do with Pascal's Triangle?

data _<=_ : Nat -> Nat -> Set where
  oz :                          zero  <= zero
  os : {n m : Nat} -> n <= m -> suc n <= suc m
  o' : {n m : Nat} -> n <= m ->     n <= suc m

-- Find all the values in each of the following <= types.
-- This is a good opportunity to learn to use C-c C-a with the -l option
--   (a.k.a. "google the type" without "I feel lucky")
-- The -s n option also helps.

all0<=4 : Vec (0 <= 4) 1
all0<=4 = o' (o' (o' (o' oz))) ,- []

all1<=4 : Vec (1 <= 4) 4
all1<=4 = o' (o' (o' (os oz))) ,-
          o' (o' (os (o' oz))) ,-
          o' (os (o' (o' oz))) ,-
          os (o' (o' (o' oz))) ,-
          []

all2<=4 : Vec (2 <= 4) 6
all2<=4 =  os (os (o' (o' oz))) ,-
           os (o' (os (o' oz))) ,-
           os (o' (o' (os oz))) ,-
           o' (os (os (o' oz))) ,-
           o' (os (o' (os oz))) ,-
           o' (o' (os (os oz))) ,-
           []

all3<=4 : Vec (3 <= 4) 4
all3<=4 = os (os (os (o' oz))) ,-
          os (os (o' (os oz))) ,-
          os (o' (os (os oz))) ,-
          o' (os (os (os oz))) ,-
          []

all4<=4 : Vec (4 <= 4) 1
all4<=4 = os (os (os (os oz))) ,- []

-- Prove the following. A massive case analysis "rant" is fine.

no5<=4 : 5 <= 4 -> Zero
no5<=4 (os (os (os (os ()))))
no5<=4 (os (os (os (o' ()))))
no5<=4 (os (os (o' (os ()))))
no5<=4 (os (os (o' (o' ()))))
no5<=4 (os (o' (os (os ()))))
no5<=4 (os (o' (os (o' ()))))
no5<=4 (os (o' (o' (os ()))))
no5<=4 (os (o' (o' (o' ()))))
no5<=4 (o' (os (os (os ()))))
no5<=4 (o' (os (os (o' ()))))
no5<=4 (o' (os (o' (os ()))))
no5<=4 (o' (os (o' (o' ()))))
no5<=4 (o' (o' (os (os ()))))
no5<=4 (o' (o' (os (o' ()))))
no5<=4 (o' (o' (o' (os ()))))
no5<=4 (o' (o' (o' (o' ()))))

------------------------------------------------------------------------------
-- Order-Preserving Embeddings Select From Vectors
------------------------------------------------------------------------------

-- Use n <= m to encode the choice of n elements from an m-Vector.
-- The os constructor tells you to take the next element of the vector;
-- the o' constructor tells you to omit the next element of the vector.

_<?=_ : {X : Set}{n m : Nat} -> n <= m -> Vec X m -> Vec X n
oz    <?= [] = []
os th <?= (x ,- xs) =  x ,- th <?= xs
o' th <?= (x ,- xs) =  th <?= xs

-- it shouldn't matter whether you map then select or select then map

vMap<?=Fact : {X Y : Set}(f : X -> Y)
              {n m : Nat}(th : n <= m)(xs : Vec X m) ->
              vMap f (th <?= xs) == (th <?= vMap f xs)
vMap<?=Fact f oz [] = refl []
vMap<?=Fact f (os th) (x ,- xs) rewrite vMap<?=Fact f th xs = refl (f x ,- (th <?= vMap f xs))
vMap<?=Fact f (o' th) (x ,- xs) rewrite vMap<?=Fact f th xs = refl (th <?= vMap f xs)

------------------------------------------------------------------------------
-- Our Favourite Thinnings
------------------------------------------------------------------------------

-- Construct the identity thinning and the empty thinning.

oi : {n : Nat} -> n <= n
oi {zero}  = oz
oi {suc n} = os oi

oe : {n : Nat} -> 0 <= n
oe {zero}  = oz
oe {suc n} = o' oe

-- Show that all empty thinnings are equal to yours.

oeUnique : {n : Nat}(th : 0 <= n) -> th == oe
oeUnique oz     = refl oz
oeUnique (o' i) with oeUnique i
oeUnique (o' .oe) | refl .oe = refl (o' oe)

-- Show that there are no thinnings of form big <= small  (TRICKY)
-- Then show that all the identity thinnings are equal to yours.
-- Note that you can try the second even if you haven't finished the first.
-- HINT: you WILL need to expose the invisible numbers.
-- HINT: check CS410-Prelude for a reminder of >=

oTooBig : {n m : Nat} -> n >= m -> suc n <= m -> Zero
oTooBig {_} {zero} n>=m ()
oTooBig {zero} {suc m} n>=m (th) = n>=m
oTooBig {suc n} {suc m} n>=m (os th) with oTooBig {n} {m} n>=m th
oTooBig {suc n} {suc m} n>=m (os th) | ()
oTooBig {suc n} {suc m} n>=m (o' th) with oTooBig {suc n} {m} (trans->= (suc n) n m (suc->= n) n>=m) th
oTooBig {suc n} {suc m} n>=m (o' th) | ()

oiUnique : {n : Nat}(th : n <= n) -> th == oi
oiUnique oz = refl oz
oiUnique (os th) with oiUnique th
oiUnique (os .oi) | refl .oi = refl (os oi)
oiUnique {n}(o' th) with oTooBig (refl->= n) th
oiUnique {.(suc _)} (o' th) | ()

-- Show that the identity thinning selects the whole vector

id-<?= : {X : Set}{n : Nat}(xs : Vec X n) -> (oi <?= xs) == xs
id-<?= [] = refl []
id-<?= (x ,- xs) rewrite id-<?= xs = refl (x ,- xs)

------------------------------------------------------------------------------
-- Composition of Thinnings
------------------------------------------------------------------------------

-- Define the composition of thinnings and show that selecting by a
-- composite thinning is like selecting then selecting again.
-- A small bonus applies to minimizing the length of the proof.
-- To collect the bonus, you will need to think carefully about
-- how to make the composition as *lazy* as possible.

_o>>_ : {p n m : Nat} -> p <= n -> n <= m -> p <= m
oz o>> th' = th'
os th o>> os th' with th o>> th'
os th o>> os th' | p = os p
os th o>> o' th' with (os th) o>> th'
os th o>> o' th' | p = o' p
o' th o>> os th' with th o>> th'
o' th o>> os th' | p = o' p
o' th o>> o' th' with (o' th) o>> th'
o' th o>> o' th' | p = o' p

cp-<?= : {p n m : Nat}(th : p <= n)(th' : n <= m) ->
         {X : Set}(xs : Vec X m) ->
         ((th o>> th') <?= xs) == (th <?= (th' <?= xs))
cp-<?= oz oz [] = refl []
cp-<?= oz (o' th') xs with o' th' <?= xs
cp-<?= oz (o' th') xs | [] = refl []
cp-<?= (os th) (os th') (x ,- xs) rewrite cp-<?= th th' xs      = refl (x ,- (th <?= (th' <?= xs)))
cp-<?= (os th) (o' th') (x ,- xs) rewrite cp-<?= (os th) th' xs = refl (os th <?= (th' <?= xs))
cp-<?= (o' th) (os th') (x ,- xs) rewrite cp-<?= th th' xs      = refl (th <?= (th' <?= xs))
cp-<?= (o' th) (o' th') (x ,- xs) rewrite cp-<?= (o' th) th' xs = refl (o' th <?= (th' <?= xs))

-- TODO: shorter solution for bonus

------------------------------------------------------------------------------
-- Thinning Dominoes
------------------------------------------------------------------------------

idThen-o>> : {n m : Nat}(th : n <= m) -> (oi o>> th) == th
idThen-o>> oz = refl oz
idThen-o>> (os th) rewrite idThen-o>> th = refl (os th)
idThen-o>> {zero}(o' th) rewrite idThen-o>> th = refl (o' th)
idThen-o>> {suc n}(o' th) rewrite idThen-o>> th = refl (o' th)

idAfter-o>> : {n m : Nat}(th : n <= m) -> (th o>> oi) == th
idAfter-o>> oz = refl oz
idAfter-o>> (os th) rewrite idAfter-o>> th = refl (os th)
idAfter-o>> (o' th) rewrite idAfter-o>> th = refl (o' th)

assoc-o>> : {q p n m : Nat}(th0 : q <= p)(th1 : p <= n)(th2 : n <= m) ->
            ((th0 o>> th1) o>> th2) == (th0 o>> (th1 o>> th2))
assoc-o>> oz th1 th2 = refl (th1 o>> th2)
assoc-o>> (os th0) (os th1) (os th2) rewrite assoc-o>> th0 th1 th2           = refl (os (th0 o>> (th1 o>> th2)))
assoc-o>> (os th0) (os th1) (o' th2) rewrite assoc-o>> (os th0) (os th1) th2 = refl (o' (os th0 o>> (os th1 o>> th2)))
assoc-o>> (os th0) (o' th1) (os th2) rewrite assoc-o>> (os th0) th1 th2      = refl (o' (os th0 o>> (th1 o>> th2)))
assoc-o>> (os th0) (o' th1) (o' th2) rewrite assoc-o>> (os th0) (o' th1) th2 = refl (o' (os th0 o>> (o' th1 o>> th2)))
assoc-o>> (o' th0) (os th1) (os th2) rewrite assoc-o>> th0 th1 th2           = refl (o' (th0 o>> (th1 o>> th2)))
assoc-o>> (o' th0) (os th1) (o' th2) rewrite assoc-o>> (o' th0) (os th1) th2 = refl (o' (o' th0 o>> (os th1 o>> th2)))
assoc-o>> (o' th0) (o' th1) (os th2) rewrite assoc-o>> (o' th0) th1 th2      = refl (o' (o' th0 o>> (th1 o>> th2)))
assoc-o>> (o' th0) (o' th1) (o' th2) rewrite assoc-o>> (o' th0) (o' th1) th2 = refl (o' (o' th0 o>> (o' th1 o>> th2)))

------------------------------------------------------------------------------
-- Vectors as Arrays
------------------------------------------------------------------------------

-- We can use 1 <= n as the type of bounded indices into a vector and do
-- a kind of "array projection". First we select a 1-element vector from
-- the n-element vector, then we take its head to get the element out.

vProject : {n : Nat}{X : Set} -> Vec X n -> 1 <= n -> X
vProject xs i = vHead (i <?= xs)

-- Your (TRICKY) mission is to reverse the process, tabulating a function
-- from indices as a vector. Then show that these operations are inverses.

-- HINT: composition of functions
vTabulate : {n : Nat}{X : Set} -> (1 <= n -> X) -> Vec X n
vTabulate {zero}  f = []
vTabulate {suc n} f with f (os oe) | vTabulate (f << o')
vTabulate {suc n} f | x | xs =  x ,- xs

-- This should be easy if vTabulate is correct.
vTabulateProjections : {n : Nat}{X : Set}(xs : Vec X n) -> vTabulate (vProject xs) == xs
vTabulateProjections [] = refl []
vTabulateProjections (x ,- xs) rewrite vTabulateProjections xs = refl (x ,- xs)

-- HINT: oeUnique
vProjectFromTable : {n : Nat}{X : Set}(f : 1 <= n -> X)(i : 1 <= n) -> vProject (vTabulate f) i == f i
vProjectFromTable f (os i) rewrite oeUnique i = refl (f (os oe))
vProjectFromTable f (o' i) rewrite vProjectFromTable (f << o') i = refl (f (o' i))


text:
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
module DTGP
  {Domain Word : Set}
  (pre post : Word → Domain → Domain)
  (_≟_ : (x y : Domain) → Dec (x ≡ y))
where
open import Function
open import Relation.Binary
open import Data.Bool hiding (_≟_)
open import Data.Nat hiding (_≥_; _≟_)
open import Data.Fin hiding (_+_; raise)
open import Data.Maybe
open import Data.Product hiding (map; swap)
open import Data.List hiding (length) renaming (_++_ to _l++_)
open import Data.Vec hiding (_++_; _>>=_; concat; map; init)
open import DTGP.Rand

infixr 5 _∷_ _++_ _++'_

data Term (inp : Domain) : Domain → Set where
  []  : Term inp inp

  _∷_ : ∀ {d} (w : Word) →
    Term inp (pre w d) → Term inp (post w d)

_++_ : ∀ {inp mid out} →
  Term mid out →
  Term inp mid →
  Term inp out
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data Split {inp out} mid : Term inp out → Set where
  _++'_ :
    (xs : Term mid out)
    (ys : Term inp mid) →
    Split mid (xs ++ ys)

swap₁ : ∀ {inp mid out} {xs ys : Term inp out} →
  Split mid xs → Split mid ys → Term inp out
swap₁ (xs ++' ys) (as ++' bs) = xs ++ bs

swap₂ : ∀ {inp mid out} {xs ys : Term inp out} →
  Split mid xs → Split mid ys → Term inp out
swap₂ (xs ++' ys) (as ++' bs) = as ++ ys

swaps : ∀ {inp mid out} {xs ys : Term inp out} →
  Split mid xs → Split mid ys →
  Term inp out × Term inp out
swaps xs ys = swap₁ xs ys , swap₂ xs ys

split : ∀ {inp out} (n : ℕ) (xs : Term inp out) → ∃ λ mid → Split mid xs
split zero xs = _ , [] ++' xs
split (suc n) [] = _ , [] ++' []
split (suc n) (x ∷ xs) with split n xs
split (suc n) (x ∷ ._) | _ , xs ++' ys = _ , (x ∷ xs) ++' ys

splits : ∀ {inp out} (n : ℕ) mid → (xs : Term inp out) → ∃ (Vec (Split mid xs))
splits zero mid xs with split zero xs
... | mid' , ys with mid ≟ mid'
... | yes p rewrite p = _ , ys ∷ []
... | no p = _ , []
splits (suc n) mid xs with split (suc n) xs
... | mid' , ys with mid ≟ mid' | splits n mid xs
... | yes p | _ , yss rewrite p = _ , ys ∷ yss
... | no p | _ , yss = _ , yss

length : ∀ {inp out} → Term inp out → ℕ
length [] = 0
length (x ∷ xs) = suc (length xs)

split♀ : ∀ {inp out} → (xs : Term inp out) → Rand (∃ λ mid → Split mid xs)
split♀ xs =
  rand >>= λ r →
  let i = r mod (suc (length xs))
  in return (split (toℕ i) xs)

split♂ : ∀ {inp out} (xs : Term inp out) mid →
  Maybe (Rand (Split mid xs))
split♂ xs B
  with splits (length xs) B xs
... | zero , [] = nothing
... | suc n , xss = just (
  rand >>= λ r →
  return (lookup (r mod suc n) xss)
 )

crossover : ∀ {inp out} (♀ ♂ : Term inp out) →
  Rand (Term inp out × Term inp out)
crossover ♀ ♂ =
  split♀ ♀ >>= λ b,xs →
  maybe′
    (_=<<_ (return ∘ (swaps (proj₂ b,xs))))
    (return (♀ , ♂))
    (split♂ ♂ (proj₁ b,xs))

Population : ∀ inp out n → Set
Population inp out n = Vec (Term inp out) (2 + n)

module Initialization
  (match : ∀ w out → Dec (∃ λ d → out ≡ pre w d))
  where

  toMaybe : ∀ {w inp out} →
    Term inp out →
    Dec (∃ λ d → out ≡ pre w d) →
    Maybe (∃ λ d → Term inp d)
  toMaybe {w = w} ws (no _) = nothing
  toMaybe {w = w} ws (yes (_ , p))
    rewrite p = just (_ , w ∷ ws)

  enum-inp : ∀ (n : ℕ) inp → List Word → List (∃ λ out → Term inp out)
  enum-inp zero inp ws = gfilter (λ w → toMaybe [] (match w inp)) ws
  enum-inp (suc n) A ws
    with enum-inp n A ws
  ... | ih = concat (map (λ out,t → gfilter (λ w →
    toMaybe (proj₂ out,t) (match w (proj₁ out,t))
      ) ws) ih) l++ ih

  filter-out : ∀ {inp} out → List (∃ (Term inp)) → List (Term inp out)
  filter-out out [] = []
  filter-out out ((out' , x) ∷ xs)
    with out' ≟ out
  ... | no p = filter-out out xs
  ... | yes p rewrite p = x ∷ filter-out out xs

  init : ∀ (n : ℕ) inp out → List Word → List (Term inp out)
  init n inp out ws = filter-out out (enum-inp n inp ws)

module Evolution {inp out} (score : Term inp out → ℕ) where

  _≥_ : ℕ → ℕ → Bool
  zero ≥ zero = true
  zero ≥ (suc n) = false
  (suc m) ≥ zero = true
  (suc m) ≥ (suc n) = m ≥ n

  select : ∀ {n} →
    Population inp out n → Rand (Term inp out)
  select {n = n} xss =
    rand >>= λ ii →
    rand >>= λ jj →
    let ♀ = lookup (ii mod (2 + n)) xss
        ♂ = lookup (jj mod (2 + n)) xss
    in return $
      if score ♀ ≥ score ♂
      then ♀ else ♂

  breed2 : ∀ {n} →
    Population inp out n →
    Rand (Term inp out × Term inp out)
  breed2 xss =
    select xss >>= λ ♀ →
    select xss >>= λ ♂ →
    crossover ♀ ♂

  breedN : ∀ {m} → (n : ℕ) →
    Population inp out m →
    Rand (Vec (Term inp out) n)
  breedN zero xss = return []
  breedN (suc n) xss =
    breed2 xss >>= λ offspring →
    breedN n xss >>= λ ih →
    return (proj₁ offspring ∷ ih)

  evolve1 : ∀ {n} →
    Population inp out n → Rand (Population inp out n)
  evolve1 xss = breedN _ xss

  evolveN : ∀ {n} → (gens : ℕ) →
    Population inp out n → Rand (Population inp out n)
  evolveN zero xss = return xss
  evolveN (suc gens) xss =
    evolveN gens xss >>= evolve1

  evolve : ∀ {n} → (seed gens : ℕ) →
    Population inp out n → Population inp out n
  evolve seed gens xss =
    runRand (evolveN gens xss) seed

max_stars_repo_name: larrytheliquid/dtgp

max_issues_repo_name: larrytheliquid/dtgp

max_forks_repo_name: larrytheliquid/dtgp


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Hash
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle sha256 sha256-cr
open import LibraBFT.Concrete.System.Parameters
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK

-- This module defines an abstract system state given a reachable
-- concrete system state.

-- An implementation must prove that, if one of its handlers sends a
-- message that contains a vote and is signed by a public key pk, then
-- either the vote's author is the peer executing the handler, the
-- epochId is in range, the peer is a member of the epoch, and its key
-- in that epoch is pk; or, a message with the same signature has been
-- sent before.  This is represented by StepPeerState-AllValidParts.
module LibraBFT.Concrete.System (sps-corr : StepPeerState-AllValidParts) where

 -- Bring in 'unwind', 'ext-unforgeability' and friends
 open Structural sps-corr

 -- TODO-1: refactor this somewhere else?  Maybe something like
 -- LibraBFT.Impl.Consensus.Types.Properties?
 sameHonestSig⇒sameVoteData : ∀ {v1 v2 : Vote} {pk}
                            → Meta-Honest-PK pk
                            → WithVerSig pk v1
                            → WithVerSig pk v2
                            → v1 ^∙ vSignature ≡ v2 ^∙ vSignature
                            → NonInjective-≡ sha256 ⊎ v2 ^∙ vVoteData ≡ v1 ^∙ vVoteData
 sameHonestSig⇒sameVoteData {v1} {v2} hpk wvs1 wvs2 refl
    with verify-bs-inj (verified wvs1) (verified wvs2)
      -- The signable fields of the votes must be the same (we do not model signature collisions)
 ...| bs≡
      -- Therefore the LedgerInfo is the same for the new vote as for the previous vote
      = sym <⊎$> (hashVote-inj1 {v1} {v2} (sameBS⇒sameHash bs≡))

 honestVoteProps : ∀ {e st} → ReachableSystemState {e} st → ∀ {pk nm v sender}
                    → Meta-Honest-PK pk
                    → v ⊂Msg nm
                    → (sender , nm) ∈ msgPool st
                    → WithVerSig pk v
                    → NonInjective-≡ sha256 ⊎ v ^∙ vEpoch < e
 honestVoteProps r hpk v⊂m m∈pool ver
   with honestPartValid r hpk v⊂m m∈pool ver
 ...| msg , valid
   =  ⊎-map id (λ { refl → vp-epoch valid })
               (sameHonestSig⇒sameVoteData hpk ver (msgSigned msg)
                                           (sym (msgSameSig msg)))

 -- We are now ready to define an 'IntermediateSystemState' view for a concrete
 -- reachable state.  We will do so by fixing an epoch that exists in
 -- the system, which will enable us to define the abstract
 -- properties. The culminaton of this 'PerEpoch' module is seen in
 -- the 'IntSystemState' "function" at the bottom, which probably the
 -- best place to start uynderstanding this.  Longer term, we will
 -- also need higher-level, cross-epoch properties.
 module PerState {e}(st : SystemState e)(r : ReachableSystemState st) where

  -- TODO-3: Remove this postulate when we are satisfied with the
  -- "hash-collision-tracking" solution. For example, when proving voo
  -- (in LibraBFT.LibraBFT.Concrete.Properties.VotesOnce), we
  -- currently use this postulate to eliminate the possibility of two
  -- votes that have the same signature but different VoteData
  -- whenever we use sameHonestSig⇒sameVoteData.  To eliminate the
  -- postulate, we need to refine the properties we prove to enable
  -- the possibility of a hash collision, in which case the required
  -- property might not hold.  However, it is not sufficient to simply
  -- prove that a hash collision *exists* (which is obvious,
  -- regardless of the LibraBFT implementation).  Rather, we
  -- ultimately need to produce a specific hash collision and relate
  -- it to the data in the system, so that we can prove that the
  -- desired properties hold *unless* an actual hash collision is
  -- found by the implementation given the data in the system.  In
  -- the meantime, we simply require that the collision identifies a
  -- reachable state; later "collision tracking" will require proof
  -- that the colliding values actually exist in that state.
  postulate  -- temporary
    meta-sha256-cr : ¬ (NonInjective-≡ sha256)

  module PerEpoch (eid : Fin e) where
   𝓔 : EpochConfig
   𝓔 = EC-lookup (availEpochs st) eid
   open import LibraBFT.Abstract.Abstract     UID _≟UID_ NodeId 𝓔 (ConcreteVoteEvidence 𝓔) as Abs hiding (qcVotes; Vote)
   open import LibraBFT.Concrete.Intermediate                   𝓔 (ConcreteVoteEvidence 𝓔)
   open import LibraBFT.Concrete.Records                        𝓔

   -- * Auxiliary definitions;
   -- Here we capture the idea that there exists a vote message that
   -- witnesses the existence of a given Abs.Vote
   record ∃VoteMsgFor (v : Abs.Vote) : Set where
     constructor mk∃VoteMsgFor
     field
       -- A message that was actually sent
       nm            : NetworkMsg
       cv            : Vote
       cv∈nm         : cv ⊂Msg nm
       -- And contained a valid vote that, once abstracted, yeilds v.
       vmsgMember    : EpochConfig.Member 𝓔
       vmsgSigned    : WithVerSig (getPubKey 𝓔 vmsgMember) cv
       vmsg≈v        : α-ValidVote 𝓔 cv vmsgMember ≡ v
       vmsgEpoch     : cv ^∙ vEpoch ≡ epochId 𝓔
   open ∃VoteMsgFor public

   record ∃VoteMsgSentFor (sm : SentMessages)(v : Abs.Vote) : Set where
     constructor mk∃VoteMsgSentFor
     field
       vmFor        : ∃VoteMsgFor v
       vmSender     : NodeId
       nmSentByAuth : (vmSender , (nm vmFor)) ∈ sm
   open ∃VoteMsgSentFor public

   ∃VoteMsgSentFor-stable : ∀ {e e'} {pre : SystemState e} {post : SystemState e'} {v}
                          → Step pre post
                          → ∃VoteMsgSentFor (msgPool pre) v
                          → ∃VoteMsgSentFor (msgPool post) v
   ∃VoteMsgSentFor-stable theStep (mk∃VoteMsgSentFor sndr vmFor sba) =
                                   mk∃VoteMsgSentFor sndr vmFor (msgs-stable theStep sba)

   record ∃VoteMsgInFor (outs : List NetworkMsg)(v : Abs.Vote) : Set where
     constructor mk∃VoteMsgInFor
     field
       vmFor    : ∃VoteMsgFor v
       nmInOuts : nm vmFor ∈ outs
   open ∃VoteMsgInFor public

   ∈QC⇒sent : ∀{e} {st : SystemState e} {q α}
            → Abs.Q q α-Sent (msgPool st)
            → Meta-Honest-Member α
            → (vα : α Abs.∈QC q)
            → ∃VoteMsgSentFor (msgPool st) (Abs.∈QC-Vote q vα)
   ∈QC⇒sent {e} {st} {α = α} vsent@(ws {sender} {nm} e≡ nm∈st (qc∈NM {cqc} {q} .{nm} valid cqc∈nm q≡)) ha va
     with All-reduce⁻ {vdq = Any-lookup va} (α-Vote cqc valid) All-self
                      (subst (Any-lookup va ∈_) (cong Abs.qVotes q≡) (Any-lookup-correctP va))
   ...| as , as∈cqc , α≡
     with  α-Vote-evidence cqc valid  as∈cqc | inspect
          (α-Vote-evidence cqc valid) as∈cqc
   ...| ev | [ refl ]
      with vote∈qc {vs = as} as∈cqc refl cqc∈nm
   ...| v∈nm =
        mk∃VoteMsgSentFor
                 (mk∃VoteMsgFor nm (₋cveVote ev) v∈nm
                                (₋ivvMember (₋cveIsValidVote ev))
                                (₋ivvSigned (₋cveIsValidVote ev)) (sym α≡)
                                (₋ivvEpoch (₋cveIsValidVote ev)))
                 sender
                 nm∈st

   -- Finally, we can define the abstract system state corresponding to the concrete state st
   IntSystemState : IntermediateSystemState ℓ0
   IntSystemState = record
     { InSys           = λ { r → r α-Sent (msgPool st) }
     ; HasBeenSent     = λ { v → ∃VoteMsgSentFor (msgPool st) v }
     ; ∈QC⇒HasBeenSent = ∈QC⇒sent {st = st}
     }

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
-- {-# OPTIONS -v 20 #-}
-- {-# OPTIONS -v tc.polarity:30 #-}
-- {-# OPTIONS -v tc.decl:30 #-}
-- {-# OPTIONS -v tc.term:30 #-}
-- {-# OPTIONS -v tc.conv.coerce:20 #-}
-- {-# OPTIONS -v tc.signature:30 #-}
-- {-# OPTIONS -v import.iface:100 #-}

module Issue1168 where

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

id : ∀{a} {A : Set a} → A → A
id {A = A} a = a

id2 : ∀{A : id Set} → id A → A
id2 x = x

plus0 : ∀ x → x + 0 ≡ x
plus0 zero = refl
plus0 (suc x) rewrite plus0 x = refl

Identity : ∀{a} {A : Set a} (f : A → A) → Set a
Identity f = ∀ x → f x ≡ x

plus-0 : Identity (_+ 0)
plus-0 = plus0

my-Fun : ∀{a b} (A : Set a) (F : A → Set b) → Set (a ⊔ b)
my-Fun A F = (x : A) → F x

syntax my-Fun A (λ x → B) = [ x ∷ A ]=> B

my-id : [ A ∷ Set ]=> [ x ∷ A ]=> A
my-id A x = x

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


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

open import Groups.Definition
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Functions.Definition
open import Rings.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.Orders.Partial.Definition {n m : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+_ _*_) where

open Ring R
open Group additiveGroup
open Setoid S
open import Groups.Orders.Partial.Definition

record PartiallyOrderedRing {p : _} {_<_ : Rel {_} {p} A} (pOrder : SetoidPartialOrder S _<_) : Set (lsuc n ⊔ m ⊔ p) where
  field
    orderRespectsAddition : {a b : A} → (a < b) → (c : A) → (a + c) < (b + c)
    orderRespectsMultiplication : {a b : A} → (0R < a) → (0R < b) → (0R < (a * b))
  open SetoidPartialOrder pOrder

toGroup : {p : _} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} → PartiallyOrderedRing pOrder → PartiallyOrderedGroup additiveGroup pOrder
PartiallyOrderedGroup.orderRespectsAddition (toGroup p) = PartiallyOrderedRing.orderRespectsAddition p


text:
data D : Set₁ where
  ⟨_⟩_ : Set → Set → D

Test : D → Set
Test ((⟨_⟩ X) _) = X

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Relation.Binary.Core

module BBHeap.Drop {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import BBHeap.Compound _≤_
open import BBHeap.Equality _≤_
open import BBHeap.Equality.Properties _≤_
open import BBHeap.Subtyping.Properties _≤_ trans≤
open import BBHeap.Perfect _≤_
open import BBHeap.Properties _≤_
open import BBHeap.Push _≤_ tot≤ trans≤
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Bound.Lower.Order.Properties _≤_ trans≤
open import Data.Empty
open import Data.Product renaming (_×_ to _∧_)
open import Data.Sum renaming (_⊎_ to _∨_)
open import Order.Total _≤_ tot≤

root : {b : Bound}{h : BBHeap b}(cₕ : Compound h) → A
root (cl {x = x} _ _) = x
root (cr {x = x} _ _) = x

mutual
  drop : {b : Bound}{h : BBHeap b}(cₕ : Compound h) → BBHeap (val (root cₕ))
  drop (cl b≤x l⋘r) = drop⋘ b≤x l⋘r
  drop (cr b≤x l⋙r) = drop⋙ b≤x l⋙r

  drop⋘ : {b : Bound}{x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x)) → l ⋘ r → BBHeap (val x)
  drop⋘ b≤x lf⋘ = leaf
  drop⋘ b≤x (ll⋘ {x = y₁} {x' = y₂} x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
      with tot≤ y₁ y₂ | lemma-drop⋘ (cl x≤y₁ l₁⋘r₁) (cl x≤y₂ l₂⋘r₂) (ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
  ... | inj₁ y₁≤y₂ | inj₁ (_ , l⋙dr) =
                     let pl'≈l' = lemma-push⋘ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁ ;
                          l'≈l = ≈left (lexy refl≤) x≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                          pl'≈l = trans≈ pl'≈l' l'≈l ;
                          pl'⋙dr = lemma≈⋙ pl'≈l l⋙dr ;
                          pl'⋙dr' = subtyping⋙r (lexy y₁≤y₂) pl'⋙dr
                     in right x≤y₁ pl'⋙dr'
  ... | inj₁ y₁≤y₂ | inj₂ dl⋘r =
                     let r≈r' = ≈left x≤y₂ (lexy y₁≤y₂) l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                          dl⋘r' = lemma⋘≈ dl⋘r r≈r'
                     in left x≤y₁ dl⋘r'
  ... | inj₂ y₂≤y₁ | inj₁ (_ , l⋙dr) =
                     let l'≈l = ≈left (lexy y₂≤y₁) x≤y₁ l₁⋘r₁  l₁⋘r₁ refl≈ refl≈ ;
                          l'⋙dr = lemma≈⋙ l'≈l l⋙dr
                     in right x≤y₂ l'⋙dr
  ... | inj₂ y₂≤y₁ | inj₂ dl⋘r =
                     let pr'≈r' = lemma-push⋘ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂ ;
                          r'≈pr' = sym≈ pr'≈r' ;
                          r≈r' = ≈left x≤y₂ (lexy refl≤) l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                          r≈pr' = trans≈ r≈r' r'≈pr' ;
                          dl⋘pr' = lemma⋘≈ dl⋘r r≈pr' ;
                          dl'⋘pr' = subtyping⋘l (lexy y₂≤y₁) dl⋘pr'
                     in left x≤y₂ dl'⋘pr'
  drop⋘ b≤x (lr⋘ {x = y₁} {x' = y₂} x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₁ y₂ | lemma-drop⋘ (cr x≤y₁ l₁⋙r₁) (cl x≤y₂ l₂⋘r₂) (lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₁≤y₂ | inj₂ dl⋘r =
                     let r≈r' = ≈left x≤y₂ (lexy y₁≤y₂) l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                          dl⋘r' = lemma⋘≈ dl⋘r r≈r'
                     in left x≤y₁ dl⋘r'
  ... | inj₂ y₂≤y₁ | inj₂ dl⋘r =
                     let pr'≈r' = lemma-push⋘ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂ ;
                          r'≈pr' = sym≈ pr'≈r' ;
                          r≈r' = ≈left x≤y₂ (lexy refl≤) l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                          r≈pr' = trans≈ r≈r' r'≈pr' ;
                          dl⋘pr' = lemma⋘≈ dl⋘r r≈pr' ;
                          dl'⋘pr' = subtyping⋘l (lexy y₂≤y₁) dl⋘pr'
                     in left x≤y₂ dl'⋘pr'

  drop⋙ : {b : Bound}{x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x)) → l ⋙ r → BBHeap (val x)
  drop⋙ b≤x (⋙lf x≤y) = left x≤y lf⋘
  drop⋙ b≤x (⋙rl {x = y₁} {x' = y₂} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
      with tot≤ y₁ y₂ | lemma-drop⋙ (cl x≤y₁ l₁⋘r₁) (cl x≤y₂ l₂⋘r₂) (⋙rl x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
  ... | inj₁ y₁≤y₂ | inj₁ (_ , dl⋘r) =
                       let r≈r' = ≈left x≤y₂ (lexy y₁≤y₂) l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                            dl⋘r' = lemma⋘≈ dl⋘r r≈r'
                       in left x≤y₁ dl⋘r'
  ... | inj₁ y₁≤y₂ | inj₂ l⋙dr =
                       let l'≈l = ≈left (lexy refl≤) x≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                            pl'≈l' = lemma-push⋘ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁ ;
                            pl'≈l = trans≈ pl'≈l' l'≈l ;
                            pl'⋙dr = lemma≈⋙ pl'≈l l⋙dr ;
                            pl'⋙dr' = subtyping⋙r (lexy y₁≤y₂) pl'⋙dr
                       in right x≤y₁ pl'⋙dr'
  ... | inj₂ y₂≤y₁ | inj₁ (_ , dl⋘r) =
                       let pr'≈r' = lemma-push⋘ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂ ;
                            r'≈r = ≈left (lexy refl≤) x≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                            pr'≈r = trans≈ pr'≈r' r'≈r ;
                            r≈pr' = sym≈ pr'≈r ;
                            dl⋘pr' = lemma⋘≈ dl⋘r r≈pr' ;
                            dl'⋘pr' = subtyping⋘l (lexy y₂≤y₁) dl⋘pr'
                       in left x≤y₂ dl'⋘pr'
  ... | inj₂ y₂≤y₁ | inj₂ l⋙dr =
                       let l'≈l = ≈left (lexy y₂≤y₁) x≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                            l'⋙dr = lemma≈⋙ l'≈l l⋙dr
                       in right x≤y₂ l'⋙dr
  drop⋙ b≤x (⋙rr {x = y₁} {x' = y₂} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
      with tot≤ y₁ y₂ | lemma-drop⋙ (cl x≤y₁ l₁⋘r₁) (cr x≤y₂ l₂⋙r₂) (⋙rr x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₁≤y₂ | inj₂ l⋙dr =
                       let l'≈l = ≈left (lexy refl≤) x≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                            pl'≈l' = lemma-push⋘ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁ ;
                            pl'≈l = trans≈ pl'≈l' l'≈l ;
                            pl'⋙dr = lemma≈⋙ pl'≈l l⋙dr ;
                            pl'⋙dr' = subtyping⋙r (lexy y₁≤y₂) pl'⋙dr
                       in right x≤y₁ pl'⋙dr'
  ... | inj₂ y₂≤y₁ | inj₂ l⋙dr =
                       let l'≈l = ≈left (lexy y₂≤y₁) x≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                            l'⋙dr = lemma≈⋙ l'≈l l⋙dr
                       in right x≤y₂ l'⋙dr

  lemma-drop⋘ : {b : Bound}{l r : BBHeap b}(cₗ : Compound l)(cᵣ : Compound r) → l ⋘ r → l ≃ r ∧ l ⋙ drop cᵣ ∨ drop cₗ ⋘ r
  lemma-drop⋘ (cl y≤y₁ lf⋘) (cl y≤y₂ lf⋘) (ll⋘ .y≤y₁ .y≤y₂ .lf⋘ .lf⋘ ≃lf ≃lf) = inj₁ (≃nd y≤y₁ y≤y₂ lf⋘ lf⋘ ≃lf ≃lf ≃lf , ⋙lf y≤y₁)
  lemma-drop⋘ (cl y≤y₁ (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cl y≤y₂ lf⋘) (ll⋘ .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) .lf⋘ _ ())
  lemma-drop⋘ (cl y≤y₁ (ll⋘ {x = y₃} {x' = y₄} y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cl y≤y₂ (ll⋘ {x = y₅} {x' = y₆} y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆)) (ll⋘ {x = y₁} .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) .(ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆) l₂≃r₂ r₁≃l₂)
      with tot≤ y₃ y₄ | tot≤ y₅ y₆ | lemma-drop⋘ (cl y₁≤y₃ l₃⋘r₃) (cl y₁≤y₄ l₄⋘r₄) (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) | lemma-drop⋘ (cl y₂≤y₅ l₅⋘r₅) (cl y₂≤y₆ l₆⋘r₆) (ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆)
  ... | _ | inj₁ y₅≤y₆ | inj₁ (l₁≃r₁ , _) | inj₁ (_ , l₂⋙dr₂) =
                       let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            l₁≃l₂ = trans≃ l₁≃r₁ r₁≃l₂ ;
                            pl₂'≈l₂' = lemma-push⋘ (lexy y₅≤y₆) (lexy refl≤) l₅⋘r₅ ;
                            l₂'≈l₂ = ≈left (lexy refl≤) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                            pl₂'≈l₂ = trans≈ pl₂'≈l₂' l₂'≈l₂ ;
                            pl₂'⋙dr₂ = lemma≈⋙ pl₂'≈l₂ l₂⋙dr₂ ;
                            pl₂'⋙dr₂' = subtyping⋙r (lexy y₅≤y₆) pl₂'⋙dr₂ ;
                            l₂≈pl₂' = sym≈ pl₂'≈l₂ ;
                            l₁≃pl₂' = lemma≃≈ l₁≃l₂ l₂≈pl₂'
                       in inj₁ (≃nd y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ , ⋙rr y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ pl₂'⋙dr₂' l₁≃pl₂')
  ... | _ | inj₂ y₆≤y₅ | inj₁ (l₁≃r₁ , _) | inj₁ (_ , l₂⋙dr₂) =
                       let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            l₁≃l₂ = trans≃ l₁≃r₁ r₁≃l₂ ;
                            l₂'≈l₂ = ≈left (lexy y₆≤y₅) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                            l₂'⋙dr₂ = lemma≈⋙ l₂'≈l₂ l₂⋙dr₂ ;
                            l₂≈l₂' = sym≈ l₂'≈l₂ ;
                            l₁≃l₂' = lemma≃≈ l₁≃l₂ l₂≈l₂'
                       in inj₁ (≃nd y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ , ⋙rr y≤y₁ y₂≤y₆ l₁⋘r₁ l₁≃r₁ l₂'⋙dr₂ l₁≃l₂')
  ... | inj₁ y₃≤y₄ | _ | inj₂ dl₁⋘r₁ | _ =
                       let r₁≈r₁' = ≈left y₁≤y₄ (lexy y₃≤y₄) l₄⋘r₄ l₄⋘r₄ refl≈ refl≈ ;
                            dl₁⋘r₁' = lemma⋘≈ dl₁⋘r₁ r₁≈r₁' ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            r₁'≈r₁ = sym≈ r₁≈r₁' ;
                            r₁'≃l₂ = lemma≈≃ r₁'≈r₁ r₁≃l₂
                       in inj₂ (ll⋘ y₁≤y₃ y≤y₂ dl₁⋘r₁' l₂⋘r₂ l₂≃r₂ r₁'≃l₂)
  ... | inj₂ y₄≤y₃ | _ | inj₂ dl₁⋘r₁ | _ =
                       let r₁≈r₁' = ≈left y₁≤y₄ (lexy refl≤) l₄⋘r₄ l₄⋘r₄ refl≈ refl≈ ;
                            pr₁'≈r₁' = lemma-push⋘ (lexy y₄≤y₃) (lexy refl≤) l₄⋘r₄ ;
                            dl₁⋘r₁' = lemma⋘≈ dl₁⋘r₁ r₁≈r₁' ;
                            r₁'≈pr₁' = sym≈ pr₁'≈r₁' ;
                            r₁≈pr₁' = trans≈ r₁≈r₁' r₁'≈pr₁' ;
                            dl₁⋘pr₁' = lemma⋘≈ dl₁⋘r₁ r₁≈pr₁' ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            dl₁'⋘pr₁' = subtyping⋘l (lexy y₄≤y₃) dl₁⋘pr₁' ;
                            r₁'≈r₁ = sym≈ r₁≈r₁' ;
                            r₁'≃l₂ = lemma≈≃ r₁'≈r₁ r₁≃l₂ ;
                            pr₁'≃l₂ = lemma≈≃ pr₁'≈r₁' r₁'≃l₂
                       in inj₂ (ll⋘ y₁≤y₄ y≤y₂ dl₁'⋘pr₁' l₂⋘r₂ l₂≃r₂ pr₁'≃l₂)
  ... | _ | _ | inj₁ (l₁≃r₁ , l₁⋙dr₁) | inj₂ dl₂⋘r₂
      with lemma-drop-⊥ y₂≤y₅ l₅⋘r₅ (lemma-⋘-≃ dl₂⋘r₂ (sym≃ l₂≃r₂))
  ... | ()
  lemma-drop⋘ (cl y≤y₁ (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cl y≤y₂ (lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆)) (ll⋘ .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) .(lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆) _ ())
  lemma-drop⋘ (cl y≤y₁ (lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄)) (cl y≤y₂ lf⋘) (ll⋘ .y≤y₁ .y≤y₂ .(lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄) .lf⋘ _ ())
  lemma-drop⋘ (cl y≤y₁ (lr⋘ {x = y₃} {x' = y₄} y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄)) (cl y≤y₂ (ll⋘ {x = y₅} {x' = y₆} y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆)) (ll⋘ .y≤y₁ .y≤y₂ .(lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄) .(ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆) l₂≃r₂ r₁≃l₂)
      with tot≤ y₃ y₄ | tot≤ y₅ y₆ | lemma-drop⋘ (cr y₁≤y₃ l₃⋙r₃) (cl y₁≤y₄ l₄⋘r₄) (lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄) | lemma-drop⋘ (cl y₂≤y₅ l₅⋘r₅) (cl y₂≤y₆ l₆⋘r₆) (ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆)
  ... | _ | inj₁ y₅≤y₆ | inj₁ (l₁≃r₁ , _) | inj₁ (_ , l₂⋙dr₂) =
                       let l₁⋘r₁ = lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄ ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            l₁≃l₂ = trans≃ l₁≃r₁ r₁≃l₂ ;
                            pl₂'≈l₂' = lemma-push⋘ (lexy y₅≤y₆) (lexy refl≤) l₅⋘r₅ ;
                            l₂'≈l₂ = ≈left (lexy refl≤) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                            pl₂'≈l₂ = trans≈ pl₂'≈l₂' l₂'≈l₂ ;
                            pl₂'⋙dr₂ = lemma≈⋙ pl₂'≈l₂ l₂⋙dr₂ ;
                            pl₂'⋙dr₂' = subtyping⋙r (lexy y₅≤y₆) pl₂'⋙dr₂ ;
                            l₂≈pl₂' = sym≈ pl₂'≈l₂ ;
                            l₁≃pl₂' = lemma≃≈ l₁≃l₂ l₂≈pl₂'
                       in inj₁ (≃nd y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ , ⋙rr y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ pl₂'⋙dr₂' l₁≃pl₂')
  ... | _ | inj₂ y₆≤y₅ | inj₁ (l₁≃r₁ , _) | inj₁ (_ , l₂⋙dr₂) =
                       let l₁⋘r₁ = lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄ ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            l₁≃l₂ = trans≃ l₁≃r₁ r₁≃l₂ ;
                            l₂'≈l₂ = ≈left (lexy y₆≤y₅) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                            l₂'⋙dr₂ = lemma≈⋙ l₂'≈l₂ l₂⋙dr₂ ;
                            l₂≈l₂' = sym≈ l₂'≈l₂ ;
                            l₁≃l₂' = lemma≃≈ l₁≃l₂ l₂≈l₂'
                       in inj₁ (≃nd y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ , ⋙rr y≤y₁ y₂≤y₆ l₁⋘r₁ l₁≃r₁ l₂'⋙dr₂ l₁≃l₂')
  ... | inj₁ y₃≤y₄ | _ | inj₂ dl₁⋘r₁ | _ =
                       let r₁≈r₁' = ≈left y₁≤y₄ (lexy y₃≤y₄) l₄⋘r₄ l₄⋘r₄ refl≈ refl≈ ;
                            dl₁⋘r₁' = lemma⋘≈ dl₁⋘r₁ r₁≈r₁' ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            r₁'≈r₁ = sym≈ r₁≈r₁' ;
                            r₁'≃l₂ = lemma≈≃ r₁'≈r₁ r₁≃l₂
                       in inj₂ (ll⋘ y₁≤y₃ y≤y₂ dl₁⋘r₁' l₂⋘r₂ l₂≃r₂ r₁'≃l₂)
  ... | inj₂ y₄≤y₃ | _ | inj₂ dl₁⋘r₁ | _ =
                       let r₁≈r₁' = ≈left y₁≤y₄ (lexy refl≤) l₄⋘r₄ l₄⋘r₄ refl≈ refl≈ ;
                            pr₁'≈r₁' = lemma-push⋘ (lexy y₄≤y₃) (lexy refl≤) l₄⋘r₄ ;
                            dl₁⋘r₁' = lemma⋘≈ dl₁⋘r₁ r₁≈r₁' ;
                            r₁'≈pr₁' = sym≈ pr₁'≈r₁' ;
                            r₁≈pr₁' = trans≈ r₁≈r₁' r₁'≈pr₁' ;
                            dl₁⋘pr₁' = lemma⋘≈ dl₁⋘r₁ r₁≈pr₁' ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            dl₁'⋘pr₁' = subtyping⋘l (lexy y₄≤y₃) dl₁⋘pr₁' ;
                            r₁'≈r₁ = sym≈ r₁≈r₁' ;
                            r₁'≃l₂ = lemma≈≃ r₁'≈r₁ r₁≃l₂ ;
                            pr₁'≃l₂ = lemma≈≃ pr₁'≈r₁' r₁'≃l₂
                       in inj₂ (ll⋘ y₁≤y₄ y≤y₂ dl₁'⋘pr₁' l₂⋘r₂ l₂≃r₂ pr₁'≃l₂)
  ... | _ | _ | inj₁ (l₁≃r₁ , l₁⋙dr₁) | inj₂ dl₂⋘r₂
      with lemma-drop-⊥ y₂≤y₅ l₅⋘r₅ (lemma-⋘-≃ dl₂⋘r₂ (sym≃ l₂≃r₂))
  ... | ()
  lemma-drop⋘ (cl y≤y₁ (lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄)) (cl y≤y₂ (lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆)) (ll⋘ .y≤y₁ .y≤y₂ .(lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄) .(lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆) () _)
  lemma-drop⋘ (cr y≤y₁ (⋙lf y₁≤y₃)) (cl y≤y₂ lf⋘) (lr⋘ .y≤y₁ .y≤y₂ .(⋙lf y₁≤y₃) .lf⋘ ≃lf (⋗lf .y₁≤y₃)) = inj₂ (ll⋘ y₁≤y₃ y≤y₂ lf⋘ lf⋘ ≃lf ≃lf)
  lemma-drop⋘ (cr y≤y₁ (⋙lf y₁≤y₃)) (cl y≤y₂ (ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆)) (lr⋘ .y≤y₁ .y≤y₂ .(⋙lf y₁≤y₃) .(ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆) _ (⋗nd .y₁≤y₃ .y₂≤y₅ .lf⋘ .l₅⋘r₅ _ _ ()))
  lemma-drop⋘ (cr y≤y₁ (⋙lf y₁≤y₃)) (cl y≤y₂ (lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆)) (lr⋘ .y≤y₁ .y≤y₂ .(⋙lf y₁≤y₃) .(lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆) () _)
  lemma-drop⋘ (cr y≤y₁ (⋙rl {x = y₃} {x' = y₄} y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₃≃r₃ l₄⋘r₄ l₃⋗r₄)) (cl y≤y₂ l₂⋘r₂) (lr⋘ .y≤y₁ .y≤y₂ .(⋙rl y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₃≃r₃ l₄⋘r₄ l₃⋗r₄) .l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₃ y₄ | lemma-drop⋙ (cl y₁≤y₃ l₃⋘r₃) (cl y₁≤y₄ l₄⋘r₄) (⋙rl y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₃≃r₃ l₄⋘r₄ l₃⋗r₄)
  ... | inj₁ y₃≤y₄ | inj₁ (l₁⋗r₁ , dl₁⋘r₁) =
                       let r₁≈r₁' = ≈left y₁≤y₄ (lexy y₃≤y₄) l₄⋘r₄ l₄⋘r₄ refl≈ refl≈ ;
                            dl₁⋘r₁' = lemma⋘≈ dl₁⋘r₁ r₁≈r₁' ;
                            r₁'≈r₁ = sym≈ r₁≈r₁' ;
                            r₁≃l₂ = lemma⋗⋗' l₁⋗r₁ l₁⋗l₂ ;
                            r₁'≃l₂ = lemma≈≃ r₁'≈r₁ r₁≃l₂
                       in inj₂ (ll⋘ y₁≤y₃ y≤y₂ dl₁⋘r₁' l₂⋘r₂ l₂≃r₂ r₁'≃l₂)
  ... | inj₁ y₃≤y₄ | inj₂ l₁⋙dr₁ =
                       let l₁'≈l₁ = ≈left (lexy refl≤) y₁≤y₃ l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            pl₁'≈l₁' = lemma-push⋘ (lexy y₃≤y₄) (lexy refl≤) l₃⋘r₃ ;
                            pl₁'≈l₁ = trans≈ pl₁'≈l₁' l₁'≈l₁ ;
                            pl₁'⋙dr = lemma≈⋙ pl₁'≈l₁ l₁⋙dr₁ ;
                            pl₁'⋙dr₁' = subtyping⋙r (lexy y₃≤y₄) pl₁'⋙dr ;
                            pl₁'⋗l₂ = lemma≈⋗ pl₁'≈l₁ l₁⋗l₂
                       in inj₂ (lr⋘ y₁≤y₃ y≤y₂ pl₁'⋙dr₁' l₂⋘r₂ l₂≃r₂ pl₁'⋗l₂)
  ... | inj₂ y₄≤y₃ | inj₁ (l₁⋗r₁ , dl₁⋘r₁) =
                       let r₁'≈r₁ = ≈left (lexy refl≤) y₁≤y₄ l₄⋘r₄ l₄⋘r₄ refl≈ refl≈ ;
                            pr₁'≈r₁' = lemma-push⋘ (lexy y₄≤y₃) (lexy refl≤) l₄⋘r₄ ;
                            r₁'≈pr₁' = sym≈ pr₁'≈r₁' ;
                            pr₁'≈r₁ = trans≈ pr₁'≈r₁' r₁'≈r₁ ;
                            r₁≈pr₁' = sym≈ pr₁'≈r₁ ;
                            dl₁⋘pr₁' = lemma⋘≈ dl₁⋘r₁ r₁≈pr₁' ;
                            dl₁'⋘pr₁' = subtyping⋘l (lexy y₄≤y₃) dl₁⋘pr₁' ;
                            r₁≃l₂ = lemma⋗⋗' l₁⋗r₁ l₁⋗l₂ ;
                            pr₁'≃l₂ = lemma≈≃ pr₁'≈r₁ r₁≃l₂
                       in inj₂ (ll⋘ y₁≤y₄ y≤y₂ dl₁'⋘pr₁' l₂⋘r₂ l₂≃r₂ pr₁'≃l₂)
  ... | inj₂ y₄≤y₃ | inj₂ l₁⋙dr₁ =
                       let l₁'≈l₁ = ≈left (lexy y₄≤y₃) y₁≤y₃ l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            l₁'⋙dr₁ = lemma≈⋙ l₁'≈l₁ l₁⋙dr₁ ;
                            l₁'⋗l₂ = lemma≈⋗ l₁'≈l₁ l₁⋗l₂
                       in inj₂ (lr⋘ y₁≤y₄ y≤y₂ l₁'⋙dr₁ l₂⋘r₂ l₂≃r₂ l₁'⋗l₂)
  lemma-drop⋘ (cr y≤y₁ (⋙rr {x = y₃} {x' = y₄} y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₃≃r₃ l₄⋙r₄ l₃≃l₄)) (cl y≤y₂ l₂⋘r₂) (lr⋘ .y≤y₁ .y≤y₂ .(⋙rr y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₃≃r₃ l₄⋙r₄ l₃≃l₄) .l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₃ y₄ | lemma-drop⋙ (cl y₁≤y₃ l₃⋘r₃) (cr y₁≤y₄ l₄⋙r₄) (⋙rr y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₃≃r₃ l₄⋙r₄ l₃≃l₄)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₃≤y₄ | inj₂ l₁⋙dr₁ =
                       let l₁'≈l₁ = ≈left (lexy refl≤) y₁≤y₃ l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            pl₁'≈l₁' = lemma-push⋘ (lexy y₃≤y₄) (lexy refl≤) l₃⋘r₃ ;
                            pl₁'≈l₁ = trans≈ pl₁'≈l₁' l₁'≈l₁ ;
                            pl₁'⋙dr = lemma≈⋙ pl₁'≈l₁ l₁⋙dr₁ ;
                            pl₁'⋙dr₁' = subtyping⋙r (lexy y₃≤y₄) pl₁'⋙dr ;
                            pl₁'⋗l₂ = lemma≈⋗ pl₁'≈l₁ l₁⋗l₂
                       in inj₂ (lr⋘ y₁≤y₃ y≤y₂ pl₁'⋙dr₁' l₂⋘r₂ l₂≃r₂ pl₁'⋗l₂)
  ... | inj₂ y₄≤y₃ | inj₂ l₁⋙dr₁ =
                       let l₁'≈l₁ = ≈left (lexy y₄≤y₃) y₁≤y₃ l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            l₁'⋙dr₁ = lemma≈⋙ l₁'≈l₁ l₁⋙dr₁ ;
                            l₁'⋗l₂ = lemma≈⋗ l₁'≈l₁ l₁⋗l₂
                       in inj₂ (lr⋘ y₁≤y₄ y≤y₂ l₁'⋙dr₁ l₂⋘r₂ l₂≃r₂ l₁'⋗l₂)

  lemma-drop⋙ : {b : Bound}{l r : BBHeap b}(cₗ : Compound l)(cᵣ : Compound r) → l ⋙ r → l ⋗ r ∧ drop cₗ ⋘ r ∨ l ⋙ drop cᵣ
  lemma-drop⋙ (cl y≤y₁ lf⋘) (cl y≤y₂ l₂⋘r₂) (⋙rl .y≤y₁ .y≤y₂ .lf⋘ _ .l₂⋘r₂ ())
  lemma-drop⋙ (cl y≤y₁ (ll⋘ {x = y₃} {x' = y₄} y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cl y≤y₂ lf⋘) (⋙rl .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) l₁≃r₁ .lf⋘ l₁⋗r₂)
      with tot≤ y₃ y₄ | lemma-drop⋘ (cl y₁≤y₃ l₃⋘r₃) (cl y₁≤y₄ l₄⋘r₄) (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)
  ... | inj₁ y₃≤y₄ | inj₁ (_ , l₁⋙dr₁) =
                       let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                            l₁⋗l₂ = lemma⋗≃ l₁⋗r₂ ≃lf ;
                            l₁'≈l₁ = ≈left (lexy refl≤) y₁≤y₃  l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            pl₁'≈l₁' = lemma-push⋘ (lexy y₃≤y₄) (lexy refl≤) l₃⋘r₃ ;
                            pl₁'≈l₁ = trans≈ pl₁'≈l₁' l₁'≈l₁ ;
                            pl₁'⋙dr₁ = lemma≈⋙ pl₁'≈l₁ l₁⋙dr₁ ;
                            pl₁'⋙dr₁' = subtyping⋙r (lexy y₃≤y₄) pl₁'⋙dr₁ ;
                            pl₁'⋗l₂ = lemma≈⋗ pl₁'≈l₁ l₁⋗l₂
                       in inj₁ (⋗nd y≤y₁ y≤y₂ l₁⋘r₁ lf⋘ l₁≃r₁ ≃lf l₁⋗l₂ , lr⋘ y₁≤y₃ y≤y₂ pl₁'⋙dr₁' lf⋘ ≃lf pl₁'⋗l₂)
  ... | inj₂ y₄≤y₃ | inj₁ (_ , l₁⋙dr₁) =
                       let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                            l₁⋗l₂ = lemma⋗≃ l₁⋗r₂ ≃lf ;
                            l₁'≈l₁ = ≈left (lexy y₄≤y₃) y₁≤y₃ l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            l₁'⋙dr₁ = lemma≈⋙ l₁'≈l₁ l₁⋙dr₁ ;
                            l₁'⋗l₂ = lemma≈⋗ l₁'≈l₁ l₁⋗l₂
                       in inj₁ (⋗nd y≤y₁ y≤y₂ l₁⋘r₁ lf⋘ l₁≃r₁ ≃lf l₁⋗l₂ , lr⋘ y₁≤y₄ y≤y₂ l₁'⋙dr₁ lf⋘ ≃lf l₁'⋗l₂)
  ... | _ | inj₂ dl₁⋘r₁
      with lemma-drop-⊥ y₁≤y₃ l₃⋘r₃ (lemma-⋘-≃ dl₁⋘r₁ (sym≃ l₁≃r₁))
  ... | ()
  lemma-drop⋙ (cl y≤y₁ (ll⋘ {x = y₃} {x' = y₄} y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cl y≤y₂ (ll⋘ {x = y₅} {x' = y₆} y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆)) (⋙rl .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) l₁≃r₁ .(ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆) l₁⋗r₂)
      with tot≤ y₃ y₄ | tot≤ y₅ y₆ | lemma-drop⋘ (cl y₂≤y₅ l₅⋘r₅) (cl y₂≤y₆ l₆⋘r₆) (ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆) | lemma-drop⋘ (cl y₁≤y₃ l₃⋘r₃) (cl y₁≤y₄ l₄⋘r₄)  (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)
  ... | inj₁ y₃≤y₄ | _ | inj₁ (l₂≃r₂ , _) | inj₁ (_ , l₁⋙dr₁) =
                       let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            r₂≃l₂ = sym≃ l₂≃r₂ ;
                            l₁⋗l₂ = lemma⋗≃ l₁⋗r₂ r₂≃l₂ ;
                            l₁'≈l₁ = ≈left (lexy refl≤) y₁≤y₃  l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            pl₁'≈l₁' = lemma-push⋘ (lexy y₃≤y₄) (lexy refl≤) l₃⋘r₃ ;
                            pl₁'≈l₁ = trans≈ pl₁'≈l₁' l₁'≈l₁ ;
                            pl₁'⋙dr₁ = lemma≈⋙ pl₁'≈l₁ l₁⋙dr₁ ;
                            pl₁'⋙dr₁' = subtyping⋙r (lexy y₃≤y₄) pl₁'⋙dr₁ ;
                            pl₁'⋗l₂ = lemma≈⋗ pl₁'≈l₁ l₁⋗l₂
                       in inj₁ (⋗nd y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂ , lr⋘ y₁≤y₃ y≤y₂ pl₁'⋙dr₁' l₂⋘r₂ l₂≃r₂ pl₁'⋗l₂)
  ... | inj₂ y₄≤y₃ | _ | inj₁ (l₂≃r₂ , _) | inj₁ (_ , l₁⋙dr₁) =
                       let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                            l₂⋘r₂ = ll⋘ y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₆⋘r₆ l₆≃r₆ r₅≃l₆ ;
                            r₂≃l₂ = sym≃ l₂≃r₂ ;
                            l₁⋗l₂ = lemma⋗≃ l₁⋗r₂ r₂≃l₂ ;
                            l₁'≈l₁ = ≈left (lexy y₄≤y₃) y₁≤y₃ l₃⋘r₃ l₃⋘r₃ refl≈ refl≈ ;
                            l₁'⋙dr₁ = lemma≈⋙ l₁'≈l₁ l₁⋙dr₁ ;
                            l₁'⋗l₂ = lemma≈⋗ l₁'≈l₁ l₁⋗l₂
                       in inj₁ (⋗nd y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂ , lr⋘ y₁≤y₄ y≤y₂ l₁'⋙dr₁ l₂⋘r₂ l₂≃r₂ l₁'⋗l₂)
  ... | _ | inj₁ y₅≤y₆ | inj₂ dl₂⋘r₂ | _ =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              r₂≈r₂' = ≈left y₂≤y₆ (lexy y₅≤y₆) l₆⋘r₆ l₆⋘r₆ refl≈ refl≈ ;
                              dl₂⋘r₂' = lemma⋘≈ dl₂⋘r₂ r₂≈r₂' ;
                              l₁⋗r₂' = lemma⋗≈ l₁⋗r₂ r₂≈r₂'
                         in inj₂ (⋙rl y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ dl₂⋘r₂' l₁⋗r₂')
  ... | _ | inj₂ y₆≤y₅ | inj₂ dl₂⋘r₂ | _ =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              r₂≈r₂' = ≈left y₂≤y₆ (lexy refl≤) l₆⋘r₆ l₆⋘r₆ refl≈ refl≈ ;
                              pr₂'≈r₂' = lemma-push⋘ (lexy y₆≤y₅) (lexy refl≤) l₆⋘r₆ ;
                              r₂'≈pr₂' = sym≈ pr₂'≈r₂' ;
                              r₂≈pr₂' = trans≈ r₂≈r₂' r₂'≈pr₂';
                              dl₂⋘pr₂' = lemma⋘≈ dl₂⋘r₂ r₂≈pr₂' ;
                              dl₂'⋘pr₂' = subtyping⋘l (lexy y₆≤y₅) dl₂⋘pr₂' ;
                              l₁⋗pr₂' = lemma⋗≈ l₁⋗r₂ r₂≈pr₂'
                         in inj₂ (⋙rl y≤y₁ y₂≤y₆ l₁⋘r₁ l₁≃r₁ dl₂'⋘pr₂' l₁⋗pr₂')
  ... | _ | _ | _ | inj₂ dl₁⋘r₁
      with lemma-drop-⊥ y₁≤y₃ l₃⋘r₃ (lemma-⋘-≃ dl₁⋘r₁ (sym≃ l₁≃r₁))
  ... | ()
  lemma-drop⋙ (cl y≤y₁ (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cl y≤y₂ (lr⋘ {x = y₅} {x' = y₆} y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆)) (⋙rl .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) l₁≃r₁ .(lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆) l₁⋗r₂)
      with tot≤ y₅ y₆ | lemma-drop⋘ (cr y₂≤y₅ l₅⋙r₅) (cl y₂≤y₆ l₆⋘r₆) (lr⋘ y₂≤y₅ y₂≤y₆ l₅⋙r₅ l₆⋘r₆ l₆≃r₆ l₅⋗l₆)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₅≤y₆ | inj₂ dl₂⋘r₂ =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              r₂≈r₂' = ≈left y₂≤y₆ (lexy y₅≤y₆) l₆⋘r₆ l₆⋘r₆ refl≈ refl≈ ;
                              dl₂⋘r₂' = lemma⋘≈ dl₂⋘r₂ r₂≈r₂' ;
                              l₁⋗r₂' = lemma⋗≈ l₁⋗r₂ r₂≈r₂'
                         in inj₂ (⋙rl y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ dl₂⋘r₂' l₁⋗r₂')
  ... | inj₂ y₆≤y₅ | inj₂ dl₂⋘r₂ =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              r₂≈r₂' = ≈left y₂≤y₆ (lexy refl≤) l₆⋘r₆ l₆⋘r₆ refl≈ refl≈ ;
                              pr₂'≈r₂' = lemma-push⋘ (lexy y₆≤y₅) (lexy refl≤) l₆⋘r₆ ;
                              r₂'≈pr₂' = sym≈ pr₂'≈r₂' ;
                              r₂≈pr₂' = trans≈ r₂≈r₂' r₂'≈pr₂';
                              dl₂⋘pr₂' = lemma⋘≈ dl₂⋘r₂ r₂≈pr₂' ;
                              dl₂'⋘pr₂' = subtyping⋘l (lexy y₆≤y₅) dl₂⋘pr₂' ;
                              l₁⋗pr₂' = lemma⋗≈ l₁⋗r₂ r₂≈pr₂'
                         in inj₂ (⋙rl y≤y₁ y₂≤y₆ l₁⋘r₁ l₁≃r₁ dl₂'⋘pr₂' l₁⋗pr₂')
  lemma-drop⋙ (cl y≤y₁ (lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄)) (cl y≤y₂ l₂⋘r₂) (⋙rl .y≤y₁ .y≤y₂ .(lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄) () .l₂⋘r₂ _)
  lemma-drop⋙ _ _ (⋙rr _ _ lf⋘ _ (⋙lf _) ())
  lemma-drop⋙ _ _ (⋙rr _ _ lf⋘ _ (⋙rl _ _ _ _ _ _) ())
  lemma-drop⋙ _ _ (⋙rr _ _ lf⋘ _ (⋙rr _ _ _ _ _ _) ())
  lemma-drop⋙ (cl y≤y₁ (ll⋘ y₁≤y₃ y₁≤y₄ lf⋘ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cr y≤y₂ (⋙lf y₂≤y₅)) (⋙rr .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ lf⋘ l₄⋘r₄ l₄≃r₄ r₃≃l₄) l₁≃r₁ .(⋙lf y₂≤y₅) (≃nd .y₁≤y₃ .y₂≤y₅ .lf⋘ .lf⋘ ≃lf ≃lf ≃lf)) =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ lf⋘ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              l₁⋗r₂ = ⋗lf y₁≤y₃
                         in inj₂ (⋙rl y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ lf⋘ l₁⋗r₂)
  lemma-drop⋙ _ _ (⋙rr _ _ (ll⋘ y₁≤y₃ _ (ll⋘ _ _ _ _ _ _) _ _ _) _ (⋙lf y₂≤y₅) (≃nd .y₁≤y₃ .y₂≤y₅ .(ll⋘ _ _ _ _ _ _) .lf⋘ _ ≃lf ()))
  lemma-drop⋙ _ _ (⋙rr _ _ (ll⋘ y₁≤y₃ _ (lr⋘ _ _ _ _ _ _) _ _ _) _ (⋙lf y₂≤y₅) (≃nd .y₁≤y₃ .y₂≤y₅ .(lr⋘ _ _ _ _ _ _) .lf⋘ _ ≃lf ()))
  lemma-drop⋙ (cl y≤y₁ (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cr y≤y₂ (⋙rl {x = y₅} {x' = y₆} y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₅≃r₅ l₆⋘r₆ l₅⋗r₆)) (⋙rr .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) l₁≃r₁ .(⋙rl y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₅≃r₅ l₆⋘r₆ l₅⋗r₆) l₁≃l₂)
      with tot≤ y₅ y₆ | lemma-drop⋙ (cl y₂≤y₅ l₅⋘r₅) (cl y₂≤y₆ l₆⋘r₆) (⋙rl y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₅≃r₅ l₆⋘r₆ l₅⋗r₆)
  ... | inj₁ y₅≤y₆ | inj₁ (l₂⋗r₂ , dl₂⋘r₂) =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              r₂≈r₂' = ≈left y₂≤y₆ (lexy y₅≤y₆) l₆⋘r₆ l₆⋘r₆ refl≈ refl≈ ;
                              dl₂⋘r₂' = lemma⋘≈ dl₂⋘r₂ r₂≈r₂' ;
                              l₁⋗r₂ = lemma≃⋗ l₁≃l₂ l₂⋗r₂ ;
                              l₁⋗r₂' = lemma⋗≈ l₁⋗r₂ r₂≈r₂'
                         in inj₂ (⋙rl y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ dl₂⋘r₂' l₁⋗r₂')
  ... | inj₁ y₅≤y₆ | inj₂ l₂⋙dr₂ =
                        let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                             l₂'≈l₂ = ≈left (lexy refl≤) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                             pl₂'≈l₂' = lemma-push⋘ (lexy y₅≤y₆) (lexy refl≤) l₅⋘r₅ ;
                             pl₂'≈l₂ = trans≈ pl₂'≈l₂' l₂'≈l₂ ;
                             pl₂'⋙dr₂ = lemma≈⋙ pl₂'≈l₂ l₂⋙dr₂ ;
                             l₂≈pl₂' = sym≈ pl₂'≈l₂ ;
                             pl₂'⋙dr₂' = subtyping⋙r (lexy y₅≤y₆) pl₂'⋙dr₂ ;
                             l₁≃pl₂' = lemma≃≈ l₁≃l₂ l₂≈pl₂'
                        in inj₂ (⋙rr y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ pl₂'⋙dr₂' l₁≃pl₂')
  ... | inj₂ y₆≤y₅ | inj₁ (l₂⋗r₂ , dl₂⋘r₂) =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              r₂'≈r₂ = ≈left (lexy refl≤) y₂≤y₆ l₆⋘r₆ l₆⋘r₆ refl≈ refl≈ ;
                              pr₂'≈r₂' = lemma-push⋘ (lexy y₆≤y₅) (lexy refl≤) l₆⋘r₆ ;
                              pr₂'≈r₂ = trans≈ pr₂'≈r₂' r₂'≈r₂ ;
                              r₂≈pr₂' = sym≈ pr₂'≈r₂ ;
                              dl₂⋘pr₂' = lemma⋘≈ dl₂⋘r₂ r₂≈pr₂' ;
                              dl₂'⋘pr₂' = subtyping⋘l (lexy y₆≤y₅) dl₂⋘pr₂' ;
                              l₁⋗r₂ = lemma≃⋗ l₁≃l₂ l₂⋗r₂ ;
                              l₁⋗pr₂' = lemma⋗≈ l₁⋗r₂ r₂≈pr₂'
                         in inj₂ (⋙rl y≤y₁ y₂≤y₆ l₁⋘r₁ l₁≃r₁ dl₂'⋘pr₂' l₁⋗pr₂')
  ... | inj₂ y₆≤y₅ | inj₂ l₂⋙dr₂ =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              l₂'≈l₂ = ≈left (lexy y₆≤y₅) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                              l₂'⋙dr₂ = lemma≈⋙ l₂'≈l₂ l₂⋙dr₂ ;
                              l₂≈l₂' = sym≈ l₂'≈l₂ ;
                              l₁≃l₂' = lemma≃≈ l₁≃l₂ l₂≈l₂'
                         in inj₂ (⋙rr y≤y₁ y₂≤y₆ l₁⋘r₁ l₁≃r₁ l₂'⋙dr₂ l₁≃l₂')
  lemma-drop⋙ (cl y≤y₁ (ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄)) (cr y≤y₂ (⋙rr {x = y₅} {x' = y₆} y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₅≃r₅ l₆⋙r₆ l₅≃l₆)) (⋙rr .y≤y₁ .y≤y₂ .(ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄) l₁≃r₁ .(⋙rr y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₅≃r₅ l₆⋙r₆ l₅≃l₆) l₁≃l₂)
      with tot≤ y₅ y₆ | lemma-drop⋙ (cl y₂≤y₅ l₅⋘r₅) (cr y₂≤y₆ l₆⋙r₆) (⋙rr y₂≤y₅ y₂≤y₆ l₅⋘r₅ l₅≃r₅ l₆⋙r₆ l₅≃l₆)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₅≤y₆ | inj₂ l₂⋙dr₂ =
                        let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                             l₂'≈l₂ = ≈left (lexy refl≤) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                             pl₂'≈l₂' = lemma-push⋘ (lexy y₅≤y₆) (lexy refl≤) l₅⋘r₅ ;
                             pl₂'≈l₂ = trans≈ pl₂'≈l₂' l₂'≈l₂ ;
                             pl₂'⋙dr₂ = lemma≈⋙ pl₂'≈l₂ l₂⋙dr₂ ;
                             l₂≈pl₂' = sym≈ pl₂'≈l₂ ;
                             pl₂'⋙dr₂' = subtyping⋙r (lexy y₅≤y₆) pl₂'⋙dr₂ ;
                             l₁≃pl₂' = lemma≃≈ l₁≃l₂ l₂≈pl₂'
                        in inj₂ (⋙rr y≤y₁ y₂≤y₅ l₁⋘r₁ l₁≃r₁ pl₂'⋙dr₂' l₁≃pl₂')
  ... | inj₂ y₆≤y₅ | inj₂ l₂⋙dr₂ =
                         let l₁⋘r₁ = ll⋘ y₁≤y₃ y₁≤y₄ l₃⋘r₃ l₄⋘r₄ l₄≃r₄ r₃≃l₄ ;
                              l₂'≈l₂ = ≈left (lexy y₆≤y₅) y₂≤y₅ l₅⋘r₅ l₅⋘r₅ refl≈ refl≈ ;
                              l₂'⋙dr₂ = lemma≈⋙ l₂'≈l₂ l₂⋙dr₂ ;
                              l₂≈l₂' = sym≈ l₂'≈l₂ ;
                              l₁≃l₂' = lemma≃≈ l₁≃l₂ l₂≈l₂'
                         in inj₂ (⋙rr y≤y₁ y₂≤y₆ l₁⋘r₁ l₁≃r₁ l₂'⋙dr₂ l₁≃l₂')
  lemma-drop⋙ (cl y≤y₁ (lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄)) (cr y≤y₂ l₂⋙r₂) (⋙rr .y≤y₁ .y≤y₂ .(lr⋘ y₁≤y₃ y₁≤y₄ l₃⋙r₃ l₄⋘r₄ l₄≃r₄ l₃⋗l₄) () .l₂⋙r₂ _)

  lemma-drop-⊥ : {b : Bound}{x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋘r : l ⋘ r) → drop (cl b≤x l⋘r) ⋘ (left b≤x l⋘r) → ⊥
  lemma-drop-⊥ _ lf⋘ ()
  lemma-drop-⊥ b≤x (ll⋘ {x = y₁} {x' = y₂} x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂) dxlr⋘xlr
      with tot≤ y₁ y₂ | lemma-drop⋘ (cl x≤y₁ l₁⋘r₁) (cl x≤y₂ l₂⋘r₂) (ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂) | dxlr⋘xlr | lemma-perfect dxlr⋘xlr
  ... | inj₁ y₁≤y₂ | inj₁ (l≃r , l⋙dr) | _dxlr⋘xlr | _ =
                         let l⋘r = ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                              pl'≈l' = lemma-push⋘ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁ ;
                              l'≈l = ≈left (lexy refl≤) x≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                              pl'≈l = trans≈ pl'≈l' l'≈l ;
                              pl'⋙dr = lemma≈⋙ pl'≈l l⋙dr ;
                              pl'⋙dr' = subtyping⋙r (lexy y₁≤y₂) pl'⋙dr ;
                              r≃l = sym≃ l≃r ;
                              l≃l = trans≃ l≃r r≃l ;
                              pl'≃l = lemma≈≃ pl'≈l l≃l
                         in lemma-⋘-⊥ x≤y₁ b≤x pl'⋙dr' l⋘r pl'≃l _dxlr⋘xlr
  ... | inj₂ y₂≤y₁ | inj₁ (l≃r , l⋙dr) | _dxlr⋘xlr | _ =
                         let l⋘r = ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                              l'≈l = ≈left (lexy y₂≤y₁) x≤y₁ l₁⋘r₁  l₁⋘r₁ refl≈ refl≈ ;
                              l'⋙dr = lemma≈⋙ l'≈l l⋙dr ;
                              r≃l = sym≃ l≃r ;
                              l≃l = trans≃ l≃r r≃l ;
                              l'≃l = lemma≈≃ l'≈l l≃l
                         in lemma-⋘-⊥ x≤y₂ b≤x l'⋙dr l⋘r l'≃l _dxlr⋘xlr
  ... | _ | inj₂ dl⋘r | _ | pnd .b≤x .(ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂) l≃r =
                         let r≃l = sym≃ l≃r ;
                              dl⋘l = lemma-⋘-≃ dl⋘r r≃l
                         in lemma-drop-⊥ x≤y₁ l₁⋘r₁ dl⋘l
  lemma-drop-⊥ b≤x (lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗r₂) dxlr⋘xlr
      with lemma-perfect dxlr⋘xlr
  ... | pnd .b≤x .(lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗r₂) ()

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting