Library PAInfTheoryDi

Require Import ZArith.
Require Import Omega.
Require Import Bool.

Module Type VARIABLE.
Parameter var : Type.
Parameter var_eq_dec : forall v1 v2 : var, {v1 = v2} + {v1 <> v2}.
End VARIABLE.

Module Type NUMBER.

  Parameter A : Type.
  Parameter Const0 : A.
  Parameter Const1 : A.
  Parameter num_eq_dec : forall n1 n2 : A, {n1 = n2} + {n1 <> n2}.
  Parameter num_neg : A -> A.
  Parameter num_plus : A -> A -> A.
  Parameter num_leq : A -> A -> bool.

  Axiom leq01 : num_leq Const0 Const1 = true.
  Axiom nleq10 : num_leq Const1 Const0 = false.

End NUMBER.

Module ZInfinity <: NUMBER.

  Inductive ZE : Type :=
  | ZE_Fin : Z -> ZE
  | ZE_Inf : ZE
  | ZE_NegInf : ZE.

  Definition ZE_eq_dec : forall ze1 ze2 : ZE, {ze1 = ze2} + {ze1 <> ze2}.
  Proof.
    destruct ze1; destruct ze2; auto; try (right; intro; discriminate).
    destruct (Z_eq_dec z z0). left; congruence.
    right; congruence.
  Defined.

  Definition ZEneg (ze : ZE) : ZE :=
    match ze with
        ZE_Fin z => ZE_Fin (- z)
      | ZE_Inf => ZE_NegInf
      | ZE_NegInf => ZE_Inf
    end.

  Definition A := option ZE.

  Definition Const0 := Some (ZE_Fin 0).
  Definition Const1 := Some (ZE_Fin 1).

  Definition num_eq_dec : forall n1 n2 : A, {n1 = n2} + {n1 <> n2}.
  Proof.
    intros. destruct n1, n2; auto.
    destruct (ZE_eq_dec z z0).
    left; f_equal; auto.
    right; congruence.
    right; congruence.
    right; congruence.
  Defined.

  Definition num_neg := option_map ZEneg.

  Definition num_plus (ze1 ze2 : option ZE) : option ZE :=
    match ze1, ze2 with
      | None, _
      | _, None
      | Some ZE_Inf, Some ZE_NegInf
      | Some ZE_NegInf, Some ZE_Inf => None
      | Some ZE_Inf, _
      | _, Some ZE_Inf => Some ZE_Inf
      | Some ZE_NegInf, _
      | _, Some ZE_NegInf => Some ZE_NegInf
      | Some (ZE_Fin z1), Some (ZE_Fin z2) => Some (ZE_Fin (z1 + z2))
    end.

  Definition num_leq (ze1 ze2 : option ZE) : bool :=
    match ze1, ze2 with
      | None, _
      | _, None => false
      | _, Some ZE_Inf => true
      | Some ZE_NegInf, _ => true
      | Some ZE_Inf, Some x => if ZE_eq_dec x ZE_Inf then true else false
      | Some x, Some ZE_NegInf => if ZE_eq_dec x ZE_NegInf then true else false
      | Some (ZE_Fin z1), Some (ZE_Fin z2) => if Z_le_dec z1 z2 then true else false
    end.

  Lemma leq01 : num_leq Const0 Const1 = true.
  Proof. simpl; auto. Qed.

  Lemma nleq10 : num_leq Const1 Const0 = false.
  Proof. simpl; auto. Qed.

  Lemma numplus_finite : forall v1 v2 z, num_plus v1 v2 = Some (ZE_Fin z)
                                       -> exists z1 z2, (v1 = Some (ZE_Fin z1)) /\
                                                        (v2 = Some (ZE_Fin z2)) /\
                                                        (z1 + z2 = z)%Z.
  Proof.
    intros until z.
    destruct v1, v2; intros; try discriminate H.
    destruct z0, z1; try discriminate H.
    exists z0, z1; simpl in *.
    split; auto.
    split; auto.
    injection H; auto.
    destruct z0; discriminate H.
  Qed.

  Lemma numneg_finite : forall v z, num_neg v = Some (ZE_Fin z)
                                  -> exists x, v = Some (ZE_Fin x) /\ (- x = z)%Z.
  Proof.
    intros until z.
    destruct v; intros; try discriminate H.
    destruct z0; try discriminate H.
    exists z0.
    split; auto.
    simpl in H.
    injection H.
    auto.
  Qed.

  Lemma numplus_inf : forall v1 v2, num_plus v1 v2 = Some ZE_Inf
                                    -> ((exists z, v1 = Some (ZE_Fin z)) /\ v2 = Some ZE_Inf) \/
                                       (v1 = Some ZE_Inf /\ (exists z, v2 = Some (ZE_Fin z))) \/
                                       (v1 = Some ZE_Inf /\ v2 = Some ZE_Inf).
  Proof.
    intros.
    destruct v1, v2.
    destruct z, z0; simpl in *; auto;
    try (discriminate H).
    left; split; auto; exists z; auto.
    right; left; split; auto; exists z; auto.
    simpl in H; destruct z; discriminate H.
    simpl in H; destruct z; discriminate H.
    simpl in H; discriminate H.
  Qed.

  Lemma numplus_neginf : forall v1 v2, num_plus v1 v2 = Some ZE_NegInf
                                       -> ((exists z, v1 = Some (ZE_Fin z)) /\ v2 = Some ZE_NegInf) \/
                                          (v1 = Some ZE_NegInf /\ (exists z, v2 = Some (ZE_Fin z))) \/
                                          (v1 = Some ZE_NegInf /\ v2 = Some ZE_NegInf).
  Proof.
    intros.
    destruct v1, v2.
    destruct z, z0; simpl in *; auto;
    try (discriminate H).
    left; split; auto; exists z; auto.
    right; left; split; auto; exists z; auto.
    simpl in H; destruct z; discriminate H.
    simpl in H; destruct z; discriminate H.
    simpl in H; discriminate H.
  Qed.

  Lemma numneg_inf : forall v, num_neg v = Some ZE_Inf
                                  -> v = Some (ZE_NegInf).
  Proof.
    destruct v; intros; try discriminate H.
    destruct z; try discriminate H.
    auto.
  Qed.

  Lemma numneg_neginf : forall v, num_neg v = Some ZE_NegInf
                                  -> v = Some (ZE_Inf).
  Proof.
    destruct v; intros; try discriminate H.
    destruct z; try discriminate H.
    auto.
  Qed.

  Lemma numplus_none : forall v1 v2, num_plus v1 v2 = None -> v1 = None \/ v2 = None \/
                                                              (v1 = Some ZE_Inf /\ v2 = Some ZE_NegInf) \/
                                                              (v1 = Some ZE_NegInf /\ v2 = Some ZE_Inf).
  Proof.
    intros.
    destruct v1, v2.
    right; right.
    destruct z, z0; try discriminate H.
    left; auto.
    right; auto.
    right; left; auto.
    left; auto.
    left; auto.
  Qed.

  Lemma numneg_none: forall v, num_neg v = None -> v = None.
  Proof.
    intros.
    destruct v.
    destruct z; simpl in H; discriminate H.
    auto.
  Qed.

  Lemma num_plus_assoc: forall a b c, num_plus (Some a) (num_plus (Some b) (Some c)) =
                                      num_plus (num_plus (Some a) (Some b)) (Some c).
  Proof.
    intros; destruct a, b, c; simpl; auto; do 2 f_equal; omega.
  Qed.

  Lemma num_plus_commutation: forall a b, num_plus (Some a) (Some b) = num_plus (Some b) (Some a).
  Proof.
    intros; destruct a, b; simpl; auto; do 2 f_equal; omega.
  Qed.

  Lemma num_plus_zero: forall a, num_plus (Some a) Const0 = Some a.
  Proof.
    destruct a; simpl; auto. f_equal. f_equal. omega.
  Qed.

  Lemma num_leq_plus: forall a b c, num_leq (Some a) (Some b) = true ->
                                    num_plus (Some a) (Some c) <> None ->
                                    num_plus (Some b) (Some c) <> None ->
                                    num_leq (num_plus (Some a) (Some c))
                                            (num_plus (Some b) (Some c)) = true.
  Proof.
    intros; destruct a, b, c; simpl in *; auto.
    destruct (Z_le_dec z z0), (Z_le_dec (z + z1) (z0 + z1)); auto.
    exfalso; omega.
  Qed.

End ZInfinity.

Module ZNumLattice <: NUMBER.
  Definition A := Z.
  Definition Const0 := 0%Z.
  Definition Const1 := 1%Z.
  Definition num_eq_dec := Z_eq_dec.
  Definition num_neg (x : A) := (0 - x)%Z.
  Definition num_plus (x y : A) := (x + y)%Z.
  Definition num_leq (x y : A) := if Z_le_dec x y then true else false.

  Lemma leq01 : num_leq Const0 Const1 = true.
  Proof.
    simpl; auto.
  Qed.

  Lemma nleq10 : num_leq Const1 Const0 = false.
  Proof.
    simpl; auto.
  Qed.

End ZNumLattice.

Module NatNumLattice <: NUMBER.
  Definition A := nat.
  Definition Const0 := 0%nat.
  Definition Const1 := 1%nat.
  Definition num_eq_dec := eq_nat_dec.
  Definition num_neg (x : A) := x%nat.
  Definition num_plus (x y : A) := (x + y)%nat.
  Definition num_leq (x y : A) := if le_dec x y then true else false.

  Lemma leq01 : num_leq Const0 Const1 = true.
  Proof.
    simpl; auto.
  Qed.

  Lemma nleq10 : num_leq Const1 Const0 = false.
  Proof.
    simpl; auto.
  Qed.

End NatNumLattice.

Module Type SEMANTICS_INPUT.
  Declare Module N : NUMBER.
  Import N.
  Parameter Q : Type.
  Parameter QT : Q -> Type.
  Parameter conv : forall q, (QT q) -> A.
End SEMANTICS_INPUT.

Module PureInfinity <: SEMANTICS_INPUT.
  Module N := ZInfinity.
  Import N.
  Inductive AQ : Type :=
    Q_Z | Q_ZE.
  Definition Q : Type := AQ.
  Definition QT (q : Q) : Type := match q with Q_Z => Z | Q_ZE => ZE end.
  Definition conv {q : Q} (x : QT q) : A :=
    match q return (QT q -> A) with
     | Q_Z => fun x : Z => Some (ZE_Fin x)
     | Q_ZE => fun x : ZE => Some x
    end x.
End PureInfinity.

Module PureInt <: SEMANTICS_INPUT.
  Module N := ZNumLattice.
  Definition Q := unit.
  Definition QT (q : Q) : Type := Z.
  Definition conv {q : Q} (x : QT q) := x.
End PureInt.

Module PureNat <: SEMANTICS_INPUT.
  Module N := NatNumLattice.
  Definition Q := unit.
  Definition QT (q : Q) : Type := nat.
  Definition conv {q : Q} (x : QT q) := x.
End PureNat.

Module IntToInfinity <: SEMANTICS_INPUT.
  Module N := ZInfinity.
  Import N.
  Definition Q := unit.
  Definition QT (q : Q) : Type := Z.
  Definition conv {q : Q} (x : QT q) := Some (ZE_Fin x).
End IntToInfinity.

Module ArithSemantics (I : SEMANTICS_INPUT) (V : VARIABLE).
Import I.
Import N.
Import V.

Section OriginalForm.

  Inductive ZExp : Type :=
  | ZExp_Var : var -> ZExp
  | ZExp_Const : A -> ZExp
  | ZExp_Add : ZExp -> ZExp -> ZExp
  | ZExp_Inv : ZExp -> ZExp
  | ZExp_Sub : ZExp -> ZExp -> ZExp
  | ZExp_Mult : Z -> ZExp -> ZExp.
  Inductive ZBF : Type :=
  | ZBF_Const : bool -> ZBF
  | ZBF_Lt : ZExp -> ZExp -> ZBF
  | ZBF_Lte : ZExp -> ZExp -> ZBF
  | ZBF_Gt : ZExp -> ZExp -> ZBF
  | ZBF_Gte : ZExp -> ZExp -> ZBF
  | ZBF_Eq : ZExp -> ZExp -> ZBF
  | ZBF_Eq_Max : ZExp -> ZExp -> ZExp -> ZBF
  | ZBF_Eq_Min : ZExp -> ZExp -> ZExp -> ZBF
  | ZBF_Neq : ZExp -> ZExp -> ZBF.
  Inductive ZF : Type :=
  | ZF_BF : ZBF -> ZF
  | ZF_And : ZF -> ZF -> ZF
  | ZF_Or : ZF -> ZF -> ZF
  | ZF_Imp : ZF -> ZF -> ZF
  | ZF_Not : ZF -> ZF
  | ZF_Forall : var -> Q -> ZF -> ZF
  | ZF_Exists : var -> Q -> ZF -> ZF.
End OriginalForm.

Section DirectSemantics.

  Fixpoint num_mult_nat (n : nat) (x : A) : A :=
    match n with
      | O => Const0
      | S n => num_plus x (num_mult_nat n x)
    end.

  Definition num_mult (z : Z) (exp : A) : A :=
    match z with
      | Z0 => Const0
      | Zpos x => num_mult_nat (nat_of_P x) exp
      | Zneg x => num_neg (num_mult_nat (nat_of_P x) exp)
    end.

  Fixpoint subst_exp (p : var * A) (exp : ZExp) : ZExp :=
    match exp with
        ZExp_Var v => if var_eq_dec (fst p) v then ZExp_Const (snd p) else exp
      | ZExp_Const _ => exp
      | ZExp_Add e1 e2 => ZExp_Add (subst_exp p e1) (subst_exp p e2)
      | ZExp_Inv e => ZExp_Inv (subst_exp p e)
      | ZExp_Sub e1 e2 => ZExp_Sub (subst_exp p e1) (subst_exp p e2)
      | ZExp_Mult n e => ZExp_Mult n (subst_exp p e)
    end.

  Fixpoint subst_bf (p : var * A) (bf : ZBF) : ZBF :=
    match bf with
        ZBF_Const _ => bf
      | ZBF_Lt e1 e2 => ZBF_Lt (subst_exp p e1) (subst_exp p e2)
      | ZBF_Lte e1 e2 => ZBF_Lte (subst_exp p e1) (subst_exp p e2)
      | ZBF_Gt e1 e2 => ZBF_Gt (subst_exp p e1) (subst_exp p e2)
      | ZBF_Gte e1 e2 => ZBF_Gte (subst_exp p e1) (subst_exp p e2)
      | ZBF_Eq e1 e2 => ZBF_Eq (subst_exp p e1) (subst_exp p e2)
      | ZBF_Eq_Max e1 e2 e3 => ZBF_Eq_Max (subst_exp p e1) (subst_exp p e2) (subst_exp p e3)
      | ZBF_Eq_Min e1 e2 e3 => ZBF_Eq_Min (subst_exp p e1) (subst_exp p e2) (subst_exp p e3)
      | ZBF_Neq e1 e2 => ZBF_Neq (subst_exp p e1) (subst_exp p e2)
    end.

  Fixpoint substitute (p : var * A) (form : ZF) : ZF :=
    match form with
        ZF_BF bf => ZF_BF (subst_bf p bf)
      | ZF_And f1 f2 => ZF_And (substitute p f1) (substitute p f2)
      | ZF_Or f1 f2 => ZF_Or (substitute p f1) (substitute p f2)
      | ZF_Imp f1 f2 => ZF_Imp (substitute p f1) (substitute p f2)
      | ZF_Not f => ZF_Not (substitute p f)
      | ZF_Forall v q f => if var_eq_dec (fst p) v then form else ZF_Forall v q (substitute p f)
      | ZF_Exists v q f => if var_eq_dec (fst p) v then form else ZF_Exists v q (substitute p f)
    end.

  Lemma same_var_subst_exp: forall exp v a1 a2, subst_exp (v, a1) (subst_exp (v, a2) exp) = subst_exp (v, a2) exp.
  Proof.
    induction exp; simpl; intros.
    destruct (var_eq_dec v0 v); simpl; auto.
    destruct (var_eq_dec v0 v); simpl; tauto.
    auto.
    rewrite IHexp1, IHexp2; auto.
    rewrite IHexp; auto.
    rewrite IHexp1, IHexp2; auto.
    rewrite IHexp; auto.
  Qed.

  Lemma same_var_subst_bf: forall bf v a1 a2, subst_bf (v, a1) (subst_bf (v, a2) bf) = subst_bf (v, a2) bf.
  Proof.
    destruct bf; simpl; intros; auto;
    try (rewrite same_var_subst_exp, same_var_subst_exp, same_var_subst_exp; auto);
    try (rewrite same_var_subst_exp, same_var_subst_exp; auto).
  Qed.

  Lemma same_var_subst: forall f v a1 a2, substitute (v, a1) (substitute (v, a2) f) = substitute (v, a2) f.
  Proof.
    induction f; intros;
    try (unfold substitute; rewrite same_var_subst_bf; auto);
    try (unfold substitute; fold substitute; rewrite IHf1, IHf2; auto);
    try (unfold substitute; fold substitute; rewrite IHf; auto);
    try (unfold substitute; fold substitute; unfold fst;
    destruct (var_eq_dec v0 v);
    unfold substitute; fold substitute; unfold fst;
    destruct (var_eq_dec v0 v); auto; try tauto;
    rewrite IHf; auto).
  Qed.

  Lemma diff_var_subst_exp: forall exp v1 v2 a1 a2, v1 <> v2 -> subst_exp (v1, a1) (subst_exp (v2, a2) exp) =
                                                                subst_exp (v2, a2) (subst_exp (v1, a1) exp).
  Proof.
    induction exp; simpl; intros.
    destruct (var_eq_dec v2 v), (var_eq_dec v1 v).
    rewrite <- e in e0; tauto.
    simpl; destruct (var_eq_dec v2 v); tauto.
    simpl; destruct (var_eq_dec v1 v); tauto.
    simpl. destruct (var_eq_dec v2 v), (var_eq_dec v1 v); tauto.
    auto.
    rewrite IHexp1, IHexp2; auto.
    rewrite IHexp; auto.
    rewrite IHexp1, IHexp2; auto.
    rewrite IHexp; auto.
  Qed.

  Lemma diff_var_subst_bf: forall bf v1 v2 a1 a2, v1 <> v2 -> subst_bf (v1, a1) (subst_bf (v2, a2) bf) =
                                                              subst_bf (v2, a2) (subst_bf (v1, a1) bf).
  Proof.
    destruct bf; simpl; intros; auto;
    (rewrite diff_var_subst_exp with (exp := z);
     try rewrite diff_var_subst_exp with (exp := z0);
     try rewrite diff_var_subst_exp with (exp := z1);
     auto).
  Qed.

  Lemma diff_var_subst: forall f v1 v2 a1 a2, v1 <> v2 -> substitute (v1, a1) (substitute (v2, a2) f) =
                                                          substitute (v2, a2) (substitute (v1, a1) f).
  Proof.
    induction f; intros;
    try (unfold substitute; rewrite diff_var_subst_bf; auto);
    try (unfold substitute; fold substitute; rewrite IHf1, IHf2; auto);
    try (unfold substitute; fold substitute; rewrite IHf; auto);
    (unfold substitute; fold substitute; unfold fst;
     destruct (var_eq_dec v2 v), (var_eq_dec v1 v); auto;
     try (rewrite <- e in e0; tauto);
     try (simpl; destruct (var_eq_dec v2 v), (var_eq_dec v1 v); try tauto);
     rewrite IHf; auto).
  Qed.

  Fixpoint dexp2ZE (exp : ZExp) : A :=
    match exp with
        ZExp_Var _ => Const0
      | ZExp_Const z => z
      | ZExp_Add e1 e2 => num_plus (dexp2ZE e1) (dexp2ZE e2)
      | ZExp_Inv e => num_neg (dexp2ZE e)
      | ZExp_Sub e1 e2 => num_plus (dexp2ZE e1) (num_neg (dexp2ZE e2))
      | ZExp_Mult z e => num_mult z (dexp2ZE e)
    end.

  Fixpoint dzbf2bool (bf : ZBF) : bool :=
    match bf with
        ZBF_Const b => b
      | ZBF_Lt e1 e2 => let v1 := dexp2ZE e1 in
                         let v2 := dexp2ZE e2 in
                         num_leq v1 v2 && (negb (num_leq v2 v1))
      | ZBF_Lte e1 e2 => num_leq (dexp2ZE e1) (dexp2ZE e2)
      | ZBF_Gt e1 e2 => let v1 := dexp2ZE e1 in
                         let v2 := dexp2ZE e2 in
                         num_leq v2 v1 && (negb (num_leq v1 v2))
      | ZBF_Gte e1 e2 => num_leq (dexp2ZE e2) (dexp2ZE e1)
      | ZBF_Eq e1 e2 => let v1 := dexp2ZE e1 in
                         let v2 := dexp2ZE e2 in
                         num_leq v1 v2 && num_leq v2 v1
      | ZBF_Eq_Max e1 e2 e3 =>
                         let v1 := dexp2ZE e1 in
                         let v2 := dexp2ZE e2 in
                         let v3 := dexp2ZE e3 in
                         ((num_leq v3 v2) && num_leq v1 v2 && num_leq v2 v1)
                         || ((num_leq v2 v3) && num_leq v1 v3 && num_leq v3 v1)
      | ZBF_Eq_Min e1 e2 e3 =>
                         let v1 := dexp2ZE e1 in
                         let v2 := dexp2ZE e2 in
                         let v3 := dexp2ZE e3 in
                         ((num_leq v3 v2) && num_leq v1 v3 && num_leq v3 v1)
                         || ((num_leq v2 v3) && num_leq v1 v2 && num_leq v2 v1)
      | ZBF_Neq e1 e2 => let v1 := dexp2ZE e1 in
                         let v2 := dexp2ZE e2 in
                         negb (num_leq v1 v2 && num_leq v2 v1)
    end.

  Fixpoint length_zform (form : ZF) : nat :=
    match form with
        ZF_BF _ => 1
      | ZF_And f1 f2 => S (length_zform f1 + length_zform f2)
      | ZF_Or f1 f2 => S (length_zform f1 + length_zform f2)
      | ZF_Imp f1 f2 => S (length_zform f1 + length_zform f2)
      | ZF_Not f => S (length_zform f)
      | ZF_Forall _ _ f => S (length_zform f)
      | ZF_Exists _ _ f => S (length_zform f)
    end.

  Fixpoint dvalid_zform' (form : ZF) (c : nat) : Prop :=
    match c with
        0 => False
      | S c' =>
        match form with
            ZF_BF bf => dzbf2bool bf = true
          | ZF_And f1 f2 => dvalid_zform' f1 c' /\ dvalid_zform' f2 c'
          | ZF_Or f1 f2 => dvalid_zform' f1 c' \/ dvalid_zform' f2 c'
          | ZF_Imp f1 f2 => (~ dvalid_zform' f1 c') \/ dvalid_zform' f2 c'
          | ZF_Not f => ~ (dvalid_zform' f c')
          | ZF_Forall v q f => forall x : QT q, dvalid_zform' (substitute (v , @conv q x) f) c'
          | ZF_Exists v q f => exists x : QT q, dvalid_zform' (substitute (v , @conv q x) f) c'
        end
    end.
  Definition dvalid_zform (form : ZF) : Prop := dvalid_zform' form (length_zform form).

  Lemma substitute_length_inv : forall f x v, length_zform f = length_zform (substitute (v, x) f).
  Proof.
    induction f; simpl; try tauto; intros;
    try (rewrite <- IHf1; rewrite <- IHf2);
    try rewrite <- IHf;
    try (case (var_eq_dec v0 v); intros; simpl); auto.
  Qed.

  Lemma large_c_holds : forall f c1 c2, c1 >= length_zform f -> c2 >= length_zform f ->
                                        (dvalid_zform' f c1 <-> dvalid_zform' f c2).
  Proof.
    intros f c1; revert f; induction c1.
    intros; exfalso; destruct f; simpl in H; omega.

    destruct f; intros; simpl in H; simpl in H0;
    destruct c2;
    simpl;
    try (exfalso; omega);
    try tauto;

    try (rewrite (IHc1 f1 c2), (IHc1 f2 c2);
         try tauto; try omega; try (exfalso; omega));

    try (rewrite (IHc1 f c2); try tauto; omega);

    try (split; intros;
         try (destruct H1; exists x);
         [rewrite <- (IHc1 (substitute (v, conv q x) f) c2) | rewrite (IHc1 (substitute (v, conv q x) f) c2)];
         try apply H1;
         rewrite <- substitute_length_inv with (x := conv q x) (v := v);
         omega).
  Qed.

  Lemma and_dvalid_eq : forall f1 f2, dvalid_zform (ZF_And f1 f2) <-> dvalid_zform f1 /\ dvalid_zform f2.
  Proof.
    unfold dvalid_zform at 1.
    simpl.
    unfold dvalid_zform.
    intros.
    split; intros; split; inversion H;
    [ apply large_c_holds with (c2 := length_zform f1 + length_zform f2) |
      apply large_c_holds with (c2 := length_zform f1 + length_zform f2) |
      apply large_c_holds with (c2 := length_zform f1) |
      apply large_c_holds with (c2 := length_zform f2) ];
    try auto; try omega.
  Qed.

  Lemma or_dvalid_eq : forall f1 f2, dvalid_zform (ZF_Or f1 f2) <-> dvalid_zform f1 \/ dvalid_zform f2.
  Proof.
    unfold dvalid_zform at 1.
    simpl.
    unfold dvalid_zform.
    intros.
    split; intros; inversion H;
    [left | right | left | right];
    [ apply large_c_holds with (c2 := length_zform f1 + length_zform f2) |
      apply large_c_holds with (c2 := length_zform f1 + length_zform f2) |
      apply large_c_holds with (c2 := length_zform f1) |
      apply large_c_holds with (c2 := length_zform f2) ];
    try auto; try omega.
  Qed.

  Lemma imp_dvalid_eq : forall f1 f2, dvalid_zform (ZF_Imp f1 f2) <-> ~ dvalid_zform f1 \/ dvalid_zform f2.
  Proof.
    unfold dvalid_zform at 1.
    simpl.
    unfold dvalid_zform.
    intros.
    split; intros; inversion H;
    [left | right | left | right];
    [ intro; apply large_c_holds with (c2 := length_zform f1 + length_zform f2) in H1; [contradiction | omega | omega] |
      apply large_c_holds with (c2 := length_zform f1 + length_zform f2) |
      intro; apply large_c_holds with (c2 := length_zform f1) in H1; [contradiction | omega | omega] |
      apply large_c_holds with (c2 := length_zform f2) ];
    try auto; try omega.
  Qed.

  Lemma not_dvalid_eq : forall f, dvalid_zform (ZF_Not f) <-> ~ dvalid_zform f.
  Proof.
    unfold dvalid_zform at 1.
    simpl.
    unfold dvalid_zform.
    tauto.
  Qed.

End DirectSemantics.

Section Simplification.

  Definition eliminateMinMax (bf : ZBF) : ZF :=
    match bf with
        ZBF_Eq_Max e1 e2 e3 => ZF_Or (ZF_And (ZF_BF (ZBF_Eq e1 e2)) (ZF_BF (ZBF_Lte e3 e2)))
                                     (ZF_And (ZF_BF (ZBF_Eq e1 e3)) (ZF_BF (ZBF_Lte e2 e3)))
      | ZBF_Eq_Min e1 e2 e3 => ZF_Or (ZF_And (ZF_BF (ZBF_Eq e1 e2)) (ZF_BF (ZBF_Lte e2 e3)))
                                     (ZF_And (ZF_BF (ZBF_Eq e1 e3)) (ZF_BF (ZBF_Lte e3 e2)))
      | _ => ZF_BF bf
    end.

  Lemma eliminate_ok: forall bf, dvalid_zform (ZF_BF bf) <-> dvalid_zform (eliminateMinMax bf).
  Proof.
    destruct bf; simpl; try tauto;
    unfold dvalid_zform; simpl;
    rewrite orb_true_iff;
    repeat rewrite andb_true_iff;
    tauto.
  Qed.

  Fixpoint simplifyZF (form : ZF) : ZF :=
    match form with
        ZF_BF bf => eliminateMinMax bf
      | ZF_And f1 f2 => match (simplifyZF f1), (simplifyZF f2) with
                            ZF_BF (ZBF_Const true), e
                          | e, ZF_BF (ZBF_Const true) => e
                          | ZF_BF (ZBF_Const false), _
                          | _, ZF_BF (ZBF_Const false) => ZF_BF (ZBF_Const false)
                          | e1, e2 => ZF_And e1 e2
                        end
      | ZF_Or f1 f2 => match (simplifyZF f1), (simplifyZF f2) with
                            ZF_BF (ZBF_Const true), _
                          | _, ZF_BF (ZBF_Const true) => ZF_BF (ZBF_Const true)
                          | ZF_BF (ZBF_Const false), e
                          | e, ZF_BF (ZBF_Const false) => e
                          | e1, e2 => ZF_Or e1 e2
                       end
      | ZF_Imp f1 f2 => match (simplifyZF f1), (simplifyZF f2) with
                            ZF_BF (ZBF_Const false), _
                          | _, ZF_BF (ZBF_Const true) => ZF_BF (ZBF_Const true)
                          | ZF_BF (ZBF_Const true), e => e
                          | e , ZF_BF (ZBF_Const false) => match e with
                                                               ZF_BF (ZBF_Const true) => ZF_BF (ZBF_Const false)
                                                             | ZF_BF (ZBF_Const false) => ZF_BF (ZBF_Const true)
                                                             | _ => ZF_Not e
                                                           end
                          | e1, e2 => ZF_Imp e1 e2
                        end
      | ZF_Not f => match (simplifyZF f) with
                        ZF_BF (ZBF_Const true) => ZF_BF (ZBF_Const false)
                      | ZF_BF (ZBF_Const false) => ZF_BF (ZBF_Const true)
                      | e => ZF_Not e
                    end
      | ZF_Forall v q f => ZF_Forall v q (simplifyZF f)
      | ZF_Exists v q f => ZF_Exists v q (simplifyZF f)
    end.

End Simplification.

End ArithSemantics.