This fixes the problem in iris/iris!275 (comment 42062)

Dan Frumin authored 5 years ago and Robbert Krebbers committed 5 years ago

A more general implication from `head_reducible` to `reducible`.

Marianna Rapoport authored 6 years ago and Ralf Jung committed 6 years ago

- Removing head of list of observations after each reduction step in definition of wp
- Adding support for observations to state_interp and world
- Applying Ralf's suggestions to previous commit (e.g. replacing /\ and -> with unicode characters)

It can be infered now.

This reverts commit 913059d2.

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

I saw no need for `stuckness_flip`: strong atomicity always works,
while weak atomicity works only for expressions that are not stuck.
Since this seemed unclear, I split lemma `wp_atomic'` up into
`wp_strong_atomic` (parametric in the WP's `s`) and `wp_weak_atomic`
(not). The proof mode instance is stated in terms of the derived rule
`wp_atomic` (parametric in `s`).

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