如何用Coq证明euclid_gcd定理？归纳第二步遇合一错误求助

我正在尝试证明euclid_gcd定理，但在归纳证明的第二个步骤陷入困境，频繁出现合一（unify）错误。以下是我的Coq代码，恳请提供帮助：

Require Import Arith.Arith.
Import Nat.


Inductive gcd : nat -> nat -> nat -> Prop :=
  base   : forall z, gcd z z z
| step_a : forall a b z, gcd a b z -> gcd (a + b) b z
| step_b : forall a b z, gcd a b z -> gcd a (a + b) z.


Inductive euclid : nat -> nat -> nat -> Prop :=
  stop    : forall z, euclid z z z
| step_a' : forall a b z, a > b -> euclid (a - b) b z -> euclid a b z
| step_b' : forall a b z, a < b -> euclid a (b - a) z -> euclid a b z.  


Search "+" "-".


Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z.
Proof.
  intros a b z H.
  induction H.
   - apply base.
   - apply step_a' in H0. 

你的问题出在归纳步骤的错误操作：在step_a'分支里，你误用了euclid的构造子step_a'去处理归纳假设相关的命题，这完全不符合gcd的构造逻辑，自然会触发合一错误。

下面是修正后的完整证明，核心是利用gcd的构造子结合自然数的加减等式性质，将归纳假设与目标命题关联：

Require Import Arith.Arith.
Import Nat.

Inductive gcd : nat -> nat -> nat -> Prop :=
  base   : forall z, gcd z z z
| step_a : forall a b z, gcd a b z -> gcd (a + b) b z
| step_b : forall a b z, gcd a b z -> gcd a (a + b) z.

Inductive euclid : nat -> nat -> nat -> Prop :=
  stop    : forall z, euclid z z z
| step_a' : forall a b z, a > b -> euclid (a - b) b z -> euclid a b z
| step_b' : forall a b z, a < b -> euclid a (b - a) z -> euclid a b z.

Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z.
Proof.
  intros a b z H.
  induction H.
  - (* stop 分支：直接匹配gcd的base构造子 *)
    apply base.
  - (* step_a' 分支：a > b，利用归纳假设推导gcd a b z *)
    rewrite <- (add_sub_assoc b a H).
    apply step_a.
    apply IHH.
  - (* step_b' 分支：a < b，对称处理 *)
    rewrite <- (add_sub_assoc a b (Nat.lt_le_incl _ _ H)).
    apply step_b.
    apply IHH.
Qed.

关键细节： #

• step_a'分支中，通过add_sub_assoc定理将a转化为(a - b) + b（前提a > b满足定理的适用条件），再用gcd的step_a构造子，把归纳假设gcd (a - b) b z转化为目标gcd a b z。
• step_b'分支逻辑完全对称，用step_b构造子和对应的加减等式即可完成推导。

内容的提问来源于stack exchange，提问作者lam_gam