0
$\begingroup$

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

instance : Add Pos where
  add := Pos.add

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?

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$ Sep 4, 2023 at 11:57

1 Answer 1

2
$\begingroup$

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
$\endgroup$
2
  • $\begingroup$ I agree, except I would delete the "can be either true or false" part, for educational reasons. $\endgroup$ Sep 4, 2023 at 11:58
  • $\begingroup$ 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. $\endgroup$
    – Nate Glenn
    Sep 8, 2023 at 4:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.