(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Require Import Zdiv. Definition unit := unit. Parameter mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z). Axiom divides_refl : forall (n:Z), (divides n n). Axiom divides_1_n : forall (n:Z), (divides 1%Z n). Axiom divides_0 : forall (n:Z), (divides n 0%Z). Axiom divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (c * a)%Z (c * b)%Z). Axiom divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides (a * c)%Z (b * c)%Z). Axiom divides_oppr : forall (a:Z) (b:Z), (divides a b) -> (divides a (-b)%Z). Axiom divides_oppl : forall (a:Z) (b:Z), (divides a b) -> (divides (-a)%Z b). Axiom divides_oppr_rev : forall (a:Z) (b:Z), (divides (-a)%Z b) -> (divides a b). Axiom divides_oppl_rev : forall (a:Z) (b:Z), (divides a (-b)%Z) -> (divides a b). Axiom divides_plusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b + c)%Z)). Axiom divides_minusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides a c) -> (divides a (b - c)%Z)). Axiom divides_multl : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (c * b)%Z). Axiom divides_multr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a (b * c)%Z). Axiom divides_factorl : forall (a:Z) (b:Z), (divides a (b * a)%Z). Axiom divides_factorr : forall (a:Z) (b:Z), (divides a (a * b)%Z). Axiom divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/ (n = (-1%Z)%Z)). Axiom divides_antisym : forall (a:Z) (b:Z), (divides a b) -> ((divides b a) -> ((a = b) \/ (a = (-b)%Z))). Axiom divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> ((divides b c) -> (divides a c)). Axiom divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) -> ((Zabs a) <= (Zabs b))%Z). Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((Zmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((Zmod a b) = 0%Z)). Axiom mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> (((ZOmod a b) = 0%Z) -> (divides b a)). Axiom divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b a) -> ((ZOmod a b) = 0%Z)). Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z). Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z). Axiom even_or_odd : forall (n:Z), (even n) \/ (odd n). Axiom even_not_odd : forall (n:Z), (even n) -> ~ (odd n). Axiom odd_not_even : forall (n:Z), (odd n) -> ~ (even n). Axiom even_odd : forall (n:Z), (even n) -> (odd (n + 1%Z)%Z). Axiom odd_even : forall (n:Z), (odd n) -> (even (n + 1%Z)%Z). Axiom even_even : forall (n:Z), (even n) -> (even (n + 2%Z)%Z). Axiom odd_odd : forall (n:Z), (odd n) -> (odd (n + 2%Z)%Z). Axiom even_2k : forall (k:Z), (even (2%Z * k)%Z). Axiom odd_2k1 : forall (k:Z), (odd ((2%Z * k)%Z + 1%Z)%Z). Axiom even_divides : forall (a:Z), (even a) <-> (divides 2%Z a). Axiom odd_divides : forall (a:Z), (odd a) <-> ~ (divides 2%Z a). Parameter gcd: Z -> Z -> Z. Axiom gcd_nonneg : forall (a:Z) (b:Z), (0%Z <= (gcd a b))%Z. Axiom gcd_def1 : forall (a:Z) (b:Z), (divides (gcd a b) a). Axiom gcd_def2 : forall (a:Z) (b:Z), (divides (gcd a b) b). Axiom gcd_def3 : forall (a:Z) (b:Z) (x:Z), (divides x a) -> ((divides x b) -> (divides x (gcd a b))). Axiom gcd_unique : forall (a:Z) (b:Z) (d:Z), (0%Z <= d)%Z -> ((divides d a) -> ((divides d b) -> ((forall (x:Z), (divides x a) -> ((divides x b) -> (divides x d))) -> (d = (gcd a b))))). Axiom Assoc : forall (x:Z) (y:Z) (z:Z), ((gcd (gcd x y) z) = (gcd x (gcd y z))). Axiom Comm : forall (x:Z) (y:Z), ((gcd x y) = (gcd y x)). Axiom gcd_0_pos : forall (a:Z), (0%Z <= a)%Z -> ((gcd a 0%Z) = a). Axiom gcd_0_neg : forall (a:Z), (a < 0%Z)%Z -> ((gcd a 0%Z) = (-a)%Z). Axiom gcd_opp : forall (a:Z) (b:Z), ((gcd a b) = (gcd (-a)%Z b)). Axiom gcd_euclid : forall (a:Z) (b:Z) (q:Z), ((gcd a b) = (gcd a (b - (q * a)%Z)%Z)). Axiom Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a (ZOmod a b)) = (gcd a b)). Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd a (Zmod a b)) = (gcd a b)). Axiom gcd_mult : forall (a:Z) (b:Z) (c:Z), (0%Z <= c)%Z -> ((gcd (c * a)%Z (c * b)%Z) = (c * (gcd a b))%Z). Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | mk_ref contents1 => contents1 end. Implicit Arguments contents. (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_gcd : forall (x:Z), forall (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) -> forall (d:Z), forall (c:Z), forall (b:Z), forall (a:Z), forall (y1:Z), forall (x1:Z), ((0%Z <= x1)%Z /\ ((0%Z <= y1)%Z /\ (((gcd x1 y1) = (gcd x y)) /\ ((((a * x)%Z + (b * y)%Z)%Z = x1) /\ (((c * x)%Z + (d * y)%Z)%Z = y1))))) -> ((0%Z < y1)%Z -> forall (x2:Z), (x2 = y1) -> forall (y2:Z), (y2 = (ZOmod x1 y1)) -> forall (a1:Z), (a1 = c) -> forall (b1:Z), (b1 = d) -> forall (c1:Z), (c1 = (a - (c * (ZOdiv x1 y1))%Z)%Z) -> forall (d1:Z), (d1 = (b - (d * (ZOdiv x1 y1))%Z)%Z) -> ((gcd x2 y2) = (gcd x y))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. rewrite <- H4. subst x2 y2. symmetry. rewrite Comm. rewrite gcd_euclid with (q:=(ZOdiv x1 y1)). apply f_equal. rewrite (ZO_div_mod_eq x1 y1) at 1. ring. Qed. (* DO NOT EDIT BELOW *)