Switch to the standard type for relations. #16
Conversation
| lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) : | ||
| Relation.ReflTransGen R A B → | ||
| R A C → | ||
| lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) : |
There was a problem hiding this comment.
Are these identified by a linter? If so, can we enable this by default/include it in a workflow check?
| /-- Inverse of a relation. -/ | ||
| def Relation.inv (r : α → β → Prop) : β → α → Prop := flip r | ||
|
|
||
| -- /-- Composition of two relations. -/ |
There was a problem hiding this comment.
Commented out definition?
| (r1 r2 : Rel State State) (h1 : Simulation lts r1) (h2 : Simulation lts r2) : | ||
| Simulation lts (r1.comp r2) := by | ||
| (r1 r2 : State → State → Prop) (h1 : Simulation lts r1) (h2 : Simulation lts r2) : | ||
| Simulation lts (Relation.Comp r1 r2) := by |
There was a problem hiding this comment.
Does Relation.Comp have a notation? If so, that would be preferred here.
There was a problem hiding this comment.
Same question regarding the usage of Relation.inv.
| constructor | ||
| case left => | ||
| simp only [Rel.comp] | ||
| simp only [Relation.Comp] |
There was a problem hiding this comment.
All uses of simp only [Relation.Comp] in this file are not needed.
| constructor | ||
| · exact h2'tr | ||
| · simp [Rel.comp] | ||
| · simp only [Relation.Comp] |
There was a problem hiding this comment.
All uses of simp only [Relation.Comp] in this file are not needed.
| /-- Union of two relations. -/ | ||
| def Relation.union (r s : α → β → Prop) : α → β → Prop := | ||
| fun x y => r x y ∨ s x y | ||
|
|
||
| instance {α : Type u} {β : Type v} : Union (α → β → Prop) where | ||
| union := Relation.union |
There was a problem hiding this comment.
Mathlib already provides this with ⊔ notation
| /-- The identity relation. -/ | ||
| inductive Relation.Id : α → α → Prop where | ||
| | id {x : α} : Id x x |
There was a problem hiding this comment.
Oh, that's a surprising name from the textbooks I'm used to. Thanks for pointing it out, I'd been naively looking for Id.
There was a problem hiding this comment.
Ah, it's because I was looking for it in mathlib as a Rel a long time ago.. the Eq from Lean is of course what I want. Adopting it is even simplifying some proofs!
* Switch to the standard type for relations. * Missing changes
This PR creates a new
Cslib.Data.Relationfile with some utilities and a union notation for relations, merging the previous filesCslib.Utils.RelandCslib.Utils.Relation(now deleted).It removes all dependencies of the recently-changed
Reltype from mathlib, in preparation for bumping our mathlib dependency.I'm a bit in doubt as to the name styling for definitions such as 'Relation.inv' and 'Relation.union'. In mathlib, they are uppercased for
Relationbut lowercased forRel, I guess because forRelationone knows that the final type isProp. It is however a bit weird.