include "Z/compare.ma".
include "Z/plus.ma".
-include "higher_order_defs/functions.ma".
(* a fraction is a list of Z-coefficients for primes, in natural
order. The last coefficient must eventually be different from 0 *)
(\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to
(\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to
\forall f,g:fraction. R f g.
-intros 7.elim f.apply H.
-elim g.apply H2.
-apply H4.apply H5.
-apply H3.
-apply H1.
+intros 7.elim f.
+ apply H.
+ apply H1.
+ elim g.
+ apply H2.
+ apply H3.
+ apply H4.apply H5.
qed.
(* boolean equality *)
| (cons x f) \Rightarrow f].
theorem injective_pp : injective nat fraction pp.
-simplify.intros.
-change with (aux (pp x)) = (aux (pp y)).
+unfold injective.intros.
+change with ((aux (pp x)) = (aux (pp y))).
apply eq_f.assumption.
qed.
theorem injective_nn : injective nat fraction nn.
-simplify.intros.
-change with (aux (nn x)) = (aux (nn y)).
+unfold injective.intros.
+change with ((aux (nn x)) = (aux (nn y))).
apply eq_f.assumption.
qed.
theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
(cons x f) = (cons y g) \to x = y.
intros.
-change with (fhd (cons x f)) = (fhd (cons y g)).
+change with ((fhd (cons x f)) = (fhd (cons y g))).
apply eq_f.assumption.
qed.
theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
(cons x f) = (cons y g) \to f = g.
intros.
-change with (ftl (cons x f)) = (ftl (cons y g)).
+change with ((ftl (cons x f)) = (ftl (cons y g))).
apply eq_f.assumption.
qed.
-theorem not_eq_pp_nn: \forall n,m:nat. \lnot (pp n) = (nn m).
-intros.simplify. intro.
+theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
+intros.unfold Not. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
| (nn n) \Rightarrow True
theorem not_eq_pp_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
-\lnot (pp n) = (cons x f).
-intros.simplify. intro.
+pp n \neq cons x f.
+intros.unfold Not. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
| (nn n) \Rightarrow True
theorem not_eq_nn_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
-\lnot (nn n) = (cons x f).
-intros.simplify. intro.
+nn n \neq cons x f.
+intros.unfold Not. intro.
change with match (nn n) with
[ (pp n) \Rightarrow True
| (nn n) \Rightarrow False
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)).
-intros.elim g1.
-elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
-left.apply eq_f. assumption.
-right.intro.apply H.apply injective_pp.assumption.
-right.apply not_eq_pp_cons.
-right.apply not_eq_pp_nn.
-intros. elim g1.
-right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
-right.apply not_eq_nn_cons.
-elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
-left. apply eq_f. assumption.
-right.intro.apply H.apply injective_nn.assumption.
-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)).
-left.apply eq_f2.assumption. assumption.
-right.intro.apply H2.
-apply eq_cons_to_eq1 f1 g1.assumption.
-right.intro.apply H1.
-apply eq_cons_to_eq2 x y f1 g1.assumption.
+intros.unfold decidable.
+apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
+ intros.elim g1.
+ 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) : 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) : 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.
+ right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption.
qed.
theorem eqfb_to_Prop: \forall f,g:fraction.
match (eqfb f g) with
[true \Rightarrow f=g
-|false \Rightarrow \lnot f=g].
-intros.apply fraction_elim2
+|false \Rightarrow f \neq g].
+intros.apply (fraction_elim2
(\lambda f,g.match (eqfb f g) with
[true \Rightarrow f=g
-|false \Rightarrow \lnot f=g]).
-intros.elim g1.
-simplify.
-apply eqb_elim.
-intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply injective_pp.assumption.
-simplify.apply not_eq_pp_cons.
-simplify.apply not_eq_pp_nn.
-intros.
-elim g1.simplify.
-intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
-simplify.apply not_eq_nn_cons.
-simplify.apply eqb_elim.
-intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply injective_nn.assumption.
-intros.
-simplify.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq. assumption.
-intros.simplify.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq. assumption.
-intros.
-change in match (eqfb (cons x f1) (cons y g1)) with
-(andb (eqZb x y) (eqfb f1 g1)).
-apply eqZb_elim.
-intro.generalize in match H.
-elim (eqfb f1 g1).
-simplify.apply eq_f2.assumption.apply H2.
-simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption.
-intro.simplify.
-intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption.
+|false \Rightarrow f \neq g])).
+ intros.elim g1.
+ simplify.apply eqb_elim.
+ intro.simplify.apply eq_f.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
+ simplify.apply not_eq_pp_nn.
+ simplify.apply not_eq_pp_cons.
+ intros.elim g1.
+ simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
+ simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
+ intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
+ simplify.apply not_eq_nn_cons.
+ intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
+ intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
+ intros.
+ change in match (eqfb (cons x f1) (cons y g1))
+ with (andb (eqZb x y) (eqfb f1 g1)).
+ apply eqZb_elim.
+ intro.generalize in match H.elim (eqfb f1 g1).
+ simplify.apply eq_f2.assumption.
+ apply H2.
+ simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
+ intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
qed.
let rec finv f \def
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)).
-apply eq_f.apply sym_Zplus.
-change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
-rewrite < sym_Zplus.reflexivity.
-change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
-apply eq_f.apply sym_Zplus.
-intros.elim g.
-change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos 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).
-rewrite < sym_Zplus.reflexivity.
-change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
-apply eq_f.apply sym_Zplus.
-intros.
-change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (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).
-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)] =
- match ftimes g f with
- [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
- | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
-rewrite < H.rewrite < sym_Zplus.
-reflexivity.
+unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
+ intros.elim g.
+ 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 (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
+ apply eq_f.apply sym_Zplus.
+ 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 (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
+ apply eq_f.apply sym_Zplus.
+ 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 (neg n + z) f) = frac (cons (z + neg n) f)).
+ rewrite < sym_Zplus.reflexivity.
+ intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
+ rewrite < sym_Zplus.reflexivity.
+ 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 (x1 + y1)
+ | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
+ match ftimes g f with
+ [ 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.
-rewrite > Zplus_Zopp.reflexivity.
+intro.elim f.
+ change with (Z_to_ratio (pos n + - (pos n)) = one).
+ rewrite > Zplus_Zopp.reflexivity.
+ 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.
-rewrite > H.
-rewrite > Zplus_Zopp.reflexivity.
-change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one.
-rewrite > Zplus_Zopp.reflexivity.
+ change with
+ (match ftimes f1 (finv f1) with
+ [ one \Rightarrow Z_to_ratio (z + - z)
+ | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
+ rewrite > H.rewrite > Zplus_Zopp.reflexivity.
qed.
definition rtimes : ratio \to ratio \to ratio \def
| (frac g) \Rightarrow ftimes f g]].
theorem symmetric_rtimes : symmetric ratio rtimes.
-change with \forall r,s:ratio. rtimes r s = rtimes s r.
+change with (\forall r,s:ratio. rtimes r s = rtimes s r).
intros.
elim r. elim s.
reflexivity.
intro.elim r.
reflexivity.
simplify.apply ftimes_finv.
-qed.
\ No newline at end of file
+qed.
projects / helm.git / blobdiff