# Zulip Chat Archive

## Stream: new members

### Topic: Using_well_founded

#### 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.

#### 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: 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 (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)⟩],
}
```

#### 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.

#### 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: 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 (Mar 24 2021 at 09:26):

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

#### 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