# PermBasic Techniques for Comparisons and Permutations

To verify sorting algorithms (and some data structures) we need to reason about comparisons and permutations.

# The Less-Than Order on the Natural Numbers

Coq defines propositional and Boolean less-than operators.

Locate "_ < _". (* "x < y" := lt x y *)
Check lt : natnatProp.

Locate "_ <? _". (* x <? y  := Nat.ltb x y *)
Check Nat.ltb : natnatbool.

Check Nat.ltb_lt : n m : nat, (n <? m) = truen < 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 :: arif 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: al,
maybe_swap (maybe_swap al) = maybe_swap al.
Proof.
intros [ | a [ | b al]]; simpl; try reflexivity.
destruct (b <? a) eqn:Hb_lt_a; simpl.
- destruct (a <? b) eqn:Ha_lt_b; simpl.
+ Fail omega.
Abort.
Let's set up some machinery to enable using omega on boolean tests.

## Reflection

The reflect type, defined in the standard library (and presented in IndProp), relates a proposition to a Boolean. That is, a value of type reflect P b contains a proof of P if b is true, or a proof of ¬ P if b is false.

Print reflect.

Check iff_reflect : (P : Prop) (b : bool),
Pb = truereflect P b.
Using that theorem, we can quickly prove that the (in)equality operators are reflections.

Lemma eqb_reflect : x y, reflect (x = y) (x =? y).
Proof.
intros x y. apply iff_reflect. symmetry.
apply Nat.eqb_eq.
Qed.

Lemma ltb_reflect : x y, reflect (x < y) (x <? y).
Proof.
intros x y. apply iff_reflect. symmetry.
apply Nat.ltb_lt.
Qed.

Lemma leb_reflect : x y, reflect (xy) (x <=? y).
Proof.
intros x y. apply iff_reflect. symmetry.
apply Nat.leb_le.
Qed.
An example of using ltb_reflect:

Example reflect_example1: a,
(if a <? 5 then a else 2) < 6.
Proof.
intros a.
(* The next two lines aren't strictly necessary, but they
help make it clear what destruct does. *)

assert (R: reflect (a < 5) (a <? 5)) by apply ltb_reflect.
remember (a <? 5) as guard.
destruct R as [H|H] eqn:HR.
× (* ReflectT *) omega.
× (* ReflectF *) omega.
Qed.
A less didactic version of the above proof wouldn't do the assert and remember: we can directly skip to destruct.

Example reflect_example1': a,
(if a <? 5 then a else 2) < 6.
Proof.
intros a. destruct (ltb_reflect a 5); omega.
Qed.
It would be nice to be able to just say something like destruct (a <? 5) and get the reflection "for free." That's what we'll engineer, next.

## A Tactic for Boolean Destruction

Hint Resolve ltb_reflect leb_reflect eqb_reflect : bdestruct.

Ltac bdestruct X :=
let H := fresh in let e := fresh "e" in
evar (e: Prop);
assert (H: reflect e X); subst e;
[eauto with bdestruct
| destruct H as [H|H];
[ | try first [apply not_lt in H | apply not_le in H]]].
This tactic makes quick, easy-to-read work of our running example.

Example reflect_example2: a,
(if a <? 5 then a else 2) < 6.
Proof.
intros.
bdestruct (a <? 5); (* instead of: destruct (ltb_reflect a 5). *)
omega.
Qed.

## Finishing the maybe_swap Proof

Now that we have bdestruct, we can finish the proof of maybe_swap's idempotence.

Theorem maybe_swap_idempotent: al,
maybe_swap (maybe_swap al) = maybe_swap al.
Proof.
intros [ | a [ | b al]]; simpl; try reflexivity.
bdestruct (a >? b); simpl.
Note how b < a is a hypothesis, rather than b <? a = true.
- bdestruct (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: 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 :: _ab
| _True
end.

Theorem maybe_swap_correct: 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.