structures with contracts

Stream: general

[Matthew Pocock]

Say I have a type

structure OrdPair
  lower : Nat
  higher : Nat

I want this struct to have the additional contractual guarantee that lower < higher. So can I have the struct carry the proof somehow? Something like this?

structure OrdPair
  lower : Nat
  higher : Nat
  is_ord: lower < higher

Is this possible? Is it considered a code smell or a sound design choice? I couldn't see any examples like this in the Functional Programming in Lean book, but I may well have missed it.

[Kyle Miller]

Yeah, I'd say that's fine. There's a bit of a tradeoff where it puts more of a proof burden inside of your algorithms, vs proving your algorithms are correct after the fact, but especially if you're not going to formally verify an algorithm, it's great being able to take advantage of Lean to embed contracts like this.

Here's something else you can do:

structure OrdPair
  lower : Nat
  higher : Nat
  is_ord : lower < higher := by simp

Then in simple cases like def p : OrdPair := {lower := 1, higher := 10} the tactic will fill in the proof automatically.

[Kevin Buzzard]

Surely := by norm_num?

[Matthew Pocock]

Kyle Miller said:

but especially if you're not going to formally verify an algorithm, it's great being able to take advantage of Lean to embed contracts like this.

At the moment these structs are there to model the domain of my proofs.

Here's something else you can do:

structure OrdPair
  lower : Nat
  higher : Nat
  is_ord : lower < higher := by simp

Oh, that's neat. Thanks :D

[Matthew Pocock]

Kyle Miller said:

Yeah, I'd say that's fine.

So I've written my first thing :D

def collatz (n : Nat) := if Even n then n / 2 else 3 * n + 1

structure CollatzSequence where
    left: Nat
    right: Nat
    length: Nat
    is_valid : Nat.iterate collatz length left = right

def CollatzSequence.join (ls rs : CollatzSequence) (touch: ls.right = rs.left): CollatzSequence :=
    { left := ls.left, right := rs.right , length := rs.length + ls.length, is_valid := by
        have lh := ls.is_valid
        have rh := rs.is_valid
        rw [touch] at lh
        rw [Eq.symm lh] at rh
        have cmp := Function.iterate_add_apply collatz rs.length ls.length ls.left
        simp [Eq.symm cmp] at rh
        assumption
    }

Not sure if it will be useful in practice, but it was a good learning exercise.

[Eric Rodriguez]

you can write Eq.symm cmp as cmp.symm by the way :) or in tactics like simp and rw, also as ←cmp.

[Matthew Pocock]

Ah, that certainly tidies it up a bit @Eric Rodriguez . The apply? tactic doesn't seem to know about this :/