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

Community
,
1

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
2

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.

3

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.

4

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 =
         self#advance && self#test
      method private advance =
         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.

5

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
6

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
7

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.)
  | Add(u,R(k)) -> derive(u)
  | Add(u,v)    -> Add(derive(u),derive(v))
  | Mul(R(k),X) -> R(k)
  | Mul(R(k),u) -> product(R(k),derive(u))
  | Mul(u,v) -> Add(product(derive(u),v),product(u,derive(v)))
  | 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.)))
8

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
9

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) (~-)
  | Add(a,b) ->
     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))
10

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
   let add ma mb =
      Array.map2 (Array.map2 M.plus) ma mb
end
11

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
12

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)}
	let add n m =
		{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
13

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}     
   let add n {front;rear} =
      queue front (n::rear)
   let remove {front;rear} =
      match front with
      | [] -> failwith "Queue.remove"
      | _::t -> queue t rear
end
14

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
15

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
16

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 []
17

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
18

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,add n r)
   | 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 []
19

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 *)
Fixpoint add n t :=
  match t with
  | Empty => Fork Empty n Empty  (* on crée un singleton *)
  | Fork l m r =>
      match n ?= m with
      | Eq => t                  (* déjà présent *)
      | 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.

(* trouve le plus petit élément de l'arbre t *)
Fixpoint minimum acc t :=
  match t with
  | Empty => acc
  | Fork l n r => minimum n l  
  end.

(* supprime le plus petit élément de l'arbre t *)
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 *)
(* les Ă©lĂ©ments de ta doivent ĂȘtre strictement infĂ©rieurs aux Ă©lĂ©ments de 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.

(* supprime l'élément n de l'arbre t *)
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.

(* nombres d'éléments de l'arbre t *)
Fixpoint cardinal t :=
  match t with
  | Empty => 0
  | Fork l _ r => cardinal l + 1 + cardinal r
  end.
	
(* c'est là qu'est défini l'opérateur && *)
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.

(* inclusion réciproque *)
Definition equal ta tb :=
  subset ta tb && subset tb ta.  
  
(* découpe t en deux parties inférieures et supérieures à n *)
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).

Theorem add_main_property :
  forall n t, member n (add n t).
Proof.
  intros n t. induction t.
  (* Empty *)
  unfold add.
    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.

Theorem add_is_conservative :
  forall m n t, member m t -> member m (add n t).
Proof.
  intros m n t H. induction t. 
  (* Empty *)
  unfold add.
    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.
    contradict Hlt. apply lt_irrefl.
    assumption.
    apply tree_more_lower_bound with (m:=n) in H5.
      contradict H5. apply gt_asym. assumption.
      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.
    contradict Hlt. apply lt_irrefl.
    apply tree_less_upper_bound with (m:=n) in H4.
      contradict H4. apply lt_asym. assumption. assumption.
    assumption.
Qed.

Lemma add_preserves_less:
  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.
 
Lemma add_preserves_more:
  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.

Theorem add_preserves_order :
  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
20

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 )?