How to prove Theorem euclid_gcd : forall a b z, euclid a b z -> gcd a b z. using coq?

Question

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. 

Answer 1

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.