CODEWITHSUNDEEP
coq
Marko Grdinić
Marko Grdinić

Reputation: 4062

How to apply a rewrite to the right side of a conditional without splitting on it?

Lemma in_app_iff : forall A l l' (a:A),
  In a (l++l') <-> In a l \/ In a l'.
Proof.
  intros.
  split.
  - induction l.
    + simpl.
      induction l'.
      * simpl. intros. inversion H.
      * simpl.
        intros [HL | HR].
        right. left. apply HL.
        right. right. apply HR.
    + simpl.
      intros [HL | HR].
      * left. left. apply HL.
      * apply or_assoc.
        right.
        apply IHl.
        apply HR.
  - intros [HL | HR].
    + induction l.
      * inversion HL.
      * simpl in HL.
        simpl.

  A : Type
  x : A
  l, l' : list A
  a : A
  HL : x = a \/ In a l
  IHl : In a l -> In a (l ++ l')
  ============================
  x = a \/ In a (l ++ l')

I am thinking that if I could somehow apply IHl on the right side only, then I could apply HL to solve the case but I am not sure how.

If I use split here then I would lose the ability to solve this problem as I would have to prove that x = a in the In a l branch of the hypothesis and vice versa.

Upvotes: 0

Views: 572

Answers (1)

ejgallego
ejgallego

Reputation: 6852

A couple of notes:

  • First, your proof is too long. Think a bit more, in particular see if you are maybe doing too many inductions or splitting in the wrong place.

  • Secondly, these kind of rewrites are a bit hard to do, but some of them are possible with "Setoids" and iff. You may be interested in the or_iff_compat_l lemma:

    or_iff_compat_l : forall A B C : Prop, B <-> C -> A \/ B <-> A \/ C

  • Indeed, some libraries prefer to use the Boolean versions of /\ and \/ to improve rewriting.

  • And lastly, your goal is proved immediately if you destruct HL.

Upvotes: 2

Related Questions