simplified coercDb implementation with additional info about the position of

[helm.git] / helm / software / matita / contribs / dama / dama / models / list_support.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/list_support.ma b/helm/software/matita/contribs/dama/dama/models/list_support.ma
index 3aec1a0242a1b3c86c7f4743c29c8f5277c21fb9..1125e2a91f119eeaaa0d549336693db925dedace 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/list_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/list_support.ma
@@ -41,10 +41,24 @@ lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.\len (\mk_list f n) = n.
 intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;
 qed.
 
-inductive sorted (T:Type) (lt : T → T → Prop): list T → Prop ≝ 
-| sorted_nil : sorted T lt []
-| sorted_one : ∀x. sorted T lt [x]
-| sorted_cons : ∀x,y,tl. lt x y → sorted T lt (y::tl) → sorted T lt (x::y::tl). 
+record rel : Type ≝ {
+  rel_T :> Type;
+  rel_op :2> rel_T → rel_T → Prop
+}.
+
+record trans_rel : Type ≝ {
+  o_rel :> rel;
+  o_tra : ∀x,y,z: o_rel.o_rel x y → o_rel y z → o_rel x z 
+}.
+
+lemma trans: ∀r:trans_rel.∀x,y,z:r.r x y → r y z → r x z.
+apply o_tra;
+qed.
+
+inductive sorted (lt : trans_rel): list (rel_T lt) → Prop ≝ 
+| sorted_nil : sorted lt []
+| sorted_one : ∀x. sorted lt [x]
+| sorted_cons : ∀x,y,tl. lt x y → sorted lt (y::tl) → sorted lt (x::y::tl). 
 
 lemma nth_nil: ∀T,i.∀def:T. \nth [] def i = def.
 intros; elim i; simplify; [reflexivity;] assumption; qed.
@@ -61,25 +75,23 @@ lemma len_gt_non_empty :
 intros; cases l in H; [intros; cases (not_le_Sn_O ? H);] intros; constructor 1;
 qed. 
 
-lemma sorted_tail: ∀T,r,x,l.sorted T r (x::l) → sorted T r l.
+lemma sorted_tail: ∀r,x,l.sorted r (x::l) → sorted r l.
 intros; inversion H; intros; [destruct H1;|destruct H1;constructor 1;]
 destruct H4; assumption;
 qed.
 
-lemma sorted_skip: 
- ∀T,r,x,y,l. 
-  transitive T r → sorted T r (x::y::l) → sorted T r (x::l).
-intros; inversion H1; intros; [1,2: destruct H2]
-destruct H5; inversion H3; intros; [destruct H5]
-[1: destruct H5; constructor 2;
-|2: destruct H8; constructor 3; [apply (H ??? H2 H5);]
-    apply (sorted_tail ???? H3);]
+lemma sorted_skip: ∀r,x,y,l. sorted r (x::y::l) → sorted r (x::l).
+intros (r x y l H1); inversion H1; intros; [1,2: destruct H]
+destruct H4; inversion H2; intros; [destruct H4]
+[1: destruct H4; constructor 2;
+|2: destruct H7; constructor 3; [ apply (o_tra ? ??? H H4);]
+    apply (sorted_tail ??? H2);]
 qed.
 
-lemma sorted_tail_bigger : ∀T,r,x,l,d.sorted T r (x::l) → ∀i. i < \len l → r x (\nth l d i).
+lemma sorted_tail_bigger : ∀r,x,l,d.sorted r (x::l) → ∀i. i < \len l → r x (\nth l d i).
 intros 4; elim l; [ cases (not_le_Sn_O i H1);]
 cases i in H2;
-[2: intros; apply (H d ? n);[apply (sorted_skip ????? H1)|apply le_S_S_to_le; apply H2]
+[2: intros; apply (H ? n);[apply (sorted_skip ???? H1)|apply le_S_S_to_le; apply H2]
 |1: intros; inversion H1; intros; [1,2: destruct H3]
     destruct H6; simplify; assumption;]
 qed.