daniel2.v

Ltac save h1 h2 := 
  (*pose proof h1 as h2*)
  let t := type of h1 in 
    assert (h2 : t) by (exact h1).

Tactic Notation "save" constr(h1) "as" ident(h2) := 
  save h1 h2.


(* Ltac replace_equivalent a b p :=
  let at := type of a in
  let bt := type of b in
  match type of p with
  | at <-> bt => *)

Require Import List.
Import ListNotations.

Fixpoint map {X Y:Type} (f:X -> Y) (l:list X) : (list Y) :=
  match l with
  | [] => []
  | x :: l' => (f x) :: (map f l')
  end.

Fixpoint drop {A : Type} (n : nat) (l : list A) : list A :=
  match n with
  | 0 => l
  | S n' => drop n' (tail l)
  end.


Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | [] => False
  | x' :: l' => x = x' \/ In x l'
  end.

Inductive elementhood {A : Type} : A -> list A -> Prop :=
  | element_of : forall a l, In a l -> elementhood a l.

Notation "a '∈' l" := (elementhood a l) (at level 70).

Theorem in_equiv: 
  forall (A : Type) (x : A) (l : list A),
    In x l <-> x ∈ l.
Proof.
  intros A x l. 
  split.
  - apply element_of.
  - intros H1. destruct H1. assumption.
Qed.


Lemma test: 
  forall (A : Type) (a : A) (l : list A),
    In a l -> In a (a :: l).
Proof.
  intros A a.
  intros l.
  intros H.
  destruct l.
  - simpl. left. reflexivity.
  - simpl. left. reflexivity.
Qed.


Lemma if_In_then_drop_head:
  forall (A : Type) (l : list A) (x : A),
    In x l -> 
      exists n l', drop n l = x :: l'.
Proof.
  intros A l x.
  intros H1.
  induction l.
  - simpl in H1. contradiction.
  - simpl in H1.
    destruct H1 as [ H1_1 | H1_2 ].
    + rewrite <- H1_1.
      exists 0,l.
      reflexivity.
    + apply IHl in H1_2 as H2.
      save H2 as H3.
      destruct H3 as [m [l1 H4]].
      exists (S m).
      exists l1.
      simpl.
      assumption.
Qed.




Lemma In_map: 
  forall (A B : Type) (f : A -> B) l x,
    In x l -> In (f x) (map f l).
Proof.
  intros A B f l x.
  intros H1.
  generalize dependent l.
  induction l.
  (* all: try (unfold In; left; auto). *)
  - unfold In. simpl. contradiction.
  - intros H2. simpl.
    save H2 as H3. simpl in H3.
    destruct H3 as [ H4 | H5 ].
    + left. rewrite H4. reflexivity.
    + right. apply IHl in H5. assumption.
Qed.


Lemma in_app_iff: 
  forall (A : Type) (x : A) l1 l2,
    In x (l1 ++ l2) <-> In x l1 \/ In x l2.
Proof.
  intros A x l1 l2.
  split; intros H1.
  - induction l1.
    + simpl in H1. right. assumption.
    + simpl in H1.
      destruct H1 as [H2 | H3].
      * left. rewrite H2. simpl. left. reflexivity.
      * save IHl1 as H4.
        apply H4 in H3 as H5.
        destruct H5 as [H6 | H7].
        -- left. simpl. right. assumption.
        -- right. assumption.
  - induction l1; destruct H1 as [H2 | H3]; simpl.
    + simpl. contradiction.
    + assumption.
    + destruct H2.
      -- left. assumption.
      -- assert (H3 : In x l1 \/ In x l2).
          { left. assumption. }
        apply IHl1 in H3. right. assumption. 
    + right.
      assert (H4: In x l1 \/ In x l2).
        { right. assumption. }
     apply IHl1. right. assumption.
Qed.


Definition subseq {A : Type} (l1 l2 : list A) : Prop :=
  forall x, In x l1 -> In x l2.

Notation "l1 '⊆' l2" := (subseq l1 l2) (at level 70).

Lemma subseq_refl: 
  forall (A : Type) (l : list A),
    l ⊆ l.
Proof.
  intros A l.
  unfold subseq.
  intros x.
  intros H1.
  assumption.
Qed.

Lemma in_split: 
  forall (A : Type) (x : A) l,
    In x l -> 
      exists l1 l2, 
        l = l1 ++ x :: l2.
Proof.
  intros A x l.
  intros H1.
  induction l as [| x' l' IHl'].
  - unfold In in H1.
    contradiction.
  - unfold In in H1.
    destruct H1 as [H1_1 | H1_2].
    + exists [].
      exists l'.
      simpl.
      rewrite H1_1.
      reflexivity.
    + assert (H4 : In x l').
        { apply H1_2. }
      pose proof (IHl' H4) as H5.
      pose proof H5 as H6.
      destruct H5 as [l3 [l4 H5]].
      exists (x' :: l3).
      exists l4.
      simpl.
      rewrite H5.
      reflexivity.
Qed.