(****************************************************************************)
(*                                                                          *)
(*                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 ty3_defs.

      Inductive wf3 [g:G] : C -> C -> Prop :=
         | wf3_sort: (m:?) (wf3 g (CSort m) (CSort m))
         | wf3_bind: (c1,c2:?) (wf3 g c1 c2) -> (u,t:?) (ty3 g c1 u t) ->
                     (b:?) (wf3 g (CHead c1 (Bind b) u) (CHead c2 (Bind b) u))
         | wf3_void: (c1,c2:?) (wf3 g c1 c2) -> (u:?)
                     ((t:?) (ty3 g c1 u t) -> False) ->
                     (b:?) (wf3 g (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort (0))))
         | wf3_flat: (c1,c2:?) (wf3 g c1 c2) ->
                     (u:?; f:?) (wf3 g (CHead c1 (Flat f) u) c2).

      Hint wf3 : ld := Constructors wf3.

   Section wf3_gen_base. (***************************************************)

      Lemma wf3_gen_sort1: (g:?; x:?; m:?) (wf3 g (CSort m) x) ->
                           x = (CSort m).
      Proof.
      Intros; InsertEq H '(CSort m); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma wf3_gen_bind1: (g:?; c1,x:?; v:?; b:?)
                           (wf3 g (CHead c1 (Bind b) v) x) ->
                           (EX c2 w | x = (CHead c2 (Bind b) v) &
                                     (wf3 g c1 c2) & (ty3 g c1 v w)
                           ) \/
                           (EX c2 | x = (CHead c2 (Bind Void) (TSort (0))) &
                                    (wf3 g c1 c2) &
                                    ((w:?) (ty3 g c1 v w) -> False)
                           ).
      Proof.
      Intros; InsertEq H '(CHead c1 (Bind b) v); XElim H; Clear x y;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

      Lemma wf3_gen_flat1: (g:?; c1,x:?; v:?; f:?)
                           (wf3 g (CHead c1 (Flat f) v) x) -> (wf3 g c1 x).
      Proof.
      Intros; InsertEq H '(CHead c1 (Flat f) v); XElim H; Clear x y;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma wf3_gen_head2: (g:?; x,c:?; v:?; k:?) (wf3 g x (CHead c k v)) ->
                           (EX b | k = (Bind b)).
      Proof.
      Intros; InsertEq H '(CHead c k v); XElim H; Clear x y;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

   End wf3_gen_base.

      Tactic Definition WF3GenBase := (
         Match Context With
            | [ H: (wf3 ? (CSort ?) ?) |- ? ] ->
               XPoseClear H '(wf3_gen_sort1 ? ? ? H); Subst; XInv
            | [ H: (wf3 ? (CHead ? (Bind ?) ?) ?) |- ? ] ->
               XDecomPoseClear H '(wf3_gen_bind1 ? ? ? ? ? H); Subst
            | [ H: (wf3 ? (CHead ? (Flat ?) ?) ?) |- ? ] ->
               XPoseClear H '(wf3_gen_flat1 ? ? ? ? ? H)
            | [ H: (wf3 ? ? (CHead ? ? ?)) |- ? ] ->
               XDecomPoseClear H '(wf3_gen_head2 ? ? ? ? ? H); Subst; XInv
         ).

   Section wf3_props_base. (*************************************************)

      Theorem wf3_mono: (g:?; c,c1:?) (wf3 g c c1) -> (c2:?) (wf3 g c c2) ->
                        c1 = c2.
      Proof.
      Intros until 1; XElim H; Clear c c1;
      Intros; WF3GenBase; XAuto.
(* case 1: first conclusion *)
      XDecomPose '(H6 ? H1).
(* case 2: second conclusion *)
      XDecomPose '(H1 ? H6).
      Qed.

      Lemma wf3_clear_conf: (c1,c:?) (clear c1 c) ->
                            (g:?; c2:?) (wf3 g c1 c2) -> (wf3 g c c2).
      Proof.
      Intros until 1; XElim H; Clear c1 c; Intros.
(* case 1: clear_bind *)
      XAuto.
(* case 2: clear_flat *)
      WF3GenBase; XAuto.
      Qed.

      Lemma clear_wf3_trans: (c1,d1:?) (clear c1 d1) ->
                             (g:?; d2:?) (wf3 g d1 d2) ->
                             (EX c2 | (wf3 g c1 c2) & (clear c2 d2)).
      Proof.
      Intros until 1; XElim H; Clear c1 d1; Intros.
(* case 1: clear_bind *)
      WF3GenBase; XDEAuto 3.
(* case 2: clear_flat *)
      XDecomPoseClear H0 '(H0 ? ? H1); Clear H1; XDEAuto 3.
      Qed.

      Lemma wf3_getl_conf: (b:?; i:?; c1,d1:?; v:?)
                           (getl i c1 (CHead d1 (Bind b) v)) ->
                           (g:?; c2:?) (wf3 g c1 c2) ->
                           (w:?) (ty3 g d1 v w) ->
                           (EX d2 | (getl i c2 (CHead d2 (Bind b) v)) &
                                    (wf3 g d1 d2)
                           ).
      Proof.
      XElim i.
(* case 1: i = 0 *)
      Intros; GetLGenBase.
      XPoseClear H '(wf3_clear_conf ? ? H ? ? H0); Clear H0.
      WF3GenBase; [ XDEAuto 2 | XDecomPose '(H4 ? H1) ].
(* case 2: i > 0 *)
      XElim c1; Intros; GetLGenBase.
      NewInduction k; WF3GenBase; Simpl in H1.
(* case 2.1; wf3_bind *)
      Clear H0 H7.
      XDecomPoseClear H '(H ? ? ? H1 ? ? H6 ? H3); Clear H1 H6 H3.
      XDEAuto 3.
(* case 2.2; wf3_void *)
      Clear H0 H7.
      XDecomPoseClear H '(H ? ? ? H1 ? ? H6 ? H3); Clear H1 H6 H3.
      XDEAuto 3.
(* case 2.2; wf3_flat *)
      Clear H; XDEAuto 3.
      Qed.

   End wf3_props_base.

      Tactic Definition WF3PropsBase := (
         Match Context With
            | [ H1: (wf3 ?0 ?1 ?); H2: (wf3 ?0 ?1 ?) |- ? ] ->
               XPoseClear H2 '(wf3_mono ? ? ? H1 ? H2); Subst
            | [ H1: (getl ? ?1 (CHead ?2 (Bind ?) ?3)); H2: (wf3 ?0 ?1 ?);
                H3: (ty3 ?0 ?2 ?3 ?) |- ? ] ->
               XDecomPose '(wf3_getl_conf ? ? ? ? ? H1 ? ? H2 ? H3)
         ).