问Agda证明中的替代项
EN

Stack Overflow用户

提问于 2021-08-07 13:55:46

回答 1查看 52关注 0票数 1

我是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))

agda

回答 1

Stack Overflow用户

回答已采纳

发布于 2021-08-08 07:14:44

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

它会产生这样的结果：ccw (cw ( cw ( cw ( cw t)))) ≡ ( cw ( cw ( cw t)))

用( cw ( cw ( cw t)))实质上取代了t

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/68692993

复制

相似问题

问Agda证明中的替代项
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Agda证明中的替代项EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Agda证明中的替代项
EN