Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC