Formalization of Succinctness

src/Vatras/Data/IndexedSet.lagda.md

@@ -882,3 +882,15 @@ re-index {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-
   , re-indexʳ {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent
 ```
 
+### Ungrouped Properties
+
+```agda
+module _ where
+  open import Data.Nat as ℕ using (ℕ)
+  open import Data.Fin as Fin using (Fin)
+  open import Data.List using (lookup; tabulate)
+
+  tabulate⁺ : ∀ {j} {J : Set j} {n : ℕ} {A : IndexedSet (Fin n)} {B : IndexedSet J} → A ⊆ B → lookup (tabulate A) ⊆ B
+  tabulate⁺ {n = ℕ.suc n} x Fin.zero = x Fin.zero
+  tabulate⁺ {n = ℕ.suc n} x (Fin.suc i) = tabulate⁺ (x ∘ Fin.suc) i
+```

src/Vatras/Framework/Definitions.agda

@@ -1,9 +1,12 @@
 module Vatras.Framework.Definitions where
 
 open import Data.Maybe using (Maybe; just)
+open import Data.Nat as ℕ using (ℕ; zero)
 open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂) renaming (_,_ to _and_)
+import Data.Product.Properties as Product
+open import Data.String as String using (String)
 open import Data.Unit using (⊤; tt) public
-open import Function using (id; _∘_)
+open import Function using (id; _∘_; const)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Nullary.Negation using (¬_)
@@ -20,12 +23,13 @@ the core definitions because it is quite reasonable.
 Any actual data we can think of to plug in here (e.g., strings, tokens or
 nodes of an abstract syntax tree) can be checked for equality.
 -}
-𝔸 : Set₁
-𝔸 = Σ Set DecidableEquality
-
--- retrieve the set of atoms from an atom type 𝔸
-atoms : 𝔸 → Set
-atoms = proj₁
+record 𝔸 : Set₁ where
+  no-eta-equality
+  field
+    atoms : Set
+    atomsEqual? : DecidableEquality atoms
+    atomSize : atoms → ℕ
+open 𝔸 public
 
 {-|
 Variant Language.
@@ -63,14 +67,23 @@ and hence expressions are parameterized in the type of this atomic data.
 𝔼 = 𝔸 → Set₁
 
 -- some default atoms
-module _ where
-  open import Data.String using (String; _≟_)
-
-  STRING : 𝔸
-  STRING = String and _≟_
+STRING : 𝔸
+STRING = record
+  { atoms = String
+  ; atomsEqual? = String._≟_
+  ; atomSize = String.length
+  }
 
-module _ where
-  open import Data.Nat using (ℕ; _≟_)
+NAT : 𝔸
+NAT = record
+  { atoms = ℕ × ℕ
+  ; atomsEqual? = Product.≡-dec ℕ._≟_ ℕ._≟_
+  ; atomSize = proj₂
+  }
 
-  NAT : 𝔸
-  NAT = ℕ and _≟_
+NAT' : 𝔸
+NAT' = record
+  { atoms = ℕ
+  ; atomsEqual? = ℕ._≟_
+  ; atomSize = const zero
+  }

src/Vatras/Framework/Variants.agda

@@ -7,7 +7,7 @@ module Vatras.Framework.Variants where
 
 open import Data.List using (List; []; _∷_; map)
 open import Data.Maybe using (nothing; just)
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.String using (String; _++_; intersperse)
 open import Data.Unit using (⊤; tt)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl)
@@ -16,7 +16,7 @@ open Eq.≡-Reasoning
 open import Function using (id; _∘_; flip)
 open import Size using (Size; ↑_; ∞)
 
-open import Vatras.Framework.Definitions using (𝕍; 𝔸; atoms)
+open import Vatras.Framework.Definitions using (𝕍; 𝔸; atoms; atomsEqual?)
 open import Vatras.Framework.VariabilityLanguage
 open import Vatras.Framework.Compiler using (LanguageCompiler)
 open LanguageCompiler
@@ -77,11 +77,17 @@ GrulerVL = Variant-is-VL GrulerVariant
 RoseVL : VariabilityLanguage (Rose ∞)
 RoseVL = Variant-is-VL (Rose ∞)
 
+{-|
+Lemma to conclude that the child lists of two equal rose trees must be equal as well.
+-}
+Rose-injective : ∀ {A : 𝔸} {a₁ a₂ : atoms A} {cs₁ cs₂ : List (Rose ∞ A)} → a₁ -< cs₁ >- ≡ a₂ -< cs₂ >- → (a₁ ≡ a₂) × (cs₁ ≡ cs₂)
+Rose-injective refl = refl , refl
+
 {-|
 Lemma to conclude that the child lists of two equal rose trees must be equal as well.
 -}
 children-equality : ∀ {A : 𝔸} {a₁ a₂ : atoms A} {cs₁ cs₂ : List (Rose ∞ A)} → a₁ -< cs₁ >- ≡ a₂ -< cs₂ >- → cs₁ ≡ cs₂
-children-equality refl = refl
+children-equality = proj₂ ∘ Rose-injective
 
 {-|
 Show function for rose trees.
@@ -149,6 +155,6 @@ open import Data.Bool using (Bool; true)
 open import Data.Bool.ListAction using (or)
 
 has-atom : ∀ {A i} → atoms A → Rose i A → Bool
-has-atom {A , _≟_} a (b -< cs >-) with a ≟ b
+has-atom {A} a (b -< cs >-) with atomsEqual? A a b
 ... | yes refl = true
 ... | no x = or (map (has-atom b) cs)

src/Vatras/Lang/2CC/Encode.agda

@@ -0,0 +1,58 @@
+open import Vatras.Framework.Definitions using (𝔽)
+module Vatras.Lang.2CC.Encode {Dimension : 𝔽} where
+
+open import Data.List as List using (List; []; _∷_)
+
+open import Size using (∞)
+open import Data.Bool using (false)
+open import Data.Unit using (⊤; tt)
+open import Data.List.Properties using (map-∘; map-id; map-cong)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+
+open import Vatras.Data.EqIndexedSet using (_≅[_][_]_; irrelevant-index-≅)
+open import Vatras.Framework.Variants as V using (Rose; Variant-is-VL; VariantEncoder)
+open import Vatras.Framework.Relation.Function using (_⇔_; to; from)
+open import Vatras.Framework.VariabilityLanguage using (Semantics; Config)
+open import Vatras.Lang.2CC Dimension
+
+encode : ∀ {i} {A} → Rose i A → 2CC ∞ A
+encode (a V.-< cs >-) = a -< List.map encode cs >-
+
+confs : ⊤ ⇔ Config 2CCL
+confs = record
+  { to = λ where tt _ → false
+  ; from = λ _ → tt
+  }
+
+2cc-encode-idemp : ∀ {A} (v : Rose ∞ A) → (c : Configuration) → ⟦ encode v ⟧ c ≡ v
+2cc-encode-idemp {A} v@(a V.-< cs >-) c =
+  begin
+    ⟦ encode v ⟧ c
+  ≡⟨⟩
+    a V.-< List.map (λ x → ⟦ x ⟧ c) (List.map encode cs) >-
+  ≡⟨ Eq.cong (a V.-<_>-) (map-∘ cs) ⟨
+    a V.-< List.map (λ x → ⟦ encode x ⟧ c) cs >-
+  ≡⟨ Eq.cong (a V.-<_>-) (go cs) ⟩
+    v
+  ∎
+  where
+  open Eq.≡-Reasoning
+
+  go : (cs' : List (Rose ∞ A)) → List.map (λ c' → ⟦ encode c' ⟧ c) cs' ≡ cs'
+  go [] = refl
+  go (c' ∷ cs') = Eq.cong₂ _∷_ (2cc-encode-idemp c' c) (go cs')
+
+preserves : ∀ {A} → (v : Rose ∞ A)
+  → Semantics (Variant-is-VL (Rose ∞)) v ≅[ to confs ][ from confs ] ⟦ encode v ⟧
+preserves {A} v = irrelevant-index-≅ v
+  (λ { tt → refl })
+  (2cc-encode-idemp v)
+  (to confs)
+  (from confs)
+
+encoder : VariantEncoder (Rose ∞) 2CCL
+encoder = record
+  { compile = encode
+  ; config-compiler = λ _ → confs
+  ; preserves = preserves
+  }

src/Vatras/Lang/2CC/FixedArtifactLength.agda

@@ -0,0 +1,118 @@
+open import Vatras.Framework.Definitions using (𝔽; 𝔸; atoms)
+module Vatras.Lang.2CC.FixedArtifactLength (Dimension : 𝔽) (A : 𝔸) where
+
+open import Data.Bool using (true; false)
+open import Data.Empty using (⊥-elim)
+open import Data.List as List using (List; []; _∷_; _++_)
+import Data.List.Properties as List
+open import Data.List.Relation.Ternary.Interleaving.Propositional using (Interleaving; []; consˡ; consʳ)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+import Data.List.Relation.Unary.All.Properties
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
+open import Data.Nat as ℕ using (ℕ; suc; _+_; _∸_; _*_; _≤_; z≤n; s≤s; _≥_)
+import Data.Nat.Properties as ℕ
+open import Data.Product using (_×_; _,_; proj₂; ∃-syntax)
+open import Function using (_∘_; const)
+open import Relation.Binary.PropositionalEquality as Eq using (refl; _≡_; _≢_)
+open import Size using (Size; ∞)
+
+import Vatras.Util.List as List
+open import Vatras.Data.EqIndexedSet using (_∈_; _⊆_)
+open import Vatras.Framework.Variants using (Rose; children-equality)
+open import Vatras.Lang.2CC Dimension using (2CC; _⟨_,_⟩; _-<_>-; ⟦_⟧)
+open import Vatras.Lang.2CC.ReflectsVariantSize using (reflectsVariantSize)
+open import Vatras.Succinctness.Sizes using (sizeRose; size2CC)
+
+_≉_ : Rose ∞ A → Rose ∞ A → Set
+(a₁ Rose.-< cs₁ >-) ≉ (a₂ Rose.-< cs₂ >-) = List.length cs₁ ≢ List.length cs₂
+
+fixedChildCount : ∀ {i}
+  → {a₁ : atoms A} {cs₁ : List (Rose ∞ A)}
+  → {a₂ : atoms A} {cs₂ : List (2CC i A)}
+  → (a₁ Rose.-< cs₁ >-) ∈ ⟦ a₂ -< cs₂ >- ⟧
+  → List.length cs₁ ≡ List.length cs₂
+fixedChildCount {cs₁ = cs₁} {cs₂ = cs₂} (c , v≡e) =
+    List.length cs₁
+  ≡⟨ Eq.cong List.length (children-equality v≡e) ⟩
+    List.length (List.map (λ e → ⟦ e ⟧ c) cs₂)
+  ≡⟨ List.length-map (λ e → ⟦ e ⟧ c) cs₂ ⟩
+    List.length cs₂
+  ∎
+  where
+  open Eq.≡-Reasoning
+
+partition : ∀ {i : Size}
+  → (D : Dimension) (c₁ c₂ : 2CC i A)
+  → (vs : List (Rose ∞ A))
+  → AllPairs _≉_ vs
+  → All (_∈ ⟦ D 2CC.⟨ c₁ , c₂ ⟩ ⟧) vs
+  → ∃[ vs₁ ] ∃[ vs₂ ]
+    Interleaving vs₁ vs₂ vs
+  × All (_∈ ⟦ c₁ ⟧) vs₁
+  × All (_∈ ⟦ c₂ ⟧) vs₂
+partition D c₁ c₂ [] unique-vs vs⊆e = [] , [] , [] , [] , []
+partition D c₁ c₂ (v ∷ vs) (v∉vs ∷ unique-vs) ((c , v≡e) ∷ vs⊆e)
+  with partition D c₁ c₂ vs unique-vs vs⊆e
+... | vs₁ , vs₂ , partition , vs₁⊆e , vs₂⊆e
+  with c D
+... | true = v ∷ vs₁ , vs₂ , consˡ partition , (c , v≡e) ∷ vs₁⊆e , vs₂⊆e
+... | false = vs₁ , v ∷ vs₂ , consʳ partition , vs₁⊆e , (c , v≡e) ∷ vs₂⊆e
+
+sum≤size2CC : ∀ {i : Size}
+  → (e : 2CC i A)
+  → (vs : List (Rose ∞ A))
+  → AllPairs (_≉_) vs
+  → All (_∈ ⟦ e ⟧) vs
+  → List.sum (List.map sizeRose vs) ≤ size2CC e
+sum≤size2CC (a -< cs >-) [] unique-vs vs⊆e = z≤n
+sum≤size2CC (a -< cs >-) (v ∷ []) unique-vs (v∈e ∷ []) =
+  begin
+    List.sum (List.map sizeRose (v ∷ []))
+  ≡⟨⟩
+    sizeRose v + 0
+  ≡⟨ ℕ.+-identityʳ (sizeRose v) ⟩
+    sizeRose v
+  ≤⟨ reflectsVariantSize v (a -< cs >-) v∈e ⟩
+    size2CC (a -< cs >-)
+  ∎
+  where
+  open ℕ.≤-Reasoning
+sum≤size2CC (a -< cs >-) ((a₁ Rose.-< cs₁ >-) ∷ (a₂ Rose.-< cs₂ >-) ∷ vs) ((v₁≢v₂ ∷ v₁∉vs) ∷ unique-vs) (v₁∈e ∷ v₂∈e ∷ vs⊆e) =
+  ⊥-elim (v₁≢v₂ (Eq.trans (fixedChildCount v₁∈e) (Eq.sym (fixedChildCount v₂∈e))))
+sum≤size2CC (D ⟨ c₁ , c₂ ⟩) vs unique-vs vs⊆e with partition D c₁ c₂ vs unique-vs vs⊆e
+... | vs₁ , vs₂ , partition , vs₁⊆c₁ , vs₂⊆c₂ =
+  begin
+    List.sum (List.map sizeRose vs)
+  ≡⟨ List.sum-Interleaving (List.map-Interleaving partition) ⟨
+    List.sum (List.map sizeRose vs₁) + List.sum (List.map sizeRose vs₂)
+  ≤⟨ ℕ.+-mono-≤ (sum≤size2CC c₁ vs₁ (List.AllPairs-resp-⊆ (List.Interleaving⇒Sublistˡ partition) unique-vs) vs₁⊆c₁) (sum≤size2CC c₂ vs₂ (List.AllPairs-resp-⊆ (List.Interleaving⇒Sublistʳ partition) unique-vs) vs₂⊆c₂) ⟩
+    size2CC c₁ + size2CC c₂
+  <⟨ ℕ.n<1+n (size2CC c₁ + size2CC c₂) ⟩
+    size2CC (D ⟨ c₁ , c₂ ⟩)
+  ∎
+  where
+  open ℕ.≤-Reasoning
+
+different-children-counts :
+  ∀ {i : Size}
+  → (n : ℕ)
+  → (e : 2CC i A)
+  → (vs : List (Rose ∞ A))
+  → All (_∈ ⟦ e ⟧) vs
+  → All (λ v → sizeRose v ≥ n) vs
+  → AllPairs _≉_ vs
+  → size2CC e ≥ List.length vs * n
+different-children-counts n e vs vs⊆e vs≥n unique-vs =
+  begin
+    List.length vs * n
+  ≡⟨ List.sum-replicate (List.length vs) n ⟨
+    List.sum (List.replicate (List.length vs) n)
+  ≡⟨ Eq.cong List.sum (List.map-const n vs) ⟨
+    List.sum (List.map (const n) vs)
+  ≤⟨ List.sum-map-≤-with∈ vs (λ v v∈vs → All.lookup vs≥n v∈vs) ⟩
+    List.sum (List.map sizeRose vs)
+  ≤⟨ sum≤size2CC e vs unique-vs (vs⊆e) ⟩
+    size2CC e
+  ∎
+  where
+  open ℕ.≤-Reasoning

src/Vatras/Lang/2CC/ReflectsVariantSize.agda

@@ -0,0 +1,75 @@
+open import Vatras.Framework.Definitions using (𝔽; 𝔸; atomSize)
+module Vatras.Lang.2CC.ReflectsVariantSize {Dimension : 𝔽} {A : 𝔸} where
+
+open import Data.Bool using (true; false)
+open import Data.List as List using (List; []; _∷_)
+import Data.List.Properties as List
+open import Data.Nat using (suc; _+_; _≤_; s≤s)
+import Data.Nat.Properties as ℕ
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Size using (Size; ∞)
+
+open import Vatras.Data.EqIndexedSet using (_∈_)
+open import Vatras.Framework.Variants using (Rose; Rose-injective)
+open import Vatras.Lang.2CC Dimension using (2CC; _⟨_,_⟩; _-<_>-; ⟦_⟧)
+open import Vatras.Succinctness.Sizes using (sizeRose; size2CC)
+
+reflectsVariantSize : ∀ {i : Size}
+  → (v : Rose ∞ A)
+  → (e : 2CC i A)
+  → v ∈ ⟦ e ⟧
+  → sizeRose v ≤ size2CC e
+reflectsVariantSize v (D ⟨ l , r ⟩) (config , v≡e) with config D
+reflectsVariantSize v (D ⟨ l , r ⟩) (config , v≡e) | true =
+  begin
+    sizeRose v
+  ≤⟨ reflectsVariantSize v l (config , v≡e) ⟩
+    size2CC l
+  <⟨ ℕ.n<1+n (size2CC l) ⟩
+    suc (size2CC l)
+  ≤⟨ s≤s (ℕ.m≤m+n (size2CC l) (size2CC r)) ⟩
+    suc (size2CC l + size2CC r)
+  ≡⟨⟩
+    size2CC (D ⟨ l , r ⟩)
+  ∎
+  where
+  open ℕ.≤-Reasoning
+reflectsVariantSize v (D ⟨ l , r ⟩) (config , v≡e) | false =
+  begin
+    sizeRose v
+  ≤⟨ reflectsVariantSize v r (config , v≡e) ⟩
+    size2CC r
+  <⟨ ℕ.n<1+n (size2CC r) ⟩
+    suc (size2CC r)
+  ≤⟨ s≤s (ℕ.m≤n+m (size2CC r) (size2CC l)) ⟩
+    suc (size2CC l + size2CC r)
+  ≡⟨⟩
+    size2CC (D ⟨ l , r ⟩)
+  ∎
+  where
+  open ℕ.≤-Reasoning
+reflectsVariantSize (a Rose.-< cs >-) (a' -< cs' >-) (config , v≡e) =
+  begin
+    sizeRose (a Rose.-< cs >-)
+  ≡⟨⟩
+    suc (atomSize A a + List.sum (List.map sizeRose cs))
+  ≤⟨ s≤s (ℕ.+-monoʳ-≤ (atomSize A a) (go cs cs' (proj₂ (Rose-injective v≡e)))) ⟩
+    suc (atomSize A a + List.sum (List.map size2CC cs'))
+  ≡⟨⟩
+    size2CC (a -< cs' >-)
+  ≡⟨ Eq.cong (λ x → size2CC (x -< cs' >-)) (proj₁ (Rose-injective v≡e)) ⟩
+    size2CC (a' -< cs' >-)
+  ∎
+  where
+  open ℕ.≤-Reasoning
+
+  go : ∀ {i : Size}
+    → (cs : List (Rose ∞ A)) (cs' : List (2CC i A))
+    → cs ≡ List.map (λ c → ⟦ c ⟧ config) cs'
+    → List.sum (List.map sizeRose cs) ≤ List.sum (List.map size2CC cs')
+  go [] [] cs≡cs' = ℕ.≤-refl
+  go (c ∷ cs) (c' ∷ cs') cs≡cs' =
+    ℕ.+-mono-≤
+      (reflectsVariantSize c c' (config , List.∷-injectiveˡ cs≡cs'))
+      (go cs cs' (List.∷-injectiveʳ cs≡cs'))

src/Vatras/Lang/2CC/Show.agda

@@ -9,12 +9,12 @@ open import Data.List as List using ([]; _∷_)
 open import Vatras.Show.Lines
 open import Vatras.Lang.2CC Dimension using (2CC; _⟨_,_⟩; _-<_>-)
 
-show : ∀ {i} → 2CC i (String , String._≟_) → String
+show : ∀ {i} → 2CC i STRING → String
 show (a -< [] >-) = a
 show (a -< es@(_ ∷ _) >-) = a ++ "-<" ++ (String.intersperse ", " (List.map show es)) ++ ">-"
 show (D ⟨ l , r ⟩) = show-D D ++ "⟨" ++ (show l) ++ ", " ++ (show r) ++ "⟩"
 
-pretty : ∀ {i : Size} → 2CC i (String , String._≟_) → Lines
+pretty : ∀ {i : Size} → 2CC i STRING → Lines
 pretty (a -< [] >-) = > a
 pretty (a -< es@(_ ∷ _) >-) = do
   > a ++ "-<"