Force evaluation of List.tail

Stream: new members

[Kevin Cheung]

For the following,

example : ∃ x, x = [3,4] := by
  let g := [2,3,4]
  let h := g.tail
  simp [g] at h
  refine Exists.intro h ?_
  sorry -- simp [h, g] closes the goal

the infoview right before sorry shows

1 goal
g : List Nat := [2, 3, 4]
h : List Nat := g.tail
⊢ h = [3, 4]

Is there a way to force evaluation of g.tail so that it shows h : List Nat := [3,4]?

[Kenny Lau]

@Kevin Cheung not exactly what you asked, but does this work?

example : ∃ x, x = [3,4] := by
  let g := [2,3,4]
  let h := g.tail
  simp [g] at h
  refine Exists.intro h ?_
  have : h = [3,4] := rfl
  sorry -- simp [h, g] closes the goal

[Kevin Cheung]

I need something that doesn't mention [3,4] explicitly because I need to do something like this programmatically in a larger context.

[Aaron Liu]

Why do you want to force evaluation like this?

[Kevin Cheung]

Because I need to tail part and then take the head in a proof. If it doesn't reduce, the head does not return an element.

[Aaron Liu]

Sorry, I don't really understand.

[Kenny Lau]

@Kevin Cheung generalize does what you want (but the equality is flipped):

import Mathlib

example : ∃ x, x = [3,4] := by
  generalize h₁ : [2,3,4] = l₁
  generalize h₂ : l₁.tail = l₂
  rw [← h₁, List.tail_cons] at h₂
  exact Exists.intro l₂ h₂.symm

[Kenny Lau]

it introduces a new variable with an equality as two separate lines in the infoview

[Kenny Lau]

but yeah this might be an XY problem (as Aaron is alluding to), you might find better solutions if you provide more context

[Aaron Liu]

Kevin Cheung said:

I need something that doesn't mention [3,4] explicitly because I need to do something like this programmatically in a larger context.

Well without any knowledge of the larger context I can't really help you.

[Kevin Cheung]

Here is the bigger context:

import Mathlib

def sumOfKPrimes (k n : ℕ) := ∃ primes : List ℕ, primes.all Nat.Prime ∧ primes.length = k ∧ primes.sum = n

def foo (f : List ℕ) :=
  match f with
  | List.nil => True
  | List.cons s f' => sumOfKPrimes 2 s ∧ (foo f')

example : foo [13, 18, 20] := by
  dsimp [foo]
  let g := [[2,11], [5,13], [3,17]]
  apply And.intro
  . use g.head (by simp)
    simp [g]
    decide
  . let g' := List.tail g
    have : g' ≠ [] := by aesop
    apply And.intro
    . use g'.head this
      simp [g', g]
      decide
    . let g'' := List.tail g'
      have : g'' ≠ [] := by aesop
      apply And.intro
      . use g''.head this
        simp [g'', g', g]
        decide
      . trivial

example : foo [13, 18, 20] := by
  simp [foo]
  constructorm* _ ∧ _
  . use [2, 11]; simp; decide
  . use [5, 13]; simp; decide
  . use [3, 17]; simp; decide

I need a way to handle a proof like this when the list has say 1000 items instead of 3. If there are better ways to do this, I would like to learn them.

[Aaron Liu]

So which part do you want to automate?

[Kenny Lau]

Kevin Cheung said:

I need a way to handle a proof like this when the list has say 1000 items instead of 3.

Forced evaluation wouldn't be a very good idea either, Lean is not a calculator :melt:

[Kevin Cheung]

Let's say I want to automate the use parts if I have a list of 1000 pairs that I know will work.

[Aaron Liu]

So you want to automatically find a pair that will work and insert it into the proof?

[Aaron Liu]

Or do you have the list of pairs on hand somewhere?

[Kevin Cheung]

Say the statement is foo xs where xs is a list of 1000 numbers. But I also already know ys a list of 1000 pairs of primes that for sure will work.

[Aaron Liu]

So you want to use ys as a witness to complete the proof?

[Kenny Lau]

@Kevin Cheung I would first write a function that can take the two lists and compute everything

[Kevin Cheung]

Basically, I want to construct a proof of foo xs from ys.

[Kenny Lau]

you don't want to copy that part of the code and paste 1000 times

[Kenny Lau]

(and please don't use a for loop to circumvent that)

[Kevin Cheung]

Kenny Lau said:

you don't want to copy that part of the code and paste 1000 times

I know I can just do this. But I hope that I don't need to.

[Aaron Liu]

This seems a lot like what is done with pi in file#Data/Real/Pi/Bounds

[Yakov Pechersky]

Can docs#List.foldr eliminate into Prop?

[Yakov Pechersky]

No :( because if it could, your foo is a fold over the list, and we have recursors for folds

[Kenny Lau]

@Kevin Cheung to demonstrate what I meant:

import Mathlib

def sumOfKPrimes (k n : ℕ) := ∃ primes : List ℕ, primes.all Nat.Prime ∧ primes.length = k ∧ primes.sum = n

def foo (f : List ℕ) :=
  match f with
  | List.nil => True
  | List.cons s f' => sumOfKPrimes 2 s ∧ (foo f')

theorem foo_of (target : List ℕ) (evidence : List (ℕ × ℕ)) (h1 : target.length = evidence.length)
    (h2 : ∀ i, (evidence.get i).1 + (evidence.get i).2 = target.get (Fin.cast h1.symm i)) : foo target :=
  sorry

example : foo [13, 18, 20] := by
  let g := [(2,11), (5,13), (3,17)]
  exact foo_of _ g rfl (by decide)

(there's probably a better way to do that)

[Aaron Liu]

Yakov Pechersky said:

Can docs#List.foldr eliminate into Prop?

Actually I see no reason why it couldn't

[Yakov Pechersky]

One could write an inline Tactic do that takes your list g and does a forM and calls the use tactic at each step

[Kenny Lau]

import Mathlib

def sumOfKPrimes (k n : ℕ) := ∃ primes : List ℕ, primes.all Nat.Prime ∧ primes.length = k ∧ primes.sum = n

def foo (f : List ℕ) :=
  match f with
  | List.nil => True
  | List.cons s f' => sumOfKPrimes 2 s ∧ (foo f')

inductive PartialDecide (α : Prop) : Type
  | decided (prf : α) : PartialDecide α
  | undecided : PartialDecide α

def PartialDecide.result {α : Prop} : PartialDecide α → Prop
  | decided _ => α
  | undecided => True

theorem PartialDecide.prf {α : Prop} : (h : PartialDecide α) → h.result
  | decided prf => prf
  | undecided => trivial

def foo_of : (target : List ℕ) → (evidence : List (ℕ × ℕ)) → PartialDecide (foo target)
  | [], [] => .decided trivial
  | [], (e :: et) => .undecided
  | (t :: tt), [] => .undecided
  | (t :: tt), (e :: et) => match foo_of tt et with
      | .decided ih => if h : e.1 + e.2 = t ∧ e.1.Prime ∧ e.2.Prime then
          .decided ⟨⟨[e.1, e.2], by simp [h]⟩, ih⟩ else .undecided
      | .undecided => .undecided

example : foo [13, 18, 20] :=
  (foo_of [13, 18, 20] [(2,11), (5,13), (3,17)]).prf

example : let tg := [13, 18, 20]; foo tg := by
  intro tg
  exact (foo_of tg [(2,11), (5,13), (3,17)]).prf

def List.repeat {α : Type*} (x : α) : ℕ → List α
  | 0 => []
  | (n+1) => x :: List.repeat x n

set_option trace.profiler true -- 3.89 sec
set_option maxRecDepth 100000 in
example : let tg := List.repeat 13 1000; foo tg := by
  intro tg
  exact (foo_of tg (List.repeat (2, 11) 1000)).prf

[Kenny Lau]

@Kevin Cheung this is the "better" code

[Kenny Lau]

it has a partial decision algorithm

[Kenny Lau]

comes at the cost that you would have to repeat the target twice... which could be circumvented if you make it a separate definition first
(edited: used let to avoid repeating it twice)

[Kevin Cheung]

Amazing. I can surely learn from these solutions. Thank you.

[Kenny Lau]

edit: stress tested the function for a list of length 1000, took 3.89 seconds