Zulip Chat Archive

Stream: new members

Topic: Prove sizeof small


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 23:38):

why do you want this theorem?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 23:40):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bjørn Kjos-Hanssen (Nov 01 2020 at 00:59):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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 ['(','(',')']

view this post on Zulip Yakov Pechersky (Nov 01 2020 at 01:20):

Let's try slim_check

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Bjørn Kjos-Hanssen (Nov 01 2020 at 01:36):

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

view this post on Zulip 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)⟩]}

view this post on Zulip 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⟩] }

view this post on Zulip Mario Carneiro (Nov 01 2020 at 01:42):

ah, brian beat me

view this post on Zulip Bryan Gin-ge Chen (Nov 01 2020 at 01:42):

Ah, but your proof is much nicer.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Nov 01 2020 at 02:03):

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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 02:20):

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

view this post on Zulip Bjørn Kjos-Hanssen (Nov 01 2020 at 07:39):

Case closed. :briefcase:


Last updated: May 10 2021 at 19:16 UTC