# PermBasic Techniques for Comparisons and Permutations

# The Less-Than Order on the Natural Numbers

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

Check lt : nat → nat → Prop.

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

Check Nat.ltb : nat → nat → bool.

Check Nat.ltb_lt : ∀ n m : nat, (n <? m) = true ↔ 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

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: ∀ 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.
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.

## Reflection

Print reflect.

Check iff_reflect : ∀ (P : Prop) (b : bool),

P ↔ b = true → reflect P b.

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 (x ≤ y) (x <=? y).

Proof.

intros x y. apply iff_reflect. symmetry.

apply Nat.leb_le.

Qed.

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]]].

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

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.

+ 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

*permutes*list elements.

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

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 :: _ ⇒ a ≤ b

| _ ⇒ 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.Ltac inv H := inversion H; clear H; subst.