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

Предположим, мы хотели бы иметь «правильный» minus для Nats, требуя 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

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

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


dependent-type idris
person 0xd34df00d    schedule 27.02.2019    source источник
comment
Может быть, вы можете включить свое доказательство для plusTossS, чтобы люди могли лучше воспроизвести ваш код.   -  person Niko    schedule 28.02.2019
comment
Вероятно, вам нужно сделать что-то умное с доказательствами: ```minusPlusTossS n m Z {prf1 = LTEZero} {prf2 = LTEZero} = let tossPrf = plusTossS n m in rewrite tossPrf in Refl ```проверки типов, но не тотальные.   -  person Markus    schedule 28.02.2019
comment
@Markus Я думаю, это связано с тем, что средство проверки типов не может сопоставить k `LTE` n + S m с доступной формой для LTESucc. Конечно, мы могли бы переписать это доказательство в виде k `LTE` S (n + m), но мне это не особо помогло.   -  person 0xd34df00d    schedule 28.02.2019

Ответы (1)


arrow_upward
2
arrow_downward

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

Итак, у нас есть доказательство того, что два уменьшаемых числа 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
person 0xd34df00d    schedule 28.02.2019