Generalize no more required for elim.

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

diff --git a/helm/software/matita/library/list/sort.ma b/helm/software/matita/library/list/sort.ma
index 939cecedec6486a27274a4ce6ac834888f7c58ce..4c67cb636842ca20eaf5c1f1e7df431c693777a4 100644 (file)
--- a/helm/software/matita/library/list/sort.ma
+++ b/helm/software/matita/library/list/sort.ma
@@ -12,23 +12,30 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/list/sort/".
-
 include "datatypes/bool.ma".
 include "datatypes/constructors.ma".
-include "list/list.ma".
+include "list/in.ma".
 
-let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝
- match l with
-  [ nil ⇒ false
-  | (cons a l') ⇒
-    match eq x a with
-     [ true ⇒ true
-     | false ⇒ mem A eq x l'
-     ]
-  ].
-  
-let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝
+inductive sorted (A:Type) (P:A \to A \to Prop): list A \to Prop \def
+| sort_nil : sorted A P []
+| sort_cons : \forall x,l.sorted A P l \to (\forall y.in_list ? y l \to P x y)
+              \to sorted A P (x::l).
+              
+lemma sorted_cons_to_sorted : \forall A,P,x,l.sorted A P (x::l) \to sorted A P l.
+intros;inversion H;intros
+  [destruct H1
+  |destruct H4;assumption]
+qed.
+
+lemma sorted_to_minimum : \forall A,P,x,l.sorted A P (x::l) \to 
+                          \forall y.in_list ? y l \to P x y.
+intros;inversion H;intros;
+  [destruct H2
+  |destruct H5;apply H4;assumption]
+qed.
+
+
+let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝
  match l with
   [ nil ⇒ true
   | (cons x l') ⇒
@@ -39,7 +46,46 @@ let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝
       ]
   ].
   
-let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
+lemma sorted_to_eq_sorted_b_true :
+      \forall A,ord,ordb.
+      (\forall x,y.ord x y \to ordb x y = true) \to 
+      \forall l.sorted A ord l \to ordered A ordb l = true.
+intros 5;elim l
+  [reflexivity
+  |simplify;rewrite > H1;generalize in match H2;cases l1;intros
+     [reflexivity
+     |simplify;rewrite > H
+        [reflexivity
+        |apply (sorted_to_minimum ? ? ? ? H3);apply in_list_head]
+     |apply sort_nil
+     |apply (sorted_cons_to_sorted ? ? ? ? H3)]]
+qed.
+
+(* 
+   TODO
+   per far funzionare questa dimostrazione bisogna appoggiarsi a un
+   eqb (e utilizzare quindi in_list <-> mem), oppure modificare la definizione 
+   di sorted in modo che non si appoggi più a in_list:
+   sorted []
+   sorted [x] per ogni x
+   sorted x::y::l se ord x y e sorted y::l
+
+lemma eq_sorted_b_true_to_sorted :
+      \forall A,ord,ordb.
+      (\forall x,y.ordb x y = true \to ord x y) \to
+      \forall l.ordered A ordb l = true \to sorted A ord l.
+intros 5;elim l
+  [apply sort_nil
+  |apply sort_cons
+     [apply H1;simplify in H2;generalize in match H2;cases l1;intros
+        [reflexivity
+        |simplify in H3;simplify;apply (andb_true_true_r ? ? H3)]
+     |intros;apply H;generalize in match H2;
+      generalize in match (in_list_to_mem_true ? ? ? ? H
+        [
+*)
+
+let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝
  match l with
   [ nil ⇒ [x]
   | (cons he l') ⇒
@@ -50,7 +96,7 @@ 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.
+ ∀A:Type. ∀le: A → A → bool. ∀x.
   ∀P:(list A → list A → Prop).
    ∀H:(∀l: list A. l=[] → P [] [x]).
     ∀H2:
@@ -86,7 +132,7 @@ lemma insert_ind :
 qed.
 
 
-let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
+let rec insertionsort (A:Type) (le: A → A → bool) (l: list A) on l ≝
  match l with
   [ nil ⇒ []
   | (cons he l') ⇒
@@ -95,22 +141,20 @@ let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
   ].
 
 lemma ordered_injective:
-  ∀A:Set. ∀le:A → A → bool.
+  ∀A:Type. ∀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;
   | simplify;
-    generalize in match H1;
-    clear H1;
-    elim l1;
+    elim l1 in H1 ⊢ %;
     [ simplify; reflexivity;
-    | cut ((le s s1 \land ordered A le (s1::l2)) = true);
+    | cut ((le a a1 \land ordered A le (a1::l2)) = true);
       [ generalize in match Hcut; 
         apply andb_elim;
-        elim (le s s1);
+        elim (le a a1);
         [ simplify;
-          fold simplify (ordered ? le (s1::l2));
+          fold simplify (ordered ? le (a1::l2));
           intros; assumption;
         | simplify;
           intros (Habsurd);
@@ -126,7 +170,7 @@ lemma ordered_injective:
 qed.
 
 lemma insert_sorted:
-  \forall A:Set. \forall le:A\to A\to bool.
+  \forall A:Type. \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.
@@ -135,11 +179,10 @@ lemma insert_sorted:
  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;
+      elim l' in H4 ⊢ %; simplify;
       [ rewrite > H5;
         reflexivity
-      | elim (le x s); simplify;
+      | elim (le x a); simplify;
         [ rewrite > H5;
           reflexivity
         | simplify in H4;
@@ -157,7 +200,7 @@ lemma insert_sorted:
 qed.
   
 theorem insertionsort_sorted:
-  ∀A:Set.
+  ∀A:Type.
   ∀le:A → A → bool.∀eq:A → A → bool.
   (∀a,b:A. le a b = false → le b a = true) \to
   ∀l:list A.
@@ -166,7 +209,7 @@ theorem insertionsort_sorted:
   elim l;
   [ simplify;
     reflexivity;
-  | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
+  | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) a);
     assumption;
   ]
 qed.
\ No newline at end of file