Module UtilLemmas

Utility lemmas.

Require Import List TheoryList.
Require Import BinPos.
Require Import Arith.
Require Import SetoidList.

Require Import Errors.
Require Import Coqlib.
Require Import Registers.
Require Import Maps.
Require Import RTL.

Require Import UtilTacs.
Require Import UtilBase.

Local Open Scope nat_scope.

Lemma plus_one_S:
  forall n,
    n + 1 = S n.
Proof.
  intros. lia2.
Qed.

Lemma neq_none:
  forall {A : Type} (o : option A),
    o <> None -> exists a, o = Some a.
Proof.
  intros.
  case_eq o; intros; trim.
  exists a; auto.
Qed.

Lemma Pmem_f_In:
  forall f n,
    Pmem n f.(fn_code) = true <-> f_In n f.
Proof.
  intros.
  unfold Pmem.
  optDecGN GET; split; intros; trim.
Qed.

Lemma Pmem_iff_PIn:
  forall p t,
    Pmem p t = true <-> PIn p t.
Proof.
  unfold PIn; intuition.
Qed.

Lemma list_forall_dec:
  forall {A : Type} (P Q : A -> Prop),
    (forall a : A, {P a} + {Q a}) ->
    forall l : list A,
      {(forall a, In a l -> P a)} + {(exists a, In a l /\ Q a)}.
Proof.
  induction l; intros.
  left.
  intros; trim.
  destruct IHl.
  destruct (X a).
  left.
  intros.
  destruct H; trim.
  apply p; auto.
  right.
  exists a. split; auto. left; auto.
  right.
  destruct e as [n [IN NP]].
  exists n. split; auto.
  right; auto.
Qed.

Lemma list_forall_dec':
  forall {A : Type} (P Q : A -> Prop),
    (forall a : A, {P a} + {Q a}) ->
    forall l : list A,
      {(exists a, In a l /\ P a)} + {(forall a, In a l -> Q a)}.
Proof.
  induction l; intros.
  right.
  intros; trim.
  destruct IHl.
  destruct (X a).
  left.
  exists a; split; auto.
  left; auto.
  left.
  destruct e as [a' [IN A']].
  exists a'; split; auto.
  right; auto.
  destruct (X a).
  left.
  exists a; split; auto.
  left; auto.
  right.
  intros.
  destruct H; trim.
  subst; auto.
Qed.

Lemmas related to lists with decidable equality.
Section LIST_DEC.

  Variable T : Type.
  Hypothesis Tdec : forall (a b : T), {a = b} + {a <> b}.

Lemma mem_iff_In:
  forall (a : T) l,
    mem Tdec a l = true <-> In a l.
Proof.
  induction l; intros; split; intros; unfold mem in *; try cong; auto;
    case_eq (Tdec a a0); intro.
  subst. left. refl.
  right. apply IHl. rewrite H0 in H. asmp.
  subst. refl.
  destruct H; subst. cong.
  intro. apply IHl. asmp.
Qed.

Lemma mem_iff_In_conv {A : Type}:
  forall (a : T) l,
    mem Tdec a l = false <-> ~ In a l.
Proof.
  induction l; intros; split; intros; unfold mem in *.
  apply in_nil.
  refl.
  intro.
  destruct H0; subst.
  destruct (Tdec a a); intros; subst.
  inv H. cong.
  destruct (Tdec a a0); intros; subst.
  inv H.
  intuition.
  destruct (Tdec a a0); intros; subst.
  intuition.
  apply IHl.
  intro.
  apply H.
  right; auto.
Qed.

Section LIST_PREFIX.

  Fixpoint list_prefix (p l : list T) : Prop :=
    match p, l with
      | nil, _ => True
      | _ :: _, nil => False
      | n :: p', n' :: l' => n = n' /\ list_prefix p' l'
    end.

  Lemma list_prefix_nil:
    forall p,
      list_prefix p nil -> p = nil.
Proof.
    intros.
    destruct p; trim.
  Qed.

  Lemma list_prefix_refl:
    forall l,
      list_prefix l l.
Proof.
    induction l; trim;
      unfolds; auto.
  Qed.

  Lemma list_prefix_cons_ex:
    forall p l n,
      list_prefix p (n :: l) -> p = nil \/ exists p', p = n :: p' /\ list_prefix p' l.
Proof.
    intros.
    destruct p; auto.
    simpls.
    right.
    destruct H; subst.
    exists p; auto.
  Qed.

  Lemma list_prefix_cons:
    forall p l n,
      list_prefix p l -> list_prefix (n :: p) (n :: l).
Proof.
    intros; simpl; auto.
  Qed.

  Lemma no_list_prefix_cons_l:
    forall l n,
      ~ list_prefix (n :: l) l.
Proof.
    induction l; intros; trim.
    intro.
    inv H.
    apply IHl with (n := a).
    apply H1.
  Qed.

  Lemma list_prefix_app_r:
    forall p l,
       list_prefix p (p ++ l).
Proof.
    induction p; intros; simpls; trim.
    split; auto.
  Qed.

  Lemma list_prefix_app:
    forall p l l',
       list_prefix (p ++ l) (p ++ l') <-> list_prefix l l'.
Proof.
    induction p; intros; split; intros; simpls; trim.
    destruct H.
    apply IHp; auto.
    split; auto.
    apply IHp; auto.
  Qed.

  Lemma in_list_prefix:
    forall p l n,
      In n p ->
      list_prefix p l ->
      In n l.
Proof.
    induction p; trim; intros.
    destruct l; trim.
    inv H0. destruct H; subst.
    left; auto. right; auto.
  Qed.

  Lemma not_in_list_prefix:
    forall l p n,
      ~ In n l ->
      list_prefix p l ->
      ~ In n p.
Proof.
    induction l; intros; intro.
    apply list_prefix_nil in H0; trim.
    destruct (Tdec n a); subst.
    destruct p; trim.
    apply H. left; auto.
    destruct p; trim.
    inv H0.
    destruct H1; trim.
    eapply IHl in H3; eauto.
    intro. apply H.
    right; auto.
  Qed.

  Lemma no_list_prefix:
    forall p l n,
      In n p ->
      ~ In n l ->
      ~ list_prefix p l.
Proof.
    induction p; intros; trim.
    intro.
    destruct H.
    subst.
    destruct l; trim.
    inv H1.
    apply H0; left; auto.
    destruct l.
    apply list_prefix_nil in H1; trim.
    inv H1.
    eapply in_list_prefix in H3; eauto.
    apply H0; right; auto.
  Qed.

  Lemma list_prefix_length:
    forall p l,
      list_prefix p l ->
      length p <= length l.
Proof.
    induction p; intros; simpls.
    lia2.
    destruct l; trim.
    destruct H.
    apply IHp in H0.
    simpl; lia2.
  Qed.

  Lemma no_list_prefix_length:
    forall p l,
      length p > length l ->
      ~ list_prefix p l.
Proof.
    induction p; intros; simpls.
    lia2.
    destruct l; trim.
    intro.
    destruct H0.
    apply IHp in H1; trim.
    simpls; lia2.
  Qed.

End LIST_PREFIX.

Lemma not_in_count_occ:
  forall l n,
    ~ In n l -> count_occ Tdec l n = 0.
Proof.
  induction l; intros; trim.
  simpl.
  optDecG; trim; subst.
  exfalso. apply H. left; auto.
  apply IHl.
  intro.
  apply H. right; asmp.
Qed.

Lemma count_occ_app:
  forall l1 l2 n,
    count_occ Tdec (l1 ++ l2) n = count_occ Tdec l1 n + count_occ Tdec l2 n.
Proof.
  induction l1; intros; trim.
  simpls.
  optDecG; trim.
  subst a.
  rewrite IHl1.
  auto.
Qed.

Lemma count_occ_map_app:
  forall {A : Type} (f : A -> T) (l1 l2 : list A) n,
    count_occ Tdec (map f (l1 ++ l2)) n = count_occ Tdec (map f l1) n + count_occ Tdec (map f l2) n.
Proof.
  induction l1; intros; trim.
  simpls.
  optDecG; trim.
  rewrite map_app.
  rewrite count_occ_app.
  refl.
Qed.

Lemma count_map_app:
  forall {A : Type} (f : A -> positive) l l' n,
    count (map f (l ++ l')) n = count (map f l) n + count (map f l') n.
Proof.
  induction l; intros; simpls; trim.
  optDecG; trim.
  rewrite IHl; auto.
Qed.

Lemma count_app:
  forall l l' n,
    count (l ++ l') n = count l n + count l' n.
Proof.
  induction l; trim; intros.
  simpls.
  optDecG; subst; trim.
  rewrite IHl; auto.
Qed.

Lemma count_rev:
  forall l n,
    count (rev l) n = count l n.
Proof.
  induction l; intros; simpls; trim.
  optDecG; subst; trim;
  rewrite count_app; simpl;
  optDecG; trim;
  rewrite IHl; lia2.
Qed.

Lemma count_map_rev:
  forall {A : Type} (f : A -> positive) l n,
    count (map f (rev l)) n = count (map f l) n.
Proof.
  induction l; intros; simpls; trim.
  rewrite <- IHl.
  optDecG; subst; simpls.
  rewrite count_map_app.
  simpls.
  optDecG; simpls; lia2.
  rewrite count_map_app; simpl.
  optDecG; simpls; lia2.
Qed.


Lemma remove_not_In:
  forall (l : list T) a,
    ~ In a l -> remove Tdec a l = l.
Proof.
  induction l; intros; trim.
  simpls.
  optDecG; subst; trim.
  f_equal.
  apply IHl.
  intro.
  apply H; auto.
Qed.

Lemma remove_inv:
  forall (l : list T) a x,
    x <> a -> In x l -> In x (remove Tdec a l).
Proof.
  induction l; trim; intros.
  destruct H0; subst.
  simpl. optDecG; trim.
  left; refl.
  simpl. optDecG; trim.
  apply IHl; auto.
  eapply IHl in H0; eauto.
  right; asmp.
Qed.

Lemma remove_length:
  forall (l : list T) a,
    In a l -> length (remove Tdec a l) < length l.
Proof.
  induction l; trim; intros; simpls.
  destruct H; subst.
  optDecG; trim.
  destruct (In_dec Tdec a0 l).
  apply IHl in i. lia2.
  rewrite remove_not_In; auto.
  optDecG; subst; apply IHl in H; auto.
  simpl. lia2.
Qed.

Theorem pigeonhole_principle:
  forall (l1 l2: list T),
    (forall x, In x l1 -> In x l2) ->
    length l2 < length l1 ->
    ~ NoDup l1.
Proof.
  induction l1; intros; trim.
  intro.
  assert (In a l2).
  apply H; auto. left; refl.
  set (l2' := remove Tdec a l2).
  assert (length l2' < length l2).
  apply remove_length; auto.
  assert (~ In a l2').
  eapply remove_In.
  assert (forall x, x <> a -> In x l2 -> In x l2').
  apply remove_inv.
  inv H1.
  assert (forall x, In x l1 -> In x l2').
  intros.
  apply H5.
  intro; subst; trim.
  apply H. right; asmp.
  eapply IHl1; eauto.
  simpl in H0. lia2.
Qed.

Lemma pigeonhole_NoDup:
  forall (l1 l2: list T),
    (forall x, In x l1 -> In x l2) ->
    NoDup l1 ->
    length l1 <= length l2.
Proof.
  intros.
  destruct (le_dec (length l1) (length l2)); trim.
  exfalso. apply not_ge in n.
  apply pigeonhole_principle in n; auto.
Qed.

End LIST_DEC.

Section LIST.

Lemma zero_length:
  forall {A : Type} (l : list A),
    length l = 0 <-> l = nil.
Proof.
  intros; split; intro; destruct l; auto; inv H.
Qed.

Lemma app_cons_last {A : Type}:
  forall l (e : A) def_e, last (l ++ e :: nil) def_e = e.
Proof.
  induction l; intros; auto.
  simpl.
  rewrite IHl.
  case_eq (l ++ e :: nil); intros.
  generalize (app_cons_not_nil l nil e); intro. cong.
  refl.
Qed.

Lemma app_cons_nil_cons:
  forall {A : Type} (l1 l2 : list A) (a1 a2 : A),
    (l1 ++ a1 :: nil) ++ a2 :: l2 = l1 ++ a1 :: a2 :: l2.
Proof.
  induction l1; intros; trim.
  simpl.
  rewrite IHl1; auto.
Qed.

Lemma app_cons_false {A : Type}:
  forall x y (e: A), x ++ e :: y = nil -> False.
Proof.
    intros. gen (app_cons_not_nil x y e). cong.
  Qed.

Lemma last_not_nil_cons {A : Type}:
  forall (e : A) el def_e,
    el <> nil -> last el def_e = last (e :: el) def_e.
Proof.
  intros.
  simpl.
  destruct el.
  cong.
  auto.
Qed.

Lemma in_removelast:
  forall {A : Type} (l : list A) n,
    In n (removelast l) ->
      In n l.
Proof.
  induction l; intros; trim.
  simpls.
  destruct l; simpls; trim.
  destruct H; trim.
  apply IHl in H; trim.
Qed.

Lemma not_last_in_removelast:
  forall {A : Type} (l : list A) n,
    In n l ->
    forall n',
      n <> last l n' ->
      In n (removelast l).
Proof.
  induction l; intros; trim.
  simpls.
  destruct l; simpls; trim.
  destruct H; trim.
  destruct H; trim.
  apply IHl in H0; trim.
Qed.

Lemma last_map_comm_nnil:
  forall {A B : Type} (f : A -> B) (l : list A) (a : A) (def : B),
    l <> nil ->
    last (map f l) def = f (last l a).
Proof.
  induction l; intros; trim.
  destruct l; auto; simpls.
  erewrite IHl; eauto; trim.
Qed.

Lemma in_app_not {A : Type}:
  forall (l1 l2 : list A) n,
    ~ In n l1 ->
    In n (l1 ++ l2) ->
    In n l2.
Proof.
  induction l1; intros; trim.
  destruct H0.
  subst a.
  exfalso. apply H; left; auto.
  assert (In n (l1 ++ l2)) by auto.
  apply in_app in H1.
  destruct H1; trim.
  exfalso. apply H; right; auto.
Qed.

Lemma cons_in:
  forall {A : Type} l (e : A) l',
    l = e :: l' -> In e l.
Proof.
  induction l; intros.
  inv H.
  inv H. apply in_eq.
Qed.

Lemma cons_app:
  forall {A : Type} (l : list A) (a : A),
    a :: l = a :: nil ++ l.
Proof.
auto. Qed.

Lemma flat_map_eq_nil:
  forall (A B : Type) (f : A -> list B) (l : list A), flat_map f l = nil -> l = nil \/ forall e, In e l -> f e = nil.
Proof.
  induction l; intros.
  left. refl.
  simpl in *.
  right.
  intros.
  apply app_eq_nil in H.
  inv H.
  inv H0.
  asmp.
  apply IHl in H2.
  inv H2.
  inv H.
  apply H0. asmp.
Qed.

Fixpoint eq_length {A B : Type} (ll1 : list (list A)) (ll2 : list (list B)) :=
  match ll1 with
    | nil => ll2 = nil
    | l1 :: lr1 => match ll2 with
                     | nil => False
                     | l2 :: lr2 => length l1 = length l2 /\ eq_length lr1 lr2
                   end
  end.

Lemma eq_length_cons:
  forall A B ll1 ll2 l1 l2,
    (length l1 = length l2) /\ @eq_length A B ll1 ll2 <-> @eq_length A B (l1 :: ll1) (l2 :: ll2).
Proof.
  intros; split; intro.
  asmp.
  simpl in H. asmp.
Qed.

Lemma eq_length_same_length:
  forall A B ll1 ll2, @eq_length A B ll1 ll2 -> length ll1 = length ll2.
Proof.
  induction ll1; destruct ll2; intros; auto; simpl.
  inv H.
  inv H.
  rewrite IHll1 with (ll2 := ll2); auto.
  simpl in H. destruct H; asmp.
Qed.

Lemma flat_map_id_length:
  forall {A B : Type} (l1 : list (list A)) (l2 : list (list B)),
    eq_length l1 l2 ->
    length (flat_map (fun e => e) l1) = length (flat_map (fun e => e) l2).
Proof.
  induction l1; destruct l2; intros; simpl.
  refl.
  inv H.
  inv H.
  simpl in H; destruct H.
  repeat rewrite app_length; simpl.
  rewrite IHl1 with (l2 := l2); auto.
Qed.

Lemma eq_length_map:
  forall (A B C : Type) (f1 : A -> list B) (f2 : A -> list C) (l : list A),
    (forall e, In e l -> length (f1 e) = length (f2 e)) ->
    eq_length (map f1 l) (map f2 l).
Proof.
  induction l; intros; simpl.
  refl.
  split.
  apply H. left; refl.
  apply IHl.
  intros.
  apply H.
  right; asmp.
Qed.

Lemma in_combine_length:
  forall (A B : Type) (l : list A) (l' : list B) x,
    length l = length l' -> In x l ->
    exists y, In y l' /\ In (x, y) (combine l l').
Proof.
  induction l; destruct l'; intros.
  inv H0.
  inv H0.
  inv H.
  simpl in *.
  inv H.
  destruct H0.
  subst.
  exists b.
  split. left. refl.
  left. refl.

  apply IHl with (x := x) in H2.
  inv H2.
  exists x0.
  split.
  right.
  inv H0; asmp.
  right.
  inv H0; asmp.
  asmp.
Qed.

Lemma in_singleton:
  forall {A : Type} (e : A) l,
    l = e :: nil -> In e l /\ forall e', In e' l -> e' = e.
Proof.
  intros. subst.
  split.
  left. refl.
  intros.
  inv H. refl. inv H0.
Qed.

Lemma map_app_cons:
  forall {A B : Type} (f : A -> B) (l : list A) (l1 l2 : list B) e,
    map f l = l1 ++ e :: l2 ->
    exists l1', exists e', exists l2',
      l1 = map f l1' /\
      e = f e' /\
      l2 = map f l2' /\
      l = l1' ++ e' :: l2'.
Proof.
  induction l; intros.
  Case "nil".
    symmetry in H.
    simpl in H.
    apply app_eq_nil in H. intuition; nsolve.
  Case "a :: l".
    destruct l1.
    simpl in *.
    inv H.
    exists nil. exists a. exists l. intuition. simpl.
    simpl in H.
    inv H.
    apply IHl in H2.
    decs H2.
    exists (a :: x). exists x0. exists x1. intuition.
    simpl. rewrite H0. refl.
    simpl.
    rewrite H4. refl.
Qed.

Lemma last_not_nil:
  forall {A : Type} (l : list A) a d d',
    last (a :: l) d = last (a :: l) d'.
Proof.
  induction l; intros; trim.
  apply IHl.
Qed.

Lemma last_map_cons:
  forall {A B : Type} (f : A -> B) (l : list A) a a' d,
    last (map f (a :: a' :: l)) d = last (map f (a' :: l)) d.
Proof.
  induction l; intros; trim.
Qed.

Lemma last_map_not_nil:
  forall {A B : Type} (f : A -> B) (l : list A) a d d',
  last (map f (a :: l)) d = last (map f (a :: l)) d'.
Proof.
  induction l; intros; trim.
  repeat rewrite last_map_cons.
  apply IHl.
Qed.

Lemma map_ext_In:
  forall (A B : Type) (f g : A -> B) (l : list A),
  (forall a : A, In a l -> f a = g a) -> map f l = map g l.
Proof.
  induction l; intros; auto.
  simpl.
  f_equal.
  apply H. left; refl.
  apply IHl. intros. apply H. right; asmp.
Qed.

Lemma firstn_all:
  forall {A : Type} (l : list A),
    firstn (length l) l = l.
Proof.
  induction l; intros; simpl in *; trim.
Qed.

Lemma firstn_all2:
  forall {A : Type} (l : list A) n,
    n >= length l ->
    firstn n l = l.
Proof.
  induction l; intros; simpl in *; trim.
  destruct n; auto.
  destruct n; auto. lia2.
  simpl.
  rewrite IHl; auto. lia2.
Qed.

Lemma firstn_in_nil:
  forall {A : Type} (a : A) n,
    ~ In a (firstn n nil).
Proof.
  induction n; auto.
Qed.

Lemma firstn_in:
  forall {A : Type} (l : list A) n (a : A),
    In a (firstn n l) -> In a l.
Proof.
  induction l; simpl; intros; trim.
  apply firstn_in_nil in H; auto.
  destruct n; simpl in *; trim.
  destruct H. left; asmp.
  right. eapply IHl; eauto.
Qed.

Lemma rev_singleton:
  forall {A : Type} (a : A),
    rev (a :: nil) = a :: nil.
Proof.
  auto.
Qed.

Lemma rev_nil:
  forall {A : Type} (l : list A),
    rev l = nil -> l = nil.
Proof.
  induction l; intros; trim.
  simpls.
  exploit app_cons_not_nil; eauto.
  trim.
Qed.

Lemma app_singleton:
  forall {A : Type} (l : list A) (a : A),
    (a :: nil) ++ l = a :: l.
Proof.
  auto.
Qed.

Lemma last_map_comm:
  forall {A B : Type} (f : A -> B) (l : list A) (a : A),
    last (map f l) (f a) = f (last l a).
Proof.
  induction l; intros; auto.
  simpl.
  optDecGN MAP.
  apply map_eq_nil in MAP.
  rewrite MAP; auto.
  simpls.
  destruct l0; simpl.
  destruct l; trim.
  rewrite <- IHl; simpls.
  inv MAP; trim.
  rewrite H1; refl.
  destruct l0; destruct l; trim;
  rewrite <- IHl;
  rewrite MAP; trim.
Qed.

Lemma in_last:
  forall {A : Type} (l : list A) n d,
    last l d = n ->
    l = nil /\ n = d \/ In n l.
Proof.
  induction l; intros; auto.
  destruct l; simpls; auto.
  apply IHl in H.
  decs H; trim.
Qed.

Lemma last_in:
  forall {A : Type} (l : list A) def a,
    l <> nil ->
    a = last l def ->
    In a l.
Proof.
  induction l; trim; intros.
  subst a0.
  destruct l; simpls; auto.
  assert (a0 :: l <> nil) by trim.
  eapply IHl in H0; eauto.
Qed.

Lemma acnn:
  forall {A : Type} (x y : list A) (a : A), x ++ a :: y <> nil.
Proof.
  intros. intro. symmetry in H. apply app_cons_not_nil in H; auto.
Qed.

Lemma last_app_r:
  forall {A : Type} (l2 l1 : list A) def,
    l2 <> nil ->
    last (l1 ++ l2) def = last l2 def.
Proof.
  induction l2; intros; trim.
  destruct l2; simpls.
  apply app_cons_last.
  simpls.
  rewrite <- IHl2 with (l1 := l1 ++ a :: nil); eauto.
  rewrite <- app_assoc; auto.
  intro; trim.
Qed.

Lemma not_nil_in_last:
  forall {A : Type} (l : list A) (def : A),
    l <> nil -> In (last l def) l.
Proof.
  induction l; intros; trim.
  simpl.
  destruct l; trim.
  right.
  apply IHl; trim.
Qed.

Lemma last_map:
  forall {A B : Type} (f : A -> B) (l : list A) def def_f,
    l <> nil ->
    last (map f l) def = f (last l def_f).
Proof.
  induction l; intros; trim.
  destruct l; trim.
  assert (a0 :: l <> nil) by trim.
  simpls.
  eapply IHl in H0; eauto.
Qed.

Lemma map_nnil:
  forall {A B : Type} (f : A -> B) (l : list A),
    l <> nil -> map f l <> nil.
Proof.
  induction l; trim; intros.
  simpl.
  intro; trim.
Qed.

Lemma rev_sym:
  forall {A : Type} (l1 l2 : list A),
    l1 = rev l2 <-> rev l1 = l2.
Proof.
  intros; split; intros.
  rewrite H. rewrite rev_involutive; auto.
  rewrite <- H. rewrite rev_involutive; auto.
Qed.

Lemma in_list_in_dec:
  forall {A : Type} (Adec: forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) (P : A -> Prop) (Pdec: forall a, {P a} + {~ P a}) (l : list A),
    {forall a, In a l -> P a} + {exists a, In a l /\ ~ P a}.
Proof.
  induction l; intros; simpls.
  left. intros; trim.
  gen (Pdec a).
  destruct IHl; destruct H.
  left. intros.
  destruct H; trim.
  apply p; auto.
  right. exists a; trim.
  right. destruct e. exists x; trim.
  right. exists a; trim.
Qed.

Lemma in_list_in_dec_neg:
  forall {A : Type} (Adec: forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) (P : A -> Prop) (Pdec: forall a, {P a} + {~ P a}) (l : list A),
    {forall a, In a l -> ~ P a} + {exists a, In a l /\ P a}.
Proof.
  induction l; intros; simpls.
  left. intros; trim.
  gen (Pdec a).
  destruct IHl; destruct H.
  right. exists a; trim.
  left. intros.
  destruct H; trim.
  apply n; auto.
  right. destruct e. exists x; trim.
  right. decs e. exists x; trim.
Qed.

Lemma flat_map_app:
  forall {A B : Type} (f : A -> list B) (l1 l2 : list A),
    flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2.
Proof.
  induction l1; intros; trim; simpls.
  rewrite IHl1.
  rewrite app_assoc; auto.
Qed.

Lemma flatten_app:
  forall {A : Type} (ll : list (list A)) l1 l2,
    (flatten ll ++ l1 :: nil) ++ l2 = (flatten ll) ++ l1 :: l2.
Proof.
  induction ll; intros; trim; simpls.
  rewrite <- app_assoc; auto.
Qed.

Lemma flatten_app_2:
  forall {A : Type} (ll : list (list A)) l1 l2,
    (flatten ll ++ l1) ++ l2 = (flatten ll) ++ l1 ++ l2.
Proof.
  induction ll; intros; trim; simpls.
  rewrite <- app_assoc; auto.
Qed.

Lemma flatten_map_map:
  forall {A B : Type} (f : A -> B) ll,
    flatten (map (map f) ll) = map f (flatten ll).
Proof.
  induction ll; intros; simpls; trim.
  rewrite IHll.
  rewrite map_app; auto.
Qed.

Lemma rev_flatten:
  forall {A : Type} (ll : list (list A)),
    rev (flatten ll) = flatten (rev (map (fun l => rev l) ll)).
Proof.
  induction ll; trim.
  simpls.
  rewrite rev_app_distr.
  rewrite IHll.
  rewrite flat_map_app; simpl.
  rewrite app_nil_r; auto.
Qed.

Lemma flatten_unit:
  forall {A : Type} (l : list A),
    l = flatten (l :: nil).
Proof.
  intros; simpl; rewrite app_nil_r; auto.
Qed.

Lemma nnil_in_hd:
  forall {A : Type} (l : list A) def,
    l <> nil -> In (hd def l) l.
Proof.
  induction l; intros; trim.
  simpls; auto.
Qed.

Lemma hd_nnil_map:
  forall {A B : Type} (f : A -> B) (l : list A) defa defb,
    l <> nil ->
    hd defa (map f l) = f (hd defb l).
Proof.
  destruct l; trim.
Qed.

Lemma hd_nnil_app:
  forall {A : Type} (l1 l2 : list A) def,
    l1 <> nil ->
    hd def (l1 ++ l2) = hd def l1.
Proof.
  induction l1; intros; trim.
Qed.

Lemma hd_rev:
  forall {A : Type} (l : list A) def,
    hd def (rev l) = last l def.
Proof.
  induction l; intros; trim.
  destruct l; trim.
  simpls.
  rewrite <- IHl.
  rewrite hd_nnil_app; auto.
  apply acnn.
Qed.

Lemma in_tl:
  forall {A : Type} (l : list A) a def,
    In a l ->
    a <> hd def l ->
    In a (tl l).
Proof.
  induction l; intros; trim.
  simpls.
  destruct H; trim.
Qed.

Lemma map_hd:
  forall {A B : Type} (f : A -> B) (l : list A) def,
    f (hd def l) = hd (f def) (map f l).
Proof.
  induction l; trim.
Qed.

Lemma map_tl:
  forall {A B : Type} (f : A -> B) (l : list A),
    map f (tl l) = tl (map f l).
Proof.
  induction l; trim.
Qed.

Lemma not_in_removelast:
  forall {A : Type} (l : list A) a,
    ~ In a l -> ~ In a (removelast l).
Proof.
  induction l; intros; trim.
  intro.
  simpls.
  destruct l; simpls; trim.
  destruct H0; trim.
  eapply IHl; eauto.
Qed.

Lemma in_or_map_app:
  forall {A B : Type} (f : A -> B) (l1 l2 : list A) b,
    In b (map f l1) \/ In b (map f l2) -> In b (map f (l1 ++ l2)).
Proof.
  induction l1; intros; simpls.
  destruct H; trim.
  destruct H.
  destruct H; trim.
  right.
  apply in_map_iff in H. decs H.
  apply in_map_iff. eexists; split; eauto.
  apply in_app; auto.
  apply in_map_iff in H. decs H.
  right. apply in_map_iff. eexists; split; eauto.
  apply in_app; auto.
Qed.

Lemma in_map_rev:
  forall {A B : Type} (f : A -> B) (l : list A) a,
    In a (map f (rev l)) <-> In a (map f l).
Proof.
  intros; split; intros.
  apply in_map_iff in H. decs H.
  subst a.
  apply in_map. rewrite in_rev; auto.
  rewrite map_rev.
  rewrite <- in_rev; auto.
Qed.

Lemma last_map_unit:
  forall {A B : Type} (f : A -> B) (l : list A) a def,
    last (map f (l ++ a :: nil)) def = (f a).
Proof.
  induction l; intros; trim.
  rewrite <- app_comm_cons.
  simpl.
  rewrite IHl.
  optDecGN APP; trim.
  symmetry in APP. rewrite map_app in APP. simpls.
  apply app_cons_not_nil in APP; trim.
Qed.

Lemma app_cons_nil_app:
  forall {A : Type} (l1 l2 : list A) a,
    (l1 ++ a :: nil) ++ l2 = l1 ++ a :: l2.
Proof.
  induction l1; intros; trim.
  simpls.
  f_equal.
  rewrite IHl1; auto.
Qed.

Lemma removelast_unit:
  forall {A : Type} (l : list A) a,
    removelast (l ++ a :: nil) = l.
Proof.
  induction l; intros; trim.
  rewrite <- app_comm_cons.
  simpl.
  rewrite IHl.
  optDecGN APP; trim.
  symmetry in APP. apply app_cons_not_nil in APP; trim.
Qed.

Lemma removelast_map_unit:
  forall {A B : Type} (f : A -> B) (l : list A) a,
    removelast (map f (l ++ a :: nil)) = (map f l).
Proof.
  induction l; intros; trim.
  rewrite <- app_comm_cons.
  simpl.
  rewrite IHl.
  optDecGN APP; trim.
  symmetry in APP. rewrite map_app in APP. simpls.
  apply app_cons_not_nil in APP; trim.
Qed.

Lemma in_tl_in:
  forall {A : Type} (l : list A) a,
    In a (tl l) ->
    In a l.
Proof.
  induction l; intros; simpls; trim.
Qed.

Lemma rev_tl:
  forall {A : Type} (l : list A),
    rev (tl l) = removelast (rev l).
Proof.
  induction l; intros; trim.
  destruct l; trim.
  simpls.
  rewrite removelast_unit; auto.
Qed.

Lemma tl_app:
  forall {A : Type} (l1 l2 : list A),
    l1 <> nil ->
    tl l1 ++ l2 = tl (l1 ++ l2).
Proof.
  induction l1; intros; trim.
Qed.

Lemma tl_map:
  forall {A B : Type} (f : A -> B) (l : list A),
    tl (map f l) = map f (tl l).
Proof.
  induction l; trim.
Qed.

Lemma rev_removelast:
  forall {A : Type} (l : list A),
    rev (removelast l) = tl (rev l).
Proof.
  induction l; intros; trim.
  simpls.
  destruct l; trim.
  simpls.
  rewrite IHl.
  rewrite tl_app; trim.
  apply acnn.
Qed.

Lemma in_hd_tl:
  forall {A : Type} (l : list A) a def,
    In a l ->
    a = hd def l \/ In a (tl l).
Proof.
  induction l; intros; trim.
  destruct H; trim.
  subst a; auto.
Qed.

Lemma hd_app_disj:
  forall {A : Type} (l1 l2: list A) def v,
    hd def (l1 ++ l2) = v ->
    hd def l1 = v \/ l1 = nil /\ hd def l2 = v.
Proof.
  induction l1; intros; trim.
Qed.

Lemma hd_tl:
  forall {A : Type} (l: list A) def,
    l <> nil ->
    l = hd def l :: tl l.
Proof.
  induction l; trim.
Qed.

Lemma list_forall2_rev:
  forall {A B : Type} (f : A -> B -> Prop) (l1 : list A) (l2 : list B),
    list_forall2 f l1 l2 ->
    list_forall2 f (rev l1) (rev l2).
Proof.
  induction l1; intros; inv H.
  constructor.
  simpl.
  apply list_forall2_app; auto.
  constructor; auto.
  constructor.
Qed.

Lemma list_ex_unique:
  forall {A : Type} (l : list A) (e e' : A),
    In e l ->
    In e' l ->
    length l = 1%nat ->
    e = e'.
Proof.
  intros.
  destruct l; trim.
  destruct l; trim.
  inv H; trim.
  inv H0; trim.
Qed.

Lemma norepet_NoDup:
  forall {A : Type} (l : list A),
    list_norepet l <-> NoDup l.
Proof.
  induction l; intros; split; intro; try (solve [constructor]); try (inv H; constructor); auto.
  apply IHl; auto.
  apply IHl; auto.
Qed.

Lemma NoDup_dec:
  forall {A : Type} (Adec: forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) (l : list A),
    {NoDup l} + {~ NoDup l}.
Proof.
  intros.
  gen (list_norepet_dec Adec l).
  destruct H.
  left. apply norepet_NoDup; asmp.
  right. intro. apply n. apply norepet_NoDup; asmp.
Qed.

End LIST.

Section OPTION_BEQ.
  Variable A : Type.
  Variable Aeq : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}.

  Lemma option_beq_refl:
    forall o,
      option_beq A Aeq o o = true.
Proof.
    intros.
    destruct o; auto.
    unfold option_beq.
    case_eq (Aeq a a); intros.
    refl.
    cong.
  Qed.
  
  Lemma option_beq_eq:
    forall o1 o2,
      option_beq A Aeq o1 o2 = true -> o1 = o2.
Proof.
    intros.
    destruct o1; destruct o2; auto; unfold option_beq in H; try nsolve.
    destruct (Aeq a a0); nsolve.
  Qed.

  Lemma option_beq_neq:
    forall o1 o2,
      option_beq A Aeq o1 o2 = false -> o1 <> o2.
Proof.
    intros.
    destruct o1; destruct o2; auto; unfold option_beq in H; try nsolve.
    destruct (Aeq a a0); nsolve.
  Qed.

End OPTION_BEQ.

Section PAIR_BEQ.
  Variable A : Type.
  Variable Aeq : forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}.
  Variable B : Type.
  Variable Beq : forall (b1 b2 : B), {b1 = b2} + {b1 <> b2}.
  Notation pair_beq' := (pair_beq A Aeq B Beq).

  Lemma pair_beq_refl:
    forall o,
      pair_beq' o o = true.
Proof.
    intros.
    destruct o; auto.
    unfold pair_beq.
    case_eq (Aeq a a); intros.
    case_eq (Beq b b); intros.
    refl.
    cong.
    cong.
  Qed.
  
  Lemma pair_beq_eq:
    forall o1 o2,
      pair_beq' o1 o2 = true -> o1 = o2.
Proof.
    intros.
    destruct o1; destruct o2; auto; unfold pair_beq in H; try nsolve.
    destruct (Aeq a a0); destruct (Beq b b0); nsolve.
  Qed.

  Lemma pair_beq_neq:
    forall o1 o2,
      pair_beq' o1 o2 = false -> o1 <> o2.
Proof.
    intros.
    destruct o1; destruct o2; auto; unfold pair_beq in H; try nsolve.
    destruct (Aeq a a0); destruct (Beq b b0); nsolve.
  Qed.

End PAIR_BEQ.

Lemma option_N_node_beq_eq:
  forall o1 o2,
    option_N_node_beq o1 o2 = true ->
    o1 = o2.
Proof.
  intros.
  unfolds in H.
  apply option_beq_eq in H.
  asmp.
Qed.

Lemma option_N_N_node_beq_eq:
  forall o1 o2,
    option_N_N_node_beq o1 o2 = true ->
    o1 = o2.
Proof.
  intros.
  unfolds in H.
  apply option_beq_eq in H.
  asmp.
Qed.

Lemma option_mem_In_true:
  forall n ol,
    option_mem n ol = true -> ol = None \/ exists l, ol = Some l /\ In n l.
Proof.
  unfold option_mem.
  intros.
  destruct ol; intuition.
  rewrite mem_iff_In in H; eauto.
Qed.

Lemma option_mem_In_some:
  forall n l,
    option_mem n (Some l) = true -> In n l.
Proof.
  unfold option_mem.
  intros.
  rewrite mem_iff_In in H; auto.
Qed.

Section MISC.

Lemma Peqb_neq:
  forall p1 p2, p1 <> p2 <-> Peqb p1 p2 = false.
Proof.
  intros. case_eq (Peqb p1 p2); intros; split; intros; trim. rewrite Peqb_eq in H. contra.
  intro; subst. rewrite Peqb_refl in H. cong.
Qed.

Lemma Peqb_sym:
  forall p1 p2, Peqb p1 p2 = Peqb p2 p1.
Proof.
  intros.
  case_eq (Peqb p1 p2); case_eq (Peqb p2 p1); intros; trim.
  rewrite Peqb_eq in H0; subst. rewrite Peqb_refl in H. cong.
  rewrite Peqb_eq in H; subst. rewrite Peqb_refl in H0. cong.
Qed.

Lemma regset_In_dec:
  forall r s,
    {Regset.In r s} + {~ Regset.In r s}.
Proof.
  intros.
  destruct (In_dec positive_eq_dec r (Regset.elements s)).
  left.
  apply Regset.elements_2.
  apply SetoidList.In_InA; auto.
  right.
  intro.
  apply Regset.elements_1 in H.
  apply SetoidList.InA_alt in H; auto.
  decs H; trim.
Qed.

Lemma regset_in_singleton:
  forall r,
    Regset.In r (Regset.singleton r).
Proof.
  unfold Regset.singleton.
  intros.
  apply Regset.MSet.singleton_spec.
  refl.
Qed.

Lemma regset_in_singleton_eq:
  forall r1 r2,
    Regset.In r1 (Regset.singleton r2) -> r1 = r2.
Proof.
  unfold Regset.singleton.
  intros.
  apply Regset.MSet.singleton_spec.
  asmp.
Qed.

Lemma regset_in_singleton_neq:
  forall r1 r2,
    r1 <> r2 -> ~ Regset.In r1 (Regset.singleton r2).
Proof.
  intros.
  unfold Regset.singleton.
  intro.
  apply Regset.MSet.singleton_spec in H0.
  contra.
Qed.


Lemma pmap_get_disj:
  forall {A : Type} def (t : PTree.t A) n v,
    (def, t) # n = v ->
    t ! n = Some v \/ v = def.
Proof.
  intros.
  unfold PMap.get in H; simpls.
  optDec H; auto.
  left.
  subst; refl.
Qed.

Lemma ptree_gnd:
  forall {A : Type} def (t : PTree.t A) n v,
    t ! n = Some v ->
    v <> def ->
    (def, t) # n = v.
Proof.
  intros.
  unfold PMap.get.
  optDecGN GET; simpl in GET; rewrite H in GET; trim.
Qed.

Lemma pmap_gnd:
  forall {A : Type} def (t : PTree.t A) n v,
    (def, t) # n = v ->
    v <> def ->
    t ! n = Some v.
Proof.
  intros.
  unfold PMap.get in H.
  optDecN H GET; simpls; trim.
Qed.

Lemma list_norepet_map_fst:
  forall {A B : Type} (l : list (A * B)),
    list_norepet (map (@fst A B) l) -> list_norepet l.
Proof.
  induction l; intros; trim; constructor.
  intro.
  inv H.
  apply H3.
  apply in_map; asmp.
  apply IHl.
  inv H.
  asmp.
Qed.

Lemma ptree_elements_norepet:
  forall {A : Type} (m : PTree.t A),
    list_norepet (PTree.elements m).
Proof.
  intros.
  apply list_norepet_map_fst.
  apply PTree.elements_keys_norepet.
Qed.

Lemma pigeonhole_ptree:
  forall {A : Type} (Adec: forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) (l: list (positive * A)) (t : PTree.t A),
    (forall x, In x (PTree.elements t) -> In x l) ->
    (ptree_cardinal t <= length l)%nat.
Proof.
  intros.
  unfold ptree_cardinal.
  destruct (le_dec (length (PTree.elements t)) (length l)); trim.
  exfalso. apply not_ge in n.
  apply pigeonhole_principle in n; auto.
  apply n.
  apply norepet_NoDup.
  apply ptree_elements_norepet.
  repeat decide equality.
Qed.

Lemma pigeonhole_ptree_2:
  forall {A : Type} (Adec: forall (a1 a2 : A), {a1 = a2} + {a1 <> a2}) (l: list (positive * A)) (t : PTree.t A),
    NoDup l ->
    (forall x, In x l -> In x (PTree.elements t)) ->
    (length l <= ptree_cardinal t)%nat.
Proof.
  intros.
  unfold ptree_cardinal.
  destruct (le_dec (length l) (length (PTree.elements t))); trim.
  exfalso. apply not_ge in n.
  apply pigeonhole_principle in n; auto.
  repeat decide equality.
Qed.

Section SETOID.

  Require Import SetoidList.
  Variable T : Type.
  Hypothesis Tdec : forall (a b : T), {a = b} + {a <> b}.
  Variable teq : T -> T -> Prop.
  Hypothesis teq_dec: forall (t1 t2 : T), {teq t1 t2} + {~ teq t1 t2}.
  Hypothesis teq_refl: forall t, teq t t.
  Hypothesis teq_sym: forall t1 t2, teq t1 t2 -> teq t2 t1.
  Hypothesis teq_trans: forall t1 t2 t3, teq t1 t2 -> teq t2 t3 -> teq t1 t3.

  Hint Immediate teq_refl.
  Hint Immediate teq_sym.
  Hint Immediate teq_trans.

  Notation IN := (InA teq).
  Notation Remove := (removeA teq_dec).

  Lemma removeA_not_In:
    forall (l : list T) a,
      ~ IN a l -> Remove a l = l.
Proof.
    induction l; intros; trim.
    simpls.
    optDecG; subst.
    exfalso. apply H; auto.
    f_equal.
    apply IHl.
    intro.
    apply H; auto.
  Qed.

  Lemma removeA_length:
    forall (l : list T) a,
      IN a l -> length (Remove a l) < length l.
Proof.
    induction l; intros; simpls; trim.
    inv H.
    optDecG; trim.
    destruct (InA_dec teq_dec a0 l).
    subst.
    apply IHl in i. lia2.
    rewrite removeA_not_In; auto.
    optDecG; subst; apply IHl in H1; auto.
    simpl. lia2.
  Qed.

  Lemma removeA_inv:
    forall (l : list T) a x,
      ~ teq x a -> IN x l -> IN x (Remove a l).
Proof.
    induction l; trim; intros.
    destruct (teq_dec x a).
    simpl.
    optDecG. apply teq_sym in t0. apply teq_trans with (t1 := x) in t0; trim.
    left; auto.
    apply InA_cons in H0.
    destruct H0.
    simpl. optDecG; trim.
    simpl. optDecG.
    apply IHl; auto.
    eapply IHl in H0; eauto.
  Qed.

  Lemma teq_equiv : Equivalence teq.
Proof.
    apply Build_Equivalence; red; auto.
  Qed.
  Hint Immediate teq_equiv.

  Theorem pigeonhole_setoid:
    forall (l1 l2: list T),
      (forall x, IN x l1 -> IN x l2) ->
      length l2 < length l1 ->
      ~ NoDupA teq l1.
Proof.
    induction l1; intros; trim.
    intro.
    assert (IN a l2) by (apply H; auto).
    set (l2' := Remove a l2).
    assert (length l2' < length l2).
      subst l2'. apply removeA_length; auto.
    assert (~ IN a l2').
      intro.
      subst l2'.
      eapply removeA_InA with (1 := teq_equiv); auto.
      eapply H4.
    assert (forall x, ~ teq x a -> IN x l2 -> IN x l2').
      eapply removeA_inv.
    inv H1.
    assert (forall x, IN x l1 -> IN x l2').
      intros.
      subst l2'.
      apply H5.
      intro.
      apply InA_eqA with (y := a) in H1; auto.
    apply H. right; asmp.
    eapply IHl1; eauto.
    simpl in H0. lia2.
  Qed.

  Lemma pigeonhole_setoid_NoDup:
    forall (l1 l2: list T),
      (forall x, IN x l1 -> IN x l2) ->
      NoDupA teq l1 ->
      length l1 <= length l2.
Proof.
    intros.
    destruct (le_dec (length l1) (length l2)); trim.
    exfalso. apply not_ge in n.
    apply pigeonhole_setoid in n; auto.
  Qed.

End SETOID.

Definition option_count {A : Type} (o : option A) : nat :=
  match o with | None => 0 | Some _ => 1 end.

Fixpoint t_length {A : Type} (t : PTree.t A) : nat :=
  match t with
    | PTree.Leaf => 0
    | PTree.Node t1 o t2 => t_length t1 + option_count o + t_length t2
  end.

Lemma ptree_xelements_length:
  forall {A : Type} (t : PTree.t A) p p',
    length (PTree.xelements t p) = length (PTree.xelements t p').
Proof.
  induction t; simpl; intros; auto.
  destruct o; simpl.
  repeat rewrite app_length; simpl. erewrite IHt1; erewrite IHt2; eauto.
  repeat rewrite app_length; simpl. erewrite IHt1; erewrite IHt2; eauto.
Qed.

Lemma ptree_xelements_t_length:
  forall {A : Type} (t : PTree.t A) p,
    length (PTree.xelements t p) = t_length t.
Proof.
  induction t; simpl; intros; auto.
  destruct o; simpls;
  rewrite app_length; simpl;
  rewrite IHt1; rewrite IHt2; lia2.
Qed.

Lemma ptree_elements_t_length:
  forall {A : Type} (t : PTree.t A),
    length (PTree.elements t) = t_length t.
Proof.
  unfold PTree.elements; intros. apply ptree_xelements_t_length.
Qed.

Local Open Scope error_monad_scope.

Lemma fold_error:
  forall {A B : Type} (f : A -> B -> res B) (l : list A) m,
    fold_left (fun rb0 a =>
      do b0 <- rb0; f a b0) l (Error m) = Error m.
Proof.
  induction l; intros; trim.
  simpl.
  apply IHl.
Qed.

Lemma Npos_ex_Nsucc:
  forall p,
    exists n', Npos p = Nsucc n'.
Proof.
  induction p; intros.
  destruct IHp as [n' EQ].
  exists (Npred (Npos p~1)); auto.
  destruct IHp as [n' EQ].
  exists (Npred (Npos p~0)); auto.
  simpl.
  rewrite Psucc_o_double_minus_one_eq_xO.
  refl.
  exists 0%N; auto.
Qed.

Lemma nat_of_N_eq_0:
  forall n,
    Nnat.nat_of_N n = 0 -> n = N0.
Proof.
  intros.
  unfolds in H.
  destruct n; trim.
  gen (lt_O_nat_of_P p); lia2.
Qed.

End MISC.

Section DIFF.

  Lemma In_diff_1:
    forall l l' n,
      In n (diff l l') ->
      In n l /\ ~ In n l'.
Proof.
    intros.
    unfold diff in H.
    rewrite filter_In in H.
    rewrite negb_true_iff in H.
    rewrite mem_iff_In_conv in H.
    asmp.
    apply positive.
  Qed.

  Lemma In_diff_2:
    forall l l' n,
      In n l ->
      ~ In n l' ->
      In n (diff l l').
Proof.
    intros.
    unfold diff.
    rewrite filter_In.
    rewrite negb_true_iff.
    rewrite mem_iff_In_conv.
    auto.
    apply positive.
  Qed.

  Lemma not_In_diff_1:
    forall l l' n,
      ~ In n (diff l l') ->
      ~ In n l \/ In n l'.
Proof.
    unfold diff.
    intros.
    rewrite filter_In in H.
    destruct (In_dec positive_eq_dec n l).
    destruct (In_dec positive_eq_dec n l'); auto.
    exfalso.
    apply H. split; auto.
    rewrite negb_true_iff.
    rewrite mem_iff_In_conv.
    asmp.
    apply positive.
    auto.
  Qed.

  Lemma not_In_diff_2:
    forall l l' n,
      ~ In n (diff l l') ->
      ~ In n l' ->
      ~ In n l.
Proof.
    intros.
    apply not_In_diff_1 in H.
    destruct H; trim.
  Qed.

  Lemma filter_nil:
    forall {A : Type} (f : A -> bool) (l : list A),
      filter f l = nil <-> l = nil \/ forall x, In x l -> f x = false.
Proof.
    induction l; intros; auto.
    split; intros.
    right; trim.
    simpls; auto.
    split; intros.
    right; intros.
    destruct H0; subst.
    simpls. optDec H; trim.
    simpl in H.
    optDec H; trim.
    apply IHl in H.
    destruct H; subst; trim.
    apply H; auto.
    destruct H; trim.
    simpls.
    optDecGN F.
    assert (f a = false) by (apply H; auto).
    trim.
    apply IHl; auto.
  Qed.

  Lemma diff_neq:
    forall l l',
      (diff l l') <> nil ->
      l <> l'.
Proof.
    intros.
    intro. subst.
    apply H.
    unfold diff.
    apply filter_nil.
    right.
    intros.
    rewrite negb_false_iff.
    rewrite mem_iff_In.
    asmp.
  Qed.

End DIFF.

Require Import Utils.

Lemma fold_andb_true:
  forall (A: Type) (f: positive -> A -> bool) l,
    (forall i x, In (i, x) l -> f i x = true) ->
    fold_left (fun (a : bool) (p : node * A) => a && f (fst p) (snd p)) l true = true.
Proof.
  induction l; intros; trim.
  simpls.
  destruct a; simpls.
  assert (FP: f p a = true).
    apply H; auto.
  rewrite FP.
  rewrite IHl; auto.
Qed.

Lemma ptree_forall_true:
  forall (A: Type) (f: positive -> A -> bool) (m: PTree.t A),
    (forall i x, m!i = Some x -> f i x = true) ->
    forall_ptree f m = true.
Proof.
  intros.
  unfolds.
  rewrite PTree.fold_spec.
  rewrite fold_andb_true; auto.
  intros.
  apply PTree.elements_complete in H0; auto.
Qed.
Generated by coq2html