1

假设我有一个渲染功能：

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₂

但我怀疑这不是我的意思，通过谷歌搜索我认为我需要定义一个比较渲染值的运算符？还涉及某种 sigma 类型？

4

1 回答 1

4

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

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₂
于 2021-08-10T02:38:19.687 回答