(* *)
(**************************************************************************)
-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') ⇒
]
].
-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') ⇒
].
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:
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') ⇒
].
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
clear H1;
elim l1;
[ simplify; reflexivity;
- | cut ((le s s1 \land ordered A le (s1::l2)) = true);
+ | cut ((le t t1 \land ordered A le (t1::l2)) = true);
[ generalize in match Hcut;
apply andb_elim;
- elim (le s s1);
+ elim (le t t1);
[ simplify;
- fold simplify (ordered ? le (s1::l2));
+ fold simplify (ordered ? le (t1::l2));
intros; assumption;
| simplify;
intros (Habsurd);
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.
elim l'; simplify;
[ rewrite > H5;
reflexivity
- | elim (le x s); simplify;
+ | elim (le x t); simplify;
[ rewrite > H5;
reflexivity
| simplify in H4;
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.
elim l;
[ simplify;
reflexivity;
- | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
+ | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) t);
assumption;
]
qed.
\ No newline at end of file