Library Corps_tes


Require Relation_Definitions.




Parameter Q:Set.

Parameter OQ:Q.

Parameter multQ_neg: Q -> Q.

Parameter plusQ: Q->Q->Q.

Parameter multQ: Q->Q->Q.

Parameter invQ: Q -> Q.

Parameter unQ: Q.




Parameter eqQ: Q->Q->Prop.




Axiom no_trivial: ~(eqQ unQ OQ).

Hints Resolve no_trivial.




Parameter eqQ_refl: (reflexive Q eqQ).

Hints Resolve eqQ_refl.




Parameter eqQ_sym: (symmetric Q eqQ).

Hints Resolve eqQ_sym.




Parameter eqQ_trans: (transitive Q eqQ).

Hints Resolve eqQ_trans.




Parameter plusQ_conm: (k,k':Q)(eqQ (plusQ k k') (plusQ k' k)).

Hints Resolve plusQ_conm.




Parameter plusQ_assoc: (k1,k2,k3:Q)(eqQ (plusQ k1 (plusQ k2 k3))

                         (plusQ (plusQ k1 k2) k3)).

Hints Resolve plusQ_assoc.




Parameter neut_plusQ: (k:Q)(eqQ (plusQ k OQ) k).

Hints Resolve neut_plusQ.




Parameter ex_op: (k:Q) (eqQ (plusQ k (multQ_neg k)) OQ).

Hints Resolve ex_op.




Parameter multQ_conm: (k,k':Q)(eqQ (multQ k k') (multQ k' k)).

Hints Resolve multQ_conm.




Parameter multQ_assoc: (k1,k2,k3:Q)(eqQ (multQ k1 (multQ k2 k3))

                         (multQ (multQ k1 k2) k3)).

Hints Resolve multQ_assoc.




Parameter neut_multQ: (k:Q)(eqQ (multQ k unQ) k).

Hints Resolve neut_multQ.




Parameter inv_divQ:(k:Q)(~(eqQ k OQ))->

(eqQ (multQ k (invQ k)) unQ).

Hints Resolve inv_divQ.




Parameter distrQ: (k1,k2,k3:Q) (eqQ (multQ k1 (plusQ k2 k3))

                               (plusQ (multQ k1 k2) (multQ k1 k3))).

Hints Resolve distrQ.




Parameter decQ: (k:Q){eqQ k OQ}+{~(eqQ k OQ)}.

Hints Resolve decQ.




Axiom plusQ_comp_r: (k,k':Q)(eqQ k k')->(y:Q)(eqQ (plusQ k y) (plusQ k' y)).

Hints Resolve plusQ_comp_r.




Axiom multQ_comp_r: (k,k':Q)(eqQ k k')->(y:Q)(eqQ (multQ k y) (multQ k' y)).

Hints Resolve multQ_comp_r.




Definition divQ:= [k1,k2:Q] (multQ k1 (invQ k2)).

Hints Unfold divQ.




Lemma division:(k1,k2:Q) (~(eqQ k2 OQ)) ->(eqQ (divQ k1 k2) (multQ k1 (divQ unQ k2))).




Intros.

Unfold divQ.

(Apply eqQ_trans with (multQ (multQ k1 unQ) (invQ k2)); Auto).

Save.

Hints Resolve division.




Lemma comp_nOQ: (c,c':Q)(eqQ c c')->(~(eqQ c OQ))->

   (~(eqQ c' OQ)).




Intros.

Red in H0.

Red; Intros.

Apply H0.

Apply eqQ_trans with c'; Trivial.




Save.

Hints Resolve comp_nOQ.




Lemma plusQ_comp_l: (k,k':Q)(eqQ k k')->(y:Q)(eqQ (plusQ y k) (plusQ y k')).




Intros.

Apply eqQ_trans with (plusQ k y); Auto.

Apply eqQ_trans with (plusQ k' y); Auto.

Save.

Hints Resolve plusQ_comp_l.




Lemma suma_igual:(k,k',y:Q)(eqQ (plusQ k y) (plusQ k' y)) ->(eqQ k k').




Intros.

Cut (eqQ (plusQ k (plusQ y (multQ_neg y)))

      (plusQ k' (plusQ y (multQ_neg y)))); Intros.

Apply eqQ_trans with (plusQ k' (plusQ y (multQ_neg y))).

Apply eqQ_trans with (plusQ k (plusQ y (multQ_neg y))); Auto.

Apply eqQ_trans with (plusQ k OQ); Auto.




Apply eqQ_trans with (plusQ k' OQ); Auto.




Apply eqQ_trans with (plusQ (plusQ k y) (multQ_neg y)); Auto.

Apply eqQ_trans with (plusQ (plusQ k' y) (multQ_neg y)); Auto.




Save.

Hints Resolve suma_igual.




Lemma multQ_comp_l: (k,k':Q)(eqQ k k')->

 (y:Q)(eqQ (multQ y k) (multQ y k')).




Intros.

Apply eqQ_trans with (multQ k y); Auto.

Apply eqQ_trans with (multQ k' y); Auto.

Save.

Hints Resolve multQ_comp_l.




Lemma plusQ_comp: (k,k',c,c':Q)(eqQ k k')->(eqQ c c')->

   (eqQ (plusQ k c) (plusQ k' c')).




Intros.

Apply eqQ_trans with (plusQ k' c); Auto.




Save.

Hints Resolve plusQ_comp.




Lemma multQ_comp: (k,k',c,c':Q)(eqQ k k')->(eqQ c c')->

   (eqQ (multQ k c) (multQ k' c')).




Intros.

(Apply eqQ_trans with (multQ k' c); Auto).

Save.

Hints Resolve multQ_comp.




Lemma suma_op: (c,c':Q)(eqQ c (multQ_neg c'))->

   (eqQ (plusQ c c') OQ).




Intros.

Apply eqQ_trans with (plusQ (multQ_neg c') c'); Auto.

Apply eqQ_trans with (plusQ c' (multQ_neg c')); Auto.




Save.

Hints Resolve suma_op.




Lemma suma_op_inv: (c,c':Q)(eqQ (plusQ c c') OQ)->

   (eqQ c (multQ_neg c')).




Intros.

Apply eqQ_trans with (plusQ c (plusQ c' (multQ_neg c'))).

Apply eqQ_trans with (plusQ c OQ); Auto.




Apply eqQ_trans with (plusQ (plusQ c c') (multQ_neg c')); Auto.

Apply eqQ_trans with (plusQ OQ (multQ_neg c')); Auto.

Apply eqQ_trans with (plusQ (multQ_neg c') OQ); Auto.




Save.

Hints Resolve suma_op_inv.




Lemma neg_OQ: (eqQ (multQ_neg OQ) OQ).




Auto.




Save.

Hints Resolve neg_OQ.




Lemma plusQ_zero: (c,c':Q)(eqQ c OQ)->(eqQ c' OQ)->

   (eqQ (plusQ c c') OQ).




Intros.

Apply eqQ_trans with (plusQ c OQ); Auto.

Apply eqQ_trans with c; Auto.




Save.

Hints Resolve plusQ_zero.




Lemma plusQ_zero_nzero: (c,c':Q)(eqQ c OQ)->(~(eqQ c' OQ))->

   (~(eqQ (plusQ c c') OQ)).




Intros.

(Apply comp_nOQ with c'; Auto).

(Apply eqQ_trans with (plusQ OQ c'); Auto).

(Apply eqQ_trans with (plusQ c' OQ); Auto).




Save.

Hints Resolve plusQ_zero_nzero.




Lemma multQ_n_OQ: (c:Q)(~(eqQ c OQ))->(~(eqQ (multQ_neg c) OQ)).




Intros.

Red in H.

Red; Intros.

Apply H.

Apply eqQ_trans with (plusQ c (multQ_neg c)); Auto.

Apply eqQ_trans with (plusQ c OQ); Auto.




Save.

Hints Resolve multQ_n_OQ.




Lemma neg_neg_Q: (c:Q)(eqQ c (multQ_neg (multQ_neg c))).




Auto.




Save.

Hints Resolve neg_neg_Q.




Lemma multQ_zero:(c:Q)(eqQ (multQ c OQ) OQ).




Intros.

(Cut (eqQ (multQ_neg (multQ c OQ)) (multQ_neg (multQ c OQ))); Intros;

 Auto).

(Cut (eqQ (multQ c OQ) (plusQ (multQ c OQ) (multQ c OQ))); Intros).

(Cut (eqQ (plusQ (multQ_neg (multQ c OQ)) (multQ c OQ))

       (plusQ (multQ_neg (multQ c OQ))

         (plusQ (multQ c OQ) (multQ c OQ)))); Intros; Auto).

(Cut (eqQ (plusQ (multQ_neg (multQ c OQ)) (multQ c OQ))

       (plusQ (plusQ (multQ_neg (multQ c OQ)) (multQ c OQ))

         (multQ c OQ))); Intros).

(Apply eqQ_trans with (plusQ (multQ c OQ) OQ); Auto).

(Apply eqQ_trans with (plusQ (multQ_neg (multQ c OQ)) (multQ c OQ));

 Auto).

(Apply eqQ_trans

  with (plusQ (plusQ (multQ_neg (multQ c OQ)) (multQ c OQ))

         (multQ c OQ)); Auto).

(Apply eqQ_trans with (plusQ OQ (multQ c OQ)); Auto).




(Apply eqQ_trans

  with (plusQ (multQ_neg (multQ c OQ))

         (plusQ (multQ c OQ) (multQ c OQ))); Auto).




(Apply eqQ_trans with (multQ c (plusQ OQ OQ)); Auto).




Save.

Hints Resolve multQ_zero.




Lemma multQ_neg_unQ: (k:Q)(eqQ (multQ k (multQ_neg unQ))

                  (multQ_neg k)).




Intros.

Apply suma_op_inv.

(Apply eqQ_trans with (plusQ (multQ k (multQ_neg unQ)) (multQ k unQ));

 Auto).

(Apply eqQ_trans with (multQ k (plusQ (multQ_neg unQ) unQ)); Auto).

(Apply eqQ_trans with (multQ k OQ); Auto).

Save.

Hints Resolve multQ_neg_unQ.




Lemma multQ_neg_plusQ: (c,c':Q)(eqQ (multQ_neg (plusQ c c'))

   (plusQ (multQ_neg c) (multQ_neg c'))).




Intros.

Apply eqQ_trans with (multQ (plusQ c c') (multQ_neg unQ)); Auto.

Apply eqQ_trans with (multQ (multQ_neg unQ) (plusQ c c')); Auto.

Apply eqQ_trans

  with (plusQ (multQ (multQ_neg unQ) c) (multQ (multQ_neg unQ) c'));

 Auto.

Apply plusQ_comp.

Apply eqQ_trans with (multQ c (multQ_neg unQ)); Auto.




Apply eqQ_trans with (multQ c' (multQ_neg unQ)); Auto.




Save.

Hints Resolve multQ_neg_plusQ.




Lemma multQ_neg1: (c,c':Q)(eqQ (multQ_neg (multQ c c'))

   (multQ (multQ_neg c) c')).




Intros.

Apply eqQ_trans with (multQ (multQ c c') (multQ_neg unQ)); Auto.

Apply eqQ_trans with (multQ (multQ c (multQ_neg unQ)) c'); Auto.

Apply eqQ_trans with (multQ c (multQ (multQ_neg unQ) c')); Auto.

Apply eqQ_trans with (multQ c (multQ c' (multQ_neg unQ))); Auto.




Save.

Hints Resolve multQ_neg1.




Lemma multQ_neg2: (c,c':Q)(eqQ (multQ_neg (multQ c c'))

   (multQ c (multQ_neg c'))).




Intros.

(Apply eqQ_trans with (multQ (multQ c c') (multQ_neg unQ)); Auto).

(Apply eqQ_trans with (multQ c (multQ c' (multQ_neg unQ))); Auto).

Save.

Hints Resolve multQ_neg2.




Lemma eq_mulQ_neg: (c,c':Q)(eqQ c c')->(eqQ (multQ_neg c') (multQ_neg c)).




Intros.

Apply eqQ_trans with (multQ (multQ_neg unQ) c).

Apply eqQ_trans with (multQ (multQ_neg unQ) c'); Auto.

Apply eqQ_trans with (multQ c' (multQ_neg unQ)); Auto.




Apply eqQ_trans with (multQ c (multQ_neg unQ)); Auto.




Save.

Hints Resolve eq_mulQ_neg.




Lemma nuevo1: (c1:Q)~(eqQ c1 OQ)->(eqQ unQ (multQ c1 (divQ unQ c1))).




Intros.

(Apply eqQ_trans with (multQ c1 (invQ c1)); Auto).

Apply multQ_comp_l.

Unfold divQ.

(Apply eqQ_trans with (multQ (invQ c1) unQ); Auto).

Save.

Hints Resolve eq_mulQ_neg.




Lemma igual:(c1,c2,x,y:Q)(eqQ c1 c2) ->(~(eqQ c1 OQ))->

 (eqQ (multQ c1 x) (multQ c2 y))->(eqQ x y).




Intros.

Apply eqQ_trans with (multQ (divQ unQ c1) (multQ c2 y)).

(Apply eqQ_trans with (multQ (divQ unQ c1) (multQ c1 x)); Auto).

(Apply eqQ_trans with (multQ (multQ (divQ unQ c1) c1) x); Auto).

(Apply eqQ_trans with (multQ x unQ); Auto).

(Apply eqQ_trans with (multQ unQ x); Auto).

Apply multQ_comp_r.

(Apply eqQ_trans with (multQ c1 (divQ unQ c1)); Auto).

(Apply eqQ_trans with (multQ c1 (invQ c1)); Auto).

Apply multQ_comp_l.

Unfold divQ.

(Apply eqQ_trans with (multQ (invQ c1) unQ); Auto).




(Apply eqQ_trans with (multQ (multQ (divQ unQ c1) c2) y); Auto).

Apply eqQ_trans with (multQ unQ y).

Apply multQ_comp_r.

(Apply eqQ_trans with (multQ (divQ unQ c1) c1); Auto).

(Apply eqQ_trans with (multQ c1 (divQ unQ c1)); Auto).

(Apply eqQ_trans with (multQ c1 (invQ c1)); Auto).

Apply multQ_comp_l.

Unfold divQ.

(Apply eqQ_trans with (multQ (invQ c1) unQ); Auto).




(Apply eqQ_trans with (multQ y unQ); Auto).




Save.

Hints Resolve igual.




Lemma zero_multQ: (c,c':Q)((eqQ c OQ)\/(eqQ c' OQ))->(eqQ (multQ c c') OQ).




Intros.

Elim H; Intros.

Apply eqQ_trans with (multQ OQ c'); Auto.

Apply eqQ_trans with (multQ c' OQ); Auto.




Apply eqQ_trans with (multQ c OQ); Auto.




Save.

Hints Resolve zero_multQ.




Lemma resul_multQ_zero:(c1,c2:Q)(~(eqQ (multQ c1 c2) OQ))->

 (~(eqQ c1 OQ))/\(~(eqQ c2 OQ)).




Intros.

Split.

Red in H.

Red; Intros.

Apply H; Auto.




Red in H.

Red; Intros.

Apply H; Auto.




Save.

Hints Resolve resul_multQ_zero.




Lemma no_zero_invQ: (c:Q)(~(eqQ c OQ))->~(eqQ (invQ c) OQ).




Intros.

(Cut ~(eqQ (multQ c (invQ c)) OQ); Auto).

(Apply comp_nOQ with unQ; Auto).

Save.

Hints Resolve no_zero_invQ.




Lemma multQ_n_z: (c,c':Q)(~(eqQ c OQ))->(~(eqQ c' OQ))->

                  (~(eqQ (multQ c c') OQ)).




Intros.

(Cut (eqQ (multQ c (invQ c)) unQ); Intros; Auto).

(Red; Intros).

(Cut (eqQ c' (multQ (multQ (invQ c) c) c')); Intros).

(Cut (eqQ c' OQ); Intros; Auto).

(Apply eqQ_trans with (multQ (multQ (invQ c) c) c'); Auto).

(Apply eqQ_trans with (multQ (invQ c) (multQ c c')); Auto).




(Apply eqQ_trans with (multQ c' unQ); Auto).

(Apply eqQ_trans with (multQ c' (multQ (invQ c) c)); Auto).

(Apply multQ_comp_l; Auto).

(Apply eqQ_trans with (multQ c (invQ c)); Auto).




Save.

Hints Resolve multQ_n_z.




Lemma div_Q_eq: (c:Q)(~(eqQ c OQ))->(eqQ unQ (divQ c c)).




Intros.

(Apply eqQ_trans with (multQ c (invQ c)); Auto).




Save.

Hints Resolve div_Q_eq.




Lemma multQ_divQ1: (c,c1,c2:Q)(~(eqQ c OQ))->

   (eqQ (multQ (divQ c1 c) c2) (divQ (multQ c1 c2) c)).




Intros.

Apply eqQ_trans with (multQ (divQ unQ c) (multQ c1 c2)).

Apply eqQ_trans with (multQ (multQ (divQ unQ c) c1) c2); Auto.

Apply multQ_comp_r.

Apply eqQ_trans with (multQ c1 (divQ unQ c)); Auto.




Apply eqQ_trans with (multQ (multQ c1 c2) (divQ unQ c)); Auto.




Save.

Hints Resolve multQ_divQ1.




Lemma ec_invQ: (c1,c2:Q)(eqQ (multQ c1 c2) unQ)->(eqQ c2 (invQ c1)).




Intros.

(Cut (eqQ (multQ (multQ (invQ c1) c1) c2) (invQ c1)); Intros).

(Apply eqQ_trans with (multQ (multQ (invQ c1) c1) c2); Trivial).

Apply eqQ_trans with (multQ unQ c2).

(Apply eqQ_trans with (multQ c2 unQ); Auto).




(Apply multQ_comp; Auto).

(Apply eqQ_trans with (multQ c1 (invQ c1)); Auto).

Apply eqQ_sym.

Apply inv_divQ.

(Cut ~(eqQ c1 OQ)/\~(eqQ c2 OQ); Intros).

(Elim H1; Trivial).




Apply resul_multQ_zero.

(Apply comp_nOQ with unQ; Auto).




(Apply eqQ_trans with (multQ (invQ c1) (multQ c1 c2)); Auto).

(Apply eqQ_trans with (multQ (invQ c1) unQ); Auto).

Save.

Hints Resolve ec_invQ.




Lemma eg_denomQ: (c,c1,c2:Q)(~(eqQ c OQ))->(eqQ c1 c2)->

   (eqQ (divQ c1 c) (divQ c2 c)).




Intros.

Apply eqQ_trans with (multQ c1 (divQ unQ c)); Auto.

Apply eqQ_trans with (multQ c2 (divQ unQ c)); Auto.




Save.

Hints Resolve eg_denomQ.




Lemma nuevo2: (c1,c2:Q)(~(eqQ c1 OQ))->(eqQ c1 c2)->

   (eqQ (invQ c1) (invQ c2)).




Intros.

(Cut (eqQ (multQ c1 (divQ c1 c1)) (multQ c2 (divQ c1 c1))); Intros;

 Auto).

(Cut (eqQ (multQ c1 (divQ c2 c2)) (multQ c2 (divQ c2 c2))); Intros;

 Auto).

(Cut (eqQ (multQ (multQ c1 c1) (invQ c1))

       (multQ (multQ c2 c2) (invQ c2))); Intros).

(Apply igual with (multQ c1 c1) (multQ c2 c2); Auto).




(Apply eqQ_trans with (multQ c1 (multQ c1 (invQ c1))); Auto).

(Apply eqQ_trans with (multQ c2 (multQ c2 (invQ c2))); Auto).

(Apply eqQ_trans with (multQ c1 unQ); Auto).

(Apply eqQ_trans with (multQ c2 unQ); Auto).

Apply multQ_comp_l.

Apply eqQ_sym.

Apply inv_divQ.

(Apply comp_nOQ with c1; Auto).

Save.

Hints Resolve nuevo2.




Lemma eg_numeraQ: (c,c1,c2:Q)(~(eqQ c1 OQ))->(eqQ c1 c2)->

   (eqQ (divQ c c1) (divQ c c2)).




Intros.

(Apply eqQ_trans with (multQ c (invQ c1)); Auto).

(Apply eqQ_trans with (multQ c (invQ c2)); Auto).




Save.

Hints Resolve eg_numeraQ.




Lemma divQ_0_n: (q:Q)~(eqQ q OQ)->(eqQ (divQ OQ q) OQ).




Intros.

Apply eqQ_trans with (multQ OQ (invQ q)); Auto.

Save.

Hints Resolve divQ_0_n.




Lemma divQ_0: (q,q0:Q)~(eqQ q OQ)->(eqQ q0 OQ)->(eqQ (divQ q0 q) OQ).




Intros.

Apply eqQ_trans with (multQ q0 (divQ unQ q)); Auto.




Save.

Hints Resolve divQ_0.




Lemma neg_divQ: (k,k':Q)(~(eqQ k' OQ))->(eqQ 

   (multQ_neg (divQ k k')) (divQ (multQ_neg k) k')).




Intros.

Apply eqQ_trans with (multQ (divQ k k') (multQ_neg unQ)); Auto.

Apply eqQ_trans with (multQ (multQ k (divQ unQ k')) (multQ_neg unQ));

 Auto.

Apply eqQ_trans with (multQ (multQ_neg k) (divQ unQ k')); Auto.

Apply eqQ_trans with (multQ (multQ_neg unQ) (multQ k (divQ unQ k')));

 Auto.

Apply eqQ_trans with (multQ (multQ (multQ_neg unQ) k) (divQ unQ k'));

 Auto.

Apply multQ_comp_r.

Apply eqQ_trans with (multQ k (multQ_neg unQ)); Auto.




Save.

Hints Resolve neg_divQ.




Lemma simpl_divQ: (c,c':Q)(~(eqQ c OQ))->(eqQ 

   (divQ (multQ c c') c) c').




Intros.

Apply eqQ_trans with (multQ (divQ c c) c'); Auto.

Apply eqQ_trans with (multQ unQ c'); Auto.

Apply eqQ_trans with (multQ c' unQ); Auto.




Save.

Hints Resolve simpl_divQ.




Lemma distr_divQ: (k,k',q:Q)(~(eqQ q OQ))->

  (eqQ (plusQ (divQ k q) (divQ k' q)) (divQ (plusQ k k') q)).




Intros.

Apply eqQ_trans with (multQ (plusQ k k') (divQ unQ q)); Auto.

Apply eqQ_trans with (multQ (divQ unQ q) (plusQ k k')); Auto.

Apply eqQ_trans

  with (plusQ (multQ (divQ unQ q) k) (multQ (divQ unQ q) k')); 

 Auto.

Apply plusQ_comp.

Apply eqQ_trans with (multQ k (divQ unQ q)); Auto.




Apply eqQ_trans with (multQ k' (divQ unQ q)); Auto.




Save.

Hints Resolve distr_divQ.




Lemma plusQ_frac: (k,k1,k2:Q)(~(eqQ k2 OQ))->(eqQ

   (plusQ k (divQ k1 k2)) (divQ (plusQ (multQ k k2) k1) k2)).




Intros.

Apply eqQ_trans with (multQ (plusQ (multQ k k2) k1) (divQ unQ k2));

 Auto.

Apply eqQ_trans with (multQ (divQ unQ k2) (plusQ (multQ k k2) k1));

 Auto.

Apply eqQ_trans

  with (plusQ (multQ (divQ unQ k2) (multQ k k2))

         (multQ (divQ unQ k2) k1)); Auto.

Apply plusQ_comp.

Apply eqQ_trans with (multQ (multQ k k2) (divQ unQ k2)); Auto.

Apply eqQ_trans with (divQ (multQ k k2) k2); Auto.

Apply eqQ_trans with (divQ (multQ k2 k) k2); Auto.




Apply eqQ_trans with (multQ k1 (divQ unQ k2)); Auto.




Save.

Hints Resolve plusQ_frac.




Lemma no_divQ_zero: (c,c':Q)(~(eqQ c OQ))->

 (~(eqQ c' OQ))->~(eqQ (divQ c c') OQ).




Intros.

Apply comp_nOQ with (multQ c (invQ c')); Auto.

Save.




Lemma decQ_t: (k,k':Q) {eqQ k k'}+{~(eqQ k k')}.




Intros.

(Elim (decQ (plusQ k (multQ_neg k'))); Intros).

Left.

(Apply eqQ_trans with (multQ_neg (multQ_neg k')); Auto).




Right.

(Red; Intros).

Elim b.

Apply suma_op.

(Apply eqQ_trans with k'; Auto).

Save.

Hints Resolve decQ_t.
Index
This page has been generated by coqdoc