如何解决Coq:关联变量的归纳
如果我真的需要,我可以想出如何证明下面的“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 一起使用。
解决方法
您似乎想使用 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.
(* ... *)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。