Понимание индукции на доказательствах в coq - PullRequest
Новая
       101

Понимание индукции на доказательствах в coq

0 голосов
/ 23 мая 2019

Я работаю над теоремой ev_ev__ev в IndProp.v из Основы программного обеспечения (Том 1: Логические основы) . 

Theorem ev_ev__ev : forall n m,
  even (n+m) -> even n -> even m.
Proof.
  intros n m Enm En. induction En as [| n' Hn' IHn'].
  - (* En: ev_0 *) simpl in Enm. apply Enm.
  - (* En: ev_SS n' Hn': even n' 
              with IHn': even (n' + m) -> even m *)
    apply IHn'. simpl in Enm. inversion Enm as [| n'm H]. apply H.
Qed.

где even определяется как: 

Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

В пункте второй маркированной строки - контекст и цель заключаются в следующем: 

m, n' : nat
Enm : even (S (S n') + m)
Hn' : even n'
IHn' : even (n' + m) -> even m
______________________________________(1/1)
even m

Я понимаю, как m, n', Enm, Hn' в контексте генерируются.Однако, как генерируется IHn'?

1 Ответ

3 голосов
/ 23 мая 2019

Гипотезы индукции систематически создаются для помещений конструкторов одного семейства.Таким образом, вы можете смотреть на каждый конструктор независимо.

Предположим, у вас есть индуктивное определение типа, которое начинается с: 

Inductive arbitraryName : A -> B -> Prop :=

Будет создан индукционный принцип, называемый arbitraryName_ind, которыйначинается с количественного определения произвольного предиката, обычно называемого P с тем же типом 

forall P : A -> B -> Prop,

Теперь, если у вас есть конструктор вида 

arbitrary_constructor : forall x y, arbitraryName x y -> ...

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

forall x y, arbitraryName x y -> P x y -> ...

Наконец, каждый конструкториндуктивное определение должно заканчиваться применением определенного семейства типов (в данном случае arbitraryName).В конце предложения для этого конструктора применяется функция P к тому же аргументу.

Вернемся к arbitrary_constructor и предположим, что он имеет следующий полный тип: 

arbitrary_constructor : forall x y, arbitraryName x y -> arbitraryName (g x y) (h x y)

В этом случае пункт в принципе индукции: 

 (forall x y, arbitraryName x y -> P x y -> P (g x y) (h x y))

В случае even существует конструктор ev_SS, имеющий следующую форму: 

ev_SS : forall x, even x -> even (S (S x))

Таким образом, сгенерированное предложение имеет следующую форму: 

(forall x, even x -> P x -> P (S (S x)))

Гипотеза индукции IHn' точно соответствует этому P в предложении.

Принцип полной индукции имеет следующую форму. 

forall P : nat -> Prop, P 0 -> 
   (forall x, even x -> P x -> P (S (S x))) ->
   forall n, even n -> P n

При вводе induction En применяется эта теорема.Гипотеза even n, где n определяется повсеместно, сопоставляется с текстом En в цели на тот момент.Оказывается, что утверждение этой гипотезы even n (n здесь зафиксировано в цели), так что универсально количественно n создается с локальным n из контекста цели.Затем тактика пытается найти все гипотезы в контексте, где появляется этот n.В этом случае существует Enm, поэтому эта гипотеза используется для определения P, на котором будет реализован принцип индукции.В некотором смысле происходит то, что Enm возвращается в заключении цели, как если бы он выполнил revert Enm.

Нам нужно, чтобы P n было таким же, как even (n + m) -> even m.Наиболее естественным решением является то, что P равно функции fun x => even (x + m) -> even m

Так что во втором случае доказательства по индукции вводится новый n' и P применяется к n' дать содержание гипотезы индукции: 

(even (n' + m) -> even m)

и P применяется к S (S n'), чтобы дать содержание конечной цели. 

 even (S (S n') + m) -> even m

Теперь, вВо время вызова тактики induction гипотеза Enm была в контексте, поэтому утверждение even (S (S n') + m), которое морально является потомком Enm, возвращается в контекст с тем же именем.Обратите внимание, что в другой цели уже была гипотеза с именем Enm, но утверждение снова было другим.

Это нормально, что у вас возникает вопрос о том, как возникла эта индуктивная гипотеза, потому что в действительности происходитнесколько операций.

...