theorem decidable_eq_fraction: \forall f,g:fraction.
decidable (f = g).
intros.simplify.
-apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)).
+apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)).
intros.elim g1.
- elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+ elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
left.apply eq_f. assumption.
right.intro.apply H.apply injective_pp.assumption.
right.apply not_eq_pp_nn.
right.apply not_eq_pp_cons.
intros. elim g1.
right.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
- elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+ elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
left. apply eq_f. assumption.
right.intro.apply H.apply injective_nn.assumption.
right.apply not_eq_nn_cons.
intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
intros.elim H.
- elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
+ elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
left.apply eq_f2.assumption.
assumption.
right.intro.apply H2.apply eq_cons_to_eq1 f1 g1.assumption.
match f with
[ (pp n) \Rightarrow
match g with
- [(pp m) \Rightarrow Z_to_ratio (Zplus (pos n) (pos m))
- | (nn m) \Rightarrow Z_to_ratio (Zplus (pos n) (neg m))
- | (cons y g1) \Rightarrow frac (cons (Zplus (pos n) y) g1)]
+ [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
+ | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
+ | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
| (nn n) \Rightarrow
match g with
- [(pp m) \Rightarrow Z_to_ratio (Zplus (neg n) (pos m))
- | (nn m) \Rightarrow Z_to_ratio (Zplus (neg n) (neg m))
- | (cons y g1) \Rightarrow frac (cons (Zplus (neg n) y) g1)]
+ [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
+ | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
+ | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
| (cons x f1) \Rightarrow
match g with
- [ (pp m) \Rightarrow frac (cons (Zplus x (pos m)) f1)
- | (nn m) \Rightarrow frac (cons (Zplus x (neg m)) f1)
+ [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
+ | (nn m) \Rightarrow frac (cons (x + neg m) f1)
| (cons y g1) \Rightarrow
match ftimes f1 g1 with
- [ one \Rightarrow Z_to_ratio (Zplus x y)
- | (frac h) \Rightarrow frac (cons (Zplus x y) h)]]].
+ [ one \Rightarrow Z_to_ratio (x + y)
+ | (frac h) \Rightarrow frac (cons (x + y) h)]]].
theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
intros.elim g.
- change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)).
+ change with Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n).
apply eq_f.apply sym_Zplus.
- change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
+ change with Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n).
apply eq_f.apply sym_Zplus.
- change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
+ change with frac (cons (pos n + z) f) = frac (cons (z + pos n) f).
rewrite < sym_Zplus.reflexivity.
intros.elim g.
- change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)).
+ change with Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n).
apply eq_f.apply sym_Zplus.
- change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
+ change with Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n).
apply eq_f.apply sym_Zplus.
- change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f).
+ change with frac (cons (neg n + z) f) = frac (cons (z + neg n) f).
rewrite < sym_Zplus.reflexivity.
- intros.change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f).
+ intros.change with frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f).
rewrite < sym_Zplus.reflexivity.
- intros.change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f).
+ intros.change with frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f).
rewrite < sym_Zplus.reflexivity.
intros.
change with
match ftimes f g with
- [ one \Rightarrow Z_to_ratio (Zplus x1 y1)
- | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] =
+ [ one \Rightarrow Z_to_ratio (x1 + y1)
+ | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
match ftimes g f with
- [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
- | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
+ [ one \Rightarrow Z_to_ratio (y1 + x1)
+ | (frac h) \Rightarrow frac (cons (y1 + x1) h)].
rewrite < H.rewrite < sym_Zplus.reflexivity.
qed.
theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
intro.elim f.
- change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one.
+ change with Z_to_ratio (pos n + - (pos n)) = one.
rewrite > Zplus_Zopp.reflexivity.
- change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one.
+ change with Z_to_ratio (neg n + - (neg n)) = one.
rewrite > Zplus_Zopp.reflexivity.
(* again: we would need something to help finding the right change *)
change with
match ftimes f1 (finv f1) with
- [ one \Rightarrow Z_to_ratio (Zplus z (Zopp z))
- | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one.
+ [ one \Rightarrow Z_to_ratio (z + - z)
+ | (frac h) \Rightarrow frac (cons (z + - z) h)] = one.
rewrite > H.rewrite > Zplus_Zopp.reflexivity.
qed.