There is a bug in how nested let patterns with the same variable names are substituted under certain circumstances, which leads to unsoundness.
Reproduction:
require import List AllCore.
op dupl (pkt : int) = (pkt, 0) axiomatized by duplE.
op a: int list = [1; 1] axiomatized by aE.
op b: int = 0 axiomatized by bE.
op f (a b c: int): int = a + b + c axiomatized by fE.
lemma phoo1 :
foldl
(fun (accum : int)
(b : int) =>
let (fst, _) = dupl accum in
f fst accum b)
b (rcons a b) = 11.
proof.
rewrite foldl_rcons.
iota.
case _: (dupl _) => fst tmp H.
zeta.
rewrite aE bE => /=.
rewrite duplE => /=.
rewrite duplE => /=.
rewrite !fE.
simplify.
rewrite duplE aE bE in H.
move: H.
move => /=.
rewrite !duplE.
have H1: (let (fst1, _) = (0, 0) in f fst1 0 1) = f 0 0 1 by done.
rewrite H1.
have H2: (let (fst0, _) = (f 0 0 1, 0) in f fst0 (f 0 0 1) 1) = f (f 0 0 1) (f 0 0 1) 1 by done.
rewrite H2.
rewrite !fE.
simplify.
move => />.
qed.
lemma phoo2 :
foldl
(fun (accum : int)
(b : int) =>
let (fst, _) = dupl accum in
f fst accum b)
b (rcons a b) = 6.
proof.
rewrite aE bE foldl_rcons. zeta. iota. iota.
rewrite !duplE.
have H0: (let (fst0, _) = (0, 0) in f fst0 0 1) = f 0 0 1.
- smt().
rewrite H0.
have H1: (let (fst0, _) = (f 0 0 1, 1) in
f fst0 (f 0 0 1) 1) = f (f 0 0 1) (f 0 0 1) 1.
- smt().
rewrite H1.
simplify.
rewrite !fE.
trivial.
qed.
lemma bad: 6 = 11 by rewrite -phoo1 -phoo2.
Related example that runs into assertion failure:
(* This snippet appears to do something strange *)
lemma phoo1 :
foldl
(fun (accum : int)
(b : int) =>
let (fst, _) = dupl accum in
f fst accum b)
b (rcons a b) = 11.
proof.
rewrite foldl_rcons.
iota.
case _: (dupl _) => fst tmp H.
zeta.
rewrite aE bE => /=.
rewrite duplE => /=.
rewrite duplE => /=.
rewrite !fE.
simplify.
rewrite duplE aE bE in H.
move: H.
move => /=.
rewrite !duplE => /=.
There is a bug in how nested let patterns with the same variable names are substituted under certain circumstances, which leads to unsoundness.
Reproduction:
Related example that runs into assertion failure: