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

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

Fixpoint fgroundNExp (n : nat) (e : exp) {struct e} : bool :=
  match e with
  | Num _ ⇒ true
  | Var i ⇒ ltdec i n
  | Plus a b ⇒
      match fgroundNExp n a with
      | true ⇒ fgroundNExp n b
      | false ⇒ false
      end
  end.
Hint Constructors groundNExp.

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.

Fixpoint fgroundNForm (n : nat) (f : form) {struct f} : bool :=
  match f with
  | TRue ⇒ true
  | FAlse ⇒ true
  | Neg a ⇒ fgroundNForm n a
  | ANd a b ⇒
      match fgroundNForm n a with
      | true ⇒ fgroundNForm n b
      | false ⇒ false
      end
  | Or a b ⇒
      match fgroundNForm n a with
      | true ⇒ fgroundNForm n b
      | false ⇒ false
      end
  | Imp a b ⇒
      match fgroundNForm n a with
      | true ⇒ fgroundNForm n b
      | false ⇒ false
      end
  | Form.Eq a b ⇒
      match fgroundNExp n a with
      | true ⇒ fgroundNExp n b
      | false ⇒ false
      end
  | Cong i a b ⇒
      match fgroundNExp n a with
      | true ⇒ fgroundNExp n b
      | false ⇒ false
      end
  | Forall a ⇒ fgroundNForm (S n) a
  | Exists a ⇒ fgroundNForm (S n) a
  end.
Hint Constructors groundExp.
Hint Constructors groundNForm.

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

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.

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
 | true ⇒ groundNExp 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
 | true ⇒ groundNForm 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.