Arthur Charguéraud - May 2006
The key idea of the solution has alreay been presented.
In this document, we will give detailed explainations of the definitions, proofs and tactics used.
Some sections of this document are explained on slides. Those slides cover:
We will write "See the slides" to refer to those illustrations.
We will follow the structure of the COQ file:
In Appendix:
In this document:
[X := U]T" is a notation for "update X U T"
In the COQ file:
<: (ie safe subtyping)
<¤ (ie the unsafe subtyping)
S X" means "1+X" (defined by COQ)
Set Implicit Arguments. Unset Strict Implicit.
These lines tells that we do not need to give all arguments if some of them can be deduced from the others. We use this to make functions easier to work with. Let's see on an example. We have a proposition:
Lemma weaken_preserves_sub : forall (X : nat) (T1 T2 : typ),
T1 <¤ T2 -> (weaken X T1) <¤ (weaken X T2).
And also we have an hypothesis H of type "U1 <¤ U2", and we would like to give "(weaken Y U1) <¤ (weaken Y U2)" as parameter to another function. Then we shall give to that function the result of lemma weaken_preserves_sub applied to X U1 U2 and U1 <¤ U2. Without implicit arguments, we would write
weaken_preserves_sub Y U1 U2 H
Turning implicit arguments on, COQ is able to guess when we give H to find out that we wanted T1=U1 and T2=U2. Thus we just need to write:
weaken_preserves_sub Y H
Require Import Arith. Require Import Omega.
Those two lines let us access tactic "omega", an automatic decision procedure for Presburger arithmetic. We use it to prove some simple equalities or inequalities, or to find a contradiction in a set of such relations.
Ltac naming E e expr :=
set (e := expr) in * |- *; assert (E : e = expr);
[ trivial | clearbody e ].
Call "naming E e expr" with E and e fresh identifiers and expr being a term. This tactic introduce the equality "E : e = expr" in the context, and replace all occurences of expr by e, both in the goal and in the premisses. This tactic is used to rewrite hypotheses that are used in inductions or in inversions.
Ltac func_equal :=
(match goal with
| [ |- (?F _ = ?F _ ) ] => apply (f_equal F)
| [ |- (?F _ _ = ?F _ _) ] => apply (f_equal2 F)
| _ => idtac
end); auto.
This tactif expects a goal of the form "f x1 x2 .. xN = f y1 y2 .. yN", where f is either a function or a inductive contructor, and generates subgoals xi = yi for all i. This tactic just a convenient way to call COQ tactics "f_equal", "f_equal2", "f_equal3" and so on.
Ltac absurd_maths := intros; assert False; [ omega | contradiction ].
This tactic proves a goal when there exists a contradiction between some of the hypothesis using basic operators such as '=', '+', 'S', '<', '<=' and '>'. This tactic is useful to discriminate impossible cases when doing comparison of De Bruijn indices.
Tactic Notation "change_maths" constr(T) "with" constr(U) :=
replace T with U; [ idtac | omega ].
This tactic let us replace a mathematical expression by another one, with the same value. Example of use:
change_maths (S (S X + Y)) with (S (0+(1+X+Y)))
See the slides for the definitions.
Weaken X does insert 1+X variable in the environment:
Fixpoint weaken (X : nat) (T : typ) {struct X} : typ :=
match X with
| O => insert 0 T
| S P => insert 0 (weaken P T)
end.
So why didn't we simply insert X variables in the environment?
Fixpoint weaken (X : nat) (T : typ) {struct X} : typ :=
match X with
| O => T
| S P => insert 0 (weaken P T)
end.
The reason is that a good number of results that we need (for the crossing lemmas) are of the form:
forall X > 0, ... some property about (weaken X)
And it makes life much easier in COQ to have:
forall X >= 0, ... some property about (weaken (1+X))
Becauses this translates as "forall (X : nat)" and does not require any extra hypothesis.
In our definition of update, the type U is carried down to the place we want to use it, going through 1+Y bindings, and then at this point it is weakened by inserting 1+Y variables in the environment.
Fixpoint update (X : nat) (U : typ) (T : typ) {struct T} : typ :=
| all T1 T2 => all (update X U T1) (update (S X) U T2)
| var Y T1 => var Y (if eq_nat_dec X Y then weaken Y U
else update X U T1)
There is an equivalent way of doing this which is to weaken U once each time we pass a binding. It would be:
Fixpoint update (X : nat) (U : typ) (T : typ) {struct T} : typ :=
| all T1 T2 => all (update X U T1) (update (S X) (insert 0 U) T2)
| var Y T1 => var Y (if eq_nat_dec X Y then insert 0 U
else update X U T1)
The reason we prefer the first technique is that it simplifies the proofs. Indeed, we don't need to invoke a crossing lemma each time we pass through a binding, we only need to do this at the end on the variable.
Ltac analyse_update H :=
match type of H with ?R = update ?X ?U ?T =>
destruct T; try discriminate; simpl update in H;
try (injection H; intros; clear H)
end.
This is an elaborated inversion tactic for function update, to capture the fact that update go through types and only modify labels. We give an example:
Input:
H : arrow U1 U2 = update X U T
Output:
H1 : T = arrow T1 T2
H2 : U1 = T1
H3 : U2 = T2
Tactic Notation "ind_on_weaken" ident(X) :=
intro X; induction X as [ | X IHX ]; intros;
simpl weaken; auto.
This one is used to prove a property about "weaken X" by induction on X. It simply helps to perform the induction, doing the necessary introductions and simplifications, and solving easy cases.
This part is rather technical, and we are not going to get into all details, but just provide a little summary and give an example:
Let's look at the proof of the crossing lemma insert_above_insert (the actual paper proof is detailed in the next section, here we just show how the tactics prove the lemma).
Lemma insert_above_insert : forall (T : typ) (X Y : nat),
insert (S (X + Y)) (insert X T) = insert X (insert (X + Y) T).
We call ind_for_cross, which solves all cases but the one where T is a variable:
IHT : forall X Y : nat, insert (S (X + Y)) (insert X T)
= insert X (insert (X + Y) T)
_______________________________________________________(1/1)
insert (S (X + Y)) (insert X (var n T))
= insert X (insert (X + Y) (var n T))
Then we call case_insert_update, which splits according to comparison between indices:
E : X <= n E0 : S (X + Y) <= S n E1 : X + Y <= n E2 : X <= S n ________________________________________________(1/3) var (S (S n)) (insert (S (X + Y)) (insert X T)) = var (S (S n)) (insert X (insert (X + Y) T)) E : X <= n E0 : S (X + Y) > S n E1 : X + Y > n ________________________________________________(2/3) var (S n) (insert (S (X + Y)) (insert X T)) = var (S n) (insert X (insert (X + Y) T)) E : X > n E0 : S (X + Y) > n E1 : X + Y > n ________________________________________________(3/3) var n (insert (S (X + Y)) (insert X T)) = var n (insert X (insert (X + Y) T))
All these cases are easily solved using the induction hypothese IHT which is available (but not shown here) in the three cases.
The final proof of this lemma is:
ind_for_cross. case_insert_update; use IHT.
Now let's see the proof of the crossing lemma insert_above_insert:
Lemma insert_below_weaken : forall (X Y : nat) (T : typ),
insert X (weaken (X+Y) T) = weaken (1+X+Y) T.
We call tactic ind_on_weaken X, which solves the base case and leaves us with:
IHX : forall (Y : nat) (T : typ),
insert X (weaken (X + Y) T) = weaken (S (X + Y)) T
__________________________________________________________(1/1)
insert (S X) (insert 0 (weaken (X + Y) T))
= insert 0 (insert 0 (weaken (X + Y) T))
This is a instance of lemma insert_above_insert that we have just proved, modulo the invokation of IHX.
For some reasons we need to explicitely tell COQ that X is equal to (X+0) before we can call "rewrite insert_above_insert", and that's what tactic rewrite_for_0 helps us to do.
The final proof of this lemma is:
ind_on_weaken X. rewrite_for_0 X insert_above_insert. use IHX.
See the slides for the proof graph of all the crossing lemmas, and also the illustration of the proof for the first crossing lemma. In this section we detail the proofs. We show the full details of the induction on types only for the first lemma, it goes exactly the same way in all other lemmas that use the "ind_for_cross" tactic. In the proofs, we don't detail what happens for the labels of the variables, since it is always just an application of the induction hypothesis.
Lemma insert_on_insert :
insert X (insert (X+Y) T) = insert (1+X+Y) (insert X T).
by induction on T
- case top:
LHS = top
RHS = top
- case arrow:
LHS = arrow (insert X (insert X+Y) T1) (insert X (insert X+Y) T2)
RHS = arrow (insert (1+X+Y) (insert X T1)) (insert (1+X+Y) (insert X T2))
apply each of the two induction hypotheses
- case all:
LHS = all (insert X (insert X+Y) T1) (insert 1+X (insert 1+X+Y) T2)
RHS = all (insert (1+X+Y) (insert X T1)) (insert (1+1+X+Y) (insert (1+X) T2))
apply each of the two induction hypotheses, IH2 with X+1 instead of X
- case var Z:
- case X <= Z:
- case X+Y <= Z
LHS = 1+1+Z (using X <= 1+Z)
RHS = 1+1+Z (using 1+X+Y <= 1+Z)
- case X+Y > Z
LHS = 1+Z
RHS = 1+Z (using 1+Z < 1+X+Y)
- case X > Z:
LHS = Z (using Z < X+Y)
RHS = Z (using Z < 1+X+Y)
Lemma insert_below_weaken :
insert X (weaken (X+Y) T) = weaken (1+X+Y) T
by induction on X (case 0 is trivial):
insert (1+X) (weaken (1+1+X+Y) T) then by def of weaken
= insert (1+X) (insert 0 (weaken (1+X+Y) T)) then by insert_on_insert
= insert 0 (insert X (weaken (X+Y) T)) then by IH
= insert 0 (weaken (1+X+Y) T) then by def of weaken
= weaken (1+1+X+Y) T
Lemma insert_above_weaken :
insert (1+X+Y)) (weaken X T) = weaken X (insert Y T).
by induction on X (case 0 is trivial):
insert (1+1+X+Y) (weaken (1+X) T) then by def of weaken
= insert (1+1+X+Y) (insert 0 (weaken X T)) then by insert_on_insert
= insert 0 (insert (0+1+X+Y) (weaken X T)) then by IH
= insert 0 (weaken (X (insert Y T)) then by def of weaken
= weaken (1+X) (insert Y T)
Lemma insert_above_weaken :
update X U (insert X T) = insert X T.
by induction on X T:
- case T = var Z T1:
update X U (insert X (var Z T1)) = insert X (var Z T1)
- case X <= Z
LHS: Z+1 (using X <> Z+1)
RHS: Z+1
- case X > Z
LHS: Z
RHS: Z
Lemma update_above_insert :
update (1+X+Y) U (insert X T) = insert X (update (X+Y) U T).
- case Z = 1+X+Y:
LHS = weaken (1+X+Y) U (using 1+Z = 1+X+Y)
RHS = insert X (weaken (X+Y) U)
conclude using insert_below_weaken
- case Z <> X+Y
- case X <= Z
LHS = 1+Z (using 1+Z <> 1+X+Y)
RHS = 1+Z
- case X > Z
LHS = Z
RHS = Z
Lemma insert_above_update :
insert (1+X+Y) (update X U T) = update X (insert Y U) (insert (1+X+Y) T).
- case Z = Y:
LHS = insert (1+X+Y) (weaken Y U)
RHS = weaken X (insert Y U) (using 1+X+Y <> X)
conclude using insert_above_weaken
- case Z <> Y
- case 1+X+Y <= Z
LHS = 1+Z
RHS = 1+Z (using 1+Z <> X)
- case 1+X+Y > Z
LHS = Z
RHS = Z
Lemma update_below_weaken :
update X U (weaken (X+Y) T) = weaken (X+Y) T.
by induction on X:
- case X = 0
goal = update 0 U (weaken Y T) = weaken Y T.
by induction on Y
- case Y = 0
goal = update 0 U (insert 0 T) = insert 0 T.
this is update_at_insert
- case Y = Y'+1
trivial using induction hypothesis
- case X = X'+1
update (1+X) U (weaken (1+X+Y) T) then by def of weaken
= update (1+X) U (insert 0 (weaken (X+Y) T)) then by update_above_insert
= insert 0 (update X U (weaken (X+Y) T)) then by IHX
= insert 0 (weaken (X+Y) T) then by def of weaken
= weaken (1+X+Y) T.
Lemma update_above_weaken =
update (1+X+Y) U (weaken X T) = weaken X (update Y U T).
by induction on X
- case X = 0
update (1+Y) U (insert 0 T) = insert 0 (update Y U T).
this is an instance of update_above_insert
- case X = X'+1
update (1+1+X+Y) U (weaken (1+X) T) then by def of weaken
= update (1+1+X+Y) U (insert 0 (weaken X T)) then by update_above_insert
= insert 0 (weaken X (update Y U T)) then by IHX
= weaken (1+X) (update Y U T).
Lemma update_above_update :
update (1+X+Y) P (update X U T) = update X (update Y P U) (update (1+X+Y) P T).
by induction on T
- case var Z:
- case Z = X, Z = 1+X+Y
contradiction
- case Z = X, Z <> 1+X+Y
LHS = update (1+X+Y) P (weaken X U)
RHS = update X (update Y P U) Z
RHS = weaken X (update Y P U)
conclude using update_above_weaken
- case Z <> X, Z = 1+X+Y
LHS = weaken (1+X+Y) P
RHS = update X (update Y P U) (weaken (1+Y+X) P)
conclude using update_below_weaken
- case Z <> X, Z <> 1+Y+X
LHS = Z
RHS = Z
See the slides for the intuition.
Lemma insert_on_push :
insert (1+X) (push P T) = push (insert X P) (insert (1+X) T).
insert (1+X) (push P T) then by def of push
= insert (1+X) (update 0 P T) then by insert_above_update
= update 0 (insert X P) (insert (1+X)) T) then by def of push
= push (insert X U) (insert (1+X) T)
Lemma update_on_push :
update (S X) U (push P T) = push (update X U P) (update (S X) U T)
update (S X) U (push P T) then by def of push
= update (S X) U (update 0 P T) then by update_above_update
= update 0 (update X U P) (update (S X) U T) then by def of push
= push (update X U P) (update (S X) U T)
Lemma update_at_weaken : update X U (weaken X T) = weaken X T. this is an instance of update_below_weaken
Lemma update_and_equality : update X P T1 = update X P T2 -> update X Q T1 = update X Q T2. by induction on T1 with a case analysis on T2 using the analyse_update tactic
The point of writing these tactics is to get a clear distinction between the arguments used in the induction on the size and the induction on the abstract notion of type. We will use these tactics to prove both reflexivity and transitivity of subtyping.
This tactic takes a goal of the form "forall (T : typ), P T", where P is some property over types. It proves it by induction on the size of T. The new goal states that property P is true for all T of size less than s, this statement holding for all size s:
forall (s : nat) (T : typ), size T < s -> P T
We then invoke an induction on the natural s, and solve the case s = 0 by contradiction. It leaves:
IHs : forall T : typ, size T < s -> P T
T : typ
Hs : size T < S s
______________________________________
P T
To see this tactic in action on sub_reflexivity, you may use the debug mode, or simply expand the tactic:
Lemma sub_reflexivity' : forall (T : typ), T <¤ T.
intro T. generalize (lt_n_Sn (size T)).
naming E s (S (size T)). generalize T. clear E T.
induction s as [ | s IHs T Hs ]. intros. absurd_by_omega.
induction T; fix_ind_on_size_hypotheses IHs Hs; auto.
To prove the goal stated above, we would then have an induction on T. This generates one subgoal for each constructor of the inductive structure "typ". We detail the case of arrow to illustrate the working of the tactic that "fixes" induction hypotheses. Here is the goal:
T1 : typ
T2 : typ
IHT1 : size T1 < S s -> P T1
IHT2 : size T2 < S s -> P T2
Hs : size (arrow T1 T2) < S s
______________________________________
P (arrow T1 T2)
The induction hypotheses are not very nice looking. We would like to have the "standard" induction hypotheses which are simply:
IH1 : P T1
IH2 : P T2
______________________________________
P (arrow T1 T2)
But this is not quite enough. To go through operations that preserve size, we'll need two other versions, more general:
IH1': forall T1' : typ, size T1' = size T1 -> P T1'
IH2': forall T2' : typ, size T2' = size T2 -> P T2'
______________________________________
P (arrow T1 T2)
Our tactic is going to remove hypotheses IHT1, IHT2 and Hs from the context and replace them by IH1 and IH2. To do this, it uses the omega tactic to prove that Hs implies "size T1 < S s", and then it applies it to IHT1 and IHT2, and obtains exactly IH1 and IH2.
Let's look at what happens for the case of abstraction $X<¤T1.T2 (the one we did all this work for). We transform the goal:
T1 : typ
T2 : typ
IHT1 : size T1 < S s -> P T1
IHT2 : size T2 < S s -> P T2
Hs : size (all T1 T2) < S s
______________________________________
P (all T1 T2)
By this one:
IH1 : P T1
IH2 : forall U : typ, P (push U T2)
IH1': forall T1' : typ, size T1' = size T1 -> P T1'
IH2': forall T2' : typ, size T2' = size T2 -> P T2'
______________________________________
P (all T1 T2)
IH2 states that the property P holds on T2 whatever label is being attached to all instances of X in T2. It is more general than the induction hypothesis "P (push T1 T2)", and we need this flexibility to prove sub_substitution and sub_transitivity.
See the presentation of the solution.
See the slides for the proof graph.
Lemma insert_preserves_sub : forall (X : nat) (T1 T2 : typ),
T1 <¤ T2 -> (insert X T1) <¤ (insert X T2).
we prove that:
forall (X : nat), (insert X S) <¤ (insert X T)
by induction on the derivation of S <¤ T
we need to use insert_on_push to go through the binding in case SA_all
Lemma weaken_preserves_sub : forall (X : nat) (T1 T2 : typ), T1 <¤ T2 -> (weaken X T1) <¤ (weaken X T2). by induction on X, using insert_preserves_sub for both cases
Lemma narrow_preserves_sub : (assuming transitivity holds)
[X := Q]S <¤ [X := Q]T -> P <¤ Q ->
[X := P]S <¤ [X := P]T
Proof by induction on the first unsafe subtyping derivation, with induction hypothesis:
forall X S T,
U = [X := Q]S ->
V = [X := Q]T ->
[X := P]S <¤ [X := P]T
- in this case, V = top - rewriting this into V = [X := Q]T gives: Top = [X := Q]T - by an inversion argument, we have: T = top - rewriting the goal then gives: [X := P]S <¤ top - and we solve it by SA-Top
- in this case, U = U1->U2 and V = V1->V2
and we also have: V1 <¤ U1 and U2 <¤ V2
- IH1 looks like:
U1 = [X' := Q]S' ->
V1 = [X' := Q]T' ->
[X' := P]S' <¤ [X' := P]T'
IH2 looks the same, replacing U1 and V1 by U2 and V2.
- our goal is [X := P](S1->S2) <¤ [X := P](T1->T2)
which simplify the substitution expands to:
[X := P]S1 -> [X := P]S2 <¤ [X := P]T1 -> [X := P]T2
- an inversion argument on U1->U2 = [X := Q]S gives S = S1->S2
an inversion argument on V1->V2 = [X := Q]T gives T = T1->T2
- unfolding the definition of change in the above relation gives:
U1 = [X := Q]S1 and U2 = [X := Q]S2
V1 = [X := Q]T1 and V2 = [X := Q]T2
- we apply the two induction hypotheses to get:
[X := P]T1 <¤ [X := P]S1
[X := P]S2 <¤ [X := P]T2
and we can conclude with SA-Arrow
- in this case, U = $Y<¤U1.U2 and $Y<¤V1.V2
and we also have: V1 <¤ U1 and (push V1 U2) <¤ (push V1 V2)
- IH1 looks like:
U1 = [X' := Q]S' ->
V1 = [X' := Q]T' ->
[X' := P]S' <¤ [X' := P]T'
IH2 looks like:
(push V1 U2) = [X' := Q]S' ->
(push V1 V2) = [X' := Q]T' ->
[X' := P]S' <¤ [X' := P]T'
- an inversion argument on $Y<¤U1.U2 = [X := Q]S gives S = $Y<¤S1.S2
an inversion argument on $Y<¤V1.V2 = [X := Q]T gives T = $Y<¤T1.T2
- unfolding the definition of change in the above relation gives:
U1 = [X := Q]S1 and U2 = [X+1 := Q]S2
V1 = [X := Q]T1 and V2 = [X+1 := Q]T2
- our goal rewrites as:
[X := P]($Y<¤S1.S2) <¤ [X := P]($Y<¤T1.T2)
which is after unfolding substitution gives:
$Y<¤[X:=P]S1.[X+1:=P]S2 <¤ $Y<¤[X:=P]T1.[X+1:=P]T2
- to prove this result, we apply SA-All, and we have two subgoals:
[X:=P]T1 <¤ [X:=P]S1
push ([X:=P]T1) ([X+1:=P]S2) <¤ push ([X:=P]T1) ([X+1:=P]T2)
- the first one is the immediate application of IH1,
but to apply the second one, we need just a little more work.
we use lemma update_on_push, which is:
[X+1:=P](push S T) = push ([X:=P]S) ([X+1:=P]T).
- the new subgoal is then
[X+1:=P](push T1 S2) <¤ [X+1:=P](push T1 T2)
which we prove using IH2, with
X as X+1
S' as (push T1 S2)
T' as (push T1 T2)
and we need to prove the two premisses of IH2:
push V1 U2 = [X+1 := Q](push T1 S2)
push V1 V2 = [X+1 := Q](push T1 T2)
- we apply lemma update_on_push again, to get
push V1 U2 = push ([X := Q]T1) ([X+1 := Q]S2)
push V1 V2 = push ([X := Q]T1) ([X+1 := Q]T2)
and we can conclude by applying f_equal2 and the initial assumptions
- in this case, U = Y^R and V = Y^R
- an inversion argument on Y^R = [X := Q]S gives S = YS^MS
an inversion argument on Y^R = [X := Q]T gives T = YT^MT
- the goal is [X := P](YS^MS) <¤ [X := P](YT^MT)
- there are four possible cases from the comparison of X with YS and YT.
* Case X = YS = YT
The goal rewrites as P <¤ P, and is solved by reflexivity of subtyping
* Case X = YS and X <> YT
U = [X := Q]S gives Y^R = X^Q
V = [X := Q]T gives Y^R = YT^MT
This is absurd since X and YT were assumed to be different
* Case X <> YS and X = YT
Symmetric to the previous case, also absurd.
* Case X <> YS and Y <> YT
U = [X := Q]S gives Y^R = YS^([X := Q]MS)
V = [X := Q]T gives Y^R = YT^([X := Q]MT)
By injection, we get:
Y = YS = YT
R = [X := Q]MS = [X := Q]MT
And our goal is
Y ^ [X := P]MS <¤ Y ^ [X := P]MT
We prove it by subreflexivity as soon as we can prove
[X := P]MS = [X := P]MT
And this is given by lemma update_and_equality, which states that:
[X := Q]MS = [X := Q]MT -> [X := P]MS = [X := P]MT
- in this case, U = Y^R and we have R <¤ V
we have U = [X := Q]S and V = [X := Q]T
- the induction hypothesis looks like:
R = [X' := Q]S' ->
V = [X' := Q]T' ->
[X' := P]S' <¤ [X' := P]T'
- an inversion argument on Y^R = [X := Q]S gives S = Z^M
so the goal is now: [X := P](Z^M) <¤ [X := P]T
- there are two possible cases accoarding to comparison of X and Z:
* Case X = Z
- we can rewrite U = [X := Q]S as Y^R = X^(weaken X Q)
then by injection Y = X and R = weaken X Q,
also hypothesis R <¤ V can be rewritten as (weaken X Q) <¤ V
- our goal gets simplified to X^(weaken X P) <¤ [X := P]T
which by SA-trans-tvar gives: (weaken X P) <¤ [X := P]T
- we prove this by transitivity:
(weaken X P) <¤ (weaken X Q) <¤ [X := P]T
which we can do this we have assumed transitivity for all weaken of Q
this gives two subgoal:
(weaken X P) <¤ (weaken X Q)
(weaken X Q) <¤ [X := P]T
- the first subgoal is just weaken_preserves_sub applied to P <¤ Q
- to prove the second subgoal we instanciate the induction hypothesis with
X'=X, S'=(weaken X Q), T'=T:
weaken X Q = [X := Q](weaken X Q) ->
V = [X := Q]T ->
[X := P](weaken X Q) <¤ [X := P]T
- then we use two equalities given by update_at_weaken:
[X := P](weaken X Q) = (weaken X Q)
[X := Q](weaken X Q) = (weaken X Q)
to rewite this induction hypothesis as
V = [X := Q]T -> (weaken X Q) <¤ [X := P]T
- this is our goal, and the premise is an earlier hypothesis
* Case X <> Z
- our goal rewrites as: Z^([X>>P]M) <¤ [X := P]T
- and we can rewrite Y^R = [X := Q](Z^M) as Y^R = Z^([X>>X^Q]M)
- which by injection gives us Y = Z and R = [X>>X^Q]M
- we apply the induction hypothesis with S'=M and get:
[X := P]M <¤ [X := P]T
- now the goal is the application of SA-Trans-Tvar to this judgment
Lemma sub_transitivity : forall (Q S T : typ), S <¤ Q -> Q <¤ T -> S <¤ T
We prove this with an induction on the size of Q. In this induction, we have an induction on the first subtyping judgment, and a nested inversion on the second subtyping judgment.
All cases are solved by auto, but the case SA-All that we shall detail here.
- we have the following relations:
S = $X<¤S1.S2
Q = $X<¤Q1.Q2
T = $X<¤T1.T2
Q1 <¤ S1
(push Q1 S2) <¤ (push Q1 Q2)
T1 <¤ Q1
(push T1 Q2) <¤ (push T1 T2)
- IH1 looks like:
S' <¤ Q1 -> Q1 <¤ T' -> S' <¤ T'
IH2 looks like:
S' <¤ (push Q1 Q2) -> (push Q1 Q2) <¤ T' -> S' <¤ T'
IH2' is a generalization of IH2 and it looks like:
size R = size Q2 -> S' <¤ R -> R <¤ T' -> S' <¤ T'
- using IH1 with S'=T1 and T'=S1 gives
T1 <¤ S1
- on hypothesis (push Q1 S2) <¤ (push Q1 Q2)
apply update_preserves_sub with X = 0 and T1 <¤ Q1 to get:
(push T1 S2) <¤ (push T1 Q2)
- now apply IH2' with R = push T1 Q2 (noticing that push preserves size)
to prove the transitivity on the relations:
(push T1 S2) <¤ (push T1 Q2) <¤ (push T1 T2)
- we prove the goal applying SA-All to the two hypothesis that we have proven:
T1 <¤ S1
(push T1 S2) <¤ (push T1 T2)
First we define what transitivity and narrowing are:
Definition sub_trans_prop (Q : typ) :=
forall (S T : typ), S <¤ Q -> Q <¤ T -> S <¤ T.
Definition narrow_preserves_sub_prop (Q : typ) :=
forall (X : nat) (P S T : typ), P <¤ Q ->
(update X Q S) <¤ (update X Q T) -> (update X P S) <¤ (update X P T).
The we define the following statement: a proposition G holds for all possible weakening of a type T. Here it is:
Definition true_for_weaken_of T G := forall X, G (weaken X T).
First we prove narrowing assuming transitivity holds for all weakening of its argument:
Lemma narrow_preserves_sub_when_trans : forall (Q : typ),
true_for_weaken_of Q sub_trans_prop -> narrow_preserves_sub_prop Q.
Then we prove transitivity, using the result about narrowing:
Lemma sub_transitivity : forall (Q : typ), sub_trans_prop Q.
Finally, we could prove narrowing without the transitivity hypothesis:
Lemma narrow_preserves_sub : forall Q, narrow_preserves_sub_prop Q.
intro Q. apply (narrow_preserves_sub_when_trans (Q := Q)).
unfold true_for_weaken_of. intro X. apply sub_transitivity.
Qed.
However we don't bother doing it, since narrowing is only used for transitivity.
See the presentation of the solution, and also the slides.
See the presentation of the solution.
See the presentation of the solution.
The first implication is easy: we extract induction hypotheses given for the root, and then have an induction to prove the unsafe relation. In the induction, we only need to forget about well-formation statements, so "auto" solves it easily.
Lemma subtyping_to_sub : forall (E : env) (S T : typ),
E |- S <: T -> wf_env E /\ wf E S /\ wf E T /\ S <¤ T.
intros. repeat split; induction H; auto.
Qed.
The other way needs just a little more work. We need to carry the well-formation hypotheses as we explore the unsafe subtyping relation and want to reconstruct the safe subtyping relation. The difficulty is to desconstruct well-formation hypotheses at each step: this is what the two inversions are for.
Lemma sub_to_subtyping : forall (S T : typ), S <¤ T ->
forall (E : env), wf_env E -> wf E S -> wf E T -> E |- S <: T.
intros S T H. induction H; intros E wfE wfS wfT;
inversion wfS; auto; inversion wfT; auto.
Qed.
See the presentation of the solution.
Note: those figures as accurate to 2 or 3 units.
71 lines of proof (among which 20 are for narrowing) 80 lines of tactics 57 lines of lemmas statements 28 lines of functions definitions 50 lines of inductive definitions 12 lines of meta controls 26 lines containg just "Qed" (i.e. the end of the proof of a lemma) ------ 329 lines in total (without blank lines and comments)
I haven't tried to handle part 1B and add records, but I did add pairs. It took 5 minutes, and here is the list of changes:
More precisely, here is the (beautified) diff:
+ | pair : typ -> typ -> typ. + | pair T1 T2 => pair (insert X T1) (insert X T2) + | pair T1 T2 => pair (update X U T1) (update X U T2) - induction T as [ | T1 IHT1 T2 IHT2 | T1 IHT1 T2 IHT2 | ]; intros X Y; + induction T as [ | T1 IHT1 T2 IHT2 | T1 IHT1 T2 IHT2 | | ]; intros X Y; + | simpl; rewrite (IHT1 X Y); rewrite (IHT2 X Y); reflexivity ]). + | pair T1 T2 => 1 + (size T1) + (size T2) + | pair ?T1 ?T2 => fix_ih T1; fix_ih T2 + | SA_prod : forall (T1 T2 U1 U2 : typ), + T1 <¤ U1 -> T2 <¤ U2 -> (pair T1 T2) <¤ (pair U1 U2) - induction H as [ | | | Y T1 | Y R V RsubV IH X ]; intros. + induction H as [ | | | Y T1 | Y R V RsubV IH X | ]; intros. + (* case SA_Prod *) + analyse_update DU. analyse_update DV. simpl. auto. + | wf_prod : forall (E : env) (T1 T2 : typ), + wf E T1 -> wf E T2 -> wf E (pair T1 T2). + | SA_Prod : forall (E : env) (T1 T2 U1 U2 : typ), + wf_env E -> wf E (pair T1 T2) -> wf E (pair U1 U2) -> + E |- T1 <: U1 -> E |- T2 <: U2 -> + E |- (pair T1 T2) <: (pair U1 U2)