Zulip Chat Archive

Stream: new members

Topic: Deriving hypothesis from if statements


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:00):

I seem to be so close.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:01):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:03):

I have no idea what I am doing here.

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:03):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:03):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:03):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:04):

Rob suggested to use "assumption", right?

view this post on Zulip 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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:05):

Will ook for assumption in the lean doc

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:13):

Great.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:13):

I got this working.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:14):

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

view this post on Zulip Rob Lewis (Oct 02 2018 at 19:15):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:16):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:16):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:16):

Is what I see in the else branch.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:16):

This seems to be an obvious rewrite.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:16):

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

view this post on Zulip Rob Lewis (Oct 02 2018 at 19:16):

le_of_not_gt

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:17):

No you need a lemma here

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:17):

Yes, that lemma

view this post on Zulip 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.

view this post on Zulip 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))"

view this post on Zulip 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))

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:20):

Which seems to not type-check even syntactically.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:20):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Rob Lewis (Oct 02 2018 at 19:24):

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

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:24):

And my daughter tried to help you

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:25):

This is very much appreciated!

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:25):

The full family working on lean!

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 02 2018 at 19:26):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:26):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:26):

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

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:26):

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

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:27):

I meant my daughter tried to help Rob winning the race

view this post on Zulip 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).

view this post on Zulip Rob Lewis (Oct 02 2018 at 19:28):

Or by tobias in this case.

view this post on Zulip 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.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:33):

I see.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:33):

Got it.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:33):

I can now successfully forward the hypothesis.

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:33):

Thanks again, I learned sth new.

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:35):

I can feel the approximate SMT solver temptation here

view this post on Zulip Tobias Grosser (Oct 02 2018 at 19:35):

:D

view this post on Zulip Patrick Massot (Oct 02 2018 at 19:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 02 2018 at 20:19):

I can feel the approximate SMT solver temptation here

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

view this post on Zulip Tobias Grosser (Oct 03 2018 at 07:55):

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

view this post on Zulip 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."

view this post on Zulip Tobias Grosser (Oct 03 2018 at 08:00):

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

view this post on Zulip 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