## Stream: new members

### Topic: defining functions out of set

#### ????? (Feb 03 2020 at 17:56):

I defined the set of natural numbers $\omega$ in a language (whose terms are elements of the type Exp) as the lfp of the functionmath f : set(Exp) \to set(Exp), s \to \{zero\} \cup \{suc(e) \mid e \in s\}. Now I want to show that $\omega$ is equivalent to $\N$ as defined in lean. I need to define $\omega \to \N$, but this is not possible due to the Prop restriction. Is there another way of doing this (short of redefining set(A) to be $A \to Type$?

#### Reid Barton (Feb 03 2020 at 21:16):

If omega : set Exp, then defining a function omega -> nat really means subtype omega -> nat, where an element of subtype omega is a pair of e : Exp and a proof that e belongs to omega. Presuming Exp is an inductive type, you can then define your function by induction on e, using the property that e belongs to omega to discard any impossible cases.

#### Reid Barton (Feb 03 2020 at 21:16):

Also, you can write LaTeX in Zulip by surrounding it in $...$.

#### ????? (Feb 03 2020 at 21:20):

thanks for the latex tip

#### ????? (Feb 03 2020 at 21:28):

So as you said I'm defining a function  subtype omega -> nat. The "impossible cases" work fine since false has a large eliminator (for some reason). But for the case such as when (e : Exp) = zero, the hypothesis one gets is that $e \in zero \iff e = zero \lor e \in \emptyset$. For this case, after I apply or.elim, I'm stuck in Prop. Since I actually want to construct a number in this case, I can't use the same trick as before.

#### Floris van Doorn (Feb 03 2020 at 21:37):

Can you show a minimal example that we can copy, and which compiles? That helps a lot to help you.

What Reid mentioned is that you want to induct on e. Something like

def foo : subtype omega -> nat :=
begin
intro x,
cases x with e he,
induction e,
[...]
end


(or by using pattern matching)

#### ????? (Feb 03 2020 at 21:40):

That is my approach

#### ????? (Feb 03 2020 at 21:40):

I will try to make an example

#### ????? (Feb 03 2020 at 21:54):

import order.fixed_points

open lattice

inductive Exp
| Zero : Exp
| Suc : Exp → Exp

open Exp

instance exp.complete_lattice: complete_lattice (set Exp) := pi.complete_lattice

def fsucc : set(Exp) → Exp → Prop := λ α x,
∃ w, x = Suc w ∧ set.mem w α

def fω := λ α, set.union { Zero } (fsucc α)
def ω : set Exp := @lfp (set Exp) _ fω
def w := {x : Exp // set.mem x ω}

theorem fmono : monotone fω :=
begin
unfold monotone,
intros a b h,
unfold fω,
apply set.union_subset_union,
{
apply set.subset.refl
},
{
unfold fsucc,
intros x g,
induction g with w h1,
induction h1 with h2 h3,
refine ⟨ w, _ ⟩,
apply and.intro,
exact h2,
apply set.mem_of_subset_of_mem h,
exact h3
}
end

def wtoN : w → ℕ :=
begin
intros,
induction a with e p,
induction e,
{
have g : ω = fω(ω), from lfp_eq fmono,
rw g at p,
unfold fω at p,
unfold set.union at p,
apply @or.elim _ _ ℕ p,
}
end


#### ????? (Feb 03 2020 at 21:55):

So the last or.elim in  wtoN does not type check since I'm trying to eliminate in Type instead of Prop

#### Reid Barton (Feb 03 2020 at 22:35):

Inside the { } in wtoN, you are already in the case that e is Zero. So you just want to return 0.

#### Reid Barton (Feb 03 2020 at 22:36):

In fact, for this type Exp, w is the set of all Exps (w = set.univ).

#### Reid Barton (Feb 03 2020 at 22:36):

So you would never need the hypothesis p.

ah right

#### Reid Barton (Feb 03 2020 at 22:41):

Also, it's probably better to write the recursive definition using pattern matching and not tactics.
Say you changed Exp to

inductive Exp
| Zero : Exp
| Suc : Exp → Exp
| Neg : Exp → Exp


without changing anything after that.

#### Reid Barton (Feb 03 2020 at 22:41):

Then you could start to define wtoN this way:

def ωtoN : Π (e : Exp), e ∈ ω → ℕ
| Zero h := 0
| (Suc e') h := ωtoN e' _ + 1
| (Neg e') h := false.elim _

def wtoN : w → ℕ := λ x, ωtoN x.1 x.2


#### Reid Barton (Feb 03 2020 at 22:42):

You will have to fill in the two _s

#### Reid Barton (Feb 03 2020 at 22:42):

But these are just propositions, so you will not need large elimination

#### ????? (Feb 03 2020 at 22:42):

I see, that's pretty nice.

#### ????? (Feb 03 2020 at 22:43):

I tried the pattern matching definition before, but sometimes I would run into issues with size

#### ????? (Feb 03 2020 at 22:43):

so size inequalities like size(e1) < size(e1) + size(e2) is not automatically discharged

#### Reid Barton (Feb 03 2020 at 22:46):

Maybe you were doing recursion on the value of type w, rather than splitting it into two arguments like I did above

#### Reid Barton (Feb 03 2020 at 22:47):

That recursion is not quite structural, because you have to build a new proof of membership which is not contained in the original one

#### ????? (Feb 03 2020 at 22:48):

that might be it. Also, in tactic mode i can do repeat { ... } for the impossible cases. I suppose this is not possible if you use pattern matching or the recursor?

#### Reid Barton (Feb 03 2020 at 22:50):

Yes, that's right. If you write definitions in tactic mode then you should be careful to use only "simple" tactics that will generate a predictable term, like induction, refine, exact, inside the parts of the definition that are data. Otherwise it will be hard to prove things about your definition later.

#### Reid Barton (Feb 03 2020 at 22:50):

Inside the proof parts you can use any tactics because proofs are irrelevant.

#### ????? (Feb 03 2020 at 22:51):

okay thanks!

Last updated: May 16 2021 at 19:19 UTC