Skip to content

Commit fd164c8

Browse files
pmbittnerpmbittner
authored
Merge pull request #89 from VariantSync/variation-tree-rename
Prove that variation tree feature names can be renamed
2 parents 55b59ef + c5aa71a commit fd164c8

3 files changed

Lines changed: 222 additions & 3 deletions

File tree

‎src/Vatras/Data/Prop/Rename.agda‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
{-|
2+
This module renames variables in Prop expressions.
3+
4+
The idea of this translation is to apply a renaming function `f : F₁ → F₂` to
5+
all elements of `F₁` in the datastructure `Prop F₁` to obtain a new datastructure
6+
`Prop F₂`. To prove preservation of the semantics, we also require a left inverse
7+
`f⁻¹ : D₂ → D₁` of `f` as a proof that `f` is injective. This precondition is
8+
necessary because a non-injective rename could reduce the number of variables.
9+
-}
10+
module Vatras.Data.Prop.Rename where
11+
12+
import Data.Bool as Bool
13+
open import Function using (_∘_; id)
14+
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_)
15+
16+
open import Vatras.Data.Prop
17+
18+
rename : {F₁ F₂ : Set} → (F₁ → F₂) → Prop F₁ → Prop F₂
19+
rename f true = true
20+
rename f false = false
21+
rename f (var v) = var (f v)
22+
rename f (¬ p) = ¬ (rename f p)
23+
rename f (p ∧ q) = rename f p ∧ rename f q
24+
25+
rename-spec
26+
: {F₁ F₂ : Set}
27+
→ (f : F₁ → F₂)
28+
→ (p : Prop F₁)
29+
→ (c : Assignment F₂)
30+
→ eval (rename f p) c ≡ eval p (c ∘ f)
31+
rename-spec f true c = refl
32+
rename-spec f false c = refl
33+
rename-spec f (var v) c = refl
34+
rename-spec f (¬ p) c = Eq.cong Bool.not (rename-spec f p c)
35+
rename-spec f (p ∧ q) c = Eq.cong₂ Bool._∧_ (rename-spec f p c) (rename-spec f q c)
36+
37+
rename-preserves
38+
: {F₁ F₂ : Set}
39+
→ (f : F₁ → F₂)
40+
→ (f⁻¹ : F₂ → F₁)
41+
→ f⁻¹ ∘ f ≗ id
42+
→ (p : Prop F₁)
43+
→ (c : Assignment F₁)
44+
→ eval (rename f p) (c ∘ f⁻¹) ≡ eval p c
45+
rename-preserves f f⁻¹ f∘f⁻¹≗id true c = refl
46+
rename-preserves f f⁻¹ f∘f⁻¹≗id false c = refl
47+
rename-preserves f f⁻¹ f∘f⁻¹≗id (var v) c = Eq.cong c (f∘f⁻¹≗id v)
48+
rename-preserves f f⁻¹ f∘f⁻¹≗id (¬ p) c = Eq.cong Bool.not (rename-preserves f f⁻¹ f∘f⁻¹≗id p c)
49+
rename-preserves f f⁻¹ f∘f⁻¹≗id (p ∧ q) c = Eq.cong₂ Bool._∧_ (rename-preserves f f⁻¹ f∘f⁻¹≗id p c) (rename-preserves f f⁻¹ f∘f⁻¹≗id q c)

‎src/Vatras/Translation/Lang/VT/Rename.agda‎

Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
{-|
2+
This module renames dimensions in variation tree expressions.
3+
4+
The idea of this translation is to apply a renaming function `f : D₁ → D₂` to
5+
all elements of `D₁` in the datastructure `VT D₁` to obtain a new datastructure
6+
`VT D₂`. To prove preservation of the semantics, we also require a left inverse
7+
`f⁻¹ : D₂ → D₁` of `f` as a proof that `f` is injective. This precondition is
8+
necessary because a non-injective rename would reduce the number of possible
9+
variants.
10+
-}
11+
module Vatras.Translation.Lang.VT.Rename where
12+
13+
open import Data.Bool using (if_then_else_)
14+
open import Data.List as List using (List; []; _∷_; _++_)
15+
open import Data.Product using (_,_)
16+
open import Function using (id; _∘_)
17+
open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_)
18+
19+
open import Vatras.Util.AuxProofs using (if-congˡ; if-cong)
20+
open import Vatras.Data.EqIndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
21+
open import Vatras.Framework.Compiler using (LanguageCompiler)
22+
open import Vatras.Framework.Definitions using (𝔸; 𝔽)
23+
open import Vatras.Framework.Variants as V using (Forest)
24+
open import Vatras.Framework.Relation.Expressiveness Forest using (_≽_; expressiveness-from-compiler)
25+
open import Vatras.Framework.Relation.Function using (from; to)
26+
import Vatras.Data.Prop as Prop
27+
import Vatras.Data.Prop.Rename as Prop
28+
29+
open import Vatras.Lang.All
30+
open VT using (VT; UnrootedVT; VTL; _-<_>-; if[_]then[_]; if[_]then[_]else[_]; if-true[_])
31+
32+
open Eq.≡-Reasoning
33+
34+
VT-map-config : ∀ {D₁ D₂ : 𝔽}
35+
→ (D₂ → D₁)
36+
→ VT.Configuration D₁
37+
→ VT.Configuration D₂
38+
VT-map-config f config = config ∘ f
39+
40+
rename' : ∀ {D₁ D₂ : 𝔽} {A : 𝔸}
41+
→ (D₁ → D₂)
42+
→ UnrootedVT D₁ A
43+
→ UnrootedVT D₂ A
44+
45+
rename'-all : ∀ {D₁ D₂ : 𝔽} {A : 𝔸}
46+
→ (D₁ → D₂)
47+
→ List (UnrootedVT D₁ A)
48+
→ List (UnrootedVT D₂ A)
49+
50+
rename' f (a -< cs >-) = a -< rename'-all f cs >-
51+
rename' f if[ p ]then[ l ] = if[ Prop.rename f p ]then[ rename'-all f l ]
52+
rename' f if[ p ]then[ l ]else[ r ] = if[ Prop.rename f p ]then[ rename'-all f l ]else[ rename'-all f r ]
53+
54+
rename'-all f [] = []
55+
rename'-all f (x ∷ xs) = rename' f x ∷ rename'-all f xs
56+
57+
rename : ∀ {D₁ D₂ : 𝔽} {A : 𝔸}
58+
→ (D₁ → D₂)
59+
→ VT D₁ A → VT D₂ A
60+
rename f if-true[ l ] = if-true[ rename'-all f l ]
61+
62+
module _ {D₁ D₂ : 𝔽} {A : 𝔸} (f : D₁ → D₂) where
63+
preserves-⊆ : (expr : UnrootedVT D₁ A)
64+
→ VT.configure (rename' f expr) ⊆[ VT-map-config f ] VT.configure expr
65+
66+
preserves-⊆-all : (expr : List (UnrootedVT D₁ A))
67+
→ VT.configure-all (rename'-all f expr) ⊆[ VT-map-config f ] VT.configure-all expr
68+
69+
preserves-⊆ (a -< l >-) config =
70+
VT.configure (rename' f (a -< l >-)) config
71+
≡⟨⟩
72+
a V.-< VT.configure-all (rename'-all f l) config >- ∷ []
73+
≡⟨ Eq.cong (λ x → a V.-< x >- ∷ []) (preserves-⊆-all l config) ⟩
74+
a V.-< VT.configure-all l (config ∘ f) >- ∷ []
75+
≡⟨⟩
76+
VT.configure (a -< l >-) (config ∘ f)
77+
∎
78+
preserves-⊆ if[ p ]then[ l ] config =
79+
VT.configure (rename' f (if[ p ]then[ l ])) config
80+
≡⟨⟩
81+
(if Prop.eval (Prop.rename f p) config then VT.configure-all (rename'-all f l) config else [])
82+
≡⟨ Eq.cong (if_then _ else []) (Prop.rename-spec f p config) ⟩
83+
(if Prop.eval p (config ∘ f) then VT.configure-all (rename'-all f l) config else [])
84+
≡⟨ if-congˡ (Prop.eval p (config ∘ f)) (preserves-⊆-all l config) ⟩
85+
(if Prop.eval p (config ∘ f) then VT.configure-all l (config ∘ f) else [])
86+
≡⟨⟩
87+
VT.configure (if[ p ]then[ l ]) (config ∘ f)
88+
∎
89+
preserves-⊆ if[ p ]then[ l ]else[ r ] config =
90+
VT.configure (rename' f (if[ p ]then[ l ]else[ r ])) config
91+
≡⟨⟩
92+
(if Prop.eval (Prop.rename f p) config then VT.configure-all (rename'-all f l) config else VT.configure-all (rename'-all f r) config)
93+
≡⟨ Eq.cong (if_then _ else _) (Prop.rename-spec f p config) ⟩
94+
(if Prop.eval p (config ∘ f) then VT.configure-all (rename'-all f l) config else VT.configure-all (rename'-all f r) config)
95+
≡⟨ if-cong _ (preserves-⊆-all l config) (preserves-⊆-all r config) ⟩
96+
(if Prop.eval p (config ∘ f) then VT.configure-all l (config ∘ f) else VT.configure-all r (config ∘ f))
97+
≡⟨⟩
98+
VT.configure (if[ p ]then[ l ]else[ r ]) (config ∘ f)
99+
∎
100+
101+
preserves-⊆-all [] config = refl
102+
preserves-⊆-all (x ∷ xs) config = Eq.cong₂ _++_ (preserves-⊆ x config) (preserves-⊆-all xs config)
103+
104+
module _ {D₁ D₂ : 𝔽} {A : 𝔸} (f : D₁ → D₂) (f⁻¹ : D₂ → D₁) (f∘f⁻¹≗id : f⁻¹ ∘ f ≗ id) where
105+
preserves-⊇ : (expr : UnrootedVT D₁ A)
106+
→ VT.configure expr ⊆[ VT-map-config f⁻¹ ] VT.configure (rename' f expr)
107+
108+
preserves-⊇-all : (expr : List (UnrootedVT D₁ A))
109+
→ VT.configure-all expr ⊆[ VT-map-config f⁻¹ ] VT.configure-all (rename'-all f expr)
110+
111+
preserves-⊇ (a -< l >-) config =
112+
VT.configure (a -< l >-) config
113+
≡⟨⟩
114+
a V.-< VT.configure-all l config >- ∷ []
115+
≡⟨ Eq.cong (λ x → a V.-< x >- ∷ []) (preserves-⊇-all l config) ⟩
116+
a V.-< VT.configure-all (rename'-all f l) (config ∘ f⁻¹) >- ∷ []
117+
≡⟨⟩
118+
VT.configure (rename' f (a -< l >-)) (config ∘ f⁻¹)
119+
∎
120+
preserves-⊇ if[ p ]then[ l ] config =
121+
VT.configure (if[ p ]then[ l ]) config
122+
≡⟨⟩
123+
(if Prop.eval p config then VT.configure-all l config else [])
124+
≡⟨ if-congˡ (Prop.eval p config) (preserves-⊇-all l config) ⟩
125+
(if Prop.eval p config then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else [])
126+
≡⟨ Eq.cong (if_then _ else []) (Prop.rename-preserves f f⁻¹ f∘f⁻¹≗id p config) ⟨
127+
(if Prop.eval (Prop.rename f p) (config ∘ f⁻¹) then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else [])
128+
≡⟨⟩
129+
VT.configure (rename' f (if[ p ]then[ l ])) (config ∘ f⁻¹)
130+
∎
131+
preserves-⊇ if[ p ]then[ l ]else[ r ] config =
132+
VT.configure (if[ p ]then[ l ]else[ r ]) config
133+
≡⟨⟩
134+
(if Prop.eval p config then VT.configure-all l config else VT.configure-all r config)
135+
≡⟨ if-cong _ (preserves-⊇-all l config) (preserves-⊇-all r config) ⟩
136+
(if Prop.eval p config then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else VT.configure-all (rename'-all f r) (config ∘ f⁻¹))
137+
≡⟨ Eq.cong (if_then _ else _) (Prop.rename-preserves f f⁻¹ f∘f⁻¹≗id p config) ⟨
138+
(if Prop.eval (Prop.rename f p) (config ∘ f⁻¹) then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else VT.configure-all (rename'-all f r) (config ∘ f⁻¹))
139+
≡⟨⟩
140+
VT.configure (rename' f (if[ p ]then[ l ]else[ r ])) (config ∘ f⁻¹)
141+
∎
142+
143+
preserves-⊇-all [] config = refl
144+
preserves-⊇-all (x ∷ xs) config = Eq.cong₂ _++_ (preserves-⊇ x config) (preserves-⊇-all xs config)
145+
146+
preserves : (e : VT D₁ A)
147+
→ VT.⟦ rename f e ⟧ ≅[ VT-map-config f ][ VT-map-config f⁻¹ ] VT.⟦ e ⟧
148+
preserves if-true[ e ] = preserves-⊆-all f e , preserves-⊇-all e
149+
150+
VT-rename : ∀ {D₁ D₂ : 𝔽}
151+
→ (f : D₁ → D₂)
152+
→ (f⁻¹ : D₂ → D₁)
153+
→ f⁻¹ ∘ f ≗ id
154+
→ LanguageCompiler (VTL D₁) (VTL D₂)
155+
VT-rename f f⁻¹ is-inverse .LanguageCompiler.compile = rename f
156+
VT-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .to = VT-map-config f⁻¹
157+
VT-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .from = VT-map-config f
158+
VT-rename f f⁻¹ is-inverse .LanguageCompiler.preserves expr = ≅[]-sym (preserves f f⁻¹ is-inverse expr)
159+
160+
VT-rename≽VT : ∀ {D₁ D₂ : Set}
161+
→ (f : D₁ → D₂)
162+
→ (f⁻¹ : D₂ → D₁)
163+
→ f⁻¹ ∘ f ≗ id
164+
→ VTL D₂ ≽ VTL D₁
165+
VT-rename≽VT f f⁻¹ is-inverse = expressiveness-from-compiler (VT-rename f f⁻¹ is-inverse)

‎src/Vatras/Translation/LanguageMap.lagda.md‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ open import Vatras.Util.String using (diagonal-ℕ; diagonal-ℕ⁻¹; diagonal-
3434
3535
import Vatras.Framework.Proof.ForFree
3636
open Vatras.Framework.Proof.ForFree Variant using (less-expressive-from-completeness; completeness-by-expressiveness; soundness-by-expressiveness)
37-
open Vatras.Framework.Proof.ForFree using () renaming (soundness-by-expressiveness to soundness-by-expressiveness-on)
37+
open Vatras.Framework.Proof.ForFree using () renaming (completeness-by-expressiveness to completeness-by-expressiveness-on; soundness-by-expressiveness to soundness-by-expressiveness-on)
3838
3939
import Vatras.Framework.Properties.Completeness
4040
import Vatras.Framework.Properties.Soundness
@@ -57,6 +57,7 @@ open VT using (VTL)
5757
open import Vatras.Lang.CCC.Encode using () renaming (encoder to CCC-Rose-encoder)
5858
open import Vatras.Translation.Lang.NCC.Rename using (NCC-rename≽NCC)
5959
open import Vatras.Translation.Lang.2CC.Rename using (2CC-rename; 2CC-rename≽2CC)
60+
open import Vatras.Translation.Lang.VT.Rename using (VT-rename≽VT)
6061
6162
import Vatras.Translation.Lang.CCC-to-NCC as CCC-to-NCC
6263
import Vatras.Translation.Lang.NCC-to-CCC as NCC-to-CCC
@@ -371,8 +372,12 @@ open import Vatras.Lang.VariantList.Properties
371372
ADT-is-sound-on : ∀ {F : 𝔽} (V : 𝕍) (_==_ : DecidableEquality F) → Sound-on V (ADTL F V)
372373
ADT-is-sound-on {F} V _==_ = soundness-by-expressiveness-on V (VariantList-is-sound-on V) (ADT-to-VariantList.VariantList≽ADT F V _==_)
373374
374-
VT-is-complete : Complete-on Forest (VTL ℕ)
375-
VT-is-complete = VariantList-to-VT.VT-is-complete
375+
VTℕ-is-complete : Complete-on Forest (VTL ℕ)
376+
VTℕ-is-complete = VariantList-to-VT.VT-is-complete
377+
378+
VT-is-complete : {F : 𝔽} (f : ℕ → F) (f⁻¹ : F → ℕ) (f⁻¹∘f≗id : f⁻¹ ∘ f ≗ id)
379+
→ Complete-on Forest (VTL F)
380+
VT-is-complete f f⁻¹ f⁻¹∘f≗id = completeness-by-expressiveness-on Forest VTℕ-is-complete (VT-rename≽VT f f⁻¹ f⁻¹∘f≗id)
376381
377382
VT-is-sound : ∀ {F : 𝔽} (_==_ : DecidableEquality F) → Sound-on Forest (VTL F)
378383
VT-is-sound {F} _==_ = soundness-by-expressiveness-on Forest (ADT-is-sound-on Forest _==_) (VT-to-ADT.ADT≽VT F)

0 commit comments

Comments
 (0)