Commit 64d55fe6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix Combine.v

parent 2cfc4c73
......@@ -5,7 +5,7 @@
* time credits and time receipts, including proof-mode tactics.
*)
From iris.heap_lang Require Import proofmode notation adequacy lang.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants.
From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
......@@ -283,13 +283,12 @@ Section Definitions.
iApply "InvClose". auto with iFrame.
Qed.
Theorem tick_spec s E e v n :
Theorem tick_spec s E (v : val) n :
tctrN E
IntoVal e v
TCTR_invariant -
{{{ TC 1 TRdup n }}} tick e @ s ; E {{{ RET v ; TR 1 TRdup (n+1) }}}.
{{{ TC 1 TRdup n }}} tick v @ s ; E {{{ RET v ; TR 1 TRdup (n+1) }}}.
Proof using max_tr.
intros ? <-. iIntros "#Inv" (Ψ) "!# [Hγ◯ Hγ2◯] HΨ".
intros ?. iIntros "#Inv" (Ψ) "!# [Hγ◯ Hγ2◯] HΨ".
iLöb as "IH".
wp_lam.
(* open the invariant, in order to read the value m of location : *)
......@@ -380,9 +379,8 @@ Section Tactics.
Implicit Types Φ : val iProp Σ.
Implicit Types Δ : envs (uPredI (iResUR Σ)).
Lemma tac_wp_tick `{tctrHeapG Σ} Δ Δ1 Δ2 Δ3 Δ' i j1 j2 j3 max_tc m n p s E K e v Φ :
Lemma tac_wp_tick `{tctrHeapG Σ} Δ Δ1 Δ2 Δ3 Δ' i j1 j2 j3 max_tc m n p s E K (v : val) Φ :
tctrN E
IntoVal e v
MaybeIntoLaterNEnvs 1 Δ Δ1
envs_lookup i Δ = Some (true, TCTR_invariant max_tc)
envs_lookup j1 Δ1 = Some (false, TC (S m))
......@@ -392,7 +390,7 @@ Section Tactics.
envs_simple_replace j3 false (Esnoc Enil j3 (TR (S n))) Δ3 = Some Δ2
envs_simple_replace j2 false (Esnoc Enil j2 (TRdup (S p))) Δ2 = Some Δ'
envs_entails Δ' (WP fill K v @ s; E {{ Φ }})
envs_entails Δ (WP fill K (App tick e) @ s; E {{ Φ }}).
envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
Admitted.
End Tactics.
......@@ -402,8 +400,8 @@ Ltac wp_tick :=
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[ reshape_expr e ltac:(fun K e' =>
eapply (tac_wp_tick _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ K) ; [ | exact _ | ..]
[ reshape_expr false e ltac:(fun K e' =>
eapply (tac_wp_tick _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ K)
)
| fail 1 "wp_tick: cannot find 'tick ?v' in" e ] ;
[ try solve_ndisj
......
......@@ -552,7 +552,7 @@ Section Tactics.
End Tactics.
Ltac wp_tick :=
Ltac wp_tick ::=
let solve_TICKCTXT _ :=
iAssumptionCore || fail "wp_tick: cannot find TC_invariant" in
let solve_TC _ :=
......@@ -574,21 +574,3 @@ Ltac wp_tick :=
| wp_expr_simpl ]
| _ => fail "wp_tick: not a 'wp'"
end.
Ltac wp_tick_closure := wp_closure; wp_tick.
Ltac wp_tick_pair := wp_tick; wp_pair.
Ltac wp_tick_inj := wp_tick; wp_inj.
Ltac wp_tick_rec := wp_tick ; wp_rec; simpl_trans.
Ltac wp_tick_lam := wp_tick_rec.
Ltac wp_tick_let := wp_tick_closure; wp_tick_lam.
Ltac wp_tick_seq := wp_tick_let.
Ltac wp_tick_op := wp_tick ; wp_op.
Ltac wp_tick_if := wp_tick ; wp_if.
Ltac wp_tick_match :=
wp_tick; wp_match; (wp_let || wp_seq); wp_lam;
wp_closure; wp_tick; wp_tick; wp_lam.
Ltac wp_tick_proj := wp_tick ; wp_proj.
Ltac wp_tick_alloc loc := wp_tick ; wp_alloc loc.
Ltac wp_tick_load := wp_tick ; wp_load.
Ltac wp_tick_store := wp_tick ; wp_store.
......@@ -581,3 +581,29 @@ Section ClosureFree.
Qed.
End ClosureFree.
(*
* Proofmode wp_* tactics.
*)
(* wp_tick is a stub to be redefined for each particular definition of
the tick function. *)
Ltac wp_tick := idtac.
Ltac wp_tick_closure := wp_closure; wp_tick.
Ltac wp_tick_pair := wp_tick; wp_pair.
Ltac wp_tick_inj := wp_tick; wp_inj.
Ltac wp_tick_rec := wp_tick ; wp_rec; simpl_trans.
Ltac wp_tick_lam := wp_tick_rec.
Ltac wp_tick_let := wp_tick_closure; wp_tick_lam.
Ltac wp_tick_seq := wp_tick_let.
Ltac wp_tick_op := wp_tick ; wp_op.
Ltac wp_tick_if := wp_tick ; wp_if.
Ltac wp_tick_match :=
wp_tick; wp_match; (wp_let || wp_seq); wp_lam;
wp_closure; wp_tick; wp_tick; wp_lam.
Ltac wp_tick_proj := wp_tick ; wp_proj.
Ltac wp_tick_alloc loc := wp_tick ; wp_alloc loc.
Ltac wp_tick_load := wp_tick ; wp_load.
Ltac wp_tick_store := wp_tick ; wp_store.
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