Solving X<>Y

[AdamBJ]

To solve the proof below I used update_neq:

1 subgoals
n : nat
st : id -> nat
H : st X = 0 /\ st Y = 0
st' : state
H0 : par_loop / st ==>c* par_loop / st' /\ st' X = n /\ st' Y = 0
H1 : par_loop / st ==>c* par_loop / st'
H2 : st' X = n /\ st' Y = 0
H3 : st' X = n
H4 : st' Y = 0
______________________________________(1/1)
update st' X (S n) Y = 0

| V

st' Y = 0
______________________________________(2/2)
X <> Y

| V

X <> Y

And here I'm stuck. How can I show that X!=Y?

[alkaza]

Try destruct (eq_id_dec X Y).

[AdamBJ]

That did it! Thanks:)

[jaewooklee93]

I prefer

unfold update. simpl. omega.

[woong8556]

And I prefer

intro H. inversion H.

To be specific, I use the following often:

apply update_neq; try intro Hx; try inversion Hx.