Zulip Chat Archive

Stream: new members

Topic: removing ite


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

view this post on Zulip Johan Commelin (May 15 2020 at 14:10):

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

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

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

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

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

view this post on Zulip Reid Barton (May 15 2020 at 14:42):

Oh yes I see, sorry.

view this post on Zulip Reid Barton (May 15 2020 at 14:43):

You need a lemma next: rw if_pos,

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

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

view this post on Zulip Reid Barton (May 15 2020 at 14:55):

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

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

view this post on Zulip Mario Carneiro (May 15 2020 at 14:57):

Anyway, simp should be able to clean up this goal

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

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