Make equalities available in with clause ("inspect" pattern)

[yforster]

The Program mode automatically makes the equations behind a match accessible in proofs:

Program Definition test (n : nat) : {n = 0} + {n <> 0} :=
  match Nat.eqb n 0 with
    | true => left _ 
    | false => right _
  end.
Next Obligation.
  symmetry in Heq_anonymous. now eapply EqNat.beq_nat_true in Heq_anonymous.
Qed.
Next Obligation.
  symmetry in Heq_anonymous. now eapply EqNat.beq_nat_false in Heq_anonymous.
Qed.

To replay this in Equations, one has to use a trick which is apparently known as the "inspect pattern":

Notation "( a ; b )" := (exist _ a b).

Definition inspect {Y} (x : Y) : {y | x = y}.
Proof. now exists x. Qed.

Equations test (n : nat) : {n = 0} + {n <> 0} :=
  test n with inspect (Nat.eqb n 0) => {
    test n (true;H) => left _ ;
    test n (false;H) => right _
  }.
Next Obligation.
  now eapply EqNat.beq_nat_true in H.
Qed.
Next Obligation.
  now eapply EqNat.beq_nat_false in H.
Qed.

It would be nice if Equations would generate this equations automatically as well, for instance by introducing a witheq syntax, or even something more explicit where a user can choose the name of the equation.

[ybertot]

I agree. I added an example in example/Basics.v to illustrate the inspect pattern, but programming with it is error-prone.

[ybertot]

Here is a proposition for syntax:

Equations test (n : nat) : {n = 0} + {n <> 0} :=
  test n with_inspect (Nat.eqb n 0) as eq_name => {
    test n true => left _;
    test n false => right _
  }.
Next Obligation.
  now eapply EqNat.beq_nat_true in eq_name.

and so on. This forces blocking with_inspect as a key word and otherwise it fixes the name of the equation once and for all in the (as ...) clause.