Proof using function induction terminated. It's really gorgeous.

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index 455462d8d67f823e3712a4cc587cee284da76964..e620ed5369d3eefaa3c387a87e0fe5c12ec54693 100644 (file)
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -49,6 +49,43 @@ let rec insert (A:Set) (le: A → A → bool) x (l: list A) on 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
   [ nil ⇒ []
@@ -90,59 +127,34 @@ 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).
- 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 ⇒ ?
-   | (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 ⇒ ?
-        | false ⇒ let res ≝ insert_ind l' in ?         
-        ]
-       (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;
+ apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
+ intros; simplify; intros;
+  [2: rewrite > H1;
+    [ generalize in match (H ? ? H2); clear H2; intro;
+      generalize in match H4; clear H4;
       elim l'; simplify;
-      [ rewrite > H4;
+      [ rewrite > H5;
         reflexivity
       | elim (le x s); simplify;
-        [ rewrite > H4;
+        [ rewrite > H5;
           reflexivity
-        | simplify in H3;
-          rewrite > (andb_true_true ? ? H3);
+        | simplify in H4;
+          rewrite > (andb_true_true ? ? H4);
           reflexivity
         ]
       ]
-      
-    | apply (ordered_injective ? ? ? H3)
+    | apply (ordered_injective ? ? ? H4)
     ]
-  | rewrite > H1;
-    rewrite > H3;
-    reflexivity
   | reflexivity
+  | rewrite > H2;
+    rewrite > H4;
+    reflexivity
   ].
 qed.