Commit 8ad4065f by Hoang-Hai Dang

add wf for cell_cut

parent e7d67bb8
Pipeline #5167 passed with stages
in 13 minutes 24 seconds
......@@ -2566,6 +2566,17 @@ Section Memory.
move => [m' /cell_cut_lookup_Some [Eq' ?]]. by eexists.
Qed.
Lemma cell_cut_wf (C: cell) (WF: wf C) t:
wf (cell_cut t C).
Proof.
constructor.
- move => to. destruct (cell_cut t C !! to) as [m|] eqn:Ht; [|done].
apply cell_cut_lookup_Some in Ht as [Ht _]. solve_wfs [wf Ht].
- move => ?? /cell_cut_lookup_Some [? _]. by apply WF.
- move => ???? /cell_cut_lookup_Some [? _] /cell_cut_lookup_Some [? _].
by apply WF.
Qed.
(** Mem cut --------------------------------------------------------------- *)
Definition mem_cut_filter (V : timeMap) (lt : loc * time) : Prop :=
from_option (λ t', t' lt.2) False (V !! lt.1).
......
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