# OCaml code snippets proposed as CC-BY-SA 4.0 candidates

The idea is quite simple. There are many people lurking here that wish to write an OCaml book or tutorial or blogpost, however :

• either they miss the most illustrative ocaml code snippet
• or they know what the best code could be but there is a (potential) Statement of Rights violation

I want to help these people, starting with @dmbaturin and OCaml From the Ground Up.
I will publish here my own code as CC-BY-SA 4.0.
Also i will link to resources that are known to be CC-BY-SA 4.0-compatible.
And i invite you to post your own code as CC-BY-SA 4.0 so that it can be inspiring and used in educational material.

4 Likes

The excellent Alaska Ataca a Kamtchatka blog by MatĂ­as Giovannini is claimed (in right column) to be CC0 1.0.
Thus i guess all ocaml code here can be borrowed by a CC-BY-SA 4.0 book / tutorial.

I am specially interested by Braun heap and Polymorphic recursion with rank-2 polymorphism.

The Knight Tour problem backtracking
(This is my own original code)

Put a knight on a chessboard corner square. The knight tour problem is to jump from square to square until all chessboard squares have been visited exactly once.

``````let board =
Array.make_matrix 8 8 0

let bounded x y =
if x < 0 || x > 7 then false
else if y < 0 || y > 7 then false
else true

let print_board () =
Array.iter (fun a -> Array.iter
(fun k -> if k < 10 then print_char '0'; print_int k; print_char ' ') a;
print_newline ())
board

let rec forward_chaining n x y =
if bounded x y && board.(x).(y) = 0 then begin
board.(x).(y) <- n;
if n = 8 * 8 then
(print_board (); print_newline ())
else begin
forward_chaining (n + 1) (x + 1) (y + 2);
forward_chaining (n + 1) (x + 2) (y + 1);
forward_chaining (n + 1) (x + 2) (y - 1);
forward_chaining (n + 1) (x + 1) (y - 2);
forward_chaining (n + 1) (x - 1) (y - 2);
forward_chaining (n + 1) (x - 2) (y - 1);
forward_chaining (n + 1) (x - 2) (y + 1);
forward_chaining (n + 1) (x - 1) (y + 2);
end;
board.(x).(y) <- 0;
end

let () = forward_chaining 1 0 0
``````

This program prints all Knight Tour solutions until you are fed up and press Ctrl + C.
Note that` bounded x y && board.(x).(y)=0` is possible only because `&&` is semi-strict.

The 8-Queens problem backtracking, the OOP-style
(This code is an ocaml translation of a Little Smalltalk code example, unknown original author)

The 8-queens problem is to place 8 queens on a regular chessboard without any threatening possible.

``````let null_queen =
object
method first = false
method next = false
method check (x:int) (y:int) = false
method print = print_newline ()
end

class queen column (neighbor:queen) =
object (self)
val mutable row = 1
method check r c =
let diff = c - column in
(row = r) ||
(row + diff = r) || (row - diff = r) ||
neighbor#check r c
method private test =
try
while neighbor#check row column do
if not self#advance then raise Exit
done;
true
with
| Exit -> false
method first =
ignore(neighbor#first);
row <- 1;
self#test
method next =
if row = 8 then
(if neighbor#next then (row <- 1; true) else false)
else (row <- row + 1; true)
method  print : unit =
print_int row; print_char ' '; neighbor#print
end

let () =
let last = ref null_queen in
for i = 1 to 8 do
last := new queen i !last
done;
if !last#first then begin
!last#print;
while !last#next do
!last#print
done
end else
print_string "Zero solution."
``````

This program prints all 8-Queens 92 solutions.

The poker_hand algebraic datatype
(This is my own original code)

Algebraic datatypes are the bread and butter of functional programming. An algebraic datatype models a disjoint union set. Practically it is an enumeration of (optional) tuples.

``````type poker_hand =
| HighCard of int * int * int * int * int
| OnePair of int * int * int * int
| TwoPair of int * int * int
| ThreeOfAKind of int
| Straight of int
| Flush of int * int * int * int * int
| FullHouse of int * int
| FourOfAKind of int
| StraightFlush of int
``````

With the following card values :

``````# let ace,king,queen,jack = 50,40,30,20;;
val ace : int = 50
val king : int = 40
val queen : int = 30
val jack : int = 20
``````

Tuples values are from the strongest card value to the weakest card value. Now a poker hand can be compared to another poker hand :

``````HighCard(king,queen,jack,10,7) > HighCard(king,queen,jack,10,5);;
-: bool = true
OnePair(queen,king,jack,10) > OnePair(queen,king,jack,7);;
-: bool = true
FullHouse(queen,jack) > FullHouse(queen,10);;
-: bool = true
StraightFlush(8) > StraightFlush(6);;
-: bool = true
``````

A simple calculator
(Arguably not something revolutionary but this is my own original code)

``````type arithmetic =
| Int of int
| Neg of arithmetic
| Add of arithmetic * arithmetic
| Sub of arithmetic * arithmetic
| Mul of arithmetic * arithmetic
| Div of arithmetic * arithmetic

let rec eval = function
| Int n -> n
| Neg a -> - eval a
| Add(a,b) -> eval a + eval b
| Sub(a,b) -> eval a - eval b
| Mul(a,b) -> eval a * eval b
| Div(a,b) -> eval a / eval b
``````

A formal function deriver
(This is my own original code)

``````type function_x =
| X          (* the x variable *)
| R of float (* a real number  *)
| Sin of function_x
| Cos of function_x
| Tan of function_x
| Log of function_x
| Exp of function_x
| Power of function_x * float
| Add of function_x * function_x
| Mul of function_x * function_x

let factor = function
| R(1.),u -> u
| u,v -> Mul(u,v)

let product = function
| R(a),Mul(R(b),u) -> factor(R(a*.b),u)
| Mul(R(a),u),R(b) -> factor(R(a*.b),u)
| Mul(R(a),u),Mul(R(b),v) -> factor(R(a*.b),Mul(u,v))
| u,Mul(R(k),v) -> Mul(R(k),Mul(u,v))
| Mul(R(k),u),v -> Mul(R(k),Mul(u,v))
| u,v -> factor(u,v)

let rec derive = function
| X -> R(1.)
| R(k) -> R(0.)
| Mul(R(k),X) -> R(k)
| Mul(R(k),u) -> product(R(k),derive(u))
| Sin(u) -> product(derive(u),Cos(u))
| Cos(u) -> product(R(-1.),product(derive(u),Sin(u)))
| Tan(u) -> product(derive(u),Power(Cos(u),-2.))
| Log(u) -> product(derive(u),Power(u,-1.))
| Exp(u) -> product(derive(u),Exp(u))
| Power(u,2.) -> product(R(2.),product(derive(u),u))
| Power(u,a)  -> product(R(a),product(derive(u),Power(u,a-.1.)))
``````

The sketch of an ultra minimalist lisp-like interpreter
(Arguably not something revolutionary but this is my own original code)

``````type lexpr =
| Var of int
| Abs of lexpr
| App of lexpr * lexpr
| Let of lexpr * lexpr
| Fun of (lexpr -> lexpr)
| Int of int

let rec eval expr env =
match expr with
| Var n       -> List.nth env n
| Abs body    -> Fun (fun x -> eval body (x::env))
| App (f,arg) ->
( match eval f env with
| Fun f -> f (eval arg env)
| _ -> invalid_arg "Can't apply, not a function" )
| Let (e,body) -> eval body (eval e env::env)
| _ -> expr
``````

Simple calculator again, the exception-less style
(Arguably not something revolutionary but this is my own original code)

``````let ok1 v f =
match v with
| Ok x -> Ok (f x)
| Error _ -> v

let ok2 v1 v2 f =
match v1,v2 with
| Ok x1,Ok x2 -> Ok (f x1 x2)
| Error _, _ -> v1
| _, Error _ -> v2

let result2 v1 v2 f =
match v1,v2 with
| Ok x1,Ok x2 -> f x1 x2
| Error _, _ -> v1
| _, Error _ -> v2

let rec eval = function
| Int n ->
Ok n
| Neg a ->
ok1 (eval a) (~-)
ok2 (eval a) (eval b) (+)
| Sub(a,b) ->
ok2 (eval a) (eval b) (-)
| Mul(a,b) ->
ok2 (eval a) (eval b) ( * )
| Div(a,b) ->
result2
(eval a) (eval b)
(fun a b -> if b=0 then Error Division_by_zero else Ok (a/b))
``````

The SquareMatrix module
(This is my own original code)

``````module SquareMatrix
(M :
sig
type t
val size : int
val plus : t -> t -> t
end
)
:
sig
type t
val make : M.t -> t
val add : t -> t -> t
end
=
struct
type t =
M.t array array
let make x =
Array.make_matrix M.size M.size x
Array.map2 (Array.map2 M.plus) ma mb
end
``````

Generative modules as records
(This is my own original code)

``````module Counter () =
struct
let ticks = ref 0
let tick () = incr ticks
let count () = !ticks
end
``````

Church nat arithmetic
(This is my own original code inspired by a contribution by @gasche)

``````module ChurchArith
:
sig
type t
val zero : t
val one : t
val two : t
val three : t
val inc : t -> t
val add : t -> t -> t
val mul : t -> t -> t
val power : t -> t -> t
val to_int : t -> int
end
=
struct
type t =
{c: 'a. ('a -> 'a) -> ('a -> 'a)}
let zero =
{c = fun f x -> x}
let one =
{c = fun f x -> f x}
let two =
{c = fun f x -> f (f x)}
let three =
{c = fun f x -> f (f (f x))}
let inc n =
{c = fun f x -> f (n.c f x)}
{c = fun f x -> n.c f (m.c f x)}
let mul n m =
{c = fun f x -> n.c (m.c f) x}
let power n m =
{c = fun f x -> m.c n.c f x}
let to_int t =
t.c succ 0
end
``````

A simple functional queue (FIFO datatype)
(This code is outrageous plagiarism of the excellent Chris Okasaki book, page 43)
(This is common knowledge, i donât see why this code could not be CC-BY-SA 4.0)

``````module Queue
:
sig
type +'a t
val empty : 'a t
val member : 'a t -> 'a
val add : 'a -> 'a t -> 'a t
val remove : 'a t -> 'a t
end
=
struct
type +'a t =
{front:'a list;rear:'a list}
let empty =
{front=[];rear=[]}
let member {front;_} =
match front with
| [] -> failwith "Queue.member"
| h::_ -> h
let queue front rear =
match front with
| [] -> {front=List.rev rear;rear=[]}
| _ -> {front;rear}
queue front (n::rear)
let remove {front;rear} =
match front with
| [] -> failwith "Queue.remove"
| _::t -> queue t rear
end
``````

A polymorphic 2D-tree datatype
(This is my own original code)
(The `to_list` function is a contribution by @gasche)

``````module DoubleDimension
:
sig
type (+'a,+'b) t
val empty : ('a,'b) t
val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
val member : 'a -> 'b -> ('a,'b) t -> bool
val first :  'b -> ('a,'b) t -> 'a list
val second : 'a -> ('a,'b) t -> 'b list
val for_all : ('a -> 'b -> bool) -> ('a,'b) t -> bool
val subset : ('a,'b) t -> ('a,'b) t -> bool
val equal :  ('a,'b) t -> ('a,'b) t -> bool
val to_list : ('a,'b) t -> ('a * 'b) list
end
=
struct

type (+'a,+'b) t =
| Empty
| Fork of ('b,'a) t * 'a * 'b * ('b,'a) t

let empty =
Empty

let rec add : 'a 'b . 'a -> 'b -> ('a,'b) t -> ('a,'b) t =
fun x y -> function
| Empty -> Fork(Empty,x,y,Empty)
| Fork (l,u,v,r) as g ->
if x < u then Fork (add y x l,u,v,r)
else if x > u then Fork (l,u,v,add y x r)
else if y = v then g
else Fork (l,u,v,add y x r)

let rec member : 'a 'b . 'a -> 'b -> ('a,'b) t -> bool =
fun x y -> function
| Empty -> false
| Fork (l,u,v,r) ->
if x < u then member y x l
else if x > u then member y x r
else if y = v then true
else member y x r

let apply f w acc = function
| Empty -> acc
| Fork (l,u,v,r) ->
f w (f w (if w = v then u::acc else acc) r) l

let rec loop key acc = function
| Empty -> []
| Fork (l,u,v,r) ->
if key < u then apply loop key acc l
else if key > u then apply loop key acc r
else v::apply loop key acc r

let first y =
apply loop y []

let second x =
loop x []

let rec for_all :
'a 'b .
('a -> 'b -> bool) -> ('b -> 'a -> bool) -> ('a,'b) t -> bool
=
fun p q -> function
| Empty -> true
| Fork (l,u,v,r) -> for_all q p l && p u v && for_all q p r

(* apply 2 function arguments in swapped order *)
let flip f x y =
f y x

(* checks if all elements satisfy the predicate p *)
let for_all p =
for_all p (flip p)

(* is ta a subset of tb ? *)
let subset ta tb =
for_all (fun a b -> member a b tb) ta

(* set equality *)
let equal ta tb =
subset ta tb && subset tb ta

(* linearization *)
let rec to_list :
'a 'b .
'c list -> ('a -> 'b -> 'c) -> ('b -> 'a -> 'c) -> ('a,'b) t -> 'c list
=
fun acc fu fv -> function
| Empty ->
acc
| Fork (l,u,v,r) ->
to_list (fu u v::to_list acc fv fu r) fv fu l

let to_list t =
to_list [] (fun u v -> u,v) (fun v u -> u,v) t

end
``````

Binary Search Tree using inline record, the functional style
(Arguably not something revolutionary but this is my own original code)

``````   type +'a t =
| Empty
| Fork of {left:'a t;item:'a;right:'a t}
let rec add x t =
match t with
| Empty -> Fork {left=Empty;item=x;right=Empty}
| Fork n ->
if x < n.item then Fork {n with left=add x n.left}
else if x > n.item then Fork {n with right=add x n.right}
else t
``````

Binary Search Tree using inline record, the destructive style

``````   type 'a t =
| Empty
| Fork of {mutable left:'a t;item:'a;mutable right:'a t}
let rec add x t =
match t with
| Empty -> Fork {left=Empty;item=x;right=Empty}
| Fork n ->
if x < n.item then (n.left <- add x n.left; t)
else if x > n.item then (n.right <- add x n.right; t)
else t
``````

Binary Search Tree set of `int` , very much like `Stdlib.Set` without the balancing stuff.
(This code is outrageous plagiarism of `Stdlib.Set.ml`)

``````type t =
| Empty
| Fork of t * int * t

let empty =
Empty

let is_empty t =
t = Empty

let singleton n =
Fork(Empty,n,Empty)

let rec strahler = function
| Empty -> 0
| Fork(l,n,r) ->
let sl = strahler l and sr = strahler r in
if sl = sr then sl+1 else max sl sr

let rec add n t =
match t with
| Empty -> singleton n
| Fork(l,m,r) ->
if n < m then Fork(add n l,m,r)
else if n > m then Fork(l,m,add n r)
else t

let rec member n = function
| Empty -> false
| Fork(l,m,r) ->
if n < m then member n l
else if n > m then member n r
else true

let rec interval low high = function
| Empty -> Empty
| Fork(l,n,r) ->
if high < n then interval low high l
else if low > n then interval low high r
else Fork(interval low high l,n,interval low high r)

let rec cardinal = function
| Empty -> 0
| Fork(l,_,r) -> cardinal l + 1 + cardinal r

let rec cardinal acc = function
| Empty -> acc
| Fork(l,_,r) -> cardinal (cardinal acc r + 1) l

let cardinal =
cardinal 0

let rec minimum acc = function
| Empty -> acc
| Fork(l,n,r) -> minimum n l

let rec remove_minimum la na ra =
match la with
| Empty -> ra
| Fork(lb,nb,rb) -> Fork(remove_minimum lb nb rb,na,ra)

let concat ta tb =
match ta,tb with
| _,Empty -> ta
| Empty,_ -> tb
| _,Fork(lb,nb,rb) ->
Fork(ta,minimum nb lb,remove_minimum lb nb rb)

let rec remove n = function
| Empty -> Empty
| Fork(l,m,r) ->
if n < m then Fork(remove n l,m,r)
else if n > m then Fork(l,m,remove n r)
else concat l r

let rec filter cond = function
| Empty -> Empty
| Fork(l,n,r) ->
if cond n then Fork(filter cond l,n,filter cond r)
else concat (filter cond l) (filter cond r)

let rec split n = function
| Empty -> Empty,false,Empty
| Fork(l,m,r) ->
if n < m then
let la,present,ra = split n l in la,present,Fork(ra,m,r)
else if n > m then
let lb,present,rb = split n r in Fork(l,m,lb),present,rb
else l,true,r

let rec union ta tb =
match ta,tb with
| _,Empty -> ta
| Empty,_ -> tb
| Fork(la,na,ra),_ ->
let lb,_,rb = split na tb
in Fork(union la lb,na,union ra rb)

let rec intersection ta tb =
match ta,tb with
| _,Empty | Empty,_ -> Empty
| Fork(la,na,ra),_ ->
let lb,present,rb = split na tb in
if present then Fork(intersection la lb,na,intersection ra rb)
else concat (intersection la lb) (intersection ra rb)

let rec difference ta tb =
match ta,tb with
| _,Empty -> ta
| Empty,_ -> Empty
| Fork(la,na,ra),_ ->
let lb,present,rb = split na tb in
if present then concat (difference la lb) (difference ra rb)
else Fork(difference la lb,na,difference ra rb)

let rec disjoint ta tb =
match ta,tb with
| _,Empty | Empty,_ -> true
| Fork(la,na,ra),_ ->
let lb,present,rb = split na tb in
if present then false
else disjoint la lb && disjoint ra rb

let rec subset ta tb =
match ta,tb with
| Empty,_ -> true
| _,Empty -> false
| Fork(la,na,ra),Fork(lb,nb,rb) ->
if na < nb then
subset (Fork(la,na,Empty)) lb && subset ra tb
else if na > nb then
subset (Fork(Empty,na,ra)) rb && subset la tb
else
subset la lb && subset ra rb

let equal ta tb =
subset ta tb && subset tb ta

(* recursive linearization *)
let rec to_list = function
| Empty -> []
| Fork(l,n,r) -> to_list l @ [n] @ to_list r

(* iterative linearization *)
let rec to_list acc = function
| Empty -> acc
| Fork(l,n,r) -> to_list (n::to_list acc r) l
let to_list =
to_list []
``````

A monomorphic version of DoubleDimension used as a directed graph datatype, vertices are labelled with `int`, edges are unlabelled
(This is my own original code)

``````module DirectedGraph
:
sig
type t
val empty : t
val add : int -> int -> t -> t
val member : int -> int -> t -> bool
val successors : int -> t -> int list
val predecessors : int -> t -> int list
val subgraph : t -> t -> bool
val equal : t -> t -> bool
end
=
struct

type t =
| Empty
| Fork of t * int * int * t

let empty =
Empty

(* add an edge (x,y) to the graph *)
let rec add x y = function
| Empty -> Fork(Empty,x,y,Empty)
| Fork (l,u,v,r) as g ->
if x < u then Fork (add y x l,u,v,r)
else if x > u then Fork (l,u,v,add y x r)
else if y = v then g
else Fork (l,u,v,add y x r)
(* else Fork (l,u,(min v y),add (max v y) x r)  proposed by gasche *)

(* is the edge (x,y) in the graph ? *)
let rec member x y = function
| Empty -> false
| Fork (l,u,v,r) ->
if x < u then member y x l
else if x > u then member y x r
else if y = v then true
else member y x r

(* deal with the non-discriminating levels *)
let apply f w acc = function
| Empty -> acc
| Fork (l,u,v,r) ->
f w (f w (if w = v then u::acc else acc) r) l

(* deal with the discriminating levels *)
let rec loop x acc = function
| Empty -> acc
| Fork (l,u,v,r) ->
if x < u then apply loop x acc l
else if x > u then apply loop x acc r
else v::apply loop x acc r
(* successors   *)
let successors x =
loop x []
(* predecessors *)
let predecessors y =
apply loop y []

(* is ga a subgraph of gb ? *)
let subgraph ga gb =
let rec sub1 = function
| Empty -> true
| Fork (l,u,v,r) -> member u v gb && sub2 l && sub2 r
and sub2 = function
| Empty -> true
| Fork (l,u,v,r) -> member v u gb && sub1 l && sub1 r
in sub1 ga

(* graph equality *)
let equal ga gb =
subgraph ga gb && subgraph gb ga

end
``````

A max-heap that memorize the insertion order
(by an unknown contributor of La lettre de Caml nÂ°5)

``````type t =
| Empty
| Fork of t * int * t

let empty =
Empty

let singleton n =
Fork(Empty,n,Empty)

let rec add n t =
match t with
| Empty -> singleton n
| Fork(_,m,_) when n > m -> Fork(t,n,Empty)
| Fork(l,m,Empty) -> Fork(l,m,singleton n)
| Fork(l,m,(Fork(_,k,_) as r)) when k > n ->
| Fork(l,m,r) -> Fork(l,m,Fork(r,n,Empty))

let rec member = function
| Empty -> invalid_arg "RetraceHeap.member"
| Fork(_,n,_) -> n

let rec remove = function
| Empty -> invalid_arg "RetraceHeap.remove"
| Fork(Empty,n,Empty) -> Empty
| Fork(l,n,Empty) -> l
| Fork(Empty,n,r) -> r
| Fork((Fork(la,na,ra) as l),n,(Fork(lb,nb,rb) as r)) ->
if nb > na then
let ll = remove (Fork(l,n,lb))
in  Fork(ll,nb,rb)
else
let rr = remove (Fork(ra,n,r))
in  Fork(la,na,rr)

let rec to_list acc = function
| Empty -> acc
| Fork(l,n,r) -> to_list (n::to_list acc r) l
let to_list =
to_list []
``````

Certification of adding an item to a binary search tree set of ints
(The easy parts are my own original code, the difficult parts are by dividee, i donât know his / her real life name)

``````(* un arbre est soit vide soit une sĂ©paration en deux *)
Inductive tree : Set :=
| Empty: tree
| Fork: tree -> nat -> tree -> tree.

Require Import Arith.Arith_base.

(* nombre de strahler *)
Fixpoint strahler t :=
match t with
| Empty => 0
| Fork l n r =>
let sl := strahler l in
let sr := strahler r in
if beq_nat sl sr then S sl else max sl sr
end.

(* recherche d'un entier n dans un arbre t *)
Fixpoint member_of n t :=
match t with
| Empty => false     (* absent *)
| Fork l m r =>
match n ?= m with
| Eq => true     (* on l'a trouvĂ© *)
| Lt => member_of n l (* on cherche Ă  gauche *)
| Gt => member_of n r (* on cherche Ă  droite *)
end
end.

(* insertion d'un entier n dans un arbre t *)
match t with
| Empty => Fork Empty n Empty  (* on crĂ©e un singleton *)
| Fork l m r =>
match n ?= m with
| Lt => Fork (add n l) m r (* on insĂšre Ă  gauche *)
| Gt => Fork l m (add n r) (* on insĂšre Ă  droite *)
end
end.

(* extraction de l'intervalle [low,high] de l'arbre t *)
Fixpoint interval low high t :=
match t with
| Empty => Empty
| Fork l n r =>
match high ?= n with
| Lt => interval low high l
| Gt | Eq =>
match low ?= n with
| Gt => interval low high r
| Lt | Eq => Fork (interval low high l) n (interval low high r)
end
end
end.

(* c'est lĂ  qu'est dĂ©fini le type list *)
Require Import Lists.List.

(* conversion de l'arbre t en une liste triĂ©e *)
Fixpoint to_list acc t :=
match t with
| Empty => acc
| Fork l n r => to_list (n::to_list acc r) l
end.

Fixpoint minimum acc t :=
match t with
| Empty => acc
| Fork l n r => minimum n l
end.

Fixpoint remove_minimum la na ra :=
match la with
| Empty => ra
| Fork lb nb rb => Fork (remove_minimum lb nb rb) na ra
end.

(* agglomĂšre les arbres ta et tb *)
Fixpoint concat ta tb :=
match ta,tb with
| _,Empty => ta
| Empty,_ => tb
| _,Fork lb nb rb =>
Fork ta (minimum nb lb) (remove_minimum lb nb rb)
end.

Fixpoint remove n t :=
match t with
| Empty => Empty
| Fork l m r =>
match n ?= m with
| Lt => Fork (remove n l) m r
| Gt => Fork l m (remove n r)
| Eq => concat l r
end
end.

(* filtre l'arbre t suivant le prĂ©dicat cond *)
Fixpoint filter (cond : nat -> bool) t :=
match t with
| Empty => Empty
| Fork l n r =>
if cond n then Fork (filter cond l) n (filter cond r)
else concat (filter cond l) (filter cond r)
end.

Fixpoint cardinal t :=
match t with
| Empty => 0
| Fork l _ r => cardinal l + 1 + cardinal r
end.

Require Import Bool.Bool.

Require Import Coq.Program.Wf.

(* l'arbre ta est-il un sous-ensemble de l'arbre tb ? *)
Program Fixpoint subset (ta : tree) (tb : tree) {measure (cardinal ta + cardinal tb)} : bool :=
match ta,tb with
| Empty,_ => true
| _,Empty => false
| Fork la na ra,Fork lb nb rb =>
match na ?= nb with
| Lt => subset (Fork la na Empty) lb && subset ra tb
| Gt => subset (Fork Empty na ra) rb && subset la tb
| Eq => subset la lb && subset ra rb
end
end.

Definition equal ta tb :=
subset ta tb && subset tb ta.

Fixpoint split n t :=
match t with
| Empty => (Empty,false,Empty)
| Fork l m r =>
match n ?= m with
| Lt => let '(la,present,ra) := split n l in (la,present,Fork ra m r)
| Gt => let '(lb,present,rb) := split n r in (Fork l m lb,present,rb)
| Eq => (l,true,r)
end
end.

(* fusionne les arbres ta et tb *)
Fixpoint union ta tb :=
match ta,tb with
| _,Empty => ta
| Empty,_ => tb
| Fork la na ra,_ =>
let '(lb,_,rb) := split na tb
in Fork (union la lb) na (union ra rb)
end.

Fixpoint intersection ta tb :=
match ta,tb with
| _,Empty | Empty,_ => Empty
| Fork la na ra,_ =>
let '(lb,present,rb) := split na tb in
if present then Fork (intersection la lb) na (intersection ra rb)
else concat (intersection la lb) (intersection ra rb)
end.

Fixpoint disjoint ta tb :=
match ta,tb with
| _,Empty | Empty,_ => true
| Fork la na ra,_ =>
let '(lb,present,rb) := split na tb in
if present then false
else disjoint la lb && disjoint ra rb
end.

Fixpoint difference ta tb :=
match ta,tb with
| _,Empty => ta
| Empty,_ => Empty
| Fork la na ra,_ =>
let '(lb,present,rb) := split na tb in
if present then concat (difference la lb) (difference ra rb)
else Fork (difference la lb) na (difference ra rb)
end.

Inductive member : nat -> tree -> Prop :=
| root_member :
forall l n r,
member n (Fork l n r)
| left_member :
forall m n l r,
member n l ->
member n (Fork l m r)
| right_member :
forall m n l r,
member n r ->
member n (Fork l m r).

forall n t, member n (add n t).
Proof.
intros n t. induction t.
(* Empty *)
apply root_member.
(* Fork *)
unfold add. remember (n ?= n0) as cmp.
destruct cmp.
(* Eq *)
symmetry in Heqcmp.
apply (nat_compare_eq n n0) in Heqcmp.
subst n0. apply root_member.
(* Lt *)
apply left_member. exact IHt1.
(* Gt *)
apply right_member. exact IHt2.
Qed.

forall m n t, member m t -> member m (add n t).
Proof.
intros m n t H. induction t.
(* Empty *)
apply left_member. exact H.
(* Fork *)
remember (Fork t1 n0 t2) as node.
destruct H.
(* root_member *)
unfold add. destruct (n ?= n1).
apply root_member.
apply root_member.
apply root_member.
(* left_member *)
inversion Heqnode. rewrite H1 in H.
unfold add. destruct (n ?= n0).
apply left_member. exact H.
apply IHt1 in H. apply left_member. exact H.
apply left_member. exact H.
(* right_member *)
inversion Heqnode. rewrite H3 in H.
unfold add. destruct (n ?= n0).
apply right_member. exact H.
apply right_member. exact H.
apply IHt2 in H. apply right_member. exact H.
Qed.

Inductive tree_less : tree -> nat -> Prop :=
| empty_tree_less :
forall b, tree_less Empty b
| fork_tree_less :
forall l m r b,
tree_less l b -> tree_less r b -> m < b ->
tree_less (Fork l m r) b.

Inductive tree_more : tree -> nat -> Prop :=
| empty_tree_more :
forall a, tree_more Empty a
| fork_tree_more :
forall l m r a,
tree_more l a -> tree_more r a -> m > a ->
tree_more (Fork l m r) a.

Inductive tree_ordered : tree -> Prop :=
| empty_tree_ordered :
tree_ordered Empty
| fork_tree_ordered :
forall l m r,
tree_ordered l -> tree_ordered r ->
tree_less l m -> tree_more r m ->
tree_ordered (Fork l m r).

Fact tree_less_upper_bound:
forall t n, tree_less t n <-> forall m, member m t -> m < n.
Proof.
split.
(* -> *)
intros Hless m Hm. induction t.
inversion Hm.
inversion Hm; inversion Hless; subst; auto.
(* <- *)
intros H. induction t.
constructor.
constructor.
apply IHt1. intros m Hm. apply H. apply left_member. assumption.
apply IHt2. intros m Hm. apply H. apply right_member. assumption.
apply H. apply root_member.
Qed.

Fact tree_more_lower_bound:
forall t n, tree_more t n <-> forall m, member m t -> m > n.
Proof.
split.
(* -> *)
intros Hmore m Hm. induction t.
inversion Hm.
inversion Hm; inversion Hmore; subst; auto.
(* <- *)
intros H. induction t.
constructor.
constructor.
apply IHt1. intros m Hm. apply H. apply left_member. assumption.
apply IHt2. intros m Hm. apply H. apply right_member. assumption.
apply H. apply root_member.
Qed.

(* Require Import Arith.Lt Arith.Gt. *)

Lemma member_left:
forall l m r n, tree_ordered (Fork l m r) -> member n (Fork l m r) -> n < m -> member n l.
Proof.
intros l m r n Hord Hmem Hlt.
inversion Hord; subst; clear Hord.
inversion Hmem; subst; clear Hmem.
assumption.
apply tree_more_lower_bound with (m:=n) in H5.
assumption.
Qed.

Lemma member_right:
forall l m r n, tree_ordered (Fork l m r) -> member n (Fork l m r) -> n > m -> member n r.
Proof.
intros l m r n Hord Hmem Hlt.
inversion Hord; subst; clear Hord.
inversion Hmem; subst; clear Hmem.
apply tree_less_upper_bound with (m:=n) in H4.
contradict H4. apply lt_asym. assumption. assumption.
assumption.
Qed.

forall t n m, tree_less t n -> m < n -> tree_less (add m t) n.
Proof.
induction t; intros; inversion H; subst; clear H.
repeat constructor. assumption.
simpl. destruct (m ?= n); constructor; auto.
Qed.

forall t n m, tree_more t n -> m > n -> tree_more (add m t) n.
Proof.
induction t; intros; inversion H; subst; clear H.
repeat constructor. assumption.
simpl. destruct (m ?= n); constructor; auto.
Qed.

forall t, tree_ordered t ->
forall n, tree_ordered (add n t).
Proof.
induction t; intros.
(* Empty *)
simpl. repeat constructor.
(* Fork *)
simpl. remember (n0 ?= n) as cmp. symmetry in Heqcmp.
destruct cmp.
assumption.
inversion H; subst; clear H. constructor; auto.
apply nat_compare_lt in Heqcmp. apply add_preserves_less; assumption.
inversion H; subst; clear H. constructor; auto.
apply nat_compare_gt in Heqcmp. apply add_preserves_more; assumption.
Qed.
``````

Note that `Program Fixpoint subset` does not compile as it is now (any help appreciated).

1 Like

What is a âStatement of Rights violationâ? Are you referring to the fact that currently all user contributions to this Discourse are licensed under CC BY-NC-SA ( Terms of Service - OCaml )?