I can figure out how to prove my "degree_descent" Theorem below if I really need to:
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.
but this "hacky_rephrasing" Lemma is an ugly and unintuitive pattern to me. Is there a better way to prove degree_descent all by itself? For example, using set or pose to introduce n := degree x and then invoking induction n isn't working because it annihilates the hypothesis from the subsequent contexts (if someone could explain why this occurs, too, that would be helpful!). I can't figure out how to get generalize to work with me here, either.
PS: This is just weak induction for simplicity, but ideally I would like the solution to work with custom induction schemes via induction ... using ....
It looks like you would like to use the remember tactic:
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.
(* ... *)