涉及可判决平等的证明

我想证明一些使用可判决平等的函数的一些简单事情。这里是一个大大简化例如：涉及可判决平等的证明

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

，而不是使用嵌套块荒唐的模式，我只是使用'Data.Empty'中的'⊥-elim'：'no¬p=⊥-elim（¬p（DecSetoid.refl ds））''。 – copumpkin

@copumpkin：谢谢，至少摆脱了一些混乱。 – hammar

由于我的功能与示例中的功能一样，并不在意x ≟ y返回的证明对象，所以我可以用⌊ x ≟ y ⌋替换它返回布尔值。

，让我写这个引理

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

，我可以再与rewrite使用我的证明简化为

check-same x rewrite ≟-refl x = refl

来源

2012-10-28 20:06:41 hammar

涉及可判决平等的证明

回答

相关问题