boolean - 当 `T b` 已经匹配时证明 `b`

Question

我试图证明一些简单的事情:

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基于 - 的解决方案不起作用。

Answer 1

如安德拉斯·科瓦奇 说归纳案例需要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 的类型从被重写为好。