How to destruct/generalize over Program's rewritten match statements

Question

When using Program, match statements are rewritten into a "proof-passing" style. This makes evidence of the match available in the branches—which can be critical.

However, it also seems to make case analysis more difficult. For example:

Require Import ZArith.

Open Scope Z_scope.

Program Definition test (x:Z) : option (x <= 100) :=
  match Z_le_gt_dec x 100 with
  | left bound => Some _
  | right bound => None
  end.

Lemma test_gt_100 : forall x:Z, x > 100 -> test x = None.
Proof.
  intros x bound.
  unfold test.

At this point, one would normally destruct (Z_le_gt_dec x 100) and the proof is then easy. However, the rewritten match gives this context:

x : Z
bound : x > 100
============================
 match
   Z_le_gt_dec x 100 as x0
   return (x0 = Z_le_gt_dec x 100 -> option (x <= 100))
 with
 | left bound0 =>
     fun Heq_anonymous : left bound0 = Z_le_gt_dec x 100 =>
     Some (test_obligation_1 x bound0 Heq_anonymous)
 | right bound0 => fun _ : right bound0 = Z_le_gt_dec x 100 => None
 end eq_refl = None

With this, the destruct fails:

Toplevel input, characters 20-48:
Error: Abstracting over the term "s" leads to a term
"fun s : {x <= 100} + {x > 100} =>
 match s as x0 return (x0 = s -> option (x <= 100)) with
 | left bound =>
     fun Heq_anonymous : left bound = s =>
     Some (test_obligation_1 x bound Heq_anonymous)
 | right bound => fun _ : right bound = s => None
 end eq_refl = None" which is ill-typed.

Going more slowly and trying just to generalize (Z_le_gt_dec x 100) shows why:

Toplevel input, characters 0-30:
Error: Illegal application (Type Error): 
The term "test_obligation_1" of type
 "forall x : Z,
  let filtered_var := Z_le_gt_dec x 100 in
  forall bound : x <= 100, left bound = filtered_var -> x <= 100"
cannot be applied to the terms
 "x" : "Z"
 "bound0" : "x <= 100"
 "Heq_anonymous" : "left bound0 = s"
The 3rd term has type "left bound0 = s" which should be coercible to
 "left bound0 = Z_le_gt_dec x 100".

While that makes some sense, I'm at a loss about what to do about it.

(I've put this in collacoq if it's helpful. Don't forget to execute just the Comment line at first and then wait until all the libraries have loaded before importing ZArith.)

Answer 1

The problem here is that you depend on a specific equality term, abstracting over it should allow you to proceed. (It is is general good practice to state lemmas that are independent of proofs).

Here's your example, using ssreflect's rewrite. Sorry, I was unable to instruct Coq's one to do the proper pattern selection.

Comments "pkgs: coq-reals".
From mathcomp Require Import ssreflect.
Require Import Coq.ZArith.ZArith.

Open Scope Z_scope.

Program Definition test (x:Z) : option (x <= 100) :=
  match Z_le_gt_dec x 100 with
  | left  bound => Some _
  | right bound => None
  end.

Lemma test_gt_100 : forall x:Z, x > 100 -> test x = None.
Proof.
intros x hb; unfold test.
assert (Z_le_gt_dec x 100 = right hb) as Hz. admit.
move: eq_refl; rewrite {1 3}Hz.
done.

[Also at https://x80.org/collacoq/xareboqura.coq ]

Best regards, E.

EDIT: A bit more detail: At the beginning, the argument of the match is eq_refl : forall x, x = x which is ok as the function inside the match expects a term of type Z.le .... = Z.le ..... However, when performing the rewrite, the type in the match annotation will become of the form Z_le ... = right ..., but if argument is still eq_refl this will result in a badly typed term, as eq_refl can never be typed as Z.le ... = right ...!

Thus, we modify our goal so that the proof for the equality doesn't necessarily have to be eq_refl, then we rewrite.

Why the proof was done with eq_refl in the first place? This is usually done to have good reduction behavior in the presence of equality proofs.

It would be interesting to add proof-irrelevance support to Program thou. (I ignore if there's already some).