blob: 8f62641348c67e592eb7d75ddf97311d1f80c7ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
Require Import List Program.Syntax.
Variable A:Type.
Variable le:A->A->Prop.
Infix "<=" := le.
(*
if of_sumbool H then _ else _
if H then _ else _
*)
Inductive locally_sorted : list A -> Prop :=
| nil_locally_sorted : locally_sorted []
| cons1_locally_sorted a : locally_sorted [a]
| consn_locally_sorted a b l : locally_sorted (b::l) -> a <= b -> locally_sorted (a::b::l).
Inductive lelist (a:A) : list A -> Prop :=
| nil_le : lelist a nil
| cons_le : forall (b:A) (l:list A), le a b -> lelist a (b :: l).
Inductive sort : list A -> Prop :=
| nil_sort : sort nil
| cons_sort :
forall (a:A) (l:list A), sort l -> lelist a l -> sort (a :: l).
Goal forall l, sort l -> locally_sorted l.
induction l.
constructor.
inversion 1; subst.
destruct l; constructor.
apply IHl; trivial.
inversion H3; auto.
Qed.
Goal forall l, lelist
Goal forall l, locally_sorted l -> sort l.
induction 1; constructor.
constructor.
constructor.
assumption.
inversion IHlocally_sorted; subst.
|
