Eval with Prop

Stream: new members

[Hunter Spink]

I'm trying to #eval to test my code on examples, all of which uses Prop instead of Bool. I was told this was the better choice for proving theorems, and currently all of my code is at the moment in def environments. A stripped down version of my problem is that the following code

Import Mathlib
def E (a:ℕ):Prop := a>5
#eval E 1

gives the error
failed to synthesize
Decidable (E 1)

How can I coerce Prop to Bool or resolve the error another way?

[Kyle Miller]

Decidable is essentially the typeclass for coercing Prop to Bool. It's telling you that it couldn't find a coercion.

What you could do here is change the def to an abbrev, to let typeclass search see into the definition.

[Hunter Spink]

Thanks -- as a followup, I have a slightly more complex example, which I've stripped down to isolate the problem. It appears that looping the "add edge" function is breaking #eval even though adding a single edge is fine.

Any advice?

import Mathlib

structure Graph (α : Type u) where
  V: List α
  E: α → α → Prop := (fun x y => False)

abbrev addEdge (G: Graph α) (x y:α): Graph α:=
  have E' (a b : α): Prop :=
    ((a=x ∧ b=y)∨(a=y ∧ b=x)∨(G.E a b))
  { V := G.V, E := E' : Graph α}

abbrev addEdges (G: Graph α) (Edges:List (α× α)): Graph α:=
  loop Edges G
where
  loop : List (α×α)→ (Graph α)→ (Graph α)
    | [], G => G
    | (⟨x,y⟩)::as, G => loop as (addEdge G x y)

abbrev testGraph : Graph ℕ:= {V:=[1,2,3]}
abbrev testGraph1 : Graph ℕ:= addEdge testGraph 1 2
abbrev testGraph2: Graph ℕ:= addEdges testGraph [(1,2)]

#eval testGraph1.E 1 2 --works
#eval testGraph2.E 1 2 --doesn't work

[Kyle Miller]

abbrev works for simple sorts of definitions, but addEdges is recursive. One way is to write a Decidable instance.

Another is to switch E to be Bool-valued (at the cost of it being more natural to use boolean notations rather than proposition notations).

[Kyle Miller]

I guess another solution is to avoid a recursive definition:

abbrev addEdges (G : Graph α) (edges : List (α × α)) : Graph α :=
  let E' (a b : α) : Prop := (a, b) ∈ edges ∨ (b, a) ∈ edges ∨ G.E a b
  { V := G.V, E := E' }

It's a Prop, so there's no need to write it like you're computing anything. (A Decidable instance is what turns a given Prop into a computation.)

[Chris Bailey]

Alternatively you can supply more information about E. This works, assuming the alpha type has decidable equality:

universe u
variable {α : Type} [DecidableEq α]
structure Graph (α : Type u) [DecidableEq α] where
  (V: List α)
  (E: α → α → Prop := (fun x y => False))
  [hDec : DecidableRel E]

instance (g : Graph α) : DecidableRel g.E := g.hDec

abbrev addEdge (G: Graph α) (x y:α): Graph α:=
  let E' (a b : α): Prop :=
    ((a=x ∧ b=y)∨(a=y ∧ b=x) ∨(G.E a b))
  { V := G.V, E := E' : Graph α}

abbrev addEdges (G: Graph α) (Edges:List (α× α)): Graph α:=
  loop Edges G
where
  loop : List (α×α)→ (Graph α)→ (Graph α)
    | [], G => G
    | (⟨x,y⟩)::as, G => loop as (addEdge G x y)

abbrev testGraph : Graph ℕ:= {V:=[1,2,3]}
abbrev testGraph1 : Graph ℕ:= addEdge testGraph 1 2
abbrev testGraph3: Graph ℕ:= addEdges testGraph []

abbrev testGraph2: Graph ℕ:= addEdges testGraph [(1,2)]

#eval testGraph1.E 1 2 --works
#eval testGraph2.E 1 2
#eval testGraph3.E 1 2

[Kyle Miller]

If you include DecidableRel in the structure, I think you may as well make it be E : α → α → Bool. (I'd also avoid adding DecidableEq to the type. You can move that to addEdge and addEdges.)

[Chris Bailey]

Good call on moving the decidable Eq instance. I'm way out of practice as an end user of lean, but I do remember really needing to baby-step propagation of decidable instances when doing stuff like this.