Almost have Church-Rosser ...
rpol...@inf.ed.ac.uk
I've almost finished a proof that parallel reduction has the diamond
property (.mod and .thm files are attached, which also have some random
facts about pr1 and cd1). I have one remaining problem (see the only
occurrence of "skip" in the .thm file).
Here is the problem. I want to prove:
Theorem pr1_subst_lem: forall A1 A2 B1 B2 L K J,
ctxs L K J ->
{K |- pr1 (abs A1) (abs A2)} -> {K |- pr1 B1 B2} ->
{K |- pr1 (A1 B1) (A2 B2)}.
The corresponding informal theorem is a "substitution lemma"
forall S1 S2 T1 T2 x. pr1 S1 S2 -> pr1 T1 T2 -> pr1 (S1[T1/x]) (S2[T2/x)
that is proved by induction on the first pr1 assumption. In that
proof, all cases are trivial except the contraction case, where the
proof uses the usual substitution lemma:
M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]
Thanks for help,
Randy
Andrew Gacek
The corresponding lemma to this informal one is the following,
Theorem pr1_subst_lem_alt: forall A1 A2 B1 B2 L K J, nabla x,
ctxs L K J ->
{K, pr1 x x |- pr1 (A1 x) (A2 x)} -> {K |- pr1 B1 B2} ->
{K |- pr1 (A1 B1) (A2 B2)}.
Note that nabla quantification is used for x since it represents a
variable and it should not, for example, be instantiated with a value
like (app ...) or (abs ...). Unfortunately, proving this theorem
directly in Abella is not completely direct since the unification
underlying the search tactic is only higher-order pattern unification
rather than full blown higher-order unification. Thus we will
sometimes need to construct goals explicitly rather than using the
search tactic. For this reason we introduce the trivial lemmas
pr1_clause2 and pr1_clause3. In the future, I should look at ways of
avoiding these issues.
Here's the full proof of pr1_subst_lem as you stated it. Please let me
know if you have any questions about it.
%% We introduce these clause lemmas to get around unification issues
%% which arise when applying the search tactic
Theorem pr1_clause3 : forall K T1 S1 T2 S2,
{K |- pr1 (abs T1) (abs T2)} -> {K |- pr1 S1 S2} ->
{K |- pr1 (app (abs T1) S1) (T2 S2)}.
intros. search.
Theorem pr1_clause2 : forall K S1 S2, nabla x,
{K, pr1 x x |- pr1 (S1 x) (S2 x)} -> {K |- pr1 (abs S1) (abs S2)}.
intros. search.
%% We use the hypothesis 'name x' to control which value gets
%% instantiated for x when the inductive hypothesis is applied.
%% In the future, Abella should support an "apply ... with x = n2"
%% style of tactic which eliminates the need for 'name x' here.
Theorem pr1_subst_lem_alt: forall A1 A2 B1 B2 L K J, nabla x,
ctxs L K J -> name x ->
{K, pr1 x x |- pr1 (A1 x) (A2 x)} -> {K |- pr1 B1 B2} ->
{K |- pr1 (A1 B1) (A2 B2)}.
induction on 3. intros. case H3.
case H5.
search.
apply pr1_worlds to H1 H6. case H7. search. search.
apply IH to H1 H2 H5 H4. apply IH to H1 H2 H6 H4. search.
apply IH to _ H2 H5 H4. apply pr1_clause2 to H6. search.
apply IH to H1 H2 H5 H4. apply IH to H1 H2 H6 H4.
apply pr1_clause3 to H7 H8. search.
Theorem pr1_subst_lem: forall A1 A2 B1 B2 L K J,
ctxs L K J ->
{K |- pr1 (abs A1) (abs A2)} -> {K |- pr1 B1 B2} ->
{K |- pr1 (A1 B1) (A2 B2)}.
intros. case H2.
apply pr1_worlds to H1 H4. case H5.
apply pr1_subst_lem_alt to H1 _ H4 H3. search.
-Andrew