Принцип индукции для `le` - PullRequest
Новая
       92

Принцип индукции для `le`

0 голосов
/ 16 марта 2019

Для индуктивного типа nat сгенерированный принцип индукции использует конструкторы O и S в своем утверждении: 

Inductive nat : Set :=  O : nat | S : nat -> nat

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

Но для le сгенерированный оператор не использует конструкторы le_n и le_S: 

Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

le_ind
 : forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0

Однако можно сформулировать и доказать принцип индукции, следуя той же форме, что и для nat: 

Lemma le_ind' : forall n (P : forall m, le n m -> Prop),
P n (le_n n) ->
(forall m (p : le n m), P m p -> P (S m) (le_S n m p)) ->
forall m (p : le n m), P m p.
Proof.
fix H 6; intros; destruct p.
apply H0.
apply H1, H.
apply H0.
apply H1.
Qed.

Полагаю, сгенерированный более удобен. Но как Coq выбирает форму для своего сгенерированного принципа индукции? Если есть какое-либо правило, я не могу найти их в справочном руководстве. А как насчет других помощников, таких как Агда?

Ответы [ 2 ]

1 голос
/ 04 апреля 2019

Вы можете вручную создать принцип индукции для индуктивного типа, используя команду Scheme (см. Документацию ).

Команда поставляется в двух вариантах:

  • Scheme scheme := Induction for Sort Prop генерирует стандартную индукционную схему.
  • Scheme scheme := Minimality for Sort Prop создает упрощенную индукционную схему, более подходящую для индуктивных предикатов.

Если вы определяете индуктивный тип вType, порожденный принцип индукции первого рода.Если вы определяете индуктивный тип в Prop (т. Е. Индуктивный предикат), сгенерированный принцип индукции относится ко второму виду.

Чтобы получить принцип индукции, который вам нужен в случае le, выможете определить его в Type: 

Inductive le (n : nat) : nat -> Type :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m).

Check le_ind.
(* forall (n : nat) (P : forall n0 : nat, le n n0 -> Prop),
   P n (le_n n) ->
   (forall (m : nat) (l : le n m), P m l -> P (S m) (le_S n m l)) ->
   forall (n0 : nat) (l : le n n0), P n0 l
*)

или вы можете вручную попросить Coq сгенерировать ожидаемый принцип индукции: 

Inductive le (n : nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m : nat, le n m -> le n (S m).

Check le_ind.
(* forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, le n m -> P m -> P (S m)) ->
   forall n0 : nat, le n n0 -> P n0
*)

Scheme le_ind2 := Induction for le Sort Prop.
Check le_ind2.
(* forall (n : nat) (P : forall n0 : nat, le n n0 -> Prop),
   P n (le_n n) ->
   (forall (m : nat) (l : le n m), P m l -> P (S m) (le_S n m l)) ->
   forall (n0 : nat) (l : le n n0), P n0 l
*)
0 голосов
/ 16 марта 2019

Это потому что le_S и le_n были расширены. 

le_ind
 : forall (n : nat) (P : nat -> Prop),
   P n ->                                         1) le_n case
   (forall m : nat, n <= m -> P m -> P (S m)) ->  2) le_S case
   forall n0 : nat, n <= n0 -> P n0

n <= n0 может быть построен двумя способами:

  1. По le_n Итак, у вас есть n <= n. Вы должны показать P n. Поскольку у вас нет никаких последствий в конструкторе, у вас нет никаких предпосылок.
  2. По le_S. Итак, у вас есть n <= m -> n <= S m. Вы хотите показать P (S m). Поскольку у вас есть n <= m, вы можете предположить, что n <= m и (гипотеза индукции) P m истинны.
...