Commit 1ef06fb4 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix warnings about missing Global

parent f8d092f9
Pipeline #59597 passed with stage
in 22 minutes and 15 seconds
......@@ -32,6 +32,7 @@ build-coq.8.14.1:
variables:
OPAM_PINS: "coq version 8.14.1"
MANGLE_NAMES: "1"
DENY_WARNINGS: "1"
build-coq.8.13.2:
<<: *template
......
......@@ -33,11 +33,11 @@ Fixpoint obs_val (v_t v_s : val) {struct v_s} : Prop :=
(** The simulang instance of [prog_ref]. *)
Definition prog_ref := prog_ref init_state "main" #() obs_val.
Instance obs_val_refl : Reflexive obs_val.
Global Instance obs_val_refl : Reflexive obs_val.
Proof.
intros v. induction v as [ [ | | | | | ] | | | ]; naive_solver.
Qed.
Instance obs_val_trans : Transitive obs_val.
Global Instance obs_val_trans : Transitive obs_val.
Proof.
intros v1 v2 v3 H1 H2.
induction v3 as [ [ | | | | | ] | v31 IH1 v32 IH2 | v3 IH | v3 IH] in v1, v2, H1, H2 |-*.
......
......@@ -29,10 +29,10 @@ Qed.
Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' (λ l, (loc_block l, loc_idx l)) (λ '(i, j), {| loc_block := i; loc_idx := j |})); intros []. Qed.
Program Instance block_infinite : Infinite block :=
Global Program Instance block_infinite : Infinite block :=
inj_infinite DynBlock (λ b, if b is DynBlock b then Some b else None) _.
Next Obligation. done. Qed.
Program Instance loc_infinite : Infinite loc :=
Global Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ '(i, j), {| loc_block := i; loc_idx := j |}) (λ l, Some ((loc_block l, loc_idx l))) _.
Next Obligation. done. Qed.
......
......@@ -94,8 +94,8 @@ Section definitions.
End definitions.
Typeclasses Opaque heap_mapsto heap_block_size heap_mapsto_vec.
Instance: Params (@heap_mapsto) 4 := {}.
Instance: Params (@heap_block_size) 5 := {}.
Global Instance: Params (@heap_mapsto) 4 := {}.
Global Instance: Params (@heap_block_size) 5 := {}.
(* Notation "l ↦{ q } v" := (heap_mapsto l q v) *)
(* (at level 20, q at level 50, format "l ↦{ q } v") : bi_scope. *)
......
......@@ -1136,7 +1136,7 @@ End safe_reach.
(* discrete OFE instance for expr and thread_id *)
Definition exprO {Λ : language} := leibnizO (expr Λ).
Instance expr_equiv {Λ} : Equiv (expr Λ). apply exprO. Defined.
Global Instance expr_equiv {Λ} : Equiv (expr Λ). apply exprO. Defined.
Definition thread_idO := leibnizO thread_id.
Instance thread_id_equiv : Equiv thread_id. apply thread_idO. Defined.
Global Instance thread_id_equiv : Equiv thread_id. apply thread_idO. Defined.
......@@ -29,7 +29,7 @@ Definition grants (perm: permission) (access: access_kind) : bool :=
Definition matched_grant (access: access_kind) (bor: tag) (it: item) :=
grants it.(perm) access it.(tg) = bor.
Instance matched_grant_dec (access: access_kind) (bor: tag) (it : item) :
Global Instance matched_grant_dec (access: access_kind) (bor: tag) (it : item) :
Decision (matched_grant access bor it) := _.
(** Difference from the paper/Miri in indexing of stacks: *)
......@@ -54,7 +54,7 @@ Definition is_active_protector cids (it: item) :=
| Some c => Is_true (is_active cids c) it.(perm) Disabled
| _ => False
end.
Instance is_active_protector_dec cids it : Decision (is_active_protector cids it).
Global Instance is_active_protector_dec cids it : Decision (is_active_protector cids it).
Proof. rewrite /is_active_protector. case_match; solve_decision. Qed.
(* Find the top active protector *)
......@@ -381,9 +381,9 @@ Definition tag_values_included (v: value) nxtp :=
l tg, ScPtr l tg v tg <t nxtp.
Infix "<<t" := tag_values_included (at level 60, no associativity).
Instance tag_included_dec tg nxtp : Decision (tag_included tg nxtp).
Global Instance tag_included_dec tg nxtp : Decision (tag_included tg nxtp).
Proof. destruct tg; cbn; apply _. Qed.
Instance tag_values_included_dec v nxtp : Decision (tag_values_included v nxtp).
Global Instance tag_values_included_dec v nxtp : Decision (tag_values_included v nxtp).
Proof.
rewrite /tag_values_included. induction v as [ | sc v IH].
- left; intros l tg Ha. exfalso. by eapply not_elem_of_nil.
......
......@@ -24,7 +24,7 @@ Definition stack_item_included (stk: stack) (nxtp: ptr_id) (nxtc: call_id) :=
Definition is_tagged (it: item) :=
match it.(tg) with Tagged _ => True | _ => False end.
Instance is_tagged_dec it: Decision (is_tagged it).
Global Instance is_tagged_dec it: Decision (is_tagged it).
Proof. intros. rewrite /is_tagged. case tg; solve_decision. Defined.
Definition stack_item_tagged_NoDup (stk : stack) :=
NoDup (fmap tg (filter is_tagged stk)).
......
......@@ -85,34 +85,34 @@ Proof.
Qed.
(** SqSubsetEq for option *)
Instance option_sqsubseteq `{SqSubsetEq A} : SqSubsetEq (option A) :=
Global Instance option_sqsubseteq `{SqSubsetEq A} : SqSubsetEq (option A) :=
λ o1 o2, if o1 is Some x1 return _ then
if o2 is Some x2 return _ then x1 x2 else False
else True.
Instance option_sqsubseteq_preorder `{SqSubsetEq A} `{!@PreOrder A ()} :
Global Instance option_sqsubseteq_preorder `{SqSubsetEq A} `{!@PreOrder A ()} :
@PreOrder (option A) ().
Proof.
split.
- move=>[x|] //. apply (@reflexivity A () _).
- move=>[x|] [y|] [z|] //. apply (@transitivity A () _).
Qed.
Instance option_sqsubseteq_antisymm `{SqSubsetEq A} `{!@AntiSymm A eq ()} :
Global Instance option_sqsubseteq_antisymm `{SqSubsetEq A} `{!@AntiSymm A eq ()} :
@AntiSymm (option A) eq ().
Proof.
intros [a|] [b|] Ha Hb; [|done|done|done]. f_equal. by apply : anti_symm.
Qed.
Instance option_sqsubseteq_po `{SqSubsetEq A} `{!@PartialOrder A ()} :
Global Instance option_sqsubseteq_po `{SqSubsetEq A} `{!@PartialOrder A ()} :
@PartialOrder (option A) ().
Proof. split; apply _. Qed.
Instance nat_sqsubseteq : SqSubsetEq nat := le.
Instance nat_sqsubseteq_po : @PartialOrder nat () := _.
Global Instance nat_sqsubseteq : SqSubsetEq nat := le.
Global Instance nat_sqsubseteq_po : @PartialOrder nat () := _.
Instance elem_of_list_suffix_proper {A : Type} (x:A) :
Global Instance elem_of_list_suffix_proper {A : Type} (x:A) :
Proper ((suffix) ==> impl) (x .).
Proof. intros l1 l2 [? ->] ?. rewrite elem_of_app. by right. Qed.
Instance elem_of_list_sublist_proper {A : Type} (x:A) :
Global Instance elem_of_list_sublist_proper {A : Type} (x:A) :
Proper ((sublist) ==> impl) (x .).
Proof.
intros l1 l2 SUB. induction SUB; [done|..].
......@@ -172,7 +172,7 @@ Proof.
- move => /NoDup_cons [NI /IH //].
Qed.
Instance NoDup_sublist_proper {A: Type} :
Global Instance NoDup_sublist_proper {A: Type} :
Proper (sublist ==> flip impl) (@NoDup A).
Proof. intros ????. by eapply NoDup_sublist. Qed.
......
......@@ -59,7 +59,7 @@ Lemma to_of_result v : to_result (of_result v) = Some v.
Proof. by destruct v as [[]|]. Qed.
Lemma of_to_result e v : to_result e = Some v of_result v = e.
Proof. destruct e=>//=; intros; by simplify_eq. Qed.
Instance of_result_inj : Inj (=) (=) of_result.
Global Instance of_result_inj : Inj (=) (=) of_result.
Proof. by intros ?? Hv; apply (inj Some); rewrite -2!to_of_result Hv /=. Qed.
Lemma is_closed_to_result X e v : to_result e = Some v is_closed X e.
Proof. intros <-%of_to_result. apply is_closed_of_result. Qed.
......@@ -77,9 +77,9 @@ Proof. induction vl as [|v vl IH]; [done|]. by rewrite 3!fmap_cons IH. Qed.
(** Equality and other typeclass stuff *)
Instance bin_op_eq_dec : EqDecision bin_op.
Global Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
Instance bin_op_countable : Countable bin_op.
Global Instance bin_op_countable : Countable bin_op.
Proof.
refine (inj_countable'
(λ o, match o with AddOp => 0 | SubOp => 1 | LeOp => 2 |
......@@ -88,9 +88,9 @@ Proof.
3 => LtOp | 4 => EqOp | _ => OffsetOp end) _); by intros [].
Qed.
Instance scalar_eq_dec : EqDecision scalar.
Global Instance scalar_eq_dec : EqDecision scalar.
Proof. solve_decision. Defined.
Instance scalar_countable : Countable scalar.
Global Instance scalar_countable : Countable scalar.
Proof.
refine (inj_countable
(λ v, match v with
......@@ -109,9 +109,9 @@ Proof.
end) _); by intros [].
Qed.
Instance retag_kind_eq_dec : EqDecision retag_kind.
Global Instance retag_kind_eq_dec : EqDecision retag_kind.
Proof. solve_decision. Defined.
Instance retag_kind_countable : Countable retag_kind.
Global Instance retag_kind_countable : Countable retag_kind.
Proof.
refine (inj_countable
(λ k, match k with
......@@ -186,11 +186,11 @@ Proof.
clear FIX. naive_solver.
Qed.
Instance expr_dec_eq : EqDecision expr.
Global Instance expr_dec_eq : EqDecision expr.
Proof.
refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
Defined.
Instance expr_countable : Countable expr.
Global Instance expr_countable : Countable expr.
Proof.
refine (inj_countable'
(fix go e := match e with
......@@ -263,11 +263,11 @@ Proof.
- fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
Qed.
Instance result_dec_eq : EqDecision result.
Global Instance result_dec_eq : EqDecision result.
Proof.
refine (λ v1 v2, cast_if (decide (of_result v1 = of_result v2))); abstract naive_solver.
Defined.
Instance result_countable : Countable result.
Global Instance result_countable : Countable result.
Proof.
refine (inj_countable
(λ v, match v with
......@@ -281,10 +281,10 @@ Proof.
by intros [].
Qed.
Instance scalar_inhabited : Inhabited scalar := populate ScPoison.
Instance expr_inhabited : Inhabited expr := populate (#[])%E.
Instance result_inhabited : Inhabited result := populate (ValR []%S).
Instance state_Inhabited : Inhabited state.
Global Instance scalar_inhabited : Inhabited scalar := populate ScPoison.
Global Instance expr_inhabited : Inhabited expr := populate (#[])%E.
Global Instance result_inhabited : Inhabited result := populate (ValR []%S).
Global Instance state_Inhabited : Inhabited state.
Proof. do 2!econstructor; exact: inhabitant. Qed.
Canonical Structure locO := leibnizO loc.
......@@ -296,7 +296,7 @@ Canonical Structure stateO := leibnizO state.
(** Basic properties about the language *)
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Global Instance fill_inj K : Inj (=) (=) (fill K).
Proof. induction K; intros ???; by simplify_eq/=. Qed.
......
......@@ -33,9 +33,9 @@ Inductive tag :=
| Tagged (t: ptr_id)
| Untagged.
Instance tag_eq_dec : EqDecision tag.
Global Instance tag_eq_dec : EqDecision tag.
Proof. solve_decision. Defined.
Instance tag_countable : Countable tag.
Global Instance tag_countable : Countable tag.
Proof.
refine (inj_countable
(λ tg, match tg with
......@@ -49,9 +49,9 @@ Proof.
Qed.
Inductive permission := Unique | SharedReadWrite | SharedReadOnly | Disabled.
Instance permission_eq_dec : EqDecision permission.
Global Instance permission_eq_dec : EqDecision permission.
Proof. solve_decision. Defined.
Instance permission_countable : Countable permission.
Global Instance permission_countable : Countable permission.
Proof.
refine (inj_countable
(λ p,
......@@ -71,7 +71,7 @@ Record item := mkItem {
tg : tag;
protector : option call_id;
}.
Instance item_eq_dec : EqDecision item.
Global Instance item_eq_dec : EqDecision item.
Proof. solve_decision. Defined.
Definition stack := list item.
......@@ -208,9 +208,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
#[global]
Hint Mode Closed + + : typeclass_instances.
Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Global Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
Global Instance closed_decision env e : Decision (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
(** Irreducible (language values) *)
......
......@@ -22,7 +22,7 @@ Proof. solve_decision. Qed.
Global Instance loc_inhabited : Inhabited loc := populate (1%positive, 0).
Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' (λ l, l) (λ '(i, j), (i, j))); intros []. Qed.
Program Instance loc_infinite : Infinite loc :=
Global Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ '(i, j), (i, j)) (λ l, Some l) _.
Next Obligation. intros []. done. Qed.
......@@ -42,7 +42,7 @@ Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
Lemma shift_loc_0_nat l : l + 0%nat = l.
Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
Lemma shift_loc_block l n : (l + n).1 = l.1.
......
......@@ -11,7 +11,7 @@ Definition tagged_sublist (stk1 stk2: stack) :=
it1, it1 stk1 it2,
it2 stk2 it1.(tg) = it2.(tg) it1.(protector) = it2.(protector)
(it1.(perm) Disabled it2.(perm) = it1.(perm)).
Instance tagged_sublist_preorder : PreOrder tagged_sublist.
Global Instance tagged_sublist_preorder : PreOrder tagged_sublist.
Proof.
constructor.
- intros ??. naive_solver.
......@@ -20,7 +20,7 @@ Proof.
intros ND3. specialize (ND ND3). rewrite ND2 // ND //.
Qed.
Instance tagged_sublist_proper stk : Proper (() ==> impl) (tagged_sublist stk).
Global Instance tagged_sublist_proper stk : Proper (() ==> impl) (tagged_sublist stk).
Proof. move => ?? SUB H1 ? /H1 [? [/SUB ? ?]]. naive_solver. Qed.
Lemma tagged_sublist_app l1 l2 k1 k2 :
......@@ -176,7 +176,7 @@ Lemma stack_item_tagged_NoDup_app stk1 stk2 :
stack_item_tagged_NoDup stk1 stack_item_tagged_NoDup stk2.
Proof. rewrite /stack_item_tagged_NoDup filter_app fmap_app NoDup_app. naive_solver. Qed.
Instance stack_item_tagged_NoDup_proper :
Global Instance stack_item_tagged_NoDup_proper :
Proper (Permutation ==> iff) stack_item_tagged_NoDup.
Proof. intros stk1 stk2 PERM. by rewrite /stack_item_tagged_NoDup PERM. Qed.
......
......@@ -12,7 +12,7 @@ Definition tag_on_top (stks: stacks) l t pm : Prop :=
Definition active_preserving (cids: call_id_set) (stk stk': stack) :=
pm t c, c cids mkItem pm t (Some c) stk mkItem pm t (Some c) stk'.
Instance active_preserving_preorder cids : PreOrder (active_preserving cids).
Global Instance active_preserving_preorder cids : PreOrder (active_preserving cids).
Proof.
constructor.
- intros ??. done.
......
......@@ -174,20 +174,20 @@ End type_general_ind.
(** Decidability *)
Instance type_inhabited : Inhabited type := populate (FixedSize 0).
Global Instance type_inhabited : Inhabited type := populate (FixedSize 0).
Instance mutability_eq_dec : EqDecision mutability.
Global Instance mutability_eq_dec : EqDecision mutability.
Proof. solve_decision. Defined.
Instance mutability_countable : Countable mutability.
Global Instance mutability_countable : Countable mutability.
Proof.
refine (inj_countable'
(λ m, match m with Mutable => 0 | Immutable => 1 end)
(λ x, match x with 0 => Mutable | _ => Immutable end) _); by intros [].
Qed.
Instance pointer_kind_eq_dec : EqDecision pointer_kind.
Global Instance pointer_kind_eq_dec : EqDecision pointer_kind.
Proof. solve_decision. Defined.
Instance pointer_kind_countable : Countable pointer_kind.
Global Instance pointer_kind_countable : Countable pointer_kind.
Proof.
refine (inj_countable
(λ k, match k with
......@@ -239,11 +239,11 @@ Proof.
specialize (FIX Ts1h). naive_solver. }
clear FIX. naive_solver.
Qed.
Instance type_eq_dec : EqDecision type.
Global Instance type_eq_dec : EqDecision type.
Proof.
refine (λ T1 T2, cast_if (decide (type_beq T1 T2))); by rewrite -type_beq_correct.
Defined.
Instance type_countable : Countable type.
Global Instance type_countable : Countable type.
Proof.
refine (inj_countable'
(fix go T := match T with
......
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