Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement