diff options
| -rw-r--r-- | LocallySorted.v | 44 |
1 files changed, 0 insertions, 44 deletions
diff --git a/LocallySorted.v b/LocallySorted.v deleted file mode 100644 index 8f62641348..0000000000 --- a/LocallySorted.v +++ /dev/null @@ -1,44 +0,0 @@ -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. - - |