How to define observational equality in Agda

Question

Let's say I have a render function:

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

I need to prove this statement:

if rasterize w h t1 = rasterize w h t2 then t1 ≡ t2

in other words if t1 and t2 render to the same value given the same width and height, then they are equal.

I dont know how to say this in agda, I came up with the following:

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

but I suspect this is not what I mean and from googling around I think I need to define an operator that compares the rendered values? Also some kind of sigma type is involved?

Answer 1

Your parenthesization is wrong: when you write

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

it means that if I give you any two tiles and any two dimensions, such that the tiles rasterize to the same picture at those dimensions, then you can prove that they are equal.

Consider what happens if I choose w = 0 and h = 0 for you...

But what you want to say is that if I give you any two tiles, and a proof that for any two dimensions they rasterize to the same picture, then you can prove that the tiles are equal:

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