Require bottom element to actually be bottom; finish proof

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Equivalence.agda

@@ -2,7 +2,7 @@ module Equivalence where
 
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.Definitions
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
 
 module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
     IsReflexive : Set a
@@ -19,3 +19,10 @@ module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
             ≈-refl : IsReflexive
             ≈-sym : IsSymmetric
             ≈-trans : IsTransitive
+
+isEquivalence-≡ : ∀ {a} {A : Set a} → IsEquivalence A _≡_
+isEquivalence-≡ = record
+    { ≈-refl = refl
+    ; ≈-sym = sym
+    ; ≈-trans = trans
+    }

Language/Graphs.agda

@@ -18,7 +18,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl;
 open import Relation.Nullary using (¬_)
 
 open import Lattice
-open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct; fins; fins-complete)
 
 record Graph : Set where
     constructor MkGraph
@@ -124,28 +124,6 @@ buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
 buildCfg (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
 buildCfg (while _ repeat s) = loop (buildCfg s)
 
-private
-    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
-    z≢sf f ()
-
-    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
-    z≢mapsfs [] = []
-    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    finValues 0 = ([] , Utils.empty)
-    finValues (suc n') =
-        let
-            (inds' , unids') = finValues n'
-        in
-            ( zero ∷ List.map suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
-    finValues-complete (suc n') zero = RelAny.here refl
-    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
-
 module _ (g : Graph) where
     open import Data.Product.Properties as ProdProp using ()
     private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g})
@@ -154,13 +132,13 @@ module _ (g : Graph) where
     open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_)
 
     indices : List (Graph.Index g)
-    indices = proj₁ (finValues (Graph.size g))
+    indices = proj₁ (fins (Graph.size g))
 
     indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
-    indices-complete = finValues-complete (Graph.size g)
+    indices-complete = fins-complete (Graph.size g)
 
     indices-Unique : Unique indices
-    indices-Unique = proj₂ (finValues (Graph.size g))
+    indices-Unique = proj₂ (fins (Graph.size g))
 
     predecessors : (Graph.Index g) → List (Graph.Index g)
     predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

Lattice.agda

@@ -96,6 +96,12 @@ record IsSemilattice {a} (A : Set a)
                     (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
                 ∎
 
+    -- need to show: a₁ ⊔ (a₁ ⊔ a₂) ≈ a₁ ⊔ a₂
+    -- (a₁ ⊔ a₁) ⊔ a₂ ≈ a₁ ⊔ (a₁ ⊔ a₂)
+
+    x≼x⊔y : ∀ (a₁ a₂ : A) → a₁ ≼ (a₁ ⊔ a₂)
+    x≼x⊔y a₁ a₂ = ≈-sym (≈-trans (≈-⊔-cong (≈-sym (⊔-idemp a₁)) (≈-refl {a₂})) (⊔-assoc a₁ a₁ a₂))
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -113,6 +119,18 @@ record IsSemilattice {a} (A : Set a)
             a₃
         ∎
 
+    ≼-antisym : ∀ {a₁ a₂ : A} → a₁ ≼ a₂ → a₂ ≼ a₁ → a₁ ≈ a₂
+    ≼-antisym {a₁} {a₂} a₁⊔a₂≈a₂ a₂⊔a₁≈a₁ =
+        begin
+            a₁
+        ∼⟨ ≈-sym a₂⊔a₁≈a₁ ⟩
+            a₂ ⊔ a₁
+        ∼⟨ ⊔-comm _ _ ⟩
+            a₁ ⊔ a₂
+        ∼⟨ a₁⊔a₂≈a₂ ⟩
+            a₂
+        ∎
+
     ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
     ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
         begin
@@ -237,16 +255,25 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         {{fixedHeight}} : FixedHeight h
 
+    private
+        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+
+    open MyChain.Height fixedHeight using (⊥; ⊤) public
+
+    Known-⊥ : Set a
+    Known-⊥ = ∀ (a : A) → ⊥ ≼ a
+
+    Known-⊤ : Set a
+    Known-⊤ = ∀ (a : A) → a ≼ ⊤
+
     -- If the equality is decidable, we can prove that the top and bottom
     -- elements of the chain are least and greatest elements of the lattice
     module _ {{≈-Decidable : IsDecidable _≈_}} where
         open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
 
-        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
-        open MyChain.Height fixedHeight using (⊥; ⊤) public
         open MyChain.Height fixedHeight using (bounded; longestChain)
 
-        ⊥≼ : ∀ (a : A) → ⊥ ≼ a
+        ⊥≼ : Known-⊥
         ⊥≼ a with ≈-dec a ⊥
         ...   | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a)
         ...   | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥)

Utils.agda

@@ -1,19 +1,32 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
-open import Data.Product as Prod using (_×_)
+open import Data.Product as Prod using (Σ; _×_; _,_; proj₁; proj₂)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat using (ℕ; suc)
+open import Data.Fin as Fin using (Fin; suc; zero)
+open import Data.Fin.Properties using (suc-injective)
 open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
-open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional using (_∈_; lose)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
-open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; all?; lookup)
+open import Data.List.Relation.Unary.All.Properties using (++⁻ˡ; ++⁻ʳ)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?) -- TODO: re-export these with nicer names from map
 open import Data.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
+open import Relation.Binary using (Antisymmetric) renaming (Decidable to Decidable²)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
-open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary using (¬_; yes; no; Dec)
+open import Relation.Nullary.Decidable using (¬?)
 open import Relation.Unary using (Decidable)
 
+All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
+All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
+All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+
+Decidable-¬ : ∀ {p c} {C : Set c} {P : C → Set p} → Decidable P → Decidable (λ x → ¬ P x)
+Decidable-¬ Decidable-P x = ¬? (Decidable-P x)
+
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
     push : ∀ {x : C} {xs : List C}
@@ -34,6 +47,24 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
         help {[]} _ = x'≢x ∷ []
         help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
 
+Unique-++⁻ˡ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique xs
+Unique-++⁻ˡ [] Unique-ys = empty
+Unique-++⁻ˡ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = push (++⁻ˡ xs {ys = ys} x≢xs++ys) (Unique-++⁻ˡ xs Unique-xs++ys)
+
+Unique-++⁻ʳ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique ys
+Unique-++⁻ʳ [] Unique-ys = Unique-ys
+Unique-++⁻ʳ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = Unique-++⁻ʳ xs Unique-xs++ys
+
+Unique-∈-++ˡ : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs → ¬ x ∈ ys
+Unique-∈-++ˡ [] _ ()
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push x≢xs++ys _) (here refl) = All¬-¬Any (++⁻ʳ xs x≢xs++ys)
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-∈-++ˡ xs Unique-xs++ys x̷∈xs
+
+Unique-narrow : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs →  Unique (x ∷ ys)
+Unique-narrow [] _ ()
+Unique-narrow {x = x} (x' ∷ xs) (push x≢xs++ys Unique-xs++ys) (here refl) = push (++⁻ʳ xs x≢xs++ys) (Unique-++⁻ʳ xs Unique-xs++ys)
+Unique-narrow {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-narrow xs Unique-xs++ys x̷∈xs
+
 All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
             Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
             All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
@@ -46,9 +77,8 @@ Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
 Unique-map {l = []} _ _ _ = empty
 Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
 
-All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
-All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
-All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+¬Any-map : ∀ {p₁ p₂ c} {C : Set c} {P₁ : C → Set p₁} {P₂ : C → Set p₂} {l : List C} → (∀ {x} → P₁ x → P₂ x) → ¬ Any P₂ l → ¬ Any P₁ l
+¬Any-map f ¬Any-P₂ Any-P₁ = ¬Any-P₂ (Any.map f Any-P₁)
 
 All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
@@ -106,3 +136,42 @@ _∧_ P Q a = P a × Q a
 
 it : ∀ {a} {A : Set a} {{_ : A}} → A
 it {{x}} = x
+
+z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (Fin.zero ≡ Fin.suc f)
+z≢sf f ()
+
+z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
+z≢mapsfs [] = []
+z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+fins : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+fins 0 = ([] , empty)
+fins (suc n') =
+    let
+        (inds' , unids') = fins n'
+    in
+        ( zero ∷ mapˡ suc inds'
+        , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+        )
+
+fins-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ (proj₁ (fins n))
+fins-complete (suc n') zero = here refl
+fins-complete (suc n') (suc f') = there (x∈xs⇒fx∈fxs suc (fins-complete n' f'))
+
+findUniversal : ∀ {p c} {C : Set c} {R : C → C → Set p} (l : List C) →  Decidable² R →
+                Dec (Any (λ x → All (R x) l) l)
+findUniversal l Rdec = any? (λ x → all? (Rdec x) l) l
+
+findUniversal-unique : ∀ {p c} {C : Set c} (R : C → C → Set p) (l : List C) →
+                       Antisymmetric _≡_ R →
+                       ∀ x₁ x₂ → x₁ ∈ l → x₂ ∈ l → All (R x₁) l → All (R x₂) l →
+                       x₁ ≡ x₂
+findUniversal-unique R l Rantisym x₁ x₂ x₁∈l x₂∈l Allx₁ Allx₂ = Rantisym (lookup Allx₁ x₂∈l) (lookup Allx₂ x₁∈l)
+
+x∷xs≢[] : ∀ {a} {A : Set a} (x : A) (xs : List A) → ¬ (x ∷ xs ≡ [])
+x∷xs≢[] x xs ()
+
+foldr₁ : ∀ {a} {A : Set a} {l : List A} → ¬ (l ≡ []) → (A → A → A) → A
+foldr₁ {l = x ∷ []} _ _ = x
+foldr₁ {l = x ∷ x' ∷ xs} _ f = f x (foldr₁ {l = x' ∷ xs} (x∷xs≢[] x' xs) f)
+foldr₁ {l = []} l≢[] _ = ⊥-elim (l≢[] refl)