• API
• FAQ
• Tools
• Archive
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.

Top