Require Export PolyList. Require Export Arith. Require Export Compare_dec. (* A list is sorted if each element is smaller than the one that follows *) Inductive sorted : (list nat) -> Prop := sorted_nil: fill_in_the_blank | sorted_1: fill_in_the_blank | sorted_2: fill_in_blank . (* A proof that can be done with only the constructors. *) Theorem test1: (sorted (cons (S (S (S O))) (cons (S (S (S (S (S O))))) (cons (S (S (S (S (S (S (S O))))))) (nil nat))))). (* Find the right Hint command so that the following proof goes completely automatically *) Theorem test1': (sorted (cons (S (S (S O))) (cons (S (S (S (S (S O))))) (cons (S (S (S (S (S (S (S O))))))) (nil nat))))). Auto 20 with *. Qed. (* Lookup the documentation of the Inversion tactic. *) Theorem test2: ~ (sorted (cons (S (S O)) (cons (S O) (nil nat)))). (* The interested readers should check the value of le_lt_dec. *) Fixpoint insert [n : nat; l : (list nat)] : (list nat) := Cases l of nil => (cons n (nil nat)) | (cons n1 l1) => Cases (le_lt_dec n n1) of (left h) => (cons n (cons n1 l1)) | (right h) => (cons n1 (insert n l1)) end end. (* insert produces a sorted list, provided it received a sorted list. *) Theorem isert_sorted: (l : (list nat)) (n : nat) (sorted l) -> (sorted (insert n l)). (* Construct a function that uses insert to sort a list. *) Fixpoint sort [l : (list nat)] : Fill_in_the_blank := Fill_in_blank. Theorem sort_correct1: (l : (list nat)) (sorted (sort l)). (* One should also make sure that the result is a permutation of the input. *) Inductive permutation : (list nat) -> (list nat) -> Prop := same_permutation: (l : (list nat)) (permutation l l) | transposition_then_permutation: (l1, l2, l3, l4 : (list nat)) (n1, n2 : nat) (permutation (app l1 (cons n2 (app l2 (cons n1 l3)))) l4) -> (permutation (app l1 (cons n1 (app l2 (cons n2 l3)))) l4) . Theorem permutation_trans: Fill_in_the_blank. Theorem permutation_sym: Fill_in_the_blank. Theorem insert_permutation: (l : (list nat)) (n : nat) (permutation (cons n l) (insert n l)). Theorem sort_permutation: (l : (list nat)) (permutation l (sort l)).