Local definitions in mutual inductive type block

Stream: lean4

[Avi Craimer]

@Mario Carneiro @Tomas Skrivan

Mario, I'm not sure I can give a minimum working example, because I can't get it to work :wink:

However, I've tried to separate the data from the constaint checking. For the data I've used a structure with a generic type variable, and then I use a recursive function to figure out the correct nested type.

structure MorphData (d:Nat) (α :Type u)  where
  name: Name
  input: α
  output: α

def MorphDataT (d:Nat)  :=
match d with
 | 0 => MorphData 0 {⋆}
 | nonZero => MorphData nonZero  (MorphDataT (nonZero - 1))

It's obvious to me that this recursion terminates, but I get an error,

fail to show termination for
  MorphDataT
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    MorphDataT (nonZero - 1)

However, I don't know what to put in the termination_by clause. I searched for examples, but the obvious things don't work. I need to say that d will keep getting smaller until it terminates upon reaching zero,

A good general learning point for me would be this. Is there a way to print the proposition that needs to be proven to prove recursion for a function that is not itself a theorem?

[Mario Carneiro]

The easiest way to fix this particular error is to use n + 1 instead of n in the nonzero case

[Mario Carneiro]

If I understand your construction correctly, this should do what you want:

inductive RawMorph : Nat → Type u where
  | unit : RawMorph 0
  | pair (nm : Name) (i : RawMorph n) (o : RawMorph n) : RawMorph (n+1)

inductive RawMorph.isGlobular : RawMorph n → Prop
  | unit : RawMorph.isGlobular .unit
  | self {i : RawMorph n} : i.isGlobular → (i.pair nm i).isGlobular
  | parallel {i o : RawMorph n} :
    (i.pair nm₁ o).isGlobular → (i.pair nm₃ o).isGlobular →
    ((i.pair nm₁ o).pair nm₂ (i.pair nm₃ o)).isGlobular

def Morph (n) := { m : RawMorph n // m.isGlobular }

[Avi Craimer]

Thanks for the code example. I don't entirely understand it, but I'll try to figure it out.

My own version is progressing. With the recursive morphism data structure type I can eliminate the mutual recursion between Constraint and MorphSym. Since they both depend only on MorphData.

structure MorphData (d:Nat) (α :Type u)  where
  name: Name
  input: α
  output: α
deriving Repr

def MorphDataT (d:Nat)  :=
match d with
 | 0 => MorphData 0 {⋆}
 | n + 1 => MorphData d  (MorphDataT (n))

inductive Constraint :  Type u :=
| globular (d:Nat) (input: MorphDataT d)  (output: MorphDataT d) (p:(input = output) ∨ (input.input = output.input ∧ input.output = output.output)) : Constraint

However, now I get the error:

input : MorphDataT d
invalid field 'input', the environment does not contain 'MorphDataT.input'
  input
has type
  MorphDataT dLean

I'm guessing this is because the type checker doesn't resolve MorphDataT d to the type it returns. Is there some flag I should add to MorphDataT to tell the compiler to replace it with the actual type it returns?

[Avi Craimer]

@Mario Carneiro Thanks again. I managed to adapt and build on the code sample you posted above. I think I see how to do what I wanted to do now. If I understand correctly, the basic strategy is have a "raw" type that gives you all the values with their basic shape but without propositional constraints on which ones can be formed. Then use subtyping to form the actual set of relevant values. Is this a common pattern?

I was also curious to know what the difference is between using a Sigma type and using the { _ // _ } notation. At first I assumed the { _ // _ } notation must be syntactic sugar for a Sigma type, but it seems to produce something different.

[Mario Carneiro]

The difference between Sigma and Subtype is that one takes A : Type and B : A -> Type and the other takes A : Type and p : A -> Prop

[Jason Rute]

@Avi Craimer See docs#sigma and docs#subtype (Lean 3 but I doubt it is different in Lean 4).

[Avi Craimer]

Alright, I understand now. If I want to filter our certain elements with a proposition use Subtype, if I want a dependent product where the second value can be more than a singleton use Sigma.