Доказательство равенства типов в зависимости от (дальнейших) доказательств - PullRequest
Новая
       45

Доказательство равенства типов в зависимости от (дальнейших) доказательств

0 голосов
/ 27 февраля 2019

Предположим, мы хотели бы иметь "правильные" minus на Nat с, требующие m <= n для n `minus` m, чтобы иметь смысл: 

%hide minus

minus : (n, m : Nat) -> { auto prf : m `LTE` n } -> Nat
minus { prf = LTEZero } n Z = n
minus { prf = LTESucc prevPrf } (S n) (S m) = minus n m

Теперь давайте попробуем доказатьследующая лемма о том, что (n + (1 + m)) - k = ((1 + n) + m) - k, при условии, что обе стороны верны: 

minusPlusTossS : (n, m, k : Nat) ->
                 { auto prf1 : k `LTE` n + S m } ->
                 { auto prf2 : k `LTE` S n + m } ->
                 minus (n + S m) k = minus (S n + m) k

Цель предполагает, что может помочь следующая сублемма: 

plusTossS : (n, m : Nat) -> n + S m = S n + m
plusTossS Z m = Refl
plusTossS (S n) m = cong $ plusTossS n m

, поэтому мы пытаемся использовать ее: 

minusPlusTossS n m k =
  let tossPrf = plusTossS n m
  in rewrite tossPrf in ?rhs

И здесь мы терпим неудачу: 

When checking right hand side of minusPlusTossS with expected type
        minus (n + S m) k = minus (S n + m) k

When checking argument prf to function Main.minus:
        Type mismatch between
                LTE k (S n + m) (Type of prf2)
        and
                LTE k replaced (Expected type)

        Specifically:
                Type mismatch between
                        S (plus n m)
                and
                        replaced

Если я правильно понимаю эту ошибку, это просто означает, что она пытается переписать RHS целевого равенства (то есть minus { prf = prf2 } (S n + m) k)до minus { prf = prf2 } (n + S m) k и не удается.Правильно, конечно, поскольку prf является доказательством другого неравенства!И хотя replace может быть использовано для создания доказательства (S n + m) k (или prf1 также сработает), не похоже, что можно одновременно перезаписать и изменить объект доказательства так, чтобы он соответствовал перезаписи.

Как мне обойти это?Или, в более общем смысле, как мне доказать эту лемму?

1 Ответ

0 голосов
/ 28 февраля 2019

Хорошо, наверное, я решил это.Итог: если вы не знаете, что делать, сделайте лемму!

Итак, у нас есть доказательство того, что два минунда n1, n2 равны, и нам нужно получить доказательство n1 `minus` m = n2 `minus` m.Давайте запишем это! 

minusReflLeft : { n1, n2, m : Nat } -> (prf : n1 = n2) -> (prf_n1 : m `LTE` n1) -> (prf_n2 : m `LTE` n2) -> n1 `minus` m = n2 `minus` m
minusReflLeft Refl LTEZero LTEZero = Refl
minusReflLeft Refl (LTESucc prev1) (LTESucc prev2) = minusReflLeft Refl prev1 prev2

Мне даже больше не нужно plusTossS, которое можно заменить на более применимую лемму: 

plusRightS : (n, m : Nat) -> n + S m = S (n + m)
plusRightS Z m = Refl
plusRightS (S n) m = cong $ plusRightS n m

После этого оригиналчеловек становится тривиальным: 

minusPlusTossS : (n, m, k : Nat) ->
                 { auto prf1 : k `LTE` n + S m } ->
                 { auto prf2 : k `LTE` S n + m } ->
                 minus (n + S m) k = minus (S n + m) k
minusPlusTossS {prf1} {prf2} n m k = minusReflLeft (plusRightS n m) prf1 prf2
...