Prove sizeof small

Stream: new members

[Bjørn Kjos-Hanssen]

I feel like the theorem below is "obvious" since a subinterval should have smaller sizeof, but how to prove?

  def excess_left_parens: list char → ℤ
-- excess_left_parens ['(','(',')'] = 1
 | [] := 0
 | (c::x) :=
    if c='(' then 1 + excess_left_parens x else
    if c=')' then -1 + excess_left_parens x else
    excess_left_parens x

def last_balanced_suffix : list char → list char
| [] := []
|(c::x) :=
if last_balanced_suffix x = [] then
    if excess_left_parens x = -1 then
        if c='(' then (append [c] x) else []
    else []
else (last_balanced_suffix x)

theorem maybe {x : list char}  : (last_balanced_suffix x).sizeof ≤ x.sizeof :=
by sorry

[Mario Carneiro]

You probably shouldn't be proving any theorems directly about sizeof, it's mostly an implementation detail

[Mario Carneiro]

why do you want this theorem?

[Mario Carneiro]

(append [c] x) could be written just c::x

[Mario Carneiro]

and it appears that you can prove that it is a suffix of the original list, list_balanced_suffix x <:+ x

[Mario Carneiro]

from which it follows that (list_balanced_suffix x).length <= x.length, which should be used in preference to a theorem about sizeof

[Bjørn Kjos-Hanssen]

Thanks @Mario Carneiro it seemed that the unproved goal in another definition required proving something about sizeof but I'll see what I can do with your hints

[Mario Carneiro]

Usually sizeof comes up when you want to write a recursive function and the automatic well founded recursion proof technique fails. In that case you should just replace the well founded metric with the right one for the definition, in this case something involving list.length

[Bjørn Kjos-Hanssen]

Now how do we tell Lean to use length instead of sizeof?

[Bryan Gin-ge Chen]

Can you share the other goal in the form of a #mwe ? This page on well-founded recursion on the community website might be useful.

[Yakov Pechersky]

Is this an equivalent defn?

def excess_left_parens: list char → ℤ
-- excess_left_parens ['(','(',')'] = 1
 | [] := 0
 | (c::x) :=
    if c='(' then 1 + excess_left_parens x else
    if c=')' then -1 + excess_left_parens x else
    excess_left_parens x

def last_balanced_suffix : list char → list char
| [] := []
| ('('::l) := ite (last_balanced_suffix l = [] ∧ excess_left_parens l = -1) ('(' :: l) []
| ( _ ::l) := last_balanced_suffix l

[Yakov Pechersky]

Oh that's too bad, that doesn't work because the eq compiler seems to freak out at the decidable equality of char

[Yakov Pechersky]

OK, this?

def excess_left_parens: list char → ℤ
-- excess_left_parens ['(','(',')'] = 1
 | [] := 0
 | (c::x) :=
    excess_left_parens x + ite (c = '(') 1 (ite (c = ')') (-1) 0)

def last_balanced_suffix : list char → list char
| [] := []
| (c::l) := ite (last_balanced_suffix l = [])
  (ite (c = '(' ∧ excess_left_parens l = -1) ('('::l) [])
  (last_balanced_suffix l)

[Bjørn Kjos-Hanssen]

Here's a minimal example that doesn't work (although it is so minimal that it no longer tries to do anything useful).

def last_balanced_suffix : list char → list char
| [] := []
|(c::x) := []

def truth_value : list char → ℕ → ℕ
|   [] n := 0
|   (c::x) n := (truth_value (last_balanced_suffix x) 0)

[Yakov Pechersky]

def excess_left_parens: list char → ℤ
-- excess_left_parens ['(','(',')'] = 1
 | [] := 0
 | (c::x) :=
    excess_left_parens x + ite (c = '(') 1 (ite (c = ')') (-1) 0)

def last_balanced_suffix : list char → list char
| [] := []
| (c::l) := ite (last_balanced_suffix l = [])
  (ite (c = '(' ∧ excess_left_parens l = -1) ('('::l) [])
  (last_balanced_suffix l)

/-
1
-/

#eval excess_left_parens ['(','(',')']
/-
['(', ')']
-/

#eval last_balanced_suffix ['(','(',')']

[Yakov Pechersky]

Let's try slim_check

[Bjørn Kjos-Hanssen]

Yes @Yakov Pechersky that has the desired behavior. The problem is when I then add say

def truth_value : list char → ℕ → ℕ
|   [] n := 0
|   (c::x) n := (truth_value (last_balanced_suffix x) 0)

[Yakov Pechersky]

I'm not particularly good at solving those sorts of well-foundedness problems. Seems like your minimal example is a bit removed from what you're trying to do -- so maybe we can fix the actual issue? Otherwise, I'm not sure what to do about this failing example.

[Bjørn Kjos-Hanssen]

OK I'll make a minimal but still purposeful example...

[Bryan Gin-ge Chen]

I managed to solve it, following the last bit of the well-foundedness tutorial I linked above:

import tactic

def excess_left_parens: list char → ℤ
-- excess_left_parens ['(','(',')'] = 1
 | [] := 0
 | (c::x) :=
    excess_left_parens x + ite (c = '(') 1 (ite (c = ')') (-1) 0)

def last_balanced_suffix : list char → list char
| [] := []
| (c::l) := ite (last_balanced_suffix l = [])
  (ite (c = '(' ∧ excess_left_parens l = -1) ('('::l) [])
  (last_balanced_suffix l)

def truth_value : list char → ℕ → ℕ
|   [] n := 0
|   (c::x) n :=
  have (last_balanced_suffix x).length < x.length + 1 :=
  begin
    induction x with c' x' hx',
    { simp [last_balanced_suffix, nat.zero_lt_one], },
    { simp [last_balanced_suffix], split_ifs,
      { simp, },
      { simp, },
      { calc _ < _ : hx'
        ... < _ : lt_add_one _, } }
  end,
  (truth_value (last_balanced_suffix x) 0)
  -- I copied this from the last part of the well-foundedness doc
  -- except that I replaced `card` with a type using `length`
  using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, list.length x.1)⟩]}

[Mario Carneiro]

import data.list.basic

  def excess_left_parens: list char → ℤ
-- excess_left_parens ['(','(',')'] = 1
 | [] := 0
 | (c::x) :=
    if c='(' then 1 + excess_left_parens x else
    if c=')' then -1 + excess_left_parens x else
    excess_left_parens x

def last_balanced_suffix : list char → list char
| [] := []
| (c::x) :=
  if last_balanced_suffix x = [] then
    if excess_left_parens x = -1 ∧ c = '(' then c :: x else []
  else last_balanced_suffix x

theorem last_balanced_suffix_is_suffix : ∀ l, last_balanced_suffix l <:+ l
| [] := list.nil_suffix _
| (c::x) := begin
  rw last_balanced_suffix, split_ifs,
  { refl },
  { apply list.nil_suffix },
  { exact (last_balanced_suffix_is_suffix x).trans (list.suffix_cons _ _) }
end

def truth_value : list char → ℕ → ℕ
| [] := λ n, 0
| (c::x) := λ n,
  have (last_balanced_suffix x).length < (c::x).length, from
    nat.lt_succ_of_le $ list.length_le_of_infix $
    list.infix_of_suffix $ last_balanced_suffix_is_suffix _,
  truth_value (last_balanced_suffix x) 0
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf list.length⟩] }

[Mario Carneiro]

ah, brian beat me

[Bryan Gin-ge Chen]

Ah, but your proof is much nicer.

[Mario Carneiro]

Hey, it just occurred to me that we could improve the ergonomics of that using_well_founded bit using something like

using_well_founded by wf on list.length

[Mario Carneiro]

There are a bunch of messy arguments in using_well_founded that we could paper over with a custom tactic parser

[Mario Carneiro]

For example rel_tac takes two arguments that I have never ever used because I only ever want to use exact

[Bryan Gin-ge Chen]

Ooh, that'd be great. Then we could change the error message in core Lean to mention wf.

[Bjørn Kjos-Hanssen]

Thanks a lot, I almost have my version working except for this

type mismatch at application
  measure_wf list.length
term
  list.length
has type
  list ?m_1 → ℕ : Type ?
but is expected to have type
  (Σ' (a : list char), ℕ) → ℕ : Type

[Bryan Gin-ge Chen]

Try replacing measure_wf list.length with measure_wf (λ x, list.length x.1).

[Mario Carneiro]

Or do induction only on the first argument by using lambda for the second

[Bjørn Kjos-Hanssen]

Case closed. :briefcase: