 22 Jul, 2016 40 commits


Robbert Krebbers authored
There was not really a need for the lattice type classes, so I removed these.

Robbert Krebbers authored
Similar files (gmap, listset, ...) were already in singular form and matched the name of the set/map data type.

 25 May, 2016 40 commits


Robbert Krebbers authored
 Make the carrier argument of the constructors for the canonical structures cofeT and cmraT explicit. This way we make sure the carrier is properly exposed, instead of some alias of the carrier.  Make derived constructions (such as discreteC and discreteR) notations instead of definitions. This is yet again to make sure that the carrier is properly exposed.  Turn DRA into a canonical structure (it used to be a type class). This fixes some issues, notably it fixes some broken rewrites in algebra/sts and it makes canonical structures work properly with dec_agree.

 23 Mar, 2016 40 commits


Robbert Krebbers authored

 11 Mar, 2016 40 commits


Ralf Jung authored

Robbert Krebbers authored
Should be restored later.

Robbert Krebbers authored
The only drawback is that we have to restrict iprod to finite types, but that is fine.

 10 Mar, 2016 40 commits


Robbert Krebbers authored
Thanks to Amin Timany for the suggestion.

 08 Mar, 2016 40 commits


Ralf Jung authored

 07 Mar, 2016 40 commits


Ralf Jung authored

 03 Mar, 2016 40 commits


Robbert Krebbers authored
Contrary to destruct_conj from Program.

 01 Mar, 2016 40 commits


Robbert Krebbers authored

 29 Feb, 2016 40 commits


Ralf Jung authored

 25 Feb, 2016 40 commits
 24 Feb, 2016 40 commits


Robbert Krebbers authored
It now traverses terms at most once, whereas the setoid_rewrite approach was travering terms many times. Also, the tactic can now be extended by defining type class instances.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This way it behaves better for discrete CMRAs.

 23 Feb, 2016 40 commits


Ralf Jung authored
 22 Feb, 2016 40 commits


Robbert Krebbers authored
due to an accidental git commit amend after a git push.

Robbert Krebbers authored
In most cases there is a lot of duplicate proof search performed by both naive_solver and eauto. Especially since naive_solver calls its tactic (in the case of set_solver this used to be eauto) quite eagerly this made it very slow. Note that set_solver is this too slow and should be improved.

Robbert Krebbers authored
In most cases there is a lot of duplicate proof search performed by both naive_solver and eauto. Especially since naive_solver calls its tactic (in the case of set_solver this used to be eauto) quite eagerly this made it very slow. Note that set_solver is this too slow and should be improved.

Robbert Krebbers authored

 21 Feb, 2016 40 commits


Ralf Jung authored
This is all still pretty ad hoc, but oh well. Also, I have no idea why I had to make those instances in sta_dra global, but it complained about missing instances. Actually, I wonder how they could *not* be global previously...

Ralf Jung authored
This strengthens some lemmas that are written using the notion of closednes, shortening some proofs all the way up to barrier.v

 20 Feb, 2016 40 commits
 19 Feb, 2016 40 commits


Robbert Krebbers authored

 17 Feb, 2016 40 commits


Robbert Krebbers authored
It is doing much more than just dealing with ∈, it solves all kinds of goals involving set operations (including ≡ and ⊆).

Robbert Krebbers authored
simplify_equality => simplify_eq simplify_equality' => simplify_eq/= simplify_map_equality => simplify_map_eq simplify_map_equality' => simplify_map_eq/= simplify_option_equality => simplify_option_eq simplify_list_equality => simplify_list_eq f_equal' => f_equal/= The /= suffixes (meaning: do simpl) are inspired by ssreflect.

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

 16 Feb, 2016 40 commits


Robbert Krebbers authored
* Clearly separate the file algebra/sts in three parts: 1.) The definition of an STS, step relations, and closure stuff 2.) The construction as a disjoint RA (this module should never be used) 3.) The construction as a CMRA with many derived properties * Turn stsT into a canonical structure so that we can make more of its arguments implicit. * Rename the underlying step relation of STSs to prim_step (similar naming as for languages, but here in a module to avoid ambiguity) * Refactor program_logic/sts by moving general properties of the STS CMRA to algebra/sts.v * Make naming and use of modules in program_logic/sts more consistent with program_logic/auth and program_logic/saved_prop * Prove setoid properties of all definitions in program_logic/sts

Ralf Jung authored

Ralf Jung authored
