DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Lock down more equivalence relation proofs

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-11 15:46:18 +02:00
parent c1c34c69a5
commit d59ae90cef
1 changed files with 54 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
Lattice/Builder.agda
View File

@ -287,17 +287,49 @@ eqL (plt ∷ plts) (inj₂ v₁ ) (inj₂ v₂) = eqL plts v₁ v₂
eqL (plt ∷ plts) (inj₁ _) (inj₂ _) = Empty _
eqL (plt ∷ plts) (inj₂ _) (inj₁ _) = Empty _
eqL-trans : ∀ {a} (L : List (PartialLatticeType a)) {lv₁ lv₂ lv₃ : ListValue L} → eqL L lv₁ lv₂ → eqL L lv₂ lv₃ → eqL L lv₁ lv₃
eqL-trans [] {()}
eqL-trans (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} {inj₁ v₃} v₁≈v₂ v₂≈v₃ = PartialLatticeType.≈-trans plt v₁≈v₂ v₂≈v₃
eqL-trans (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} {inj₂ lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqL-trans plts lv₁≈lv₂ lv₂≈lv₃
eqL-sym : ∀ {a} (L : List (PartialLatticeType a)) {lv₁ lv₂ : ListValue L} → eqL L lv₁ lv₂ → eqL L lv₂ lv₁
eqL-sym [] {()}
eqL-sym (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} v₁≈v₂ = PartialLatticeType.≈-sym plt v₁≈v₂
eqL-sym (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} lv₁≈lv₂ = eqL-sym plts lv₁≈lv₂
eqL-refl : ∀ {a} (L : List (PartialLatticeType a)) (lv : ListValue L) → eqL L lv lv
eqL-refl [] ()
eqL-refl (plt ∷ plts) (inj₁ v) = IsEquivalence.≈-refl (PartialLatticeType.≈-equiv plt)
eqL-refl (plt ∷ plts) (inj₂ v) = eqL-refl plts v
instance
eqL-Equivalence : ∀ {a} {L : List (PartialLatticeType a)} → IsEquivalence (ListValue L) (eqL L)
eqL-Equivalence {L = L} = record
{ ≈-trans = eqL-trans L
; ≈-sym = eqL-sym L
; ≈-refl = λ {lv} → eqL-refl L lv
}
eqLv : ∀ {a} (L : Layer a) → LayerValue L → LayerValue L → Set a
eqLv L = eqL (toList L)
eqLv-trans : ∀ {a} (L : Layer a) → {lv₁ lv₂ lv₃ : LayerValue L} → eqLv L lv₁ lv₂ → eqLv L lv₂ lv₃ → eqLv L lv₁ lv₃
eqLv-trans L {lv₁} {lv₂} {lv₃} = eqL-trans (toList L) {lv₁} {lv₂} {lv₃}
eqLv-sym : ∀ {a} (L : Layer a) → {lv₁ lv₂ : LayerValue L} → eqLv L lv₁ lv₂ → eqLv L lv₂ lv₁
eqLv-sym L {lv₁} {lv₂} = eqL-sym (toList L) {lv₁} {lv₂}
eqLv-refl : ∀ {a} (L : Layer a) → (lv : LayerValue L) → eqLv L lv lv
eqLv-refl L = eqL-refl (toList L)
instance
eqLv-Equivalence : ∀ {a} {L : Layer a} → IsEquivalence (LayerValue L) (eqLv L)
eqLv-Equivalence {L = L} = record
{ ≈-trans = λ {lv₁} {lv₂} {lv₃} → eqLv-trans L {lv₁} {lv₂} {lv₃}
; ≈-sym = λ {lv₁} {lv₂} → eqLv-sym L {lv₁} {lv₂}
; ≈-refl = λ {lv} → eqLv-refl L lv
}
eqPath' : ∀ {a} (Ls : Layers a) → Path' Ls → Path' Ls → Set a
eqPath' (single l) lv₁ lv₂ = eqLv l lv₁ lv₂
eqPath' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = eqLv l lv₁ lv₂
@ -309,6 +341,20 @@ eqPath' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = eqPath' ls p₁ p
eqPath' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = Empty _
eqPath' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = Empty _
eqPath'-trans : ∀ {a} (Ls : Layers a) → {p₁ p₂ p₃ : Path' Ls} → eqPath' Ls p₁ p₂ → eqPath' Ls p₂ p₃ → eqPath' Ls p₁ p₃
eqPath'-trans (single l) {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqLv-trans l {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃
eqPath'-trans (add-via-least l ls) {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqLv-trans l {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃
eqPath'-trans (add-via-least l ls) {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} p₁≈p₂ p₂≈p₃ = eqPath'-trans ls p₁≈p₂ p₂≈p₃
eqPath'-trans (add-via-greatest l ls) {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqLv-trans l {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃
eqPath'-trans (add-via-greatest l ls) {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} p₁≈p₂ p₂≈p₃ = eqPath'-trans ls p₁≈p₂ p₂≈p₃
eqPath'-sym : ∀ {a} (Ls : Layers a) → {p₁ p₂ : Path' Ls} → eqPath' Ls p₁ p₂ → eqPath' Ls p₂ p₁
eqPath'-sym (single l) {lv₁} {lv₂} lv₁≈lv₂ = eqLv-sym l {lv₁} {lv₂} lv₁≈lv₂
eqPath'-sym (add-via-least l ls) {inj₁ lv₁} {inj₁ lv₂}lv₁≈lv₂ = eqLv-sym l {lv₁} {lv₂} lv₁≈lv₂
eqPath'-sym (add-via-least l ls) {inj₂ p₁} {inj₂ p₂} p₁≈p₂ = eqPath'-sym ls p₁≈p₂
eqPath'-sym (add-via-greatest l ls) {inj₁ lv₁} {inj₁ lv₂}lv₁≈lv₂ = eqLv-sym l {lv₁} {lv₂} lv₁≈lv₂
eqPath'-sym (add-via-greatest l ls) {inj₂ p₁} {inj₂ p₂} p₁≈p₂ = eqPath'-sym ls p₁≈p₂
eqPath'-refl : ∀ {a} (Ls : Layers a) → (p : Path' Ls) → eqPath' Ls p p
eqPath'-refl (single l) lv = eqLv-refl l lv
eqPath'-refl (add-via-least l ls) (inj₁ lv) = eqLv-refl l lv
@ -316,6 +362,14 @@ eqPath'-refl (add-via-least l ls) (inj₂ p) = eqPath'-refl ls p
eqPath'-refl (add-via-greatest l ls) (inj₁ lv) = eqLv-refl l lv
eqPath'-refl (add-via-greatest l ls) (inj₂ p) = eqPath'-refl ls p
instance
eqPath'-Equivalence : ∀ {a} {Ls : Layers a} → IsEquivalence (Path' Ls) (eqPath' Ls)
eqPath'-Equivalence {Ls = Ls} = record
{ ≈-trans = eqPath'-trans Ls
; ≈-sym = eqPath'-sym Ls
; ≈-refl = λ {x} → eqPath'-refl Ls x
}
-- Now that we can compare paths for "equality", we can state and
-- prove theorems such as commutativity and idempotence.