 05 Jun, 2019 5 commits


Maxime Lesourd authored

Maxime Lesourd authored

Maxime Lesourd authored

Maxime Lesourd authored

Björn Brandenburg authored
Using the official Coq Docker images kindly provided by the Coq community: https://github.com/coqcommunity/dockercoq/wiki/CIsetup Using the following CI template as a starting point: https://gitlab.com/erikmd/dockercoqgitlabcidemo1/blob/master/.gitlabci.yml

 26 May, 2019 1 commit


Sergey Bozhko authored

 19 May, 2019 1 commit


Sergey Bozhko authored

 16 May, 2019 10 commits


Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored
...and introduce a bunch of helper lemmas to get there.

Björn Brandenburg authored

Björn Brandenburg authored
Let's not clutter up the spec with facts files all over the place. Instead, let's collect the facts files in a separate folder / hierarchy.

Björn Brandenburg authored

Björn Brandenburg authored
 port completed_implies_scheduled_before  port lemmas on service prior to arrival  port scheduled_implies_pending and greatly simplify the proof while at it  port and simplify job_pending_at_arrival  port cumulative_service_implies_scheduled and simplify proof of positive_service_implies_scheduled_before  port service_is_a_step_function

Björn Brandenburg authored

Björn Brandenburg authored

 13 May, 2019 9 commits


Björn Brandenburg authored

Björn Brandenburg authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Björn Brandenburg authored
...from model/schedule/uni/schedule.v. To simplify some of the rather long proofs in the original file, the patch introduces a bunch of small and simple rewriting and helper lemmas that we previously lacked, but that we *should* have to avoid having to reason at the level of sslreflect "big" operators in every lemma.

 12 May, 2019 1 commit


Sergey Bozhko authored

 07 May, 2019 3 commits


Björn Brandenburg authored
If one names a branch "somethingsomethingfile.v", then the current script will find it in the .git directory and try to compile git's branch description as a Coq file...

Björn Brandenburg authored
See https://beyondgrep.com/ for details.

Maxime Lesourd authored
Initial draft of the base for the behavior part of the refactored hierarchy. Implements most of the proposal discussed in Braunschweig.

 03 May, 2019 1 commit


Sergey Bozhko authored

 29 Apr, 2019 1 commit


Björn Brandenburg authored
The proof got stuck at the goal of {in l1, forall x0 : T, x0 != x} which requires unfolding of prop_in1 to get at the x0 before intros can be effective.

 09 Apr, 2019 1 commit


Björn Brandenburg authored

 05 Apr, 2019 7 commits


Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored
