Zulip Chat Archive

Stream: new members

Topic: defining functions out of set


view this post on Zulip ????? (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\N as defined in lean. I need to define ωN\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 ATypeA \to Type?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Feb 03 2020 at 21:16):

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

view this post on Zulip ????? (Feb 03 2020 at 21:20):

thanks for the latex tip

view this post on Zulip ????? (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 ezero    e=zeroee \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.

view this post on Zulip 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)

view this post on Zulip ????? (Feb 03 2020 at 21:40):

That is my approach

view this post on Zulip ????? (Feb 03 2020 at 21:40):

I will try to make an example

view this post on Zulip ????? (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

view this post on Zulip ????? (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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Feb 03 2020 at 22:36):

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

view this post on Zulip Reid Barton (Feb 03 2020 at 22:36):

So you would never need the hypothesis p.

view this post on Zulip ????? (Feb 03 2020 at 22:40):

ah right

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Feb 03 2020 at 22:42):

You will have to fill in the two _s

view this post on Zulip Reid Barton (Feb 03 2020 at 22:42):

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

view this post on Zulip ????? (Feb 03 2020 at 22:42):

I see, that's pretty nice.

view this post on Zulip ????? (Feb 03 2020 at 22:43):

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

view this post on Zulip ????? (Feb 03 2020 at 22:43):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip ????? (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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Feb 03 2020 at 22:50):

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

view this post on Zulip ????? (Feb 03 2020 at 22:51):

okay thanks!


Last updated: May 16 2021 at 19:19 UTC