X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flist%2Fsort.ma;h=939cecedec6486a27274a4ce6ac834888f7c58ce;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=ffd1e21872cd85c53c38fd3c9c518bc3a381a211;hpb=1276d3c7b85f4edc049a5d68a6120816fe64c806;p=helm.git

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index ffd1e2187..939cecede 100644
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -48,26 +48,43 @@ let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
        | false ⇒ he::(insert A le x l')
        ]
   ].
-(*
-theorem insert_ind:
- ∀A:Set. ∀le: A → A → bool. ∀x:A.
-  ∀P: list A → Prop.
-   ∀l:list A. P (insert A le x l).
- intros (A le x P H l).
- apply (
- let rec insert_ind (l: list A) ≝
-  match l in list return λl.P (insert A le x l) with
-   [ nil ⇒ (? : P [x])
-   | (cons he l') ⇒
-       match le x he return λb.P (match b with [ true ⇒ x::he::l' | false ⇒ he::(insert A le x l') ]) with
-        [ true ⇒ (H2 : P (x::he::l'))
-        | false ⇒ (? : P (he::(insert A le x l')))
-        ]
-   ]
- in
-  insert_ind l).
+
+lemma insert_ind :
+ ∀A:Set. ∀le: A → A → bool. ∀x.
+  ∀P:(list A → list A → Prop).
+   ∀H:(∀l: list A. l=[] → P [] [x]).
+    ∀H2:
+    (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+      le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
+     ∀H3:
+     (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+       le x he = true → l=he::l' → P (he::l') (x::he::l')).
+    ∀l:list A. P l (insert ? le x l).
+  intros.
+  apply (
+    let rec insert_ind (l: list A) \def
+    match l in list
+    return
+      λli.
+       l = li → P li (insert ? le x li)
+    with
+     [ nil ⇒ H l
+     | (cons he l') ⇒
+         match le x he
+         return
+          λb. le x he = b → l = he::l' →
+           P (he::l')
+            (match b with 
+              [ true ⇒ x::he::l'
+              | false ⇒ he::(insert ? le x l') ])
+         with
+          [ true ⇒ H2 l he l' (insert_ind l')
+          | false ⇒ H1 l he l' (insert_ind l')
+          ]
+         (refl_eq ? (le x he))
+     ] (refl_eq ? l) in insert_ind l).
 qed.
-*)
+
 
 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
  match l with
@@ -78,10 +95,8 @@ let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
   ].
 
 lemma ordered_injective:
-  ∀ A:Set. ∀ le:A → A → bool.
-  ∀ l:list A.
-  ordered A le l = true
-  \to ordered A le (tail A l) = true.
+  ∀A:Set. ∀le:A → A → bool.
+   ∀l:list A. ordered A le l = true → ordered A le (tail A l) = true.
   intros 3 (A le l).
   elim l
   [ simplify; reflexivity;
@@ -110,126 +125,37 @@ lemma ordered_injective:
   ].
 qed.
 
-(*
 lemma insert_sorted:
   \forall A:Set. \forall le:A\to A\to bool.
   (\forall a,b:A. le a b = false \to le b a = true) \to
   \forall l:list A. \forall x:A.
     ordered A le l = true \to ordered A le (insert A le x l) = true.
- intros (A le H l x K).
- letin P ≝ (\lambda ll. ordered A le ll = true).
- fold simplify (P (insert A le x l)).
- apply (
-  let rec insert_ind (l: list A) \def
-  match l in list return λli. l = li → P (insert A le x li) with
-   [ nil ⇒ (? : l = [] → P [x])
-   | (cons he l') ⇒
-       match le x he
-       return
-        λb. le x he = b → l = he::l' → P (match b with 
-             [ true ⇒ x::he::l'
-             | false ⇒ he::(insert A le x l') ])
-       with
-        [ true ⇒ (? : le x he = true → l = he::l' → P (x::he::l'))
-        | false ⇒
-            (? : \forall lrec. P (insert A le x lrec) \to
-                  le x he = false → l = he::l' → P (he::(insert A le x l')))
-            l' (insert_ind l')
+ intros 5 (A le H l x).
+ apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
+ clear l; intros; simplify; intros;
+  [2: rewrite > H1;
+    [ generalize in match (H ? ? H2); clear H2; intro;
+      generalize in match H4; clear H4;
+      elim l'; simplify;
+      [ rewrite > H5;
+        reflexivity
+      | elim (le x s); simplify;
+        [ rewrite > H5;
+          reflexivity
+        | simplify in H4;
+          rewrite > (andb_true_true ? ? H4);
+          reflexivity
         ]
-       (refl_eq ? (le x he))
-   ] (refl_eq ? l) in insert_ind l);
-  
-  intros; simplify;
-  [ rewrite > H1;
-    apply andb_elim; simplify;
-    generalize in match K; clear K;
-    rewrite > H2; intro;
-    apply H3
-  | 
+      ]
+    | apply (ordered_injective ? ? ? H4)
+    ]
   | reflexivity
-  ]. 
-    
-    
-    
-
-  
-  
-  [ rewrite > H1; simplify;
-    generalize in match (ordered_injective A le l K);
-    rewrite > H2; simplify; intro; change with (ordered A le l' = true).
-    elim l'; simplify;
-     [ reflexivity 
-     | 
-          
-    
-  rewrite > H1; simplify.
-    elim l'; [ reflexivity | simplify; 
-  | simplify.
-  | reflexivity.
+  | rewrite > H2;
+    rewrite > H4;
+    reflexivity
   ].
-*)
-
-lemma insert_sorted:
-  \forall A:Set. \forall le:A\to A\to bool.
-  (\forall a,b:A. le a b = false \to le b a = true) \to
-  \forall l:list A. \forall x:A.
-    ordered A le l = true \to ordered A le (insert A le x l) = true.
-  intros 5 (A le H l x).
-  elim l;
-  [ 2: simplify;
-       apply (bool_elim ? (le x s));
-       [ intros;
-         simplify;
-         fold simplify (ordered ? le (s::l1));
-         apply andb_elim;
-         rewrite > H3;
-         assumption;
-       | change with (le x s = false → ordered ? le (s::insert A le x l1) = true);
-         generalize in match H2;
-         clear H1; clear H2;
-         generalize in match s;
-         clear s;
-         elim l1
-         [ simplify;
-           rewrite > (H x a H2);
-           reflexivity;
-         | simplify in \vdash (? ? (? ? ? %) ?);
-            change with (ordered A le (a::(insert A le x (s::l2))) = true);
-            simplify;
-            apply (bool_elim ? (le x s));
-            [ intros;
-              simplify;
-              fold simplify (ordered A le (s::l2));
-              apply andb_elim;
-              rewrite > (H x a H3);
-              simplify;
-              fold simplify (ordered A le (s::l2));
-              apply andb_elim;
-              rewrite > H4;
-              apply (ordered_injective A le (a::s::l2));
-              assumption;
-            | intros;
-              simplify;
-              fold simplify (ordered A le (s::(insert A le x l2)));
-              apply andb_elim;
-              simplify in H2;
-              fold simplify (ordered A le (s::l2)) in H2;
-              generalize in match H2;
-              apply (andb_elim (le a s));
-              elim (le a s);
-              [ change with (ordered A le (s::l2) = true \to ordered A le (s::insert A le x l2) = true);
-                intros;
-                apply (H1 s);
-                assumption;
-              | simplify; intros; assumption
-              ]
-           ]
-         ]
-      ]
-   | simplify; reflexivity;
-   ]
 qed.
-
+  
 theorem insertionsort_sorted:
   ∀A:Set.
   ∀le:A → A → bool.∀eq:A → A → bool.
@@ -240,7 +166,7 @@ theorem insertionsort_sorted:
   elim l;
   [ simplify;
     reflexivity;
-  | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
+  | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
     assumption;
   ]
 qed.
\ No newline at end of file