added a function to reorder the metasenv.

[helm.git] / helm / matita / library / Q / q.ma

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index 0e6678dc935e2910c6abbf2ad3d5e653d62c6c9e..d7c2816a15cbdc8997d27d5472b82e0fe5be66cf 100644 (file)
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -45,11 +45,13 @@ theorem fraction_elim2:
 (\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 *)
@@ -154,27 +156,26 @@ 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.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_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)).
+        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)).
+      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.
@@ -185,33 +186,28 @@ 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.
+  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_nn.
+    simplify.apply not_eq_pp_cons.
+  intros.elim g1.
+    simplify.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
+    simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
+    intro.simplify.intro.apply H.apply injective_nn.assumption.
+  simplify.apply not_eq_nn_cons.
+  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.
 qed.
 
 let rec finv f \def
@@ -248,54 +244,48 @@ let rec ftimes f g \def
         | (frac h) \Rightarrow frac (cons (Zplus 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.
+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 Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (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).
+     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)).
+     apply eq_f.apply sym_Zplus.
+    change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (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).
+     rewrite < sym_Zplus.reflexivity.
+  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.
 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 (Zplus (pos n) (Zopp (pos n))) = one.
+   rewrite > Zplus_Zopp.reflexivity.
+  change with Z_to_ratio (Zplus (neg n) (Zopp (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 (Zplus z (Zopp z))
+  | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one.
+  rewrite > H.rewrite > Zplus_Zopp.reflexivity.
 qed.
 
 definition rtimes : ratio \to ratio \to ratio \def