New framework for regression of bad tests.

[helm.git] / helm / matita / library / list / sort.ma

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index 1cc127759f0b37f8778491389718224a0215a85f..ffd1e21872cd85c53c38fd3c9c518bc3a381a211 100644 (file)
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -48,6 +48,26 @@ 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).
+qed.
+*)
 
 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
  match l with
@@ -56,7 +76,7 @@ let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
       let l'' ≝ insertionsort A le l' in
        insert A le he l''
   ].
-  
+
 lemma ordered_injective:
   ∀ A:Set. ∀ le:A → A → bool.
   ∀ l:list A.
@@ -90,6 +110,65 @@ 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')
+        ]
+       (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
+  | 
+  | 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.
+  ].
+*)
+
 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
@@ -105,7 +184,8 @@ lemma insert_sorted:
          apply andb_elim;
          rewrite > H3;
          assumption;
-       | generalize in match H2;
+       | 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;
@@ -114,6 +194,8 @@ lemma insert_sorted:
            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;
@@ -161,22 +243,4 @@ theorem insertionsort_sorted:
   | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
     assumption;
   ]
-qed.
-
-(*
-theorem insertionsort_correct:
-  ∀A:Set.
-  ∀le:A → A → bool.∀eq:A → A → bool.
-  (∀a,b:A. le a b = false → le b a = true) \to
-  ∀l,l':list A.
-  l' = insertionsort A le l
-  \to ordered A le l' = true
-    ∧ ((\forall x:A. mem A eq x l = true \to mem A eq x l' = true)
-        ∧ (\forall x:A. mem A eq x l = true \to mem A eq x l' = true)).
-  intros;
-  split;
-  [ rewrite > H1; 
-    apply (insertionsort_sorted A le eq H);
-  | split;
-    [ TO BE CONTINUED ...
-*)
+qed.
\ No newline at end of file