Automatically specialize forall when the parameters are in scope

Question

Consider the following simple problem:

Goal forall (R : relation nat) (a b c d e f g h : nat), 
  (forall m n : nat, R m n -> False) -> (R a b) -> False.
Proof.
  intros ? a b c d e f g h H1 H2.
  saturate H1. (* <-- TODO implement this *)
  assumption.
Qed.

My current implementation of saturate instantiates H1 with every possible combination of nat hypotheses, leading to quadratic blowup in time and memory usage. Instead I would like it to inspect forall and see that it requires a R m n, so the only combination of parameters that makes sense in context is a and then b.

Is there a known solution to this? My intuition is to use evars, but if I could avoid them without sacrificing significant performance I would like to.

Answer 1

This might be too simplistic, the idea is to try apply H1 on every hypothesis:

Ltac saturate H :=
  match goal with
    (* For any hypothesis I... *)
  | [ I : _ |- _ ] =>

    (* 1. Clone it (to not lose information). *)
    let J := fresh I in pose proof I as J;

    (* 2. apply H. *)
    apply H in J;

    (* 3. Abort if we already knew the resulting fact. *)
    let T := type of J in
    match goal with
    | [ I1 : T, I2 : T |- _ ] => fail 2
    end + idtac;

    (* 4. Keep going *)
    try (saturate H)
  end.

Example:

Require Setoid. (* To get [relation] in scope so the example compiles *)

(* Made the example a little less trivial to better test the backtracking logic. *)
Goal forall (R S : relation nat) (a b c d e f g h : nat), 
  (forall m n : nat, R m n -> S m n) -> (R a b) -> R c d -> S a b.
Proof.
  intros R S a b c d e f g h H1 H2 H3.

  (* --- BEFORE ---
     H2: R a b
     H3: R c d
   *)

  saturate H1.

  (* --- AFTER ---
     H2: R a b
     H3: R c d
     H0: S c d
     H4: S a b
   *)

  assumption.
Qed.