Substitute terms in Agda proofs

Question

I'm a beginner with Agda and im stuck with a hole in my proof here:

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym; subst; trans)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

data Tile : Set where

-- 90° rotation
postulate cw : Tile → Tile
-- -90° rotation
postulate ccw : Tile → Tile

postulate cw/cw/cw/cw : ∀ (t : Tile) → cw (cw (cw (cw t))) ≡ t
postulate ccw/cw : ∀ (t : Tile) → ccw (cw t) ≡ t
postulate cw/ccw : ∀ (t : Tile) → cw (ccw t) ≡ t

cw/cw/cw/ccw : ∀ (t : Tile) → ccw t ≡ cw (cw (cw t))
cw/cw/cw/ccw t =
  begin
    ccw t
  ≡⟨ cong ccw ( sym (cw/cw/cw/cw t)) ⟩
    ccw ( cw ( cw ( cw ( cw t))))
  ≡⟨ {!!} ⟩
    cw (cw (cw t))
  ∎

I simply need to show that given the ccw/cw postulation, ccw (cw (cw (cw (cw t)))) ≡ cw (cw (cw t))

Farzad Bekran Farzad Bekran · Accepted Answer · 2021-08-08T07:14:44

Found it: I needed to put this in the hole: (ccw/cw ( cw ( cw ( cw t))))

which produces this: ccw (cw ( cw ( cw ( cw t)))) ≡ ( cw ( cw ( cw t))),

essentially replacing t with ( cw ( cw ( cw t)))

Substitute terms in Agda proofs

1 Answers