Commit af3458d2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Change order or premises of rule_seq, prove admits in ExampleListProofMode.

parent 8f523096
......@@ -174,9 +174,12 @@ Lemma rule_new_cell' : forall v q,
Proof using.
intros. eapply rule_app_fun2 =>//=; [].
eapply rule_let; [apply rule_alloc_cell|]=>p /=. xpull=> p' v' q' ->.
eapply rule_seq; last admit.
eapply rule_seq.
{ rewrite MCell_eq. ram_apply rule_set_hd. auto with iFrame. }
unlock. eapply rule_seq; last admit. { ram_apply rule_set_tl. auto with iFrame. }
{ unlock. iIntros (u Hu) "[-> ?] //". }
unlock. eapply rule_seq.
{ ram_apply rule_set_tl. auto with iFrame. }
{ unlock. iIntros (u Hu) "[-> ?] //". }
unlock. eapply rule_val. iPrepare. auto with iFrame.
Qed.
......@@ -308,9 +311,9 @@ Proof using.
- unlock. xpull=>[= Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|]. xpull=>p' x L' ?. subst.
applys rule_let. { ram_apply rule_get_tl. auto with iFrame. }
unlock. move=> q /=. xpull=>->.
unlock=> q /=. xpull=>->.
applys rule_let. { ram_apply (IH L'); [done|]. auto with iFrame. }
unlock. move=> n /=. xpull=>->. ram_apply rule_add.
unlock=> n /=. xpull=>->. ram_apply rule_add.
iIntros "??" (?) "->". iSplitR.
{ iPureIntro. f_equal. math. } { iApply MList_cons. iFrame. }
- unlock. eapply rule_val. iPrepare. iIntros "HL" ([= Hp]). revert Hp.
......@@ -345,9 +348,9 @@ Lemma rule_mlist_length_loop : forall L p,
Proof using.
intros L p. eapply rule_app_fun=>//=.
applys rule_let. { ram_apply rule_ref. auto with iFrame. }
unlock. move=> ? /=. xpull=>r ->.
unlock=> ? /=. xpull=>r ->.
applys rule_let. { ram_apply rule_ref. auto with iFrame. }
unlock. move=> ? /=. xpull=>n ->. applys rule_seq; last admit.
unlock=> ? /=. xpull=>n ->. applys rule_seq.
- applys rule_while=>t R.
cuts K: (forall (nacc:int),
triple t (n ~~~> nacc \* MList L p \* r ~~~> p)
......@@ -355,23 +358,26 @@ Proof using.
{ ram_apply K. auto with iFrame. }
gen p. induction_wf: list_sub_wf L=>p nacc. apply R. applys rule_if'.
+ eapply rule_let. ram_apply rule_get. { auto with iFrame. }
unlock. move=>pp /=. xpull=>->. ram_apply rule_neq. eauto with iFrame.
unlock=>pp /=. xpull=>->. ram_apply rule_neq. eauto with iFrame.
+ unlock. xpull. intros [=Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|iPrepare; auto with iFrame|].
xpull=>p' x L' ?. subst. applys rule_seq; last admit.
* applys rule_seq; last admit. { ram_apply rule_incr. auto with iFrame. }
xpull=>p' x L' ?. subst. applys rule_seq.
{ applys rule_seq. { ram_apply rule_incr. auto with iFrame. }
{ unlock. iIntros (u Hu) "(? & ? & ? & -> & ?) //". }
unlock. eapply rule_let. { ram_apply rule_get. auto with iFrame. }
unlock. xpull=>? -> /=. eapply rule_let.
{ ram_apply rule_get_tl. auto with iFrame. }
unlock. move=>? /=. xpull=>->. ram_apply rule_set. auto with iFrame.
* unlock. ram_apply (IH L'); [done|]. iIntros. iFrame.
iIntros (?) "$ Hn ?". iSplitL "Hn".
-- by math_rewrite ((nacc + 1) + length L' = nacc + S (length (L')))%Z.
-- iApply MList_cons. iFrame.
unlock=>? /=. xpull=>->. ram_apply rule_set. auto with iFrame. }
{ unlock. iIntros (u Hu) "(? & ? & ? & -> & ?) //". }
unlock. ram_apply (IH L'); [done|]. iIntros. iFrame.
iIntros (?) "$ Hn ?". iSplitL "Hn".
* by math_rewrite ((nacc + 1) + length L' = nacc + S (length (L')))%Z.
* iApply MList_cons. iFrame.
+ unlock. iApply rule_val_htop. iPrepare. iIntros "? HL ?" ([= Hp]).
revert Hp. rewrite false_eq_isTrue_eq. intros [= ->]%not_not_inv.
iDestruct (MList_null_inv with "HL") as "[$ ->]". rewrite plus_zero_r. by iFrame.
+ unlock. iIntros ([] Hb) "(? & ? & ? & %)"=>//. destruct Hb. eexists _. auto.
- unlock. iIntros (u Hu) "[-> ?] //".
- unlock. apply rule_htop_post. ram_apply rule_get. auto with iFrame.
Qed.
......
......@@ -605,20 +605,20 @@ Qed.
Lemma rule_seq : forall t1 t2 H Q Q1,
triple t1 H Q1 ->
triple t2 (Q1 val_unit) Q ->
(forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) ->
triple t2 (Q1 val_unit) Q ->
triple (trm_seq t1 t2) H Q.
Proof using.
introv M1 M2 M3. intros HF h N.
lets~ (h1'&v1&R1&K1): (rm M1) HF h.
asserts E: (v1 = val_unit).
{ specializes M3 v1. applys not_not_inv. intros E.
{ specializes M2 v1. applys not_not_inv. intros E.
asserts Z: ((\[False] \* \Top \* HF) h1').
{ applys himpl_trans K1. hchange~ M3. hsimpl. }
{ applys himpl_trans K1. hchange~ M2. hsimpl. }
repeat rewrite hfalse_hstar_any in Z.
lets: hpure_inv Z. false*. }
(* TODO: shorten this, and factorize with rule_if *)
subst. forwards* (h2'&v2&R2&K2): (rm M2) (\Top \* HF) h1'.
subst. forwards* (h2'&v2&R2&K2): (rm M3) (\Top \* HF) h1'.
exists h2' v2. splits~.
{ applys~ red_seq R2. }
{ rewrite <- htop_hstar_htop. hhsimpl. }
......@@ -1030,8 +1030,8 @@ Lemma rule_seq' : forall t1 t2 H Q H1,
Proof using.
introv M1 M2. applys rule_seq.
{ applys M1. }
{ applys rule_extract_hprop. intros. applys M2. }
{ intros v E. hpull; false. }
{ applys rule_extract_hprop. intros. applys M2. }
Qed.
......
......@@ -582,9 +582,9 @@ Lemma Rule_seq : forall t1 t2 H,
Proof using.
introv M1 M2. applys rule_seq.
{ applys M1. }
{ unfold Post. xpull ;=> V E. destruct V. applys M2. }
{ intros v N. unfold Post. hpull ;=> V E. subst. false N.
rewrite enc_unit_eq. hnfs*. } (* todo : simplify ?*)
{ unfold Post. xpull ;=> V E. destruct V. applys M2. }
Qed.
Lemma Rule_let : forall x t1 t2 H,
......
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