# Perm: Basic Techniques for Permutations and Ordering

- sort a sequence of numbers;
- finite maps from numbers to (arbitrary-type) data
- finite maps from any ordered type to (arbitrary-type) data
- priority queues: finding/deleting the highest number in a set

- less-than comparisons on natural numbers
- permutations (rearrangements of lists)

Require Import Coq.Strings.String.

Require Export Coq.Bool.Bool.

Require Export Coq.Arith.Arith.

Require Export Coq.Arith.EqNat.

Require Export Coq.omega.Omega.

Require Export Coq.Lists.List.

Export ListNotations.

Require Export Permutation.

# The Less-Than Order on the Natural Numbers

*Propositional*and the

*Boolean*less-than operators in the Coq standard library.

Check Nat.lt. Check lt. Goal Nat.lt = lt. Proof. reflexivity. Qed. Check Nat.ltb. Locate "_ < _". Locate "<?".

We write x < y for the Proposition that x

*is*less than y, and we write x <? y for the computable*test*that returns true or false depending on whether x<y. The theorem that lt is related in this way to ltb is this one:
For some reason, the Coq library has <? and <=?
notations, but is missing these three:

Notation "a >=? b" := (Nat.leb b a)

(at level 70, only parsing) : nat_scope.

Notation "a >? b" := (Nat.ltb b a)

(at level 70, only parsing) : nat_scope.

Notation " a =? b" := (beq_nat a b)

(at level 70) : nat_scope.

That is, reflect P b means that P<->True if and only if b=true.
The way to use reflect is, for each of your operators, make a
lemma like these next three:

Lemma beq_reflect : forall x y, reflect (x = y) (x =? y).

Proof.

intros x y.

apply iff_reflect. symmetry. apply beq_nat_true_iff.

Qed.

Lemma blt_reflect : forall x y, reflect (x < y) (x <? y).

Proof.

intros x y.

apply iff_reflect. symmetry. apply Nat.ltb_lt.

Qed.

Lemma ble_reflect : forall x y, reflect (x <= y) (x <=? y).

Proof.

intros x y.

apply iff_reflect. symmetry. apply Nat.leb_le.

Qed.

Here's an example of how you could use these lemmas.
Suppose you have this simple program, (if a <? 5 then a else 2),
and you want to prove that it evaluates to a number smaller than 6.
You can use blt_reflect "by hand":

Example reflect_example1: forall a, (if a<?5 then a else 2) < 6.

Proof.

intros.

destruct (blt_reflect a 5) as [H|H].

*

omega. *

apply not_lt in H. omega.

Qed.

But there's another way to use blt_reflect, etc: read on.

## Some Advanced Tactical Hacking

You may skip ahead to "Inversion/clear/subst". Right here, we build some machinery that you'll want to*use*, but you won't need to know how to

*build*it.

Hint Resolve blt_reflect ble_reflect beq_reflect : bdestruct.

Our high-tech

*boolean destruction*tactic: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]]].

Here's a brief example of how to use bdestruct. There
are more examples later.

Example reflect_example2: forall a, (if a<?5 then a else 2) < 6.

Proof.

intros.

bdestruct (a<?5). *

omega. *

omega.

Qed.

## inversion / clear / subst

Coq's inversion H tactic is so good at extracting information from the hypothesis H that H 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 ? This motivates the following useful tactic, inv:Ltac inv H := inversion H; clear H; subst.

## Linear Integer Inequalities

Module Exploration1.

Theorem omega_example1:

forall i j k,

i < j ->

~ (k - 3 <= j) ->

k > i.

Proof.

intros.

Now, there's a hard way to prove this, and an easy way.
Here's the hard way.

Search (~ _ <= _ -> _).

apply not_le in H0.

Search (_ > _ -> _ > _ -> _ > _).

apply gt_trans with j.

apply gt_trans with (k-3).

Abort.

Theorem bogus_subtraction: ~ (forall k:nat, k > k - 3).

Proof.

intro.

specialize (H O).

simpl in H. inversion H.

Qed.

With bogus subtraction, this omega_example1 theorem even True?
Yes it is; let's try again, the hard way, to find the proof.

Theorem omega_example1:

forall i j k,

i < j ->

~ (k - 3 <= j) ->

k > i.

Proof. intros.

apply not_le in H0.

unfold gt in H0.

unfold gt.

Search (_ < _ -> _ <= _ -> _ < _).

apply lt_le_trans with j.

apply H.

apply le_trans with (k-3).

Search (_ < _ -> _ <= _).

apply lt_le_weak.

auto.

apply le_minus.

Qed.

And here's the easy way.

Here we have used the omega tactic, made available by importing
Coq.omega.Omega as we have done above. Omega is an algorithm
for integer linear programming, invented in 1991 by William Pugh.
Because ILP is NP-complete, we might expect that this algorithm is
exponential-time in the worst case, and indeed that's true: if you
have N equations, it could take 2^N time. But in the typical
cases that result from reasoning about programs, omega is much
faster than that. Coq's omega tactic is an implementation of
this algorithm that generates a machine-checkable Coq proof. It
"understands" the types Z and nat, and these operators: < = > <=
>= + - ~, as well as multiplication by small integer
literals (such as 0,1,2,3...) and some uses of \/ and /\.
Omega does
Now let's consider a silly little program: swap the first two
elements of a list, if they are out of order.

*not*understand other operators. It treats things like a*b and f x y as if they were variables. That is, it can prove f x y > a*b -> f x y + 3 >= a*b, in the same way it would prove u > v -> u+3 >= v.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.

We cannot compute with elements of Prop: we need some kind of
constructible (and pattern-matchable) value. For that we use
bool.

Locate ">?".

The name ltb stands for "less-than boolean."

Instead of defining an operator Nat.geb, the standard library just
defines the notation for greater-or-equal-boolean as a
less-or-equal-boolean with the arguments swapped.

Here's a theorem: maybe_swap is idempotent -- that is, applying it
twice gives the same result as applying it once.

Theorem maybe_swap_idempotent:

forall al, maybe_swap (maybe_swap al) = maybe_swap al.

Proof.

intros.

destruct al as [ | a al].

simpl.

reflexivity.

destruct al as [ | b al].

simpl.

reflexivity.

simpl.

What do we do here? We must proceed by case analysis on
whether a>b.

Now what? Look at the hypotheses H: b<a and H0: a<b
above the line. They can't both be true. In fact, omega
"knows" how to prove that kind of thing. Let's try it:

try omega.

omega didn't work, because it operates on comparisons in Prop,
such as a>b; not upon comparisons yielding bool, such as a>?b.
We need to convert these comparisons to Prop, so that we can use
omega.
Actually, we don't "need" to. Instead, we could reason directly
about these operations in bool. But that would be even more
tedious than the omega_example1 proof. Therefore: let's set up
some machinery so that we can use omega on boolean tests.

Abort.

Let's try again, a new way:

Theorem maybe_swap_idempotent:

forall al, maybe_swap (maybe_swap al) = maybe_swap al.

Proof.

intros.

destruct al as [ | a al].

simpl.

reflexivity.

destruct al as [ | b al].

simpl.

reflexivity.

simpl.

This is where we left off before. Now, watch:

The omega tactic noticed that above the line we have an
arithmetic contradiction. Perhaps it seems wasteful to bring
out the "big gun" to shoot this flea, but really, it's easier
than remembering the names of all those lemmas about
arithmetic!

Moral of this story: When proving things about a program that uses
boolean comparisons (a <? b), use bdestruct. Then use
omega. Let's review that proof without all the comments.

Theorem maybe_swap_idempotent':

forall al, maybe_swap (maybe_swap al) = maybe_swap al.

Proof.

intros.

destruct al as [ | a al].

simpl.

reflexivity.

destruct al as [ | b al].

simpl.

reflexivity.

simpl.

bdestruct (b <? a).

*

simpl.

bdestruct (a <? b).

omega.

reflexivity.

*

simpl.

bdestruct (b <? a).

omega.

reflexivity.

Qed.

# Permutations

*permutation*of the input. The Coq Permutation library has an inductive definition of permutations, along with some lemmas about them.

We say "list al is a permutation of list bl",
written Permutation al bl, if the elements of al can be
reordered (without insertions or deletions) to get the list bl.

You might wonder, "is that really the right definition?" And
indeed, it's important that we get a right definition, because
Permutation is going to be used in the specification of
correctness of our searching and sorting algorithms. If we have
the wrong specification, then all our proofs of "correctness" will
be useless.
It's not obvious that this is indeed the right specification of
permutations. (It happens to be true, but it's not obvious!) In
order to gain confidence that we have the right specification, we
should use this specification to prove some properties that we
think permutations ought to have.
YOUR ASSIGNMENT: Add three more properties. Write them here:
Now, let's examine all the theorems in the Coq library about
permutations:

#### Exercise: 2 stars (Permutation_properties)

Think of some properties of the Permutation relation and write them down informally in English, or a mix of Coq and English. Here are four to get you started:- 1. If Permutation al bl, then length al = length bl.
- 2. If Permutation al bl, then Permutation bl al.
- 3. [1;1] is NOT a permutation of [1;2].
- 4. [1;2;3;4] IS a permutation of [3;4;2;1].

Which of the properties that you wrote down above have already
been proved as theorems by the Coq library developers? Answer
here:

☐
Let's use the permutation rules in the library to prove the
following theorem.

Example butterfly: forall b u t e r f l y : nat,

Permutation ([b;u;t;t;e;r]++[f;l;y]) ([f;l;u;t;t;e;r]++[b;y]).

Proof.

intros.

change [b;u;t;t;e;r] with ([b]++[u;t;t;e;r]).

change [f;l;u;t;t;e;r] with ([f;l]++[u;t;t;e;r]).

remember [u;t;t;e;r] as utter.

clear Hequtter.

Check app_assoc.

rewrite <- app_assoc.

rewrite <- app_assoc.

Check perm_trans.

apply perm_trans with (utter ++ [f;l;y] ++ [b]).

rewrite (app_assoc utter [f;l;y]).

Check Permutation_app_comm.

apply Permutation_app_comm.

eapply perm_trans.

2: apply Permutation_app_comm.

rewrite <- app_assoc.

Search (Permutation (_++_) (_++_)).

apply Permutation_app_head.

eapply perm_trans.

2: apply Permutation_app_comm.

simpl.

Check perm_skip.

apply perm_skip.

apply perm_skip.

Search (Permutation (_::_) (_::_)).

apply perm_swap.

Qed.

That example illustrates a general method for proving
permutations involving cons :: and append ++.
You identify some portion appearing in both sides;
you bring that portion to the front on each side using
lemmas such as Permutation_app_comm and perm_swap,
with generous use of perm_trans. Then, you use
perm_skip to cancel a single element, or Permutation_app_head
to cancel an append-chunk.

#### Exercise: 3 stars (permut_example)

Use the permutation rules in the library (see the Search, above) to prove the following theorem. These Check commands are a hint about what lemmas you'll need.Check perm_skip.

Check Permutation_refl.

Check Permutation_app_comm.

Check app_assoc.

Example permut_example: forall (a b: list nat),

Permutation (5::6::a++b) ((5::b)++(6::a++[])).

Proof.

Admitted.

☐

#### Exercise: 1 star (not_a_permutation)

Prove that [1;1] is not a permutation of [1;2]. Hints are given as Check commands.Check Permutation_cons_inv.

Check Permutation_length_1_inv.

Example not_a_permutation:

~ Permutation [1;1] [1;2].

Proof.

Admitted.

☐
Back to maybe_swap. We prove that it doesn't lose or gain
any elements, only reorders them.

Theorem maybe_swap_perm: forall al,

Permutation al (maybe_swap al).

Proof.

intros.

destruct al as [ | a al].

simpl. apply Permutation_refl.

destruct al as [ | b al].

simpl. apply Permutation_refl.

simpl.

bdestruct (a>?b).

apply perm_swap.

apply Permutation_refl.

Qed.

Now let us specify functional correctness of maybe_swap:
it rearranges the elements in such a way that the first is
less-or-equal than 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.

destruct al as [ | a al].

simpl. auto.

destruct al as [ | b al].

simpl. auto.

simpl.

bdestruct (b <? a).

simpl.

omega.

simpl.

omega.

Qed.

End Exploration1.

# Summary: Comparisons and Permutations

#### Exercise: 2 stars (Forall_perm)

To close, a useful utility lemma. Prove this by induction; but is it induction on al, or on bl, or on Permutation al bl, or on Forall f al ?Theorem Forall_perm: forall {A} (f: A -> Prop) al bl,

Permutation al bl ->

Forall f al -> Forall f bl.

Proof.

Admitted.

☐