let l'' ≝ insertionsort A le l' in
insert A le he l''
].
-
+
lemma ordered_injective:
∀ A:Set. ∀ le:A → A → bool.
∀ l:list A.
].
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).
- elim l;
- [ 2: simplify;
- apply (bool_elim ? (le x s));
- [ intros;
- simplify;
- fold simplify (ordered ? le (s::l1));
- apply andb_elim;
- rewrite > H3;
- assumption;
- | 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 (? ? (? ? ? %) ?);
- 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
- ]
- ]
- ]
+ 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;
+ elim l'; simplify;
+ [ rewrite > H4;
+ reflexivity
+ | elim (le x s); simplify;
+ [ rewrite > H4;
+ reflexivity
+ | simplify in H3;
+ rewrite > (andb_true_true ? ? H3);
+ reflexivity
+ ]
]
- | simplify; reflexivity;
- ]
+
+ | apply (ordered_injective ? ? ? H3)
+ ]
+ | rewrite > H1;
+ rewrite > H3;
+ reflexivity
+ | reflexivity
+ ].
qed.
-
+
theorem insertionsort_sorted:
∀A:Set.
∀le:A → A → bool.∀eq:A → A → bool.
| apply (insert_sorted A le le_tot (insertionsort A le l1) s);
assumption;
]
-qed.
-
-(*
-theorem insertionsort_correct:
- ∀A:Set.
- ∀le:A → A → bool.∀eq:A → A → bool.
- (∀a,b:A. le a b = false → le b a = true) \to
- ∀l,l':list A.
- l' = insertionsort A le l
- \to ordered A le l' = true
- ∧ ((\forall x:A. mem A eq x l = true \to mem A eq x l' = true)
- ∧ (\forall x:A. mem A eq x l = true \to mem A eq x l' = true)).
- intros;
- split;
- [ rewrite > H1;
- apply (insertionsort_sorted A le eq H);
- | split;
- [ TO BE CONTINUED ...
-*)
+qed.
\ No newline at end of file