Cop2.eqb_type_refl

[andrew-appel]

Cop2.eqb_type_refl should probably end with Defined rather than Qed.

The symptom is that entailer! sometimes returns subgoals like this, which should have simplified away.

(if
  eqb_type (tarray (tarray tuchar fec_max_cols) fec_max_h)
    (tarray (tarray tuchar fec_max_cols) fec_max_h)
 then v_s = v_s
 else Wrong_type_for_lvar_variable _s) /\
(if
  eqb_type (tarray (tarray tuchar (fec_max_h * 2)) fec_max_h)
    (tarray (tarray tuchar (fec_max_h * 2)) fec_max_h)
 then v_v = v_v
 else Wrong_type_for_lvar_variable _v)

[andrew-appel]

What I meant to say was, Cop2.eqb_type should probably... , not Cop2.eqb_type_refl. And in fact, Cop2.eqb_type is defined transparently, so that is not the bug. The illustrated goal, a residual goal of entailer!, is caused by the fact that fec_max_cols is an opaque constant, so that eqb_type cannot solve it by computation.

If there is something to be done here, it would be to rewrite by eqb_type_refl in the entailer, perhaps.

[andrew-appel]

P.R. #554 fixes this by adding a rewrite rule to the entailer_rewrite database.