Commit f1b30a2e by Robbert Krebbers

### Make iSpecialize work with coercions.

```For example, when having `"H" : ∀ x : Z, P x`, using
`iSpecialize ("H" \$! (0:nat))` now works. We do this by first
resolving the `IntoForall` type class, and then instantiating
the quantifier.```
parent 2dfb8987
Pipeline #3880 canceled with stage
in 53 seconds
 ... @@ -791,12 +791,14 @@ Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) : ... @@ -791,12 +791,14 @@ Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) : (∀ a, Δ ⊢ ⌜φ a⌝) → Δ ⊢ ⌜∀ a, φ a⌝. (∀ a, Δ ⊢ ⌜φ a⌝) → Δ ⊢ ⌜∀ a, φ a⌝. Proof. intros. rewrite pure_forall. by apply forall_intro. Qed. Proof. intros. rewrite pure_forall. by apply forall_intro. Qed. Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q x : Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q : envs_lookup i Δ = Some (p, P) → IntoForall P Φ → envs_lookup i Δ = Some (p, P) → IntoForall P Φ → envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' → (∃ x : A, (Δ' ⊢ Q) → Δ ⊢ Q. envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' ∧ (Δ' ⊢ Q)) → Δ ⊢ Q. Proof. Proof. intros. rewrite envs_simple_replace_sound //; simpl. intros ?? (x&?&?). rewrite envs_simple_replace_sound //; simpl. by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r. by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r. Qed. Qed. ... ...
 ... @@ -272,11 +272,11 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := ... @@ -272,11 +272,11 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := match xs with match xs with | hnil => idtac | hnil => idtac | hcons ?x ?xs => | hcons ?x ?xs => eapply tac_forall_specialize with _ H _ _ _ x; (* (i:=H) (a:=x) *) eapply tac_forall_specialize with _ H _ _ _; (* (i:=H) (a:=x) *) [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found" [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found" |let P := match goal with |- IntoForall ?P _ => P end in |let P := match goal with |- IntoForall ?P _ => P end in apply _ || fail 1 "iSpecialize: cannot instantiate" P "with" x apply _ || fail 1 "iSpecialize: cannot instantiate" P "with" x |env_cbv; reflexivity|go xs] |exists x; split; [env_cbv; reflexivity|go xs]] end in end in go xs. go xs. ... ...
 ... @@ -120,3 +120,7 @@ Qed. ... @@ -120,3 +120,7 @@ Qed. Lemma demo_11 (M : ucmraT) (P Q R : uPred M) : Lemma demo_11 (M : ucmraT) (P Q R : uPred M) : (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R. (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R. Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed. Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed. (* Check coercions *) Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x. Proof. iIntros "HP". iExists (0:nat). iApply ("HP" \$! (0:nat)). Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!