Library Part1a
Authors: Andre' Hirschowitz and Marco Maggesi
Web page: http://www.math.unifi.it/~maggesi/fsub/
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.
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.
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.
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.
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.