Commit 73c911a1 authored by Ralf Jung's avatar Ralf Jung
Browse files

HACK to kill left/right bind lemmas

parent 30bb1748
......@@ -90,8 +90,7 @@ Proof.
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
{ rewrite lookup_insert. done. }
apply: sim_body_result=>_. simpl.
apply: sim_body_result=>Hval. split.
apply: sim_body_result=>Hval. simpl. split.
- eexists. split; first done. admit. (* end_call_sat *)
- constructor; simpl; auto.
Admitted.
......
......@@ -133,26 +133,6 @@ Proof.
pclearbot. right. by apply CIH. }
Qed.
Lemma sim_body_bind_r fs ft
(Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
r n es σs σt Φ :
r {n,fs,ft} (#[], σs) (et, σt)
: (λ r' n' _ _ et' σt',
r' {n',fs,ft} (es, σs) (fill Kt et', σt') : Φ)
r {n,fs,ft} (es, σs) (fill Kt et, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_bind_l fs ft
(Ks: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) es
r n et σs σt Φ :
r {n,fs,ft} (es, σs) (#[], σt)
: (λ r' n' es' σs' _ _,
r' {n',fs,ft} (fill Ks es', σs') (et, σt) : Φ)
r {n,fs,ft} (fill Ks es, σs) (et, σt) : Φ.
Proof.
Admitted.
Lemma sim_body_bind_call r n fs ft es σs et σt (fns fnt: result) (pres pret: list result) posts postt Φ :
r {n,fs,ft} (es, σs) (et, σt)
: (λ r' n' rs' σs' rt' σt',
......
......@@ -98,43 +98,64 @@ Tactic Notation "sim_apply" open_constr(lem) :=
)
end.
(* HACK to avoid a bind-left/right rule. Does not work in general (e.g. when
there is an [Alloc T] in eval position on the left), but works for now. *)
Ltac test_pure_head e :=
match e with
| of_result _ => idtac
| Val _ => idtac
| Place _ _ _ => idtac
| _ => fail
end.
Tactic Notation "sim_bind_r" open_constr(efoc) :=
match goal with
| |- _ {_,_,_} (_, _) (?et, _) : _ =>
reshape_expr et ltac:(fun Kt et =>
unify et efoc;
eapply (sim_body_bind_r _ _ Kt et)
| |- _ {_,_,_} (?es, _) (?et, _) : _ =>
reshape_expr es ltac:(fun Ks es =>
test_pure_head es;
reshape_expr et ltac:(fun Kt et =>
unify et efoc;
sim_body_bind_core Ks es Kt et
)
)
end.
Tactic Notation "sim_apply_r" open_constr(lem) :=
match goal with
| |- _ {_,_,_} (?es, _) (?et, _) : _ =>
reshape_expr et ltac:(fun Kt et =>
eapply (sim_body_bind_r _ _ Kt et);
apply: lem
reshape_expr es ltac:(fun Ks es =>
test_pure_head es;
reshape_expr et ltac:(fun Kt et =>
sim_body_bind_core Ks es Kt et;
apply: lem
)
)
end.
Tactic Notation "sim_bind_l" open_constr(efoc) :=
match goal with
| |- _ {_,_,_} (?es, _) (_, _) : _ =>
| |- _ {_,_,_} (?es, _) (?et, _) : _ =>
reshape_expr es ltac:(fun Ks es =>
unify es efoc;
eapply (sim_body_bind_l _ _ Ks es)
reshape_expr et ltac:(fun Kt et =>
test_pure_head et;
sim_body_bind_core Ks es Kt et
)
)
end.
Tactic Notation "sim_apply_l" open_constr(lem) :=
match goal with
| |- _ {_,_,_} (?es, _) (_, _) : _ =>
reshape_expr es ltac:(fun Ks es =>
eapply (sim_body_bind_l _ _ Ks es);
apply: lem
| |- _ {_,_,_} (?es, _) (?et, _) : _ =>
reshape_expr et ltac:(fun Kt et =>
test_pure_head et;
reshape_expr es ltac:(fun Ks es =>
sim_body_bind_core Ks es Kt et;
apply: lem
)
)
end.
(** The expectation is that lemmas state their resource requirements as
[r frame what_lemma_needs]. Users eapply the lemma, and [frame]
becomes an evar. [solve_res] solves such goals. *)
......
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