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

Inductive groundNExp : nat -> exp -> Prop :=
  | GNNum : forall i n : nat, groundNExp n (Num i)
  | GNVar : forall i n : nat, i < n -> groundNExp n (Var i)
  | GNPlus :
      forall 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 : forall n : nat, groundNForm n TRue
  | GNFalse : forall n : nat, groundNForm n FAlse
  | GNNeg : forall a n, groundNForm n a -> groundNForm n (Neg a)
  | GNAnd :
      forall a b n m p,
      n <= p ->
      m <= p -> groundNForm n a -> groundNForm m b -> groundNForm p (ANd a b)
  | GNOr :
      forall a b n m p,
      n <= p ->
      m <= p -> groundNForm n a -> groundNForm m b -> groundNForm p (Or a b)
  | GNImp :
      forall a b n m p,
      n <= p ->
      m <= p -> groundNForm n a -> groundNForm m b -> groundNForm p (Imp a b)
  | GNEq :
      forall a b n m p,
      n <= p ->
      m <= p ->
      groundNExp n a -> groundNExp m b -> groundNForm p (Form.Eq a b)
  | GNCong :
      forall i a b n m p,
      n <= p ->
      m <= p ->
      groundNExp n a -> groundNExp m b -> groundNForm p (Cong i a b)
  | GNForall : forall f m, groundNForm (S m) f -> groundNForm m (Forall f)
  | GNExists : forall 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 : forall n : nat, groundNL n nil
  | GNVCons :
      forall a l n, groundNForm n a -> groundNL n l -> groundNL n (a :: l).

Inductive groundNL2 : nat -> list (nat * form) -> Prop :=
  | GNNil2 : forall n : nat, groundNL2 n nil
  | GNVCons2 :
      forall a l n m,
      groundNForm n a -> groundNL2 n l -> groundNL2 n ((m, a) :: l).
Hint Constructors groundNL.
Hint Constructors groundNL2.

Theorem groundNL_app :
 forall 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 :
 forall 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 :
 forall 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 :
 forall 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 : forall 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 : forall 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 :
 forall 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 :
 forall 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 :
 forall 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 :
 forall 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 :
 forall 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.