# Lift Quantifiers

Require Export Form.

Inductive prenex : form Prop :=
| pExists : a : form, prenex a prenex (Exists a)
| pForall : a : form, prenex a prenex (Forall a)
| pNoBinder : a : form, noBinder a prenex a.
Hint Constructors prenex.

# Lift If

• ((x:?)(P x) Q) gives (Ex [x:?] ((P x) Q)) )
• (Ex [x:?](P x) Q) gives (x:?) ((P x) Q) )
• Q->(x:?)(P x) gives (x:?) Q (P x)
• Q->(Ex[x:?](P x) gives (Ex [x:?] Q->(P x)
Fixpoint lift_if1 (n m : nat) (f1 f2 : form) {struct f2} : form :=
match f2 with
| Forall bForall (lift_if1 n (S m) f1 b)
| Exists bExists (lift_if1 n (S m) f1 b)
| _Imp (shiftForm n m m f1) (shiftForm m 0 n f2)
end.

Fixpoint lift_if2 (n : nat) (f1 : form) {struct f1} :
form form :=
fun f2 : form
match f1 with
| Forall bExists (lift_if2 (S n) b f2)
| Exists bForall (lift_if2 (S n) b f2)
| _lift_if1 n 0 f1 f2
end.

Definition lift_if (f1 f2 : form) := lift_if2 0 f1 f2.

Theorem noBinder_shift :
(f : form) (th i o : nat),
noBinder f noBinder (shiftForm th i o f).
intros f th i o H; generalize th i o; elim H; simpl in |- *; auto.
Qed.
Hint Resolve noBinder_shift.

Theorem lift_if1_noBinder :
(n m : nat) (f1 f2 : form),
noBinder f2
lift_if1 n m f1 f2 = Imp (shiftForm n m m f1) (shiftForm m 0 n f2).
intros n m f1 f2 H; elim H; simpl in |- *; auto.
Qed.

Theorem lift_if1_prenex :
(n m : nat) (f1 f2 : form),
noBinder f1 prenex f2 prenex (lift_if1 n m f1 f2).
intros n m f1 f2 H1 H2; generalize n m; elim H2; simpl in |- *; auto.
intros a H3; elim H3; simpl in |- *; auto.
Qed.
Hint Resolve lift_if1_prenex.
Require Import GroundN.
Require Import ArithRing.
Require Import Max.

Theorem lift_if1_groundN :
f1 f2 n m p,
prenex f2
noBinder f1
groundNForm (p + n) f1
groundNForm (p + m) f2 groundNForm (p + (m + n)) (lift_if1 n m f1 f2).
intros f1 f2 n m p H H1; generalize m p; elim H; clear H m p;
unfold lift_if1 in |- *; lazy beta in |- *; fold lift_if1 in |- *;
auto.
intros a H H0 m p H2 H3.
apply GNExists; auto.
replace (S (p + (m + n))) with (p + (S m + n)).
apply H0; auto.
replace (p + S m) with (S (p + m)).
inversion H3; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
intros a H H0 m p H2 H3.
apply GNForall; auto.
replace (S (p + (m + n))) with (p + (S m + n)).
apply H0; auto.
replace (p + S m) with (S (p + m)).
inversion H3; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
intros a H; elim H; unfold lift_if1 in |- *; lazy beta in |- *;
fold lift_if1 in |- *; auto; intros;
apply GNImp with (n := p + (m + n)) (m := p + (m + n));
auto with arith;
try
(replace (p + (m + n)) with (max (n + m) (p + n + m));
[ apply shiftForm_groundN; auto
| replace (p + (m + n)) with (p + n + m); auto with arith; ring ]);
try
(replace (p + (m + n)) with (max (m + 0) (p + m + n));
[ apply shiftForm_groundN; auto; replace (p + (m + n)) with (m + (p + n));
auto with arith
| ring_simplify; rewrite plus_comm; auto with arith]);
try (replace (p + m + n) with (m + (n + p)); auto with arith; try ring).
Qed.

Theorem lift_if2_prenex :
(n : nat) (f1 f2 : form),
prenex f1 prenex f2 prenex (lift_if2 n f1 f2).
intros n f1 f2 H; generalize n f2; elim H; simpl in |- *; clear n f2 H; auto.
intros a H; elim H; clear H a; simpl in |- *; auto.
Qed.
Hint Resolve lift_if2_prenex.

Theorem lift_if2_groundN :
f1 f2 n p,
prenex f1
prenex f2
groundNForm (p + n) f1
groundNForm p f2 groundNForm (p + n) (lift_if2 n f1 f2).
intros f1 f2 n p H H1; generalize n p; elim H; clear H n p;
unfold lift_if2 in |- *; lazy beta in |- *; fold lift_if2 in |- ×.
intros a H0 H2 n p H3 H4.
apply GNForall; auto.
replace (S (p + n)) with (p + S n); auto with arith.
apply H2; auto.
replace (p + S n) with (S (p + n)); auto with arith.
inversion H3; auto.
intros a H0 H2 n p H3 H4.
apply GNExists; auto.
replace (S (p + n)) with (p + S n); auto with arith.
apply H2; auto.
replace (p + S n) with (S (p + n)); auto with arith.
inversion H3; auto.
intros a H; elim H; unfold lift_if2 in |- *; lazy beta in |- *;
fold lift_if2 in |- *; auto; intros; replace (p + n) with (p + (0 + n));
try apply lift_if1_groundN; auto with arith; rewrite plus_comm;
simpl in |- *; auto.
Qed.

Theorem lift_if_prenex :
f1 f2 : form, prenex f1 prenex f2 prenex (lift_if f1 f2).
intros; unfold lift_if in |- *; auto.
Qed.
Hint Resolve lift_if_prenex.

Theorem lift_if_groundN :
f1 f2 p,
prenex f1
prenex f2
groundNForm p f1 groundNForm p f2 groundNForm p (lift_if f1 f2).
intros f1 f2 p H H0 H1 H2; unfold lift_if in |- ×.
replace p with (p + 0); auto with arith.
apply lift_if2_groundN; auto with arith; rewrite plus_comm; simpl in |- *;
auto with arith.
Qed.

Definition iso_list (th i o : nat) (l1 l2 : list Z) :=
n : nat,
(n < th nth n l1 0%Z = nth (n + i) l2 0%Z)
(th n nth n l1 0%Z = nth (n + o) l2 0%Z).

Theorem iso_shiftExp :
(l1 l2 : list Z) (th i o : nat),
iso_list th i o l1 l2
e : exp, exp2Z l1 e = exp2Z l2 (shiftExp th i o e).
intros l1 l2 th i o H e; elim e; simpl in |- *; auto.
intros n; generalize (H n); generalize (ltdec_correct n th);
case (ltdec n th); intros H1 H2; case H2; auto.
intros e0 H0 e1 H1; rewrite H0; rewrite H1; auto.
Qed.
Hint Resolve iso_shiftExp.

Theorem iso_shiftForm :
(th i o : nat) (l1 l2 : list Z),
iso_list th i o l1 l2
f : form,
noBinder f (form2Prop l1 f form2Prop l2 (shiftForm th i o f)).
intros th i o l1 l2 H f H0; elim H0; simpl in |- *; auto; intros;
repeat rewrite <- (iso_shiftExp l1); intuition; auto.
Qed.

Definition iso_list3 (n m : nat) (l1 l2 l3 : list Z) :=
p : nat,
((p < m nth p l3 0%Z = nth p l2 0%Z)
(m p nth (p + n) l3 0%Z = nth p l2 0%Z))
nth (p + m) l3 0%Z = nth p l1 0%Z.

Theorem iso_iso3_1 :
l1 l2 l3 n m, iso_list3 n m l1 l2 l3 iso_list n m m l1 l3.
intros l1 l2 l3 n m H; red in |- *; intros p.
case (H p); intros H0 H1; intuition.
Qed.

Theorem iso_iso3_2 :
l1 l2 l3 n m, iso_list3 n m l1 l2 l3 iso_list m 0 n l2 l3.
intros l1 l2 l3 n m H; red in |- *; intros p.
case (H p); intros H0 H1; rewrite plus_comm; simpl in |- *; intuition.
Qed.

Theorem iso3_1 :
(n m : nat) (x : Z) l1 l2 l3,
iso_list3 n m l1 l2 l3 iso_list3 n (S m) l1 (x :: l2) (x :: l3).
intros n m x l1 l2 l3 H; red in |- *; intros p; repeat split; try intros H1.
generalize H1; clear H1; case p; simpl in |- *; auto.
intros p' H1.
cut (p' < m); [ intros H2 | apply lt_S_n; auto ].
case (H p'); intros (H3, H4) H5; auto.
generalize H1; clear H1; case p; simpl in |- *; auto.
intros H1; inversion H1.
intros p' H1.
cut (m p'); [ intros H2 | apply le_S_n; auto ].
case (H p'); intros (H3, H4) H5; auto.
replace (p + S m) with (S (p + m)); simpl in |- *; [ idtac | auto ].
case (H p); intros (H3, H4) H5; auto.
Qed.
Hint Resolve iso3_1.

Theorem iso_lift_i1 :
f1 f2 : form,
noBinder f1
prenex f2
(n m : nat) (l1 l2 l3 : list Z),
iso_list3 n m l1 l2 l3
((form2Prop l1 f1 form2Prop l2 f2) form2Prop l3 (lift_if1 n m f1 f2)).
intros f1 f2 H H0; elim H0.
simpl in |- *; intros a H1 H2 n m l1 l2 l3 H3; split.
intros H4.
case (classic (form2Prop l1 f1)); intros H5.
case (H4 H5); clear H4; intros x H4; x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
0%Z.
case (H2 n (S m) l1 (0%Z :: l2) (0%Z :: l3)); auto.
intros H6 H7; apply H6; auto.
intros H8; case H5; auto.
intros H4 H5; case H4; clear H4; intros x H4; x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
simpl in |- *; intros a H1 H2 n m l1 l2 l3 H3; split.
intros H4 x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros H4 H5 x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros a H1 n m l1 l2 l3 H2.
rewrite lift_if1_noBinder; simpl in |- *; auto.
case (iso_shiftForm n m m l1 l3) with (f := f1); auto.
apply iso_iso3_1 with (l2 := l2); auto.
case (iso_shiftForm m 0 n l2 l3) with (f := a); auto.
apply iso_iso3_2 with (l1 := l1); auto.
intuition.
Qed.

Theorem iso3_2 :
(n : nat) (x : Z) l1 l2 l3,
iso_list3 n 0 l1 l2 l3 iso_list3 (S n) 0 (x :: l1) l2 (x :: l3).
intros n x l1 l2 l3 H; red in |- *; intros p; repeat split; try intros H1.
inversion H1.
replace (p + S n) with (S (p + n));
[ simpl in |- × | repeat rewrite (plus_comm p); simpl in |- *; auto ].
case (H p); intros (H2, H3) H4; auto.
case p; simpl in |- *; auto.
intros p'; case (H p'); intros (H1, H2) H3; auto.
Qed.
Hint Resolve iso3_2.

Theorem iso_lift_i2 :
f1 f2 : form,
prenex f1
prenex f2
(n : nat) (l1 l2 l3 : list Z),
iso_list3 n 0 l1 l2 l3
((form2Prop l1 f1 form2Prop l2 f2) form2Prop l3 (lift_if2 n f1 f2)).
intros f1 f2 H H1; elim H; clear H; simpl in |- *; auto.
intros a H H0 n l1 l2 l3 H2; split.
intros H3 x.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H4 H5; auto.
apply H4; auto.
intros H6; apply H3; x; auto.
intros H3 H4; case H4; clear H4; intros x H4.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros a H H0 n l1 l2 l3 H2; split.
intros H3.
case (classic ( x : Z, form2Prop (x :: l1) a)); intros H4.
0%Z.
case (H0 (S n) (0%Z :: l1) l2 (0%Z :: l3)); auto.
case (classic (ex (fun x : Zform2Prop (x :: l3) (lift_if2 (S n) a f2))));
intros H5; auto.
elim H4; intros x.
case (classic (form2Prop (x :: l1) a)); intros H6; auto.
case H5; x.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H7 H8; apply H7; intros H9; case H6; auto.
intros H3 H4; case H3; clear H3; intros x H3.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros a H; elim H; clear H; unfold lift_if2 in |- *; intros;
apply iso_lift_i1; auto.
Qed.

Theorem correct_lift_if :
f1 f2 : form,
prenex f1
prenex f2
l : list Z,
(form2Prop l f1 form2Prop l f2) form2Prop l (lift_if f1 f2).
intros f1 f2 H H0 l; unfold lift_if in |- *; apply iso_lift_i2; auto.
red in |- *; repeat split; (repeat rewrite (plus_comm p); simpl in |- *);
auto.
Qed.

# Lift And

• ((x:?)(P x) Q) gives (x:?) ((P x) Q)) )
• (Ex [x:?](P x) Q) gives (Ex [x:?] ((P x) Q) )
• Q/\(x:?)(P x) gives (x:?) Q (P x)
• Q/\(Ex[x:?](P x) gives (Ex [x:?] Q/\(P x)

Fixpoint lift_andor1 (op : form form form) (n m : nat)
(f1 f2 : form) {struct f2} : form :=
match f2 with
| Forall bForall (lift_andor1 op n (S m) f1 b)
| Exists bExists (lift_andor1 op n (S m) f1 b)
| _op (shiftForm n m m f1) (shiftForm m 0 n f2)
end.

Fixpoint lift_andor2 (op : form form form) (n : nat)
(f1 : form) {struct f1} : form form :=
fun f2 : form
match f1 with
| Forall bForall (lift_andor2 op (S n) b f2)
| Exists bExists (lift_andor2 op (S n) b f2)
| _lift_andor1 op n 0 f1 f2
end.

Definition lift_andor (op : form form form) (f1 f2 : form) :=
lift_andor2 op 0 f1 f2.

Theorem lift_andor1_noBinder :
op (n m : nat) (f1 f2 : form),
noBinder f2
lift_andor1 op n m f1 f2 = op (shiftForm n m m f1) (shiftForm m 0 n f2).
intros op n m f1 f2 H; elim H; simpl in |- *; auto.
Qed.

Theorem lift_andor1_prenex :
op,
( f1 f2, noBinder f1 noBinder f2 noBinder (op f1 f2))
(n m : nat) (f1 f2 : form),
noBinder f1 prenex f2 prenex (lift_andor1 op n m f1 f2).
intros op H n m f1 f2 H1 H2; generalize n m; elim H2; simpl in |- *; auto.
intros a H3; elim H3; simpl in |- *; auto.
Qed.
Hint Resolve lift_andor1_prenex.

Theorem lift_andor2_prenex :
op,
( f1 f2, noBinder f1 noBinder f2 noBinder (op f1 f2))
(n : nat) (f1 f2 : form),
prenex f1 prenex f2 prenex (lift_andor2 op n f1 f2).
intros op Rec n f1 f2 H; generalize n f2; elim H; simpl in |- *; clear n f2 H;
auto.
intros a H; elim H; clear H a; simpl in |- *; auto.
Qed.
Hint Resolve lift_andor2_prenex.

Theorem lift_andor_prenex :
op,
( f1 f2, noBinder f1 noBinder f2 noBinder (op f1 f2))
f1 f2 : form, prenex f1 prenex f2 prenex (lift_andor op f1 f2).
intros; unfold lift_andor in |- *; auto.
Qed.
Hint Resolve lift_andor_prenex.

Theorem lift_andor1_and_groundN :
f1 f2 n m p,
prenex f2
noBinder f1
groundNForm (p + n) f1
groundNForm (p + m) f2
groundNForm (p + (m + n)) (lift_andor1 ANd n m f1 f2).
intros f1 f2 n m p H H1; generalize m p; elim H; clear H m p;
unfold lift_andor1 in |- *; lazy beta in |- *; fold lift_andor1 in |- *;
auto.
intros a H H0 m p H2 H3.
apply GNExists; auto.
replace (S (p + (m + n))) with (p + (S m + n)).
apply H0; auto.
replace (p + S m) with (S (p + m)).
inversion H3; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
intros a H H0 m p H2 H3.
apply GNForall; auto.
replace (S (p + (m + n))) with (p + (S m + n)).
apply H0; auto.
replace (p + S m) with (S (p + m)).
inversion H3; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
intros a H; elim H; unfold lift_andor1 in |- *; lazy beta in |- *;
fold lift_andor1 in |- *; auto; intros;
apply GNAnd with (n := p + (m + n)) (m := p + (m + n));
auto with arith;
try
(replace (p + (m + n)) with (max (n + m) (p + n + m));
[ apply shiftForm_groundN; auto
| replace (p + (m + n)) with (p + n + m); auto with arith; ring ]);
try
(replace (p + (m + n)) with (max (m + 0) (p + m + n));
[ apply shiftForm_groundN; auto; replace (p + (m + n)) with (m + (p + n));
auto with arith
| ring_simplify; rewrite plus_comm; auto with arith ]);
try (replace (p + m + n) with (m + (n + p)); auto with arith; try ring).
Qed.

Theorem lift_andor1_or_groundN :
f1 f2 n m p,
prenex f2
noBinder f1
groundNForm (p + n) f1
groundNForm (p + m) f2
groundNForm (p + (m + n)) (lift_andor1 Or n m f1 f2).
intros f1 f2 n m p H H1; generalize m p; elim H; clear H m p;
unfold lift_andor1 in |- *; lazy beta in |- *; fold lift_andor1 in |- *;
auto.
intros a H H0 m p H2 H3.
apply GNExists; auto.
replace (S (p + (m + n))) with (p + (S m + n)).
apply H0; auto.
replace (p + S m) with (S (p + m)).
inversion H3; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
intros a H H0 m p H2 H3.
apply GNForall; auto.
replace (S (p + (m + n))) with (p + (S m + n)).
apply H0; auto.
replace (p + S m) with (S (p + m)).
inversion H3; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
repeat rewrite (plus_comm p); simpl in |- *; auto.
intros a H; elim H; unfold lift_andor1 in |- *; lazy beta in |- *;
fold lift_andor1 in |- *; auto; intros;
apply GNOr with (n := p + (m + n)) (m := p + (m + n));
auto with arith;
try
(replace (p + (m + n)) with (max (n + m) (p + n + m));
[ apply shiftForm_groundN; auto
| replace (p + (m + n)) with (p + n + m); auto with arith; ring ]);
try
(replace (p + (m + n)) with (max (m + 0) (p + m + n));
[ apply shiftForm_groundN; auto; replace (p + (m + n)) with (m + (p + n));
auto with arith
| ring_simplify; rewrite plus_comm; auto with arith ]);
try (replace (p + m + n) with (m + (n + p)); auto with arith; try ring).
Qed.

Theorem lift_andor2_and_groundN :
f1 f2 n p,
prenex f1
prenex f2
groundNForm (p + n) f1
groundNForm p f2 groundNForm (p + n) (lift_andor2 ANd n f1 f2).
intros f1 f2 n p H H1; generalize n p; elim H; clear H n p;
unfold lift_andor2 in |- *; lazy beta in |- *; fold lift_andor2 in |- ×.
intros a H0 H2 n p H3 H4.
apply GNExists; auto.
replace (S (p + n)) with (p + S n); auto with arith.
apply H2; auto.
replace (p + S n) with (S (p + n)); auto with arith.
inversion H3; auto.
intros a H0 H2 n p H3 H4.
apply GNForall; auto.
replace (S (p + n)) with (p + S n); auto with arith.
apply H2; auto.
replace (p + S n) with (S (p + n)); auto with arith.
inversion H3; auto.
intros a H; elim H; unfold lift_andor2 in |- *; lazy beta in |- *;
fold lift_andor2 in |- *; auto; intros; replace (p + n) with (p + (0 + n));
try apply lift_andor1_and_groundN; auto with arith;
rewrite plus_comm; simpl in |- *; auto.
Qed.

Theorem lift_andor2_or_groundN :
f1 f2 n p,
prenex f1
prenex f2
groundNForm (p + n) f1
groundNForm p f2 groundNForm (p + n) (lift_andor2 Or n f1 f2).
intros f1 f2 n p H H1; generalize n p; elim H; clear H n p;
unfold lift_andor2 in |- *; lazy beta in |- *; fold lift_andor2 in |- ×.
intros a H0 H2 n p H3 H4.
apply GNExists; auto.
replace (S (p + n)) with (p + S n); auto with arith.
apply H2; auto.
replace (p + S n) with (S (p + n)); auto with arith.
inversion H3; auto.
intros a H0 H2 n p H3 H4.
apply GNForall; auto.
replace (S (p + n)) with (p + S n); auto with arith.
apply H2; auto.
replace (p + S n) with (S (p + n)); auto with arith.
inversion H3; auto.
intros a H; elim H; unfold lift_andor2 in |- *; lazy beta in |- *;
fold lift_andor2 in |- *; auto; intros; replace (p + n) with (p + (0 + n));
try apply lift_andor1_or_groundN; auto with arith;
rewrite plus_comm; simpl in |- *; auto.
Qed.

Theorem lift_andor_and_groundN :
f1 f2 p,
prenex f1
prenex f2
groundNForm p f1 groundNForm p f2 groundNForm p (lift_andor ANd f1 f2).
intros f1 f2 p H H0 H1 H2; unfold lift_andor in |- ×.
replace p with (p + 0); auto with arith.
apply lift_andor2_and_groundN; auto with arith; rewrite plus_comm;
simpl in |- *; auto with arith.
Qed.

Theorem lift_andor_or_groundN :
f1 f2 p,
prenex f1
prenex f2
groundNForm p f1 groundNForm p f2 groundNForm p (lift_andor Or f1 f2).
intros f1 f2 p H H0 H1 H2; unfold lift_andor in |- ×.
replace p with (p + 0); auto with arith.
apply lift_andor2_or_groundN; auto with arith; rewrite plus_comm;
simpl in |- *; auto with arith.
Qed.

Theorem iso_lift_andor_and1 :
f1 f2 : form,
noBinder f1
prenex f2
(n m : nat) (l1 l2 l3 : list Z),
iso_list3 n m l1 l2 l3
(form2Prop l1 f1 form2Prop l2 f2
form2Prop l3 (lift_andor1 ANd n m f1 f2)).
intros f1 f2 H H0; elim H0.
simpl in |- *; intros a H1 H2 n m l1 l2 l3 H3; split.
intros (H4, (x, H5)); x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros (x, H4).
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros H5 H6; (split; [ idtac | x ]); case H6; auto.
simpl in |- *; intros a H1 H2 n m l1 l2 l3 H3; split.
intros (H4, H5) x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros H4; split.
case (H2 n (S m) l1 (0%Z :: l2) (0%Z :: l3)); auto.
intros H5 H6; case H6; auto.
intros x; case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros H5 H6; case H6; auto.
intros a H1 n m l1 l2 l3 H2.
rewrite lift_andor1_noBinder; simpl in |- *; auto.
case (iso_shiftForm n m m l1 l3) with (f := f1); auto.
apply iso_iso3_1 with (l2 := l2); auto.
case (iso_shiftForm m 0 n l2 l3) with (f := a); auto.
apply iso_iso3_2 with (l1 := l1); auto.
intuition.
Qed.

Theorem iso_lift_andor_or1 :
f1 f2 : form,
noBinder f1
prenex f2
(n m : nat) (l1 l2 l3 : list Z),
iso_list3 n m l1 l2 l3
(form2Prop l1 f1 form2Prop l2 f2
form2Prop l3 (lift_andor1 Or n m f1 f2)).
intros f1 f2 H H0; elim H0.
simpl in |- *; intros a H1 H2 n m l1 l2 l3 H3; split.
intros [H4| (x, H4)].
case (H2 n (S m) l1 (0%Z :: l2) (0%Z :: l3)); auto.
intros H5 H6; 0%Z; auto.
x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros (x, H4).
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros H5 H6; case H6; auto; intros H7.
right; x; auto.
simpl in |- *; intros a H1 H2 n m l1 l2 l3 H3; split.
intros [H4| H4] x; case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros H4; case (classic (form2Prop l1 f1)); intros H5; auto.
right; intros x.
case (H2 n (S m) l1 (x :: l2) (x :: l3)); auto.
intros H6 H7; case H7; auto.
intros H8; case H5; auto.
intros a H1 n m l1 l2 l3 H2.
rewrite lift_andor1_noBinder; simpl in |- *; auto.
case (iso_shiftForm n m m l1 l3) with (f := f1); auto.
apply iso_iso3_1 with (l2 := l2); auto.
case (iso_shiftForm m 0 n l2 l3) with (f := a); auto.
apply iso_iso3_2 with (l1 := l1); auto.
intuition.
Qed.

Theorem iso_lift_andor_and2 :
f1 f2 : form,
prenex f1
prenex f2
(n : nat) (l1 l2 l3 : list Z),
iso_list3 n 0 l1 l2 l3
(form2Prop l1 f1 form2Prop l2 f2
form2Prop l3 (lift_andor2 ANd n f1 f2)).
intros f1 f2 H H1; elim H; clear H; simpl in |- *; auto.
intros a H H0 n l1 l2 l3 H2; split.
intros ((x, H3), H4); x.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros (x, H3); split; [ x | idtac ].
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H4 H5; case H5; auto.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H4 H5; case H5; auto.
intros a H H0 n l1 l2 l3 H2; split.
intros (H3, H4) x.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H3; (split; [ intros | idtac ]).
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H4 H5; case H5; auto.
case (H0 (S n) (0%Z :: l1) l2 (0%Z :: l3)); auto.
intros H4 H5; case H5; auto.
intros a H; elim H; clear H; unfold lift_andor2 in |- *; intros;
apply iso_lift_andor_and1; auto.
Qed.

Theorem iso_lift_andor_or2 :
f1 f2 : form,
prenex f1
prenex f2
(n : nat) (l1 l2 l3 : list Z),
iso_list3 n 0 l1 l2 l3
(form2Prop l1 f1 form2Prop l2 f2
form2Prop l3 (lift_andor2 Or n f1 f2)).
intros f1 f2 H H1; elim H; clear H; simpl in |- *; auto.
intros a H H0 n l1 l2 l3 H2; split.
intros [(x, H3)| H4]; [ x | 0%Z ].
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
case (H0 (S n) (0%Z :: l1) l2 (0%Z :: l3)); auto.
intros (x, H3).
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H4 H5; case H5; auto.
intros H6; left; x; auto.
intros a H H0 n l1 l2 l3 H2; split.
intros [H3| H3] x; case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H3; case (classic (form2Prop l2 f2)); auto; left; intros x.
case (H0 (S n) (x :: l1) l2 (x :: l3)); auto.
intros H5 H6; case H6; auto.
intros H7; case H4; auto.
intros a H; elim H; clear H; unfold lift_andor2 in |- *; intros;
apply iso_lift_andor_or1; auto.
Qed.

Theorem correct_lift_andor_and :
f1 f2 : form,
prenex f1
prenex f2
l : list Z,
form2Prop l f1 form2Prop l f2 form2Prop l (lift_andor ANd f1 f2).
intros f1 f2 H H0 l; unfold lift_andor in |- *; apply iso_lift_andor_and2;
auto.
red in |- *; repeat split; (repeat rewrite (plus_comm p); simpl in |- *);
auto.
Qed.

Theorem correct_lift_andor_or :
f1 f2 : form,
prenex f1
prenex f2
l : list Z,
form2Prop l f1 form2Prop l f2 form2Prop l (lift_andor Or f1 f2).
intros f1 f2 H H0 l; unfold lift_andor in |- *; apply iso_lift_andor_or2;
auto.
red in |- *; repeat split; (repeat rewrite (plus_comm p); simpl in |- *);
auto.
Qed.

# Lift Neg

• ~((x:?)(P x)) gives (Ex [x:?] ~(P x))
• ~([x:?](P x)) gives (x:?) ~(P x)

Fixpoint lift_neg (f : form) : form :=
match f with
| Forall bExists (lift_neg b)
| Exists bForall (lift_neg b)
| bNeg b
end.

Theorem lift_neg_prenex : f : form, prenex f prenex (lift_neg f).
intros f H; elim H; simpl in |- *; auto.
intros a H1; elim H1; simpl in |- *; auto.
Qed.
Hint Resolve lift_neg_prenex.

Theorem lift_neg_groundN :
f p, prenex f groundNForm p f groundNForm p (lift_neg f).
intros f p H; generalize p; elim H; clear H p; unfold lift_neg in |- *;
lazy beta in |- *; fold lift_neg in |- ×.
intros a H H0 p H1; inversion H1; auto.
intros a H H0 p H1; inversion H1; auto.
intros a H; elim H; simpl in |- *; auto.
Qed.

Theorem correct_lift_neg :
f : form,
prenex f l : list Z, ¬ form2Prop l f form2Prop l (lift_neg f).
intros f H; elim H; simpl in |- *; auto.
intros a H0 H1 l; split.
intros H2 x.
case (H1 (x :: l)); auto.
intros H3 H4; apply H3; auto; red in |- *; intros; case H2; x; auto.
intros H2; red in |- *; intros (x, H3).
case (H1 (x :: l)); auto.
intros H4 H5; apply H5; auto.
intros a H0 H1 l; split.
intros H2; case (classic (ex (fun x : Zform2Prop (x :: l) (lift_neg a))));
intros H3; auto.
elim H2; intros x.
case (classic (form2Prop (x :: l) a)); intros H4; auto.
case H3; x.
case (H1 (x :: l)); auto.
intros (x, H2); red in |- *; intros H3.
case (H1 (x :: l)); auto.
intros H4 H5; apply H5; auto.
intros a H1; elim H1; simpl in |- *; auto; intuition.
Qed.

Lift quantifier
Fixpoint lift_quant (f : form) : form :=
match f with
| Forall f1Forall (lift_quant f1)
| Exists f1Exists (lift_quant f1)
| Imp f1 f2lift_if (lift_quant f1) (lift_quant f2)
| ANd f1 f2lift_andor ANd (lift_quant f1) (lift_quant f2)
| Or f1 f2lift_andor Or (lift_quant f1) (lift_quant f2)
| Neg f1lift_neg (lift_quant f1)
| f1f1
end.

Theorem lift_quant_prenex : f : form, prenex (lift_quant f).
intros f; elim f; simpl in |- *; auto.
Qed.
Hint Resolve lift_quant_prenex.

Theorem lift_quant_groundN :
f p, groundNForm p f groundNForm p (lift_quant f).
intros f; elim f; clear f; unfold lift_quant in |- *; lazy beta in |- *;
fold lift_quant in |- *; auto.
intros f H p H0; inversion H0; auto.
intros f H p H0; inversion H0; auto.
intros f H f0 H0 p H1; inversion H1; apply lift_andor_and_groundN; auto.
apply groundNForm_le with (2 := H4); auto.
apply groundNForm_le with (2 := H5); auto.
intros f H f0 H0 p H1; inversion H1; apply lift_andor_or_groundN; auto.
apply groundNForm_le with (2 := H4); auto.
apply groundNForm_le with (2 := H5); auto.
intros f H f0 H0 p H1; inversion H1; apply lift_if_groundN; auto.
apply groundNForm_le with (2 := H4); auto.
apply groundNForm_le with (2 := H5); auto.
intros f H p H0; inversion H0; apply lift_neg_groundN; auto.
Qed.

Theorem correct_lift_quant :
(f : form) (l : list Z), form2Prop l f form2Prop l (lift_quant f).
intros f; elim f; simpl in |- *; auto; try (intuition; fail).
intros f0 H l; split; intros H0 x; case (H (x :: l)); auto.
intros f0 H l; split; intros (x, H0); x; case (H (x :: l)); auto.
intros f1 H f2 H0 l; case (H l); intros H1 H2; case (H0 l); intros H3 H4;
case (correct_lift_andor_and (lift_quant f1) (lift_quant f2)) with (l := l);
intuition.
intros f1 H f2 H0 l; case (H l); intros H1 H2; case (H0 l); intros H3 H4;
case (correct_lift_andor_or (lift_quant f1) (lift_quant f2)) with (l := l);
intuition.
intros f1 H f2 H0 l; case (H l); intros H1 H2; case (H0 l); intros H3 H4;
case (correct_lift_if (lift_quant f1) (lift_quant f2)) with (l := l);
intuition.
intros f1 H l; case (H l); intros H1 H2;
case (correct_lift_neg (lift_quant f1)) with (l := l);
intuition.
Qed.