RDestruct.v

Require Export RelDefinitions.

(** * The [RDestruct] class *)

(** ** Tactics *)

(** The [rdestruct] tactic locates and uses an [RDestruct] instance
  for a given hypothesis. *)

Ltac rdestruct H :=
  lazymatch type of H with
    | ?R ?m ?n =>
      not_evar R;
      pattern m, n;
      apply (rdestruct (R:=R) m n H);
      clear H;
      Delay.split_conjunction
  end.

(** The [rinversion] tactic is similar, but it remembers the terms
  related by the destructed hypothesis. *)

Ltac rinversion_tac H Hm Hn :=
  lazymatch type of H with
    | ?R ?m ?n =>
      not_evar R;
      pattern m, n;
      lazymatch goal with
        | |- ?Q _ _ =>
          generalize (eq_refl m), (eq_refl n);
          change ((fun x y => Delay.delayed_goal (x = m -> y = n -> Q x y)) m n);
          apply (rdestruct (R:=R) m n H);
          Delay.split_conjunction;
          intros Hm Hn
      end
  end.

Tactic Notation "rinversion" constr(H) "as" ident(Hl) "," ident(Hr) :=
  rinversion_tac H Hl Hr.

Tactic Notation "rinversion" hyp(H) :=
  let Hl := fresh H "l" in
  let Hr := fresh H "r" in
  rinversion_tac H Hl Hr.

Tactic Notation "rinversion" constr(H) :=
  let Hl := fresh "Hl" in
  let Hr := fresh "Hr" in
  rinversion_tac H Hl Hr.

(** ** 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 [match]es.

  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 [RStep]s, 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.