-
-
Save mietek/866c6b11c0d0f3a0e798244361691ebc to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 | |
om5-lemma11 : {mIdx mIdx' : Maybe SomeFin} | |
→ {datas datas' : ISDList} | |
→ {size size' : ℕ} | |
→ {someStates : Vec Bool someMax₁} | |
→ (cIdx≡ : mIdx ≡ mIdx') | |
→ datas ≡ datas' | |
→ (sz≡ : size ≡ size') | |
→ 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 : ℕ} | |
→ ((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'))) | |
→ (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 refl uniqueP cIdx membership membership' sizeRange sizeRange' lookupData≡lookupData' invariant i (s≤s i<idx') i≢idx i<sz p¬nil | |
rewrite sym $ idsUnique⇒membershipUnique membership membership' uniqueP | |
| sym $ sizesEqual⇒ProofsEqual sizeRange sizeRange' | |
| lookupData≡lookupData' | |
= {!!} -- inv i (≤∧≢⇒< i<idx' i≢idx) i<sz p¬nil |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment