(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export ground_1.

      Structure G: Set := {
         next: nat -> nat;
         next_lt: (n:?) (lt n (next n))
      }.

      Hints Resolve next_lt : ld.

      Fixpoint next_plus [g:G; n:nat; i:nat]: nat := Cases i of
         | (0)   => n
         | (S i) => (next g (next_plus g n i))
      end.

   Section next_plus_props. (************************************************)

      Lemma next_plus_assoc: (g:?; n,h1,h2:?)
                             (next_plus g (next_plus g n h1) h2) =
                             (next_plus g n (plus h1 h2)).
      Proof.
      XElim h1; Simpl.
(* case 1: h1 = 0 *)
      XAuto.
(* case 2: h1 > 0 *)
      XElim h2; Simpl; Intros.
(* case 2.1: h2 = 0 *)
      Rewrite <- plus_n_O; XAuto.
(* case 2.1: h2 > 0 *)
      Rewrite <- plus_n_Sm; Simpl; XAuto.
      Qed.

      Lemma next_plus_next: (g:?; n,h:?) (next_plus g (next g n) h) =
                                         (next g (next_plus g n h)).
      Proof.
      Intros; Fold (next_plus g n (1)).
      Rewrite next_plus_assoc; XAuto.
      Qed.

      Lemma next_plus_lt: (g:?; h,n:?) (lt n (next_plus g (next g n) h)).
      Proof.
      XElim h; Simpl; Intros.
(* case 1: h = 0 *)
      XAuto.
(* case 2: h > 0 *)
      Rewrite <- next_plus_next.
      EApply lt_trans; [ EApply next_lt | XAuto ].
      Qed.

   End next_plus_props.

      Hints Resolve next_plus_lt : ld.