英文:
How to prove Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z. using 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.
希望这能帮助你解决问题。
英文:
I am trying to prove euclid_gcd Theorem but Im getting stuck at the second case of the induction. most of the time I'm getting unify errors.
I will be glad for some help please.
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.
答案1
得分: 2
你可以重新表述你的子目标 gcd a b z，以便应用 gcd 的某个构造函数。
英文:
You may rephrase your subgoal gcd a b z in order to apply some constructor of gcd.
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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论