]> matita.cs.unibo.it Git - helm.git/commitdiff
some more work on q
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 30 Jun 2008 18:54:26 +0000 (18:54 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 30 Jun 2008 18:54:26 +0000 (18:54 +0000)
helm/software/matita/contribs/dama/dama/cprop_connectives.ma
helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
helm/software/matita/contribs/dama/dama/models/q_bars.ma
helm/software/matita/contribs/dama/dama/models/q_function.ma
helm/software/matita/library/nat/compare.ma

index 14e21700011917fd53902f5e19eae5cf548d5b72..09b9a6c67fb189d61070b5adf27f5f131bf5a547 100644 (file)
@@ -21,6 +21,25 @@ inductive Or (A,B:CProp) : CProp ≝
 
 interpretation "constructive or" 'or x y = (Or x y).
 
+inductive Or3 (A,B,C:CProp) : CProp ≝
+ | Left3 : A → Or3 A B C
+ | Middle3 : B → Or3 A B C
+ | Right3 : C → Or3 A B C.
+
+interpretation "constructive ternary or" 'or3 x y z= (Or3 x y z).
+
+notation < "hvbox(a break ∨ b break ∨ c)" with precedence 35 for @{'or3 $a $b $c}.
+
+inductive Or4 (A,B,C,D:CProp) : CProp ≝
+ | Left3 : A → Or4 A B C D
+ | Middle3 : B → Or4 A B C D
+ | Right3 : C → Or4 A B C D
+ | Extra3: D → Or4 A B C D.
+
+interpretation "constructive ternary or" 'or4 x y z t = (Or4 x y z t).
+
+notation < "hvbox(a break ∨ b break ∨ c break ∨ d)" with precedence 35 for @{'or4 $a $b $c $d}.
+
 inductive And (A,B:CProp) : CProp ≝
  | Conj : A → B → And A B.
  
@@ -29,16 +48,16 @@ interpretation "constructive and" 'and x y = (And x y).
 inductive And3 (A,B,C:CProp) : CProp ≝
  | Conj3 : A → B → C → And3 A B C.
 
-notation < "a ∧ b ∧ c" with precedence 35 for @{'and3 $a $b $c}.
+notation < "hvbox(a break ∧ b break ∧ c)" with precedence 35 for @{'and3 $a $b $c}.
  
-interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
+interpretation "constructive ternary and" 'and3 x y z = (And3 x y z).
 
 inductive And4 (A,B,C,D:CProp) : CProp ≝
  | Conj4 : A → B → C → D → And4 A B C D.
 
-notation < "a ∧ b ∧ c ∧ d" with precedence 35 for @{'and4 $a $b $c $d}.
+notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for @{'and4 $a $b $c $d}.
  
-interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
+interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
 
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
@@ -93,3 +112,4 @@ definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A
 definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
 
 definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
index bc009b5c6fc6bcdb67dee6c63d84ddd7e819eed4..cb73c2d5f42aa617f167d4954ba63da2d3297496 100644 (file)
@@ -17,17 +17,6 @@ include "supremum.ma".
 include "nat/le_arith.ma".
 include "russell_support.ma".
 
-inductive cmp_cases (n,m:nat) : CProp ≝
-  | cmp_lt : n < m → cmp_cases n m
-  | cmp_eq : n = m → cmp_cases n m
-  | cmp_gt : m < n → cmp_cases n m.
-  
-lemma cmp_nat: ∀n,m.cmp_cases n m.
-intros; generalize in match (nat_compare_to_Prop n m);
-cases (nat_compare n m); intros;
-[constructor 1|constructor 2|constructor 3] assumption;
-qed.
-
 alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
 lemma nat_dedekind_sigma_complete:
index efa45f7f3d3467ab88312f76bed0c9280a1c42ed..75721e4db8561896691800a256ce599c40d1fa3e 100644 (file)
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "nat_ordered_set.ma".
 include "models/q_support.ma".
 include "models/list_support.ma".
 include "cprop_connectives.ma". 
@@ -44,6 +45,84 @@ axiom sum_bases_empty_nat_of_q_le_q:
 axiom sum_bases_empty_nat_of_q_le_q_one:
   ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one.
 
+lemma sum_bases_ge_OQ:
+  ∀l,n. OQ ≤ sum_bases l n.
+intro; elim l; simplify; intros;
+[1: elim n; [apply q_eq_to_le;reflexivity] simplify;
+    apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
+|2: cases n; [apply q_eq_to_le;reflexivity] simplify; 
+    apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]]
+qed.
+
+lemma sum_bases_O:
+  ∀l.∀x.sum_bases l x ≤ OQ → x = O.
+intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
+cases (q_le_cases ?? H); 
+[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); 
+|2: apply (q_lt_antisym ??? H1);] clear H H1; cases l;
+simplify; apply q_lt_plus_trans;
+try apply q_pos_lt_OQ; 
+try apply (sum_bases_ge_OQ []);
+apply (sum_bases_ge_OQ l1);
+qed.
+
+lemma sum_bases_increasing:
+  ∀l,x.sum_bases l x < sum_bases l (S x). 
+intro; elim l;
+[1: elim x;
+    [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+        apply q_pos_lt_OQ;
+    |2: simplify in H ⊢ %; 
+        apply q_lt_plus; rewrite > q_elim_minus;
+        rewrite < q_plus_assoc; rewrite < q_elim_minus;
+        rewrite > q_plus_minus; rewrite > q_plus_OQ;
+        assumption;]
+|2: elim x;
+    [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+        apply q_pos_lt_OQ;
+    |2: simplify; change in ⊢ (? ? (? % ?)) with (sum_bases l1 (S n)) ;  
+        apply q_lt_plus; rewrite > q_elim_minus;
+        rewrite < q_plus_assoc; rewrite < q_elim_minus;
+        rewrite > q_plus_minus; rewrite > q_plus_OQ; apply H]]
+qed.
+
+lemma sum_bases_lt_canc:
+  ∀l,x,y.sum_bases l (S x) < sum_bases l (S y) → sum_bases l x < sum_bases l y.
+intro; elim l; [apply (q_lt_canc_plus_r ?? (Qpos one));apply H]
+generalize in match H1;apply (nat_elim2 (?:? → ? → CProp) ??? x y);
+intros 2;
+[3: intros 2; simplify; apply q_lt_inj_plus_r; apply H;
+    apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H3;
+|2: cases (?:False); simplify in H2;
+    apply (q_lt_le_incompat (sum_bases l1 (S n)) OQ);[2: apply sum_bases_ge_OQ;]
+    apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H2;
+|1: cases n in H2; intro; 
+    [1: cases (?:False); apply (q_lt_corefl ? H2);
+    |2: simplify; apply  q_lt_plus_trans; [apply sum_bases_ge_OQ]
+        apply q_pos_lt_OQ;]]
+qed.
+
+lemma sum_bars_increasing2:
+  ∀l.∀n1,n2:nat.n1<n2→sum_bases l n1 < sum_bases l n2.                           
+intro; elim l 0;
+[1: intros 2; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
+    [1: intro; cases n;
+        [1: intro X; cases (not_le_Sn_O ? X);
+        |2: simplify; intros; apply q_lt_plus_trans;
+            [1: apply sum_bases_ge_OQ;|2: apply (q_pos_lt_OQ one)]]
+    |2: simplify; intros;  cases (not_le_Sn_O ? H);
+    |3: simplify; intros; apply q_lt_inj_plus_r;
+        apply H; apply le_S_S_to_le; apply H1;]
+|2:  intros 5; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
+    [1: simplify; intros; cases n in H1; intros;
+        [1: cases (not_le_Sn_O ? H1);
+        |2: simplify; apply q_lt_plus_trans;
+            [1: apply sum_bases_ge_OQ;|2: apply q_pos_lt_OQ]]
+    |2: simplify; intros; cases (not_le_Sn_O ? H1);
+    |3: simplify; intros; apply q_lt_inj_plus_r; apply H;
+        apply le_S_S_to_le; apply H2;]]
+qed.
+
 definition eject1 ≝
   λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p].
 coercion eject1.
@@ -52,16 +131,19 @@ coercion inject1 with 0 1 nocomposites.
 
 definition value : 
   ∀f:q_f.∀i:ℚ.∃p:nat × ℚ. 
-   match q_cmp i (start f) with
-   [ 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))) 
-         (\snd p = \snd (nth (bars f) ▭ (\fst p)))].
+   Or4
+    (And3 (i ≤ start f) (\fst p = O) (\snd p = OQ))
+    (And3 
+     (start f + sum_bases (bars f) (len (bars f)) ≤ i) 
+     (\fst p = O) (\snd p = OQ))
+    (And3 (bars f = []) (\fst p = O) (\snd p = OQ)) 
+    (And4 
+     (start f ≤ i ∧ i < start f + sum_bases (bars f) (len (bars f)))
+     (\fst p ≤ (len (bars f))) 
+     (\snd p = \snd (nth (bars f) ▭ (\fst p)))
+     (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f] ∧
+       (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))))).
 intros;
-alias symbol "pi2" = "pair pi2".
-alias symbol "pi1" = "pair pi1".
 letin value ≝ (
   let rec value (p: ℚ) (l : list bar) on l ≝
     match l with
@@ -80,10 +162,37 @@ letin value ≝ (
        (\snd p = \snd (nth l ▭ (\fst p))));
 [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 (q_dist_ge_OQ ? ?)); clear Hp value;
-        exists[1,3:apply p]; simplify; split; assumption;]
+    [2: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption; 
+        try reflexivity; apply q_lt_to_le; assumption;
+    |1: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption; 
+        try reflexivity; apply q_eq_to_le; assumption;
+    |3: cases (q_cmp i (start f+sum_bases (bars f) (len (bars f))));
+        [1: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption; 
+            try reflexivity; rewrite > H1; apply q_eq_to_le; reflexivity;  
+        |3: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption; 
+            try reflexivity; apply q_lt_to_le; assumption;
+        |2: generalize in match (refl_eq ? (bars f): bars f = bars f);
+            generalize in match (bars f) in ⊢ (??? % → %); intro X; cases X; clear X;
+            intros;
+            [1: exists [apply 〈O,OQ〉] simplify; constructor 3; split; reflexivity;
+            |2: cases (value ⅆ[i,start f] (b::l)) (p Hp);
+                cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value;
+                exists [apply p]; constructor 4; split; try split; try assumption;
+                [1: apply q_lt_to_le; assumption;
+                |2: rewrite < H2; assumption;
+                |3: cases (cmp_nat (\fst p) (len (bars f)));
+                    [1:apply lt_to_le;rewrite <H2; assumption|rewrite > H6;rewrite < H2;apply le_n]   
+                    cases (?:False); cases (\fst p) in H3 H4 H6; clear H5;
+                    [1:  intros; apply (not_le_Sn_O ? H5);
+                    |2: rewrite > q_d_sym; rewrite > q_d_noabs; [2: apply q_lt_to_le; assumption]
+                        intros; lapply (q_lt_inj_plus_r ?? (Qopp (start f)) H1); clear H1;
+                        generalize in match Hletin;
+                        rewrite > (q_plus_sym (start f)); rewrite < q_plus_assoc;
+                        do 2 rewrite < q_elim_minus; rewrite > q_plus_minus;
+                        rewrite > q_plus_OQ; intro K; apply (q_lt_corefl (i-start f));
+                        apply (q_lt_le_trans ???? H3); rewrite < H2; 
+                        apply (q_lt_trans ??? K); apply sum_bars_increasing2; 
+                        assumption;]]]]]                                 
 |1,3: intros; split;
     [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1);
            cases (H2 (q_le_to_diff_ge_OQ ?? (? H1)));
@@ -106,8 +215,7 @@ letin value ≝ (
     |2: apply sum_bases_empty_nat_of_q_le_q_one;
     |3: elim (nat_of_q q); [reflexivity] simplify; assumption]] 
 qed.
-    
-          
+              
 definition same_values ≝
   λl1,l2:q_f.
    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). 
@@ -122,65 +230,3 @@ 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 l n.
-intro; elim l; simplify; intros;
-[1: elim n; [apply q_eq_to_le;reflexivity] simplify;
-    apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
-|2: cases n; [apply q_eq_to_le;reflexivity] simplify; 
-    apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]]
-qed.
-
-lemma sum_bases_O:
-  ∀l.∀x.sum_bases l x ≤ OQ → x = O.
-intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
-cases (q_le_cases ?? H); 
-[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); 
-|2: apply (q_lt_antisym ??? H1);] clear H H1; cases l;
-simplify; apply q_lt_plus_trans;
-try apply q_pos_lt_OQ; 
-try apply (sum_bases_ge_OQ []);
-apply (sum_bases_ge_OQ l1);
-qed.
-
-lemma sum_bases_increasing:
-  ∀l,x.sum_bases l x < sum_bases l (S x). 
-intro; elim l;
-[1: elim x;
-    [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
-        apply q_pos_lt_OQ;
-    |2: simplify in H ⊢ %; 
-        apply q_lt_plus; rewrite > q_elim_minus;
-        rewrite < q_plus_assoc; rewrite < q_elim_minus;
-        rewrite > q_plus_minus; rewrite > q_plus_OQ;
-        assumption;]
-|2: elim x;
-    [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
-        apply q_pos_lt_OQ;
-    |2: simplify; change in ⊢ (? ? (? % ?)) with (sum_bases l1 (S n)) ;  
-        apply q_lt_plus; rewrite > q_elim_minus;
-        rewrite < q_plus_assoc; rewrite < q_elim_minus;
-        rewrite > q_plus_minus; rewrite > q_plus_OQ; apply H]]
-qed.
-
-lemma sum_bases_lt_canc:
-  ∀l,x,y.sum_bases l (S x) < sum_bases l (S y) → sum_bases l x < sum_bases l y.
-intro; elim l; [apply (q_lt_canc_plus_r ?? (Qpos one));apply H]
-generalize in match H1;apply (nat_elim2 (?:? → ? → CProp) ??? x y);
-intros 2;
-[3: intros 2; simplify; apply q_lt_inj_plus_r; apply H;
-    apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H3;
-|2: cases (?:False); simplify in H2;
-    apply (q_lt_le_incompat (sum_bases l1 (S n)) OQ);[2: apply sum_bases_ge_OQ;]
-    apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H2;
-|1: cases n in H2; intro; 
-    [1: cases (?:False); apply (q_lt_corefl ? H2);
-    |2: simplify; apply  q_lt_plus_trans; [apply sum_bases_ge_OQ]
-        apply q_pos_lt_OQ;]]
-qed.
-
index a58a82b1f763300201ee66c874b3e2bc67cc4b88..6c8fc1caea5a23390c4664ccec94f8eaa76a4e37 100644 (file)
 include "nat_ordered_set.ma".
 include "models/q_bars.ma".
 
-axiom le_le_eq: ∀x,y:Q. x ≤ y → y ≤ x → x = y.
-
 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]
+[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);
+cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input) (v1 Hv1); 
+(*cases (value l1 input) (v2 Hv2); *)
+cases Hv1 (HV1 HV1 HV1 HV1); (* cases Hv2 (HV2 HV2 HV2 HV2); clear Hv1 Hv2; *) 
+cases HV1 (Hi1 Hv11 Hv12); (*cases HV2 (Hi2 Hv21 Hv22);*) clear HV1 (*HV2*);
+(* simplify; *)
+rewrite > Hv12; (*rewrite > Hv22;*) try reflexivity;
+[1: simplify in Hi1; cases (?:False);
+    apply (q_lt_corefl (start l1)); cases (Hi2);
+    autobatch by Hi2, Hi1, q_le_trans, H4, H, q_le_lt_trans, q_lt_le_trans.
+|2: simplify in Hi1; cases (?:False);  
+    apply (q_lt_corefl (start l1+sum_bases (bars l1) (len (bars l1))));
+    cases Hi2; apply (q_le_lt_trans ???? H5);
+    apply (q_le_trans ???? Hi1); 
+    rewrite > H2; rewrite > (q_plus_sym ? (start l1-init));
+    rewrite > q_plus_assoc; apply q_le_inj_plus_r;
+    apply q_eq_to_le; 
+    rewrite > q_elim_minus; rewrite > (q_plus_sym (start l1));
+    rewrite > q_plus_assoc; rewrite < q_elim_minus;
+    rewrite > q_plus_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+    reflexivity;
+|3: simplify in Hi1; destruct Hi1;
+|4: simplify in Hi1 H3 Hv12 Hv11 ⊢ %; cases H3; clear H3;
+    cases (\fst v1) in H4; [intros;reflexivity] intros;
+    simplify; simplify in H3; 
+
+
+
+
+
 simplify in ⊢ (? ? ? (? ? ? %));
 cases (q_cmp input (start (mk_q_f init (〈w,OQ〉::bars l1)))) in H3;
 whd in ⊢ (% → ?); simplify in H3;
index dd9589e7bfab7d75cf8b33d60c0c60d22e34d259..c01f089bd57005e7168515615f0e5414df8fb221 100644 (file)
@@ -317,3 +317,14 @@ apply ((H H3)).
 apply ((H1 H3)).
 apply ((H2 H3)).
 qed.
+
+inductive cmp_cases (n,m:nat) : CProp ≝
+  | cmp_lt : n < m → cmp_cases n m
+  | cmp_eq : n = m → cmp_cases n m
+  | cmp_gt : m < n → cmp_cases n m.
+
+lemma cmp_nat: ∀n,m.cmp_cases n m.
+intros; generalize in match (nat_compare_to_Prop n m);
+cases (nat_compare n m); intros;
+[constructor 1|constructor 2|constructor 3] assumption;
+qed.