Inferring `tail([])=[]`

[EmilyOng]

let rec iter xs =
  match xs with
  | [] -> []
  | x :: xs1 -> iter xs1

let iter_example ()
(*@ ens res=[] @*)
= iter []

Proof sketch:

[unfold iter]

iter(xs,res) ==
    (* base case *)
    Norm(is_nil(xs)=true/\res=[])
    (* inductive case: note that head(xs) is removed from normalization *)
    \/ ex v1 xs1; ens tail(xs)=xs1/\is_cons(xs)=true; iter(xs1, v1); Norm(res=v1)

[then, proceed on base case and inductive case]

Base case: ex v18; req emp; iter([], v18); req emp; Norm(res=v18) <: req emp; Norm(res=[])

• [substitute LHS with the unfolding] ex v18; req emp; Norm(is_nil([])=true/\res=[])
• [VCs for precondition] nothing
• [VCs for postcondition] is_nil([])=true/\res=[] => res=[]

Inductive case: ex v18 v33; req emp; ens tail([])=v33/\is_cons([])=true; iter(v33, v18); req emp; Norm(res=v18) <: req emp; Norm(res=[]) (direct substitution with the unfolding)

• Increasing unfolding_bound will not help

  ran out of tricks to make effect stage iter and normal stage match | _1371
  lemmas: {}
  predicates: {iter -> iter(xs,res) == Norm(is_nil(xs)=true/\res=[]) \/ ex v1 xs1; ens tail(xs)=xs1/\is_cons(xs)=true; iter(xs1, v1); Norm(res=v1)}
  predicates left: {}
  predicates right: {}
  q_vars: [v18]
  unfolded: [(iter, L)]
  applied: []
  fvenv: <...>

[dariusf]

This is the same problem as the one you encountered for quicksort. In the inductive case, is_cons([])=true is false, so we have ens false; ... with some other stages after. The proof then fails because entailment between flows is only defined when they have the same length.

The solution is to normalize ens false; ... to ens false, because ens false models an unreachable/nonterminating program state, so whatever comes after shouldn't matter. We can then (vacuously) prove false => res=[]. I just pushed this fix.

[EmilyOng]

Ooh, I see, thanks for responding!