Coq：关联变量的归纳

Question

如果我真的需要，我可以弄清楚如何证明下面的“degree_descent”定理：

Variable X : Type.
Variable degree : X -> nat.
Variable P : X -> Prop.
Axiom inductive_by_degree : forall n, (forall x, S (degree x) = n -> P x) -> (forall x, degree x = n -> P x).



Lemma hacky_rephrasing : forall n, forall x, degree x = n -> P x.
Proof. induction n; intros.
  - apply (inductive_by_degree 0). discriminate. exact H.
  - apply (inductive_by_degree (S n)); try exact H. intros y K. apply IHn. injection K; auto.
Qed.

Theorem degree_descent : forall x, P x.
Proof. intro. apply (hacky_rephrasing (degree x)); reflexivity.
Qed.

但是这个“hacky_rephrasing”引理对我来说是一个丑陋且不直观的模式。有没有更好的方法来单独证明 degree_descent ？例如，使用 set 或 pose 引入 n := degree x 然后调用 induction n 不起作用，因为它从后续上下文中消除了假设（如果有人可以解释为什么这也会发生，那会很有帮助！）。我也不知道如何让 generalize 在这里和我一起工作。

PS：为了简单起见，这只是弱归纳法，但理想情况下，我希望解决方案通过 induction ... using ....

与 custom induction schemes 一起使用

Answer 1

您似乎想使用 remember 策略：

Variable X : Type.
Variable degree : X -> nat.
Variable P : X -> Prop.
Axiom inductive_by_degree : forall n, (forall x, S (degree x) = n -> P x) -> (forall x, degree x = n -> P x).

Theorem degree_descent : forall x, P x.
Proof.
  intro x. remember (degree x) as n eqn:E.
  symmetry in E. revert x E.
  (* Goal: forall x : X, degree x = n -> P x *)
  Restart. From Coq Require Import ssreflect.
  (* Or ssreflect style *)
  move=> x; move: {2}(degree x) (eq_refl : degree x = _)=> n.
  (* ... *)

Coq：关联变量的归纳

Coq: Induction on associated variable

coq

induction