Congruence Rule with Heterogeneous Equality in Agda

Congruence rule plays an important role in reasoning in Agda, and things become mystery as working under heterogeneous equality. In the standard library of Agda2, the type of Relation.Binary.HeterogeneousEquality.cong is

∀{a b} (f : a → b) {i : a} {j : a} → i ≅ j → f i ≅ f j

Since i and j are the same type, the equality between i and j becomes propositional instead of heterogeneous.

View for (mod n)

延續上一個 Bound View, 稍微修改之後, 再配合 結構, 可以得到一個對 的模數 n 的 view。首先修改 Bound 為

data Bound (k : ℕ) : ℕ → Set where
below : (n : ℕ) → (l : ℕ) → (l+n=k : l + (suc n) ≡ k)
　　　　→ Bound k n
above : (n : ℕ) → (l : ℕ) → (l+k=n : l + k ≡ n) → Bound k n

亦即將 below 的條件改為 ，而 above 則是 。toBound 根據此稍作修改。接下來是 的結構定義，因為要作成 的 view，index 上放入自然數。

data Z (k : ℕ) : ℕ → Set where
　cl : (m : ℕ){m<k : (suc m) ≤ k} (n : ℕ) → Z k (m + (n * k))

接下來就是將自然數轉成 ：

Data.Vec.Equality …

後來還是把改過的東西丟上去了 …現在 Vec 也有 decidable equality 可以用, 加上最近 Agda 上把 DecSetoid 都補上去, 大部分內建的 data structure 都能夠拿來比較相等了？連整數也有大小比較 ..

最近試著從 commutative monoid 構造 abelian group, …

快瘋了

想證明 pop 跟 push 對於 queue 的操作而言, 會保持等式, 也就是 (即 ), 而對於同樣的 queue, pop 跟 push 必須產生同樣的結果, 而不管用什麼樣的表示。

但光是把 case split 出來, 就一堆東西了, 到底要怎麼寫啊, 不是這樣的吧 囧

Decidable setoid in Agda

If you have known setoid in Agda, the decidable setoid may be quite easy to understand. We first explain (I hope so …) what is decidable relation. A decidable relation is defined as follows in Agda,

Setoids in Agda

Setoid is a record type in Agda, and it appears everywhere from Relation.Binary.EqReasoning to Algebra. But, why do we need such a type ? After reading “setoids in type theory”, I thought that setoids are used for mathematical constructions like subset, quotients in the intensional type theory and the Calculus of Inductive Construction. Since some of functional data structure could be represented as such constructions, it also may be useful for functional programming, at least for understanding it.