Going under binding?
Randy Pollack
Here is today's question. The .mod file is as yesterday.
I'm appending a .thy file that checks (thanks to your help). In the
scope of those theorems I want to prove
Theorem cd1_unique: forall A B C L K J,
ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.
I can do every case except the one that goes under the binder, which I
skip in the following proof:
induction on 2. intros. case H2 (keep).
case H3. apply cd1_worlds to H1 H4.
apply cd1_worlds to H1 H5. search.
apply cd1_worlds to H1 H4. case H8.
apply cd1_worlds to H1 H4. case H6.
apply cd1_worlds to H1 H4. case H7.
case H3 (keep). apply cd1_worlds to H1 H7. case H8.
apply IH to H1 H5 H8. apply IH to H1 H6 H9. search.
apply notabs_not_abs to H1 H4.
skip. %%% THIS IS THE QUESTION
case H3 (keep). apply cd1_worlds to H1 H6. case H7.
apply notabs_not_abs to H1 H6.
apply IH to H1 H4 H6. apply IH to H1 H5 H7. search.
Can you help me with that case? BTW, can you see how to simplify
this proof in this logic?
Thanks,
Randy
---
Define ctxs nil nil nil.
Define nabla x, ctxs (trm x :: L) (pr1 x x :: K) (cd1 x x :: notabs x :: J)
:= ctxs L K J.
Define nabla x, name x.
Theorem ctxs_tails: forall A B C D L K J,
ctxs (A::L) (B::K) (C::D::J) -> ctxs L K J.
induction on 1. intros. case H1. search.
Theorem trm_worlds : forall A L K J,
ctxs L K J -> member (trm A) L ->
name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\
member (notabs A) J.
induction on 2. intros. case H2.
case H1. search.
case H1. apply IH to H4 H3. search.
Theorem pr1_worlds : forall A B L K J,
ctxs L K J -> member (pr1 A B) K ->
name A /\ A = B /\ member (trm A) L /\
member (cd1 A B) J /\ member (notabs A) J.
induction on 2. intros. case H2.
case H1. search.
case H1. apply IH to H4 H3. search.
Theorem cd1_worlds : forall A B L K J,
ctxs L K J -> member (cd1 A B) J ->
name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J.
induction on 2. intros. case H2.
case H1. search.
case H1. case H3. apply IH to H4 H5. search.
Theorem notabs_worlds : forall A L K J,
ctxs L K J -> member (notabs A) J ->
name A /\ member (trm A) L /\ member (pr1 A A) K /\
member (cd1 A A) J.
induction on 2. intros. case H2.
case H1. search.
case H1. case H3. search.
apply IH to H4 H5. search.
Theorem notabs_not_abs: forall A L K J,
ctxs L K J -> {J |- notabs (abs A)} -> false.
induction on 2. intros. case H2 (keep).
apply notabs_worlds to H1 H3. case H4.
Theorem pre_cd1_pr1 : forall A B L K J,
ctxs L K J -> {L |- trm A} -> {J |- cd1 A B} -> {K |- pr1 A B}.
induction on 2. intros. case H2.
% 1) member (cd1 A B) J. Then A = B, and we know pr1 is reflexive.
apply trm_worlds to H1 H4. case H3.
apply cd1_worlds to H1 H9. search.
case H5.
case H5.
case H5.
% 2) {J |- cd1 (app M N) B}. Should work by IH.
case H3.
apply cd1_worlds to H1 H6. case H7.
apply IH to H1 H4 H7. apply IH to H1 H5 H8. search.
apply IH to H1 H4 H6. apply IH to H1 H5 H7. skip.
% 3) {J |- cd1 (abs M) B}. Should work by IH.
case H3.
apply cd1_worlds to H1 H5. case H6.
apply IH to _ H4 H5. search.
% Here we establish that {J |- cd1 A B} implies A is a term
Theorem cd1_trm : forall A B L K J,
ctxs L K J -> {J |- cd1 A B} -> {L |- trm A}.
induction on 2. intros. case H2.
apply cd1_worlds to H1 H3. search.
apply IH to H1 H4. apply IH to H1 H5. search.
apply IH to _ H3. search.
apply IH to H1 H3. apply IH to H1 H4. search.
Theorem cd1_pr1 : forall A B L K J,
ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B}.
intros.
apply cd1_trm to H1 H2.
apply pre_cd1_pr1 to H1 H3 H2.
search.
Theorem pr1_rfl : forall A L K J,
ctxs L K J -> {L |- trm A} -> {K |- pr1 A A}.
induction on 2. intros. case H2.
apply trm_worlds to H1 H3. search.
apply IH to H1 H3. apply IH to H1 H4. search.
apply IH to _ H3. search.
Andrew Gacek
> Theorem cd1_unique: forall A B C L K J,
> ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.
>
> I can do every case except the one that goes under the binder, which I
> skip in the following proof:
>
> induction on 2. intros. case H2 (keep).
> case H3. apply cd1_worlds to H1 H4.
> apply cd1_worlds to H1 H5. search.
> apply cd1_worlds to H1 H4. case H8.
> apply cd1_worlds to H1 H4. case H6.
> apply cd1_worlds to H1 H4. case H7.
> case H3 (keep). apply cd1_worlds to H1 H7. case H8.
> apply IH to H1 H5 H8. apply IH to H1 H6 H9. search.
> apply notabs_not_abs to H1 H4.
>
> skip. %%% THIS IS THE QUESTION
Here I was able to complete the subgoal with
case H3. apply cd1_worlds to H1 H5. case H6.
apply IH to _ H4 H5. search.
> case H3 (keep). apply cd1_worlds to H1 H6. case H7.
> apply notabs_not_abs to H1 H6.
> apply IH to H1 H4 H6. apply IH to H1 H5 H7. search.
>
> Can you help me with that case? BTW, can you see how to simplify
> this proof in this logic?
Later today I'll try to look through the proof in more detail and see
if I can find a way to restructure or improve it. All these uses of
*_worlds are annoying, but unavoidable given the current logic.
> Theorem notabs_worlds : forall A L K J,
> ctxs L K J -> member (notabs A) J ->
> name A /\ member (trm A) L /\ member (pr1 A A) K /\
> member (cd1 A A) J.
> induction on 2. intros. case H2.
> case H1. search.
> case H1. case H3. search.
> apply IH to H4 H5. search.
On the line "case H1. search." the search is unnecessary since case
finishes the subgoal.
-Andrew
Andrew Gacek
> Theorem cd1_unique: forall A B C L K J,
> ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.
I looked through the proof of this theorem and I didn't see much to
change. You can slightly rearrange the worlds cases to make the
beginning a little simpler. Here's what I ended up with,
Theorem cd1_unique: forall A B C L K J,
ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.
induction on 2. intros. case H2.
apply cd1_worlds to H1 H4. case H3.
apply cd1_worlds to H1 H9. search.
case H5.
case H5.
case H5.
case H3. apply cd1_worlds to H1 H7. case H8.
apply IH to H1 H5 H8. apply IH to H1 H6 H9. search.
apply notabs_not_abs to H1 H4.
case H3. apply cd1_worlds to H1 H5. case H6.
apply IH to _ H4 H5. search.
case H3. apply cd1_worlds to H1 H6. case H7.
apply notabs_not_abs to H1 H6.
apply IH to H1 H4 H6. apply IH to H1 H5 H7. search.
The worlds reasoning is a little more present than in other theorems
since we want to consider all possible ways of deriving {J |- cd1 A B}
and all possible ways of deriving {J |- cd1 A C}. Of course we always
have the consider the case for each of these that cd1 comes from the
context J.
-Andrew
Andrew Gacek
the following proof.
Theorem cd1_unique: forall A B C L K J,
ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.
induction on 2. intros. case H2.
apply cd1_worlds to H1 H4. case H5. case H3.
apply cd1_worlds to H1 H9. search.
case H3. apply cd1_worlds to H1 H7. case H8.
apply IH to H1 H5 H8. apply IH to H1 H6 H9. search.
apply notabs_not_abs to H1 H4.
case H3. apply cd1_worlds to H1 H5. case H6.
apply IH to _ H4 H5. search.
case H3. apply cd1_worlds to H1 H6. case H7.
apply notabs_not_abs to H1 H6.
apply IH to H1 H4 H6. apply IH to H1 H5 H7. search.
But if you follow the reasoning for that initial worlds stuff, it's a
little messy with the nominal constant n1 appearing all over the
place. Personally, I prefer the longer proof script which has more
understandable subgoals during the proof.
-Andrew