Library coqrel.RDestruct

Require Export RelDefinitions.

The RDestruct class

Introducing the hypothesis to be destructed

The goal of rdestruct is usually to make progress on a goal relating two match constructions, by breaking down the terms being matched. The instances below will attempt to prove automatically that these terms are related, then destruct the resulting hypothesis in order to break them down and reduce the matches.

If proving the destructed hypothesis automatically is not possible, the user can use the following tactic to introduce it manually.

Ltac rdestruct_assert :=
  lazymatch goal with
    | |- _ (match ?m with _ ⇒ _ end) (match ?n with _ ⇒ _ end) ⇒
      let Tm := type of m in
      let Tn := type of n in
      let R := fresh "R" in
      evar (R: rel Tm Tn);
      assert (R m n); subst R
  end.

RDestruct steps

Sometimes we want to remember what the destructed terms were. To make this possible, we use the following relation to wrap the subgoals generated by the RDestruct instance.

Definition rdestruct_result {A B} m n (Q: rel A B): rel A B :=
fun x y ⇒ m = x ∧ n = y → Q x y.

To use RDestruct instances to reduce a goal involving pattern matching G := _ (match m with _ end) (match n with _ end), we need to establish that m and n are related by some relation R, then locate an instance of RDestruct that corresponds to R. It is essential that this happens in one step. At some point, I tried to split the process in two different RSteps, so that the user could control the resolution of the ?R m n subgoal. However, in situation where RDestruct is not the right strategy, this may push a delayed rauto into a dead end. Thankfully, now we can use the RAuto typeclass to solve the ?R m n subgoal in one swoop.

Lemma rdestruct_rstep {A B} m n (R: rel A B) P (Q: rel _ _):
  RAuto (R m n) →
  RDestruct R P →
  P (rdestruct_result m n Q) →
  Q m n.
Proof.
  intros Hmn HR H.
  firstorder.
Qed.

Ltac use_rdestruct_rstep m n :=
  let H := fresh in
  intro H;
  pattern m, n;
  eapply (rdestruct_rstep m n);
  [ .. | eexact H].

Hint Extern 40 (RStep _ (_ (match ?m with _⇒_ end) (match ?n with _⇒_ end))) ⇒
  use_rdestruct_rstep m n : typeclass_instances.

Choosing to discard or keep equations

The RStep above will leave us with a bunch of rdestruct_result subgoals. The next RStep will unpack them, and either discard or keep equations.

By default, we discard equations. This is to prevent them from cluttering the context, possibly interfering with further steps, and introducing unwanted dependencies. However, the user can use the rdestruct_remember and rdestruct_forget tactics below to control this behavior.

CoInductive rdestruct_remember := rdestruct_remember_intro.

Ltac rdestruct_remember :=
  lazymatch goal with
    | _ : rdestruct_remember |- _ ⇒
      idtac
    | _ ⇒
      let H := fresh "Hrdestruct" in
      pose proof rdestruct_remember_intro as H
  end.

Ltac rdestruct_forget :=
  lazymatch goal with
    | H : rdestruct_remember |- _ ⇒
      clear H
    | _ ⇒
      idtac
  end.

The following RStep instance will keep or discard the equations in rdestruct_result based on the user's choice.

Lemma rdestruct_forget_rintro {A B} m n (Q: rel A B) x y:
  RIntro (Q x y) (rdestruct_result m n Q) x y.
Proof.
  firstorder.
Qed.

Lemma rdestruct_remember_rintro {A B} m n (Q: rel A B) x y:
  RIntro (m = x → n = y → Q x y) (rdestruct_result m n Q) x y.
Proof.
  firstorder.
Qed.

Ltac rdestruct_result_rintro :=
  lazymatch goal with
    | _ : rdestruct_remember |- _ ⇒
      eapply rdestruct_remember_rintro
    | _ ⇒
      eapply rdestruct_forget_rintro
  end.

Hint Extern 100 (RIntro _ (rdestruct_result _ _ _) _ _) ⇒
  rdestruct_result_rintro : typeclass_instances.

Default instance

We provide a default instance of RDestruct by reifying the behavior of the destruct tactic on the relational hypothesis that we're trying to destruct.

Ltac default_rdestruct :=
  let m := fresh "m" in
  let n := fresh "n" in
  let Hmn := fresh "H" m n in
  let P := fresh "P" in
  let H := fresh in
  intros m n Hmn P H;
  revert m n Hmn;
  delayed_conjunction (intros m n Hmn; destruct Hmn; delay);
  pattern P;
  eexact H.

Hint Extern 100 (RDestruct _ _) ⇒
  default_rdestruct : typeclass_instances.

In the special case where the terms matched on the left- and right-hand sides are identical, we want to destruct that term instead. We accomplish this by introducing a special instance of RDestruct for the relation eq.

Ltac eq_rdestruct :=
  let m := fresh "m" in
  let n := fresh "n" in
  let Hmn := fresh "H" m n in
  let P := fresh "P" in
  let H := fresh in
  intros m n Hmn P H;
  revert m n Hmn;
  delayed_conjunction (intros m n Hmn; destruct Hmn; destruct m; delay);
  pattern P;
  eexact H.

Hint Extern 99 (RDestruct eq _) ⇒
  eq_rdestruct : typeclass_instances.