imandra-ai / imandra-docs Goto Github PK

• integer syntax compiles to Z.t (Imandra's int), floating syntax compiles to Q.t (Imandra's real)
• syntax extensions for ocaml integers and floats are <n>i and <n>p
• Int/Real modules
• gotchas about reasoning over Floats

Imandra's logic is purely computational, without existential quantifiers.
In order to prove forall x exists y s.t. phi(x,y), you define a computable witnessing Skolem function f(x) and use Imandra to prove forall x (phi(x, f(x)))

How to use the existing plugins/make new ones

Imandra cannot generally synthesize induction schemes for mutually recursive functions, a lot of of the times in the presence of mutually recursive functions, induction would just never work.

Users can provide induction schemes manually (using a custom functional induction scheme), but usually it's much better (if possible) to write in a style that doesn't require mutual recursion (especially in higher order position)

Request from @ignaden

https://docs.imandra.ai/

The DiscoverBalancedTrees notebook is no longer compatible with the new version of Imandra. @Bronsa suspects it might have something to do with recent changes to the Gen_rand module.

I've reverted the Imandra version upgrade commit in the short term as we want to release something else, but this will be re-applied on the next imandra-dist release.

From a proof-theoretic perspective, Imandra's logic is effectively a typed version of PRA (Skolem's Primitive Recursive Arithmetic) extended with Transfinite Induction up to the ordinal epsilon_0.
It's a multisorted first-order logic, but Imandra has various niceties that allow it to handle a 'specializable' fragment of Higher-Order Logic

Since in Imandra everything is a program, all judgments are computational and because we live in a quantifier-free world of discrete combinatorial structures, we can admit classical logic and still obtain results that are constructively valid

In Imandra's logic all functions must be total and terminating, extension to the logic are accepted via defining new types or functions validated by Imandra's definitional principle, which analyses definitions to ensure they are admissible, to ensure that any extension by definitions is a conservative extension.

For exception-raising functions like List.hd, List.tl and /, Imandra has a semantics that under-specifies them, allowing them to take on any value in their 'exceptional' cases

Whenever you have an explicit equality hypothesis between a variable and a non-variable term that doesn't contain it, that leads to an 'explicit substitution' that eliminates the variable - that's so that we have minimal hypotheses before an induction.
In certain cases, this can lead to Imandra removing "manual" destructor elimination, and thus failing to automatically prove a goal by induction.

A key takeaway is, if you have a goal that is going to be proved by induction, always try to make it as strong as possible. As much as possible, you never want to have spurious hypotheses in something you're proving by induction, because then your inductive hypotheses are weaker.

using #allow_full_ho true

e.g. given

type t = { x : unit list; y : unit list }
let length a = List.length a.x + List.length a.y
let rec g xs =
  match xs.x, xs.y with
  | _::x, y when List.length xs.x > List.length xs.y ->
    Some {x;y}
  | x,_::y ->
    g {x;y}
  | _ -> None

we can do

lemma g_len xs =
  match g xs with
  | None -> true
  | Some xs' ->
    length xs' < length xs
[@@fc] [@@auto]
let rec f xs =
  match g xs with
  | None -> ()
  | Some xs ->
    f xs
[@@measure Ordinal.of_int (length xs)]
[@@disable length]

or

let rec f xs =
  match g xs with
  | None -> ()
  | Some xs ->
    f xs
[@@measure Ordinal.of_int (length xs)]
[@@validate_induct]