feature request: bool/prop hypthesis canonicalization

[andres-erbsen-sifive]

we should probably decide on some convention for the hypotheses format that our tactics support, and then write a tactic that translates obvious variants into that format. For example, getBool (weq x $0) can come from symbolic execution of kami code and I tend to state my invariants in terms of Logic.eq, e.g. x <> $0 or word.unsigned x <> 0%Z.

Is there something of this sort already?

One way of doing this: https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/Decidable/Bool2Prop.v

[whonore]

I've been using a somewhat ad-hoc tactic to do this but I agree it would be nice to have a more systematic approach.

Ltac simpl_bool :=
  repeat match goal with
  | H: _ && false = _ |- _ => rewrite andb_false_r in H
  | H: _ || true = _ |- _ => rewrite orb_true_r in H
  | H: _ && _ = true |- _ => rewrite andb_true_iff in H; destruct H
  | H: _ || _ = true |- _ => rewrite orb_true_iff in H
  | H: negb _ = _ |- _ => rewrite ?negb_true_iff, ?negb_false_iff in H
  | H: getBool (wlt_dec _ _) = true |- _ => apply wlt_dec_true in H
  | H: getBool (wlt_dec _ _) = false |- _ => apply wlt_dec_false in H
  | H: getBool (weq _ _) = true |- _ => apply weq_true in H
  | H: getBool (weq _ _) = false |- _ => apply weq_false in H
  end.

[andres-erbsen-sifive]

Where are weq_true and weq_false from? grep in my RiscvSpecFormal checkout turned out nothing.

[whonore]

Oh sorry, they're lemmas I made.

Lemma weq_true : forall sz (w1 w2: word sz), getBool (weq w1 w2) = true <-> (w1 = w2)%word.
Proof. intros *; now destruct (weq _ _). Qed.

And similarly for weq_false, wlt_dec_true, wlt_dec_false.

[andres-erbsen-sifive]

Indeed, I believe these lemmas are not difficult. Eventually we should probably consolidate such code in the Kami open-source repository though, right?

[whonore]

Yes I think that would make sense.