Inductive Types

Stream: new members

[Yasmine Sharoda]

Hello, I am writing my first program in lean. I defined the following inductive type

inductive Expr (A : Type)
| singleton : A -> Expr

Expr is a parameterized type, and so instances would have type Expr A for some type A. But the occurrence of the type Expr in the definition of singleton does not include the parameter? Is their a good reason?
PS: I am type checking this using the online tool: https://leanprover.github.io/live/latest/

[Mario Carneiro]

It does actually have the parameter, as you can see with #print Expr.singleton

[Mario Carneiro]

but in the definition, the parameters to the inductive type are left off so you can't change them

[Yury G. Kudryashov]

You're not allowed to use Expr with any other parameter inside | singleton : A → Expr line, so you don't write the parameter at all.

[Mario Carneiro]

technically speaking, inside the types for the constructors, a local variable called Expr : Type is available for use to refer to the type being defined, and when the constructor is actually created, this variable is replaced with Expr A where Expr : Type -> Type is the new constant

[Alex Zhang]

If I define mynat as follows

inductive mynat : Type
| zero : mynat
| succ : mynat → mynat

example : mynat.zero ≠ mynat.succ mynat.zero :=
begin
  intros h,
  sorry
end

example : function.injective mynat.succ :=
begin
  intros a b h,
  sorry
end

Then do I have "mynat.zero ≠ mynat.succ mynat.zero" and "mynat.succ is injective" by the definition? If so, how can I prove them?

[Mario Carneiro]

nat.no_confusion can be used to prove both of them

[Mario Carneiro]

the equation compiler knows about both of these lemmas though so you can get some slicker proofs using it

example : mynat.zero ≠ mynat.succ mynat.zero.
example : function.injective mynat.succ | _ _ rfl := rfl

[Alex Zhang]

Could you please explain the function of nat.no_confusion?

[Kevin Buzzard]

https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/