提问人：lam_gam 提问时间：6/8/2023 最后编辑：lam_gam 更新时间：6/9/2023 访问量：50
如何使用 coq 证明定理 euclid_gcd ： forall a b z， euclid a b z -> gcd a b z？
How to prove Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z. using coq?
问：
我试图证明euclid_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.
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.
答：
2赞
Pierre Castéran
6/9/2023
#1
您可以重新表述您的子目标，以便应用 的一些构造函数。gcd a b zgcd
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.
- replace a with ((a-b) + b).
(* ... *)
Qed.
评论