rfl not working for well founded recursion

Stream: general

[Frederick Pu]

does anyone know why rfl fails in this case?

protected inductive ComputedAutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk : ComputedAutoDiffTree.DiffTree α β outShape

protected inductive AutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : Array (Σ shape, AutoDiffTree.DiffTree α β shape))
    : AutoDiffTree.DiffTree α β outShape
| ofComputed {shape : List Nat}: ComputedAutoDiffTree.DiffTree α β shape → AutoDiffTree.DiffTree α β shape

protected def ComputedAutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : ComputedAutoDiffTree.DiffTree α β shape → Prop :=
  fun x => True
def AutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : AutoDiffTree.DiffTree α β shape → Prop
| ofComputed computedTree => computedTree.valid
| mk _ parents => ∀ x ∈ parents, x.2.valid
termination_by
    t => sizeOf t
decreasing_by
    have : sizeOf x < sizeOf parents := Array.sizeOf_lt_of_mem (by assumption)
    cases x
    simp
    simp at this
    omega

example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) : (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid :=
  rfl
/-
    type mismatch
    rfl
  has type
    ?m.4183 = ?m.4183 : Prop
  but is expected to have type
    (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid : Prop
-/

[François G. Dorais]

Wellfounded definitions are irreducible. Use this to make it work:

unseal AutoDiffTree.DiffTree.valid in
example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) : (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid :=
  rfl

[Frederick Pu]

what does unseal do?

[François G. Dorais]

It locally makes the definition semireducible.

[Frederick Pu]

so is it like sorry?

[François G. Dorais]

No, not at all.

[François G. Dorais]

It allows lean to see the definition of AutoDiffTeee.DiffTree.valid.

[Frederick Pu]

still broken for me

unseal AutoDiffTree.DiffTree.valid in
example {α : Type u} {β : Type v} {shape : List Nat} (c : ComputedAutoDiffTree.DiffTree α β shape) : (DiffTree.ofComputed c).valid = c.valid := by
    rfl
/-
tactic 'rfl' failed, the left-hand side
  (DiffTree.ofComputed c).valid
is not definitionally equal to the right-hand side
-/

[François G. Dorais]

Works fine for me.

[François G. Dorais]

https://live.lean-lang.org/#codez=A4Jw9gLgpgxtAmACAlgO3gVzsgblRAwmALbAYICC5YAIsgGb0AqIUUAdHYy24gBSBG4EQAuREwCewfBgCU/QE3AIsZPw45ogDLIAzhEQA5AIZ7ASYTKp/YoYAeiDIjUAoAD6JiAayVFS5KPCoQtAzMrBxcIbxCimDkAMoAFoZSjo6gkLAIKOhYELj4AUHcoZzBPPiCShIWsgqVKg7qiFq6BsaIZlXlVrb2Tq4ejohD/DEQCUn4mjp6RhAyg8N8wIasqBDaShQgIIbi/IDFwIjaiVIANIgF4WUlRZGIiscTMvPDm9RXxR930XEnUC6IMD0bxkTIAb0eFimLVmAF9RCDfP53qVPqjvkc/u0LijbmF0fgopiJik0tA4H5EPAoPRCCRQX5LgSbhEODhDAAbZBIMFCUSdOywxBgxT8+o4IUQrHQmbGIUI+lIpl4lllRBEyH4MwABXAwBEAF4FvQMKhELYDQA+MQgDD/am05Ws1XFdlcnl88zSSWir0OSWapTNWUQeU4wJffF49X3YkWHV6gFAxGZGCKhBqq2INM+DOuzncgEeRAAfUQy1W60QWcAAETmxCACCJyysoGttOdrOwAEzsN2F6AgYhoYzIMCoEsAI3ECyGeiz2mQAC8oAB5WkQRzUmCsQwL1AAc0n09eiTwSgXy7X9YAPEcl6vaRXW1XhAaLttduwLw+SxyICWgRLYgoGIfgp0QXdtAwUhcjHF5hhgXcoA2awZzvUg0IXUgIL0CB4h0NCSCgfdDBSU1tCgTlw0KZ1I17AskDQRwoGsQxSA5fBeTqaofW41QA2lJpplaUN+FsBVc0ZXFaIJGMHj+Ro+Cda46OTdNKWsGR6PdatzW07lDQWEB6A5RwAHoAFo0Igeoh20KwIBgeI0OM0yhkSDYbOSV4AH5iHYAAWABGAAOABmXS/MC0KItEXUwGABYJ3IFANhYqQKSQQJEFPfAvP+V4lOklTmTUySkE0/SkDfTs+yQOLEwsszHCAA

[Frederick Pu]

this breaks rfl tho: https://live.lean-lang.org/#codez=A4Jw9gLgpgxtAmACAlgO3gVzsgblRAwmALbAYICC5YAIsgGb0AqIUUAdHYy24gBSBG4EQAuREwCewfBgCU/QE3AIsZPw45ogDLIAzhEQA5AIZ7ASYTKp/YoYAeiDIjUAoAD6JiAa0eJv/MOQDKABaGFpo6ekYQMl4+fMCGrKgQ2koUICCG4vyAxcCI2sFSADSEJGSU1FzMrByVPPhCivkhUDLRPkpEpORQ8FQQtAxVbJyDdYgNiH4QQc2OjqCQsAgo6FgQuPh9A9zVIzu8gkoSFrIKRyoO6ohaugbGiGbH+HxWtvZOrh4x3nxTM6HXcJ3KLffjxRLJVLpTI5PIFKDFLa1XbI3gTJpSVqg0RI0YovFoxCKP7wlyTeidMo9RAAbwx+DCt0iAF9RJTur0KgSatzxkS4c0HohcfseaK+Y1SfNwNA4NT4FB6CUuuV+qixUMODhDAAbZBIGlCURPOzM2mKY0XHBmunwpQ3CLGM1s0ockWavaaiUCixmAAK4GAIgAvDF6BhUIhbMGAHxiEAYKCOBVK911T3p7V6g1G8zSG0WvMOG30+1AlmpLmijPVb2l/2BslgCmu5YwVs9MaxxDtlWd3ZZ/VkjyIAD6iHBUCSKW7gAAiKOIQAQRBOElPksVrOwAEzsQfwRzQEDENDGZBgVCjgBG4lBem72mQAC8oAB5JUQZOwViGB+oADmV43u0wR4EoD7Pm+C4ADx5E+r5KpO04hsK0LiOw4HwaOOoQKOzajsQUDEPw16ID+2gYKQ6znm0PgwD+UApNYoIPqQzHIKQpF6BAgQ6KCJBQH+hhzBG2hQLqwpVh66q7rq+orI4UDWIYpA6vghrnCcBYaaoJZ2oyjoQGafC2C6facmq3I1oSkrNFcfBpvi1bNuyyzWDIMnZogwZRh5cnCKG3ggPQOqOAA9AAtAeFzHtoVgQDAgQxEFIXBCkEAqDEAD8xDsAArAALLlADMXmINleWFSVogBmAwCOJe5AoCkilSHKSD9IgIH4OlUgxPZknptJzkdkgbm+Ug3mbnuSg1XV4WhY4QA

[Frederick Pu]

protected inductive ComputedAutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : Array (Σ shape, ComputedAutoDiffTree.DiffTree α β shape))
    : ComputedAutoDiffTree.DiffTree α β outShape

protected inductive AutoDiffTree.DiffTree (α : Type u) (β : Type v) : List Nat → Type (max u v)
| mk
    (outShape : List Nat)
    (parents : Array (Σ shape, AutoDiffTree.DiffTree α β shape))
    : AutoDiffTree.DiffTree α β outShape
| ofComputed {shape : List Nat}: ComputedAutoDiffTree.DiffTree α β shape → AutoDiffTree.DiffTree α β shape

protected def ComputedAutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : ComputedAutoDiffTree.DiffTree α β shape → Prop :=
  fun x => True
def AutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : AutoDiffTree.DiffTree α β shape → Prop
| ofComputed computedTree => computedTree.valid
| mk _ parents => ∀ x ∈ parents, x.2.valid
termination_by
    t => sizeOf t
decreasing_by
    have : sizeOf x < sizeOf parents := Array.sizeOf_lt_of_mem (by assumption)
    cases x
    simp
    simp at this
    omega

unseal AutoDiffTree.DiffTree.valid in
example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) : (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid :=
  rfl
/-
type mismatch
  rfl
has type
  ?m.5453 = ?m.5453 : Prop
but is expected to have type
  (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid : Prop
-/

[François G. Dorais]

Why do you think it should work?

[Frederick Pu]

because of the definition of AutoDiffTree.DiffTree.valid

[Mario Carneiro]

Note that well founded definitions don't always reduce by rfl. This is the reason they were made irreducible in the first place

[Frederick Pu]

def AutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : AutoDiffTree.DiffTree α β shape → Prop
| ofComputed computedTree => computedTree.valid
| mk _ parents => ∀ x ∈ parents, x.2.valid

[Frederick Pu]

all i did was change the definition ComputedAutoDiffTree.DiffTree
so i dont see why that should make rfl suddenly fail

[Mario Carneiro]

If you really want this to be true by rfl, you will probably have to do the structural recursion by hand

[Mario Carneiro]

Since this is a prop, another approach that should not be so bad is to define it as an inductive type

[Mario Carneiro]

inductive AutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} : ∀ {shape : List Nat}, AutoDiffTree.DiffTree α β shape → Prop
  | ofComputed : computedTree.valid → (ofComputed computedTree).valid
  | mk : (∀ x ∈ parents, valid x.2) → (mk shape parents).valid

[Mario Carneiro]

the direct function definition by mutual recursion is still quite painful to write, but it has at least some of the definitional equalities you want:

def AutoDiffTree.DiffTree.valid {α : Type u} {β : Type v} {shape : List Nat} : AutoDiffTree.DiffTree α β shape → Prop := by
  apply AutoDiffTree.DiffTree.rec
    (motive_1 := fun a b => Prop) (motive_2 := fun a => Prop)
    (motive_3 := fun a => Prop) (motive_4 := fun a => Prop)
  case mk => intro _ _ ih; exact ih
  case ofComputed => intro _ computedTree; exact computedTree.valid
  case /-Array.-/ mk => intro _ ih; exact ih
  case /-List.-/ nil => exact True
  case /-List.-/ cons => intro _ _ ih1 ih2; exact ih1 ∧ ih2
  case /-Prod.-/ mk => intro _ _ ih; exact ih

example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) :
  (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid := rfl -- ok

example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) :
  (AutoDiffTree.DiffTree.mk shape parents).valid = ∀ x ∈ parents, x.2.valid := rfl -- fail

[Frederick Pu]

Mario Carneiro said:

Since this is a prop, another approach that should not be so bad is to define it as an inductive type

but then u still dont have a way of showing if (ofComputed c).valid then c.valid tho

[Frederick Pu]

nvm ig pattern matching solves that somehow

[Frederick Pu]

where did the additional shape✝ variable come from?

def forward {α : Type u} {β : Type v} {shape : List Nat} : AutoDiffTree α β shape → ComputedAutoDiffTree α β shape
| ⟨AutoDiffTree.DiffTree.ofComputed c, h⟩ => ⟨c, by {
    cases h
    trivial
}⟩
| ⟨AutoDiffTree.DiffTree.mk (parents : Array (Σ shape, AutoDiffTree.DiffTree α β shape)) (ctx : Σ shapes, EFunction α β shapes shape) (tensor : DualTensor α β shape), h⟩ =>
    let temp := ctx.2.forward sorry sorry -- parents tensor
    ⟨⟨parents.map (fun ⟨shape, tree⟩ => ⟨shape, (⟨tree, sorry⟩ : AutoDiffTree α β shape).forward.1⟩), by {
        exact ⟨ctx.snd.saveShapes,
            ⟨⟨
            ((List.finRange parents.size).map
                (fun x =>
                let tree := (parents.get x.val sorry).2
                ⟨(parents.get x.val _).fst, tree.tensor⟩
                )).toArray,
            sorry⟩, sorry⟩
        ⟩
    }, ctx, sorry⟩, sorry⟩
termination_by
    t => sizeOf t
decreasing_by
    simp_wf
/-
α : Type u
β : Type v
shape✝ : List Nat
parents : Array ((shape : List Nat) × AutoDiffTree.DiffTree α β shape)
ctx : (shapes : Array (List Nat)) × EFunction α β shapes shape✝
tensor : DualTensor α β shape✝
h : (DiffTree.mk parents ctx tensor).valid
shape : List Nat
tree : AutoDiffTree.DiffTree α β shape
⊢ sizeOf tree < 1 + sizeOf shape✝ + sizeOf parents + sizeOf ctx + sizeOf tensor
-/

[Frederick Pu]

Mario Carneiro said:

If you really want this to be true by rfl, you will probably have to do the structural recursion by hand

so is there any way of proving stuff about well founded functions?

[Kyle Miller]

Yes, you can use tactics like unfold/simp to unfold the definitions. You may need to do cases on arguments to make them unfoldable (according to the match patterns)

[Kyle Miller]

For example, using the code from the first message in this thread,

example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) : (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid := by
  simp [AutoDiffTree.DiffTree.valid]

[Kyle Miller]

In particular, it's the first equation lemma that applies here:

example {α : Type u} {β : Type v} {shape : List Nat} (x : ComputedAutoDiffTree.DiffTree α β shape) : (AutoDiffTree.DiffTree.ofComputed x).valid = x.valid :=
  AutoDiffTree.DiffTree.valid.eq_1 ..

(I don't think it's good practice to refer to equation lemmas directly, that's what unfold/simp are for, but I'm mentioning it for illustration. Lean does know, somewhere, that the function satisfies the equation you gave it.)

[Frederick Pu]

i wonder if there's a brute force tactic that could do this casework automatically for simpler definitions

[Frederick Pu]

can grind do this?

[Kim Morrison]

Kyle Miller said:

simp [AutoDiffTree.DiffTree.valid]

grind [AutoDiffTree.DiffTree.valid] works equally well?