Proof of inductive type variant

Stream: general

[Spencer Killen]

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]

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]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

Or what Mario said

[Mario Carneiro]

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]

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]

do you have a more realistic example?

[Mario Carneiro]

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

[Spencer Killen]

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]

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]

Ah, that makes sense

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Spencer Killen]

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]

that's exactly when we can be the most help

[Mario Carneiro]

the definitions are the hardest part

[Mario Carneiro]

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

[Spencer Killen]

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

[Mario Carneiro]

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