-(* 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.