Commit b67e07ce authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

list_pre properties proved. some changes in queue_spec.

parent c201286c
......@@ -9,6 +9,16 @@ Proof.
inversion 1. by apply IH.
Qed.
Lemma both_prefix_eq {A: Type} (x y : list A) :
x `prefix_of` y y `prefix_of` x x = y.
Proof.
intros. inversion H. inversion H0.
rewrite H1 in H2. rewrite <- app_assoc in H2.
apply eq_app_nil in H2 as H3. subst.
apply app_eq_nil in H3 as [H4 _]. subst. rewrite app_nil_r.
reflexivity.
Qed.
Instance prefix_PO {A: Type}: PartialOrder (@prefix A).
Proof.
split; [apply _|].
......@@ -63,16 +73,21 @@ Section ListMaster.
Proof.
split.
- unfold Proper, "==>". intros.
destruct x0, y; try done; try inversion H1. subst.
induction H4. done. destruct x. done. unfold "⋅", lp_op.
destruct (decide (l0 `prefix_of` x0 :: l)). admit. admit.
destruct x0, y; try done; try inversion H1. simplify_eq. done.
- intros. exists cx. split; [|done]. rewrite <- H2.
destruct x, y; try done; try inversion H1. admit.
destruct x, y; try done; try inversion H1. simplify_eq. done.
- unfold Proper, "==>", impl. intros.
destruct x, y; try done; try inversion H2; try inversion H1.
- unfold Assoc. intros. destruct x, y, z; try done. admit. admit.
- unfold Comm. intros. destruct x, y; try done. admit.
- intros. destruct x. done. inversion H1. rewrite H3. admit.
- unfold Assoc. intros. destruct x, y, z; try done.
assert (ListSome l0 ListBot = ListBot). done.
destruct (ListSome l ListSome l0); rewrite H1; try done.
unfold "⋅", lp_op. admit.
- unfold Comm. intros. destruct x, y; try done.
unfold "⋅", lp_op. destruct (decide (l `prefix_of` l0));
destruct (decide (l0 `prefix_of` l)); try done.
apply (both_prefix_eq l l0) in p. subst. done. done.
- intros. destruct x. done. destruct cx; inversion H1.
unfold "⋅", lp_op. destruct (decide (l0 `prefix_of` l0)); try done.
- intros. destruct x. inversion H1. inversion H1. done.
- intros. destruct x eqn:E, y; inversion H2. admit. admit.
- intros. destruct x, y; try inversion H1; try done.
......
......@@ -211,7 +211,7 @@ Section MSQueue.
wp_load.
iMod ("Hclose" with "[Hhq Htq Ht Hγc● Hγm●]") as "_".
{ iNext. iExists _, _, _, _. iFrame. iExists _. iFrame. iExists _. iFrame. done. }
iModIntro. wp_proj. wp_op. wp_if. wp_store.
iModIntro. wp_proj. wp_op. wp_if.
Admitted.
Lemma prefix_app_inv : (A : Type) (l l1 l2 : list A),
......
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