-- Code file for paper "Deep Induction for Inductive-Inductive Types"
-- by Patricia Johann and Ben Lenox
-- Verified with Agda version 2.6.4.1 and standard library version 1.7.2

{-# OPTIONS --type-in-type #-}

import Data.Nat as Nat using (_≥_)
open import Data.Nat using (zero ; suc ; _>_) renaming (ℕ to Nat)
open import Agda.Builtin.Unit using (⊤ ; tt)
open import Agda.Builtin.Nat using (_==_)
open import Agda.Builtin.List using (List ; [] ; _∷_)
open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Relation.Binary.PropositionalEquality using (cong ; _≢_)
open import Relation.Binary.PropositionalEquality.Core using (≢-sym)
open import Data.Nat.Properties using (0≢1+n ; 1+n≢0 ; suc-injective ; <⇒≤ ; ≤∧≢⇒< ; ≤-reflexive ; m≤n+m ; n≤1+n)
open import Agda.Builtin.Bool using (true ; false)
open import Data.Empty using (⊥)
open import Data.Product using (_×_ ; _,_ ; Σ-syntax ; ∃-syntax) renaming (proj₁ to fst ; proj₂ to snd)

module 26-tfp-code where

-- Generalized variables for more concise implicit arguments
-- (https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html)
private
  variable
    a b : Set
    m n : Nat


-- Code for Section 2:


{- Type constructor for the ADT of lists as defined in Agda's standard Library
data List (a : Set) : Set where
  []  : List a
  _∷_ : a → List a → List a
-}

{- Type constructor for the ADT of natural numbers as defined in Agda's standard library
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat
-}


-- Type constructor for the IF of vectors
data Vec (a : Set) : Nat → Set where
   vnil  : Vec a zero
   vcons : a → Vec a n → Vec a (suc n)


-- Type constructors for the IIT of contexts and types
mutual
  data Ctxt : Set where
    ε   : Ctxt
    _⋅_ : (Γ : Ctxt) → Ty Γ → Ctxt

  data Ty : Ctxt → Set where
    ι : {Γ : Ctxt} → Ty Γ
    Π : {Γ : Ctxt} → (A : Ty Γ) → Ty (Γ ⋅ A) → Ty Γ


-- Class that defines a type supporting an arbitrary binary relation
record Ordered (a : Set) : Set where
  field
    _≥_ : a → a → Set

open Ordered {{...}} public

-- Type constructors for the IIT of sorted lists
mutual
  data SList (a : Set) {{orda : Ordered a}} : Set where
    snil  : SList a
    scons : {x : a} → {xs : SList a} → x ≥L xs → SList a

  data _≥L_ {a : Set} {{orda : Ordered a}} (x : a) : SList a → Set where
    triv : x ≥L snil
    extn : {y : a} → {ys : SList a} → (y≥ys : y ≥L ys) → x ≥ y →
                x ≥L ys → x ≥L (scons y≥ys)


-- Class that defines a type supporting a transitive ordering
record TOrdered (a : Set) : Set where
  field
    _<_ : a → a → Set
    <trans : {x y z : a} → x < y → y < z → x < z

open TOrdered {{...}} public

-- Type constructors for the IIT of dense order completions
mutual
  data _* (a : Set) {{ord : TOrdered a}} : Set where
    inj : a → a *
    mid : {x y : a *} → x <* y → a *

  data _<*_ {a : Set} {{ord : TOrdered a}} : a * → a * → Set where
    inj<  : {x y : a} → x < y → inj x <* inj y
    l<mid : {x y : a *} → (x<*y : x <* y) → x <* (mid x<*y)
    mid<r : {x y : a *} → (x<*y : x <* y) → (mid x<*y) <* y


-- Code for Section 3:


-- Structural induction rule for lists
ListSInd : (P : List a → Set) →
           P [] →
           ((x : a) → (xs : List a) → P xs → P (x ∷ xs)) →
           (xs : List a) → P xs
ListSInd P hnil hcons [] = hnil
ListSInd P hnil hcons (x ∷ xs) = hcons x xs (ListSInd P hnil hcons xs)

-- Predicate lifting for lists
List^ : (a → Set) → List a → Set
List^ Q [] = ⊤
List^ Q (x ∷ xs) = Q x × List^ Q xs

-- Deep induction rule for lists
ListDInd : (Q : a → Set) → (P : List a → Set) →
           P [] →
           ((x : a) → (xs : List a) → Q x → P xs → P (x ∷ xs)) →
           (xs : List a) → List^ Q xs → P xs
ListDInd Q P hnil hcons [] Qxs = hnil
ListDInd Q P hnil hcons (x ∷ xs) (Qx , Qxs) = hcons x xs Qx (ListDInd Q P hnil hcons xs Qxs)


-- Predicate lifting for vectors
Vec^ : (a → Set) → (Nat → Set) → Vec a n → Set
Vec^ {n = zero} Qa QN vnil = QN zero
Vec^ {n = suc m} Qa QN (vcons x xs) = Qa x × Vec^ Qa QN xs × (QN m → QN (suc m))

-- Not in the paper, but needed to construct the proof terms for the deep induction rule for Vec
Vec^QN⇒QN : {a : Set} → {Qa : a → Set} → (QN : Nat → Set) → (xs : Vec a n) → Vec^ Qa QN xs → QN n
Vec^QN⇒QN QN vnil QNzero = QNzero
Vec^QN⇒QN QN (vcons x xs) (Qax , QaQNxs , hQN) = hQN (Vec^QN⇒QN QN xs QaQNxs)

-- Deep induction rule for vectors
VecDInd : (Qa : a → Set) → (QN : Nat → Set) → (P : {n : Nat} → Vec a n → Set) →
          (QN zero → P vnil) →
          ({n : Nat} → (x : a) → (xs : Vec a n) → QN (suc n) → Qa x → P xs → P (vcons x xs)) →
          (xs : Vec a n) → Vec^ Qa QN xs → P xs
VecDInd Qa QN P hnil hcons vnil QNzero = hnil QNzero
VecDInd Qa QN P hnil hcons (vcons x xs) QaQNxxs@(Qax , QaQNxs , hQN) =
    hcons x xs (Vec^QN⇒QN {Qa = Qa} QN (vcons x xs) QaQNxxs) Qax (VecDInd Qa QN P hnil hcons xs QaQNxs)


-- Code for Section 5:


{- Predicate lifting for the IIT of contexts and types derived from our construction
mutual
  Ctxt^ : ((Γ : Ctxt) → Ty Γ → Set) → Ctxt → Set
  Ctxt^ Q ε = ⊤                                                     -- no types from steps (i), (ii), or (iii)
  Ctxt^ Q (Γ ⋅ A) = Ty^ Q Γ A × Ctxt^ Q Γ                           -- step (ii)

  Ty^ : ((Γ : Ctxt) → Ty Γ → Set) → ((Γ : Ctxt) → Ty Γ → Set)
  Ty^ Q Γ ι = Q Γ ι ×                                               -- step (i)
              Ctxt^ Q Γ                                             -- step (ii) or (iii)
  Ty^ Q Γ (Π A B) = Q Γ (Π A B) ×                                   -- step (i)
                    Ctxt^ Q Γ × Ty^ Q Γ A × Ty^ Q (Γ ⋅ A) B ×       -- step (ii)
                    ((Ctxt^ Q Γ × Ctxt^ Q (Γ · A)) → Ctxt^ Q Γ)     -- step (iii)
-}

-- Predicate lifting for the IIT of contexts and types after simplification using CTprojPrim and CTprojIndex below
mutual
  Ctxt^ : ((Γ : Ctxt) → Ty Γ → Set) → Ctxt → Set
  Ctxt^ Q ε = ⊤
  Ctxt^ Q (Γ ⋅ A) = Ty^ Q Γ A
                    -- × Ctxt^ Q Γ                                  -- can be obtained from Ty^ Q Γ A using CTprojIndex

  Ty^ : ((Γ : Ctxt) → Ty Γ → Set) → ((Γ : Ctxt) → Ty Γ → Set)
  Ty^ Q Γ ι = Q Γ ι × Ctxt^ Q Γ
  Ty^ Q Γ (Π A B) = Q Γ (Π A B) × Ty^ Q (Γ ⋅ A) B
                    -- × Ctxt^ Q Γ                                  -- can be obtained from
                    -- × Ty^ Q Γ A                                  -- can be obtained from Ty^ Q (Γ ⋅ A) B using CTprojIndex
                    -- × ((Ctxt^ Q Γ × Ctxt^ Q (Γ · A)) → Ctxt^ Q Γ)-- the conclusion of this arrow type is already present as Ctxt^ Q Γ and so it can be omitted


-- If Q can be lifted to type A in context Γ, then Q holds of Γ and A
CTprojPrim : {Q : (Γ : Ctxt) → Ty Γ → Set} → {Γ : Ctxt} → (A : Ty Γ) →
              Ty^ Q Γ A → Q Γ A
CTprojPrim ι (Qι , ^QΓ) = Qι
CTprojPrim (Π A B) (QΠAB , ^QB) = QΠAB

-- If Q can be lifted to a type A in context Γ, then Q can be lifted to Γ
CTprojIndex : {Q : (Γ : Ctxt) → Ty Γ → Set} → {Γ : Ctxt} → (A : Ty Γ) →
              Ty^ Q Γ A → Ctxt^ Q Γ
CTprojIndex ι (Qι , ^QΓ) = ^QΓ
CTprojIndex (Π A B) (QΠAB , ^QB) = CTprojIndex A (CTprojIndex B ^QB)


-- Predicate that checks whether or not a type is not a function type
data nonFunction (Γ : Ctxt) : Ty Γ → Set where
  nfι : nonFunction Γ ι

-- Predicate that checks whether or not a type is left-simple, i.e., has no function type on the left of a Π
leftSimple : (Γ : Ctxt) → Ty Γ → Set
leftSimple Γ ι = nonFunction Γ ι
leftSimple Γ (Π A B) = nonFunction Γ A

-- Predicate that checks whether or not a type is first-order, i.e., has no function type on the left of a Π,
-- and is recursively first-order on the right
firstOrder : (Γ : Ctxt) → Ty Γ → Set
firstOrder Γ ι = nonFunction Γ ι
firstOrder Γ (Π A B) = nonFunction Γ A × firstOrder (Γ ⋅ A) B


-- Deep induction rule for the IIT of contexts and types
mutual
  CtxtDInd :
    (Q : (Γ : Ctxt) → Ty Γ → Set) →
    (Pc : Ctxt → Set) →
    (Pt : (Γ : Ctxt) → Ty Γ → Pc Γ → Set) →
    (hε : Pc ε) →
    (h⋅ : (Γ : Ctxt) → (A : Ty Γ) → Q Γ A → (PcΓ : Pc Γ) → Pt Γ A PcΓ → Pc (Γ ⋅ A)) →
    (hι : (Γ : Ctxt) → Q Γ ι → (PcΓ : Pc Γ) → Pt Γ ι PcΓ) →
    (hΠ : (Γ : Ctxt) → (A : Ty Γ) → (B : Ty (Γ ⋅ A)) →
          Q Γ A → Q (Γ ⋅ A) B → Q Γ (Π A B) →
          (PcΓ : Pc Γ) → Pt Γ A PcΓ →
          (PcΓA : Pc (Γ ⋅ A)) → Pt (Γ ⋅ A) B PcΓA →
          Pt Γ (Π A B) PcΓ) →
    (Γ : Ctxt) → Ctxt^ Q Γ → Pc Γ
  CtxtDInd Q Pc Pt hε h⋅ hι hΠ ε ^Qε = hε
  CtxtDInd Q Pc Pt hε h⋅ hι hΠ (Γ ⋅ A) ^QA = h⋅ Γ A (CTprojPrim A ^QA)
    (CtxtDInd Q Pc Pt hε h⋅ hι hΠ Γ (CTprojIndex A ^QA))
    (TyDInd Q Pc Pt hε h⋅ hι hΠ Γ A ^QA)

  TyDInd :
    (Q : (Γ : Ctxt) → Ty Γ → Set) →
    (Pc : Ctxt → Set) →
    (Pt : (Γ : Ctxt) → Ty Γ → Pc Γ → Set) →
    (hε : Pc ε) →
    (h⋅ : (Γ : Ctxt) → (A : Ty Γ) → Q Γ A → (PcΓ : Pc Γ) → Pt Γ A PcΓ → Pc (Γ ⋅ A)) →
    (hι : (Γ : Ctxt) → Q Γ ι → (PcΓ : Pc Γ) → Pt Γ ι PcΓ) →
    (hΠ : (Γ : Ctxt) → (A : Ty Γ) → (B : Ty (Γ ⋅ A)) →
          Q Γ A → Q (Γ ⋅ A) B → Q Γ (Π A B) →
          (PcΓ : Pc Γ) → Pt Γ A PcΓ →
          (PcΓA : Pc (Γ ⋅ A)) → Pt (Γ ⋅ A) B PcΓA →
          Pt Γ (Π A B) PcΓ) →
    (Γ : Ctxt) → (A : Ty Γ) → (^QA : Ty^ Q Γ A) →
    Pt Γ A (CtxtDInd Q Pc Pt hε h⋅ hι hΠ Γ (CTprojIndex A ^QA))
  TyDInd Q Pc Pt hε h⋅ hι hΠ Γ ι (Qι , ^QΓ) = hι Γ Qι (CtxtDInd Q Pc Pt hε h⋅ hι hΠ Γ ^QΓ)
  TyDInd Q Pc Pt hε h⋅ hι hΠ Γ (Π A B) (QΠAB , ^QB) = hΠ Γ A B (CTprojPrim A (CTprojIndex B ^QB)) (CTprojPrim B ^QB) QΠAB
    (CtxtDInd Q Pc Pt hε h⋅ hι hΠ Γ (CTprojIndex A (CTprojIndex B ^QB)))
    (TyDInd Q Pc Pt hε h⋅ hι hΠ Γ A (CTprojIndex B ^QB))
    (CtxtDInd Q Pc Pt hε h⋅ hι hΠ (Γ ⋅ A) (CTprojIndex B ^QB))
    (TyDInd Q Pc Pt hε h⋅ hι hΠ (Γ ⋅ A) B ^QB)


-- Proof by deep induction that a type that is hereditarily left-simple is first-order
hls⇒fo : (Γ : Ctxt) → (A : Ty Γ) → Ty^ leftSimple Γ A → firstOrder Γ A
hls⇒fo Γ A hyp = TyDInd Q Pc Pt hε h⋅ hι hΠ Γ A hyp
  where
  Q : (Γ : Ctxt) → Ty Γ → Set
  Q = leftSimple

  Pc : Ctxt → Set
  Pc Γ = ⊤

  Pt : (Γ : Ctxt) → Ty Γ → Pc Γ → Set
  Pt Γ A PcΓ = firstOrder Γ A

  hε : Pc ε
  hε = tt

  h⋅ : (Γ : Ctxt) → (A : Ty Γ) → Q Γ A → (PcΓ : Pc Γ) → Pt Γ A PcΓ → Pc (Γ ⋅ A)
  h⋅ Γ A QA PcΓ PtA = PcΓ

  hι : (Γ : Ctxt) → Q Γ ι → (PcΓ : Pc Γ) → Pt Γ ι PcΓ
  hι Γ Qι PcΓ = Qι

  hΠ : (Γ : Ctxt) → (A : Ty Γ) → (B : Ty (Γ ⋅ A)) → Q Γ A → Q (Γ ⋅ A) B → Q Γ (Π A B) →
        (PcΓ : Pc Γ) → Pt Γ A PcΓ → (PcΓA : Pc (Γ ⋅ A)) → Pt (Γ ⋅ A) B PcΓA →
        Pt Γ (Π A B) PcΓ
  hΠ Γ A B QA QB QΠAB PcΓ PtA PcΓA PtB = (QΠAB , PtB)


-- Code for Section 6:


{- Predicate lifting for the IIT of sorted lists derived from our construction
mutual
  SList^ : {{orda : Ordered a}} → (a → Set) → SList a → Set
  SList^ Q snil = ⊤                                                                   -- no types from steps (i), (ii), or (iii)
  SList^ Q (scons {x} {xs} x≥xs) = Q x ×                                              -- step (i)
                                   SList^ Q xs × ≥L^ Q x≥xs                           -- step (ii)
                                                                                      -- no types from step 3 because elements of SList a do not have term indices

  ≥L^ : {{orda : Ordered a}} → (a → Set) → {x : a} → {xs : SList a} → x ≥L xs → Set
  ≥L^ Q {x} triv = Q x ×                                                              -- step (i)
                   SList^ Q snil                                                      -- step (ii) or (iii)
  ≥L^ Q (extn {x} {y} {ys} y≥ys _ x≥ys) = Q x × Q y ×                                 -- step (i)
                                          SList^ Q ys × ≥L^ Q y≥ys × ≥L^ Q x≥ys ×     -- step (ii)
                                          (SList^ Q ys → SList^ Q (scons y≥ys))       -- step (iii)
-}

-- Predicate lifting for the IIT of sorted lists after simplification using SprojPrim and SprojIndex below
mutual
  SList^ : {{orda : Ordered a}} → (a → Set) → SList a → Set
  SList^ Q snil = ⊤
  SList^ Q (scons x≥xs) = ≥L^ Q x≥xs
                          -- × Q x                                                    -- can be obtained from ≥L^ Q x≥xs using SprojPrim
                          -- × SList^ Q xs                                            -- can be obtained from ≥L^ Q x≥xs using SprojIndex

  ≥L^ : {{orda : Ordered a}} → (a → Set) → {x : a} → {xs : SList a} → x ≥L xs → Set
  ≥L^ Q {x} triv = Q x
                   -- × SList^ Q snil                                                 -- this type simplifies to ⊤ and so can be omitted
  ≥L^ Q (extn y≥ys _ x≥ys) = ≥L^ Q y≥ys × ≥L^ Q x≥ys
                   -- × Q x × Q y                                                     -- can be obtained from ≥L^ Q x≥ys and ≥L^ Q y≥ys respectively using SprojPrim
                   -- × (SList^ Q ys → SList^ Q (scons y≥ys))                         -- the conclusion of this arrow type is already present as ≥L^ Q y≥ys and so it can be omitted


-- If Q can be lifted to x≥xs, then Q holds of x
SprojPrim : {{orda : Ordered a}} → {Q : a → Set} → {x : a} →
            {xs : SList a} → (x≥xs : x ≥L xs) → ≥L^ Q x≥xs → Q x
SprojPrim triv Qx = Qx
SprojPrim (extn _ _ x≥ys) (_ , Qx≥ys) = SprojPrim x≥ys Qx≥ys

-- If Q can be lifted to x≥xs, then Q can be lifted to xs
SprojIndex : {{orda : Ordered a}} → {Q : a → Set} → {x : a} →
            {xs : SList a} → (x≥xs : x ≥L xs) → ≥L^ Q x≥xs → SList^ Q xs
SprojIndex triv _ = tt
SprojIndex (extn _ _ _) (Qy≥ys , _) = Qy≥ys


-- Deep induction rule for the IIT of sorted lists
mutual
  SListDInd : {{orda : Ordered a}} → (Q : a → Set) →
            (Pl : SList a → Set) →
            (P≥ : {x : a} → {xs : SList a} → x ≥L xs → Pl xs → Set) →
            (hnil : Pl snil) →
            (hcons : {x : a} → {xs : SList a} → (x≥xs : x ≥L xs) → Q x →
              (Plxs : Pl xs) → P≥ x≥xs Plxs → Pl (scons x≥xs)) →
            (htriv : {x : a} → Q x → P≥ {x} triv hnil) →
            (hextn : {x y : a} → {ys : SList a} → (y≥ys : y ≥L ys) →
               (x≥y : x ≥ y) → (x≥ys : x ≥L ys) → Q x → (Qy : Q y) →
               (Plys1 : Pl ys) → (P≥yys : P≥ y≥ys Plys1) →
               (Plys2 : Pl ys) → P≥ x≥ys Plys2 →
               P≥ (extn y≥ys x≥y x≥ys) (hcons y≥ys Qy Plys1 P≥yys)) →
            (xs : SList a) → SList^ Q xs → Pl xs
  SListDInd Q Pl P≥ hnil hcons htriv hextn snil Qxs = hnil
  SListDInd Q Pl P≥ hnil hcons htriv hextn (scons {xs = xs} x≥xs) Qx≥xs =
    hcons x≥xs (SprojPrim x≥xs Qx≥xs)
      (SListDInd Q Pl P≥ hnil hcons htriv hextn xs (SprojIndex x≥xs Qx≥xs))
      (≥LDInd Q Pl P≥ hnil hcons htriv hextn x≥xs Qx≥xs)

  ≥LDInd : {{orda : Ordered a}} → (Q : a → Set) →
         (Pl : SList a → Set) →
         (P≥ : {x : a} → {xs : SList a} → x ≥L xs → Pl xs → Set) →
         (hnil : Pl snil) →
         (hcons : {x : a} → {xs : SList a} → (x≥xs : x ≥L xs) →
            Q x → (Plxs : Pl xs) → P≥ x≥xs Plxs → Pl (scons x≥xs)) →
         (htriv : {x : a} → Q x → P≥ {x} triv hnil) →
         (hextn : {x y : a} → {ys : SList a} → (y≥ys : y ≥L ys) → (x≥y : x ≥ y) →
            (x≥ys : x ≥L ys) → Q x → (Qy : Q y) → (Plys1 : Pl ys) → (P≥yys : P≥ y≥ys Plys1) →
            (Plys2 : Pl ys) → P≥ x≥ys Plys2 →
            P≥ (extn y≥ys x≥y x≥ys) (hcons y≥ys Qy Plys1 P≥yys)) →
         {x : a} → {xs : SList a} → (x≥xs : x ≥L xs) → (Qx≥xs : ≥L^ Q x≥xs) →
         P≥ x≥xs (SListDInd Q Pl P≥ hnil hcons htriv hextn xs (SprojIndex x≥xs Qx≥xs))
  ≥LDInd Q Pl P≥ hnil hcons htriv hextn {x} triv Qx = htriv Qx
  ≥LDInd Q Pl P≥ hnil hcons htriv hextn {x} (extn {ys = ys} y≥ys x≥y x≥ys) (Qy≥ys , Qx≥ys) =
    hextn y≥ys x≥y x≥ys (SprojPrim x≥ys Qx≥ys) (SprojPrim y≥ys Qy≥ys)
      (SListDInd Q Pl P≥ hnil hcons htriv hextn ys (SprojIndex y≥ys Qy≥ys))
      (≥LDInd Q Pl P≥ hnil hcons htriv hextn y≥ys Qy≥ys)
      (SListDInd Q Pl P≥ hnil hcons htriv hextn ys (SprojIndex x≥ys Qx≥ys))
      (≥LDInd Q Pl P≥ hnil hcons htriv hextn x≥ys Qx≥ys)


-- Code for Section 7:


-- Nat is ordered by the built-in ordering ≥
instance
  NatOrdered : Ordered Nat
  _≥_ {{NatOrdered}} = Nat._≥_


-- Predicate that checks whether or not a natural number is even
even : Nat → Set
even zero = ⊤
even (suc zero) = ⊥
even (suc (suc n)) = even n

-- Predicate that checks whether or not a sorted list contains numbers in strictly decreasing order
mutual
  >SList : SList Nat → Set
  >SList snil = ⊤
  >SList (scons x≥xs) = >L x≥xs

  >L : {x : Nat} → {xs : SList Nat} → x ≥L xs → Set
  >L triv = ⊤
  >L {x} (extn {y} y≥ys _ x≥ys) = x > y × >L x≥ys × >L y≥ys

-- Predicates that check whether or not a sorted list contains only even numbers in strictly decreasing order
^Even&DecrSList : SList Nat → Set
^Even&DecrSList xs = SList^ even xs × >SList xs

^Even&Decr≥L : {x : Nat} → {xs : SList Nat} → x ≥L xs → Set
^Even&Decr≥L x≥xs = ≥L^ even x≥xs × >L x≥xs


-- Functions that prove that if a sorted list contains only even numbers in strictly decreasing order,
-- then all of its elements are even and they appear in strictly decreasing order

^Even&DecrSList⇒^Even : (xs : SList Nat) → ^Even&DecrSList xs → SList^ even xs
^Even&DecrSList⇒^Even xs (evenxs , _) = evenxs

^Even&DecrSList⇒Decr : (xs : SList Nat) → ^Even&DecrSList xs → >SList xs
^Even&DecrSList⇒Decr xs (_ , decrxs) = decrxs

^Even&Decr≥L⇒^Even : {x : Nat} → {xs : SList Nat} → (x≥xs : x ≥L xs) → ^Even&Decr≥L x≥xs → ≥L^ even x≥xs
^Even&Decr≥L⇒^Even x≥xs (evenx≥xs , _) = evenx≥xs

^Even&Decr≥L⇒Decr : {x : Nat} → {xs : SList Nat} → (x≥xs : x ≥L xs) → ^Even&Decr≥L x≥xs → >L x≥xs
^Even&Decr≥L⇒Decr x≥xs (_ , x>xs) = x>xs


-- Predicate that checks whether or not a function preserves evenness of natural numbers
evenPres : (Nat → Nat) → Set
evenPres f = (x : Nat) → even x → even (f x)

-- Predicate that checks whether or not a function preserves the > ordering on natural numbers
>Pres : (f : Nat → Nat) → Set
>Pres f = (x y : Nat) → x > y → f x > f y


-- Predicate that checks whether or not a function from a to b is monotone with respect to orderings on a and b
monotone : {{orda : Ordered a}} → {{ordb : Ordered b}} → (f : a → b) → Set
monotone {a} f = (a1 a2 : a) → a1 ≥ a2 → f a1 ≥ f a2

-- Map function for the IIT of sorted lists
mutual
  mapSList : {{orda : Ordered a}} → {{ordb : Ordered b}} → (f : a → b) → monotone f → SList a → SList b
  mapSList _ _ snil = snil
  mapSList f monof (scons x≥xs) = scons (map≥L f monof x≥xs)

  map≥L : {{orda : Ordered a}} → {{ordb : Ordered b}} →
    (f : a → b) → (monof : monotone f) → {x : a} → {xs : SList a} → x ≥L xs → f x ≥L mapSList f monof xs
  map≥L _ _ triv = triv
  map≥L f monof {x} (extn {y} y≥ys x≥y x≥ys) = extn (map≥L f monof y≥ys) (monof x y x≥y) (map≥L f monof x≥ys)


-- Lemmas relating boolean equality (==) to definitional equality (≡)
==⇒≡ : (m == n) ≡ true → m ≡ n
==⇒≡ {zero} {zero} p = refl
==⇒≡ {suc a} {suc b} p = cong suc (==⇒≡ p)

¬==⇒≢ : (m == n) ≡ false → m ≢ n
¬==⇒≢ {zero} {suc b} p = 0≢1+n
¬==⇒≢ {suc a} {zero} p = 1+n≢0
¬==⇒≢ {suc a} {suc b} p suca≡sucb = ¬==⇒≢ p (suc-injective suca≡sucb)


-- A >-preserving function is monotone with respect to ≥
>Pres⇒Mono : (f : Nat → Nat) → >Pres f → monotone f
>Pres⇒Mono f >Presf a1 a2 a1≥a2 with a1 == a2 in p
... | false = <⇒≤ (>Presf a1 a2 (≤∧≢⇒< a1≥a2 (≢-sym (¬==⇒≢ p))))
... | true rewrite ==⇒≡ {a1} {a2} p = ≤-reflexive refl


-- Function that proves that mapping an evenness-preserving and >-preserving function over a list
-- whose elements are all even and appear in strictly decreasing order results in another such list
mapPres>&Even : (f : Nat → Nat) → (>Presf : >Pres f) → evenPres f → (xs : SList Nat) →
        SList^ even xs → >SList xs → ^Even&DecrSList (mapSList f (>Pres⇒Mono f >Presf) xs)
mapPres>&Even f >Presf evenPresf xs evenxs = SListDInd even
                                        (λ ys → >SList ys → ^Even&DecrSList (mapSListf ys))
                                        (λ y≥ys _ → >L y≥ys → ^Even&Decr≥L (map≥Lf y≥ys))
                                        hnil hcons htriv hextn xs evenxs where

          monof : monotone f
          monof = >Pres⇒Mono f >Presf

          mapSListf : SList Nat → SList Nat
          mapSListf = mapSList f monof

          map≥Lf : {x : Nat} → {xs : SList Nat} → x ≥L xs → f x ≥L mapSListf xs
          map≥Lf = map≥L f monof

          hnil : >SList snil → ^Even&DecrSList snil
          hnil tt = tt , tt

          hcons : {x : Nat} → {xs : SList Nat} → (x≥xs : x ≥L xs) →
            even x → (>SList xs → ^Even&DecrSList (mapSListf xs)) →
            (>L x≥xs → ^Even&Decr≥L (map≥Lf x≥xs)) →
            >SList (scons x≥xs) → ^Even&DecrSList (scons (map≥Lf x≥xs))
          hcons x≥xs evenx Plxs P≥xxs x>xs = P≥xxs x>xs

          htriv : {x : Nat} → even x → >L (triv {x = x}) → ^Even&Decr≥L {f x} triv
          htriv {x} evenx tt = evenPresf x evenx , tt

          hextn : {x y : Nat} → {ys : SList Nat} → (y≥ys : y ≥L ys) →
                  (x≥y : x Nat.≥ y) → (x≥ys : x ≥L ys) →
                  even x → even y →
                  (>SList ys → ^Even&DecrSList (mapSListf ys)) →
                  (>L y≥ys → ^Even&Decr≥L (map≥Lf y≥ys)) →
                  (>SList ys → ^Even&DecrSList (mapSListf ys)) →
                  (>L x≥ys → ^Even&Decr≥L (map≥Lf x≥ys)) →
                  >L (extn y≥ys x≥y x≥ys) →
                  ^Even&Decr≥L (extn (map≥Lf y≥ys) (monof x y x≥y) (map≥Lf x≥ys))
          hextn {x} {y} y≥ys x≥y x≥ys evenx eveny Plys1 P≥yys Plys2 P≥xys (x>y , x>ys , y>ys) =
              (^Even&Decr≥L⇒^Even (map≥Lf y≥ys) (P≥yys y>ys) ,
                ^Even&Decr≥L⇒^Even (map≥Lf x≥ys) (P≥xys x>ys)) ,
              >Presf x y x>y ,
              ^Even&Decr≥L⇒Decr (map≥Lf x≥ys) (P≥xys x>ys) ,
              ^Even&Decr≥L⇒Decr (map≥Lf y≥ys) (P≥yys y>ys)


----------- The following code is mentioned in the paper but does not appear there -----------

-- Test cases to verify that the computed proof is the proof we expect:


-- Example of a function that preserves evenness and >
2+ : Nat → Nat
2+ x = suc (suc x)

evenPres2+ : evenPres 2+
evenPres2+ x evenx = evenx

>Pres2+ : >Pres 2+
>Pres2+ a1 a2 a1>a2 = Nat.s≤s (Nat.s≤s a1>a2)


-- First test term
[6,4,2] : SList Nat
[6,4,2] = scons {x = 6}
               {xs = scons {x = 4}
                  {xs = scons {x = 2}
                    {xs = snil} triv}
                  (extn triv (m≤n+m 2 2) triv)}
               (extn (extn triv (m≤n+m 2 2) triv) (m≤n+m 4 2) (extn triv (m≤n+m 2 4) triv))

-- [6,4,2] is composed of even natural numbers in strictly decreasing order
^Even&Decr[6,4,2] : ^Even&DecrSList [6,4,2]
^Even&Decr[6,4,2] = ((tt , tt) , tt , tt) , (n≤1+n 5) , (m≤n+m 3 3 , tt , tt) , n≤1+n 3 , tt , tt

-- Result of mapping (2+) over every data element in [6,4,2]
map⟮2+⟯[6,4,2] : SList Nat
map⟮2+⟯[6,4,2] = mapSList 2+ (>Pres⇒Mono 2+ >Pres2+) [6,4,2]

-- Function that proves that the result of mapping (2+) over every data element in [6,4,2] is composed of even numbers in strictly decreasing order
^Even&DecrMap⟮2+⟯[6,4,2] : ^Even&DecrSList map⟮2+⟯[6,4,2]
^Even&DecrMap⟮2+⟯[6,4,2] = ((tt , tt) , tt , tt) , (n≤1+n 7) , (m≤n+m 5 3 , tt , tt) , n≤1+n 5 , tt , tt

-- Test that mapPres>&Even yields the proof we expect when applied to our first test term
mapPres>&EvenTest[6,4,2] : ^Even&DecrMap⟮2+⟯[6,4,2] ≡ mapPres>&Even 2+ >Pres2+ evenPres2+ [6,4,2]
    (^Even&DecrSList⇒^Even [6,4,2] ^Even&Decr[6,4,2]) (^Even&DecrSList⇒Decr [6,4,2] ^Even&Decr[6,4,2])
mapPres>&EvenTest[6,4,2] = refl


-- Second test term
[10,6,4,0] : SList Nat
[10,6,4,0] = scons {x = 10}
                  {xs = scons {x = 6}
                    {xs = scons {x = 4}
                      {xs = scons {x = 0}
                        {xs = snil} triv}
                      (extn triv Nat.z≤n triv)}
                    (extn (extn triv Nat.z≤n triv) (m≤n+m 4 2) (extn triv Nat.z≤n triv))}
                  (extn
                    (extn (extn triv Nat.z≤n triv) (m≤n+m 4 2) (extn triv Nat.z≤n triv))
                    (m≤n+m 6 4)
                    (extn (extn triv Nat.z≤n triv) (m≤n+m 4 6) (extn triv Nat.z≤n triv)))

-- [10,6,4,0] is composed of even natural numbers in strictly decreasing order
^Even&Decr[10,6,4,0] : ^Even&DecrSList [10,6,4,0]
^Even&Decr[10,6,4,0] = (((tt , tt) , tt , tt) , (tt , tt) , tt , tt) , m≤n+m 7 3 ,
    (m≤n+m 5 5 , (m≤n+m 1 9 , tt , tt) , m≤n+m 1 3 , tt , tt) , (n≤1+n 5) , (m≤n+m 1 5 , tt , tt) , m≤n+m 1 3 , tt , tt

-- Result of mapping (2+) over every data element in [10,6,4,0]
map⟮2+⟯[10,6,4,0] : SList Nat
map⟮2+⟯[10,6,4,0] = mapSList 2+ (>Pres⇒Mono 2+ >Pres2+) [10,6,4,0]

-- Function that proves that the result of mapping (2+) over every data element in [10,6,4,0] is composed of even numbers in strictly decreasing order
^Even&DecrMap⟮2+⟯[10,6,4,0] : ^Even&DecrSList map⟮2+⟯[10,6,4,0]
^Even&DecrMap⟮2+⟯[10,6,4,0] = (((tt , tt) , tt , tt) , (tt , tt) , tt , tt) , m≤n+m 9 3 , (m≤n+m 7 5 , (m≤n+m 3 9 , tt , tt) , m≤n+m 3 3 , tt , tt ) , n≤1+n 7 , (m≤n+m 3 5 , tt , tt) , m≤n+m 3 3 , tt , tt

-- Test that mapPres>&Even yields the proof we expect when applied to our second test term
mapPres>&EvenTest[10,6,4,0] : ^Even&DecrMap⟮2+⟯[10,6,4,0] ≡ mapPres>&Even 2+ >Pres2+ evenPres2+ [10,6,4,0]
    (^Even&DecrSList⇒^Even [10,6,4,0] ^Even&Decr[10,6,4,0]) (^Even&DecrSList⇒Decr [10,6,4,0] ^Even&Decr[10,6,4,0])
mapPres>&EvenTest[10,6,4,0] = refl


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


-- Code for the deep induction rule for the IIT of dense order completions:

{- Predicate lifting for the IIT of dense order completions derived from our construction
mutual
  *^ : {a : Set} → {{ord : TOrdered a}} → (a → Set) → a * → Set
  *^ Q (inj x) = Q x                                                  -- step (i)
  *^ Q (mid {x} {y} x<*y) = *^ Q x × *^ Q y ×                         -- step (i)
                            <*^ Q x<*y                                -- step (ii)

  <*^ : {a : Set} → {{ord : TOrdered a}} → (a → Set) → {x y : a *} → x <* y → Set
  <*^ Q (inj< {x} {y} x<y) = Q x × Q y ×                              -- step (i)
                             *^ Q (inj x) × *^ Q (inj y)              -- step (iii)
  <*^ Q (l<mid x<*y) = *^ Q x × *^ Q y × <*^ Q x<*y ×                 -- step (ii)
                       (*^ Q x × *^ Q y → *^ Q x × *^ Q (mid x<*y))   -- step (iii)
  <*^ Q (mid<r x<*y) = *^ Q x × *^ Q y × <*^ Q x<*y ×                 -- step (ii)
                       (*^ Q x × *^ Q y → *^ Q (mid x<*y) × *^ Q y)   -- step (iii)
-}

-- Predicate lifting for the IIT of dense order completions after simplification using DOCprojIndex below
mutual
  *^ : {a : Set} → {{ord : TOrdered a}} → (a → Set) → a * → Set
  *^ Q (inj x) = Q x
  *^ Q (mid x<*y) = <*^ Q x<*y
                    -- × *^ Q x × *^ Q y                                            -- can be obtained from <*^ Q x<*y using DOCprojIndex

  <*^ : {a : Set} → {{ord : TOrdered a}} → (a → Set) → {x y : a *} → x <* y → Set
  <*^ Q (inj< {x} {y} x<y) = *^ Q (inj x) × *^ Q (inj y)
                              -- × Q x × Q y                                        -- *^ Q (inj x) × *^ Q (inj y) simplify to these terms
  <*^ Q (l<mid x<*y) = *^ Q (mid x<*y)
                              -- × *^ Q x × *^ Q y                                  -- can be obtained from *^ Q (mid x<*y) using DOCprojIndex
                              -- × (*^ Q x × *^ Q y → *^ Q x × *^ Q (mid x<*y))     -- the conclusion of this arrow type is two terms:
                                                                                    -- *^ Q x can be obtained from *^ Q (mid x<*y) using DOCprojIndex
                                                                                    -- *^ Q (mid x<*y) is already present in this type
                                                                                    -- the arrow type can therefore be omitted

  <*^ Q (mid<r x<*y) = *^ Q (mid x<*y)
                              -- × *^ Q x × *^ Q y                                  -- can be obtained from *^ Q (mid x<*y) using DOCprojIndex
                              -- × (*^ Q x × *^ Q y → *^ Q (mid x<*y) × *^ Q y)     -- the conclusion of this arrow type is two terms:
                                                                                    -- *^ Q (mid x<*y) is already present in this type
                                                                                    -- *^ Q y can be obtained from *^ Q (mid x<*y) using DOCprojIndex
                                                                                    -- the arrow type can therefore be omitted


-- There is no analogue DOCprojPrim of CTprojPrim or SprojPrim for the IIT of dense order completions
-- because no new primitive data is needed to construct an element x<*y : x <* y

-- If Q can be lifted to x<*y, then Q can be lifted to x and Q can be lifted to y
DOCprojIndex : {a : Set} → {{ord : TOrdered a}} → {Q : a → Set} → {x y : a *} → (x<*y : x <* y) →
  <*^ Q x<*y → *^ Q x × *^ Q y
DOCprojIndex (inj< x<y) (Qx , Qy) = (Qx , Qy)
DOCprojIndex (l<mid x<*y) ^Qx<*y = (fst (DOCprojIndex x<*y ^Qx<*y) , ^Qx<*y)
DOCprojIndex (mid<r x<*y) ^Qx<*y = (^Qx<*y , snd (DOCprojIndex x<*y ^Qx<*y))


-- Deep induction rule for the IIT of dense order completions
mutual
  *DInd : {a : Set} → {{ord : TOrdered a}} →
    (Q : a → Set) →
    (P* : a * → Set) →
    (P<* : {x y : a *} → x <* y → P* x → P* y → Set) →
    (hinj : (x : a) → Q x → P* (inj x)) →
    (hmid : {x y : a *} → (x<*y : x <* y) → (P*x : P* x) → (P*y : P* y) → P<* x<*y P*x P*y → P* (mid x<*y)) →
    (hinj< : {x y : a} → (x<y : x < y) → (Qx : Q x) → (Qy : Q y) → P<* (inj< x<y) (hinj x Qx) (hinj y Qy)) →
    (hl<mid : {x y : a *} → (x<*y : x <* y) → (P*x : P* x) → (P*y : P* y) → (P<*x<*y : P<* x<*y P*x P*y) →
              P<* (l<mid x<*y) P*x (hmid x<*y P*x P*y P<*x<*y)) →
    (hmid<r : {x y : a *} → (x<*y : x <* y) → (P*x : P* x) → (P*y : P* y) → (P<*x<*y : P<* x<*y P*x P*y) →
              P<* (mid<r x<*y) (hmid x<*y P*x P*y P<*x<*y) P*y) →
    (x : a *) → *^ Q x → P* x
  *DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r (inj x) Qx = hinj x Qx
  *DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r (mid {x} {y} x<*y) ^Qx<*y = hmid x<*y
    (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r x (fst (DOCprojIndex x<*y ^Qx<*y)))
    (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r y (snd (DOCprojIndex x<*y ^Qx<*y)))
    (<*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r x<*y ^Qx<*y)

  <*DInd : {a : Set} → {{ord : TOrdered a}} →
    (Q : a → Set) →
    (P* : a * → Set) →
    (P<* : {x y : a *} → x <* y → P* x → P* y → Set) →
    (hinj : (x : a) → Q x → P* (inj x)) →
    (hmid : {x y : a *} → (x<*y : x <* y) → (P*x : P* x) → (P*y : P* y) → P<* x<*y P*x P*y → P* (mid x<*y)) →
    (hinj< : {x y : a} → (x<y : x < y) → (Qx : Q x) → (Qy : Q y) → P<* (inj< x<y) (hinj x Qx) (hinj y Qy)) →
    (hl<mid : {x y : a *} → (x<*y : x <* y) → (P*x : P* x) → (P*y : P* y) → (P<*x<*y : P<* x<*y P*x P*y) →
              P<* (l<mid x<*y) P*x (hmid x<*y P*x P*y P<*x<*y)) →
    (hmid<r : {x y : a *} → (x<*y : x <* y) → (P*x : P* x) → (P*y : P* y) → (P<*x<*y : P<* x<*y P*x P*y) →
              P<* (mid<r x<*y) (hmid x<*y P*x P*y P<*x<*y) P*y) →
    {x y : a *} → (x<*y : x <* y) → (^Qx<*y : <*^ Q x<*y) →
      P<* x<*y (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r x (fst (DOCprojIndex x<*y ^Qx<*y)))
                (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r y (snd (DOCprojIndex x<*y ^Qx<*y)))
  <*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r (inj< {x} {y} x<y) (Qx , Qy) = hinj< x<y Qx Qy
  <*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r (l<mid {x} {y} x<*y) ^Qx<*y = hl<mid x<*y
    (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r x (fst (DOCprojIndex x<*y ^Qx<*y)))
    (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r y (snd (DOCprojIndex x<*y ^Qx<*y)))
    (<*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r x<*y ^Qx<*y)
  <*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r (mid<r {x} {y} x<*y) ^Qx<*y = hmid<r x<*y
    (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r x (fst (DOCprojIndex x<*y ^Qx<*y)))
    (*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r y (snd (DOCprojIndex x<*y ^Qx<*y)))
    (<*DInd Q P* P<* hinj hmid hinj< hl<mid hmid<r x<*y ^Qx<*y)