text:
module Numeral.FixedPositional where

import      Lvl
open import Data using (<>)
open import Data.List
open import Data.Boolean hiding (elim)
open import Data.Boolean.Stmt
open import Numeral.Finite
open import Numeral.Natural
open import Functional
open import Syntax.Number
open import Type

private variable ℓ : Lvl.Level
private variable z : Bool
private variable b n : ℕ

-- A formalization of the fixed positional radix numeral system for the notation of numbers.
-- Each number is represented by a list of digits.
-- Digits are a finite set of ordered objects starting with zero (0), and a finite number of its successors.
-- Examples using radix 10 (b = 10):
--   ∅                               represents 0
--   # 0                             represents 0
--   # 0 · 0                         represents 0
--   # 2                             represents 2
--   # 1 · 3                         represents 13
--   # 5 · 0 · 4 · 0 · 0             represents 50400
--   # 0 · 5 · 0 · 4 · 0 · 0         represents 50400
--   # 0 · 0 · 0 · 5 · 0 · 4 · 0 · 0 represents 50400
--   # 5 · 0 · 4 · 0 · 0 · 0         represents 504000
-- Example using radix 2 (b = 2):
--   # 1 · 1             represents 3
--   # 0 · 1 · 0 · 1 · 1 represents 11
-- Note: The radix is also called base.
-- Note: This representation is in little endian: The deepest digit in the list is the most significant digit (greatest), and the first position of the list is the least significant digit. Note that the (_·_) operator is a reversed list cons operator, so it constructs a list from right to left when written without parenthesis.
Positional = List ∘ 𝕟
pattern # n = n ⊰ ∅
pattern _·_ a b = b ⊰ a
infixl 100 _·_

private variable x y : Positional(b)
private variable d : 𝕟(n)

-- Two positionals are equal when the sequence of digits in the lists are the same.
-- But also, when there are zeroes at the most significant positions, they should be skipped.
-- Examples:
--   # 4 · 5         ≡ₚₒₛ # 4 · 5
--   # 0 · 0 · 4 · 5 ≡ₚₒₛ # 4 · 5
--   # 4 · 5         ≡ₚₒₛ # 0 · 0 · 4 · 5
--   # 0 · 0 · 4 · 5 ≡ₚₒₛ # 0 · 4 · 5
data _≡ₚₒₛ_ : Positional b → Positional b → Type{Lvl.𝟎} where
  empty : (_≡ₚₒₛ_ {b} ∅ ∅)
  skipₗ : (x ≡ₚₒₛ ∅) → (x · 𝟎 ≡ₚₒₛ ∅)
  skipᵣ : (∅ ≡ₚₒₛ y) → (∅ ≡ₚₒₛ y · 𝟎)
  step  : (x ≡ₚₒₛ y) → (x · d ≡ₚₒₛ y · d)

module _ where
  open import Numeral.Natural.Oper

  -- Converts a positional to a number by adding the first digit and multiplying the rest with the radix.
  -- Examples in radix 10 (b = 10):
  --   to-ℕ (# 1 · 2 · 3) = 10 ⋅ (10 ⋅ (10 ⋅ 0 + 1) + 2) + 3 = ((0 + 100) + 20) + 3 = 100 + 20 + 3 = 123
  --   to-ℕ (# a · b · c) = 10 ⋅ (10 ⋅ (10 ⋅ 0 + a) + b) + c = (10² ⋅ a) + (10¹ ⋅ b) + c = (10² ⋅ a) + (10¹ ⋅ b) + (10⁰ ⋅ c)
  to-ℕ : Positional b → ℕ
  to-ℕ     ∅       = 𝟎
  to-ℕ {b} (l · n) = (b ⋅ (to-ℕ l)) + (𝕟-to-ℕ n)

  import      Data.List.Functions as List
  open import Logic.Propositional
  open import Numeral.Finite.Proofs
  open import Numeral.Natural.Inductions
  open import Numeral.Natural.Oper.Comparisons
  open import Numeral.Natural.Oper.FlooredDivision
  open import Numeral.Natural.Oper.FlooredDivision.Proofs
  open import Numeral.Natural.Oper.Modulo
  open import Numeral.Natural.Oper.Modulo.Proofs
  open import Numeral.Natural.Relation.Order
  open import Numeral.Natural.Relation.Order.Decidable
  open import Numeral.Natural.Relation.Order.Proofs
  open import Structure.Relator.Ordering
  import      Structure.Relator.Names as Names
  open import Structure.Relator.Equivalence
  open import Structure.Relator.Properties
  open import Syntax.Transitivity
  open import Type.Properties.Decidable
  open import Type.Properties.Decidable.Proofs

  -- Converts a number to its positional representation in the specified radix.
  -- This is done by extracting the next digit using modulo of the radix and then dividing the rest.
  -- This is the inverse of to-ℕ.
  from-ℕ-rec : ⦃ b-size : IsTrue(b >? 1) ⦄ → (x : ℕ) → ((prev : ℕ) ⦃ _ : prev < x ⦄ → Positional(b)) → Positional(b)
  from-ℕ-rec b@{𝐒(𝐒 _)} 𝟎       _    = ∅
  from-ℕ-rec b@{𝐒(𝐒 _)} n@(𝐒 _) prev = (prev(n ⌊/⌋ b) ⦃ [⌊/⌋]-ltₗ {n}{b} ⦄) · (ℕ-to-𝕟 (n mod b) ⦃ [↔]-to-[→] decider-true (mod-maxᵣ{n}{b}) ⦄)
  from-ℕ : ℕ → Positional(b)
  from-ℕ {0}        = const ∅
  from-ℕ {1}        = List.repeat 𝟎
  from-ℕ b@{𝐒(𝐒 _)} = Strict.Properties.wellfounded-recursion(_<_) from-ℕ-rec

  instance
    [≡ₚₒₛ]-reflexivity : Reflexivity(_≡ₚₒₛ_ {b})
    [≡ₚₒₛ]-reflexivity = intro p where
      p : Names.Reflexivity(_≡ₚₒₛ_ {b})
      p {x = ∅}     = empty
      p {x = _ ⊰ _} = _≡ₚₒₛ_.step p

  instance
    [≡ₚₒₛ]-symmetry : Symmetry(_≡ₚₒₛ_ {b})
    [≡ₚₒₛ]-symmetry = intro p where
      p : Names.Symmetry(_≡ₚₒₛ_ {b})
      p empty            = empty
      p (skipₗ eq)       = skipᵣ (p eq)
      p (skipᵣ eq)       = skipₗ (p eq)
      p (_≡ₚₒₛ_.step eq) = _≡ₚₒₛ_.step (p eq)

  instance
    [≡ₚₒₛ]-transitivity : Transitivity(_≡ₚₒₛ_ {b})
    [≡ₚₒₛ]-transitivity = intro p where
      p : Names.Transitivity(_≡ₚₒₛ_ {b})
      p empty           empty           = empty
      p empty           (skipᵣ b)       = skipᵣ b
      p (skipₗ a)       empty           = skipₗ a
      p (skipₗ a)       (skipᵣ b)       = _≡ₚₒₛ_.step (p a b)
      p (skipᵣ a)       (skipₗ b)       = p a b
      p (skipᵣ a)       (_≡ₚₒₛ_.step b) = skipᵣ (p a b)
      p (_≡ₚₒₛ_.step a) (skipₗ b)       = skipₗ (p a b)
      p (_≡ₚₒₛ_.step a) (_≡ₚₒₛ_.step b) = _≡ₚₒₛ_.step (p a b)

  instance
    [≡ₚₒₛ]-equivalence : Equivalence(_≡ₚₒₛ_ {b})
    [≡ₚₒₛ]-equivalence = intro

  open import Structure.Setoid using (Equiv ; intro)

  Positional-equiv : Equiv(Positional(b))
  Positional-equiv {b} = intro _ ⦃ [≡ₚₒₛ]-equivalence {b} ⦄

  open import Lang.Instance
  open import Numeral.Natural.Relation.Proofs
  open import Structure.Function
  open import Structure.Operator
  open import Relator.Equals
  open import Relator.Equals.Proofs

  from-ℕ-digit : ⦃ b-size : IsTrue(b >? 1) ⦄ → ⦃ _ : IsTrue(n <? b) ⦄ → (from-ℕ {b} n ≡ₚₒₛ ℕ-to-𝕟 n ⊰ ∅)
  from-ℕ-digit b@{𝐒(𝐒 bb)} {n} = Strict.Properties.wellfounded-recursion-intro(_<_) {rec = from-ℕ-rec} {φ = \{n} expr → ⦃ _ : IsTrue(n <? b) ⦄ → (expr ≡ₚₒₛ (ℕ-to-𝕟 n ⊰ ∅))} p {n} where
    p : (y : ℕ) → _ → _ → ⦃ _ : IsTrue(y <? b) ⦄ → (from-ℕ y ≡ₚₒₛ (ℕ-to-𝕟 y ⊰ ∅))
    p 𝟎 prev eq = skipᵣ empty
    p (𝐒 y) prev eq ⦃ ord ⦄ =
      from-ℕ (𝐒(y))                                                         🝖[ _≡ₚₒₛ_ ]-[ sub₂(_≡_)(_≡ₚₒₛ_) (eq{y} ⦃ reflexivity(_≤_) ⦄) ]
      from-ℕ (𝐒(y) ⌊/⌋ b) · ℕ-to-𝕟 (𝐒(y) mod b) ⦃ yb-ord? ⦄                 🝖[ _≡ₚₒₛ_ ]-[ _≡ₚₒₛ_.step (prev ⦃ [⌊/⌋]-ltₗ{𝐒 y}{b}  ⦄ ⦃ div-ord ⦄) ]
      ∅ · ℕ-to-𝕟 (𝐒(y) ⌊/⌋ b) ⦃ div-ord ⦄ · ℕ-to-𝕟 (𝐒(y) mod b) ⦃ yb-ord? ⦄ 🝖[ _≡ₚₒₛ_ ]-[ sub₂(_≡_)(_≡ₚₒₛ_) (congruence₂ᵣ(_·_)(_) (congruence-ℕ-to-𝕟 ⦃ infer ⦄ ⦃ yb-ord? ⦄ (mod-lesser-than-modulus {𝐒 y}{𝐒 bb} ⦃ yb-ord ⦄))) ]
      ∅ · ℕ-to-𝕟 (𝐒(y) ⌊/⌋ b) ⦃ div-ord ⦄ · ℕ-to-𝕟 (𝐒(y))                   🝖[ _≡ₚₒₛ_ ]-[ _≡ₚₒₛ_.step (sub₂(_≡_)(_≡ₚₒₛ_) (congruence₂ᵣ(_·_)(_) (congruence-ℕ-to-𝕟 ⦃ infer ⦄ ⦃ div-ord ⦄ ([⌊/⌋]-zero {𝐒 y}{b} yb-ord2)))) ]
      ∅ · 𝟎 · ℕ-to-𝕟 (𝐒(y))                                                 🝖[ _≡ₚₒₛ_ ]-[ _≡ₚₒₛ_.step (skipₗ empty) ]
      ∅ · ℕ-to-𝕟 (𝐒(y))                                                     🝖-end
      where
        yb-ord? = [↔]-to-[→] decider-true (mod-maxᵣ {𝐒(y)}{b} ⦃ infer ⦄)
        yb-ord = [↔]-to-[←] (decider-true ⦃ [<]-decider ⦄) ord
        yb-ord2 = [↔]-to-[←] (decider-true ⦃ [<]-decider ⦄) ord
        div-ord = [↔]-to-[→] decider-true ([⌊/⌋]-preserve-[<]ₗ {𝐒 y}{b}{b} yb-ord2)

  from-ℕ-step : ⦃ b-size : IsTrue(b >? 1) ⦄
              → let pos = [↔]-to-[←] Positive-greater-than-zero ([≤]-predecessor ([↔]-to-[←] (decider-true ⦃ [<]-decider {1}{b} ⦄) b-size))
                in (from-ℕ {b} n ≡ₚₒₛ (from-ℕ {b} ((n ⌊/⌋ b) ⦃ pos ⦄)) · (ℕ-to-𝕟 ((n mod b) ⦃ pos ⦄) ⦃ [↔]-to-[→] decider-true (mod-maxᵣ{n}{b} ⦃ pos ⦄) ⦄))
  from-ℕ-step b@{𝐒(𝐒 bb)} {n} = Strict.Properties.wellfounded-recursion-intro(_<_) {rec = from-ℕ-rec} {φ = \{n} expr → (expr ≡ₚₒₛ from-ℕ {b} (n ⌊/⌋ b) · (ℕ-to-𝕟 (n mod b) ⦃ ord n ⦄))} p {n} where
    ord = \n → [↔]-to-[→] decider-true (mod-maxᵣ{n}{b})
    p : (y : ℕ) → _ → _ → Strict.Properties.accessible-recursion(_<_) from-ℕ-rec y ≡ₚₒₛ from-ℕ (y ⌊/⌋ b) · ℕ-to-𝕟 (y mod b) ⦃ ord y ⦄
    p 𝟎     prev eq = skipᵣ empty
    p (𝐒 y) prev eq = (sub₂(_≡_)(_≡ₚₒₛ_) (eq {y} ⦃ reflexivity(_≤_) ⦄))

  open import Numeral.Natural.Oper.FlooredDivision.Proofs.Inverse
  open import Numeral.Natural.Oper.Proofs
  open import Structure.Operator.Properties
  from-ℕ-step-invs : ⦃ b-size : IsTrue(b >? 1) ⦄ → (from-ℕ {b} ((b ⋅ n) + (𝕟-to-ℕ d)) ≡ₚₒₛ (from-ℕ {b} n) · d)
  from-ℕ-step-invs b@{𝐒(𝐒 bb)} {n}{d} =
    from-ℕ (b ⋅ n + 𝕟-to-ℕ d)                                                     🝖[ _≡ₚₒₛ_ ]-[ from-ℕ-step {n = b ⋅ n + 𝕟-to-ℕ d} ]
    from-ℕ ((b ⋅ n + 𝕟-to-ℕ d) ⌊/⌋ b) · (ℕ-to-𝕟 ((b ⋅ n + 𝕟-to-ℕ d) mod b) ⦃ _ ⦄) 🝖[ _≡ₚₒₛ_ ]-[ sub₂(_≡_)(_≡ₚₒₛ_) (congruence₂(_·_) (congruence₁(from-ℕ) r) (congruence-ℕ-to-𝕟 ⦃ infer ⦄ ⦃ ord1 ⦄ ⦃ ord2 ⦄ q 🝖 ℕ-𝕟-inverse)) ]
    from-ℕ n · d                                                                  🝖-end where
      ord1 = [↔]-to-[→] decider-true (mod-maxᵣ{(b ⋅ n) + (𝕟-to-ℕ d)}{b})
      ord2 = [↔]-to-[→] decider-true ([<]-of-𝕟-to-ℕ {b}{d})
      q =
        ((b ⋅ n) + 𝕟-to-ℕ d) mod b 🝖[ _≡_ ]-[ congruence₁(_mod b) (commutativity(_+_) {b ⋅ n}{𝕟-to-ℕ d}) ]
        (𝕟-to-ℕ d + (b ⋅ n)) mod b 🝖[ _≡_ ]-[ mod-of-modulus-sum-multiple {𝕟-to-ℕ d}{b}{n} ]
        (𝕟-to-ℕ d) mod b           🝖[ _≡_ ]-[ mod-lesser-than-modulus ⦃ [≤]-without-[𝐒] [<]-of-𝕟-to-ℕ ⦄ ]
        𝕟-to-ℕ d                   🝖-end
      r =
        (b ⋅ n + 𝕟-to-ℕ d) ⌊/⌋ b             🝖[ _≡_ ]-[ [⌊/⌋][+]-distributivityᵣ {b ⋅ n}{𝕟-to-ℕ d}{b} ]
        ((b ⋅ n) ⌊/⌋ b) + ((𝕟-to-ℕ d) ⌊/⌋ b) 🝖[ _≡_ ]-[ congruence₂(_+_) ([⌊/⌋][swap⋅]-inverseOperatorᵣ {b}{n}) ([⌊/⌋]-zero ([<]-of-𝕟-to-ℕ {b}{d})) ]
        n + 𝟎                                🝖[ _≡_ ]-[]
        n                                    🝖-end

  open import Numeral.Natural.Oper.DivMod.Proofs
  open import Structure.Function.Domain
  import      Structure.Function.Names as Names

  instance
    from-to-inverse : ⦃ b-size : IsTrue(b >? 1) ⦄ → Inverseᵣ ⦃ Positional-equiv{b} ⦄ from-ℕ to-ℕ
    from-to-inverse b@{𝐒(𝐒 _)} = intro p where
      p : Names.Inverses ⦃ Positional-equiv{b} ⦄ from-ℕ to-ℕ
      p{x = ∅}     = empty
      p{x = x · n} = from-ℕ-step-invs{b}{to-ℕ x}{n} 🝖 _≡ₚₒₛ_.step (p{x = x})

  instance
    to-from-inverse : ⦃ b-size : IsTrue(b >? 1) ⦄ → Inverseᵣ(to-ℕ{b}) (from-ℕ{b})
    to-from-inverse {b@(𝐒(𝐒 bb))} = intro (\{n} → Strict.Properties.wellfounded-recursion-intro(_<_) {rec = from-ℕ-rec {b}} {φ = \{n} expr → (to-ℕ expr ≡ n)} p {n}) where
      p : (y : ℕ) → _ → _ → (to-ℕ {b} (from-ℕ {b} y) ≡ y)
      p 𝟎     _    _  = [≡]-intro
      p (𝐒 y) prev eq =
        to-ℕ {b} (from-ℕ (𝐒 y))                                                       🝖[ _≡_ ]-[ congruence₁(to-ℕ) (eq {𝐒(y) ⌊/⌋ b} ⦃ ord2 ⦄) ]
        to-ℕ {b} ((from-ℕ (𝐒(y) ⌊/⌋ b)) · (ℕ-to-𝕟 (𝐒(y) mod b) ⦃ _ ⦄))                🝖[ _≡_ ]-[]
        (b ⋅ to-ℕ {b} (from-ℕ {b} (𝐒(y) ⌊/⌋ b))) + 𝕟-to-ℕ (ℕ-to-𝕟 (𝐒(y) mod b) ⦃ _ ⦄) 🝖[ _≡_ ]-[ congruence₂(_+_) (congruence₂ᵣ(_⋅_)(b) (prev{𝐒(y) ⌊/⌋ b} ⦃ ord2 ⦄)) (𝕟-ℕ-inverse {b}{𝐒(y) mod b} ⦃ ord1 ⦄) ]
        (b ⋅ (𝐒(y) ⌊/⌋ b)) + (𝐒(y) mod b)                                             🝖[ _≡_ ]-[ [⌊/⌋][mod]-is-division-with-remainder-pred-commuted {𝐒 y}{b} ]
        𝐒(y)                                                                          🝖-end
        where
          ord1 = [↔]-to-[→] decider-true (mod-maxᵣ{𝐒(y)}{b})
          ord2 = [⌊/⌋]-ltₗ {𝐒 y}{b}

  instance
    to-ℕ-function : ⦃ b-size : IsTrue(b >? 1) ⦄ → Function ⦃ Positional-equiv ⦄ ⦃ [≡]-equiv ⦄ (to-ℕ {b})
    to-ℕ-function {b} = intro p where
      p : Names.Congruence₁ ⦃ Positional-equiv ⦄ ⦃ [≡]-equiv ⦄ (to-ℕ {b})
      p empty                          = reflexivity(_≡_)
      p (skipₗ xy) rewrite p xy        = reflexivity(_≡_)
      p (skipᵣ {y = ∅} xy)             = reflexivity(_≡_)
      p (skipᵣ {y = 𝟎 ⊰ y} (skipᵣ xy))
        rewrite symmetry(_≡_) (p xy)   = reflexivity(_≡_)
      p (_≡ₚₒₛ_.step xy)
        rewrite p xy = reflexivity(_≡_)

  open import Logic.Predicate
  open import Structure.Function.Domain.Proofs

  instance
    from-ℕ-bijective : ⦃ b-size : IsTrue(b >? 1) ⦄ → Bijective ⦃ [≡]-equiv ⦄ ⦃ Positional-equiv ⦄ (from-ℕ {b})
    from-ℕ-bijective = [↔]-to-[→] (invertible-when-bijective ⦃ _ ⦄ ⦃ _ ⦄) ([∃]-intro to-ℕ ⦃ [∧]-intro infer ([∧]-intro infer infer) ⦄)

  instance
    to-ℕ-bijective : ⦃ b-size : IsTrue(b >? 1) ⦄ → Bijective ⦃ Positional-equiv ⦄ ⦃ [≡]-equiv ⦄ (to-ℕ {b})
    to-ℕ-bijective = [↔]-to-[→] (invertible-when-bijective ⦃ _ ⦄ ⦃ _ ⦄) ([∃]-intro from-ℕ ⦃ [∧]-intro ([≡]-to-function ⦃ Positional-equiv ⦄) ([∧]-intro infer infer) ⦄)

  import      Data.Option.Functions as Option
  open import Function.Names
  open import Numeral.Natural.Relation.Order.Proofs

  -- TODO: Trying to define a bijection, but not really possible because not all functions
  PositionalSequence : List(𝕟(𝐒 b)) → (ℕ → 𝕟(𝐒 b))
  PositionalSequence l n = (List.index₀ n l) Option.or 𝟎

  sequencePositional : (f : ℕ → 𝕟(𝐒 b)) → ∃(N ↦ (f ∘ (_+ N) ⊜ const 𝟎)) → List(𝕟(𝐒 b))
  sequencePositional f ([∃]-intro 𝟎)           = ∅
  sequencePositional f ([∃]-intro (𝐒 N) ⦃ p ⦄) = f(𝟎) ⊰ sequencePositional (f ∘ 𝐒) ([∃]-intro N ⦃ \{n} → p{n} ⦄)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module All where

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

map : {A B : Set} -> (A -> B) -> List A -> List B
map f []        = []
map f (x :: xs) = f x :: map f xs

_++_ : {A : Set} -> List A -> List A -> List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f z [] = z
foldr f z (x :: xs) = f x (foldr f z xs)

data All {A : Set}(P : A -> Set) : List A -> Set where
  ∅   : All P []
  _▹_ : {x : A}{xs : List A} -> P x -> All P xs -> All P (x :: xs)

data Some {A : Set}(P : A -> Set) : List A -> Set where
  hd : {x : A}{xs : List A} -> P x       -> Some P (x :: xs)
  tl : {x : A}{xs : List A} -> Some P xs -> Some P (x :: xs)

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

_∈_ : {A : Set} -> A -> List A -> Set
x ∈ xs = Some (_==_ x) xs

infixr 40 _,_

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

_∧_ : (A B : Set) -> Set
A ∧ B = A × \_ -> B

_!_ : {A : Set}{P : A -> Set}{Q : A -> Set}{xs : List A} ->
      All P xs -> Some Q xs -> A × (\x -> P x ∧ Q x)
ε ! ()
(p ▹ ps) ! hd q = _ , (p , q)
(p ▹ ps) ! tl q = ps ! q

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Properties related with the totality of the rose tree type
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Mirror.Tree.TotalityNonTerminationI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.Type
open import FOTC.Program.Mirror.Forest.TotalityI
open import FOTC.Program.Mirror.Forest.PropertiesI

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

-- Requires --injective-type-constructors
-- Peter: To use injectivity of type constructors means asking for
-- trouble. The logic behind this is very unclear.
node-Forest : ∀ {d ts} → Tree (node d ts) → Forest ts
node-Forest {d} (tree .d Fts) = Fts

postulate reverse-∷' : ∀ x ys → reverse (x ∷ ys) ≡ reverse ys ++ (x ∷ [])

-- The termination checker can not determine that the function mirror-Tree
-- defined by
--
-- mirror-Tree (tree d (fcons {t} {ts} Tt Fts)) =
--   ... mirror-Tree (tree d Fts) ... mirror-Tree Tt ...
--
-- is structurally recursive.

-- Andreas Abel: The function does not terminate because we are using
-- postulates (i.e. D, _∷_, etc). In particular, x is not structurally
-- smaller than x ∷ xs.

{-# TERMINATING #-}
mirror-Tree : ∀ {t} → Tree t → Tree (mirror · t)
mirror-Tree (tree d fnil) =
  subst Tree (sym (mirror-eq d [])) (tree d helper₂)
    where
      helper₁ : rev (map mirror []) [] ≡ []
      helper₁ =
          rev (map mirror []) []
            ≡⟨ subst (λ x → rev (map mirror []) [] ≡ rev x [])
                     (map-[] mirror)
                     refl
           ⟩
          rev [] []
            ≡⟨ rev-[] [] ⟩
          [] ∎

      helper₂ : Forest (rev (map mirror []) [])
      helper₂ = subst Forest (sym helper₁) fnil

mirror-Tree (tree d (fcons {t} {ts} Tt Fts)) =
  subst Tree (sym (mirror-eq d (t ∷ ts))) (tree d helper)

  where
     h₁ : Tree (node d (reverse (map mirror ts)))
     h₁ = subst Tree (mirror-eq d ts) (mirror-Tree (tree d Fts))

     h₂ : Forest (reverse (map mirror ts))
     h₂ = node-Forest h₁

     h₃ : Forest ((reverse (map mirror ts)) ++ (mirror · t ∷ []))
     h₃ = ++-Forest h₂ (fcons (mirror-Tree Tt) fnil)

     h₄ : Forest (reverse (mirror · t ∷ map mirror ts))
     h₄ = subst Forest (sym (reverse-∷' (mirror · t) (map mirror ts))) h₃

     helper : Forest (reverse (map mirror (t ∷ ts)))
     helper = subst Forest
              (subst (λ x → reverse x ≡ reverse (map mirror (t ∷ ts)))
                     (map-∷ mirror t ts)
                     refl)
              h₄

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module L.Base.Id where

-- Reexport definitions
open import L.Base.Id.Core public

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
{-# OPTIONS --cubical #-}
module Agda.Builtin.Cubical.Sub where

  open import Agda.Primitive.Cubical

  {-# BUILTIN SUB Sub #-}

  postulate
    inc : ∀ {ℓ} {A : Set ℓ} {φ} (x : A) → Sub A φ (λ _ → x)

  {-# BUILTIN SUBIN inc #-}

  primitive
    primSubOut : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → Sub _ φ u → A

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
{-# OPTIONS --safe #-}
module TEST where

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

arith-sum : ℕ → ℕ
arith-sum zero = zero
arith-sum (suc n) = suc n + arith-sum n

arith-formula : ℕ → ℕ
arith-formula n = ⌊ n * (n + 1) /2⌋

silly : ∀ (n m : ℕ) →  ⌊ n + n + m * (m + 1) /2⌋ ≡ n +  ⌊ m * (m + 1) /2⌋
silly zero m = refl
silly (suc n) m rewrite +-suc n n = cong suc (silly n m)

lemma : ∀ (n : ℕ) →  ⌊ suc n * (suc n + 1) /2⌋ ≡ suc n +  ⌊ n * (n + 1) /2⌋
lemma n rewrite *-comm n (suc n + 1) | +-assoc n 1 (n + (n + 1) * n) | *-comm (n + 1) n | +-comm n (suc (n + n * (n + 1)))
                                     | +-assoc n (n * (n + 1)) n | +-comm (n * (n + 1)) n | sym (silly n n) | +-assoc n n (n * (n + 1)) = refl

arith-eq : (n : ℕ) -> arith-formula n ≡ arith-sum n
arith-eq zero = refl
arith-eq (suc n) rewrite lemma n =  cong (_+_ (suc n)) (arith-eq n)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Rings.Homomorphisms.Definition

module Fields.CauchyCompletion.Ring {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Field F
open Group (Ring.additiveGroup R)

open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Multiplication order F
open import Fields.CauchyCompletion.Addition order F
open import Fields.CauchyCompletion.Setoid order F
open import Fields.CauchyCompletion.Group order F

private
  abstract
    c*Assoc : {a b c : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a *C (b *C c)) ((a *C b) *C c)
    c*Assoc {a} {b} {c} ε 0<e = 0 , ans
      where
        ans : {m : ℕ} → 0 <N m → abs (index (CauchyCompletion.elts ((a *C (b *C c)) +C (-C ((a *C b) *C c)))) m) < ε
        ans {m} 0<m rewrite indexAndApply (CauchyCompletion.elts (a *C (b *C c))) (CauchyCompletion.elts (-C ((a *C b) *C c))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)) _*_ {m} | equalityCommutative (mapAndIndex (apply _*_ (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (CauchyCompletion.elts c)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts c) _*_ {m} | indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (CauchyCompletion.elts c) _*_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (transferToRight'' (Ring.additiveGroup R) (Ring.*Associative R))) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e

    c*Ident : {a : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (injection (Ring.1R R) *C a) a
    c*Ident {a} ε 0<e = 0 , ans
      where
        ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (injection (Ring.1R R) *C a)) (map inverse (CauchyCompletion.elts a))) m) < ε
        ans {m} 0<m rewrite indexAndApply (CauchyCompletion.elts (injection (Ring.1R R) *C a)) (map inverse (CauchyCompletion.elts a)) _+_ {m} | indexAndApply (constSequence (Ring.1R R)) (CauchyCompletion.elts a) _*_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) | indexAndConst (Ring.1R R) m = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (transferToRight'' (Ring.additiveGroup R) (Ring.identIsIdent R))) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) (absZero)))) (Equivalence.reflexive eq) 0<e

    *CDistribute : {a b c : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a *C (b +C c)) ((a *C b) +C (a *C c))
    *CDistribute {a} {b} {c} e 0<e = 0 , ans
      where
        ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (a *C (b +C c))) (map inverse (CauchyCompletion.elts ((a *C b) +C (a *C c))))) m) < e
        ans {m} N<m rewrite indexAndApply (CauchyCompletion.elts (a *C (b +C c))) (map inverse (CauchyCompletion.elts ((a *C b) +C (a *C c)))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (apply _+_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)) _*_ {m} | equalityCommutative (mapAndIndex (apply _+_ (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c))) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts c) _+_ {m} | indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _*_ {m} = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (transferToRight'' (Ring.additiveGroup R) (Ring.*DistributesOver+ R))) (absZeroIsZero))) (Equivalence.reflexive eq) 0<e

CRing : Ring cauchyCompletionSetoid _+C_ _*C_
Ring.additiveGroup CRing = CGroup
Ring.*WellDefined CRing {a} {b} {c} {d} r=t s=u = multiplicationWellDefined {a} {c} {b} {d} r=t s=u
Ring.1R CRing = injection (Ring.1R R)
Ring.groupIsAbelian CRing {a} {b} = +CCommutative a b
Ring.*Associative CRing {a} {b} {c} = c*Assoc {a} {b} {c}
Ring.*Commutative CRing {a} {b} = *CCommutative {a} {b}
Ring.*DistributesOver+ CRing {a} {b} {c} = *CDistribute {a} {b} {c}
Ring.identIsIdent CRing {a} = c*Ident {a}

private
  injectionIsRingHom : (a b : A) → Setoid._∼_ cauchyCompletionSetoid (injection (a * b)) (injection a *C injection b)
  injectionIsRingHom a b ε 0<e = 0 , ans
    where
      ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (injection (a * b))) (map inverse (CauchyCompletion.elts (injection a *C injection b)))) m) < ε
      ans {m} 0<m rewrite indexAndApply (constSequence (a * b)) (map inverse (apply _*_ (constSequence a) (constSequence b))) _+_ {m} | indexAndConst (a * b) m | equalityCommutative (mapAndIndex (apply _*_ (constSequence a) (constSequence b)) inverse m) | indexAndApply (constSequence a) (constSequence b) _*_ {m} | indexAndConst a m | indexAndConst b m = <WellDefined (symmetric (transitive (absWellDefined _ _ invRight) absZeroIsZero)) reflexive 0<e

CInjectionRingHom : RingHom R CRing injection
RingHom.preserves1 CInjectionRingHom = Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {injection (Ring.1R R)}
RingHom.ringHom CInjectionRingHom {a} {b} = injectionIsRingHom a b
RingHom.groupHom CInjectionRingHom = CInjectionGroupHom


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

open import LogicalFormulae
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations

module Fields.FieldOfFractions.Multiplication {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

open import Fields.FieldOfFractions.Setoid I

fieldOfFractionsTimes : fieldOfFractionsSet → fieldOfFractionsSet → fieldOfFractionsSet
fieldOfFractionsTimes (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 }) = record { num = a * c ; denom = b * d ; denomNonzero = ans }
  where
    open Setoid S
    open Ring R
    ans : ((b * d) ∼ Ring.0R R) → False
    ans pr with IntegralDomain.intDom I pr
    ans pr | f = exFalso (d!=0 (f b!=0))

fieldOfFractionsTimesWellDefined : {a b c d : fieldOfFractionsSet} → (Setoid._∼_ fieldOfFractionsSetoid a c) → (Setoid._∼_ fieldOfFractionsSetoid b d) → (Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsTimes a b) (fieldOfFractionsTimes c d))
fieldOfFractionsTimesWellDefined {record { num = a ; denom = b }} {record { num = c ; denom = d }} {record { num = e ; denom = f }} {record { num = g ; denom = h }} af=be ch=dg = need
  where
    open Setoid S
    open Equivalence eq
    need : ((a * c) * (f * h)) ∼ ((b * d) * (e * g))
    need = transitive (Ring.*WellDefined R reflexive (Ring.*Commutative R)) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (symmetric (Ring.*Associative R)) reflexive) (transitive (Ring.*WellDefined R (Ring.*WellDefined R reflexive ch=dg) reflexive) (transitive (Ring.*Commutative R) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (Ring.*Commutative R) reflexive) (transitive (Ring.*WellDefined R af=be reflexive) (transitive (Ring.*Associative R) (transitive (Ring.*WellDefined R (transitive (symmetric (Ring.*Associative R)) (transitive (Ring.*WellDefined R reflexive (Ring.*Commutative R)) (Ring.*Associative R))) reflexive) (symmetric (Ring.*Associative R)))))))))))


text:
module Structure.Operator.Monoid.Category where

open import Data
open import Data.Tuple as Tuple using (_,_)
open import Functional
import      Lvl
open import Structure.Setoid
open import Structure.Category
open import Structure.Categorical.Properties
open import Structure.Operator.Monoid
open import Structure.Operator.Monoid.Homomorphism
open import Structure.Operator.Properties using (associativity ; identityₗ ; identityᵣ)
open import Structure.Operator
open import Type

private variable ℓ ℓₑ ℓₗ ℓₗₑ : Lvl.Level
private variable T : Type{ℓ}
private variable _▫_ : T → T → T

module _
  ⦃ equiv : Equiv{ℓₑ}(T) ⦄
  ⦃ oper : BinaryOperator(_▫_) ⦄
  (M : Monoid{T = T}(_▫_))
  where

  -- A monoid as a special case of a category with a single object and morphisms in and out of this object.
  -- Composition and identity in the category is the binary operator and the identity element from the monoid.
  monoidCategory : Category{Obj = Unit{Lvl.𝟎}}(const(const(T)))
  Category._∘_            monoidCategory = (_▫_)
  Category.id             monoidCategory = Monoid.id(M)
  Category.binaryOperator monoidCategory = oper
  Category.associativity  monoidCategory = Morphism.intro(associativity(_▫_))
  Category.identity       monoidCategory = Morphism.intro (identityₗ(_▫_)(Monoid.id(M))) , Morphism.intro ((identityᵣ(_▫_)(Monoid.id(M))))

module _ where
  open import Function.Equals
  open import Function.Equals.Proofs
  open import Function.Proofs
  open import Logic.Predicate
  open import Logic.Propositional
  open import Structure.Function.Multi
  open import Structure.Function
  open import Structure.Relator.Equivalence
  open import Structure.Relator.Properties
  open import Syntax.Function
  open import Syntax.Transitivity

  private variable x y z : MonoidObject{ℓₗ}{ℓₗₑ}

  instance
    [→ᵐᵒⁿᵒⁱᵈ]-equiv : Equiv(x →ᵐᵒⁿᵒⁱᵈ y)
    Equiv._≡_ [→ᵐᵒⁿᵒⁱᵈ]-equiv ([∃]-intro F) ([∃]-intro G) = F ⊜ G
    Reflexivity.proof  (Equivalence.reflexivity  (Equiv.equivalence [→ᵐᵒⁿᵒⁱᵈ]-equiv)) = reflexivity(_⊜_)
    Symmetry.proof     (Equivalence.symmetry     (Equiv.equivalence [→ᵐᵒⁿᵒⁱᵈ]-equiv)) = symmetry(_⊜_)
    Transitivity.proof (Equivalence.transitivity (Equiv.equivalence [→ᵐᵒⁿᵒⁱᵈ]-equiv)) = transitivity(_⊜_)

  -- Identity monoid homomorphism.
  idᵐᵒⁿᵒⁱᵈ : x →ᵐᵒⁿᵒⁱᵈ x
  ∃.witness idᵐᵒⁿᵒⁱᵈ = id
  Homomorphism.function                      (∃.proof idᵐᵒⁿᵒⁱᵈ)  = id-function
  Preserving.proof (Homomorphism.preserve-op (∃.proof idᵐᵒⁿᵒⁱᵈ)) = reflexivity(_≡_)
  Preserving.proof (Homomorphism.preserve-id (∃.proof idᵐᵒⁿᵒⁱᵈ)) = reflexivity(_≡_)

  -- Composition of monoid homomorphisms.
  _∘ᵐᵒⁿᵒⁱᵈ_ : let _ = x in (y →ᵐᵒⁿᵒⁱᵈ z) → (x →ᵐᵒⁿᵒⁱᵈ y) → (x →ᵐᵒⁿᵒⁱᵈ z)
  ∃.witness (([∃]-intro F) ∘ᵐᵒⁿᵒⁱᵈ ([∃]-intro G)) = F ∘ G
  Homomorphism.function                      (∃.proof (([∃]-intro F) ∘ᵐᵒⁿᵒⁱᵈ ([∃]-intro G)))  = [∘]-function {f = F}{g = G}
  Preserving.proof (Homomorphism.preserve-op (∃.proof (_∘ᵐᵒⁿᵒⁱᵈ_ {x = A} {y = B} {z = C} ([∃]-intro F) ([∃]-intro G)))) {x} {y} =
    (F ∘ G)(x ⦗ MonoidObject._▫_ A ⦘ y)          🝖[ _≡_ ]-[]
    F(G(x ⦗ MonoidObject._▫_ A ⦘ y))             🝖[ _≡_ ]-[ congruence₁(F) (preserving₂(G) (MonoidObject._▫_ A) (MonoidObject._▫_ B)) ]
    F(G(x) ⦗ MonoidObject._▫_ B ⦘ G(y))          🝖[ _≡_ ]-[ preserving₂(F) (MonoidObject._▫_ B) (MonoidObject._▫_ C) ]
    F(G(x)) ⦗ MonoidObject._▫_ C ⦘ F(G(y))       🝖[ _≡_ ]-[]
    (F ∘ G)(x) ⦗ MonoidObject._▫_ C ⦘ (F ∘ G)(y) 🝖-end
  Preserving.proof (Homomorphism.preserve-id (∃.proof (_∘ᵐᵒⁿᵒⁱᵈ_ {x = A} {y = B} {z = C} ([∃]-intro F) ([∃]-intro G)))) =
    (F ∘ G)(MonoidObject.id A) 🝖[ _≡_ ]-[]
    F(G(MonoidObject.id A))    🝖[ _≡_ ]-[ congruence₁(F) (preserving₀(G) (MonoidObject.id A) (MonoidObject.id B)) ]
    F(MonoidObject.id B)       🝖[ _≡_ ]-[ preserving₀(F) (MonoidObject.id B) (MonoidObject.id C) ]
    MonoidObject.id C          🝖-end

  -- A category where the objects are monoids themselves and the morphisms are homomorphism between them.
  instance
    monoidObjectCategory : Category{Obj = MonoidObject{ℓₗ}{ℓₗₑ}}(_→ᵐᵒⁿᵒⁱᵈ_)
    Category._∘_            monoidObjectCategory = _∘ᵐᵒⁿᵒⁱᵈ_
    Category.id             monoidObjectCategory = idᵐᵒⁿᵒⁱᵈ
    Category.binaryOperator monoidObjectCategory = intro(\p q → [⊜][∘]-binaryOperator-raw p q)
    Category.associativity  monoidObjectCategory = Morphism.intro (reflexivity(_⊜_))
    Category.identity       monoidObjectCategory = [∧]-intro (Morphism.intro(reflexivity(_⊜_))) (Morphism.intro(reflexivity(_⊜_)))

  monoidObjectCategoryObject : ∀{ℓₗ ℓₑ} → CategoryObject
  monoidObjectCategoryObject{ℓₗ}{ℓₑ} = intro(monoidObjectCategory{ℓₗ}{ℓₑ})


text:
------------------------------------------------------------------------------
-- Totality properties respect to OrdList (flatten-OrdList-helper)
------------------------------------------------------------------------------

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

-- The termination checker can not determine that the function
-- flatten-OrdList-helper is defined by structural recursion because
-- we are using postulates.

module FOT.FOTC.Program.SortList.Properties.Totality.OrdList.FlattenI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.Type
open import FOTC.Data.List
open import FOTC.Program.SortList.Properties.Totality.BoolI
open import FOTC.Program.SortList.Properties.Totality.ListN-I
open import FOTC.Program.SortList.Properties.Totality.OrdTreeI
open import FOTC.Program.SortList.Properties.MiscellaneousI
open import FOTC.Program.SortList.SortList

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

{-# TERMINATING #-}
flatten-OrdList-helper : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ →
                         OrdTree (node t₁ i t₂) →
                         ≤-Lists (flatten t₁) (flatten t₂)

flatten-OrdList-helper {t₂ = t₂} tnil Ni Tt₂ OTt =
  subst (λ t → ≤-Lists t (flatten t₂))
        (sym (flatten-nil))
        (le-Lists-[] (flatten t₂))

flatten-OrdList-helper (ttip {i₁} Ni₁) _ tnil OTt =
  le-Lists (flatten (tip i₁)) (flatten nil)
    ≡⟨ subst₂ (λ x₁ x₂ → le-Lists (flatten (tip i₁)) (flatten nil) ≡
                         le-Lists x₁ x₂)
              (flatten-tip i₁)
              flatten-nil
              refl
    ⟩
  le-Lists (i₁ ∷ []) []
    ≡⟨ le-Lists-∷ i₁ [] [] ⟩
  le-ItemList i₁ [] && le-Lists [] []
    ≡⟨ subst₂ (λ x₁ x₂ → le-ItemList i₁ [] && le-Lists [] [] ≡ x₁ && x₂)
              (le-ItemList-[] i₁)
              (le-Lists-[] [])
              refl
    ⟩
  true && true
    ≡⟨ t&&x≡x true ⟩
  true ∎

flatten-OrdList-helper {i = i} (ttip {i₁} Ni₁) Ni (ttip {i₂} Ni₂) OTt =
  le-Lists (flatten (tip i₁)) (flatten (tip i₂))
    ≡⟨ subst₂ (λ x₁ x₂ → le-Lists (flatten (tip i₁)) (flatten (tip i₂)) ≡
                         le-Lists x₁ x₂)
              (flatten-tip i₁)
              (flatten-tip i₂)
              refl
    ⟩
  le-Lists (i₁ ∷ []) (i₂ ∷ [])
    ≡⟨ le-Lists-∷ i₁ [] (i₂ ∷ []) ⟩
  le-ItemList i₁ (i₂ ∷ []) && le-Lists [] (i₂ ∷ [])
    ≡⟨ subst (λ t → le-ItemList i₁ (i₂ ∷ []) && le-Lists [] (i₂ ∷ []) ≡
                    t && le-Lists [] (i₂ ∷ []))
             (le-ItemList-∷ i₁ i₂ [])
             refl
    ⟩
  (le i₁ i₂ && le-ItemList i₁ []) && le-Lists [] (i₂ ∷ [])
    ≡⟨ subst (λ t → (le i₁ i₂ && le-ItemList i₁ []) && le-Lists [] (i₂ ∷ []) ≡
                    (t        && le-ItemList i₁ []) && le-Lists [] (i₂ ∷ []))
             lemma
             refl
    ⟩
  (true && le-ItemList i₁ []) && le-Lists [] (i₂ ∷ [])
    ≡⟨ subst₂ (λ x₁ x₂ → (true && le-ItemList i₁ []) && le-Lists [] (i₂ ∷ []) ≡
                         (true && x₁)               && x₂)
              (le-ItemList-[] i₁)
              (le-Lists-[] (i₂ ∷ []))
              refl
    ⟩
  (true && true) && true
    ≡⟨ &&-assoc btrue btrue btrue ⟩
  true && true && true
    ≡⟨ &&-list₃-all-t btrue btrue btrue (refl , refl , refl) ⟩
  true
  ∎
  where
    helper₁ : Bool (ordTree (tip i₁))
    helper₁ = ordTree-Bool (ttip Ni₁)

    helper₂ : Bool (ordTree (tip i₂))
    helper₂ = ordTree-Bool (ttip Ni₂)

    helper₃ : Bool (le-TreeItem (tip i₁) i)
    helper₃ = le-TreeItem-Bool (ttip Ni₁) Ni

    helper₄ : Bool (le-ItemTree i (tip i₂))
    helper₄ = le-ItemTree-Bool Ni (ttip Ni₂)

    helper₅ : ordTree (tip i₁) &&
              ordTree (tip i₂) &&
              le-TreeItem (tip i₁) i &&
              le-ItemTree i (tip i₂) ≡ true
    helper₅ = trans (sym (ordTree-node (tip i₁) i (tip i₂))) OTt

    lemma : i₁ ≤ i₂
    lemma = ≤-trans Ni₁ Ni Ni₂ i₁≤i i≤i₂
     where
       i₁≤i : i₁ ≤ i
       i₁≤i = trans (sym (le-TreeItem-tip i₁ i))
                    (&&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅)

       i≤i₂ : i ≤ i₂
       i≤i₂ = trans (sym (le-ItemTree-tip i i₂))
                    (&&-list₄-t₄ helper₁ helper₂ helper₃ helper₄ helper₅)

flatten-OrdList-helper {i = i} (ttip {i₁} Ni₁) Ni
                       (tnode {t₂₁} {i₂} {t₂₂} Tt₂₁ Ni₂ Tt₂₂) OTt =
  le-Lists (flatten (tip i₁)) (flatten (node t₂₁ i₂ t₂₂))
    ≡⟨ subst (λ x → le-Lists (flatten (tip i₁)) (flatten (node t₂₁ i₂ t₂₂)) ≡
                    le-Lists (flatten (tip i₁)) x)
             (flatten-node t₂₁ i₂ t₂₂)
             refl
    ⟩
  le-Lists (flatten (tip i₁)) (flatten t₂₁ ++ flatten t₂₂)
    ≡⟨ xs≤ys→xs≤zs→xs≤ys++zs (flatten-ListN (ttip Ni₁))
                             (flatten-ListN Tt₂₁)
                             (flatten-ListN Tt₂₂)
                             lemma₁
                             lemma₂
    ⟩
  true ∎
  where
    -- Helper terms to get the conjuncts from OTt.
    helper₁ = ordTree-Bool (ttip Ni₁)
    helper₂ = ordTree-Bool (tnode Tt₂₁ Ni₂ Tt₂₂)
    helper₃ = le-TreeItem-Bool (ttip Ni₁) Ni
    helper₄ = le-ItemTree-Bool Ni (tnode Tt₂₁ Ni₂ Tt₂₂)
    helper₅ = trans (sym (ordTree-node (tip i₁) i (node t₂₁ i₂ t₂₂))) OTt

    -- Helper terms to get the conjuncts from the fourth conjunct of OTt.
    helper₆ = le-ItemTree-Bool Ni Tt₂₁
    helper₇ = le-ItemTree-Bool Ni Tt₂₂
    helper₈ = trans (sym (le-ItemTree-node i t₂₁ i₂ t₂₂))
                    (&&-list₄-t₄ helper₁ helper₂ helper₃ helper₄ helper₅)

    -- Common terms for the lemma₁ and lemma₂.
    OrdTree-tip-i₁ : OrdTree (tip i₁)
    OrdTree-tip-i₁ = &&-list₄-t₁ helper₁ helper₂ helper₃ helper₄ helper₅

    ≤-TreeItem-tip-i₁-i : ≤-TreeItem (tip i₁) i
    ≤-TreeItem-tip-i₁-i = &&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅

    lemma₁ : ≤-Lists (flatten (tip i₁)) (flatten t₂₁)
    lemma₁ = flatten-OrdList-helper (ttip Ni₁) Ni Tt₂₁ OT
      where
        OrdTree-t₂₁ : OrdTree t₂₁
        OrdTree-t₂₁ =
          leftSubTree-OrdTree Tt₂₁ Ni₂ Tt₂₂ (&&-list₄-t₂ helper₁ helper₂ helper₃
                                                         helper₄ helper₅)

        ≤-ItemTree-i-t₂₁ : ≤-ItemTree i t₂₁
        ≤-ItemTree-i-t₂₁ = &&-list₂-t₁ helper₆ helper₇ helper₈

        OT : OrdTree (node (tip i₁) i t₂₁)
        OT = ordTree (node (tip i₁) i t₂₁)
               ≡⟨ ordTree-node (tip i₁) i t₂₁ ⟩
             ordTree (tip i₁) &&
             ordTree t₂₁ &&
             le-TreeItem (tip i₁) i &&
             le-ItemTree i t₂₁
               ≡⟨ subst₄ (λ w x y z → ordTree (tip i₁) &&
                                      ordTree t₂₁ &&
                                      le-TreeItem (tip i₁) i &&
                                      le-ItemTree i t₂₁ ≡
                                      w && x && y && z)
                         OrdTree-tip-i₁
                         OrdTree-t₂₁
                         ≤-TreeItem-tip-i₁-i
                         ≤-ItemTree-i-t₂₁
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true ∎

    lemma₂ : ≤-Lists (flatten (tip i₁)) (flatten t₂₂)
    lemma₂ = flatten-OrdList-helper (ttip Ni₁) Ni Tt₂₂ OT
      where
        OrdTree-t₂₂ : OrdTree t₂₂
        OrdTree-t₂₂ =
          rightSubTree-OrdTree Tt₂₁ Ni₂ Tt₂₂ (&&-list₄-t₂ helper₁ helper₂ helper₃
                                                          helper₄ helper₅)

        ≤-ItemTree-i-t₂₂ : ≤-ItemTree i t₂₂
        ≤-ItemTree-i-t₂₂ = &&-list₂-t₂ helper₆ helper₇ helper₈

        OT : OrdTree (node (tip i₁) i t₂₂)
        OT = ordTree (node (tip i₁) i t₂₂)
               ≡⟨ ordTree-node (tip i₁) i t₂₂ ⟩
             ordTree (tip i₁) &&
             ordTree t₂₂ &&
             le-TreeItem (tip i₁) i &&
             le-ItemTree i t₂₂
               ≡⟨ subst₄ (λ w x y z → ordTree (tip i₁) &&
                                      ordTree t₂₂ &&
                                      le-TreeItem (tip i₁) i &&
                                      le-ItemTree i t₂₂ ≡
                                      w && x && y && z)
                         OrdTree-tip-i₁
                         OrdTree-t₂₂
                         ≤-TreeItem-tip-i₁-i
                         ≤-ItemTree-i-t₂₂
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true ∎

flatten-OrdList-helper {i = i} (tnode {t₁₁} {i₁} {t₁₂} Tt₁₁ Ni₁ Tt₁₂) Ni tnil OTt =
  le-Lists (flatten (node t₁₁ i₁ t₁₂)) (flatten nil)
    ≡⟨ subst (λ x → le-Lists (flatten (node t₁₁ i₁ t₁₂)) (flatten nil) ≡
                    le-Lists x                           (flatten nil))
             (flatten-node t₁₁ i₁ t₁₂)
             refl
    ⟩
  le-Lists (flatten t₁₁ ++  flatten t₁₂) (flatten nil)
    ≡⟨ xs≤zs→ys≤zs→xs++ys≤zs (flatten-ListN Tt₁₁)
                             (flatten-ListN Tt₁₂)
                             (flatten-ListN tnil)
                             lemma₁
                             lemma₂
    ⟩
  true ∎
  where
    -- Helper terms to get the conjuncts from OTt.
    helper₁ = ordTree-Bool (tnode Tt₁₁ Ni₁ Tt₁₂)
    helper₂ = ordTree-Bool tnil
    helper₃ = le-TreeItem-Bool (tnode Tt₁₁ Ni₁ Tt₁₂) Ni
    helper₄ = le-ItemTree-Bool Ni tnil
    helper₅ = trans (sym (ordTree-node (node t₁₁ i₁ t₁₂) i nil)) OTt

    -- Helper terms to get the conjuncts from the third conjunct of OTt.
    helper₆ = le-TreeItem-Bool Tt₁₁ Ni
    helper₇ = le-TreeItem-Bool Tt₁₂ Ni
    helper₈ = trans (sym (le-TreeItem-node t₁₁ i₁ t₁₂ i))
                    (&&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅)

    -- Common terms for the lemma₁ and lemma₂.
    ≤-ItemTree-i-niltree : ≤-ItemTree i nil
    ≤-ItemTree-i-niltree = &&-list₄-t₄ helper₁ helper₂ helper₃ helper₄ helper₅

    lemma₁ : ≤-Lists (flatten t₁₁) (flatten nil)
    lemma₁ = flatten-OrdList-helper Tt₁₁ Ni tnil OT
      where
        OrdTree-t₁₁ : OrdTree t₁₁
        OrdTree-t₁₁ =
          leftSubTree-OrdTree Tt₁₁ Ni₁ Tt₁₂ (&&-list₄-t₁ helper₁ helper₂ helper₃
                                                         helper₄ helper₅)

        ≤-TreeItem-t₁₁-i : ≤-TreeItem t₁₁ i
        ≤-TreeItem-t₁₁-i = &&-list₂-t₁ helper₆ helper₇ helper₈

        OT : OrdTree (node t₁₁ i nil)
        OT = ordTree (node t₁₁ i nil)
               ≡⟨ ordTree-node t₁₁ i nil ⟩
             ordTree t₁₁ &&
             ordTree nil &&
             le-TreeItem t₁₁ i &&
             le-ItemTree i nil
               ≡⟨ subst₄ (λ w x y z → ordTree t₁₁ &&
                                      ordTree nil &&
                                      le-TreeItem t₁₁ i &&
                                      le-ItemTree i nil ≡
                                      w && x && y && z)
                         OrdTree-t₁₁
                         ordTree-nil
                         ≤-TreeItem-t₁₁-i
                         ≤-ItemTree-i-niltree
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true ∎

    lemma₂ : ≤-Lists (flatten t₁₂) (flatten nil)
    lemma₂ = flatten-OrdList-helper Tt₁₂ Ni tnil OT
      where
        OrdTree-t₁₂ : OrdTree t₁₂
        OrdTree-t₁₂ =
          rightSubTree-OrdTree Tt₁₁ Ni₁ Tt₁₂ (&&-list₄-t₁ helper₁ helper₂ helper₃
                                                          helper₄ helper₅)

        ≤-TreeItem-t₁₂-i : ≤-TreeItem t₁₂ i
        ≤-TreeItem-t₁₂-i = &&-list₂-t₂ helper₆ helper₇ helper₈

        OT : OrdTree (node t₁₂ i nil)
        OT = ordTree (node t₁₂ i nil)
              ≡⟨ ordTree-node t₁₂ i nil ⟩
             ordTree t₁₂ &&
             ordTree nil &&
             le-TreeItem t₁₂ i &&
             le-ItemTree i nil
               ≡⟨ subst₄ (λ w x y z → ordTree t₁₂ &&
                                      ordTree nil &&
                                      le-TreeItem t₁₂ i &&
                                      le-ItemTree i nil ≡
                                      w && x && y && z)
                         OrdTree-t₁₂
                         ordTree-nil
                         ≤-TreeItem-t₁₂-i
                         ≤-ItemTree-i-niltree
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true ∎

flatten-OrdList-helper {i = i} (tnode {t₁₁} {i₁} {t₁₂} Tt₁₁ Ni₁ Tt₁₂) Ni
                       (ttip {i₂} Ni₂) OTt =
  le-Lists (flatten (node t₁₁ i₁ t₁₂)) (flatten (tip i₂))
    ≡⟨ subst (λ x → le-Lists (flatten (node t₁₁ i₁ t₁₂)) (flatten (tip i₂)) ≡
                    le-Lists x                           (flatten (tip i₂)))
             (flatten-node t₁₁ i₁ t₁₂)
             refl
    ⟩
  le-Lists (flatten t₁₁ ++  flatten t₁₂) (flatten (tip i₂))
    ≡⟨ xs≤zs→ys≤zs→xs++ys≤zs (flatten-ListN Tt₁₁)
                             (flatten-ListN Tt₁₂)
                             (flatten-ListN (ttip Ni₂))
                             lemma₁
                             lemma₂
    ⟩
  true ∎
  where
    -- Helper terms to get the conjuncts from OTt.
    helper₁ = ordTree-Bool (tnode Tt₁₁ Ni₁ Tt₁₂)
    helper₂ = ordTree-Bool (ttip Ni₂)
    helper₃ = le-TreeItem-Bool (tnode Tt₁₁ Ni₁ Tt₁₂) Ni
    helper₄ = le-ItemTree-Bool Ni (ttip Ni₂)
    helper₅ = trans (sym (ordTree-node (node t₁₁ i₁ t₁₂) i (tip i₂))) OTt

    -- Helper terms to get the conjuncts from the third conjunct of OTt.
    helper₆ = le-TreeItem-Bool Tt₁₁ Ni
    helper₇ = le-TreeItem-Bool Tt₁₂ Ni
    helper₈ = trans (sym (le-TreeItem-node t₁₁ i₁ t₁₂ i))
                    (&&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅)

    -- Common terms for the lemma₁ and lemma₂.
    OrdTree-tip-i₂ : OrdTree (tip i₂)
    OrdTree-tip-i₂ = &&-list₄-t₂ helper₁ helper₂ helper₃ helper₄ helper₅

    ≤-ItemTree-i-tip-i₂ : ≤-ItemTree i (tip i₂)
    ≤-ItemTree-i-tip-i₂ = &&-list₄-t₄ helper₁ helper₂ helper₃ helper₄ helper₅

    lemma₁ : ≤-Lists (flatten t₁₁) (flatten (tip i₂))
    lemma₁ = flatten-OrdList-helper Tt₁₁ Ni (ttip Ni₂) OT
      where
        OrdTree-t₁₁ : OrdTree t₁₁
        OrdTree-t₁₁ =
          leftSubTree-OrdTree Tt₁₁ Ni₁ Tt₁₂ (&&-list₄-t₁ helper₁ helper₂ helper₃
                                                         helper₄ helper₅)

        ≤-TreeItem-t₁₁-i : ≤-TreeItem t₁₁ i
        ≤-TreeItem-t₁₁-i = &&-list₂-t₁ helper₆ helper₇ helper₈

        OT : OrdTree (node t₁₁ i (tip i₂))
        OT = ordTree (node t₁₁ i (tip i₂))
               ≡⟨ ordTree-node t₁₁ i (tip i₂) ⟩
             ordTree t₁₁ &&
             ordTree (tip i₂) &&
             le-TreeItem t₁₁ i &&
             le-ItemTree i (tip i₂)
               ≡⟨ subst₄ (λ w x y z → ordTree t₁₁ &&
                                      ordTree (tip i₂) &&
                                      le-TreeItem t₁₁ i &&
                                      le-ItemTree i (tip i₂) ≡
                                      w && x && y && z)
                         OrdTree-t₁₁
                         OrdTree-tip-i₂
                         ≤-TreeItem-t₁₁-i
                         ≤-ItemTree-i-tip-i₂
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true ∎

    lemma₂ : ≤-Lists (flatten t₁₂) (flatten (tip i₂))
    lemma₂ = flatten-OrdList-helper Tt₁₂ Ni (ttip Ni₂) OT
      where
        OrdTree-t₁₂ : OrdTree t₁₂
        OrdTree-t₁₂ =
          rightSubTree-OrdTree Tt₁₁ Ni₁ Tt₁₂ (&&-list₄-t₁ helper₁ helper₂ helper₃
                                                          helper₄ helper₅)

        ≤-TreeItem-t₁₂-i : ≤-TreeItem t₁₂ i
        ≤-TreeItem-t₁₂-i = &&-list₂-t₂ helper₆ helper₇ helper₈

        OT : OrdTree (node t₁₂ i (tip i₂))
        OT = ordTree (node t₁₂ i (tip i₂))
               ≡⟨ ordTree-node t₁₂ i (tip i₂) ⟩
             ordTree t₁₂ &&
             ordTree (tip i₂) &&
             le-TreeItem t₁₂ i &&
             le-ItemTree i (tip i₂)
               ≡⟨ subst₄ (λ w x y z → ordTree t₁₂ &&
                                      ordTree (tip i₂) &&
                                      le-TreeItem t₁₂ i &&
                                      le-ItemTree i (tip i₂) ≡
                                      w && x && y && z)
                         OrdTree-t₁₂
                         OrdTree-tip-i₂
                         ≤-TreeItem-t₁₂-i
                         ≤-ItemTree-i-tip-i₂
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true ∎

flatten-OrdList-helper {i = i} (tnode {t₁₁} {i₁} {t₁₂} Tt₁₁ Ni₁ Tt₁₂) Ni
                       (tnode {t₂₁} {i₂} {t₂₂} Tt₂₁ Ni₂ Tt₂₂) OTt =
  le-Lists (flatten (node t₁₁ i₁ t₁₂)) (flatten (node t₂₁ i₂ t₂₂))
    ≡⟨ subst (λ x → le-Lists (flatten (node t₁₁ i₁ t₁₂))
                            (flatten (node t₂₁ i₂ t₂₂)) ≡
                    le-Lists x (flatten (node t₂₁ i₂ t₂₂)))
             (flatten-node t₁₁ i₁ t₁₂)
             refl
    ⟩
  le-Lists (flatten t₁₁ ++  flatten t₁₂) (flatten (node t₂₁ i₂ t₂₂))
    ≡⟨ xs≤zs→ys≤zs→xs++ys≤zs (flatten-ListN Tt₁₁)
                             (flatten-ListN Tt₁₂)
                             (flatten-ListN (tnode Tt₂₁ Ni₂ Tt₂₂))
                             lemma₁
                             lemma₂
    ⟩
  true ∎
  where
    -- Helper terms to get the conjuncts from OTt.
    helper₁ = ordTree-Bool (tnode Tt₁₁ Ni₁ Tt₁₂)
    helper₂ = ordTree-Bool (tnode Tt₂₁ Ni₂ Tt₂₂)
    helper₃ = le-TreeItem-Bool (tnode Tt₁₁ Ni₁ Tt₁₂) Ni
    helper₄ = le-ItemTree-Bool Ni (tnode Tt₂₁ Ni₂ Tt₂₂)
    helper₅ = trans (sym (ordTree-node (node t₁₁ i₁ t₁₂) i (node t₂₁ i₂ t₂₂))) OTt

    -- Helper terms to get the conjuncts from the third conjunct of OTt.
    helper₆ = le-TreeItem-Bool Tt₁₁ Ni
    helper₇ = le-TreeItem-Bool Tt₁₂ Ni
    helper₈ = trans (sym (le-TreeItem-node t₁₁ i₁ t₁₂ i))
                    (&&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅)

    -- Common terms for the lemma₁ and lemma₂.
    OrdTree-node-t₂₁-i₂-t₂₂ : OrdTree (node t₂₁ i₂ t₂₂)
    OrdTree-node-t₂₁-i₂-t₂₂ = &&-list₄-t₂ helper₁ helper₂ helper₃ helper₄ helper₅

    ≤-ItemTree-i-node-t₂₁-i₂-t₂₂ : ≤-ItemTree i (node t₂₁ i₂ t₂₂)
    ≤-ItemTree-i-node-t₂₁-i₂-t₂₂ = &&-list₄-t₄ helper₁ helper₂ helper₃ helper₄
                                                helper₅

    lemma₁ : ≤-Lists (flatten t₁₁) (flatten (node t₂₁ i₂ t₂₂))
    lemma₁ = flatten-OrdList-helper Tt₁₁ Ni (tnode Tt₂₁ Ni₂ Tt₂₂) OT
      where
        OrdTree-t₁₁ : OrdTree t₁₁
        OrdTree-t₁₁ =
          leftSubTree-OrdTree Tt₁₁ Ni₁ Tt₁₂ (&&-list₄-t₁ helper₁ helper₂ helper₃
                                                         helper₄ helper₅)

        ≤-TreeItem-t₁₁-i : ≤-TreeItem t₁₁ i
        ≤-TreeItem-t₁₁-i = &&-list₂-t₁ helper₆ helper₇ helper₈

        OT : OrdTree (node t₁₁ i (node t₂₁ i₂ t₂₂))
        OT = ordTree (node t₁₁ i (node t₂₁ i₂ t₂₂))
               ≡⟨ ordTree-node t₁₁ i (node t₂₁ i₂ t₂₂) ⟩
             ordTree t₁₁ &&
             ordTree (node t₂₁ i₂ t₂₂) &&
             le-TreeItem t₁₁ i &&
             le-ItemTree i (node t₂₁ i₂ t₂₂)
               ≡⟨ subst₄ (λ w x y z → ordTree t₁₁ &&
                                      ordTree (node t₂₁ i₂ t₂₂) &&
                                      le-TreeItem t₁₁ i &&
                                      le-ItemTree i (node t₂₁ i₂ t₂₂) ≡
                                      w && x && y && z)
                         OrdTree-t₁₁
                         OrdTree-node-t₂₁-i₂-t₂₂
                         ≤-TreeItem-t₁₁-i
                         ≤-ItemTree-i-node-t₂₁-i₂-t₂₂
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true ∎

    lemma₂ : ≤-Lists (flatten t₁₂) (flatten (node t₂₁ i₂ t₂₂))
    lemma₂ = flatten-OrdList-helper Tt₁₂ Ni (tnode Tt₂₁ Ni₂ Tt₂₂) OT
      where
        OrdTree-t₁₂ : OrdTree t₁₂
        OrdTree-t₁₂ =
          rightSubTree-OrdTree Tt₁₁ Ni₁ Tt₁₂ (&&-list₄-t₁ helper₁ helper₂ helper₃
                                                          helper₄ helper₅)

        ≤-TreeItem-t₁₂-i : ≤-TreeItem t₁₂ i
        ≤-TreeItem-t₁₂-i = &&-list₂-t₂ helper₆ helper₇ helper₈

        OT : OrdTree (node t₁₂ i (node t₂₁ i₂ t₂₂))
        OT = ordTree (node t₁₂ i (node t₂₁ i₂ t₂₂))
               ≡⟨ ordTree-node t₁₂ i (node t₂₁ i₂ t₂₂) ⟩
             ordTree t₁₂ &&
             ordTree (node t₂₁ i₂ t₂₂) &&
             le-TreeItem t₁₂ i &&
             le-ItemTree i (node t₂₁ i₂ t₂₂)
               ≡⟨ subst₄ (λ w x y z → ordTree t₁₂ &&
                                      ordTree (node t₂₁ i₂ t₂₂) &&
                                      le-TreeItem t₁₂ i &&
                                      le-ItemTree i (node t₂₁ i₂ t₂₂) ≡
                                      w && x && y && z)
                         OrdTree-t₁₂
                         OrdTree-node-t₂₁-i₂-t₂₂
                         ≤-TreeItem-t₁₂-i
                         ≤-ItemTree-i-node-t₂₁-i₂-t₂₂
                         refl
             ⟩
             true && true && true && true
               ≡⟨ &&-list₄-all-t btrue btrue btrue btrue (refl , refl , refl , refl) ⟩
             true
           ∎


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion from naturals to universe levels
------------------------------------------------------------------------

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

module Level.Literals where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.FromNat
open import Agda.Builtin.Unit
open import Level using (Level; 0ℓ)

-- Increase a Level by a number of sucs.

_ℕ+_ : ℕ → Level → Level
zero  ℕ+ ℓ = ℓ
suc n ℕ+ ℓ = Level.suc (n ℕ+ ℓ)

-- Nat-computed Level.

infix 10 #_

#_ : ℕ → Level
#_ = _ℕ+ 0ℓ

-- Literal overloading for levels.

Levelℕ : Number Level
Levelℕ .Number.Constraint _ = ⊤
Levelℕ .Number.fromNat    n = # n


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by posets
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.Poset
   {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where

open Poset P renaming (Carrier to A)

open import Function using (flip)
import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
import Relation.Binary.Properties.Preorder preorder as PreorderProperties
open import Relation.Nullary using (¬_)

private
  _≉_ : Rel A p₂
  x ≉ y = ¬ (x ≈ y)

------------------------------------------------------------------------
-- The _≥_ relation is also a poset.

infix 4 _≥_

_≥_ : Rel A p₃
x ≥ y = y ≤ x

open PreorderProperties public
  using ()
  renaming
  ( invIsPreorder to ≥-isPreorder
  ; invPreorder   to ≥-preorder
  )

≥-isPartialOrder : IsPartialOrder _≈_ _≥_
≥-isPartialOrder = record
  { isPreorder   = PreorderProperties.invIsPreorder
  ; antisym      = flip antisym
  }

≥-poset : Poset p₁ p₂ p₃
≥-poset = record
  { isPartialOrder = ≥-isPartialOrder
  }

open Poset ≥-poset public
  using ()
  renaming
  ( refl      to ≥-refl
  ; reflexive to ≥-reflexive
  ; trans     to ≥-trans
  ; antisym   to ≥-antisym
  )

------------------------------------------------------------------------
-- Partial orders can be turned into strict partial orders

infix 4 _<_

_<_ : Rel A _
_<_ = ToStrict._<_

<-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
<-isStrictPartialOrder = ToStrict.<-isStrictPartialOrder isPartialOrder

<-strictPartialOrder : StrictPartialOrder _ _ _
<-strictPartialOrder = record
  { isStrictPartialOrder = <-isStrictPartialOrder
  }

open StrictPartialOrder <-strictPartialOrder public
  using ( <-resp-≈; <-respʳ-≈; <-respˡ-≈)
  renaming
  ( irrefl to <-irrefl
  ; asym   to <-asym
  ; trans  to <-trans
  )

<⇒≉ : ∀ {x y} → x < y → x ≉ y
<⇒≉ = ToStrict.<⇒≉

≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
≤∧≉⇒< = ToStrict.≤∧≉⇒<

<⇒≱ : ∀ {x y} → x < y → ¬ (y ≤ x)
<⇒≱ = ToStrict.<⇒≱ antisym

≤⇒≯ : ∀ {x y} → x ≤ y → ¬ (y < x)
≤⇒≯ = ToStrict.≤⇒≯ antisym

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.2

invIsPartialOrder = ≥-isPartialOrder
{-# WARNING_ON_USAGE invIsPartialOrder
"Warning: invIsPartialOrder was deprecated in v1.2.
Please use ≥-isPartialOrder instead."
#-}

invPoset = ≥-poset
{-# WARNING_ON_USAGE invPoset
"Warning: invPoset was deprecated in v1.2.
Please use ≥-poset instead."
#-}

strictPartialOrder = <-strictPartialOrder
{-# WARNING_ON_USAGE strictPartialOrder
"Warning: strictPartialOrder was deprecated in v1.2.
Please use <-strictPartialOrder instead."
#-}


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

module Cubical.Structures.Poset where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv        hiding   (_■)
open import Cubical.Foundations.SIP          renaming (SNS-≡ to SNS)
open import Cubical.Core.Primitives
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Sigma.Properties

-- We will adopt the convention of denoting the level of the carrier
-- set by ℓ₀ and the level of the relation result by ℓ₁.
private
  variable
    ℓ₀ ℓ₁ : Level

Order : (ℓ₁ : Level) → Type ℓ₀ → Type (ℓ-max ℓ₀ (ℓ-suc ℓ₁))
Order ℓ₁ A = A → A → hProp ℓ₁

order-iso : (M N : Σ (Type ℓ₀) (Order ℓ₁)) →  fst M ≃ fst N → Type (ℓ-max ℓ₀ ℓ₁)
order-iso (A , _⊑₀_) (B , _⊑₁_) (f , _) = (x y : A) → [ x ⊑₀ y ⇔ f x ⊑₁ f y ]

isSetOrder : (ℓ₁ : Level) (A : Type ℓ₀) → isSet (Order ℓ₁ A)
isSetOrder ℓ₁ A = isSetΠ2 λ _ _ → isSetHProp

Order-is-SNS : SNS {ℓ₀} (Order ℓ₁) order-iso
Order-is-SNS {ℓ₁ = ℓ₁} {X = X}  _⊑₀_ _⊑₁_ = f , f-equiv
  where
    f : order-iso (X , _⊑₀_) (X , _⊑₁_) (idEquiv X) → _⊑₀_ ≡ _⊑₁_
    f i = funExt λ x → funExt λ y → ⇔toPath (fst (i x y)) (snd (i x y))

    ⇔-prop : isProp ((x y : X) → [ x ⊑₀ y ⇔ x ⊑₁ y ])
    ⇔-prop = isPropΠ2 λ x y → snd (x ⊑₀ y ⇔ x ⊑₁ y)

    f-equiv : isEquiv f
    f-equiv = record { equiv-proof = λ eq → (g eq , sec eq) , h eq }
      where
        g : (eq : _⊑₀_ ≡ _⊑₁_)
          → (x y : X)
          → ([ x ⊑₀ y ] → [ x ⊑₁ y ]) × ([ x ⊑₁ y ] → [ x ⊑₀ y ])
        g eq x y = subst (λ { _⊑⋆_ → [ x ⊑⋆ y ] }) eq
                 , subst (λ { _⊑⋆_ → [ x ⊑⋆ y ] }) (sym eq)

        sec : section f g
        sec p = isSetOrder _ X _⊑₀_ _⊑₁_ (f (g p)) p

        h : (p : _⊑₀_ ≡ _⊑₁_) → (fib : fiber f p) → (g p , sec p) ≡ fib
        h p (i , _) = ΣProp≡ A-prop B-prop
          where
            A-prop = λ i′ → isOfHLevelSuc 2 (isSetOrder ℓ₁ X) _⊑₀_ _⊑₁_ (f i′) p
            B-prop = ⇔-prop (g p) i

-- We now write down the axioms for a partial order.

isReflexive : {A : Type ℓ₀} → Order ℓ₁ A → hProp (ℓ-max ℓ₀ ℓ₁)
isReflexive {A = X} _⊑_ = ((x : X) → [ x ⊑ x ]) , isPropΠ λ x → snd (x ⊑ x)

isTransitive : {A : Type ℓ₀} → Order ℓ₁ A → hProp (ℓ-max ℓ₀ ℓ₁)
isTransitive {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} {A = X} _⊑_ = φ , φ-prop
  where
    φ      : Type (ℓ-max ℓ₀ ℓ₁)
    φ      = ((x y z : X) → [ x ⊑ y ⇒ y ⊑ z ⇒ x ⊑ z ])
    φ-prop : isProp φ
    φ-prop = isPropΠ3 λ x y z → snd (x ⊑ y ⇒ y ⊑ z ⇒ x ⊑ z)

isAntisym : {A : Type ℓ₀} → isSet A → Order ℓ₁ A → hProp (ℓ-max ℓ₀ ℓ₁)
isAntisym {ℓ₀ = ℓ₀} {ℓ₁ = ℓ₁} {A = X} A-set _⊑_ = φ , φ-prop
  where
    φ      : Type (ℓ-max ℓ₀ ℓ₁)
    φ      = ((x y : X) → [ x ⊑ y ] → [ y ⊑ x ] → x ≡ y)
    φ-prop : isProp φ
    φ-prop = isPropΠ3 λ x y z → isPropΠ λ _ → A-set x y

-- The predicate expressing that a given order satisfies the partial order
-- axioms.
satPosetAx : (ℓ₁ : Level) (A : Type ℓ₀) → Order ℓ₁ A → hProp (ℓ-max ℓ₀ ℓ₁)
satPosetAx {ℓ₀ = ℓ₀} ℓ₁ A _⊑_ = φ , φ-prop
  where
    isPartial : isSet A → hProp (ℓ-max ℓ₀ ℓ₁)
    isPartial A-set = isReflexive _⊑_ ⊓ isTransitive _⊑_ ⊓ isAntisym A-set _⊑_

    φ         = Σ[ A-set ∈ isSet A ] [ isPartial A-set ]
    φ-prop    = isOfHLevelΣ 1 isPropIsSet (λ x → snd (isPartial x))

-- The poset structure.
PosetStr : (ℓ₁ : Level) → Type ℓ₀ → Type (ℓ-max ℓ₀ (ℓ-suc ℓ₁))
PosetStr ℓ₁ = add-to-structure (Order ℓ₁) λ A _⊑_ → [ satPosetAx ℓ₁ A _⊑_ ]

PosetStr-set : (ℓ₁ : Level) (A : Type ℓ₀) → isSet (PosetStr ℓ₁ A)
PosetStr-set ℓ₁ A =
  isSetΣ
    (isSetΠ2 λ _ _ → isSetHProp) λ _⊑_ →
      isProp→isSet (snd (satPosetAx ℓ₁ A _⊑_))

Poset : (ℓ₀ ℓ₁ : Level) → Type (ℓ-max (ℓ-suc ℓ₀) (ℓ-suc ℓ₁))
Poset ℓ₀ ℓ₁ = TypeWithStr ℓ₀ (PosetStr ℓ₁)

-- Some projections for syntactic convenience.

-- Carrier set of a poset.
∣_∣ₚ : Poset ℓ₀ ℓ₁ → Type ℓ₀
∣ X , _ ∣ₚ = X

strₚ : (P : Poset ℓ₀ ℓ₁) → PosetStr ℓ₁ ∣ P ∣ₚ
strₚ (_ , s) = s

rel : (P : Poset ℓ₀ ℓ₁) → ∣ P ∣ₚ → ∣ P ∣ₚ → hProp ℓ₁
rel (_ , _⊑_ , _) = _⊑_

syntax rel P x y = x ⊑[ P ] y

⊑[_]-refl : (P : Poset ℓ₀ ℓ₁) → (x : ∣ P ∣ₚ) → [ x ⊑[ P ] x ]
⊑[_]-refl (_ , _ , _ , ⊑-refl , _) = ⊑-refl

⊑[_]-trans : (P : Poset ℓ₀ ℓ₁) (x y z : ∣ P ∣ₚ)
           → [ x ⊑[ P ] y ] → [ y ⊑[ P ] z ] → [ x ⊑[ P ] z ]
⊑[_]-trans (_ , _ , _ , _ , ⊑-trans , _) = ⊑-trans

⊑[_]-antisym : (P : Poset ℓ₀ ℓ₁) (x y : ∣ P ∣ₚ)
             → [ x ⊑[ P ] y ] → [ y ⊑[ P ] x ] → x ≡ y
⊑[_]-antisym (_ , _ , _ , _ , _ , ⊑-antisym) = ⊑-antisym

carrier-is-set : (P : Poset ℓ₀ ℓ₁) → isSet ∣ P ∣ₚ
carrier-is-set (_ , _ , is-set , _) = is-set

module PosetReasoning (P : Poset ℓ₀ ℓ₁) where

  _⊑⟨_⟩_ : (x : ∣ P ∣ₚ) {y z : ∣ P ∣ₚ}
         → [ x ⊑[ P ] y ] → [ y ⊑[ P ] z ] → [ x ⊑[ P ] z ]
  _ ⊑⟨ p ⟩ q = ⊑[ P ]-trans _ _ _ p q

  _■ : (x : ∣ P ∣ₚ) → [ x ⊑[ P ] x ]
  _■ = ⊑[ P ]-refl

  infixr 0 _⊑⟨_⟩_
  infix  1 _■

-- Poset univalence.
RP-iso-prop : (P Q : Σ (Type ℓ₀) (Order ℓ₁))
            → (eqv : fst P ≃ fst Q) → isProp (order-iso P Q eqv)
RP-iso-prop (A , _⊑₀_) (B , _⊑₁_) (f , _) =
  isPropΠ2 λ x y → snd (x ⊑₀ y ⇔ f x ⊑₁ f y)

poset-iso : (P Q : Poset ℓ₀ ℓ₁) → ∣ P ∣ₚ ≃ ∣ Q ∣ₚ → Type (ℓ-max ℓ₀ ℓ₁)
poset-iso {ℓ₁ = ℓ₁} = add-to-iso order-iso (λ A _⊑_ → [ satPosetAx ℓ₁ A _⊑_ ])

-- We collect poset isomorphisms in the following type.
_≃ₚ_ : Poset ℓ₀ ℓ₁ → Poset ℓ₀ ℓ₁ → Type (ℓ-max ℓ₀ ℓ₁)
_≃ₚ_ P Q = Σ[ i ∈ (∣ P ∣ₚ ≃ ∣ Q ∣ₚ) ] poset-iso P Q i

poset-ax-props : (A : Type ℓ₀) (str : Order ℓ₁ A)
                   → isProp [ satPosetAx ℓ₁ A str ]
poset-ax-props {ℓ₁ = ℓ₁} A str = snd (satPosetAx ℓ₁ A str)

poset-is-SNS : SNS {ℓ₀} (PosetStr ℓ₁) poset-iso
poset-is-SNS {ℓ₁ = ℓ₁} =
    SNS-PathP→SNS-≡ _ poset-iso (add-axioms-SNS _ poset-ax-props isSNS-PathP)
  where
    isSNS-PathP : SNS-PathP (Order ℓ₁) order-iso
    isSNS-PathP = SNS-≡→SNS-PathP order-iso Order-is-SNS

poset-is-SNS-PathP : SNS-PathP {ℓ₀} (PosetStr ℓ₁) poset-iso
poset-is-SNS-PathP = SNS-≡→SNS-PathP poset-iso poset-is-SNS

poset-SIP : (A : Type ℓ₀) (B : Type ℓ₀) (eqv : A ≃ B)
            (P : PosetStr ℓ₁ A) (Q : PosetStr ℓ₁ B)
          → poset-iso (A , P) (B , Q) eqv
          → (A , P) ≡ (B , Q)
poset-SIP {ℓ₁ = ℓ₁} A B eqv P Q i = φ (eqv , i)
  where
    φ : (A , P) ≃[ poset-iso ] (B , Q) → (A , P) ≡ (B , Q)
    φ = equivFun (SIP poset-is-SNS-PathP (A , P) (B , Q))

≃ₚ→≡ : (P Q : Poset ℓ₀ ℓ₁) → P ≃ₚ Q → P ≡ Q
≃ₚ→≡ (A , A-pos) (B , B-pos) (eqv , i) = poset-SIP A B eqv A-pos B-pos i


text:
-- An ATP axiom must be used with postulates or data constructors.

-- This error is detected by TypeChecking.Rules.Decl.

module ATPBadAxiom where

foo : Set → Set
foo A = A
{-# ATP axiom foo #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text: open import Issue623.A


text:
open import FRP.JS.Nat using ( ℕ )
open import FRP.JS.String using ( String )

module FRP.JS.Geolocation.Distance where

postulate
  Distance : Set
  _m : ℕ → Distance
  toString : Distance → String

{-# COMPILED_JS _m function(x) { return x; } #-}
{-# COMPILED_JS toString function(x) { return x.toString(); } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Using do-notation to implement a type checker for simply-typed
-- lambda-calculus.
module _ where

open import Agda.Builtin.Nat hiding (_==_)
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.String

-- Preliminaries --

--- Decidable equality ---

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

data Dec (P : Set) : Set where
  yes : P → Dec P
  no  : ¬ P → Dec P

record Eq (A : Set) : Set where
  field _==_ : (x y : A) → Dec (x ≡ y)

open Eq {{...}}

--- Functors, Applicatives, and Monads ---

record Functor (F : Set → Set) : Set₁ where
  field fmap : ∀ {A B} → (A → B) → F A → F B

open Functor {{...}}

record Applicative (F : Set → Set) : Set₁ where
  field
    pure : ∀ {A} → A → F A
    _<*>_ : ∀ {A B} → F (A → B) → F A → F B
    overlap {{super}} : Functor F

open Applicative {{...}}

record Monad (M : Set → Set) : Set₁ where
  field
    _>>=_ : ∀ {A B} → M A → (A → M B) → M B
    overlap {{super}} : Applicative M
  _>>_ : ∀ {A B} → M A → M B → M B
  m >> m' = m >>= λ _ → m'

open Monad {{...}}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

instance
  FunctorMaybe : Functor Maybe
  fmap {{FunctorMaybe}} f nothing  = nothing
  fmap {{FunctorMaybe}} f (just x) = just (f x)

  ApplicativeMaybe : Applicative Maybe
  pure  {{ApplicativeMaybe}} = just
  _<*>_ {{ApplicativeMaybe}} nothing  _        = nothing
  _<*>_ {{ApplicativeMaybe}} (just _) nothing  = nothing
  _<*>_ {{ApplicativeMaybe}} (just f) (just x) = just (f x)

  MonadMaybe : Monad Maybe
  _>>=_ {{MonadMaybe}} nothing  f = nothing
  _>>=_ {{MonadMaybe}} (just x) f = f x

--- List membership ---

infix 2 _∈_
data _∈_ {A : Set} (x : A) : List A → Set where
  zero : ∀ {xs} → x ∈ x ∷ xs
  suc  : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs

rawIndex : ∀ {A} {x : A} {xs} → x ∈ xs → Nat
rawIndex zero    = zero
rawIndex (suc i) = suc (rawIndex i)

-- Simply typed λ-calculus --

infixr 7 _=>_
data Type : Set where
  nat : Type
  _=>_ : Type → Type → Type

--- Decidable equality for Type ---
private
  =>-inj₁ : ∀ {σ₁ σ₂ τ₁ τ₂} → (σ₁ => τ₁) ≡ (σ₂ => τ₂) → σ₁ ≡ σ₂
  =>-inj₁ refl = refl

  =>-inj₂ : ∀ {σ₁ σ₂ τ₁ τ₂} → σ₁ => τ₁ ≡ σ₂ => τ₂ → τ₁ ≡ τ₂
  =>-inj₂ refl = refl

instance
  EqType : Eq Type
  _==_ {{EqType}} nat nat = yes refl
  _==_ {{EqType}} nat (τ => τ₁) = no λ()
  _==_ {{EqType}} (σ => σ₁) nat = no λ()
  _==_ {{EqType}} (σ => σ₁) (τ => τ₁) with σ == τ | σ₁ == τ₁
  ... | yes refl | yes refl = yes refl
  ... | yes refl | no neq   = no λ eq → neq (=>-inj₂ eq)
  ... | no neq   | _        = no λ eq → neq (=>-inj₁ eq)

--- Raw terms ---
data Expr : Set where
  var : Nat → Expr
  app : Expr → Expr → Expr
  lam : Type → Expr → Expr
  lit : Nat → Expr
  suc : Expr

--- Well-typed terms ---
Context = List Type

data Term (Γ : Context) : Type → Set where
  var : ∀ {τ} (x : τ ∈ Γ) → Term Γ τ
  app : ∀ {σ τ} (s : Term Γ (σ => τ)) (t : Term Γ σ) → Term Γ τ
  lam : ∀ σ {τ} (t : Term (σ ∷ Γ) τ) → Term Γ (σ => τ)
  lit : (n : Nat) → Term Γ nat
  suc : Term Γ (nat => nat)

--- Erasing types ---
forgetTypes : ∀ {Γ τ} → Term Γ τ → Expr
forgetTypes (var x)   = var (rawIndex x)
forgetTypes (app s t) = app (forgetTypes s) (forgetTypes t)
forgetTypes (lam σ t) = lam σ (forgetTypes t)
forgetTypes (lit n)   = lit n
forgetTypes suc       = suc

--- Type checking ---

TC = Maybe

typeError : ∀ {A} → TC A
typeError = nothing

data WellTyped (Γ : Context) (e : Expr) : Set where
  ok : (σ : Type) (t : Term Γ σ) → forgetTypes t ≡ e → WellTyped Γ e

data InScope (Γ : Context) (n : Nat) : Set where
  ok : (σ : Type) (i : σ ∈ Γ) → rawIndex i ≡ n → InScope Γ n

infix 2 _∋_
pattern _∋_ σ x = ok σ x refl

lookupVar : ∀ Γ n → TC (InScope Γ n)
lookupVar []      n       = typeError
lookupVar (σ ∷ Γ) zero    = pure (σ ∋ zero)
lookupVar (σ ∷ Γ) (suc n) = do
  τ ∋ i ← lookupVar Γ n
  pure (τ ∋ suc i)

-- Correct-by-construction type inference
infer : ∀ Γ e → TC (WellTyped Γ e)

infer Γ (var x) = do
  τ ∋ i ← lookupVar Γ x
  pure (τ ∋ var i)

infer Γ (app e e₁) = do
  σ => τ ∋ s ← infer Γ e where nat ∋ s → typeError
  σ′     ∋ t ← infer Γ e₁
  yes refl ← pure (σ == σ′) where no _ → typeError
  pure (τ ∋ app s t)

infer Γ (lam σ e) = do
  τ ∋ t ← infer (σ ∷ Γ) e
  pure (σ => τ ∋ lam σ t)

infer Γ (lit x) = pure (nat ∋ lit x)
infer Γ suc     = pure (nat => nat ∋ suc)

-- Check that it works
test : infer [] (lam (nat => nat) (lam nat (app (var 1) (var 0)))) ≡
       pure ((nat => nat) => nat => nat ∋
             lam (nat => nat) (lam nat (app (var (suc zero)) (var zero))))
test = refl


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

module Data.String.Printf where

open import Data.List using (List; []; _∷_; foldr)
open import Data.String hiding (show)
open import Data.Nat hiding (_≟_)
open import Data.Char as Char using (Char)
import Level
open import Relation.Nullary

infixr 6 _%_
record FormatUnit : Set (Level.suc Level.zero) where
  constructor _%_
  field
    marker : Char
    {type} : Set
    conv   : type → String
open FormatUnit public

module Internal where
  data Formatter : Set (Level.suc Level.zero) where
    chr : Char → Formatter
    cnv : (t : Set) → (t → String) → Formatter

  formatUnitTy : Formatter → Set → Set
  formatUnitTy (chr _) xs = xs
  formatUnitTy (cnv t _) xs = t → xs

  formatTy : List Formatter → Set
  formatTy = foldr formatUnitTy String

  toFormat : List FormatUnit → List Char → List Formatter
  toFormat fs [] = []
  toFormat fs ('%' ∷ x ∷ xs) = go fs x xs where
    go : List FormatUnit → Char → List Char → List Formatter
    go [] x xs = chr x ∷ toFormat fs xs
    go (f ∷ fs) x xs with marker f Char.≟ x
    go (f ∷ _ ) x xs | yes p = cnv _ (conv f) ∷ toFormat fs xs
    go (f ∷ fs) x xs | no ¬p = go fs x xs
  toFormat fs (x ∷ xs) = chr x ∷ toFormat fs xs

  printf : (fs : List FormatUnit) → (xs : String) → formatTy (toFormat fs (toList xs))
  printf fs xs = go "" (toFormat fs (toList xs))
    where
    go : String → (xs : List Formatter) → formatTy xs
    go k [] = k
    go k (chr x ∷ xs) = go (k ++ fromList (x ∷ [])) xs
    go k (cnv _ c ∷ xs) = λ x → go (k ++ c x) xs
import Data.Nat.Show
open import Function

standard : List FormatUnit
standard = 'i' % Data.Nat.Show.show ∷ 's'% id ∷ []

module Printf (fs : List FormatUnit) where
  printf : (xs : String) → Internal.formatTy (Internal.toFormat fs (toList xs))
  printf = Internal.printf fs

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
-- Andreas, 2014-06-27 test case by Ulf
-- {-# OPTIONS -v tc.lhs:40 #-}
{-# OPTIONS --copatterns #-}

record Coind : Set where
  coinductive
  field ind : Coind

open Coind

loop : Set -> Coind
ind A loop = ind (loop A)

-- WAS: Internal error.

-- NOW: Proper error.
-- Ill-formed projection pattern ind A
-- when checking that the clause ind A loop = ind (loop A) has type
-- Set → Coind


text:
{-# OPTIONS --without-K #-}
module function.isomorphism.properties where

open import level
open import sum
open import sets.nat.core
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.fibration
open import function.overloading
open import function.extensionality.core
open import function.extensionality.proof
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.isomorphism.lift
open import function.isomorphism.utils
open import function.isomorphism.two-out-of-six
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.level.core
open import hott.loop.core
open import sets.unit

iso-adjunction : ∀ {i j}{X : Set i}{Y : Set j}
               → (isom : X ≅ Y)(x : X)(y : Y)
               → (apply isom x ≡ y) ≅ (x ≡ invert isom y)
iso-adjunction {i}{j}{X}{Y} isom x y
  = family-eq-iso total' (λ { (y , x) q → comm' x y q }) (y , x)
  where
    open _≅_ isom
    open ≅-Reasoning

    to-we : weak-equiv to
    to-we = proj₂ (≅⇒≈ isom)

    total' : (Σ (Y × X) λ { (y , x) → to x ≡ y })
           ≅ (Σ (Y × X) λ { (y , x) → x ≡ from y})
    total' = Σ-assoc-iso
           ·≅ ( Σ-ap-iso refl≅ λ y
              → contr-⊤-iso (to-we y)
              ·≅ sym≅ (contr-⊤-iso (singl-contr' (from y))) )
           ·≅ sym≅ Σ-assoc-iso

    comm' : (x : X)(y : Y)(p : to x ≡ y)
          → proj₁ (apply total' ((y , x) , p)) ≡ (y , x)
    comm' x y q = ap (_,_ y) (sym (ap from q) · iso₁ x)

private
  iso≡-lem : ∀ {i j}{X : Set i}{Y : Set j}
           → (isom : X ≅ Y)
           → (x x' : X)
           → weak-equiv (λ (p : x ≡ x') → ap (invert isom) (ap (apply isom) p))
  iso≡-lem {X = X} isom x x' = step₃
    where
      step₁ : ∀ {k}{A : Set k}(a a' : A)
            → weak-equiv {X = a ≡ a'} {Y = a ≡ a'} (ap (λ x → x))
      step₁ a a' = subst weak-equiv (sym (funext ap-id)) (proj₂ (≅⇒≈ refl≅))

      step₂ : weak-equiv (λ (p : x ≡ x') → ap (invert isom ∘ apply isom) p)
      step₂ = subst (λ u → weak-equiv {X = x ≡ x'} (ap u)) (sym (funext (_≅_.iso₁ isom)))
                    (step₁ x x')

      step₃ = subst weak-equiv (sym (funext λ p → ap-hom (apply isom) (invert isom) p)) step₂

iso≡ : ∀ {i j}{X : Set i}{Y : Set j}
     → (isom : X ≅ Y)
     → {x x' : X}
     → (x ≡ x')
     ≅ (apply isom x ≡ apply isom x')
iso≡ isom {x}{x'} = two-out-of-six.f-iso
  (ap (apply isom))
  (ap (invert isom))
  (ap (apply isom))
  (iso≡-lem isom x x')
  (iso≡-lem (sym≅ isom) (apply isom x) (apply isom x'))

private
  abstract
    Ω-iso' : ∀ {i j}{X : Set i}{Y : Set j}(n : ℕ)
           → (φ : X ≅ Y)(x : X)
           → Ω n x ≅ Ω n (apply φ x)
    Ω-iso' {X = X}{Y = Y} zero φ x = φ
    Ω-iso' (suc n) φ x = Ω-iso' n (iso≡ φ) refl

    Ω-iso-β : ∀ {i j}{X : Set i}{Y : Set j}(n : ℕ)
            → (φ : X ≅ Y)(x : X)
            → (p : Ω n x)
            → apply (Ω-iso' n φ x) p ≡ mapΩ n (apply φ) p
    Ω-iso-β zero φ x p = refl
    Ω-iso-β (suc n) φ x p = Ω-iso-β n (iso≡ φ) refl p

Ω-iso : ∀ {i j}{X : Set i}{Y : Set j}(n : ℕ)
      → (φ : X ≅ Y)(x : X)
      → Ω n x ≅ Ω n (apply φ x)
Ω-iso n φ x = ≈⇒≅ ( (λ p → mapΩ n (apply φ) p)
                  , subst weak-equiv eq we)
  where
    abstract
      we : weak-equiv (apply (Ω-iso' n φ x))
      we = proj₂ (≅⇒≈ (Ω-iso' n φ x))

      eq : apply (Ω-iso' n φ x) ≡ mapΩ n (apply φ)
      eq = funext (Ω-iso-β n φ x)

abstract
  subtype-eq : ∀ {i j k}{A : Set i}{P : A → Set j}
             → ((x : A) → h 1 (P x))
             → {X : Set k}
             → (isom : X ≅ Σ A P)
             → {x y : X}
             → (proj₁ (apply isom x) ≡ proj₁ (apply isom y))
             → x ≡ y
  subtype-eq hP isom p = iso⇒inj isom
    (unapΣ (p , h1⇒prop (hP _) _ _))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
------------------------------------------------------------------------------
-- Arithmetic properties (added for the Collatz function example)
------------------------------------------------------------------------------

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

module FOTC.Program.Collatz.Data.Nat.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityI
open import FOTC.Program.Collatz.Data.Nat

------------------------------------------------------------------------------
-- Congruence properties

divLeftCong : ∀ {m n o} → m ≡ n → div m o ≡ div n o
divLeftCong refl = refl

divRightCong : ∀ {m n o} → n ≡ o → div m n ≡ div m o
divRightCong refl = refl

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

^-N : ∀ {m n} → N m → N n → N (m ^ n)
^-N {m} Nm nzero          = subst N (sym (^-0 m)) (nsucc nzero)
^-N {m} Nm (nsucc {n} Nn) = subst N (sym (^-S m n)) (*-N Nm (^-N Nm Nn))

div-0-x≡0 : ∀ {n} → N n → n ≢ 0' → div 0' n ≡ 0'
div-0-x≡0 nzero          h = ⊥-elim (h refl)
div-0-x≡0 (nsucc {n} Nn) h = div-x<y h (lt-0S n)

div-x-x≡1 : ∀ {n} → N n → n ≢ 0' → div n n ≡ 1'
div-x-x≡1 {n} Nn h =
  div n n               ≡⟨ div-x≥y h (x≤x Nn) ⟩
  succ₁ (div (n ∸ n) n) ≡⟨ succCong (divLeftCong (x∸x≡0 Nn)) ⟩
  succ₁ (div 0' n)      ≡⟨ succCong (div-0-x≡0 Nn h) ⟩
  1'                    ∎

div-2x-2≡x : ∀ {n} → N n → div (2' * n) 2' ≡ n
div-2x-2≡x nzero = prf
  where
  -- See the combined proof.
  postulate prf : div (2' * zero) 2' ≡ zero

div-2x-2≡x (nsucc nzero) =
  div (2' * 1') 2'
    ≡⟨ divLeftCong (*-rightIdentity 2-N) ⟩
  div 2' 2'
    ≡⟨ div-x≥y S≢0 (x≤x 2-N) ⟩
  succ₁ (div (2' ∸ 2') 2')
    ≡⟨ succCong (divLeftCong (x∸x≡0 2-N)) ⟩
  succ₁ (div zero 2')
    ≡⟨ succCong (div-x<y S≢0 (lt-0S 1')) ⟩
  1' ∎

div-2x-2≡x (nsucc (nsucc {n} Nn)) = prf
  where
  -- See the combined proof.
  postulate prf : div (2' * (succ₁ (succ₁ n))) 2' ≡ succ₁ (succ₁ n)

div-2^[x+1]-2≡2^x : ∀ {n} → N n → div (2' ^ succ₁ n) 2' ≡ 2' ^ n
div-2^[x+1]-2≡2^x {n} Nn =
  div (2' ^ succ₁ n) 2'
    ≡⟨ divLeftCong (^-S 2' n) ⟩
  div (2' * 2' ^ n) 2'
    ≡⟨ div-2x-2≡x (^-N 2-N Nn) ⟩
  2' ^ n ∎

+∸2 : ∀ {n} → N n → n ≢ zero → n ≢ 1' → n ≡ succ₁ (succ₁ (n ∸ 2'))
+∸2 nzero                  n≢0 _   = ⊥-elim (n≢0 refl)
+∸2 (nsucc nzero)          _   n≢1 = ⊥-elim (n≢1 refl)
+∸2 (nsucc (nsucc {n} Nn)) _   _   = sym prf
  where
  prf : succ₁ (succ₁ (succ₁ (succ₁ n) ∸ 2')) ≡ succ₁ (succ₁ n)
  prf = succ₁ (succ₁ (succ₁ (succ₁ n) ∸ 2'))
          ≡⟨ succCong (succCong (S∸S (nsucc Nn) (nsucc nzero))) ⟩
        succ₁ (succ₁ ((succ₁ n) ∸ 1'))
          ≡⟨ succCong (succCong (S∸S Nn nzero)) ⟩
        succ₁ (succ₁ (n ∸ zero))
          ≡⟨ succCong (succCong (∸-x0 n)) ⟩
        succ₁ (succ₁ n) ∎

x^1≡x : ∀ {n} → N n → n ^ 1' ≡ n
x^1≡x {n} Nn =
  n ^ 1'     ≡⟨ ^-S n 0' ⟩
  n * n ^ 0' ≡⟨ *-rightCong (^-0 n) ⟩
  n * 1'     ≡⟨ *-rightIdentity Nn ⟩
  n          ∎

2^x≢0 : ∀ {n} → N n → 2' ^ n ≢ zero
2^x≢0 nzero          h = ⊥-elim (0≢S (trans (sym h) (^-0 2')))
2^x≢0 (nsucc {n} Nn) h =
  case (λ 2≡0 → ⊥-elim (0≢S (sym 2≡0)))
       (λ 2^n≡0 → ⊥-elim (2^x≢0 Nn 2^n≡0))
       (xy≡0→x≡0∨y≡0 2-N (^-N 2-N Nn) (trans (sym (^-S 2' n)) h))

2^[x+1]≢1 : ∀ {n} → N n → 2' ^ succ₁ n ≢ 1'
2^[x+1]≢1 {n} Nn h =
  Sx≢x 1-N (xy≡1→x≡1 2-N (^-N 2-N Nn) (trans (sym (^-S 2' n)) h))

Sx-Even→x-Odd : ∀ {n} → N n → Even (succ₁ n) → Odd n
Sx-Even→x-Odd nzero h = ⊥-elim (t≢f (trans₂ (sym h) (even-S zero) odd-0))
Sx-Even→x-Odd (nsucc {n} Nn) h = trans (sym (even-S (succ₁ n))) h

Sx-Odd→x-Even : ∀ {n} → N n → Odd (succ₁ n) → Even n
Sx-Odd→x-Even nzero          _ = even-0
Sx-Odd→x-Even (nsucc {n} Nn) h = trans (sym (odd-S (succ₁ n))) h

∸-Even : ∀ {m n} → N m → N n → Even m → Even n → Even (m ∸ n)
∸-Odd : ∀ {m n} → N m → N n → Odd m → Odd n → Even (m ∸ n)

∸-Even {m} Nm nzero                      h₁ _ = subst Even (sym (∸-x0 m)) h₁
∸-Even     nzero          (nsucc {n} Nn) h₁ _ = subst Even (sym (0∸x (nsucc Nn))) h₁
∸-Even     (nsucc {m} Nm) (nsucc {n} Nn) h₁ h₂ =
  subst Even (sym (S∸S Nm Nn))
        (∸-Odd Nm Nn (Sx-Even→x-Odd Nm h₁) (Sx-Even→x-Odd Nn h₂))

∸-Odd nzero          Nn             h₁ _  = ⊥-elim (t≢f (trans (sym h₁) odd-0))
∸-Odd (nsucc Nm)     nzero          _  h₂ = ⊥-elim (t≢f (trans (sym h₂) odd-0))
∸-Odd (nsucc {m} Nm) (nsucc {n} Nn) h₁ h₂ =
  subst Even (sym (S∸S Nm Nn))
        (∸-Even Nm Nn (Sx-Odd→x-Even Nm h₁) (Sx-Odd→x-Even Nn h₂))

x-Even→SSx-Even : ∀ {n} → N n → Even n → Even (succ₁ (succ₁ n))
x-Even→SSx-Even nzero h =
  even 2'   ≡⟨ even-S 1' ⟩
  odd 1'    ≡⟨ odd-S zero ⟩
  even zero ≡⟨ even-0 ⟩
  true      ∎

x-Even→SSx-Even (nsucc {n} Nn) h =
  even (succ₁ (succ₁ (succ₁ n)))
    ≡⟨ even-S (succ₁ (succ₁ n)) ⟩
  odd (succ₁ (succ₁ n))
    ≡⟨ odd-S (succ₁ n) ⟩
  even (succ₁ n)
    ≡⟨ h ⟩
  true ∎

2-Even : Even 2'
2-Even = x-Even→SSx-Even nzero even-0

x+x-Even : ∀ {n} → N n → Even (n + n)
x+x-Even nzero          = subst Even (sym (+-rightIdentity nzero)) even-0
x+x-Even (nsucc {n} Nn) = subst Even (sym prf)
                                (x-Even→SSx-Even (+-N Nn Nn) (x+x-Even Nn))
  where
  prf : succ₁ n + succ₁ n ≡ succ₁ (succ₁ (n + n))
  prf = succ₁ n + succ₁ n
          ≡⟨ +-Sx n (succ₁ n) ⟩
        succ₁ (n + succ₁ n)
          ≡⟨ succCong (+-comm Nn (nsucc Nn)) ⟩
        succ₁ (succ₁ n + n)
          ≡⟨ succCong (+-Sx n n) ⟩
        succ₁ (succ₁ (n + n)) ∎

2x-Even : ∀ {n} → N n → Even (2' * n)
2x-Even nzero          = subst Even (sym (*-rightZero 2-N)) even-0
2x-Even (nsucc {n} Nn) = subst Even (sym prf)
                               (x-Even→SSx-Even (+-N Nn Nn) (x+x-Even Nn))
  where
  prf : 2' * succ₁ n ≡ succ₁ (succ₁ (n + n))
  prf =
    2' * succ₁ n
      ≡⟨ *-Sx 1' (succ₁ n) ⟩
    succ₁ n + 1' * succ₁ n
      ≡⟨ +-Sx n (1' * succ₁ n) ⟩
    succ₁ (n + 1' * succ₁ n)
      ≡⟨ succCong (+-rightCong (*-Sx zero (succ₁ n))) ⟩
    succ₁ (n + (succ₁ n + zero * succ₁ n))
      ≡⟨ succCong (+-rightCong (+-rightCong (*-leftZero (succ₁ n)))) ⟩
    succ₁ (n + (succ₁ n + zero))
      ≡⟨ succCong (+-rightCong (+-rightIdentity (nsucc Nn))) ⟩
    succ₁ (n + succ₁ n)
      ≡⟨ succCong (+-comm Nn (nsucc Nn)) ⟩
    succ₁ (succ₁ n + n)
      ≡⟨ succCong (+-Sx n n) ⟩
    succ₁ (succ₁ (n + n)) ∎

2^[x+1]-Even : ∀ {n} → N n → Even (2' ^ succ₁ n)
2^[x+1]-Even {n} Nn = subst Even (sym (^-S 2' n)) (2x-Even (^-N 2-N Nn))


text:
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; _≢_ ; refl ; subst ; subst₂)
open import Data.Nat as Nat
  using (ℕ ; _≤′_ ; _+_)
open import Relation.Binary.PropositionalEquality using (sym)

import Relation.Unary as U

open import Function
  using (_∘_)

open import Relation.Nullary

module Data.FiniteMap
  {Key : Set}
  (inject : Key → ℕ)
  (surject : ℕ → Key)
  (inject-injective : ∀ {k1 k2} → inject k1 ≡ inject k2 → k1 ≡ k2)
  (surject-inject : ∀ {k} → inject (surject k) ≡ k)
  where

open import utility

open import Data.Maybe using (just)
open import Data.Empty
  using (⊥-elim)
open import Data.List
  using (List ; _++_ ; [_] ; [] ; _∷_)
open import Data.List.Any
  using (any ; here ; there ; Any)
open import Data.Nat
  using (ℕ ; zero ; suc)
open import Data.Sum
  using (inj₁ ; inj₂ ; _⊎_)
open import Data.Product
  using (Σ ; Σ-syntax ; ∃ ; proj₁ ; proj₂ ; _×_ ; _,_ ; ∃-syntax ; uncurry ; map)
open import Function
  using (id ; _$_)
open import Relation.Nullary
  using (yes ; no)
open import Data.OrderedListMap(Key)(inject) as OMap hiding (insert-mono ; U-mono)
open import Data.Bool using (Bool ; true ; false)

private
  nbiject : ∀ {k1 k2} → k1 ≢ k2 → inject k1 ≢ inject k2
  nbiject = (_∘ inject-injective)

Map : Set → Set
Map = LMap

keys : ∀{Value} → Map Value → List ℕ
keys{Value} l = (Dom' Value l)

keys+∈ : ∀{Value} → (l : Map Value) → List (∃[ n ] (n ∈ (Dom' Value l)))
keys+∈{Value} l = (Dom'+∈ Value l)

inj= : Key → ℕ → Set
inj= = _≡_ ∘ inject

∈Dom : ∀{Value} → Key → Map Value → Set
∈Dom{Value} k m = (inject k) ∈ (Dom' Value m)

in-inject : ∀ {Value}{x : ℕ} → (l : Map Value) → x ∈ Dom' Value l → ∈Dom (surject x) l
in-inject{x = x} l ∈ rewrite surject-inject{x} = ∈

key-map : ∀{Value}{a}{L : Set a} → (l : Map Value) → (f : (k : Key) → (∈Dom k l) → L) → List L
key-map{L = L} l f
  = Data.List.map ((uncurry f) ∘ (map surject (in-inject l)))
                   (keys+∈ l)

∈Check : ∀{Value}
         → (k : Key)
         → (m : Map Value)
         → Relation.Nullary.Dec (∈Dom k m)
∈Check{Value} k m = any (Nat._≟_ (inject k)) (Dom' Value m)

lookup : ∀{Value k} → (l : Map Value) → (∈Dom k l) → Value
lookup{Value}{k = k} m k∈ = deref Value (inject k) m k∈

update : ∀{Value} → (l : Map Value) → Key → Value → Map Value
update{Value} l k v = m-insert Value (just v) (inject k) l

-- Union map. For repeated keys, the values from the second map is preferred.
union : ∀{Value} → Map Value → Map Value → Map Value
union{Value} m1 m2 = (_U_ Value m1 m2)

empty : ∀{Value} → Map Value
empty = []

[_↦_] : ∀{Value} → (k : Key) → (v : Value) → Map  Value
[ k ↦ v ] = update empty k v

[_↦_,_↦_] : ∀{Value} →
              (k₁ : Key) → (v₁ : Value) →
              (k₂ : Key) → (v₂ : Value) →
              Map Value
[ k₁ ↦ v₁ , k₂ ↦ v₂ ] = update [ k₁ ↦ v₁ ] k₂ v₂

keys-1map : ∀{Value} → (k : Key) → (v : Value) → keys [ k ↦ v ] ≡ inject k ∷ []
keys-1map {Value} k v = Dom'-1map Value (inject k) v

keys-2map : ∀{Value} → (k₁ : Key) → (v₁ : Value) → (k₂ : Key) → (v₂ : Value) →
  (keys [ k₁ ↦ v₁ , k₂ ↦ v₂ ] ≡ inject k₁ ∷ [] × k₁ ≡ k₂) ⊎
  (keys [ k₁ ↦ v₁ , k₂ ↦ v₂ ] ≡ inject k₁ ∷ inject k₂ ∷ []) ⊎
  (keys [ k₁ ↦ v₁ , k₂ ↦ v₂ ] ≡ inject k₂ ∷ inject k₁ ∷ [])
keys-2map {Value} k₁ v₁ k₂ v₂ =
  Data.Sum.map (Data.Product.map id inject-injective) id
    (Dom'-2map Value (inject k₁) v₁ (inject k₂) v₂)

keys-1map-distinct : ∀{Value} → (k1 k2 : Key) → (v1 v2 : Value) → ¬ (k1 ≡ k2) → utility.distinct' (keys [ k1 ↦ v1 ]) (keys [ k2 ↦ v2 ])
keys-1map-distinct k1 k2 v1 v2 neg z k1∈ k2∈ rewrite (keys-1map k1 v1) | (keys-1map k2 v2) with k1∈ | k2∈
... | here refl | here px = (nbiject neg) px
... | there () | _
... | here px | there ()

keys-1map∈ : ∀{Value} → (k1 : Key) → (v1 : Value) → (inject k1) ∈ keys [ k1 ↦ v1 ]
keys-1map∈ k v rewrite keys-1map k v = here refl

2map-eq-one : ∀{V} k1 k2 v k1∈ →  (lookup{V}{k1} ([ k1 ↦ v , k2 ↦ v ]) k1∈) ≡ v
2map-eq-one {V} k1 k2 = insert-two-eq-one V (inject k1) (inject k2)

2map-eq-two : ∀{V} k1 k2 v k2∈ →  (lookup{V}{k2} ([ k1 ↦ v , k2 ↦ v ]) k2∈) ≡ v
2map-eq-two {V} k1 k2 = insert-two-eq-two V (inject k1) (inject k2)

-- theorems

update-in-keys : ∀{V} m k v →  ∈Dom k (update{V} m k v)
update-in-keys {V} m k = insert-in-domain V m (inject k)

lookup-∈-irr : ∀{Value k m} → (∈1 : ∈Dom k m) → (∈2 : ∈Dom k m) → lookup{Value}{k} m ∈1 ≡ lookup{Value}{k} m ∈2
lookup-∈-irr{Value} ∈1 ∈2 = deref-∈-irr Value ∈1 ∈2

insert-mono : ∀{Value k m k' v} → ∈Dom k m → ∈Dom k (update{Value} m k' v)
insert-mono{Value}{k}{m}{k'}{v} i = (OMap.insert-mono Value {m}{inject k}{inject k'}{v} i)

U-mono : ∀{Value m m' k} → ∈Dom k m → ∈Dom k (union{Value} m m')
U-mono{V}{m}{m'}{k} i =  OMap.U-mono V {m}{m'}{inject k} i

union-comm : ∀ {Value} → (m1 : Map Value) → (m2 : Map Value) → distinct' (keys m1) (keys m2) →  union m1 m2 ≡ union m2 m1
union-comm {Value} m1 m2 keys-m1≠keys-m2 = U-comm Value {m1} {m2} keys-m1≠keys-m2

union-assoc : ∀ {Value} → (m1 m2 m3 : Map Value) → union m1 (union m2 m3) ≡ union (union m1 m2) m3
union-assoc {Value} = U-assoc Value

keys-assoc-comm : ∀ {Value} m1 m2 m3 →
  keys (union {Value} (union {Value} m1 m2) m3) ≡
  keys (union {Value} (union {Value} m1 m3) m2)
keys-assoc-comm {Value} = Dom'-assoc-comm Value

U⁻-m : ∀ {Value m m' n} → ∈Dom n (union {Value} m m') → ∈Dom n m ⊎ ∈Dom n m'
U⁻-m {Value} {m} {m'} {n} = U⁻ Value {m} {m'} {inject n}

U-∉-irr-get-help-m : ∀{Value m m' k} → (k∈m : ∈Dom k m) → ¬ (∈Dom k m') → (k∈' : ∈Dom k (union {Value} m m'))→ lookup {Value} {k} m k∈m ≡ lookup {Value} {k} (union {Value} m m') k∈'
U-∉-irr-get-help-m {Value} = U-∉-irr-get-help Value

U-∉-irr-get-m : ∀{Value m m' k} → (k∈m : ∈Dom k m) → ¬ (∈Dom k m') → ∃ λ k∈' → lookup {Value} {k} m k∈m ≡ lookup {Value} {k} (union {Value} m m') k∈'
U-∉-irr-get-m {Value} = U-∉-irr-get Value

get-U-right-irr-m : ∀ {Value} k m m' →
  (k∈mUm' : ∈Dom k (union {Value} m m')) →
  (k∈m'   : ∈Dom k m') →
  lookup {Value} {k} (union {Value} m m') k∈mUm' ≡ lookup {Value} {k} m' k∈m'
get-U-right-irr-m {Value} k = deref-U-right-irr Value (inject k)

∈-get-U-irr-m : ∀ {Value} k m m' m'' k∈mUm'' k∈m'Um'' →
  (k∈m'' : ∈Dom k m'') →
    lookup {Value} {k} (union {Value} m  m'') k∈mUm'' ≡
    lookup {Value} {k} (union {Value} m' m'') k∈m'Um''
∈-get-U-irr-m {Value} k = ∈-deref-U-irr Value (inject k)

get-U-both-irr-m : ∀ {Value} k m m' m'' k∈m k∈m' k∈mUm'' k∈m'Um'' →
  lookup {Value} {k} m k∈m ≡ lookup {Value} {k} m' k∈m' →
    lookup {Value} {k} (union {Value} m  m'') k∈mUm'' ≡
    lookup {Value} {k} (union {Value} m' m'') k∈m'Um''
get-U-both-irr-m {Value} k = deref-U-both-irr Value (inject k)

putputget : ∀{Value m k k' v v'}
            → ¬ k ≡ k'
            → (∈1 : ∈Dom k m)
            → (∈2 : ∈Dom k (update{Value} m k' v'))
            → lookup{Value}{k} m ∈1 ≡ v
            → lookup{Value}{k} (update{Value} m k' v') ∈2 ≡ v
putputget{V}{m}{k}{k'}{v}{v'} neq kin1 kin2 eq = putputget-neq V {inject k}{inject k'}{m} (nbiject neq) kin1 kin2 eq

putput-overwrite : ∀{Value} m k v v'
                   → (update{Value} (update{Value} m k v) k v') ≡ (update m k v')
putput-overwrite {V} m k v v' = putputget-eq V (inject k) m v v'

getput-m : ∀ {Value} k m →
  (∈1 : ∈Dom k m) →
  m ≡ update {Value} m k (lookup {Value} {k} m ∈1)
getput-m {Value} k = getput Value (inject k)

putget-m : ∀{Value m k v} → (kin : ∈Dom k (update{Value} m k v)) → (lookup{Value}{k} (update{Value} m k v) kin) ≡ v
putget-m {V}{m}{k}{v} kin = putget V kin

update-union-union : ∀ {Value} k v m m' →
  (∈1 : ∈Dom k m) →
  (∈2 : ∈Dom k m') →
    union {Value} m m' ≡
    union {Value} (update {Value} m k v) m'
update-union-union {Value} k = put-U-U Value (inject k)

ineq-m : ∀{Value k m} → (k1 : ∈Dom{Value} k m) → (k2 : ∈Dom k m) → k1 ≡ k2
ineq-m {V}{k}{m} k1 k2 = ineq V {inject k}{m} k1 k2

put-comm : ∀{Value m k1 k2 v1 v2}
          → ¬ k1 ≡ k2 → (update (update{Value} m k1 v1) k2 v2) ≡ (update (update m k2 v2) k1 v1)
put-comm{V}{m}{k1}{k2}{v1}{v2} ¬k1≡k2 = insert-comm V {m}{inject k1}{inject k2}{v1}{v2} (nbiject ¬k1≡k2)

put-union-comm : ∀ {Value} k v m m' →
  ¬ (∈Dom k m') →
    union {Value} (update {Value} m k v) m' ≡
    update {Value} (union {Value} m m') k v
put-union-comm {Value} k = insert-U-comm Value (inject k)

union-=-irr : ∀ {Value} m m' → (keys{Value} m) ≡ (keys{Value} m') → ∀ k k∈ k∈2 → (lookup{Value}{k} (union m m') k∈) ≡ (lookup{Value}{k} m' k∈2)
union-=-irr {V} m m' eql k = U-=-irr V m m' eql (inject k)

union-single-overwrite : ∀ {V} k v1 v2 → union{V} [ k ↦ v1 ] [ k ↦ v2 ] ≡ [ k ↦ v2 ]
union-single-overwrite {V} k v1 v2 = U-single-overwrite V (inject k) v1 v2

update-single-val : ∀ {V} k v k∈ → lookup{V}{k} [ k ↦ v ] k∈ ≡ v
update-single-val {V} k v k∈ = set-single-val V (inject k) v k∈

single-val-overwrite : ∀ {V} k v m → (∈Dom{V} k m) → union{V}  ([ k ↦ v ]) m ≡ m
single-val-overwrite {V} k = overwrite-single-val V (inject k)

union-insert-eq : ∀{V} k v m → (update{V} m k v) ≡ (union{V} m [ k ↦ v ])
union-insert-eq {V} k = U-insert-eq V (inject k)

update-domain-eq : ∀{V} k v m → (inject k) ∈ keys{V} m → (keys m) ≡ (keys (update{V} m k v))
update-domain-eq {V} k = insert-domain-eq V (inject k)

--(OMap.insert-mono Value {m}{inject k}{inject k'}{v} i)
keys-2map∈ : ∀{Value} → (k1 : Key) → (v1 : Value) → (k2 : Key) → (v2 : Value) → (∈Dom k1 [ k1 ↦ v1 , k2 ↦ v2 ]) × (∈Dom k2 [ k1 ↦ v1 , k2 ↦ v2 ])
keys-2map∈ {V} k1 v1 k2 v2 = insert-mono (keys-1map∈ k1 v1) , update-in-keys ([ k1 ↦ v1 ]) k2 v2

count : ∀ {V} -> (V -> Bool) -> Map V -> ℕ
count {V} p m = ocount V p m

change-one-count-goes-down :
  ∀ {Value} (m : Map Value) ->
    (p : Value -> Bool) ->
    (k : Key) ->
    (k∈ : ∈Dom k m) ->
    p (lookup m k∈) ≡ true ->
    (v : Value) ->
    p v ≡ false ->
    count p m ≡ suc (count p (update m k v))
change-one-count-goes-down {V} m p k =
  change-one-ocount-goes-down V m p (inject k)

change-nothing-count-stays-same :
  ∀ {Value} (m : Map Value) ->
    (p : Value -> Bool) ->
    (k : Key) ->
    (k∈ : ∈Dom k m) ->
    (v : Value) ->
    p (lookup m k∈) ≡ p v ->
    count p m ≡ count p (update m k v)
change-nothing-count-stays-same {V} m p k =
  change-nothing-ocount-stays-same V m p (inject k)

count-merge≤′sum-count :
  ∀ {Value}
    (m1 m2 : Map Value) ->
    (p : Value -> Bool) ->
    count p (union m1 m2) ≤′ count p m1 + count p m2
count-merge≤′sum-count {V} m1 m2 p =
  ocount-merge≤′sum-ocount V m1 m2 p

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus