(** * Perm: Basic Techniques for Comparisons and Permutations *)
(** To verify sorting algorithms (and some data structures) we
need to reason about comparisons and permutations. *)
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Strings.String. (* for manual grading *)
From Coq Require Export Bool.Bool.
From Coq Require Export Arith.Arith.
From Coq Require Export Arith.EqNat.
From Coq Require Export Omega.
From Coq Require Export Lists.List.
Export ListNotations.
From Coq Require Export Permutation.
(* ################################################################# *)
(** * The Less-Than Order on the Natural Numbers *)
(** Coq defines propositional and Boolean less-than operators. *)
Locate "_ < _". (* "x < y" := lt x y *)
Check lt : nat -> nat -> Prop.
Locate "_ nat -> bool.
Check Nat.ltb_lt : forall n m : nat, (n n < m.
(** For unknown reasons, [Nat] does not define notations
for [>?] or [>=?]. So we define them here: *)
Notation "a >=? b" := (Nat.leb b a)
(at level 70) : nat_scope.
Notation "a >? b" := (Nat.ltb b a)
(at level 70) : nat_scope.
(* ################################################################# *)
(** * Swapping *)
(** Consider trying to sort a list of natural numbers. As a small piece of
a sorting algorithm, we might need to swap the first two elements of a list
if they are out of order. *)
Definition maybe_swap (al: list nat) : list nat :=
match al with
| a :: b :: ar => if a >? b then b :: a :: ar else a :: b :: ar
| _ => al
end.
Example maybe_swap_123:
maybe_swap [1; 2; 3] = [1; 2; 3].
Proof. reflexivity. Qed.
Example maybe_swap_321:
maybe_swap [3; 2; 1] = [2; 3; 1].
Proof. reflexivity. Qed.
(** Applying [maybe_swap] twice should give the same result as applying it once.
That is, [maybe_swap] is _idempotent_. *)
Theorem maybe_swap_idempotent: forall al,
maybe_swap (maybe_swap al) = maybe_swap al.
Proof.
intros [ | a [ | b al]]; simpl; try reflexivity.
destruct (b b = true -> reflect P b.
(** Using that theorem, we can quickly prove that the (in)equality operators
are reflections. *)
Lemma eqb_reflect : forall x y, reflect (x = y) (x =? y).
Proof.
intros x y. apply iff_reflect. symmetry.
apply Nat.eqb_eq.
Qed.
Lemma ltb_reflect : forall x y, reflect (x < y) (x ? b); simpl.
(** Note how [b < a] is a hypothesis, rather than [b ? a); simpl.
+ (** [omega] can take care of the contradictory propositional inequalities. *)
omega.
+ reflexivity.
- bdestruct (a >? b); simpl.
+ omega.
+ reflexivity.
Qed.
(** When proving theorems about a program that uses Boolean
comparisons, use [bdestruct] followed by [omega], rather than
[destruct] followed by application of various theorems about
Boolean operators. *)
(* ################################################################# *)
(** * Permutations *)
(** Function [maybe_swap] _permutes_ list elements. *)
(** Coq's [Permutation] library has an inductive definition of
permutations. *)
Print Permutation.
Example perm_example : Permutation [1;1;2] [2;1;1].
Proof.
(* WORK IN CLASS *) Admitted.
(** The [Permutation] library has many useful theorems, too. *)
Search Permutation.
(* ================================================================= *)
(** ** Correctness of [maybe_swap] *)
(** Now we can prove that [maybe_swap] is a permutation: it reorders
elements but does not add or remove any. *)
Theorem maybe_swap_perm: forall al,
Permutation al (maybe_swap al).
Proof.
(* WORK IN CLASS *) Admitted.
(** And, we can prove that [maybe_swap] permutes elements such that
the first is less than or equal to the second. *)
Definition first_le_second (al: list nat) : Prop :=
match al with
| a :: b :: _ => a <= b
| _ => True
end.
Theorem maybe_swap_correct: forall al,
Permutation al (maybe_swap al)
/\ first_le_second (maybe_swap al).
Proof.
intros. split.
- apply maybe_swap_perm.
- (* WORK IN CLASS *) Admitted.
(** * An Inversion Tactic
We define it here for sake of import in future files. *)
(** Coq's [inversion H] tactic is so good at extracting
information from the hypothesis [H] that [H] sometimes becomes
completely redundant, and one might as well [clear] it from the
goal. Then, since the [inversion] typically creates some equality
facts, why not then [subst] ? Tactic [inv] does just that. *)
Ltac inv H := inversion H; clear H; subst.