New proof based on an hand-made functional induction.

[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 2d60662a4d8f19e3d3d5894110782878a9927092..2716235d0914f0cd0a4da052a5d45b58cbc9583b 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.
@@ -74,7 +94,8 @@ lemma ordered_injective:
       [ generalize in match Hcut; 
         apply andb_elim;
         elim (le s s1);
-        [ change with (ordered A le (s1::l2) = true \to ordered A le (s1::l2) = true).
+        [ simplify;
+          fold simplify (ordered ? le (s1::l2));
           intros; assumption;
         | simplify;
           intros (Habsurd);
@@ -89,61 +110,72 @@ 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 5 (A le H l x).
-  elim l;
-  [ 2: change with (ordered A le (match le x s with
-         [ true ⇒ x::(s::l1) | false ⇒ s::(insert A le x l1) ]) = true).
-       apply (bool_elim ? (le x s));
-       [ intros;
-         change with ((le x s \land ordered A le (s::l1)) = true);
-         apply andb_elim;
-         rewrite > H3;
-         assumption;
-       | generalize in match H2;
-         clear H1; clear H2;
-         generalize in match s;
-         clear s;
-         elim l1
-         [ simplify;
-           rewrite > (H x a H2);
-           reflexivity;
-         | change with ((ordered A le (a::match le x s with
-              [ true ⇒ x::s::l2 | false ⇒ s::(insert A le x l2) ])) = true).
-            apply (bool_elim ? (le x s));
-            [ intros;
-              change with ((le a x \land (le x s \land ordered A le (s::l2))) = true).
-              apply andb_elim;
-              rewrite > (H x a H3);
-              change with ((le x s \land ordered A le (s::l2)) = true).
-              apply andb_elim;
-              rewrite > H4;
-              apply (ordered_injective A le (a::s::l2));
-              assumption;
-            | intros;
-              change with ((le a s \land ordered A le (s::(insert A le x l2))) = true);
-              apply andb_elim;
-              change in H2 with ((le a s \land ordered A le (s::l2)) = true); 
-              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
-              ]
-           ]
-         ]
+ intros 5 (A le H l x).
+ apply (
+  let rec insert_ind (l: list A) \def
+  match l in list
+  return
+    λli.
+     l = li → ordered ? le li = true →
+      ordered ? le (insert A le x li) = true
+  with
+   [ nil ⇒ (? : l = [] → ordered ? le [] = true → ordered ? le [x] = true)
+   | (cons he l') ⇒
+       match le x he
+       return
+        λb. le x he = b → l = he::l' →
+         ordered ? le (he::l') = true → ordered ? le
+          (match b with 
+            [ true ⇒ x::he::l'
+            | false ⇒ he::(insert A le x l') ]) = true
+       with
+        [ true ⇒
+            (? :
+              le x he = true →
+               l = he::l' →
+                ordered ? le (he::l') = true →
+                 ordered ? le (x::he::l') = true)
+        | false ⇒
+           let res ≝ insert_ind l' in
+            (? :                  
+                  le x he = false → l = he::l' →
+                   ordered ? le (he::l') = true →
+                    ordered ? le (he::(insert ? le x l')) = true)           
+        ]
+       (refl_eq ? (le x he))
+   ] (refl_eq ? l) in insert_ind l);
+  
+  intros; simplify;
+  [ rewrite > insert_ind;
+    [ generalize in match (H ? ? H1); clear H1; intro;
+      generalize in match H3; clear H3;
+      elim l'; simplify;
+      [ rewrite > H4;
+        reflexivity
+      | elim (le x s); simplify;
+        [ rewrite > H4;
+          reflexivity
+        | simplify in H3;
+          rewrite > (andb_true_true ? ? H3);
+          reflexivity
+        ]
       ]
-   | simplify; reflexivity;
-   ]
+      
+    | apply (ordered_injective ? ? ? H3)
+    ]
+  | rewrite > H1;
+    rewrite > H3;
+    reflexivity
+  | reflexivity
+  ].
 qed.
-
+  
 theorem insertionsort_sorted:
   ∀A:Set.
   ∀le:A → A → bool.∀eq:A → A → bool.
@@ -157,22 +189,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