AGDA는 <a href="https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Base.agda" rel="nofollow noreferrer">the standard library</a>에서 <code>ℕ</code> 및 <code>_≟_</code>를 사용하여 목표 유형

Question

의 발현을 감소 만들기, 나는

open import Data.Nat 
open import Relation.Binary.PropositionalEquality 
open import Relation.Nullary 

foo : ℕ -> ℕ -> ℕ 
foo x y with x ≟ y 
foo x .x | yes refl = x 
foo x y | no contra = y 

data Bar : ℕ -> Set where 
    bar : (x : ℕ) -> Bar (foo x x) 

내가

mkBar : (x : ℕ) -> Bar x 
mkBar x = bar x 

AGDA 불평,

Type mismatch: 
expected: x 
    actual: foo x x | x ≟ x 
when checking that the expression bar x 
has type Bar x 

이 구현하고자하는이 나에게 이해가된다 : Agda는 모른다 선험적으로은 x ≟ x으로 항상 yes refl으로 평가되므로 x에 대해 조금 더 알기 전까지는 foo x x을 평가하지 않을 것입니다.

그래서 나는 yes refl에

eq-refl : forall x -> (x ≟ x) ≡ yes refl 
eq-refl x with x ≟ x 
eq-refl x | yes refl = refl 
eq-refl x | no contra = ⊥-elim (contra refl) 

mkBar : (x : ℕ) -> Bar x 
mkBar x rewrite eq-refl x = bar x 

를 해결하기 위해 x ≟ x을 강제로 목표를 재 작성 시도했지만 아무 소용. 같은 오류 메시지. 또한 foo x x ≡ x에 의해 재 작성 시도 :

foo-eq : forall x -> foo x x ≡ x 
foo-eq x rewrite eq-refl x = refl 

mkBar : (x : ℕ) -> Bar x 
mkBar x rewrite foo-eq x = bar x 

This answer 제안 mkBar의 왼쪽에 x ≟ x에 일치하지만, 또한 아무런 영향이없는 것으로 보인다 패턴 :

mkBar : (x : ℕ) -> Bar x 
mkBar x with x ≟ x 
mkBar x | yes refl = bar x 
mkBar x | no contra = ⊥-elim (contra refl) 

내가 트릭을 누락해야합니다 이리. 목표 유형에서 |을 제거하고 foo x x을 x으로 줄이려면 어떻게해야합니까? (나는 mkBar의 LHS에 직접 x을 검사하지 않으려는 것입니다.)

Answer 1

당신 거의 있었다 : 주목해야 할 중요한 것은 rewrite가 x ≡ y 소요 목표에 y에 의해 x을 대체한다는 것이다. foo-eq x 유형은 foo x x ≡ x이지만 목표를 대체 할 foo x x은 없습니다!

mkBar : (x : ℕ) → Bar x 
mkBar x rewrite sym (foo-eq x) = bar x 

Bar x 다음이된다 Bar (foo x x)을 당신이 당신의 생성자를 적용 할 수 있습니다 의미 : 당신이해야 할 일은

은과 같이 sym (foo-eq x)에 의해 재 작성합니다.