Commit d6b49ab2 authored by Ralf Jung's avatar Ralf Jung

more restrictive Proof Using hints in base_logic, algebra

parent 60d82286
Pipeline #3607 passed with stage
in 10 minutes and 28 seconds
......@@ -208,7 +208,7 @@ Section list_theory.
Lemma list_agrees_fmap `{Equivalence _ R'} al :
list_agrees R al list_agrees R' (f <$> al).
Proof using All.
Proof using Type*.
move=> /list_agrees_alt Hl. apply (list_agrees_alt R') => a' b'.
intros (a & -> & Ha)%elem_of_list_fmap (b & -> & Hb)%elem_of_list_fmap.
apply Hf. exact: Hl.
......
From iris.algebra Require Export excl local_updates.
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import classes.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
Add Printing Constructor auth.
......
From mathcomp Require Export ssreflect.
From iris.prelude Require Export prelude.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
From iris.algebra Require Export ofe.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Class PCore (A : Type) := pcore : A option A.
Instance: Params (@pcore) 2.
......@@ -428,6 +428,7 @@ Qed.
(** ** Total core *)
Section total_core.
Set Default Proof Using "Type*".
Context `{CMRATotal A}.
Lemma cmra_core_l x : core x x x.
......
From iris.algebra Require Export cmra list.
From iris.prelude Require Import functions gmap gmultiset.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** The operator [ [⋅] Ps ] folds [⋅] over the list [Ps]. This operator is not a
quantifier, so it binds strongly.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import cmra_big_op.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections coPset.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
......
......@@ -205,7 +205,7 @@ Instance fold_ne : Proper (dist n ==> dist n) fold.
Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F.
Proof using All.
Proof using Type*.
apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
- move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import local_updates.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
......
From iris.algebra Require Import ofe cmra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(* Old notation for backwards compatibility. *)
......
From iris.algebra Require Export cmra updates.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
(* setoids *)
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Notation frac := Qp (only parsing).
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
From iris.prelude Require Export gmap.
From iris.algebra Require Import updates local_updates.
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Section cofe.
Context `{Countable K} {A : ofeT}.
......@@ -334,6 +334,7 @@ Proof.
Qed.
Section freshness.
Set Default Proof Using "Type*".
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma alloc_updateP_strong (Q : gmap K A Prop) (I : gset K) m x :
x ( i, m !! i = None i I Q (<[i:=x]>m)) m ~~>: Q.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.prelude Require Export collections gmap mapset.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(* The union CMRA *)
Section gset.
......@@ -155,6 +155,7 @@ Section gset_disj.
Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
Section fresh_updates.
Set Default Proof Using "Type*".
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma gset_disj_alloc_updateP (Q : gset_disj K Prop) X :
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
From iris.prelude Require Import finite.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** * Indexed product *)
(** Need to put this in a definition to make canonical structures to work. *)
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
From iris.prelude Require Export list.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Section cofe.
Context {A : ofeT}.
......
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** * Local updates *)
Definition local_update {A : cmraT} (x y : A * A) := n mz,
......
From iris.algebra Require Export base.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** This files defines (a shallow embedding of) the category of OFEs:
Complete ordered families of equivalences. This is a cartesian closed
......@@ -159,6 +159,7 @@ Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.
Section contractive.
Set Default Proof Using "Type*".
Context {A B : ofeT} (f : A B) `{!Contractive f}.
Implicit Types x y : A.
......
From iris.prelude Require Export set.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
......
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** * Frame preserving updates *)
(* This quantifies over [option A] for the frame. That is necessary to
......@@ -86,6 +86,7 @@ Qed.
(** ** Frame preserving updates for total CMRAs *)
Section total_updates.
Set Default Proof Using "Type*".
Context `{CMRATotal A}.
Lemma cmra_total_updateP x (P : A Prop) :
......
From iris.prelude Require Export vector.
From iris.algebra Require Export ofe.
From iris.algebra Require Import list.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Section ofe.
Context {A : ofeT}.
......
From iris.base_logic Require Export derived.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Module Import uPred.
Export upred.uPred.
......
From iris.algebra Require Export list cmra_big_op.
From iris.base_logic Require Export base_logic.
From iris.prelude Require Import gmap fin_collections gmultiset functions.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
......
From iris.base_logic Require Import primitive.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
Notation "■ φ" := (uPred_pure φ%C%type)
......
From iris.base_logic Require Export primitive.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import upred.uPred primitive.uPred.
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P Q) (Q P))%I.
......
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(* In this file we show that the bupd can be thought of a kind of
step-indexed double-negation when our meta-logic is classical *)
......@@ -274,7 +274,7 @@ Qed.
Section classical.
Context (not_all_not_ex: (P : M Prop), ¬ ( n : M, ¬ P n) n : M, P n).
Lemma nnupd_bupd P: (|=n=> P) (|==> P).
Proof.
Proof using Type*.
rewrite /uPred_nnupd.
split. uPred.unseal; red; rewrite //=.
intros n x ? Hforall k yf Hle ?.
......
From iris.prelude Require Export hlist.
From iris.base_logic Require Export base_logic.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Fixpoint uPred_hexist {M As} : himpl As (uPred M) uPred M :=
......
......@@ -3,7 +3,7 @@ From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(* The CMRA we need. *)
......@@ -117,7 +117,7 @@ Section auth.
auth_inv γ f φ auth_own γ a ={E}= t,
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={E}= auth_inv γ f φ auth_own γ b.
Proof.
Proof using Type*.
iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
iModIntro. iExists t.
......@@ -133,7 +133,7 @@ Section auth.
auth_ctx γ N f φ auth_own γ a ={E,E∖↑N}= t,
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={E∖↑N,E}= auth_own γ b.
Proof.
Proof using Type*.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
[auth_acc] and [inv_open] -- but since we don't have any good support
......
......@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import auth gmap agree.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** The CMRAs we need. *)
......
From iris.base_logic.lib Require Export invariants fractional.
From iris.algebra Require Export frac.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Class cinvG Σ := cinv_inG :> inG Σ fracR.
......
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** The "core" of an assertion is its maximal persistent part.
......
From iris.base_logic Require Import base_logic soundness.
From iris.proofmode Require Import tactics.
Set Default Proof Using "All".
Set Default Proof Using "Type*".
(** This proves that we need the ▷ in a "Saved Proposition" construction with
name-dependent allocation. *)
......@@ -39,7 +39,7 @@ Module savedprop. Section savedprop.
Qed.
Lemma contradiction : False.
Proof.
Proof using All.
apply (@soundness M False 1); simpl.
iIntros "". iMod A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
......@@ -186,7 +186,7 @@ Module inv. Section inv.
Qed.
Lemma contradiction : False.
Proof.
Proof using All.
apply consistency. iIntros "".
iMod A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
......
......@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Export invG.
Import uPred.
......
......@@ -2,7 +2,7 @@ From iris.prelude Require Import gmap gmultiset.
From iris.base_logic Require Export derived.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import classes class_instances.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Class Fractional {M} (Φ : Qp uPred M) :=
fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p Φ q.
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import fractional.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
......
......@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates namespaces.
From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** Derived forms and lemmas about them. *)
......
From iris.base_logic Require Export base_logic.
From iris.algebra Require Import iprod gmap.
From iris.algebra Require cofe_solver.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** In this file we construct the type [iProp] of propositions of the Iris
logic. This is done by solving the following recursive domain equation:
......
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Export gmap gset coPset.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(* Non-atomic ("thread-local") invariants. *)
......
From iris.prelude Require Export countable coPset.
From iris.algebra Require Export base.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Definition namespace := list positive.
Instance namespace_eq_dec : EqDecision namespace := _.
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Import iprod gmap.
From iris.base_logic Require Import big_op.
From iris.base_logic Require Export iprop.
From iris.proofmode Require Import classes.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
......
From iris.base_logic Require Export own.
From iris.algebra Require Import agree.
From iris.prelude Require Import gmap.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
......
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Export sts.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** The CMRA we need. *)
......
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
( (P - |={E1,E2}=> Q))%I.
......
......@@ -3,7 +3,7 @@ From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Module invG.
Class invG (Σ : gFunctors) : Set := WsatG {
......
From iris.base_logic Require Export upred.
From iris.algebra Require Export updates.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Local Hint Extern 1 (_ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ _) => etrans; [|eassumption].
Local Hint Extern 10 (_ _) => omega.
......
From iris.base_logic Require Export base_logic.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Section adequacy.
......
From iris.prelude Require Import gmap.
From iris.base_logic Require Export base_logic big_op.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Module uPred_reflection. Section uPred_reflection.
......
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** The basic definition of the uPred type, its metric and functor laws.
You probably do not want to import this file. Instead, import
......
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