## Stream: new members

### Topic: JB

#### Jáchym Barvínek (Apr 11 2021 at 12:11):

Hello, my name is Jáchym Barvínek. I am a PhD student from CTU in Prague. I am mainly doing research in logic-based AI. I have recently started learning LEAN (have played with other dependently typed systems before). I would be very happy if could look for help here with LEAN novice issues or perhaps have people criticize my code.

#### Scott Morrison (Apr 11 2021 at 12:16):

You've come to the right place! Feel free to post code snippets (try to make them a #mwe, please), or links to github branches/repos.

#### Scott Morrison (Apr 11 2021 at 12:16):

You may also be interested in the "Machine Learning for Theorem Proving" stream here.

#### Jáchym Barvínek (Apr 11 2021 at 12:33):

One thing I am currently working on concerns holonomic (a.k.a. P-recursive) sequences. I have tried to define them using lean. I think the following code mostly captures the idea, but I have no clue whether the code is "good" in terms of something that would be useful for working with in proofs. I would be happy if someone points me in a better direction :)

import data.polynomial

open finset
open polynomial
open vector

structure HolnomicSequence : Type :=
(order : ℕ)
(seq : ℕ → ℤ)
(initial_values : vector ℤ order)
(representing_polynomials : vector (polynomial ℤ) order)
(initial_values_cert : ∀ (i : fin order), (nth initial_values i = seq i) )
(recurrence : ∀ (i : ℕ) (i ≥ order),
let f (m : fin order) :=
(eval (nth representing_polynomials m) i) * seq (m - i),
indices : finset (fin order) :=
fintype.elems (fin order)
in
0 = indices.sum f
)


#### Mario Carneiro (Apr 11 2021 at 12:44):

It looks pretty good. I only have a few tips:

import data.polynomial
open finset polynomial vector
open_locale big_operators

structure HolonomicSequence : Type :=
(order : ℕ)
(seq : ℕ → ℤ)
(representing_polynomials : fin order → polynomial ℤ)
(recurrence (i ≥ order) :
∑ m : fin order, eval (representing_polynomials m) i * seq (m - i) = 0)


#### Mario Carneiro (Apr 11 2021 at 12:50):

• You should use fin n -> A for finite sequences instead of vector. There's a type alias for this but I forget the name
• Use finset.univ instead of fintype.elems A.
• fintype.univ.sum f has special notation ∑ a : A, f a, available through open_locale big_operators
• The initial_values field is unnecessary since it is uniquely determined by seq. Instead, prove an extensionality lemma saying that two holonomic sequences that agree on the first order values are equal, and an existence lemma saying that given values at the first order elements it is possible to fill in the rest using the recurrence.
• You should generally avoid lets in statements since they get in the way when proving theorems.
• ∀ (i ≥ order), expands to ∀ (i) (H : i ≥ order), so recurrence had two i binders in it.

#### Eric Wieser (Apr 11 2021 at 12:50):

This looks a bit like docs#linear_recurrence, which might have some API design you could copy

#### Eric Wieser (Apr 11 2021 at 12:53):

Should that be i - m instead of m - i? The latter is always 0 given that i ≥ order and m < order

#### Jáchym Barvínek (Apr 11 2021 at 17:46):

Mario Carneiro, thanks for the insight. Your solution looks much cleaner. I have one more nooby question: If I want to make and study a specific instance with, say order := 2, how do I actually construct a specific instance of fin 2 → whatever. Can I somehow pattern match on fin 2? So far, I was unable to figure out how to write that. I know this should be very basic.

#### Eric Rodriguez (Apr 11 2021 at 18:03):

def asd : fin 2 → ℕ
| ⟨0, _⟩ := 1
| ⟨1, _⟩ := 123
| ⟨n+2, h⟩ := -- this is a contradiction


The actual theorem name that shows that h is a contradiction is vanishing from my mind right now, but this is the main idea

#### Kevin Buzzard (Apr 11 2021 at 18:08):

import tactic

def asd : fin 2 → ℕ
| ⟨0, _⟩ := 1
| ⟨1, _⟩ := 123
| ⟨n+2, h⟩ := by linarith


#### Eric Wieser (Apr 11 2021 at 19:50):

def asd := ![1, 123] is easier

#### Eric Wieser (Apr 11 2021 at 19:50):

(import data.matrix.notation first)

#### Jáchym Barvínek (Apr 11 2021 at 20:47):

Thanks for the support guys. Where I could learn more about using the big operators? I am currently stuck at trying to prove the obvious thing that: ∀ (f : fin 2 → ℤ), ((∑ (x : fin 2), f) = f 0 + f 1)

#### Yakov Pechersky (Apr 11 2021 at 20:50):

by simp [fin.sum_univ_succ]

#### Yakov Pechersky (Apr 11 2021 at 20:50):

docs#fin.sum_univ_succ

#### Yakov Pechersky (Apr 11 2021 at 20:51):

Lemmas about sum are usually stated in term of prod, and are scattered across different files.

#### Jáchym Barvínek (Apr 11 2021 at 20:56):

Ah, I was just missing the argument x inside the summation and nothing seemed to work, including simp. But, explicitly using the simp [fin.sum_univ_succ] rule helped reveal that.

#### Eric Rodriguez (Apr 11 2021 at 21:52):

Eric Wieser said:

def asd := ![1, 123] is easier

woah thats really cool notation, thanks Eric!

#### Jáchym Barvínek (Apr 11 2021 at 22:14):

I am confused about the polynomials library. There is

/-- eval x p is the evaluation of the polynomial p at x -/
def eval : R → polynomial R → R := eval₂ (ring_hom.id _)
/-- monomial s a is the monomial a * X^s -/
def monomial (n : ℕ) : R →ₗ[R] polynomial R := finsupp.lsingle n


So according to the documentation, I would expect that: eval (monomial (2 : ℕ) (3 : ℤ)) (5 : ℤ) would corresponds to

$3x^2, x = 5$

which evaluates to 75. But instead lean tells me that:

example : eval (monomial (2 : ℕ) (3 : ℤ)) (5 : ℤ) = 5 := by simp;


I guess this must be somehow related to the ring_hom.id in definition of eval, which I do not I understand precisely, but it makes the result somehow live in the same space of polynomials over ℤ instead of ℤ, but that should not be a problem in itself if I can just prove it's constant and extract the value? So how do I get the "expected" behavior with eval₂? Do I need to construct a ring homomorphism from polynomials ℤ to ℤ or something?

#### Thomas Browning (Apr 11 2021 at 22:41):

You have the arguments to eval the wrong way around.

#### Thomas Browning (Apr 11 2021 at 22:42):

You are evaluating the constant polynomial 5 : polynomial (polynomial ℤ) at the polynomial monomial (2 : ℕ) (3 : ℤ)

#### Jáchym Barvínek (Apr 11 2021 at 22:48):

oh, wow, thanks, I feel kinda dumb now, but at the same impressed that this has passes the typecheck, haha.

#### Jáchym Barvínek (Apr 12 2021 at 08:58):

Still struggling working with the big operators. Using the simp [fin.sum_univ_succ] works only partially for me and I cannot understand why it's not possible to simplify some things in the sums, where I would expect rewrite to do the job, but it does not. Modified the above example based on your various tips:

import data.polynomial
import data.matrix.notation

open finset polynomial vector nat
open_locale big_operators

structure HolonomicSequence : Type :=
(order : ℕ)
(representing_polynomials : fin (order + 1) → polynomial ℤ)

-- Inspired by the API of linear_recurrence.is_solution
-- Does not consider initial sequence terms now (for simplicity)
def is_solution (A : HolonomicSequence) (seq : ℕ → ℤ) :=
∀ (i : ℕ), (i ≥ A.order) →
(∑ m : fin (A.order + 1),
eval ↑i (A.representing_polynomials m) * seq (i - m)
) = 0

/-- Representation of factorial as a holonomic sequence --/
noncomputable def factorial_rep : HolonomicSequence := {
order := 1,
representing_polynomials := ![monomial 0 (-1), monomial 1 1]
}

lemma factorial_holonomic : is_solution factorial_rep ↑factorial :=
begin
have ho : factorial_rep.order = 1 := by tauto,
intro i,
assume i_bound,
--rewrite ho, -- Attempt to rewrite factorial_rep.order inside goal.
-- But that doesn't work, why?
simp [fin.sum_univ_succ],
-- simp fails to expand the sum completely.
-- Apparently because fin (factorial_rep.order + 1) was unevaluated.
-- but how to evaluate that when rewrite can't do that?
sorry,
end


#### Kevin Buzzard (Apr 12 2021 at 09:11):

Does this help?

lemma factorial_holonomic : is_solution factorial_rep ↑factorial :=
begin
have ho : factorial_rep.order = 1 := by tauto,
intro i,
assume i_bound,
cases factorial_rep,
dsimp at *,
subst ho,
simp [fin.sum_univ_succ],
sorry,
end


You can't rewrite for several technical reasons. The first is that the rw tactic can't see under binders (like a sum). The second is that you have "motive is not type correct" issues -- the rewrite changes the type fin (order + 1) to fin 1 + 1 and then terms of that type get confused. This is a subtle issue and there are lots of solutions. The easiest way to get around it is the subst tactic, but this doesn't work either, immediately at least, because we need to take factorial_rep apart before we can get to the term we want to substitute.

#### Kevin Buzzard (Apr 12 2021 at 09:18):

PS actually here's a better approach. You have made this definition factorial_rep and I think the first thing to do is just to remove it -- this solves all your problems immediately. I also tidied up the polynomials -- you don't really want be working directly with monomials I don't think.

import data.polynomial
import data.matrix.notation

open finset polynomial vector nat
open_locale big_operators

structure HolonomicSequence : Type :=
(order : ℕ)
(representing_polynomials : fin (order + 1) → polynomial ℤ)

-- Inspired by the API of linear_recurrence.is_solution
-- Does not consider initial sequence terms now (for simplicity)
def is_solution (A : HolonomicSequence) (seq : ℕ → ℤ) :=
∀ (i : ℕ), (i ≥ A.order) →
(∑ m : fin (A.order + 1),
eval ↑i (A.representing_polynomials m) * seq (i - m)
) = 0

open polynomial
/-- Representation of factorial as a holonomic sequence --/
noncomputable def factorial_rep : HolonomicSequence := {
order := 1,
representing_polynomials := ![-1, X] -- much more readable
}

lemma factorial_holonomic : is_solution factorial_rep ↑factorial :=
begin
rw factorial_rep, -- remove this def ASAP and now it's fine
intro i,
dsimp at *, -- tidy up the mess left by the def
assume i_bound,
simp [fin.sum_univ_succ],
sorry,
end


#### Eric Wieser (Apr 12 2021 at 09:27):

Here's another way to state your condition that may or may not be better:

def is_solution (A : HolonomicSequence) (seq : ℕ → ℤ) :=
∀ (i : ℕ), (∑ m in finset.nat.antidiagonal A.order,
eval (A.order + ↑i) (A.representing_polynomials m.1) * seq (m.2 + i)
) = 0


#### Eric Wieser (Apr 12 2021 at 09:28):

Actually, that's probably akward due to the mixture of fin and nat

#### Jáchym Barvínek (Apr 12 2021 at 11:02):

OK, thanks all, I managed to complete the proof of the "obvious by definition for a human" fact, that factorial is holonomic. I am kinda proud of myself :D but also concerned how long the proof seems given the triviality of the problem. But I guess that may be inevitable in many cases with proof assistants?

lemma factorial_holonomic : is_solution factorial_rep ↑factorial :=
begin
rewrite factorial_rep,
intro i,
--dsimp at *, -- has aesthetic value, but technically not needed
assume i_bound,
simp [fin.sum_univ_succ],
let i_pred := i - 1,
have h_i_pred : i = succ i_pred :=
by refine pred_inj i_bound _ rfl; norm_num,
have factorial_rec : factorial i = i * factorial (i-1) :=
by rewrite h_i_pred; simp,
unfold_coes,
rewrite factorial_rec,
simp,
end


#### Eric Wieser (Apr 12 2021 at 11:18):

It becomes a lot easier if you avoid docs#lift_fn_range (which ↑factorial uses):

lemma factorial_holonomic : is_solution factorial_rep (λ x, factorial x) :=
begin
rewrite factorial_rep,
intro i i_bound,
obtain ⟨x, rfl⟩ := nat.exists_eq_add_of_le i_bound,
end


#### Jáchym Barvínek (Apr 12 2021 at 11:32):

That seems much more reasonable, Eric. Is there a simple way to search for the useful simplification rules (fin.sum_univ_succ, add_comm 1 x here)? I doubt that I would be able to find any of those in the library myself. Do we mostly have to rely on naming conventions and text search or is there any automation like with library_search or suggest?

#### Eric Wieser (Apr 12 2021 at 11:36):

I reached for add_comm because I had (1 + x).factorial but knew that the simp lemma was for x.succ.factorial = (x + 1).factorial

#### Eric Wieser (Apr 12 2021 at 11:36):

suggest might have been able to find fin.sum_univ_succ

#### Jáchym Barvínek (Apr 12 2021 at 12:46):

Inspired by your solution i managed to solve the coercion by a single unfold_coes even for the lifted case.

example : is_solution factorial_rep ↑factorial :=
begin
rewrite factorial_rep,
rintro _ i_bound,
obtain ⟨i_pred, h_i_pred⟩ := exists_eq_add_of_le i_bound,
unfold_coes,
simp [fin.sum_univ_succ, h_i_pred, add_comm 1 i_pred],
end


#### Jáchym Barvínek (Apr 14 2021 at 15:53):

I guess this should be a very common question, but still: What is the closest I get in LEAN to Isabelle's sledgehammer? I use suggest, hint and library_search for some automation, but often that's not much. Is there more? I understand it is difficult to reasonably run a resolution-based prover when using higher order logics, but perhaps it would be possible in some limited contexts?

#### Kevin Buzzard (Apr 14 2021 at 16:01):

The closest you get is @Gabriel Ebner's work on a hammer for Lean, which I think is waiting for Lean 4.

#### Kevin Buzzard (Apr 14 2021 at 16:02):

PS I am only tagging Gabriel because you have adopted a rather poor naming policy for your threads.

#### Gabriel Ebner (Apr 14 2021 at 16:05):

Yes, I hope to pick up the hammer again now that Lean 4 is out. There is a Lean 3 prototype, but it's way too slow to be useful.

#### Johan Commelin (Apr 14 2021 at 16:15):

@Jáchym Barvínek there's also tidy` which can be quite helpful at times.

Last updated: May 14 2021 at 21:11 UTC