Stream: Coq users

Topic: help from library

view this post on Zulip sara lee (Aug 27 2022 at 16:18):

I am converting
(S a) <= b) into boolean form but it is giving error. What could be reason?

view this post on Zulip Julin S (Aug 29 2022 at 03:55):

Could you also include the code giving the error? Could help people understand what's the error is about better.

view this post on Zulip sara lee (Aug 30 2022 at 15:13):

I want to prove above relation . lt from library may helpful in proving the above relation(in the presence of H: b > 0) ? Secondly,

 (a0+2 <? a1)  && (a2 <? a3) &&  (a4 <? a5) = true

I am applying command " try rewrite ltb_lt" , but it is not working.

view this post on Zulip Pierre Castéran (Aug 30 2022 at 18:44):

You should transform your goal before applying Nat.ltb_lt.

repeat rewrite Bool.andb_true_iff.  repeat rewrite Nat.ltb_lt.

Last updated: Oct 03 2023 at 21:01 UTC