## Stream: new members

### Topic: removing ite

#### Alcides Fonseca (May 15 2020 at 14:08):

First of all, this community has been really helpful in learning lean.

I have a small issue related to decidability, which I cannot get my head around.
I am including a small part of my code (and I hoped for it to be even smaller, but to no avail).

In the second-to-last sorry, I cannot rewrite ite tt, and it shows a little uparrow before tt. I understand it is complaining it cannot be decidable. However, I would like just to branch on the decision. Is this not possible?

inductive symbol : Type
| name : nat -> symbol

inductive heap : Type
| empty : heap
| happend : symbol → int → heap → heap

open heap

def same_name : symbol → symbol → bool
| (symbol.name a) (symbol.name b) := a = b

def find : heap → symbol → int
| empty _ := 0
| (happend name v h) oname := if same_name name oname then v else find h oname

theorem lookup_is_always_ok  (h:heap) (n:symbol) : ∃ (i:int), find h n = i :=
begin
induction h,
{
existsi (0 : int),
rw find,
},
{
by_cases same_name h_a n = tt,
{
rw find,
rw h,
sorry,
},
{
sorry
}
}
end


#### Johan Commelin (May 15 2020 at 14:10):

You can always do it anyway by starting your proof with classical,

#### Reid Barton (May 15 2020 at 14:11):

That's unnecessary in this case though--ite on a coerced bool is really just doing cases on the bool.

#### Alcides Fonseca (May 15 2020 at 14:25):

Johan Commelin said:

You can always do it anyway by starting your proof with classical,

Unfortunately it does not work in my lean installation:

unknown identifier 'classical'


However, I do open classical in my program and the result is the same.

#### Reid Barton (May 15 2020 at 14:32):

I'm not sure I remember the syntax, but I think you just want something like cases H : same_name h_a n.

#### Alcides Fonseca (May 15 2020 at 14:35):

It has exactly the same behaviour. If I go on by rewriting ite, I get something like:

∃ (i : ℤ),
decidable.rec_on (bool.decidable_eq ff tt) (λ (hnc : ¬↥ff), find h_a_2 n) (λ (hc : ↥ff), h_a_1) = i


Which I am enable to get rid of, even rewriting bool.decidable_eq.

#### Reid Barton (May 15 2020 at 14:42):

Oh yes I see, sorry.

#### Reid Barton (May 15 2020 at 14:43):

You need a lemma next: rw if_pos,

#### Reid Barton (May 15 2020 at 14:44):

Alternatively, if you used bool.rec_on instead of if-then-else (since you really have a bool to start with anyways), you could just reduce it.

#### Alcides Fonseca (May 15 2020 at 14:49):

Reid Barton said:

Oh yes I see, sorry.

Using if_pos creates a second goal for tt, which I cannot get to.

1 goal
n h_a : symbol,
h_a_1 : ℤ,
h_a_2 : heap,
h_ih : ∃ (i : ℤ), find h_a_2 n = i,
h : same_name h_a n = tt
⊢ ↥tt


I am afraid I might be mixing the interpreter, with reasoning about it (bool vs Prop).

#### Reid Barton (May 15 2020 at 14:55):

↥tt is true, and the proof of true is trivial.

#### Mario Carneiro (May 15 2020 at 14:56):

Alcides Fonseca said:

Johan Commelin said:

You can always do it anyway by starting your proof with classical,

Unfortunately it does not work in my lean installation:

unknown identifier 'classical'


However, I do open classical in my program and the result is the same.

Do you have mathlib? import tactic will give you the classical tactic

#### Mario Carneiro (May 15 2020 at 14:57):

Anyway, simp should be able to clean up this goal

#### Alcides Fonseca (May 15 2020 at 15:01):

Mario Carneiro said:

Anyway, simp should be able to clean up this goal

simp did work! Thank you very much!

I guess I didn't try it as I though the problem was more complex than it actually way!

#### Reid Barton (May 15 2020 at 15:05):

It is true that you are mixing Prop and bool a bit (a = b in the definition of same_name is a Prop, but it gets coerced to bool using the decidability of equality on nat; then in if same_name ... it gets coerced back into a Prop) but this is fine, and normal style if you really intend to do it.

Last updated: May 14 2021 at 04:22 UTC