Commit 88638cda authored by Ralf Jung's avatar Ralf Jung
Browse files

simplify sep_split (patch is by Robbert)

parent 324b4863
...@@ -106,30 +106,14 @@ Module uPred_reflection. Section uPred_reflection. ...@@ -106,30 +106,14 @@ Module uPred_reflection. Section uPred_reflection.
by rewrite IH. by rewrite IH.
Qed. Qed.
Fixpoint remove_all (l k : list nat) : option (list nat) := Lemma split_l Σ e ns e' :
match l with cancel ns e = Some e' eval Σ e (eval Σ (to_expr ns) eval Σ e')%I.
| [] => Some k
| n :: l => '(i,_) list_find (n =) k; remove_all l (delete i k)
end.
Lemma remove_all_permutation l k k' : remove_all l k = Some k' k l ++ k'.
Proof.
revert k k'; induction l as [|n l IH]; simpl; intros k k' Hk.
{ by simplify_eq. }
destruct (list_find _ _) as [[i ?]|] eqn:?Hk'; simplify_eq/=.
move: Hk'; intros [? <-]%list_find_Some.
rewrite -(IH (delete i k) k') // -delete_Permutation //.
Qed.
Lemma split_l Σ e l k :
remove_all l (flatten e) = Some k
eval Σ e (eval Σ (to_expr l) eval Σ (to_expr k))%I.
Proof. Proof.
intros He%remove_all_permutation. intros He%flatten_cancel.
by rewrite eval_flatten He fmap_app big_sep_app !eval_to_expr. by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
Qed. Qed.
Lemma split_r Σ e l k : Lemma split_r Σ e ns e' :
remove_all l (flatten e) = Some k cancel ns e = Some e' eval Σ e (eval Σ e' eval Σ (to_expr ns))%I.
eval Σ e (eval Σ (to_expr k) eval Σ (to_expr l))%I.
Proof. intros. rewrite /= comm. by apply split_l. Qed. Proof. intros. rewrite /= comm. by apply split_l. Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}. Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
...@@ -198,7 +182,7 @@ Tactic Notation "to_front" open_constr(Ps) := ...@@ -198,7 +182,7 @@ Tactic Notation "to_front" open_constr(Ps) :=
| uPred_reflection.QuoteArgs _ _ ?ns' => ns' | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in end in
eapply entails_equiv_l; eapply entails_equiv_l;
first (apply uPred_reflection.split_l with (l:=ns'); cbv; reflexivity); first (apply uPred_reflection.split_l with (ns:=ns'); cbv; reflexivity);
simpl). simpl).
Tactic Notation "to_back" open_constr(Ps) := Tactic Notation "to_back" open_constr(Ps) :=
...@@ -209,7 +193,7 @@ Tactic Notation "to_back" open_constr(Ps) := ...@@ -209,7 +193,7 @@ Tactic Notation "to_back" open_constr(Ps) :=
| uPred_reflection.QuoteArgs _ _ ?ns' => ns' | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in end in
eapply entails_equiv_l; eapply entails_equiv_l;
first (apply uPred_reflection.split_r with (l:=ns'); cbv; reflexivity); first (apply uPred_reflection.split_r with (ns:=ns'); cbv; reflexivity);
simpl). simpl).
(** [sep_split] is used to introduce a (★). (** [sep_split] is used to introduce 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