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