in coq how to assume equality of two natural numbers

Question

I want to use this definition to assume that certain equalities on the members of set R hold:


Definition wiring: Prop
    (globalHasVoltage -> (voltageOf voltageIn) = vcc)
    /\
    (globalHasGround -> (
                            (voltageOf control) = zero
                            /\
                            (voltageOf ground) = zero
                        )
    )
.

It seems coq distinguishes between Prop and bool, what are the differences, and how may i solve that issue?

Also If this definition implies some other definition (per say lets call it toBeEvaluated) and assuming that conversion between bool and prop can be done could this

Definition toBeEvaluated: Prop := (voltageOf voltageIn) = vcc.

be proven using unwraps and tauto. (In particular will it work with functions which have exact definitions)

Regarding your first question, you might want to look at https://stackoverflow.com/a/31568076/1633770. Regarding your second question, it would help if you could give us a bit more context to understand what you are trying to do. Can you give us a code snippet that we can run in a self-contained way? — Arthur Azevedo De Amorim, Apr 24 '22 at 19:13

M Soegtrop · Answer 1 · 2022-04-25T08:29:57.973

The difference between Prop and bool is that definitions in Prop might be undecidable, while definitions in bool can always be computed (unless you use axioms). Many number types have bool and Prop equality operators, but R doesn't because equality in R is in principle undecidable, so one can't write an equality function for R which results in a bool. Imagine e.g. the equality of different infinite series which sum up to pi - one can't design a general algorithm which decides if two series result in pi or not. Electronics uses functions like sin which rely on such infinite series.

A few options / thoughts:

R is not a very appropriate type for signal levels. E.g. voltage levels like GND or VCC are not mathematically equal everywhere. You could e.g. work with ranges in Q to express signal levels.
Another appropriate type might be floating point numbers, which are supported by Coq (meanwhile also natively). Have a look at the coq-flocq package. For floating point numbers equality is decidable, but they won't be able to represent a voltage like 1.8V exactly.
Another option is to have an inductive type which has a few well known signal levels (GND, VCC, ...) but also a constructor for arbitrary R (either classic or constructive). At least for the well known levels equality would be decidable then, but not for the arbitrary levels.
Even though = is not decidable in R, you can usually proof equality of R expressions, e.g. using the ring or field tactic. But you can't prove automatically that say sin(pi/4)=cos(pi/4). Well of cause one can automate this as well, but such automation always will have limits. But this means that your equalities always need to be proven with tactics and can't be just computed.

P.S.: The standard library has definitions like `Req_EM_T: forall r1 r2 : R, {r1 = r2} + {r1 <> r2}` from one could derive a bool equality function for R, but such definitions use axioms of R and don't compute. — M Soegtrop, Apr 25 '22 at 08:26

in coq how to assume equality of two natural numbers

1 Answers1