removing ite

Stream: new members

[Alcides Fonseca]

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]

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

[Reid Barton]

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

[Alcides Fonseca]

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]

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]

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]

Oh yes I see, sorry.

[Reid Barton]

You need a lemma next: rw if_pos,

[Reid Barton]

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]

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]

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

[Mario Carneiro]

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]

Anyway, simp should be able to clean up this goal

[Alcides Fonseca]

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]

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.