Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (* compiles with COQ 8.7*)
- Theorem nsr_plus_associative: forall a b c:nat, a+(b+c) = (a+b)+c.
- Proof.
- induction a.
- intros.
- simpl.
- reflexivity.
- intros.
- simpl.
- rewrite IHa.
- reflexivity.
- Qed.
- Theorem nsr_plus_commutative: forall x y:nat, x+y = y + x.
- Proof.
- induction x.
- intro.
- rewrite <-plus_n_O.
- simpl.
- reflexivity.
- intro.
- simpl.
- rewrite <-plus_n_Sm.
- rewrite IHx.
- reflexivity.
- Qed.
- Theorem nsr_right_distributivity: forall x y z:nat, (x+y)*z = (x*z)+(y*z).
- Proof.
- induction x.
- simpl.
- reflexivity.
- simpl.
- intros.
- assert (z+ x * z + y * z = z + (x * z + y * z)).
- apply eq_sym.
- apply nsr_plus_associative.
- rewrite H.
- apply f_equal.
- apply IHx.
- Qed.
- Theorem nsr_mult_commutative: forall x y:nat, x*y = y*x.
- Proof.
- induction x.
- simpl.
- intro.
- rewrite <- mult_n_O.
- reflexivity.
- simpl.
- assert (forall a b:nat, b * (S a) = b + b * a).
- induction b.
- simpl.
- reflexivity.
- simpl.
- rewrite IHb.
- apply f_equal.
- rewrite nsr_plus_associative.
- rewrite nsr_plus_associative.
- rewrite nsr_plus_commutative with (x:=a) (y:=b).
- reflexivity.
- intro.
- apply eq_sym.
- rewrite IHx.
- apply H.
- Qed.
- Theorem nsr_left_distributivity: forall x y z:nat, z*(x+y) = (z*x)+(z*y).
- Proof.
- intros.
- rewrite nsr_mult_commutative with (x:=z) (y:=x+y).
- rewrite nsr_mult_commutative with (x:=z) (y:=x).
- rewrite nsr_mult_commutative with (x:=z) (y:=y).
- apply nsr_right_distributivity.
- Qed.
- Theorem nsr_mult_associative: forall x y z:nat, x*(y*z)=(x*y)*z.
- Proof.
- induction x.
- intros.
- simpl.
- reflexivity.
- simpl.
- intros.
- rewrite nsr_right_distributivity.
- rewrite IHx.
- reflexivity.
- Qed.
- Theorem nsr_O_absorbs: forall n:nat, 0 * n = 0.
- Proof.
- intros.
- simpl.
- reflexivity.
- Qed.
- Theorem nsr_I_mult_neutral: forall n:nat, 1 * n = n.
- Proof.
- cut(forall n:nat, n * 1 =n ).
- intros.
- rewrite nsr_mult_commutative.
- apply H.
- induction n.
- simpl.
- reflexivity.
- simpl.
- rewrite IHn.
- reflexivity.
- Qed.
- Theorem nsr_O_plus_neutral: forall n:nat, n = 0 + n.
- Proof.
- intros.
- simpl.
- reflexivity.
- Qed.
- Lemma nat_sum_regularity: forall x y z:nat, x+ y = x + z -> y = z.
- Proof.
- induction x.
- simpl.
- intros.
- assumption.
- intro.
- intro.
- rewrite plus_Sn_m.
- rewrite plus_Sn_m.
- intro.
- apply IHx.
- apply eq_add_S.
- assumption.
- Qed.
- Lemma eq_prod: forall a a' b b':nat, a=a' -> b=b' -> (a,b)=(a',b').
- Proof.
- intros.
- rewrite H.
- rewrite H0.
- reflexivity.
- Qed.
- Notation Relative_integer := (prod nat nat).
- Definition eqz (a b:Relative_integer):Prop := fst a + snd b = fst b + snd a.
- Lemma eqz_reflexive: forall a:Relative_integer, eqz a a.
- Proof.
- intro.
- destruct a.
- unfold eqz.
- reflexivity.
- Qed.
- Lemma eqz_symmetric: forall a b:Relative_integer, eqz a b -> eqz b a.
- Proof.
- unfold eqz.
- intros.
- rewrite H.
- reflexivity.
- Qed.
- Lemma eqz_transitive: forall a b c:Relative_integer, eqz a b -> eqz b c -> eqz a c.
- Proof.
- unfold eqz.
- intro.
- intro.
- intro.
- destruct a as (p_a,q_a).
- destruct b as (p_b,q_b).
- destruct c as (p_c,q_c).
- simpl.
- intros.
- apply nat_sum_regularity with (x:= q_b).
- rewrite nsr_plus_associative.
- rewrite nsr_plus_associative.
- assert (q_b+p_a=p_a+q_b).
- apply nsr_plus_commutative.
- rewrite H1.
- rewrite H.
- assert (q_b + p_c = p_c + q_b).
- apply nsr_plus_commutative.
- rewrite H2.
- rewrite <- H0.
- rewrite <- nsr_plus_associative.
- rewrite <- nsr_plus_associative.
- apply f_equal.
- apply nsr_plus_commutative.
- Qed.
- Definition Z_plus (a b:Relative_integer):Relative_integer := (fst a + fst b, snd a + snd b).
- Definition Z_zero:Relative_integer:= (0,0).
- Definition Z_un:Relative_integer:= (1,0).
- Lemma Z_plus_associative_equal:
- forall (a b c:Relative_integer), Z_plus a (Z_plus b c) = Z_plus (Z_plus a b) c.
- Proof.
- intro.
- destruct a as (p_a,q_a).
- intro.
- destruct b as (p_b,q_b).
- intro.
- destruct c as (p_c,q_c).
- unfold Z_plus.
- simpl.
- assert (forall u v w x:nat, u=w -> v = x -> (u,v)=(w,x)) as LEMMA.
- intros.
- rewrite H.
- rewrite H0.
- reflexivity.
- apply LEMMA.
- apply nsr_plus_associative.
- apply nsr_plus_associative.
- Qed.
- Theorem Z_plus_associative: forall (a b c:Relative_integer),
- eqz ( Z_plus a (Z_plus b c)) ( Z_plus (Z_plus a b) c).
- Proof.
- intros.
- rewrite Z_plus_associative_equal.
- apply eqz_reflexive.
- Qed.
- Notation "a +Z b":= (Z_plus a b) (left associativity, at level 61).
- Notation "a =Z b":= (eqz a b) (left associativity, at level 71).
- Definition Z_mult (x y:Relative_integer):Relative_integer:=
- ((fst x)*(fst y) + (snd x)* (snd y), (fst x)*(snd y)+(snd x)*(fst y)).
- Notation "a *Z b":= (Z_mult a b) (left associativity, at level 59).
- (*the following are abreviations used in manually done computations *)
- Ltac arl p q r := rewrite nsr_plus_associative with (a:=p) (b:=q) (c:=r).
- Ltac alr p q r := rewrite <- nsr_plus_associative with (a:=p) (b:=q) (c:=r).
- Ltac com p q := rewrite nsr_plus_commutative with (x:= p) (y:=q).
- Ltac mrl p q r := rewrite nsr_mult_associative with (x:=p) (y:=q) (z:=r).
- Ltac mlr p q r := rewrite <- nsr_mult_associative with (x:=p) (y:=q) (z:=r).
- Ltac mom p q := rewrite nsr_mult_commutative with (x:= p) (y:=q).
- Ltac dir p q r := rewrite nsr_right_distributivity with (x:=p) (y:=q)(z:=r).
- Ltac dil p q r := rewrite nsr_left_distributivity with (x:=q) (y:=r) (z:=p).
- Ltac fir p q r := rewrite <- nsr_right_distributivity with (x:=p) (y:=q)(z:=r).
- Ltac fil p q r := rewrite <- nsr_left_distributivity with (x:=q) (y:=r) (z:=p).
- Theorem Z_mult_associative: forall x y z:Relative_integer, x *Z (y *Z z) =Z x *Z y *Z z.
- Proof.
- intro.
- destruct x as (a,b).
- intro.
- destruct y as (c,d).
- intro.
- destruct z as (e,f).
- unfold Z_mult.
- unfold eqz.
- simpl.
- rewrite nsr_left_distributivity with (z:=a) (x:=c * e) (y:= d * f).
- rewrite nsr_mult_associative with (x:= a) (y:=c) (z:=e).
- rewrite nsr_mult_associative with (x:= a) (y:=d) (z:=f).
- rewrite nsr_left_distributivity with (z:=b) (x:=c * f) (y:= d * e).
- rewrite nsr_mult_associative with (x:= b) (y:=c) (z:=f).
- rewrite nsr_mult_associative with (x:= b) (y:=d) (z:=e).
- rewrite nsr_left_distributivity with (z:=a) (x:=c * f) (y:= d * e).
- rewrite nsr_mult_associative with (x:= a) (y:=c) (z:=f).
- rewrite nsr_mult_associative with (x:= a) (y:=d) (z:=e).
- rewrite nsr_left_distributivity with (z:=b) (x:=c * e) (y:= d * f).
- rewrite nsr_mult_associative with (x:= b) (y:=c) (z:=e).
- rewrite nsr_mult_associative with (x:= b) (y:=d) (z:=f).
- rewrite nsr_right_distributivity with (x:= a * c) (y:= b * d) (z:=f).
- rewrite nsr_right_distributivity with (x:= a * d) (y:= b * c) (z:=e).
- rewrite nsr_right_distributivity with (x:= a * c) (y:= b * d) (z:=e).
- rewrite nsr_right_distributivity with (x:= a * d) (y:= b * c) (z:=f).
- assert (forall (ace adf bcf bde acf bdf ade bce:nat),
- ace + adf + (bcf + bde) + (acf + bdf + (ade + bce)) =
- ace + bde + (adf + bcf) + (acf + ade + (bce + bdf))) as L.
- intros.
- com bcf bde.
- alr ace adf (bde + bcf).
- arl adf bde bcf.
- com adf bde.
- alr ace bde (adf + bcf).
- alr bde adf bcf.
- com bce bdf.
- arl (acf + ade) bdf bce.
- alr acf ade bdf.
- com ade bdf.
- arl acf bdf ade.
- alr (acf + bdf) ade bce.
- reflexivity.
- apply L.
- Qed.
- Theorem Z_plus_commutative: forall a b:Relative_integer, a +Z b =Z b +Z a.
- Proof.
- intros.
- unfold eqz.
- unfold Z_plus.
- simpl.
- com (fst a) (fst b).
- com (snd a) (snd b).
- reflexivity.
- Qed.
- Theorem Z_mult_commutative: forall a b:Relative_integer, a *Z b =Z b *Z a.
- Proof.
- intros.
- unfold eqz.
- unfold Z_mult.
- simpl.
- mom (fst a) (fst b).
- mom (snd a) (snd b).
- mom (fst a) (snd b).
- mom (fst b) (snd a).
- com (snd a * fst b) (snd b * fst a).
- reflexivity.
- Qed.
- Theorem Z_right_distributivity: forall a b c:Relative_integer, (a +Z b) *Z c =Z (a *Z c) +Z (b *Z c).
- Proof.
- intros.
- destruct a as (p,q).
- destruct b as (r,s).
- destruct c as (t,u).
- unfold eqz.
- unfold Z_plus.
- unfold Z_mult.
- simpl.
- dir p r t.
- dir q s u.
- dir p r u.
- dir q s t.
- assert (forall (a b c d:nat), a + b + (c + d) = a + c + (b + d)) as L.
- intros.
- alr a b (c+d).
- arl b c d.
- com b c.
- alr c b d.
- arl a c (b + d).
- reflexivity.
- rewrite L with (a:= p * t) (b:= r * t) (c:= q * u) (d:= s * u).
- apply f_equal.
- apply L.
- Qed.
- Theorem Z_zero_plus_neutral: forall a:Relative_integer, Z_zero +Z a =Z a.
- Proof.
- intro.
- unfold eqz.
- unfold Z_plus.
- unfold Z_zero.
- simpl.
- reflexivity.
- Qed.
- Notation O_Z:= (Z_zero).
- Notation I_Z := (Z_un).
- Theorem Z_un_neutral: forall a:Relative_integer, I_Z *Z a =Z a.
- Proof.
- intros.
- destruct a as (x,y).
- unfold eqz.
- unfold Z_mult.
- unfold Z_un.
- simpl.
- alr x 0 0.
- alr x (0 + 0) y.
- com (0+0) y.
- arl y 0 0.
- reflexivity.
- Qed.
- Definition Z_opp (a:Relative_integer):Relative_integer:= (snd a,fst a).
- Definition Z_minus (a b:Relative_integer):Relative_integer:= ((fst a) + (snd b), (snd a)+ (fst b)).
- Notation "a -Z b" := (Z_minus a b) (at level 69).
- Theorem Z_opp_group: forall x:Relative_integer, x +Z (Z_opp x) =Z O_Z.
- Proof.
- intros.
- destruct x as (p,q).
- unfold eqz.
- unfold Z_plus.
- unfold Z_opp.
- simpl.
- com p q.
- com (q + p) 0.
- simpl.
- reflexivity.
- Qed.
- Theorem Z_minus_opp: forall x y:Relative_integer, x -Z y =Z x +Z (Z_opp y).
- Proof.
- intros.
- unfold eqz.
- unfold Z_plus.
- unfold Z_minus.
- unfold Z_opp.
- simpl.
- reflexivity.
- Qed.
- Theorem Z_sum_compatibility: forall x x0 y y0:Relative_integer,
- x =Z y -> x0 =Z y0 -> (x +Z x0) =Z (y +Z y0).
- Proof.
- intro.
- intro.
- intro.
- intro.
- unfold eqz.
- unfold Z_plus.
- destruct x as (a,b).
- destruct y as (c,d).
- destruct x0 as (e,f).
- destruct y0 as (g,h).
- simpl.
- intros.
- arl (a+e) d h.
- alr a e d.
- com e d.
- arl a d e.
- rewrite H.
- alr (c+b) e h.
- rewrite H0.
- arl (c + b) g f.
- arl (c + g) b f.
- alr c b g.
- alr c g b.
- com b g.
- reflexivity.
- Qed.
- Theorem Z_mult_compatibility: forall x x0 y y0:Relative_integer,
- x =Z y -> x0 =Z y0 -> (x *Z x0) =Z (y *Z y0).
- Proof.
- assert (forall p q r:Relative_integer, eqz p q -> eqz (p *Z r) (q *Z r)) as L.
- unfold eqz.
- unfold Z_mult.
- intro.
- intro.
- intro.
- destruct p as (a,b).
- destruct q as (c,d).
- destruct r as (x,y).
- simpl.
- intros.
- alr (a * x) (b * y) (c * y + d * x).
- arl (b * y) (c * y) (d * x).
- fir b c y.
- com b c.
- rewrite <- H.
- com (a * y) (b * x).
- com (c * x) (d * y).
- alr (d * y) (c * x) (b * x + a * y).
- arl (c * x) (b * x) (a * y).
- fir c b x.
- rewrite <- H.
- dir a d x.
- dir a d y.
- alr (a * x) (d * x) (a * y).
- com (d * x) (a * y).
- arl (a * x) (a * y) (d * x).
- arl (d * y) (a * x + a * y) (d * x).
- arl (d * y) (a * x) (a * y).
- com (d * y) (a * x).
- alr (a * x) (d * y) (a * y).
- arl (a * x) (a * y + d * y) (d * x).
- com (a * y) (d * y).
- reflexivity.
- intros.
- apply eqz_transitive with (b:= y *Z x0).
- apply L.
- assumption.
- apply eqz_transitive with (b:= x0 *Z y).
- apply Z_mult_commutative.
- apply eqz_transitive with (b:= y0 *Z y).
- apply L.
- assumption.
- apply Z_mult_commutative.
- Qed.
- Theorem Z_opp_compatibility: forall x y:Relative_integer, x =Z y -> Z_opp x =Z Z_opp y.
- Proof.
- unfold eqz.
- unfold Z_opp.
- intros.
- simpl.
- rewrite nsr_plus_commutative.
- rewrite <- H.
- apply nsr_plus_commutative.
- Qed.
- Theorem Z_left_distributivity: forall a b c:Relative_integer, c *Z (a +Z b) =Z (c *Z a) +Z (c *Z b).
- Proof.
- intros.
- apply eqz_transitive with (b:= (a +Z b) *Z c).
- apply Z_mult_commutative.
- apply eqz_transitive with (b:= (a *Z c)+Z (b *Z c)).
- apply Z_right_distributivity.
- apply Z_sum_compatibility.
- apply Z_mult_commutative.
- apply Z_mult_commutative.
- Qed.
- Theorem Z_sum_regularity: forall x y z:Relative_integer, x +Z z =Z y +Z z -> x =Z y.
- Proof.
- intros.
- assert (forall p r:Relative_integer, p =Z (p +Z r) +Z (Z_opp r))as LEMMA1.
- intros.
- apply eqz_transitive with (b:= p +Z (r +Z (Z_opp r))).
- apply eqz_transitive with (b:= p +Z O_Z).
- apply eqz_transitive with (b:= O_Z +Z p).
- apply eqz_symmetric.
- apply Z_zero_plus_neutral.
- apply Z_plus_commutative.
- apply Z_sum_compatibility.
- apply eqz_reflexive.
- apply eqz_symmetric.
- apply Z_opp_group.
- apply Z_plus_associative.
- intros.
- apply eqz_transitive with (b:= (x +Z z) +Z (Z_opp z)).
- apply LEMMA1.
- apply eqz_transitive with (b:= (y +Z z) +Z (Z_opp z)).
- apply Z_sum_compatibility.
- assumption.
- apply eqz_reflexive.
- apply eqz_symmetric.
- apply LEMMA1.
- Qed.
- Theorem Z_zero_product:forall x:Relative_integer, x *Z O_Z =Z O_Z.
- (*we show this property is a consequence of ring axioms as coq intended them, rather
- than using the specific structure of Relative_integer defined above*)
- Proof.
- intros.
- apply Z_sum_regularity with (z:= x *Z I_Z).
- apply eqz_transitive with (b:= x *Z (O_Z +Z I_Z)).
- apply eqz_symmetric.
- apply Z_left_distributivity.
- apply eqz_transitive with (b:= x *Z I_Z).
- apply Z_mult_compatibility.
- apply eqz_reflexive.
- apply Z_zero_plus_neutral.
- apply eqz_symmetric.
- apply Z_zero_plus_neutral.
- Qed.
- Theorem sign_rule:forall x y:Relative_integer,
- (Z_opp x) *Z (Z_opp y) =Z x *Z y.
- Proof.
- intros.
- assert (forall p r:Relative_integer, p =Z (p +Z r) +Z (Z_opp r))as LEMMA1.
- intros.
- apply eqz_transitive with (b:= p +Z (r +Z (Z_opp r))).
- apply eqz_transitive with (b:= p +Z O_Z).
- apply eqz_transitive with (b:= O_Z +Z p).
- apply eqz_symmetric.
- apply Z_zero_plus_neutral.
- apply Z_plus_commutative.
- apply Z_sum_compatibility.
- apply eqz_reflexive.
- apply eqz_symmetric.
- apply Z_opp_group.
- apply Z_plus_associative.
- assert (forall p q r:Relative_integer, p +Z r =Z q +Z r -> p =Z q) as LEMMA2.
- intros.
- apply eqz_transitive with (b:= (p +Z r) +Z (Z_opp r)).
- apply LEMMA1.
- apply eqz_transitive with (b:= (q +Z r) +Z (Z_opp r)).
- apply Z_sum_compatibility.
- assumption.
- apply eqz_reflexive.
- apply eqz_symmetric.
- apply LEMMA1.
- apply LEMMA2 with (r:= (Z_opp x) *Z y).
- apply eqz_transitive with (b:= O_Z).
- apply eqz_transitive with (b:= (Z_opp x) *Z ((Z_opp y +Z y))).
- apply eqz_symmetric.
- apply Z_left_distributivity.
- apply eqz_transitive with (b:= Z_opp x *Z O_Z).
- apply Z_mult_compatibility.
- apply eqz_reflexive.
- apply eqz_transitive with (b:= y +Z (Z_opp y)).
- apply Z_plus_commutative.
- apply Z_opp_group.
- apply Z_zero_product.
- apply eqz_transitive with (b:= O_Z *Z y).
- apply eqz_symmetric.
- apply eqz_transitive with (b:= y *Z O_Z).
- apply eqz_symmetric.
- apply Z_mult_commutative.
- apply Z_zero_product.
- apply eqz_transitive with (b:= (x +Z (Z_opp x)) *Z y).
- apply Z_mult_compatibility.
- apply eqz_symmetric.
- apply Z_opp_group.
- apply eqz_reflexive.
- apply Z_right_distributivity.
- Qed.
- Ltac zer := apply eqz_reflexive.
- Ltac zes := apply eqz_symmetric.
- Ltac zet p:= apply eqz_transitive with (b:=p).
- Ltac zcom:= apply Z_mult_commutative.
- Section Signs_of_relative_integers.
- Fixpoint zsign_nat (p q:nat):Relative_integer:=
- match p with
- |0 => match q with
- |0 => O_Z
- |S t => (0,1)
- end
- |S r => match q with
- |0 => I_Z
- |S u => zsign_nat r u
- end
- end.
- Definition zsign (x:Relative_integer):Relative_integer:= zsign_nat (fst x) (snd x).
- Lemma calc_AOO: forall x:nat, zsign_nat x x = O_Z.
- Proof.
- induction x.
- simpl.
- reflexivity.
- simpl.
- apply IHx.
- Qed.
- Lemma calc_AOS: forall x y:nat, zsign_nat x (S (y + x)) = (0,1).
- Proof.
- induction x.
- intro.
- simpl.
- reflexivity.
- intros.
- simpl.
- rewrite <- plus_n_Sm with (n:=y) (m:=x).
- apply IHx.
- Qed.
- Lemma calc_ASO: forall x y:nat, zsign_nat (S (y + x)) x = (1,0).
- Proof.
- induction x.
- intro.
- simpl.
- reflexivity.
- intro.
- simpl.
- rewrite <- plus_n_Sm with (n:= y) (m:= x).
- apply IHx.
- Qed.
- Lemma zsign_compat: forall (x y:Relative_integer), x =Z y -> zsign x = zsign y.
- Proof.
- assert (forall a b c d:nat, a+d=b+c -> zsign_nat a b = zsign_nat c d) as L.
- induction a.
- intros.
- induction b.
- rewrite plus_O_n in H.
- rewrite plus_O_n in H.
- rewrite H.
- rewrite calc_AOO.
- rewrite calc_AOO.
- reflexivity.
- rewrite plus_O_n in H.
- rewrite H.
- simpl.
- rewrite calc_AOS.
- reflexivity.
- induction b.
- intros.
- rewrite plus_O_n in H.
- rewrite plus_Sn_m in H.
- rewrite <- H.
- rewrite calc_ASO.
- simpl.
- reflexivity.
- intros.
- simpl.
- rewrite plus_Sn_m with (n:=a) (m:=d) in H.
- rewrite plus_Sn_m with (n:=b) (m:=c) in H.
- apply eq_add_S in H.
- apply IHa.
- assumption.
- intro.
- intro.
- unfold eqz.
- unfold zsign.
- intros.
- apply L.
- rewrite H.
- apply nsr_plus_commutative.
- Qed.
- Lemma cases_sign: forall x:Relative_integer,
- (x =Z O_Z) \/ (exists p:nat, x =Z (S p,0)) \/ (exists q:nat, x=Z (0,S q)).
- Proof.
- assert (forall a b:nat,
- a + 0 = 0 + b \/
- (exists c:nat, a + 0 = S c + b) \/
- (exists d:nat, a + S d = 0 + b)) as L.
- induction a.
- induction b.
- left.
- simpl.
- reflexivity.
- simpl in IHb.
- destruct IHb.
- rewrite <- H.
- right.
- right.
- exists 0.
- reflexivity.
- right.
- right.
- exists b.
- reflexivity.
- induction b.
- right.
- left.
- exists a.
- reflexivity.
- destruct IHb.
- right.
- right.
- exists 0.
- rewrite <- plus_n_Sm with (n:=S a) (m:=0).
- rewrite <- plus_n_Sm with (n:=0) (m:=b).
- apply eq_S.
- assumption.
- destruct H.
- destruct H as (e,He).
- induction e.
- left.
- rewrite <- plus_n_Sm with (n:= 0) (m:=b).
- rewrite <- plus_Sn_m with (n:=0) (m:=b).
- assumption.
- right.
- left.
- exists e.
- rewrite <- plus_n_Sm with (n:= S e) (m:=b).
- rewrite <- plus_Sn_m with (n:=S e) (m:=b).
- assumption.
- right.
- right.
- destruct H as (f,Hf).
- exists (S f).
- rewrite <- plus_n_Sm with (n:= S a) (m:= S f).
- rewrite <- plus_n_Sm with (n:= 0) (m:= b).
- apply eq_S.
- assumption.
- intro.
- unfold eqz.
- simpl.
- simpl in L.
- apply L.
- Qed.
- Lemma zsign_zero: zsign O_Z = O_Z.
- Proof.
- simpl.
- reflexivity.
- Qed.
- Lemma zsign_positive: forall n:nat, zsign (S n, 0) = (1,0).
- Proof.
- intros.
- unfold zsign.
- simpl.
- reflexivity.
- Qed.
- Lemma zsign_negative: forall n:nat, zsign (0, S n) = (0,1).
- Proof.
- intros.
- unfold zsign.
- simpl.
- reflexivity.
- Qed.
- Ltac zrac m n:= rewrite zsign_compat with (x:=m) (y:=n).
- Lemma zsign_morphism: forall x y:Relative_integer, (zsign (x *Z y)) = (zsign x) *Z (zsign y).
- Proof.
- intros.
- destruct cases_sign with (x:=x).
- apply eq_trans with (y:= zsign (O_Z *Z y)).
- apply zsign_compat.
- apply Z_mult_compatibility.
- assumption.
- zer.
- rewrite zsign_compat with (x:=x) (y:= O_Z).
- rewrite zsign_compat with (x:= O_Z *Z y) (y:= O_Z).
- rewrite zsign_zero.
- unfold Z_mult.
- simpl.
- reflexivity.
- zet (y *Z O_Z).
- zcom.
- apply Z_zero_product.
- assumption.
- destruct cases_sign with (x:=y).
- apply eq_trans with (y:= zsign (x *Z O_Z)).
- apply zsign_compat.
- apply Z_mult_compatibility.
- zer.
- assumption.
- rewrite zsign_compat with (x:=y) (y:= O_Z).
- rewrite zsign_compat with (x:= x *Z O_Z) (y:= O_Z).
- unfold Z_mult.
- simpl.
- mom (fst (zsign x)) 0.
- mom (snd (zsign x)) 0.
- simpl.
- rewrite zsign_zero.
- reflexivity.
- apply Z_zero_product.
- assumption.
- destruct H.
- destruct H as(p,Hp).
- destruct H0.
- destruct H as (q, Hq).
- zrac x (S p,0).
- zrac y (S q,0).
- zrac (x *Z y) ((S p, 0) *Z (S q, 0)).
- unfold Z_mult.
- simpl.
- mom p 0.
- simpl.
- apply zsign_positive.
- apply Z_mult_compatibility.
- assumption.
- assumption.
- assumption.
- assumption.
- destruct H as (q, Hq).
- zrac x (S p,0).
- zrac y (0,S q).
- zrac (x *Z y) ((S p, 0) *Z (0, S q)).
- unfold Z_mult.
- simpl.
- mom p 0.
- simpl.
- apply zsign_negative.
- apply Z_mult_compatibility.
- assumption.
- assumption.
- assumption.
- assumption.
- destruct H as(p,Hp).
- destruct H0.
- destruct H as (q, Hq).
- zrac x (0, S p).
- zrac y (S q,0).
- zrac (x *Z y) ((0, S p) *Z (S q, 0)).
- unfold Z_mult.
- simpl.
- mom p 0.
- simpl.
- apply zsign_negative.
- apply Z_mult_compatibility.
- assumption.
- assumption.
- assumption.
- assumption.
- destruct H as (q, Hq).
- zrac x (0, S p).
- zrac y (0,S q).
- zrac (x *Z y) ((0, S p) *Z (0, S q)).
- unfold Z_mult.
- simpl.
- mom p 0.
- simpl.
- apply zsign_positive.
- apply Z_mult_compatibility.
- assumption.
- assumption.
- assumption.
- assumption.
- Qed.
- Lemma zsign_involution: forall x:Relative_integer, zsign (zsign x) = (zsign x).
- Proof.
- intros.
- destruct cases_sign with (x:=x).
- zrac x O_Z.
- compute.
- reflexivity.
- assumption.
- destruct H.
- destruct H as (p,Hp).
- zrac x (S p,0).
- compute.
- reflexivity.
- assumption.
- destruct H as (q,Hq).
- zrac x (0,S q).
- compute.
- reflexivity.
- assumption.
- Qed.
- End Signs_of_relative_integers.
- (* ****** BONUS ******
- In the section below, we build a counter-example to the following fallacy seen on a forum:
- "the distributivity of the product over the sum is equivalent to the sign rule"
- *)
- Section bonus_signs.
- Let D_map (x y:Relative_integer):= zsign x *Z zsign y.
- Ltac zrac m n:= rewrite zsign_compat with (x:=m) (y:=n).
- Lemma D_associative: forall x y z:Relative_integer, D_map (D_map x y) z = D_map x (D_map y z).
- Proof.
- intros.
- unfold D_map.
- apply eq_trans with (y:= zsign (zsign x *Z zsign y) *Z (zsign (zsign z))).
- apply f_equal.
- apply eq_sym.
- apply zsign_involution.
- apply eq_trans with (y:= zsign ((zsign x *Z zsign y) *Z (zsign z))).
- apply eq_sym.
- apply zsign_morphism.
- apply eq_trans with (y:= zsign (zsign x) *Z (zsign (zsign y *Z zsign z))).
- apply eq_trans with (y:= zsign ((zsign x) *Z (zsign y *Z zsign z))).
- apply zsign_compat.
- zes.
- apply Z_mult_associative.
- apply zsign_morphism.
- rewrite zsign_involution with (x:=x).
- reflexivity.
- Qed.
- Lemma D_commutative: forall x y:Relative_integer, D_map x y = D_map y x.
- Proof.
- intros.
- unfold D_map.
- rewrite <- zsign_morphism.
- rewrite <- zsign_morphism.
- apply zsign_compat.
- zcom.
- Qed.
- Lemma D_zero: forall x:Relative_integer, D_map x O_Z = O_Z.
- Proof.
- intros.
- unfold D_map.
- rewrite <- zsign_morphism.
- zrac (x *Z O_Z) O_Z.
- apply zsign_zero.
- apply Z_zero_product.
- Qed.
- Lemma D_sign_rule: forall x y:Relative_integer, D_map x y = D_map (Z_opp x) (Z_opp y).
- Proof.
- intros.
- unfold D_map.
- rewrite <- zsign_morphism.
- rewrite <- zsign_morphism.
- apply zsign_compat.
- zes.
- apply sign_rule.
- Qed.
- Lemma D_compat:forall x x' y y':Relative_integer, ((x =Z x')/\(y =Z y'))-> D_map x y = D_map x' y'.
- Proof.
- intros.
- unfold D_map.
- rewrite <- zsign_morphism.
- rewrite <- zsign_morphism.
- apply zsign_compat.
- apply Z_mult_compatibility.
- apply H.
- apply H.
- Qed.
- Theorem sign_counter_example: exists D: Relative_integer -> Relative_integer -> Relative_integer,
- (forall x x' y y':Relative_integer, ((x =Z x')/\(y =Z y'))-> D x y =Z D x' y')/\
- (forall x y:Relative_integer, D x y =Z D(Z_opp x) (Z_opp y)) /\
- (forall p q r:Relative_integer, D p (D q r) =Z D (D p q) r) /\
- (forall x y:Relative_integer, D x y =Z D y x) /\
- (forall x:Relative_integer, D x (0,0) =Z (0,0)) /\
- (~(D (I_Z +Z I_Z) I_Z) =Z (D I_Z I_Z) +Z (D I_Z I_Z)).
- Proof.
- assert (forall x y:Relative_integer, x = y -> x =Z y) as R.
- intros.
- rewrite H.
- zer.
- exists D_map.
- split.
- intros.
- apply R.
- unfold D_map.
- apply D_compat.
- assumption.
- split.
- intros.
- apply R.
- apply D_sign_rule.
- split.
- intros.
- apply R.
- apply eq_sym.
- apply D_associative.
- split.
- intros.
- apply R.
- apply D_commutative.
- split.
- intros.
- apply R.
- apply D_zero.
- compute.
- discriminate.
- Qed.
- End bonus_signs.
- Section nat_embedding.
- Definition n_to_z (x:nat):Relative_integer:= (x,0).
- Theorem n_to_z_injective: forall x y:nat, (n_to_z x) =Z (n_to_z y) -> x = y.
- Proof.
- intro.
- intro.
- unfold n_to_z.
- unfold eqz.
- simpl.
- com x 0.
- com y 0.
- simpl.
- intro.
- assumption.
- Qed.
- Theorem n_to_z_zero: n_to_z 0 =Z O_Z.
- Proof.
- unfold n_to_z.
- unfold eqz.
- simpl.
- reflexivity.
- Qed.
- Theorem n_to_z_one: n_to_z 1 =Z I_Z.
- Proof.
- unfold n_to_z.
- unfold eqz.
- simpl.
- reflexivity.
- Qed.
- Theorem n_to_z_sum: forall x y:nat, n_to_z (x + y) =Z (n_to_z x) +Z (n_to_z y).
- Proof.
- unfold n_to_z.
- unfold eqz.
- intros.
- simpl.
- reflexivity.
- Qed.
- Theorem n_to_z_product: forall x y:nat, n_to_z (x * y) =Z (n_to_z x) *Z (n_to_z y).
- Proof.
- unfold n_to_z.
- unfold eqz.
- intros.
- simpl.
- mom x 0.
- simpl.
- com (x * y + 0) 0.
- simpl.
- reflexivity.
- Qed.
- Theorem n_generates_z: forall x:Relative_integer, exists m n:nat, x +Z (n_to_z m) =Z (n_to_z n).
- Proof.
- intros.
- destruct x as (p,q).
- exists q.
- exists p.
- unfold n_to_z.
- unfold eqz.
- simpl.
- alr p q 0.
- reflexivity.
- Qed.
- (*The above theorem states that every relative integer is the difference of two natural
- integers.*)
- End nat_embedding.
- (*
- (*Uncomment this part if you want to use the ring library, declare nat as a semi ring
- and Relative_integer as a ring and incorporate rings tactics *)
- Require Import Ring.
- Theorem nat_semi_ring: @semi_ring_theory nat 0 1 plus mult eq.
- Proof.
- split.
- apply nsr_O_plus_neutral.
- apply nsr_plus_commutative.
- apply nsr_plus_associative.
- apply nsr_I_mult_neutral.
- apply nsr_O_absorbs.
- apply nsr_mult_commutative.
- apply nsr_mult_associative.
- apply nsr_right_distributivity.
- Qed.
- Add Ring the_set_of_natural_integers_is_a_semi_ring: nat_semi_ring.
- Require Import Setoid.
- Lemma equiv_eqz: Equivalence eqz.
- Proof.
- split.
- unfold Reflexive.
- apply eqz_reflexive.
- unfold Symmetric.
- apply eqz_symmetric.
- unfold Transitive.
- apply eqz_transitive.
- Qed.
- Theorem Z_ring: @ring_theory Relative_integer O_Z I_Z Z_plus Z_mult Z_minus Z_opp eqz.
- Proof.
- split.
- apply Z_zero_plus_neutral.
- apply Z_plus_commutative.
- apply Z_plus_associative.
- apply Z_un_neutral.
- apply Z_mult_commutative.
- apply Z_mult_associative.
- apply Z_right_distributivity.
- apply Z_minus_opp.
- apply Z_opp_group.
- Qed.
- Lemma Z_compatibility: ring_eq_ext Z_plus Z_mult Z_opp eqz.
- Proof.
- unfold Morphisms.Proper.
- unfold Morphisms.respectful.
- split.
- unfold Morphisms.Proper.
- unfold Morphisms.respectful.
- intro.
- intro.
- intros.
- apply Z_sum_compatibility.
- assumption.
- assumption.
- unfold Morphisms.Proper.
- unfold Morphisms.respectful.
- intros.
- apply Z_mult_compatibility.
- assumption.
- assumption.
- unfold Morphisms.Proper.
- unfold Morphisms.respectful.
- apply Z_opp_compatibility.
- Qed.
- *)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement