(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Q/frac".
-
-include "nat/factorization.ma".
-include "Q/q.ma".
-
-(* transformation from nat_fact to fracion *)
-let rec nat_fact_to_fraction l \def
- match l with
- [nf_last a \Rightarrow pp a
- |nf_cons a p \Rightarrow
- cons (Z_of_nat a) (nat_fact_to_fraction p)
- ]
-.
-
-(* returns the numerator of a fraction in the form of a nat_fact_all *)
-let rec numerator f \def
- match f with
- [pp a \Rightarrow nfa_proper (nf_last a)
- |nn a \Rightarrow nfa_one
- |cons a l \Rightarrow
- let n \def numerator l in
- match n with
- [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
- |nfa_one \Rightarrow
- match a with
- [OZ \Rightarrow nfa_one
- |pos x \Rightarrow nfa_proper (nf_last x)
- |neg x \Rightarrow nfa_one
- ]
- |nfa_proper g \Rightarrow
- match a with
- [OZ \Rightarrow nfa_proper (nf_cons O g)
- |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
- |neg x \Rightarrow nfa_proper (nf_cons O g)
- ]
- ]
- ]
-.
-
-theorem not_eq_numerator_nfa_zero:
-\forall f.numerator f \neq nfa_zero.
-intro.elim f
- [simplify.intro.destruct H
- |simplify.intro.destruct H
- |simplify.generalize in match H.
- cases (numerator f1)
- [intro.elim H1.reflexivity
- |simplify.intro.
- cases z;simplify;intro;destruct H2
- |simplify.intro.
- cases z;simplify;intro;destruct H2
- ]
- ]
-qed.
-
-theorem or_numerator_nfa_one_nfa_proper:
-\forall f.(numerator f = nfa_one \land \exists g.numerator (finv f) =
-nfa_proper g) \lor \exists g.numerator f = nfa_proper g.
-intro.elim f
- [simplify.right.
- apply (ex_intro ? ? (nf_last n)).reflexivity
- |simplify.left.split
- [reflexivity
- |apply (ex_intro ? ? (nf_last n)).reflexivity
- ]
- |elim H;clear H
- [elim H1.clear H1.
- elim H2.clear H2.
- elim z
- [simplify.
- rewrite > H.rewrite > H1.simplify.
- left.split
- [reflexivity
- |apply (ex_intro ? ? (nf_cons O a)).reflexivity
- ]
- |simplify.
- rewrite > H.rewrite > H1.simplify.
- right.apply (ex_intro ? ? (nf_last n)).reflexivity
- |simplify.
- rewrite > H.rewrite > H1.simplify.
- left.split
- [reflexivity
- |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
- ]
- ]
- |elim H1.clear H1.
- elim z
- [simplify.
- rewrite > H.simplify.
- right.
- apply (ex_intro ? ? (nf_cons O a)).reflexivity
- |simplify.
- rewrite > H.simplify.
- right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
- |simplify.
- rewrite > H.simplify.
- right.
- apply (ex_intro ? ? (nf_cons O a)).reflexivity
- ]
- ]
- ]
-qed.
-
-theorem eq_nfa_one_to_eq_finv_nfa_proper:
-\forall f.numerator f = nfa_one \to
-\exist h.numerator (finv f) = nfa_proper h.
-intro.elim f
- [simplify in H.destruct H
- |simplify.apply (ex_intro ? ? (nf_last n)).reflexivity
- |generalize in match H1.clear H1.
- generalize in match H.clear H.
- simplify.
- cases (numerator f1);simplify
- [intros;destruct H1
- |intros;elim (H (refl_eq ? ?)).
- rewrite > H2.simplify.
- elim z;simplify
- [apply (ex_intro ? ? (nf_cons O a)).reflexivity
- |apply (ex_intro ? ? (nf_cons O a)).reflexivity
- |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
- ]
- |elim z;destruct H1
- ]
- ]
-qed.
-
-theorem numerator_nat_fact_to_fraction: \forall g:nat_fact.
-numerator (nat_fact_to_fraction g) = nfa_proper g.
-intro.
-elim g
- [simplify.reflexivity.
- |simplify.rewrite > H.simplify.
- cases n;reflexivity
- ]
-qed.
-
-definition numeratorQ \def
-\lambda q.match q with
- [OQ \Rightarrow nfa_zero
- |pos r \Rightarrow
- match r with
- [one \Rightarrow nfa_one
- |frac x \Rightarrow numerator x
- ]
- |neg r \Rightarrow
- match r with
- [one \Rightarrow nfa_one
- |frac x \Rightarrow numerator x
- ]
- ]
-.
-
-definition nat_fact_all_to_Q \def
-\lambda n.
- match n with
- [nfa_zero \Rightarrow OQ
- |nfa_one \Rightarrow Qpos one
- |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
- ]
-.
-
-theorem numeratorQ_nat_fact_all_to_Q: \forall g.
-numeratorQ (nat_fact_all_to_Q g) = g.
-intro.cases g
- [reflexivity
- |reflexivity
- |apply numerator_nat_fact_to_fraction
- ]
-qed.
-
-definition nat_to_Q \def
-\lambda n. nat_fact_all_to_Q (factorize n).
-
+(*
let rec nat_fact_to_fraction_inv l \def
match l with
[nf_last a \Rightarrow nn a
]
.
-(*
definition nat_fact_all_to_Q_inv \def
\lambda n.
match n with
\lambda n. nat_fact_all_to_Q_inv (factorize n).
*)
-definition Qinv \def
-\lambda q.match q with
-[OQ \Rightarrow OQ
-|Qpos r \Rightarrow Qpos (rinv r)
-|Qneg r \Rightarrow Qneg (rinv r)
-].
-
definition frac:nat \to nat \to Q \def
\lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
intro.cases r;reflexivity.
qed.
-definition Qone \def Qpos one.
-
-theorem Qtimes_Qoner: \forall q.Qtimes q Qone = q.
-intro.cases q
- [reflexivity
- |cases r
- [reflexivity
- |reflexivity
- ]
- |cases r
- [reflexivity
- |reflexivity
- ]
- ]
-qed.
-
-theorem Qtimes_Qonel: \forall q.Qtimes Qone q = q.
-intros.cases q
- [reflexivity
- |cases r
- [reflexivity
- |reflexivity
- ]
- |cases r
- [reflexivity
- |reflexivity
- ]
- ]
-qed.
-
let rec times_f h g \def
match h with
[nf_last a \Rightarrow
Qinv(Qtimes p q) =
Qtimes (Qinv p) (Qinv q).
intros.
-rewrite < Qtimes_Qonel in ⊢ (? ? ? %).
+rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
rewrite < (Qtimes_Qinv (Qtimes p q))
[lapply (Qtimes_Qinv ? H).
lapply (Qtimes_Qinv ? H1).
rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
rewrite > Hletin1.
- rewrite > Qtimes_Qoner.
+ rewrite > Qtimes_q_Qone.
rewrite > Hletin.
- rewrite > Qtimes_Qoner.
+ rewrite > Qtimes_q_Qone.
reflexivity
|intro.
elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
(* la prova seguente e' tutta una ripetizione. Sistemare. *)
-
+(*CSC
theorem Qtimes1: \forall f:fraction.
Qtimes (nat_fact_all_to_Q (numerator f))
(Qinv (nat_fact_all_to_Q (numerator (finv f))))
|generalize in match H.
rewrite > H2.
rewrite > H3.
- rewrite > Qtimes_Qoner.
+ rewrite > Qtimes_q_Qone.
intro.
destruct H1.
assumption
|generalize in match H.
rewrite > H2.
rewrite > H3.
- rewrite > Qtimes_Qoner.
+ rewrite > Qtimes_q_Qone.
intro.
destruct H1.
assumption
|generalize in match H.
rewrite > H2.
rewrite > H3.
- rewrite > Qtimes_Qoner.
+ rewrite > Qtimes_q_Qone.
intro.
destruct H1.
assumption
]
]
qed.
-
+*)
(*
definition numQ:Q \to Z \def
\lambda q.
|Qpos q \Rightarrow Qneg q
|Qneg q \Rightarrow Qpos q
].
-
+(*CSC
theorem frac_numQ_denomQ1: \forall r:ratio.
frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
intro.
|apply Qtimes1.
]
]
-qed.
+qed.*)
+(*CSC
theorem frac_numQ_denomQ2: \forall r:ratio.
frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
intro.
|apply Qtimes1.
]
]
-qed.
+qed.*)
definition Qabs:Q \to Q \def \lambda q.
match q with
|Qpos q \Rightarrow Qpos q
|Qneg q \Rightarrow Qpos q
].
-
+(*CSC
theorem frac_numQ_denomQ: \forall q.
frac (numQ q) (denomQ q) = (Qabs q).
intros.
|simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
|simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
]
-qed.
-
+qed.*)
+(*CSC
definition Qfrac: Z \to nat \to Q \def
\lambda z,n.match z with
[OZ \Rightarrow OQ
|simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
]
qed.
-
+*)
projects / helm.git / blobdiff