Irrelevance-Issue.agda

open import Data.Nat as Nat

module Irrelevance-Issue (someMax₁ : ℕ) where

  open import Level using () renaming ( _⊔_ to _⊔ₗ_)
  open import Function

  open import Data.Fin as Fin renaming (_≟_ to _≟f_)
                              hiding (_<_; _≤_; _+_)
  open import Data.Product as Product
  open import Data.Vec as Vec
  open import Data.List as List
  open import Data.List.Any as LAny hiding (index)
  open import Data.List.All as LAll hiding (toList)
  open import Data.List.All.Properties as LAllP
  open import Data.Empty as Empty

  open import Data.Bool as Bool hiding (_≟_; _≤_; _<_)
  open import Data.Unit as Unit using (⊤; tt)

  open import Data.Maybe

  open import Data.Nat.Properties

  open import Relation.Binary.PropositionalEquality

{-
  m≤m : (m : ℕ) → m ≤ m
  m≤m zero = z≤n
  m≤m (suc m) = s≤s (m≤m m)
-}

  ≡⇒≤ : {n m : ℕ} → n ≡ m → n ≤ m
  ≡⇒≤ refl = m≤m _
  
  _∈_ : ∀ {a} {A : Set a} → A → List A → Set a
  a ∈ as = LAny.Any (a ≡_) as

  data AllTails {a} {A : Set a} {p} (P : A → List A → Set p) : List A → Set (a Level.⊔ p) where
    empty : AllTails P []
    cons : {x : A} → {xs : List A} → P x xs → AllTails P xs → AllTails P (x ∷ xs)

  Unique : ∀ {a} {A : Set a} → (xs : List A) → Set a
  Unique = AllTails (λ x ys → LAll.All (x ≢_) ys)

  SomeFin : Set
  SomeFin = Fin someMax₁

  data SomeData : Set where
    thing : SomeFin → SomeData
    notThing : SomeData

  IndexedSizedData : Set
  IndexedSizedData = Σ[ i ∈ SomeFin ] Σ[ s ∈ ℕ ] Vec SomeData s

  ISDList : Set
  ISDList = List IndexedSizedData

  indices : ISDList → List SomeFin
  indices = List.map proj₁

  isThing : SomeData → Set
  isThing (thing x) = ⊤
  isThing notThing = ⊥

  getFin[isThing] : (d : SomeData) → isThing d → SomeFin
  getFin[isThing] (thing x) tt = x
  getFin[isThing] notThing ()

  lookupById : {i : SomeFin} → {os : ISDList} → i ∈ (indices os) → IndexedSizedData
  lookupById {_} {[]} ()
  lookupById {_} {x ∷ _} (here refl) = x
  lookupById {_} {_ ∷ _} (there l) = lookupById l

  sizeEqualIfDataEqual : {o o' : IndexedSizedData} → o ≡ o' → (proj₁ $ proj₂ o) ≡ (proj₁ $ proj₂ o')
  sizeEqualIfDataEqual refl = refl

  idsUnique⇒membershipUnique : {i : SomeFin}
                             → {os : ISDList}
                             → (mem : i ∈ indices os)
                             → (mem' : i ∈ indices os)
                             → Unique (indices os)
                             → mem ≡ mem'
  idsUnique⇒membershipUnique {os = []} () mem' nubP
  idsUnique⇒membershipUnique {os = x ∷ os} (here refl) (here refl) nubP = refl
  idsUnique⇒membershipUnique {os = x ∷ os} (here refl) (there mem') (cons r _)
    = ⊥-elim $ LAllP.All¬⇒¬Any r mem'
  idsUnique⇒membershipUnique {os = x ∷ os} (there mem) (here refl) (cons r _)
    = ⊥-elim $ LAllP.All¬⇒¬Any r mem
  idsUnique⇒membershipUnique {os = x ∷ os} (there mem) (there mem') (cons _ nubP)
    = cong there $ idsUnique⇒membershipUnique mem mem' nubP

  sizesEqual⇒ProofsEqual : {sz : ℕ}
               → {v : ℕ}
               → (p₁ : sz ≡ v)
               → (p₂ : sz ≡ v)
               → p₁ ≡ p₂
  sizesEqual⇒ProofsEqual refl refl = refl

  inv : {mIdx mIdx' : Maybe SomeFin}
      → {datas datas' : ISDList}
      → (someStates : Vec Bool someMax₁)
      → ℕ
      → (size : ℕ)
      → (cIdx≡ : mIdx ≡ mIdx')
      → (cIdx : Is-just mIdx)
      → (membership : to-witness cIdx ∈ indices datas)
      → (membership' : to-witness (subst Is-just cIdx≡ cIdx) ∈ indices datas')
      → (lookupById membership ≡ lookupById membership')
      → (sizeRange : size ≤ (proj₁ $ proj₂ $ lookupById membership))
      → Set
  inv someStates idx size cIdx≡ cIdx membership membership' lookupData≡lookupData' sizeRange =
    (i : ℕ) → i < idx → (ip : i < size)
                         → (p' : isThing $ Vec.lookup (subst (Vec SomeData)
                                                                  (sym $ sizeEqualIfDataEqual lookupData≡lookupData')
                                                                  (proj₂ $ proj₂ $ lookupById $ membership'))
                                                           (fromℕ≤ $ ≤-trans ip sizeRange))
                         → T (Vec.lookup someStates
                                         (getFin[isThing] (Vec.lookup (subst (Vec SomeData)
                                                                             (sym $ sizeEqualIfDataEqual lookupData≡lookupData')
                                                                             (proj₂ $ proj₂ $ lookupById $ membership'))
                                                                      (fromℕ≤ $ ≤-trans ip sizeRange))
                                                          p'))

  om5-lemma11 : {mIdx mIdx' : Maybe SomeFin}
              → {datas datas' : ISDList}
              → {size : ℕ}
              → {someStates : Vec Bool someMax₁}
              → (cIdx≡ : mIdx ≡ mIdx')
              → datas ≡ datas'
              → Unique (indices datas)
              → (cIdx : Is-just mIdx)
              → (membership : to-witness cIdx ∈ indices datas)
              → (membership' : to-witness (subst Is-just cIdx≡ cIdx) ∈ indices datas')
              → (sizeRange : size ≤ (proj₁ $ proj₂ $ lookupById membership))
              → (sizeRange' : size ≤ (proj₁ $ proj₂ $ lookupById membership'))
              → (lookupData≡lookupData' : lookupById membership ≡ lookupById membership')
              → {idx : ℕ}
              -- → inv someStates idx size cIdx≡ cIdx membership membership' lookupData≡lookupData' sizeRange
              → (i : ℕ)
              → (i<idx' : i < suc idx)
              → (i≢idx : i ≢ idx)
              → (i<sz : i < size)
              -- → (p¬nil : isThing (Vec.lookup (proj₂ $ proj₂ $ lookupById $ membership')
              --                               (fromℕ≤ $ ≤-trans i<sz sizeRange')))
              → T $ Vec.lookup someStates {!!} {- (getFin[isThing] (Vec.lookup (proj₂ $ proj₂ $ lookupById $ membership')
                                                                       (fromℕ≤ $ ≤-trans i<sz sizeRange'))
                                                           p¬nil) -}
  om5-lemma11 refl refl uniqueP cIdx membership membership' sizeRange sizeRange' lookupData≡lookupData' {- invariant -} i (s≤s i<idx') i≢idx i<sz -- p¬nil
    with {!!}
  ... | x = {!!}
  -- rewrite sym $ idsUnique⇒membershipUnique membership membership' uniqueP
      -- | sym $ sizesEqual⇒ProofsEqual sizeRange sizeRange'
       -- | lookupData≡lookupData'
--     = {!!} -- inv i (≤∧≢⇒< i<idx' i≢idx) i<sz p¬nil