Автоматически специализировать поля, когда параметры находятся в области видимости - PullRequest
Новая
       65

Автоматически специализировать поля, когда параметры находятся в области видимости

1 голос
/ 18 марта 2020

Рассмотрим следующую простую проблему: 

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.

Моя текущая реализация saturate создает H1 с каждой возможной комбинацией nat гипотез, что приводит к квадратному c взрыву во времени и памяти Применение. Вместо этого я хотел бы, чтобы он осмотрел forall и увидел, что для этого требуется R m n, поэтому единственная комбинация параметров, которая имеет смысл в контексте, это a, а затем b.

Есть ли Известное решение этого? Моя интуиция состоит в том, чтобы использовать evars, но если бы я мог избежать их, не жертвуя при этом значительной производительностью, я бы хотел.

1 Ответ

0 голосов
/ 19 марта 2020

Это может быть слишком просто c, идея состоит в том, чтобы попробовать apply H1 на каждой гипотезе: 

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.

Пример: 

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.
...