The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Pierre,

thanks a lot, especially for the hint to BoolOrderFacts. I missed this under 
the "Order relations derived from a compare function" headline and started to 
implement it myself. So the elegant way to do what I want is to use 
BoolOrderFacts.

I think it would make sense to insert something like a "Boolean order facts" 
headline - it is easy to miss this important module functor.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Pierre Letouzey
Sent: Thursday, May 7, 2015 11:00 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Most elegant way to prove ltb properties from lt 
properties?


Hi Michael

The coercion by itself won't bring you far, it's just a convenient way to 
shorten statements. For instance in Orders.v, a statement such as (Transitive 
X.leb) would have to be written (Transitive (fun a b => X.leb a b = true)) if 
you don't use coercion.

For proving things about leb or ltb, all depends on the known facts about 
them. For instance, in Orders.v I tend to specify leb and ltb by equivalence 
w.r.t. some logical relation le and lt (see leb_le and ltb_lt), so proofs 
about leb and ltb would start by some rewrite such as leb_le or ltb_lt, and 
then exploit some properties of le and lt. You can have a look at the functor 
BoolOrderFacts in OrdersFacts.v, it contains a few proofs made this way 
(including your ltb_irrefl). Of course, the conversion from leb/ltb to le/lt 
could be automated more (for instance via a few rewrite rules given to 
autorewrite, or any more advanced technics such as reflection). But for the 
moment, the small amount of proofs made about leb/ltb hasn't made me spend 
much time on this aspect.

Best regards,
Pierre Letouzey

----- Mail original -----
> Dear Coq Users,
> 
> the standard library file Coq.Structures.Orders.v contains the comment:
> 
> For stating properties like transitivity of leb, we coerce bool into Prop.
> 
> which makes me think there is a better way than tedious manual proofs 
> for things like transitivity or irreflexivity of ltb, but I couldn't 
> find it. I added
> 
> Local Coercion is_true : bool >-> Sortclass.
> 
> but I don't see how this would help me to e.g. get a trivial proof for
> 
> Lemma ltb_irrefl: forall x : t, ltb x x = false.
> 
> Thanks & best regards,
> 
> Michael
> 
>