GitLab

This is to avoid confusion when Coq loads the module.

It now produces a lambda that when evaluated with a value runs the underlying
lambda that value after acquiring the lock. As before, the lock is released
afterwards.

It now returns the value of the expression evaluated.

We used to have:

(λ x, b) a ->β b[a/x]

But now we have:

(λ f x, b) a ->β b[a/x, (λ f x, b)/f]

There is one admit that needs to be taken care of. The admitted case is validity
of a monoid element of iprod. At the moment iris doesn't seem to have necessary
lemmas to prove this easily.

With this change, recursive types don't use the context for type variables.
This allows us to assume that all types in typing context are universally
quantified, i.e., they are all polymorphic types.

We divide the binary fundamental lemma for Fμ,ref,par into several lemmas.
This also generalizes the lemmas. We used to show

Δ ∥ Γ ⊩ e ≤log≤ e ∷ τ

in the fundamental lemma. But now in smaller lemmas in each case we show

Δ ∥ Γ ⊩ e ≤log≤ e' ∷ τ

Given some hypotheses of course.

We still need to prove the many admitted lemmas in rules_binary module.

The way the binary relation is defined, the binary fundamental lemma simply
doesn't hold. I overlooked the fact that we need to enable CAS only for types
where equality is checkable.

These will be put in a separate file.

The parts of Fμ,ref,par that we have are now compatible with the latest
version of iris.