gcd_bezout_WP_GcdBezout_WP_parameter_gcd_1.v 5.55 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(* 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.

11
Parameter at1: forall (a:Type), a -> mark -> a.
12 13 14

Implicit Arguments at1.

15
Parameter old: forall (a:Type), a -> a.
16 17 18

Implicit Arguments old.

19
Definition divides(d:Z) (n:Z): Prop := exists q:Z, (n = (q * d)%Z).
20

21
Axiom divides_refl : forall (n:Z), (divides n n).
22

23
Axiom divides_1_n : forall (n:Z), (divides 1%Z n).
24

25
Axiom divides_0 : forall (n:Z), (divides n 0%Z).
26

27 28
Axiom divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) ->
  (divides (c * a)%Z (c * b)%Z).
29

30 31
Axiom divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) ->
  (divides (a * c)%Z (b * c)%Z).
32

33
Axiom divides_oppr : forall (a:Z) (b:Z), (divides a b) -> (divides a (-b)%Z).
34

35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
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).

59 60
Axiom divides_n_1 : forall (n:Z), (divides n 1%Z) -> ((n = 1%Z) \/
  (n = (-1%Z)%Z)).
61 62 63 64 65 66 67 68 69

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).
70

71
Axiom mod_divides_euclidean : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
72 73
  (((Zmod a b) = 0%Z) -> (divides b a)).

74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
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).
108

109
Parameter gcd: Z -> Z -> Z.
110 111 112 113 114 115 116 117 118 119 120


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))).

121 122 123 124
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))))).

125 126 127 128 129
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)).

130 131 132 133 134
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)).
135 136 137 138 139 140 141 142 143

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)).
144

145 146 147
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).

148 149 150 151 152 153 154 155 156 157
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.

158 159 160 161
(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

162 163
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),
164 165
  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) /\
166 167 168 169
  (((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),
170
  (d1 = (b - (d * (ZOdiv x1 y1))%Z)%Z) -> ((gcd x2 y2) = (gcd x y))).
171 172
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
173
rewrite <- H4.
174
subst x2 y2.
175 176 177
symmetry.
rewrite Comm.
rewrite gcd_euclid with (q:=(ZOdiv x1 y1)).
178 179 180
apply f_equal.
rewrite (ZO_div_mod_eq x1 y1) at 1.
ring.
181 182 183 184
Qed.
(* DO NOT EDIT BELOW *)