include "Z/plus.ma".
include "Q/fraction/fraction.ma".
-let rec finv f \def
+let rec finv f ≝
match f with
- [ (pp n) \Rightarrow (nn n)
- | (nn n) \Rightarrow (pp n)
- | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
+ [ pp n ⇒ nn n
+ | nn n ⇒ pp n
+ | cons x g ⇒ cons (Zopp x) (finv g)].
theorem finv_finv: ∀f. finv (finv f) = f.
intro;
reflexivity
]
qed.
-
-theorem or_numerator_nfa_one_nfa_proper:
-∀f.
- (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨
- ∃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:
-∀f.numerator f = nfa_one → ∃h.numerator (finv f) = nfa_proper h.
- intros;
- elim (or_numerator_nfa_one_nfa_proper f); cases H1;
- [ assumption
- | rewrite > H in H2;
- destruct
- ]
-qed.