Splitting a premise with conjunction conclusion in Coq

1
votes

I often have to do "induction loading" to prove goals in Coq, where I prove multiple things simultaneously by induction.

The problem is, I often end up with Inductive Hypotheses of the following form:

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

This is fine, but tactics like eauto really don't know how to handle things like this, so it kills automation most of the time.

What I'm wondering is, is there a way to automatically break such a premise into m different premises, i.e.

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

The main problem I'm running into is that I don't know how to match with an arbitrary length chain of arrows in LTac. I could hard-code up to a certain length, but I'm hoping there's a better way.

Additionally, if it were possible to do the dual (i.e. split on all combinations of disjunctions in Premise1 .. Premise_k) that would also be useful.

2
functional-programmingcoqdependent-typecoq-tacticltac

2 Answers

4
votes

I am not an expert of Ltac, but I gave it a try and came up with the following tactic.

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 searches occurrences of conjunctions in H, then decomposes it into H' and H'', clean the state and calls itself recursively.

On a trivial example, this seems to work.

1
votes

Perhaps something like this (minus the debug printouts)?

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.

This leaves you with the goals

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