splitAt равноправие в Агде

Как можно доказать это равенство

≡splitAt : {α : Level} {A : Set α} {l₁ l₂ : Nat}
         -> (xs₁ : Vec A l₁)
         -> (xs₂ : Vec A l₂)
         -> (xs₁ , xs₂ , refl) ≡ splitAt l₁ (xs₁ ++ xs₂)

? Базовый случай очевиден

≡splitAt  []       xs₂ = refl

Но потом

≡splitAt (x ∷ xs₁) xs₂

дает

Goal: (x ∷ xs₁ , xs₂ , refl) ≡
      (splitAt (suc .n) (x ∷ xs₁ ++ xs₂)
       | splitAt .n (xs₁ ++ xs₂))

Этот

≡splitAt (x ∷ xs₁) xs₂ with ≡splitAt xs₁ xs₂
... | refl = {!!}

выдает ошибку: «Отказаться в разрешении разнородного ограничения refl ...».

И это

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ with splitAt l₁ (xs₁ ++ xs₂)
...                                  | (xs₁' , xs₂' , refl)

выдает ошибку: «xs₁! = xs₁ 'типа Vec A l₁ ...». Я написал это определение:

++≡++ : {α : Level} {A : Set α} {l₁ l₂ : Nat}
      -> (xs₁ : Vec A l₁)
      -> (xs₂ : Vec A l₂)
      -> (xs₁' : Vec A l₁)
      -> (xs₂' : Vec A l₂)
      -> xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'
++≡++ _ _ _ _ = {!!}

но не знаю, как им пользоваться.

Может быть, есть какой-то источник, откуда я могу узнать больше о выражениях с помощью?

Спасибо.


theorem-proving agda
person user3237465    schedule 01.02.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Хорошее практическое правило при доказательстве чего-либо, связанного с функцией, определенной сопоставлением с образцом (например, здесь splitAt), - использовать в доказательстве те же образцы. Итак, вы на правильном пути, написав

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ with splitAt l₁ (xs₁ ++ xs₂)
...                                  | (xs₁' , xs₂' , e) = ?

Здесь e имеет тип xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'. Agda не знает, как решить это уравнение, поскольку оно содержит функцию _++_, поэтому вы не можете заменить ее на refl. Поэтому вместо этого мы должны немного помочь Агде:

split≡ : {α : Level} {A : Set α} (l₁ : Nat) {l₂ : Nat}
       -> (xs₁ xs₁' : Vec A l₁)
       -> (xs₂ xs₂' : Vec A l₂)
       -> xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'
       -> (xs₁ ≡ xs₁') × (xs₂ ≡ xs₂')

Случай с zero снова прост:

split≡ zero [] [] xs₂ .xs₂ refl = refl , refl

В случае с suc l₁ мы используем cong из стандартной библиотеки, чтобы разделить доказательство равенства e на равенство по головам и одному по хвостам, подавая последнее в рекурсивный вызов split≡:

split≡ (suc l₁) (x ∷ xs₁) (x' ∷ xs₁') xs₂ xs₂' e with cong head e | split≡ l₁ xs₁ xs₁' xs₂ xs₂' (cong tail e)
split≡ (suc l₁) (x ∷ xs₁) (.x ∷ .xs₁) xs₂ .xs₂ e    | refl        | refl , refl = refl , refl

Теперь, когда у нас есть split≡, мы можем вернуться к определению splitAt:

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | xs₁' , xs₂' , e with split≡ l₁ xs₁ xs₁' xs₂ xs₂' e
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | .xs₁ , .xs₂ , e | refl , refl = {!!}

Мы почти у цели: мы знаем, что xs₁ = xs₁' и xs₂ = xs₂', но еще не это e = refl. К сожалению, сопоставление с образцом на e напрямую не работает:

xs₁ != xs₁' of type Vec A l₁
when checking that the pattern refl has type
xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'

Причина в том, что Agda рассматривает шаблоны слева направо, но нам нужен другой порядок здесь. На помощь приходит еще один паттерн with:

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | xs₁' , xs₂' , e with split≡ l₁ xs₁ xs₁' xs₂ xs₂' e | e
≡splitAt {α} {A} {ℕ.suc l₁} (x ∷ xs₁) xs₂ | .xs₁ , .xs₂ , e | refl , refl | refl = refl

Вот мой полный код для справки:

split≡ : {α : Level} {A : Set α} (l₁ : Nat) {l₂ : Nat}
       -> (xs₁ xs₁' : Vec A l₁)
       -> (xs₂ xs₂' : Vec A l₂)
       -> xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'
       -> (xs₁ ≡ xs₁') × (xs₂ ≡ xs₂')
split≡ zero [] [] xs₂ .xs₂ refl = refl , refl
split≡ (suc l₁) (x ∷ xs₁) (x' ∷ xs₁') xs₂ xs₂' e with cong head e | split≡ l₁ xs₁ xs₁' xs₂ xs₂' (cong tail e)
split≡ (suc l₁) (x ∷ xs₁) (.x ∷ .xs₁) xs₂ .xs₂ e | refl | refl , refl = refl , refl

≡splitAt : {α : Level} {A : Set α} {l₁ l₂ : Nat}
         -> (xs₁ : Vec A l₁)
         -> (xs₂ : Vec A l₂)
         -> (xs₁ , xs₂ , refl) ≡ splitAt l₁ (xs₁ ++ xs₂)
≡splitAt [] xs₂ = refl
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ with splitAt l₁ (xs₁ ++ xs₂)
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | xs₁' , xs₂' , e with split≡ l₁ xs₁ xs₁' xs₂ xs₂' e | e
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | .xs₁ , .xs₂ , e | refl , refl | refl = refl

Возможно, есть более простой способ доказать это, но это лучшее, что я мог придумать.

Что касается вашего вопроса, как узнать больше о шаблонах с помощью, лучший способ научиться - это много писать самостоятельно (по крайней мере, так я узнал). Не забудьте позволить Agda помочь вам в различении регистра (используя C-c C-c в Emacs).

person Jesper    schedule 02.02.2014