# Re: [isabelle] Calculation-style reasoning, reflexive equality, and strangeness

```On Tue, 14 Sep 2010, Simon Winwood wrote:

```
```Consider the following proof

lemma
"X = Y"
proof -
have "X = z" sorry
also have "\<dots> = z" by simp
also (* want X = z, get X = X *)

After the 'also', calculation is "X = X", rather than
the "X = z" you would expect.  We figured that the reason for
this is that the chaining rule is forw_subst

[| a = b; P b |] ==> P a

which, when unified with the above two rules gives P == %x. x = x
hence P X == X = X

```
I suppose this is a corner case, but it could be solved by trying trans before forw_subst.
```
```
The calculational system tries rules from the context in the given order (cf. print_trans_rules), and trans comes before forw_subst in the main HOL library as one would normally expect.
```
```
The reason why the intermediate reflexive step above is ignored is due to the policy to filter out results that do not make progress: composing trans with a reflexive result duplicates the original fact, so it is filtered out in the enumeration. This principle has been there in Isar calculations almost from the very beginning around 1999/2000 -- it allows more useful steps involving advanced substitution rules.
```

Makarius

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.