Zulip Chat Archive

Stream: general

Topic: or.dcases_on

Zesen Qian (Jul 02 2018 at 16:24):

In general, what does this message mean? induction tactic failed, recursor "or.dcases_on" can only eliminate into Prop.

Zesen Qian (Jul 02 2018 at 16:24):

this happens at the head of a inductive function def.

Kenny Lau (Jul 02 2018 at 16:24):

it means you can't decompose an or into data

Zesen Qian (Jul 02 2018 at 16:49):

is it just or, or any inductive types in general? because there is no or in my code.

Chris Hughes (Jul 02 2018 at 16:52):

A lot of (but not all) inductive propositions cannot eliminate into data. inductive non-propositions can always eliminate into data.

Kevin Buzzard (Jul 02 2018 at 17:02):

Stupid question: can one get around this somehow with classical or noncomputable assumptions? Or does one run into contradictions in this generality?

Kevin Buzzard (Jul 02 2018 at 17:02):

is it just or, or any inductive types in general? because there is no or in my code.

@Zesen Qian If you post a minimal working example as a gist then perhaps someone can locate the or ;-)

Chris Hughes (Jul 02 2018 at 17:04):

You can, but you have to decide what to do when both sides are true.

Chris Hughes (Jul 02 2018 at 17:08):

So you might end up with a function whose behaviour is unknown when they're both true.

Simon Hudon (Jul 02 2018 at 17:13):

By using prod_decidable, you can make a function to go from or to sum:

local attribute [instance] classical.prop_decidable

noncomputable def or.to_sum (h : p ∨ q) : plift p ⊕ plift q :=
if h' : p then sum.inl ⟨ h' ⟩
          else sum.inr ⟨ by { rw ← false_or q, exact or.imp_left h' h } ⟩

Reid Barton (Jul 02 2018 at 17:35):

What you can't get when eliminating into non-Prop is the computation rule that reduces an application or.cases_on (or.inl p) f g to f p and also or.cases_on (or.inr q) f g to g q, since or.inl trivial = or.inr trivial but f trivial might not be equal to g trivial (unless the result type is a proposition).

Zesen Qian (Jul 02 2018 at 17:58):

sorry so what's default universe level of inductive types that's not specified level? Is it polymorphisized on all levels?

Simon Hudon (Jul 02 2018 at 18:01):

I'm sorry I can't parse your question. Are you talking of an error message?

Zesen Qian (Jul 02 2018 at 18:03):

no I mean like 

inductive bool
| true
| false

will there be universe polymorphism for this, or just Type 1?

Kenny Lau (Jul 02 2018 at 18:03):

universe

Simon Hudon (Jul 02 2018 at 18:06):

I would guess it's a Type 0 but I recommend you discover it for yourself. Try #check bool

Zesen Qian (Jul 02 2018 at 18:08):

yes it's Type 0, thank you.

Kevin Buzzard (Jul 02 2018 at 18:09):

inductive bool1
| true : bool1
| false : bool1

#check bool1 -- Type

universe u

inductive bool2 : Type u
| true : bool2
| false : bool2

#check bool2 -- Type u_1 (i.e. universe is "whatever")

universe v

#check bool2.{v} -- Type v

Kevin Buzzard (Jul 02 2018 at 18:09):

There are some tricks

Zesen Qian (Jul 02 2018 at 18:13):

Thanks, I guess we can use it to workaround "universe too big" issue with this?

Zesen Qian (Jul 02 2018 at 18:14):

I now have an error saying the argument of a constructor is too big.

Zesen Qian (Jul 02 2018 at 18:14):

inductive t0 : Type u
...

inductive t1 : Type u
| cons : t0 -> t1

Simon Hudon (Jul 02 2018 at 18:15):

On t1?

Zesen Qian (Jul 02 2018 at 18:18):

yeah, says the first argument of cons, t0, is too big.

Kevin Buzzard (Jul 02 2018 at 18:19):

If you don't tell t1 what type it is then this might fix it

Kevin Buzzard (Jul 02 2018 at 18:20):

universe u

inductive t0 : Type u
| foo : t0

inductive t1
| cons : t0 -> t1

Reid Barton (Jul 02 2018 at 18:20):

Maybe the u of t0 is not the same u as in t1, although I would expect a different error message then

Simon Hudon (Jul 02 2018 at 18:20):

I was thinking maybe this would be required:

inductive t1 : Type u
| cons : t0.{u} -> t1

Simon Hudon (Jul 02 2018 at 18:21):

But more generally, there is no reason for t0 not to be in Type 0

Zesen Qian (Jul 02 2018 at 18:21):

@Simon Hudon thanks, this fixes it.

Zesen Qian (Jul 02 2018 at 18:21):

basically I'm still trying out the universes.

Kevin Buzzard (Jul 02 2018 at 18:22):

inductive t0 : Type
| foo : t0

inductive t1 : Type
| cons : t0 → t1

Simon Hudon (Jul 02 2018 at 18:22):

I learned this the hard way: when definitions are more universe polymorphic than strictly necessary, it gets really painful

Zesen Qian (Jul 02 2018 at 18:24):

@Kevin Buzzard but this doesn't provide universe polymorphism.

Simon Hudon (Jul 02 2018 at 18:24):

Case in point: my current traversable pull request took me one year to set up. It was not all about universe polymorphism but it certainly made it difficult

Zesen Qian (Jul 02 2018 at 18:24):

and I kind of feel my first error in this stream, has something to do with it.

Andrew Ashworth (Jul 02 2018 at 18:24):

I'm not sure what universe polymorphism is good for when it comes to concrete programs

Kenny Lau (Jul 02 2018 at 18:24):

universe is for consistency

Andrew Ashworth (Jul 02 2018 at 18:24):

I feel like everything I need to do lives in Type, for the most part

Kenny Lau (Jul 02 2018 at 18:25):

and strengthening

Zesen Qian (Jul 02 2018 at 18:25):

I don't know what dependent types is good for when it comes to concrete programs, TBH.

Kenny Lau (Jul 02 2018 at 18:25):

and category theory

Andrew Ashworth (Jul 02 2018 at 18:26):

dtt is a bit of an academic stretch right now, true, but one day when there's an efficient method for program extraction, it might be awesome

Simon Hudon (Jul 02 2018 at 18:27):

I think we can weaken @Andrew Ashworth 's suggestion and generalize it into: work in Type 0 until you run into trouble. Then make the smallest necessary universe generalization

Andrew Ashworth (Jul 02 2018 at 18:27):

if you knew how terribly written most of the software that runs the electronics around us was, you'd be rooting for Lean too :)

Simon Hudon (Jul 02 2018 at 18:27):

There are tools for lifting monomorphic definitions to using them in polymorphic contexts so Type 0 is not handicapping

Simon Hudon (Jul 02 2018 at 18:28):

Amen

Simon Hudon (Jul 02 2018 at 18:29):

@Andrew Ashworth I'm getting ready for the DeepSpec summer school where people like Adam Chlipala will show us how he uses dependent type theory for building reliable cryptographic implementation. It's hard to argue that it's really just academic

Andrew Ashworth (Jul 02 2018 at 18:30):

isn't anything chlipala does academic by definition ;]

Simon Hudon (Jul 02 2018 at 18:31):

It depends. Is your definition of academic "anything that happens in a university"? In that case, is the university's janitor studying academic sweeping?

Simon Hudon (Jul 02 2018 at 18:33):

In the case of the DeepSpec project, academics are playing the role of leader but the project involves industrial partners so the point is not (only) publication but building systems that work Monday through Sunday

Zesen Qian (Jul 02 2018 at 18:34):

before it's getting too far, let me ask one last question: can I define structure as universe polymorphic?

Hoang Le Truong (Jul 02 2018 at 18:34):

Yes it depend. how I get f (x:α) because I need it to define next object

Simon Hudon (Jul 02 2018 at 18:39):

@Hoang Le Truong I think you're in the wrong thread

Reid Barton (Jul 02 2018 at 18:40):

@Zesen Qian about your original error, it has to do with the difference between Prop and Type (or more generally Type u), which is rather different from the difference between Type u for varying u

Reid Barton (Jul 02 2018 at 18:42):

You can generalize over both Prop and Type with Sort, but all the Type u for different u work pretty much the same way, while Prop has some different rules

Zesen Qian (Jul 02 2018 at 19:17):

thanks, I will look into it.

Zesen Qian (Jul 03 2018 at 15:21):

yeah I give up. Here is the line causing this error:
https://github.com/riaqn/smtlean/blob/6e5c20aaa344e972528d8089af01f638819ff06c/src/cvc4.lean#L129

Last updated: Dec 20 2023 at 11:08 UTC