Zulip Chat Archive

Stream: new members

Topic: Function decreasing on n-th argument


view this post on Zulip Pedro Minicz (Jul 03 2020 at 23:54):

How do I tell Lean that a given function is decreasing on the n-th argument? shift.main is "obviously" decreasing on the third argument (term (D + G)).

import tactic.linarith

inductive term :   Type
| app {G : } (M N : term G) : term G
| lam {G : } (M : term (G + 1)) : term G
| var {G : } (x : fin G) : term G

open term

def shift.elem :  {G D : }, fin (G + D)  fin (G + D + 1)
| 0       D x          := x + 1
| (G + 1) D 0, h     := 0, nat.lt.step h
| (G + 1) D x + 1, h := shift.elem x, nat.lt_of_succ_lt h

def shift.main :  {G D : }, term (D + G)  term (D + G + 1)
| G D (app M N) := app (shift.main M) (shift.main N)
| G D (lam M)   := lam (shift.main M) -- Lean complains here.
| G D (var x)   := var (shift.elem x)

I suspect telling Lean that might not be enough, though, so for a second question: where can I read on well founded relations on Lean (and in general)?

view this post on Zulip Mario Carneiro (Jul 03 2020 at 23:56):

If this was a recursion on the third argument, it would not have D + G in the index

view this post on Zulip Marc Huisinga (Jul 03 2020 at 23:57):

tpil: https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#well-founded-recursion-and-induction
mathlib docs: https://leanprover-community.github.io/extras/well_founded_recursion.html

view this post on Zulip Mario Carneiro (Jul 03 2020 at 23:58):

Don't let well founded recursion errors fool you; that's just the fallback because the structural recursion compilation failed

view this post on Zulip Mario Carneiro (Jul 03 2020 at 23:58):

this should be a structural recursion

view this post on Zulip Pedro Minicz (Jul 04 2020 at 00:06):

Mario Carneiro said:

Don't let well founded recursion errors fool you; that's just the fallback because the structural recursion compilation failed

I see. That makes sense.

view this post on Zulip Pedro Minicz (Jul 04 2020 at 00:10):

Mario Carneiro said:

If this was a recursion on the third argument, it would not have D + G in the index

Yes! Indeed. Changing that fixed the issue.

view this post on Zulip Pedro Minicz (Jul 04 2020 at 01:25):

Why can't Lean see that M is structurally smaller than lam M. It may have something to do with the fact that lam M has type term Γ while M : term (Γ + 1).

import data.fin

@[derive decidable_eq]
inductive term :   Type
| app {Γ : } (M N : term Γ) : term Γ
| lam {Γ : } (M : term (Γ + 1)) : term Γ
| var {Γ : } (x : fin Γ) : term Γ

open term

def shift.main :  {Γ : }, fin (Γ + 1)  term Γ  term (Γ + 1)
| Γ σ (app M N) := app (shift.main σ M) (shift.main σ N)
| Γ σ (lam M)   := lam (@shift.main (Γ + 1) (σ + 1) M)
| Γ σ (var x)   := var $ if σ  x then x + 1 else x

abbreviation shift {Γ : } : term Γ  term (Γ + 1) := shift.main 0

def subst.main :  {Γ : }, fin (Γ + 1)  term Γ  term (Γ + 1)  term Γ
| Γ σ L (app M N) := app (subst.main σ L M) (subst.main σ L N)
| Γ σ L (lam M)   := lam (@subst.main (Γ + 1) (σ + 1) (shift L) M) -- This line.
| Γ σ L (var x)   := sorry

Last updated: May 13 2021 at 17:42 UTC