Доказательство теорем в Coq

Фон

Я обучаю помощи, Coq, самостоятельно. До сих пор я закончил читать Coq Ива Берто в спешке . Теперь моя цель состоит в том, чтобы доказать некоторые базовые результаты, касающиеся натуральных чисел, что завершается так называемым алгоритмом деления. Однако я столкнулся с некоторыми препятствиями на пути к этой цели. В частности, два следующих результата доказали (каламбур), что было труднее доказать в Coq, чем я первоначально представлял. На самом деле, после многих бесплодных попыток я прибегаю к тому, чтобы доказать их вручную (как показано ниже). Это явно не помогает мне стать более опытным в обращении с Coq; вот почему я перехожу на этот форум. Я надеюсь, что кто-то на этом сайте может и хочетчтобы помочь мне перевести мои доказательства ниже в доказательство, которое принимает Coq. Вся помощь искренне ценится!

Теорема А

Для всех Доказательство: $x,y \in N$

x < S (y) \subset x < y \lor I (N, x, y)

$\begin{equation} x < S(y) \subset x < y \lor \text{I}(N,x,y) \end{equation}$

Предположим, что . Следовательно, существует с Отсюда (Пеано 1b и 3) $x < S(y)$ $z \in N$

\begin{matrix} (*) & I (N, x + S (z), S (y)) \end{matrix}

$\begin{equation} \text{I}(N,x+S(z),S(y)) \tag{*}\end{equation}$

I (N, x + z, y)

$\begin{equation} \text{I}(N,x+z,y) \end{equation}$

Определить предикат

Q (u) := (I (N, x + u, y) \subset x < y \lor I (N, x, y)

$\begin{equation} Q(u):=(\text{I}(N,x+u,y) \subset x<y \lor \text{I}(N,x,y) \end{equation}$

Достаточно показать . Докажем это индукцией по . Чтобы увидеть , а не этат, если имеет место, то верно для Пеано 1a. Таким образом, . Теперь докажем : Предположим, . Из этого определения мы имеем и, следовательно, также в этом случае. Наконец, пятая аксиома Пеано дает и по мы получаем . $Q(z)$ $z$ $Q(0)$ $\text{I}(N,x+0,y)$ $\text{I}(N,x,y)$ $x<y \lor \text{I}(n,x,y)$ $Q(S(v))$ $\text{I}(N,x+S(v),y)$ $x<y$ $x<y \lor \text{I}(N,x,y)$ $Q(z)$ $(*)$ $x < y \lor \text{I}(N,x,y)$

\begin{matrix} (◻) \end{matrix}

$\begin{equation} \tag{$\square$} \end{equation}$

Теорема Б

Для всех Доказательство: $x,y \in N$

x < y \lor I (N, x, y) \lor y < x

$\begin{equation} x <y \lor \text{I}(N,x,y) \lor y<x \end{equation}$

Если то по определению, а если то также по определению. Если и то по транзитивности и рефлексивности имеем , что противоречит. Следовательно, не более одного из утверждений верно. $x<y$ $\neg \text{I}(N,x,y)$ $x>y$ $\neg \text{I}(N,x,y)$ $x>y$ $y>x$ $\text{I}(N,x,y)$

Мы держим фиксированным и индуцируем на . Когда мы имеем для всех , что доказывает базовый случай. Далее, предположим, что теорема верна для ; Теперь мы хотим доказать теорему для . Из трихотомии для есть три случая: и . Если , то ясно, что . Если , то (как для всех ). Наконец, предположим, что $y$ $x$ $\text{I}(N,0,y)$ $0 < y \lor \text{I}(N,0,y)$ $y$ $x$ $S(x)$ $x$ $x<y,\text{I}(N,x,y)$ $x>y$ $x>y$ $S(x) >y$ $\text{I}(N,x,y)$ $S(x) >y$ $S(x) >x$ $x\in \mathbb{N}$ $x <y$ Тогда по теореме A мы имеем или , и в любом случае мы закончили. $S(x) < y$ $\text{I}(N,S(x),y)$

\begin{matrix} (◻) \end{matrix}

$\begin{equation} \tag{$\square$} \end{equation}$

Теоремы, которые я хочу доказать, можно выразить в Coq следующим образом.

Лемма less_lem (xy: N): меньше x (succ y) -> или (меньше xy) (IN xy).

Теорема Ntrichotomy: (для всего xy: N, или (меньше xy) (или (IN xy) (меньше yx))).

Полезные результаты

Здесь я собрал некоторые результаты, которые я определил, и подтвердил до этого момента. Это те, на которые я ссылаюсь выше. * Это код, который мне удалось написать до сих пор, обратите внимание, что большинство состоит из определений. *

(* Sigma types *)


Inductive Sigma (A:Set)(B:A -> Set) :Set :=
  Spair: forall a:A, forall b : B a,Sigma A B.

Definition E (A:Set)(B:A -> Set)
  (C: Sigma A B -> Set)
  (c: Sigma A B)
  (d: (forall x:A, forall y:B x, 
      C (Spair A B x y))): C c :=

match c as c0 return (C c0) with
| Spair a b => d a b
end. 


(* Binary sum type *)

Inductive sum' (A B:Set):Set := 
inl': A -> sum' A B | inr': B -> sum' A B.

Print sum'_rect.

Definition D (A B : Set)(C: sum' A B -> Set)
(c: sum' A B)
(d: (forall x:A, C (inl' A B x)))
(e: (forall y:B, C (inr' A B y))): C c :=

match c as c0 return C c0 with
| inl' x => d x
| inr' y => e y
end.

(* Three useful finite sets *)

Inductive N_0: Set :=.

Definition R_0
  (C:N_0 -> Set)
  (c: N_0): C c :=
match c as c0 return (C c0) with
end.

Inductive N_1: Set := zero_1:N_1.

Definition R_1 
  (C:N_1 -> Set)
  (c: N_1)
  (d_zero: C zero_1): C c :=
match c as c0 return (C c0) with
  | zero_1 => d_zero
end.

Inductive N_2: Set := zero_2:N_2 | one_2:N_2.

Definition R_2 
  (C:N_2 -> Set)
  (c: N_2)
  (d_zero: C zero_2)
  (d_one: C one_2): C c :=
match c as c0 return (C c0) with
  | zero_2 => d_zero
  | one_2  => d_one
end.


(* Natural numbers *)

Inductive N:Set :=
zero: N | succ : N -> N.

Print N. 

Print N_rect.

Definition R 
  (C:N -> Set)
  (d: C zero)
  (e: (forall x:N, C x -> C (succ x))):
  (forall n:N, C n) :=
fix F (n: N): C n :=
  match n as n0 return (C n0) with
  | zero => d
  | succ n0 => e n0 (F n0)
  end.

(* Boolean to truth-value converter *)

Definition Tr (c:N_2) : Set :=
match c as c0 with
  | zero_2 => N_0
  | one_2 => N_1
end.

(* Identity type *)

Inductive I (A: Set)(x: A) : A -> Set :=
r :  I A x x.

Print I_rect.

Theorem J 
  (A:Set)
  (C: (forall x y:A, 
              forall z: I A x y, Set))
  (d: (forall x:A, C x x (r A x)))
  (a:A)(b:A)(c:I A a b): C a b c.
induction c.
apply d.
Defined.

(* functions are extensional wrt
  identity types *)

Theorem I_I_extensionality (A B: Set)(f: A -> B):
(forall x y:A, I A x y -> I B (f x) (f y)).
Proof.
intros x y P.
induction P.
apply r.
Defined.


(* addition *)

Definition add (m n:N) : N 
 := R (fun z=> N) m (fun x y => succ y) n.

(* multiplication *)

Definition mul (m n:N) : N 
 := R (fun z=> N) zero (fun x y => add y m) n.


(* Axioms of Peano verified *)

Theorem P1a: (forall x: N, I N (add x zero) x).
intro x.
(* force use of definitional equality
  by applying reflexivity *)
apply r.
Defined.


Theorem P1b: (forall x y: N, 
I N (add x (succ y)) (succ (add x y))).
intros.
apply r.
Defined.


Theorem P2a: (forall x: N, I N (mul x zero) zero).
intros.
apply r.
Defined.


Theorem P2b: (forall x y: N, 
I N (mul x (succ y)) (add (mul x y) x)).
intros.
apply r.
Defined.

Definition pd (n: N): N :=
R (fun _=> N) zero (fun x y=> x) n.

(* alternatively
Definition pd (x: N): N :=
match x as x0 with
  | zero => zero
  | succ n0 => n0
end.
*)

Theorem P3: (forall x y:N, 
I N (succ x) (succ y) -> I N x y).
intros x y p.
apply (I_I_extensionality N N pd (succ x) (succ y)).
apply p.
Defined.

Definition not (A:Set): Set:= (A -> N_0).

Definition isnonzero (n: N): N_2:=
R (fun _ => N_2) zero_2 (fun x y => one_2) n.


Theorem P4 : (forall x:N, 
not (I N (succ x) zero)).
intro x.
intro p.

apply (J N (fun x y z => 
    Tr (isnonzero x) -> Tr (isnonzero y))
    (fun x => (fun t => t)) (succ x) zero)
.
apply p.
simpl.
apply zero_1.
Defined.

Theorem P5 (P:N -> Set):
P zero -> (forall x:N, P x -> P (succ x))
   -> (forall x:N, P x).
intros base step n.
apply R.
apply base.
apply step.
Defined.

(* I(A,-,-) is an equivalence relation *)

Lemma Ireflexive (A:Set): (forall x:A, I A x x).
intro x.
apply r.
Defined.

Lemma Isymmetric (A:Set): (forall x y:A, I A x y -> I A y x).
intros x y P.
induction P.
apply r.
Defined.

Lemma Itransitive (A:Set): 
(forall x y z:A, I A x y -> I A y z -> I A x z).
intros x y z P Q.
induction P.
assumption.
Defined.


Lemma succ_cong : (forall m n:N, I N m n -> I N (succ m) (succ n)).
intros m n H.
induction H.
apply r.
Defined.

Lemma zeroadd: (forall n:N, I N (add zero n) n).
intro n.
induction n.
simpl.
apply r.
apply succ_cong.
auto.

Defined.

Lemma succadd: (forall m n:N, I N (add (succ m) n) (succ (add m n))).
intros.
induction n.
simpl.
apply r.
simpl.
apply succ_cong.
auto.

Defined.

Lemma commutative_add: (forall m n:N, I N (add m n) (add n m)).
intros n m; elim n.
apply zeroadd.
intros y H; elim (succadd m y).
simpl.
rewrite succadd.
apply succ_cong.
assumption.


Defined.

Lemma associative_add: (forall m n k:N, 
I N (add (add m n) k) (add m (add n k))).
intros m n k.
induction k.
simpl.
apply Ireflexive.
simpl.
apply succ_cong.
assumption.
Defined.

Definition or (A B : Set):= sum' A B.


Definition less (m n: N) :=
 Sigma N (fun z => I N (add m (succ z)) n).



Lemma less_lem (x y:N) : 
less x (succ y) -> or (less x y) (I N x y).
intro.
destruct H.
right.

(* Here is where I'm working right now *)

Defined.


Theorem Ntrichotomy: (forall x y:N, 
or (less x y) (or (I N x y) (less y x))).

automated-theorem-proving proof-assistants mathematical-programming coq user11942
источник

Чтобы понять, как далеко вы продвинулись, было бы полезно, если бы вы опубликовали свой код Coq до сих пор, чтобы мы могли загрузить его и проверить, что то, что мы предлагаем, работает для ваших определений.

Жиль "ТАК - перестань быть злым"

Несколько комментариев и уточняющих вопросов: - Будет ли достаточно для ваших целей просто использовать синтаксическое равенство ("=" в Coq) вместо I (N, x, y)? Есть ли причина использовать «или», как вы это определили? Coq (ну, основные библиотеки для Coq) имеют способ выражения логической дизъюнкции, который облегчает некоторые приятные аспекты доказательств. Точно так же есть способ определить «меньше», который может быть более подходящим для вас. С этой целью вы, возможно, захотите взглянуть на первые главы Фондов программного обеспечения . Пока конец книги ...

Люк Мэтисон

... о проверке программ и т. д., начало довольно хорошее введение в Coq и содержит теоремы, подобные тем, которые вы получили в качестве упражнений и примеров. Это бесплатно, и на самом деле все написано в виде сценариев Coq, так что вы можете выполнять упражнения и компилировать их во время чтения. Для того, что вы делаете здесь, есть интересные фрагменты в главах Основы, Индукция, Опора и Логика - и, возможно, некоторые зависимости от промежуточных битов.

Люк Мэтисон

Еще одно замечание: Thm P5 (индуктивный принцип) встроен в Coq в более сильной форме (структурная индукция), поэтому вам не нужно явно принимать это за аксиому.

Люк Мэтисон

Я разместил код Coq, который я написал до сих пор.

user11942

Ответы:

Coq немного более жесток, чем бумажные доказательства: когда вы пишете «и мы закончили» или «ясно» в бумажном доказательстве, часто гораздо больше нужно сделать, чтобы убедить Coq.

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

Несколько замечаний:

Я использовал встроенные типы данных и определения, где я думал, что это не повредит вашим намерениям. Обратите внимание, что если бы я использовал встроенное равенство вместо identityвстроенного отношения «меньше», доказательства были бы намного проще, так как многие ваши леммы находятся в базе данных известных теорем, которые проверяются при каждом вызове
```
auto with arith.
```
Я использовал некоторую тактику, о которой вы, вероятно, не знаете, но у «настоящего» суперпользователя Coq была бы гораздо более мощная тактика под рукой и она написала бы свою собственную, чтобы упростить работу. Я всегда рекомендую CPDT как место, чтобы научиться эффективно использовать тактику.
Я использовал нотации и табуляции для улучшения читабельности и встроенные конструкции, такие как сопоставление и inductionтактика, чтобы упростить доказательство и перефакторинг. В частности, с вашим определением lessбыло трудно работать, вы можете видеть, как я немного изменил его с на эквивалент (но более простой в использовании) этот вид «тонкой настройки» определение бывает много в формальных доказательств.
$\exists x, m + (x + 1) = n$ $\exists x,\ m + (x+1) = n$ $\exists x, (x + m) + 1 = n$ $\exists x,\ (x + m)+1 = n$
Хотя вы можете получить ответы на эти вопросы здесь, я настоятельно рекомендую вам представить свою работу в Coq-Club, который был создан с конкретной целью ответить на эти вопросы.

Коди
источник

Отличный ответ, Коди! Замечательно узнать, что есть такие щедрые люди, как ты, которые готовы помогать другим, нуждающимся. Я искренне ценю это! Я определенно остановлюсь на CPDT и Coq-Club; оба из которых мне, скорее всего, понадобятся в ближайшем будущем, так как я продолжаю работать над проверкой алгоритма деления в Coq.

user11942

Спасибо! Обратите внимание, что это часто называют «евклидовым делением» и уже присутствует в некоторых библиотеках (хотя и над целыми числами)

cody

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

user11942

Ответ Коди превосходен и отвечает на ваш вопрос о переводе вашего доказательства в Coq. В качестве дополнения к этому, я хотел добавить те же результаты, но доказал, что использовал другой маршрут, в основном, как иллюстрацию некоторых кусочков Coq, и продемонстрировал то, что вы можете доказать синтаксически с очень небольшим количеством дополнительной работы. Однако это не утверждение, что это самый короткий маршрут - просто другой. Доказательства включают только одну дополнительную вспомогательную лемму и опираются только на основные определения, я не привожу сложение, умножение или любые их свойства, или функциональную экстенсиональность, и только аксиомы Пеано являются простой формой a <= b -> a + c <= b + c в лемме о помощнике (только для c = 1) и структурной индукции, которая в любом случае приходит с индуктивными типами бесплатно.

Как Cody, где я думал, что это не имеет значения, я использовал предопределенные типы и т. Д., Поэтому перед доказательством я опишу их:

Я использовал встроенный тип nat для натуральных чисел, который имеет (с точностью до именования) то же определение, что и у вас:

Индуктивный nat: Set: = O: nat | S: nat -> nat

Я использовал встроенные le и lt для значений меньше или равных и меньше соответственно, которые имеют сокращенные обозначения «<=» и «<» для удобства чтения. Они определены:

Индуктивный le: nat -> nat -> Prop: =
| le_n: для всего n, le nn
| le_S: всего нм, (le нм) -> (le n (S m)).

а также

Определение lt (nm: nat): = le (S n) m.

Встроенный eq (сокращение "=") является синтаксическим равенством и работает так же, как ваше "I", с одним конструктором, который просто говорит, что все равно самому себе. Симметричные и транзитивные свойства являются несложными доказательствами, но в этом случае они нам не понадобятся. Определение для eq ниже имеет встроенную запись.

Индуктивное уравнение (A: Тип) (x: A): A -> Prop: = eq_refl: x = x

Наконец, я использовал пропозициональный или (сокращенно "\ /" - это обратный слэш обратный слэш), который имеет два конструктора, в основном, что у вас есть либо доказательство для левого аргумента, либо для правого аргумента. Coq также имеет некоторые сокращенные тактики, левые и правые, которые просто означают «apply or_introl» и «apply or_intror» соответственно.

Индуктивный или (AB: Prop): Prop: =
or_introl: A -> A / B | or_intror: B -> A / B

Ниже приведены мои доказательства, в принципе, если разметка не мешает, вы можете просто вырезать и вставить это в файл Coq .v, и это сработает. Я включил комментарии, чтобы отметить интересные фрагменты, но они находятся в (* *) разделителях, поэтому вам не нужно их удалять.

Theorem lt_or_eq: forall (n m : nat),
  n < S m -> n < m \/ n = m.
Proof.
(*
  This proof is just a case analysis on n and m, whether they're zero or
  a successor of something.
*)
destruct n as [|n']; destruct m as [|m']. 

(*n = 0, m = 0*)
intros.
  right. reflexivity.

(*n = 0, m = S m'*)
intros H.
  inversion H.
  inversion H1.
  left. unfold lt. constructor.
  (*The constructor tactic tries to match the goal to a constructor
    that's in the environment.*) 
  left. unfold lt. constructor. assumption.
  (*Assumption tries to match the goal to something that's in the
    current context*)

(*n = S n', m = 0
  This case is false, so we can invert our way out of it.*)
intros.
  inversion H. inversion H1.

(*n = S n', m = S m'*)
intros.
  inversion H.
    right. reflexivity.
    left. unfold lt. assumption.
Qed.


(*
  The following lemma with be useful in the proof of the trichotomy theorem,
  it's pretty obviously true, and easy to prove. The interesting part for
  anyone relatively new to Coq is that the induction is done on the
  hypothesis "a <= b", rather than on either a or b.
*)
Lemma a_le_b_implies_Sa_le_Sb: forall a b, a <= b -> S a <= S b.
Proof.
  intros a b Hyp.
  induction Hyp.
  constructor.
  constructor.
  apply IHHyp.
Qed.

(*
  The proof of the trichotomy theorem is a little more involved than the
  last one but again we don't use anything particularly tricky. 
  Other than the helper lemma above, we don't use anything other than the
  definitions.

  The proof proceeds by induction on n, then induction on m.  My personal
  feeling is that this can probably be shortened.  
*)
Theorem trich: forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  induction n.
    induction m.
      right. left. reflexivity.
        inversion IHm.
          left. unfold lt. constructor. unfold lt in H. assumption.
          inversion H.
          left. unfold lt. subst. constructor.
          inversion H0.     
    induction m.
      assert (n < 0 \/ n = 0 \/ 0 < n).
      apply IHn.
      inversion H.
      inversion H0.
      inversion H0.
      right. right. subst. unfold lt. constructor.
      right. right. unfold lt. constructor. assumption.
      inversion IHm. unfold lt in H.
      left. unfold lt. constructor. assumption.
      inversion H; subst.
      left. unfold lt. constructor.
      inversion H0.
      right. left. reflexivity.
      right. right. apply lt_or_eq in H0.

      inversion H0.
      apply a_le_b_implies_Sa_le_Sb. assumption.
      subst. unfold lt. apply a_le_b_implies_Sa_le_Sb. assumption.
Qed.

(*
  The following is just to show what can be done with some of the tactics
  The omega tactic implements a Pressburger arithmetic solver, so anything
  with natural numbers, plus, multiplication by constants, and basic logic
  can just be solved. Not very interesting for practicing Coq, but cool to
  know.
*)

Require Import Omega.

Example trich' : forall (n m : nat),
  n < m \/ n = m \/ m < n.
Proof.
  intros.
  omega.
Qed.

Люк Мэтисон
источник

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

user11942