Commit 9ea6fa45 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve `iSpecialize ("H" $! x1 .. xn)`.

Instead of doing all the instantiations by invoking a single type
class search, it now performs the instantiations by invoking
individual type class searches. This a.) gives better error messages
and b.) works when `xj` depends on `xi`.
parent 211c2363
Pipeline #3872 passed with stage
in 3 minutes and 49 seconds
......@@ -601,6 +601,13 @@ Global Instance into_exist_laterN {A} n P (Φ : A → uPred M) :
IntoExist P Φ Inhabited A IntoExist (^n P) (λ a, ^n (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A uPred M) : IntoForall ( a, Φ a) Φ.
Proof. done. Qed.
Global Instance into_forall_always {A} P (Φ : A uPred M) :
IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
(* FromModal *)
Global Instance from_modal_later P : FromModal ( P) P.
Proof. apply later_intro. Qed.
......
......@@ -88,6 +88,11 @@ Class IntoExist {M A} (P : uPred M) (Φ : A → uPred M) :=
Arguments into_exist {_ _} _ _ {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
Class IntoForall {M A} (P : uPred M) (Φ : A uPred M) :=
into_forall : P x, Φ x.
Arguments into_forall {_ _} _ _ {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.
Class FromModal {M} (P Q : uPred M) := from_modal : Q P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
......
......@@ -791,27 +791,13 @@ Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) :
( a, Δ ⌜φ a) Δ a, φ a.
Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
Class ForallSpecialize {As} (xs : hlist As)
(P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P Φ xs.
Arguments forall_specialize {_} _ _ _ {_}.
Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
Proof. done. Qed.
Global Instance forall_specialize_cons A As x xs Φ (Ψ : A himpl As (uPred M)) :
( x, ForallSpecialize xs (Φ x) (Ψ x))
ForallSpecialize (hcons x xs) ( x : A, Φ x) Ψ.
Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
Global Instance forall_specialize_always As xs P (Ψ : himpl As (uPred M)) :
ForallSpecialize xs P Ψ ForallSpecialize xs ( P) Ψ | 101.
Proof. rewrite /ForallSpecialize=> ->. by rewrite always_elim. Qed.
Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
envs_lookup i Δ = Some (p, P) ForallSpecialize xs P Φ
envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ'
Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A uPred M) Q x :
envs_lookup i Δ = Some (p, P) IntoForall P Φ
envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ'
(Δ' Q) Δ Q.
Proof.
intros. rewrite envs_simple_replace_sound //; simpl.
by rewrite right_id (forall_specialize _ P) wand_elim_r.
by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r.
Qed.
Lemma tac_forall_revert {A} Δ (Φ : A uPred M) :
......@@ -849,5 +835,3 @@ Proof.
rewrite right_id HΔ always_if_elim. by apply elim_modal.
Qed.
End tactics.
Hint Mode ForallSpecialize + - - ! - : typeclass_instances.
......@@ -268,15 +268,17 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
match xs with
| hnil => idtac
| _ =>
eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
[env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
|let P := match goal with |- ForallSpecialize _ ?P _ => P end in
apply _ || fail 1 "iSpecialize:" P "not a forall of the right arity or type"
|cbn [himpl hcurry]; reflexivity|]
end.
let rec go xs :=
match xs with
| hnil => idtac
| hcons ?x ?xs =>
eapply tac_forall_specialize with _ H _ _ _ x; (* (i:=H) (a:=x) *)
[env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
|let P := match goal with |- IntoForall ?P _ => P end in
apply _ || fail 1 "iSpecialize:" P "not a forall or not a forall of the right type"
|env_cbv; reflexivity|go xs]
end in
go xs.
Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let solve_to_wand H1 :=
......
  • Thanks :)

    Do you think we should have dedicated testcases for things like this? LambdaRust may stop using this feature at some point; also, it'd be nice to notice such regressions before lambdaRust is updated to a new Iris.

  • I don't think these things break arbitrarily, but I can put something involving a dependent type in tests/proofmode.v.

    Edited by Robbert Krebbers
  • I'm quite suspicious for this change, given that the default behavior of Coq tactics is to do a single typeclass (isn't it?). For example, it seems like it would prevent using mutually dependent type classes.

  • I don't understand what you mean. You could give an example of "mutually dependent type classes."

  • I don't have a specific example in mind, but imagine you have two typeclasses A and Bwith one parameter each. Consider the typeclass search problem A ?x, B ?x. I.e., the search algorithm has to find an instance for A and an instance for B, such that the value of the parameter coincides. The only way to solve this problem properly is to consider both A and B at the same time. If you consider them one after the other, you will potentially find a instance for A that leaves no possibility for B.

  • Alright, in your problem this would be problematic when you have

    Class C (x : A) := c : A x -> B x -> C x.

    Then if you infer C ?x, it would backtrack on different instantiations of A ?x, but that would not happen when you infer A ?x and B ?x separately.

    In the code concerning this commit this problem does not apply: there is no non-determinism when instantiating a universal quantifier (and hence no backtracking).

  • By the way, I initially implemented the idea of instantiating a list of universal quantifiers in one to improve performance. But as shown here, this optimization did not work out well with dependent types.

    Edited by Robbert Krebbers
  • there is no non-determinism when instantiating a universal quantifier (and hence no backtracking).

    I don't see why there would be no non-determinism, given that there is a typeclass search.

  • Because the instances of IntoForall are unique

  • Right, but what if the expression I am using for instantiating triggers a typeclass search?

  • Alright, I see the problem, but this did not work with the old iSpecialize either, for example:

    From iris.proofmode Require Import tactics.
    
    Class A := a : nat.
    Class B := b : nat.
    Class C (x : A) (y : B).
    
    Instance a1 : A := 1.
    Instance a2 : A := 2.
    
    Instance b1 : B := 1.
    
    Instance c11 : C a1 b1.
    
    Goal  M : ucmraT,
      ( (x : A) (y : B) (z : C x y), False) - (False : uPred M).
    iIntros (M) "H".
    iPoseProof ("H" $! a1 b1) as "Hfoo". (* picks a1 b1 *)
    iSpecialize ("H" $! a1 b1 _). (* already failed work with the old iSpecialize *)
    Edited by Robbert Krebbers
  • I was thinking of a situation like this:

    From iris.proofmode Require Import tactics.
    
    Class A (n : nat) := a : True.
    Class B (n : nat) := b : n = 1.
    
    Instance a1 : A 1 := I.
    Instance a2 : A 2 := I.
    
    Instance b1 : B 1 := eq_refl.
    
    Goal ∀ M : ucmraT,
      (∀ n (x : A n) (y : B n), False) -∗ (False: uPred M).
    iIntros (M) "H".
    iPoseProof ("H" $! _) as "Hfoo".
    iSpecialize ("Hfoo" $! _ _).
    done.

    It used to work, but no longer now. But now that I see an actual example, I am figuring out that this might not be THAT important.

  • It would be interesting to figure out how to make that AND the actual example work. I don't know.

    Also, in the old setting I would not know how to achieve something like f1b30a2e.

  • mentioned in commit 0e1825e2

    Toggle commit list
  • but I can put something involving a dependent type in tests/proofmode.v.

    Done, see 0e1825e2.

  • Thanks :)

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