Deriving hypothesis from if statements

Stream: new members

[Tobias Grosser]

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]

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]

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]

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]

I seem to be so close.

[Tobias Grosser]

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

[Patrick Massot]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Patrick Massot]

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]

I have no idea what I am doing here.

[Patrick Massot]

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

[Tobias Grosser]

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

[Tobias Grosser]

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

[Tobias Grosser]

Rob suggested to use "assumption", right?

[Tobias Grosser]

This gives:

test.lean:7:52: error

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

command expected

[Tobias Grosser]

Will ook for assumption in the lean doc

[Rob Lewis]

{ } 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]

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]

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]

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]

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]

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.

[Tobias Grosser]

Great.

[Tobias Grosser]

I got this working.

[Tobias Grosser]

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

[Rob Lewis]

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

[Tobias Grosser]

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

[Tobias Grosser]

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

[Tobias Grosser]

Is what I see in the else branch.

[Tobias Grosser]

This seems to be an obvious rewrite.

[Tobias Grosser]

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

[Rob Lewis]

le_of_not_gt

[Patrick Massot]

No you need a lemma here

[Patrick Massot]

Yes, that lemma

[Rob Lewis]

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

[Tobias Grosser]

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

[Tobias Grosser]

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

[Tobias Grosser]

Which seems to not type-check even syntactically.

[Tobias Grosser]

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

[Tobias Grosser]

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

[Patrick Massot]

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]

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

[Patrick Massot]

And my daughter tried to help you

[Tobias Grosser]

This is very much appreciated!

[Tobias Grosser]

The full family working on lean!

[Tobias Grosser]

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

[Rob Lewis]

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

[Tobias Grosser]

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

[Tobias Grosser]

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

[Tobias Grosser]

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

[Patrick Massot]

I meant my daughter tried to help Rob winning the race

[Rob Lewis]

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]

Or by tobias in this case.

[Patrick Massot]

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.

[Tobias Grosser]

I see.

[Tobias Grosser]

Got it.

[Tobias Grosser]

I can now successfully forward the hypothesis.

[Tobias Grosser]

Thanks again, I learned sth new.

[Tobias Grosser]

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]

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]

I can feel the approximate SMT solver temptation here

[Tobias Grosser]

:D

[Patrick Massot]

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

[Tobias Grosser]

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

[Tobias Grosser]

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]

I can feel the approximate SMT solver temptation here

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

[Tobias Grosser]

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

[Tobias Grosser]

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]

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

[Rob Lewis]

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.