| false ⇒ he::(insert A le x l')
]
].
-(*
-theorem insert_ind:
- ∀A:Set. ∀le: A → A → bool. ∀x:A.
- ∀P: list A → Prop.
- ∀l:list A. P (insert A le x l).
- intros (A le x P H l).
- apply (
- let rec insert_ind (l: list A) ≝
- match l in list return λl.P (insert A le x l) with
- [ nil ⇒ (? : P [x])
- | (cons he l') ⇒
- match le x he return λb.P (match b with [ true ⇒ x::he::l' | false ⇒ he::(insert A le x l') ]) with
- [ true ⇒ (H2 : P (x::he::l'))
- | false ⇒ (? : P (he::(insert A le x l')))
- ]
- ]
- in
- insert_ind l).
+
+lemma insert_ind :
+ ∀A:Set. ∀le: A → A → bool. ∀x.
+ ∀P:(list A → list A → Prop).
+ ∀H:(∀l: list A. l=[] → P [] [x]).
+ ∀H2:
+ (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+ le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
+ ∀H3:
+ (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+ le x he = true → l=he::l' → P (he::l') (x::he::l')).
+ ∀l:list A. P l (insert ? le x l).
+ intros.
+ apply (
+ let rec insert_ind (l: list A) \def
+ match l in list
+ return
+ λli.
+ l = li → P li (insert ? le x li)
+ with
+ [ nil ⇒ H l
+ | (cons he l') ⇒
+ match le x he
+ return
+ λb. le x he = b → l = he::l' →
+ P (he::l')
+ (match b with
+ [ true ⇒ x::he::l'
+ | false ⇒ he::(insert ? le x l') ])
+ with
+ [ true ⇒ H2 l he l' (insert_ind l')
+ | false ⇒ H1 l he l' (insert_ind l')
+ ]
+ (refl_eq ? (le x he))
+ ] (refl_eq ? l) in insert_ind l).
qed.
-*)
+
let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
match l with
].
lemma ordered_injective:
- ∀ A:Set. ∀ le:A → A → bool.
- ∀ l:list A.
- ordered A le l = true
- \to ordered A le (tail A l) = true.
+ ∀A:Set. ∀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;
].
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 (A le H l x K).
- letin P ≝ (\lambda ll. ordered A le ll = true).
- fold simplify (P (insert A le x l)).
- apply (
- let rec insert_ind (l: list A) \def
- match l in list return λli. l = li → P (insert A le x li) with
- [ nil ⇒ (? : l = [] → P [x])
- | (cons he l') ⇒
- match le x he
- return
- λb. le x he = b → l = he::l' → P (match b with
- [ true ⇒ x::he::l'
- | false ⇒ he::(insert A le x l') ])
- with
- [ true ⇒ (? : le x he = true → l = he::l' → P (x::he::l'))
- | false ⇒
- (? : \forall lrec. P (insert A le x lrec) \to
- le x he = false → l = he::l' → P (he::(insert A le x l')))
- l' (insert_ind l')
+ intros 5 (A le H l x).
+ apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
+ 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;
+ [ rewrite > H5;
+ reflexivity
+ | elim (le x s); simplify;
+ [ rewrite > H5;
+ reflexivity
+ | simplify in H4;
+ rewrite > (andb_true_true ? ? H4);
+ reflexivity
]
- (refl_eq ? (le x he))
- ] (refl_eq ? l) in insert_ind l);
-
- intros; simplify;
- [ rewrite > H1;
- apply andb_elim; simplify;
- generalize in match K; clear K;
- rewrite > H2; intro;
- apply H3
- |
+ ]
+ | apply (ordered_injective ? ? ? H4)
+ ]
| reflexivity
- ].
-
-
-
-
-
-
- [ rewrite > H1; simplify;
- generalize in match (ordered_injective A le l K);
- rewrite > H2; simplify; intro; change with (ordered A le l' = true).
- elim l'; simplify;
- [ reflexivity
- |
-
-
- rewrite > H1; simplify.
- elim l'; [ reflexivity | simplify;
- | simplify.
- | reflexivity.
+ | rewrite > H2;
+ rewrite > H4;
+ reflexivity
].
-*)
-
-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;
- ]
qed.
-
+
theorem insertionsort_sorted:
∀A:Set.
∀le:A → A → bool.∀eq:A → A → bool.
elim l;
[ simplify;
reflexivity;
- | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
+ | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
assumption;
]
qed.
\ No newline at end of file
projects / helm.git / blobdiff