Commit 280d91b0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Clean up some ndisjoint stuff in the proofmode tactics.

parent 4f918d4a
...@@ -105,7 +105,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) := ...@@ -105,7 +105,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
[let e' := match goal with |- to_val ?e' = _ => e' end in [let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_alloc:" e' "not a value" wp_done || fail "wp_alloc:" e' "not a value"
|iAssumption || fail "wp_alloc: cannot find heap_ctx" |iAssumption || fail "wp_alloc: cannot find heap_ctx"
|done || eauto with ndisj |solve_ndisj
|apply _ |apply _
|first [intros l | fail 1 "wp_alloc:" l "not fresh"]; |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split; eexists; split;
...@@ -126,7 +126,7 @@ Tactic Notation "wp_load" := ...@@ -126,7 +126,7 @@ Tactic Notation "wp_load" :=
|fail 1 "wp_load: cannot find 'Load' in" e]; |fail 1 "wp_load: cannot find 'Load' in" e];
eapply tac_wp_load; eapply tac_wp_load;
[iAssumption || fail "wp_load: cannot find heap_ctx" [iAssumption || fail "wp_load: cannot find heap_ctx"
|done || eauto with ndisj |solve_ndisj
|apply _ |apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
...@@ -145,7 +145,7 @@ Tactic Notation "wp_store" := ...@@ -145,7 +145,7 @@ Tactic Notation "wp_store" :=
[let e' := match goal with |- to_val ?e' = _ => e' end in [let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_store:" e' "not a value" wp_done || fail "wp_store:" e' "not a value"
|iAssumption || fail "wp_store: cannot find heap_ctx" |iAssumption || fail "wp_store: cannot find heap_ctx"
|done || eauto with ndisj |solve_ndisj
|apply _ |apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
...@@ -167,7 +167,7 @@ Tactic Notation "wp_cas_fail" := ...@@ -167,7 +167,7 @@ Tactic Notation "wp_cas_fail" :=
|let e' := match goal with |- to_val ?e' = _ => e' end in |let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_cas_fail:" e' "not a value" wp_done || fail "wp_cas_fail:" e' "not a value"
|iAssumption || fail "wp_cas_fail: cannot find heap_ctx" |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
|done || eauto with ndisj |solve_ndisj
|apply _ |apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
...@@ -189,7 +189,7 @@ Tactic Notation "wp_cas_suc" := ...@@ -189,7 +189,7 @@ Tactic Notation "wp_cas_suc" :=
|let e' := match goal with |- to_val ?e' = _ => e' end in |let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_cas_suc:" e' "not a value" wp_done || fail "wp_cas_suc:" e' "not a value"
|iAssumption || fail "wp_cas_suc: cannot find heap_ctx" |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
|done || eauto with ndisj |solve_ndisj
|apply _ |apply _
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
......
...@@ -67,3 +67,5 @@ Hint Resolve ndisj_subseteq_difference : ndisj. ...@@ -67,3 +67,5 @@ Hint Resolve ndisj_subseteq_difference : ndisj.
Hint Extern 0 (_ .@ _ _ .@ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Extern 0 (_ .@ _ _ .@ _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj. Hint Resolve ndot_preserve_disjoint_r : ndisj.
Ltac solve_ndisj := eauto with ndisj.
...@@ -39,7 +39,7 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) := ...@@ -39,7 +39,7 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
[let P := match goal with |- IsFSA ?P _ _ _ _ => P end in [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P apply _ || fail "iInv: cannot viewshift in goal" P
|try fast_done (* atomic *) |try fast_done (* atomic *)
|done || eauto with ndisj (* [eauto with ndisj] is slow *) |solve_ndisj
|iAssumption || fail "iInv: invariant" N "not found" |iAssumption || fail "iInv: invariant" N "not found"
|env_cbv; reflexivity |env_cbv; reflexivity
|simpl (* get rid of FSAs *)]. |simpl (* get rid of FSAs *)].
...@@ -65,7 +65,7 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) := ...@@ -65,7 +65,7 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
[let P := match goal with |- IsFSA ?P _ _ _ _ => P end in [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P apply _ || fail "iInv: cannot viewshift in goal" P
|try fast_done (* atomic *) |try fast_done (* atomic *)
|done || eauto with ndisj (* [eauto with ndisj] is slow *) |solve_ndisj
|iAssumption || fail "iOpenInv: invariant" N "not found" |iAssumption || fail "iOpenInv: invariant" N "not found"
|let P := match goal with |- TimelessP ?P => P end in |let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iInv:" P "not timeless" apply _ || fail "iInv:" P "not timeless"
......
...@@ -41,6 +41,6 @@ Tactic Notation "iSts" constr(H) "as" ...@@ -41,6 +41,6 @@ Tactic Notation "iSts" constr(H) "as"
|try fast_done (* atomic *) |try fast_done (* atomic *)
|iAssumptionCore || fail "iSts:" H "not found" |iAssumptionCore || fail "iSts:" H "not found"
|iAssumption || fail "iSts: invariant not found" |iAssumption || fail "iSts: invariant not found"
|done || eauto with ndisj (* [eauto with ndisj] is slow *) |solve_ndisj
|intros s Hs; eexists; split; [env_cbv; reflexivity|simpl]]. |intros s Hs; eexists; split; [env_cbv; reflexivity|simpl]].
Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?. Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?.
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