text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Weight biased leftist heap that proves rank invariant: size of   --
-- left subtree of a node is not smaller than size of right         --
-- subtree. Uses a two-pass merging algorithm.                      --
----------------------------------------------------------------------

module TwoPassMerge.RankProof where

open import Basics

-- To prove the rank invariant we will index each Heap by its size,
-- (remember that size of a heap is its rank). Therefore index of
-- value n says that a Heap stores n elements. When merging two heaps
-- we will use the index to ensure that rank invariant is maintained.
--
-- Again, Heap has two constructor:
--
--  1) empty constructs a heap containing no elements. Therefore the
--     index is 0.
--
--  2) node takes two subtrees: one containing l elements, the other
--     containing r elements. The size of resulting heap is the sum of
--     l and r plus one for the element stored by the node itself. To
--     enforce the rank invariant node constructor expects a proof
--     that invariant holds: a value of type l ≥ r. If we can
--     construct value of this type then it proves the invariant.
data Heap : Rank → Set where
  empty : Heap zero
  node  : {l r : Rank} → Priority → l ≥ r →
          Heap l → Heap r → Heap (suc (l + r))

-- Since rank is now an index we no longer need rank function to
-- extract Rank from a node. We can pattern match on the index
-- instead.

-- Singleton heap stores only one element. Therefore it has size of
-- one. To prove the rank invariant we must show that 0 ≥ 0. We
-- construct a value of this type using ge0 constructor.
singleton : Priority → Heap one
singleton p = node p ge0 empty empty

-- Note [Proving rank invariant (merge using makeT)]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- Proving the rank invariant itself is surprisingly simple. We just
-- need to supply a proof that rank of left subtree is not smaller
-- than rank of right subtree. We can easily obtain evidence that it
-- is so by using order function which return result of comparing two
-- natural numbers (which will be tree ranks in this case) together
-- with a proof of the result.
--
-- But there is a different difficulty here. Since we index heaps by
-- their size we now require that makeT and merge construct trees of
-- correct size. Prooving this requires some substantial work on our
-- side.
--
-- We need to prove that the size of merged heap is equal to the sum
-- of sizes of heaps being merged. Recall that our merging algorithm
-- is two pass: we use merge to actually do the merging and makeT to
-- restore the rank invariant if necessary (see Note [Two-pass merging
-- algorithm]). This means our proof will be two-stage. We need to
-- prove that:
--
--  1) makeT creates a node of required size, even if it swaps left
--     and right children.
--
--  2) recursive calls to merge produce heaps of required size.

-- Note [Proving makeT]
-- ~~~~~~~~~~~~~~~~~~~~
--
-- makeT takes two subtrees of size l and r and produces a new tree of
-- size 1 + l + r. We must prove that each of two cases of makeT
-- returns tree of correct size:
--
--  1) size of l is ≥ than size of r: no extra proof is necessary as
--     everything follows from the definition of +.
--
--  2) size of r is ≥ than size of l: in this case we swap left and
--     right subtrees. This requires us to prove that:
--
--       suc (r + l) ≡ suc (l + r)
--
--     That proof is done using congruence on suc function and
--     commutativity of addition. We will define that proof as
--     makeT-lemma as we will be using in subsequent proofs.

makeT-lemma : (a b : Nat) → suc (a + b) ≡ suc (b + a)
makeT-lemma a b = cong suc (+comm a b)

makeT : {l r : Rank} → Priority → Heap l → Heap r → Heap (suc (l + r))
makeT {l-rank} {r-rank} p l r with order l-rank r-rank
makeT {l-rank} {r-rank} p l r | ge l≥r
  = node p l≥r l r
makeT {l-rank} {r-rank} p l r | le r≥l
  = subst Heap (makeT-lemma r-rank l-rank) (node p r≥l r l)

-- Note [Notation for proving heap merge]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- In the proofs of heap merge we will use following notation:
--
--  h1, h2 - rank of heaps being merged
--  p1, p2 - priority of root element
--  l1     - rank of left  subtree in the first  heap
--  r1     - rank of right subtree in the first  heap
--  l2     - rank of left  subtree in the second heap
--  r2     - rank of right subtree in the second heap
--
-- Note that:
--
--    h1 = suc (l1 + r1)
--    h2 = suc (l2 + r2)
--
--     h1         h2
--
--     p1         p2
--    /  \       /  \
--   /    \     /    \
--  l1    r1   l2    r2

-- Note [Proving merge]
-- ~~~~~~~~~~~~~~~~~~~~
--
-- We need to prove that all four cases of merge (see [Two-pass merging
-- algorithm]) produce heap of required size, which is h1 + h2. Since
-- in the proofs we will always operate on l1, r1, l2 and r2 we have:
--
--   h1 + h2 ̄≡ suc (l1 + r1) + suc (l2 + r2)
--           ≡ suc ((l1 + r1) + suc (l2 + r2))
--
-- (Second transformation comes from definition of +). This is the
-- expected size and therefore the final result we must prove in every
-- case that we analyze.

-- It is best to study the implementation of merge now and then read
-- the explanation of proofs.

-- Note [merge, proof 0a]
-- ~~~~~~~~~~~~~~~~~~~~~~
--
-- h1 ≡ 0, therefore: h1 + h2 ≡ 0 + h2 ≡ h2 ∎
--
-- This is definitional equality based on _+_
--
-- ∎

-- Note [merge, proof 0b]
-- ~~~~~~~~~~~~~~~~~~~~~~
--
-- h2 ≡ 0, therefore expected size is h1 + h2 ≡ h1 + 0. We need to
-- show that:
--
--    h1 ≡ h1 + 0
--
-- This is a simple statement that 0 is right identity of addition. We
-- proved that as one of basic properties of addition in
-- Basics.Reasoning module, except our proof had the sides of equality
-- reversed, ie. we proved a + 0 ≡ a, not a ≡ a + 0). We use symmetry
-- to construct a proof of latter from the former.
--
-- ∎

-- Note [merge, proof 1]
-- ~~~~~~~~~~~~~~~~~~~~~
--
-- We have p1 < p2. We keep p1 as the root and need to prove that
-- merging r1 with h2 gives correct size.  Here's how the term that
-- performs the merge corresponds to its type (for the sake of
-- readability I elided implict parameters):
--
--   makeT p1 x1 l1 (merge r1 (node p2 l2≥r2 l2 r2))
--    |          |         |   \__________________/
--    |   +------+         |            |
--    |   |     +----------+            |
--    |   |     |             +---------+
--    |   |     |     ________|__
--    |   |     |    /           \
--   suc (l1 + (r1 + suc (l2 + r2)))
--
-- Formally:
--
--   suc (l1 + (r1 + suc (l2 + r2))) ≡ suc ((l1 + r1) + suc (l2 + r2))
--
-- Recall that RHS of this equality comes from [Proving merge]. We
-- begin proof with congruence on suc:
--
--   cong suc X
--
-- where X proves
--
--   l1 + (r1 + suc (l2 + r2)) ≡ (l1 + r1) + suc (l2 + r2)
--
-- Substituting a = l1, b = r1 and c = suc (l2 + r2) we have
--
--   a + (b + c) ≡ (a + b) + c
--
-- Which is associativity of addition that we have already proved in
-- Basics.Reasoning.
--
-- ∎

proof-1 : (l1 r1 l2 r2 : Nat) → suc ( l1 + (r1 + suc (l2 + r2)))
                              ≡ suc ((l1 + r1) + suc (l2 + r2))
proof-1 l1 r1 l2 r2 = cong suc (+assoc l1 r1 (suc (l2 + r2)))

-- Note [merge, proof 2]
-- ~~~~~~~~~~~~~~~~~~~~~
--
-- We have p2 < p1. We keep p2 as the root and need to prove that
-- merging r2 with h1 gives correct size. Again, here's the
-- corespondence between the term and its type:
--
--   makeT p2 x2 l2 (merge r2 (node p1 l1≥r1 l1 r1))
--    |          |         |   \_________________/
--    |   +------+         |            |
--    |   |     +----------+  +---------+
--    |   |     |     ________|__
--    |   |     |    /           \
--   suc (l2 + (r2 + suc (l1 + r1)))
--
-- Formally:
--
--   suc (l2 + (r2 + suc (l1 + r1))) ≡ suc ((l1 + r1) + suc (l2 + r2))
--
-- Again we use cong to deal with the outer calls to suc and
-- substitute a = l2, b = r2 and c = l1 + r1. This leaves us with a
-- proof of lemma A:
--
--   a + (b + suc c) ≡ c + suc (a + b)
--
-- From associativity we know that:
--
--   a + (b + suc c) ≡ (a + b) + suc c
--
-- If we prove lemma B:
--
--  (a + b) + suc c = c + suc (a + b)
--
-- we can combine it using transitivity to get the final proof. We can
-- rewrite lemma B as:
--
--    n + suc m ≡ m + suc n
--
-- where n = a + b and m = c. From symmetry of +suc we have:
---
--   n + (suc m) ≡ suc (n + m)
--
-- Using transitivity we combine it with congruence on commutativity
-- of addition to prove:
--
--   suc (n + m) ≡ suc (m + n)
--
-- Again, using transitivity we combine it with +suc:
--
--   suc (m + n) ≡ m + suc n
--
-- Which proves lemma B and therefore the whole proof is complete.
--
-- ∎

lemma-B : (n m : Nat) → n + suc m ≡ m + suc n
lemma-B n m = trans (sym (+suc n m)) (trans (cong suc (+comm n m)) (+suc m n))

lemma-A : (a b c : Nat) → a + (b + suc c) ≡ c + suc (a + b)
lemma-A a b c = trans (+assoc a b (suc c)) (lemma-B (a + b) c)

proof-2 : (l1 r1 l2 r2 : Nat) → suc (l2 + (r2  + suc (l1 + r1)))
                              ≡ suc ((l1 + r1) + suc (l2 + r2))
proof-2 l1 r1 l2 r2 = cong suc (lemma-A l2 r2 (l1 + r1))

-- Note [Constructing equality proofs using transitivity]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- Now that constructed two specific proofs we can focus on a more
-- general technique used in both cases. Let's rewrite proof-2 in a
-- different fassion to see closely what is happening at each
-- step. Inlining lemmas A and B into proof-2 gives:
--
--   proof-2i : (l1 r1 l2 r2 : Nat) → suc (l2 + (r2  + suc (l1 + r1)))
--                                  ≡ suc ((l1 + r1) + suc (l2 + r2))
--   proof-2i l1 r1 l2 r2 =
--     cong suc (trans (+assoc l2 r2 (suc (l1 + r1)))
--              (trans (sym (+suc (l2 + r2) (l1 + r1)))
--              (trans (cong suc (+comm (l2 + r2) (l1 + r1)))
--                     (+suc (l1 + r1) (l2 + r2))))
--
-- We see a lot of properties combined using transitivity. In general,
-- if we have to prove:
--
--   a ≡ e
--
-- and we can prove:
--
--   a ≡ b, b ≡ c, c ≡ d, d ≡ e
--
-- then we can combine these proofs using transitivity:
--
--   trans (a ≡ b) (trans (b ≡ c) (trans (c ≡ d) (d ≡ e)))
--
-- While simple to use, combining proofs with transitivity can be not
-- so obvious at first. Let's rewrite the proof we have conducted
-- using following notation:
--
--  a ≡[ proof 1 ]
--  b ≡[ proof 2 ]
--  c ≡[ proof 3 ]
--  d ≡[ proof 4 ]
--  e ∎
--
-- Where proof 1 proves a ≡ b, proof 2 proves b ≡ c and so on. In our
-- particular case this will be:
--
--  suc  (l2 + (r2 + suc (l1 + r1))) ≡[ cong suc ]
-- [suc]  l2 + (r2 + suc (l1 + r1))  ≡[+assoc l2 r2 (suc (l1 + r1))]
-- [suc] (l2 + r2) + suc (l1 + r1)   ≡[ sym (+suc (l2 + r2) (l1 + r1))]
-- [suc] suc ((l2 + r2) + (l1 + r1)) ≡[ cong suc (+comm (l2 + r2) (l1 + r1)) ]
-- [suc] suc ((l1 + r1) + (l2 + r2)) ≡[+suc (l1 + r1) (l2 + r2) ]
-- [suc] (l1 + r1) + suc (l2 + r2) ∎
--
-- We use [suc] to denote that everything happens under a call to suc
-- (thanks to using congruence). Compare this notation with code of
-- proof-2i.

-- Note [Notation in merge]
-- ~~~~~~~~~~~~~~~~~~~~~~~~
--
-- merge uses different notation than the proofs. We use l1, r1, l2
-- and r2 to denote the respective subtrees and l1-rank, r1-rank,
-- l2-rank and r2-rank to denote their ranks. We use h1 and h2 to
-- denote heaps.
merge : {l r : Rank} → Heap l → Heap r → Heap (l + r)
merge empty h2 = h2 -- See [merge, proof 0a]
merge {suc l} {zero} h1 empty
  = subst Heap (sym (+0 (suc l))) h1 -- See [merge, proof 0b]
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {l1-rank} {r1-rank} p1 l1≥r1 l1 r1)
  (node {l2-rank} {r2-rank} p2 l2≥r2 l2 r2)
  with p1 < p2
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {l1-rank} {r1-rank} p1 l1≥r1 l1 r1)
  (node {l2-rank} {r2-rank} p2 l2≥r2 l2 r2)
  | true
  = subst Heap
          (proof-1 l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 1]
          (makeT p1 l1 (merge r1 (node p2 l2≥r2 l2 r2)))
merge {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {l1-rank} {r1-rank} p1 l1≥r1 l1 r1)
  (node {l2-rank} {r2-rank} p2 l2≥r2 l2 r2)
  | false
  = subst Heap
          (proof-2 l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 2]
          (makeT p2 l2 (merge r2 (node p1 l1≥r1 l1 r1)))

-- We require that inserting an element into the heap increases its
-- size by one. As previously we define insert as merge and a
-- singleton heap. Size of singleton heap is (suc zero), while already
-- existing heap has size n. According to definition of merge the
-- resulting heap will therefore have size:
--
--   (suc zero) + n
--
-- By definition of + this can be normalized to:
--
--   suc (zero + n)
--
-- and finally to
--
--   suc n
--
-- Which is size we require in the type signature. This means we don't
-- need any additional proof because expected result follows from
-- definitions.
insert : {n : Rank} → Priority → Heap n → Heap (suc n)
insert p h = merge (singleton p) h

-- By indexing heap with its size we can finally have means to ensure
-- that heap passed to findMin or deleteMin is not empty.
findMin : {n : Rank} → Heap (suc n) → Priority
findMin (node p _ _ _) = p

deleteMin : {n : Rank} → Heap (suc n) → Heap n
deleteMin (node _ _ l r) = merge l r

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
------------------------------------------------------------------------
-- M-types
------------------------------------------------------------------------

{-# OPTIONS --without-K --sized-types #-}

open import Equality

module M
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq as Bijection using (_↔_)
open Derived-definitions-and-properties eq
import Equivalence eq as Eq
open import Function-universe eq hiding (_∘_)
open import Function-universe.Size eq
open import H-level eq
open import H-level.Closure eq
open import Prelude
open import Prelude.Size

------------------------------------------------------------------------
-- M-types

mutual

  data M {a b} (A : Type a) (B : A → Type b) (i : Size) :
         Type (a ⊔ b) where
    dns : (x : A) (f : B x → M′ A B i) → M A B i

  record M′ {a b} (A : Type a) (B : A → Type b) (i : Size) :
            Type (a ⊔ b) where
    coinductive
    field
      force : {j : Size< i} → M A B j

open M′ public

-- Projections.

pɐǝɥ : ∀ {a b i} {A : Type a} {B : A → Type b} →
       M A B i → A
pɐǝɥ (dns x f) = x

lıɐʇ : ∀ {a b i} {j : Size< i} {A : Type a} {B : A → Type b} →
       (x : M A B i) → B (pɐǝɥ x) → M A B j
lıɐʇ (dns x f) y = force (f y)

------------------------------------------------------------------------
-- Equality

-- M-types are isomorphic to Σ-types containing M-types (almost).

M-unfolding : ∀ {a b} {i} {A : Type a} {B : A → Type b} →
              M A B i ↔ ∃ λ (x : A) → B x → M′ A B i
M-unfolding = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (dns x f) → x , f }
      ; from = uncurry dns
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = λ { (dns x f) → refl (dns x f) }
  }

abstract

  -- Equality between elements of an M-type can be proved using a pair
  -- of equalities (assuming extensionality and a kind of η law).
  --
  -- Note that, because the equality type former is not sized, this
  -- lemma is perhaps not very useful.

  M-≡,≡↔≡ :
    ∀ {a b i} {A : Type a} {B : A → Type b} →
    Extensionality b (a ⊔ b) →
    (∀ {x} {f g : B x → M′ A B i} →
       _≡_ {A = B x → {j : Size< i} → M A B j}
           (force ∘ f) (force ∘ g) ↔
       f ≡ g) →
    ∀ {x y} {f : B x → M′ A B i} {g : B y → M′ A B i} →
    (∃ λ (p : x ≡ y) → ∀ b {j : Size< i} →
       force (f b) {j = j} ≡ force (g (subst B p b))) ↔
    _≡_ {A = M A B i} (dns x f) (dns y g)
  M-≡,≡↔≡ {a} {i = i} {A} {B} ext η {x} {y} {f} {g} =
    (∃ λ (p : x ≡ y) → ∀ b {j : Size< i} →
       force (f b) {j = j} ≡ force (g (subst B p b)))         ↝⟨ ∃-cong lemma ⟩
    (∃ λ (p : x ≡ y) → subst (λ x → B x → M′ A B i) p f ≡ g)  ↝⟨ Bijection.Σ-≡,≡↔≡ ⟩
    (_≡_ {A = ∃ λ (x : A) → B x → M′ A B i} (x , f) (y , g))  ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ M-unfolding) ⟩□
    (dns x f ≡ dns y g)                                       □
    where
    lemma : (p : x ≡ y) →
            ((b : B x) {j : Size< i} →
             f b .force {j = j} ≡ g (subst B p b) .force) ↔
            (subst (λ x → B x → M′ A B i) p f ≡ g)
    lemma p = elim
      (λ {x y} p → (f : B x → M′ A B i) (g : B y → M′ A B i) →
                   (∀ b {j : Size< i} → f b .force {j = j} ≡
                                        g (subst B p b) .force) ↔
                   (subst (λ x → B x → M′ A B i) p f ≡ g))
      (λ x f g →
         (∀ b {j : Size< i} → f b .force {j = j} ≡
                              g (subst B (refl x) b) .force)            ↝⟨ subst (λ h → (∀ b {j : Size< i} → f b .force ≡ g (h b) .force) ↔
                                                                                (∀ b {j : Size< i} → f b .force ≡ g b .force))
                                                                                (sym (apply-ext (lower-extensionality lzero a ext)
                                                                                (subst-refl B)))
                                                                                Bijection.id ⟩

         (∀ b {j : Size< i} → f b .force {j = j} ≡ g b .force)          ↔⟨ ∀-cong ext (λ _ → implicit-Π-size-≃-Π-size) ⟩

         (∀ b (j : Size< i) → f b .force {j = j} ≡ g b .force)          ↔⟨ ∀-cong ext (λ _ → Π-size-≃) ⟩

         (∀ b (j : Size< i in-type) → f b .force {j = size j} ≡
                                      g b .force {j = size j})          ↔⟨ ∀-cong ext (λ _ → Eq.extensionality-isomorphism
                                                                                (lower-extensionality _ lzero ext)) ⟩
         ((b : B x) → _≡_ {A = (j : Size< i in-type) → M A B (size j)}
                          (λ j → f b .force {j = size j})
                          (λ j → g b .force {j = size j}))              ↔⟨ ∀-cong ext (λ _ → Eq.≃-≡ $ Eq.↔⇒≃ Bijection.implicit-Π↔Π) ⟩

         ((b : B x) → _≡_ {A = {j : Size< i in-type} → M A B (size j)}
                          (λ {j} → f b .force {j = size j})
                          (λ {j} → g b .force {j = size j}))            ↔⟨ ∀-cong ext (λ _ → Eq.≃-≡ implicit-Π-size-≃) ⟩

         ((b : B x) → _≡_ {A = {j : Size< i} → M A B j}
                          (λ { {j} → f b .force {j = j} })
                          (λ { {j} → g b .force {j = j} }))             ↔⟨ Eq.extensionality-isomorphism ext ⟩

         (force ∘ f ≡ force ∘ g)                                        ↝⟨ η ⟩

         (f ≡ g)                                                        ↝⟨ subst (λ h → (f ≡ g) ↔ (h ≡ g))
                                                                                (sym $ subst-refl (λ x' → B x' → M′ A B i) f)
                                                                                Bijection.id ⟩□
         (subst (λ x → B x → M′ A B i) (refl x) f ≡ g)                  □)
      p f g

------------------------------------------------------------------------
-- Bisimilarity and bisimilarity for bisimilarity

-- Bisimilarity.

mutual

  infix 4 [_]_≡M_ [_]_≡M′_

  data [_]_≡M_ {a b} {A : Type a} {B : A → Type b}
               (i : Size) (x y : M A B ∞) : Type (a ⊔ b) where
    dns : (p : pɐǝɥ x ≡ pɐǝɥ y) →
          (∀ b → [ i ] lıɐʇ x b ≡M′ lıɐʇ y (subst B p b)) →
          [ i ] x ≡M y

  record [_]_≡M′_ {a b} {A : Type a} {B : A → Type b}
                  (i : Size) (x y : M A B ∞) : Type (a ⊔ b) where
    coinductive
    field
      force : {j : Size< i} → [ j ] x ≡M y

open [_]_≡M′_ public

-- Projections.

pɐǝɥ≡ :
  ∀ {a b i} {A : Type a} {B : A → Type b} {x y : M A B ∞} →
  [ i ] x ≡M y → pɐǝɥ x ≡ pɐǝɥ y
pɐǝɥ≡ (dns p q) = p

lıɐʇ≡ :
  ∀ {a b i} {A : Type a} {B : A → Type b} {x y : M A B ∞} →
  (p : [ i ] x ≡M y) →
  ∀ b {j : Size< i} → [ j ] lıɐʇ x b ≡M lıɐʇ y (subst B (pɐǝɥ≡ p) b)
lıɐʇ≡ (dns p q) y = force (q y)

-- Equality implies bisimilarity.

≡⇒≡M : ∀ {a b i} {A : Type a} {B : A → Type b} {x y : M A B ∞} →
       x ≡ y → [ i ] x ≡M y
≡⇒≡M {i = i} {B = B} {dns x f} {dns y g} p =
  dns (proj₁ q) helper
  where
  q = elim (λ {m m′} m≡m′ →
              ∃ λ (x≡y : pɐǝɥ m ≡ pɐǝɥ m′) →
                  ∀ b → lıɐʇ m b ≡ lıɐʇ m′ (subst B x≡y b))
           (λ m → refl (pɐǝɥ m) , λ b →
              lıɐʇ m b                            ≡⟨ cong (lıɐʇ m) (sym $ subst-refl B _) ⟩∎
              lıɐʇ m (subst B (refl (pɐǝɥ m)) b)  ∎)
           p

  helper :
    ∀ b →
    [ i ] lıɐʇ (dns x f) b ≡M′ lıɐʇ (dns y g) (subst B (proj₁ q) b)
  force (helper b) = ≡⇒≡M (proj₂ q b)

-- Bisimilarity for the bisimilarity type.

mutual

  data [_]_≡≡M_ {a b} {A : Type a} {B : A → Type b} {x y : M A B ∞}
                (i : Size) (p q : [ ∞ ] x ≡M y) : Type (a ⊔ b) where
    dns : (r : pɐǝɥ≡ p ≡ pɐǝɥ≡ q) →
          (∀ b → [ i ] lıɐʇ≡ p b ≡≡M′
                       subst (λ p → [ ∞ ] lıɐʇ x b ≡M
                                          lıɐʇ y (subst B p b))
                             (sym r)
                             (lıɐʇ≡ q b)) →
          [ i ] p ≡≡M q

  record [_]_≡≡M′_ {a b} {A : Type a} {B : A → Type b} {x y : M A B ∞}
                   (i : Size) (p q : [ ∞ ] x ≡M y) : Type (a ⊔ b) where
    coinductive
    field
      force : {j : Size< i} → [ j ] p ≡≡M q

open [_]_≡≡M′_ public

------------------------------------------------------------------------
-- Closure under various h-levels

abstract

  -- If we assume a notion of extensionality (bisimilarity implies
  -- equality) then Contractible is closed under M.

  M-closure-contractible :
    ∀ {a b} {A : Type a} {B : A → Type b} →
    ({x y : M A B ∞} → [ ∞ ] x ≡M y → x ≡ y) →
    Contractible A → Contractible (M A B ∞)
  M-closure-contractible {A = A} {B} ext (z , irrA) = (x , ext ∘ irr)
    where
    x : ∀ {i} → M A B i
    x = dns z λ _ → λ { .force → x }

    irr : ∀ {i} y → [ i ] x ≡M y
    irr {i} (dns x′ f) = dns (irrA x′) helper
      where
      helper : ∀ y → [ i ] x ≡M′ force (f (subst B (irrA x′) y))
      force (helper _) = irr _

  -- The same applies to Is-proposition.

  M-closure-propositional :
    ∀ {a b} {A : Type a} {B : A → Type b} →
    ({x y : M A B ∞} → [ ∞ ] x ≡M y → x ≡ y) →
    Is-proposition A → Is-proposition (M A B ∞)
  M-closure-propositional {A = A} {B} ext p =
    λ x y → ext $ irrelevant x y
    where
    irrelevant : ∀ {i} (x y : M A B ∞) → [ i ] x ≡M y
    irrelevant {i} (dns x f) (dns y g) = dns (p x y) helper
      where
      helper :
        (y′ : B x) →
        [ i ] force (f y′) ≡M′ force (g (subst B (p x y) y′))
      force (helper _) = irrelevant _ _

  -- If we assume that we have another notion of extensionality, then
  -- Is-set is closed under M.

  M-closure-set :
    ∀ {a b} {A : Type a} {B : A → Type b} →
    ({x y : M A B ∞} {p q : x ≡ y} → [ ∞ ] ≡⇒≡M p ≡≡M ≡⇒≡M q → p ≡ q) →
    Is-set A → Is-set (M A B ∞)
  M-closure-set {A = A} {B} ext s =
    λ p q → ext $ uip (≡⇒≡M p) (≡⇒≡M q)
    where
    uip : ∀ {i} {x y : M A B ∞} (p q : [ ∞ ] x ≡M y) → [ i ] p ≡≡M q
    uip {i} {x} {y} (dns p f) (dns q g) = dns (s p q) helper
      where
      helper :
        (b : B (pɐǝɥ x)) →
        [ i ] force (f b) ≡≡M′
              subst (λ eq → [ ∞ ] lıɐʇ x b ≡M lıɐʇ y (subst B eq b))
                    (sym (s p q))
                    (force (g b))
      force (helper _) = uip _ _

ext: agda

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Sane where

import Data.Fin as F
--
-- open import Data.Empty
open import Data.Unit
-- open import Data.Unit.Core
open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _>_ )
open import Data.Sum using (inj₁ ; inj₂ )
-- open import Data.Product renaming (map to _×→_)
open import Data.Vec
open import Function using ( id ) renaming (_∘_ to _○_)
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong ; module ≡-Reasoning )
open ≡-Reasoning

-- start re-splitting things up, as this is getting out of hand
open import FT -- Finite Types
open import VecHelpers
open import NatSimple
open import Eval

-- not sure where else to put this [Z][A]
hetType : {A B : Set} → (a : A) → A ≡ B → B
hetType a refl = a

-- construct a combinator which represents the swapping of the i-th and
-- (i+1)-th 'bit' of a finite type.
-- Best to think of this as an 'elementary permutation', in the same way
-- we have 'elementary matrices' (which turn out to be permutations when they
-- are unitary).
swapi : {n : ℕ} → F.Fin n → (fromℕ (suc n)) ⇛ (fromℕ (suc n))
swapi {zero}  ()
swapi {suc n} F.zero    = assocl₊⇛ ◎ swap₊⇛ ⊕ id⇛ ◎ assocr₊⇛
swapi {suc n} (F.suc i) = id⇛ ⊕ swapi {n} i

-- swapUpTo i permutes the combinator left by one up to i
-- if possible values are X a b c Y d e, swapUpTo 3's possible outputs
-- are a b c X Y d e
swapUpTo : {n : ℕ} → F.Fin n → (fromℕ (suc n)) ⇛ (fromℕ (suc n))
swapUpTo F.zero    = id⇛
swapUpTo (F.suc i) = (id⇛ ⊕ swapUpTo i) ◎ swapi F.zero

-- swapDownFrom i permutes the combinator right by one up to i (the reverse
-- of swapUpTo)
swapDownFrom : {n : ℕ} → F.Fin n → (fromℕ (suc n)) ⇛ (fromℕ (suc n))
swapDownFrom F.zero    = id⇛
swapDownFrom (F.suc i) = swapi F.zero ◎ (id⇛ ⊕ swapDownFrom i)

-- TODO: verify that this is actually correct
-- Idea: To swap n < m with each other, swap n, n + 1, ... , m - 1, m, then
-- go back down, so that m and n are swapped and everything else is in the
-- same spot
-- makeSingleComb {combinator size} (arrayElement) (arrayIndex),
-- gives a combinator which 'does' that, assuming i<j, else id⇛
makeSingleComb : {n : ℕ} → F.Fin n → F.Fin n → (fromℕ n) ⇛ (fromℕ n)
makeSingleComb F.zero   F.zero     = id⇛
makeSingleComb F.zero   (F.suc i)  = id⇛
makeSingleComb (F.suc j) F.zero   = swapDownFrom j ◎ swapi j ◎ swapUpTo j
makeSingleComb (F.suc j) (F.suc i) = id⇛ ⊕ makeSingleComb j i

-- swapm i returns a combinator that swaps 0 and i
swapm : {n : ℕ} → F.Fin n → (fromℕ n) ⇛ (fromℕ n)
swapm F.zero = id⇛
swapm (F.suc i) = swapUpTo i ◎ swapi i ◎ swapDownFrom i

-- Correctness: after putting together i indices, the partial combinator c' is
-- represented by the vector [1, 2, ... , n - (i +1)] ++ (last i v)
--
-- Might want to bake in the correctness proof here---have the output be a
-- combinator c, a vector v, and a proof that vecRep c v, then we just prove
-- that the vector at the end is just the vector from the beginning
--
-- Or just put them together and prove that they're related by vecRep with
-- foldrWorks and that the end vector is the input vector; this is probably simpler
-- (and is the approach currently reflected in the code below)

-- swapInd i j returns a vector v′ where v′[i] = j, v′[j] = i, and v′[k] = k
-- where k != j and k != i

zeroIfEq : {n n′ : ℕ} → F.Fin n → F.Fin n → F.Fin (suc n′) → F.Fin (suc n′)
zeroIfEq F.zero    F.zero   ret = F.zero
zeroIfEq F.zero   (F.suc j) ret = ret
zeroIfEq (F.suc i) F.zero   ret = ret
zeroIfEq (F.suc i) (F.suc j) ret = zeroIfEq i j ret

swapIndFn : {n : ℕ} → F.Fin n → F.Fin n → (F.Fin n → F.Fin n)
swapIndFn               F.zero     j          F.zero   = j
swapIndFn               (F.suc i)  F.zero     F.zero   = F.suc i
swapIndFn               (F.suc i) (F.suc j)   F.zero   = F.zero
swapIndFn               F.zero     F.zero    (F.suc x) = F.suc x
swapIndFn {suc zero}    F.zero   (F.suc ()) (F.suc x)
swapIndFn {suc (suc n)} F.zero   (F.suc j)  (F.suc x) = zeroIfEq j x (F.suc x)
swapIndFn               (F.suc i)  F.zero    (F.suc x) = zeroIfEq i x (F.suc x)
swapIndFn               (F.suc i) (F.suc j)  (F.suc x) = F.suc (swapIndFn i j x)

swapInd : {n : ℕ} → F.Fin n → F.Fin n → Vec (F.Fin n) n
swapInd i j = tabulate (swapIndFn i j)

swapIndVec : {n : ℕ} → F.Fin n → F.Fin n → Vec (F.Fin n) n → Vec (F.Fin n) n
swapIndVec i j v = tabulate (λ k → v !! swapIndFn i j k)

-- useful abbreviations
2+ : ℕ → ℕ
2+ n = suc (suc n)

3+ : ℕ → ℕ
3+ n = suc (2+ n)

F2+ : {n : ℕ} → F.Fin n → F.Fin (2+ n)
F2+ i = F.suc (F.suc i)

F3+ : {n : ℕ} → F.Fin n → F.Fin (3+ n)
F3+ i = F.suc (F2+ i)

swap01 : {n : ℕ} → Vec (F.Fin (2+ n)) (2+ n)
swap01 = F.suc F.zero ∷ F.zero ∷ tabulate F2+

swapIndIdAfterOne : {n : ℕ} → (i : F.Fin n) →
                    (F2+ i) ≡ swapIndFn F.zero (F.suc F.zero) (F2+ i)
swapIndIdAfterOne i = refl -- yesss finally it just works!

swapIndSucDist : {n : ℕ} → (i j x : F.Fin n) →
                 (F.suc (swapIndFn i j x)) ≡
                 (swapIndFn (F.suc i) (F.suc j) (F.suc x))
swapIndSucDist i j x = refl

-- more useful abbreviations
F1+swap : {n : ℕ} → (i : F.Fin n) → Vec (F.Fin (2+ n)) (suc n)
F1+swap i = vmap F.suc (swapInd (F.inject₁ i) (F.suc i))

swapIndFn+ : {n : ℕ} → (i : F.Fin n) → F.Fin (suc n) → F.Fin (suc n)
swapIndFn+ i = swapIndFn (F.inject₁ i) (F.suc i)

swapInd++ : {n : ℕ} → (i : F.Fin n) → Vec (F.Fin (2+ n)) (2+ n)
swapInd++ i = swapInd (F.inject₁ (F.suc i)) (F2+ i)

swap≡ind₁ : {n : ℕ} → (i : F.Fin n) → F.zero ∷ F1+swap i ≡ swapInd++ i
swap≡ind₁ {n} i = begin
  F.zero ∷ F1+swap i
    ≡⟨ cong (_∷_ F.zero)
      (begin
          F1+swap i
        ≡⟨ mapTab F.suc (swapIndFn+ i) ⟩
          tabulate (F.suc ○ swapIndFn+ i)
        ≡⟨ tabf∼g _ _ (swapIndSucDist (F.inject₁ i) (F.suc i)) ⟩
          (tabulate (swapIndFn+ (F.suc i) ○ F.suc)
          ∎)) ⟩
  swapInd++ i ∎

-- vecRep c v relates a combinator c over normal types to the output
-- vector it results in. This works only over a subset of combinators
-- used in decompilation.
data vecRep : {n : ℕ} → (fromℕ n) ⇛ (fromℕ n) → Vec (F.Fin n) n → Set where
  vr-id    : {n : ℕ} → vecRep (id⇛ {fromℕ n}) (upTo n)
  vr-swap  : {n : ℕ} → vecRep {suc (suc n)} (swapi {suc n} F.zero) swap01
  vr-comp  : {n : ℕ} {c₁ c₂ : (fromℕ n) ⇛ (fromℕ n)} {v₁ v₂ : Vec (F.Fin n) n} →
    vecRep c₁ v₁ → vecRep c₂ v₂ →
    vecRep (c₁ ◎ c₂) (v₁ ∘̬ v₂)
  vr-plus : {n : ℕ} → {c : (fromℕ n) ⇛ (fromℕ n)} → {v : Vec (F.Fin n) n} →
    vecRep {n} c v →
    vecRep {suc n} (id⇛ ⊕ c) (F.zero ∷ (vmap F.suc v))

-- Record for keeping a combinator, a vector, and a proof that they compute
-- the same function.
record Compiled (n : ℕ) : Set where
  constructor
    _►_⟨_⟩
  field
    comb   : (fromℕ n) ⇛ (fromℕ n)
    vec    : Vec (F.Fin n) n
    proof  : vecRep comb vec

-- TODO: there might be a better vector to put in the vecRep here
-- we'll need to see what's most amenable to proving swapUpToWorks
swapiWorks : {n : ℕ} → (i : F.Fin n) → vecRep (swapi i) (swapInd (F.inject₁ i) (F.suc i))
swapiWorks {zero} ()
swapiWorks {suc n} F.zero = vr-swap
swapiWorks {suc n} (F.suc i) =
    hetType (vr-plus (swapiWorks i)) (cong (vecRep (id⇛ ⊕ swapi i)) (swap≡ind₁ i))

-- permutations on vectors for specifying swapUpTo/DownFrom

data _<F_ : {n : ℕ} → F.Fin n → F.Fin n → Set where
  zero-leq : {n : ℕ} → {i : F.Fin n} → F.zero <F (F.suc i)
  suc-leq  : {n : ℕ} → {i j : F.Fin n} → i <F j → (F.suc i) <F (F.suc j)

<suc : {n : ℕ} → (i j : F.Fin n) → (F.suc i) <F (F.suc j) → i <F j
<suc i j (suc-leq p) = p

dec<F : {n : ℕ} → (i j : F.Fin n) → Dec (i <F j)
dec<F F.zero    F.zero   = no (λ ())
dec<F F.zero   (F.suc j) = yes zero-leq
dec<F (F.suc i) F.zero   = no (λ ())
dec<F (F.suc i) (F.suc j) with dec<F i j
dec<F (F.suc i) (F.suc j) | yes x = yes (suc-leq x)
dec<F (F.suc i) (F.suc j) | no x = no (λ p → x (<suc i j p))

-- swap args of F.inject+
inj+ : {m n : ℕ} → F.Fin m → F.Fin (n + m)
inj+ {m} {n} i = hetType (F.inject+ n i) (cong F.Fin (+-comm m n))

-- the library definition of + on Fin isn't what we want here, ugh
_+F_ : {m n : ℕ} → F.Fin (suc m) → F.Fin n → F.Fin (m + n)
_+F_ {m} {zero} F.zero ()
_+F_ {m} {suc n} F.zero j = inj+ {suc n} {m} j
_+F_ {zero} {n} (F.suc ()) _
_+F_ {suc m} {n} (F.suc i) j = F.suc (i +F j)

data _h≡_ {A : Set} : {B : Set} → A → B → Set₁ where
  hrefl : (x : A) → _h≡_ {A} {A} x x

hetTypeIsID : {A B : Set} → (x : A) → (p : A ≡ B) → (hetType x p) h≡ x
hetTypeIsID x refl = hrefl x

-- Permute the first i elements of v to the right one (and i^th down to 0)
-- Should correspond with swapDownFrom
-- permuteRight : {n : ℕ} → (i : F.Fin n) → Vec (F.Fin n) n → Vec (F.Fin n) n
-- permuteRight i v = tabulate (permRightFn v i)

permuteRight : {n : ℕ} → (i : F.Fin n) → Vec (F.Fin n) n
permuteRight {zero} ()
permuteRight {suc n} F.zero = upTo _
permuteRight {suc zero} (F.suc ())
permuteRight {suc (suc n)} (F.suc i) =
  F.suc (head (permuteRight i)) ∷ F.zero ∷ vmap F.suc (tail (permuteRight i))

-- redundant helper
permRightID : {n : ℕ} → F.Fin n → Vec (F.Fin n) n
permRightID i = permuteRight i

-- The opposite of permuteRight; should correspond with swapUpTo
pl′ : {m : ℕ} {A : Set} → F.Fin m → Vec A m → A → Vec A (suc m)
pl′ {m = zero} () _ _
pl′ {m = suc m} F.zero (x ∷ xs) first = x ∷ first ∷ xs
pl′ (F.suc i) (x ∷ xs) first = x ∷ (pl′ i xs first)

permuteLeft : {n : ℕ} {A : Set} → (i : F.Fin n) → Vec A n → Vec A n
permuteLeft {zero} () _
permuteLeft {suc n} F.zero v = v
permuteLeft {suc zero} (F.suc ()) _
permuteLeft {suc (suc n)} (F.suc i) (a ∷ b ∷ rest) = pl′ i (b ∷ rest) a

permLeftID : {n : ℕ} → F.Fin n → Vec (F.Fin n) n
permLeftID i = permuteLeft i (upTo _)

permLeftId₀ : {n : ℕ} → (upTo (suc n)) ≡ permuteLeft F.zero (upTo (suc n))
permLeftId₀ {n} = refl

permLeftIdPasti : {n : ℕ} → (v : Vec (F.Fin (2+ n)) (2+ n)) →
                  (i : F.Fin n) →
                  permuteLeft (F.suc F.zero) v !! (F2+ i) ≡ v !! F2+ i
permLeftIdPasti (x ∷ x₁ ∷ x₂ ∷ v) F.zero = refl
permLeftIdPasti (x ∷ x₁ ∷ x₂ ∷ v) (F.suc i) = refl

-- it should actually be possible to recur on this!
-- and as an added bonus, it should actually be true! [Z]
plCorr : {m n : ℕ} (v : Vec (F.Fin m) n) (i : F.Fin n) →
         vmap F.suc (pl′ i (vmap F.suc v) F.zero) ∘̬′ swap01 ≡
         pl′ i (vmap F.suc (vmap F.suc v)) F.zero
plCorr [] ()
plCorr (x ∷ v) F.zero =
  begin
  vmap F.suc (pl′ F.zero (vmap F.suc (x ∷ v)) F.zero) ∘̬′ swap01
    ≡⟨ refl ⟩
  (F.suc (F.suc x) ∷ F.suc F.zero ∷ vmap F.suc (vmap F.suc v)) ∘̬′ swap01
    ≡⟨ refl ⟩
  ((tabulate (F.suc ○ F.suc)) !! x) ∷ (F.suc F.zero ∷ vmap F.suc (vmap F.suc v)) ∘̬′ swap01
    ≡⟨ cong (λ x → x ∷ (F.suc F.zero ∷ vmap F.suc (vmap F.suc v)) ∘̬′ swap01)
            (lookupTab x) ⟩
  (F.suc (F.suc x)) ∷ ((F.suc F.zero ∷ vmap F.suc (vmap F.suc v)) ∘̬′ swap01)
    ≡⟨ refl ⟩
  (F.suc (F.suc x)) ∷ F.zero ∷ ((vmap F.suc (vmap F.suc v)) ∘̬′ swap01)
    ≡⟨ cong (λ q → F.suc (F.suc x) ∷ F.zero ∷ q) (map2+id v) ⟩
  F.suc (F.suc x) ∷ F.zero ∷ vmap F.suc (vmap F.suc v)
    ≡⟨ refl ⟩
  pl′ F.zero (vmap F.suc (vmap F.suc (x ∷ v))) F.zero ∎
plCorr (x ∷ v) (F.suc i) =
  begin
  vmap F.suc (pl′ (F.suc i) (vmap F.suc (x ∷ v)) F.zero) ∘̬′ swap01
    ≡⟨ refl ⟩
  (tabulate (F.suc ○ F.suc) !! x) ∷
    ((vmap F.suc (pl′ i (vmap F.suc v) F.zero)) ∘̬′ swap01)
    ≡⟨ cong (λ q → q ∷ ((vmap F.suc (pl′ i (vmap F.suc v) F.zero)) ∘̬′ swap01))
            (lookupTab x) ⟩
  F.suc (F.suc x) ∷
    ((vmap F.suc (pl′ i (vmap F.suc v) F.zero)) ∘̬′ swap01)
    ≡⟨ cong (_∷_ (F.suc (F.suc x))) (plCorr v i) ⟩
  F.suc (F.suc x) ∷ pl′ i (vmap F.suc (vmap F.suc v)) F.zero
    ≡⟨ refl ⟩
  pl′ (F.suc i) (vmap F.suc (vmap F.suc (x ∷ v))) F.zero ∎

fzero : F.Fin 7
fzero = F.zero

fone : F.Fin 7
fone = F.suc F.zero

ftwo : F.Fin 7
ftwo = F.suc (F.suc F.zero)

fthree : F.Fin 7
fthree = F.suc (F.suc (F.suc F.zero))

ffour : F.Fin 7
ffour = F.suc (F.suc (F.suc (F.suc F.zero)))

ffive : F.Fin 7
ffive = F.suc (F.suc (F.suc (F.suc (F.suc F.zero))))

fsix : F.Fin 7
fsix = F.suc (F.suc (F.suc (F.suc (F.suc (F.suc F.zero)))))

--

gzero : F.Fin 6
gzero = F.zero

gone : F.Fin 6
gone = F.suc F.zero

gtwo : F.Fin 6
gtwo = F.suc (F.suc F.zero)

gthree : F.Fin 6
gthree = F.suc (F.suc (F.suc F.zero))

gfour : F.Fin 6
gfour = F.suc (F.suc (F.suc (F.suc F.zero)))

gfive : F.Fin 6
gfive = F.suc (F.suc (F.suc (F.suc (F.suc F.zero))))

-- i=3
-- n=5

test1 : Vec (F.Fin 7) 7
test1 = permuteLeft
          ffour
          (fzero ∷ fone ∷ ftwo ∷ fthree ∷ ffour ∷ ffive ∷ fsix ∷ [])

{--
test1 = (0 1)
        (1 2)
        (2 3)
        (3 4)
        (4 0)
        (5 5)
        (6 6)
--}

test2 : Vec (F.Fin 6) 6
test2 = permuteLeft
          gthree
          (gzero ∷ gone ∷ gtwo ∷ gthree ∷ gfour ∷ gfive ∷ [])

{--
test2 = (0 1)
        (1 2)
        (2 3)
        (3 0)
        (4 4)
        (5 5)

vmap F.suc test2 =
        (0 2)
        (1 3)
        (2 4)
        (3 1)
        (4 5)
        (5 6)

F.zero ∷ vmap F.suc test2 =
        (0 0)
        (1 2)
        (2 3)
        (3 4)
        (4 1)
        (5 5)
        (6 6)

swap01 =
        (0 1)
        (1 0)
        (2 2)
        (3 3)
        (4 4)
        (5 5)
        (6 6)

(F.zero ∷ vmap F.suc test2) ∘̬ swap01 =
        (0 1)
        (1 2)
        (2 3)
        (3 4)
        (4 0)
        (5 5)
        (6 6)

test1 = (0 1)
        (1 2)
        (2 3)
        (3 4)
        (4 0)
        (5 5)
        (6 6)

--}

-- glue lemma between plCorr and swapUpToWorks to deal with the difference between
-- the result type of swapUpToWorks and the result type of the VecRep combinators
-- We need this glue here to get from swapUpToWorks (which has two calls to permuteLeft)
-- to plCorr (which has two calls to pl′), since permuteLeft is a wrapper around pl′.
-- Once we've removed the wrapper, we can eat the delicious candy^W^W^W^Wactually do
-- induction; hopefully the type of plCorr is general enough for this but not too general
-- to, er, be true. [Z]
sucWorks : {n : ℕ} → (i : F.Fin n) →
                  (F.zero ∷ vmap F.suc (permuteLeft (F.inject₁ i) (upTo (suc n))))
                  ∘̬ swap01
                  ≡ pl′ {suc n} (F.inject₁ i) (tail (upTo (suc (suc n)))) F.zero
sucWorks {suc n} F.zero =
  begin
    (F.zero ∷ vmap F.suc (permuteLeft F.zero (upTo (suc (suc n)))))
    ∘̬ swap01
      ≡⟨ cong (λ x → (F.zero ∷ vmap F.suc x) ∘̬ swap01)
               (sym (permLeftId₀)) ⟩
    (F.zero ∷ vmap F.suc (upTo (suc (suc n))))
    ∘̬ swap01
       ≡⟨ cong (λ x → (F.zero ∷ x) ∘̬ swap01) ((mapTab F.suc id)) ⟩
    upTo (suc (suc (suc n))) ∘̬ swap01
      ≡⟨ ∘̬simpleid swap01 ⟩
    swap01
      ≡⟨ refl ⟩
    pl′ F.zero (tail (upTo (suc (suc (suc n))))) F.zero ∎
sucWorks {suc zero} (F.suc ())
sucWorks {suc (suc n)} (F.suc i) =
  begin
    (F.zero ∷ vmap F.suc (permuteLeft (F.inject₁ (F.suc i)) (upTo (suc (suc (suc n))))))
    ∘̬ swap01
      ≡⟨ ∘̬≡∘̬′
           (F.zero ∷
            vmap F.suc
            (permuteLeft (F.inject₁ (F.suc i)) (upTo (suc (suc (suc n))))))
           swap01 ⟩
    (F.zero ∷ vmap F.suc (permuteLeft (F.inject₁ (F.suc i)) (upTo (suc (suc (suc n))))))
    ∘̬′ swap01
      ≡⟨ refl ⟩
    (F.zero ∷ vmap F.suc (pl′ (F.inject₁ i) (tail (upTo (suc (suc (suc n))))) F.zero))
    ∘̬′ swap01
      ≡⟨ refl ⟩
    (F.suc F.zero) ∷
      ((vmap F.suc (pl′ (F.inject₁ i) (tabulate F.suc) F.zero))
      ∘̬′ swap01)
      ≡⟨ cong
           (λ q →
              F.suc F.zero ∷ vmap F.suc (pl′ (F.inject₁ i) q F.zero) ∘̬′ swap01)
           (sym (mapTab F.suc id)) ⟩
    (F.suc F.zero) ∷
      ((vmap F.suc (pl′ (F.inject₁ i) (vmap F.suc (tabulate id)) F.zero))
      ∘̬′ swap01)
      ≡⟨ cong (_∷_ (F.suc F.zero)) (plCorr (tabulate id) (F.inject₁ i)) ⟩
    (F.suc F.zero) ∷
      (pl′ (F.inject₁ i) (vmap F.suc (vmap F.suc (tabulate id))) F.zero)
      ≡⟨ cong (λ q → F.suc F.zero ∷ pl′ (F.inject₁ i) (vmap F.suc q) F.zero)
           (mapTab F.suc id) ⟩
    (F.suc F.zero) ∷ pl′ (F.inject₁ i) (vmap F.suc (tail (upTo (suc (suc (suc n)))))) F.zero
      ≡⟨ cong (λ x → (F.suc F.zero) ∷ pl′ (F.inject₁ i) x F.zero)
               (sym (upToTail (suc (suc n)))) ⟩
    F.suc F.zero ∷ pl′ (F.inject₁ i) (tail (tail (upTo (suc (suc (suc (suc n))))))) F.zero
      ≡⟨ refl ⟩
    pl′ (F.inject₁ (F.suc i)) (tail (upTo (suc (suc (suc (suc n)))))) F.zero ∎

-- NB: I added the F.inject₁ in calls to permuteLeft/Right to get it to work
-- with swapUpTo/DownFrom; I'm not sure that this is correct? It might
-- be a sign that the type of the swap functions is too specific, instead.
-- (though now it looks like it will at least make the type of shuffle a bit nicer) [Z]
swapUpToWorks : {n : ℕ} → (i : F.Fin n) →
                vecRep (swapUpTo i) (permuteLeft (F.inject₁ i) (upTo (suc n)))
swapUpToWorks F.zero = vr-id
swapUpToWorks (F.suc i) = hetType (vr-comp (vr-plus (swapUpToWorks i)) vr-swap)
                         (cong (vecRep (swapUpTo (F.suc i))) (sucWorks i))

sdfWorks : {n : ℕ} → (i : F.Fin (suc n)) →
           swap01 ∘̬ (F.zero ∷ vmap F.suc (permuteRight i)) ≡
           permuteRight (F.suc i)
sdfWorks i =
  begin
  swap01 ∘̬ (F.zero ∷ vmap F.suc (permuteRight i))
    ≡⟨ ∘̬≡∘̬′ swap01 (F.zero ∷ vmap F.suc (permuteRight i)) ⟩
  swap01 ∘̬′ (F.zero ∷ vmap F.suc (permuteRight i))
    ≡⟨ refl ⟩
  (vmap F.suc (permuteRight i) !! F.zero) ∷ F.zero ∷
    (tabulate (F.suc ○ F.suc) ∘̬′ (F.zero ∷ vmap F.suc (permuteRight i)))
    ≡⟨ cong
         (λ q →
            q ∷
            F.zero ∷
            tabulate (F.suc ○ F.suc) ∘̬′
            (F.zero ∷ vmap F.suc (permuteRight i)))
         (head!!0 (vmap F.suc (permuteRight i))) ⟩
  (head (vmap F.suc (permuteRight i))) ∷ F.zero ∷
    (tabulate (F.suc ○ F.suc) ∘̬′ (F.zero ∷ vmap F.suc (permuteRight i)))
    ≡⟨ cong
         (λ q →
            q ∷
            F.zero ∷
            tabulate (F.suc ○ F.suc) ∘̬′
            (F.zero ∷ vmap F.suc (permuteRight i)))
         (headmap (permuteRight i)) ⟩
  (F.suc (head (permuteRight i))) ∷ F.zero ∷
    (tabulate (F.suc ○ F.suc) ∘̬′ (F.zero ∷ vmap F.suc (permuteRight i)))
    ≡⟨ cong (λ q → F.suc (head (permuteRight i)) ∷ F.zero ∷ q)
         (sym
          (∘̬≡∘̬′ (tabulate (F.suc ○ F.suc))
           (F.zero ∷ vmap F.suc (permuteRight i)))) ⟩
  (F.suc (head (permuteRight i))) ∷ F.zero ∷
    (tabulate (F.suc ○ F.suc) ∘̬ (F.zero ∷ vmap F.suc (permuteRight i)))
    ≡⟨ cong (λ q → F.suc (head (permuteRight i)) ∷ F.zero ∷ q)
         (2suc∘̬2tail (F.zero ∷ vmap F.suc (permuteRight i))) ⟩
  (F.suc (head (permuteRight i))) ∷ F.zero ∷
    (tail (vmap F.suc (permuteRight i)))
    ≡⟨ cong (λ q → F.suc (head (permuteRight i)) ∷ F.zero ∷ q)
         (tailmap (permuteRight i)) ⟩
  (F.suc (head (permuteRight i))) ∷ F.zero ∷ (vmap F.suc (tail (permuteRight i)))
    ≡⟨ refl ⟩
  permuteRight (F.suc i) ∎

swapDownFromWorks : {n : ℕ} → (i : F.Fin n) →
                    vecRep (swapDownFrom i) (permuteRight (F.inject₁ i))
swapDownFromWorks F.zero = vr-id
swapDownFromWorks (F.suc i) =
  hetType (vr-comp vr-swap (vr-plus (swapDownFromWorks i)))
          (cong (vecRep (swapDownFrom (F.suc i))) (sdfWorks (F.inject₁ i)))

_◎∘̬_ : {n : ℕ} → Compiled n → Compiled n → Compiled n
(c₁ ► v₁ ⟨ p₁ ⟩) ◎∘̬ (c₂ ► v₂ ⟨ p₂ ⟩) = ((c₁ ◎ c₂) ► v₁ ∘̬ v₂ ⟨ vr-comp p₁ p₂ ⟩ )

vecToComb : {n : ℕ} → Vec (F.Fin n) n → (fromℕ n) ⇛ (fromℕ n)
vecToComb {n} vec =
  foldr (λ i → fromℕ n ⇛ fromℕ n) _◎_ id⇛ (map (λ i → makeSingleComb (vec !! i) i) (upTo n))

finToVal : {n : ℕ} → F.Fin n → ⟦ fromℕ n ⟧
finToVal F.zero = inj₁ tt
finToVal (F.suc n) = inj₂ (finToVal n)

valToFin : {n : ℕ} → ⟦ fromℕ n ⟧ → F.Fin n
valToFin {zero} ()
valToFin {suc n} (inj₁ tt) = F.zero
valToFin {suc n} (inj₂ v) = F.suc (valToFin v)

finToValToFin : {n : ℕ} → (v : ⟦ fromℕ n ⟧) → finToVal (valToFin v) ≡ v
finToValToFin {zero} ()
finToValToFin {suc n} (inj₁ tt)  = refl -- (inj₁ tt)
finToValToFin {suc n} (inj₂ v) = cong inj₂ (finToValToFin v)

valToFinToVal : {n : ℕ} → (i : F.Fin n) → valToFin (finToVal i) ≡ i
valToFinToVal F.zero = refl -- F.zero
valToFinToVal (F.suc i) = cong F.suc (valToFinToVal i)

combToVec : {n : ℕ} → (fromℕ n) ⇛ (fromℕ n) → Vec (F.Fin n) n
combToVec c = tabulate (valToFin ○ (evalComb c) ○ finToVal)

twoF4 : F.Fin four
twoF4 = F.suc (F.suc F.zero)

fourF5 : F.Fin five
fourF5 = F.suc (F.suc F.zero)

swapUpToTest : Vec (F.Fin five) five
swapUpToTest = combToVec (swapUpTo twoF4)

pltest : (n : ℕ) → (i : F.Fin n) → Vec (F.Fin n) n
pltest n i = permuteLeft i (upTo n)

prtest : Vec (F.Fin five) five
prtest = permuteRight fourF5 -- (F.suc (F.suc (F.suc (F.suc F.zero))))

sdftest : Vec (F.Fin five) five
sdftest = combToVec (swapDownFrom twoF4)

sucomptest : {n : ℕ} → (i : F.Fin n) → Vec (F.Fin (suc (suc n))) (suc (suc n))
sucomptest {n} i = (F.zero ∷ vmap F.suc (permuteLeft (F.inject₁ i) (upTo (suc n))))
                   ∘̬ (F.suc F.zero ∷ F.zero ∷ vmap (F.suc ○ F.suc) (upTo n))

sit : Vec (F.Fin five) five
sit = combToVec (swapi (F.suc (F.suc F.zero)))

mntest : Vec (F.Fin five) five
mntest = combToVec (makeSingleComb (F.suc (F.suc (F.suc F.zero))) F.zero)

evalVec : {n : ℕ} → Vec (F.Fin n) n → F.Fin n → ⟦ fromℕ n ⟧
evalVec vec i = finToVal (lookup i vec)

permLeftTest : F.Fin four
permLeftTest = valToFin (evalVec (permLeftID (F.suc (F.suc F.zero))) (F.zero))

lookupToEvalVec : {n : ℕ} → (i : F.Fin n) → (v : Vec (F.Fin n) n) → lookup i v ≡ valToFin (evalVec v i)
lookupToEvalVec i v = sym (valToFinToVal (lookup i v) )

--  Might want to take a ⟦ fromℕ n ⟧ instead of a Fin n as the second
--  argument here?
combToVecWorks : {n : ℕ} → (c : (fromℕ n) ⇛ (fromℕ n)) →
  (i : F.Fin n) → (evalComb c (finToVal i)) ≡ evalVec (combToVec c) i
combToVecWorks c i = (sym (finToValToFin _)) ∘ (cong finToVal (sym (lookupTab i)))

-- This lemma is the hammer that will let us use vecRep to (hopefully) simply
-- prove some lemmas about the helper functions used in vecToComb, then apply
-- vecRepWorks at the end to make sure they all "do the right thing"
vecRepWorks : {n : ℕ} → {c : (fromℕ n) ⇛ (fromℕ n)} → {v : Vec (F.Fin n) n} →
  vecRep c v → (i : F.Fin n) → (evalVec v i) ≡ (evalComb c (finToVal i))
vecRepWorks vr-id i = cong finToVal (lookupTab i)
vecRepWorks vr-swap F.zero = refl -- (inj₂ (inj₁ tt))
vecRepWorks vr-swap (F.suc F.zero) = refl -- (inj₁ tt)
vecRepWorks {suc (suc n)} vr-swap (F.suc (F.suc i)) = cong finToVal (lookupTab i)
vecRepWorks (vr-comp {n} {c₁} {c₂} {v₁} {v₂} vr vr₁) i = begin
  finToVal (lookup i (tabulate (λ j → lookup (lookup j v₁) v₂)))
 ≡⟨ cong finToVal (lookup∘tabulate i (λ j → lookup (lookup j v₁) v₂)) ⟩
  finToVal (lookup (lookup i v₁) v₂)
 ≡⟨ cong (λ x → finToVal (lookup x v₂)) (lookupToEvalVec i v₁) ⟩
  finToVal (lookup (valToFin (evalVec v₁ i)) v₂)
 ≡⟨ cong (λ x → finToVal (lookup (valToFin x) v₂)) (vecRepWorks vr i) ⟩
  finToVal (lookup (valToFin (evalComb c₁ (finToVal i))) v₂)
 ≡⟨ cong finToVal (lookupToEvalVec (valToFin (evalComb c₁ (finToVal i))) v₂) ⟩
  finToVal (valToFin (evalVec v₂ (valToFin (evalComb c₁ (finToVal i)))))
 ≡⟨ finToValToFin (evalVec v₂ (valToFin (evalComb c₁ (finToVal i)))) ⟩
 evalVec v₂ (valToFin (evalComb c₁ (finToVal i)))
 ≡⟨ vecRepWorks vr₁ (valToFin (evalComb c₁ (finToVal i))) ⟩
 evalComb c₂ (finToVal (valToFin (evalComb c₁ (finToVal i))))
 ≡⟨ cong (evalComb c₂) (finToValToFin (evalComb c₁ (finToVal i))) ⟩
 evalComb (c₁ ◎ c₂) (finToVal i) ∎
vecRepWorks {suc n} (vr-plus vr) F.zero = refl -- (inj₁ tt)
vecRepWorks (vr-plus {c = c} {v = v} vr) (F.suc i) = begin
  evalVec (F.zero ∷ vmap F.suc v) (F.suc i)  ≡⟨ cong finToVal (map!! F.suc v i) ⟩
  inj₂ (finToVal (v !! i))                  ≡⟨ cong inj₂ (vecRepWorks vr i) ⟩
  (evalComb (id⇛ ⊕ c) (finToVal (F.suc i)) ∎)

record Permut (n : ℕ) : Set where
  constructor per
  field
    vec : Vec (F.Fin n) n
    uniq : ∀ {i j : F.Fin n} → (vec !! i) ≡ (vec !! j) → i ≡ j

-- this should also take a proof that i>0.
pred′ : {n : ℕ} (i : F.Fin (suc (suc n))) → F.Fin (suc n)
pred′ F.zero = F.zero
pred′ (F.suc i) = i

record NormComb (n : ℕ) : Set where
  constructor ⟪_,_⟫
  field
    v : Vec (F.Fin n) n
    -- We can't actually have it be the stronger condition and still be
    -- able to properly recur on it as in vtc′.
    p : ∀ (i : F.Fin n) (j : F.Fin′ i) → (v !! (F.inject j) ≡ i) → (v !! i ≡ (F.inject j))

predToSuc : {n : ℕ} (i : F.Fin (suc n)) (j : F.Fin′ i) (x : F.Fin (suc (suc n)))
            (v : Vec (F.Fin (suc (suc n))) (suc n)) →
            vmap pred′ v !! F.inject j ≡ i →
            (∀ (i : F.Fin (suc (suc n))) (j : F.Fin′ i) →
              ((x ∷ v) !! (F.inject j) ≡ i) → ((x ∷ v) !! i ≡ (F.inject j))) →
            (x ∷ v) !! F.inject (F.suc j) ≡ F.suc i
predToSuc i j x v p p₁ =
  begin
    (x ∷ v) !! F.inject (F.suc j)
      ≡⟨ refl ⟩
    v !! F.inject j
      ≡⟨ {!refl!} ⟩
    F.suc i ∎

nctail : {n : ℕ} → NormComb (suc n) → NormComb n
nctail {zero}  ⟪ x ∷ [] , p ⟫ = ⟪ [] , (λ ()) ⟫
nctail {suc n} ⟪ x ∷ v , p ⟫ = ⟪ vmap pred′ v , {!!} ⟫

vtc′ : {n : ℕ} (v : Vec (F.Fin n) n) → (fromℕ n) ⇛ (fromℕ n)
vtc′ {zero} [] = id⇛
vtc′ {suc zero} (x ∷ []) = id⇛ -- can only swap with itself
vtc′ {suc (suc n)} (F.zero ∷ v) = id⇛ ⊕ (vtc′ (vmap pred′ v))
vtc′ {suc (suc n)} ((F.suc i) ∷ v) =
  (id⇛ ⊕ (vtc′ (vmap pred′ v))) ◎ (swapm (F.suc i))

testvtc : {n : ℕ} → Vec (F.Fin n) n → Vec (F.Fin n) n
testvtc v = combToVec (vtc′ v)

testvtc0 : {n : ℕ} → Vec (F.Fin n) n → Vec (F.Fin n) n
testvtc0 v = combToVec (vecToComb v)

pl2 : Vec (F.Fin 5) 5
pl2 = permuteLeft (F.suc (F.suc F.zero)) (upTo 5)

pr2 : Vec (F.Fin 5) 5
pr2 = permuteRight (F.suc (F.suc F.zero))

pred∘suc : {n : ℕ} (x : F.Fin (suc (suc n))) → ((F.toℕ x) > zero) → F.suc (pred′ x) ≡ x
pred∘suc F.zero ()
pred∘suc (F.suc _)  _ = refl

-- Assumptions we need so far:
-- - If the first element of a vec is zero, no other element is zero
--   (to prove that "vmap F.suc (vmap pred′ v) == v")
-- - Probably something for the last case, too
magic1 : {n : ℕ} (v : Vec (F.Fin n) n) → vecRep (vtc′ v) v
magic1 {zero} [] = vr-id
magic1 {suc zero} (F.zero ∷ []) = vr-id
magic1 {suc zero} (F.suc () ∷ [])
-- this will need something reminiscent of LeftCancellation?
magic1 {suc (suc n)} (F.zero ∷ v) = hetType
    (vr-plus (magic1 {suc n} (vmap pred′ v)))
    (cong (λ x → vecRep (id⇛ ⊕ vtc′ (vmap pred′ v)) (F.zero ∷ x))
    ((vmap∘vmap F.suc pred′ v) ∘ (vmap∘id {!!}) ))
-- swap and recurse?
magic1 {suc (suc n)} (F.suc x ∷ v) = {!!}

-- [JC] flip the conclusion around, as 'evalVec v i' is trivial.  Makes
-- equational reasoning easier
vecToCombWorks : {n : ℕ} →
  (v : Vec (F.Fin n) n) → (i : F.Fin n) →
  (evalComb (vtc′ v) (finToVal i)) ≡ (evalVec v i)
vecToCombWorks v i = sym (vecRepWorks (magic1 v) i)

------------------------------------------------------------------
-- Goal:

lemma1 : {n : ℕ} (v : Vec (F.Fin n) n) → (i : F.Fin n) →
    (evalVec v i) ≡ (evalComb (vtc′ v) (finToVal i))
lemma1 v i = sym (vecToCombWorks v i)

lemma2 : {n : ℕ} (c : (fromℕ n) ⇛ (fromℕ n)) → (i : F.Fin n) →
    (evalComb c (finToVal i)) ≡ evalVec (combToVec c) i
lemma2 c i = combToVecWorks c i

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Data.Vec.Membership.Properties where

open import Data.Vec
open import Data.Vec.Membership
open import Data.Vec.Any.Membership.Propositional

max_stars_repo_name: tizmd/agda-vector-any

max_issues_repo_name: tizmd/agda-vector-any

max_forks_repo_name: tizmd/agda-vector-any


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Susp where

open import Cubical.HITs.Susp.Base public

-- open import Cubical.HITs.Susp.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical