## Stream: new members

### Topic: Deriving hypothesis from if statements

#### Tobias Grosser (Oct 02 2018 at 18:55):

Hi, I am currently cleaning up my gaussian elimination proof. At one point I defined the following functions:

def fin_first {n m} (i : fin (n + m)) {h: i.val < n}: fin (n) :=
⟨i.1, begin apply h end⟩

def fin_second {n m} (i : fin (n + m)) {h: i.val >= n}: fin (m) :=
⟨i.1 - n, begin sorry end⟩

def block_mx {m_down m_up n_left n_right: nat} :
matrix (fin m_up) (fin n_left) α →
matrix (fin m_up) (fin n_right) α →
matrix (fin m_down) (fin n_left) α →
matrix (fin m_down) (fin n_right) α →
matrix (fin (m_up + m_down)) (fin (n_left + n_right)) α
| up_left up_right down_left down_right :=
λ i j,
if i.val < m_up
then
if j.val < n_left
then
up_left (fin_first i) (fin_first j)
else
up_right (fin_first i) (fin_second j)
else
if j.val < n_left
then
down_left (fin_second i)  (fin_first j)
else
down_right (fin_second i) (fin_second j)
 app

Whenever I apply fin_first and fin_second, I would like to make the hypothesis "h" available based on the information in the if-condition.


#### Tobias Grosser (Oct 02 2018 at 18:56):

I feel this is a super trivial question, but I did not find a good example googling for it. Can somebody throw me the right keywords / reference?

#### Rob Lewis (Oct 02 2018 at 18:59):

If you write if h : j.val < n_left then _ else _ you'll get local hypotheses with the right types in the placeholders.

#### Tobias Grosser (Oct 02 2018 at 19:00):

test.lean:25:29: error

don't know how to synthesize placeholder
context:
α : Type,
m_down m_up n_left n_right : ℕ,
block_mx :
matrix (fin m_up) (fin n_left) α →
matrix (fin m_up) (fin n_right) α →
matrix (fin m_down) (fin n_left) α →
matrix (fin m_down) (fin n_right) α → matrix (fin (m_up + m_down)) (fin (n_left + n_right)) α,
up_left : matrix (fin m_up) (fin n_left) α,
up_right : matrix (fin m_up) (fin n_right) α,
down_left : matrix (fin m_down) (fin n_left) α,
down_right : matrix (fin m_down) (fin n_right) α,
i : fin (m_up + m_down),
j : fin (n_left + n_right),
h : j.val < n_left
⊢ j.val < n_left


#### Tobias Grosser (Oct 02 2018 at 19:00):

I seem to be so close.

#### Tobias Grosser (Oct 02 2018 at 19:00):

I would hope lean picks this from the context. But it does not seem to do so.

#### Patrick Massot (Oct 02 2018 at 19:01):

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html?highlight=dite#decidable-propositions

#### Rob Lewis (Oct 02 2018 at 19:01):

You want Lean to fill in those arguments automatically when it finds them in the local context?

#### Rob Lewis (Oct 02 2018 at 19:02):

You can write def fin_first {n m} (i : fin (n + m)) {h: i.val < n . assumption}: fin (n)

#### Rob Lewis (Oct 02 2018 at 19:02):

(I think that's the right syntax, don't have Lean open right this second to check.)

#### Patrick Massot (Oct 02 2018 at 19:02):

binders in def fin_first {n m} (i : fin (n + m)) {h: i.val < n}: fin (n) are a bit strange, how h could be inferred from the explicit arguments?

#### Tobias Grosser (Oct 02 2018 at 19:03):

I have no idea what I am doing here.

#### Patrick Massot (Oct 02 2018 at 19:03):

Of course Rob's solution should work in your use case

#### Tobias Grosser (Oct 02 2018 at 19:03):

I hoped "{" and "}" would create a "free" argument

#### Tobias Grosser (Oct 02 2018 at 19:03):

Which would be filled in if available in the local context.

#### Tobias Grosser (Oct 02 2018 at 19:04):

Rob suggested to use "assumption", right?

#### Tobias Grosser (Oct 02 2018 at 19:04):

This gives:

test.lean:7:52: error

invalid declaration, '}' expected
test.lean:7:55: error

command expected


#### Tobias Grosser (Oct 02 2018 at 19:05):

Will ook for assumption in the lean doc

#### Rob Lewis (Oct 02 2018 at 19:05):

{ } creates implicit arguments. They're arguments that can be filled in completely from other arguments, basically. Lean won't automatically search your local context for matches, because (1) there could be tons of stuff in the context, and (2) there could be multiple matches there.

#### Tobias Grosser (Oct 02 2018 at 19:06):

I see. How do I tell lean which matches I want? Should I use ! to make the parameters explicit and then provide the ones needed explicitly?

#### Rob Lewis (Oct 02 2018 at 19:06):

Here's the correct syntax for using auto parameters like my suggestion:

def f (n : ℕ) (h : n > 1 . tactic.assumption) : true := trivial

example (n : ℕ) : true :=
if h : n > 1 then f n else trivial


#### Rob Lewis (Oct 02 2018 at 19:08):

With auto parameters, you give a tactic that will be executed to fill in that argument. So using tactic.assumption with an auto param will try to find something in the context that will work.

#### Rob Lewis (Oct 02 2018 at 19:10):

I see. How do I tell lean which matches I want? Should I use ! to make the parameters explicit and then provide the ones needed explicitly?

I'm not sure exactly what you mean. It's usually clear in a signature which arguments are inferrable from others, assuming the declaration is fully applied. The custom is to make as much implicit as you can.

#### Rob Lewis (Oct 02 2018 at 19:10):

There's no ! syntax anymore, that was only in Lean 2. But you can use placeholders _ to ask the elaborator to fill in explicit arguments.

Great.

#### Tobias Grosser (Oct 02 2018 at 19:13):

I got this working.

#### Tobias Grosser (Oct 02 2018 at 19:14):

I previously used "{}" around the assumption tactic, but I need to use "()"

#### Rob Lewis (Oct 02 2018 at 19:15):

Great! Sorry, I should have checked before I wrote it with {}, heh.

#### Tobias Grosser (Oct 02 2018 at 19:16):

These seem to be really basic questions, but I have now only a last issue.

#### Tobias Grosser (Oct 02 2018 at 19:16):

h_j : ¬j.val < n_left
⊢ j.val ≥ n_left

#### Tobias Grosser (Oct 02 2018 at 19:16):

Is what I see in the else branch.

#### Tobias Grosser (Oct 02 2018 at 19:16):

This seems to be an obvious rewrite.

#### Tobias Grosser (Oct 02 2018 at 19:16):

Unfortunately, I don't understand where I would even insert my tactic to do the rewrite.

#### Rob Lewis (Oct 02 2018 at 19:16):

le_of_not_gt

#### Patrick Massot (Oct 02 2018 at 19:17):

No you need a lemma here

Yes, that lemma

#### Rob Lewis (Oct 02 2018 at 19:17):

Are you using the auto param trick? Because I see that this might complicate things a bit.

#### Tobias Grosser (Oct 02 2018 at 19:19):

I currently write "up_right (fin_first i) (fin_second j (begin rw of_not_gt at h_j end))"

#### Tobias Grosser (Oct 02 2018 at 19:19):

up_right (fin_first i) (fin_second j (begin rw of_not_gt at h_j end))


#### Tobias Grosser (Oct 02 2018 at 19:20):

Which seems to not type-check even syntactically.

#### Tobias Grosser (Oct 02 2018 at 19:20):

I feel I mix proofs and normal programs beyond what is reasonable.

#### Tobias Grosser (Oct 02 2018 at 19:22):

Also, as a lemma I seem to need "ge_of_not_lt", but I can fix this.

#### Patrick Massot (Oct 02 2018 at 19:23):

meta def tobias : tactic unit :=
[apply le_of_not_gt,  assumption] <|>  [assumption]

def f (n : ℕ) (h : n ≤ 1 . tobias) : true := trivial

example (n : ℕ) : true :=
if h : ¬ n > 1 then f n else trivial

example (n : ℕ) : true :=
if h :  n ≤ 1 then f n else trivial


#### Rob Lewis (Oct 02 2018 at 19:24):

Haha, you beat me to it, I just wrote almost exactly the same thing.

#### Tobias Grosser (Oct 02 2018 at 19:25):

This is very much appreciated!

#### Tobias Grosser (Oct 02 2018 at 19:25):

The full family working on lean!

#### Tobias Grosser (Oct 02 2018 at 19:25):

What I understand is that I can only provide tactics at function definition, not at the call-site.

#### Rob Lewis (Oct 02 2018 at 19:26):

Oh, you can certainly provide them at the call site too.

#### Tobias Grosser (Oct 02 2018 at 19:26):

In this case, I could just change the hypothesis of fin_second to what I want.

#### Tobias Grosser (Oct 02 2018 at 19:26):

I tried to avoid this, as I felt the hypothesis that I stated is more canonical.

#### Tobias Grosser (Oct 02 2018 at 19:26):

Cool so how would I add them to the call site?

#### Patrick Massot (Oct 02 2018 at 19:27):

I meant my daughter tried to help Rob winning the race

#### Rob Lewis (Oct 02 2018 at 19:27):

If you make the inequality hypotheses to fin_first and fin_second explicit arguments, using (h : i.val < n), then you can apply it using fin_first i (by assumption).

#### Rob Lewis (Oct 02 2018 at 19:28):

Or by tobias in this case.

#### Patrick Massot (Oct 02 2018 at 19:30):

More seriously, the basics of implicit arguments goes like this: say you have a lemma (or function) with arguments (f : a -> b) (hf : continuous f). Then having hf forces the value of f, so you can mark f as implicit by changing the declaration to {f : a -> b} (hf : continuous f). This was you can provide only hf when applying the lemma and Lean will figure out f. In your case Lean had no hope to figure out h from other arguments so you need to keep it explicit, or use auto-param like in Rob's solution.

I see.

Got it.

#### Tobias Grosser (Oct 02 2018 at 19:33):

I can now successfully forward the hypothesis.

#### Tobias Grosser (Oct 02 2018 at 19:33):

Thanks again, I learned sth new.

#### Tobias Grosser (Oct 02 2018 at 19:34):

For completeness, this is how my code looks like:

import ring_theory.matrix

variables {α : Type} {n m : Type} [fintype n] [fintype m]

local infixl  *ₘ  : 70 := matrix.mul

def fin_first {n m} (i : fin (n + m)) (h : i.val < n ): fin (n) :=
⟨i.1, begin apply h end⟩

def fin_second {n m} (i : fin (n + m)) (h: i.val >= n): fin (m) :=
⟨i.1 - n, sorry⟩

def block_mx {m_down m_up n_left n_right: nat} :
matrix (fin m_up) (fin n_left) α →
matrix (fin m_up) (fin n_right) α →
matrix (fin m_down) (fin n_left) α →
matrix (fin m_down) (fin n_right) α →
matrix (fin (m_up + m_down)) (fin (n_left + n_right)) α
| up_left up_right down_left down_right :=
λ i j,
if h_i: i.val < m_up
then
if h_j: j.val < n_left
then
up_left (fin_first i (by assumption)) (fin_first j (by assumption))
else
up_right (fin_first i (by assumption)) (fin_second j (by apply le_of_not_gt; assumption))
else
if h_j: j.val < n_left
then
down_left (fin_second i (by apply le_of_not_gt; assumption))  (fin_first j (by assumption))
else
down_right (fin_second i (by apply le_of_not_gt; assumption)) (fin_second j (by apply le_of_not_gt; assumption))


#### Rob Lewis (Oct 02 2018 at 19:34):

It's not that common to use auto params, but this is actually a pretty good application. linarith would be a reasonable auto param too if it handled negations of inequalities.

#### Patrick Massot (Oct 02 2018 at 19:35):

I can feel the approximate SMT solver temptation here

:D

#### Patrick Massot (Oct 02 2018 at 19:35):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/linarith.20.26.20nat/near/134919571

#### Tobias Grosser (Oct 02 2018 at 19:35):

I certainly would like to explore more powerful linarithmetic tactics here. But this is a separate discussion.

#### Tobias Grosser (Oct 02 2018 at 19:36):

I know, we have a solver for full Presburger arithmetic based on dual simplex. Eventually, this is what I would like to understand if we can make it work in lean.

#### Rob Lewis (Oct 02 2018 at 20:19):

I can feel the approximate SMT solver temptation here

https://github.com/leanprover/mathlib/pull/384

#### Tobias Grosser (Oct 03 2018 at 07:55):

Amazing. This got even merged already. Will try to use it.

#### Tobias Grosser (Oct 03 2018 at 07:59):

I fact, i tried to use it already and it did not work. Thought I need to dig deeper, but then I found this in the tactic description: "In particular, it will not work on nat."

#### Tobias Grosser (Oct 03 2018 at 08:00):

Seems that's a problem in my case. Any reason why it would not work?

#### Rob Lewis (Oct 03 2018 at 08:59):

Oops, I guess the description is outdated. It will work on nat`, but it isn't complete (it's just doing Fourier Motzkin elimination). It also doesn't know about nat subtraction, which could be a problem in your case.

Last updated: May 13 2021 at 18:26 UTC