ssreflect - [ssreflect] Partial order extension

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Partial order extension

From: Felipe Cerqueira <>
To: "" <>
Subject: [ssreflect] Partial order extension
Date: Mon, 19 Sep 2016 11:23:05 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:OcagtxNTIGEx7pYl6m8l6mtUPXoX/o7sNwtQ0KIMzox0Kfz6rarrMEGX3/hxlliBBdydsKMdzbqK+Pi/ESxYuNDa4ShEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9GO35F8bogtit0KjqotuIMlwO1Gb2Oew6bE3v616A7o9O2coqA51y4yOBmmFPdeVSyDEgDnOotDG42P2N+oV++T9bofMr+p0Ie6z7e6MlUe4QV2x+YChmrPHs4FPYVhGC6H8RWXk+lwFSRgnD9hDzGJb3qCrz8ORnkmHOJtbsQL4wVD++x6JwUlrpjj0GPng49nvWg4p+lvQIjgimoklRzorVeIzdH/dkZ77QfMkTDT5PU8JQTyFKKoakbs4UEPFHOvxX+dqu72ASpAezUFH/TNjkzSVF0yf7

Hi everyone,

In my development I have a "<=" relation over a finite type that is total but not antisymmetric,
so when I restrict it to the strict order "<", it is no longer total.
I need to create an extension of < that preserves totality.

I already have an implementation for Prop relations, but it's not compatible with
Mathematical Components.
Does anyone know of an existing implementation for such a partial order extension?

In case I need to implement it myself, it seems that the definitions of transitive closure
are the ones in the graph library, right? I haven't worked with that library so far.

Thanks,
Felipe

[ssreflect] Partial order extension, Felipe Cerqueira, 09/19/2016
- [ssreflect] Non-reflexive version of connect, Felipe Cerqueira, 09/27/2016

List archive

[ssreflect] Partial order extension