Require Import Coq.Structures.Equalities.

Require Import TVSMT.Coqlib.
Require Import TVSMT.Maps.
Require Import TVSMT.Errors.
Require Import TVSMT.Sat.
Require Import TVSMT.Common.
Require Import TVSMT.Hashtree.

Local Open Scope error_monad_scope.
Local Open Scope positive.

(** The [predicate] type defines the path predicates that are used in the [Ieta] and [Igamma]
    instructions. *)
Inductive pred {A}: Type :=
| Ptrue : pred
| Pfalse : pred
| Pundef : pred
| Pbase : A -> pred
| Pand : pred -> pred -> pred
| Por : pred -> pred -> pred
| Pimp : pred -> pred -> pred
| Pnot : pred -> pred.

Module PredicateNotation.

  Declare Scope predicate.

  Notation "A ∧ B" := (Pand A B) (at level 20, left associativity) : predicate.
  Notation "A ∨ B" := (Por A B) (at level 25, left associativity) : predicate.
  Notation "A → B" := (Pimp A B) (at level 30, right associativity) : predicate.
  Notation "¬ A" := (Pnot A) (at level 15) : predicate.
  Notation "⟂" := (Pfalse) : predicate.
  Notation "'T'" := (Ptrue) : predicate.
  Notation "○" := (Pundef) : predicate.

End PredicateNotation.

Import PredicateNotation.
Local Open Scope predicate.
Local Open Scope bool.
Local Open Scope positive.

Module ThreeValued(Base: UsualDecidableTypeBoth).

Definition A := Base.t.
Definition el_dec: forall a b: A, {a = b} + {a <> b} := Base.eq_dec.

Module Import AH := HashTree(Base).
Module Import AH_Prop := HashTreeProperties(Base).

Section EVAL.

Context (eval: A -> option bool).

Definition predicate := @pred A.

(* This evaluation follows Łukasiewicz logic. *)
Fixpoint eval_predicate (p: predicate) : option bool :=
  match p with
  | T => Some true
  | ⟂ => Some false
  | ○ => None
  | ¬ p =>
      match eval_predicate p with
      | None => None
      | Some b => Some (negb b)
      end
  | Pbase c =>
    match eval c with
    | Some p => Some p
    | None => None
    end
  | p1 ∧ p2 =>
    match eval_predicate p1, eval_predicate p2 with
    | Some p1', Some p2' => Some (p1' && p2')
    | Some false, None => Some false
    | None, Some false => Some false
    | _, _ => None
    end
  | p1 ∨ p2 =>
    match eval_predicate p1, eval_predicate p2 with
    | Some p1', Some p2' => Some (p1' || p2')
    | Some true, None => Some true
    | None, Some true => Some true
    | _, _ => None
    end
  | p1 → p2 =>
      match eval_predicate p1, eval_predicate p2 with
      | Some p1', Some p2' => Some (negb p1' || p2')
      | None, Some false => None
      | Some true, None => None
      | _, _ => Some true
      end
  end.

Definition equiv {A} (a b: @pred A) :=
  Pand (Pimp a b) (Pimp b a).

Definition hash_pred := @pred positive.

Definition hash_tree := PTree.t A.

Lemma comp_list_dec :
  forall (a b: list positive),
    {a = b} + {a <> b}.
Proof. generalize Pos.eq_dec. decide equality. Defined.

Lemma hash_pred_dec :
  forall (a b: hash_pred),
    {a = b} + {a <> b}.
Proof. generalize Pos.eq_dec. generalize bool_dec. repeat decide equality. Defined.

Lemma predicate_dec :
  forall (a b: predicate),
    {a = b} + {a <> b}.
Proof. generalize el_dec. generalize bool_dec. repeat decide equality. Defined.

Definition find_tree (el: A) (h: hash_tree) : option positive :=
  match
    filter (fun x => match x with (a, b) => if el_dec el b then true else false end)
           (PTree.elements h) with
  | (p, _) :: nil => Some p
  | _ => None
  end.

Definition combine_option {A} (a b: option A) : option A :=
  match a, b with
  | Some a', _ => Some a'
  | _, Some b' => Some b'
  | _, _ => None
  end.

Definition max_key {A} (t: PTree.t A) :=
  fold_right Pos.max 1 (map fst (PTree.elements t)).

Fixpoint hash_predicate (p: predicate) (h: PTree.t A)
  : hash_pred * PTree.t A :=
  match p with
  | T => (T, h)
  | ⟂ => (⟂, h)
  | ○ => (○, h)
  | ¬ p => let (p', t) := hash_predicate p h in (¬ p', t)
  | Pbase c =>
      match find_tree c h with
      | Some p => (Pbase p, h)
      | None =>
          let nkey := max_key h + 1 in
          (Pbase nkey, PTree.set nkey c h)
      end
  | p1 ∧ p2 =>
      let (p1', t1) := hash_predicate p1 h in
      let (p2', t2) := hash_predicate p2 t1 in
      (p1' ∧ p2', t2)
  | p1 ∨ p2 =>
      let (p1', t1) := hash_predicate p1 h in
      let (p2', t2) := hash_predicate p2 t1 in
      (p1' ∨ p2', t2)
  | p1 → p2 =>
      let (p1', t1) := hash_predicate p1 h in
      let (p2', t2) := hash_predicate p2 t1 in
      (p1' → p2', t2)
  end.

Fixpoint eval_hash_pred (p: hash_pred) (a: PTree.t bool) : option bool :=
  match p with
  | T => Some true
  | ⟂ => Some false
  | ○ => None
  | ¬ p =>
      match eval_hash_pred p a with
      | Some b => Some (negb b)
      | None => None
      end
  | Pbase k => a ! k
  | p1 ∧ p2 =>
    match eval_hash_pred p1 a, eval_hash_pred p2 a with
    | Some p1', Some p2' => Some (p1' && p2')
    | Some false, None => Some false
    | None, Some false => Some false
    | _, _ => None
    end
  | p1 ∨ p2 =>
    match eval_hash_pred p1 a, eval_hash_pred p2 a with
    | Some p1', Some p2' => Some (p1' || p2')
    | Some true, None => Some true
    | None, Some true => Some true
    | _, _ => None
    end
  | p1 → p2 =>
      match eval_hash_pred p1 a, eval_hash_pred p2 a with
      | Some p1', Some p2' => Some (negb p1' || p2')
      | None, Some false => None
      | Some true, None => None
      | _, _ => Some true
      end
  end.

(** The [predicate] type defines the path predicates that are used in the [Ieta] and [Igamma]
    instructions. *)
Inductive pred_bin {A}: Type :=
| PBtrue : pred_bin
| PBfalse : pred_bin
| PBbase : (bool * A) -> pred_bin
| PBand : pred_bin -> pred_bin -> pred_bin
| PBor : pred_bin -> pred_bin -> pred_bin.

Definition hash_pred_bin : Type := @pred_bin positive * @pred_bin positive.

Fixpoint eval_hash_pred_bin1 (p1: @pred_bin positive) (m: PMap.t bool) : bool :=
  match p1 with
  | PBtrue => true
  | PBfalse => false
  | PBbase (b, p) => if b then m!!p else negb m!!p
  | PBand p1 p2 => eval_hash_pred_bin1 p1 m && eval_hash_pred_bin1 p2 m
  | PBor p1 p2 => eval_hash_pred_bin1 p1 m || eval_hash_pred_bin1 p2 m
  end.

Definition eval_hash_pred_bin (p1: hash_pred_bin) (m: PMap.t bool) : (bool * bool) :=
  (eval_hash_pred_bin1 (fst p1) m, eval_hash_pred_bin1 (snd p1) m).

Fixpoint negate (h: @pred_bin positive) : @pred_bin positive :=
  match h with
  | PBtrue => PBfalse
  | PBfalse => PBtrue
  | PBbase (b, p) => PBbase (negb b, p)
  | PBand p1 p2 => PBor (negate p1) (negate p2)
  | PBor p1 p2 => PBand (negate p1) (negate p2)
  end.

Fixpoint conv_hash_pred (p: hash_pred) (h: PTree.t positive) (fresh: positive):
  (hash_pred_bin * PTree.t positive * positive) :=
  match p with
  | Ptrue => ((PBfalse, PBtrue), h, fresh)
  | Pfalse => ((PBfalse, PBfalse), h, fresh)
  | Pundef => ((PBtrue, PBfalse), h, fresh)
  | Pnot p => let '((p1, p2), h', fresh') := conv_hash_pred p h fresh in
              ((p1, negate p2), h', fresh')
  | Pand p1 p2 =>
      let '((p1s, p1'), h', fresh') := conv_hash_pred p1 h fresh in
      let '((p2s, p2'), h'', fresh'') := conv_hash_pred p2 h' fresh' in
      ((PBor (PBand p1' p2s) (PBor (PBand p1s p2s) (PBand p1s p2')),
         PBand p1' p2'), h'', fresh'')
  | Por p1 p2 =>
      let '((p1s, p1'), h', fresh') := conv_hash_pred p1 h fresh in
      let '((p2s, p2'), h'', fresh'') := conv_hash_pred p2 h' fresh' in
      ((PBor (PBand (negate p1') p2s) (PBor (PBand (negate p2') p1s) (PBand p1s p2s)),
         PBor p1' p2'), h'', fresh'')
  | Pimp p1 p2 =>
      let '((p1s, p1'), h', fresh') := conv_hash_pred p1 h fresh in
      let '((p2s, p2'), h'', fresh'') := conv_hash_pred p2 h' fresh' in
      ((PBor (PBand (negate p1s) (PBand p1' p2s)) (PBand (negate p2s) (PBand (negate p2') p1s)),
        PBor p1s (PBor (negate p1') p2')), h'', fresh'')
  | Pbase k =>
      ((PBbase (true, fresh), PBbase (true, k)), PTree.set k fresh h, fresh+1)
  end.

Fixpoint mult {A: Type} (a b: list (list A)) : list (list A) :=
  match a with
  | nil => nil
  | l :: ls => mult ls b ++ (List.map (fun x => l ++ x) b)
  end.

Definition simplify' {A} (p: @pred A) :=
  match p with
  | A ∧ T => A
  | T ∧ A => A
  | _ ∧ ⟂ => ⟂
  | ⟂ ∧ _ => ⟂
  | ○ ∧ ○ => ○
  | A ∨ ⟂ => A
  | ⟂ ∨ A => A
  | _ ∨ T => T
  | T ∨ _ => T
  | ○ ∨ ○ => ○
  | T → A => A
  | ⟂ → _ => T
  | _ → T => T
  | ○ → ○ => T
  | ¬ T => ⟂
  | ¬ ⟂ => T
  | ¬ ○ => ○
  | A => A
  end.

Fixpoint simplify {A} (dec: forall a b: @pred A, {a = b} + {a <> b} ) (p: @pred A) :=
  match p with
  | A ∧ B =>
    let A' := simplify dec A in
    let B' := simplify dec B in
    if dec A' B' then A' else simplify' (A' ∧ B')
  | A ∨ B =>
    let A' := simplify dec A in
    let B' := simplify dec B in
    if dec A' B' then A' else simplify' (A' ∨ B')
  | A → B =>
    let A' := simplify dec A in
    let B' := simplify dec B in
    if dec A' B' then A' else simplify' (A' → B')
  | ¬ p => simplify' (¬ (simplify dec p))
  | T => T
  | ⟂ => ⟂
  | ○ => ○
  | Pbase a => Pbase a
  end.

Fixpoint sat_hash_pred_bin1' (p: @pred_bin positive) (a: asgn) : bool :=
  match p with
  | PBtrue => true
  | PBfalse => false
  | PBbase (b, p') => if b then a (Pos.to_nat p') else negb (a (Pos.to_nat p'))
  | PBand p1 p2 => sat_hash_pred_bin1' p1 a && sat_hash_pred_bin1' p2 a
  | PBor p1 p2 => sat_hash_pred_bin1' p1 a || sat_hash_pred_bin1' p2 a
  end.

Fixpoint sat_hash_pred_bin1 (p: @pred_bin positive) (a: PMap.t bool) : bool :=
  match p with
  | PBtrue => true
  | PBfalse => false
  | PBbase (b, p') => if b then a !! p' else negb (a !! p')
  | PBand p1 p2 => sat_hash_pred_bin1 p1 a && sat_hash_pred_bin1 p2 a
  | PBor p1 p2 => sat_hash_pred_bin1 p1 a || sat_hash_pred_bin1 p2 a
  end.

Definition sat_hash_pred_bin (p: hash_pred_bin) (a: PMap.t bool) : bool :=
  negb (sat_hash_pred_bin1 (fst p) a) && sat_hash_pred_bin1 (snd p) a.

Definition conv_tree (p: PTree.t positive) (assigns: PTree.t bool) : PMap.t bool :=
  PTree.fold (fun m i a =>
                match assigns ! i with
                | Some true => PMap.set a false (PMap.set i true m)
                | Some false => PMap.set a false (PMap.set i false m)
                | None => PMap.set a true (PMap.set i false m)
                end) p (PMap.init false).

Definition interp_bin (b: bool * bool): option bool :=
  match b with | (true, _) => None | (_, b) => Some b end.

Fixpoint max_hash_pred (p: hash_pred) :=
  match p with
  | T | ⟂ | ○ => 1
  | Pbase k => k
  | p1 ∧ p2 | p1 ∨ p2 | p1 → p2 => Pos.max (max_hash_pred p1) (max_hash_pred p2)
  | ¬ p' => max_hash_pred p'
  end.

Definition eval_through_bin (p: hash_pred) (a: PTree.t bool) :=
  let '(p', h, f) := conv_hash_pred p (PTree.empty _) (max_hash_pred p + 1) in
  let m := conv_tree h a in
  interp_bin (sat_hash_pred_bin1 (fst p') m, sat_hash_pred_bin1 (snd p') m).

(*Compute eval_hash_pred (Pand (Por (Pbase 1) (Pbase 2)) (Pbase 3))
        (PTree.set 1 true (PTree.set 3 true (PTree.empty _))).
Compute eval_through_bin (Pand (Por (Pbase 1) (Pbase 2)) (Pbase 3))
        (PTree.set 1 true (PTree.set 3 true (PTree.empty _))).*)

Lemma satFormula_concat:
  forall a b agn,
  satFormula a agn ->
  satFormula b agn ->
  satFormula (a ++ b) agn.
Proof. induction a; crush. Qed.

Lemma satFormula_concat2:
  forall a b agn,
  satFormula (a ++ b) agn ->
  satFormula a agn /\ satFormula b agn.
Proof.
  induction a; simplify;
    try apply IHa in H1; crush.
Qed.

Lemma satClause_concat:
  forall a a1 a0,
  satClause a a1 ->
  satClause (a0 ++ a) a1.
Proof. induction a0; crush. Qed.

Lemma satClause_concat2:
  forall a a1 a0,
  satClause a0 a1 ->
  satClause (a0 ++ a) a1.
Proof.
  induction a0; crush.
  inv H; crush.
Qed.

Lemma satClause_concat3:
  forall a b c,
  satClause (a ++ b) c ->
  satClause a c \/ satClause b c.
Proof.
  induction a; crush.
  inv H; crush.
  apply IHa in H0; crush.
  inv H0; crush.
Qed.

Lemma satFormula_mult':
  forall p2 a a0,
  satFormula p2 a0 \/ satClause a a0 ->
  satFormula (map (fun x : list lit => a ++ x) p2) a0.
Proof.
  induction p2; crush.
  - inv H. inv H0. apply satClause_concat. auto.
    apply satClause_concat2; auto.
  - apply IHp2.
    inv H; crush; inv H0; crush.
Qed.

Lemma satFormula_mult2':
  forall p2 a a0,
  satFormula (map (fun x : list lit => a ++ x) p2) a0 ->
  satClause a a0 \/ satFormula p2 a0.
Proof.
  induction p2; crush.
  apply IHp2 in H1. inv H1; crush.
  apply satClause_concat3 in H0.
  inv H0; crush.
Qed.

Lemma satFormula_mult:
  forall p1 p2 a,
  satFormula p1 a \/ satFormula p2 a ->
  satFormula (mult p1 p2) a.
Proof.
  induction p1; crush.
  apply satFormula_concat; crush.
  inv H. inv H0.
  apply IHp1. auto.
  apply IHp1. auto.
  apply satFormula_mult';
  inv H; crush.
Qed.

Lemma satFormula_mult2:
  forall p1 p2 a,
  satFormula (mult p1 p2) a ->
  satFormula p1 a \/ satFormula p2 a.
Proof.
  induction p1; crush.
  apply satFormula_concat2 in H; crush.
  apply IHp1 in H0.
  inv H0; crush.
  apply satFormula_mult2' in H1. inv H1; crush.
Qed.

Fixpoint trans_pred (p: @pred_bin positive) :
  {fm: formula | forall a, sat_hash_pred_bin1' p a = true <-> satFormula fm a}.
  refine
    (match p with
     | PBtrue => exist _ nil _
     | PBfalse => exist _ (nil :: nil) _
     | PBbase (b, p') => exist _ (((b, Pos.to_nat p') :: nil) :: nil) _
     | PBand p1 p2 =>
         match trans_pred p1, trans_pred p2 with
         | exist p1' _, exist p2' _ => exist _ (p1' ++ p2') _
         end
     | PBor p1 p2 =>
         match trans_pred p1, trans_pred p2 with
         | exist p1' _, exist p2' _ => exist _ (mult p1' p2') _
         end
     end); split; crush.
  - destruct_match; subst. tauto. simplify. tauto.
  - inv H0; crush. destruct_match; crush. subst. apply negb_true_iff. crush.
  - apply satFormula_concat. apply i; auto. apply i0; auto.
  - apply satFormula_concat2 in H. simplify. apply andb_true_intro.
    split. apply i in H0. auto.
    apply i0 in H1. auto.
  - apply orb_prop in H. inv H; apply satFormula_mult. apply i in H0. auto.
    apply i0 in H0. auto.
  - apply orb_true_intro.
    apply satFormula_mult2 in H. inv H. apply i in H0. auto.
    apply i0 in H0. auto.
Qed.

Definition sat_pred (bound: nat) (p: @pred_bin positive) :
  option ({al : alist | sat_hash_pred_bin1' p (interp_alist al) = true}
          + {forall a : asgn, sat_hash_pred_bin1' p a = false}).
  refine
    ( match trans_pred p with
      | exist fm _ =>
          match boundedSat bound fm with
          | Some (inleft (exist a _)) => Some (inleft (exist _ a _))
          | Some (inright _) => Some (inright _)
          | None => None
          end
      end ).
  - apply i in s1. auto.
  - intros. specialize (n a). specialize (i a).
    destruct (sat_hash_pred_bin1' p a). exfalso.
    apply n. apply i. auto. auto.
Qed.

Lemma negate_correct :
  forall h a, sat_hash_pred_bin1' (negate h) a = negb (sat_hash_pred_bin1' h a).
Proof.
  induction h; crush.
  - repeat destruct_match; subst; crush; symmetry; apply negb_involutive.
  - rewrite negb_andb; crush.
  - rewrite negb_orb; crush.
Qed.

Lemma sat_implication :
  forall h h' a,
    sat_hash_pred_bin1' (PBand (negate h) h') a = false ->
    sat_hash_pred_bin1' h' a = true ->
    sat_hash_pred_bin1' h a = true.
Proof.
  intros. simplify. rewrite negate_correct in H.
  rewrite H0 in H. rewrite andb_true_r in H. crush.
Qed.

Fixpoint trans_pred_simple (p: @pred_bin positive) :=
  match p with
  | PBtrue => nil
  | PBfalse => nil :: nil
  | PBbase (b, p') => ((b, Pos.to_nat p') :: nil) :: nil
  | PBand p1 p2 =>
      match trans_pred_simple p1, trans_pred_simple p2 with
      | p1', p2' => (p1' ++ p2')
      end
  | PBor p1 p2 =>
      match trans_pred_simple p1, trans_pred_simple p2 with
      | p1', p2' => (mult p1' p2')
      end
  end.

(*Compute trans_pred_simple (PBand (PBbase (false, 1)) (PBbase (true, 3))).*)

Definition sat_pred_simple (bound: nat) (p: @pred_bin positive) :=
  boundedSatSimple bound (trans_pred_simple p).

Definition sat_hash_pred_simple (bound: nat) (p: hash_pred_bin) :=
  match sat_pred_simple bound (PBor (fst p) (negate (snd p))) with
  | Some None => Some None
  | Some (Some a) => Some (Some a)
  | None => None
  end.

Definition sat_hpred_simple bound (p: hash_pred) :=
  let '(p', h, f) := conv_hash_pred p (PTree.empty _) (max_hash_pred p + 1) in
  sat_hash_pred_simple bound p'.

Lemma max_key_correct' :
  forall l hi, In hi l -> hi <= fold_right Pos.max 1 l.
Proof.
  induction l; crush.
  inv H. lia.
  destruct (Pos.max_dec a (fold_right Pos.max 1 l)); rewrite e.
  - apply Pos.max_l_iff in e.
    assert (forall a b c, a <= c -> c <= b -> a <= b) by lia.
    eapply H; eauto.
  - apply IHl; auto.
Qed.

Definition bar (p1: lit): lit := (negb (fst p1), (snd p1)).

Definition stseytin_or (cur p1 p2: lit) : formula :=
  (bar cur :: p1 :: p2 :: nil)
    :: (cur :: bar p1 :: nil)
    :: (cur :: bar p2 :: nil) :: nil.

Definition stseytin_and (cur p1 p2: lit) : formula :=
  (cur :: bar p1 :: bar p2 :: nil)
    :: (bar cur :: p1 :: nil)
    :: (bar cur :: p2 :: nil) :: nil.

Fixpoint xtseytin (next: nat) (p: @pred_bin positive) {struct p} : (nat * lit * formula) :=
  match p with
  | PBbase (b, p') => (next, (b, Pos.to_nat p'), nil)
  | PBtrue =>
      ((next+1)%nat, (true, next), ((true, next)::nil)::nil)
  | PBfalse =>
      ((next+1)%nat, (true, next), ((false, next)::nil)::nil)
  | PBor p1 p2 =>
      let '(m1, n1, f1) := xtseytin next p1 in
      let '(m2, n2, f2) := xtseytin m1 p2 in
      ((m2+1)%nat, (true, m2), stseytin_or (true, m2) n1 n2 ++ f1 ++ f2)
  | PBand p1 p2 =>
      let '(m1, n1, f1) := xtseytin next p1 in
      let '(m2, n2, f2) := xtseytin m1 p2 in
      ((m2+1)%nat, (true, m2), stseytin_and (true, m2) n1 n2 ++ f1 ++ f2)
  end.

Lemma stseytin_and_correct :
  forall cur p1 p2 fm c,
    stseytin_and cur p1 p2 = fm ->
    satLit cur c ->
    satLit p1 c /\ satLit p2 c ->
    satFormula fm c.
Proof.
  intros.
  unfold stseytin_and in *. rewrite <- H.
  unfold satLit in *. destruct p1. destruct p2. destruct cur.
  simpl in *|-. cbn. unfold satLit. cbn. crush.
Qed.

Lemma stseytin_or_correct :
  forall cur p1 p2 fm c,
    stseytin_or cur p1 p2 = fm ->
    satLit cur c ->
    satLit p1 c \/ satLit p2 c ->
    satFormula fm c.
Proof.
  intros.
  unfold stseytin_or in *. rewrite <- H. inv H1.
  unfold satLit in *. destruct p1. destruct p2. destruct cur.
  simpl in *|-. cbn. unfold satLit. cbn. crush.
  unfold satLit in *. destruct p1. destruct p2. destruct cur.
  simpl in *|-. cbn. unfold satLit. cbn. crush.
Qed.

Fixpoint max_predicate (p: @pred_bin positive) : positive :=
  match p with
  | PBbase (b, p) => p
  | PBtrue => 1
  | PBfalse => 1
  | PBand a b => Pos.max (max_predicate a) (max_predicate b)
  | PBor a b => Pos.max (max_predicate a) (max_predicate b)
  end.

Definition tseytin_simple (p: @pred_bin positive) : formula :=
    let m := Pos.to_nat (max_predicate p + 1) in
    let '(m, n, fm) := xtseytin m p in
    (n::nil) :: fm.

Definition sat_pred_simple_tseytin (p: @pred_bin positive) : option (option alist) :=
  match boundedSatSimple 10000%nat (tseytin_simple p) with
  | Some (Some a) => Some (Some a)
  | Some None => Some None
  | None => None
  end.

Definition sat_hash_pred_simple_tseytin (p: hash_pred_bin) :=
  match sat_pred_simple_tseytin (PBor (fst p) (negate (snd p))) with
  | Some None => Some None
  | Some (Some a) => Some (Some a)
  | None => None
  end.

Definition sat_hpred_simple_tseytin (p: hash_pred) :=
  let '(p', h, f) := conv_hash_pred p (PTree.empty _) (max_hash_pred p + 1) in
  sat_hash_pred_simple_tseytin p'.

(*Compute sat_hpred_simple_tseytin ((Pbase 1 ∨ Pbase 2) → (Pbase 1 ∨ Pbase 2)).
Compute sat_hpred_simple 1000%nat (simplify ((Pbase 1 ∨ Pbase 2) → (Pbase 1 ∨ Pbase 2))).*)

Lemma max_key_correct :
  forall A h_tree hi (c: A),
    h_tree ! hi = Some c ->
    hi <= max_key h_tree.
Proof.
  unfold max_key. intros. apply PTree.elements_correct in H.
  apply max_key_correct'.
  eapply in_map with (f := fst) in H. auto.
Qed.

Lemma hash_constant :
  forall p h h_tree hi c h_tree',
    h_tree ! hi = Some c ->
    hash_predicate p h_tree = (h, h_tree') ->
    h_tree' ! hi = Some c.
Proof.
  induction p; crush.
  - repeat (destruct_match; crush); subst.
    pose proof H as X. apply max_key_correct in X.
    rewrite PTree.gso by lia; auto.
  - repeat (destruct_match; crush). exploit IHp1; eauto.
  - repeat (destruct_match; crush). exploit IHp1; eauto.
  - repeat (destruct_match; crush). exploit IHp1; eauto.
  - repeat (destruct_match; crush). exploit IHp; eauto.
Qed.

Lemma find_tree_correct :
  forall c h_tree p,
    find_tree c h_tree = Some p ->
    h_tree ! p = Some c.
Proof.
  intros.
  unfold find_tree in H. destruct_match; crush.
  destruct_match; simplify.
  destruct_match; crush.
  assert (In (p, a) (filter
           (fun x : positive * A =>
            let (_, b) := x in if el_dec c b then true else false) (PTree.elements h_tree))).
  { rewrite Heql. constructor. auto. }
  apply filter_In in H. simplify. destruct_match; crush. subst.
  apply PTree.elements_complete; auto.
Qed.

Lemma find_tree_unique :
  forall c h_tree p p',
    find_tree c h_tree = Some p ->
    h_tree ! p' = Some c ->
    p = p'.
Proof.
  intros.
  unfold find_tree in H.
  repeat (destruct_match; crush; []).
  assert (In (p, a) (filter
           (fun x : positive * A =>
            let (_, b) := x in if el_dec c b then true else false) (PTree.elements h_tree))).
  { rewrite Heql. constructor. auto. }
  apply filter_In in H. simplify.
  destruct (Pos.eq_dec p p'); auto.
  exfalso.
  destruct_match; subst; crush.
  assert (In (p', a) (PTree.elements h_tree) /\ (fun x : positive * A =>
            let (_, b) := x in if el_dec a b then true else false) (p', a) = true).
  { split. apply PTree.elements_correct. auto. rewrite Heqs. auto. }
  apply filter_In in H. rewrite Heql in H. inv H. simplify. crush. crush.
Qed.

Lemma hash_predicate_hash_le :
  forall p n p' n',
    hash_predicate p n = (p', n') ->
    (PTree_Properties.cardinal n <= PTree_Properties.cardinal n')%nat.
Proof.
  induction p; crush.
  - repeat (destruct_match; crush).
    assert (n ! (max_key n + 1) = None).
    { destruct (n ! (max_key n + 1)) eqn:?; auto.
      apply max_key_correct in Heqo0. lia. }
    exploit PTree_Properties.cardinal_set; eauto.
    instantiate (1 := a); intros. lia.
  - repeat (destruct_match; crush).
    apply IHp1 in Heqp. apply IHp2 in Heqp0. lia.
  - repeat (destruct_match; crush).
    apply IHp1 in Heqp. apply IHp2 in Heqp0. lia.
  - repeat (destruct_match; crush).
    apply IHp1 in Heqp. apply IHp2 in Heqp0. lia.
  - repeat (destruct_match; crush).
    apply IHp in Heqp0. lia.
Qed.

Lemma hash_predicate_hash_len :
  forall p n p' n',
    hash_predicate p n = (p', n') ->
    PTree_Properties.cardinal n = PTree_Properties.cardinal n' ->
    n = n'.
Proof.
  induction p; crush.
  - repeat (destruct_match; crush).
    assert (n ! (max_key n + 1) = None).
    { destruct (n ! (max_key n + 1)) eqn:?; auto.
      apply max_key_correct in Heqo0. lia. }
    exploit PTree_Properties.cardinal_set; eauto.
    instantiate (1 := a); intros. lia.
  - repeat (destruct_match; crush).
    pose proof Heqp as X; apply hash_predicate_hash_le in X.
    pose proof Heqp0 as X0; apply hash_predicate_hash_le in X0.
    exploit IHp1; eauto. lia. intros; subst.
    exploit IHp2; eauto.
  - repeat (destruct_match; crush).
    pose proof Heqp as X; apply hash_predicate_hash_le in X.
    pose proof Heqp0 as X0; apply hash_predicate_hash_le in X0.
    exploit IHp1; eauto. lia. intros; subst.
    exploit IHp2; eauto.
  - repeat (destruct_match; crush).
    pose proof Heqp as X; apply hash_predicate_hash_le in X.
    pose proof Heqp0 as X0; apply hash_predicate_hash_le in X0.
    exploit IHp1; eauto. lia. intros; subst.
    exploit IHp2; eauto.
  - repeat (destruct_match; crush).
    pose proof Heqp0 as X; apply hash_predicate_hash_le in X.
    exploit IHp; eauto.
Qed.

Inductive pred_In {A} : A -> @pred A -> Prop :=
| pred_In_Pbase : forall a, pred_In a (Pbase a)
| pred_In_Pand1 : forall c p1 p2, pred_In c p1 -> pred_In c (p1 ∧ p2)
| pred_In_Pand2 : forall c p1 p2, pred_In c p2 -> pred_In c (p1 ∧ p2)
| pred_In_Por1 : forall c p1 p2, pred_In c p1 -> pred_In c (p1 ∨ p2)
| pred_In_Por2 : forall c p1 p2, pred_In c p2 -> pred_In c (p1 ∨ p2)
| pred_In_Pimp1 : forall c p1 p2, pred_In c p1 -> pred_In c (p1 → p2)
| pred_In_Pimp2 : forall c p1 p2, pred_In c p2 -> pred_In c (p1 → p2)
| pred_In_Pnot : forall c p, pred_In c p -> pred_In c (¬ p).

Lemma pred_In_dec :
  forall A (c: A) p,
    (forall a b : A, { a = b } + { a <> b }) ->
    { pred_In c p } + { ~ pred_In c p }.
Proof.
  induction p; crush.
  - right. unfold not. intros. inv H.
  - right. unfold not. intros. inv H.
  - right. unfold not. intros. inv H.
  - destruct (X c a); subst.
    { left. constructor. }
    { right. unfold not. intros. inv H. auto. }
  - pose proof X as X1. pose proof X as X2.
    apply IHp1 in X1. apply IHp2 in X2.
    inv X1; inv X2. left. constructor. tauto.
    left. constructor. auto.
    left. apply pred_In_Pand2. auto.
    right. unfold not. intros. inv H1; auto.
  - pose proof X as X1. pose proof X as X2.
    apply IHp1 in X1. apply IHp2 in X2.
    inv X1; inv X2. left. constructor. tauto.
    left. constructor. auto.
    left. apply pred_In_Por2. auto.
    right. unfold not. intros. inv H1; auto.
  - pose proof X as X1. pose proof X as X2.
    apply IHp1 in X1. apply IHp2 in X2.
    inv X1; inv X2. left. constructor. tauto.
    left. constructor. auto.
    left. apply pred_In_Pimp2. auto.
    right. unfold not. intros. inv H1; auto.
  - pose proof X as X1. apply IHp in X1.
    inv X1. left. constructor. tauto.
    right. unfold not. intros. inv H0; auto.
Qed.

Lemma pred_In_hash :
  forall p n p' n' c,
    hash_predicate p n = (p', n') ->
    pred_In c p ->
    exists t, n' ! t = Some c /\ pred_In t p'.
Proof.
  induction p; simplify.
  - inv H0.
  - inv H0.
  - inv H0.
  - repeat (destruct_match; crush; []); subst.
    destruct_match; simplify.
    { inv H0. apply find_tree_correct in Heqo.
      econstructor; ecrush core. constructor. }
    { inv H0. econstructor. rewrite PTree.gss. crush. constructor. }
  - repeat (destruct_match; crush; []). inv H0.
    exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto.
    constructor; auto.
    exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pand2. auto.
  - repeat (destruct_match; crush; []). inv H0.
    exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto.
    constructor; auto.
    exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Por2. auto.
  - repeat (destruct_match; crush; []). inv H0.
    exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto.
    constructor; auto.
    exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pimp2. auto.
  - repeat (destruct_match; crush; []). inv H0. exploit IHp; eauto; simplify.
    econstructor; simplify; eauto. econstructor; auto.
Qed.

Lemma hash_pred_In' :
  forall p h t c n n',
    hash_predicate p n = (h, n') ->
    n ! t = None ->
    n' ! t = Some c ->
    pred_In c p.
Proof.
  induction p; crush.
  - repeat (destruct_match); subst; crush.
    destruct (Pos.eq_dec t (max_key n + 1)); subst.
    { rewrite PTree.gss in H1. simplify. constructor. }
    { rewrite PTree.gso in H1; crush. }
  - repeat (destruct_match); subst; crush.
    destruct (t0 ! t) eqn:?.
    { pose proof Heqo as X. eapply hash_constant in X; eauto. simplify.
      constructor. eapply IHp1; eauto. }
    { apply pred_In_Pand2; eapply IHp2; eauto. }
  - repeat (destruct_match); subst; crush.
    destruct (t0 ! t) eqn:?.
    { pose proof Heqo as X. eapply hash_constant in X; eauto. simplify.
      constructor. eapply IHp1; eauto. }
    { apply pred_In_Por2; eapply IHp2; eauto. }
  - repeat (destruct_match); subst; crush.
    destruct (t0 ! t) eqn:?.
    { pose proof Heqo as X. eapply hash_constant in X; eauto. simplify.
      constructor. eapply IHp1; eauto. }
    { apply pred_In_Pimp2; eapply IHp2; eauto. }
  - repeat (destruct_match); subst; crush.
    exploit IHp; eauto; intros. econstructor; auto.
Qed.

Lemma hash_pred_In :
  forall p h p' h' c n,
    hash_predicate p (PTree.empty _) = (h, n) ->
    hash_predicate p' n = (h', n) ->
    pred_In c p' -> pred_In c p.
Proof.
  intros. exploit pred_In_hash; eauto. simplify.
  eapply hash_pred_In'; eauto. apply PTree.gempty.
Qed.

Lemma pred_In_hash2 :
  forall p h n n' t,
    hash_predicate p n = (h, n') ->
    pred_In t h ->
    exists c, n' ! t = Some c /\ pred_In c p.
Proof.
  induction p; simplify.
  - inv H0.
  - inv H0.
  - inv H0.
  - repeat (destruct_match; crush; []); subst.
    destruct_match; simplify.
    { inv H0. apply find_tree_correct in Heqo.
      econstructor; ecrush core. constructor. }
    { inv H0. econstructor. rewrite PTree.gss. crush. constructor. }
  - repeat (destruct_match; crush; []). inv H0.
    exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto.
    constructor; auto.
    exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pand2. auto.
  - repeat (destruct_match; crush; []). inv H0.
    exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto.
    constructor; auto.
    exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Por2. auto.
  - repeat (destruct_match; crush; []). inv H0.
    exploit IHp1; eauto. simplify. econstructor. simplify. eapply hash_constant; eauto.
    constructor; auto.
    exploit IHp2; eauto. simplify. econstructor; ecrush core. apply pred_In_Pimp2. auto.
  - repeat (destruct_match; crush; []). inv H0.
    exploit IHp; eauto; simplify; repeat econstructor; ecrush core.
Qed.

Lemma hash_constant2 :
  forall p n h n' v c c',
    hash_predicate p n = (h, n') ->
    n ! v = Some c ->
    n' ! v = Some c' ->
    c = c'.
Proof.
  intros.
  eapply hash_constant in H; eauto. rewrite H1 in H. crush.
Qed.

Lemma pred_not_in_Pand :
  forall A (c: A) p1 p2,
    ~ pred_In c (p1 ∧ p2) ->
    ~ pred_In c p1 /\ ~ pred_In c p2.
Proof.
  intros. split.
  - unfold not in *. intros. apply H. constructor. auto.
  - unfold not in *. intros. apply H. apply pred_In_Pand2. auto.
Qed.

Lemma pred_not_in_Por :
  forall A (c: A) p1 p2,
    ~ pred_In c (p1 ∨ p2) ->
    ~ pred_In c p1 /\ ~ pred_In c p2.
Proof.
  intros. split.
  - unfold not in *. intros. apply H. constructor. auto.
  - unfold not in *. intros. apply H. apply pred_In_Por2. auto.
Qed.

Lemma simplify'_correct :
  forall h a,
    eval_hash_pred (simplify' h) a = eval_hash_pred h a.
Proof. destruct h; crush; repeat (destruct_match; crush). Qed.

Lemma eval_hash_pred_Pand_destr :
  forall p1 p2 p1' p2' a,
    eval_hash_pred p1 a = eval_hash_pred p1' a ->
    eval_hash_pred p2 a = eval_hash_pred p2' a ->
    eval_hash_pred (Pand p1 p2) a = eval_hash_pred (Pand p1' p2') a.
Proof. intros. simpl. rewrite H in *. rewrite H0 in *. auto. Qed.

Lemma eval_hash_pred_Pand_symm :
  forall p1 p2 a,
    eval_hash_pred (Pand p1 p2) a = eval_hash_pred (Pand p2 p1) a.
Proof. simplify. repeat destruct_match; auto. Qed.

Lemma eval_hash_pred_Por_symm :
  forall p1 p2 a,
    eval_hash_pred (Por p1 p2) a = eval_hash_pred (Por p2 p1) a.
Proof. simplify. repeat destruct_match; auto. Qed.

Lemma eval_hash_pred_Por_destr :
  forall p1 p2 p1' p2' a,
    eval_hash_pred p1 a = eval_hash_pred p1' a ->
    eval_hash_pred p2 a = eval_hash_pred p2' a ->
    eval_hash_pred (Por p1 p2) a = eval_hash_pred (Por p1' p2') a.
Proof. intros. simpl. rewrite H in *. rewrite H0 in *. auto. Qed.

Lemma eval_hash_pred_Pand_refl :
  forall p1 a,
    eval_hash_pred (Pand p1 p1) a = eval_hash_pred p1 a.
Proof. intros. simpl. repeat destruct_match; auto. Qed.

Lemma eval_hash_pred_Por_refl :
  forall p1 a,
    eval_hash_pred (Por p1 p1) a = eval_hash_pred p1 a.
Proof. intros. simpl. repeat destruct_match; auto. Qed.

  Lemma pand_false :
  forall a b l,
    eval_hash_pred (Pand a b) l <> Some true ->
    eval_hash_pred b l = Some true ->
    eval_hash_pred a l <> Some true.
Proof. simplify. repeat destruct_match; crush. Qed.

Lemma pand_true :
  forall a b l,
    eval_hash_pred (Pand a b) l = Some true ->
    eval_hash_pred a l = Some true /\ eval_hash_pred b l = Some true.
Proof. simplify; repeat destruct_match; crush. Qed.

Lemma pand_true2 :
  forall a b l,
    eval_hash_pred b l = Some true ->
    eval_hash_pred a l = Some true ->
    eval_hash_pred (Pand a b) l = Some true.
Proof. simplify; repeat destruct_match; crush. Qed.

Lemma eval_hash_pred_fold_Pand :
  forall l x la,
    eval_hash_pred (fold_left Pand l x) la = Some true ->
    eval_hash_pred x la = Some true.
Proof.
  induction l as [| el l' IHl ]; [tauto|].
  intros * EVAL. cbn in *.
  eapply IHl in EVAL. eapply pand_true in EVAL; tauto.
Qed.

Lemma eval_hash_pred_fold_Pand2 :
  forall l x la y,
    eval_hash_pred (fold_left Pand l x) la = Some true ->
    eval_hash_pred y la = Some true ->
    eval_hash_pred (fold_left Pand l y) la = Some true.
Proof.
  induction l as [| el l' IHl ]; [tauto|].
  intros * EVAL EVALY. cbn in *.
  pose proof EVAL as EVAL2.
  apply eval_hash_pred_fold_Pand in EVAL.
  eapply IHl; eauto. apply pand_true2; apply pand_true in EVAL; tauto.
Qed.

Lemma eval_hash_pred_fold_Pand3 :
  forall l x la,
    eval_hash_pred (fold_left Pand l x) la = Some true ->
    eval_hash_pred (fold_left Pand l T) la = Some true.
Proof. eauto using eval_hash_pred_fold_Pand2. Qed.

Lemma eval_hash_pred_fold_Pand4 :
  forall l x la,
    eval_hash_pred (fold_left Pand l x) la = Some true ->
    eval_hash_pred (fold_left Pand l T) la = Some true /\ eval_hash_pred x la = Some true.
Proof.
  intros; split;
    eauto using eval_hash_pred_fold_Pand3, eval_hash_pred_fold_Pand.
Qed.

Lemma eval_equiv2 :
  forall a b la,
    eval_hash_pred a la = eval_hash_pred b la ->
    eval_hash_pred (equiv a b) la = Some true.
Proof.
  unfold equiv; intros. unfold eval_hash_pred in *. fold eval_hash_pred in *.
  repeat destruct_match; try discriminate; crush.
Qed.

Lemma eval_equiv :
  forall a b la,
    eval_hash_pred (equiv a b) la = Some true ->
    eval_hash_pred a la = eval_hash_pred b la.
Proof.
  unfold equiv; intros. unfold eval_hash_pred in *. fold eval_hash_pred in *.
  repeat destruct_match; try discriminate; crush.
Qed.

Lemma eval_hash_pred_T_Pand :
  forall a l,
    eval_hash_pred (Pand T a) l = eval_hash_pred a l.
Proof.
  intros; unfold eval_hash_pred; fold eval_hash_pred;
  destruct_match; auto.
Qed.

Lemma fold_and_forall :
  forall p a pt,
    eval_hash_pred (fold_left Pand p pt) a = Some true ->
    Forall (fun x => eval_hash_pred x a = Some true) p.
Proof.
  induction p; crush.
  constructor.
  - apply eval_hash_pred_fold_Pand in H. eapply pand_true; eauto.
  - eapply IHp. eauto.
Qed.

Lemma fold_and_forall2 :
  forall p a pt,
    eval_hash_pred pt a = Some true ->
    Forall (fun x => eval_hash_pred x a = Some true) p ->
    eval_hash_pred (fold_left Pand p pt) a = Some true.
Proof.
  induction p; crush. inv H0.
  eapply IHp; eauto.
  apply pand_true2; eauto.
Qed.

Lemma fold_and_forall3 :
  forall p a,
    Forall (fun x => eval_hash_pred x a = Some true) p <->
      eval_hash_pred (fold_left Pand p T) a = Some true.
Proof.
  intros; split; intros.
  eapply fold_and_forall2; eauto.
  eapply fold_and_forall; eauto.
Qed.

Lemma eval_hash_pred_gso2 :
  forall p x y b,
    ~ pred_In y p ->
    eval_hash_pred p (PTree.set y b x) = eval_hash_pred p x.
Proof.
  induction p; try solve [crush].
  - intros * MAX. cbn in *. rewrite PTree.gso; auto. unfold not; intros.
    apply MAX; subst; constructor.
  - intros. cbn in H. simplify. erewrite !IHp1.
    erewrite !IHp2. auto. unfold not in *; intros; apply H; now apply pred_In_Pand2.
    unfold not in *; intros; apply H; now constructor.
  - intros. cbn in H. simplify. erewrite !IHp1.
    erewrite !IHp2. auto. unfold not in *; intros; apply H; now apply pred_In_Por2.
    unfold not in *; intros; apply H; now constructor.
  - intros. cbn in H. simplify. erewrite !IHp1.
    erewrite !IHp2. auto. unfold not in *; intros; apply H; now apply pred_In_Pimp2.
    unfold not in *; intros; apply H; now constructor.
  - intros. cbn in H. simplify. erewrite !IHp. auto.
    unfold not in *; intros; apply H; now constructor.
Qed.

Lemma eval_hash_pred_gso :
  forall p x y b,
    (max_hash_pred p < y)%positive ->
    eval_hash_pred p (PTree.set y b x) = eval_hash_pred p x.
Proof.
  induction p; try solve [crush].
  - intros * MAX. cbn in *. now rewrite PTree.gso by lia.
  - intros. cbn in H. simplify. erewrite !IHp1 by lia.
    now erewrite !IHp2 by lia.
  - intros. cbn in H. simplify. erewrite !IHp1 by lia.
    now erewrite !IHp2 by lia.
  - intros. cbn in H. simplify. erewrite !IHp1 by lia.
    now erewrite !IHp2 by lia.
  - intros. cbn in H. simplify. now erewrite !IHp by lia.
Qed.

Lemma eval_hash_pred_get :
  forall p a,
    eval_hash_pred (Pbase p) a = a ! p.
Proof. crush. Qed.

Lemma eval_hash_pred_except :
  forall p a a0 a0',
    ~ pred_In a p ->
    (forall x : positive, x <> a -> a0 ! x = a0' ! x) ->
    eval_hash_pred p a0 = eval_hash_pred p a0'.
Proof.
  induction p; crush.
  - destruct (peq a0 a); subst.
    + exfalso. apply H. constructor.
    + now rewrite H0 by auto.
  - erewrite IHp1; eauto.
    erewrite IHp2; eauto.
    unfold not; intros; apply H. apply pred_In_Pand2; auto.
    unfold not; intros; apply H. constructor; auto.
  - erewrite IHp1; eauto.
    erewrite IHp2; eauto.
    unfold not; intros; apply H. apply pred_In_Por2; auto.
    unfold not; intros; apply H. constructor; auto.
  - erewrite IHp1; eauto.
    erewrite IHp2; eauto.
    unfold not; intros; apply H. apply pred_In_Pimp2; auto.
    unfold not; intros; apply H. constructor; auto.
  - erewrite IHp; eauto.
    unfold not; intros; apply H. constructor; auto.
Qed.

Lemma eval_hash_pred_pand :
  forall p p1 p2 p3 a a',
    eval_hash_pred p1 a = eval_hash_pred p a' ->
    eval_hash_pred p2 a = eval_hash_pred p3 a' ->
    eval_hash_pred (p1 ∧ p2) a = eval_hash_pred (p ∧ p3) a'.
Proof. simplify; rewrite !H; now rewrite !H0. Qed.

Lemma eval_hash_pred_por :
  forall p p1 p2 p3 a a',
    eval_hash_pred p1 a = eval_hash_pred p a' ->
    eval_hash_pred p2 a = eval_hash_pred p3 a' ->
    eval_hash_pred (p1 ∨ p2) a = eval_hash_pred (p ∨ p3) a'.
Proof. simplify; rewrite !H; now rewrite !H0. Qed.

Lemma eval_hash_pred_pimp :
  forall p p1 p2 p3 a a',
    eval_hash_pred p1 a = eval_hash_pred p a' ->
    eval_hash_pred p2 a = eval_hash_pred p3 a' ->
    eval_hash_pred (p1 → p2) a = eval_hash_pred (p → p3) a'.
Proof. simplify; rewrite !H; now rewrite !H0. Qed.

Lemma eval_hash_pred_pnot :
  forall p p' a a',
    eval_hash_pred p a = eval_hash_pred p' a' ->
    eval_hash_pred (¬ p) a = eval_hash_pred (¬ p') a'.
Proof. simplify; now rewrite !H. Qed.

Lemma fold_left_Pand_rev :
  forall l b,
    eval_hash_pred (fold_left Pand (rev l) T) b = Some true ->
    eval_hash_pred (fold_left Pand l T) b = Some true.
Proof.
  intros.
  apply fold_and_forall3.
  apply fold_and_forall3 in H.
  apply Forall_forall; intros.
  now eapply Forall_forall in H; [|rewrite <- in_rev; eassumption].
Qed.

Lemma fold_left_Pand_rev2 :
  forall l b,
    eval_hash_pred (fold_left Pand l T) b = Some true ->
    eval_hash_pred (fold_left Pand (rev l) T) b = Some true.
Proof.
  intros.
  apply fold_and_forall3.
  apply fold_and_forall3 in H.
  apply Forall_forall; intros.
  now eapply Forall_forall in H; [|rewrite in_rev; eassumption].
Qed.

Lemma eval_hash_pred_T_Pand2 :
  forall a b l,
    eval_hash_pred b l = Some true ->
    eval_hash_pred (Pand a b) l = eval_hash_pred a l.
Proof.
  intros; unfold eval_hash_pred; fold eval_hash_pred.
    repeat (destruct_match; crush).
Qed.

Lemma eval_hash_pred_T_Pand3:
  forall b a,
    eval_hash_pred (b ∧ T) a = eval_hash_pred b a.
Proof.
  unfold eval_hash_pred; crush.
  repeat (destruct_match; crush).
Qed.

End EVAL.

End ThreeValued.