The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

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
> 
>