当'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

我认为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

正如AndrásKovács所说,归纳案例需要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

使用保护模式有时也很有用:

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被重写.