SHARE
TWEET

Untitled

a guest Aug 25th, 2019 74 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. open import Data.Nat as Nat
  2.  
  3. module Irrelevance-Issue (someMax₁ : ℕ) where
  4.  
  5.   open import Level using () renaming ( _⊔_ to _⊔ₗ_)
  6.   open import Function
  7.  
  8.   open import Data.Fin as Fin renaming (_≟_ to _≟f_)
  9.                               hiding (_<_; _≤_; _+_)
  10.   open import Data.Product as Product
  11.   open import Data.Vec as Vec
  12.   open import Data.List as List
  13.   open import Data.List.Any as LAny hiding (index)
  14.   open import Data.List.All as LAll hiding (toList)
  15.   open import Data.List.All.Properties as LAllP
  16.   open import Data.Empty as Empty
  17.  
  18.   open import Data.Bool as Bool hiding (_≟_; _≤_; _<_)
  19.   open import Data.Unit as Unit using (⊤; tt)
  20.  
  21.   open import Data.Maybe
  22.  
  23.   open import Data.Nat.Properties
  24.  
  25.   open import Relation.Binary.PropositionalEquality
  26.  
  27. {-
  28.   m≤m : (m : ℕ) → m ≤ m
  29.   m≤m zero = z≤n
  30.   m≤m (suc m) = s≤s (m≤m m)
  31. -}
  32.  
  33.   ≡⇒≤ : {n m : ℕ} → n ≡ m → n ≤ m
  34.   ≡⇒≤ refl = m≤m _
  35.  
  36.   _∈_ : ∀ {a} {A : Set a} → A → List A → Set a
  37.   a ∈ as = LAny.Any (a ≡_) as
  38.  
  39.   data AllTails {a} {A : Set a} {p} (P : A → List A → Set p) : List A → Set (a Level.⊔ p) where
  40.     empty : AllTails P []
  41.     cons : {x : A} → {xs : List A} → P x xs → AllTails P xs → AllTails P (x ∷ xs)
  42.  
  43.   Unique : ∀ {a} {A : Set a} → (xs : List A) → Set a
  44.   Unique = AllTails (λ x ys → LAll.All (x ≢_) ys)
  45.  
  46.   SomeFin : Set
  47.   SomeFin = Fin someMax₁
  48.  
  49.   data SomeData : Set where
  50.     thing : SomeFin → SomeData
  51.     notThing : SomeData
  52.  
  53.   IndexedSizedData : Set
  54.   IndexedSizedData = Σ[ i ∈ SomeFin ] Σ[ s ∈ ℕ ] Vec SomeData s
  55.  
  56.   ISDList : Set
  57.   ISDList = List IndexedSizedData
  58.  
  59.   indices : ISDList → List SomeFin
  60.   indices = List.map proj₁
  61.  
  62.   isThing : SomeData → Set
  63.   isThing (thing x) = ⊤
  64.   isThing notThing = ⊥
  65.  
  66.   getFin[isThing] : (d : SomeData) → isThing d → SomeFin
  67.   getFin[isThing] (thing x) tt = x
  68.   getFin[isThing] notThing ()
  69.  
  70.   lookupById : {i : SomeFin} → {os : ISDList} → i ∈ (indices os) → IndexedSizedData
  71.   lookupById {_} {[]} ()
  72.   lookupById {_} {x ∷ _} (here refl) = x
  73.   lookupById {_} {_ ∷ _} (there l) = lookupById l
  74.  
  75.   sizeEqualIfDataEqual : {o o' : IndexedSizedData} → o ≡ o' → (proj₁ $ proj₂ o) ≡ (proj₁ $ proj₂ o')
  76.   sizeEqualIfDataEqual refl = refl
  77.  
  78.   idsUnique⇒membershipUnique : {i : SomeFin}
  79.                              → {os : ISDList}
  80.                              → (mem : i ∈ indices os)
  81.                              → (mem' : i ∈ indices os)
  82.                              → Unique (indices os)
  83.                              → mem ≡ mem'
  84.   idsUnique⇒membershipUnique {os = []} () mem' nubP
  85.   idsUnique⇒membershipUnique {os = x ∷ os} (here refl) (here refl) nubP = refl
  86.   idsUnique⇒membershipUnique {os = x ∷ os} (here refl) (there mem') (cons r _)
  87.     = ⊥-elim $ LAllP.All¬⇒¬Any r mem'
  88.   idsUnique⇒membershipUnique {os = x ∷ os} (there mem) (here refl) (cons r _)
  89.     = ⊥-elim $ LAllP.All¬⇒¬Any r mem
  90.   idsUnique⇒membershipUnique {os = x ∷ os} (there mem) (there mem') (cons _ nubP)
  91.     = cong there $ idsUnique⇒membershipUnique mem mem' nubP
  92.  
  93.   sizesEqual⇒ProofsEqual : {sz : ℕ}
  94.                → {v : ℕ}
  95.                → (p₁ : sz ≡ v)
  96.                → (p₂ : sz ≡ v)
  97.                → p₁ ≡ p₂
  98.   sizesEqual⇒ProofsEqual refl refl = refl
  99.  
  100.   inv : {mIdx mIdx' : Maybe SomeFin}
  101.       → {datas datas' : ISDList}
  102.       → (someStates : Vec Bool someMax₁)
  103.       → ℕ
  104.       → (size : ℕ)
  105.       → (cIdx≡ : mIdx ≡ mIdx')
  106.       → (cIdx : Is-just mIdx)
  107.       → (membership : to-witness cIdx ∈ indices datas)
  108.       → (membership' : to-witness (subst Is-just cIdx≡ cIdx) ∈ indices datas')
  109.       → (lookupById membership ≡ lookupById membership')
  110.       → (sizeRange : size ≤ (proj₁ $ proj₂ $ lookupById membership))
  111.       → Set
  112.   inv someStates idx size cIdx≡ cIdx membership membership' lookupData≡lookupData' sizeRange =
  113.     (i : ℕ) → i < idx → (ip : i < size)
  114.                          → (p' : isThing $ Vec.lookup (subst (Vec SomeData)
  115.                                                                   (sym $ sizeEqualIfDataEqual lookupData≡lookupData')
  116.                                                                   (proj₂ $ proj₂ $ lookupById $ membership'))
  117.                                                            (fromℕ≤ $ ≤-trans ip sizeRange))
  118.                          → T (Vec.lookup someStates
  119.                                          (getFin[isThing] (Vec.lookup (subst (Vec SomeData)
  120.                                                                              (sym $ sizeEqualIfDataEqual lookupData≡lookupData')
  121.                                                                              (proj₂ $ proj₂ $ lookupById $ membership'))
  122.                                                                       (fromℕ≤ $ ≤-trans ip sizeRange))
  123.                                                           p'))
  124.  
  125.   om5-lemma11 : {mIdx mIdx' : Maybe SomeFin}
  126.               → {datas datas' : ISDList}
  127.               → {size : ℕ}
  128.               → {someStates : Vec Bool someMax₁}
  129.               → (cIdx≡ : mIdx ≡ mIdx')
  130.               → datas ≡ datas'
  131.               → Unique (indices datas)
  132.               → (cIdx : Is-just mIdx)
  133.               → (membership : to-witness cIdx ∈ indices datas)
  134.               → (membership' : to-witness (subst Is-just cIdx≡ cIdx) ∈ indices datas')
  135.               → (sizeRange : size ≤ (proj₁ $ proj₂ $ lookupById membership))
  136.               → (sizeRange' : size ≤ (proj₁ $ proj₂ $ lookupById membership'))
  137.               → (lookupData≡lookupData' : lookupById membership ≡ lookupById membership')
  138.               → {idx : ℕ}
  139.               -- → inv someStates idx size cIdx≡ cIdx membership membership' lookupData≡lookupData' sizeRange
  140.               → (i : ℕ)
  141.               → (i<idx' : i < suc idx)
  142.               → (i≢idx : i ≢ idx)
  143.               → (i<sz : i < size)
  144.               -- → (p¬nil : isThing (Vec.lookup (proj₂ $ proj₂ $ lookupById $ membership')
  145.               --                               (fromℕ≤ $ ≤-trans i<sz sizeRange')))
  146.               → T $ Vec.lookup someStates {!!} {- (getFin[isThing] (Vec.lookup (proj₂ $ proj₂ $ lookupById $ membership')
  147.                                                                        (fromℕ≤ $ ≤-trans i<sz sizeRange'))
  148.                                                            p¬nil) -}
  149.   om5-lemma11 refl refl uniqueP cIdx membership membership' sizeRange sizeRange' lookupData≡lookupData' {- invariant -} i (s≤s i<idx') i≢idx i<sz -- p¬nil
  150.     with {!!}
  151.   ... | x = {!!}
  152.   -- rewrite sym $ idsUnique⇒membershipUnique membership membership' uniqueP
  153.       -- | sym $ sizesEqual⇒ProofsEqual sizeRange sizeRange'
  154.        -- | lookupData≡lookupData'
  155. --     = {!!} -- inv i (≤∧≢⇒< i<idx' i≢idx) i<sz p¬nil
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top