Library Theory

Require Import Omega.
Require Import Bool.
Require Import FunctionalExtensionality.
Require Import Classical.

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

Module Type SEM_VAL.
  Parameter Val : Set.
  Parameter val_eq_dec : forall v1 v2 : Val, {v1 = v2} + {v1 <> v2}.
  Parameter truth_and : Val -> Val -> Val.
  Parameter truth_or : Val -> Val -> Val.
  Parameter truth_not : Val -> Val.
  Parameter Top : Val.
  Parameter Btm : Val.
  Axiom top_neq_btm : Top <> Btm.
  Axiom truth_and_comm : forall v1 v2, truth_and v1 v2 = truth_and v2 v1.
  Axiom truth_or_comm : forall v1 v2, truth_or v1 v2 = truth_or v2 v1.
  Axiom truth_and_assoc : forall v1 v2 v3, truth_and v1 (truth_and v2 v3) = truth_and (truth_and v1 v2) v3.
  Axiom truth_or_assoc : forall v1 v2 v3, truth_or v1 (truth_or v2 v3) = truth_or (truth_or v1 v2) v3.
  Axiom truth_or_true_iff : forall v1 v2, truth_or v1 v2 = Top -> v1 = Top \/ v2 = Top.
  Axiom truth_and_true_iff : forall v1 v2, truth_and v1 v2 = Top -> v1 = Top /\ v2 = Top.
  Axiom truth_or_false_iff : forall v1 v2, truth_or v1 v2 = Btm -> v1 = Btm /\ v2 = Btm.
  Axiom truth_and_false_iff : forall v1 v2, truth_and v1 v2 = Btm -> v1 = Btm \/ v2 = Btm.
  Axiom tautology_1 : truth_not Btm = Top.
  Axiom tautology_2 : truth_not Top = Btm.
  Axiom tautology_3 : forall v, truth_and v v = v.
  Axiom tautology_4 : truth_and Top Btm = Btm.
  Axiom tautology_5 : forall v, truth_or v v = v.
  Axiom tautology_6 : truth_or Top Btm = Top.
End SEM_VAL.

Module Three_Val_NoneError <: SEM_VAL.

  Inductive Val_Impl := VTrue | VFalse | VError.
  Definition Val := Val_Impl.

  Definition val_eq_dec : forall v1 v2 : Val, {v1 = v2} + {v1 <> v2}.
  Defined.

  Definition Top := VTrue.
  Definition Btm := VFalse.

  Lemma top_neq_btm: Top <> Btm.

  Definition truth_not v :=
    match v with
      | VTrue => VFalse
      | VError => VError
      | VFalse => VTrue
    end.

  Definition truth_and (v1 v2 : Val) :=
    match v1, v2 with
      | VTrue , VTrue => VTrue
      | VTrue , VError => VError
      | VTrue , VFalse => VFalse
      | VError , _ => VError
      | VFalse , VError => VError
      | VFalse , VFalse => VFalse
      | VFalse , VTrue => VFalse
    end.

  Definition truth_or (v1 v2 : Val) :=
    match v1, v2 with
      | VTrue , VFalse => VTrue
      | VTrue , VTrue => VTrue
      | VTrue , VError => VError
      | VError , _ => VError
      | VFalse , VTrue => VTrue
      | VFalse , VError => VError
      | VFalse , VFalse => VFalse
    end.

  Lemma truth_and_comm : forall v1 v2, truth_and v1 v2 = truth_and v2 v1.

  Lemma truth_or_comm : forall v1 v2, truth_or v1 v2 = truth_or v2 v1.

  Lemma truth_and_assoc : forall v1 v2 v3, truth_and v1 (truth_and v2 v3) = truth_and (truth_and v1 v2) v3.

  Lemma truth_or_assoc : forall v1 v2 v3, truth_or v1 (truth_or v2 v3) = truth_or (truth_or v1 v2) v3.

  Lemma truth_or_true_iff : forall v1 v2, truth_or v1 v2 = Top -> v1 = Top \/ v2 = Top.

  Lemma truth_and_true_iff : forall v1 v2, truth_and v1 v2 = Top -> v1 = Top /\ v2 = Top.

  Lemma truth_or_false_iff : forall v1 v2, truth_or v1 v2 = Btm -> v1 = Btm /\ v2 = Btm.

  Lemma truth_and_false_iff : forall v1 v2, truth_and v1 v2 = Btm -> v1 = Btm \/ v2 = Btm.

  Lemma tautology_1 : truth_not Btm = Top.
  Lemma tautology_2 : truth_not Top = Btm.
  Lemma tautology_3 : forall v, truth_and v v = v.
  Lemma tautology_4 : truth_and Top Btm = Btm.
  Lemma tautology_5 : forall v, truth_or v v = v.
  Lemma tautology_6 : truth_or Top Btm = Top.
End Three_Val_NoneError.

Module Bool_Val <: SEM_VAL.
  Definition Val := bool.
  Definition truth_and := andb.
  Definition truth_or := orb.
  Definition truth_not := negb.
  Definition Top := true.
  Definition Btm := false.
  Definition val_eq_dec : forall v1 v2 : Val, {v1 = v2} + {v1 <> v2}.
  Defined.

  Lemma top_neq_btm: Top <> Btm.

  Lemma truth_and_comm : forall v1 v2, truth_and v1 v2 = truth_and v2 v1.

  Lemma truth_or_comm : forall v1 v2, truth_or v1 v2 = truth_or v2 v1.

  Lemma truth_and_assoc : forall v1 v2 v3, truth_and v1 (truth_and v2 v3) = truth_and (truth_and v1 v2) v3.

  Lemma truth_or_assoc : forall v1 v2 v3, truth_or v1 (truth_or v2 v3) = truth_or (truth_or v1 v2) v3.

  Lemma truth_or_true_iff : forall v1 v2, truth_or v1 v2 = Top -> v1 = Top \/ v2 = Top.

  Lemma truth_and_true_iff : forall v1 v2, truth_and v1 v2 = Top -> v1 = Top /\ v2 = Top.

  Lemma truth_or_false_iff : forall v1 v2, truth_or v1 v2 = Btm -> v1 = Btm /\ v2 = Btm.

  Lemma truth_and_false_iff : forall v1 v2, truth_and v1 v2 = Btm -> v1 = Btm \/ v2 = Btm.

  Lemma tautology_1 : truth_not Btm = Top.
  Lemma tautology_2 : truth_not Top = Btm.
  Lemma tautology_3 : forall v, truth_and v v = v.
  Lemma tautology_4 : truth_and Top Btm = Btm.
  Lemma tautology_5 : forall v, truth_or v v = v.
  Lemma tautology_6 : truth_or Top Btm = Top.

End Bool_Val.

Module Type NUMBER.
  Parameter A : Type.
  Parameter Const0 : A.
  Parameter num_eq_dec : forall n1 n2 : A, {n1 = n2} + {n1 <> n2}.
  Parameter num_neg : A -> A.
  Parameter num_plus : A -> A -> A.
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}.

  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 num_eq_dec : forall n1 n2 : A, {n1 = n2} + {n1 <> n2}.

  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.

  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.

  Lemma numneg_finite : forall v z, num_neg v = Some (ZE_Fin z)
                                    -> exists x, v = Some (ZE_Fin x) /\ (- x = z)%Z.

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

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

  Lemma numneg_inf : forall v, num_neg v = Some ZE_Inf
                               -> v = Some (ZE_NegInf).

  Lemma numneg_neginf : forall v, num_neg v = Some ZE_NegInf
                                  -> v = Some (ZE_Inf).

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

  Lemma numneg_none: forall v, num_neg v = None -> v = None.

End ZInfinity.

Module ZNumLattice <: NUMBER.
  Definition A := Z.
  Definition Const0 := 0%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.
End ZNumLattice.

Module Type LEQ_RELATION (NUM : NUMBER) (VAL : SEM_VAL).
  Import NUM.
  Import VAL.
  Parameter num_leq : A -> A -> Val.
  Axiom num_leq_top: forall x y, num_leq x y = Top -> x = y \/ num_leq y x = Btm.
  Axiom num_leq_btm:
    forall x y, num_leq x y = Btm -> num_leq y x = Top \/ (((forall z, num_leq z x = Btm /\ num_leq x z = Btm) \/
                                                            (forall z, num_leq z y = Btm /\ num_leq y z = Btm)) /\
                                                           (forall m n, num_leq m n = Top \/ num_leq m n = Btm)).
  Axiom num_leq_trans: forall x y z, num_leq x y = Top -> num_leq y z = Top -> num_leq x z = Top.
  Axiom num_leq_both_leq: forall x y z, num_leq x z = Top -> num_leq y z = Top -> num_leq x y = Top \/ num_leq x y = Btm.
  Axiom num_leq_leq_both: forall x y z, num_leq z x = Top -> num_leq z y = Top -> num_leq x y = Top \/ num_leq x y = Btm.
  Axiom num_leq_both_leq_btm: forall x y z, num_leq x z = Btm -> num_leq y z = Btm -> num_leq x y = Top \/ num_leq x y = Btm.
  Axiom num_leq_leq_both_btm: forall x y z, num_leq z x = Btm -> num_leq z y = Btm -> num_leq x y = Top \/ num_leq x y = Btm.
  Axiom num_leq_trans_btm_top: forall x y z, num_leq x y = Btm -> num_leq y z = Top -> num_leq x z = Top \/ num_leq x z = Btm.
  Axiom num_leq_trans_top_btm: forall x y z, num_leq x y = Top -> num_leq y z = Btm -> num_leq x z = Top \/ num_leq x z = Btm.
  Axiom num_leq_before_normal: forall x y z, num_leq x z = Btm -> num_leq y z = Top -> num_leq x y = Top \/ num_leq x y = Btm.
  Axiom num_leq_after_normal: forall x y z, num_leq z x = Btm -> num_leq z y = Top -> num_leq x y = Top \/ num_leq x y = Btm.
End LEQ_RELATION.

Module FinLeqRelation (VAL : SEM_VAL) <: LEQ_RELATION ZNumLattice VAL.
  Import ZNumLattice.
  Import VAL.

  Definition num_leq (x y : A) := if Z_le_dec x y then Top else Btm.

  Lemma num_leq_top: forall x y, num_leq x y = Top -> x = y \/ num_leq y x = Btm.

  Lemma num_leq_btm:
    forall x y, num_leq x y = Btm -> num_leq y x = Top \/ (((forall z, num_leq z x = Btm /\ num_leq x z = Btm) \/
                                                            (forall z, num_leq z y = Btm /\ num_leq y z = Btm)) /\
                                                           (forall m n, num_leq m n = Top \/ num_leq m n = Btm)).

  Ltac solve_num_leq_trans_fin :=
    repeat match goal with
             | [|- forall _, _] => intros
             | [|- context[num_leq _ _]] => unfold num_leq
             | [H: context[num_leq _ _] |- _] => unfold num_leq in H
             | [|- context[Z_le_dec ?z1 ?z0]] => destruct (Z_le_dec z1 z0)
             | [H: context[Z_le_dec ?z1 ?z0] |- _] => destruct (Z_le_dec z1 z0)
             | [|- ?A = ?A] => trivial
             | [H: ?A |- ?A] => apply H
             | [|- ?A = ?A \/ _] => left; trivial
             | [|- _ \/ ?A = ?A ] => right; trivial
           end.

  Lemma num_leq_trans: forall x y z, num_leq x y = Top -> num_leq y z = Top -> num_leq x z = Top.

  Lemma num_leq_both_leq: forall x y z, num_leq x z = Top -> num_leq y z = Top -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_leq_both: forall x y z, num_leq z x = Top -> num_leq z y = Top -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_both_leq_btm: forall x y z, num_leq x z = Btm -> num_leq y z = Btm -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_leq_both_btm: forall x y z, num_leq z x = Btm -> num_leq z y = Btm -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_trans_btm_top: forall x y z, num_leq x y = Btm -> num_leq y z = Top -> num_leq x z = Top \/ num_leq x z = Btm.

  Lemma num_leq_trans_top_btm: forall x y z, num_leq x y = Top -> num_leq y z = Btm -> num_leq x z = Top \/ num_leq x z = Btm.

  Lemma num_leq_before_normal: forall x y z, num_leq x z = Btm -> num_leq y z = Top -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_after_normal: forall x y z, num_leq z x = Btm -> num_leq z y = Top -> num_leq x y = Top \/ num_leq x y = Btm.

End FinLeqRelation.

Module Type NONE_RELATION (VAL : SEM_VAL).
  Import VAL.
  Parameter noneVal : Val.
  Axiom none_neq_top : noneVal <> Top.
  Axiom none_tautology_1 : truth_and noneVal (truth_not noneVal) = noneVal.
  Axiom none_tautology_2 : truth_and noneVal Top = noneVal.
  Axiom none_tautology_3 : truth_or (truth_and noneVal Btm) noneVal = noneVal.
  Axiom none_tautology_4 : truth_or noneVal Btm = noneVal.
End NONE_RELATION.

Module NoneError3ValRel <: NONE_RELATION Three_Val_NoneError.
  Import Three_Val_NoneError.
  Definition noneVal := VError.
  Lemma none_neq_top: noneVal <> Top.
  Lemma none_tautology_1 : truth_and noneVal (truth_not noneVal) = noneVal.
  Lemma none_tautology_2 : truth_and noneVal Top = noneVal.
  Lemma none_tautology_3 : truth_or (truth_and noneVal Btm) noneVal = noneVal.
  Lemma none_tautology_4 : truth_or noneVal Btm = noneVal.
End NoneError3ValRel.

Module NoneAlwaysFalse (VAL : SEM_VAL) <: NONE_RELATION VAL.
  Import VAL.
  Definition noneVal := Btm.
  Lemma none_neq_top: noneVal <> Top.
  Lemma none_tautology_1 : truth_and noneVal (truth_not noneVal) = noneVal.

  Lemma none_tautology_2 : truth_and noneVal Top = noneVal.

  Lemma none_tautology_3 : truth_or (truth_and noneVal Btm) noneVal = noneVal.

  Lemma none_tautology_4 : truth_or noneVal Btm = noneVal.

End NoneAlwaysFalse.

Module InfLeqRelation (VAL : SEM_VAL) (S: NONE_RELATION VAL) <: LEQ_RELATION ZInfinity VAL.
  Import ZInfinity.
  Import VAL.
  Import S.
  Definition num_leq (ze1 ze2 : A) : Val :=
    match ze1, ze2 with
      | None, _
      | _, None => noneVal
      | _, Some ZE_Inf => Top
      | Some ZE_NegInf, _ => Top
      | Some ZE_Inf, Some x => if ZE_eq_dec x ZE_Inf then Top else Btm
      | Some x, Some ZE_NegInf => if ZE_eq_dec x ZE_NegInf then Top else Btm
      | Some (ZE_Fin z1), Some (ZE_Fin z2) => if Z_le_dec z1 z2 then Top else Btm
    end.

  Ltac solve_num_leq_top :=
    repeat match goal with
             | [|- forall _, _] => intros
             | [x : A |- _] => destruct x
             | [x : ZE |- _] => destruct x
             | [H : context[num_leq (Some _) (Some _)] |- _] => simpl in H
             | [H : context[num_leq (Some _) None] |- _] => simpl in H
             | [H : context[num_leq None (Some _)] |- _] => simpl in H
             | [H : context[num_leq None None] |- _] => simpl in H
             | [|- context[num_leq (Some _) (Some _)]] => simpl
             | [|- context[num_leq (Some _) None]] => simpl
             | [|- context[num_leq None (Some _)]] => simpl
             | [|- context[num_leq None None]] => simpl
             | [H : noneVal = Top |- _] =>
               let H0 := fresh "H0" in generalize none_neq_top; intro H0; rewrite H in H0; exfalso; intuition
             | [H : context[Z_le_dec ?z0 ?z] |- _] => destruct (Z_le_dec z0 z)
             | [H : Btm = Top |- _] =>
               let H0 := fresh "H0" in generalize top_neq_btm; intro H0; rewrite H in H0; exfalso; intuition
             | [|- _ \/ ?A = ?A] => right; trivial
             | [|- ?A = ?A \/ _] => left; trivial
           end.

  Lemma num_leq_top: forall x y, num_leq x y = Top -> x = y \/ num_leq y x = Btm.

  Ltac solve_num_leq_val:=
    repeat match goal with
             | [|- forall _, _] => intros
             | [x : A |- _] => destruct x
             | [x : ZE |-_] => destruct x
             | [|- context[num_leq _ _]] => simpl
             | [H: context[num_leq _ _] |- _] => simpl in H
             | [|- ?A = ?A \/ _] => left; trivial
             | [|- _ \/ ?A = ?A \/ _] => right; left; trivial
             | [|- _ \/ _ \/ ?A = ?A] => right; right; trivial
           end.

  Lemma num_leq_val: forall x y, num_leq x y = Top \/ num_leq x y = Btm \/ num_leq x y = noneVal.

  Ltac solve_num_leq_btm :=
    repeat match goal with
             | [|- forall _, _] => intros
             | [x : A |- _] => destruct x
             | [x : ZE |-_] => destruct x
             | [H: Top = Btm |- _] => exfalso; apply top_neq_btm; apply H
             | [|- ?A = ?A \/ _] => left; trivial
             | [|- num_leq _ _ = _ \/ _ ] => simpl
             | [H: num_leq _ _ = _ |- _] => simpl in H
             | [H : noneVal = Btm |- noneVal = Top \/ _] => right
             | [H: noneVal = Btm |- (forall _, num_leq _ None = Btm /\ noneVal = Btm) \/ _] => left; split; auto
             | [H: noneVal = Btm |- _ \/ (forall _, num_leq _ None = Btm /\ noneVal = Btm)] => right; split; auto
             | [|- num_leq _ _ = _] => simpl
             | [H: ?A |- ?A] => apply H
             | [H: context[Z_le_dec ?x ?y] |- _] => destruct (Z_le_dec x y)
             | [|- context[Z_le_dec ?x ?y]] => destruct (Z_le_dec x y)
             | [|- _ /\ _] => split
             | [|- _ \/ ?A = ?A] => right; trivial
           end.

  Lemma num_leq_btm:
    forall x y, num_leq x y = Btm -> num_leq y x = Top \/ (((forall z, num_leq z x = Btm /\ num_leq x z = Btm) \/
                                                            (forall z, num_leq z y = Btm /\ num_leq y z = Btm)) /\
                                                           (forall m n, num_leq m n = Top \/ num_leq m n = Btm)).

  Ltac solve_num_leq_trans :=
    repeat match goal with
             | [|- forall _, _] => intros
             | [x : A |- _] => destruct x
             | [x : ZE |- _] => destruct x
             | [|- context[num_leq _ _]] => simpl
             | [H: context[num_leq _ _] |- _] => simpl in H
             | [H: ?A |- ?A] => apply H
             | [H: ?A = ?B |- ?B = ?A] => rewrite H; trivial
             | [|- ?A = ?A] => trivial
             | [H: noneVal = Top |- _] =>
               let S := fresh "S" in generalize none_neq_top; intro S; exfalso; rewrite H in S; apply S; trivial
             | [H: Btm = Top |- _] => exfalso; apply top_neq_btm
             | [|- context[Z_le_dec ?z1 ?z0]] => destruct (Z_le_dec z1 z0)
             | [H: context[Z_le_dec ?z1 ?z0] |- _] => destruct (Z_le_dec z1 z0)
             | [|- ?A = ?A \/ _] => left; trivial
             | [|- _ \/ ?A = ?A ] => right; trivial
             | [H: ?A |- ?A \/ _] => left; apply H
             | [H: ?A |- _ \/ ?A] => right; apply H
           end.

  Lemma num_leq_trans: forall x y z, num_leq x y = Top -> num_leq y z = Top -> num_leq x z = Top.

  Lemma num_leq_both_leq: forall x y z, num_leq x z = Top -> num_leq y z = Top -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_leq_both: forall x y z, num_leq z x = Top -> num_leq z y = Top -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_both_leq_btm: forall x y z, num_leq x z = Btm -> num_leq y z = Btm -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_leq_both_btm: forall x y z, num_leq z x = Btm -> num_leq z y = Btm -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_trans_btm_top: forall x y z, num_leq x y = Btm -> num_leq y z = Top -> num_leq x z = Top \/ num_leq x z = Btm.

  Lemma num_leq_trans_top_btm: forall x y z, num_leq x y = Top -> num_leq y z = Btm -> num_leq x z = Top \/ num_leq x z = Btm.

  Lemma num_leq_before_normal: forall x y z, num_leq x z = Btm -> num_leq y z = Top -> num_leq x y = Top \/ num_leq x y = Btm.

  Lemma num_leq_after_normal: forall x y z, num_leq z x = Btm -> num_leq z y = Top -> num_leq x y = Top \/ num_leq x y = Btm.

End InfLeqRelation.

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 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 Type ZERO_PRODUCT (NUM : NUMBER).
  Import NUM.
  Parameter zero_times: A -> A.
End ZERO_PRODUCT.

Module Type ZERO_FIN <: ZERO_PRODUCT ZNumLattice.
  Import ZNumLattice.
  Parameter zero_times: A -> A.
  Axiom all_is_zero: forall x, zero_times x = 0%Z.
End ZERO_FIN.

Module FinZero <: ZERO_FIN.
  Import ZNumLattice.
  Definition zero_times (_ : A) := 0%Z.
  Lemma all_is_zero: forall x, zero_times x = 0%Z.
End FinZero.

Module Type ZERO_INF <: ZERO_PRODUCT ZInfinity.
  Import ZInfinity.
  Parameter zero_times: A -> A.
  Axiom zero_times_spec: (forall x, zero_times x = Some (ZE_Fin 0)) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => None end) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end).
End ZERO_INF.

Module InfZeroAll <: ZERO_INF.
  Import ZInfinity.
  Definition zero_times (_ : A) := Some (ZE_Fin 0).
  Lemma zero_times_spec: (forall x, zero_times x = Some (ZE_Fin 0)) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => None end) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end).

End InfZeroAll.

Module InfZeroFinOnly <: ZERO_INF.
  Import ZInfinity.
  Definition zero_times (x : A) :=
    match x with
      | Some (ZE_Fin _) => Some (ZE_Fin 0)
      | _ => None
    end.
  Lemma zero_times_spec: (forall x, zero_times x = Some (ZE_Fin 0)) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => None end) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end).

End InfZeroFinOnly.

Module InfZeroInf <: ZERO_INF.
  Import ZInfinity.
  Definition zero_times (x : A) :=
    match x with
      | Some (ZE_Fin _) => Some (ZE_Fin 0)
      | _ => x
    end.
  Lemma zero_times_spec: (forall x, zero_times x = Some (ZE_Fin 0)) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => None end) \/
                         (forall x, zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end).

End InfZeroInf.

Module ArithSemantics (I : SEMANTICS_INPUT) (V : VARIABLE) (VAL : SEM_VAL) (L : LEQ_RELATION I.N VAL) (ZT : ZERO_PRODUCT I.N).
  Import I N V VAL L ZT.

  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 : Val -> 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 => zero_times x
        | S O => x
        | S n => num_plus x (num_mult_nat n x)
      end.

    Lemma num_mult_nat_2_unfold: forall n x, num_mult_nat (S (S n)) x = num_plus x (num_mult_nat (S n) x).

    Definition num_mult (z : Z) (exp : A) : A :=
      match z with
        | Z0 => zero_times exp
        | 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.

    Lemma same_var_subst_bf: forall bf v a1 a2, subst_bf (v, a1) (subst_bf (v, a2) bf) = subst_bf (v, a2) bf.

    Lemma same_var_subst: forall f v a1 a2, substitute (v, a1) (substitute (v, a2) f) = substitute (v, a2) f.

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

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

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

    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) : Val :=
      match bf with
          ZBF_Const b => b
        | ZBF_Lt e1 e2 => let v1 := dexp2ZE e1 in
                           let v2 := dexp2ZE e2 in
                           truth_and (num_leq v1 v2) (truth_not (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
                           truth_and (num_leq v2 v1) (truth_not (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
                           truth_and (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
          truth_or (truth_and (num_leq v3 v2) (truth_and (num_leq v1 v2) (num_leq v2 v1)))
                   (truth_and (num_leq v2 v3) (truth_and (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
          truth_or (truth_and (num_leq v3 v2) (truth_and (num_leq v1 v3) (num_leq v3 v1)))
                   (truth_and (num_leq v2 v3) (truth_and (num_leq v1 v2) (num_leq v2 v1)))
        | ZBF_Neq e1 e2 => let v1 := dexp2ZE e1 in
                           let v2 := dexp2ZE e2 in
                           truth_not (truth_and (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.

    Lemma substitute_length_inv : forall f x v, length_zform f = length_zform (substitute (v, x) f).

    Inductive Input := Sat: ZF -> Input | DisSat: ZF -> Input | Udtmd: ZF -> Input.

    Definition length_input (inp : Input) :=
      match inp with
        | Sat f => length_zform f
        | DisSat f => length_zform f
        | Udtmd f => length_zform f
      end.

    Definition inputOrder (f1 f2 : Input) := length_input f1 < length_input f2.

    Lemma inputOrder_wf': forall len f, length_input f <= len -> Acc inputOrder f.

    Theorem inputOrder_wf: well_founded inputOrder.

    Ltac smash := intros; unfold inputOrder; simpl; omega || rewrite <- substitute_length_inv; omega.

    Lemma sat_and_1: forall f1 f2, inputOrder (Sat f1) (Sat (ZF_And f1 f2)).
    Lemma sat_and_2: forall f1 f2, inputOrder (Sat f2) (Sat (ZF_And f1 f2)).
    Lemma sat_or_1: forall f1 f2, inputOrder (Sat f1) (Sat (ZF_Or f1 f2)).
    Lemma sat_or_2: forall f1 f2, inputOrder (Sat f2) (Sat (ZF_Or f1 f2)).
    Lemma sat_or_3: forall f1 f2, inputOrder (DisSat f1) (Sat (ZF_Or f1 f2)).
    Lemma sat_or_4: forall f1 f2, inputOrder (DisSat f2) (Sat (ZF_Or f1 f2)).
    Lemma sat_imp_1: forall f1 f2, inputOrder (DisSat f1) (Sat (ZF_Imp f1 f2)).
    Lemma sat_imp_2: forall f1 f2, inputOrder (Sat f2) (Sat (ZF_Imp f1 f2)).
    Lemma sat_imp_3: forall f1 f2, inputOrder (Sat f1) (Sat (ZF_Imp f1 f2)).
    Lemma sat_imp_4: forall f1 f2, inputOrder (DisSat f2) (Sat (ZF_Imp f1 f2)).
    Lemma sat_not : forall f, inputOrder (DisSat f) (Sat (ZF_Not f)).
    Lemma sat_forall:forall f v q(x:QT q),inputOrder(Sat (substitute (v, @conv q x) f))(Sat (ZF_Forall v q f)).
    Lemma sat_exists:forall f v q(x:QT q),inputOrder(Sat (substitute (v, @conv q x) f))(Sat (ZF_Exists v q f)).
    Lemma dst_and_1: forall f1 f2, inputOrder (DisSat f1) (DisSat (ZF_And f1 f2)).
    Lemma dst_and_2: forall f1 f2, inputOrder (DisSat f2) (DisSat (ZF_And f1 f2)).
    Lemma dst_and_3: forall f1 f2, inputOrder (Sat f1) (DisSat (ZF_And f1 f2)).
    Lemma dst_and_4: forall f1 f2, inputOrder (Sat f2) (DisSat (ZF_And f1 f2)).
    Lemma dst_or_1: forall f1 f2, inputOrder (DisSat f1) (DisSat (ZF_Or f1 f2)).
    Lemma dst_or_2: forall f1 f2, inputOrder (DisSat f2) (DisSat (ZF_Or f1 f2)).
    Lemma dst_imp_1: forall f1 f2, inputOrder (Sat f1) (DisSat (ZF_Imp f1 f2)).
    Lemma dst_imp_2: forall f1 f2, inputOrder (DisSat f2) (DisSat (ZF_Imp f1 f2)).
    Lemma dst_not : forall f, inputOrder (Sat f) (DisSat (ZF_Not f)).
    Lemma dst_forall:forall f v q(x:QT q),inputOrder(DisSat(substitute (v,@conv q x) f))(Sat (ZF_Forall v q f)).
    Lemma dst_exists:forall f v q(x:QT q),inputOrder(DisSat(substitute (v,@conv q x) f))(Sat (ZF_Exists v q f)).
    Lemma udd_and_1 : forall f1 f2, inputOrder (Sat f1) (Udtmd (ZF_And f1 f2)).
    Lemma udd_and_2 : forall f1 f2, inputOrder (Sat f2) (Udtmd (ZF_And f1 f2)).
    Lemma udd_and_3 : forall f1 f2, inputOrder (DisSat f1) (Udtmd (ZF_And f1 f2)).
    Lemma udd_and_4 : forall f1 f2, inputOrder (DisSat f2) (Udtmd (ZF_And f1 f2)).
    Lemma udd_or_1 : forall f1 f2, inputOrder (Sat f1) (Udtmd (ZF_Or f1 f2)).
    Lemma udd_or_2 : forall f1 f2, inputOrder (Sat f2) (Udtmd (ZF_Or f1 f2)).
    Lemma udd_or_3 : forall f1 f2, inputOrder (DisSat f1) (Udtmd (ZF_Or f1 f2)).
    Lemma udd_or_4 : forall f1 f2, inputOrder (DisSat f2) (Udtmd (ZF_Or f1 f2)).
    Lemma udd_imp_1 : forall f1 f2, inputOrder (DisSat f1) (Udtmd (ZF_Imp f1 f2)).
    Lemma udd_imp_2 : forall f1 f2, inputOrder (Sat f2) (Udtmd (ZF_Imp f1 f2)).
    Lemma udd_imp_3 : forall f1 f2, inputOrder (Sat f1) (Udtmd (ZF_Imp f1 f2)).
    Lemma udd_imp_4 : forall f1 f2, inputOrder (DisSat f2) (Udtmd (ZF_Imp f1 f2)).
    Lemma udd_not_1 : forall f, inputOrder (DisSat f) (Udtmd (ZF_Not f)).
    Lemma udd_not_2 : forall f, inputOrder (Sat f) (Udtmd (ZF_Not f)).
    Lemma udd_forall_1:forall f v q(x:QT q),inputOrder(Sat(substitute(v,@conv q x)f))(Udtmd(ZF_Forall v q f)).
    Lemma udd_forall_2:forall f v q(x:QT q),inputOrder(DisSat(substitute(v,@conv q x)f))(Udtmd(ZF_Forall v q f)).
    Lemma udd_exists_1:forall f v q(x:QT q),inputOrder(Sat(substitute(v,@conv q x)f))(Udtmd(ZF_Exists v q f)).
    Lemma udd_exists_2:forall f v q(x:QT q),inputOrder(DisSat(substitute(v,@conv q x)f))(Udtmd(ZF_Exists v q f)).

    Definition three_pred : Input -> Prop :=
      Fix inputOrder_wf (fun _ => Prop)
          (fun (inp : Input) =>
             match inp return ((forall ff : Input, inputOrder ff inp -> Prop) -> Prop) with
               | Sat g =>
                 match g with
                   | ZF_BF bf => fun _ => dzbf2bool bf = Top
                   | ZF_And f1 f2 => fun tpF => (tpF (Sat f1) (sat_and_1 f1 f2)) /\ (tpF (Sat f2) (sat_and_2 f1 f2))
                   | ZF_Or f1 f2 => fun tpF => ((tpF (Sat f1) (sat_or_1 f1 f2)) /\ (tpF (Sat f2) (sat_or_2 f1 f2))) \/
                                                 ((tpF (DisSat f1) (sat_or_3 f1 f2)) /\ (tpF (Sat f2) (sat_or_2 f1 f2))) \/
                                                 ((tpF (Sat f1) (sat_or_1 f1 f2)) /\ (tpF (DisSat f2) (sat_or_4 f1 f2)))
                   | ZF_Imp f1 f2 => fun tpF => ((tpF (Sat f1) (sat_imp_3 f1 f2)) /\ (tpF (Sat f2) (sat_imp_2 f1 f2))) \/
                                                 ((tpF (DisSat f1) (sat_imp_1 f1 f2)) /\ (tpF (Sat f2) (sat_imp_2 f1 f2))) \/
                                                 ((tpF (DisSat f1) (sat_imp_1 f1 f2)) /\ (tpF (DisSat f2) (sat_imp_4 f1 f2)))
                   | ZF_Not f => fun tpF => (tpF (DisSat f) (sat_not f))
                   | ZF_Forall v q f => fun tpF => forall x: QT q, tpF (Sat (substitute (v, @conv q x) f)) (sat_forall f v q x)
                   | ZF_Exists v q f => fun tpF =>
                                          (exists x: QT q, tpF (Sat (substitute (v, @conv q x) f)) (sat_exists f v q x)) /\
                                          (forall x: QT q, (tpF (Sat (substitute (v, @conv q x) f)) (sat_exists f v q x)) \/
                                                           (tpF (DisSat (substitute (v, @conv q x) f)) (sat_exists f v q x)))
                 end
               | DisSat g =>
                 match g with
                   | ZF_BF bf => fun _ => dzbf2bool bf = Btm
                   | ZF_And f1 f2 => fun tpF => ((tpF (DisSat f1) (dst_and_1 f1 f2)) /\ (tpF (DisSat f2) (dst_and_2 f1 f2))) \/
                                                ((tpF (Sat f1) (dst_and_3 f1 f2)) /\ (tpF (DisSat f2) (dst_and_2 f1 f2))) \/
                                                ((tpF (DisSat f1) (dst_and_1 f1 f2)) /\ (tpF (Sat f2) (dst_and_4 f1 f2)))
                   | ZF_Or f1 f2 => fun tpF => (tpF (DisSat f1) (dst_or_1 f1 f2)) /\ (tpF (DisSat f2) (dst_or_2 f1 f2))
                   | ZF_Imp f1 f2 => fun tpF => (tpF (Sat f1) (dst_imp_1 f1 f2)) /\ (tpF (DisSat f2) (dst_imp_2 f1 f2))
                   | ZF_Not f => fun tpF => (tpF (Sat f) (dst_not f))
                   | ZF_Forall v q f => fun tpF =>
                                          (exists x: QT q, tpF (DisSat (substitute (v, @conv q x) f)) (dst_exists f v q x)) /\
                                          (forall x: QT q, (tpF (Sat (substitute (v, @conv q x) f)) (dst_exists f v q x)) \/
                                                           (tpF (DisSat (substitute (v, @conv q x) f)) (dst_exists f v q x)))
                   | ZF_Exists v q f => fun tpF => forall x : QT q,
                                                     tpF (DisSat (substitute (v, @conv q x) f)) (dst_exists f v q x)
                 end
               | Udtmd g =>
                 match g with
                   | ZF_BF bf => fun _ => (dzbf2bool bf <> Top) /\ (dzbf2bool bf <> Btm)
                   | ZF_And f1 f2 => fun tpF =>
                                       (~ ((tpF (Sat f1) (sat_and_1 f1 f2)) /\ (tpF (Sat f2) (sat_and_2 f1 f2)))) /\
                                       (~ (((tpF (DisSat f1) (dst_and_1 f1 f2)) /\ (tpF (DisSat f2) (dst_and_2 f1 f2))) \/
                                           ((tpF (Sat f1) (dst_and_3 f1 f2)) /\ (tpF (DisSat f2) (dst_and_2 f1 f2))) \/
                                           ((tpF (DisSat f1) (dst_and_1 f1 f2)) /\ (tpF (Sat f2) (dst_and_4 f1 f2)))))
                   | ZF_Or f1 f2 => fun tpF =>
                                      (~ (((tpF (Sat f1) (sat_or_1 f1 f2)) /\ (tpF (Sat f2) (sat_or_2 f1 f2))) \/
                                          ((tpF (DisSat f1) (sat_or_3 f1 f2)) /\ (tpF (Sat f2) (sat_or_2 f1 f2))) \/
                                          ((tpF (Sat f1) (sat_or_1 f1 f2)) /\ (tpF (DisSat f2) (sat_or_4 f1 f2))))) /\
                                      (~ ((tpF (DisSat f1) (dst_or_1 f1 f2)) /\ (tpF (DisSat f2) (dst_or_2 f1 f2))))
                   | ZF_Imp f1 f2 => fun tpF =>
                                       (~ (((tpF (Sat f1) (sat_imp_3 f1 f2)) /\ (tpF (Sat f2) (sat_imp_2 f1 f2))) \/
                                           ((tpF (DisSat f1) (sat_imp_1 f1 f2)) /\ (tpF (Sat f2) (sat_imp_2 f1 f2))) \/
                                           ((tpF (DisSat f1) (sat_imp_1 f1 f2)) /\ (tpF (DisSat f2) (sat_imp_4 f1 f2))))) /\
                                       (~ ((tpF (Sat f1) (dst_imp_1 f1 f2)) /\ (tpF (DisSat f2) (dst_imp_2 f1 f2))))
                   | ZF_Not f => fun tpF => (~ (tpF (DisSat f) (sat_not f))) /\ (~ (tpF (Sat f) (dst_not f)))
                   | ZF_Forall v q f =>
                     fun tpF => (~ (forall x: QT q, tpF (Sat (substitute (v, @conv q x) f)) (sat_forall f v q x))) /\
                                (~ ((exists x: QT q, tpF (DisSat (substitute (v, @conv q x) f)) (dst_exists f v q x)) /\
                                    (forall x: QT q, (tpF (Sat (substitute (v, @conv q x) f)) (dst_exists f v q x)) \/
                                                     (tpF (DisSat (substitute (v, @conv q x) f)) (dst_exists f v q x)))))
                   | ZF_Exists v q f =>
                     fun tpF => (~ ((exists x: QT q, tpF (Sat (substitute (v, @conv q x) f)) (sat_exists f v q x)) /\
                                    (forall x: QT q, (tpF (Sat (substitute (v, @conv q x) f)) (sat_exists f v q x)) \/
                                                     (tpF (DisSat (substitute (v, @conv q x) f)) (sat_exists f v q x))))) /\
                                (~ (forall x : QT q, tpF (DisSat (substitute (v, @conv q x) f)) (dst_exists f v q x)))
                 end
             end).
    Definition satisfied form := three_pred (Sat form).
    Definition dissatisfied form := three_pred (DisSat form).
    Definition undetermined form := three_pred (Udtmd form).

    Lemma satisfied_unfold :
      forall zf, satisfied zf = match zf with
                                  | ZF_BF bf => (dzbf2bool bf = Top)
                                  | ZF_And f1 f2 => (satisfied f1) /\ (satisfied f2)
                                  | ZF_Or f1 f2 => ((satisfied f1) /\ (satisfied f2)) \/
                                                     ((dissatisfied f1) /\ (satisfied f2)) \/
                                                     ((satisfied f1) /\ (dissatisfied f2))
                                  | ZF_Imp f1 f2 => ((satisfied f1) /\ (satisfied f2)) \/
                                                     ((dissatisfied f1) /\ (satisfied f2)) \/
                                                     ((dissatisfied f1) /\ (dissatisfied f2))
                                  | ZF_Not f => dissatisfied f
                                  | ZF_Forall v q f => forall x : QT q, (satisfied (substitute (v , @conv q x) f))
                                  | ZF_Exists v q f => (exists x : QT q, satisfied (substitute (v , @conv q x) f)) /\
                                                       (forall x : QT q, (satisfied (substitute (v , @conv q x) f)) \/
                                                                         (dissatisfied (substitute (v , @conv q x) f)))
                                end.

    Lemma dissatisfied_unfold :
      forall zf, dissatisfied zf = match zf with
                                     | ZF_BF bf => (dzbf2bool bf = Btm)
                                     | ZF_And f1 f2 => ((dissatisfied f1) /\ (dissatisfied f2)) \/
                                                        ((satisfied f1) /\ (dissatisfied f2)) \/
                                                        ((dissatisfied f1) /\ (satisfied f2))
                                     | ZF_Or f1 f2 => (dissatisfied f1) /\ (dissatisfied f2)
                                     | ZF_Imp f1 f2 => (satisfied f1) /\ (dissatisfied f2)
                                     | ZF_Not f => satisfied f
                                     | ZF_Forall v q f => (exists x : QT q, dissatisfied (substitute (v , @conv q x) f)) /\
                                                          (forall x : QT q, (satisfied (substitute (v , @conv q x) f)) \/
                                                                            (dissatisfied (substitute (v , @conv q x) f)))
                                     | ZF_Exists v q f => forall x : QT q, (dissatisfied (substitute (v , @conv q x) f))
                                   end.

    Lemma undetermined_unfold : forall zf, undetermined zf <-> (~ satisfied zf) /\ (~ dissatisfied zf).

    Lemma sat_dissat_disj: forall zf, ~ (satisfied zf /\ dissatisfied zf).

    Lemma sat_undtmd_disj : forall zf, ~ (satisfied zf /\ undetermined zf).

    Lemma dissat_undtmd_disj : forall zf, ~ (dissatisfied zf /\ undetermined zf).

    Eval compute in satisfied (ZF_BF (ZBF_Const Btm)).

    Eval compute in satisfied (ZF_Or (ZF_BF (ZBF_Const Top)) (ZF_BF (ZBF_Const Btm))).

    Lemma three_possible: forall zf, satisfied zf \/ dissatisfied zf \/ undetermined zf.

    Lemma sat_dis_udt_eq: forall zf T, (satisfied zf <-> satisfied (T zf)) -> (dissatisfied zf <-> dissatisfied (T zf)) ->
                                       (undetermined zf <-> undetermined (T zf)).

  End DirectSemantics.

  Section ZFWellFounded.

    Definition lengthOrder (f1 f2 : ZF) := length_zform f1 < length_zform f2.

    Lemma lengthOrder_wf': forall len f, length_zform f <= len -> Acc lengthOrder f.

    Theorem lengthOrder_wf: well_founded lengthOrder.

    Ltac smash := intros; unfold lengthOrder; simpl; omega || rewrite <- substitute_length_inv; omega.

    Lemma lengthOrder_forall:forall f v q (x: QT q), lengthOrder (substitute (v, @conv q x) f) (ZF_Forall v q f).
    Lemma lengthOrder_forall_trivial: forall f v q, lengthOrder f (ZF_Forall v q f).
    Lemma lengthOrder_exists:forall f v q (x: QT q), lengthOrder (substitute (v, @conv q x) f) (ZF_Exists v q f).
    Lemma lengthOrder_exists_trivial: forall f v q, lengthOrder f (ZF_Exists v q f).
    Lemma lengthOrder_and_1: forall f1 f2, lengthOrder f1 (ZF_And f1 f2).
    Lemma lengthOrder_and_2: forall f1 f2, lengthOrder f2 (ZF_And f1 f2).
    Lemma lengthOrder_or_1: forall f1 f2, lengthOrder f1 (ZF_Or f1 f2).
    Lemma lengthOrder_or_2: forall f1 f2, lengthOrder f2 (ZF_Or f1 f2).
    Lemma lengthOrder_imp_1: forall f1 f2, lengthOrder f1 (ZF_Imp f1 f2).
    Lemma lengthOrder_imp_2: forall f1 f2, lengthOrder f2 (ZF_Imp f1 f2).
    Lemma lengthOrder_not: forall f, lengthOrder f (ZF_Not f).

  End ZFWellFounded.

  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 num_leq_refl: forall x y, num_leq x y = Top -> num_leq y x = Top -> x = y.

    Lemma num_leq_btm_trans: forall x y z, num_leq x y = Btm -> num_leq y z = Btm -> num_leq x z = Btm \/ num_leq x z = Top.

    Ltac solve_eliminate :=
      repeat match goal with
               | [|- forall _, _] => intros
               | [z: ZBF |- _] => destruct z
               | [|- context[satisfied _]] => rewrite satisfied_unfold; simpl
               | [|- context[dissatisfied _]] => rewrite dissatisfied_unfold; simpl
               | [|- _ /\ _] => split
               | [|- _ <-> _] => split
               | [|- _ -> _] => intros
               | [|- context [eliminateMinMax _]] => simpl
               | [H: ?A |- ?A] => apply H
               | [H: truth_or _ _ = Top |- _] => apply truth_or_true_iff in H
               | [H: truth_or _ _ = Btm |- _] => apply truth_or_false_iff in H
               | [H: _ \/ _ |- _] => destruct H
               | [H: truth_and _ _ = Top |- _] => apply truth_and_true_iff in H
               | [H: truth_and _ _ = Btm |- _] => apply truth_and_false_iff in H
               | [H: _ /\ _ |- _] => destruct H
               | [H: ?A = _ |- context[?A]] => rewrite H
               | [|- context[truth_and ?A ?A]] => rewrite tautology_3
               | [H1 : num_leq ?A ?A = Top, H2 : num_leq ?A ?A = Top |- _] => clear H1
               | [H1 : num_leq ?A ?B = Top, H2 : num_leq ?B ?A = Top |- _] =>
                 let H := fresh "H" in
                 generalize (num_leq_refl _ _ H1 H2); intro H; rewrite H in *; clear H H1
               | [|- context[truth_and ?v (truth_and ?v _)]] => rewrite truth_and_assoc, tautology_3
               | [H : num_leq ?A ?B = Top |- context[num_leq ?B ?A]] => destruct (num_leq_top _ _ H)
               | [|- context[truth_or ?A ?A]] => rewrite tautology_5
               | [|- ?A = ?A] => trivial
               | [|- context[truth_and Btm Top]] => rewrite (truth_and_comm Btm Top), tautology_4
               | [|- context[truth_and Top Btm]] => rewrite tautology_4
               | [|- context[truth_or Top Btm]] => rewrite tautology_6
               | [|- context[truth_or Btm Top]] => rewrite (truth_or_comm Btm Top), tautology_6
               | [H : num_leq ?A ?B = Btm |- context[num_leq ?B ?A]] => destruct (num_leq_btm _ _ H); clear H
               | [|- ?A = ?A \/ _] => left; trivial
               | [H : forall _, num_leq _ ?A = Btm /\ num_leq ?A _ = Btm |- context[num_leq ?B ?A]] =>
                 let H1 := fresh "H1" in let H2 := fresh "H2" in destruct (H B) as [H1 H2]; rewrite H1
               | [H : forall _, num_leq _ ?A = Btm /\ num_leq ?A _ = Btm |- context[num_leq ?A ?B]] =>
                 let H1 := fresh "H1" in let H2 := fresh "H2" in destruct (H B) as [H1 H2]; rewrite H2
               | [H : forall _, num_leq _ ?A = Btm /\ num_leq ?A _ = Btm, T: num_leq ?B ?A = Top |- _] =>
                 let H1 := fresh "H1" in let H2 := fresh "H2" in destruct (H B) as [H1 H2]; rewrite T in H1;
                                                                 exfalso; apply top_neq_btm; apply H1
               | [H : forall _, num_leq _ ?A = Btm /\ num_leq ?A _ = Btm, T: num_leq ?A ?B = Top |- _] =>
                 let H1 := fresh "H1" in let H2 := fresh "H2" in destruct (H B) as [H1 H2]; rewrite T in H2;
                                                                 exfalso; apply top_neq_btm; apply H2
               | [|- context[Top = Top]] => tauto
               | [|- context[Btm = Btm]] => tauto
               | [H1 : num_leq ?x ?z = Top, H2: num_leq ?y ?z = Top |- context[num_leq ?x ?y]] =>
                 destruct (num_leq_both_leq x y z H1 H2)
               | [H1 : ?A = ?B, H2: context[?A] |- _] => rewrite H1 in H2
               | [H : forall m n : A, num_leq m n = Top \/ num_leq m n = Btm |- context[num_leq ?A ?B]] => destruct (H A B)
               | [H1 : num_leq ?x ?y = Top, H2: num_leq ?y ?z = Top |- context[num_leq ?x ?z]] =>
                 let H := fresh "H" in generalize (num_leq_trans _ _ _ H1 H2); intro H; rewrite H
               | [H1 : num_leq ?z ?x = Top, H2: num_leq ?z ?y = Top |- context[num_leq ?x ?y]] =>
                 destruct (num_leq_leq_both x y z H1 H2)
               | [H1 : num_leq ?x ?y = Btm, H2: num_leq ?y ?z = Btm |- context[num_leq ?x ?z]] =>
                 let H := fresh "H" in destruct (num_leq_btm_trans _ _ _ H1 H2) as [H | H]; rewrite H
               | [H1: num_leq ?x ?y = Btm, H2: num_leq ?y ?x = Btm |- _] => destruct (num_leq_btm _ _ H1)
               | [H: Btm = Top |- _] => exfalso; apply top_neq_btm
               | [H1 : num_leq ?x ?z = Btm, H2: num_leq ?y ?z = Btm |- context[num_leq ?x ?y]] =>
                 destruct (num_leq_both_leq_btm x y z H1 H2)
               | [H1 : num_leq ?z ?x = Btm, H2: num_leq ?z ?y = Btm |- context[num_leq ?x ?y]] =>
                 destruct (num_leq_leq_both_btm x y z H1 H2)
               | [H1 : num_leq ?x ?y = Top, H2: num_leq ?y ?z = Btm |- context[num_leq ?x ?z]] =>
                 let H := fresh "H" in destruct (num_leq_trans_top_btm _ _ _ H1 H2) as [H | H]; rewrite H
               | [H1 : num_leq ?x ?y = Btm, H2: num_leq ?y ?z = Top |- context[num_leq ?x ?z]] =>
                 let H := fresh "H" in destruct (num_leq_trans_btm_top _ _ _ H1 H2) as [H | H]; rewrite H
               | [H1 : num_leq ?x ?y = Top, H2: num_leq ?y ?z = Btm |- context[num_leq ?z ?x]] =>
                 destruct (num_leq_trans_top_btm _ _ _ H1 H2)
               | [H1 : num_leq ?x ?y = Btm, H2: num_leq ?y ?z = Top |- context[num_leq ?z ?x]] =>
                 destruct (num_leq_trans_btm_top _ _ _ H1 H2)
               | [H1 : num_leq ?x ?z = Btm, H2: num_leq ?y ?z = Top |- context[num_leq ?x ?y]] =>
                 destruct (num_leq_before_normal _ _ _ H1 H2)
               | [H1 : num_leq ?x ?z = Btm, H2: num_leq ?y ?z = Top |- context[num_leq ?y ?x]] =>
                 destruct (num_leq_before_normal _ _ _ H1 H2)
               | [H1 : num_leq ?z ?x = Btm, H2: num_leq ?z ?y = Top |- context[num_leq ?x ?y]] =>
                 destruct (num_leq_after_normal _ _ _ H1 H2)
               | [H1 : num_leq ?z ?x = Btm, H2: num_leq ?z ?y = Top |- context[num_leq ?y ?x]] =>
                 destruct (num_leq_after_normal _ _ _ H1 H2)
             end.

    Lemma eliminate_ok: forall z, (satisfied (ZF_BF z) <-> satisfied (eliminateMinMax z)) /\
                                  (dissatisfied (ZF_BF z) <-> dissatisfied (eliminateMinMax z)).

  End Simplification.

End ArithSemantics.