helm/software/matita/library/Q/fraction/numerator_denominator.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/fraction/finv.ma".
  16
  17 (* returns the numerator of a fraction in the form of a nat_fact_all *)
  18 let rec numerator f \def
  19   match f with
  20   [pp a \Rightarrow nfa_proper (nf_last a)
  21   |nn a \Rightarrow nfa_one
  22   |cons a l \Rightarrow
  23     let n \def numerator l in
  24     match n with
  25     [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
  26     |nfa_one  \Rightarrow
  27       match a with
  28       [OZ \Rightarrow nfa_one
  29       |pos x \Rightarrow nfa_proper (nf_last x)
  30       |neg x \Rightarrow nfa_one
  31       ]
  32     |nfa_proper g \Rightarrow
  33       match a with
  34       [OZ \Rightarrow nfa_proper (nf_cons O g)
  35       |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
  36       |neg x \Rightarrow nfa_proper (nf_cons O g)
  37       ]]].
  38
  39 definition denominator ≝ λf.numerator (finv f).
  40
  41 theorem not_eq_numerator_nfa_zero: ∀f.numerator f ≠ nfa_zero.
  42 intro.elim f
  43   [simplify.intro.destruct H
  44   |simplify.intro.destruct H
  45   |simplify.generalize in match H.
  46    cases (numerator f1)
  47     [intro.elim H1.reflexivity
  48     |simplify.intro.
  49      cases z;simplify;intro;destruct H2
  50     |simplify.intro.
  51      cases z;simplify;intro;destruct H2]]
  52 qed.
  53
  54 theorem not_eq_denominator_nfa_zero: ∀f.denominator f ≠ nfa_zero.
  55  unfold denominator; intro; apply not_eq_numerator_nfa_zero.
  56 qed.
  57
  58 theorem numerator_nat_fact_to_fraction: ∀g:nat_fact.
  59 numerator (nat_fact_to_fraction g) = nfa_proper g.
  60 intro.
  61 elim g
  62   [simplify.reflexivity.
  63   |simplify.rewrite > H.simplify.
  64    cases n;reflexivity
  65   ]
  66 qed.
  67
  68 theorem denominator_nat_fact_to_fraction: ∀g:nat_fact.
  69 denominator (finv (nat_fact_to_fraction g)) = nfa_proper g.
  70  unfold denominator;
  71  intro;
  72  rewrite > finv_finv;
  73  apply numerator_nat_fact_to_fraction.
  74 qed.
  75
  76 theorem or_numerator_nfa_one_nfa_proper:
  77 ∀f.
  78  (numerator f = nfa_one ∧ ∃g.denominator f = nfa_proper g) ∨
  79  ∃g.numerator f = nfa_proper g.
  80 intro.elim f
  81   [simplify.right.
  82    apply (ex_intro ? ? (nf_last n)).reflexivity
  83   |simplify.left.split
  84     [reflexivity
  85     |apply (ex_intro ? ? (nf_last n)).reflexivity
  86     ]
  87   |elim H;clear H
  88     [elim H1.clear H1.
  89      elim H2.clear H2.
  90      elim z
  91       [simplify.
  92        rewrite > H.rewrite > H1.simplify.
  93        left.split
  94         [reflexivity
  95         |apply (ex_intro ? ? (nf_cons O a)).reflexivity
  96         ]
  97       |simplify.
  98        rewrite > H.rewrite > H1.simplify.
  99        right.apply (ex_intro ? ? (nf_last n)).reflexivity
 100       |simplify.
 101        rewrite > H.rewrite > H1.simplify.
 102        left.split
 103         [reflexivity
 104         |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
 105         ]
 106       ]
 107     |elim H1.clear H1.
 108       elim z
 109       [simplify.
 110        rewrite > H.simplify.
 111        right.
 112        apply (ex_intro ? ? (nf_cons O a)).reflexivity
 113       |simplify.
 114        rewrite > H.simplify.
 115        right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
 116       |simplify.
 117        rewrite > H.simplify.
 118        right.
 119        apply (ex_intro ? ? (nf_cons O a)).reflexivity
 120       ]
 121     ]
 122   ]
 123 qed.
 124
 125 theorem eq_nfa_one_to_eq_finv_nfa_proper:
 126 ∀f.numerator f = nfa_one → ∃h.denominator f = nfa_proper h.
 127   intros;
 128   elim (or_numerator_nfa_one_nfa_proper f); cases H1;
 129    [ assumption
 130    | rewrite > H in H2;
 131      destruct]
 132 qed.