Using_well_founded

Stream: new members

[Guilherme Espada]

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.

[Guilherme Espada]

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: T→T): 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.

[Guilherme Espada]

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)⟩],
}

[Bryan Gin-ge Chen]

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

[Guilherme Espada]

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: T→T): 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.

[Guilherme Espada]

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

[Guilherme Espada]

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)