hahn
hahn copied to clipboard
vafeiadis
Hahn: A Coq library
It seems that the index given to the `LTS_final` predicate is incorrect in [HahnTrace, line 733](https://github.com/vafeiadis/hahn/blob/master/HahnTrace.v#L733). If I am not mistaken, `LTS_final` is used to denote the terminal state. However...
Adds a tactic for easier work with constrictive_indefinite_description, which I needed reasonably often in a couple of my recent projects. To me, the tactic has a distinct des_something feel about...
It seems some lemmas are incompatible with 8.15.1, or something is wrong on my end. The problems are in HahnMinPath and HahnWf. the problem in HahnWf seems to be related...
These lemmas are used in the 'relive' project. Most of them are general, except for `LTS_traceE'` which, together with existing `LTS_traceE`, states the equivalence of two LTS trace definitions.
This is not an actual "issue", but rather a question about the design of the library. I am a bit confused about the relationship between `(co)dom_rel` and `doma`/`domb`. `dom_rel` is...
``` Goal forall a b c d e f g h i : relation actid, a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h...
``` Lemma plain_coherence_helper (r s t : relation actid) : r ∩ s⁻¹ ∪ t ≡ ∅₂ -> irreflexive (s ⨾ r). Proof. basic_solver 42. ``` gives me ``` All...