Hi,

I've observed a failure of `rewrite`

which puzzles me.

In a proof, after having written these commands to the 2nd-to-last line. The `destruct ... eqn:cond_val`

is supposed to take care of a boolean condition which occurs in the outermost `if`

of the variable `res`

.

```
destruct (Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level) era1.(Level_repr.cycle_era.first_level) &&
Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle) era1.(Level_repr.cycle_era.first_cycle)) eqn:cond_val.
{ reflexivity. } { (**** the local context here is below ***)
Fail rewrite cond_val in res. }
```

I have this in the local contex:

```
res: (let? ' _
:= (if
Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level) era1.(Level_repr.cycle_era.first_level) &&
Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle) era1.(Level_repr.cycle_era.first_cycle)
(*** above, the boolean that I save and destruct ***)
then
(fix aux (era : Level_repr.cycle_era) (older_eras : list Level_repr.cycle_era) {struct older_eras} : M? unit :=
match older_eras with
| [] => return? tt
| previous_era :: even_older_eras =>
if
Raw_level_repr.op_gt era.(Level_repr.cycle_era.first_level) previous_era.(Level_repr.cycle_era.first_level) &&
Cycle_repr.op_gt era.(Level_repr.cycle_era.first_cycle) previous_era.(Level_repr.cycle_era.first_cycle)
then aux previous_era even_older_eras
else Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
end) era1 cycle_eras
else Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt))
in return? (era0 :: era1 :: cycle_eras)) = V0.Pervasives.Ok l
cond_val: Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level) era1.(Level_repr.cycle_era.first_level) &&
Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle) era1.(Level_repr.cycle_era.first_cycle) = true
1/1
false = true
```

So, how come the `rewrite cond_val in res.`

fails whereas the left-hand side of `cond_val`

occurs explicitly in `res`

?

Btw, for some reason, this works with the case

```
destruct (_ && _) eqn:cond_val in res. { assumption. }
{ inversion res. }
```

but I would like to understand what is wrong.

Note: this takes place in the CoqTezosOfOCaml project and this specific codes handles an error monad, but I don't think (perhaps I'm wrong) that this could be relevant here...

... in absence of better answers, have you tried refolding that `fix`

point? Unfolded fixpoints are uncommon, and this one has a partial match for your pattern

also, reposting the goal after (EDIT)

```
set (C1 :=
Raw_level_repr.op_gt
era0.(Level_repr.cycle_era.first_level)
era1.(Level_repr.cycle_era.first_level)).
set (C2 :=
Cycle_repr.op_gt
era0.(Level_repr.cycle_era.first_cycle)
era1.(Level_repr.cycle_era.first_cycle)).
```

etc _might_ make it more readable (and fit the screen)...

Especially because the next step is checking if `cond_val`

's LHS _actually_ occurs in `res`

— all we see is a term with the same pretty-printing, but as `Set Printing All`

reminds us, Printing isn't injective...

Whether that's "equal", and what's the appropriate meaning of equal (syntactic equality, unification according to some algorithm, ...), varies...

I edited the suggestion above, because I was the syntax for ssreflect's `set`

not plain `set`

, and ssreflect set is fancier and does not search for occurrences using syntactic equality, but a form of unification (https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#coq:tacn.set-(ssreflect)).

Thank your for your answer! I did your suggestion i.e. `Set Printing All`

but the conditions where exactly the same, so this was not a pretty printing issue.

However, what solved the problem was to `destruct`

the records `era`

and `era0`

which contain the integers I was trying to compare, doing a `simpl`

and the goal could be easily solved. I don't know if refolding the fixpoint would have the same effect

are first_level or first_cycle primitive projections? it may happen that they don't match due to the hidden unfolding state

Gaëtan Gilbert said:

are first_level or first_cycle primitive projections? it may happen that they don't match due to the hidden unfolding state

Yes, they are.

You mean that they could be implicitly unfolded in one occurrence and folded in another in the same local environment?

yes

So I guess that `destruct (_ && _) eqn:cond_val in res. `

works because unification triggers some evaluation. That's it?

I don't know

Coq has at least two unification algorithms and a bunch of options, so an unspecified difference between these two tactics is within the realm of what Coq's currently entitled to do

Last updated: Jan 29 2023 at 01:02 UTC