defining functions out of set

Stream: new members

[?????]

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]

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]

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

[?????]

thanks for the latex tip

[?????]

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]

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)

[?????]

That is my approach

[?????]

I will try to make an example

[?????]

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

[?????]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

So you would never need the hypothesis p.

[?????]

ah right

[Reid Barton]

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]

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]

You will have to fill in the two _s

[Reid Barton]

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

[?????]

I see, that's pretty nice.

[?????]

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

[?????]

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

[Reid Barton]

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

[Reid Barton]

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

[?????]

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]

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]

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

[?????]

okay thanks!