Showing mutually inductive recursion is well founded

Stream: new members

[Julian Sutherland]

I'm trying to show that a group of mutually inductive functions over a set of mutually inductive type families is well founded.

To do so, I need to project to the last argument of each function and then "tell" lean to consider the well founded relation induced by the structure of the mutually inductive type families. I cannot however move this argument earlier in the list of the functions arguments as it type depends on all previous arguments.

I run into the same issue if I try and define some function that simply computes the "depth" of the mutually inductive term (so as to create a map to ℕ). Is there anyway to simply "tell" lean to only consider this last argument when trying to prove the recursion is well-founded?

[Huỳnh Trần Khanh]

oh? :eyes: you might want to take a look at the merge_sort implementation https://github.com/leanprover-community/mathlib/blob/master/src/data/list/sort.lean#L257

[Huỳnh Trần Khanh]

:joy: if you need more assistance please tell us

[Julian Sutherland]

Thank you! Unfortunately, inv_image.wf doesn't work for my use case as the function, f : α → β,projecting to the well-founded type does not allow the the output type, β, to depend on the input type, α.

Unfortunately, I need this for my case, as in all cases, the type of the last element I want to project to depends on all other previous arguments to the function.

[Huỳnh Trần Khanh]

@Julian Sutherland then give us a #mwe, quick :joy: I'm here to help, and it's very likely that the problem isn't as hard as you think it is

[Julian Sutherland]

Thank you! I'm on it :)

[Julian Sutherland]

I think the simplest possible example that I can concoct that exhibits this behaviour is:

mutual inductive C, C'
with C : ℕ → Type
| C1 : ∀ n : ℕ, C' (n + 1) → C n
| C2 : ∀ n : ℕ, C n
with C' : ℕ -> Type
| C1' : ∀ n : ℕ, C (n + 1) → C' n

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ (C.C1 _ c') := 1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ (C'.C1' _ c) := c_depth c

So clearly there is a well-founded relation induced by the inductive structure of the mutually inductive type families C and C'. Therefore, since all recursive calls occur on some inductive subterm of one of these in the c_depth and c'_depth functions, these mutually recursive functions are well-founded. However, lean first considers the earlier argument to the two functions (the naturals parametrising the C and C' type families) and see that they increase and therefore is unable to show that this recursion is well-founded:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n))
    (@has_well_founded_of_has_sizeof (psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n))
       (@psum.has_sizeof_alt (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n)
          (@psigma.has_sizeof ℕ (λ {n : ℕ}, C n) nat.has_sizeof (λ (a : ℕ), C.has_sizeof_inst a))
          (@psigma.has_sizeof ℕ (λ {n : ℕ}, C' n) nat.has_sizeof (λ (a : ℕ), C'.has_sizeof_inst a))))
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
default_dec_tac failed
state:
_x : ℕ,
c' : C' (_x + 1)
⊢ 1 + (_x + 1) + C'.sizeof (_x + 1) c' < 1 + _x + (1 + _x + C'.sizeof (_x + 1) c')

These arguments cannot be moved as the two type families depend on them.

[Julian Sutherland]

Interestingly, when considering a similar example with only a single type family rather than two mutually recursive ones, this is not a problem and lean seems to be able to automatically realise that it need only consider the last argument when showing a recursive function is well-founded.

[Mario Carneiro]

You should consider using an inductive family rather than a mutual inductive. The kernel supports the former directly, so you won't need to resort to well founded recursion as much

[Julian Sutherland]

While possible, this would introduce a huge amount of overhead... My actual use case has a large number of mutually inductive type families with different numbers of arguments. Doing so would require a large number of "dummy" arguments and predicates to restrict inductive references to the appropriate "subtypes" corresponding to each previous mutually inductive type.

Is there no alternative using these mutually inductive type families directly?

[Mario Carneiro]

I don't think it should; you need an inductive type to describe the index type of the main inductive, but I have done this sort of thing "at scale" before and it works alright

[Kyle Miller]

I've never seen this error before:

inductive C_type | type_C | type_C'
open C_type

inductive C_mut : C_type → ℕ → Type
| C1 : ∀ n : ℕ, C_mut type_C' (n + 1) → C_mut type_C n
| C2 : ∀ n : ℕ, C_mut type_C n
| C1' : ∀ n : ℕ, C_mut type_C (n + 1) → C_mut type_C' n

def c_depth : ∀ {n : ℕ} {t : C_type}, C_mut t n → ℕ
| _ t (C_mut.C1 _ c') := 1 + c_depth c'
| _ t (C_mut.C2 _) := 0
| _ t (C_mut.C1' _ c) := c_depth c

/-
equation compiler failed to prove equation lemma (workaround: disable lemma
generation using `set_option eqn_compiler.lemmas false`)
-/

I removed these pattern definitions just to check they weren't the cause:

@[pattern] def C.C1 (n : ℕ) : C' (n + 1) → C n := C_mut.C1 n
@[pattern] def C.C2 (n : ℕ) : C n := C_mut.C2 n
@[pattern] def C'.C1' (n : ℕ) : C (n + 1) → C' n := C_mut.C1' n

def c_depth : ∀ {n : ℕ} {t : C_type}, C_mut t n → ℕ
| _ _ (C.C1 _ c') := 1 + c_depth c'
| _ _ (C.C2 _) := 0
| _ _ (C'.C1' _ c) := c_depth c

[Mario Carneiro]

I think you want this on your example, although there is still some work to do to prove the calls decrease:

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ (C.C1 _ c') := 1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ (C'.C1' _ c) := c_depth c
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf
    (λ p, psum.cases_on p (λ p, C.sizeof _ p.2) (λ p, C'.sizeof _ p.2))⟩],
  dec_tac := `[assumption] }

[Mario Carneiro]

Here's an example using a plain inductive:

inductive C_kind
| C : ℕ → C_kind
| C' : ℕ → C_kind

inductive CC : C_kind → Type
| C1 : ∀ n : ℕ, CC (C_kind.C' (n + 1)) → CC (C_kind.C n)
| C2 : ∀ n : ℕ, CC (C_kind.C n)
| C1' : ∀ n : ℕ, CC (C_kind.C (n + 1)) → CC (C_kind.C' n)

def cc_depth : ∀ {k}, CC k → ℕ
| _ (CC.C1 _ c') := 1 + cc_depth c'
| _ (CC.C2 _) := 0
| _ (CC.C1' _ c) := cc_depth c

[Julian Sutherland]

Thank you! I'll first try and see if I can expand your partial solution for the mutually inductive types into a solution that works for my use case, and, if not, I can use the parametric solution as a backup! :) (But tomorrow, it's past 2am here!)

[Kyle Miller]

@Mario Carneiro Do you have any idea why in yours works but mine doesn't?

[Mario Carneiro]

you have n and t in reversed order relative to their occurrence in C_mut, this seems to trip lean up

[Kyle Miller]

Ah, thanks

[Julian Sutherland]

I couldn't resist trying a little more and started setting things up to prove the well-foundedness of the recursion in this toy example:

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| p := psum.cases_on p (λ p, C.sizeof _ p.2) (λ p, C'.sizeof _ p.2)

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ c@(C.C1 n c') :=
  have metric (psum.inl $ psigma.mk n c) > metric (psum.inr $ psigma.mk (n+1) c'),
  from
    begin
      rw metric,
      rw psum.cases_on,
      sorry,
    end,
  1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ c'@(C'.C1' n c) :=
  have metric (psum.inr $ psigma.mk n c') > metric (psum.inl $ psigma.mk (n+1) c),
  from
    begin
      sorry
    end,
  c_depth c
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf metric⟩],
  dec_tac := `[assumption] }

When I attempt to rewrite psum.cases_on with its definition, I get an error:

rewrite tactic failed, lemma is not an equality nor a iff

[Huỳnh Trần Khanh]

oops... yeah ofc cases_on is like... a constant, an axiom so ofc there's no "definition"

[Huỳnh Trần Khanh]

just go to bed already, staying up late harms your cognitive abilities and makes you even worse at lean

[Julian Sutherland]

You're probably right! I'm about to do so, but for tomorrow morning: is there anyway that I can then evaluate (given that I know, for the proof in c_depth, that the value of the psum uses the psum.inl constructor) the psum.cases_on application to the left case (the application of C.sizeof)?

Will I then have similar issues with showing C.sizeof (C.C1 n c') > C'.sizeof c'?

[Mario Carneiro]

If you are going to make a definition for it, you may as well not use psum.cases_on and write it using the equation compiler instead

[Julian Sutherland]

I won't be able to do so with C.sizeof and C'.sizeof however, as defining these functions "manually" would run into the same issue I'm stuck with. Is there any way around this?

[Mario Carneiro]

you don't need to define C.sizeof, it is defined by the mutual induction simulation framework

[Mario Carneiro]

but if that isn't sufficient, you either have to use the underlying _nest inductive that lean generates (which is equivalent to the inductive I wrote but much uglier), or do the simulation yourself

[Mario Carneiro]

I believe the proof of C.sizeof (C.C1 n c') > C'.sizeof c' is that the lhs is defeq to 1 + sizeof n + C'.sizeof c' and then there is some linear arithmetic

[Mario Carneiro]

In your code snippet, you can replace rw psum.cases_on with dsimp only

[Julian Sutherland]

Yes, you're absolute right, I was concerned I would hit upon the same error when attempting to do a rewrite using the definitions of C.sizeof and C'.sizeof.

Having replaced the psum.cases_of with an explicit match:

mutual inductive C, C'
with C : ℕ → Type
| C1 : ∀ n : ℕ, C' (n + 1) → C n
| C2 : ∀ n : ℕ, C n
with C' : ℕ -> Type
| C1' : ∀ n : ℕ, C (n + 1) → C' n

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| p := match p with
         | (psum.inl p) := C.sizeof _ p.2
         | (psum.inr p) := C'.sizeof _ p.2
      end

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ c@(C.C1 n c') :=
  have metric (psum.inl $ psigma.mk n c) > metric (psum.inr $ psigma.mk (n+1) c'),
  from
    begin
      rw metric,
      rw metric._match_1,
      rw psigma.fst,
      sorry,
    end,
  1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ c'@(C'.C1' n c) :=
  have metric (psum.inr $ psigma.mk n c') > metric (psum.inl $ psigma.mk (n+1) c),
  from
    begin
      sorry
    end,
  c_depth c
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf metric⟩],
  dec_tac := `[assumption] }

[Mario Carneiro]

I was thinking more like

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| (psum.inl p) := C.sizeof _ p.2
| (psum.inr p) := C'.sizeof _ p.2

or

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| (psum.inl ⟨_, c⟩) := C.sizeof _ c
| (psum.inr ⟨_, c⟩) := C'.sizeof _ c

[Mario Carneiro]

But it doesn't really matter, you can just have C'.sizeof _ c' < C.sizeof _ c, instead of have metric (psum.inl $ psigma.mk n c) > metric (psum.inr $ psigma.mk (n+1) c'), and assumption will handle the unfolding

[Mario Carneiro]

after a bit of optimization, here's a version that works:

import tactic.linarith

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ c@(C.C1 n c') :=
  have sizeof c' < C.sizeof _ c, by { rw C.sizeof, linarith },
  1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ c'@(C'.C1' n c) :=
  have sizeof c < C'.sizeof _ c', by { rw C'.sizeof, linarith },
  c_depth c
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf metric⟩],
  dec_tac := `[assumption] }

[Julian Sutherland]

Thank you very much! I'll try and decipher it fully in the morning.

I did notice however that it seems that the default definition of C.sizeof n (C.C1 n c') is 1 + sizeof n + sizeof c', which would seem problematic, but clearly not as you have a working solution! :)

[Mario Carneiro]

What's problematic about it?

[Mario Carneiro]

There is a slight inconvenience that it ends with sizeof c' instead of C'.sizeof _ c' but sizeof is a typeclass function and with the typeclass argument it unfolds to the same thing in the end

[Julian Sutherland]

Sorry, ignored me, I'm exhausted! Shouldn't be working on lean in this state! You're completely right!

[Julian Sutherland]

Still can't sleep, however, I managed to successfully apply this methodology to my use case! Thank you all for your help!

But I have a further problem, I have to nest one of my types within a function passed as an argument to one of my other types' constructors. In this case the default associated sizeof does not consider the size of the types "nested" within the codomain of this function. If I need to recurse over the elements in this codomain, the metric induced by sizeof does not work.

Here is my #mwe:

mutual inductive C, C'
with C : ℕ → Type
| C1 : ∀ n : ℕ, C' (n + 1) → C n
| C2 : ∀ n : ℕ, C n
with C' : ℕ -> Type
| C1' : ∀ n : ℕ, (fin n → C (n + 1)) → C' n

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| (psum.inl ⟨_, c⟩) := C.sizeof _ c
| (psum.inr ⟨_, C'.C1' n f⟩) := 1 + (list.foldl max 0
    (list.map (λ i : fin n, C.sizeof (n+1) (f i)) (list.fin_range n)))

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ c@(C.C1 n c') :=
  have metric (psum.inr ⟨n+1, c'⟩) < metric (psum.inl ⟨n, c⟩),
  by {
    rw metric,
    cases c',
    rw metric,
    sorry
  },
  1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ c'@(C'.C1' n f) :=
  list.foldl max 0 (list.map (λ i : fin n,
    have metric (psum.inl ⟨n + 1, f i⟩) < metric (psum.inr ⟨n, c'⟩), by { sorry },
    c_depth (f i)) (list.fin_range n))
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf metric⟩],
  dec_tac := `[assumption] }

I have changed the definition of the metric to find the maximal depth of any of the elements nested with the function. However, when I try to write the proof that my metric decreases for the cases of my function, if I try and run the tactic rw metric when the input is some element of C', the rewrite fails with the error message failed. Any ideas why this is?

[Julian Sutherland]

Actually, sorry, the metric function here is not actually what I want, it should be:

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| (psum.inl ⟨_, C.C1 n c'⟩) := 1 + (metric (psum.inr ⟨n+1, c'⟩))
| (psum.inl ⟨_, C.C2 n⟩) := 0
| (psum.inr ⟨_, C'.C1' n f⟩) := 1 + (list.foldl max 0
    (list.map (λ i : fin n, metric (psum.inl ⟨n+1,f i⟩)) (list.fin_range n)))

Which seems to prevent me from using the automatically generated sizeof to solve my bootstrapping problem...

[Huỳnh Trần Khanh]

tip: if rw says failed, that usually means that the equation compiler generated equations that are different from what you expect. to see the generated equations, type #print prefix metric on an empty line

[Julian Sutherland]

Thank you for the hint! However, I still have the deeper problem that the metric function itself now suffers from the same problem I was trying to solve...

[Kyle Miller]

The problem was that this is thing you were trying to rewrite

metric (psum.inr ⟨n + 1, C'.C1' (n.add 0).succ c'_ᾰ⟩)

but rewriting using the equation lemma involves looking for something of this form:

metric (psum.inr ⟨n, C'.C1' n f⟩)

This ends up being a way to fix the rewrite:

change metric (psum.inr ⟨n + 1, C'.C1' (n + 1) _⟩) < _,
rw metric,

[Julian Sutherland]

Thank you! I figured out a way of fixing this by massaging the definition of metric as in my second to last post :)

[Mario Carneiro]

The definition of C.sizeof in the presence of functions does not have the right behavior:

#print C._mut_.sizeof

@[irreducible]
protected def C._mut_.sizeof : Π (a : psum (Σ' (ᾰ : ℕ), unit) (Σ' (ᾰ : ℕ), unit)), C._mut_ a → ℕ :=
λ (a : psum (Σ' (ᾰ : ℕ), unit) (Σ' (ᾰ : ℕ), unit)),
  C._mut_.rec
    (λ (n : ℕ)
     (ᾰ : C._mut_ ((λ (idx : Σ' (ᾰ : ℕ), unit), psum.inr idx) ((λ (ᾰ : ℕ), ⟨ᾰ, ()⟩) (n + 1))))
     (ih : ℕ), 1 + sizeof n + ih)
    (λ (n : ℕ), 1 + sizeof n)
    (λ (n : ℕ)
     (ᾰ :
       fin n → C._mut_ ((λ (idx : Σ' (ᾰ : ℕ), unit), psum.inl idx) ((λ (ᾰ : ℕ), ⟨ᾰ, ()⟩) (n + 1))))
     (ih : fin n → ℕ), 1 + sizeof n)

This says that C'.sizeof (C'.C1 n f) = 1 + sizeof n without taking f into account.

[Mario Carneiro]

I really think you should turn back at this point, because this means that every definition you make on this mutual inductive will have this issue

[Julian Sutherland]

I'm aware :) Hence my new definition of metric that does not use sizeof. However this definition suffers from the same problem I started off with... I guess there is no way to get around this?

[Mario Carneiro]

Well, you can do induction on C._mut_...

[Julian Sutherland]

I'm going to have to figure out what that is first! :D

[Huỳnh Trần Khanh]

no but really, don't touch mutual inductives even with a 10ft pole! they're a can of worms :bug: what stops you from using an index parameter? I don't think using an index parameter would cause problems, I've done this before, you don't need dummy parameters or anything I swear

[Mario Carneiro]

which looks like this

def metric' : ∀ {a}, C._mut_ a → ℕ
| _ (C._mut_.C1_0 n c') := 1 + metric' c'
| _ (C._mut_.C2_0 n) := 0
| _ (C._mut_.C1'_1 n f) := 1 + (list.foldl max 0
    (list.map (λ i : fin n, metric' (f i)) (list.fin_range n)))

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| (psum.inl ⟨_, c⟩) := metric' c
| (psum.inr ⟨_, c⟩) := metric' c

[Mario Carneiro]

but at this point you may as well use the plain inductive, which is basically the same thing as this but without lean playing middleman (poorly)

[Julian Sutherland]

I believe you! I'm open to transitioning to this solution, but I'm curious to see if it is possible out of intellectual curiosity :) Clearly it couldn't hurt me to learn more lean! :D

[Mario Carneiro]

That is to say, this inductive that lean generates:

mutual inductive C, C'
with C : ℕ → Type
| C1 : ∀ n : ℕ, C' (n + 1) → C n
| C2 : ∀ n : ℕ, C n
with C' : ℕ -> Type
| C1' : ∀ n : ℕ, (fin n → C (n + 1)) → C' n

#print C._mut_

inductive C._mut_ : psum (Σ' (ᾰ : ℕ), unit) (Σ' (ᾰ : ℕ), unit) → Type
constructors:
C._mut_.C1_0 : Π (n : ℕ),
  C._mut_ ((λ (idx : Σ' (ᾰ : ℕ), unit), psum.inr idx) ((λ (ᾰ : ℕ), ⟨ᾰ, ()⟩) (n + 1))) →
  C._mut_ ((λ (idx : Σ' (ᾰ : ℕ), unit), psum.inl idx) ((λ (ᾰ : ℕ), ⟨ᾰ, ()⟩) n))
C._mut_.C2_0 : Π (n : ℕ), C._mut_ ((λ (idx : Σ' (ᾰ : ℕ), unit), psum.inl idx) ((λ (ᾰ : ℕ), ⟨ᾰ, ()⟩) n))
C._mut_.C1'_1 : Π (n : ℕ),
  (fin n → C._mut_ ((λ (idx : Σ' (ᾰ : ℕ), unit), psum.inl idx) ((λ (ᾰ : ℕ), ⟨ᾰ, ()⟩) (n + 1)))) →
  C._mut_ ((λ (idx : Σ' (ᾰ : ℕ), unit), psum.inr idx) ((λ (ᾰ : ℕ), ⟨ᾰ, ()⟩) n))

is essentially the same as the CC inductive from my earlier message.

[Julian Sutherland]

Thank you very much for the help, my first partial attempt:

import tactic.linarith

mutual inductive C, C'
with C : ℕ → Type
| C1 : ∀ n : ℕ, C' (n + 1) → C n
| C2 : ∀ n : ℕ, C n
with C' : ℕ -> Type
| C1' : ∀ n : ℕ, (fin n → C (n + 1)) → C' n

def metric' : ∀ {a}, C._mut_ a → ℕ
| _ (C._mut_.C1_0 n c') := 1 + metric' c'
| _ (C._mut_.C2_0 n) := 0
| _ (C._mut_.C1'_1 n f) := 1 + (list.foldl max 0
    (list.map (λ i : fin n, metric' (f i)) (list.fin_range n)))

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| (psum.inl ⟨_, c⟩) := metric' c
| (psum.inr ⟨_, c⟩) := metric' c

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ c@(C.C1 n c') :=
  have metric (psum.inr ⟨n+1, c'⟩) < metric (psum.inl ⟨n, c⟩),
  by {
    repeat {rw metric},
    change _ < 1 + (metric' c'),
    linarith,
  },
  1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ c'@(C'.C1' n f) :=
  list.foldl max 0 (list.map (λ i : fin n,
    have metric (psum.inl ⟨n + 1, f i⟩) < metric (psum.inr ⟨n, c'⟩),
    by {
      repeat {rw metric},
      change _ < 1 + (list.foldl max 0
        (list.map (λ i : fin n, metric' (f i)) (list.fin_range n))),
      sorry,
    },
    c_depth (f i)) (list.fin_range n))
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf metric⟩],
  dec_tac := `[assumption] }

I will complete the more complex remaining case after a few hours sleep :)

[Mario Carneiro]

Note that this code is also a lot simpler if you skip the "bootstrap" part:

def c_depth_mut : ∀ {a}, C._mut_ a → ℕ
| _ (C._mut_.C1_0 n c') := 1 + c_depth_mut c'
| _ (C._mut_.C2_0 n) := 0
| _ (C._mut_.C1'_1 n f) := 1 + (list.foldl max 0
    (list.map (λ i : fin n, c_depth_mut (f i)) (list.fin_range n)))

def c_depth {n : ℕ} (c : C n) : ℕ := c_depth_mut c
def c'_depth {n : ℕ} (c : C' n) : ℕ := c_depth_mut c

[Mario Carneiro]

This has some fundamental advantages too, for example it works even if C1' had a function over an infinite set instead of fin n, while metric only works when the order type of the inductive is at most $\omega$

[Julian Sutherland]

In case this is useful for everyone, here is my final solution:

import tactic.linarith

import data.list.of_fn
import data.set.basic

mutual inductive C, C'
with C : ℕ → Type
| C1 : ∀ n : ℕ, C' (n + 1) → C n
| C2 : ∀ n : ℕ, C n
with C' : ℕ -> Type
| C1' : ∀ n : ℕ, (fin n → C (n + 1)) → C' n

def nat_list_max : list ℕ → ℕ
| [] := 0
| (x :: xs) := max x (nat_list_max xs)

lemma max_ge_elems : ∀ {ls : list ℕ} {n : ℕ}, n ∈ ls → n ≤ nat_list_max ls :=
  begin
    intros ls n n_in_ls,
    induction ls,
    exfalso,
    exact list.not_mem_nil n n_in_ls,
    change (n = ls_hd) ∨ (n ∈ ls_tl) at n_in_ls,
    cases n_in_ls,
    rw nat_list_max,
    rw n_in_ls,
    apply le_max_of_le_left,
    refl,
    rw nat_list_max,
    apply le_max_of_le_right,
    exact ls_ih n_in_ls,
  end

lemma f_i_in_list_fn : ∀ {n : ℕ} (i : fin n) {α : Type} (f : fin n → α), f i ∈ list.of_fn f :=
  begin
    intros n i α f,
    apply (list.mem_of_fn f (f i)).2,
    exact set.mem_range_self i,
  end

def metric' : ∀ {a}, C._mut_ a → ℕ
| _ (C._mut_.C1_0 n c') := 1 + metric' c'
| _ (C._mut_.C2_0 n) := 0
| _ (C._mut_.C1'_1 n f) := 1 + nat_list_max (list.of_fn (λ i : fin n, metric' (f i)))

def metric : psum (Σ' {n : ℕ}, C n) (Σ' {n : ℕ}, C' n) → ℕ
| (psum.inl ⟨_, c⟩) := metric' c
| (psum.inr ⟨_, c⟩) := metric' c

mutual def c_depth, c'_depth
with c_depth : ∀ {n : ℕ}, C n → ℕ
| _ c@(C.C1 n c') :=
  have metric (psum.inr ⟨n+1, c'⟩) < metric (psum.inl ⟨n, c⟩),
  by {
    repeat {rw metric},
    change _ < 1 + (metric' c'),
    linarith,
  },
  1 + c'_depth c'
| _ (C.C2 _) := 0
with c'_depth : ∀ {n : ℕ}, C' n → ℕ
| _ c'@(C'.C1' n f) :=
  list.foldl max 0 (list.map (λ i : fin n,
    have metric (psum.inl ⟨n + 1, f i⟩) < metric (psum.inr ⟨n, c'⟩),
    by {
      repeat {rw metric},
      cases n,
      exfalso,
      exact @fin.elim0 (λ_, false) i,
      change (metric' (f i)) + 1 ≤
        1 + nat_list_max (list.of_fn (λ i : fin n.succ, metric' (f i))),
      rw (nat.add_comm 1 _),
      apply (λp, nat.add_le_add_right p),
      exact max_ge_elems (f_i_in_list_fn i (λ i : fin n.succ, metric' (f i))),
    },
    c_depth (f i)) (list.fin_range n))
using_well_founded {
  rel_tac := λ _ _, `[exact ⟨_, measure_wf metric⟩],
  dec_tac := `[assumption] }

[Huỳnh Trần Khanh]

congratulations... oh wait. I have a sense of what the next stage would be like :joy: you will find yourself typing cases and induction to traverse your definitions and boom... you got 40 cases? how could you deal with... boom, now there are so many cases :joy:

[Huỳnh Trần Khanh]

well founded recursion doesn't compare with the mess that you're about to get into...

[Huỳnh Trần Khanh]

anyway, as usual, if you have any problems don't be afraid to ask us!

[Notification Bot]

Julian Sutherland has marked this topic as resolved.

[Notification Bot]

Julian Sutherland has marked this topic as unresolved.