Prop in function type as precondition

Stream: new members

[Ivan Tsoninski]

def make_greater : Π min:nat, Π n:nat, (n > min) → nat := λ _ n _, n
#eval make_greater 4 6 sorry -- should give 6

I am trying to write this function. The idea is that there is a predicate as a pre-condition. Is this possible?
What can I replace sorry with?

[Yakov Pechersky]

In this case, dec_trivial

[Ivan Tsoninski]

Thanks! And do you know if it is possible to make it implicit with curly braces like:

def make_greater : Π min:nat, Π n:nat, {n > min} → nat := λ _ n _, n

So that you don't have to pass dec_trivial.
It complains with "failed to synthesize type class instance for min n : % |- has_singleton Prop (Sort ?)"
but I don't know how to address that.

[Yakov Pechersky]

How would you want to the proof to be inferred implicitly? What if I said make_greater 0 0?

[Yakov Pechersky]

What's your larger goal? #xy

[Ivan Tsoninski]

Yakov Pechersky said:

How would you want to the proof to be inferred implicitly? What if I said make_greater 0 0?

If you said that then it wouldn't type check. The same if you said make_greater 0 0 dec_trivial.
The larger goal is to learn how a dependently typed language can allow me to encode preconditions. I am starting with a simple precondition.
I can imagine I would have to manually build proofs for more complex cases but it would be cool if I don't have to pass them around.

[Yakov Pechersky]

make_greater 0 0 would definitely still typecheck, it would be a function of 0 < 0 -> 0.

[Yakov Pechersky]

You are still encoding a precondition, and whatever uses make_greater would have to supply the proof. Currently, you have an easy way of generating that proof, which is dec_trivial. For more complicated uses, you'd have to write code that knew how to generate the proper proof. That could be some other tactic.

[Yakov Pechersky]

def make_greater (min n : ℕ) (h : n > min) : ℕ := n

example (h : 0 < 0) : make_greater 0 0 h = 0 := rfl

[Yakov Pechersky]

Of course, you could say that h : 0 < 0 implies false, which implies anything, but I'm just showing here that contradictory hypotheses are possible.

[Chris B]

There's a syntax you can use for binders (x : A . t) that means "try to make x : A for me by using tactic t".

def make_greater (n min : nat) (h : n > min . tactic.dec_trivial) : nat := n
def testOK := make_greater 2 1
#eval testOK
def testNG := make_greater 1 2
-- no good

[Yakov Pechersky]

For this function, I get unexpected occurrence of field notation expression when trying to define it like your example

[Yakov Pechersky]

(deleted)

[Ivan Tsoninski]

I am also getting unexpected occurrence of field notation expression but it looks cool.

[Yakov Pechersky]

You can view https://github.com/Julian/lean-across-the-board/blob/6802cf5c4a88395c179429df3e7135295f8bb9a3/src/chess/board.lean#L68 for an example of how . dec_trivial can deal with preconditions

[Julian Berman]

For reasons I forget, you need tactic.exact_dec_trivial I think

[Chris B]

I forgot this is how logical verification has to introduce it.

meta def tactic.dec_trivial := `[exact dec_trivial]

def make_greater (n min : nat) (h : n > min . tactic.dec_trivial) : nat := n
def testOK := make_greater 2 1
#eval testOK
def testNG := make_greater 1 2

[Julian Berman]

(After which yeah that works for me here too, i.e.:

import tactic.dec_trivial

def make_greater (n min : nat) (h : (n > min) . tactic.exact_dec_trivial) : nat := n
def testOK := make_greater 2 1
#eval testOK
def testNG := make_greater 1 2

)

[Ivan Tsoninski]

Chris B said:

I forgot this is how logical verification has to introduce it.

meta def tactic.dec_trivial := `[exact dec_trivial]

def make_greater (n min : nat) (h : n > min . tactic.dec_trivial) : nat := n
def testOK := make_greater 2 1
#eval testOK
def testNG := make_greater 1 2

This works, Thanks! I don't know enough to understand it but it is very interesting!

[Ivan Tsoninski]

Julian Berman said:

(After which yeah that works for me here too, i.e.:

import tactic.dec_trivial

I think I need to download a library for this? It says the file cannot be found in the search path.

[Yakov Pechersky]

Are you working on just a lean file, or do you have a mathlib dependency? How did you set up your lean?

[Ivan Tsoninski]

Yakov Pechersky said:

Are you working on just a lean file, or do you have a mathlib dependency? How did you set up your lean?

File, I will look into setting up a project properly. Thanks!

[Yakov Pechersky]

Try leanproject new to easily set up a mathlib dependency