Лемма о максимуме индукции по натуральным числам в Coq - PullRequest
Новая
       4

Лемма о максимуме индукции по натуральным числам в Coq

0 голосов
/ 13 апреля 2019

У меня есть семейство типов T, которые нумеруются натуральными числами. Если какой-то тип обитаем, то следующий тип также обитаем. (Могу ли я сказать, что семья "заселена"?)

Предположим, что n-й тип обитаем. Как доказать, что тип с номером max (m, n) также обитаем? 

Parameter fam : nat->Type.
Axiom fam_mon : forall n, fam n -> fam (S n).
Lemma mxinh m : forall n, fam n -> fam (max m n).

1 Ответ

2 голосов
/ 13 апреля 2019

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

Например, подробное доказательство: 

Parameter fam : nat->Type.
Axiom fam_mon : forall n, fam n -> fam n.+1.

Lemma fam_gt n k (hb : fam n) : fam (k + n).
Proof. by elim: k => //= k ihk; apply: fam_mon. Qed.

Lemma mxinh m n (hb : fam n) : fam (maxn n m).
Proof. by rewrite maxnE addnC; apply: fam_gt. Qed.

(* Another proof, YMMV *)  
Lemma fam_leq n m (hl : n <= m) (hb : fam n) : fam m.
Proof. by move/subnK: hl <-; apply: fam_gt. Qed.

Lemma mxinh' m n (hb : fam n) : fam (maxn n m).
Proof. exact: fam_leq (leq_maxl _ _) hb. Qed.

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

edit для тех, кто предпочитает использовать"стандартная библиотека": 

Require Import PeanoNat.

Parameter fam : nat -> Type.
Axiom fam_mon : forall n, fam n -> fam (S n).

Lemma fam_gt n k (hb : fam n) : fam (n + k).
Proof. now rewrite Nat.add_comm; induction k; auto; apply fam_mon. Qed.

Lemma fam_leq n m (hl : n <= m) (hb : fam n) : fam m.
Proof. now rewrite <- (Nat.sub_add _ _ hl), Nat.add_comm; apply fam_gt. Qed.

Lemma mxinh m n (hb : fam n) : fam (max n m).
Proof. exact (fam_leq (Nat.le_max_l _ _) hb). Qed.
...