我试图证明一些简单的事情:
open import Data.List
open import Data.Nat
open import Data.Bool
open import Data.Bool.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Unit
repeat : ∀ {a} {A : Set a} → ℕ → A → List A
repeat zero x = []
repeat (suc n) x = x ∷ repeat n x
filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
filter p (repeat n x) ≡ repeat n x
我想证明
filter-repeat
通过 p x
上的模式匹配将很容易:filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x
filter-repeat p x () (suc n) | false
filter-repeat p x prf (suc n) | true = cong (_∷_ x) (filter-repeat p x prf n)
然而,这提示
prf : ⊤
不是 T (p x)
类型.所以我想,好吧,这似乎是一个熟悉的问题,让我们抽出inspect
:filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x | inspect p x
filter-repeat p x () (suc n) | false | _
filter-repeat p x tt (suc n) | true | [ eq ] rewrite eq = cong (_∷_ x) (filter-repeat p x {!!} n)
但尽管
rewrite
,孔的类型仍然是T (p x)
而不是 T true
.这是为什么?如何将其类型减少到 T true
所以我可以用 tt
填充它?解决方法
我可以通过使用
T-≡
来解决它:open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x | inspect p x
filter-repeat p x () (suc n) | false | _
filter-repeat p x tt (suc n) | true | [ eq ] = cong (_∷_ x) (filter-repeat p x (Equivalence.from T-≡ ⟨$⟩ eq) n)
但我仍然想了解为什么
inspect
基于 - 的解决方案不起作用。
最佳答案
如安德拉斯·科瓦奇 说归纳案例需要prf
为 T (p x)
类型虽然您已经将其更改为 ⊤
通过 p x
上的模式匹配.一个简单的解决方案就是调用filter-repeat
在 p x
上的模式匹配之前递归:
open import Data.Empty
filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf 0 = refl
filter-repeat p x prf (suc n) with filter-repeat p x prf n | p x
... | r | true = cong (x ∷_) r
... | r | false = ⊥-elim prf
有时也可以使用 the protect pattern :
data Protect {a} {A : Set a} : A → Set where
protect : ∀ x → Protect x
filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
filter p (repeat n x) ≡ repeat n x
filter-repeat p x q 0 = refl
filter-repeat p x q (suc n) with protect q | p x | inspect p x
... | _ | true | [ _ ] = cong (x ∷_) (filter-repeat p x q n)
... | _ | false | [ r ] = ⊥-elim (subst T r q)
protect q
保存 q
的类型不会被重写,但这也意味着在 false
案例 q
的类型仍然是 T (p x)
而不是 ⊥
,因此额外的 inspect
.相同想法的另一个变体是
module _ {a} {A : Set a} (p : A → Bool) (x : A) (prf : T (p x)) where
filter-repeat : ∀ n → filter p (repeat n x) ≡ repeat n x
filter-repeat 0 = refl
filter-repeat (suc n) with p x | inspect p x
... | true | [ r ] = cong (x ∷_) (filter-repeat n)
... | false | [ r ] = ⊥-elim (subst T r prf)
module _ ... (prf : T (p x)) where
阻止 prf
的类型从被重写为好。
关于boolean - 当 `T b` 已经匹配时证明 `b`,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36500605/