关于Coq中自然数的最大值、归纳法的引理

Question

我有一个用自然数计算的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).

Answer 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.