Merge pull request #95 from VariantSync/develop

Release 2.2

Author: ibbem

.github/workflows/check.yml

@@ -18,6 +18,9 @@ jobs:
       with:
         key: nix-${{ hashFiles('.github/workflows/check.yml', 'default.nix', 'nix/**') }}
         nix_file: nix/github-workflow-dependencies.nix
+    - name: Setup the environment
+      # Supress a warning about missing channels by using the shell from the environment
+      run: echo NIX_BUILD_SHELL="$(which bash)" >> "$GITHUB_ENV"
     - name: Check Agda files
       run: nix-shell --run './scripts/check-all.sh github-action'
     - name: Check for sources of inconsistencies

default.nix

@@ -9,7 +9,7 @@
     },
 }:
 pkgs.agdaPackages.mkDerivation {
-  version = "2.1";
+  version = "2.2";
   pname = "Vatras";
   src = with pkgs.lib.fileset;
     toSource {

src/Vatras/Data/IndexedSet.lagda.md

@@ -45,7 +45,7 @@ module Eq = IsEquivalence isEquivalence
 ## Definitions
 
 ```agda
-variable
+private variable
   iℓ jℓ kℓ : Level
 
 -- An index can just be any set (of any universe, which is why it looks so complicated).
@@ -130,6 +130,19 @@ _⊢_≡ⁱ_ : ∀ {I : Set iℓ} (A : IndexedSet I) → I → I → Set ℓ
 A ⊢ i ≡ⁱ j = A i ≈ A j
 ```
 
+## Inverse Operations
+
+```agda
+_∉_ : ∀ {I : Set iℓ} → Carrier → IndexedSet I → Set (ℓ ⊔ iℓ)
+a ∉ A = ∀ i → ¬ (a ≈ A i)
+
+Disjoint : ∀ {I : Set iℓ} {J : Set jℓ} (A : IndexedSet I) (B : IndexedSet J) → Set (ℓ ⊔ iℓ ⊔ jℓ)
+Disjoint A B = ∀ i → A i ∉ B
+
+Disjoint-flip : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} → Disjoint A B → Disjoint B A
+Disjoint-flip disjointAB j i Bj≈Ai = disjointAB i j (Eq.sym Bj≈Ai)
+```
+
 ## Singletons
 
 ```agda
@@ -164,11 +177,13 @@ We now prove the following theorems:
 ⊆-refl i = i , Eq.refl
 
 -- There is no antisymmetry definition in Relation.Binary.Indexed.Heterogeneous.Definition. Adding that to the standard library would be good and a low hanging fruit.
-⊆-antisym : ∀ {I : Set iℓ} {J : Set jℓ} → Antisym (_⊆_ {i₁ = I}) (_⊆_ {i₁ = J}) (_≅_)
+-- ⊆-antisym : ∀ {I : Set iℓ} {J : Set jℓ} → Antisym (_⊆_ {i₁ = I}) (_⊆_ {i₁ = J}) (_≅_)
+⊆-antisym : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} → A ⊆ B → B ⊆ A → A ≅ B
 ⊆-antisym l r = l , r
 
 -- There are no generalized transitivity, symmetry and antisymmetry definitions which allow different levels in Relation.Binary.Indexed.Heterogeneous.Definition . Adding that to the standard library would be good and a low hanging fruit.
-⊆-trans : Transitive (IndexedSet {iℓ}) _⊆_
+-- ⊆-trans : Transitive (IndexedSet {iℓ}) _⊆_
+⊆-trans : ∀ {I : Set iℓ} {J : Set jℓ} {K : Set kℓ} {A : IndexedSet I} {B : IndexedSet J} {C : IndexedSet K} → A ⊆ B → B ⊆ C → A ⊆ C
 ⊆-trans A⊆B B⊆C i =
   -- This proof looks resembles state monad bind >>=.
   -- interesting... 🤔
@@ -179,10 +194,10 @@ We now prove the following theorems:
 ≅-refl : Reflexive (IndexedSet {iℓ}) _≅_
 ≅-refl = ⊆-refl , ⊆-refl
 
-≅-sym : Symmetric (IndexedSet {iℓ}) _≅_
+≅-sym : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J} → A ≅ B → B ≅ A
 ≅-sym (l , r) = r , l
 
-≅-trans : Transitive (IndexedSet {iℓ}) _≅_
+≅-trans : ∀ {I : Set iℓ} {J : Set jℓ} {K : Set kℓ} {A : IndexedSet I} {B : IndexedSet J} {C : IndexedSet K} → A ≅ B → B ≅ C → A ≅ C
 ≅-trans (A⊆B , B⊆A) (B⊆C , C⊆B) =
     ⊆-trans A⊆B B⊆C
   , ⊆-trans C⊆B B⊆A
@@ -625,6 +640,183 @@ singleton-set-is-nonempty : (A : 𝟙 iℓ) → nonempty A
 singleton-set-is-nonempty _ = tt
 ```
 
+## Operations
+
+```agda
+module _ where
+  open import Data.Sum using (_⊎_; inj₁; inj₂)
+  private variable
+    α : Set iℓ
+    β : Set jℓ
+
+  {-|
+  Indexed Set Union (Or):
+  We can create the union of two indexed sets by accepting either of the input indices.
+  -}
+  infix 21 _⨆_
+  _⨆_ : IndexedSet α → IndexedSet β → IndexedSet (α ⊎ β)
+  (A ⨆ B) (inj₁ a) = A a
+  (A ⨆ B) (inj₂ b) = B b
+
+  {-|
+  Indexed Set Intersection (And):
+  The set intersection should contain only elements that are both in A _and_ B.
+  This means that an element is in the intersection if and only if there is an
+  index for both A and B that both point to the element.
+  Hence, the index set of the intersection set can be modelled as the type of
+  all indices from A that point to elements that also B points to.
+  -}
+  infix 21 _⨅_
+  _⨅_ : (A : IndexedSet α) → (B : IndexedSet β) → IndexedSet (Σ[ a ∈ α ] A a ∈ B)
+  (A ⨅ B) (a , b , eq) = A a -- We could also pick B b here.
+
+  {-|
+  Indexed Set Difference:
+  We can remove all elements pointed to by B from an indexed set A by restricting the set of indices
+  to those indices that do not point to elements in B.
+  Hence, the index set of the difference set can be modelled as the type of
+  all indices from A that point to elements that are not pointed at by B.
+  -}
+  infix 21 _∖_ -- use \setminus to create ∖ with Agda Input Mode in Emacs
+  _∖_ : (A : IndexedSet α) → (B : IndexedSet β) → IndexedSet (Σ[ a ∈ α ] (A a ∉ B))
+  (A ∖ B) (a , Aa∉B) = A a
+
+  module _ where
+    open import Data.Empty using (⊥-elim)
+    private variable
+      γ : Set kℓ
+      A : IndexedSet α
+      B : IndexedSet β
+      C : IndexedSet γ
+
+    -- ⨆ properties
+
+    ⊆-⨆ : A ⊆ A ⨆ B
+    ⊆-⨆ i = inj₁ i , Eq.refl
+
+    ⨆-⊆ : B ⊆ A → A ⨆ B ⊆ A
+    ⨆-⊆ _   (inj₁ a) = a , Eq.refl
+    ⨆-⊆ B⊆A (inj₂ b) = B⊆A b
+
+    ⨆-idemp : A ⨆ A ≅ A
+    ⨆-idemp = ⨆-⊆ ⊆-refl , ⊆-⨆
+
+    ⨆-comm-⊆ : A ⨆ B ⊆ B ⨆ A
+    ⨆-comm-⊆ (inj₁ a) = inj₂ a , Eq.refl
+    ⨆-comm-⊆ (inj₂ b) = inj₁ b , Eq.refl
+
+    ⨆-comm : A ⨆ B ≅ B ⨆ A
+    ⨆-comm = ⨆-comm-⊆ , ⨆-comm-⊆
+
+    ⨆-assoc-⊆ : (A ⨆ B) ⨆ C ⊆ A ⨆ (B ⨆ C)
+    ⨆-assoc-⊆ (inj₁ (inj₁ a)) = ⊆-⨆ a
+    ⨆-assoc-⊆ (inj₁ (inj₂ b)) = inj₂ (inj₁ b) , Eq.refl
+    ⨆-assoc-⊆ (inj₂ c)        = inj₂ (inj₂ c) , Eq.refl
+
+    ⨆-assoc-⊇ : A ⨆ (B ⨆ C) ⊆ (A ⨆ B) ⨆ C
+    ⨆-assoc-⊇ (inj₁ a)        = inj₁ (inj₁ a) , Eq.refl
+    ⨆-assoc-⊇ (inj₂ (inj₁ b)) = inj₁ (inj₂ b) , Eq.refl
+    ⨆-assoc-⊇ (inj₂ (inj₂ c)) = inj₂ c , Eq.refl
+
+    ⨆-assoc : (A ⨆ B) ⨆ C ≅ A ⨆ (B ⨆ C)
+    ⨆-assoc = ⨆-assoc-⊆ , ⨆-assoc-⊇
+
+    ⨆-idʳ : A ⨆ 𝟘 ≅ A
+    ⨆-idʳ = ⨆-⊆ 𝟘⊆A , ⊆-⨆
+
+    ⨆-idˡ : 𝟘 ⨆ A ≅ A
+    ⨆-idˡ = ≅-trans ⨆-comm ⨆-idʳ
+
+    -- ⨅ properties
+
+    ⨅-⊆ : A ⨅ B ⊆ A
+    ⨅-⊆ (a₁ , _ ) = a₁ , Eq.refl
+
+    ⊆-⨅ : A ⊆ B → A ⊆ A ⨅ B
+    ⊆-⨅ A⊆B a = (a , A⊆B a) , Eq.refl
+
+    ⨅-idemp : A ⨅ A ≅ A
+    ⨅-idemp = ⨅-⊆ , ⊆-⨅ ⊆-refl
+
+    ⨅-comm-⊆ : A ⨅ B ⊆ B ⨅ A
+    ⨅-comm-⊆ (a , b , Aa≈Bb) = (b , a , Eq.sym Aa≈Bb) , Aa≈Bb
+
+    ⨅-comm : A ⨅ B ≅ B ⨅ A
+    ⨅-comm = ⨅-comm-⊆ , ⨅-comm-⊆
+
+    ⨅-assoc-⊆ : (A ⨅ B) ⨅ C ⊆ A ⨅ (B ⨅ C)
+    ⨅-assoc-⊆ ((a , b , Aa≈Bb) , c , Aa≈Cc) = (a , (b , c , Eq.trans (Eq.sym Aa≈Bb) Aa≈Cc) , Aa≈Bb) , Eq.refl
+
+    ⨅-assoc-⊇ : A ⨅ (B ⨅ C) ⊆ (A ⨅ B) ⨅ C
+    ⨅-assoc-⊇ (a , (b , c , Bb≈Cc) , Aa≈Bb) = ((a , b , Aa≈Bb) , c , Eq.trans Aa≈Bb Bb≈Cc) , Eq.refl
+
+    ⨅-assoc : (A ⨅ B) ⨅ C ≅ A ⨅ (B ⨅ C)
+    ⨅-assoc = ⨅-assoc-⊆ , ⨅-assoc-⊇
+
+    ⨅-zeroˡ : 𝟘 ⨅ A ≅ 𝟘
+    ⨅-zeroˡ = ⨅-⊆  , ⊆-⨅ 𝟘⊆A
+
+    ⨅-zeroʳ : A ⨅ 𝟘 ≅ 𝟘
+    ⨅-zeroʳ = ≅-trans ⨅-comm ⨅-zeroˡ
+
+    -- "A ⨅ B ≅ 𝟘" and "Disjoint A B" are equivalent propositions.
+    -- "A ⨅ B ≅ 𝟘" is the canonical way of saying that two sets are disjoint.
+    -- "Disjoint A B" is a direct way of saying that for indexed sets.
+
+    ⨅-empty→Disjoint : A ⨅ B ≅ 𝟘 → Disjoint A B
+    ⨅-empty→Disjoint (A⨅B⊆𝟘 , 𝟘⊆A⨅B) a b Aa≈Bb with A⨅B⊆𝟘 (a , b , Aa≈Bb)
+    ... | ()
+
+    Disjoint→⨅-empty : Disjoint A B → A ⨅ B ≅ 𝟘
+    proj₁ (Disjoint→⨅-empty disjointAB) (a , b , Aa≈Bb) = ⊥-elim (disjointAB a b Aa≈Bb)
+    proj₂ (Disjoint→⨅-empty disjointAB) = 𝟘⊆A
+
+    -- ∖ properties
+
+    ∖-⊆ : A ∖ B ⊆ A
+    ∖-⊆ (a , Aa∉B) = a , Eq.refl
+
+    ⊆-∖ : A ⨅ B ≅ 𝟘 → A ⊆ (A ∖ B)
+    ⊆-∖ A⨅B≅𝟘 a = (a , ⨅-empty→Disjoint A⨅B≅𝟘 a) , Eq.refl
+
+    ≅-∖ : A ⨅ B ≅ 𝟘 → A ≅ (A ∖ B)
+    ≅-∖ A⨅B≅𝟘 = ⊆-∖ A⨅B≅𝟘 , ∖-⊆
+
+    ∖-id : A ∖ 𝟘 ≅ A
+    ∖-id = ∖-⊆ , ⊆-∖ ⨅-zeroʳ
+
+    ∖-zero-⊆ : 𝟘 ∖ A ⊆ 𝟘
+    ∖-zero-⊆ ()
+
+    ∖-zero : 𝟘 ∖ A ≅ 𝟘
+    ∖-zero = ∖-zero-⊆ , 𝟘⊆A
+
+    -- combined properties
+
+    ⨆-distrib-⨅-⊆ : A ⨆ (B ⨅ C) ⊆ (A ⨆ B) ⨅ (A ⨆ C)
+    ⨆-distrib-⨅-⊆ (inj₁ a)               = (inj₁ a , ⊆-⨆ a) , Eq.refl
+    ⨆-distrib-⨅-⊆ (inj₂ (b , c , Bb≈Cc)) = (inj₂ b , inj₂ c , Bb≈Cc) , Eq.refl
+
+    ⨆-distrib-⨅-⊇ : (A ⨆ B) ⨅ (A ⨆ C) ⊆ A ⨆ (B ⨅ C)
+    ⨆-distrib-⨅-⊇ (inj₁ a , _)              = inj₁ a , Eq.refl
+    ⨆-distrib-⨅-⊇ (inj₂ b , inj₁ a , Bb≈Aa) = inj₁ a , Bb≈Aa
+    ⨆-distrib-⨅-⊇ (inj₂ b , inj₂ c , Bb≈Cc) = inj₂ (b , c , Bb≈Cc) , Eq.refl
+
+    ⨆-distrib-⨅ : A ⨆ (B ⨅ C) ≅ (A ⨆ B) ⨅ (A ⨆ C)
+    ⨆-distrib-⨅ = ⨆-distrib-⨅-⊆ , ⨆-distrib-⨅-⊇
+
+    ⨅-distrib-⨆-⊆ : A ⨅ (B ⨆ C) ⊆ (A ⨅ B) ⨆ (A ⨅ C)
+    ⨅-distrib-⨆-⊆ (a , inj₁ b , Aa≈Bb) = inj₁ (a , b , Aa≈Bb) , Eq.refl
+    ⨅-distrib-⨆-⊆ (a , inj₂ c , Aa≈Cc) = inj₂ (a , c , Aa≈Cc) , Eq.refl
+
+    ⨅-distrib-⨆-⊇ : (A ⨅ B) ⨆ (A ⨅ C) ⊆ A ⨅ (B ⨆ C)
+    ⨅-distrib-⨆-⊇ (inj₁ (a , b , Aa≈Bb)) = (a , inj₁ b , Aa≈Bb) , Eq.refl
+    ⨅-distrib-⨆-⊇ (inj₂ (a , c , Aa≈Cc)) = (a , inj₂ c , Aa≈Cc) , Eq.refl
+
+    ⨅-distrib-⨆ : A ⨅ (B ⨆ C) ≅ (A ⨅ B) ⨆ (A ⨅ C)
+    ⨅-distrib-⨆ = ⨅-distrib-⨆-⊆ , ⨅-distrib-⨆-⊇
+```
+
 ## Further Properties
 
 ### Reindexing

src/Vatras/Lang/ADT/Merge.agda

@@ -66,11 +66,10 @@ module Named (F : 𝔽) where
 
 module Prop (F : 𝔽) where
   open import Vatras.Data.Prop
-  open Vatras.Lang.ADT (Prop F) V
   open import Vatras.Lang.ADT.Prop F V
-  open Named (Prop F)
+  open Named (Prop F) using (_⊕_) public
 
-  ⊕-specₚ : ∀ {A} (l r : ADT A) (c : Assignment F) →
+  ⊕-specₚ : ∀ {A} (l r : PropADT A) (c : Assignment F) →
      ⟦ l ⊕ r ⟧ₚ c ≡ ⟦ l ⟧ₚ c +ᵥ ⟦ r ⟧ₚ c
   ⊕-specₚ (leaf v) (leaf r) c = refl
   ⊕-specₚ (leaf l) (E ⟨ el , er ⟩) c with eval E c

src/Vatras/Lang/ADT/Prop.agda

@@ -4,10 +4,17 @@ module Vatras.Lang.ADT.Prop (F : 𝔽) (V : 𝕍) where
 open import Data.Bool using (if_then_else_)
 open import Vatras.Data.Prop using (Prop; Assignment; eval)
 open import Vatras.Framework.VariabilityLanguage
-open import Vatras.Lang.ADT (Prop F) V
 
-⟦_⟧ₚ : 𝔼-Semantics V (Assignment F) ADT
+import Vatras.Lang.ADT
+open Vatras.Lang.ADT using (ADT)
+open Vatras.Lang.ADT (Prop F) V using (⟦_⟧)
+open Vatras.Lang.ADT (Prop F) V using (leaf; _⟨_,_⟩) public
+
+PropADT : 𝔼
+PropADT = ADT (Prop F) V
+
+⟦_⟧ₚ : 𝔼-Semantics V (Assignment F) PropADT
 ⟦ e ⟧ₚ c = ⟦ e ⟧ (λ D → eval D c)
 
 PropADTL : VariabilityLanguage V
-PropADTL = ⟪ ADT , Assignment F , ⟦_⟧ₚ ⟫
+PropADTL = ⟪ PropADT , Assignment F , ⟦_⟧ₚ ⟫

src/Vatras/Lang/All.agda

@@ -17,6 +17,7 @@ import Vatras.Lang.NCC
 import Vatras.Lang.2CC
 import Vatras.Lang.NADT
 import Vatras.Lang.ADT
+import Vatras.Lang.ADT.Prop
 import Vatras.Lang.OC
 import Vatras.Lang.FST
 import Vatras.Lang.Gruler
@@ -69,6 +70,11 @@ module ADT where
   module _ {F : 𝔽} {V : 𝕍} where
     open Vatras.Lang.ADT F V hiding (ADT; ADTL; Configuration) public
 
+module PropADT where
+  open Vatras.Lang.ADT.Prop using (PropADT; PropADTL) public
+  module _ {F : 𝔽} {V : 𝕍} where
+    open Vatras.Lang.ADT.Prop F V hiding (PropADT; PropADTL) public
+
 module OC where
   open Vatras.Lang.OC using (OC; OCL; WFOC; WFOCL; Configuration) public
   module _ {F : 𝔽} where

src/Vatras/Lang/All/Fixed.agda

@@ -10,6 +10,7 @@ import Vatras.Lang.NCC
 import Vatras.Lang.2CC
 import Vatras.Lang.NADT
 import Vatras.Lang.ADT
+import Vatras.Lang.ADT.Prop
 import Vatras.Lang.OC
 import Vatras.Lang.FST
 import Vatras.Lang.Gruler
@@ -24,6 +25,7 @@ module NCC where
     open Vatras.Lang.NCC F n hiding (NCC; NCCL; Configuration) public
 module 2CC = Vatras.Lang.2CC F
 module NADT = Vatras.Lang.NADT F V
+module PropADT = Vatras.Lang.ADT.Prop F V
 module ADT = Vatras.Lang.ADT F V
 module OC = Vatras.Lang.OC F
 module FST = Vatras.Lang.FST F

src/Vatras/Lang/NCC.lagda.md

@@ -3,10 +3,12 @@
 This module defines the choice calculus in which every choice must have the same
 fixed number of alternatives, called $n-CC$ in our paper.
 
-It's required that arity $n$ is at least one to have semantics. However, we require
-that the arity is at least two, otherwise there is this annoying one-arity
-language in the NCC language family which is incomplete.
-In our paper, we also only inspect the languages with `n ≥ 2`.
+We require the arity $n$ to be at least two.
+An arity of zero would mean that all choices have zero alternatives.
+Choices with zero alternatives hence would constitute leaf terms without a clear purpose.
+Choices with exactly one alternative have only one way to be configured: selecting that single alternative.
+In both cases of an arity of zero or one, an $n-CC$ term denotes a single constant variant.
+For this reason, we restrict $n$ to be at least two, as we also did in our paper.
 
 ## Module
 
@@ -39,10 +41,8 @@ data NCC : Size → 𝔼 where
 ## Semantics
 
 The semantics is very similar to the semantics for core choice calculus.
-The differences are:
-
-- We can restrict configuration to choose alternatives within bounds because the arity of choices is known in advance.
-- We can then do a vector lookup instead of a list lookup in the semantics.
+The only difference is that we can restrict the configuration process to choose alternatives within bounds because the arity of choices is known in advance.
+We hence do a vector lookup instead of a list lookup.
 
 ```agda
 Configuration : ℂ