Attempting to define An interval

Stream: lean4

[Eric Fode (he) (S'12)]

universe u v w

---------------- The Interval   The value
class Interval (α : Type v) (β : Type w) [LE β] [BEq β]  where
  upp : α -> β
  low : α -> β
namespace Interval

#check Eq
variable {α  : Type v} {β : Type w}
variable [LE β] [BEq β]
variable (n : Interval α β)

def isEmpty : Bool := (upp n) == (low n)

Getting a failed to synthesize instance BEq (\alpha \to \beta)
how should i think about debugging this?

[Leonardo de Moura]

upp n and low n are functions. Did you mean to write

def isEmpty (a : α) : Bool := (upp n) a == (low n) a

?

[Eric Fode (he) (S'12)]

That worked, thank you. I think i'm fundamentally misunderstanding how this should fit together.

[Eric Fode (he) (S'12)]

Is the idea that "n" is a particular instance of the the Interval type class?

[Eric Fode (he) (S'12)]

and a is a particular instance of a type which this type class is defined over?

[Eric Fode (he) (S'12)]

When is Bool appropriate vs, Prop?
in this def for example
def contains (hn : β) : Prop := ((n.low a) ≤ hn) ∧ (hn ≤ (n.upp a))

[Mac]

@Eric Fode (he) (S'12) The short version is: Prop is for proofs, Bool is for computations (programming).

[Eric Fode (he) (S'12)]

So if i write that contains function (as above) I need to do one version for proofs and one version for programming?

[Eric Fode (he) (S'12)]

Or is there a way i can use one and transform it into the other?

[Eric Fode (he) (S'12)]

Is that what decidable is for?

[Mac]

To convert a (arbitrary) Prop to a Bool, the Prop needs to be decidable (i.e., be a possible instance of Decidable). To convert a Bool to a Prop one can just check for equality with true (i.e., b = true).

[Mac]

That, is of course, assuming you want the Bool to be true when the Prop holds and false when it does not.

[Mac]

For a specific p : Prop, if you already have a proof of it (i.e., x : p) or its negation (i.e., x : ~p), then you already know whether the Bool should be true or false, so you could just use either literal.

[Eric Fode (he) (S'12)]

Interesting, i'll give it a shot