Commit 523962be authored by Jaehwang Jung's avatar Jaehwang Jung
Browse files

prove proof_producer_consumer

parent 59d29dd4
......@@ -164,6 +164,7 @@ theories/examples/queue/proof_mp_graph.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_ms_closed.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_producer_consumer.v
## Chase-Lev Double-ended Queue
theories/examples/chase_lev/code.v
## Exchanger
......
......@@ -84,16 +84,6 @@ Proof.
eexists. eapply prefix_lookup; [done|by eexists].
Qed.
Lemma lookup_xo : (n e : nat) (LT : (e < n)%nat), (seq 0 n) !! e = Some e.
Proof. intros. by rewrite lookup_seq_lt. Qed.
Lemma xo_events E : Forall (λ e, is_Some (E !! e)) (seq 0 (length E)).
Proof.
rewrite Forall_lookup => i e H. have H' := H. apply lookup_lt_is_Some_2.
rewrite lookup_xo in H; simplify_eq;
apply lookup_lt_Some in H'; by rewrite seq_length in H'.
Qed.
Lemma hb_xo_add E eV
(WF : history_wf E)
(HB_XO : hb_ord E (seq 0 (length E))) :
......@@ -118,19 +108,6 @@ Proof.
eapply (HB_XO e1 e2 e1 e2 eV2); [by rewrite lookup_xo..|done|done].
Qed.
Lemma ord_nodup N ord (PERM : ord seq 0 N) : NoDup ord.
Proof. rewrite (NoDup_Permutation_proper _ _ PERM). apply NoDup_seq. Qed.
Lemma ord_idx_event E ord i e
(PERM : ord seq 0 (length E))
(Ee : ord !! i = Some e) :
eV, E !! e = Some eV.
Proof.
apply Permutation_inj in PERM as [LEN (f & _ & PERM)].
rewrite ->PERM,lookup_seq in Ee. des. subst. simpl.
by apply lookup_lt_is_Some_2.
Qed.
Lemma sublist_lookup {A} (ls1 ls2 : list A) i1 x
(SUB : ls1 `sublist_of` ls2)
(LOOKUP : ls1 !! i1 = Some x) :
......
......@@ -631,3 +631,32 @@ Proof.
apply IHi in H. by rewrite H.
Qed.
End alter.
Section xo.
Context {A : Type}.
Implicit Types (l : list A) (ord : list nat).
Lemma lookup_xo : (n e : nat) (LT : (e < n)%nat), (seq 0 n) !! e = Some e.
Proof. intros. by rewrite lookup_seq_lt. Qed.
Lemma xo_events l : Forall (λ e, is_Some (l !! e)) (seq 0 (length l)).
Proof.
rewrite Forall_lookup => i e H. have H' := H. apply lookup_lt_is_Some_2.
rewrite lookup_xo in H; simplify_eq;
apply lookup_lt_Some in H'; by rewrite seq_length in H'.
Qed.
Lemma ord_nodup N ord (PERM : ord seq 0 N) : NoDup ord.
Proof. rewrite (NoDup_Permutation_proper _ _ PERM). apply NoDup_seq. Qed.
Lemma ord_idx_event l ord i e
(PERM : ord seq 0 (length l))
(Ee : ord !! i = Some e) :
is_Some (l !! e).
Proof.
apply Permutation_inj in PERM as [LEN (f & _ & PERM)].
rewrite ->PERM,lookup_seq in Ee. destruct Ee as [-> ?]. simpl.
by apply lookup_lt_is_Some_2.
Qed.
End xo.
This diff is collapsed.
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