 12 Feb, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 11 Feb, 2016 5 commits


Robbert Krebbers authored

Robbert Krebbers authored
Also do some minor clean up.

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

 10 Feb, 2016 3 commits


Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored
Now notations are pretty printed in the same way as they are parsed. Before "let x := e1 in e2" was notation for "(fun x => e2) e1", resulting in overlapping notations for the same thing.

 09 Feb, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
We can use a named representation because we only substitute closed values. This idea is borrowed from Pierce's Software Foundations. The named representation has the following advantages: * Programs are much better readable than those using De Bruijn indexes. * Substitutions on closed terms (where all variables are explicit strings) can be performed by a mere simpl instead of Autosubst's asimpl. The performance of simpl seems better than asimpl. * Syntactic sugar refolds better.

Ralf Jung authored
add basic notions of literals, unary operators and binary operators, and use them to define +, , <=, ...

 08 Feb, 2016 1 commit


Ralf Jung authored
Actual proofs will end up using own and inv, and none of the notions defined in ownership.v

 04 Feb, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 03 Feb, 2016 5 commits


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

 02 Feb, 2016 11 commits


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored
Remarks: * eauto needs more fuel to automatically solve the sideconditions. * ssreflect rewrite works if we do a set (φ ..) first. No idea why.

Ralf Jung authored
...unfortunately, that proof actually got longer because some automation no longer works

Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored
Notable changes: * I am now using the same names for the fields of the language record and the instances in heap_lang. In order to deal with shadowing, I have put all definitions in heap_lang.v in a module. * Instead of defining evaluation contexts recursively, these are now defined using lists. This way we can easily reuse operations on lists. For example, composition of evaluation contexts is just appending lists. Also, it allowed me to simplify the rather complicated proof of step_by_val as induction on the shape of contexts no longer results in a blowup of the number of cases. * Use better automation to prove all lemmas of heap_lang. * I have introduced tactics to invert steps and to do steps. These tactics greatly helped simplifying boring parts of lifting lemmas.

 01 Feb, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This way we can more easily state lemmas for concrete languages for arbitrary global functors.

Robbert Krebbers authored
This enables us to remove a whole bunch of type annotations.

 30 Jan, 2016 3 commits