minh 'T b` khi `b` đã được kết hợp trên

Question

Tôi cố gắng để chứng minh một cái gì đó đơn giản:

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 

Tôi nghĩ minh filter-repeat sẽ là dễ dàng bằng cách mô hình kết hợp trên 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) 

Tuy nhiên, điều này phàn nàn rằng prf : ⊤ không thuộc loại T (p x). Vì vậy, tôi nghĩ, OK, điều này có vẻ như một vấn đề quen thuộc, chúng ta hãy whip ra 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) 

nhưng bất chấp sự rewrite, loại lỗ vẫn là T (p x) thay vì T true. Tại sao vậy? Tôi làm cách nào để giảm loại của mình thành T true để tôi có thể điền vào số tt?

Cách giải quyết

tôi đã có thể làm việc xung quanh nó bằng cách sử dụng 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) 

nhưng tôi vẫn muốn hiểu tại sao các giải pháp dựa trên inspect không hoạt động.

Answer 1

Như András Kovács nói trường hợp quy nạp đòi hỏi prf là loại T (p x) khi bạn đã thay đổi nó chỉ với ⊤ theo mẫu phù hợp trên p x. Một giải pháp đơn giản là chỉ để gọi filter-repeat đệ quy trước khi mô hình kết hợp trên 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 

Nó cũng đôi khi có thể hữu ích để sử dụng 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 tiết kiệm các loại q từ được viết lại, nhưng điều này cũng có nghĩa là trong trường hợp false, loại q vẫn là T (p x) thay vì ⊥, do đó bổ sung inspect.

Một biến thể của ý tưởng tương tự là

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 ngăn chặn các loại prf từ được viết lại là tốt.

Answer 2

Kết hợp mẫu phụ thuộc chỉ ảnh hưởng đến mục tiêu và ngữ cảnh tại thời điểm sử dụng chính xác. Kết hợp trên p x ghi đè ngữ cảnh hiện tại và giảm loại prf thành ⊤ trong chi nhánh true.

Tuy nhiên, khi bạn thực hiện đệ quy filter-repeat cuộc gọi, bạn lại một lần nữa cung cấp x như là đối số đó, và T (p x) trong filter-repeat phụ thuộc vào rằngx, không phải là người cũ trong bối cảnh bên ngoài, mặc dù họ đang definitionally bằng . Chúng tôi có thể đã thông qua một cái gì đó khác hơn là x, theo giả thuyết, vì vậy không có giả định nào có thể được thực hiện về nó trước cuộc gọi filter-repeat.

x thể được thực hiện bất biến trong bối cảnh của Sacombank nó ra từ cảm ứng:

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)