Commit f531cc9d by Ralf Jung

### generalize into_and_sep_affine so that generalizing just the conjunction...

`generalize into_and_sep_affine so that generalizing just the conjunction instance for IntoExist is sufficient`
parent 7da8952e
 ... @@ -608,9 +608,9 @@ Proof. ... @@ -608,9 +608,9 @@ Proof. rewrite /IntoAnd /= intuitionistically_sep rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //. -and_sep_intuitionistically intuitionistically_and //. Qed. Qed. Global Instance into_and_sep_affine P Q : Global Instance into_and_sep_affine p P Q : TCOr (Affine P) (Absorbing Q) → TCOr (Absorbing P) (Affine Q) → TCOr (Affine P) (Absorbing Q) → TCOr (Absorbing P) (Affine Q) → IntoAnd true (P ∗ Q) P Q. IntoAnd p (P ∗ Q) P Q. Proof. intros. by rewrite /IntoAnd /= sep_and. Qed. Proof. intros. by rewrite /IntoAnd /= sep_and. Qed. Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝. Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝. ... @@ -807,32 +807,32 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed. ... @@ -807,32 +807,32 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed. Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name : Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name : IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name. IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name. Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed. Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed. (* Low-priority instance falling back to treating a conjunction with a pure (* This instance is generalized to let us use [iIntros (P) "..."] and left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as [as [% ...]]. There is some risk of backtracking here, but that should only [% ...]]. happen in failing cases (assuming that appropriate modality commuting instances are provided for both conjunctions and existential quantification). The alternative of providing specialized instances for cases like ⌜P ∧ Q⌝ turned out to not be tenable. [to_ident_name H] makes the default name [H] when [P] is destructed with [to_ident_name H] makes the default name [H] when [P] is destructed with [iExistDestruct] *) [iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *) Global Instance into_exist_and_pure PQ P Q φ : Global Instance into_exist_and_pure PQ P Q (φ : Type) : IntoAnd false PQ P Q → IntoAnd false PQ P Q → IntoPureT P φ → IntoPureT P φ → IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100. IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 10. Proof. Proof. intros HPQ (φ'&->&?). rewrite /IntoAnd /= in HPQ. intros HPQ (φ'&->&?). rewrite /IntoAnd /= in HPQ. rewrite /IntoExist HPQ (into_pure P). rewrite /IntoExist HPQ (into_pure P). apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ). apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ). Qed. Qed. (* Low-priority instance falling back to treating a sep. conjunction with a pure (* [to_ident_name H] makes the default name [H] when [P] is destructed with left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as [iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *) [% ...]]. Global Instance into_exist_sep_pure P Q (φ : Type) : [to_ident_name H] makes the default name [H] when [P] is destructed with [iExistDestruct] *) Global Instance into_exist_sep_pure PQ P Q φ : IntoSep PQ P Q → IntoPureT P φ → IntoPureT P φ → TCOr (Affine P) (Absorbing Q) → TCOr (Affine P) (Absorbing Q) → IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100. IntoExist (P ∗ Q) (λ _ : φ, Q) (to_ident_name H). Proof. Proof. intros HPQ (φ'&->&?) ?. rewrite /IntoSep in HPQ. rewrite /IntoExist HPQ. intros (φ'&->&?) ?. rewrite /IntoExist. eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?. eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?. rewrite -exist_intro //. apply sep_elim_r, _. rewrite -exist_intro //. apply sep_elim_r, _. Qed. Qed. ... ...
 ... @@ -176,12 +176,21 @@ Global Arguments from_and {_} _%I _%I _%I {_}. ... @@ -176,12 +176,21 @@ Global Arguments from_and {_} _%I _%I _%I {_}. Global Hint Mode FromAnd + ! - - : typeclass_instances. Global Hint Mode FromAnd + ! - - : typeclass_instances. Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *) Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *) (** The [IntoAnd p P Q1 Q2] class is used (together with [IntoSep]) to handle [[H1 H2]] destruct patterns. If [p] is [true] then the destruct is happening in the intuitionistic context. The inputs are [p P] and the outputs are [Q1 Q2]. *) Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) := Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) := into_and : □?p P ⊢ □?p (Q1 ∧ Q2). into_and : □?p P ⊢ □?p (Q1 ∧ Q2). Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never. Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never. Global Arguments into_and {_} _ _%I _%I _%I {_}. Global Arguments into_and {_} _ _%I _%I _%I {_}. Global Hint Mode IntoAnd + + ! - - : typeclass_instances. Global Hint Mode IntoAnd + + ! - - : typeclass_instances. (** The [IntoSep P Q1 Q2] class is used (together with [IntoAnd]) to handle [[H1 H2]] destruct patterns. The input is [P] and the outputs are [Q1 Q2]. *) Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) := Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) := into_sep : P ⊢ Q1 ∗ Q2. into_sep : P ⊢ Q1 ∗ Q2. Global Arguments IntoSep {_} _%I _%I _%I : simpl never. Global Arguments IntoSep {_} _%I _%I _%I : simpl never. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!