Projection on inductive types

Stream: general

[AdLucem]

Hello, how does one define projection on inductive types? For eg:

inductive atom  : Prop
  | intro (n : ℕ) : atom

Given this piece of code, I want to define a function on atom that will return n.

[Yaël Dillies]

How could it? You need to provide n to make it a Prop, and once ypou have a Prop you can't expect to retrieve what you put in (except that in that case one of the two n is possible from the type).

[Yaël Dillies]

Also, did you mean to have to have two separate n?

[Yury G. Kudryashov]

Probably, you actually want some other type. Could you please post an #mwe with the way you are going to use this type?

[AdLucem]

Oh no, that was a mistake!
Okay, so I can't retrieve n from the Prop

[Reid Barton]

(Did you really want to make it a Prop? It seems weird with the name atom)

[Patrick Johnson]

Note that atom parameter n is unrelated to atom.intro parameter n. Which n do you want to extract? You probably want this instead:

inductive atom : ℕ → Prop
| intro (n : ℕ) : atom n

def atom.n {n : ℕ} (a : atom n) := n

Or maybe this:

inductive atom : Type
| intro (n : ℕ) : atom

def atom.n : atom → ℕ
| (atom.intro n) := n

In general, you cannot extract parameters of proposition constructors (because of proof irrelevance).

[AdLucem]

@Yury G. Kudryashov I want to define equality over atom -

def eq (a b : atom) : bool

So I need to get n for testing equality

[Vincent Beffara]

If you make it Type instead of Prop then you can:

inductive atom : Type
| intro (n : ℕ) : atom

def extract : atom → ℕ
| (atom.intro n) := n

[Yury G. Kudryashov]

But in this case you can just use

structure atom : Type := (n : nat)

[Yaël Dillies]

Or nat :stuck_out_tongue_wink:

[AdLucem]

@Patrick Johnson wait you can pattern match that way? that is useful thank you!
(ref: def atom.n {n : ℕ} (a : atom n) := n)

[AdLucem]

@Yury G. Kudryashov No, I need to be able to use atom as a constructor for type Prop. i.e: atom <some number> :: Prop

[Yaël Dillies]

This sounds like an #xy problem. Can you give us the greater picture?

[AdLucem]

Greater picture is that I'm building propositional logic in lean ( _not_ using lean's existinginfrastructure since this is for a teaching exercise). I want to be able to build "atoms" - propositional variables, essentially- and then build propositions out of them. Can I actually post the entire code that I'm trying? (I posted a simplified version of the problem- essentially that I defined atom as an inductive type and needed to get a struct-type projection for it)

[Yaël Dillies]

Yeah sure, go on! Are you one of Kevin's students by any chance?

[Yury G. Kudryashov]

You definitely can post the code.

[AdLucem]

structure var :=
  mk :: (idx : ℕ)

notation `Prp` := Sort 1

inductive atom (v : var) : Prp
  | intro : var -> atom


def p1 := atom (var.mk 1)
def p2 := atom (var.mk 2)
def p3 := atom (var.mk 3)

#check p1

The intention is: to define the 'fundamental' of propositional logic as a propositional variable (so as to not go straight to semantics, like lean does with true and false) and then define a Proposition as combinations of type variables- so as you can see, I define the homemade Prp (Proposition) in place of Type.

[AdLucem]

Yaël Dillies said:

Yeah sure, go on! Are you one of Kevin's students by any chance?

ah, no? I'm working with a prof who is introducing propositional logic with lean.

[Yury G. Kudryashov]

What is the mathematical meaning of atom v?

[Yaël Dillies]

Oh, who is it? Altenkirch?

[Yury G. Kudryashov]

Can you write "pen and paper" definitions for atom, var, etc?

[AdLucem]

Yury G. Kudryashov said:

What is the mathematical meaning of atom v?

Atom v - atomic propositional variable v

[Yury G. Kudryashov]

How is it different from v : var?

[Yury G. Kudryashov]

If Prp = Sort 1 (equivalently, Type), then you can extract information from inductive structures in Prp.

[AdLucem]

Yury G. Kudryashov said:

Can you write "pen and paper" definitions for atom, var, etc?

var : set of variables v1, v2...

p ∈ Var
------- VAR-INTRO
p ∈ Exp

[Yury G. Kudryashov]

What are Var and Exp here?

[AdLucem]

Yaël Dillies said:

Oh, who is it? Altenkirch?

Hmm no, I'm in a college called IIIT-H. Although- I think my professor might appreciate course notes/resources from other professors teaching in lean!

[Yury G. Kudryashov]

And I meant actual textbook-style definitions.

[Yury G. Kudryashov]

Or at least very readable explanations.

[AdLucem]

Yury G. Kudryashov said:

What are Var and Exp here?

Var : set of propositional variables
Exp: set of expressions in the language of propositional logic

I'm sort of writing an interpreter for a propositional logic language, so like- Var is the (only) atomic value in the language, Exp is the set of all expressions in the language

[Yury G. Kudryashov]

Why do you also need atom?

[AdLucem]

Yury G. Kudryashov said:

And I meant actual textbook-style definitions.

Ah I'm sorry! Thing is we construct Exp inductively, so a mathematical definition for Exp will be:

Exp := Atom | not Exp | Exp and Exp | Exp or Exp | Exp implies Exp (and, or, not etc. being operators)
and Atom := Atom var

[Yury G. Kudryashov]

When and, or etc enter the scene?

[Yury G. Kudryashov]

Ah, OK

[AdLucem]

Yury G. Kudryashov said:

If Prp = Sort 1 (equivalently, Type), then you can extract information from inductive structures in Prp.

what do you mean by extracting information from inductive structures in Prp ?

[Yury G. Kudryashov]

So, you actually need something like

namespace hidden

inductive expr : Type
| atom (v : var) : expr
| not : expr → expr
| and : expr → expr → expr
| or : expr → expr → expr

[Yury G. Kudryashov]

I mean that you can match on them.

[Yury G. Kudryashov]

Or use equation compiler.

[Yury G. Kudryashov]

Any two proofs of the same proposition are definitionally equal in Lean.

[Yury G. Kudryashov]

So, once you have (p : Prop) (h : p), you can't extract information from h.

[AdLucem]

I did try defining expr as an inductive type, yes! Since this is for a teaching exercise, I was trying to see if this was an alternate method of doing the same thing:

inductive not (p : Prp) : Prp
| intro : p -> not

inductive and (p q : Prp) : Prp
| intro : p -> q -> and

inductive or (p q : Prp) : Prp
| intro : p -> q -> or

inductive impl (p q : Prp) : Prp
| intro : p -> q -> impl

[AdLucem]

Yury G. Kudryashov said:

Any two proofs of the same proposition are definitionally equal in Lean.

Oh that explains why you can't extract info from things of type Prop- thanks!

[AdLucem]

Yury G. Kudryashov said:

Or use equation compiler.

hmm is there any way to see what equation compiler does? documentation etc..

[AdLucem]

Yury G. Kudryashov said:

I mean that you can match on them.

I will try this, thanks

[Yury G. Kudryashov]

This is not the same thing

[Yury G. Kudryashov]

Because you can't use two operations in the same formula

[Reid Barton]

There is potential for confusion here because you are trying to define a type of "propositions" while Lean also has a different notion that it calls propositions.

[Reid Barton]

As far as Lean is concerned, your propositional formulas might as well be any other inductive type such as list.

[Yury G. Kudryashov]

If you want to define formulas etc. before you decide what operations are allowed, then you can use this:

def var := ℕ

structure operation :=
(arity : ℕ)
(ev : vector bool arity → bool)

inductive preexpr (ops : set operation) : ℕ → Type
| atom : var → preexpr 0
| op (o : operation) (ho : o ∈ ops) : preexpr o.arity
| apply {n : ℕ} (f : preexpr (n + 1)) (e : preexpr 0) : preexpr n

-- Exercise: fill in the blanks
def preexpr.eval {ops : set operation} (ev : var → bool) :
  Π n, preexpr ops n → vector bool n → bool
| 0 (preexpr.atom v) _ := _
| _ (preexpr.op o ho) f := _
| n (preexpr.apply f e) g := _

[Yury G. Kudryashov]

UPD: in the last definition you need to tell Lean that it is decreasing on the second argument, not on the first one. I don't remember how to do it.

[Kevin Buzzard]

hmm is there any way to see what equation compiler does? documentation etc..

Chapters 7 and 8 of #tpil talk about inductive types and the equation compiler.