# proof-based Pos type class

I'm working my way through the chapter on type classes in Functional Programming in Lean. The text demonstrates type-classes by representing positive numbers this way:

inductive Pos : Type where
| one : Pos
| succ : Pos → Pos


The first exercise then asks the reader to represent them this way:

structure Pos where
succ ::
pred : Nat


I completed the exercise, and then wondered how it would be to simply package together a natural number and a proof that it's positive. This is what I have so far:

structure Pos where
n: Nat
nPos: n > 0

structure Pos where
n: Nat
nPos: n > 0

def Pos.add : Pos → Pos → Pos
| Pos.mk n _, Pos.mk k _ => Pos.mk (n + k) sorry

def seven : Pos :=
Pos.mk 7 sorry

def fourteen : Pos := seven + seven

def Pos.toNat : Pos → Nat
| Pos.mk n _ => n

instance : ToString Pos where
toString x := toString (x.toNat)

#eval s!"There are {seven}"

def Pos.mul : Pos → Pos → Pos
| Pos.mk n _, Pos.mk k _=> Pos.mk (n*k) sorry

instance : Mul Pos where
mul := Pos.mul

#eval [seven * (Pos.mk 1 sorry),
seven * seven,
(Pos.mk 2 sorry) * seven]

instance : OfNat Pos (n + 1) where
ofNat := Pos.mk (n+1) sorry

def eight : Pos := 8


Obviously this is no good because I don't know what to put instead of sorry in several places. Lean wouldn't accept Pos.mk 7 (7 > 0), but I don't quite understand the error message:

application type mismatch
{ n := 7, nPos := 7 > 0 }
argument
7 > 0
has type
Prop : Type
but is expected to have type
7 > 0 : Prop


I would also need a proof that adding two positives or multiplying two positives give another positive, which is intuitively obvious but I don't know if Lean has built-in knowledge for it.

I think this approach is probably too cumbersome, but I would like to complete it just to see how it would play out. How should I fill in the sorry's in my code?

• Writing Pos.mk 7 (7 > 0) is the same sort of mistake as writing 7 + Nat. You wrote a type 7 > 0 where its element was required. Sep 4, 2023 at 11:57

7 > 0 is a statement that can be either true or false. However what you need to provide is a proof of 7 > 0. Repeating the theorem statement doesn't count as a proof.
Think about how you will fill the following sorry:
theorem pos_seven : 7 > 0 := by sorry

• Well, the magic formula for this particular part happens to be (by decide). I still don't know what to put in add, mul, or ofNat. Sep 8, 2023 at 4:55