 09 Dec, 2016 1 commit


Ralf Jung authored

 05 Dec, 2016 1 commit


Robbert Krebbers authored
Using this new definition we can express being contractive using a Proper. This has the following advantages:  It makes it easier to state that a function with multiple arguments is contractive (in all or some arguments).  A solve_contractive tactic can be implemented by extending the solve_proper tactic.

 17 Nov, 2016 1 commit


Robbert Krebbers authored

 10 Oct, 2016 2 commits
 16 Aug, 2016 1 commit


Ralf Jung authored

 09 Aug, 2016 1 commit


Ralf Jung authored

 22 Jul, 2016 2 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 1 commit


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 1 commit


Robbert Krebbers authored

 11 Mar, 2016 3 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 1 commit


Robbert Krebbers authored
Thanks to Amin Timany for the suggestion.

 08 Mar, 2016 1 commit


Ralf Jung authored

 07 Mar, 2016 1 commit


Ralf Jung authored

 03 Mar, 2016 1 commit


Robbert Krebbers authored
Contrary to destruct_conj from Program.

 01 Mar, 2016 1 commit


Robbert Krebbers authored

 29 Feb, 2016 1 commit


Ralf Jung authored

 25 Feb, 2016 2 commits
 24 Feb, 2016 4 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 2 commits


Ralf Jung authored
 22 Feb, 2016 4 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 2 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 3 commits
 19 Feb, 2016 1 commit


Robbert Krebbers authored

 17 Feb, 2016 2 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.
