JB

Stream: new members

[Jáchym Barvínek]

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]

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]

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

[Jáchym Barvínek]

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]

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]

• 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]

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

[Eric Wieser]

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]

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]

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]

import tactic

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

[Eric Wieser]

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

[Eric Wieser]

(import data.matrix.notation first)

[Jáchym Barvínek]

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]

by simp [fin.sum_univ_succ]

[Yakov Pechersky]

docs#fin.sum_univ_succ

[Yakov Pechersky]

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

[Jáchym Barvínek]

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]

Eric Wieser said:

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

woah thats really cool notation, thanks Eric!

[Jáchym Barvínek]

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]

You have the arguments to eval the wrong way around.

[Thomas Browning]

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

[Jáchym Barvínek]

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

[Jáchym Barvínek]

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]

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]

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]

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]

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

[Jáchym Barvínek]

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]

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,
  simp [fin.sum_univ_succ, add_comm 1 x],
end

[Jáchym Barvínek]

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]

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]

suggest might have been able to find fin.sum_univ_succ

[Jáchym Barvínek]

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]

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]

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

[Kevin Buzzard]

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

[Gabriel Ebner]

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]

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