Zulip Chat Archive

Stream: general

Topic: Proof of inductive type variant


view this post on Zulip Spencer Killen (May 23 2020 at 21:20):

There are cases where I'd like to define something in terms of a particular variant of an inductive type for example

inductive Foo
|one
|two

def narrow (v : Foo.one) := Prop

But this does not work
I would like for the function's v parameter to accept only the objects of type Foo that are known to be Foo.one and not Foo.two.
Is there a way to do this?

view this post on Zulip Mario Carneiro (May 23 2020 at 21:22):

In your example there is no point because there is only one element that is Foo.one, namely Foo.one, so there is no need to pass it in

view this post on Zulip Mario Carneiro (May 23 2020 at 21:22):

Usually I would write such a function taking arguments for all the arguments of the appropriate constructor case

view this post on Zulip Sebastian Ullrich (May 23 2020 at 21:22):

There isn't (how would you even access the data of v?). You should put the constructor data in a separate structure.

view this post on Zulip Sebastian Ullrich (May 23 2020 at 21:23):

Or what Mario said

view this post on Zulip Mario Carneiro (May 23 2020 at 21:23):

You could also have (v : Foo) (h : v = Foo.one) := ... or more generally (v : Foo) (h : \exists a b, v = Foo.one a b) := ...

view this post on Zulip Spencer Killen (May 23 2020 at 21:27):

Thanks,
I'm thinking of using =
I'm not sure how I would do this with a structure and sill have a type that expresses two possibilities

view this post on Zulip Mario Carneiro (May 23 2020 at 21:27):

do you have a more realistic example?

view this post on Zulip Mario Carneiro (May 23 2020 at 21:28):

I wouldn't recommend the = method because it's just more overhead over the pass the constructor arguments method

view this post on Zulip Spencer Killen (May 23 2020 at 21:29):

This is my code, I'm just sort of picking and poking until I learn lol

    variable {a : Atom}
    variable {I : Interpretation}
    variable {A : set Atom}
    variable {Z : (m: a  A), a  I.program}
    inductive Subset (A : set Atom) (S : (m: a  A), a  I.program)
    | satisfied (holds : (m: a  A), I.eval (S m) == truthy) : Subset
    | unsatisfied (u : (m: a  A), ¬(I.eval (S m) == truthy)) : Subset

I'd like to define something that only accepts satisfied subsets. However, I'm realizing now that this would probably be better achieved through negation...

view this post on Zulip Mario Carneiro (May 23 2020 at 21:30):

Sebastian is suggesting to have

structure constructor1_args := ...

inductive foo
| constructor1 : constructor1_args -> foo
| constructor2 : ... -> foo

where all the arguments of constructor1 are packed into a data structure

view this post on Zulip Spencer Killen (May 23 2020 at 21:30):

Ah, that makes sense

view this post on Zulip Mario Carneiro (May 23 2020 at 21:31):

There are a lot of weird things in that example. Do you have a #mwe for it?

view this post on Zulip Mario Carneiro (May 23 2020 at 21:32):

Does == mean something other than its usual meaning in your code? Because the standard lean meaning is heq which you almost certainly don't want

view this post on Zulip Spencer Killen (May 23 2020 at 21:32):

No, I've been using heq because = didn't work when I tried to use it somewhere...
What's the difference?

view this post on Zulip Mario Carneiro (May 23 2020 at 21:33):

oh that means something is very wrong. = only accepts arguments of the same type, == accepts arguments of different types but asserts they are the same type

view this post on Zulip Mario Carneiro (May 23 2020 at 21:35):

It's probably a better fit for #new members stream but we could go over your code, I think it would be helpful to you

view this post on Zulip Spencer Killen (May 23 2020 at 21:35):

Ah, I think I was using different types. Though in this case both arguments
are the same type

view this post on Zulip Spencer Killen (May 23 2020 at 21:39):

Thanks, but I don't know if you could help because I mostly only have definitions and haven't done anything with them.

view this post on Zulip Mario Carneiro (May 23 2020 at 21:39):

that's exactly when we can be the most help

view this post on Zulip Mario Carneiro (May 23 2020 at 21:39):

the definitions are the hardest part

view this post on Zulip Mario Carneiro (May 23 2020 at 21:39):

and because you aren't proving anything you have no guidance from lean

view this post on Zulip Spencer Killen (May 23 2020 at 21:43):

Hm, alright. I'd appreciate some help then :) should I create a new thread in #new members ?

view this post on Zulip Mario Carneiro (May 23 2020 at 22:04):

yes, post your code and an informal description of what you are trying to define


Last updated: May 13 2021 at 18:26 UTC