Как показать инъективность функции? - PullRequest
Новая
       17

Как показать инъективность функции?

0 голосов
/ 11 января 2020

Вот что я пытаюсь доказать: Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.

+ - это обозначение plus, определенное как https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html: 

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O ⇒ m
    | S n' ⇒ S (plus n' m)
  end.

В Агде можно сделать cong (n + _), чтобы использовать тот факт, что n + m = n + p для любого нм р.

Встроенные тактики Coq injection и congruence оба казались многообещающими, но они работает только для конструкторов.

Я попробовал следующую стратегию и продолжал сталкиваться со странными ошибками или застревать:

  • сделать индуктивный тип для связывания доказательства (n + m = s): сумма (nms)

  • используйте congruence tacti c в лемме, которая показывает Sum (n m s) = Sum (n p s)

  • используйте конструкции Sum s, destruct и лемму, чтобы показать, что n + m = n + p

Есть ли более простой способ доказать это? Я чувствую, что, должно быть, есть какие-то встроенные тактики c Я пропускаю или какая-то хитрость с unfold.

ОБНОВЛЕНИЕ

Получил: 

Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.
Proof.
  intros. induction n.
  - exact H.
  - apply IHn.  (* goal: n + m = n + p *)
    simpl in H. (* H: S (n + m) = S (n + p) *)
    congruence.
Qed.

Спасибо @ ejgalle go

1 Ответ

2 голосов
/ 11 января 2020

Инъективность plus не является «элементарным» утверждением, учитывая, что функция plus может быть произвольной (и неинъективной)

Я бы сказал, что стандартное доказательство требует induction на левом аргументе, действительно с использованием этого метода, доказательство быстро следует.

Вам понадобится injection, когда вы достигнете цели вида S (n + m) = S (n + p), чтобы получить внутреннее равенство.

...