Usage of Lemmas - Githubissues


let rec length lst =
  match lst with
  | [] -> 0
  | x :: xs -> 1 + length xs

(*@
  lemma length_empty res =
    length([], res) <: ens res=0
@*)

let rec snoc lst x =
  match lst with
  | [] -> [x]
  | y :: ys -> y :: snoc ys x

let snoc_empty_length x
(*@ ens res=1 @*)
= length (snoc [] x)

Error trace

``` Fatal error: exception Invalid_argument("List.map2") Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45 Called from Hipprover__Entail.unify_lem_lhs_args in file "parsing/entail.ml", line 39, characters 9-45 ``` In the following flow: ``` ex v103 v104 v72; req emp; ens is_nil([])=true/\v72=cons(x, [])/\tail(v72)=v104/\is_cons(v72)=true; length(v104, v103); ex v70; req emp; Norm(res=1+v103) <: req emp; Norm(res=1) ``` Unification between lemma args (`[]`) (missing `res`) and concrete args (`v104`, `v103`) fails due to an unhandled invalid argument exception, because of incompatible lengths for `List.map2`.

EmilyOng / AlgebraicEffect

Usage of Lemmas #9