Stream: Coq users

Topic: Strange rewrite failure

Pierre Vial (Oct 17 2022 at 15:39):

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...

Paolo Giarrusso (Oct 18 2022 at 13:18):

... in absence of better answers, have you tried refolding that fixpoint? Unfolded fixpoints are uncommon, and this one has a partial match for your pattern

Paolo Giarrusso (Oct 18 2022 at 13:21):

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)...

Paolo Giarrusso (Oct 18 2022 at 13:23):

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...

Paolo Giarrusso (Oct 18 2022 at 13:29):

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)).

Pierre Vial (Oct 19 2022 at 09:32):

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

Gaëtan Gilbert (Oct 19 2022 at 09:40):

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

Pierre Vial (Oct 19 2022 at 12:19):

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?

Gaëtan Gilbert (Oct 19 2022 at 12:34):

yes

Pierre Vial (Oct 19 2022 at 12:48):

So I guess that destruct (_ && _) eqn:cond_val in res. works because unification triggers some evaluation. That's it?

Gaëtan Gilbert (Oct 19 2022 at 13:25):

I don't know

Paolo Giarrusso (Oct 19 2022 at 17:21):

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: Oct 13 2024 at 01:02 UTC