Commit d91f7a57 by Paul

### fix spinlock proofs: solve bounds with solve_goal

parent 093ce2fb
 ... ... @@ -141,7 +141,7 @@ Section proofs. repeat liRStep; liShow. iRename select (ticket_range _ _ _) into "Htks". iDestruct (split_first_ticket with "Htks") as "[Hnext \$]". { split; last by lia. by transitivity (min_int u16) => //. } { split; solve_goal. } iRename select (_ ∨ _)%I into "Hcases". iSplitL "Hcases". { iDestruct "Hcases" as "[[H %]|H]"; [iLeft | iRight] => //. iSplitL => //. iPureIntro. lia. } ... ... @@ -195,7 +195,7 @@ Section proofs. iRename select (p at{struct_hyp_spinlock}ₗ "next" ◁ₗ _)%I into "Hnext". iDestruct "Hrest" as "(Hfrag&Hr1&Hr2&Hcases)". iDestruct (split_first_ticket with "Hr2") as "[Hticket Hr2]". { split; last by lia. by transitivity (min_int u16). } { split; solve_goal. } iMod ("Hclose_inv" with "[Howner Hnext Hfrag Hr1 Hr2 Hcases]") as "_". { iNext. iExists owner, (next + 1). iFrame. iSplit. { iPureIntro. lia. } ... ... @@ -235,7 +235,7 @@ Section proofs. iRename select (ticket_range _ i _) into "Hrange". iDestruct (ticket_not_NO_TICKET with "Hticket") as %Hi. iApply (ticket_already_in_range with "[] Hrange Hticket"). iPureIntro. apply elem_of_seqZ. lia. } iPureIntro. apply elem_of_seqZ. solve_goal. } repeat liRStep; liShow. iSplitR "Htok"; last by iFrame. iLeft. iSplit => //. iPureIntro. lia. + repeat liRStep; liShow. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!