Normalizer has weird behavior with one-element lists (again)

[TWal]

Following the resolution of #3353, I can now use my squash (norm ...) construct in my proofs, however, I need to prove it first! I am again noticing a weird behavior when the list has only one element, see below:

// true when all elements of a list satisfy a predicate
let rec for_allP (#a:Type) (pre:a -> prop) (l:list a): prop =
  match l with
  | [] -> True
  | h::t -> pre h /\ for_allP pre t

// a type, a predicate on that type, and some values
assume val ty: Type0
assume val pre: ty -> prop

assume val v1: ty
assume val v2: ty
assume val v3: ty

// some useful lemma
assume val all_pre_lemma:
  l:list ty ->
  Lemma (for_allP pre l)

let all_v = [ v1; v2; v3 ]

// We want to have the normalization of `all_pre_lemma`'s post-condition in the context
// This works well
#push-options "--fuel 0 --ifuel 0"
val all_v_pre: squash (norm [delta_only [`%all_v; `%for_allP]; iota; zeta] (for_allP pre all_v))
let all_v_pre =
  all_pre_lemma all_v;
  norm_spec [delta_only [`%all_v; `%for_allP]; iota; zeta] (for_allP pre all_v)
#pop-options

assume val v4: ty

// But when the list only has one element...
let all_v_one = [ v4; ]

// this fails without fuel
#push-options "--fuel 0 --ifuel 0"
val all_v_one_pre: squash (norm [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one))
let all_v_one_pre =
  all_pre_lemma all_v_one;
  norm_spec [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one)
#pop-options

The workaround is to use a fuel of 1, which is not too bad, but I am still posting this issue for posterity.

Another workaround is this:

#push-options "--fuel 0 --ifuel 0"
val all_v_one_pre: squash (norm [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one))
let all_v_one_pre =
  all_pre_lemma all_v_one;
  norm_spec [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one);
  let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in
  dumb_lemma (for_allP pre all_v_one) (norm [delta_only [`%all_v_one; `%for_allP]; iota; zeta] (for_allP pre all_v_one))
#pop-options

[mtzguido]

Nice example! I think the problem is that the associated VC for this program is:

* Info at Bug3360.fst(46,0-49,4):
 - Checking VC:
   forall (pure_result: Prims.unit).
     Bug3360.for_allP Bug3360.pre Bug3360.all_v_one ==>
     (forall (pure_result: Prims.unit).
         Prims.auto_squash (Bug3360.pre Bug3360.v4) ==
         Bug3360.for_allP Bug3360.pre Bug3360.all_v_one ==>
         Prims.auto_squash (Bug3360.pre Bug3360.v4))

Which is roughly of the shape P ==> (P = Q) ==> Q, which should be trivial. But... in formula position (the last Q) the encoding will peel away the auto_squash as a simplication, but this will not happen in term position for the equality. So at the SMT level, we get something like:

Valid (allP ....) ==>
(allP ... == auto_squash (pre v4)) ==>
Valid (pre v4)

but we cannot conclude Valid (pre v4), only Valid (auto_squash (pre v4)).

I think this is roughly the same problem:

let min (p q : Type0) : Lemma (requires p /\ squash p == q) (ensures q) = ()

Replacing q in the post for squash p does work.