Merge pull request #70 from pmbittner/IndexedSet-equivalence-equivalence

Embrace constructive logic to proof `≅→≅[]`

Author: pmbittner

src/Data/IndexedSet.lagda.md

@@ -278,6 +278,39 @@ Our new relations can be converted back to the old ones by just forgetting the e
 ≅[]→≅ (A⊆[f]B , B⊆[f⁻¹]A) = ⊆[]→⊆ A⊆[f]B , ⊆[]→⊆ B⊆[f⁻¹]A
 ```
 
+
+As Agda implements constructive logic, the converse is also possible.
+```agda
+∈-index : ∀ {I : Set iℓ} {A : IndexedSet I} {a : Carrier}
+  → a ∈ A
+  → I
+∈-index (i , eq) = i
+
+∈→∈[] : ∀ {I : Set iℓ} {A : IndexedSet I} {a : Carrier}
+  → (p : a ∈ A)
+    ----------
+  → a ≈ A (∈-index p)
+∈→∈[] (i , eq) = eq
+
+⊆-index : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J}
+  → A ⊆ B
+  → I → J
+⊆-index A⊆B i = ∈-index (A⊆B i)
+
+⊆→⊆[] : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J}
+  → (subset : A ⊆ B)
+    -----------
+  → A ⊆[ ⊆-index subset ] B
+⊆→⊆[] A⊆B i = proj₂ (A⊆B i)
+
+≅→≅[] : ∀ {I : Set iℓ} {J : Set jℓ} {A : IndexedSet I} {B : IndexedSet J}
+  → (eq : A ≅ B)
+    -----------------
+  → A ≅[ ⊆-index (proj₁ eq) ][ ⊆-index (proj₂ eq) ] B
+≅→≅[] (A⊆B , B⊆A) = (⊆→⊆[] A⊆B) , (⊆→⊆[] B⊆A)
+```
+
+
 If two indexed sets are pointwise equal, they are equivelent in terms of the identify function because
 indices do not have to be translated.
 

src/Framework/Relation/Expressiveness.lagda.md

@@ -179,31 +179,15 @@ compiler-from-expressiveness : ∀ {L M : VariabilityLanguage V}
   → LanguageCompiler L M
 compiler-from-expressiveness {L} {M} exp = record
   { compile         = proj₁ ∘ exp
-  ; config-compiler = λ e → record { to = conf e ; from = fnoc e }
-  ; preserves       = λ e → ⊆-conf e , ⊆-fnoc e
+  ; config-compiler = λ e → record
+    { to   = ⊆-index (proj₁ (proj₂ (exp e)))
+    ; from = ⊆-index (proj₂ (proj₂ (exp e)))
+    }
+  ; preserves       = ≅→≅[] ∘ proj₂ ∘ exp
   }
   where
-    ⟦_⟧₁ = Semantics L
-    ⟦_⟧₂ = Semantics M
     open import Data.EqIndexedSet
 
-    conf : ∀ {A} → Expression L A → Config L → Config M
-    conf e c₁ = proj₁ (proj₁ (proj₂ (exp e)) c₁)
-
-    fnoc : ∀ {A} → Expression L A → Config M → Config L
-    fnoc e c₂ = proj₁ (proj₂ (proj₂ (exp e)) c₂)
-
-    eq : ∀ {A} → (e : Expression L A) → ⟦ e ⟧₁ ≅ ⟦ proj₁ (exp e) ⟧₂
-    eq e = proj₂ (exp e)
-
-    ⊆-conf : ∀ {A} → (e : Expression L A) → ⟦ e ⟧₁ ⊆[ conf e ] ⟦ proj₁ (exp e) ⟧₂
-    ⊆-conf e with eq e
-    ... | ⊆ , _ = proj₂ ∘ ⊆
-
-    ⊆-fnoc : ∀ {A} → (e : Expression L A) → ⟦ proj₁ (exp e) ⟧₂ ⊆[ fnoc e ] ⟦ e ⟧₁
-    ⊆-fnoc e with eq e
-    ... | _ , ⊇ = proj₂ ∘ ⊇
-
 {-|
 When M is not at least as expressive as L,
 then L can never be compiled to M.