(** * PoplMark Challenge: Solution to part 1A. *)
(** Authors: Andre' Hirschowitz and Marco Maggesi *)
(** Web page: http://www.math.unifi.it/~maggesi/fsub/ *)

(** * Preliminaries. *)

(** This section contains miscellaneous definitions, lemmas and tactics which
    are not specific to the ``Fsub'' system (they could have been defined in
    the Coq Standard Library). *)

Set Implicit Arguments.

Ltac congr :=
  match goal with
  | [ |- (?F _ = ?F _ ) ] => apply (f_equal F)
  | [ |- (?F ?x _ = ?F ?x _) ] => apply (f_equal (F x))
  | [ |- (?F _ _ = ?F _ _) ] => apply (f_equal2 F)
  | [ |- (?F ?x _ _ = ?F ?x _ _) ] => apply (f_equal2 (F x))
  | [ |- (?F _ _ _ = ?F _ _ _) ] => apply (f_equal3 F)
  end;
  trivial.
Hint Extern 1 (?x = ?y) => congr.

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

(** The empty type. *)

Inductive empty : Type := .

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

(** Composition of functions. *)

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).

(** Equality for functions. *)

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).

(** Some definitions and lemmas about [option]. *)

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.

(** * Type expressions. *)

(** We use nested data-types to encode variable binding in type expressions.
    For each type [X], our set [ftype X] represents the set of type
    expressions with free variables indexed by [X].  We call [X] the "context"
    of our type expressions and say that ``type expressions are stratified over
    contexts''. *)

Inductive ftype (X:Type) : Type :=
  | Top : ftype X
  | TVar : X -> ftype X
  | Arr : ftype X -> ftype X -> ftype X
  | Uni : ftype X -> ftype ^X -> ftype X.

(** The following definition and lemmas state that the mapping
    [ftype : Type -> Type] carries a natural structure of functor given by
    variable renaming.
    (Actually, [ftype] has a more rich structure of monad given by variable
    substitution, but we do not need to use this fact here.) *)

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

Fixpoint ftype_map X Y (f:X->Y) (t:ftype X) : ftype Y :=
  match t with
  | Top => Top Y
  | TVar x => TVar (f x)
  | Arr s t => Arr (%f s) (%f t)
  | Uni s t => Uni (%f s) (%(^f) t)
  end
where "% f" := (ftype_map f).

Lemma ftype_map_extens : forall X (s t:ftype X) (H:s=t) Y (f g:X->Y),
  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 X (t:ftype X) (f:X->X),
  (forall x, f x=x) -> %f t=t.
Proof.
induction t; simpl; intros; auto.
congr. auto.
apply IHt2. destruct x; simpl; auto.
Qed.

Lemma ftype_map_comp : forall X t Y (f:X->Y) Z (g:Y->Z),
  %g (%f t) = %(g o f) t.
Proof.
induction t; simpl; intros; auto.
repeat congr; rewrite IHt2. auto.
Qed.

(** * Environments for type expressions. *)

(** As for type expressions, type environments are stratified over contexts.
    They are encoded simply as maps [X -> ftype X] with an additional
    well-formedness condition [WF0] which is introduced later on.  The
    judgement [TVar x <: t \in G] is translated into the equation [G x = t]. *)

Definition env X := X -> ftype X.

(** The operation of adding a new binding in the environment is implemented by
    the following definition. *)

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

(** First we introduce a relative version of well-formedness, i.e., a ternary
    predicate [WF D G f] which expresses the property ``the environment [G]
    over the context [X] is well-formed with respect to the environment [D]
    over [Y] with the renaming defined by the map [f:Y->X]''. *)

Inductive WF : forall Y (D:env Y) X (G:env X) (f:Y->X), Prop :=
  | WF_inc : forall Y (D:env Y) X (G:env X) (f:Y->X) (g:X->ftype Y),
     (forall y:Y, D y = g (f y)) -> (forall x:X, G x = %f (g x)) -> WF D G f
  | WF_trans :
     forall X1 (G1:env X1) X2 (G2:env X2) X3 (G3:env X3)
       (f1:X1->X2) (f2:X2->X3) (f:X1->X3),
     (forall x, f2 (f1 x) = f x) -> WF G1 G2 f1 -> WF G2 G3 f2 -> WF G1 G3 f.

Lemma WF_commute : forall Y (D:env Y) X (G:env X) (f:Y->X),
  WF D G f -> forall y, G (f y) = %f (D y).
Proof.
induction 1; intros.
rewrite H. trivial.
rewrite <- H. rewrite IHWF2. rewrite IHWF1.
rewrite ftype_map_comp. auto.
Qed.

Lemma WF_extens : forall Y (D D':env Y) (HD : D==D')
  X (G G':env X) (HG : G==G') (f f':Y->X) (Hf : f==f'),
  WF D G f -> WF D' G' f'.
Proof.
induction 4.
apply WF_inc with g; intros.
rewrite <- (HD y). rewrite <- (Hf y). trivial.
rewrite <- (HG x). rewrite H0. apply ftype_map_extens; trivial.
apply WF_trans with (G2:=G2) (f1:=f1) (f2:=f2); auto.
intro. rewrite <- (Hf x). auto.
Qed.

Lemma WF_consenv : forall X (G:env X) (t:ftype X),
  WF G (G & t) (@Some X).
Proof.
intros. apply WF_inc with (g := default t G). reflexivity.
destruct x; reflexivity.
Qed.
Hint Resolve WF_consenv.

Lemma WF_WF_consenv : forall Y (D:env Y) X (G:env X) (f:Y->X) t,
  WF D G f -> WF D (G & t) (fun y => Some (f y)).
Proof.
intros. apply WF_trans with (2:=H) (f2:=@Some X); auto.
Qed.
Hint Resolve WF_WF_consenv.

Lemma WF_refl : forall X (G:env X) (f:X->X),
  (forall x, f x = x) -> WF G G f.
Proof.
intros.
apply WF_inc with (g:=G); intros.
rewrite H. reflexivity.
rewrite ftype_map_id; auto.
Qed.
Hint Resolve WF_refl.

Lemma WF_option_map : forall Y (D:env Y) X (G:env X) (f:Y->X) t,
  WF D G f -> WF (D & t) (G & %f t) ^f.
Proof.
induction 1.
apply WF_inc with (fun y => %(@Some Y) (default t g y)).
destruct y; simpl; auto.
destruct x; simpl; repeat rewrite ftype_map_comp; auto.
rewrite H0. rewrite ftype_map_comp. trivial.
apply WF_trans with (f1 := ^f1) (f2 := ^f2) (G2 := G2 & %f1 t); auto.
destruct x; simpl; auto.
eapply WF_extens with (4:=IHWF2 (%f1 t)); try split.
intro x; destruct x; simpl; repeat rewrite ftype_map_comp; unfold comp; auto.
Qed.
Hint Resolve WF_option_map.

(** An environment is well-formed if it is well-formed with respect to the
    empty environment (the environment over the empty context). *)

Definition WF0 X (G:env X) := WF (@empty_inc _) G (@empty_inc X).

Lemma WF0_trans : forall Y (D:env Y) X (G:env X) (f:Y->X),
  WF0 D -> WF D G f -> WF0 G.
Proof.
intros. unfold WF0.
apply WF_trans with (2:=H) (3:=H0).
destruct x.
Qed.
Hint Resolve WF0_trans.

Lemma WF0_consenv : forall X (G:env X) (t:ftype X),
  WF0 G -> WF0 (G & t).
Proof.
intros. unfold WF0.
apply WF_trans with (G2:=G) (f1:=empty_inc X) (f2:=@Some X); auto.
destruct x.
Qed.
Hint Resolve WF0_consenv.

(** ** Subtyping relation. *)

(** The subtyping judgement is encoded using an inductive predicate where each
    constructor corresponds to an inference rule. *)

Reserved Notation "G \- s << t" (at level 68, no associativity).

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

(** Unfortunately, we cannot make any useful use of the Coq built-in
    [inversion] for the [sub] inductive type.  So we implemented this rather
    crude alternative. *)

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.

(** Reflexivity of the subtyping. *)

Lemma sub_refl : forall X (G:env X) t, WF0 G -> G \- t << t.
Proof.
induction t; intro; auto.
Qed.

(** Adequacy of the subtyping, i.e., subtyping entails well-formedness. *)

Lemma sub_WF0 : forall X (G:env X) s t,
  G \- s << t -> WF0 G.
Proof.
induction 1; assumption.
Qed.
Hint Immediate sub_WF0.

(** Weakening lemma. *)

Lemma sub_weakening : forall Y (D:env Y) (s t:ftype Y),
  D \- s << t -> forall X (G:env X) (f:Y->X), WF D G f -> G \- %f s << %f t.
Proof.
induction 1; simpl; intros; eauto.
apply SA_Trans_TVar. rewrite (WF_commute H0). auto.
Qed.

(** * Proof of transitivity and narrowing lemma. *)

(** Following a schema found in the formalization by Chargueraud we divide the
    inductive proof transitivity and narrowing in two sub-lemmas, namely,
    [narrowing_lemma] and [transitivity_lemma].  The results in which we are
    actually interested are [narrowing] and [transitivity] which are easy
    consequences of these lemmas. *)

Definition trans_prop X (q:ftype X) : Prop :=
  forall Y (f:X->Y) G s t, G \- s << %f q -> G \- %f q << t -> G \- s << t.

Lemma narrowing_lemma : forall X (q:ftype X) (trs : trans_prop q)
  Y (Dq:env Y) m n (Hq : Dq \- m << n) (G:env X) (Dp:env Y) (f:^X->Y)
  (Hf : forall y, y = f None \/ Dp y = Dq y) p
  (WFp : WF (G & p) Dp f) (WFq : WF (G & q) Dq f),
  G \- p << q -> Dp \- m << n.
Proof.
induction q; intros;
(induction Hq; constructor; eauto; rename X0 into Y; rename G0 into Dq;
 try (rename x0 into v || rename x into v || rename y into v);
 [ destruct (Hf v) as [Hy | Hv]; [ idtac | rewrite Hv; eauto];
   match goal with
   | [ HH : sub ?G ?p ?q |- _ ] =>
     assert (Hv : Dq v = %(fun x => f (Some x)) q);
     [ subst v; rewrite (WF_commute WFq); simpl;
       repeat rewrite ftype_map_comp; auto
     | idtac ]
   end;
   apply (@trs _ (fun x => f (Some x)));
   [ replace (Dp v) with (%(fun x => f (Some x)) p);
     [ eapply sub_weakening; eauto; eapply WF_trans; eauto
     | subst v; rewrite (WF_commute WFp); simpl;
       rewrite ftype_map_comp; reflexivity ]
     | simpl in * |- *; rewrite <- Hv; eauto ]
 | apply IHHq2 with (fun x => Some (f x)); auto;
   destruct y; simpl; auto; destruct (Hf y); auto ]).
Qed.

Lemma transitivity_lemma : forall X (q:ftype X), 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) (Dq:=G & %f q1) (q:=%f q1) (p:=t1)
  (f:=fun x : ^X0 => x); eauto.
red; intros.
rewrite ftype_map_comp in H2. rewrite ftype_map_comp in H3. eauto.
destruct y; simpl; auto.
Qed.

Lemma narrowing : forall X (G:env X) Y (Dp Dq:env Y) (f:^X->Y) p q m n,
  (forall y, y = f None \/ Dp y = Dq y) ->
  WF (G & p) Dp f -> WF (G & q) Dq f ->
  Dq \- m << n -> G \- p << q -> Dp \- m << n.
Proof.
pose transitivity_lemma. pose narrowing_lemma; eauto.
Qed.

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