|
| 1 | +------------------------------------------------------------------------ |
| 2 | +-- The Agda standard library |
| 3 | +-- |
| 4 | +-- An example of how to use `Wrap` to help term inference. |
| 5 | +------------------------------------------------------------------------ |
| 6 | + |
| 7 | +{-# OPTIONS --without-K --safe #-} |
| 8 | + |
| 9 | +module README.Data.Wrap where |
| 10 | + |
| 11 | +open import Data.Wrap |
| 12 | + |
| 13 | +open import Algebra |
| 14 | +open import Data.Nat |
| 15 | +open import Data.Nat.Properties |
| 16 | +open import Data.Product |
| 17 | +open import Level using (Level) |
| 18 | +open import Relation.Binary |
| 19 | + |
| 20 | +private |
| 21 | + variable |
| 22 | + c ℓ : Level |
| 23 | + A : Set c |
| 24 | + m n : ℕ |
| 25 | + |
| 26 | +------------------------------------------------------------------------ |
| 27 | +-- `Wrap` for remembering instances |
| 28 | +------------------------------------------------------------------------ |
| 29 | + |
| 30 | +module Instances where |
| 31 | + |
| 32 | + -- `Monoid.Carrier` gets the carrier set from a monoid, and thus has |
| 33 | + -- type `Monoid c ℓ → Set c`. |
| 34 | + -- Using `Wrap`, we can convert `Monoid.Carrier` into an equivalent |
| 35 | + -- “wrapped” version: `MonoidEl`. |
| 36 | + MonoidEl : Monoid c ℓ → Set c |
| 37 | + MonoidEl = Wrap Monoid.Carrier |
| 38 | + |
| 39 | + -- We can turn any monoid into the equivalent monoid where the elements |
| 40 | + -- and equations have been wrapped. |
| 41 | + -- The translation mainly consists of wrapping and unwrapping everything |
| 42 | + -- via the `Wrap` constructor, `[_]`. |
| 43 | + -- Notice that the equality field is wrapping the binary relation |
| 44 | + -- `_≈_ : (x y : Carrier) → Set ℓ`, giving an example of how `Wrap` works |
| 45 | + -- for arbitrary n-ary relations. |
| 46 | + Wrap-monoid : Monoid c ℓ → Monoid c ℓ |
| 47 | + Wrap-monoid M = record |
| 48 | + { Carrier = MonoidEl M |
| 49 | + ; _≈_ = λ ([ x ]) ([ y ]) → Wrap _≈_ x y |
| 50 | + ; _∙_ = λ ([ x ]) ([ y ]) → [ x ∙ y ] |
| 51 | + ; ε = [ ε ] |
| 52 | + ; isMonoid = record |
| 53 | + { isSemigroup = record |
| 54 | + { isMagma = record |
| 55 | + { isEquivalence = record |
| 56 | + { refl = [ refl ] |
| 57 | + ; sym = λ ([ xy ]) → [ sym xy ] |
| 58 | + ; trans = λ ([ xy ]) ([ yz ]) → [ trans xy yz ] |
| 59 | + } |
| 60 | + ; ∙-cong = λ ([ xx ]) ([ yy ]) → [ ∙-cong xx yy ] |
| 61 | + } |
| 62 | + ; assoc = λ ([ x ]) ([ y ]) ([ z ]) → [ assoc x y z ] |
| 63 | + } |
| 64 | + ; identity = (λ ([ x ]) → [ identityˡ x ]) |
| 65 | + , (λ ([ x ]) → [ identityʳ x ]) |
| 66 | + } |
| 67 | + } |
| 68 | + where open Monoid M |
| 69 | + |
| 70 | + -- Usually, we would only open one monoid at a time. |
| 71 | + -- If we were to open two monoids `M` and `N` simultaneously, Agda would |
| 72 | + -- get confused whenever it came across, for example, `_∙_`, not knowing |
| 73 | + -- whether it came from `M` or `N`. |
| 74 | + -- This is true whether or not `M` and `N` can be disambiguated by some |
| 75 | + -- other means (such as by their `Carrier`s). |
| 76 | + |
| 77 | + -- However, with wrapped monoids, we are going to remember the monoid |
| 78 | + -- while checking any monoid expressions, so we can afford to have just |
| 79 | + -- one, polymorphic, version of `_∙_` visible globally. |
| 80 | + open module Wrap-monoid {c ℓ} {M : Monoid c ℓ} = Monoid (Wrap-monoid M) |
| 81 | + |
| 82 | + -- Now we can test out this construct on some existing monoids. |
| 83 | + |
| 84 | + open import Data.Nat.Properties |
| 85 | + |
| 86 | + -- Notice that, while the following two definitions appear to be defined |
| 87 | + -- by the same expression, their types are genuinely different. |
| 88 | + -- Whereas `Carrier +-0-monoid = ℕ = Carrier *-1-monoid`, `MonoidEl M` |
| 89 | + -- does not compute, and thus |
| 90 | + -- `MonoidEl +-0-monoid ≠ MonoidEl *-1-monoid` definitionally. |
| 91 | + -- This lets us use the respective monoids when checking the respective |
| 92 | + -- definitions. |
| 93 | + |
| 94 | + test-+ : MonoidEl +-0-monoid |
| 95 | + test-+ = ([ 3 ] ∙ ε) ∙ [ 2 ] |
| 96 | + |
| 97 | + test-* : MonoidEl *-1-monoid |
| 98 | + test-* = ([ 3 ] ∙ ε) ∙ [ 2 ] |
| 99 | + |
| 100 | + -- The reader is invited to normalise these two definitions |
| 101 | + -- (`C-c C-n`, then type in the name). |
| 102 | + -- `test-+` is interpreted using (ℕ, +, 0), and thus computes to `[ 5 ]`. |
| 103 | + -- Meanwhile, `test-*` is interpreted using (ℕ, *, 1), and thus computes |
| 104 | + -- to `[ 6 ]`. |
| 105 | + |
| 106 | +------------------------------------------------------------------------ |
| 107 | +-- `Wrap` for dealing with functions spoiling unification |
| 108 | +------------------------------------------------------------------------ |
| 109 | + |
| 110 | +module Unification where |
| 111 | + |
| 112 | + open import Relation.Binary.PropositionalEquality |
| 113 | + |
| 114 | + module Naïve where |
| 115 | + |
| 116 | + -- We want to work with factorisations of natural numbers in a |
| 117 | + -- “proof-relevant” style. We could draw out `Factor m n o` as |
| 118 | + -- m |
| 119 | + -- /*\ |
| 120 | + -- n o. |
| 121 | + |
| 122 | + Factor : (m n o : ℕ) → Set |
| 123 | + Factor m n o = m ≡ n * o |
| 124 | + |
| 125 | + -- We can prove a basic lemma about `Factor`: the following tree rotation |
| 126 | + -- can be done, due to associativity of `_*_`. |
| 127 | + -- m m |
| 128 | + -- /*\ /*\ |
| 129 | + -- no p ----> n op |
| 130 | + -- /*\ /*\ |
| 131 | + -- n o o p |
| 132 | + |
| 133 | + assoc-→ : ∀ {m n o p} → |
| 134 | + (∃ λ no → Factor m no p × Factor no n o) → |
| 135 | + (∃ λ op → Factor m n op × Factor op o p) |
| 136 | + assoc-→ {m} {n} {o} {p} (._ , refl , refl) = _ , *-assoc n o p , refl |
| 137 | + |
| 138 | + -- We must give at least some arguments to `*-assoc`, as Agda is unable to |
| 139 | + -- unify `? * ? * ?` with `n * o * p`, as `_*_` is a function and not |
| 140 | + -- necessarily injective (and indeed not injective when one of its |
| 141 | + -- arguments is 0). |
| 142 | + |
| 143 | + -- We now want to use this lemma in a more complex proof: |
| 144 | + -- m m |
| 145 | + -- /*\ /*\ |
| 146 | + -- nop q n opq |
| 147 | + -- /*\ ----> /*\ |
| 148 | + -- no p o pq |
| 149 | + -- /*\ /*\ |
| 150 | + -- n o p q |
| 151 | + |
| 152 | + test : ∀ {m n o p q} → |
| 153 | + (∃₂ λ no nop → Factor m nop q × Factor nop no p × Factor no n o) → |
| 154 | + (∃₂ λ pq opq → Factor m n opq × Factor opq o pq × Factor pq p q) |
| 155 | + test {n = n} (no , nop , fm , fnop , fno) = |
| 156 | + let _ , fm , fpq = assoc-→ {n = no} (_ , fm , fnop) in |
| 157 | + let _ , fm , fopq = assoc-→ {n = n} (_ , fm , fno) in |
| 158 | + _ , _ , fm , fopq , fpq |
| 159 | + |
| 160 | + -- This works okay, but where we have written `{n = no}` and similar, we |
| 161 | + -- are being forced to deal with details we don't really care about. Agda |
| 162 | + -- should be able to fill in the vertices given part of a tree, but can't |
| 163 | + -- due to similar reasons as before: `Factor ? ? ?` doesn't unify against |
| 164 | + -- `Factor m no p`, because both instances of `Factor` compute and we're |
| 165 | + -- left trying to unify `? * ?` against `no * p`. |
| 166 | + |
| 167 | + module Wrapped where |
| 168 | + |
| 169 | + -- We can use `Wrap` to stop the computation of `Factor`. |
| 170 | + |
| 171 | + Factor : (m n o : ℕ) → Set |
| 172 | + Factor = Wrap λ m n o → m ≡ n * o |
| 173 | + |
| 174 | + -- Because `assoc-→` needs access to the implementation of `Factor`, the |
| 175 | + -- proof is exactly as before except for using `[_]` to wrap and unwrap. |
| 176 | + |
| 177 | + assoc-→ : ∀ {m n o p} → |
| 178 | + (∃ λ no → Factor m no p × Factor no n o) → |
| 179 | + (∃ λ op → Factor m n op × Factor op o p) |
| 180 | + assoc-→ {m} {n} {o} {p} (._ , [ refl ] , [ refl ]) = |
| 181 | + _ , [ *-assoc n o p ] , [ refl ] |
| 182 | + |
| 183 | + -- The difference is that now we have our basic lemma, the complex proof |
| 184 | + -- can work purely in terms of `Factor` trees. In particular, |
| 185 | + -- `Factor ? ? ?` now does unify with `Factor m no p`, so we don't have to |
| 186 | + -- give `no` explicitly again. |
| 187 | + |
| 188 | + test : ∀ {m n o p q} → |
| 189 | + (∃₂ λ no nop → Factor m nop q × Factor nop no p × Factor no n o) → |
| 190 | + (∃₂ λ pq opq → Factor m n opq × Factor opq o pq × Factor pq p q) |
| 191 | + test (_ , _ , fm , fnop , fno) = |
| 192 | + let _ , fm , fpq = assoc-→ (_ , fm , fnop) in |
| 193 | + let _ , fm , fopq = assoc-→ (_ , fm , fno) in |
| 194 | + _ , _ , fm , fopq , fpq |
0 commit comments