Skip to content

spurious Hoare logic match error connected to simplification hints #775

@alleystoughton

Description

@alleystoughton
(* below is a problem with the Hoare logic match tactic
   (there is an identical problem with the one-sided match
   of pRHL)

   taking out either of the simplification hints removes
   the error *)

type ('a, 'b) epdp = {enc : 'a -> 'b; dec : 'b -> 'a option}.

op valid_epdp (epdp : ('a, 'b) epdp) : bool =
  (forall (x : 'a), epdp.`dec (epdp.`enc x) = Some x) /\
  (forall (y : 'b, x : 'a), epdp.`dec y = Some x => epdp.`enc x = y).

lemma epdp_enc_dec (epdp : ('a, 'b) epdp, x : 'a) :
  valid_epdp epdp => epdp.`dec (epdp.`enc x) = Some x.
proof.
rewrite /valid_epdp => [[enc_dec _]].
by rewrite enc_dec.
qed.

hint simplify [reduce] epdp_enc_dec.

op my_epdp : (int, int) epdp.

axiom valid_my_epdp : valid_epdp my_epdp.

hint simplify [eqtrue] valid_my_epdp.

module M = {
  proc f(m : int) : unit = {
    match (my_epdp.`dec m) with
    | None => {}
    | Some x => {}
    end;
  }
}.

lemma foo :
  hoare [M.f : m = my_epdp.`enc witness ==> true].
proof.
proc.
(*
Current goal

Type variables: <none>

------------------------------------------------------------------------
Context : {m : int}

pre = m = my_epdp.`enc witness

(1)  match (my_epdp.`dec m) with
(1)  | None => {                
(1)  }                          
(1)  | Some x => {              
(1)  }                          

post = true
*)
match.
(* error:
cannot clear x that is/are used in the conclusion
*)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions