Commit 9418275e authored by Ralf Jung's avatar Ralf Jung

mark a stronger-than-on-paper rule as such

parent 875e7747
Pipeline #28579 passed with stage
in 29 minutes and 26 seconds
......@@ -82,7 +82,7 @@ Section cont_context.
iApply ("H" with "[%]"). by apply HC1C2.
Qed.
Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n tctx) C1 C2 :
Lemma cctx_incl_cons E k L n (T1 T2 : vec val n tctx) C1 C2 :
cctx_incl E C1 C2 ( args, tctx_incl E L (T2 args) (T1 args))
cctx_incl E (k cont(L, T1) :: C1) (k cont(L, T2) :: C2).
Proof.
......@@ -99,14 +99,15 @@ Section cont_context.
Lemma cctx_incl_nil E C : cctx_incl E C [].
Proof. apply incl_cctx_incl. by set_unfold. Qed.
Lemma cctx_incl_cons E k L n (T1 T2 : vec val n tctx) C1 C2 :
(* Extra strong cctx inclusion rule that we do not have on paper. *)
Lemma cctx_incl_cons_dup E k L n (T1 T2 : vec val n tctx) C1 C2 :
k cont(L, T1) C1
( args, tctx_incl E L (T2 args) (T1 args))
cctx_incl E C1 C2
cctx_incl E C1 (k cont(L, T2) :: C2).
Proof.
intros Hin ??. rewrite <-cctx_incl_cons_match; try done.
iIntros (?) "_ #HE HC".
intros Hin ??. rewrite <-cctx_incl_cons; try done.
clear -Hin. iIntros (?) "_ #HE HC".
rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
[iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
......
......@@ -349,7 +349,7 @@ Section typing.
intros Hfn HL HE HTT' HC HT'T''.
rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
- etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%stdpp.list.elem_of_list_singleton.
apply cctx_incl_cons_match; first done. intros args. by inv_vec args.
apply cctx_incl_cons; first done. intros args. by inv_vec args.
- etrans; last by apply (tctx_incl_frame_l [_]).
apply copy_elem_of_tctx_incl; last done. apply _.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment