Как применить переписывание в правой части условного выражения без разделения на него?

Question

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') 

Я имею в виду, что если бы я мог каким-то образом применить IHl на правой стороне только, то я мог бы применить HL решить дело, но я не знаю, как.

Если я использую раскол здесь, то я бы потерял способность решить эту проблему, так как мне пришлось бы доказать, что x = a в ветке In a l гипотезы и наоборот.

Answer 1

Несколько примечаний:

• Во-первых, ваше доказательство слишком долго. Подумайте немного больше, в частности, посмотрите, можете ли вы сделать слишком много индукций или расщепление в неправильном месте.

• Во-вторых, эти перезаписи немного сложно сделать, но некоторые из них возможны с помощью «Setoids» и iff. Вы можете быть заинтересованы в or_iff_compat_l леммы:

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

• В самом деле, некоторые библиотеки предпочитают использовать булевы версии /\ и \/ для улучшения перезаписи.

• И, наконец, ваша цель доказана немедленно, если вы уничтожили HL.