Commit 33fbef9e authored by Michael Sammler's avatar Michael Sammler
Browse files

Use multisuccess of typeclasses eauto to get rid of n parameter in FindInContext

parent 1ab6c843
Pipeline #51803 passed with stage
in 31 minutes and 41 seconds
......@@ -21,10 +21,10 @@ Record find_in_context_info {Σ} : Type := {
(* The nat n is necessary to allow different options, they are tried starting from 0. *)
Definition find_in_context {Σ} (fic : find_in_context_info) (T : fic.(fic_A) iProp Σ) : iProp Σ :=
( b, fic.(fic_Prop) b T b).
Class FindInContext {Σ} (fic : find_in_context_info) (n : nat) (key : Set) : Type :=
Class FindInContext {Σ} (fic : find_in_context_info) (key : Set) : Type :=
find_in_context_proof T: iProp_to_Prop (Σ:=Σ) (find_in_context fic T)
.
Global Hint Mode FindInContext + + + - : typeclass_instances.
Global Hint Mode FindInContext + + - : typeclass_instances.
Inductive FICSyntactic : Set :=.
(** ** Instances *)
......@@ -36,7 +36,7 @@ Lemma find_in_context_direct {Σ B} P (T : B → iProp Σ):
find_in_context (FindDirect P) T.
Proof. done. Qed.
Global Instance find_in_context_direct_inst {Σ B} (P : _ iProp Σ) :
FindInContext (FindDirect P) 0%nat FICSyntactic :=
FindInContext (FindDirect P) FICSyntactic | 1 :=
λ T : B _, i2p (find_in_context_direct P T).
(** ** [FindHypEqual] *)
......
......@@ -517,22 +517,16 @@ Ltac liExist protect :=
| _ => fail "do_exist: unknown goal"
end.
Ltac liFindInContext :=
lazymatch goal with
| |- envs_entails _ (find_in_context ?fic ?T) =>
let rec go n :=
let inst := eval cbv beta in (_ : FindInContext fic n _) in
first [
lazymatch (type of inst) with
| FindInContext _ _ ?key =>
simple notypeclasses refine (tac_fast_apply (inst _).(i2p_proof) _); simpl;
repeat liExist false; liFindHypOrTrue key
end
| go constr:(S n)
]
in
go constr:(0%nat)
let key := open_constr:(_) in
(* We exploit that [typeclasses eauto] is multi-success to enable
multiple implementations of [FindInContext]. They are tried in the
order of their priorities.
See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Multi-success.20TC.20resolution.20from.20ltac.3F/near/242759123 *)
simple notypeclasses refine (tac_fast_apply ((_ : FindInContext fic key) _).(i2p_proof) _);
[ shelve | typeclasses eauto | simpl; repeat liExist false; liFindHypOrTrue key ]
end.
Ltac liTrue :=
......
......@@ -49,16 +49,16 @@ Ltac solve_loc_eq :=
Inductive FICLocSemantic : Set :=.
Global Instance find_in_context_type_loc_semantic_inst `{!typeG Σ} l :
FindInContext (FindLoc l) 2%nat FICLocSemantic :=
FindInContext (FindLoc l) FICLocSemantic | 20 :=
λ T, i2p (find_in_context_type_loc_id l T).
Global Instance find_in_context_type_val_P_loc_semantic_inst `{!typeG Σ} (l : loc) :
FindInContext (FindValP l) 2%nat FICLocSemantic :=
FindInContext (FindValP l) FICLocSemantic | 20 :=
λ T, i2p (find_in_context_type_val_P_loc_id l T).
Global Instance find_in_context_loc_in_bounds_semantic_inst `{!typeG Σ} l :
FindInContext (FindLocInBounds l) 2%nat FICLocSemantic :=
FindInContext (FindLocInBounds l) FICLocSemantic | 20 :=
λ T, i2p (find_in_context_loc_in_bounds l T).
Global Instance find_in_context_loc_in_bounds_type_semantic_inst `{!typeG Σ} l :
FindInContext (FindLocInBounds l) 3%nat FICLocSemantic :=
FindInContext (FindLocInBounds l) FICLocSemantic | 30 :=
λ T, i2p (find_in_context_loc_in_bounds_loc l T).
Lemma tac_solve_loc_eq `{!typeG Σ} l1 β1 ty1 l2 β2 ty2:
......
......@@ -95,7 +95,7 @@ Section globals.
find_in_context (FindInitialized name A) T.
Proof. iDestruct 1 as (x) "[Hinit HT]". iExists _. iFrame. Qed.
Global Instance find_in_context_initialized_inst name A :
FindInContext (FindInitialized name A) 0%nat FICSyntactic :=
FindInContext (FindInitialized name A) FICSyntactic | 1 :=
λ T, i2p (find_in_context_initialized name A T).
Lemma subsume_initialized name A (x1 x2 : A) T:
......
......@@ -358,7 +358,7 @@ Section own.
iSplit => //. by iFrame.
Qed.
Global Instance find_in_context_type_loc_own_inst l :
FindInContext (FindLoc l) 1%nat FICSyntactic :=
FindInContext (FindLoc l) FICSyntactic | 10 :=
λ T, i2p (find_in_context_type_loc_own l T).
Lemma find_in_context_type_val_own l T:
......@@ -366,7 +366,7 @@ Section own.
find_in_context (FindVal l) T.
Proof. iDestruct 1 as (ty) "[Hl HT]". iExists _ => /=. by iFrame. Qed.
Global Instance find_in_context_type_val_own_inst (l : loc) :
FindInContext (FindVal l) 1%nat FICSyntactic :=
FindInContext (FindVal l) FICSyntactic | 10 :=
λ T, i2p (find_in_context_type_val_own l T).
Lemma find_in_context_type_val_own_singleton (l : loc) T:
......@@ -374,7 +374,7 @@ Section own.
find_in_context (FindVal l) T.
Proof. iIntros "[_ HT]". iExists _ => /=. iFrame "HT". simpl. done. Qed.
Global Instance find_in_context_type_val_own_singleton_inst (l : loc):
FindInContext (FindVal l) 2%nat FICSyntactic :=
FindInContext (FindVal l) FICSyntactic | 20 :=
λ T, i2p (find_in_context_type_val_own_singleton l T).
(* We cannot use place here as it can easily lead to an infinite
......@@ -387,7 +387,7 @@ Section own.
find_in_context (FindValP l) T.
Proof. rewrite /place'. iIntros "[_ HT]". iExists _. iFrame "HT" => //=. Qed.
Global Instance find_in_context_type_val_P_own_singleton_inst (l : loc):
FindInContext (FindValP l) 3%nat FICSyntactic :=
FindInContext (FindValP l) FICSyntactic | 30 :=
λ T, i2p (find_in_context_type_val_P_own_singleton l T).
End own.
Typeclasses Opaque place'.
......
......@@ -615,7 +615,7 @@ Section typing.
find_in_context (FindLoc l) T.
Proof. iDestruct 1 as (β ty) "[Hl HT]". iExists (_, _) => /=. iFrame. Qed.
Global Instance find_in_context_type_loc_id_inst l :
FindInContext (FindLoc l) 0%nat FICSyntactic :=
FindInContext (FindLoc l) FICSyntactic | 1 :=
λ T, i2p (find_in_context_type_loc_id l T).
Lemma find_in_context_type_val_id v T:
......@@ -623,7 +623,7 @@ Section typing.
find_in_context (FindVal v) T.
Proof. iDestruct 1 as (ty) "[Hl HT]". iExists _ => /=. iFrame. Qed.
Global Instance find_in_context_type_val_id_inst v :
FindInContext (FindVal v) 0%nat FICSyntactic :=
FindInContext (FindVal v) FICSyntactic | 1 :=
λ T, i2p (find_in_context_type_val_id v T).
Lemma find_in_context_type_val_P_id v T:
......@@ -631,7 +631,7 @@ Section typing.
find_in_context (FindValP v) T.
Proof. iDestruct 1 as (ty) "[Hl HT]". iExists (ty_own_val ty _) => /=. iFrame. Qed.
Global Instance find_in_context_type_val_P_id_inst v :
FindInContext (FindValP v) 0%nat FICSyntactic :=
FindInContext (FindValP v) FICSyntactic | 1 :=
λ T, i2p (find_in_context_type_val_P_id v T).
Lemma find_in_context_type_val_P_loc_id l T:
......@@ -639,7 +639,7 @@ Section typing.
find_in_context (FindValP l) T.
Proof. iDestruct 1 as (β ty) "[Hl HT]". iExists (ty_own _ _ _) => /=. iFrame. Qed.
Global Instance find_in_context_type_val_P_loc_id_inst (l : loc) :
FindInContext (FindValP l) 1%nat FICSyntactic :=
FindInContext (FindValP l) FICSyntactic | 10 :=
λ T, i2p (find_in_context_type_val_P_loc_id l T).
Lemma find_in_context_type_val_or_loc_P_id_val (v : val) (l : loc) T:
......@@ -647,7 +647,7 @@ Section typing.
find_in_context (FindValOrLoc v l) T.
Proof. iDestruct 1 as (ty) "[Hl HT]". iExists (ty_own_val ty _) => /=. iFrame. Qed.
Global Instance find_in_context_type_val_or_loc_P_id_val_inst v l:
FindInContext (FindValOrLoc v l) 0%nat FICSyntactic :=
FindInContext (FindValOrLoc v l) FICSyntactic | 1 :=
λ T, i2p (find_in_context_type_val_or_loc_P_id_val v l T).
Lemma find_in_context_type_val_or_loc_P_val_loc (lv l : loc) T:
......@@ -655,7 +655,7 @@ Section typing.
find_in_context (FindValOrLoc lv l) T.
Proof. iDestruct 1 as (β ty) "[Hl HT]". iExists _. by iFrame. Qed.
Global Instance find_in_context_type_val_or_loc_P_val_loc_inst (lv l : loc):
FindInContext (FindValOrLoc lv l) 1%nat FICSyntactic :=
FindInContext (FindValOrLoc lv l) FICSyntactic | 10 :=
λ T, i2p (find_in_context_type_val_or_loc_P_val_loc lv l T).
Lemma find_in_context_type_val_or_loc_P_id_loc (v : val) (l : loc) T:
......@@ -663,7 +663,7 @@ Section typing.
find_in_context (FindValOrLoc v l) T.
Proof. iDestruct 1 as (β ty) "[Hl HT]". iExists (l ◁ₗ{β} ty)%I => /=. iFrame. Qed.
Global Instance find_in_context_type_val_or_loc_P_id_loc_inst v l:
FindInContext (FindValOrLoc v l) 2%nat FICSyntactic :=
FindInContext (FindValOrLoc v l) FICSyntactic | 20 :=
λ T, i2p (find_in_context_type_val_or_loc_P_id_loc v l T).
Lemma find_in_context_loc_in_bounds l T :
......@@ -671,7 +671,7 @@ Section typing.
find_in_context (FindLocInBounds l) T.
Proof. iDestruct 1 as (n) "[??]". iExists (loc_in_bounds _ _) => /=. iFrame. Qed.
Global Instance find_in_context_loc_in_bounds_inst l :
FindInContext (FindLocInBounds l) 0 FICSyntactic :=
FindInContext (FindLocInBounds l) FICSyntactic | 1 :=
λ T, i2p (find_in_context_loc_in_bounds l T).
Lemma find_in_context_loc_in_bounds_loc l T :
......@@ -679,7 +679,7 @@ Section typing.
find_in_context (FindLocInBounds l) T.
Proof. iDestruct 1 as (β ty) "[??]". iExists (ty_own _ _ _) => /=. iFrame. Qed.
Global Instance find_in_context_loc_in_bounds_loc_inst l :
FindInContext (FindLocInBounds l) 1 FICSyntactic :=
FindInContext (FindLocInBounds l) FICSyntactic | 10 :=
λ T, i2p (find_in_context_loc_in_bounds_loc l T).
Lemma find_in_context_alloc_alive_global l T :
......@@ -687,7 +687,7 @@ Section typing.
find_in_context (FindAllocAlive l) T.
Proof. iDestruct 1 as "?". iExists _ => /=. iFrame. Qed.
Global Instance find_in_context_alloc_alive_global_inst l :
FindInContext (FindAllocAlive l) 0 FICSyntactic :=
FindInContext (FindAllocAlive l) FICSyntactic | 1 :=
λ T, i2p (find_in_context_alloc_alive_global l T).
Lemma find_in_context_alloc_alive_loc l T :
......@@ -695,7 +695,7 @@ Section typing.
find_in_context (FindAllocAlive l) T.
Proof. iDestruct 1 as (β ty) "[??]". iExists (ty_own _ _ _) => /=. iFrame. Qed.
Global Instance find_in_context_alloc_alive_loc_inst l :
FindInContext (FindAllocAlive l) 1 FICSyntactic :=
FindInContext (FindAllocAlive l) FICSyntactic | 10 :=
λ T, i2p (find_in_context_alloc_alive_loc l T).
Global Instance related_to_loc l β ty : RelatedTo (l ◁ₗ{β} ty) | 100 := {| rt_fic := FindLoc l |}.
......
Supports Markdown
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