-*)
-
-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: simplify;
- apply (bool_elim ? (le x s));
- [ intros;
- simplify;
- fold simplify (ordered ? le (s::l1));
- apply andb_elim;
- rewrite > H3;
- assumption;
- | change with (le x s = false → ordered ? le (s::insert A le x l1) = true);
- generalize in match H2;
- clear H1; clear H2;
- generalize in match s;
- clear s;
- elim l1
- [ simplify;
- rewrite > (H x a H2);
- reflexivity;
- | simplify in \vdash (? ? (? ? ? %) ?);
- change with (ordered A le (a::(insert A le x (s::l2))) = true);
- simplify;
- apply (bool_elim ? (le x s));
- [ intros;
- simplify;
- fold simplify (ordered A le (s::l2));
- apply andb_elim;
- rewrite > (H x a H3);
- simplify;
- fold simplify (ordered A le (s::l2));
- apply andb_elim;
- rewrite > H4;
- apply (ordered_injective A le (a::s::l2));
- assumption;
- | intros;
- simplify;
- fold simplify (ordered A le (s::(insert A le x l2)));
- apply andb_elim;
- simplify in H2;
- fold simplify (ordered A le (s::l2)) in H2;
- 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
- ]
- ]
- ]
- ]
- | simplify; reflexivity;
- ]