michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

asdf

Browse source
This commit is contained in:
Michael Zhang 2024-12-22 19:41:14 -06:00
parent 9cef0fa691
commit c28002e625
6 changed files with 621 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
src/AOP/Consistent.agda Normal file
View file

@ -0,0 +1,66 @@
module Consistent where
open import Relation.Binary.PropositionalEquality
infixr 10 _⇒_
-- Propositional formulas
data Form : Set where
𝕡 𝕢 : Form
true : Form
false : Form
_⇒_ : Form → Form → Form
-- Unit type (from agda-stdlib)
data ⊤ : Set where tt : ⊤
-- Empty type (from agda-stdlib)
data ⊥ : Set where
-- Negation type (from agda-stdlib)
¬_ : Set → Set
¬ A = A → ⊥
-- Validity of a formula
-- i.e. `Valid A` means `A` is always true
Valid : Form → Set
Valid 𝕡 = ⊥
Valid 𝕢 = ⊥
Valid true = ⊤
Valid false = ⊥
Valid (A ⇒ B) = Valid A → Valid B
-- Example: formula `𝕡 ⇒ 𝕡` is valid
id : Valid (𝕡 ⇒ 𝕡)
id = λ z → z
-- Observe: formula `false` is not valid
false-not-valid : ¬ (Valid false)
false-not-valid ()
-- Provability of a formula
-- i.e. `Proof A` means formula `A` is derivable
data Proof : Form → Set where
T : Proof true
K : {A B : Form} → Proof (A ⇒ B ⇒ A)
S : {A B C : Form} → Proof ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C))
MP : {A B : Form} → Proof (A ⇒ B) → Proof A → Proof B
-- Example: formula `𝕡 ⇒ 𝕡` is provable
id' : Proof (𝕡 ⇒ 𝕡)
id' = MP (MP S K) (K {A = 𝕡} {B = 𝕢})
p→v : (f : Form) → Proof f → Valid f
p→v 𝕡 (MP {A} f x) with l ← p→v (A ⇒ 𝕡) f = l (p→v A x)
p→v 𝕢 (MP {A} f x) with l ← p→v (A ⇒ 𝕢) f = l (p→v A x)
p→v true p = tt
p→v false (MP {A} f x) with l ← p→v (A ⇒ false) f = l (p→v A x)
p→v (true ⇒ b) K tt vb = tt
p→v (true ⇒ b) (MP {A} f x) tt with l ← p→v (A ⇒ true ⇒ b) f = l (p→v A x) tt
p→v ((a ⇒ a') ⇒ b) K va vb va' = va va'
p→v ((a ⇒ a') ⇒ b) S va vf va' = va va' (vf va')
p→v ((a ⇒ a') ⇒ b) (MP {A} p q) va with l ← p→v (A ⇒ (a ⇒ a') ⇒ b) p = l (p→v A q) va
-- Show: `false` is not provable
consistent : ¬ (Proof false)
consistent x = p→v false x

60
src/AOP/NatUIP.agda Normal file
View file

@ -0,0 +1,60 @@
{-# OPTIONS --safe --without-K #-}
data Nat : Set where
zero : Nat
suc : Nat → Nat
data _≡_ {A : Set} : A → A → Set where
refl : ∀ {x} → x ≡ x
sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
cong : ∀ {A B x y} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl
data _≡Nat_ : Nat → Nat → Set where
zero : zero ≡Nat zero
suc : ∀ {x y} → x ≡Nat y → suc x ≡Nat suc y
≡Nat-refl : ∀ {x} → x ≡Nat x
≡Nat-refl {zero} = zero
≡Nat-refl {suc x} = suc ≡Nat-refl
≡Nat-prop : ∀ {x y} (x≡y₁ x≡y₂ : x ≡Nat y) → x≡y₁ ≡ x≡y₂
≡Nat-prop zero zero = refl
≡Nat-prop (suc x≡y₁) (suc x≡y₂) = cong suc (≡Nat-prop x≡y₁ x≡y₂)
≡Nat⇒≡ : ∀ {x y} → x ≡Nat y → x ≡ y
≡Nat⇒≡ zero = refl
≡Nat⇒≡ (suc x≡y) = cong suc (≡Nat⇒≡ x≡y)
≡⇒≡Nat : ∀ {x y} → x ≡ y → x ≡Nat y
≡⇒≡Nat {zero} {zero} x≡y = zero
≡⇒≡Nat {suc x} {suc y} refl = suc (≡⇒≡Nat refl)
suc-inj : ∀ {x y : Nat} → suc x ≡ suc y → x ≡ y
suc-inj {x} {y} refl = refl
suc-inv : ∀ {x y : Nat} → (p : suc x ≡ suc y) → p ≡ cong suc (suc-inj p)
suc-inv {x} {y} refl = refl
Nat-loop-UIP : ∀ {x : Nat} (p : x ≡ x) → ≡⇒≡Nat p ≡ ≡Nat-refl → p ≡ refl
Nat-loop-UIP {zero} refl q = refl
Nat-loop-UIP {suc x} p q =
let IH = Nat-loop-UIP {x = x} (suc-inj p) (≡Nat-prop (≡⇒≡Nat (suc-inj p)) ≡Nat-refl) in
let z = cong (λ (p : x ≡ x) → cong Nat.suc p) IH in
trans (suc-inv p) z
Nat-UIP : ∀ {x y : Nat} (x≡y₁ x≡y₂ : x ≡ y) → x≡y₁ ≡ x≡y₂
Nat-UIP {zero} {zero} refl refl = refl
Nat-UIP {suc x} {suc y} refl q = sym (Nat-loop-UIP q (≡Nat-prop (≡⇒≡Nat q) ≡Nat-refl))
transport : {A : Set} (P : A → Set) {x y : A} (p : x ≡ y) (px : P x) → P y
transport P refl px = px
K : ∀ {x : Nat} {P : x ≡ x → Set} → P (refl {x = x}) → (h : x ≡ x) → P h
K {x} {P} prefl x≡x = transport (λ x → P x) (Nat-UIP refl x≡x) prefl

83
src/AOP/Prefixes.agda Normal file
View file

@ -0,0 +1,83 @@
open import Data.Product
open import Data.List
open import Data.List.Properties
open import Data.Nat
open import Data.Empty
open import Relation.Binary.PropositionalEquality hiding ([_])
module Prefixes(Σ : Set) where
data Trace : Set where
Finite : List Σ → Trace
Infinite : (ℕ → Σ) → Trace
postulate ext : {A B : Set}{f g : A → B} → (∀ X → f X ≡ g X) → f ≡ g
fininfin : List Σ → (ℕ → Σ) → ℕ → Σ
fininfin [] f n = f n
fininfin (x ∷ l) f zero = x
fininfin (x ∷ l) f (suc n) = fininfin l f n
_append_ : Trace → Trace → Trace
Finite x append Finite x₁ = Finite (x ++ x₁)
Finite x append Infinite x₁ = Infinite (fininfin x x₁)
Infinite x append u = Infinite x
_isPrefix_ : Trace → Trace → Set
_isPrefix_ t u = ∃[ t′ ] u ≡ (t append t′)
-- lemma: fininfin-assoc
fininfin-assoc-n : ∀ {x y z} (n : ℕ) → fininfin (x ++ y) z n ≡ fininfin x (fininfin y z) n
fininfin-assoc-n {[]} {y} {z} n = refl
fininfin-assoc-n {x ∷ xs} {y} {z} zero = refl
fininfin-assoc-n {x ∷ xs} {[]} {z} (suc n) = cong (λ p → fininfin p z n) (++-identityʳ xs)
fininfin-assoc-n {x ∷ xs} {y ∷ ys} {z} (suc n) = fininfin-assoc-n {xs} {y ∷ ys} {z} n
fininfin-assoc : ∀ {x y z} → fininfin (x ++ y) z ≡ fininfin x (fininfin y z)
fininfin-assoc {x} {y} {z} = ext (fininfin-assoc-n {x} {y} {z})
-- lemma: append-assoc
append-assoc : ∀ {a b c} → (a append b) append c ≡ a append (b append c)
append-assoc {Finite x} {Finite y} {Finite z} = cong Finite (++-assoc x y z)
append-assoc {Finite x} {Finite y} {Infinite z} = cong Infinite (fininfin-assoc {x} {y} {z})
append-assoc {Finite x} {Infinite y} {c} = refl
append-assoc {Infinite x} {b} {c} = refl
Finite-inj : {a b : List Σ} → Finite a ≡ Finite b → a ≡ b
Finite-inj {[]} {[]} p = refl
Finite-inj {x ∷ xs} {y ∷ ys} refl = refl
-- lemma
lemma1 : ∀ {a r} → Finite a append r ≡ Finite a → r ≡ Finite []
lemma1 {[]} {Finite x} p = p
lemma1 {x ∷ xs} {Finite r} p = cong Finite (++-identityʳ-unique (x ∷ xs) (Finite-inj (sym p)))
lemma2 : ∀ {a b} → a append b ≡ Finite [] → a ≡ Finite [] × b ≡ Finite []
lemma2 {Finite a} {Finite b} p = (cong Finite (++-conicalˡ a b (Finite-inj p))) , cong Finite (++-conicalʳ a b (Finite-inj p))
-- doesn't matter what this is
dummy : Trace
dummy = Finite []
prefl : ∀{t} → t isPrefix t
prefl {Finite x} = Finite [] , cong Finite (sym (++-identityʳ x))
prefl {Infinite x} = dummy , refl
ptrans : ∀{t u v} → t isPrefix u → u isPrefix v → t isPrefix v
ptrans {Finite t} {u} {v} (u-t , snd) (v-u , snd₁) =
let z1 = trans snd₁ (trans (cong (λ p → p append v-u) snd) append-assoc) in
(u-t append v-u) , z1
ptrans {Infinite t} {u} {v} (fst , snd) (fst₁ , snd₁) =
let p = subst (λ x → v ≡ (x append fst₁)) snd snd₁ in
dummy , p
pantisym : ∀{t u} → t isPrefix u → u isPrefix t → t ≡ u
pantisym {Finite t} {Finite u} (u-t , p1) (t-u , p2) =
let z = subst (λ x → Finite u ≡ (x append u-t)) p2 p1 in
let z1 = trans z append-assoc in
let z2 = lemma1 (sym z1) in
let z3 = lemma2 z2 in
let z4 = subst (λ z → Finite t ≡ Finite u append z) (z3 .proj₁) p2 in
let z5 = trans z4 (cong Finite (++-identityʳ u)) in
z5
pantisym {t} {Infinite u} (u-t , p1) (t-u , p2) = p2

141
src/AOP/Thin.agda Normal file
View file

@ -0,0 +1,141 @@
open import Level using (Level)
open import Data.List.Base using (List; []; _∷_; _++_)
open import Data.Nat.Base using ()
variable
a : Level
A : Set a
x y z : A
xs ys zs as bs cs : List A
-- A thinning, also known as an order preserving embedding
-- is a first order data structure explaining how a small
-- list embeds into a bigger one.
data Thin {A : Set a} : (xs ys : List A) → Set a where
-- The empty list trivially embeds into itself
done : Thin [] []
-- The remaining constructors are named based on what
-- we do with the head of the bigger list.
keep : (x : A) → Thin xs ys → Thin (x ∷ xs) (x ∷ ys)
drop : (y : A) → Thin xs ys → Thin xs (y ∷ ys)
-- We can for instance prove that we can embed the list
-- [1,4] into the list [1,3,4] in an order preserving
-- manner by giving the following thinning.
thin₁ : Thin (1 ∷ 4 ∷ [])
(1 ∷ 3 ∷ 4 ∷ [])
thin₁ = keep 1 (drop 3 (keep 4 done))
-- And we can further embed [1,3,4] into [0,1,2,3,4]
-- using the following thinning
thin₂ : Thin ( 1 ∷ 3 ∷ 4 ∷ [])
(0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
thin₂ = drop 0 (keep 1 (drop 2 (keep 3 (keep 4 done))))
------------------------------------------------------------------------
-- Vertical composition
-- By composing two thinnings that meet in the middle
-- we ought to be able to obtain a third thinning spanning
-- the gap between the smallest list and the largest one
_seq_ : Thin xs ys →
Thin ys zs →
Thin xs zs
-- e.g. reusing our prior example, we can prove that
-- [1,4] embeds into [0,1,2,3,4] by "vertically"
-- composing thin₁ and thin₂ like so:
thin₃ : Thin ( 1 ∷ 4 ∷ [])
-- ( 1 ∷ 3 ∷ 4 ∷ [])
(0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
thin₃ = thin₁ seq thin₂
-- Implement _seq_
done seq x = x
keep .x ph2 seq keep x th2 = keep x (ph2 seq th2)
drop .x ph2 seq keep x th2 = drop x (ph2 seq th2)
keep x ph2 seq drop y th2 = drop y (keep x ph2 seq th2)
drop y ph2 seq drop z th2 = drop z ((drop y ph2) seq th2)
------------------------------------------------------------------------
-- Horizontal composition
-- Similarly if we have two separate thinnings respectively
-- between xs and ys on one hand, and as and bs on the other
-- then we can paste them together "horizontally" and obtain
-- a thinning between (xs ++ as) and (ys ++ bs)
_par_ : Thin xs ys →
Thin as bs →
Thin (xs ++ as) (ys ++ bs)
-- e.g. reusing our prior example, we can prove that
-- [1,4,1,3,4] embeds into [1,3,4,0,1,2,3,4] by "horizontally"
-- composing thin₁ with thin₂*
thin₄ : Thin (1 ∷ 4 ∷ 1 ∷ 3 ∷ 4 ∷ [])
(1 ∷ 3 ∷ 4 ∷ 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
thin₄ = thin₁ par thin₂
-- Implement _par_
open import Relation.Binary.PropositionalEquality using (sym; subst)
open import Data.List.Properties
++-identity-Thin : ∀ {x y : List A} → Thin x y → Thin (x ++ []) (y ++ [])
++-identity-Thin {x = x} {y = y} ph =
let ph1 = subst (λ xs → Thin xs y) (sym (++-identityʳ x)) ph in
subst (λ ys → Thin (x ++ []) ys) (sym (++-identityʳ y)) ph1
done par th = th
_par_ {xs = x ∷ xs₁} {ys = y ∷ ys₁} (keep x ph) done = keep x (++-identity-Thin ph)
keep x ph par keep x₁ th = keep x (ph par keep x₁ th)
keep x ph par drop y th = keep x (ph par (drop y th))
_par_ {xs = xs} {ys = y ∷ ys₁} (drop y ph) done = drop y (++-identity-Thin ph)
drop y ph par keep x th = drop y (ph par (keep x th))
drop y ph par drop y₁ th = drop y (ph par drop y₁ th)
------------------------------------------------------------------------
-- Distributivity law
-- Using our geometric intuition, a 2*2 tiling could be seen
-- as rows of columns or columns of rows. Prove that we indeed
-- get the same result no matter what:
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans)
import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning
-- Implement cast
infixl 5 _∙_
_∙_ = trans
lemma1 : ∀ (a : Thin xs ys) → a par done ≡ ++-identity-Thin a
lemma1 done = refl
lemma1 {xs = x ∷ xs₁} {ys = x ∷ ys₁} (keep x a) =
let IH = cong (keep x) (sym (lemma1 a)) in
IH ∙ {! refl !}
lemma1 (drop y a) = {! refl !}
lemma2 : ∀ (a : Thin xs ys) (b : Thin ys zs) → (a par done) seq (b par done) ≡ ++-identity-Thin (a seq b)
lemma2 done b = lemma1 b
lemma2 (keep x a) b = {! !}
lemma2 (drop y a) b = {! !}
cast :
(phᵗ : Thin xs ys) (phᵇ : Thin ys zs)
(thᵗ : Thin as bs) (thᵇ : Thin bs cs) →
(phᵗ seq phᵇ) par (thᵗ seq thᵇ) ≡ (phᵗ par thᵗ) seq (phᵇ par thᵇ)
cast a b done done = lemma1 (a seq b) ∙ {! !} ∙ {! !}
cast a b c (keep x d) = {! !}
cast a b c (drop y d) = {! !}

223
src/Misc/CRDT.agda Normal file
View file

@ -0,0 +1,223 @@
{-# OPTIONS --cubical #-}
module Misc.CRDT where
open import Agda.Primitive
open import Data.List using (List; _∷_; [])
open import Data.Nat using (ℕ)
open import Data.Product
open import Data.Bool
open import Data.Empty
open import Function
open import Function.Properties.Equivalence using () renaming (sym to symEquiv)
open import Relation.Binary.Bundles
open import Relation.Binary.Definitions
open import Relation.Binary.Consequences
open import Relation.Binary.Structures
import Relation.Binary.PropositionalEquality as Eq
open import Relation.Binary.PropositionalEquality hiding (isEquivalence)
open Eq.≡-Reasoning
open import Relation.Nullary.Decidable
open import Relation.Nullary.Reflects
private
variable
ℓ ℓ' : Level
module _ {ℓ ℓ' ℓ''} (TimeOrder : StrictTotalOrder ℓ ℓ' ℓ'') where
Time = TimeOrder .StrictTotalOrder.Carrier
record isCRDT {cℓ cℓ' : Level} (A : Set cℓ) : Set (lsuc (cℓ ⊔ cℓ' ⊔ ℓ ⊔ ℓ' ⊔ ℓ'')) where
field
op : Set cℓ'
noOp : op
apply2 : (o1 o2 : op) (t1 t2 : Time) → A → A
comm : (a : A) → (o1 o2 : op) (t1 t2 : Time) → apply2 o1 o2 t1 t2 a ≡ apply2 o2 o1 t2 t1 a
module _ where
open import Data.Nat
open isCRDT
Counter = ℕ
private
data Op : Set where
nop : Op
inc : Op
apply2' : Op → Op → Time → Time → Counter → Counter
apply2' nop nop t1 t2 c = c
apply2' nop inc t1 t2 c = suc c
apply2' inc nop t1 t2 c = suc c
apply2' inc inc t1 t2 c = suc (suc c)
comm' : (a : Counter) (o1 o2 : Op) (t1 t2 : Time) → apply2' o1 o2 t1 t2 a ≡ apply2' o2 o1 t2 t1 a
comm' c nop nop t1 t2 = refl
comm' c nop inc t1 t2 = refl
comm' c inc nop t1 t2 = refl
comm' c inc inc t1 t2 = refl
CounterIsCRDT : isCRDT Counter
CounterIsCRDT .op = Op
CounterIsCRDT .noOp = nop
CounterIsCRDT .apply2 = apply2'
CounterIsCRDT .comm = comm'
module _ (K V : Set) (DecK : DecidableEquality K) where
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Product
open StrictTotalOrder (TimeOrder) renaming (compare to tcompare; _<_ to _t<_; _>_ to _t>_)
open isCRDT
Arb = (K × V) × (K × V)
postulate
JSMap : Set → Set → Set
rawGet : JSMap K V → K → V
JSMapExt : (m1 m2 : JSMap K V) → ((k : K) → rawGet m1 k ≡ rawGet m2 k) → m1 ≡ m2
rawInsert : (k : K) (v : V) (orig : JSMap K V) → Σ (JSMap K V) λ modif → rawGet modif k ≡ v
-- funExt : {A B : Set} (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g
-- TODO: What is a clean way to get around this?
arb : (k1 k2 : K) (v1 v2 : V) → Arb
arb-comm : (k1 k2 : K) (v1 v2 : V) → arb k1 k2 v1 v2 ≡ arb k2 k1 v2 v1
private
data Op : Set where
nop : Op
insert : K → V → Op
apply : Op → JSMap K V → JSMap K V
apply nop m = m
apply (insert k v) m = rawInsert k v m .proj₁
TCompare : Time → Time → Set (ℓ' ⊔ ℓ'')
TCompare t1 t2 = Tri (t1 t< t2) (t1 ≈ t2) (flip _t<_ t1 t2)
doubleInsertSeq : (k1 k2 : K) (v1 v2 : V) → JSMap K V → JSMap K V
doubleInsertSeq k1 k2 v1 v2 m = rawInsert k2 v2 (rawInsert k1 v1 m .proj₁) .proj₁
k1Of : Arb → K
k1Of arb = arb .proj₁ .proj₁
k2Of : Arb → K
k2Of arb = arb .proj₂ .proj₁
doIt : (arb' : Arb) (d : Dec (k1Of arb' ≡ k2Of arb')) → JSMap K V → JSMap K V
-- just take the first one, since it doesn't matter
doIt arb' (true because _) m = rawInsert k1' v1' m .proj₁ where
k1' = arb' .proj₁ .proj₁
v1' = arb' .proj₁ .proj₂
k2' = arb' .proj₂ .proj₁
v2' = arb' .proj₂ .proj₂
-- insert both in order, since it doesn't matter
doIt arb' (false because _) m = doubleInsertSeq k1' k2' v1' v2' m where
k1' = arb' .proj₁ .proj₁
v1' = arb' .proj₁ .proj₂
k2' = arb' .proj₂ .proj₁
v2' = arb' .proj₂ .proj₂
doubleInsert : (k1 k2 : K) (v1 v2 : V) {t1 t2 : Time} (t1<t2 : TCompare t1 t2) → JSMap K V → JSMap K V
doubleInsert k1 k2 v1 v2 (tri< a ¬b ¬c) m = doubleInsertSeq k1 k2 v1 v2 m
doubleInsert k1 k2 v1 v2 {t1} {t2} (tri≈ ¬a b ¬c) m =
let arb' = arb k1 k2 v1 v2 in
doIt arb' (DecK (k1Of arb') (k2Of arb')) m
doubleInsert k1 k2 v1 v2 (tri> ¬a ¬b c) m = doubleInsertSeq k2 k1 v2 v1 m
apply2' : Op → Op → Time → Time → JSMap K V → JSMap K V
apply2' nop nop _ _ m = m
apply2' o1 nop _ _ m = apply o1 m
apply2' nop o2 _ _ m = apply o2 m
apply2' (insert k1 v1) (insert k2 v2) t1 t2 m = doubleInsert k1 k2 v1 v2 (tcompare t1 t2) m
comm' : (a : JSMap K V) (o1 o2 : Op) (t1 t2 : Time) → apply2' o1 o2 t1 t2 a ≡ apply2' o2 o1 t2 t1 a
comm' a nop nop t1 t2 = refl
comm' a (insert _ _) nop t1 t2 = refl
comm' a nop (insert _ _) t1 t2 = refl
comm' a (insert k1 v1) (insert k2 v2) t1 t2 = doubleInsertLemma (tcompare t1 t2) (tcompare t2 t1) where
a12 = doubleInsertSeq k1 k2 v1 v2 a
a21 = doubleInsertSeq k2 k1 v2 v1 a
x = _≈_
y = subst
doubleInsertLemma : (tc1 : TCompare t1 t2) (tc2 : TCompare t2 t1) → doubleInsert k1 k2 v1 v2 tc1 a ≡ doubleInsert k2 k1 v2 v1 tc2 a
doubleInsertLemma (tri< a ¬b ¬c) (tri< a₁ ¬b₁ ¬c₁) = ⊥-elim (asym a a₁)
doubleInsertLemma (tri< a ¬b ¬c) (tri≈ ¬a b ¬c₁) = ⊥-elim (irrefl (IsEquivalence.sym isEquivalence b) a)
doubleInsertLemma (tri< a ¬b ¬c) (tri> ¬a ¬b₁ c) = refl
doubleInsertLemma (tri≈ ¬a b ¬c) (tri< a ¬b ¬c₁) = ⊥-elim (irrefl (IsEquivalence.sym isEquivalence b) a)
doubleInsertLemma tc1 @ (tri≈ ¬a b ¬c) tc2 @ (tri≈ ¬a₁ b₁ ¬c₁) = doItLemma where
arb₁ = arb k1 k2 v1 v2
arb₂ = arb k2 k1 v2 v1
doItLemma : doIt arb₁ (DecK (k1Of arb₁) (k2Of arb₁)) a ≡ doIt arb₂ (DecK (k1Of arb₂) (k2Of arb₂)) a
doItLemma = cong (λ arb' → doIt arb' (DecK (k1Of arb') (k2Of arb')) a) (arb-comm k1 k2 v1 v2)
-- doItLemma (no ¬a) (yes a) = ⊥-elim (¬a (sym a))
-- doItLemma (yes a) (no ¬a) = ⊥-elim (¬a (sym a))
-- doItLemma (yes t) (yes t₁) = cong₂ (λ arb' q → doIt arb' q a) (arb-comm k1 k2 v1 v2) {! !} where
-- doItLemma (no ¬a) (no ¬a₁) = {! !}
-- -- doItLemma : Dec (k1 ≡ k2) → doubleInsert k1 k2 v1 v2 tc1 a ≡ doubleInsert k2 k1 v2 v1 tc2 a
-- -- doItLemma (true because proof₁) = cong (λ arb' → {! !}) arb-same
-- -- doItLemma (false because proof₁) = {! refl !}
doubleInsertLemma (tri≈ ¬a b ¬c) (tri> ¬a₁ ¬b c) = ⊥-elim (irrefl b c)
doubleInsertLemma (tri> ¬a ¬b c) (tri< a ¬b₁ ¬c) = refl
doubleInsertLemma (tri> ¬a ¬b c) (tri≈ ¬a₁ b ¬c) = ⊥-elim (irrefl b c)
doubleInsertLemma (tri> ¬a ¬b c) (tri> ¬a₁ ¬b₁ c₁) = ⊥-elim (asym c c₁)
LWWMapIsCRDT : isCRDT (JSMap K V)
LWWMapIsCRDT .op = Op
LWWMapIsCRDT .noOp = nop
LWWMapIsCRDT .apply2 = apply2'
LWWMapIsCRDT .comm = comm'
------------------------------------------------------------------------
-- Old
-- Counter = ℕ
-- private
-- data Op : Set where inc : Op
-- CounterIsCRDT : isCRDT Counter
-- CounterIsCRDT .op = Op
-- CounterIsCRDT .apply inc t y = {! !}
-- CounterIsCRDT .comm a inc inc = {! !}
-- -- Last-write wins
-- module _ (K V : Set) where
-- open import Data.Unit
-- open import Data.Nat
-- open import Data.Product
-- open isCRDT
-- postulate
-- JSMap : Set → Set → Set
-- rawNew : ⊤ → JSMap K V
-- rawGet : JSMap K V → K → V
-- funExt : {A B : Set} (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g
-- JSMapExt : (m1 m2 : JSMap K V) → ((k : K) → rawGet m1 k ≡ rawGet m2 k) → m1 ≡ m2
-- rawInsert : (k : K) (v : V) (orig : JSMap K V) → Σ (JSMap K V) λ modif → rawGet modif k ≡ v
-- {-# COMPILE JS JSMap = Map #-}
-- {-# COMPILE JS rawNew = new Map() #-}
-- private
-- data Op : Set where
-- insert : K → V → Op
-- apply' : Op → Time → JSMap K V → JSMap K V
-- apply' (insert k v) _ map = rawInsert k v map .proj₁
-- comm' : (a : JSMap K V) (o1 o2 : Op) (t1 t2 : Time) → apply' o1 t1 (apply' o2 t2 a) ≡ apply' o2 t2 (apply' o1 t1 a)
-- comm' map (insert k1 v1) (insert k2 v2) t1 t2 =
-- let res1 = rawInsert k1 v1 map in
-- let res2 = rawInsert k2 v2 map in
-- let res12 = rawInsert k2 v2 (res1 .proj₁) in
-- let res21 = rawInsert k1 v1 (res2 .proj₁) in
-- JSMapExt (res21 .proj₁) (res12 .proj₁) λ k → {! !}
-- LWWMapIsCRDT : isCRDT (JSMap K V)
-- LWWMapIsCRDT .op = Op
-- LWWMapIsCRDT .apply = apply'
-- LWWMapIsCRDT .comm = comm'

82
src/ThesisWork/EMSpace.agda
View file

@ -38,7 +38,7 @@ module _ where
open import Cubical.Algebra.Group.Instances.Int
test : S¹ ≃ K[ ℤGroup ,1]
test = isoToEquiv (iso f g {! !} {! !}) where
test = isoToEquiv (iso {! !} {! !} {! !} {! !}) where
loop^_ : ℤ → S¹-base ≡ S¹-base
-- loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop
-- loop^ pos zero = refl
@ -53,21 +53,18 @@ module _ where
-- f S¹-base = base
-- f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i
f : S¹ → K[ ℤGroup ,1]
f S¹-base = base
f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i
-- f : S¹ → K[ ℤGroup ,1]
-- f S¹-base = base
-- f (S¹-loop i) = loop (subst Code1 {! !} {! !}) i
g : K[ ℤGroup ,1] → S¹
g base = S¹-base
g (loop x i) = {! !}
g (loop-1g i i₁) = {! !}
g (loop-∙ x y i i₁) = {! !}
g (squash x x₁ p q r s i i₁ i₂) = {! !}
-- g : K[ ℤGroup ,1] → S¹
-- g base = S¹-base
-- g (loop x i) = {! !}
-- g (loop-1g i i₁) = {! !}
-- g (loop-∙ x y i i₁) = {! !}
-- g (squash x y p q r s i j k) = {! !}
module _ (G : Group ℓ) where
open GroupStr (G .snd)
-------------------------------------------------------------------------------
-- Properties
@ -104,37 +101,54 @@ module _ (G : Group ℓ) where
gf : retract (λ y → y ⊙ x) (λ y → y ⊙ inv x)
gf a = sym (·Assoc a x (inv x)) ∙ cong (a ⊙_) (·InvR x) ∙ ·IdR a
f1≡id : f 1g ≡ idEquiv ⟨ G ⟩
f1≡id i = fnEq i , isEquivEq i where
fnEq : f 1g .fst ≡ idEquiv ⟨ G ⟩ .fst
fnEq i x = ·IdR x i
feq : (g : ⟨ G ⟩) → ⟨ G ⟩ ≡ ⟨ G ⟩
feq g = ua (f g)
isEquivEq : PathP (λ i → isEquiv (fnEq i)) (f 1g .snd) (idEquiv ⟨ G ⟩ .snd)
isEquivEq = toPathP (isPropIsEquiv (idfun ⟨ G ⟩) (subst isEquiv fnEq (f 1g .snd)) (idEquiv ⟨ G ⟩ .snd))
f1≡id : f 1g ≡ idEquiv ⟨ G ⟩
f1≡id = equivEq (funExt (λ x → ·IdR x))
feq1≡refl : feq 1g ≡ refl
feq1≡refl = cong ua f1≡id ∙ uaIdEquiv
flemma2 : (x y : ⟨ G ⟩) → f (x · y) ≡ compEquiv (f x) (f y)
flemma2 x y = equivEq (funExt (λ z → ·Assoc z x y))
S = Square
transpose : {A : Type ℓ} {a00 a01 a10 a11 : A}
{a0- : a00 ≡ a01} {a1- : a10 ≡ a11} {a-0 : a00 ≡ a10} {a-1 : a01 ≡ a11}
→ Square a0- a1- a-0 a-1 → Square a-0 a-1 a0- a1-
transpose s i j = s j i
Codes : K[G,1] → hSet ℓ
Codes = GT.rec isGroupoidHSet Codes' where
CodesFunc : ⟨ G ⟩ → ⟨ G ⟩ ≃ ⟨ G ⟩
CodesFunc g = {! !}
Codes base = ⟨ G ⟩ , is-set
Codes (loop x i) = (Codes-aux.feq x i) , z i where
z : PathP (λ i → isSet (Codes-aux.feq x i)) is-set is-set
z = toPathP (isPropIsSet (transport (λ i₁ → isSet (Codes-aux.feq x i₁)) is-set) is-set)
Codes (loop-1g i j) = {! !}
Codes (loop-∙ x y i j) = {! !} , {! !}
Codes (squash x y p q r s i j k) = CodesGpd (Codes x) (Codes y) (cong Codes p) (cong Codes q) (cong (cong Codes) r) (cong (cong Codes) s) i j k where
CodesGpd = isOfHLevelTypeOfHLevel 2
Codes' : K[ G ,1] → hSet ℓ
Codes' base = ⟨ G ⟩ , is-set
Codes' (loop x i) = ⟨ G ⟩ , is-set
Codes' (loop-1g i i₁) = {! !}
Codes' (loop-∙ x y i i₁) = {! !}
Codes' x = ?
-- For point-free transports
Codes2 : K[G,1] → Type ℓ
Codes2 x = Codes x .fst
module _ where
_ : (x y : ⟨ G ⟩) → subst {! λ x → Codes x .snd !} {! !} {! !} ≡ {! !}
fact : (x y : ⟨ G ⟩) → subst Codes2 (loop x) y ≡ y ⊙ x
fact x y = let z = sym (subst-filler {! !} {! !} {! !}) in {! !}
encode : (z : K[G,1]) → ∣ base ∣₃ ≡ z → ⟨ Codes z ⟩
encode z p = {! !}
encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩
encode z p = subst Codes2 p 1g
decode : ⟨ G ⟩ → base ≡ base
decode x = loop x
encode-decode : (z : ⟨ G ⟩) → encode base (decode z) ≡ z
encode-decode z = {! !}
encode-decode : (x : ⟨ G ⟩) → encode base (decode x) ≡ x
encode-decode x =
encode base (decode x) ≡⟨ refl ⟩
encode base (loop x) ≡⟨ refl ⟩
subst Codes2 (loop x) 1g ≡⟨ fact x 1g ⟩
1g ⊙ x ≡⟨ ·IdL x ⟩
x ∎
ΩKG1≃G' : GroupIso {! ΩK[G,1] !} G