#coq
#coq
Вопрос:
У меня есть семейство типов 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:
Ммм, я не уверен, где вы находите трудности, нет особых проблем в доказательстве этого, учитывая, что 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.
Но на самом деле, как структурировать теорию, неясно, если мы не узнаем немного больше о вариантах использования.
редактировать для тех, кто предпочитает использовать «стандартную библиотеку»:
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.
Комментарии:
1. Спасибо, но я использую стандартную библиотеку.
2. Это ничего не меняет, доказательства те же; в лучшем случае вам может понадобиться доказать какую-то недостающую лемму.
3. Хорошо, если мне удастся перевести, я опубликую решение здесь. Еще раз спасибо. Однако вопрос все еще остается открытым.
4. В этом случае используемая библиотека не так важна [как вы можете видеть в моем редактировании] Не привязывайте себя к одному, здесь важно то, что является доказательством.