Agda中如何定义观测相等

Question

假设我有一个呈现函数：

rasterize : ℕ → ℕ → Tile → List (List Color

我需要证明这一说法：

如果rasterize w h t1 = rasterize w h t2那么t1 ≡ t2

换句话说，如果t1和t2在相同的宽度和高度下呈现相同的值，那么它们是相等的。

我不知道如何在agda中这样说，我想出了以下几点：

obs-eq : ∀ (t₁ t₂ : Tile) (w h : ℕ) →
  rasterize w h t₁ ≡ rasterize w h t₂ → t₁ ≡ t₂

但我怀疑这不是我的意思，通过谷歌搜索，我认为我需要定义一个操作符来比较呈现的值？也涉及某种西格玛型？

Answer 1

你的括号是错误的:当你写

obs-eq : 
  ∀ (t₁ t₂ : Tile) (w h : ℕ) →
  rasterize w h t₁ ≡ rasterize w h t₂ → 
  t₁ ≡ t₂

这意味着，如果我给你任何两个和任何两个维度，这样，瓷砖在这些维度上就会变成相同的图片，那么你就可以证明它们是相等的。

如果我为你选择w = 0和h = 0会发生什么.

但是你想要说的是，如果我给你两个瓷砖，一个证明，对于任何两个维度，它们都是一幅图片，那么你可以证明这些瓷砖是相等的：

obs-eq : 
  ∀ (t₁ t₂ : Tile) →
  (∀ w h → rasterize w h t₁ ≡ rasterize w h t₂) → 
  t₁ ≡ t₂