1

我经常需要做“归纳加载”来证明 Coq 中的目标，在 Coq 中我通过归纳同时证明多个事物。

问题是，我经常得到以下形式的归纳假设：

forall a1 ... an, 
  Premise1 -> Premise2 -> ... Premisek -> 
  Conclusion1 /\ Conclusion2 /\ ... Conclusion_m

这很好，但是像这样的战术eauto真的不知道如何处理这样的事情，所以它大部分时间都会扼杀自动化。

我想知道的是，有没有办法自动将这样的前提分解成m不同的前提，即

forall a1 ... an, 
  Premise1 -> Premise2 -> ... Premisek -> 
  Conclusion1
  ...
forall a1 ... an, 
  Premise1 -> Premise2 -> ... Premise_k -> 
  Conclusion_m

我遇到的主要问题是我不知道如何匹配 LTac 中任意长度的箭头链。我可以硬编码到一定长度，但我希望有更好的方法。

此外，如果可以进行对偶（即拆分 Premise1 .. Premise_k 中的所有析取组合），那也是有用的。

4

2 回答 2

4

我不是 Ltac 的专家，但我尝试了一下并想出了以下策略。

Ltac decomp H :=
  try match type of H with
  context c [?A /\ ?B] =>
    let H' := fresh H in
    let Pa := context c[A] in
    assert (H' : Pa) by (apply H);
    let H'' := fresh H in
    let Pb := context c[B] in
    assert (H'' : Pb) by (apply H);
    clear H;
    rename H' into H;
    rename H'' into H';
    decomp H'
  end.

Tactic Notation "decomp_hyp" hyp(H) := decomp H.

decomp H在 中搜索出现的连词H，然后将其分解为H'and H''，清理状态并递归调用自身。

在一个简单的例子中，这似乎有效。

于 2018-10-25T10:02:59.507 回答
1

也许是这样的（减去调试打印输出）？

Ltac foo :=
  match goal with
  |  |- forall q, ?X => 
       let x := fresh in intros x; idtac x q ; (try foo); generalize x as q; clear x

  |  |- ?X -> _ => 
       let x := fresh in intros x; idtac x  ; (try foo); generalize x; clear x

  |  |- _ /\ _ => repeat split
  end; idtac "done".

Goal forall {T} (a1 a2 a3:T) P1 P2 P3 Q1 Q2 Q3, P1 a1 -> P2 a2 -> P3 a3 -> Q1 /\ Q2 /\ Q3.
  foo.

这让你有了目标

3 subgoals (ID 253)

  ============================
  forall (T : Type) (a1 a2 a3 : T) (P1 P2 P3 : T -> Type) (Q1 : Prop),
  Prop -> Prop -> P1 a1 -> P2 a2 -> P3 a3 -> Q1

subgoal 2 (ID 254) is:
 forall (T : Type) (a1 a2 a3 : T) (P1 P2 P3 : T -> Type),
 Prop -> forall Q2 : Prop, Prop -> P1 a1 -> P2 a2 -> P3 a3 -> Q2
subgoal 3 (ID 255) is:
 forall (T : Type) (a1 a2 a3 : T) (P1 P2 P3 : T -> Type),
 Prop -> Prop -> forall Q3 : Prop, P1 a1 -> P2 a2 -> P3 a3 -> Q3
于 2018-10-24T14:40:29.153 回答