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

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: ∀ 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),
    P ↔ b = true → reflect 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 (x ≤ y) (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 :: _ ⇒ 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.
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.