## Stream: new members

### Topic: Prove sizeof small

#### Bjørn Kjos-Hanssen (Oct 31 2020 at 23:06):

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 (Oct 31 2020 at 23:38):

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

#### Mario Carneiro (Oct 31 2020 at 23:38):

why do you want this theorem?

#### Mario Carneiro (Oct 31 2020 at 23:40):

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

#### Mario Carneiro (Oct 31 2020 at 23:41):

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

#### Mario Carneiro (Oct 31 2020 at 23:42):

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 (Oct 31 2020 at 23:48):

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 (Oct 31 2020 at 23:49):

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 (Nov 01 2020 at 00:59):

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

#### Bryan Gin-ge Chen (Nov 01 2020 at 01:03):

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 (Nov 01 2020 at 01:10):

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 (Nov 01 2020 at 01:13):

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 (Nov 01 2020 at 01:17):

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 (Nov 01 2020 at 01:17):

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 (Nov 01 2020 at 01:18):

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 (Nov 01 2020 at 01:20):

Let's try slim_check

#### Bjørn Kjos-Hanssen (Nov 01 2020 at 01:22):

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 (Nov 01 2020 at 01:28):

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 (Nov 01 2020 at 01:36):

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

#### Bryan Gin-ge Chen (Nov 01 2020 at 01:37):

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 (Nov 01 2020 at 01:42):

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 (Nov 01 2020 at 01:42):

ah, brian beat me

#### Bryan Gin-ge Chen (Nov 01 2020 at 01:42):

Ah, but your proof is much nicer.

#### Mario Carneiro (Nov 01 2020 at 01:49):

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 (Nov 01 2020 at 01:50):

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

#### Mario Carneiro (Nov 01 2020 at 01:50):

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 (Nov 01 2020 at 01:54):

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

#### Bjørn Kjos-Hanssen (Nov 01 2020 at 02:01):

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 (Nov 01 2020 at 02:03):

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

#### Mario Carneiro (Nov 01 2020 at 02:20):

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

#### Bjørn Kjos-Hanssen (Nov 01 2020 at 07:39):

Case closed. :briefcase:

Last updated: May 10 2021 at 19:16 UTC