Простые доказательства равенства в списках в idris (доказательство xs++[x]=ys++[y]->x=y->xs=ys)

Я изучаю idris и очень заинтересован в доказательстве свойств списков.

Если вы посмотрите на стандартная библиотека, есть доказательство того, что "Два списка равны, если их головы и хвосты равны".

consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x = y -> xs = ys -> x :: xs = y :: ys
consCong2 Refl Refl = Refl

Мы также можем доказать другое направление

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x::xs = y::ys -> x = y -> xs = ys
consCong2' Refl Refl = Refl

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

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x::xs = y::ys -> x = y -> xs = ys
consCong2' prf_cons Refl = (cong {f = drop 1} prf_cons)

Было бы интересно посмотреть, можно ли доказать эти свойства также для последнего элемента в остальных и всего, что было до него. Доказать «Два списка равны, если равны первая часть и самый последний элемент» оказалось очень просто

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
x = y -> xs = ys -> xs ++ [x] = ys ++ [y]
consCong2' Refl Refl = Refl

Но в другом направлении проверка типа не проходит:

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' Refl Refl = Refl

Так как

Type mismatch between
                         ys ++ [x]
                 and
                         xs ++ [x]

Очевидно, потому что если xs ++ [x] = ys ++ [y] будет первым в выводе, Идрис не сможет объединить обе стороны.

Так что все, что нам нужно сделать, это сказать idris применить init к обеим частям уравнения, как мы сделали раньше с drop 1. Это не удается, потому что init требует доказательства того, что список не пуст, что каким-то образом не может быть здесь неявно выведено. Поэтому для этого я написал вспомогательную функцию, которая явно определяет (a ++ [x]) = a.

dropOneRight :  (xs : List a) -> List a
dropOneRight xs with (snocList xs)
  dropOneRight [] | Empty = []
  dropOneRight (a ++ [x]) | Snoc rec = a

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' prf_cons Refl = cong {f = dropOneRight} prf_cons

Но это дает

Type mismatch between
                 dropOneRight (ys ++ [x])
         and
                 ys

Я трачу некоторое время на другие подходы, разделяя регистр с помощью snocList, но не могу добиться заметного прогресса. Я не понимаю, как я могу показать Идрису, что dropOneRight (ys ++ [x]) = ys. Как я могу доказать xs ++ [x] = ys ++ [y] -> x = y -> xs = ys?


dependent-type theorem-proving idris
person Falco Winkler    schedule 11.09.2019    source источник
comment
Когда вы пишете, мы также можем доказать другое направление, ваш тип результата должен быть действительно парой доказательств того, что x = y и xs = ys.   -  person gallais    schedule 12.09.2019
comment
Да! Вы правы, спасибо, что указали на это.   -  person Falco Winkler    schedule 12.09.2019

Ответы (1)


arrow_upward
1
arrow_downward

Я предполагаю, что подход snocList будет сложным; по крайней мере, с простой стратегией доказательства, чтобы следовать определению. Чтобы доказать ys = dropOneRight (ys ++ [x]), объединение snocList (ys ++ [x]) с аргументами вызовет проблемы, грубо говоря:

prf' : (ys : List a) -> (x : a) -> ys = dropOneRight (ys ++ [x])
prf' ys x with (snocList (ys ++ [x]))
    ...
    prf' ?? x | Snoc rec = ?hole

Если вы позволите dropOneRight быть проще, это будет довольно прямолинейно:

dropOneRight : (xs : List a) -> List a
dropOneRight [] = []
dropOneRight [x] = []
dropOneRight (x :: y :: xs) = x :: dropOneRight (y :: xs)

dropPrf : (ys : List a) -> (x : a) -> ys = dropOneRight (ys ++ [x])
dropPrf [] z = Refl
dropPrf [x] z = Refl
dropPrf (x :: y :: xs) z = cong $ dropPrf (y::xs) z

consCong2' : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
             xs ++ [x] = ys ++ [y] -> x = y -> xs = ys
consCong2' {xs} {ys} {x} prf_cons Refl = 
  rewrite dropPrf ys x in rewrite dropPrf xs x in
  cong prf_cons
person xash    schedule 12.09.2019