当 `b` 已经匹配时证明 `T 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

我认为通过 p x 上的模式匹配可以很容易地证明 filter-repeat:

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

依赖模式匹配只会影响使用它们的确切位置的目标和上下文。在 p x 上匹配会重写当前上下文并将 prf 的类型减少到 true 分支中的 ⊤。

但是，当您执行递归 filter-repeat 调用时，您再次提供 x 作为参数，并且 filter-repeat 中的 T (p x) 取决于 that x，而不是外部上下文中的旧版本，即使它们在定义上是相等的。假设我们可以传递除 x 之外的其他内容，因此在 filter-repeat 调用之前无法对其做出任何假设。

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 = go where
  go : ∀ n → filter p (repeat n x) ≡ repeat n x
  go zero    = refl
  go (suc n) with p x | inspect p x
  go (suc n) | true  | [ eq ] = cong (_∷_ x) (go n)
  go (suc n) | false | [ eq ] = ⊥-elim (subst T eq prf)

Answer 2

正如 András Kovács 所说，归纳案例要求 prf 为 T (p x) 类型，而您已经将其更改为 ⊤ 通过 p x 上的模式匹配。一种简单的解决方案是在 p x:

上进行模式匹配之前递归调用 filter-repeat

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 的类型被重写。

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

Proving `T b` when `b` is already matched on

boolean

inspect

agda