# Ground formulae

Require Import Form.
Require Import sTactic.
Require Import Nat.

Definition of ground expression at level n:
• no variable has index greater than n
Inductive groundNExp : nat exp Prop :=
| GNNum : i n : nat, groundNExp n (Num i)
| GNVar : i n : nat, i < n groundNExp n (Var i)
| GNPlus :
a b n m p,
n p
m p groundNExp n a groundNExp m b groundNExp p (Plus a b).

Check if an expresssion e has level n
Fixpoint fgroundNExp (n : nat) (e : exp) {struct e} : bool :=
match e with
| Num _true
| Var iltdec i n
| Plus a b
match fgroundNExp n a with
| truefgroundNExp n b
| falsefalse
end
end.
Hint Constructors groundNExp.

Definition of ground formula at level n:
• no variable has index greater than n

Inductive groundNForm : nat form Prop :=
| GNTrue : n : nat, groundNForm n TRue
| GNFalse : n : nat, groundNForm n FAlse
| GNNeg : a n, groundNForm n a groundNForm n (Neg a)
| GNAnd :
a b n m p,
n p
m p groundNForm n a groundNForm m b groundNForm p (ANd a b)
| GNOr :
a b n m p,
n p
m p groundNForm n a groundNForm m b groundNForm p (Or a b)
| GNImp :
a b n m p,
n p
m p groundNForm n a groundNForm m b groundNForm p (Imp a b)
| GNEq :
a b n m p,
n p
m p
groundNExp n a groundNExp m b groundNForm p (Form.Eq a b)
| GNCong :
i a b n m p,
n p
m p
groundNExp n a groundNExp m b groundNForm p (Cong i a b)
| GNForall : f m, groundNForm (S m) f groundNForm m (Forall f)
| GNExists : f m, groundNForm (S m) f groundNForm m (Exists f).
Hint Constructors groundForm.

Check if an formula f has level n

Fixpoint fgroundNForm (n : nat) (f : form) {struct f} : bool :=
match f with
| TRuetrue
| FAlsetrue
| Neg afgroundNForm n a
| ANd a b
match fgroundNForm n a with
| truefgroundNForm n b
| falsefalse
end
| Or a b
match fgroundNForm n a with
| truefgroundNForm n b
| falsefalse
end
| Imp a b
match fgroundNForm n a with
| truefgroundNForm n b
| falsefalse
end
| Form.Eq a b
match fgroundNExp n a with
| truefgroundNExp n b
| falsefalse
end
| Cong i a b
match fgroundNExp n a with
| truefgroundNExp n b
| falsefalse
end
| Forall afgroundNForm (S n) a
| Exists afgroundNForm (S n) a
end.
Hint Constructors groundExp.
Hint Constructors groundNForm.

Same as groundN but for list
Inductive groundNL : nat list form Prop :=
| GNNil : n : nat, groundNL n nil
| GNVCons :
a l n, groundNForm n a groundNL n l groundNL n (a :: l).

Same as groundN but for list of pair
Inductive groundNL2 : nat list (nat × form) Prop :=
| GNNil2 : n : nat, groundNL2 n nil
| GNVCons2 :
a l n m,
groundNForm n a groundNL2 n l groundNL2 n ((m, a) :: l).
Hint Constructors groundNL.
Hint Constructors groundNL2.

Some properties of groundN and groundNL
Theorem groundNL_app :
n l1 l2, groundNL n l1 groundNL n l2 groundNL n (l1 ++ l2).
intros n l1 l2 H; generalize l2; elim H; simpl in |- *; auto.
Qed.
Hint Resolve groundNL_app.

Theorem groundNL2_app :
n l1 l2, groundNL2 n l1 groundNL2 n l2 groundNL2 n (l1 ++ l2).
intros n l1 l2 H; generalize l2; elim H; simpl in |- *; auto.
Qed.
Hint Resolve groundNL2_app.

Theorem groundNExp_le :
a n m, groundNExp n a n m groundNExp m a.
intros a n m H; generalize m; elim H; clear H n m; simpl in |- *; auto.
intros i n H m H0; apply GNVar.
apply lt_le_trans with (1 := H); auto.
intros a0 b n m p H H0 H1 H2 H3 H4 m0 H5.
apply GNPlus with (n := p) (m := p); auto.
Qed.

Theorem groundNForm_le :
a n m, groundNForm n a n m groundNForm m a.
intros a n m H; generalize m; elim H; clear H n m; simpl in |- *; auto.
intros a0 b n m p H H0 H1 H2 H3 H4 m0 H5.
apply GNAnd with (n := p) (m := p); auto.
intros a0 b n m p H H0 H1 H2 H3 H4 m0 H5.
apply GNOr with (n := p) (m := p); auto.
intros a0 b n m p H H0 H1 H2 H3 H4 m0 H5.
apply GNImp with (n := p) (m := p); auto.
intros a0 b n m p H H0 H1 H2 m0 H3.
apply GNEq with (n := p) (m := p); auto.
apply groundNExp_le with (n := n); auto.
apply groundNExp_le with (n := m); auto.
intros i a0 b n m p H H0 H1 H2 m0 H3.
apply GNCong with (n := p) (m := p); auto.
apply groundNExp_le with (n := n); auto.
apply groundNExp_le with (n := m); auto.
intros f m H H0 m0 H1.
apply GNForall; auto with arith.
intros f m H H0 m0 H1.
apply GNExists; auto with arith.
Qed.

Theorem groundNL_le : a n m, groundNL n a n m groundNL m a.
intros a n m H; generalize m; elim H; clear H n m; simpl in |- *; auto.
intros a0 l n H H0 H1 m H2.
apply GNVCons; auto.
apply groundNForm_le with (n := n); auto.
Qed.

Theorem groundNL2_le : a n m, groundNL2 n a n m groundNL2 m a.
intros a n m H; generalize m; elim H; clear H n m; simpl in |- *; auto.
intros a0 l n m H H0 H1 m1 H2.
apply GNVCons2; auto.
apply groundNForm_le with (n := n); auto.
Qed.

Theorem scal_groundN :
n a b, groundNExp n a groundNExp n (scal b a).
intros n a b H; elim b; simpl in |- *; auto.
intros n0; case n0; auto.
intros n1 H0; apply GNPlus with (n := n) (m := n); auto.
Qed.
Require Import Max.

Theorem shiftExp_groundN :
n a th i o,
groundNExp n a groundNExp (max (th + i) (n + o)) (shiftExp th i o a).
intros n a th i o H; generalize th i o; elim H; simpl in |- *; auto.
intros i0 n0 H0 th0 i1 o0; generalize (ltdec_correct i0 th0);
case (ltdec i0 th0); auto.
intros H1; apply groundNExp_le with (S (i0 + i1)); auto with arith.
apply le_trans with (th0 + i1); auto with arith.
intros H1; apply groundNExp_le with (S (i0 + o0)); auto with arith.
apply le_trans with (n0 + o0); auto with arith.
intros a0 b n0 m p H0 H1 H2 H3 H4 H5 th0 i0 o0.
apply
GNPlus with (n := max (th0 + i0) (n0 + o0)) (m := max (th0 + i0) (m + o0));
auto with arith.
case (max_Or (th0 + i0) (n0 + o0)); intros H6; rewrite H6; auto with arith.
apply le_trans with (p + o0); auto with arith.
case (max_Or (th0 + i0) (m + o0)); intros H6; rewrite H6; auto with arith.
apply le_trans with (p + o0); auto with arith.
Qed.

Theorem shiftForm_groundN :
n a th i o,
noBinder a
groundNForm n a groundNForm (max (th + i) (n + o)) (shiftForm th i o a).
intros n a th i o H; generalize th i o; elim H; simpl in |- *; auto.
intros a0 H0 H1 th0 i0 o0 H2.
inversion H2; auto.
intros a0 b H0 H1 H2 H3 th0 i0 o0 H4.
inversion H4.
apply
GNAnd with (n := max (th0 + i0) (n + o0)) (m := max (th0 + i0) (n + o0));
auto.
apply H1.
apply groundNForm_le with (1 := H10); auto.
apply H3.
apply groundNForm_le with (1 := H11); auto.
intros a0 b H0 H1 H2 H3 th0 i0 o0 H4.
inversion H4.
apply GNOr with (n := max (th0 + i0) (n + o0)) (m := max (th0 + i0) (n + o0));
auto.
apply H1.
apply groundNForm_le with (1 := H10); auto.
apply H3.
apply groundNForm_le with (1 := H11); auto.
intros a0 b H0 H1 H2 H3 th0 i0 o0 H4.
inversion H4.
apply
GNImp with (n := max (th0 + i0) (n + o0)) (m := max (th0 + i0) (n + o0));
auto.
apply H1.
apply groundNForm_le with (1 := H10); auto.
apply H3.
apply groundNForm_le with (1 := H11); auto.
intros a0 b th0 i0 o0 H0.
inversion H0.
apply GNEq with (n := max (th0 + i0) (n + o0)) (m := max (th0 + i0) (n + o0));
auto.
apply shiftExp_groundN; auto.
apply groundNExp_le with (1 := H6); auto.
apply shiftExp_groundN; auto.
apply groundNExp_le with (1 := H7); auto.
intros i1 a0 b th0 i0 o0 H0.
inversion H0.
apply
GNCong with (n := max (th0 + i0) (n + o0)) (m := max (th0 + i0) (n + o0));
auto.
apply shiftExp_groundN; auto.
apply groundNExp_le with (1 := H7); auto.
apply shiftExp_groundN; auto.
apply groundNExp_le with (1 := H8); auto.
Qed.

Theorem fgrounNExp_correct :
n e,
match fgroundNExp n e with
| truegroundNExp n e
| false¬ groundNExp n e
end.
intros n e; elim e; simpl in |- *; auto.
intros i; generalize (ltdec_correct i n); case (ltdec i n); auto.
intros H; Contradict H; inversion H; auto with arith.
intros e1; case (fgroundNExp n e1).
intros H e2; case (fgroundNExp n e2); auto.
intros H0; (apply GNPlus with (n := n) (m := n); auto).
intros H0; Contradict H0; inversion H0; auto.
apply groundNExp_le with (1 := H7); auto.
intros H e2 H0; Contradict H; inversion H; auto.
apply groundNExp_le with (1 := H6); auto.
Qed.

Theorem fgrounNForm_correct :
f n,
match fgroundNForm n f with
| truegroundNForm n f
| false¬ groundNForm n f
end.
intros f; elim f; clear f; simpl in |- *; auto.
intros f H n; generalize (H (S n)); case (fgroundNForm (S n) f); auto.
intros H0; Contradict H0; inversion H0; auto.
intros f H n; generalize (H (S n)); case (fgroundNForm (S n) f); auto.
intros H0; Contradict H0; inversion H0; auto.
intros f H f0 H0 n; generalize (H n); case (fgroundNForm n f); auto.
generalize (H0 n); case (fgroundNForm n f0); auto.
intros H1 H2; apply GNAnd with (n := n) (m := n); auto.
intros H1 H2; Contradict H1; inversion H1.
apply groundNForm_le with (1 := H9); auto.
intros H1; Contradict H1; inversion H1.
apply groundNForm_le with (1 := H7); auto.
intros f H f0 H0 n; generalize (H n); case (fgroundNForm n f); auto.
generalize (H0 n); case (fgroundNForm n f0); auto.
intros H1 H2; apply GNOr with (n := n) (m := n); auto.
intros H1 H2; Contradict H1; inversion H1.
apply groundNForm_le with (1 := H9); auto.
intros H1; Contradict H1; inversion H1.
apply groundNForm_le with (1 := H7); auto.
intros f H f0 H0 n; generalize (H n); case (fgroundNForm n f); auto.
generalize (H0 n); case (fgroundNForm n f0); auto.
intros H1 H2; apply GNImp with (n := n) (m := n); auto.
intros H1 H2; Contradict H1; inversion H1.
apply groundNForm_le with (1 := H9); auto.
intros H1; Contradict H1; inversion H1.
apply groundNForm_le with (1 := H7); auto.
intros f H n; generalize (H n); case (fgroundNForm n f); auto.
intros H1; Contradict H1; inversion H1; auto.
intros e e0 n; generalize (fgrounNExp_correct n e); case (fgroundNExp n e).
intros H1; generalize (fgrounNExp_correct n e0); case (fgroundNExp n e0);
auto.
intros H; (apply GNEq with (n := n) (m := n); auto).
intros H; Contradict H; inversion H.
apply groundNExp_le with (1 := H7); auto.
intros H; Contradict H; inversion H.
apply groundNExp_le with (1 := H5); auto.
intros i e e0 n; generalize (fgrounNExp_correct n e); case (fgroundNExp n e).
intros H1; generalize (fgrounNExp_correct n e0); case (fgroundNExp n e0);
auto.
intros H; (apply GNCong with (n := n) (m := n); auto).
intros H; Contradict H; inversion H.
apply groundNExp_le with (1 := H8); auto.
intros H; Contradict H; inversion H.
apply groundNExp_le with (1 := H6); auto.
Qed.