# Zulip Chat Archive

## Stream: general

### Topic: cases fails on exists

#### Nima (Apr 21 2018 at 07:51):

Can you explain this error message (it happens when I say `cases hm with aa bb`

, but `by_cases number.has_min α with hm`

works perfectly fine):

induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop state: α : Type u_1, _inst_1 : number α, trvk : triviality_kind, strk : strictness_kind, bnd : α, c : constraint α trvk kupper strk, ht : ¬is_trivial c, hs : is_strict c, hm : ∃ (hm : number.has_min α), number.min hm < get_bound c _ ⊢ α

#### Mario Carneiro (Apr 21 2018 at 07:55):

You can't destruct an exists directly because it's a (small eliminating) Prop. However, in the special case when it is an exists over a prop, you can use `hm.fst`

and `hm.snd`

to project out the components

#### Nima (Apr 21 2018 at 08:01):

Isn't that the same situation as

example : (∃ a:1>2, false) → false := begin intro h, cases h with a b, -- no problem here assumption end

#### Mario Carneiro (Apr 21 2018 at 08:01):

You can use cases on exists to prove a Prop, but not to construct data (something in a type that lives in Type)

#### Mario Carneiro (Apr 21 2018 at 08:02):

here it's okay because `false : Prop`

#### Mario Carneiro (Apr 21 2018 at 08:02):

while in the other case `α : Type u_1 != Prop`

#### Mario Carneiro (Apr 21 2018 at 08:04):

The basic idea is that if you want to use partial functions in your code, you have to write all the actual function calls not dependent on the proof part

#### Nima (Apr 21 2018 at 08:04):

Are you pointing to the `α`

that is used in the goal?

#### Mario Carneiro (Apr 21 2018 at 08:04):

yes

#### Mario Carneiro (Apr 21 2018 at 08:04):

why are you "proving" alpha?

#### Mario Carneiro (Apr 21 2018 at 08:05):

you should write all the functions first, in term mode, and only enter tactic mode to justify the proof part of your partial function

#### Nima (Apr 21 2018 at 08:05):

It is supposed to be a function, not a proof.

I find it easier to go into tactic mode.

#### Mario Carneiro (Apr 21 2018 at 08:07):

You want to be careful about the dependency structure that the tactic creates

#### Nima (Apr 21 2018 at 08:08):

For example, here is a function in term mode.

def has_min : Prop := if ht : is_trivial c then number.has_min α else match dirk with | klower := is_strict c → ¬number.is_dense α ∧ ∀ hm:number.has_max α, get_bound c (not_trivial_is_not_ktrv c ht) < number.max hm | kupper := ∃ hm : number.has_min α, (is_strict c → (number.min hm) < (get_bound c (not_trivial_is_not_ktrv c ht))) end

Now suppose, `has_min`

is true. What is the value of `min`

? I have to first check triviality, then direction, then whether or not alpha is dense, then ...

Every one of these gives me a different function that I should use to find minimum value. So I entered tactic mode.

#### Mario Carneiro (Apr 21 2018 at 08:08):

For example with your if then else function from before:

def f (c:check) : nat := if h : p then f₁ (begin ... end) else f₂ (begin ... end)

you should enter tactic mode for the proof part but not while determining which function to call

#### Mario Carneiro (Apr 21 2018 at 08:11):

I already mentioned before that you are making your life harder with this encoding, you really want to encode this in the structure of your inductive types. You would be better served encoding `has_min`

as an inductive type as well

#### Mario Carneiro (Apr 21 2018 at 08:16):

Have you considered using `roption`

? It encodes a pair of a proof and a partial function, which makes it easy to write super dependent partial functions like this

#### Nima (Apr 21 2018 at 08:21):

Nope, I have to look into `roption`

.

#### Mario Carneiro (Apr 21 2018 at 08:36):

Why do you use so many decidable propositions instead of bools for your work? Usually the answer is convenience but it's clearly not helping you

#### Nima (Apr 21 2018 at 08:50):

Not sure, practice ;) or avoiding coe as much as possible

#### Mario Carneiro (Apr 21 2018 at 09:03):

What do you think of having the `number`

fields like this? I find that using `option`

makes the proofs and statements much easier

def has_in_between {α} [has_lt α] (x y : α) := ∃ z : α, x < z ∧ z < y class number (α:Type*) extends decidable_linear_order α := [nonempty_decidable : decidable (nonempty α)] (arbitrary : ∀ [nonempty α], α) [subsingleton_decidable : decidable (subsingleton α)] (min : option α) (max : option α) (min_prop : ∀ a, a ∈ min ↔ ∀ m:α, a ≤ m) (max_prop : ∀ a, a ∈ max ↔ ∀ m:α, m ≤ a) (next : α → option α) (next_prop : ∀ x y, y ∈ next x ↔ x < y ∧ ∀ z:α, z ≤ x ∨ y ≤ z) (prev : α → option α) (prev_prop : ∀ x y, y ∈ next x ↔ x < y ∧ ∀ z:α, z ≤ x ∨ y ≤ z) (is_dense : bool) (is_dense_prop : if is_dense then ∀ x y : α, x < y → ∃ z : α, x < z ∧ z < y else (∀ x ∉ max, ∃ y, y ∈ next x) ∧ (∀ x ∉ min, ∃ y, y ∈ prev x)) [has_in_between_decidable : ∀ x y : α, decidable (has_in_between x y)] (zero : option α) (neg₀ : α → option α) (add₀ : α → α → option α) (mul₀ : α → α → option α) (sub₀ : α → α → option α) (div₀ : α → α → option α) (neg₁ : α → option α) (add₁ : α → α → option α) (mul₁ : α → α → option α) (sub₁ : α → α → option α) (div₁ : α → α → option α)

#### Nima (Apr 21 2018 at 09:10):

They used to be like this.

The reason I separated `min`

and `has_min`

is just for performance of the final **hypothetical** code.

`has_min`

is never slower than `min`

, but it is quite possible for it to be faster.

For example,

def has_inf : Prop := if is_satisfiable c then is_bounded_left c else number.has_max α def inf (h: has_inf c) : α := if hsat : is_satisfiable c then let hbl := eq.mp (if_pos hsat) h in if ht : is_trivial c then number.min (hbl (or.inl ht)) else if hd : dirk = kupper then number.min (hbl (or.inr hd)) else get_bound c (not_trivial_is_not_ktrv c ht) else number.max (eq.mp (if_neg hsat) h)

#### Mario Carneiro (Apr 21 2018 at 09:13):

when will knowing `has_inf`

make computation of `inf`

faster?

#### Mario Carneiro (Apr 21 2018 at 09:14):

A quick and simple addition to allow for faster implementations of `has_min`

is the following extra field:

[has_min : decidable min.is_some]

#### Nima (Apr 21 2018 at 09:15):

I did not say using `has_inf`

makes `inf`

faster, suppose all I want is `has_inf`

. If I use option, I have to call `inf`

. But `has_inf`

could have been implemented faster.

#### Mario Carneiro (Apr 21 2018 at 09:16):

or you could do it in two stages with a `bool`

function:

(has_min : bool) (has_min_prop : has_min = min.is_some)

#### Mario Carneiro (Apr 21 2018 at 09:17):

that way it won't interfere with the definition of `min`

or `inf`

or whatever

#### Nima (Apr 21 2018 at 09:17):

May be we mean different things by `implementation`

. I mean non-lean code, more specifically C++. If I did not care about performance, I would never consider C++.

#### Mario Carneiro (Apr 21 2018 at 09:19):

I care about performance more than most lean users, indeed I'm writing a compiler and we have to think about these things. But the extra hypothesis parameter is not as erasable as it appears at first

#### Nima (Apr 21 2018 at 09:20):

Are you talking about `(h: has_inf c)`

as a parameter to `inf`

?

#### Mario Carneiro (Apr 21 2018 at 09:20):

yes

#### Mario Carneiro (Apr 21 2018 at 09:20):

How do you intend to relate the lean code you are writing to C++? This affects performance considerations

#### Mario Carneiro (Apr 21 2018 at 09:21):

Is this code to be `#eval`

d? Compiled to C++ and then run? Used only for correctness verification?

#### Nima (Apr 21 2018 at 09:27):

But that is for `inf`

and not `has_inf`

.

Right now I know nothing about automatic code generation in lean. I doubt it does exactly what I wish (not sure what exactly that is either). For example, if I have a constraint, I want it to be mutable. If I define addition of two constraints, there is going to be 5 (I guess) additions, but in lean I will have only one. So mostly manual transformation. That could also be a reason why I am not a fan of `match`

in lean. I don't know any formal semantics for c++, so not much into verification/validation. But I was thinking about an interval that support both strict and non-strict constraint in both dynamic and static, and realized that is too much for me to verify on my mind. So it would be nice if I can prove the operations first (on a scratch paper) and then at least be sure about the correct behavior.

Last updated: May 11 2021 at 00:31 UTC