Zulip Chat Archive

Stream: new members

Topic: Using_well_founded


view this post on Zulip Guilherme Espada (Mar 17 2021 at 15:07):

Given the following example:

import tactic.suggest
import data.finset
import data.finmap
import data.list
import data.finmap

@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype

open ttype

instance : inhabited ttype := inhabited.mk ty_bool

@[derive decidable_eq]
inductive term
|t_var (idx:int) : term
|t_abs (T:ttype) (t:term) : term
|t_app (t1 t2: term) : term
|t_true : term
|t_false : term
|t_if (cond l r: term): term

open term

instance : inhabited term := inhabited.mk t_true

def upshift_cutoff : int  int  term  term
| d c (t_var k) := t_var (if (k<c) then k else (k + d))
| d c (t_abs T t) := t_abs T $ upshift_cutoff d (c+1) t
| d c (t_app t1 t2) := t_app (upshift_cutoff d c t1) (upshift_cutoff d c t2)
| d c t_true := t_true
| d c t_false := t_false
| d c (t_if cond l r) := t_if (upshift_cutoff d c cond) (upshift_cutoff d c l) (upshift_cutoff d c r)

def upshift (amt:int) (t1:term): term := upshift_cutoff amt 0 t1

lemma sizeof_upshift_cutoff {d c t}: sizeof t = sizeof (upshift_cutoff d c t):=by sorry
lemma sizeof_upshift {amt t}: sizeof (upshift amt t) = sizeof t :=by sorry

def subst (replacement:term) : int  term  term
| idx (t_var n) := if n = idx then replacement else t_var n
| idx (t_abs T t) := t_abs T $ (subst (idx+1) (upshift 1 t))
| idx (t_app t1 t2) := t_app (subst idx t1) (subst idx t2)
| idx t_true := t_true
| idx t_false := t_false
| idx (t_if cond l r) := t_if (subst idx cond) (subst idx l) (subst idx r)
--using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (sizeof psigma.snd)⟩]}

I'm trying to indicate that the size of the third argument (the term) decreases. My attempt at using_well_founded is commented at the bottom.

Thanks.

view this post on Zulip Guilherme Espada (Mar 23 2021 at 11:37):

Eventually changing the definition slightly allowed the recursion without a manual well_founded.

However, in a slightly different version, I am getting this issue again:

import tactic.suggest
import tactic.linarith
import data.finset
import data.finmap
import data.list
import data.finmap
import tactic.slim_check

universe u

@[derive decidable_eq]
inductive recordmap (T : Type u)
| r_nil : recordmap
| r_cons (k:string) (v : T) (tl : recordmap) : recordmap

def map_vals {T: Type u} (fn: TT): recordmap T -> recordmap T
| recordmap.r_nil := recordmap.r_nil
| (recordmap.r_cons k v tl) := recordmap.r_cons k (fn v) (map_vals tl)

inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype
| ty_record (m: (recordmap ttype)): ttype

instance : decidable_eq ttype :=
begin
  sorry,
end

open ttype


instance : inhabited ttype := inhabited.mk ty_bool


inductive term
| t_var (idx:nat) : term
| t_abs (T:ttype) (t:term) : term
| t_app (t1 t2: term) : term
| t_true : term
| t_false : term
| t_if (cond l r: term): term
| t_record (vals: recordmap term): term
| t_projection (t: term) (l:string): term

instance : decidable_eq term :=
begin
  sorry,
end

open term

notation t1 `  ` t2 := t_app t1 t2
notation :` T `, ` t := t_abs T t



def is_value : term  Prop
| t_true := true
| t_false := true
| (t_abs _ _) := true
| _ := false


instance : inhabited term := inhabited.mk t_true

def upshift_cutoff : int  nat  term  term
| d c (t_var k) := t_var (if (k<c) then k else int.to_nat((k) + d))
| d c (t_abs T t) := t_abs T $ upshift_cutoff d (c+1) t
| d c (t_app t1 t2) := t_app (upshift_cutoff d c t1) (upshift_cutoff d c t2)
| d c t_true := t_true
| d c t_false := t_false
| d c (t_if cond l r) := t_if (upshift_cutoff d c cond) (upshift_cutoff d c l) (upshift_cutoff d c r)
| d c (t_record vals) := t_record (map_vals (upshift_cutoff d c) vals)
| d c (t_projection t l) := t_projection (upshift_cutoff d c t) l

In upshift_cutoff, the size of the third argument (term) always decreases, and as such, this recursion is well founded. I'm just not sure how to tell lean that.

view this post on Zulip Guilherme Espada (Mar 23 2021 at 18:09):

In case anyone else looks for this:

Assuming a def with 3 params, and you want to indicate that a property sizeof decreases on the third param, the correct invocation is the following:

using_well_founded {
  rel_tac := λ _ _, `[exact  _, measure_wf (λ  arg1, arg2, arg3 , sizeof arg3)⟩],
}

view this post on Zulip Bryan Gin-ge Chen (Mar 23 2021 at 18:19):

We could probably use some more examples like this on our well-founded doc page.

view this post on Zulip Guilherme Espada (Mar 24 2021 at 09:17):

In the following minimal example:

import data.finmap
import tactic.slim_check


universe u


abbreviation recordmap (T) := list (string × T)

abbreviation map_vals {T: Type u} (fn: TT): recordmap T -> recordmap T := list.map (λpair,(prod.fst pair, (fn $ prod.snd pair)))


inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype
| ty_record (m: (recordmap ttype)): ttype

instance : decidable_eq ttype :=
begin
  sorry,
end

open ttype

inductive term
| t_true : term
| t_record (vals: recordmap term): term

instance : decidable_eq term :=
begin
  sorry,
end

open term

def is_value : term  Prop
| t_true := true
| _ := false

def upshift_cutoff : int  nat  term  term
| d c t_true := t_true
| d c (t_record vals) :=
  -- What is the correct have statement here, to make this well founded?
  t_record (map_vals (λx, (upshift_cutoff d c x)) vals)

using_well_founded {
  rel_tac := λ _ _, `[exact  _, measure_wf (λ  d, c, t , sizeof t)⟩],
}

How can I prove the t_record case? I tried have (∀(x:term),((sizeof x) < (sizeof (t_record vals)))), from sorry,, but lean didn't accept it.

view this post on Zulip Guilherme Espada (Mar 24 2021 at 09:26):

I agree @Bryan Gin-ge Chen , I'm finding it somewhat difficult to figure all this out

view this post on Zulip Guilherme Espada (Mar 24 2021 at 11:17):

Figured it out: you have to put the have statement inside of the lambda, as such:

def upshift_cutoff : int  nat  term  term
| d c t_true := t_true
| d c (t_record vals) :=
  -- What is the correct have statement here, to make this well founded?
  t_record (map_vals (λx, (have (sizeof x) < (sizeof (t_record vals)), from sorry, upshift_cutoff d c x)) vals)

Last updated: May 10 2021 at 19:16 UTC