Library Transformation

Require Import Theory.
Require Import ZArith.
Require Import FunctionalExtensionality.
Require Import Omega.
Require Import Classical.

Import ZInfinity.

Module InfSolver (sv:VARIABLE) (VAL : SEM_VAL) (S: NONE_RELATION VAL) (FZT : ZERO_FIN) (IZT : ZERO_INF).
  Import sv.
  Import VAL.
  Import S.

  Module InfRel := InfLeqRelation VAL S.
  Module FinRel := FinLeqRelation VAL.

  Module IA := ArithSemantics PureInfinity sv VAL InfRel IZT.

  Module FA := ArithSemantics PureInt sv VAL FinRel FZT.

  Module I2F := ArithSemantics IntToInfinity sv VAL InfRel IZT.

  Section InfinityTransformation.

    Fixpoint inf_trans_exp (exp : IA.ZExp) : I2F.ZExp :=
      match exp with
          IA.ZExp_Var v => I2F.ZExp_Var v
        | IA.ZExp_Const a => I2F.ZExp_Const a
        | IA.ZExp_Add e1 e2 => I2F.ZExp_Add (inf_trans_exp e1) (inf_trans_exp e2)
        | IA.ZExp_Inv e => I2F.ZExp_Inv (inf_trans_exp e)
        | IA.ZExp_Sub e1 e2 => I2F.ZExp_Sub (inf_trans_exp e1) (inf_trans_exp e2)
        | IA.ZExp_Mult z e => I2F.ZExp_Mult z (inf_trans_exp e)
      end.

    Lemma inf_trans_exp_ok : forall exp, IA.dexp2ZE exp = I2F.dexp2ZE (inf_trans_exp exp).

    Definition inf_trans_bf (bf : IA.ZBF) : I2F.ZBF :=
      match bf with
          IA.ZBF_Const b => I2F.ZBF_Const b
        | IA.ZBF_Lt f1 f2 => I2F.ZBF_Lt (inf_trans_exp f1) (inf_trans_exp f2)
        | IA.ZBF_Lte f1 f2 => I2F.ZBF_Lte (inf_trans_exp f1) (inf_trans_exp f2)
        | IA.ZBF_Gt f1 f2 => I2F.ZBF_Gt (inf_trans_exp f1) (inf_trans_exp f2)
        | IA.ZBF_Gte f1 f2 => I2F.ZBF_Gte (inf_trans_exp f1) (inf_trans_exp f2)
        | IA.ZBF_Eq f1 f2 => I2F.ZBF_Eq (inf_trans_exp f1) (inf_trans_exp f2)
        | IA.ZBF_Eq_Max f1 f2 f3 => I2F.ZBF_Eq_Max (inf_trans_exp f1) (inf_trans_exp f2) (inf_trans_exp f3)
        | IA.ZBF_Eq_Min f1 f2 f3 => I2F.ZBF_Eq_Min (inf_trans_exp f1) (inf_trans_exp f2) (inf_trans_exp f3)
        | IA.ZBF_Neq f1 f2 => I2F.ZBF_Neq (inf_trans_exp f1) (inf_trans_exp f2)
      end.

    Lemma inf_trans_bf_ok : forall z, IA.satisfied (IA.ZF_BF z) <-> I2F.satisfied (I2F.ZF_BF (inf_trans_bf z)).

    Lemma inf_trans_bf_dst : forall z, IA.dissatisfied (IA.ZF_BF z) <-> I2F.dissatisfied (I2F.ZF_BF (inf_trans_bf z)).

    Definition inf_trans : IA.ZF -> I2F.ZF :=
      Fix IA.lengthOrder_wf (fun _ => I2F.ZF)
          (fun (form : IA.ZF) =>
             match form return ((forall f : IA.ZF, IA.lengthOrder f form -> I2F.ZF) -> I2F.ZF) with
                 IA.ZF_BF bf => fun _ => I2F.ZF_BF (inf_trans_bf bf)
               | IA.ZF_And f1 f2 => fun infTrans => I2F.ZF_And (infTrans f1 (IA.lengthOrder_and_1 f1 f2))
                                                               (infTrans f2 (IA.lengthOrder_and_2 f1 f2))
               | IA.ZF_Or f1 f2 => fun infTrans => I2F.ZF_Or (infTrans f1 (IA.lengthOrder_or_1 f1 f2))
                                                             (infTrans f2 (IA.lengthOrder_or_2 f1 f2))
               | IA.ZF_Imp f1 f2 => fun infTrans => I2F.ZF_Imp (infTrans f1 (IA.lengthOrder_imp_1 f1 f2))
                                                               (infTrans f2 (IA.lengthOrder_imp_2 f1 f2))
               | IA.ZF_Not f' => fun infTrans => I2F.ZF_Not (infTrans f' (IA.lengthOrder_not f'))
               | IA.ZF_Forall v q f' =>
                 match q with
                     PureInfinity.Q_Z =>
                     fun infTrans => I2F.ZF_Forall v tt (infTrans f' (IA.lengthOrder_forall_trivial f' v PureInfinity.Q_Z))
                   | PureInfinity.Q_ZE =>
                     fun infTrans =>
                       I2F.ZF_And (I2F.ZF_Forall v tt (infTrans f' (IA.lengthOrder_forall_trivial f' v PureInfinity.Q_ZE)))
                                  (I2F.ZF_And (infTrans (IA.substitute (v, Some ZE_Inf) f')
                                                        (IA.lengthOrder_forall f' v PureInfinity.Q_ZE ZE_Inf))
                                              (infTrans (IA.substitute (v, Some ZE_NegInf) f')
                                                        (IA.lengthOrder_forall f' v PureInfinity.Q_ZE ZE_NegInf)))
                 end
               | IA.ZF_Exists v q f' =>
                 match q with
                     PureInfinity.Q_Z =>
                     fun infTrans => I2F.ZF_Exists v tt (infTrans f' (IA.lengthOrder_exists_trivial f' v PureInfinity.Q_Z))
                   | PureInfinity.Q_ZE =>
                     fun infTrans =>
                       I2F.ZF_Or (I2F.ZF_Exists v tt (infTrans f' (IA.lengthOrder_exists_trivial f' v PureInfinity.Q_ZE)))
                                 (I2F.ZF_Or (infTrans (IA.substitute (v, Some ZE_Inf) f')
                                                      (IA.lengthOrder_exists f' v PureInfinity.Q_ZE ZE_Inf))
                                            (infTrans (IA.substitute (v, Some ZE_NegInf) f')
                                                      (IA.lengthOrder_exists f' v PureInfinity.Q_ZE ZE_NegInf)))
                 end
             end).

    Lemma inf_trans_unfold:
      forall form,
        inf_trans form =
        match form with
            IA.ZF_BF bf => I2F.ZF_BF (inf_trans_bf bf)
          | IA.ZF_And f1 f2 => I2F.ZF_And (inf_trans f1) (inf_trans f2)
          | IA.ZF_Or f1 f2 => I2F.ZF_Or (inf_trans f1) (inf_trans f2)
          | IA.ZF_Imp f1 f2 => I2F.ZF_Imp (inf_trans f1) (inf_trans f2)
          | IA.ZF_Not f => I2F.ZF_Not (inf_trans f)
          | IA.ZF_Forall v q f =>
            match q with
                PureInfinity.Q_Z => I2F.ZF_Forall v tt (inf_trans f)
              | PureInfinity.Q_ZE => I2F.ZF_And (I2F.ZF_Forall v tt (inf_trans f))
                                                (I2F.ZF_And (inf_trans (IA.substitute (v, Some ZE_Inf) f))
                                                            (inf_trans (IA.substitute (v, Some ZE_NegInf) f)))
            end
          | IA.ZF_Exists v q f =>
            match q with
                PureInfinity.Q_Z => I2F.ZF_Exists v tt (inf_trans f)
              | PureInfinity.Q_ZE => I2F.ZF_Or (I2F.ZF_Exists v tt (inf_trans f))
                                               (I2F.ZF_Or (inf_trans (IA.substitute (v, Some ZE_Inf) f))
                                                          (inf_trans (IA.substitute (v, Some ZE_NegInf) f)))
            end
        end.

    Lemma subst_inf_trans_exp_eq : forall z v (x : option ZE),
                                     I2F.subst_exp (v, x) (inf_trans_exp z) = inf_trans_exp (IA.subst_exp (v, x) z).

    Lemma subst_inf_trans_bf_eq : forall z v (x : option ZE),
                                    I2F.substitute (v, x) (inf_trans (IA.ZF_BF z)) =
                                    inf_trans (IA.substitute (v, x) (IA.ZF_BF z)).

    Ltac unfold_right_inf_trans :=
      match goal with
        | [|- _ = inf_trans ?X] => rewrite inf_trans_unfold with X; auto
      end.

    Lemma subst_inf_trans_eq: forall f v (x: option ZE), I2F.substitute (v, x) (inf_trans f) =
                                                         inf_trans (IA.substitute (v, x) f).

    Ltac solve_le_inv :=
      match goal with
        | [|- IA.length_zform (IA.substitute _ _) <= _] => rewrite <- IA.substitute_length_inv; auto
      end.

    Lemma inf_trans_ok : forall f, (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                   (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)).
      Ltac solve_inf_trans :=
        repeat match goal with
                 | [|- _ /\ _] => split
                 | [H: IA.length_zform (IA.ZF_Not _) <= S _ |- _] => simpl in H; apply le_S_n in H
                 | [H: IA.length_zform (IA.ZF_And _ _) <= S _ |- _] => simpl in H; apply le_S_n in H
                 | [H: IA.length_zform (IA.ZF_Or _ _) <= S _ |- _] => simpl in H; apply le_S_n in H
                 | [H: IA.length_zform (IA.ZF_Imp _ _) <= S _ |- _] => simpl in H; apply le_S_n in H
                 | [H: IA.length_zform (IA.ZF_Forall _ _ _) <= S _ |- _] => simpl in H; apply le_S_n in H
                 | [H: IA.length_zform (IA.ZF_Exists _ _ _) <= S _ |- _] => simpl in H; apply le_S_n in H
                 | [|- IA.satisfied (IA.ZF_BF ?z) <-> I2F.satisfied (inf_trans (IA.ZF_BF ?z))] =>
                   rewrite inf_trans_bf_ok; intuition
                 | [|- IA.dissatisfied (IA.ZF_BF ?z) <-> I2F.dissatisfied (inf_trans (IA.ZF_BF ?z))] =>
                   rewrite inf_trans_bf_dst; intuition
                 | [|- context[IA.satisfied (IA.ZF_And _ _)]] => rewrite IA.satisfied_unfold
                 | [|- context[IA.satisfied (IA.ZF_Or _ _)]] => rewrite IA.satisfied_unfold
                 | [|- context[IA.satisfied (IA.ZF_Imp _ _)]] => rewrite IA.satisfied_unfold
                 | [|- context[IA.satisfied (IA.ZF_Forall _ _ _)]] => rewrite IA.satisfied_unfold
                 | [|- context[IA.satisfied (IA.ZF_Exists _ _ _)]] => rewrite IA.satisfied_unfold
                 | [|- context[IA.satisfied (IA.ZF_Not _)]] => rewrite IA.satisfied_unfold
                 | [|- context[I2F.satisfied (I2F.ZF_And _ _)]] => rewrite I2F.satisfied_unfold
                 | [|- context[I2F.satisfied (I2F.ZF_Or _ _)]] => rewrite I2F.satisfied_unfold
                 | [|- context[I2F.satisfied (I2F.ZF_Imp _ _)]] => rewrite I2F.satisfied_unfold
                 | [|- context[I2F.satisfied (I2F.ZF_Forall _ _ _)]] => rewrite I2F.satisfied_unfold
                 | [|- context[I2F.satisfied (I2F.ZF_Exists _ _ _)]] => rewrite I2F.satisfied_unfold
                 | [|- context[I2F.satisfied (I2F.ZF_Not _)]] => rewrite I2F.satisfied_unfold
                 | [|- context[inf_trans(IA.ZF_Not _)]] => rewrite inf_trans_unfold
                 | [|- context[inf_trans(IA.ZF_And _ _)]] => rewrite inf_trans_unfold
                 | [|- context[inf_trans(IA.ZF_Or _ _)]] => rewrite inf_trans_unfold
                 | [|- context[inf_trans(IA.ZF_Imp _ _)]] => rewrite inf_trans_unfold
                 | [|- context[inf_trans(IA.ZF_Forall _ _ _)]] => rewrite inf_trans_unfold
                 | [|- context[inf_trans(IA.ZF_Exists _ _ _)]] => rewrite inf_trans_unfold
                 | [|- context[IA.dissatisfied (IA.ZF_And _ _)]] => rewrite IA.dissatisfied_unfold
                 | [|- context[IA.dissatisfied (IA.ZF_Or _ _)]] => rewrite IA.dissatisfied_unfold
                 | [|- context[IA.dissatisfied (IA.ZF_Imp _ _)]] => rewrite IA.dissatisfied_unfold
                 | [|- context[IA.dissatisfied (IA.ZF_Forall _ _ _)]] => rewrite IA.dissatisfied_unfold
                 | [|- context[IA.dissatisfied (IA.ZF_Exists _ _ _)]] => rewrite IA.dissatisfied_unfold
                 | [|- context[IA.dissatisfied (IA.ZF_Not _)]] => rewrite IA.dissatisfied_unfold
                 | [|- context[I2F.dissatisfied (I2F.ZF_And _ _)]] => rewrite I2F.dissatisfied_unfold
                 | [|- context[I2F.dissatisfied (I2F.ZF_Or _ _)]] => rewrite I2F.dissatisfied_unfold
                 | [|- context[I2F.dissatisfied (I2F.ZF_Imp _ _)]] => rewrite I2F.dissatisfied_unfold
                 | [|- context[I2F.dissatisfied (I2F.ZF_Forall _ _ _)]] => rewrite I2F.dissatisfied_unfold
                 | [|- context[I2F.dissatisfied (I2F.ZF_Exists _ _ _)]] => rewrite I2F.dissatisfied_unfold
                 | [|- context[I2F.dissatisfied (I2F.ZF_Not _)]] => rewrite I2F.dissatisfied_unfold
                 | [q : PureInfinity.Q |- _] => destruct q

                 | [|- _ <-> _] => split; intros
                 | [H: _ /\ _ |- _] => destruct H
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : IA.satisfied ?f1 |- I2F.satisfied (inf_trans ?f1)] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f1 <= n) by omega; destruct (IHn _ S) as [S1 S2]; apply S1,H0
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : IA.satisfied ?f2 |- I2F.satisfied (inf_trans ?f2)] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f2 <= n) by omega; destruct (IHn _ S) as [S1 S2]; apply S1,H0
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : I2F.satisfied (inf_trans ?f2) |- IA.satisfied ?f2] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f2 <= n) by omega; destruct (IHn _ S) as [S1 S2]; rewrite S1; apply H0
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : I2F.satisfied (inf_trans ?f1) |- IA.satisfied ?f1] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f1 <= n) by omega; destruct (IHn _ S) as [S1 S2]; rewrite S1; apply H0
                 | [H: _ \/ _ |- _] => destruct H
                 | [H0 : IA.satisfied ?f1, H1 : IA.satisfied ?f2 |-
                    I2F.satisfied (inf_trans ?f1) /\ I2F.satisfied (inf_trans ?f2) \/ _] => left
                 | [H0 : IA.dissatisfied ?f1, H1 : IA.satisfied ?f2 |-
                    I2F.satisfied (inf_trans ?f1) /\ I2F.satisfied (inf_trans ?f2) \/ _] => right
                 | [H0 : IA.dissatisfied ?f1, H1 : IA.satisfied ?f2 |-
                    I2F.dissatisfied (inf_trans ?f1) /\ I2F.satisfied (inf_trans ?f2) \/ _] => left
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : IA.dissatisfied ?f1 |- I2F.dissatisfied (inf_trans ?f1)] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f1 <= n) by omega; destruct (IHn _ S) as [S1 S2]; apply S2,H0
                 | [H0 : IA.satisfied ?f1, H1 : IA.dissatisfied ?f2 |-
                    I2F.satisfied (inf_trans ?f1) /\ I2F.satisfied (inf_trans ?f2) \/ _] => right
                 | [H0 : IA.satisfied ?f1, H1 : IA.dissatisfied ?f2 |-
                    _ \/ I2F.satisfied (inf_trans ?f1) /\ I2F.dissatisfied (inf_trans ?f2)] => right
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : IA.dissatisfied ?f2 |- I2F.dissatisfied (inf_trans ?f2)] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f2 <= n) by omega; destruct (IHn _ S) as [S1 S2]; apply S2,H0
                 |[H0 : I2F.satisfied (inf_trans ?f1), H1 : I2F.satisfied (inf_trans ?f2)
                   |- IA.satisfied ?f1 /\ IA.satisfied ?f2 \/ _] => left
                 |[H0 : I2F.dissatisfied (inf_trans ?f1), H1 : I2F.satisfied (inf_trans ?f2)
                   |- IA.satisfied ?f1 /\ IA.satisfied ?f2 \/ _] => right
                 |[H0 : I2F.dissatisfied (inf_trans ?f1), H1 : I2F.satisfied (inf_trans ?f2)
                   |- IA.dissatisfied ?f1 /\ IA.satisfied ?f2 \/ _] => left
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : I2F.dissatisfied (inf_trans ?f1) |- IA.dissatisfied ?f1] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f1 <= n) by omega; destruct (IHn _ S) as [S1 S2]; rewrite S2; apply H0
                 |[H0 : I2F.satisfied (inf_trans ?f1), H1 : I2F.dissatisfied (inf_trans ?f2)
                   |- IA.satisfied ?f1 /\ IA.satisfied ?f2 \/ _] => right
                 |[H0 : I2F.satisfied (inf_trans ?f1), H1 : I2F.dissatisfied (inf_trans ?f2)
                   |- _ \/ IA.satisfied ?f1 /\ IA.dissatisfied ?f2] => right
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f1 + IA.length_zform ?f2 <= ?n,
                     H0 : I2F.dissatisfied (inf_trans ?f2) |- IA.dissatisfied ?f2] =>
                  let S := fresh "S" in
                  let S1 := fresh "S1" in
                  let S2 := fresh "S2" in
                  assert (S : IA.length_zform f2 <= n) by omega; destruct (IHn _ S) as [S1 S2]; rewrite S2; apply H0
                 |[H0 : IA.dissatisfied ?f1 |- I2F.dissatisfied (inf_trans ?f1) \/ _] => left
                 |[H0 : IA.dissatisfied ?f1 |- _ \/ I2F.dissatisfied (inf_trans ?f1)] => right
                 |[H0 : IA.satisfied ?f1 |- _ \/ I2F.satisfied (inf_trans ?f1)] => right
                 |[H0 : I2F.dissatisfied (inf_trans ?f1) |- IA.dissatisfied ?f1 \/ _] => left
                 |[H0 : I2F.satisfied (inf_trans ?f1) |- _ \/ IA.satisfied ?f1] => right
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f <= ?n, H0 : IA.dissatisfied ?f |- I2F.dissatisfied (inf_trans ?f)]
                  => let S1 := fresh "S1" in let S2 := fresh "S2" in destruct (IHn _ H) as [S1 S2]; apply S2, H0
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f <= ?n, H0 : I2F.dissatisfied (inf_trans ?f) |- IA.dissatisfied ?f]
                  => let S1 := fresh "S1" in let S2 := fresh "S2" in destruct (IHn _ H) as [S1 S2]; rewrite S2; apply H0
                 |[|- forall _, _] => intro
                 |[|- context[I2F.substitute (_, _) (inf_trans _)]] => rewrite subst_inf_trans_eq
                 | [H0 : IA.dissatisfied ?f1, H1 : IA.dissatisfied ?f2 |-
                    I2F.dissatisfied (inf_trans ?f1) /\ I2F.dissatisfied (inf_trans ?f2) \/ _] => left
                 | [H0 : IA.dissatisfied ?f1, H1 : IA.dissatisfied ?f2 |-
                    I2F.satisfied (inf_trans ?f1) /\ I2F.satisfied (inf_trans ?f2) \/ _] => right
                 | [H0 : IA.dissatisfied ?f1, H1 : IA.dissatisfied ?f2 |-
                    _ \/ I2F.dissatisfied (inf_trans ?f1) /\ I2F.dissatisfied (inf_trans ?f2)] => right
                 | [H0 : IA.satisfied ?f1, H1 : IA.dissatisfied ?f2 |-
                    I2F.dissatisfied (inf_trans ?f1) /\ I2F.dissatisfied (inf_trans ?f2) \/ _] => right
                 | [H0 : IA.satisfied ?f1, H1 : IA.dissatisfied ?f2 |-
                    I2F.satisfied (inf_trans ?f1) /\ I2F.dissatisfied (inf_trans ?f2) \/ _] => left
                 | [H0 : IA.dissatisfied ?f1, H1 : IA.satisfied ?f2 |-
                    I2F.dissatisfied (inf_trans ?f1) /\ I2F.dissatisfied (inf_trans ?f2) \/ _] => right
                 | [H0 : IA.dissatisfied ?f1, H1 : IA.satisfied ?f2 |-
                    _ \/ I2F.dissatisfied (inf_trans ?f1) /\ I2F.satisfied (inf_trans ?f2)] => right
                 |[H0 : I2F.dissatisfied (inf_trans ?f1), H1 : I2F.dissatisfied (inf_trans ?f2)
                   |- IA.dissatisfied ?f1 /\ IA.dissatisfied ?f2 \/ _] => left
                 |[H0 : I2F.dissatisfied (inf_trans ?f1), H1 : I2F.dissatisfied (inf_trans ?f2)
                   |- IA.satisfied ?f1 /\ IA.satisfied ?f2 \/ _] => right
                 |[H0 : I2F.dissatisfied (inf_trans ?f1), H1 : I2F.dissatisfied (inf_trans ?f2)
                   |- _ \/ IA.dissatisfied ?f1 /\ IA.dissatisfied ?f2] => right
                 |[H0 : I2F.satisfied (inf_trans ?f1), H1 : I2F.dissatisfied (inf_trans ?f2)
                   |- IA.dissatisfied ?f1 /\ IA.dissatisfied ?f2 \/ _] => right
                 |[H0 : I2F.satisfied (inf_trans ?f1), H1 : I2F.dissatisfied (inf_trans ?f2)
                   |- IA.satisfied ?f1 /\ IA.dissatisfied ?f2 \/ _] => left
                 |[H0 : I2F.dissatisfied (inf_trans ?f1), H1 : I2F.satisfied (inf_trans ?f2)
                   |- IA.dissatisfied ?f1 /\ IA.dissatisfied ?f2 \/ _] => right
                 |[H0 : I2F.dissatisfied (inf_trans ?f1), H1 : I2F.satisfied (inf_trans ?f2)
                   |- _ \/ IA.dissatisfied ?f1 /\ IA.satisfied ?f2] => right
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f <= ?n, H0 : IA.satisfied ?f |- I2F.satisfied (inf_trans ?f)]
                  => let S1 := fresh "S1" in let S2 := fresh "S2" in destruct (IHn _ H) as [S1 S2]; apply S1, H0
                 |[IHn : forall f : IA.ZF, IA.length_zform f <= ?n ->
                                           (IA.satisfied f <-> I2F.satisfied (inf_trans f)) /\
                                           (IA.dissatisfied f <-> I2F.dissatisfied (inf_trans f)),
                     H : IA.length_zform ?f <= ?n, H0 : I2F.satisfied (inf_trans ?f) |- IA.satisfied ?f]
                  => let S1 := fresh "S1" in let S2 := fresh "S2" in destruct (IHn _ H) as [S1 S2]; rewrite S1; apply H0
               end.
      Ltac assertLn IHn :=
        match goal with
          | [n : nat |- context[IA.substitute (?v, IntToInfinity.conv ?x) ?f]] =>
            let S := fresh "S" in
            let S1 := fresh "S1" in
            let S2 := fresh "S2" in
            assert (S : IA.length_zform (IA.substitute (v, @IntToInfinity.conv tt x) f) <= n) by solve_le_inv;
              destruct (IHn _ S) as [S1 S2]
          | [n : nat |- context[IA.substitute (?v, PureInfinity.conv ?x) ?f]] =>
            let S := fresh "S" in
            let S1 := fresh "S1" in
            let S2 := fresh "S2" in
            assert (S : IA.length_zform (IA.substitute (v, PureInfinity.conv x) f) <= n) by solve_le_inv;
              destruct (IHn _ S) as [S1 S2]
          | [n : nat |- context[IA.substitute (?v, PureInfinity.conv ?x) ?f]] =>
            let S := fresh "S" in
            let S1 := fresh "S1" in
            let S2 := fresh "S2" in
            assert (S : IA.length_zform (IA.substitute (v, @PureInfinity.conv PureInfinity.Q_Z x) f) <= n) by solve_le_inv;
              destruct (IHn _ S) as [S1 S2]
          | [n : nat |- context[IA.substitute (?v, Some ?x) ?f]] =>
            let S := fresh "S" in
            let S1 := fresh "S1" in
            let S2 := fresh "S2" in
            assert (S : IA.length_zform (IA.substitute (v, Some x) f) <= n) by solve_le_inv;
              destruct (IHn _ S) as [S1 S2]
          | [n : nat |- context[IA.substitute (?v, PureInfinity.conv (PureInfinity.N.ZE_Fin ?z)) ?f]] =>
            let S := fresh "S" in
            let S1 := fresh "S1" in
            let S2 := fresh "S2" in
            assert (S : IA.length_zform
                          (IA.substitute (v, @PureInfinity.conv PureInfinity.Q_ZE (PureInfinity.N.ZE_Fin z)) f) <= n)
              by solve_le_inv;
              destruct (IHn _ S) as [S1 S2]
          | [n : nat |- context[IA.substitute (?v, PureInfinity.conv ?x) ?f]] =>
            let S := fresh "S" in
            let S1 := fresh "S1" in
            let S2 := fresh "S2" in
            assert (S : IA.length_zform (IA.substitute (v, @PureInfinity.conv PureInfinity.Q_ZE x) f) <= n) by solve_le_inv;
              destruct (IHn _ S) as [S1 S2]
        end.

  End InfinityTransformation.

  Section IntegerTransformation.

    Definition embed (v : Val) := FA.ZF_BF (FA.ZBF_Const v).
    Definition FATrue := embed Top.
    Definition FAFalse := embed Btm.
    Definition FANone := embed noneVal.

    Definition proj (z : IntToInfinity.N.A) : Z :=
      match z with
          Some (ZE_Fin x) => x
        | _ => 0%Z
      end.

    Fixpoint int_trans_exp (exp : I2F.ZExp) : FA.ZExp :=
      match exp with
          I2F.ZExp_Var v => FA.ZExp_Var v
        | I2F.ZExp_Const a => FA.ZExp_Const (proj a)
        | I2F.ZExp_Add e1 e2 => FA.ZExp_Add (int_trans_exp e1) (int_trans_exp e2)
        | I2F.ZExp_Inv e => FA.ZExp_Inv (int_trans_exp e)
        | I2F.ZExp_Sub e1 e2 => FA.ZExp_Sub (int_trans_exp e1) (int_trans_exp e2)
        | I2F.ZExp_Mult z e => FA.ZExp_Mult z (int_trans_exp e)
      end.

    Definition int_trans_bf (bf : I2F.ZBF) : FA.ZF :=
      match bf with
          I2F.ZBF_Const f => FA.ZF_BF (FA.ZBF_Const f)
        | I2F.ZBF_Lt e1 e2 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2) with
              None, _
            | _, None => FANone
            | Some ZE_NegInf, Some x => if ZE_eq_dec x ZE_NegInf then FAFalse else FATrue
            | Some x, Some ZE_Inf => if ZE_eq_dec x ZE_Inf then FAFalse else FATrue
            | Some _, Some ZE_NegInf => FAFalse
            | Some ZE_Inf, Some _ => FAFalse
            | Some (ZE_Fin _), Some (ZE_Fin _) => FA.ZF_BF (FA.ZBF_Lt (int_trans_exp e1) (int_trans_exp e2))
          end
        | I2F.ZBF_Lte e1 e2 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2) with
              None, _
            | _, None => FANone
            | Some _, Some ZE_Inf => FATrue
            | Some ZE_NegInf, Some _ => FATrue
            | Some ZE_Inf, Some x => if ZE_eq_dec x ZE_Inf then FATrue else FAFalse
            | Some x, Some ZE_NegInf => if ZE_eq_dec x ZE_NegInf then FATrue else FAFalse
            | Some (ZE_Fin _), Some (ZE_Fin _) => FA.ZF_BF (FA.ZBF_Lte (int_trans_exp e1) (int_trans_exp e2))
          end
        | I2F.ZBF_Gt e1 e2 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2) with
              None, _
            | _, None => FANone
            | Some ZE_Inf, Some x => if ZE_eq_dec x ZE_Inf then FAFalse else FATrue
            | Some x, Some ZE_NegInf => if ZE_eq_dec x ZE_NegInf then FAFalse else FATrue
            | Some _, Some ZE_Inf => FAFalse
            | Some ZE_NegInf, Some _ => FAFalse
            | Some (ZE_Fin _), Some (ZE_Fin _) => FA.ZF_BF (FA.ZBF_Gt (int_trans_exp e1) (int_trans_exp e2))
          end
        | I2F.ZBF_Gte e1 e2 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2) with
              None, _
            | _, None => FANone
            | Some _, Some ZE_NegInf => FATrue
            | Some ZE_Inf, Some _ => FATrue
            | Some ZE_NegInf, Some x => if ZE_eq_dec x ZE_NegInf then FATrue else FAFalse
            | Some x, Some ZE_Inf => if ZE_eq_dec x ZE_Inf then FATrue else FAFalse
            | Some (ZE_Fin _), Some (ZE_Fin _) => FA.ZF_BF (FA.ZBF_Gte (int_trans_exp e1) (int_trans_exp e2))
          end
        | I2F.ZBF_Eq e1 e2 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2) with
              None, _
            | _, None => FANone
            | Some ZE_NegInf, Some x
            | Some x, Some ZE_NegInf => if ZE_eq_dec x ZE_NegInf then FATrue else FAFalse
            | Some ZE_Inf, Some x
            | Some x, Some ZE_Inf => if ZE_eq_dec x ZE_Inf then FATrue else FAFalse
            | Some (ZE_Fin _), Some (ZE_Fin _) => FA.ZF_BF (FA.ZBF_Eq (int_trans_exp e1) (int_trans_exp e2))
          end
        | I2F.ZBF_Eq_Max e1 e2 e3 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2), (I2F.dexp2ZE e3) with
              None, _, _
            | _, None, _
            | _, _, None => FANone
            | Some ZE_NegInf, Some x, Some y =>
              if (ZE_eq_dec x ZE_NegInf)
              then if (ZE_eq_dec y ZE_NegInf)
                   then FATrue
                   else FAFalse
              else FAFalse
            | Some ZE_Inf, Some x, Some y =>
              if ZE_eq_dec x ZE_Inf
              then FATrue
              else if ZE_eq_dec y ZE_Inf
                   then FATrue
                   else FAFalse
            | Some (ZE_Fin _), Some ZE_NegInf, Some y =>
              match y with
                  ZE_NegInf
                | ZE_Inf => FAFalse
                | _ => FA.ZF_BF (FA.ZBF_Eq (int_trans_exp e1) (int_trans_exp e3))
              end
            | Some (ZE_Fin _), Some y, Some ZE_NegInf =>
              match y with
                  ZE_NegInf
                | ZE_Inf => FAFalse
                | _ => FA.ZF_BF (FA.ZBF_Eq (int_trans_exp e1) (int_trans_exp e2))
              end
            | Some (ZE_Fin _), Some ZE_Inf, Some y
            | Some (ZE_Fin _), Some y, Some ZE_Inf => FAFalse
            | Some (ZE_Fin _), Some (ZE_Fin _), Some(ZE_Fin _) =>
              FA.ZF_BF (FA.ZBF_Eq_Max (int_trans_exp e1) (int_trans_exp e2) (int_trans_exp e3))
          end
        | I2F.ZBF_Eq_Min e1 e2 e3 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2), (I2F.dexp2ZE e3) with
              None, _, _
            | _, None, _
            | _, _, None => FANone
            | Some ZE_NegInf, Some x, Some y =>
              if ZE_eq_dec x ZE_NegInf
              then FATrue
              else if ZE_eq_dec y ZE_NegInf
                   then FATrue
                   else FAFalse
            | Some ZE_Inf, Some x, Some y =>
              if (ZE_eq_dec x ZE_Inf)
              then if (ZE_eq_dec y ZE_Inf)
                   then FATrue
                   else FAFalse
              else FAFalse
            | Some (ZE_Fin _), Some ZE_NegInf, Some y
            | Some (ZE_Fin _), Some y, Some ZE_NegInf => FAFalse
            | Some (ZE_Fin _), Some ZE_Inf, Some y =>
              match y with
                  ZE_Inf
                | ZE_NegInf => FAFalse
                | _ => FA.ZF_BF (FA.ZBF_Eq (int_trans_exp e1) (int_trans_exp e3))
              end
            | Some (ZE_Fin _), Some y, Some ZE_Inf =>
              match y with
                  ZE_Inf
                | ZE_NegInf => FAFalse
                | _ => FA.ZF_BF (FA.ZBF_Eq (int_trans_exp e1) (int_trans_exp e2))
              end
            | Some (ZE_Fin _), Some (ZE_Fin _), Some(ZE_Fin _) =>
              FA.ZF_BF (FA.ZBF_Eq_Min (int_trans_exp e1) (int_trans_exp e2) (int_trans_exp e3))
          end
        | I2F.ZBF_Neq e1 e2 =>
          match (I2F.dexp2ZE e1), (I2F.dexp2ZE e2) with
              None, _
            | _, None => embed (truth_not noneVal)
            | Some ZE_NegInf, Some x
            | Some x, Some ZE_NegInf => if ZE_eq_dec x ZE_NegInf then FAFalse else FATrue
            | Some ZE_Inf, Some x
            | Some x, Some ZE_Inf => if ZE_eq_dec x ZE_Inf then FAFalse else FATrue
            | Some (ZE_Fin _), Some (ZE_Fin _) => FA.ZF_BF (FA.ZBF_Neq (int_trans_exp e1) (int_trans_exp e2))
          end
      end.

    Ltac solve_b :=
      repeat match goal with
               |[H: Some (ZE_Fin _) = Some (ZE_Fin _) |- _] => injection H; intro; clear H
               |[H: ?X = ?Y |- ?Y = ?X] => rewrite H; trivial
               |[H: context[match ?v with _ => _ end] |- _] => destruct v
               |[H: None = Some _ |- _] => discriminate H
               |[H: Some _ = None |- _] => discriminate H
               |[H: Some ZE_Inf = Some (ZE_Fin _) |- _] => discriminate H
               |[H: Some ZE_NegInf = Some (ZE_Fin _) |- _] => discriminate H
               |[H: Some (ZE_Fin _) = Some ZE_Inf |- _] => discriminate H
               |[H: Some (ZE_Fin _) = Some ZE_NegInf |- _] => discriminate H
               |[H: Some ZE_NegInf = Some ZE_Inf |- _] => discriminate H
               |[H: Some ZE_Inf = Some ZE_NegInf |- _] => discriminate H
             end.

    Lemma nat_nummult_finite: forall c v x,
                                I2F.num_mult_nat c v = Some (IntToInfinity.N.ZE_Fin x)
                                -> ((c = 0 /\ x = 0%Z) \/ (exists n, v = Some (ZE_Fin n) /\ FA.num_mult_nat c n = x)).

    Lemma nummult_finite: forall c v x, I2F.num_mult c v = Some (IntToInfinity.N.ZE_Fin x)
                                        -> (c = 0%Z /\ x = 0%Z) \/
                                           (exists n, v = Some (ZE_Fin n) /\ FA.num_mult c n = x).

    Lemma dexp2ZE_int_trans_eq: forall z x, I2F.dexp2ZE z = Some (IntToInfinity.N.ZE_Fin x) -> FA.dexp2ZE (int_trans_exp z) = x.

    Ltac smash_int_trans_bf :=
      repeat match goal with
               | [|- context[FinRel.num_leq _ _]] => unfold FinRel.num_leq
               | [ H: FANone = _ |- _] => unfold FANone in H; unfold embed in H; inversion H; simpl
               | [|- context[truth_not Btm]] => rewrite tautology_1
               | [|- context[truth_not Top]] => rewrite tautology_2
               | [|- context[truth_and ?X ?X]] => rewrite tautology_3
               | [|- context[truth_and Top Btm]] => rewrite tautology_4
               | [|- context[truth_and Btm Top]] => rewrite (truth_and_comm Btm Top), tautology_4
               | [|- context[truth_or ?X ?X]] => rewrite tautology_5
               | [|- context[truth_or Top Btm]] => rewrite tautology_6
               | [|- context[truth_or Btm Top]] => rewrite (truth_or_comm Btm Top), tautology_6
               | [|- context[truth_and noneVal (truth_not noneVal)]] => rewrite none_tautology_1
               | [|- context[truth_and noneVal Top]] => rewrite none_tautology_2
               | [|- context[truth_and Top noneVal]] => rewrite (truth_and_comm Top noneVal), none_tautology_2
               | [|- context[truth_or (truth_and noneVal Btm) noneVal]] => rewrite none_tautology_3
               | [|- context[truth_or noneVal Btm]] => rewrite none_tautology_4
               | [|- context[truth_or Btm noneVal]] => rewrite truth_or_comm, none_tautology_4
               | [H: I2F.dexp2ZE ?z = Some (IntToInfinity.N.ZE_Fin ?x) |- context[FA.dexp2ZE (int_trans_exp ?z)]]
=> rewrite (dexp2ZE_int_trans_eq z x)
               | [|- ?X <-> ?X] => tauto
               | [H: ?X |- ?X] => apply H
               | [|- context[match (I2F.dexp2ZE ?X) with _ => _ end]] => destruct (I2F.dexp2ZE X) eqn: ?; simpl
               | [|- context[match ?X with _ => _ end]] => destruct X eqn: ?; simpl
               | [H: context[match ?X with _ => _ end] |- _] => destruct X eqn: ?; simpl
               | [|- context[InfRel.num_leq _ _]] => unfold InfRel.num_leq
               | [_: (?a <= ?b)%Z, _: ~ (?a <= ?b)%Z |- _] => contradiction
               | [_: ~ (?a <= ?b)%Z, _: ~ (?b <= ?a)%Z |- _] => exfalso; intuition
               | [|- context[truth_and Top noneVal]] => rewrite truth_and_comm, none_tautology_2
               | [|- context[truth_or noneVal (truth_and noneVal Btm)]] => rewrite truth_or_comm, none_tautology_3
               | [|- context[truth_or noneVal (truth_and Btm noneVal)]] =>
                 rewrite truth_or_comm, truth_and_comm, none_tautology_3
               | [|- context[truth_or (truth_and Btm noneVal) noneVal]] => rewrite truth_and_comm, none_tautology_3
             end.

    Lemma int_trans_bf_sat: forall bf, I2F.satisfied (I2F.ZF_BF bf) <-> FA.satisfied (int_trans_bf bf).

    Lemma int_trans_bf_dst: forall bf, I2F.dissatisfied (I2F.ZF_BF bf) <-> FA.dissatisfied (int_trans_bf bf).

    Fixpoint int_trans (form : I2F.ZF) : FA.ZF :=
      match form with
          I2F.ZF_BF bf => int_trans_bf bf
        | I2F.ZF_And f1 f2 => FA.ZF_And (int_trans f1) (int_trans f2)
        | I2F.ZF_Or f1 f2 => FA.ZF_Or (int_trans f1) (int_trans f2)
        | I2F.ZF_Imp f1 f2 => FA.ZF_Imp (int_trans f1) (int_trans f2)
        | I2F.ZF_Not f => FA.ZF_Not (int_trans f)
        | I2F.ZF_Forall v q f => FA.ZF_Forall v q (int_trans f)
        | I2F.ZF_Exists v q f => FA.ZF_Exists v q (int_trans f)
      end.

    Lemma nat_nummult_eq: forall z x, I2F.num_mult_nat z (Some (ZE_Fin x)) = Some (ZE_Fin (FA.num_mult_nat z x)).

    Lemma nummult_eq: forall z x, I2F.num_mult z (Some (ZE_Fin x)) = Some (ZE_Fin (FA.num_mult z x)).

    Lemma finite_subst2finite: forall z v x c1, I2F.dexp2ZE z = Some (ZE_Fin c1) ->
                                                (exists c2, I2F.dexp2ZE (I2F.subst_exp (v, @IntToInfinity.conv tt x) z) =
                                                            Some (ZE_Fin c2)).

    Lemma nat_nummult_inf:
      forall z v, I2F.num_mult_nat z v = Some ZE_Inf ->
                  (z > 0 /\ v = Some ZE_Inf) \/
                  (z = 0 /\ v = Some ZE_Inf /\
                   (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end)).

    Lemma nat_nummult_neginf:
      forall z v, I2F.num_mult_nat z v = Some ZE_NegInf ->
                  (z > 0 /\ v = Some ZE_NegInf) \/
                  (z = 0 /\ v = Some ZE_NegInf /\
                   (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end)).

    Lemma nummult_inf:
      forall z v, I2F.num_mult z v = Some ZE_Inf ->
                  (((z > 0)%Z /\ v = Some ZE_Inf) \/
                   ((z < 0)%Z /\ v = Some ZE_NegInf) \/
                   ((z = 0)%Z /\ v = Some ZE_Inf /\
                    (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end))).

    Lemma nummult_neginf:
      forall z v, I2F.num_mult z v = Some ZE_NegInf ->
                  (((z > 0)%Z /\ v = Some ZE_NegInf) \/
                   ((z < 0)%Z /\ v = Some ZE_Inf) \/
                   ((z = 0)%Z /\ v = Some ZE_NegInf /\
                    (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end))).

    Ltac solve_mul2inf p IHp:= induction p; auto; rewrite I2F.num_mult_nat_2_unfold in *; rewrite IHp; auto.

    Lemma num_mult_nat_inf: forall p, I2F.num_mult_nat (S p) (Some ZE_Inf) = Some ZE_Inf.

    Lemma num_mult_nat_neginf: forall p, I2F.num_mult_nat (S p) (Some ZE_NegInf) = Some ZE_NegInf.

    Ltac solve_tonat_infnone p l:= simpl; assert (exists pp, Pos.to_nat p = S pp) as SSS by
                                         (exists (pred (Pos.to_nat p)); apply (S_pred (Pos.to_nat p) 0); apply Pos2Nat.is_pos);
                                   destruct SSS as [pr S1]; rewrite S1; rewrite l; auto.

    Lemma inf_subst2inf:
      forall z v x,
        I2F.dexp2ZE z = Some ZE_Inf -> I2F.dexp2ZE (I2F.subst_exp (v, @IntToInfinity.conv tt x) z) = Some ZE_Inf
        with neginf_subst2neginf: forall z v x, I2F.dexp2ZE z = Some ZE_NegInf ->
                                                I2F.dexp2ZE (I2F.subst_exp (v, @IntToInfinity.conv tt x) z) = Some ZE_NegInf.

    Lemma nat_nummult_none:
      forall z v, I2F.num_mult_nat z v = None ->
                  (z <> 0 /\ v = None) \/
                  (z = 0 /\ (v = Some ZE_Inf \/ v = Some ZE_NegInf \/ v = None) /\
                   (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => None end)) \/
                  (z = 0 /\ v = None /\
                   (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end)).

    Lemma nummult_none:
      forall z v, I2F.num_mult z v = None ->
                  ((z <> 0)%Z /\ v = None) \/
                  (z = 0%Z /\ (v = Some ZE_Inf \/ v = Some ZE_NegInf \/ v = None) /\
                   (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => None end)) \/
                  (z = 0%Z /\ v = None /\
                   (forall x, IZT.zero_times x = match x with | Some (ZE_Fin _) => Some (ZE_Fin 0) | _ => x end)).

    Lemma num_mult_nat_none: forall p, I2F.num_mult_nat (S p) None = None.

    Lemma none_subst2none: forall z v x, I2F.dexp2ZE z = None ->
                                         I2F.dexp2ZE (I2F.subst_exp (v, @IntToInfinity.conv tt x) z) = None.

    Lemma subst_int_trans_exp_eq: forall z v x, FA.subst_exp (v, @PureInt.conv tt x) (int_trans_exp z) =
                                                int_trans_exp (I2F.subst_exp (v, @IntToInfinity.conv tt x) z).

    Ltac smash_subst_int_trans_bf_eq :=
      repeat match goal with
               | [|- ?X = ?X] => apply eq_refl
               | [H1 : I2F.dexp2ZE ?z = None, H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z) = Some _ |- _] =>
                 apply (none_subst2none z v x) in H1; rewrite H1 in H2; discriminate H2
               | [H1 : I2F.dexp2ZE ?zExp = Some ?zSome,
                       H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?zExp) = None |- _] =>
                 destruct zSome; [apply (finite_subst2finite zExp v x) in H1; destruct H1 as [? H1] |
                                  apply (inf_subst2inf zExp v x) in H1 | apply (neginf_subst2neginf zExp v x) in H1];
                 rewrite H1 in H2; discriminate H2
               |[H1 : I2F.dexp2ZE ?z = Some (IntToInfinity.N.ZE_Fin _),
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z) = Some IntToInfinity.N.ZE_Inf |- _] =>
                apply (finite_subst2finite z v x) in H1; destruct H1 as [? H1]; rewrite H1 in H2; discriminate H2
               |[H1 : I2F.dexp2ZE ?z = Some (IntToInfinity.N.ZE_Fin _),
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z) = Some IntToInfinity.N.ZE_NegInf |- _] =>
                apply (finite_subst2finite z v x) in H1; destruct H1 as [? H1]; rewrite H1 in H2; discriminate H2
               |[H1 : I2F.dexp2ZE ?z = Some IntToInfinity.N.ZE_Inf,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z) = Some (IntToInfinity.N.ZE_Fin _) |- _] =>
                apply (inf_subst2inf z v x) in H1; rewrite H1 in H2; discriminate H2
               |[H1 : I2F.dexp2ZE ?z = Some IntToInfinity.N.ZE_Inf,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z) = Some IntToInfinity.N.ZE_NegInf |- _] =>
                apply (inf_subst2inf z v x) in H1; rewrite H1 in H2; discriminate H2
               |[H1 : I2F.dexp2ZE ?z = Some IntToInfinity.N.ZE_NegInf,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z) = Some (IntToInfinity.N.ZE_Fin _) |- _] =>
                apply (neginf_subst2neginf z v x) in H1; rewrite H1 in H2; discriminate H2
               |[H1 : I2F.dexp2ZE ?z = Some IntToInfinity.N.ZE_NegInf,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z) = Some IntToInfinity.N.ZE_Inf |- _] =>
                apply (neginf_subst2neginf z v x) in H1; rewrite H1 in H2; discriminate H2
               |[H1 : I2F.dexp2ZE ?z1 = Some ?z2,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z1) = Some ?z3,
                           H3 : ?z2 = ZE_NegInf, H4 : ?z3 <> ZE_NegInf |- _] =>
                let H := fresh "H" in
                rewrite H3 in H1; apply (neginf_subst2neginf z1 v x) in H1; rewrite H1 in H2;
                injection H2; intro H; rewrite H in H4; exfalso; apply H4, eq_refl
               |[H1 : I2F.dexp2ZE ?z1 = Some ?z2,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z1) = Some ?z3,
                           H3 : ?z2 = ZE_Inf, H4 : ?z3 <> ZE_Inf |- _] =>
                let H := fresh "H" in
                rewrite H3 in H1; apply (inf_subst2inf z1 v x) in H1; rewrite H1 in H2;
                injection H2; intro H; rewrite H in H4; exfalso; apply H4, eq_refl
               |[H1 : I2F.dexp2ZE ?z1 = Some ?z2,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z1) = Some ?z3,
                           H3 : ?z2 <> ZE_NegInf, H4 : ?z3 = ZE_NegInf|- _] =>
                rewrite H4 in H2; destruct z2;
                [apply (finite_subst2finite z1 v x) in H1; destruct H1 as [? H1]; rewrite H1 in H2; discriminate H2 |
                 apply (inf_subst2inf z1 v x) in H1; rewrite H1 in H2; discriminate H2 | exfalso; apply H3, eq_refl]
               |[H1 : I2F.dexp2ZE ?z1 = Some ?z2,
                      H2 : I2F.dexp2ZE (I2F.subst_exp (?v, IntToInfinity.conv ?x) ?z1) = Some ?z3,
                           H3 : ?z2 <> ZE_Inf, H4 : ?z3 = ZE_Inf|- _] =>
                rewrite H4 in H2; destruct z2;
                [apply (finite_subst2finite z1 v x) in H1; destruct H1 as [? H1]; rewrite H1 in H2; discriminate H2 |
                 exfalso; apply H3, eq_refl | apply (neginf_subst2neginf z1 v x) in H1; rewrite H1 in H2; discriminate H2 ]
               | [H: context[ZE_eq_dec _ _] |- _] => clear H
               | [|- context[FAFalse]] => unfold FAFalse
               | [|- context[FATrue]] => unfold FATrue
               | [|- context[match I2F.dexp2ZE ?X with _ => _ end]] => destruct (I2F.dexp2ZE X) eqn: ?; simpl
               | [|- context[match ?X with _ => _ end]] => destruct X eqn: ?; simpl
               | [|- context[FA.subst_exp (_, PureInt.conv _) (int_trans_exp _)]] => rewrite subst_int_trans_exp_eq
               | [|- context[embed _]] => unfold embed
               | [|- context[FANone]] => unfold FANone
             end.

    Lemma subst_int_trans_bf_eq: forall z v x, FA.substitute (v, @PureInt.conv tt x) (int_trans (I2F.ZF_BF z)) =
                                               int_trans (I2F.substitute (v, @IntToInfinity.conv tt x) (I2F.ZF_BF z)).

    Lemma subst_int_trans_eq: forall f v x, FA.substitute (v, @PureInt.conv tt x) (int_trans f) =
                                            int_trans (I2F.substitute (v, @IntToInfinity.conv tt x) f).

    Lemma int_trans_ok: forall f, (I2F.satisfied f <-> FA.satisfied (int_trans f)) /\
                                  (I2F.dissatisfied f <-> FA.dissatisfied (int_trans f)).
      Ltac smalltrick :=
        repeat match goal with
                 | [|- _ /\ _ ] => split
                 | [H: _ /\ _ |- _] => destruct H
                 | [|- _ <-> _] => split
                 | [|- _ -> _] => intros
                 | [H: exists _, _ |- _] => let x := fresh "x" in destruct H as [x ?]
               end.

  End IntegerTransformation.

  Definition T (f : IA.ZF) : FA.ZF := int_trans (inf_trans f).

  Theorem valid_eq: forall f, (IA.satisfied f <-> FA.satisfied (T f)) /\
                              (IA.dissatisfied f <-> FA.dissatisfied (T f)).

End InfSolver.

Module ThreeValuedSimp (sv:VARIABLE) (FZT : ZERO_FIN) (IZT : ZERO_INF).
  Module InfS := InfSolver sv Three_Val_NoneError NoneError3ValRel FZT IZT.
  Import Three_Val_NoneError InfS.FA.

  Inductive SimpResult (f : ZF) :=
  | EQ_TRUE : f = ZF_BF (ZBF_Const VTrue) -> SimpResult f
  | EQ_FALSE : f = ZF_BF (ZBF_Const VFalse) -> SimpResult f
  | EQ_ERROR : f = ZF_BF (ZBF_Const VError) -> SimpResult f
  | OTHER : f <> ZF_BF (ZBF_Const VTrue) /\ f <> ZF_BF (ZBF_Const VFalse) /\ f <> ZF_BF (ZBF_Const VError) -> SimpResult f.

  Definition judge (f : ZF) : SimpResult f.
  Defined.

  Fixpoint simplify (form : ZF) : ZF :=
    match form with
      | ZF_BF bf => eliminateMinMax bf
      | ZF_And f1 f2 => match (simplify f1), (simplify f2) with
                            e1, e2 => match (judge e1), (judge e2) with
                                        | EQ_ERROR _, _
                                        | _, EQ_ERROR _ => ZF_BF (ZBF_Const VError)
                                        | EQ_FALSE _, _
                                        | _, EQ_FALSE _ => ZF_BF (ZBF_Const VFalse)
                                        | EQ_TRUE _, _ => e2
                                        | _, EQ_TRUE _ => e1
                                        | _, _ => ZF_And e1 e2
                                      end end
      | ZF_Or f1 f2 => match (simplify f1), (simplify f2) with
                           e1, e2 => match (judge e1), (judge e2) with
                                       | EQ_ERROR _, _
                                       | _, EQ_ERROR _ => ZF_BF (ZBF_Const VError)
                                       | EQ_TRUE _, _
                                       | _, EQ_TRUE _ => ZF_BF (ZBF_Const VTrue)
                                       | EQ_FALSE _, _ => e2
                                       | _, EQ_FALSE _ => e1
                                       | _, _ => ZF_Or e1 e2
                                     end end
      | ZF_Imp f1 f2 => match (simplify f1), (simplify f2) with
                            e1, e2 => match (judge e1), (judge e2) with
                                        | EQ_ERROR _, _
                                        | _, EQ_ERROR _ => ZF_BF (ZBF_Const VError)
                                        | EQ_FALSE _, _
                                        | _, EQ_TRUE _ => ZF_BF (ZBF_Const VTrue)
                                        | EQ_TRUE _, _ => e2
                                        | _, EQ_FALSE _ => ZF_Not e1
                                        | _, _ => ZF_Imp e1 e2
                                      end end
      | ZF_Not f => match (simplify f) with
                        e => match (judge e) with
                               | EQ_ERROR _ => ZF_BF (ZBF_Const VError)
                               | EQ_FALSE _ => ZF_BF (ZBF_Const VTrue)
                               | EQ_TRUE _ => ZF_BF (ZBF_Const VFalse)
                               | _ => ZF_Not e
                             end end
      | ZF_Forall v q f => match (simplify f) with
                               e => match (judge e) with
                                      | EQ_ERROR _ => ZF_BF (ZBF_Const VError)
                                      | EQ_FALSE _ => ZF_BF (ZBF_Const VFalse)
                                      | EQ_TRUE _ => ZF_BF (ZBF_Const VTrue)
                                      | _ => ZF_Forall v q e
                                    end end
      | ZF_Exists v q f => match (simplify f) with
                               e => match (judge e) with
                                      | EQ_ERROR _ => ZF_BF (ZBF_Const VError)
                                      | EQ_FALSE _ => ZF_BF (ZBF_Const VFalse)
                                      | EQ_TRUE _ => ZF_BF (ZBF_Const VTrue)
                                      | _ => ZF_Exists v q e
                                    end end
    end.

End ThreeValuedSimp.