Разделение помещения с выводом соединения в Coq - PullRequest
Новая
       101

Разделение помещения с выводом соединения в Coq

0 голосов
/ 23 октября 2018

Мне часто приходится делать «индукционную нагрузку», чтобы доказать цели в 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) это также было бы полезно.

Ответы [ 2 ]

0 голосов
/ 25 октября 2018

Я не эксперт по 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' и H'', очищают состояние и рекурсивно вызывают себя.

В тривиальном примере это работает.

0 голосов
/ 24 октября 2018

Возможно, что-то вроде этого (минус распечатки отладки)? 

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