Перепишите только некоторые части доказательства? (a = S b) и (b = c) => (a = S c) - PullRequest
Новая
       11

Перепишите только некоторые части доказательства? (a = S b) и (b = c) => (a = S c)

0 голосов
/ 01 октября 2019

Я пытаюсь реализовать функцию в Idris, которая показывает, что m - n + n = m, если m >= n. На данный момент у меня есть: 

total
minusPlus : {n : Nat} -> {m : Nat} -> (prf : LTE m n) -> n - m + m = n
minusPlus {n = Z}     {m = Z}     prf = Refl
minusPlus {n = Z}     {m = (S k)} prf   impossible
minusPlus {n = (S k)} {m = Z}     prf = rewrite plusZeroRightNeutral k in Refl
minusPlus {n = (S k)} {m = (S j)} prf =
  let mp = minusPlus (fromLteSucc prf)
      rsps = sym (plusSuccRightSucc (minus k j) j)
  in ?hole

Для отверстия есть следующая информация о типе: 

        k : Nat
        j : Nat
      prf : LTE (S j) (S k)
       mp : plus (minus k j) j = k
     rsps : plus (minus k j) (S j) = S (plus (minus k j) j)
--------------------------------------
Main.hole : plus (minus k j) (S j) = S k

Я думаю, что нужно уметь рассуждать, что из-за plus (minus k j) j = k (тп)и plus (minus k j) (S j) = S (plus (minus k j) j) (rsps) следует, что plus (minus k j) (S j) = S k (Main.hole), заменив k на plus (minus k j) j в Main.hole с правой стороны. Когда я попытался заменить отверстие на rewrite sym mp in rsps, я получил следующую ошибку 

 When checking right hand side of minusPlus with expected type
         S k - S j + S j = S k

 When checking an application of function rewrite__impl:
         Type mismatch between
                 minus k j + S j = S (minus k j + j) (Type of rsps)
         and
                 (\replaced => plus (minus replaced j) (S j) = S replaced) (k -
                                                                            j +
                                                                            j) (Expected type)

         Specifically:
                 Type mismatch between
                         plus (minus k j) (S j)
                 and
                         plus (minus (plus (minus k j) j) j) (S j)

Означает ли это, что k был заменен на правой стороне (что я и хотел), но также на левойстороны (что я предполагаю, это проблема)? Есть ли способ сделать это правильно или другой способ реализовать нужную мне функцию?

(Смежный вопрос: мне нужно / нужно ли иметь строку impossible или есть способ ее избежать? )

...