Library Freevars

Require Export Premodel.

Implicit Types Gamma Delta : context.

Implicit Types u v : inttype -> Prop.
Implicit Types m n : basetype -> Prop.

Implicit Types A B C : inttype.
Implicit Types F G H : basetype.

Implicit Types x y z : var.
Implicit Types s t : term.

Inductive FV : term -> var -> Prop :=
| FVVar x : FV x x
| FVAppL s t x : FV s x -> FV (s t) x
| FVAppR s t x : FV t x -> FV (s t) x
| FVLam s x : FV s (S x) -> FV (Lam s) x.

Instance FV_dec t x : Dec (FV t x).
revert x.
induction t ; intros y.
- decide (x = y).
  + subst. left ; eauto using FVVar.
  + right. inversion 1 ; auto.
- decide (FV t1 y) ; [ | decide (FV t2 y) ].
  + left ; eauto using FVAppL.
  + left ; eauto using FVAppR.
  + right. inversion 1 ; auto.
- decide (FV s (S y)).
  + left ; eauto using FVLam.
  + right. inversion 1 ; auto.
Qed.

Lemma agree_ty Gamma1 Gamma2 t : (forall x, FV t x -> Gamma1 x = Gamma2 x) -> forall (n :nat) T, ty n Gamma1 t T -> ty n Gamma2 t T.
intros e n T tyT.
revert Gamma2 e.
induction tyT ; intros Gamma2 e12.
- constructor. rewrite <- e12 ; auto using FVVar.
- constructor. apply IHtyT. intros [|x] ; simpl ; auto using FVLam.
- econstructor.
  + apply (IHtyT1 (fun x => if (decide (FV (s t) x)) then Gamma x else Empty x)).
    intros x H. decide (FV (s t) x) ; auto. exfalso ; auto using FVAppL.
  + apply (IHtyT2 (fun x => if (decide (FV (s t) x)) then Delta x else Gamma2 x)).
    intros x H. decide (FV (s t) x) ; auto. exfalso ; auto using FVAppR.
  + intros x. simpl. decide (FV (s t) x) ; auto. rewrite <- e12, (e x) ; auto.
- econstructor.
  + apply (IHtyT1 (fun x => if (decide (FV s x)) then Gamma x else Empty x)).
    intros x H. decide (FV s x) ; auto.
  + apply (IHtyT2 (fun x => if (decide (FV s x)) then Delta x else Gamma2 x)).
    intros x H. decide (FV s x) ; auto.
  + intros x. simpl. decide (FV s x) ; auto. rewrite <- e12, (e x) ; auto.
- auto.
Qed.

Lemma agree_equiv rho1 rho2 t : valid rho1 -> valid rho2 -> (forall x, FV t x -> rho1 x ~ rho2 x) -> [t]rho1 ~ [t]rho2.
revert rho1 rho2.
induction t ; intros rho1 rho2 rho1_val rho2_val H.
- rewrite ! int_x ; auto using FVVar.
- rewrite ! int_st ; auto.
  rewrite IHt1, IHt2 ; auto using filter_equiv_refl, FVAppL, FVAppR.
- intros A.
  split.
  + intros [n Gamma C T]. exists n (fun x => if (decide (FV s (S x))) then Gamma x else OMEGA) ; auto.
    { intros x B E. decide (FV s (S x)) ; eauto. apply H ; eauto using FVLam. }
    eapply agree_ty ; eauto.
    intros x HF. decide (FV s (S x)) ; auto. now inversion HF.
  + intros [n Gamma C T]. exists n (fun x => if (decide (FV s (S x))) then Gamma x else OMEGA) ; auto.
    { intros x B E. decide (FV s (S x)) ; eauto. apply H ; eauto using FVLam. }
    eapply agree_ty ; eauto.
    intros x HF. decide (FV s (S x)) ; auto. now inversion HF.
Qed.