some work on Q

diff --git a/helm/software/matita/contribs/dama/dama/Makefile b/helm/software/matita/contribs/dama/dama/Makefile
index d40c9e674b7158c88eaeff44570e0241fa84dd45..92a16d1f036d4690621a5558f5d561f5746e2d86 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/Makefile
+++ b/helm/software/matita/contribs/dama/dama/Makefile
@@ -11,6 +11,6 @@ clean:
 clean.opt:
        $(BIN)../matitaclean.opt
 depend:
-       $(BIN)../matitadep
+       $(BIN)../matitadep -dot && rm depends.dot
 depend.opt:
-       $(BIN)../matitadep.opt
+       $(BIN)../matitadep.opt -dot && rm depends.dot

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index eafedec440a92ed7c63dfae6bf999782f86dc58b..3299c9a2f1d5046bed0fc6fea0155ffa98b549c1 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -15,10 +15,13 @@ russell_support.ma cprop_connectives.ma nat/nat.ma
 models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
 models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
 models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
+models/q_function.ma Q/q/q.ma cprop_connectives.ma list/list.ma
 models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
 models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
 models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma
+Q/q/q.ma 
 datatypes/constructors.ma 
+list/list.ma 
 logic/equality.ma 
 nat/compare.ma 
 nat/le_arith.ma 

diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png
index 767380377bc71244f771101b601e4a77d449fe1a..487d6f8d05072eaad3fede95ae6cd6fa384f4f3a 100644 (file)
Binary files a/helm/software/matita/contribs/dama/dama/depends.png and b/helm/software/matita/contribs/dama/dama/depends.png differ

diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma
new file mode 100644 (file)
index 0000000..df368bf
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -0,0 +1,91 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Q/q/q.ma".
+include "list/list.ma".
+include "cprop_connectives.ma". 
+
+notation "\rationals" non associative with precedence 99 for @{'q}.
+interpretation "Q" 'q = Q. 
+
+record q_f : Type ≝ {
+ start : ℚ;
+ bars: list (ℚ × ℚ) (* base, height *)
+}.
+
+axiom qp : ℚ → ℚ → ℚ.
+
+interpretation "Q plus" 'plus x y = (qp x y).
+
+axiom qm : ℚ → ℚ → ℚ.
+
+interpretation "Q minus" 'minus x y = (qm x y).
+
+axiom qlt : ℚ → ℚ → CProp.
+
+interpretation "Q less than" 'lt x y = (qlt x y).
+
+inductive q_comparison (a,b:ℚ) : CProp ≝
+ | q_eq : a = b → q_comparison a b 
+ | q_lt : a < b → q_comparison a b
+ | q_gt : b < a → q_comparison a b.
+
+axiom q_cmp:∀a,b:ℚ.q_comparison a b.
+
+definition qle ≝ λa,b:ℚ.a = b ∨ a < b.
+
+interpretation "Q less or equal than" 'le x y = (qle x y).
+
+notation "'nth'" left associative with precedence 70 for @{'nth}.
+notation < "\nth \nbsp l \nbsp d \nbsp i" left associative with precedence 70 for @{'nth_appl $l $d $i}.
+interpretation "list nth" 'nth = (cic:/matita/list/list/nth.con _).
+interpretation "list nth" 'nth_appl l d i = (cic:/matita/list/list/nth.con _ l d i).
+
+notation < "\rationals \sup 2" non associative with precedence 40 for @{'q2}.
+interpretation "Q x Q" 'q2 = (product Q Q).
+
+let rec mk_list (A:Type) (def:nat→A) (n:nat) on n ≝
+  match n with
+  [ O ⇒ []
+  | S m ⇒ def m :: mk_list A def m].
+
+interpretation "mk_list appl" 'mk_list f n = (mk_list f n).
+interpretation "mk_list" 'mk_list = mk_list.   
+notation < "\mk_list \nbsp f \nbsp n" left associative with precedence 70 for @{'mk_list_appl $f $n}.
+notation "'mk_list'" left associative with precedence 70 for @{'mk_list}.
+
+alias symbol "pair" = "pair".
+definition q00 : ℚ × ℚ ≝ 〈OQ,OQ〉.
+
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
+alias symbol "pair" = "pair".
+definition rebase: 
+  q_f → q_f → 
+    ∃p:q_f × q_f.∀i.
+     fst (nth (bars (fst p)) q00 i) = 
+     fst (nth (bars (snd p)) q00 i).   
+intros (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2;
+letin aux ≝ (
+let rec aux (l1,l2:list (ℚ × ℚ)) on l1 : (list (ℚ × ℚ)) × (list (ℚ × ℚ)) ≝
+  match l1 with
+  [ nil ⇒ 〈mk_list (λi.〈fst (nth l2 q00 i),OQ〉) (length ? l2),l2〉
+  | cons he tl ⇒ 〈[],[]〉] in aux); 
+  
+cases (q_cmp s1 s2);
+[1: apply (mk_q_f s1);
+|2: apply (mk_q_f s1); cases l2;
+    [1: letin l2' ≝ (
+[1: (* offset: the smallest one *)
+    cases