Zulip Chat Archive

Stream: general

Topic: Proof of inductive type variant


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?

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

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

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.

Sebastian Ullrich (May 23 2020 at 21:23):

Or what Mario said

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) := ...

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

Mario Carneiro (May 23 2020 at 21:27):

do you have a more realistic example?

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

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...

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

Spencer Killen (May 23 2020 at 21:30):

Ah, that makes sense

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?

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

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?

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

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

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

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.

Mario Carneiro (May 23 2020 at 21:39):

that's exactly when we can be the most help

Mario Carneiro (May 23 2020 at 21:39):

the definitions are the hardest part

Mario Carneiro (May 23 2020 at 21:39):

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

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 ?

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: Aug 03 2023 at 10:10 UTC