时间戳

首页 > 解决方案 > 当参数在范围内时自动专门化 forall

coq - 当参数在范围内时自动专门化 forall

问题描述

考虑以下简单问题：

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实例化的实现，导致时间和内存使用的二次膨胀。相反，我希望它检查并看到它需要 a ，因此在上下文中有意义的唯一参数组合是and then 。H1natforallR m nab

有一个已知的解决方案吗？我的直觉是使用 evas，但如果我可以在不牺牲显着性能的情况下避免使用它们，我愿意。

标签： coqcoq-tactic

解决方案

这可能太简单了，我们的想法是尝试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.

推荐阅读