{-# OPTIONS --safe --without-K #-} open import MLTT.Spartan hiding (_+_) open import MLTT.Maybe open import MGS.MLTT using (has-decidable-equality) open import Integers.Type open import Integers.Addition module ag-SPBG where data Unit : 𝓤₀ ̇ where Meter Kilogram Second : Unit Unit-≟ : has-decidable-equality Unit Unit-≟ Meter Meter = inl refl Unit-≟ Kilogram Kilogram = inl refl Unit-≟ Second Second = inl refl Unit-≟ Meter Kilogram = inr λ () Unit-≟ Meter Second = inr λ () Unit-≟ Kilogram Meter = inr λ () Unit-≟ Kilogram Second = inr λ () Unit-≟ Second Meter = inr λ () Unit-≟ Second Kilogram = inr λ ()
為了讓構造出來的 List
裡面的單位只有一種正確排列方式，我們可以幫單位附上順序，這個順序其實並不重要，只是需要有一個來確保
List
只有一種排列方法，從而去除因為排列順序不同而無法被定義等價認出來的不同表達方式（[A, B]
跟 [B, A] 兩種構造）
_<Unit_ : Unit → Unit → 𝓤₀ ̇ Meter <Unit Meter = 𝟘 Meter <Unit Kilogram = 𝟙 Meter <Unit Second = 𝟙 Kilogram <Unit Meter = 𝟘 Kilogram <Unit Kilogram = 𝟘 Kilogram <Unit Second = 𝟙 Second <Unit _ = 𝟘 <Unit-trans : (u v w : Unit) → u <Unit v → v <Unit w → u <Unit w <Unit-trans Meter Kilogram Second _ _ = ⋆ <Unit-trans Meter Kilogram Kilogram _ () <Unit-trans Meter Kilogram Meter _ () <Unit-trans Meter Second _ _ () <Unit-trans Kilogram Second _ _ () <Unit-trans Meter Meter _ () _ <Unit-trans Kilogram Meter _ () _ <Unit-trans Kilogram Kilogram _ () _ <Unit-trans Second _ _ () _ data Tri (u v : Unit) : 𝓤₀ ̇ where is-< : u <Unit v → Tri u v is-≡ : u ＝ v → Tri u v is-> : v <Unit u → Tri u v tri : (u v : Unit) → Tri u v tri Meter Meter = is-≡ refl tri Meter Kilogram = is-< ⋆ tri Meter Second = is-< ⋆ tri Kilogram Meter = is-> ⋆ tri Kilogram Kilogram = is-≡ refl tri Kilogram Second = is-< ⋆ tri Second Meter = is-> ⋆ tri Second Kilogram = is-> ⋆ tri Second Second = is-≡ refl
單位定了順序之後，這裏規定 List 中的單位必須按照特定順序排列，確保每個組合單位的表示形式只有一種
data _<?_ : Maybe Unit → Unit → 𝓤₀ ̇ where no-bd : ∀ {u} → Nothing <? u bd : ∀ {v u} → v <Unit u → Just v <? u
接著在 cons 中我們規定 ¬ (n ＝ pos 0)
因此不會出現 3 s⁰ 這種可以直接寫成 3
的情況
data UL (lb : Maybe Unit) : 𝓤₀ ̇ where [] : UL lb cons : (u : Unit) → lb <? u → (n : ℤ) → ¬ (n ＝ pos 0) → UL (Just u) → UL lb Units : 𝓤₀ ̇ Units = UL Nothing <?-trans : ∀ {lb u v} → lb <? u → u <Unit v → lb <? v <?-trans no-bd _ = no-bd <?-trans (bd w<u) u<v = bd (<Unit-trans _ _ _ w<u u<v) weaken : ∀ {lb u} → lb <? u → UL (Just u) → UL lb weaken bd' [] = [] weaken bd' (cons v (bd u<v) n nz rest) = cons v (<?-trans bd' u<v) n nz rest insert : ∀ {lb} (u : Unit) → lb <? u → (n : ℤ) → ¬ (n ＝ pos 0) → UL lb → UL lb insert u ord n nz [] = cons u ord n nz [] insert u ord n nz (cons v ord' m nz' rest) with tri u v ... | is-< u<v = cons u ord n nz (cons v (bd u<v) m nz' rest) ... | is-> v<u = cons v ord' m nz' (insert u (bd v<u) n nz rest) ... | is-≡ refl with ℤ-is-discrete (n + m) (pos 0) ... | inl _ = weaken ord rest ... | inr nz-sum = cons u ord (n + m) nz-sum rest *-unit : ∀ {lb} → UL lb → Units → Units *-unit [] ys = ys *-unit (cons u _ n nz rest) ys = insert u no-bd n nz (*-unit rest ys)
構造一些案例來看看這種實現
1m : Units 1m = cons Meter no-bd (pos 1) (λ ()) [] 1s : Units 1s = cons Second no-bd (pos 1) (λ ()) [] 1/s : Units 1/s = cons Second no-bd (negsucc 0) (λ ()) []
對消就會得到純量
cancel : *-unit 1s 1/s ＝ [] cancel = refl
另外也嘗試證明比較複雜的案例
m³ : Units m³ = cons Meter no-bd (pos 3) (λ ()) [] 1m³s : Units 1m³s = cons Meter no-bd (pos 3) (λ ()) (cons Second (bd ⋆) (pos 1) (λ ()) []) m³-×̇-1s : *-unit m³ 1s ＝ 1m³s m³-×̇-1s = refl
這個方法的缺點是我們被迫仔細的構造構造子，構造複雜也難用，並創造了一個內容無關緊要的 strict order 與大量的輔助函數來處理這些問題。但比起另外兩個方案，這個方案並不需要 function extensionality，並且證明可以仰賴定義等價。