Coq - How can you apply an implication with a match clause?

Question

I am writing a proof of the correctness of quicksort.

My program defines a partition type, which handles the recursive partitioning step of quicksort.

Inductive partition : Type :=
  | empty
  | join (left: partition) (pivot: nat) (right: partition).

And a function which checks if a partition is sorted

Fixpoint p_sorted (p: partition) : bool :=
  match p with
  | empty => true
  | join l pivot r => match l, r with
    | empty, empty => true
    | join _ lp _, empty => if lp <=? pivot then p_sorted l else false
    | empty, join _ rp _ => if pivot <=? rp then p_sorted r else false
    | join _ lp _, join _ rp _ => if (lp <=? pivot) && (pivot <=? rp) then
      (p_sorted l) && (p_sorted r) else false
    end
  end.

I have written a Lemma with the following structure, which states that a sorted partition's left and right partitions must also be sorted. This lemma uses the "match with" syntax to break a partition apart into its left and right sub-partitions:

Lemma foo : forall (p: partition), (match p with
    | empty => True
    | join left pivot right => (p_sorted p = true) -> (p_sorted left = true) /\ (p_sorted right = true)
    end).
    Proof. (* ... proof ... *) Qed.

This lemma is already proven.

Now, I want to use it in a new proof, where the hypothesis is of the form p_sorted x = true

How do I apply my previous lemma, to transform it into p_sorted left = true /\ p_sorted right = true?

apply foo fails to unify because of the pattern matching construct.

Blaisorblade Blaisorblade · Accepted Answer · 2020-11-08T00:13:26

You can use pose proof (foo x) as Hfoo. You'll then need to use destruct x; in the case where x is not empty, you'll have something to apply.

However, such a proof is awkward, so I'd recommend improving the "API" of your theory, that is, the way foo is stated; best specialize foo to the p = join ... case.

EDIT: In fact, some proofs might be simplified by revising the definitions of p_sorted. That definition needs to pattern-match a tree “2-level down” and repeat some logic, so foo will likely need to repeat the 2-level case distinction. Instead, the code could be written similarly to the following (untested):

Definition get_root (p : partition) : option nat :=
  match p with
  | empty => None
  | join _ pivot _ => Some pivot
  end.
Definition onat_le (p1 p2 : option nat) :=
  match p1, p2 with
  | Some n1, Some n2 => n1 <=? n2
  | _, _ => false
  end.

Fixpoint p_sorted (p: partition) : bool :=
  match p with
  | empty => true
  | join l pivot r => p_sorted l && p_sorted r && onat_le (get_root l) (Some pivot) && onat_le (Some pivot) (get_root r)
  end.

Lemma foo l pivot r:
  p_sorted (join l pivot r) = true -> p_sorted l = true /\ p_sorted r = true.
Proof.
  simpl. intros Hsort. split.
  - destruct (p_sorted l); simpl in *; easy.
  - destruct (p_sorted r); simpl in *; easy.
Qed.

Coq - How can you apply an implication with a match clause?

1 Answers