CODEWITHSUNDEEP
coq
Marko Grdinić
Marko Grdinić

Reputation: 4062

How to eliminate a disjunction inside of an expression?

Lemma In_map_iff :
  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
    In y (map f l) <->
    exists x, f x = y /\ In x l.
Proof.
split.
- generalize dependent y.
  generalize dependent f.
  induction l.
  + intros. inversion H.
  + intros.
    simpl.
    simpl in H.
    destruct H.
    * exists x.
      split.
      apply H.
      left. reflexivity.
    * 

1 subgoal
A : Type
B : Type
x : A
l : list A
IHl : forall (f : A -> B) (y : B),
      In y (map f l) -> exists x : A, f x = y /\ In x l
f : A -> B
y : B
H : In y (map f l)
______________________________________(1/1)
exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 l)

Since proving exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 l) is the same as proving exists x0 : A, f x0 = y /\ In x0 l, I want to eliminate x = x0 inside the goal here so I can apply the inductive hypothesis, but I am not sure how to do this. I've tried left in (x = x0 \/ In x0 l) and various other things, but I haven't been successful in making it happen. As it turns out, defining a helper function of type forall a b c, (a /\ c) -> a /\ (b \/ c) to do the rewriting does not work for terms under an existential either.

How could this be done?

Note that the above is one of the SF book exercises.

Upvotes: 0

Views: 118

Answers (2)

Jason Gross
Jason Gross

Reputation: 6128

You can get access to the components of your inductive hypothesis with any of the following:

  • specialize (IHl f y h); destruct IHl
  • destruct (IHl f y H)
  • edestruct IHl

You can then use exists and split to manipulate the goal into a form that is easier to work with.

Upvotes: 1

Marko Grdinić
Marko Grdinić

Reputation: 4062

As it turns out, it is necessary to define a helper.

Lemma In_map_iff_helper : forall (X : Type) (a b c : X -> Prop), 
  (exists q, (a q /\ c q)) -> (exists q, a q /\ (b q \/ c q)).
Proof.
intros.
destruct H.
exists x.
destruct H.
split.
apply H.
right.
apply H0.
Qed.

This does the rewriting that is needed right off the bat. I made a really dumb error thinking that I needed a tactic rather than an auxiliary lemma. I should have studied the preceding examples more closely - if I did, I'd have realized that existentials need to be accounted for.

Upvotes: 0

Related Questions