Why structures : Prop can't contain vals but inductives can?

Stream: new members

[aron]

I'm trying to understand why structures of type Prop cannot contain any fields with values of Type, when you can just refactor the structure into a single constructor inductive that contains the value inside the constructor just fine?

I understand that you're not allowed to extract the value unless you're eliminating into Prop, but if Lean has machinery for detecting this for an inductive why can it not do the same for values taken from a structure?

Is this related to proof irrelevance? That matching on an inductive gets you in a mode where the contents of the inductive constructor can never be visible in Type but you can extract values from structures without matching on them and therefore that doesn't impose the same mode?

[Henrik Böving]

when you can just refactor the structure into a single constructor inductive that contains the value inside the constructor just fine?

Can you give an example of that?

[aron]

/-- This is fine -/
inductive TInductive : Prop where
  | mk : (x : Nat) → TInductive

/-- This is not -/
structure TStruct : Prop where
  x : Nat

[Eric Paul]

Assuming I understand what you're saying, it is due to Props only being able to eliminate into Prop. It is only an issue for structures because they try to automatically generate functions out of your structure whereas an inductive does not.

For example, the structure Test here automatically generates a function Test.t.

structure Test : Prop where
  t : 2 = 3

#check Test.t

This is a projection function. Given a term of Test, it gives you back a term of type 2 = 3.
The equivalent inductive does not generate this function.

So now in the case where there is a string:

structure Test : Prop where
  t : String

It tries to again generate a projection function Test.t whose type should be Test → String. But since you can only make functions from Test to Prop, this fails.
Since the corresponding inductive does not attempt to make these projection functions, there are no errors.

Note that even though you can create this inductive without errors (since no projections are automatically generated), you cannot write the projection functions yourself for the same reason they can't be automatically generated.

[aron]

@Eric Paul thanks for that explanation! But presumably there is some special machinery in Lean to prevent you from being able to match on props when your goal is in Type. So is there a reason why the same machinery couldn't apply that check to the generated projection functions? I.e. that you can't use Test.t unless your goal is in Prop?

[aron]

I think what I'm getting is that the restriction that prevents you from matching on props when your goal is in Type feels very ad hoc to me. So I don't see a fundamental reason for why certain operations (extracting a value from a prop) are allowed in some contexts but not others. So if matching on a prop is an ad hoc restriction anyway, why not apply that same ad hoc restriction to the generated structure projection functions?

[Chris Bailey]

Proof irrelevance + large elimination (eliminating a prop into type) is inconsistent.

[Kenny Lau]

@aron more specifically, if we allow:

/-- This is not -/
structure TStruct : Prop where
  x : Nat

and if we allow (TStruct.mk 37).x = 37 and (TStruct.mk 67).x = 67, then we can in fact derive a contradiction, because any two proofs are equal

[Kenny Lau]

axiom TStruct : Prop
axiom TStruct.mk : Nat → TStruct
axiom TStruct.x : TStruct → Nat
axiom TStruct.x_mk (n : Nat) : (TStruct.mk n).x = n

example : False :=
  have h₁ : (TStruct.mk 37).x = 37 := TStruct.x_mk 37
  have h₂ : (TStruct.mk 67).x = 67 := TStruct.x_mk 67
  -- note that Lean automatically equates TStruct.mk 37 and TStruct.mk 67
  have h₃ : 37 = 67 := h₁.symm.trans h₂
  absurd h₃ (by decide)

[aron]

@Kenny Lau thanks for the illustration, it's helpful to have a concrete demo of the exact problem.

But my question is more about what is special about matching on an inductive that puts Lean in a special mode where any values may only eliminate into Prop – and why can't that special mode also be applied to the generated projection functions on a structure?

[Kenny Lau]

because inductive doesn't generate projections automatically

[Kenny Lau]

for example, Nat is an inductive type with two constructors Nat.zero and Nat.succ, and Nat.succ eats a natural number, and there is no automatically generated Nat.pred

[Eric Paul]

Whenever you use match, you are creating a function out of your type. If your goal is a Prop, then you are using match to create a function from your type to a Prop and so it succeeds. There is no difference between using match on an inductive versus a structure. So there is no special mode. Whether or not you can match successfully depends on whether your goal is a Type or a Prop.

Since the attempted projection functions are trying to make a Type, they cannot match successfully.

[One Happy Fellow]

To ask a silly question: if the projection functions weren't generated for structures, would Aron's initial example work?

[Kenny Lau]

@One Happy Fellow a structure is just a one-constructor inductive type; if there's no projection functions, then it's just the inductive type, which we've seen work

[One Happy Fellow]

Thank you, I didn't realise these are equivalent.