splitAt равенство в Agda

Question

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

≡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₂' 
++≡++ _ _ _ _ = {!!} 

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

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

Спасибо.

Answer 1

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

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

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

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 из стандартной библиотеки, чтобы разделить равенство доказательства е в равенство на головы и один на хвостах, подавая последний в рекурсивный вызов 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 рассматривает образцы слева направо, но мы хотим, чтобы другой порядок здесь.Другой с-модель приходит на помощь:

≡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).