From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 26 Jun 2008 11:43:08 +0000 (+0000)
Subject: more work on q
X-Git-Tag: make_still_working~4990
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b82d421fb24bd0eb8848dc7b978ce1165fb526ab;p=helm.git

more work on q
---

diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma
index c458d418d..21e51808a 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -44,9 +44,21 @@ interpretation "Q less or equal than" 'leq x y = (qle x y).
 
 axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
 axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b.
+axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b.
 
-axiom dist : ℚ → ℚ → ℚ.
+axiom q_dist : ℚ → ℚ → ℚ.
 
+notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90
+for @{'distance $x $y}.
+interpretation "ℚ distance" 'distance x y = (q_dist x y).
+
+axiom q_dist_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
+
+axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
+axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a.
+axiom q_plus_OQ: ∀x:ℚ.x + OQ = x.
+axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x.
+axiom nat_of_q: ℚ → nat. 
 
 interpretation "list nth" 'nth = (nth _).
 interpretation "list nth" 'nth_appl l d i = (nth _ l d i).
@@ -82,9 +94,6 @@ interpretation "len" 'len = (length _).
 notation < "'len' \nbsp term 90 l" with precedence 69 for @{'len_appl $l}.
 interpretation "len appl" 'len_appl l = (length _ l).
 
-(* a local letin makes russell fail *)
-definition cb0h ≝ (λl.mk_list (λi.〈\fst (nth l ▭ i),OQ〉) (len l)).
-
 lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.len (mk_list f n) = n.
 intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;
 qed.
@@ -96,6 +105,13 @@ let rec sum_bases (l:list bar) (i:nat)on i ≝
          match l with
          [ nil ⇒ sum_bases l m + Qpos one
          | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]].
+         
+axiom sum_bases_empty_nat_of_q_ge_OQ:
+  ∀q:ℚ.OQ ≤ sum_bases [] (nat_of_q q). 
+axiom sum_bases_empty_nat_of_q_le_q:
+  ∀q:ℚ.sum_bases [] (nat_of_q q) ≤ q.
+axiom sum_bases_empty_nat_of_q_le_q_one:
+  ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one.
 
 definition eject1 ≝
   λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p].
@@ -109,8 +125,8 @@ definition value :
    [ q_lt _ ⇒ \snd p = OQ
    | _ ⇒ 
         And3
-         (sum_bases (bars f) (\fst p) ≤ i - start f) 
-         (i - start f < sum_bases (bars f) (S (\fst p))) 
+         (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f]) 
+         (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))) 
          (\snd p = \snd (nth (bars f) ▭ (\fst p)))].
 intros;
 alias symbol "pi2" = "pair pi2".
@@ -118,7 +134,7 @@ alias symbol "pi1" = "pair pi1".
 letin value ≝ (
   let rec value (p: ℚ) (l : list bar) on l ≝
     match l with
-    [ nil ⇒ 〈O,OQ〉
+    [ nil ⇒ 〈nat_of_q p,OQ〉
     | cons x tl ⇒
         match q_cmp p (Qpos (\fst x)) with
         [ q_lt _ ⇒ 〈O, \snd x〉
@@ -134,69 +150,129 @@ letin value ≝ (
 [5: clearbody value; 
     cases (q_cmp i (start f));
     [2: exists [apply 〈O,OQ〉] simplify; reflexivity;
-    |*: cases (value (i - start f) (bars f)) (p Hp);
-        cases Hp; clear Hp value;
+    |*: cases (value ⅆ[i,start f] (bars f)) (p Hp);
+        cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value;
         exists[1,3:apply p]; simplify; split; assumption;]
 |1,3: intros; split;
-    [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); cases H2; clear H2;
+    [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1);
+           cases (H2 (q_le_to_diff_ge_OQ ?? (? H1)));
+          [1,3: intros; [right|left;symmetry] assumption]
           simplify; apply q_le_minus; assumption;
-    |2,5: cases (value (q-Qpos (\fst b)) l1); cases H3; clear H3 H2 value;
+    |2,5: cases (value (q-Qpos (\fst b)) l1); 
+          cases (H4 (q_le_to_diff_ge_OQ ?? (? H1)));
+          [1,3: intros; [right|left;symmetry] assumption]
+          clear H3 H2 value;
           change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b));
           apply q_lt_plus; assumption;
-    |*: cases (value (q-Qpos (\fst b)) l1); simplify; cases H3; clear H3 value H2;
+    |*: cases (value (q-Qpos (\fst b)) l1); simplify; 
+        cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); 
+        [1,3: intros; [right|left;symmetry] assumption]
         assumption;]
-|2: clear value H2; simplify; split;
-    [1: 
+|2: clear value H2; simplify; intros; split; [assumption|3:reflexivity]
+    rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption;
+|4: simplify; intros; split; 
+    [1: apply sum_bases_empty_nat_of_q_le_q;
+    |2: apply sum_bases_empty_nat_of_q_le_q_one;
+    |3: elim (nat_of_q q); [reflexivity] simplify; assumption]] 
+qed.
     
           
-definition same_shape ≝
+definition same_values ≝
   λl1,l2:q_f.
-   ∀input.∃col.
-   
-    And3 
-      (sum_bases (bars l2) j ≤ offset - start l2)
-      (offset - start l2 ≤ sum_bases (bars l2) (S j))
-      (\snd (nth (bars l2)) q0 j) = \snd (nth (bars l1) q0 i).
+   ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). 
+
+definition same_bases ≝ 
+  λl1,l2:q_f.
+    (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)).
+
+axiom q_lt_corefl: ∀x:Q.x < x → False.
+axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
+axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
+axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ.
+axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False.
+axiom q_lt_plus_trans:
+  ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
+axiom q_pos_lt_OQ: ∀x.OQ < Qpos x.
+axiom q_le_plus_trans:
+  ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y. 
+
+lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
+intro; cases x; intros; [2:exists [apply r] reflexivity]
+cases (?:False);
+[ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)]
+qed.
+
+notation < "\blacksquare" non associative with precedence 90 for @{'hide}.
+definition hide ≝ λT:Type.λx:T.x.
+interpretation "hide" 'hide = (hide _ _).
+
+lemma sum_bases_ge_OQ:
+  ∀l,n. OQ ≤ sum_bases (bars l) n.
+intro; elim (bars l); simplify; intros;
+[1: elim n; [left;reflexivity] simplify;
+    apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
+|2: cases n; [left;reflexivity] simplify; 
+    apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]]
+qed.
 
-…┐─┌┐…
-\ldots\boxdl\boxh\boxdr\boxdl\ldots
+lemma sum_bases_O:
+  ∀l:q_f.∀x.sum_bases (bars l) x ≤ OQ → x = O.
+intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
+cases H; 
+[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); 
+|2: apply (q_lt_antisym ??? H1);] clear H H1; cases (bars l);
+simplify; apply q_lt_plus_trans;
+try apply q_pos_lt_OQ; 
+try apply (sum_bases_ge_OQ (mk_q_f OQ []));
+apply (sum_bases_ge_OQ (mk_q_f OQ l1));
+qed.
 
+lemma initial_shift_same_values:
+  ∀l1:q_f.∀init.init < start l1 →
+   same_values l1 
+     (mk_q_f init (〈\fst (unpos (start l1 - init) ?),OQ〉:: bars l1)).  
+[apply hide; apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption]
+intros; generalize in ⊢ (? ? (? ? (? ? (? ? ? (? ? ? (? ? %)) ?) ?))); intro;
+cases (unpos (start l1-init) H1); intro input;
+simplify in ⊢ (? ? ? (? ? ? (? ? ? (? (? ? (? ? (? ? ? % ?) ?)) ?))));
+cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input);
+simplify in ⊢ (? ? ? (? ? ? %));
+cases (q_cmp input (start (mk_q_f init (〈w,OQ〉::bars l1)))) in H3;
+whd in ⊢ (% → ?); simplify in H3;
+[1: intro; cases H4; clear H4; rewrite > H3;
+    cases (value l1 init); simplify; cases (q_cmp init (start l1)) in H4;
+    [1: cases (?:False); apply (q_lt_corefl init); rewrite > H4 in ⊢ (?? %); apply H;
+    |3: cases (?:False); apply (q_lt_antisym init (start l1)); assumption;
+    |2: whd in ⊢ (% → ?); intro; rewrite > H8; clear H8 H4;
+        rewrite > H7; clear H7; rewrite > (?:\fst w1 = O); [reflexivity]
+        symmetry; apply le_n_O_to_eq;
+        rewrite > (sum_bases_O (mk_q_f init (〈w,OQ〉::bars l1)) (\fst w1)); [apply le_n]   
+        clear H6 w2;
+        simplify in H5:(? ? (? ? %));  
+        destruct H3; rewrite > q_d_x_x in H5; assumption;]
+|2: intros;
+  
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
 definition rebase_spec ≝ 
  ∀l1,l2:q_f.∃p:q_f × q_f.
    And4
-    (len (bars (\fst p)) = len (bars (\snd p)))
+    (*len (bars (\fst p)) = len (bars (\snd p))*)
     (start (\fst p) = start (\snd p))
-    (∀i.\fst (nth (bars (\fst p)) q0 i) = \fst (nth (bars (\snd p)) q0 i))
-    (∀i,offset.
-      sum_bases (bars l1) i ≤ offset - start l1 →
-      offset - start l1 ≤ sum_bases (bars l1) (S i) →
-      ∃j.      
-        And3 
-         (sum_bases (bars (\fst p)) j ≤ offset - start (\fst p))
-         (offset - start (\fst p) ≤ sum_bases (bars (\fst p)) (S j))
-         (\snd (nth (bars (\fst p)) q0 j) = \snd (nth (bars l1) q0 i)) ∧
-        And3 
-         (sum_bases (bars (\snd p)) j ≤ offset - start (\snd p))
-         (offset - start (\snd p) ≤ sum_bases (bars (\snd p)) (S j))
-         (\snd (nth (bars (\snd p)) q0 j) = \snd (nth (bars l2) q0 i))).
+    (same_bases (\fst p) (\snd p))
+    (same_values l1 (\fst p)) 
+    (same_values l2 (\snd p)).
 
 definition rebase_spec_simpl ≝ 
- λl1,l2:list (ℚ × ℚ).λp:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).
-    len ( (\fst p)) = len ( (\snd p)) ∧
-    (∀i.
-     \fst (nth ( (\fst p)) q0 i) = 
-     \fst (nth ( (\snd p)) q0 i)) ∧
-    ∀i,offset.
-      sum_bases ( l1) i ≤ offset ∧
-      offset ≤ sum_bases ( l1) (S i)
-       →
-      ∃j.  
-        sum_bases ( (\fst p)) j ≤ offset ∧
-        offset ≤ sum_bases ((\fst p)) (S j) ∧
-        \snd (nth ( (\fst p)) q0 j) = 
-        \snd (nth ( l1) q0 i).
+ λstart.λl1,l2:list bar.λp:(list bar) × (list bar).
+   And3
+    (same_bases (mk_q_f start (\fst p)) (mk_q_f start (\snd p)))
+    (same_values (mk_q_f start l1) (mk_q_f start (\fst p))) 
+    (same_values (mk_q_f start l2) (mk_q_f start (\snd p))).
+
+(* a local letin makes russell fail *)
+definition cb0h : list bar → list bar ≝ 
+  λl.mk_list (λi.〈\fst (nth l ▭ i),OQ〉) (len l).
 
 definition eject ≝
   λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p].
@@ -207,10 +283,11 @@ coercion inject with 0 1 nocomposites.
 definition rebase: rebase_spec.
 intros 2 (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2;
 letin spec ≝ (
-  λl1,l2:list (ℚ × ℚ).λm:nat.λz:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).
-    len l1 + len l2 < m → rebase_spec_simpl l1 l2 z);
+  λs.λl1,l2.λm.λz.len l1 + len l2 < m → rebase_spec_simpl s l1 l2 z);
+alias symbol "pi1" (instance 34) = "exT \fst".
+alias symbol "pi1" (instance 21) = "exT \fst".
 letin aux ≝ ( 
-let rec aux (l1,l2:list (ℚ × ℚ)) (n:nat) on n : (list (ℚ × ℚ)) × (list (ℚ × ℚ)) ≝
+let rec aux (l1,l2:list bar) (n:nat) on n : (list bar) × (list bar) ≝
 match n with
 [ O ⇒ 〈 nil ? , nil ? 〉
 | S m ⇒ 
@@ -220,43 +297,59 @@ match n with
      match l2 with
      [ nil ⇒ 〈l1, cb0h l1〉
      | cons he2 tl2 ⇒  
-         let base1 ≝ (\fst he1) in
-         let base2 ≝ (\fst he2) in
+         let base1 ≝ Qpos (\fst he1) in
+         let base2 ≝ Qpos (\fst he2) in
          let height1 ≝ (\snd he1) in
          let height2 ≝ (\snd he2) in
          match q_cmp base1 base2 with
          [ q_eq _ ⇒ 
              let rc ≝ aux tl1 tl2 m in 
              〈he1 :: \fst rc,he2 :: \snd rc〉 
-         | q_lt _ ⇒
+         | q_lt Hp ⇒
              let rest ≝ base2 - base1 in
-             let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in
-             〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉 
-         | q_gt _ ⇒ 
+             let rc ≝ aux tl1 (〈\fst (unpos rest ?),height2〉 :: tl2) m in
+             〈〈\fst he1,height1〉 :: \fst rc,〈\fst he1,height2〉 :: \snd rc〉 
+         | q_gt Hp ⇒ 
              let rest ≝ base1 - base2 in
-             let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
-             〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉
+             let rc ≝ aux (〈\fst (unpos rest ?),height1〉 :: tl1) tl2 m in
+             〈〈\fst he2,height1〉 :: \fst rc,〈\fst he2,height2〉 :: \snd rc〉
 ]]]]
-in aux : ∀l1,l2,m.∃z.spec l1 l2 m z); unfold spec;
-[7: clearbody aux; unfold spec in aux; clear spec;
+in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec;
+[9: clearbody aux; unfold spec in aux; clear spec;
     cases (q_cmp s1 s2);
     [1: cases (aux l1 l2 (S (len l1 + len l2)));
-        cases (H1 (le_n ?)); clear H1;
-        exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s2 (\snd w)〉] repeat split;
-        [1: cases H2; assumption;
+        cases (H1 s1 (le_n ?)); clear H1;
+        exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s2 (\snd w)〉] split;
+        [1,2: assumption;
+        |3: intro; apply (H3 input);
+        |4: intro; rewrite > H in H4; 
+            rewrite > (H4 input); reflexivity;]
+    |2: letin l2' ≝ (〈\fst (unpos (s2-s1) ?),OQ〉::l2);[
+          apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+          assumption]
+        cases (aux l1 l2' (S (len l1 + len l2')));
+        cases (H1 s1 (le_n ?)); clear H1 aux;
+        exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s1 (\snd w)〉] split;
+        [1: reflexivity
         |2: assumption;
-        |3: cases H2; assumption;
-        |4: intros; cases (H3 i (offset - s1)); 
-            [2: 
-        
-        
-|1,2: simplify; generalize in ⊢ (? ? (? (? ? (? ? ? (? ? %)))) (? (? ? (? ? ? (? ? %))))); intro X; 
-      cases X (rc OK); clear X; simplify; apply eq_f; assumption;
-|3: cases (aux l4 l5 n1) (rc OK); simplify; apply eq_f; assumption;
-|4,5: simplify; unfold cb0h; rewrite > len_mk_list; reflexivity;
-|6: reflexivity]
-clearbody aux; unfold spec in aux; clear spec; 
-
-
-
+        |3: assumption;
+        |4: intro; rewrite < (H4 input); clear H3 H4 H2 w;
+            cases (value (mk_q_f s1 l2') input);
+            cases (q_cmp input (start (mk_q_f s1 l2'))) in H1;
+            whd in ⊢ (% → ?);
+            [1: intros; cases H2; clear H2; whd in ⊢ (??? %);
+                cases (value (mk_q_f s2 l2) input);
+                cases (q_cmp input (start (mk_q_f s2 l2))) in H2;
+                whd in ⊢ (% → ?);
+                [1: intros; cases H6; clear H6; change with (w1 = w);
+                          
+            (* TODO *) ]]    
+|1,2: unfold rest; apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+      assumption;        
+|3:(* TODO *)
+|4:(* TODO *)
+|5:(* TODO *)
+|6:(* TODO *)
+|7:(* TODO *)
+|8: intros; cases (?:False); apply (not_le_Sn_O ? H1);]
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index 2e0df971e..e4787fe84 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -142,21 +142,29 @@ reflexivity.
 qed.
 *)
 
-let rec nth (A:Type) l d n on n ≝
- match n with
-  [ O ⇒
-     match l with
-      [ nil ⇒ d
-      | cons (x : A) _ ⇒ x
-      ]
-  | S n' ⇒ nth A (tail ? l) d n'
-  ].
+definition nth ≝
+  λA:Type.
+    let rec nth l d n on n ≝
+      match n with
+      [ O ⇒
+         match l with
+         [ nil ⇒ d
+         | cons (x : A) _ ⇒ x
+         ]
+      | S n' ⇒ nth (tail ? l) d n']
+    in nth.
   
-let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝
-  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+definition map ≝
+  λA,B:Type.λf:A→B.
+  let rec map (l : list A) on l : list B ≝
+    match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map tl)]
+  in map.
   
-let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := 
-  match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)].
+definition foldr ≝
+  λA,B:Type.λf:A→B→B.λb:B.
+  let rec foldr (l : list A) on l : B := 
+    match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr l)]
+  in foldr.
    
 definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l.
 
diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index caffee3f1..bcad516e0 100644
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -114,7 +114,6 @@
     <keyword>left</keyword>
     <keyword>letin</keyword>
     <keyword>normalize</keyword>
-    <keyword>reduce</keyword>
     <keyword>reflexivity</keyword>
     <keyword>replace</keyword>
     <keyword>rewrite</keyword>