Using destruct on pattern match expression with 'convoy pattern'

user_5339728 0
Viewed 339

For the purpose of this question, suppose I have:

Parameter eq_bool : forall (A:Type), A -> A -> bool.

Arguments eq_bool {A} _ _.

Axiom eq_bool_correct : forall (A:Type) (x y:A),
    eq_bool x y = true -> x = y.

Axiom eq_bool_correct' : forall (A:Type) (x y:A),
     x = y -> eq_bool x y = true.

I have a function which given two valuesx y:A returns Some proof of x = y whenever x = y and None otherwise. This function is implemented with a pattern match on eq_bool x y to test for equality, and uses the convoy pattern as a trick to get access within your code to a proof of the equality corresponding to the branch of your match:

Definition test (A:Type) (x y:A) : option (x = y) :=
    match eq_bool x y as b return eq_bool x y = b -> option (x = y) with
    | true  => fun p => Some (eq_bool_correct A x y p)
    | false => fun _ => None
    end (eq_refl (eq_bool x y)).

I am now attempting to prove a simple result about this function:

Theorem basic: forall (A:Type) (x y:A),
    x = y -> test A x y <> None.
Proof.
    intros A x y H. rewrite H. unfold test.

A : Type
x, y : A
H : x = y
============================
(if eq_bool y y as b return (eq_bool y y = b -> option (y = y))
 then fun p : eq_bool y y = true => Some (eq_bool_correct A y y p)
 else fun _ : eq_bool y y = false => None) eq_refl <> None

At this point it feels I have to use destruct on eq_bool y y (possibly keeping equation):

destruct (eq_bool y y).

Error: Abstracting over the term "b" leads to a term
fun b0 : bool =>
(if b0 as b1 return (b0 = b1 -> option (y = y))
 then fun p : b0 = true => Some (eq_bool_correct A y y p)
 else fun _ : b0 = false => None) eq_refl <> None
which is ill-typed.
Reason is: Illegal application: 
The term "eq_bool_correct" of type
 "forall (A : Type) (x y : A), eq_bool x y = true -> x = y"
cannot be applied to the terms
 "A" : "Type"
 "y" : "A"
 "y" : "A"
 "p" : "b0 = true"
The 4th term has type "b0 = true" which should be coercible to
 "eq_bool y y = true".

I know I have to read CPDT (especially on convoy pattern) but I have a better learning experience with the Software Foundation book (which is suited for beginners): at my current level of skills, I cannot think of anything but destruct and was hoping someone could suggest a way to finish this proof.

coq
1 Answers

This is the typical case where careless abstraction makes terms ill-typed. In general, you want to use slightly different principles as to avoid these problems, matching on sumbool or reflect may provide you with better results.

In this particular case, in order for things to go through you first need to generalize the goal a bit (so it doesn't depend on eq_refl, which is a problem when matching as its typing rule is too strict) and then select the proper subterms. I use the ssreflect pattern language as it is far more convenient:

(* Do From Coq Require Import ssreflect. *)
Theorem basic (A : Type) (x y : A) (p : x = y) : test x y <> None.
Proof.
rewrite p /test; move: eq_refl; case: {2 3}(eq_dec y y) => //.
by rewrite eq_dec_correct'.
Qed.

Indeed, we need to select for matching the occurrences of eq_dec in the match and in the right side of the equality proof. You can step the above proof, or you could see the above as building and proving a more general lemma:

Theorem basic0 (A : Type) (x : A) b (p : eq_dec x x = b) :
  match b as b1 return eq_dec x x = b1 -> option (x = x) with
  | true  => fun p => Some (eq_dec_correct p)
  | false => fun _ => None
  end p <> None.
Proof. by case: b p; rewrite ?eq_dec_correct'. Qed.

Theorem basic1 (A : Type) (x y : A) (p : x = y) : test x y <> None.
Proof. by rewrite p; apply: basic0. Qed.

Note how here, by carefully choosing our parameters, we avoid having to perform tricks with pattern-selection. The key step is to "unlink" the boolean in the match from the eq_dec witness present in the "convoy" argument, so we can still correctly type the call to eq_dec_correct. The last interesting bit is that we also have to turn eq_dec x x = eq_dec x x into eq_dec x x = b, thus we need to abstract over the equality proof.

But as I said before, you'll likely want to define even a more general lemma. [Why not use some of the lemmas already present in eqtype?]

user_19556960
Related