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

      Inductive iso: T -> T -> Prop :=
         | iso_sort: (n1,n2:?) (iso (TSort n1) (TSort n2))
         | iso_lref: (i1,i2:?) (iso (TLRef i1) (TLRef i2))
         | iso_head: (v1,v2:?) (t1,t2:?)
                     (k:?) (iso (THead k v1 t1) (THead k v2 t2)).

      Hint iso : ld := Constructors iso.

   Section iso_gen_base. (***************************************************)

      Lemma iso_gen_sort: (u2:?; n1:?) (iso (TSort n1) u2) ->
                          (EX n2 | u2 = (TSort n2)).
      Proof.
      Intros; InsertEq H '(TSort n1); XElim H; Clear y u2;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma iso_gen_lref: (u2:?; n1:?) (iso (TLRef n1) u2) ->
                          (EX n2 | u2 = (TLRef n2)).
      Proof.
      Intros; InsertEq H '(TLRef n1); XElim H; Clear y u2;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Lemma iso_gen_head: (k:?; v1,t1,u2:?) (iso (THead k v1 t1) u2) ->
                          (EX v2 t2 | u2 = (THead k v2 t2)).
      Proof.
      Intros; InsertEq H '(THead k v1 t1); XElim H; Clear y u2;
      Intros; XInv; Subst; XDEAuto 2.
      Qed.

      Tactic Definition IsoGenBase := (
         Match Context With
            | [ H: (iso (TSort ?) ?) |- ? ] ->
               XDecomPoseClear H '(iso_gen_sort ? ? H); XInv; Subst
            | [ H: (iso (TLRef ?) ?) |- ? ] ->
               XDecomPoseClear H '(iso_gen_lref ? ? H); XInv; Subst
            | [ H: (iso (THead ? ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(iso_gen_head ? ? ? ? H); XInv; Subst
         ).

      Lemma iso_flats_lref_bind_false: (f:?; b:?; i:?; v,t:?; vs:?)
                                       (iso (THeads (Flat f) vs (TLRef i)) (THead (Bind b) v t)) ->
                                       (P:Prop) P.
      Proof.
      XElim vs; Simpl; Intros; IsoGenBase.
      Qed.

      Lemma iso_flats_flat_bind_false: (f1,f2:?; b:?; v,v2,t,t2:?; vs:?)
                                       (iso (THeads (Flat f1) vs (THead (Flat f2) v2 t2)) (THead (Bind b) v t)) ->
                                       (P:Prop) P.
      Proof.
      XElim vs; Simpl; Intros; IsoGenBase.
      Qed.

   End iso_gen_base.

      Tactic Definition IsoGenBase := (
         Match Context With
            | [ H: (iso (TSort ?) ?) |- ? ] ->
               XDecomPoseClear H '(iso_gen_sort ? ? H); Subst
            | [ H: (iso (TLRef ?) ?) |- ? ] ->
               XDecomPoseClear H '(iso_gen_lref ? ? H); Subst
            | [ H: (iso (THeads (Flat ?) ? (TLRef ?)) (THead (Bind ?) ? ?)) |- ? ] ->
               EApply iso_flats_lref_bind_false; Apply H
            | [ H: (iso (THeads (Flat ?) ? (THead (Flat ?) ? ?)) (THead (Bind ?) ? ?)) |- ? ] ->
               EApply iso_flats_flat_bind_false; Apply H
            | [ H: (iso (THead ? ? ?) ?) |- ? ] ->
               XDecomPoseClear H '(iso_gen_head ? ? ? ? H); Subst
         ).

   Section iso_props. (******************************************************)

      Lemma iso_refl: (t:?) (iso t t).
      Proof.
      XElim t; XAuto.
      Qed.

      Theorem iso_trans: (t1,t2:?) (iso t1 t2) -> (t3:?) (iso t2 t3) ->
                         (iso t1 t3).
      Proof.
      Intros until 1; XElim H; Clear t1 t2; Intros;
      IsoGenBase; XAuto.
      Qed.

   End iso_props.

      Hints Resolve iso_refl : ld.