GitLab

move test suite out of theories/ so it does not get installed; also check output of test suite so that we can test printing

This reverts commit 913059d2.

This reverts commit 849abb8d, reversing changes
made to 8de0b894.  The merge was done
accidentally, before review happened.

This problem has been reported by Léon Gondelman.

Before, when using, for example wp_alloc, in an expression like:

  ref (ref v)

It would apply `tac_wp_alloc` to the outermost ref, after which it
fails to establish that the argument `ref v` is a value. In this
commit, other evaluation positions will be tried whenever it turn
out that the argument of the construct is not a value. The same
applies to store/cas/...

I have implemented this by making use of the new `IntoVal` class.

Instead of writing a separate tactic lemma for each pure reduction,
there is a single tactic lemma for performing all of them.

The instances of PureExec can be shared between WP tactics and, e.g.
symbolic execution in the ghost  threadpool

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 editing

The WP construction now takes an invariant on states as a parameter
(part of the irisG class) and no longer builds in the authoritative
ownership of the entire state. When instantiating WP with a concrete
language on can choose its state invariant. For example, for heap_lang
we directly use `auth (gmap loc (frac * dec_agree val))`, and avoid
the indirection through invariants entirely.

As a result, we no longer have to carry `heap_ctx` around.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

Robbert Krebbers authored Nov 18, 2016 and Ralf Jung committed Nov 22, 2016

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.

Now we try to avoid adding them unnecessarily, so we don't have to remove them automatically any more.

And also rename the corresponding proof mode tactics.

rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.

As proposed by JH Jourdan in issue 34.

This is more consistent with CAS, which also can be used on any value.
Note that being able to (atomically) test for equality of any value and
being able to CAS on any value is not realistic. See the discussion at
https://gitlab.mpi-sws.org/FP/iris-coq/issues/26, and in particular JH
Jourdan's observation:

  I think indeed for heap_lang this is just too complicated.

  Anyway, the role of heap_lang is not to model any actual
  programming language, but rather to show that we can do proofs
  about certain programs. The fact that you can write unrealistic
  programs is not a problem, IMHO. The only thing which is important
  is that the program that we write are realistic (i.e., faithfully
  represents the algorithm we want to p

This commit is based on a commit by Zhen Zhang who generalized equality
to work on any literal (and not just integers).

This generalization is surprisingly easy in Iris 3.0, so I could not
resist not doing it :).

This makes stuff more uniform and also removes the need for the [inGFs]
type class. Instead, there is now a type class [subG Σ1 Σ2] which expresses
that a list of functors [Σ1] is contained in [Σ2].