## 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?

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?

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 #evald? 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