X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary_auto%2FQ%2Fq.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary_auto%2FQ%2Fq.ma;h=0000000000000000000000000000000000000000;hb=797f9ece92237a8d583a0c32ef4fa755299f9949;hp=d78400ea05e4df5fa725acb04daf4b87db03ecd6;hpb=9b6dcaba2d824263fdb849abec9fcc34a7546b5f;p=helm.git

diff --git a/helm/software/matita/library_auto/Q/q.ma b/helm/software/matita/library_auto/Q/q.ma
deleted file mode 100644
index d78400ea0..000000000
--- a/helm/software/matita/library_auto/Q/q.ma
+++ /dev/null
@@ -1,523 +0,0 @@
-(**************************************************************************)
-(*       ___	                                                            *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
-(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU Lesser General Public License Version 2.1         *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/library_auto/Q/q".
-
-include "Z/compare.ma".
-include "Z/plus.ma".
-
-(* a fraction is a list of Z-coefficients for primes, in natural
-order. The last coefficient must eventually be different from 0 *)
-
-inductive fraction : Set \def
-  pp : nat \to fraction
-| nn: nat \to fraction
-| cons : Z \to fraction \to fraction.
-
-inductive ratio : Set \def
-      one :  ratio
-    | frac : fraction \to ratio.
-
-(* a rational number is either O or a ratio with a sign *)
-inductive Q : Set \def 
-    OQ : Q
-  | Qpos : ratio  \to Q
-  | Qneg : ratio  \to Q.
-
-(* double elimination principles *)
-theorem fraction_elim2:
-\forall R:fraction \to fraction \to Prop.
-(\forall n:nat.\forall g:fraction.R (pp n) g) \to
-(\forall n:nat.\forall g:fraction.R (nn n) g) \to
-(\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to
-(\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
-| apply H1
-| elim g
-  [ apply H2
-  | apply H3
-  | auto
-    (*apply H4.
-    apply H5*)
-  ]
-]
-qed. 
-
-(* boolean equality *)
-let rec eqfb f g \def
-match f with
-[ (pp n) \Rightarrow 
-  match g with 
-  [ (pp m) \Rightarrow eqb n m
-  | (nn m) \Rightarrow false
-  | (cons y g1) \Rightarrow false]
-| (nn n) \Rightarrow 
-  match g with 
-  [ (pp m) \Rightarrow false
-  | (nn m) \Rightarrow eqb n m
-  | (cons y g1) \Rightarrow false] 
-| (cons x f1) \Rightarrow 
-  match g with 
-  [ (pp m) \Rightarrow false
-  | (nn m) \Rightarrow false
-  | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]]. 
-
-(* discrimination *)
-definition aux \def
-  \lambda f. match f with
-    [ (pp n) \Rightarrow n
-    | (nn n) \Rightarrow n
-    | (cons x f) \Rightarrow O].
-
-definition fhd \def
-\lambda f. match f with
-    [ (pp n) \Rightarrow (pos n)
-    | (nn n) \Rightarrow (neg n)
-    | (cons x f) \Rightarrow x].
-
-definition ftl \def
-\lambda f. match f with
-    [ (pp n) \Rightarrow (pp n)
-    | (nn n) \Rightarrow (nn n)
-    | (cons x f) \Rightarrow f].
-    
-theorem injective_pp : injective nat fraction pp.
-unfold injective.
-intros.
-change with ((aux(pp x)) = (aux (pp y))).
-auto.
-(*apply eq_f.
-assumption.*)
-qed.
-
-theorem injective_nn : injective nat fraction nn.
-unfold injective.
-intros.
-change with ((aux (nn x)) = (aux (nn y))).
-auto.
-(*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))).
-auto.
-(*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))).
-auto.
-(*apply eq_f.assumption.*)
-qed.
-
-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
-| (cons x f) \Rightarrow True].
-rewrite > H.
-simplify.
-exact I.
-qed.
-
-theorem not_eq_pp_cons: 
-\forall n:nat.\forall x:Z. \forall f:fraction. 
-pp n \neq cons x f.
-intros.
-unfold Not.
-intro.
-change with match (pp n) with
-[ (pp n) \Rightarrow False
-| (nn n) \Rightarrow True
-| (cons x f) \Rightarrow True].
-rewrite > H.
-simplify.
-exact I.
-qed.
-
-theorem not_eq_nn_cons: 
-\forall n:nat.\forall x:Z. \forall f:fraction. 
-nn n \neq cons x f.
-intros.
-unfold Not.
-intro.
-change with match (nn n) with
-[ (pp n) \Rightarrow True
-| (nn n) \Rightarrow False
-| (cons x f) \Rightarrow True].
-rewrite > H.
-simplify.
-exact I.
-qed.
-
-theorem decidable_eq_fraction: \forall f,g:fraction.
-decidable (f = g).
-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))
-    [ auto
-      (*left.
-      apply eq_f.
-      assumption*)
-    | right.
-      intro.
-      auto
-      (*apply H.
-      apply injective_pp.
-      assumption*)
-    ]
-  | auto
-    (*right.
-    apply not_eq_pp_nn*)
-  | auto
-    (*right.
-    apply not_eq_pp_cons*)
-  ]
-| intros.
-  elim g1
-  [ right.
-    intro.
-    apply (not_eq_pp_nn n1 n).
-    auto
-    (*apply sym_eq. 
-    assumption*)
-  | elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False))
-    [ auto
-      (*left. 
-      apply eq_f. 
-      assumption*)
-    | right.
-      intro.
-      auto
-      (*apply H.
-      apply injective_nn.
-      assumption*)
-    ]
-  | auto
-    (*right.
-    apply not_eq_nn_cons*)
-  ]
-| intros.
-  right.
-  intro.
-  apply (not_eq_pp_cons m x f1).
-  auto
-  (*apply sym_eq.
-  assumption*)
-| intros.
-  right.
-  intro.
-  apply (not_eq_nn_cons m x f1).
-  auto
-  (*apply sym_eq.
-  assumption*)
-| intros.
-  elim H
-  [ elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False))
-    [ auto
-      (*left.
-      apply eq_f2;
-        assumption*)
-    | right.
-      intro.
-      auto
-      (*apply H2.
-      apply (eq_cons_to_eq1 f1 g1).
-      assumption*)
-    ]    
-  | right.
-    intro.
-    auto
-    (*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 f \neq g].
-intros.
-apply (fraction_elim2 
-(\lambda f,g.match (eqfb f g) with
-[true \Rightarrow f=g
-|false \Rightarrow f \neq g]))
-[ intros.
-  elim g1
-  [ simplify.
-    apply eqb_elim
-    [ intro.
-      simplify.
-      auto
-      (*apply eq_f.
-      assumption*)
-    | intro.
-      simplify.
-      unfold Not.
-      intro.
-      auto
-      (*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).
-    auto
-    (*apply sym_eq.
-    assumption*)
-  | simplify.
-    apply eqb_elim
-    [ intro.
-      simplify.
-      auto
-      (*apply eq_f.
-      assumption*)
-    | intro.
-      simplify.
-      unfold Not.
-      intro.
-      auto
-      (*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).
-  auto
-  (*apply sym_eq.
-  assumption*)
-| intros.
-  simplify.
-  unfold Not.
-  intro.
-  apply (not_eq_nn_cons m x f1).
-  auto
-  (*apply sym_eq.
-  assumption*)
-| intros.
-  simplify.
-  apply eqZb_elim
-  [ intro.
-    generalize in match H.
-    elim (eqfb f1 g1)
-    [ simplify.
-      apply eq_f2
-      [ assumption
-      | (*qui auto non chiude il goal*)
-        apply H2
-      ]
-    | simplify.
-      unfold Not.
-      intro.
-      apply H2.
-      auto
-      (*apply (eq_cons_to_eq2 x y).
-      assumption*)
-    ]
-  | intro.
-    simplify.
-    unfold Not.
-    intro.
-    auto
-    (*apply H1.
-    apply (eq_cons_to_eq1 f1 g1).
-    assumption*)
-  ]
-]
-qed.
-
-let rec finv f \def
-  match f with
-  [ (pp n) \Rightarrow (nn n)
-  | (nn n) \Rightarrow (pp n)
-  | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
-
-definition Z_to_ratio :Z \to ratio \def
-\lambda x:Z. match x with
-[ OZ \Rightarrow one
-| (pos n) \Rightarrow frac (pp n)
-| (neg n) \Rightarrow frac (nn n)].
-
-let rec ftimes f g \def
-  match f with
-  [ (pp n) \Rightarrow 
-    match g with
-    [(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 (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 (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 (x + y)
-        | (frac h) \Rightarrow frac (cons (x + y) h)]]].
-        
-theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
-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)).
-    auto
-    (*apply eq_f.
-    apply sym_Zplus*)
-  | change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
-    auto
-    (*apply eq_f.
-    apply sym_Zplus*)
-  | change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
-    auto
-    (*rewrite < sym_Zplus.
-    reflexivity*)
-  ]
-| intros.
-  elim g
-  [ change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
-    auto
-    (*apply eq_f.
-    apply sym_Zplus*)
-  | change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
-    auto
-    (*apply eq_f.
-    apply sym_Zplus*)
-  | change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
-    auto
-    (*rewrite < sym_Zplus.
-    reflexivity*)
-  ]
-| intros.
-  change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
-  auto
-  (*rewrite < sym_Zplus.
-  reflexivity*)
-| intros.
-  change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
-  auto
-  (*rewrite < sym_Zplus.
-  reflexivity*)
-| intros.
-   (*CSC: simplify does something nasty here because of a redex in Zplus *)
-   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 (pos n + - (pos n)) = one).
-  auto
-  (*rewrite > Zplus_Zopp.
-  reflexivity*)
-| change with (Z_to_ratio (neg n + - (neg n)) = one).
-  auto
-  (*rewrite > Zplus_Zopp.
-  reflexivity*)
-|
-  (*CSC: simplify does something nasty here because of a redex in Zplus *)
-  (* again: we would need something to help finding the right change *)
-  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
-\lambda r,s:ratio.
-  match r with
-  [one \Rightarrow s
-  | (frac f) \Rightarrow 
-      match s with 
-      [one \Rightarrow frac f
-      | (frac g) \Rightarrow ftimes f g]].
-
-theorem symmetric_rtimes : symmetric ratio rtimes.
-change with (\forall r,s:ratio. rtimes r s = rtimes s r).
-intros.
-elim r
-[ elim s;reflexivity
-| elim s
-  [ reflexivity
-  | simplify.
-    apply symmetric2_ftimes
-  ]
-]
-qed.
-
-definition rinv : ratio \to ratio \def
-\lambda r:ratio.
-  match r with
-  [one \Rightarrow one
-  | (frac f) \Rightarrow frac (finv f)].
-
-theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
-intro.
-elim r
-[ reflexivity
-| simplify.
-  apply ftimes_finv
-]
-qed.