Set Implicit Arguments.

Hint Extern 1 (?x = ?y) => f_equal.

Ltac naming E e expr :=
  set (e := expr) in * |- *; assert (E : e = expr);
  [ auto | clearbody e ].

Inductive empty : Type := .

Definition empty_inc X (x:empty) : X :=
  match x with end.

Definition comp X Y (f:X->Y) Z (g:Y->Z) (x:X) : Z := g (f x).

Notation "g 'o' f" := (comp f g) (at level 40, left associativity).

Definition funeq X Y (f g:X->Y) : Prop :=
  forall x, f x = g x.
Hint Unfold funeq.

Notation "f == g" := (funeq f g) (at level 70, no associativity).

Notation "^ f" := (option_map f)  (at level 5, right associativity).
Notation "^ X" := (option X) : type_scope.

Definition default X Y y (f:X->Y) (x':^X) : Y :=
  match x' with Some x => f x | None => y end.

Lemma option_map_extens : forall X x y (H : x=y) Y (f g:X->Y),
  f==g -> ^f x = ^g y.
Proof.
intros until 1. subst y. destruct x; simpl; auto.
Qed.
Hint Resolve option_map_extens.

Lemma funeq_option : forall X Y (f g:^X->Y),
  f None = g None -> (forall x, f (Some x) = g (Some x)) -> f==g.
Proof.
intros; intro; destruct x; auto.
Qed.
Hint Resolve funeq_option.

Inductive ftype (V:Type) : Type :=
  | Top : ftype V
  | TVar : V -> ftype V
  | Arr : ftype V -> ftype V -> ftype V
  | Uni : ftype V -> ftype ^V -> ftype V.
Notation "x --> y" := (Arr x y) (at level 42, right associativity).
Notation "'all' t1 , t2" := (Uni t1 t2) (at level 42).

Reserved Notation "% f" (at level 5, right associativity).

Fixpoint ftype_map V W (f:V->W) (t:ftype V) : ftype W :=
  match t with
  | Top => Top W
  | TVar x => TVar (f x)
  | s --> t => %f s --> %f t
  | all s, t => all %f s, %(^f) t
end
where "% f" := (ftype_map f).

Lemma ftype_map_extens : forall V (s t:ftype V) (H:s=t) W (f g:V->W),
  f==g -> %f s = %g t.
Proof.
intros until 1. subst s.
induction t; simpl; auto.
Qed.
Hint Resolve ftype_map_extens.

Lemma ftype_map_id : forall V (t:ftype V) (f:V->V),
  (forall x, f x=x) -> %f t=t.
Proof.
induction t; simpl; intros; auto.
f_equal. auto.
apply IHt2. destruct x; simpl; auto.
Qed.
Hint Resolve ftype_map_id.

Lemma ftype_map_comp : forall U t V (f:U->V) W (g:V->W),
  %g (%f t) = %(g o f) t.
Proof.
induction t; simpl; intros; auto.
rewrite IHt2. auto.
Qed.

Definition env V := V -> ftype V.

Definition consenv V (G:env V) (t:ftype V) : env ^V := fun x =>
  match x with
  | None => %(@Some V) t
  | Some x =>  %(@Some V) (G x)
  end.
Notation "G & t" := (consenv G t) (at level 50, left associativity).

Reserved Notation "D 'extends' G 'along' f" (at level 70).

Inductive RWF : forall W (D:env W) V (G:env V) (f:W->V), Prop :=
  | RWF_refl : forall V (G G':env V) (f:V->V),
      G==G' -> (forall x, f x = x) -> G' extends G along f
  | RWF_append : forall V1 (G1:env V1) V2 (f1:V1->V2) V3 (G3:env V3)
       (f2:V2->V3) (f:V1->V3)  (g:V3->ftype V2),
     (forall x, G3 x = %f2 (g x)) -> (forall x, f2 (f1 x) = f x) ->
     g o f2 extends G1 along f1 -> G3 extends G1 along f
where "D 'extends' G 'along' f" := (RWF G D f).

Lemma RWF_commute : forall W (D:env W) V (G:env V) (f:W->V),
  G extends D along f -> forall y, G (f y) = %f (D y).
Proof.
induction 1; intros.
rewrite H0. symmetry. rewrite H. auto.
rewrite H. rewrite <- H0. unfold comp in IHRWF. rewrite IHRWF.
rewrite ftype_map_comp. auto.
Qed.

Lemma RWF_extens : forall W (D D':env W) (HD : D==D')
  V (G G':env V) (HG : G==G') (f f':W->V) (Hf : f==f'),
  G extends D along f -> G' extends D' along f'.
Proof.
induction 4.
apply RWF_refl; intro. rewrite <- HD. rewrite <- HG. auto.
rewrite <- Hf. auto.
apply RWF_append with (f1:=f1) (f2:=f2) (g:=g); intros; auto.
rewrite <- H. auto.
rewrite <- Hf. auto.
Qed.
Hint Resolve RWF_refl.

Lemma RWF_trans : forall V1 (G1:env V1) V2 (G2:env V2) (f1:V1->V2)
    V3 (G3:env V3) (f2:V2->V3) (f:V1->V3),
  G2 extends G1 along f1 -> G3 extends G2 along f2 ->
  (forall x, f2 (f1 x) = f x) ->
  G3 extends G1 along f.
Proof.
induction 2; intros.
apply RWF_extens with (2:=H0) (f:=f1) (D:=G1); try intro; auto.
rewrite <- H2. auto.
apply RWF_append with (f1:=fun v => f0(f1 v)) (f2:=f2) (g:=g);
  intros; eauto.
rewrite H1. auto.
Qed.

Lemma RWF_consenv : forall V (G:env V) (t:ftype V),
  G&t extends G along @Some V.
Proof.
intros.
apply RWF_append with
  (f1:=fun x:V => x) (f2:=@Some V) (g := default t G); auto.
destruct x; reflexivity.
Qed.
Hint Resolve RWF_consenv.

Lemma RWF_RWF_consenv : forall W (D:env W) V (G:env V) (f:W->V) t,
  G extends D along f -> G&t extends D along fun y => Some (f y).
Proof.
intros. apply RWF_trans with (1:=H) (f2:=@Some V); auto.
Qed.
Hint Resolve RWF_RWF_consenv.

Lemma RWF_option_map : forall W (D:env W) V (G:env V) (f:W->V) t,
  G extends D along f -> G & %f t extends D&t along ^f.
Proof.
induction 1.
apply RWF_refl; intro; symmetry; destruct x; simpl; auto.
apply RWF_append with (f1:=^f1) (f2:=^f2)
  (g:=fun v => %(@Some V2) (default (%f1 t) g v)).
destruct x; simpl; try rewrite H; repeat rewrite ftype_map_comp.
apply ftype_map_extens; split.
apply ftype_map_extens. split.
intro. unfold comp. simpl. auto.
destruct x; simpl; auto.
apply RWF_extens with (4:=IHRWF t); try intro; auto.
destruct x; split.
Qed.
Hint Resolve RWF_option_map.

Definition WF V (G:env V) := G extends @empty_inc _ along @empty_inc V.

Lemma WF_trans : forall W (D:env W) V (G:env V) (f:W->V),
  WF D -> G extends D along f -> WF G.
Proof.
intros. unfold WF.
apply RWF_trans with (1:=H) (2:=H0).
destruct x.
Qed.
Hint Resolve WF_trans.

Lemma WF_consenv : forall V (G:env V) (t:ftype V),
  WF G -> WF (G & t).
Proof.
intros. unfold WF.
apply RWF_append with (f1:=empty_inc V) (f2:=@Some V)
   (g:=default t G); try destruct x; auto.
apply RWF_extens with (4:=H); auto.
Qed.
Hint Resolve WF_consenv.

Reserved Notation "G |-- s << t" (at level 68).

Inductive sub : forall V (G:env V) (s t:ftype V), Prop :=
  | SA_Top : forall V (G:env V) (s:ftype V),
      WF G -> G |-- s << Top _
  | SA_Refl_TVar : forall V (G:env V) (x:V),
      WF G -> G |-- TVar x << TVar x
  | SA_Trans_TVar : forall V (G:env V) (x:V) t,
      G |-- G x << t -> G |-- TVar x << t
  | SA_Arrow : forall V (G:env V) (s1 s2 t1 t2:ftype V),
      G |-- t1 << s1 -> G |-- s2 << t2 -> G |-- s1 --> s2 << t1 --> t2
  | SA_All : forall V (G:env V) (t1 s1:ftype V) (s2 t2:ftype ^V),
      G |-- t1 << s1 -> G & t1 |-- s2 << t2 -> G |-- all s1, s2 << all t1, t2
where "G |-- s << t" := (sub G s t).
Hint Constructors sub.

Ltac subinversion H :=
  match type of H with
  | ?G' |-- ?s' << ?t' =>
    let s := fresh "s" in let Hs := fresh "Hs" in naming Hs s s';
    let t := fresh "t" in let Ht := fresh "Ht" in naming Ht t t';
    induction H;
    try discriminate Hs; try simplify_eq Hs;
    try discriminate Ht; try simplify_eq Ht;
    intros; subst
  end.

Lemma sub_refl : forall V (G:env V) t, WF G -> G |-- t << t.
Proof.
induction t; intro; auto.
Qed.

Lemma sub_WF : forall V (G:env V) s t,
  G |-- s << t -> WF G.
Proof.
induction 1; assumption.
Qed.
Hint Immediate sub_WF.

Lemma sub_weakening : forall W (D:env W) (s t:ftype W),
  D |-- s << t -> forall V (G:env V) (f:W->V),
  G extends D along f -> G |-- %f s << %f t.
Proof.
induction 1; simpl; intros; eauto.
apply SA_Trans_TVar. rewrite (RWF_commute H0). auto.
Qed.

Definition trans_prop V (q:ftype V) : Prop :=
  forall W (f:V->W) G s t, G |-- s << %f q -> G |-- %f q << t -> G |-- s << t.

Definition agrees_outside V (D E:env V) x : Prop :=
  forall y, y = x \/ D y = E y.
Notation "D 'agrees' 'with' E 'outside' x" := (agrees_outside D E x) (at level 70).

Lemma narrowing_lemma : forall V (q:ftype V) (trs : trans_prop q)
  W (D':env W) m n (Hq : D' |-- m << n) (G:env V) (D:env W) (f:^V->W)
  (Hf : D agrees with D' outside f None) p
  (RWFp : D extends G&p along f) (RWFq : D' extends G&q along f),
  G |-- p << q -> D |-- m << n.
Proof.
unfold agrees_outside.
induction q; intros;
(induction Hq; constructor; eauto; rename V0 into W; rename G0 into D';
 try (rename x into w || rename y into w);
 [ destruct (Hf w) as [Hy | Hw]; [ idtac | rewrite Hw; eauto];
   match goal with
   | [ HH : ?G |-- ?p << ?q |- _ ] =>
     assert (Hw : D' w = %(fun x => f (Some x)) q);
     [ subst w; rewrite (RWF_commute RWFq); simpl;
       repeat rewrite ftype_map_comp; auto
     | idtac ]
   end;
   apply (@trs _ (fun x => f (Some x)));
   [ replace (D w) with (%(fun x => f (Some x)) p);
     [ eapply sub_weakening; eauto; eapply RWF_trans; eauto
     | subst w; rewrite (RWF_commute RWFp); simpl;
       rewrite ftype_map_comp; reflexivity ]
     | simpl in * |- *; rewrite <- Hw; eauto ]
 | apply IHHq2 with (fun x => Some (f x)); auto;
   destruct y; simpl; auto; destruct (Hf w); auto ]).
Qed.

Lemma transitivity_lemma : forall V (q:ftype V), trans_prop q.
Proof.
induction q; red; intros;
  subinversion H; subinversion H0; constructor; eauto 4.
eapply IHq2 with (f:=^f); auto.
apply narrowing_lemma with (G:=G) (D':=G & %f q1) (q:=%f q1) (p:=t1)
  (f:=fun x : ^V0 => x); eauto.
red; intros.
rewrite ftype_map_comp in H2. rewrite ftype_map_comp in H3. eauto.
intro. destruct y; simpl; auto.
Qed.

Lemma narrowing : forall V (G:env V) W (D D':env W) (f:^V->W) p q m n,
  D agrees with D' outside f None ->
  D extends G&p along f -> D' extends G&q along f ->
  D' |-- m << n -> G |-- p << q -> D |-- m << n.
Proof.
pose transitivity_lemma. pose narrowing_lemma; eauto.
Qed.

Lemma transitivity : forall V (G:env V) s q t,
  G |-- s << q -> G |-- q << t -> G |-- s << t.
Proof.
intros.
apply transitivity_lemma with (q := q) (f := fun x : V => x);
rewrite ftype_map_id; auto.
Qed.