Commit 29a97bb2 by Ralf Jung

### use solve_proper_core for saved_pred_own_contractive

parent 8c13c02f
 ... @@ -620,9 +620,9 @@ Definition ccompose {A B C} ... @@ -620,9 +620,9 @@ Definition ccompose {A B C} (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g). (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g). Instance: Params (@ccompose) 3. Instance: Params (@ccompose) 3. Infix "◎" := ccompose (at level 40, left associativity). Infix "◎" := ccompose (at level 40, left associativity). Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n : Global Instance ccompose_ne {A B C} : f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2. NonExpansive2 (@ccompose A B C). Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed. Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed. (* Function space maps *) (* Function space maps *) Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B') Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B') ... ...
 ... @@ -95,8 +95,7 @@ Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ) ... @@ -95,8 +95,7 @@ Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ) Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ). Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ). Proof. Proof. intros n Φ Φ' HΦ. rewrite /saved_pred_own /saved_anything_own /=. solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | f_contractive | f_equiv ]). do 3 f_equiv. intros x. rewrite /=. by f_contractive. Qed. Qed. Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) : Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!