從構造就拒絕錯誤

{-# 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，並且證明可以仰賴定義等價。

從構造就拒絕錯誤 [ag-SPBG]