Iris:ea64fd148b56e1c38c08c2954e76bfa2e75b4db9 commitshttps://gitlab.mpi-sws.org/iris/iris/-/commits/ea64fd148b56e1c38c08c2954e76bfa2e75b4db92017-02-13T19:24:19+01:00https://gitlab.mpi-sws.org/iris/iris/-/commit/ea64fd148b56e1c38c08c2954e76bfa2e75b4db9Let iAssumption succeed when there is H : False.2017-02-13T19:24:19+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/a16d59ea75be4ffe0a2f8da5f8f4c59f877e26ceWhen using [iAssert ... with ">[]"], we should not use...2017-02-13T18:54:58+01:00Jacques-Henri Jourdanjjourdan@mpi-sws.orgWhen using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead.
This patch is still not ideal, because some modalities (e.g., later) preserve persistence.
https://gitlab.mpi-sws.org/iris/iris/-/commit/f1b30a2eb12d38bffd8a0aa541c90e3675af2a29Make iSpecialize work with coercions.2017-02-12T13:24:44+01:00Robbert Krebbersmail@robbertkrebbers.nl
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.https://gitlab.mpi-sws.org/iris/iris/-/commit/da56bbb0f26f4f77fe28efea60f81f06d8a2ac59Unused premises go to the last premise of iApply (instead of the first).2017-01-23T17:16:24+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/84481877eeb2fccdcb783b67459720c971c3fb43Add [] spec patterns for missing premises of iApply.2017-01-22T10:27:29+01:00Robbert Krebbersmail@robbertkrebbers.nl
This fixes issue #51.https://gitlab.mpi-sws.org/iris/iris/-/commit/60d82286172f9b82c9b8b8cecc267da91fac6ab1more restrictive Proof Using hints in heap_lang, proofmode, tests2017-01-05T19:26:39+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/commit/71abda4d8480fc6528a1617aedbadde59705747bmake "make quick" quick by adding hints about the used section variables2017-01-03T17:50:02+01:00Ralf Jungjung@mpi-sws.org
This patch was created using
find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '
and some minor manual editinghttps://gitlab.mpi-sws.org/iris/iris/-/commit/8c844e32f0424d1b5080dd6bcafe7b4231d80f6fFix issue #56.2016-12-28T10:10:03+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/6b8069fa5af75e7e6faa4a0a516fd01e88a0309fmove everything to subfolder theories/2016-12-09T23:27:29+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/commit/142065532fb0016d3826cf22ada2af7c78926ea0Curry everything in heap_lang/lib and tests.2016-12-09T16:04:22+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/243fdd139ccdf1370e5b186650e4323d5e73e54b Validity coercion from iProp to Prop. Magic wand that works at the Prop l...2016-11-24T10:29:33+01:00Jacques-Henri Jourdanjacques-henri.jourdan@normalesup.org
The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.https://gitlab.mpi-sws.org/iris/iris/-/commit/274209c206c8010b63444bb53ad62570a05f71d6Make nclose an explicit coercion.2016-11-22T18:59:16+01:00Robbert Krebbersmail@robbertkrebbers.nl
We do this by introducing a type class UpClose with notation ↑.
The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.https://gitlab.mpi-sws.org/iris/iris/-/commit/99cbb5250cc0c46ad455e74ac4b046c93d45d1a2new notation for pure assertions2016-11-22T18:31:58+01:00Ralf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/commit/cc31476d577161848c1647cfa7e5cdc1026309afUse symbol ∗ for separating conjunction.2016-11-03T10:46:49+01:00Robbert Krebbersmail@robbertkrebbers.nl
The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk *
was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was
a random choice from a unicode chart.
The new symbol ∗ (as proposed by David Swasey) corresponds better to
conventional practise and matches the symbol we use on paper.https://gitlab.mpi-sws.org/iris/iris/-/commit/b9413b6f490c98f56807b9734e2ef3891042b9e1Move program_logic stuff that does not depend on the language to base_logic/lib.2016-10-28T11:07:09+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/3f9b134d154b6ca9b5a3008bbd7e3904c8b0939fRemove dependency of fancy updates on the program language.2016-10-28T10:48:38+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/e224e89101211478d7063a1eaf8ab90c26bf7ad5Rename uPred_eq into uPred_internal_eq.2016-10-25T15:43:07+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/fc30ca08400579489e1852ce39f7ae39a57b08c2Generalize update tactics into iMod and iModIntro for modalities.2016-10-25T11:33:45+02:00Robbert Krebbersmail@robbertkrebbers.nl
There are now two proof mode tactics for dealing with modalities:
- `iModIntro` : introduction of a modality
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality
The behavior of these tactics can be controlled by instances of the `IntroModal`
and `ElimModal` type class. We have declared instances for later, except 0,
basic updates and fancy updates. The tactic `iMod` is flexible enough that it
can also eliminate an updates around a weakest pre, and so forth.
The corresponding introduction patterns of these tactics are `!>` and `>`.
These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`.
Source of backwards incompatability: the introduction pattern `!>` is used for
introduction of arbitrary modalities. It used to introduce laters by stripping
of a later of each hypotheses.https://gitlab.mpi-sws.org/iris/iris/-/commit/afae72fd182e61506387a7d86b8b5aa6f59c146cNo longer put proof mode class instances in their own file.2016-10-05T22:47:20+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/75ad3b2e22a3836b5596430dffdd932629d10000Support for framing pure hypotheses.2016-09-19T21:12:38+02:00Robbert Krebbersmail@robbertkrebbers.nl
This closes issue 32.https://gitlab.mpi-sws.org/iris/iris/-/commit/090aaea3a4162d6ce5608b4040a097f321928bc9Support for specialization of P₁ -★ .. -★ Pₙ -★ Q where Q is persistent.2016-09-09T16:06:46+02:00Robbert Krebbersmail@robbertkrebbers.nl
Before this commit, given "HP" : P and "H" : P -★ Q with Q persistent, one
could write:
iSpecialize ("H" with "#HP")
to eliminate the wand in "H" while keeping the resource "HP". The lemma:
own_valid : own γ x ⊢ ✓ x
was the prototypical example where this pattern (using the #) was used.
However, the pattern was too limited. For example, given "H" : P₁ -★ P₂ -★ Q",
one could not write iSpecialize ("H" with "#HP₁") because P₂ -★ Q is not
persistent, even when Q is.
So, instead, this commit introduces the following tactic:
iSpecialize pm_trm as #
which allows one to eliminate implications and wands while being able to use
all hypotheses to prove the premises, as well as being able to use all
hypotheses to prove the resulting goal.
In the case of iDestruct, we now check whether all branches of the introduction
pattern start with an `#` (moving the hypothesis to the persistent context) or
`%` (moving the hypothesis to the pure Coq context). If this is the case, we
allow one to use all hypotheses for proving the premises, as well as for proving
the resulting goal.https://gitlab.mpi-sws.org/iris/iris/-/commit/1c0a0e047c0e75ca59a80e24ddbb70be69553e69Enable proof mode to destruct non-separating conjunctions in spatial context.2016-08-24T10:42:00+02:00Robbert Krebbersmail@robbertkrebbers.nl
This is allowed as long as one of the conjuncts is thrown away (i.e. is a
wildcard _ in the introduction pattern). It corresponds to the principle of
"external choice" in linear logic.https://gitlab.mpi-sws.org/iris/iris/-/commit/4d8c4ac832f7a393853fbdda861a61ae0a0e5a39More introduction patterns.2016-08-05T02:13:53+02:00Robbert Krebbersmail@robbertkrebbers.nl
Also make those for introduction and elimination more symmetric:
!% pure introduction % pure elimination
!# always introduction # always elimination
!> later introduction > pat timeless later elimination
!==> view shift introduction ==> pat view shift eliminationhttps://gitlab.mpi-sws.org/iris/iris/-/commit/1f5898582d842fe69e14acabe034fa933e979253Iris 3.0: invariants and weakest preconditions encoded in the logic.2016-08-05T02:13:08+02:00Robbert Krebbersmail@robbertkrebbers.nl
This commit features:
- A simpler model. The recursive domain equation no longer involves a triple
containing invariants, physical state and ghost state, but just ghost state.
Invariants and physical state are encoded using (higher-order) ghost state.
- (Primitive) view shifts are formalized in the logic and all properties about
it are proven in the logic instead of the model. Instead, the core logic
features only a notion of raw view shifts which internalizing performing frame
preserving updates.
- A better behaved notion of mask changing view shifts. In particular, we no
longer have side-conditions on transitivity of view shifts, and we have a
rule for introduction of mask changing view shifts |={E1,E2}=> P with
E2 ⊆ E1 which allows to postpone performing a view shift.
- The weakest precondition connective is formalized in the logic using Banach's
fixpoint. All properties about the connective are proven in the logic instead
of directly in the model.
- Adequacy is proven in the logic and uses a primitive form of adequacy for
uPred that only involves raw views shifts and laters.
Some remarks:
- I have removed binary view shifts. I did not see a way to describe all rules
of the new mask changing view shifts using those.
- There is no longer the need for the notion of "frame shifting assertions" and
these are thus removed. The rules for Hoare triples are thus also stated in
terms of primitive view shifts.
TODO:
- Maybe rename primitive view shift into something more sensible
- Figure out a way to deal with closed proofs (see the commented out stuff in
tests/heap_lang and tests/barrier_client).https://gitlab.mpi-sws.org/iris/iris/-/commit/261d7c644ea5dfecd66f72c257c22bc8507c0c0eRevert "Hack to delay type class inference in iPoseProof."2016-07-27T11:13:44+02:00Robbert Krebbersmail@robbertkrebbers.nl
This reverts commit <a href="/iris/iris/-/commit/c43eb936568049de062feb16bbf03915a4733e94" data-original="c43eb936568049de062feb16bbf03915a4733e94" data-link="false" data-link-reference="false" data-project="118" data-commit="c43eb936568049de062feb16bbf03915a4733e94" data-reference-type="commit" data-container="body" data-placement="top" title="Hack to delay type class inference in iPoseProof." class="gfm gfm-commit has-tooltip">c43eb936</a>.
The hack using class_apply has some strange behaviors, see:
<a href="https://sympa.inria.fr/sympa/arc/coq-club/2016-07/msg00094.html" rel="nofollow noreferrer noopener" target="_blank">https://sympa.inria.fr/sympa/arc/coq-club/2016-07/msg00094.html</a>https://gitlab.mpi-sws.org/iris/iris/-/commit/c43eb936568049de062feb16bbf03915a4733e94Hack to delay type class inference in iPoseProof.2016-07-27T00:48:25+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/086cc92c8e5ea852d131db2ed2c2f86198748874Use round braces instead of curly braces in proof mode tactics.2016-07-13T13:45:04+02:00Robbert Krebbersmail@robbertkrebbers.nl
The intropattern {H} also meant clear (both in ssreflect, and the logic
part of the introduction pattern).https://gitlab.mpi-sws.org/iris/iris/-/commit/a9f8d0f0ba5937059bf0c02e5a9f9969f3638b67Enable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing.2016-06-30T14:37:05+02:00Robbert Krebbersmail@robbertkrebbers.nl
For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.https://gitlab.mpi-sws.org/iris/iris/-/commit/238d31bf8ca873184a8c70a033a5b012198acb6aFix order of imports.2016-06-30T12:57:31+02:00Robbert Krebbersmail@robbertkrebbers.nl
This fixes a bug in <a href="/iris/iris/-/commit/916ff44acdcdcef0bc7cbbb790a4338c8f0e9b69" data-original="916ff44a" data-link="false" data-link-reference="false" data-project="118" data-commit="916ff44acdcdcef0bc7cbbb790a4338c8f0e9b69" data-reference-type="commit" data-container="body" data-placement="top" title="Move some proof mode classes to their own file." class="gfm gfm-commit has-tooltip">916ff44a</a> causing proof mode notations not being
pretty printed.https://gitlab.mpi-sws.org/iris/iris/-/commit/caf69e069b0f7327fffd7cc246d332b7d8b8ed38Split IsPure into IntoPure and FromPure.2016-06-30T12:36:47+02:00Robbert Krebbersmail@robbertkrebbers.nl
This tweak allows us to declare pvs as an instance of FromPure (it is not
an instance of IntoPure), making some tactics (like iPureIntro and done)
work with pvs too.https://gitlab.mpi-sws.org/iris/iris/-/commit/0502f30bfaff2cd06b3efcd1522dbcadc9a11eecRemove lviewshifts.v and turn them into notations.2016-06-18T00:17:16+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/695c9baa2d398299eaf1bbdd2a73ebeed32e1a56Use |==> syntax for 'preserve pvs' specialization pattern.2016-06-01T16:12:12+02:00Robbert Krebbersmail@robbertkrebbers.nl
We used => before, which is strange, because it has another meaning
in ssreflect.https://gitlab.mpi-sws.org/iris/iris/-/commit/61adc9686aadd52809be31ca567d3a5db24c595cChange the precedence of ⊢ to be the same as →, and the precedence of ⊣⊢ to2016-05-31T21:39:22+02:00Robbert Krebbersmail@robbertkrebbers.nlbe the same as <gl-emoji title="left right arrow" data-name="left_right_arrow" data-unicode-version="1.1">↔</gl-emoji>.
This is a fairly intrusive change, but at least makes notations more
consistent, and often shorter because fewer parentheses are needed. Note
that viewshifts already had the same precedence as →.https://gitlab.mpi-sws.org/iris/iris/-/commit/2863ad3aceaef576d7b816190cc52e665071fc20Change notation of viewshifts in Coq scope.2016-05-31T15:25:19+02:00Robbert Krebbersmail@robbertkrebbers.nl
It used to be: (P ={E}=> Q) := (True ⊢ (P → |={E}=> Q))
Now it is: (P ={E}=> Q) := (P ⊢ |={E}=> Q)https://gitlab.mpi-sws.org/iris/iris/-/commit/5eb59e133fde1a3e42b7c03c134d738b390df894Hint Resolve uPred.eq_refl'.2016-05-30T13:25:12+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/69d67c60ffd5c084348e9d0e4a15bb8f63525092Introduce a canonical structure for CMRAs with a unit element.2016-05-27T14:51:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/e965b669432646c5cde0b0df3b2f80af5eecf0c0Merge iAssert and iPvsAssert.2016-05-24T14:13:08+02:00Robbert Krebbersmail@robbertkrebbers.nl
To do so, we have introduced the specialization patterns:
=>[H1 .. Hn] and =>[-H1 .. Hn]
That generate a goal in which the view shift is preserved. These specialization
patterns can also be used for e.g. iApply.
Note that this machinery is not tied to primitive view shifts, and works for
various kinds of goal (as captured by the ToAssert type class, which describes
how to transform the asserted goal based on the main goal).
TODO: change the name of these specialization patterns to reflect this
generality.https://gitlab.mpi-sws.org/iris/iris/-/commit/eacb1c46a7d4dcc871472c1a14c578a9f682a0afFlip order of arguments of iAssert/iPvsAssert.2016-05-24T13:48:45+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/iris/-/commit/65bfa071cfb0526b1bada6a3833df993a4c1b696Make specialization patterns for persistent premises more uniform.2016-05-24T13:41:43+02:00Robbert Krebbersmail@robbertkrebbers.nl
Changes:
- We no longer have a different syntax for specializing a term H : P -★ Q whose
range P or domain Q is persistent. There is just one syntax, and the system
automatically determines whether either P or Q is persistent.
- While specializing a term, always modalities are automatically stripped. This
gets rid of the specialization pattern !.
- Make the syntax of specialization patterns more consistent. The syntax for
generating a goal is [goal_spec] where goal_spec is one of the following:
H1 .. Hn : generate a goal using hypotheses H1 .. Hn
-H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn
# : generate a goal for the premise in which all hypotheses can be
used. This is only allowed when specializing H : P -★ Q where
either P or Q is persistent.
% : generate a goal for a pure premise.https://gitlab.mpi-sws.org/iris/iris/-/commit/b91a628094ba03128b37e1e3a7b4bc6bdfaffad1proofmode: add test for mask-changing view shift2016-05-21T12:31:11+02:00Ralf Jungjung@mpi-sws.org