ghulette

(* Let's look at the Ackermann-Peter function, the canonical example of a
total computable function that is not primitive recursive. As such it should
be possible to write it as a computation in Gallina but the normal Fixpoint
termination check won't work.

The function can be defined case-wise:
A(0, n)     = n+1
A(m+1, 0)   = A(m, 1)
A(m+1, n+1) = A(m,A(m+1,n))

ghulette

#[derive(Debug)]
pub struct Point<T> {
    pub x: T,
    pub y: T,
}

impl<T> Point<T> {
    pub fn new(x: T, y: T) -> Self {
        Point { x, y }
    }

ghulette

SPECIFICATION Spec

INVARIANT TypeInv
PROPERTY EventuallyC

ghulette

(*
$ ocamlopt tail.ml
$ ./a.out 100000
length (tail call) executed in 0.000256s
length (while loop) executed in 0.000366s
length (recursive) executed in 0.001092s
$ ./a.out 100000000
length (tail call) executed in 0.255737s
length (while loop) executed in 0.272046s
length (recursive) died

ghulette

Require Import ZArith.
Require Import Coq.Lists.List.
Require Import Omega.
Import ListNotations.
Local Open Scope Z_scope.

Inductive is_sum : list Z -> Z -> Prop :=
| is_sum_nil : is_sum [] 0
| is_sum_cons : forall y n ns, is_sum ns y -> is_sum (n::ns) (n + y).

ghulette

(* nats = 0 :: List.map (fun x -> x+1) nats *)

type 'a lazylist =
  | Nil
  | Cons of 'a * (unit -> 'a lazylist)

let rec take n l =
  match (n,l) with
  | 0,_ -> []
  | _,Nil -> []

ghulette

type formula =
  | False
  | True
  | Atom of string
  | Not of formula
  | And of formula * formula
  | Or of formula * formula

let is_lit = function
  | Atom _ | Not (Atom _) -> true

ghulette

Require Import Coq.Logic.Classical.

Theorem conj_iff :
  forall P Q, P /\ Q <-> ~(P -> ~Q).
Proof.
  split.
  unfold not.
  intros (HP,HQ) H.
  apply H.
  apply HP.

ghulette

open Printf
(* Labeled arguments, the easy way *)

let _ =
  (* Declare a function with labeled arguments like this: *)
  let f ~x ~y = x + y in
  (* Type: f : x:int -> y:int -> int *)
  (* Call it like this: *)
  printf "%d\n" (f ~x:5 ~y:6);

ghulette

(*******************************************************************************

   Getting a backtrace out of ocaml is not completely obvious. You
   have to compile the code with -g and then run with OCAMLRUNPARAM=b,
   like this:

   $ ocamlc -g -o test test.ml
   $ OCAMLRUNPARAM=b ./test
   backtrace_status: true
   Failure("nth")