Eliminate redundant sub-goals generated by case analysis in Coq

Link:: https://stackoverflow.com/q/45264991

Display all goals and responses

Question

With a simple definition

Inductive B := bb.
Inductive C := cc.

Inductive A :=
| mkA1 : B -> A
| mkA2 : C -> A.

Definition id (a : A) : A :=
  match a with
  | mkA1 b => mkA1 b
  | mkA2 c => mkA2 c
  end.

I try to do proofs by case analysis (destruct), something like:

Theorem Foo :
  forall a1 a2 : A , a1 <> a2 -> id a1 <> id a2.forall a1 a2 : A, a1 <> a2 -> id a1 <> id a2
Proof.forall a1 a2 : A, a1 <> a2 -> id a1 <> id a2
  destruct a1; destruct a2.b, b0: B
mkA1 b <> mkA1 b0 -> id (mkA1 b) <> id (mkA1 b0)
b: B
c: C
mkA1 b <> mkA2 c -> id (mkA1 b) <> id (mkA2 c)
c: C
b: B
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
c, c0: C
mkA2 c <> mkA2 c0 -> id (mkA2 c) <> id (mkA2 c0)

Unsurprisingly, the current prove state contains two equivalent sub-goals:

4 subgoals

  b, b0 : B
  ============================
  mkA1 b <> mkA1 b0 -> id (mkA1 b) <> id (mkA1 b0)

subgoal 2 is:
 mkA1 b <> mkA2 c -> id (mkA1 b) <> id (mkA2 c)
subgoal 3 is:
 mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
subgoal 4 is:
 mkA2 c <> mkA2 c0 -> id (mkA2 c) <> id (mkA2 c0)

It seems to me that duplicated sub-goals are quite often when doing structural case analysis. Is there some common way to remove these duplicates?

What I did is to massage the second sub-goal to look like the third:

  2: intro; apply not_eq_sym in H; apply not_eq_sym; revert H.b, b0: B
mkA1 b <> mkA1 b0 -> id (mkA1 b) <> id (mkA1 b0)
b: B
c: C
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
c: C
b: B
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
c, c0: C
mkA2 c <> mkA2 c0 -> id (mkA2 c) <> id (mkA2 c0)

Although I still have no way to ask Coq to remove the duplicates. Now I can prove a lemma for my second sub-goal, and reuse it in my third sub-goal. But I would like to know some alternatives.

Answer

Here is some tactic automation that de-duplicates subgoals. Note that not only must the goals match exactly, but the ordering of the contexts must also match. You also need to run the initialization tactic before you do case analysis. This is code for Coq >= 8.5.

Inductive B := bb.
Inductive C := cc.

Inductive A :=
| mkA1 : B -> A
| mkA2 : C -> A.

Definition id (a : A) : A :=
  match a with
  | mkA1 b => mkA1 b
  | mkA2 c => mkA2 c
  end.

Record duplicate_prod (A B : Type) :=
  duplicate_conj { duplicate_fst : A ; duplicate_snd : B }.
Definition HERE := True.

Ltac start_remove_duplicates :=
  simple refine (let H___duplicates := @duplicate_conj _ _ I _ in _);
  [ shelve | | ]; cycle 1.

Ltac find_dup H G :=
  lazymatch type of H with
  | duplicate_prod G _ => constr:(@duplicate_fst _ _ H)
  | duplicate_prod _ _ => find_dup (@duplicate_snd _ _ H) G
  end.

Ltac find_end H :=
  lazymatch type of H with
  | duplicate_prod _ _ => find_end (@duplicate_snd _ _ H)
  | _ => H
  end.

Ltac revert_until H :=
  repeat lazymatch goal with
         | [ H' : _ |- _ ]
           => first [ constr_eq H H'; fail 1
                    | revert H' ]
         end.

Ltac remove_duplicates :=
  [ > lazymatch goal with
      | [ |- duplicate_prod _ _ ] => idtac
      | [ H : duplicate_prod _ _ |- _ ]
        => generalize (I : HERE);
           revert_until H;
           let G := match goal with |- ?G => G end in
           lazymatch type of H with
           | context[duplicate_prod G]
             => let lem := find_dup H G in exact lem
           | _ => let lem := find_end H in
                  refine (@duplicate_fst _ _ lem); clear H;
                  (* clear to work around a bug in Coq *)
                  shelve
           end
      end.. ].

Ltac finish_duplicates :=
  [ > lazymatch goal with
      | [ H : duplicate_prod _ _ |- _ ] => clear H
      end..
  | repeat match goal with
           | [ |- duplicate_prod _ ?e ]
             => split;
                [ repeat lazymatch goal with
                         | [ |- HERE -> _ ] => fail
                         | _ => intro
                         end;
                  intros _
                | try (is_evar e; exact I) ]
           end ].

Theorem Foo :
  forall  a1 a2 : A , a1 <> a2 -> id a1 <> id a2.forall a1 a2 : A, a1 <> a2 -> id a1 <> id a2
Proof.forall a1 a2 : A, a1 <> a2 -> id a1 <> id a2
  start_remove_duplicates.H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
forall a1 a2 : A, a1 <> a2 -> id a1 <> id a2
?B
  destruct a1; destruct a2.H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
b, b0: B
mkA1 b <> mkA1 b0 -> id (mkA1 b) <> id (mkA1 b0)
H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
b: B
c: C
mkA1 b <> mkA2 c -> id (mkA1 b) <> id (mkA2 c)
H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
c: C
b: B
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
c, c0: C
mkA2 c <> mkA2 c0 -> id (mkA2 c) <> id (mkA2 c0)
?B
  2: intro; apply not_eq_sym in H; apply not_eq_sym; revert c b H; intros c b.H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
b, b0: B
mkA1 b <> mkA1 b0 -> id (mkA1 b) <> id (mkA1 b0)
H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
c: C
b: B
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
c: C
b: B
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
H___duplicates:= {|
  duplicate_fst := I;
  duplicate_snd := ?duplicate_snd
|}: duplicate_prod True ?B
c, c0: C
mkA2 c <> mkA2 c0 -> id (mkA2 c) <> id (mkA2 c0)
?B
  all: remove_duplicates.duplicate_prod
  (forall b b0 : B,
   HERE ->
   mkA1 b <> mkA1 b0 -> id (mkA1 b) <> id (mkA1 b0))
  (duplicate_prod
     (forall (c : C) (b : B),
      HERE ->
      mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b))
     (duplicate_prod
        (forall c c0 : C,
         HERE ->
         mkA2 c <> mkA2 c0 ->
         id (mkA2 c) <> id (mkA2 c0)) 
        ?Goal))
  all: finish_duplicates.b, b0: B
mkA1 b <> mkA1 b0 -> id (mkA1 b) <> id (mkA1 b0)
c: C
b: B
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)
c, c0: C
mkA2 c <> mkA2 c0 -> id (mkA2 c) <> id (mkA2 c0)

The idea is that you first create an evar that will hold the solutions to unique goals. Then you do the case analysis. Then you go through the goals, and solve them either with a fresh projection from the evar, or, if you see that there's already a solution to the goal you're looking at, you use that solution. Finally, you split up the evar into multiple (deduplicated) goals. There's some additional boilerplate around reverting hypotheses that didn't exist when you created the evar (necessary to appease variable scoping for well-typed terms), remembering which things came from the context originally, and reintroducing those things back into the context at the end.