Agda 证明中的替代项

Question

我是 Agda 的初学者，我在这里的证明中遇到了一个漏洞：

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))
  ∎

我只需要证明给定 ccw/cw 假设， ccw (cw (cw (cw (cw t)))) ≡ cw (cw (cw t))

Answer 1

找到了：我需要把它放进洞里：(ccw/cw ( cw ( cw ( cw t))))

产生这个：ccw (cw ( cw ( cw ( cw t)))) ≡ ( cw ( cw ( cw t))),

基本上用 ( cw ( cw ( cw t)))

替换 t

Agda 证明中的替代项

Substitute terms in Agda proofs

agda