Zulip Chat Archive

Stream: general

Topic: cases fails on exists


view this post on Zulip 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 _
 α

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 21 2018 at 08:02):

here it's okay because false : Prop

view this post on Zulip Mario Carneiro (Apr 21 2018 at 08:02):

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

view this post on Zulip 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

view this post on Zulip Nima (Apr 21 2018 at 08:04):

Are you pointing to the α that is used in the goal?

view this post on Zulip Mario Carneiro (Apr 21 2018 at 08:04):

yes

view this post on Zulip Mario Carneiro (Apr 21 2018 at 08:04):

why are you "proving" alpha?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 21 2018 at 08:07):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Nima (Apr 21 2018 at 08:21):

Nope, I have to look into roption.

view this post on Zulip 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

view this post on Zulip Nima (Apr 21 2018 at 08:50):

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

view this post on Zulip 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 α)

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 21 2018 at 09:13):

when will knowing has_inf make computation of inf faster?

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 21 2018 at 09:17):

that way it won't interfere with the definition of min or inf or whatever

view this post on Zulip 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++.

view this post on Zulip 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

view this post on Zulip Nima (Apr 21 2018 at 09:20):

Are you talking about (h: has_inf c) as a parameter to inf?

view this post on Zulip Mario Carneiro (Apr 21 2018 at 09:20):

yes

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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