## Stream: new members

### Topic: Prop in function type as precondition

#### Ivan Tsoninski (Mar 10 2021 at 17:49):

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 (Mar 10 2021 at 17:50):

In this case, dec_trivial

#### Ivan Tsoninski (Mar 10 2021 at 17:57):

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 (Mar 10 2021 at 18:06):

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

#### Ivan Tsoninski (Mar 10 2021 at 18:13):

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 (Mar 10 2021 at 18:19):

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

#### Yakov Pechersky (Mar 10 2021 at 18:20):

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 (Mar 10 2021 at 18:21):

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

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


#### Yakov Pechersky (Mar 10 2021 at 18:22):

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 (Mar 10 2021 at 18:23):

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 (Mar 10 2021 at 18:25):

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

(deleted)

#### Ivan Tsoninski (Mar 10 2021 at 18:31):

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

#### Yakov Pechersky (Mar 10 2021 at 18:33):

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 (Mar 10 2021 at 18:35):

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

#### Chris B (Mar 10 2021 at 18:35):

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 (Mar 10 2021 at 18:35):

(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 (Mar 10 2021 at 18:40):

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 (Mar 10 2021 at 18:43):

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 (Mar 10 2021 at 18:46):

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

#### Ivan Tsoninski (Mar 10 2021 at 18:49):

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 (Mar 10 2021 at 18:51):

Try leanproject new to easily set up a mathlib dependency

Last updated: Dec 20 2023 at 11:08 UTC