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

      Inductive pr0 : T -> T -> Prop :=
         | pr0_refl   : (t:?) (pr0 t t)
         | pr0_comp   : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
                        (k:?) (pr0 (THead k u1 t1) (THead k u2 t2))
         | pr0_beta   : (u,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
                        (pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u t1))
                             (THead (Bind Abbr) v2 t2))
         | pr0_upsilon: (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
                        (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
                        (pr0 (THead (Flat Appl) v1 (THead (Bind b) u1 t1))
                             (THead (Bind b) u2 (THead (Flat Appl) (lift (1) (0) v2) t2)))
         | pr0_delta  : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
                        (w:?) (subst0 (0) u2 t2 w) ->
                        (pr0 (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 w))
         | pr0_zeta   : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
                        (u:?) (pr0 (THead (Bind b) u (lift (1) (0) t1)) t2)
         | pr0_tau    : (t1,t2:?) (pr0 t1 t2) ->
                        (u:?) (pr0 (THead (Flat Cast) u t1) t2).

      Hint pr0 : ld := Constructors pr0.

   Section pr0_gen_base. (***************************************************)

      Lemma pr0_gen_sort: (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
      Proof.
      Intros; InsertEq H '(TSort n); XElim H; Clear y x;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma pr0_gen_lref: (x:?; n:?) (pr0 (TLRef n) x) -> x = (TLRef n).
      Proof.
      Intros; InsertEq H '(TLRef n); XElim H; Clear y x;
      Intros; XInv; Subst; XAuto.
      Qed.

      Lemma pr0_gen_abst: (u1,t1,x:?) (pr0 (THead (Bind Abst) u1 t1) x) ->
                          (EX u2 t2 | x = (THead (Bind Abst) u2 t2) &
                                      (pr0 u1 u2) & (pr0 t1 t2)
                          ).

      Proof.
      Intros; InsertEq H '(THead (Bind Abst) u1 t1); XElim H; Clear y x;
      Intros; XInv; Subst; Try EqFalse; XDEAuto 2.
      Qed.

      Lemma pr0_gen_appl: (u1,t1,x:?) (pr0 (THead (Flat Appl) u1 t1) x) -> (OR
                          (EX u2 t2 | x = (THead (Flat Appl) u2 t2) &
                                      (pr0 u1 u2) & (pr0 t1 t2)
                          ) |
                          (EX y1 z1 u2 t2 | t1 = (THead (Bind Abst) y1 z1) &
                                            x = (THead (Bind Abbr) u2 t2) &
                                            (pr0 u1 u2) & (pr0 z1 t2)
                          ) |
                          (EX b y1 z1 u2 v2 t2 |
                              ~b=Abst &
                              t1 = (THead (Bind b) y1 z1) &
                              x = (THead (Bind b) v2 (THead (Flat Appl) (lift (1) (0) u2) t2)) &
                              (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
                          ).
      Proof.
      Intros; InsertEq H '(THead (Flat Appl) u1 t1); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

      Lemma pr0_gen_cast: (u1,t1,x:?) (pr0 (THead (Flat Cast) u1 t1) x) ->
                          (EX u2 t2 | x = (THead (Flat Cast) u2 t2) &
                                      (pr0 u1 u2) & (pr0 t1 t2)
                          ) \/
                          (pr0 t1 x).
      Proof.
      Intros; InsertEq H '(THead (Flat Cast) u1 t1); XElim H; Clear y x;
      Intros; XInv; Subst; XDEAuto 3.
      Qed.

   End pr0_gen_base.

      Tactic Definition Pr0GenBase := (
         Match Context With
            | [ H: (pr0 (TSort ?1) ?2) |- ? ] ->
               LApply (pr0_gen_sort ?2 ?1); [ Clear H; Intros | XAuto ]
            | [ H: (pr0 (TLRef ?1) ?2) |- ? ] ->
               LApply (pr0_gen_lref ?2 ?1); [ Clear H; Intros | XAuto ]
            | [ H: (pr0 (THead (Bind Abst) ?1 ?2) ?3) |- ? ] ->
               LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
               XElim H; Intros
            | [ H: (pr0 (THead (Flat Appl) ?1 ?2) ?3) |- ? ] ->
               LApply (pr0_gen_appl ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
               XElim H; Intros H; XElim H; Intros
            | [ H: (pr0 (THead (Flat Cast) ?1 ?2) ?3) |- ? ] ->
               LApply (pr0_gen_cast ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
               XElim H; [ Intros H; XElim H; Intros | Intros ]
         ).