helm/software/matita/library/Q/q/qtimes.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Q/q/qinv.ma".
  16 include "Q/ratio/rtimes.ma".
  17
  18 definition Qtimes : Q \to Q \to Q \def
  19 \lambda p,q.
  20   match p with
  21   [OQ \Rightarrow OQ
  22   |Qpos p1 \Rightarrow
  23     match q with
  24     [OQ \Rightarrow OQ
  25     |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
  26     |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
  27     ]
  28   |Qneg p1 \Rightarrow
  29     match q with
  30     [OQ \Rightarrow OQ
  31     |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)
  32     |Qneg q1 \Rightarrow Qpos (rtimes p1 q1)
  33     ]
  34   ].
  35
  36 interpretation "rational times" 'times x y = (Qtimes x y).
  37
  38 theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
  39  intro;
  40  elim q;
  41  reflexivity.
  42 qed.
  43
  44 theorem symmetric_Qtimes: symmetric ? Qtimes.
  45  intros 2;
  46  elim x;
  47   [ rewrite > Qtimes_q_OQ; reflexivity
  48   |*:elim y;
  49      simplify;
  50      try rewrite > sym_rtimes;
  51      reflexivity
  52   ]
  53 qed.
  54
  55 theorem Qtimes_q_Qone: ∀q.q * Qone = q.
  56  intro.cases q
  57   [reflexivity
  58   |2,3: cases r; reflexivity
  59   ]
  60 qed.
  61
  62 theorem Qtimes_Qone_q: ∀q.Qone * q = q.
  63  intro.cases q
  64   [reflexivity
  65   |2,3: cases r; reflexivity
  66   ]
  67 qed.
  68
  69 theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one.
  70  intro;
  71  elim q;
  72   [ elim H; reflexivity
  73   |*:simplify;
  74      rewrite > rtimes_rinv;
  75      reflexivity
  76   ]
  77 qed.
  78
  79 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
  80 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
  81 intros.
  82 cases f;simplify
  83   [reflexivity
  84   |cases g;reflexivity
  85   |cases g;simplify
  86     [reflexivity
  87     |reflexivity
  88     |rewrite > times_f_ftimes.reflexivity]]
  89 qed.
  90
  91 theorem times_Qtimes: \forall p,q.
  92 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
  93 intros.unfold nat_to_Q.
  94 rewrite < times_fa_Qtimes.
  95 rewrite < eq_times_times_fa.
  96 reflexivity.
  97 qed.
  98
  99 theorem associative_Qtimes:associative ? Qtimes.
 100 unfold.intros.
 101 cases x
 102   [reflexivity
 103    (* non posso scrivere 2,3: ... ?? *)
 104   |cases y
 105     [reflexivity.
 106     |cases z
 107       [reflexivity
 108       |simplify.rewrite > associative_rtimes.
 109        reflexivity.
 110       |simplify.rewrite > associative_rtimes.
 111        reflexivity
 112       ]
 113     |cases z
 114       [reflexivity
 115       |simplify.rewrite > associative_rtimes.
 116        reflexivity.
 117       |simplify.rewrite > associative_rtimes.
 118        reflexivity
 119       ]
 120     ]
 121   |cases y
 122     [reflexivity.
 123     |cases z
 124       [reflexivity
 125       |simplify.rewrite > associative_rtimes.
 126        reflexivity.
 127       |simplify.rewrite > associative_rtimes.
 128        reflexivity
 129       ]
 130     |cases z
 131       [reflexivity
 132       |simplify.rewrite > associative_rtimes.
 133        reflexivity.
 134       |simplify.rewrite > associative_rtimes.
 135        reflexivity]]]
 136 qed.
 137
 138 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
 139 Qtimes p q = OQ \to p = OQ \lor q = OQ.
 140 intros 2.
 141 cases p
 142   [intro.left.reflexivity
 143   |cases q
 144     [intro.right.reflexivity
 145     |simplify.intro.destruct H
 146     |simplify.intro.destruct H
 147     ]
 148   |cases q
 149     [intro.right.reflexivity
 150     |simplify.intro.destruct H
 151     |simplify.intro.destruct H]]
 152 qed.
 153
 154 theorem Qinv_Qtimes: \forall p,q.
 155 p \neq OQ \to q \neq OQ \to Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
 156 intros.
 157 rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
 158 rewrite < (Qtimes_Qinv (Qtimes p q))
 159   [lapply (Qtimes_Qinv ? H).
 160    lapply (Qtimes_Qinv ? H1).
 161    rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
 162    rewrite > associative_Qtimes.
 163    rewrite > associative_Qtimes.
 164    rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 165    rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
 166    rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
 167    rewrite > Hletin1.
 168    rewrite > Qtimes_q_Qone.
 169    rewrite > Hletin.
 170    rewrite > Qtimes_q_Qone.
 171    reflexivity
 172   |intro.
 173    elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
 174     [apply (H H3)|apply (H1 H3)]]
 175 qed.
 176
 177 (* a stronger version, taking advantage of inv(O) = O *)
 178 theorem Qinv_Qtimes': \forall p,q. Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q).
 179 intros.
 180 cases p
 181   [reflexivity
 182   |cases q
 183     [reflexivity
 184     |apply Qinv_Qtimes;intro;destruct H
 185     |apply Qinv_Qtimes;intro;destruct H
 186     ]
 187   |cases q
 188     [reflexivity
 189     |apply Qinv_Qtimes;intro;destruct H
 190     |apply Qinv_Qtimes;intro;destruct H]]
 191 qed.
 192
 193 theorem Qtimes_numerator_denominator: ∀f:fraction.
 194   Qtimes (nat_fact_all_to_Q (numerator f)) (Qinv (nat_fact_all_to_Q (denominator f)))
 195   = Qpos (frac f).
 196 simplify.
 197 intro.elim f
 198   [reflexivity
 199   |reflexivity
 200   |elim (or_numerator_nfa_one_nfa_proper f1)
 201     [elim H1.clear H1.
 202      elim H3.clear H3.
 203      cut (finv (nat_fact_to_fraction a) = f1)
 204       [elim z;
 205        simplify;
 206        rewrite > H2;rewrite > H1;simplify;
 207        rewrite > Hcut;reflexivity
 208       |generalize in match H.
 209        rewrite > H2.rewrite > H1.simplify.
 210        intro.destruct H3.reflexivity
 211       ]
 212     |elim H1;clear H1;
 213      elim z
 214       [*:simplify;
 215        rewrite > H2;simplify;
 216        elim (or_numerator_nfa_one_nfa_proper (finv f1))
 217         [1,3,5:elim H1;clear H1;
 218          rewrite > H3;simplify;
 219          cut (nat_fact_to_fraction a = f1)
 220           [1,3,5:rewrite > Hcut;reflexivity
 221           |*:generalize in match H;
 222            rewrite > H2;
 223            rewrite > H3;
 224            rewrite > Qtimes_q_Qone;
 225            intro;
 226            simplify in H1;
 227            destruct H1;
 228            reflexivity
 229           ]
 230         |*:elim H1;clear H1;
 231          generalize in match H;
 232          rewrite > H2;
 233          rewrite > H3;simplify;
 234          intro;
 235          destruct H1;
 236          rewrite > Hcut;
 237          simplify;reflexivity
 238         ]]]]
 239 qed.
 240
 241