결정할 수있는 평등을 포함하는 증명

나는 결정할 수있는 평등을 사용하는 함수에 대해 간단한 것을 증명하려고합니다. 여기에 훨씬 단순화 된 예입니다 : 이제결정할 수있는 평등을 포함하는 증명

open import Relation.Nullary 
open import Relation.Binary 
open import Relation.Binary.PropositionalEquality 

module Foo {c} {ℓ} (ds : DecSetoid c ℓ) where 

open DecSetoid ds hiding (refl) 

data Result : Set where 
    something something-else : Result 

check : Carrier → Carrier → Result 
check x y with x ≟ y 
... | yes _ = something 
... | no _ = something-else

, 나는 이미 _≟_의 양쪽이 동일하다는 것을 보여준 곳이 뭔가를 증명하기 위해 노력하고있어.

check-same : ∀ x → check x x ≡ something 
check-same x = {!!}

이 시점에서 현재 목표는 (check ds x x | x ≟ x) ≡ something입니다. x ≟ x가 자체라면, 나는 refl 같은 것을 사용하여 그것을 해결 것이지만,이 상황에서 최선은이 같은 뭔가 가지고 올 수 :

check-same x with x ≟ x 
... | yes p = refl 
... | no ¬p with ¬p (DecSetoid.refl ds) 
... |()

자체에 의해이 나쁜 것이 아니라 큰 증거의 한가운데서 그것은 엉망입니다. 분명히 이것을하기위한 더 좋은 방법이 있어야만합니까?

출처

2012-10-27 hammar

내 증거를 단순화하기 위해 rewrite와 함께 사용할 수있는이 보조 정리

≟-refl : ∀ x → ⌊ x ≟ x ⌋ ≡ true ≟-refl x with x ≟ x ... | yes p = refl ... | no ¬p = ⊥-elim (¬p (DecSetoid.refl ds))

쓰기 허용

, 난 그냥 좋겠 'Data.Empty'에서'⊥-elim'을 사용하십시오 :'no ¬p = ⊥-elim (¬p (DecSetoid.refl ds))'. – copumpkin

@copumpkin : 고마워, 적어도 엉망진창은 없애 버린다. – hammar

예제에서와 같이 내 함수가 x ≟ y이 반환 한 증명 개체를 신경 쓰지 않아서 부울을 반환하는 ⌊ x ≟ y ⌋으로 바꿀 수있었습니다. 제가 다음 대신 터무니 패턴 블록으로 중첩 사용

check-same x rewrite ≟-refl x = refl

출처

2012-10-28 20:06:41 hammar

결정할 수있는 평등을 포함하는 증명

답변

관련 문제