Require Export pc3_defs.

(*#* #stop record *)

      Record G : Set := {
         next     : nat -> nat;
	 base     : nat;
         next_lt  : (n:?) (lt n (next n));
	 base_next: (n:?) (le base n) -> (next n) = (S n)
      }.

(*#* #start record *)

(*#* #caption "current axioms for typing",
   "well formed context sort", "well formed context binder", 
   "conversion rule", "typed sort", "typed reference to abbreviation",
   "typed reference to abstraction", "typed binder", "typed application", 
   "typed cast" 
*)
(*#* #cap #cap c, d, t, t0, t1, t2, w #alpha m in h, n in i, u in V, v in U *)

      Inductive wf0 [g:G] : C -> Prop :=
         | wf0_sort: (m:?) (wf0 g (CSort m))
         | wf0_bind: (c:?; u,t:?) (ty0 g c u t) ->
                     (b:?) (wf0 g (CTail c (Bind b) u))
      with ty0 [g:G] : C -> T -> T -> Prop :=
(* structural rules *)
         | ty0_conv: (c:?; t2,t:?) (ty0 g c t2 t) ->
                     (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
                     (ty0 g c u t2)
(* axiom rules *)
         | ty0_sort: (c:?) (wf0 g c) ->
                     (m:?) (ty0 g c (TSort m) (TSort (next g m)))
         | ty0_abbr: (c:?) (wf0 g c) ->
                     (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
                     (t:?) (ty0 g d u t) ->
                     (ty0 g c (TLRef n) (lift (S n) (0) t))
         | ty0_abst: (c:?) (wf0 g c) ->
                     (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
                     (t:?) (ty0 g d u t) ->
                     (ty0 g c (TLRef n) (lift (S n) (0) u))
         | ty0_bind: (c:?; u,t:?) (ty0 g c u t) ->
                     (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
                     (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
                     (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
         | ty0_appl: (c:?; w,u:?) (ty0 g c w u) ->
                     (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
                     (ty0 g c (TTail (Flat Appl) w v)
                              (TTail (Flat Appl) w (TTail (Bind Abst) u t))
                     )
         | ty0_cast: (c:?; t1,t2:?) (ty0 g c t1 t2) ->
                     (t0:?) (ty0 g c t2 t0) ->
                     (ty0 g c (TTail (Flat Cast) t2 t1) t2).

(*#* #stop file *)

      Hint wf0 : ltlc := Constructors wf0.

      Hint ty0 : ltlc := Constructors ty0.

   Section wf0_props. (******************************************************)

      Theorem wf0_ty0: (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
      Intros; XElim H; XAuto.
      Qed.

      Hints Resolve wf0_ty0 : ltlc.

      Theorem wf0_drop_O: (c,e:?; h:?) (drop h (0) c e) ->
                          (g:?) (wf0 g c) -> (wf0 g e).
      XElim c.
(* case 1 : CSort *)
      Intros; DropGenBase; Rewrite H; XAuto.
(* case 2 : CTail k *)
      Intros c IHc; XElim k; (
      XElim h; Intros; DropGenBase;
      [ Rewrite H in H0; XAuto | Inversion H1; XEAuto ] ).
      Qed.

   End wf0_props.

      Hints Resolve wf0_ty0 wf0_drop_O : ltlc.

      Tactic Definition Wf0Ty0 :=
         Match Context With
            [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
               LApply (wf0_ty0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
               Inversion_clear H_x.

      Tactic Definition Wf0DropO :=
         Match Context With
            | [ _: (drop ?1 (0) ?2 ?3); _: (wf0 ?4 ?2) |- ? ] ->
               LApply (wf0_drop_O ?2 ?3 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].

   Section wf0_facilities. (*************************************************)

      Theorem wf0_drop_wf0: (g:?; c:?) (wf0 g c) ->
                            (b:?; e:?; u:?; h:?)
                            (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
      Intros.
      Wf0DropO; Inversion H1; XEAuto.
      Qed.

      Theorem ty0_drop_wf0: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
                            (b:?; e:?; u:?; h:?)
                            (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
      Intros.
      EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
      Qed.

   End wf0_facilities.

      Hints Resolve wf0_drop_wf0 ty0_drop_wf0 : ltlc.

      Tactic Definition DropWf0 :=
         Match Context With
            | [ _: (ty0 ?1 ?2 ?3 ?4);
                _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
               LApply (ty0_drop_wf0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
               LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ]
            | [ _: (wf0 ?1 ?2);
                _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
               LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
               LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].