Commit 833a9d70 authored by Michael Sammler's avatar Michael Sammler
Browse files

FastDone -> TCFastDone

parent 3553bc58
Pipeline #55902 passed with stage
in 13 minutes and 20 seconds
...@@ -230,13 +230,13 @@ Section defs. ...@@ -230,13 +230,13 @@ Section defs.
apply: fsm_invariant_partial_alter => //; destruct ir, ir'; naive_solver. apply: fsm_invariant_partial_alter => //; destruct ir, ir'; naive_solver.
Qed. Qed.
Global Instance simpl_lookup_fsm_map_and mp key items n ir o `{!FastDone (fsm_invariant mp items)} `{!FastDone (probe_ref key items = Some (n, ir))}: Global Instance simpl_lookup_fsm_map_and mp key items n ir o `{!TCFastDone (fsm_invariant mp items)} `{!TCFastDone (probe_ref key items = Some (n, ir))}:
SimplBothRel (=) (mp !! key) o (item_ref_to_ty ir = o). SimplBothRel (=) (mp !! key) o (item_ref_to_ty ir = o).
Proof. unfold FastDone in *. by rewrite (fsm_invariant_lookup _ items _ n ir (item_ref_to_ty ir)). Qed. Proof. unfold TCFastDone in *. by rewrite (fsm_invariant_lookup _ items _ n ir (item_ref_to_ty ir)). Qed.
Global Instance simpl_fsm_invariant_and mp1 mp2 items `{!IsProtected mp1} `{!FastDone (fsm_invariant mp2 items)}: Global Instance simpl_fsm_invariant_and mp1 mp2 items `{!IsProtected mp1} `{!TCFastDone (fsm_invariant mp2 items)}:
SimplAndUnsafe true (fsm_invariant mp1 items) (λ T, mp1 = mp2 T) | 50. SimplAndUnsafe true (fsm_invariant mp1 items) (λ T, mp1 = mp2 T) | 50.
Proof. unfold FastDone in *. by move => ? [->]. Qed. Proof. unfold TCFastDone in *. by move => ? [->]. Qed.
Global Instance simpl_fsm_invariant_shelve_and mp items `{!ContainsProtected mp}: Global Instance simpl_fsm_invariant_shelve_and mp items `{!ContainsProtected mp}:
SimplAndUnsafe true (fsm_invariant mp items) (λ T, shelve_hint (fsm_invariant mp items) T) | 100. SimplAndUnsafe true (fsm_invariant mp items) (λ T, shelve_hint (fsm_invariant mp items) T) | 100.
Proof. move => ?; unfold shelve_hint; eauto. Qed. Proof. move => ?; unfold shelve_hint; eauto. Qed.
......
...@@ -33,11 +33,6 @@ Global Hint Extern 1 (CheckHypNotExists ?P) => (check_hyp_not_exists P; change T ...@@ -33,11 +33,6 @@ Global Hint Extern 1 (CheckHypNotExists ?P) => (check_hyp_not_exists P; change T
Class CheckOwnInContext {Σ} (P : iProp Σ) : Prop := { check_own_in_context : True }. Class CheckOwnInContext {Σ} (P : iProp Σ) : Prop := { check_own_in_context : True }.
(** * Different ways of checking if a property holds *) (** * Different ways of checking if a property holds *)
(** ** [FastDone]
Should be used if it is expected that the property shows up directly as a hypothesis. *)
Class FastDone (P : Prop) : Prop := fast_done_proof : P.
Global Hint Extern 1 (FastDone ?P) => (change P; fast_done) : typeclass_instances.
(** ** [TCDone] *) (** ** [TCDone] *)
Class TCDone (P : Prop) : Prop := done_proof : P. Class TCDone (P : Prop) : Prop := done_proof : P.
Global Hint Extern 1 (TCDone ?P) => (change P; done) : typeclass_instances. Global Hint Extern 1 (TCDone ?P) => (change P; done) : typeclass_instances.
......
...@@ -497,9 +497,9 @@ Global Instance simpl_is_Some_unfold {A} (o : option A): ...@@ -497,9 +497,9 @@ Global Instance simpl_is_Some_unfold {A} (o : option A):
SimplBoth (is_Some o) ( x, o = Some x) | 100. SimplBoth (is_Some o) ( x, o = Some x) | 100.
Proof. split; naive_solver. Qed. Proof. split; naive_solver. Qed.
Global Instance simpl_Some {A} o (x x' : A) `{!FastDone (o = Some x)}: Global Instance simpl_Some {A} o (x x' : A) `{!TCFastDone (o = Some x)}:
SimplBothRel (=) (o) (Some x') (x = x') | 1. SimplBothRel (=) (o) (Some x') (x = x') | 1.
Proof. unfold FastDone in *; subst. split; naive_solver. Qed. Proof. unfold TCFastDone in *; subst. split; naive_solver. Qed.
Global Instance simpl_both_fmap_Some A B f (o : option A) (x : B): SimplBothRel (=) (f <$> o) (Some x) ( x', o = Some x' x = f x'). Global Instance simpl_both_fmap_Some A B f (o : option A) (x : B): SimplBothRel (=) (f <$> o) (Some x) ( x', o = Some x' x = f x').
Proof. unfold SimplBothRel. rewrite fmap_Some. naive_solver. Qed. Proof. unfold SimplBothRel. rewrite fmap_Some. naive_solver. Qed.
......
...@@ -383,7 +383,7 @@ Section array. ...@@ -383,7 +383,7 @@ Section array.
(⌜l = base offset{ly}ₗ idx⌝ -∗ l ◁ₗ{β} array_ptr ly base idx len -∗ T) -∗ (⌜l = base offset{ly}ₗ idx⌝ -∗ l ◁ₗ{β} array_ptr ly base idx len -∗ T) -∗
simplify_hyp (l ◁ₗ{β} array_ptr ly base idx len) T. simplify_hyp (l ◁ₗ{β} array_ptr ly base idx len) T.
Proof. iIntros "HT [% #Hlib]". iApply "HT" => //. by iSplit. Qed. Proof. iIntros "HT [% #Hlib]". iApply "HT" => //. by iSplit. Qed.
Global Instance simplify_array_ptr_hyp_learn_loc_inst l β ly base idx len `{!TCUnless (FastDone (l = base offset{ly}ₗ idx))}: Global Instance simplify_array_ptr_hyp_learn_loc_inst l β ly base idx len `{!TCUnless (TCFastDone (l = base offset{ly}ₗ idx))}:
SimplifyHypPlace l β (array_ptr ly base idx len) (Some 0%N) | 10 := SimplifyHypPlace l β (array_ptr ly base idx len) (Some 0%N) | 10 :=
λ T, i2p (simplify_array_ptr_hyp_learn_loc l β ly base idx len T). λ T, i2p (simplify_array_ptr_hyp_learn_loc l β ly base idx len T).
*) *)
......
...@@ -48,23 +48,23 @@ Section globals. ...@@ -48,23 +48,23 @@ Section globals.
SimplifyHyp (global_with_type name β ty) (Some 0%N) := SimplifyHyp (global_with_type name β ty) (Some 0%N) :=
λ T, i2p (simplify_global_with_type_hyp name β ty T). λ T, i2p (simplify_global_with_type_hyp name β ty T).
Lemma simplify_global_with_type_goal name β ty l T `{!FastDone (global_locs !! name = Some l)} : Lemma simplify_global_with_type_goal name β ty l T `{!TCFastDone (global_locs !! name = Some l)} :
T (l ◁ₗ{β} ty) - T (l ◁ₗ{β} ty) -
simplify_goal (global_with_type name β ty) T. simplify_goal (global_with_type name β ty) T.
Proof. unfold FastDone in *. iIntros "HT". iExists _. iFrame. iIntros "?". iExists _. by iFrame. Qed. Proof. unfold TCFastDone in *. iIntros "HT". iExists _. iFrame. iIntros "?". iExists _. by iFrame. Qed.
Global Instance simplify_global_with_type_goal_inst name β ty l `{!FastDone (global_locs !! name = Some l)}: Global Instance simplify_global_with_type_goal_inst name β ty l `{!TCFastDone (global_locs !! name = Some l)}:
SimplifyGoal (global_with_type name β ty) (Some 0%N) := SimplifyGoal (global_with_type name β ty) (Some 0%N) :=
λ T, i2p (simplify_global_with_type_goal name β ty l T). λ T, i2p (simplify_global_with_type_goal name β ty l T).
Lemma simplify_initialized_hyp A (x : A) name ty l T `{!FastDone (global_locs !! name = Some l)} `{!FastDone (global_initialized_types !! name = Some ty)}: Lemma simplify_initialized_hyp A (x : A) name ty l T `{!TCFastDone (global_locs !! name = Some l)} `{!TCFastDone (global_initialized_types !! name = Some ty)}:
( (Heq : A = ty.(gt_A)), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x) - T) - ( (Heq : A = ty.(gt_A)), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x) - T) -
simplify_hyp (initialized name x) T. simplify_hyp (initialized name x) T.
Proof. Proof.
unfold FastDone in *. iDestruct 1 as (?) "HT". iDestruct 1 as (l' ??? Heq2) "Hl". simplify_eq. iApply "HT" => /=. unfold TCFastDone in *. iDestruct 1 as (?) "HT". iDestruct 1 as (l' ??? Heq2) "Hl". simplify_eq. iApply "HT" => /=.
(** HERE WE USE AXIOM K! *) (** HERE WE USE AXIOM K! *)
by rewrite (UIP_refl _ _ Heq2). by rewrite (UIP_refl _ _ Heq2).
Qed. Qed.
Global Instance simplify_initialized_hyp_inst A x name ty l `{!FastDone (global_locs !! name = Some l)} `{!FastDone (global_initialized_types !! name = Some ty)}: Global Instance simplify_initialized_hyp_inst A x name ty l `{!TCFastDone (global_locs !! name = Some l)} `{!TCFastDone (global_initialized_types !! name = Some ty)}:
SimplifyHyp (initialized name x) (Some 0%N) := SimplifyHyp (initialized name x) (Some 0%N) :=
λ T, i2p (simplify_initialized_hyp A x name ty l T). λ T, i2p (simplify_initialized_hyp A x name ty l T).
...@@ -75,11 +75,11 @@ Section globals. ...@@ -75,11 +75,11 @@ Section globals.
initialized name x. initialized name x.
Proof. iIntros (??) "Hl". iExists _, _. by iFrame. Qed. Proof. iIntros (??) "Hl". iExists _, _. by iFrame. Qed.
Lemma simplify_initialized_goal A (x : A) name l ty T `{!FastDone (global_locs !! name = Some l)} `{!FastDone (global_initialized_types !! name = Some ty)} : Lemma simplify_initialized_goal A (x : A) name l ty T `{!TCFastDone (global_locs !! name = Some l)} `{!TCFastDone (global_initialized_types !! name = Some ty)} :
T (( (Heq : A = ty.(gt_A)), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x))) - T (( (Heq : A = ty.(gt_A)), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x))) -
simplify_goal (initialized name x) T. simplify_goal (initialized name x) T.
Proof. unfold FastDone in *. iIntros "HT". iExists _. iFrame. by iApply initialized_intro. Qed. Proof. unfold TCFastDone in *. iIntros "HT". iExists _. iFrame. by iApply initialized_intro. Qed.
Global Instance simplify_initialized_goal_inst A (x : A) name ty l `{!FastDone (global_locs !! name = Some l)} `{!FastDone (global_initialized_types !! name = Some ty)}: Global Instance simplify_initialized_goal_inst A (x : A) name ty l `{!TCFastDone (global_locs !! name = Some l)} `{!TCFastDone (global_initialized_types !! name = Some ty)}:
SimplifyGoal (initialized name x) (Some 0%N) := SimplifyGoal (initialized name x) (Some 0%N) :=
λ T, i2p (simplify_initialized_goal A x name l ty T). λ T, i2p (simplify_initialized_goal A x name l ty T).
......
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