Доказательство, если n = m и m = o, тогда n + m = m + o в Идрисе? - PullRequest
Новая
       26

Доказательство, если n = m и m = o, тогда n + m = m + o в Идрисе?

0 голосов
/ 26 мая 2018

Я пытаюсь улучшить свой навык Idris, взглянув на некоторые из упражнений Основы программного обеспечения (изначально для Coq, но я надеюсь, что перевод на Idris будет не слишком плохим).У меня проблемы с "Упражнение: 1 звезда (plus_id_exercise)" , которое гласит:

Удалить "Допущено".и заполните доказательство. 

Theorem plus_id_exercise : ∀ n m o : nat,
  n = m → m = o → n + m = m + o.
Proof.
  (* FILL IN HERE *) Admitted.

Я перевел на следующую проблему в Idris: 

plusIdExercise : (n : Nat) ->
                 (m : Nat) ->
                 (o : Nat) ->
                 (n == m) = True ->
                 (m == o) = True ->
                 (n + m == m + o) = True

Я пытаюсь выполнить анализ каждого случая, и яиметь много проблем.Первый случай: 

plusIdExercise Z Z Z n_eq_m n_eq_o = Refl

, кажется, работает, но затем я хочу сказать, например: 

plusIdExercise (S n) Z Z n_eq_m n_eq_o = absurd

Но это не работает и дает: 

When checking right hand side of plusIdExercise with expected type
        S n + 0 == 0 + 0 = True

Type mismatch between
        t -> a (Type of absurd)
and
        False = True (Expected type)

Specifically:
        Type mismatch between
                \uv => t -> uv
        and
                (=) FalseUnification failure

Я пытаюсь сказать, что этот случай никогда не может произойти, потому что n == m, но Z (= m) никогда не является преемником любого числа (n).Что я могу сделать, чтобы это исправить?Я правильно подхожу к этому?Я несколько смущен.

1 Ответ

0 голосов
/ 26 мая 2018

Я бы сказал, что перевод не совсем корректен.Лемма, изложенная в Coq, не использует логическое равенство на натуральных числах, она использует так называемое пропозициональное равенство.В Coq вы можете попросить систему предоставить вам больше информации о вещах: 

Coq < About "=".
eq : forall A : Type, A -> A -> Prop

Вышеуказанное значение = (это синтаксический сахар для типа eq) принимает два аргумента некоторого типа Aи выдает предложение , а не логическое значение.

Это означает, что прямым переводом будет следующий фрагмент 

plusIdExercise : (n = m) -> (m = o) -> (n + m = m + o)
plusIdExercise Refl Refl = Refl

И при сопоставлении с образцом значенийIdris по существу переписывает термины в соответствии с соответствующим уравнением (это примерно эквивалентно тактике Coq rewrite).

Кстати, вы можете найти Software Foundations в Idris Проект полезен.

...