Skip to content

Instantly share code, notes, and snippets.

@palmskog

palmskog/fitch_system.ml

Created March 30, 2020 01:16
Show Gist options
  • Save palmskog/83249675cb78fe605f5eab1a40b54200 to your computer and use it in GitHub Desktop.
Save palmskog/83249675cb78fe605f5eab1a40b54200 to your computer and use it in GitHub Desktop.
Download ZIP
Verified Fitch-style proof checker extracted from Coq to OCaml
Raw
fitch_system.ml
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
type ('a, 'b) sum =
| Inl of 'a
| Inr of 'b
(** val fst : ('a1 * 'a2) -> 'a1 **)
let fst = function
| (x, _) -> x
(** val snd : ('a1 * 'a2) -> 'a2 **)
let snd = function
| (_, y) -> y
(** val length : 'a1 list -> int **)
let rec length = function
| [] -> 0
| _ :: l' -> Pervasives.succ (length l')
type comparison =
| Eq
| Lt
| Gt
module type EqLtLe =
sig
type t
end
module MakeOrderTac =
functor (O:EqLtLe) ->
functor (P:sig
end) ->
struct
end
module Nat =
struct
(** val compare : int -> int -> comparison **)
let rec compare = fun n m -> if n=m then Eq else if n<m then Lt else Gt
end
(** val in_dec : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 list -> bool **)
let rec in_dec h a = function
| [] -> false
| y :: l1 -> let s = h y a in if s then true else in_dec h a l1
(** val last : 'a1 list -> 'a1 -> 'a1 **)
let rec last l0 d =
match l0 with
| [] -> d
| a :: l1 -> (match l1 with
| [] -> a
| _ :: _ -> last l1 d)
(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)
let rec fold_right f a0 = function
| [] -> a0
| b :: t0 -> f b (fold_right f a0 t0)
(** val string_dec : char list -> char list -> bool **)
let rec string_dec s x =
match s with
| [] -> (match x with
| [] -> true
| _::_ -> false)
| a::s0 ->
(match x with
| [] -> false
| a0::s1 -> if (=) a a0 then string_dec s0 s1 else false)
type 'x compare0 =
| LT
| EQ
| GT
module type OrderedType =
sig
type t
val compare : t -> t -> t compare0
val eq_dec : t -> t -> bool
end
module OrderedTypeFacts =
functor (O:OrderedType) ->
struct
module TO =
struct
type t = O.t
end
module IsTO =
struct
end
module OrderTac = MakeOrderTac(TO)(IsTO)
(** val eq_dec : O.t -> O.t -> bool **)
let eq_dec =
O.eq_dec
(** val lt_dec : O.t -> O.t -> bool **)
let lt_dec x y =
match O.compare x y with
| LT -> true
| _ -> false
(** val eqb : O.t -> O.t -> bool **)
let eqb x y =
if eq_dec x y then true else false
end
module KeyOrderedType =
functor (O:OrderedType) ->
struct
module MO = OrderedTypeFacts(O)
end
module type S =
sig
module E :
OrderedType
type key = E.t
type 'x t
val empty : 'a1 t
val is_empty : 'a1 t -> bool
val add : key -> 'a1 -> 'a1 t -> 'a1 t
val find : key -> 'a1 t -> 'a1 option
val remove : key -> 'a1 t -> 'a1 t
val mem : key -> 'a1 t -> bool
val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t
val mapi : (key -> 'a1 -> 'a2) -> 'a1 t -> 'a2 t
val map2 :
('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t -> 'a3 t
val elements : 'a1 t -> (key * 'a1) list
val cardinal : 'a1 t -> int
val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2
val equal : ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool
end
module Raw =
functor (X:OrderedType) ->
struct
module MX = OrderedTypeFacts(X)
module PX = KeyOrderedType(X)
type key = X.t
type 'elt t = (X.t * 'elt) list
(** val empty : 'a1 t **)
let empty =
[]
(** val is_empty : 'a1 t -> bool **)
let is_empty = function
| [] -> true
| _ :: _ -> false
(** val mem : key -> 'a1 t -> bool **)
let rec mem k = function
| [] -> false
| p0 :: l0 ->
let (k', _) = p0 in
(match X.compare k k' with
| LT -> false
| EQ -> true
| GT -> mem k l0)
type 'elt coq_R_mem =
| R_mem_0 of 'elt t
| R_mem_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_mem_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_mem_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * bool * 'elt coq_R_mem
(** val coq_R_mem_rect :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2) -> 'a1 t ->
bool -> 'a1 coq_R_mem -> 'a2 **)
let rec coq_R_mem_rect k f f0 f1 f2 _ _ = function
| R_mem_0 s -> f s __
| R_mem_1 (s, k', _x, l0) -> f0 s k' _x l0 __ __ __
| R_mem_2 (s, k', _x, l0) -> f1 s k' _x l0 __ __ __
| R_mem_3 (s, k', _x, l0, _res, r0) ->
f2 s k' _x l0 __ __ __ _res r0 (coq_R_mem_rect k f f0 f1 f2 l0 _res r0)
(** val coq_R_mem_rec :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2) -> 'a1 t ->
bool -> 'a1 coq_R_mem -> 'a2 **)
let rec coq_R_mem_rec k f f0 f1 f2 _ _ = function
| R_mem_0 s -> f s __
| R_mem_1 (s, k', _x, l0) -> f0 s k' _x l0 __ __ __
| R_mem_2 (s, k', _x, l0) -> f1 s k' _x l0 __ __ __
| R_mem_3 (s, k', _x, l0, _res, r0) ->
f2 s k' _x l0 __ __ __ _res r0 (coq_R_mem_rec k f f0 f1 f2 l0 _res r0)
(** val mem_rect :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let rec mem_rect k f2 f1 f0 f s =
let f3 = f2 s in
let f4 = f1 s in
let f5 = f0 s in
let f6 = f s in
(match s with
| [] -> f3 __
| p0 :: l0 ->
let (t0, e) = p0 in
let f7 = f6 t0 e l0 __ in
let f8 = fun _ _ ->
let hrec = mem_rect k f2 f1 f0 f l0 in f7 __ __ hrec
in
let f9 = f5 t0 e l0 __ in
let f10 = f4 t0 e l0 __ in
(match X.compare k t0 with
| LT -> f10 __ __
| EQ -> f9 __ __
| GT -> f8 __ __))
(** val mem_rec :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let mem_rec =
mem_rect
(** val coq_R_mem_correct : key -> 'a1 t -> bool -> 'a1 coq_R_mem **)
let coq_R_mem_correct k s _res =
Obj.magic mem_rect k (fun y _ _ _ -> R_mem_0 y)
(fun y y0 y1 y2 _ _ _ _ _ -> R_mem_1 (y, y0, y1, y2))
(fun y y0 y1 y2 _ _ _ _ _ -> R_mem_2 (y, y0, y1, y2))
(fun y y0 y1 y2 _ _ _ y6 _ _ -> R_mem_3 (y, y0, y1, y2, (mem k y2),
(y6 (mem k y2) __))) s _res __
(** val find : key -> 'a1 t -> 'a1 option **)
let rec find k = function
| [] -> None
| p0 :: s' ->
let (k', x) = p0 in
(match X.compare k k' with
| LT -> None
| EQ -> Some x
| GT -> find k s')
type 'elt coq_R_find =
| R_find_0 of 'elt t
| R_find_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_find_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_find_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt option
* 'elt coq_R_find
(** val coq_R_find_rect :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find -> 'a2 -> 'a2) -> 'a1
t -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
let rec coq_R_find_rect k f f0 f1 f2 _ _ = function
| R_find_0 s -> f s __
| R_find_1 (s, k', x, s') -> f0 s k' x s' __ __ __
| R_find_2 (s, k', x, s') -> f1 s k' x s' __ __ __
| R_find_3 (s, k', x, s', _res, r0) ->
f2 s k' x s' __ __ __ _res r0 (coq_R_find_rect k f f0 f1 f2 s' _res r0)
(** val coq_R_find_rec :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find -> 'a2 -> 'a2) -> 'a1
t -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
let rec coq_R_find_rec k f f0 f1 f2 _ _ = function
| R_find_0 s -> f s __
| R_find_1 (s, k', x, s') -> f0 s k' x s' __ __ __
| R_find_2 (s, k', x, s') -> f1 s k' x s' __ __ __
| R_find_3 (s, k', x, s', _res, r0) ->
f2 s k' x s' __ __ __ _res r0 (coq_R_find_rec k f f0 f1 f2 s' _res r0)
(** val find_rect :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let rec find_rect k f2 f1 f0 f s =
let f3 = f2 s in
let f4 = f1 s in
let f5 = f0 s in
let f6 = f s in
(match s with
| [] -> f3 __
| p0 :: l0 ->
let (t0, e) = p0 in
let f7 = f6 t0 e l0 __ in
let f8 = fun _ _ ->
let hrec = find_rect k f2 f1 f0 f l0 in f7 __ __ hrec
in
let f9 = f5 t0 e l0 __ in
let f10 = f4 t0 e l0 __ in
(match X.compare k t0 with
| LT -> f10 __ __
| EQ -> f9 __ __
| GT -> f8 __ __))
(** val find_rec :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let find_rec =
find_rect
(** val coq_R_find_correct :
key -> 'a1 t -> 'a1 option -> 'a1 coq_R_find **)
let coq_R_find_correct k s _res =
Obj.magic find_rect k (fun y _ _ _ -> R_find_0 y)
(fun y y0 y1 y2 _ _ _ _ _ -> R_find_1 (y, y0, y1, y2))
(fun y y0 y1 y2 _ _ _ _ _ -> R_find_2 (y, y0, y1, y2))
(fun y y0 y1 y2 _ _ _ y6 _ _ -> R_find_3 (y, y0, y1, y2, (find k y2),
(y6 (find k y2) __))) s _res __
(** val add : key -> 'a1 -> 'a1 t -> 'a1 t **)
let rec add k x s = match s with
| [] -> (k, x) :: []
| p0 :: l0 ->
let (k', y) = p0 in
(match X.compare k k' with
| LT -> (k, x) :: s
| EQ -> (k, x) :: l0
| GT -> (k', y) :: (add k x l0))
type 'elt coq_R_add =
| R_add_0 of 'elt t
| R_add_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_add_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_add_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt t
* 'elt coq_R_add
(** val coq_R_add_rect :
key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_add -> 'a2 ->
'a2) -> 'a1 t -> 'a1 t -> 'a1 coq_R_add -> 'a2 **)
let rec coq_R_add_rect k x f f0 f1 f2 _ _ = function
| R_add_0 s -> f s __
| R_add_1 (s, k', y, l0) -> f0 s k' y l0 __ __ __
| R_add_2 (s, k', y, l0) -> f1 s k' y l0 __ __ __
| R_add_3 (s, k', y, l0, _res, r0) ->
f2 s k' y l0 __ __ __ _res r0 (coq_R_add_rect k x f f0 f1 f2 l0 _res r0)
(** val coq_R_add_rec :
key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_add -> 'a2 ->
'a2) -> 'a1 t -> 'a1 t -> 'a1 coq_R_add -> 'a2 **)
let rec coq_R_add_rec k x f f0 f1 f2 _ _ = function
| R_add_0 s -> f s __
| R_add_1 (s, k', y, l0) -> f0 s k' y l0 __ __ __
| R_add_2 (s, k', y, l0) -> f1 s k' y l0 __ __ __
| R_add_3 (s, k', y, l0, _res, r0) ->
f2 s k' y l0 __ __ __ _res r0 (coq_R_add_rec k x f f0 f1 f2 l0 _res r0)
(** val add_rect :
key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let rec add_rect k x f2 f1 f0 f s =
let f3 = f2 s in
let f4 = f1 s in
let f5 = f0 s in
let f6 = f s in
(match s with
| [] -> f3 __
| p0 :: l0 ->
let (t0, e) = p0 in
let f7 = f6 t0 e l0 __ in
let f8 = fun _ _ ->
let hrec = add_rect k x f2 f1 f0 f l0 in f7 __ __ hrec
in
let f9 = f5 t0 e l0 __ in
let f10 = f4 t0 e l0 __ in
(match X.compare k t0 with
| LT -> f10 __ __
| EQ -> f9 __ __
| GT -> f8 __ __))
(** val add_rec :
key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let add_rec =
add_rect
(** val coq_R_add_correct :
key -> 'a1 -> 'a1 t -> 'a1 t -> 'a1 coq_R_add **)
let coq_R_add_correct k x s _res =
add_rect k x (fun y _ _ _ -> R_add_0 y) (fun y y0 y1 y2 _ _ _ _ _ ->
R_add_1 (y, y0, y1, y2)) (fun y y0 y1 y2 _ _ _ _ _ -> R_add_2 (y, y0,
y1, y2)) (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_add_3 (y, y0, y1, y2,
(add k x y2), (y6 (add k x y2) __))) s _res __
(** val remove : key -> 'a1 t -> 'a1 t **)
let rec remove k s = match s with
| [] -> []
| p0 :: l0 ->
let (k', x) = p0 in
(match X.compare k k' with
| LT -> s
| EQ -> l0
| GT -> (k', x) :: (remove k l0))
type 'elt coq_R_remove =
| R_remove_0 of 'elt t
| R_remove_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_remove_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
| R_remove_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt t
* 'elt coq_R_remove
(** val coq_R_remove_rect :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 -> 'a2) -> 'a1 t
-> 'a1 t -> 'a1 coq_R_remove -> 'a2 **)
let rec coq_R_remove_rect k f f0 f1 f2 _ _ = function
| R_remove_0 s -> f s __
| R_remove_1 (s, k', x, l0) -> f0 s k' x l0 __ __ __
| R_remove_2 (s, k', x, l0) -> f1 s k' x l0 __ __ __
| R_remove_3 (s, k', x, l0, _res, r0) ->
f2 s k' x l0 __ __ __ _res r0 (coq_R_remove_rect k f f0 f1 f2 l0 _res r0)
(** val coq_R_remove_rec :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 -> 'a2) -> 'a1 t
-> 'a1 t -> 'a1 coq_R_remove -> 'a2 **)
let rec coq_R_remove_rec k f f0 f1 f2 _ _ = function
| R_remove_0 s -> f s __
| R_remove_1 (s, k', x, l0) -> f0 s k' x l0 __ __ __
| R_remove_2 (s, k', x, l0) -> f1 s k' x l0 __ __ __
| R_remove_3 (s, k', x, l0, _res, r0) ->
f2 s k' x l0 __ __ __ _res r0 (coq_R_remove_rec k f f0 f1 f2 l0 _res r0)
(** val remove_rect :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let rec remove_rect k f2 f1 f0 f s =
let f3 = f2 s in
let f4 = f1 s in
let f5 = f0 s in
let f6 = f s in
(match s with
| [] -> f3 __
| p0 :: l0 ->
let (t0, e) = p0 in
let f7 = f6 t0 e l0 __ in
let f8 = fun _ _ ->
let hrec = remove_rect k f2 f1 f0 f l0 in f7 __ __ hrec
in
let f9 = f5 t0 e l0 __ in
let f10 = f4 t0 e l0 __ in
(match X.compare k t0 with
| LT -> f10 __ __
| EQ -> f9 __ __
| GT -> f8 __ __))
(** val remove_rec :
key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
let remove_rec =
remove_rect
(** val coq_R_remove_correct : key -> 'a1 t -> 'a1 t -> 'a1 coq_R_remove **)
let coq_R_remove_correct k s _res =
Obj.magic remove_rect k (fun y _ _ _ -> R_remove_0 y)
(fun y y0 y1 y2 _ _ _ _ _ -> R_remove_1 (y, y0, y1, y2))
(fun y y0 y1 y2 _ _ _ _ _ -> R_remove_2 (y, y0, y1, y2))
(fun y y0 y1 y2 _ _ _ y6 _ _ -> R_remove_3 (y, y0, y1, y2,
(remove k y2), (y6 (remove k y2) __))) s _res __
(** val elements : 'a1 t -> 'a1 t **)
let elements m =
m
(** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 **)
let rec fold f m acc =
match m with
| [] -> acc
| p0 :: m' -> let (k, e) = p0 in fold f m' (f k e acc)
type ('elt, 'a) coq_R_fold =
| R_fold_0 of 'elt t * 'a
| R_fold_1 of 'elt t * 'a * X.t * 'elt * (X.t * 'elt) list * 'a
* ('elt, 'a) coq_R_fold
(** val coq_R_fold_rect :
(key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a2 -> ('a1, 'a2)
coq_R_fold -> 'a3 -> 'a3) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
coq_R_fold -> 'a3 **)
let rec coq_R_fold_rect f f0 f1 _ _ _ = function
| R_fold_0 (m, acc) -> f0 m acc __
| R_fold_1 (m, acc, k, e, m', _res, r0) ->
f1 m acc k e m' __ _res r0
(coq_R_fold_rect f f0 f1 m' (f k e acc) _res r0)
(** val coq_R_fold_rec :
(key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a2 -> ('a1, 'a2)
coq_R_fold -> 'a3 -> 'a3) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
coq_R_fold -> 'a3 **)
let rec coq_R_fold_rec f f0 f1 _ _ _ = function
| R_fold_0 (m, acc) -> f0 m acc __
| R_fold_1 (m, acc, k, e, m', _res, r0) ->
f1 m acc k e m' __ _res r0 (coq_R_fold_rec f f0 f1 m' (f k e acc) _res r0)
(** val fold_rect :
(key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a3 -> 'a3) -> 'a1 t ->
'a2 -> 'a3 **)
let rec fold_rect f1 f0 f m acc =
let f2 = f0 m acc in
let f3 = f m acc in
(match m with
| [] -> f2 __
| p0 :: l0 ->
let (t0, e) = p0 in
let f4 = f3 t0 e l0 __ in
let hrec = fold_rect f1 f0 f l0 (f1 t0 e acc) in f4 hrec)
(** val fold_rec :
(key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a3 -> 'a3) -> 'a1 t ->
'a2 -> 'a3 **)
let fold_rec =
fold_rect
(** val coq_R_fold_correct :
(key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
coq_R_fold **)
let coq_R_fold_correct f m acc _res =
fold_rect f (fun y y0 _ _ _ -> R_fold_0 (y, y0))
(fun y y0 y1 y2 y3 _ y5 _ _ -> R_fold_1 (y, y0, y1, y2, y3,
(fold f y3 (f y1 y2 y0)), (y5 (fold f y3 (f y1 y2 y0)) __))) m acc _res
__
(** val equal : ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool **)
let rec equal cmp m m' =
match m with
| [] -> (match m' with
| [] -> true
| _ :: _ -> false)
| p0 :: l0 ->
let (x, e) = p0 in
(match m' with
| [] -> false
| p1 :: l' ->
let (x', e') = p1 in
(match X.compare x x' with
| EQ -> (&&) (cmp e e') (equal cmp l0 l')
| _ -> false))
type 'elt coq_R_equal =
| R_equal_0 of 'elt t * 'elt t
| R_equal_1 of 'elt t * 'elt t * X.t * 'elt * (X.t * 'elt) list * X.t
* 'elt * (X.t * 'elt) list * bool * 'elt coq_R_equal
| R_equal_2 of 'elt t * 'elt t * X.t * 'elt * (X.t * 'elt) list * X.t
* 'elt * (X.t * 'elt) list * X.t compare0
| R_equal_3 of 'elt t * 'elt t * 'elt t * 'elt t
(** val coq_R_equal_rect :
('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
-> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> bool -> 'a1 coq_R_equal -> 'a2 ->
'a2) -> ('a1 t -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t
-> 'a1 -> (X.t * 'a1) list -> __ -> X.t compare0 -> __ -> __ -> 'a2) ->
('a1 t -> 'a1 t -> 'a1 t -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t ->
'a1 t -> bool -> 'a1 coq_R_equal -> 'a2 **)
let rec coq_R_equal_rect cmp f f0 f1 f2 _ _ _ = function
| R_equal_0 (m, m') -> f m m' __ __
| R_equal_1 (m, m', x, e, l0, x', e', l', _res, r0) ->
f0 m m' x e l0 __ x' e' l' __ __ __ _res r0
(coq_R_equal_rect cmp f f0 f1 f2 l0 l' _res r0)
| R_equal_2 (m, m', x, e, l0, x', e', l', _x) ->
f1 m m' x e l0 __ x' e' l' __ _x __ __
| R_equal_3 (m, m', _x, _x0) -> f2 m m' _x __ _x0 __ __
(** val coq_R_equal_rec :
('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
-> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> bool -> 'a1 coq_R_equal -> 'a2 ->
'a2) -> ('a1 t -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t
-> 'a1 -> (X.t * 'a1) list -> __ -> X.t compare0 -> __ -> __ -> 'a2) ->
('a1 t -> 'a1 t -> 'a1 t -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t ->
'a1 t -> bool -> 'a1 coq_R_equal -> 'a2 **)
let rec coq_R_equal_rec cmp f f0 f1 f2 _ _ _ = function
| R_equal_0 (m, m') -> f m m' __ __
| R_equal_1 (m, m', x, e, l0, x', e', l', _res, r0) ->
f0 m m' x e l0 __ x' e' l' __ __ __ _res r0
(coq_R_equal_rec cmp f f0 f1 f2 l0 l' _res r0)
| R_equal_2 (m, m', x, e, l0, x', e', l', _x) ->
f1 m m' x e l0 __ x' e' l' __ _x __ __
| R_equal_3 (m, m', _x, _x0) -> f2 m m' _x __ _x0 __ __
(** val equal_rect :
('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
-> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> ('a1 t -> 'a1 t ->
X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> X.t compare0 -> __ -> __ -> 'a2) -> ('a1 t -> 'a1 t -> 'a1 t
-> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t -> 'a1 t -> 'a2 **)
let rec equal_rect cmp f2 f1 f0 f m m' =
let f3 = f2 m m' in
let f4 = f1 m m' in
let f5 = f0 m m' in
let f6 = f m m' in
let f7 = f6 m __ in
let f8 = f7 m' __ in
(match m with
| [] -> let f9 = f3 __ in (match m' with
| [] -> f9 __
| _ :: _ -> f8 __)
| p0 :: l0 ->
let (t0, e) = p0 in
let f9 = f5 t0 e l0 __ in
let f10 = f4 t0 e l0 __ in
(match m' with
| [] -> f8 __
| p1 :: l1 ->
let (t1, e0) = p1 in
let f11 = f9 t1 e0 l1 __ in
let f12 = let _x = X.compare t0 t1 in f11 _x __ in
let f13 = f10 t1 e0 l1 __ in
let f14 = fun _ _ ->
let hrec = equal_rect cmp f2 f1 f0 f l0 l1 in f13 __ __ hrec
in
(match X.compare t0 t1 with
| EQ -> f14 __ __
| _ -> f12 __)))
(** val equal_rec :
('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
-> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
(X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> ('a1 t -> 'a1 t ->
X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 -> (X.t * 'a1) list
-> __ -> X.t compare0 -> __ -> __ -> 'a2) -> ('a1 t -> 'a1 t -> 'a1 t
-> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t -> 'a1 t -> 'a2 **)
let equal_rec =
equal_rect
(** val coq_R_equal_correct :
('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool -> 'a1 coq_R_equal **)
let coq_R_equal_correct cmp m m' _res =
equal_rect cmp (fun y y0 _ _ _ _ -> R_equal_0 (y, y0))
(fun y y0 y1 y2 y3 _ y5 y6 y7 _ _ _ y11 _ _ -> R_equal_1 (y, y0, y1,
y2, y3, y5, y6, y7, (equal cmp y3 y7), (y11 (equal cmp y3 y7) __)))
(fun y y0 y1 y2 y3 _ y5 y6 y7 _ y9 _ _ _ _ -> R_equal_2 (y, y0, y1, y2,
y3, y5, y6, y7, y9)) (fun y y0 y1 _ y3 _ _ _ _ -> R_equal_3 (y, y0, y1,
y3)) m m' _res __
(** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
let rec map f = function
| [] -> []
| p0 :: m' -> let (k, e) = p0 in (k, (f e)) :: (map f m')
(** val mapi : (key -> 'a1 -> 'a2) -> 'a1 t -> 'a2 t **)
let rec mapi f = function
| [] -> []
| p0 :: m' -> let (k, e) = p0 in (k, (f k e)) :: (mapi f m')
(** val option_cons :
key -> 'a1 option -> (key * 'a1) list -> (key * 'a1) list **)
let option_cons k o l0 =
match o with
| Some e -> (k, e) :: l0
| None -> l0
(** val map2_l :
('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a3 t **)
let rec map2_l f = function
| [] -> []
| p0 :: l0 ->
let (k, e) = p0 in option_cons k (f (Some e) None) (map2_l f l0)
(** val map2_r :
('a1 option -> 'a2 option -> 'a3 option) -> 'a2 t -> 'a3 t **)
let rec map2_r f = function
| [] -> []
| p0 :: l' ->
let (k, e') = p0 in option_cons k (f None (Some e')) (map2_r f l')
(** val map2 :
('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t -> 'a3 t **)
let rec map2 f m = match m with
| [] -> map2_r f
| p0 :: l0 ->
let (k, e) = p0 in
let rec map2_aux m' = match m' with
| [] -> map2_l f m
| p1 :: l' ->
let (k', e') = p1 in
(match X.compare k k' with
| LT -> option_cons k (f (Some e) None) (map2 f l0 m')
| EQ -> option_cons k (f (Some e) (Some e')) (map2 f l0 l')
| GT -> option_cons k' (f None (Some e')) (map2_aux l'))
in map2_aux
(** val combine : 'a1 t -> 'a2 t -> ('a1 option * 'a2 option) t **)
let rec combine m = match m with
| [] -> map (fun e' -> (None, (Some e')))
| p0 :: l0 ->
let (k, e) = p0 in
let rec combine_aux m' = match m' with
| [] -> map (fun e0 -> ((Some e0), None)) m
| p1 :: l' ->
let (k', e') = p1 in
(match X.compare k k' with
| LT -> (k, ((Some e), None)) :: (combine l0 m')
| EQ -> (k, ((Some e), (Some e'))) :: (combine l0 l')
| GT -> (k', (None, (Some e'))) :: (combine_aux l'))
in combine_aux
(** val fold_right_pair :
('a1 -> 'a2 -> 'a3 -> 'a3) -> ('a1 * 'a2) list -> 'a3 -> 'a3 **)
let fold_right_pair f l0 i =
fold_right (fun p0 -> f (fst p0) (snd p0)) i l0
(** val map2_alt :
('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t ->
(key * 'a3) list **)
let map2_alt f m m' =
let m0 = combine m m' in
let m1 = map (fun p0 -> f (fst p0) (snd p0)) m0 in
fold_right_pair option_cons m1 []
(** val at_least_one :
'a1 option -> 'a2 option -> ('a1 option * 'a2 option) option **)
let at_least_one o o' =
match o with
| Some _ -> Some (o, o')
| None -> (match o' with
| Some _ -> Some (o, o')
| None -> None)
(** val at_least_one_then_f :
('a1 option -> 'a2 option -> 'a3 option) -> 'a1 option -> 'a2 option ->
'a3 option **)
let at_least_one_then_f f o o' =
match o with
| Some _ -> f o o'
| None -> (match o' with
| Some _ -> f o o'
| None -> None)
end
module Make =
functor (X:OrderedType) ->
struct
module Raw = Raw(X)
module E = X
type key = E.t
type 'elt slist =
'elt Raw.t
(* singleton inductive, whose constructor was Build_slist *)
(** val this : 'a1 slist -> 'a1 Raw.t **)
let this s =
s
type 'elt t = 'elt slist
(** val empty : 'a1 t **)
let empty =
Raw.empty
(** val is_empty : 'a1 t -> bool **)
let is_empty m =
Raw.is_empty (this m)
(** val add : key -> 'a1 -> 'a1 t -> 'a1 t **)
let add x e m =
Raw.add x e (this m)
(** val find : key -> 'a1 t -> 'a1 option **)
let find x m =
Raw.find x (this m)
(** val remove : key -> 'a1 t -> 'a1 t **)
let remove x m =
Raw.remove x (this m)
(** val mem : key -> 'a1 t -> bool **)
let mem x m =
Raw.mem x (this m)
(** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
let map f m =
Raw.map f (this m)
(** val mapi : (key -> 'a1 -> 'a2) -> 'a1 t -> 'a2 t **)
let mapi f m =
Raw.mapi f (this m)
(** val map2 :
('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t -> 'a3 t **)
let map2 f m m' =
Raw.map2 f (this m) (this m')
(** val elements : 'a1 t -> (key * 'a1) list **)
let elements m =
Raw.elements (this m)
(** val cardinal : 'a1 t -> int **)
let cardinal m =
length (this m)
(** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 **)
let fold f m i =
Raw.fold f (this m) i
(** val equal : ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool **)
let equal cmp m m' =
Raw.equal cmp (this m) (this m')
end
module type UsualOrderedType =
sig
type t
val compare : t -> t -> t compare0
val eq_dec : t -> t -> bool
end
module Nat_as_OT =
struct
type t = int
(** val compare : int -> int -> int compare0 **)
let compare x y =
match Nat.compare x y with
| Eq -> EQ
| Lt -> LT
| Gt -> GT
(** val eq_dec : int -> int -> bool **)
let eq_dec =
(=)
end
type 'a dyadic = ('a, 'a * 'a) sum
(** val dyadic_eq_dec :
('a1 -> 'a1 -> bool) -> 'a1 dyadic -> 'a1 dyadic -> bool **)
let dyadic_eq_dec a_eq_dec d d' =
match d with
| Inl wildcard' ->
(match d' with
| Inl a' -> a_eq_dec wildcard' a'
| Inr _ -> false)
| Inr wildcard' ->
let (a0, a1) = wildcard' in
(match d' with
| Inl _ -> false
| Inr p0 ->
let (a'0, a'1) = p0 in
let filtered_var = a_eq_dec a0 a'0 in
let filtered_var0 = a_eq_dec a1 a'1 in
if filtered_var then filtered_var0 else false)
(** val dyadic_compare :
('a1 -> 'a1 -> 'a1 compare0) -> 'a1 dyadic -> 'a1 dyadic -> 'a1 dyadic
compare0 **)
let dyadic_compare a_compare x y =
match x with
| Inl l0 ->
(match y with
| Inl l1 ->
let filtered_var = a_compare l0 l1 in
(match filtered_var with
| LT -> LT
| EQ -> EQ
| GT -> GT)
| Inr _ -> LT)
| Inr p0 ->
let (l0, l0') = p0 in
(match y with
| Inl _ -> GT
| Inr p1 ->
let (l1, l1') = p1 in
let filtered_var = a_compare l0 l1 in
(match filtered_var with
| LT -> LT
| EQ ->
let filtered_var0 = a_compare l0' l1' in
(match filtered_var0 with
| LT -> LT
| EQ -> EQ
| GT -> GT)
| GT -> GT))
module DyadicLexLtUsualOrderedType =
functor (UOT:UsualOrderedType) ->
struct
type t = UOT.t dyadic
(** val eq_dec : UOT.t dyadic -> UOT.t dyadic -> bool **)
let eq_dec =
dyadic_eq_dec UOT.eq_dec
(** val compare : UOT.t dyadic -> UOT.t dyadic -> UOT.t dyadic compare0 **)
let compare =
dyadic_compare UOT.compare
end
module Fitch =
functor (UOT:UsualOrderedType) ->
functor (DUOT:sig
type t = UOT.t dyadic
val compare : t -> t -> t compare0
val eq_dec : t -> t -> bool
end) ->
functor (Map:S with module E = DUOT) ->
struct
type 'a p = 'a
type l = UOT.t
type n = int
(** val eq_n : n -> n -> bool **)
let rec eq_n n0 x0 =
(fun fO fS n -> if n=0 then fO () else fS (n-1))
(fun _ ->
(fun fO fS n -> if n=0 then fO () else fS (n-1))
(fun _ -> true)
(fun _ -> false)
x0)
(fun n1 ->
(fun fO fS n -> if n=0 then fO () else fS (n-1))
(fun _ -> false)
(fun n2 -> eq_n n1 n2)
x0)
n0
type justification =
| Coq_justification_premise
| Coq_justification_lem
| Coq_justification_copy of l
| Coq_justification_andi of l * l
| Coq_justification_ande1 of l
| Coq_justification_ande2 of l
| Coq_justification_ori1 of l
| Coq_justification_ori2 of l
| Coq_justification_impe of l * l
| Coq_justification_nege of l * l
| Coq_justification_conte of l
| Coq_justification_negnegi of l
| Coq_justification_negnege of l
| Coq_justification_mt of l * l
| Coq_justification_impi of l * l
| Coq_justification_negi of l * l
| Coq_justification_ore of l * l * l * l * l
| Coq_justification_pbc of l * l
(** val justification_rect :
'a1 -> 'a1 -> (l -> 'a1) -> (l -> l -> 'a1) -> (l -> 'a1) -> (l -> 'a1)
-> (l -> 'a1) -> (l -> 'a1) -> (l -> l -> 'a1) -> (l -> l -> 'a1) -> (l
-> 'a1) -> (l -> 'a1) -> (l -> 'a1) -> (l -> l -> 'a1) -> (l -> l ->
'a1) -> (l -> l -> 'a1) -> (l -> l -> l -> l -> l -> 'a1) -> (l -> l ->
'a1) -> justification -> 'a1 **)
let justification_rect f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 = function
| Coq_justification_premise -> f
| Coq_justification_lem -> f0
| Coq_justification_copy x -> f1 x
| Coq_justification_andi (x, x0) -> f2 x x0
| Coq_justification_ande1 x -> f3 x
| Coq_justification_ande2 x -> f4 x
| Coq_justification_ori1 x -> f5 x
| Coq_justification_ori2 x -> f6 x
| Coq_justification_impe (x, x0) -> f7 x x0
| Coq_justification_nege (x, x0) -> f8 x x0
| Coq_justification_conte x -> f9 x
| Coq_justification_negnegi x -> f10 x
| Coq_justification_negnege x -> f11 x
| Coq_justification_mt (x, x0) -> f12 x x0
| Coq_justification_impi (x, x0) -> f13 x x0
| Coq_justification_negi (x, x0) -> f14 x x0
| Coq_justification_ore (x, x0, x1, x2, x3) -> f15 x x0 x1 x2 x3
| Coq_justification_pbc (x, x0) -> f16 x x0
(** val justification_rec :
'a1 -> 'a1 -> (l -> 'a1) -> (l -> l -> 'a1) -> (l -> 'a1) -> (l -> 'a1)
-> (l -> 'a1) -> (l -> 'a1) -> (l -> l -> 'a1) -> (l -> l -> 'a1) -> (l
-> 'a1) -> (l -> 'a1) -> (l -> 'a1) -> (l -> l -> 'a1) -> (l -> l ->
'a1) -> (l -> l -> 'a1) -> (l -> l -> l -> l -> l -> 'a1) -> (l -> l ->
'a1) -> justification -> 'a1 **)
let justification_rec f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 = function
| Coq_justification_premise -> f
| Coq_justification_lem -> f0
| Coq_justification_copy x -> f1 x
| Coq_justification_andi (x, x0) -> f2 x x0
| Coq_justification_ande1 x -> f3 x
| Coq_justification_ande2 x -> f4 x
| Coq_justification_ori1 x -> f5 x
| Coq_justification_ori2 x -> f6 x
| Coq_justification_impe (x, x0) -> f7 x x0
| Coq_justification_nege (x, x0) -> f8 x x0
| Coq_justification_conte x -> f9 x
| Coq_justification_negnegi x -> f10 x
| Coq_justification_negnege x -> f11 x
| Coq_justification_mt (x, x0) -> f12 x x0
| Coq_justification_impi (x, x0) -> f13 x x0
| Coq_justification_negi (x, x0) -> f14 x x0
| Coq_justification_ore (x, x0, x1, x2, x3) -> f15 x x0 x1 x2 x3
| Coq_justification_pbc (x, x0) -> f16 x x0
type reason =
| Coq_reason_assumption
| Coq_reason_justification of justification
(** val reason_rect : 'a1 -> (justification -> 'a1) -> reason -> 'a1 **)
let reason_rect f f0 = function
| Coq_reason_assumption -> f
| Coq_reason_justification x -> f0 x
(** val reason_rec : 'a1 -> (justification -> 'a1) -> reason -> 'a1 **)
let reason_rec f f0 = function
| Coq_reason_assumption -> f
| Coq_reason_justification x -> f0 x
type 'a prop =
| Coq_prop_p of 'a p
| Coq_prop_neg of 'a prop
| Coq_prop_and of 'a prop * 'a prop
| Coq_prop_or of 'a prop * 'a prop
| Coq_prop_imp of 'a prop * 'a prop
| Coq_prop_cont
(** val prop_rect :
('a1 p -> 'a2) -> ('a1 prop -> 'a2 -> 'a2) -> ('a1 prop -> 'a2 -> 'a1
prop -> 'a2 -> 'a2) -> ('a1 prop -> 'a2 -> 'a1 prop -> 'a2 -> 'a2) ->
('a1 prop -> 'a2 -> 'a1 prop -> 'a2 -> 'a2) -> 'a2 -> 'a1 prop -> 'a2 **)
let rec prop_rect f f0 f1 f2 f3 f4 = function
| Coq_prop_p p5 -> f p5
| Coq_prop_neg prop5 -> f0 prop5 (prop_rect f f0 f1 f2 f3 f4 prop5)
| Coq_prop_and (prop5, prop') ->
f1 prop5 (prop_rect f f0 f1 f2 f3 f4 prop5) prop'
(prop_rect f f0 f1 f2 f3 f4 prop')
| Coq_prop_or (prop5, prop') ->
f2 prop5 (prop_rect f f0 f1 f2 f3 f4 prop5) prop'
(prop_rect f f0 f1 f2 f3 f4 prop')
| Coq_prop_imp (prop5, prop') ->
f3 prop5 (prop_rect f f0 f1 f2 f3 f4 prop5) prop'
(prop_rect f f0 f1 f2 f3 f4 prop')
| Coq_prop_cont -> f4
(** val prop_rec :
('a1 p -> 'a2) -> ('a1 prop -> 'a2 -> 'a2) -> ('a1 prop -> 'a2 -> 'a1
prop -> 'a2 -> 'a2) -> ('a1 prop -> 'a2 -> 'a1 prop -> 'a2 -> 'a2) ->
('a1 prop -> 'a2 -> 'a1 prop -> 'a2 -> 'a2) -> 'a2 -> 'a1 prop -> 'a2 **)
let rec prop_rec f f0 f1 f2 f3 f4 = function
| Coq_prop_p p5 -> f p5
| Coq_prop_neg prop5 -> f0 prop5 (prop_rec f f0 f1 f2 f3 f4 prop5)
| Coq_prop_and (prop5, prop') ->
f1 prop5 (prop_rec f f0 f1 f2 f3 f4 prop5) prop'
(prop_rec f f0 f1 f2 f3 f4 prop')
| Coq_prop_or (prop5, prop') ->
f2 prop5 (prop_rec f f0 f1 f2 f3 f4 prop5) prop'
(prop_rec f f0 f1 f2 f3 f4 prop')
| Coq_prop_imp (prop5, prop') ->
f3 prop5 (prop_rec f f0 f1 f2 f3 f4 prop5) prop'
(prop_rec f f0 f1 f2 f3 f4 prop')
| Coq_prop_cont -> f4
type 'a derivation =
| Coq_derivation_deriv of l * 'a prop * reason
(** val derivation_rect :
(l -> 'a1 prop -> reason -> 'a2) -> 'a1 derivation -> 'a2 **)
let derivation_rect f = function
| Coq_derivation_deriv (x, x0, x1) -> f x x0 x1
(** val derivation_rec :
(l -> 'a1 prop -> reason -> 'a2) -> 'a1 derivation -> 'a2 **)
let derivation_rec f = function
| Coq_derivation_deriv (x, x0, x1) -> f x x0 x1
type 'a entry =
| Coq_entry_derivation of 'a derivation
| Coq_entry_box of 'a entry list
| Coq_entry_invalid
(** val entry_rect :
('a1 derivation -> 'a2) -> ('a1 entry list -> 'a2) -> 'a2 -> 'a1 entry
-> 'a2 **)
let entry_rect f f0 f1 = function
| Coq_entry_derivation x -> f x
| Coq_entry_box x -> f0 x
| Coq_entry_invalid -> f1
(** val entry_rec :
('a1 derivation -> 'a2) -> ('a1 entry list -> 'a2) -> 'a2 -> 'a1 entry
-> 'a2 **)
let entry_rec f f0 f1 = function
| Coq_entry_derivation x -> f x
| Coq_entry_box x -> f0 x
| Coq_entry_invalid -> f1
type 'a proplist = 'a prop list
type 'a proof = 'a entry list
type 'a judgment =
| Coq_judgment_follows of 'a proplist * 'a prop
(** val judgment_rect :
('a1 proplist -> 'a1 prop -> 'a2) -> 'a1 judgment -> 'a2 **)
let judgment_rect f = function
| Coq_judgment_follows (x, x0) -> f x x0
(** val judgment_rec :
('a1 proplist -> 'a1 prop -> 'a2) -> 'a1 judgment -> 'a2 **)
let judgment_rec f = function
| Coq_judgment_follows (x, x0) -> f x x0
type 'a dyadicprop = 'a prop dyadic
type 'a claim =
| Coq_claim_judgment_proof of 'a judgment * 'a proof
(** val claim_rect :
('a1 judgment -> 'a1 proof -> 'a2) -> 'a1 claim -> 'a2 **)
let claim_rect f = function
| Coq_claim_judgment_proof (x, x0) -> f x x0
(** val claim_rec :
('a1 judgment -> 'a1 proof -> 'a2) -> 'a1 claim -> 'a2 **)
let claim_rec f = function
| Coq_claim_judgment_proof (x, x0) -> f x x0
type 'a coq_G = 'a dyadicprop Map.t
end
module FitchProgram =
functor (UOT:UsualOrderedType) ->
functor (DUOT:sig
type t = UOT.t dyadic
val compare : t -> t -> t compare0
val eq_dec : t -> t -> bool
end) ->
functor (Map:S with module E = DUOT) ->
struct
module FitchPI = Fitch(UOT)(DUOT)(Map)
(** val prop_eq_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.prop -> 'a1 FitchPI.prop -> bool **)
let prop_eq_dec a_eq_dec prop5 prop' =
FitchPI.prop_rect (fun p5 x ->
match x with
| FitchPI.Coq_prop_p p0 -> a_eq_dec p5 p0
| _ -> false) (fun _ x x0 ->
match x0 with
| FitchPI.Coq_prop_neg prop1 -> x prop1
| _ -> false) (fun _ x _ x0 x1 ->
match x1 with
| FitchPI.Coq_prop_and (prop1, prop'1) ->
if x prop1 then x0 prop'1 else false
| _ -> false) (fun _ x _ x0 x1 ->
match x1 with
| FitchPI.Coq_prop_or (prop1, prop'1) ->
if x prop1 then x0 prop'1 else false
| _ -> false) (fun _ x _ x0 x1 ->
match x1 with
| FitchPI.Coq_prop_imp (prop1, prop'1) ->
if x prop1 then x0 prop'1 else false
| _ -> false) (fun x ->
match x with
| FitchPI.Coq_prop_cont -> true
| _ -> false) prop5 prop'
(** val valid_derivation_deriv_premise_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> bool **)
let valid_derivation_deriv_premise_dec a_eq_dec _ proplist5 _ prop5 =
in_dec (prop_eq_dec a_eq_dec) prop5 proplist5
(** val valid_derivation_deriv_lem_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> bool **)
let valid_derivation_deriv_lem_dec a_eq_dec _ _ _ = function
| FitchPI.Coq_prop_or (prop', prop'0) ->
(match prop'0 with
| FitchPI.Coq_prop_neg prop7 -> prop_eq_dec a_eq_dec prop' prop7
| FitchPI.Coq_prop_cont -> false
| _ -> false)
| FitchPI.Coq_prop_cont -> false
| _ -> false
(** val valid_derivation_deriv_copy_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_copy_dec a_eq_dec g5 _ _ prop5 l6 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl prop' -> prop_eq_dec a_eq_dec prop5 prop'
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_andi_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_andi_dec a_eq_dec g5 _ _ prop5 l6 l7 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl prop6 ->
(match Map.find (Inl l7) g5 with
| Some d0 ->
(match d0 with
| Inl prop7 ->
prop_eq_dec a_eq_dec prop5 (FitchPI.Coq_prop_and (prop6,
prop7))
| Inr _ -> false)
| None -> false)
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_ande1_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_ande1_dec a_eq_dec g5 _ _ prop5 l6 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl p0 ->
(match p0 with
| FitchPI.Coq_prop_and (prop6, _) ->
prop_eq_dec a_eq_dec prop5 prop6
| _ -> false)
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_ande2_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_ande2_dec a_eq_dec g5 _ _ prop5 l6 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl p0 ->
(match p0 with
| FitchPI.Coq_prop_and (_, prop7) ->
prop_eq_dec a_eq_dec prop5 prop7
| _ -> false)
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_ori1_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_ori1_dec a_eq_dec g5 _ _ prop5 l6 =
match prop5 with
| FitchPI.Coq_prop_or (prop6, _) ->
(match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl prop' -> prop_eq_dec a_eq_dec prop6 prop'
| Inr _ -> false)
| None -> false)
| _ -> false
(** val valid_derivation_deriv_ori2_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_ori2_dec a_eq_dec g5 _ _ prop5 l6 =
match prop5 with
| FitchPI.Coq_prop_or (_, prop7) ->
(match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl prop' -> prop_eq_dec a_eq_dec prop7 prop'
| Inr _ -> false)
| None -> false)
| _ -> false
(** val valid_derivation_deriv_impe_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_impe_dec a_eq_dec g5 _ _ prop5 l6 l7 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl prop6 ->
(match Map.find (Inl l7) g5 with
| Some d0 ->
(match d0 with
| Inl p0 ->
(match p0 with
| FitchPI.Coq_prop_imp (prop7, prop8) ->
if prop_eq_dec a_eq_dec prop6 prop7
then prop_eq_dec a_eq_dec prop5 prop8
else false
| _ -> false)
| Inr _ -> false)
| None -> false)
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_nege_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_nege_dec a_eq_dec g5 _ _ prop5 l6 l7 =
match prop5 with
| FitchPI.Coq_prop_cont ->
(match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl prop6 ->
(match Map.find (Inl l7) g5 with
| Some d0 ->
(match d0 with
| Inl p0 ->
(match p0 with
| FitchPI.Coq_prop_neg prop7 ->
prop_eq_dec a_eq_dec prop6 prop7
| _ -> false)
| Inr _ -> false)
| None -> false)
| Inr _ -> false)
| None -> false)
| _ -> false
(** val valid_derivation_deriv_conte_dec :
'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist -> FitchPI.l -> 'a1
FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_conte_dec g5 _ _ _ l6 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl p0 -> (match p0 with
| FitchPI.Coq_prop_cont -> true
| _ -> false)
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_negnegi_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_negnegi_dec a_eq_dec g5 _ _ prop5 l6 =
match prop5 with
| FitchPI.Coq_prop_neg prop0 ->
(match prop0 with
| FitchPI.Coq_prop_neg prop6 ->
(match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl prop7 -> prop_eq_dec a_eq_dec prop6 prop7
| Inr _ -> false)
| None -> false)
| _ -> false)
| _ -> false
(** val valid_derivation_deriv_negnege_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> bool **)
let valid_derivation_deriv_negnege_dec a_eq_dec g5 _ _ prop5 l6 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl p0 ->
(match p0 with
| FitchPI.Coq_prop_neg prop0 ->
(match prop0 with
| FitchPI.Coq_prop_neg prop6 -> prop_eq_dec a_eq_dec prop5 prop6
| _ -> false)
| _ -> false)
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_mt_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_mt_dec a_eq_dec g5 _ _ prop5 l6 l7 =
match prop5 with
| FitchPI.Coq_prop_neg prop6 ->
(match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl p0 ->
(match p0 with
| FitchPI.Coq_prop_imp (prop7, prop8) ->
if prop_eq_dec a_eq_dec prop6 prop7
then (match Map.find (Inl l7) g5 with
| Some d0 ->
(match d0 with
| Inl p1 ->
(match p1 with
| FitchPI.Coq_prop_neg prop9 ->
prop_eq_dec a_eq_dec prop8 prop9
| _ -> false)
| Inr _ -> false)
| None -> false)
else false
| _ -> false)
| Inr _ -> false)
| None -> false)
| _ -> false
(** val valid_derivation_deriv_impi_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_impi_dec a_eq_dec g5 _ _ prop5 l6 l7 =
match prop5 with
| FitchPI.Coq_prop_imp (prop6, prop7) ->
(match Map.find (Inr (l6, l7)) g5 with
| Some d ->
(match d with
| Inl _ -> false
| Inr p0 ->
let (prop8, prop9) = p0 in
if prop_eq_dec a_eq_dec prop6 prop8
then prop_eq_dec a_eq_dec prop7 prop9
else false)
| None -> false)
| _ -> false
(** val valid_derivation_deriv_negi_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_negi_dec a_eq_dec g5 _ _ prop5 l6 l7 =
match prop5 with
| FitchPI.Coq_prop_neg prop6 ->
(match Map.find (Inr (l6, l7)) g5 with
| Some d ->
(match d with
| Inl _ -> false
| Inr p0 ->
let (prop7, p1) = p0 in
(match p1 with
| FitchPI.Coq_prop_cont -> prop_eq_dec a_eq_dec prop6 prop7
| _ -> false))
| None -> false)
| _ -> false
(** val valid_derivation_deriv_ore_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> FitchPI.l ->
FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_ore_dec a_eq_dec g5 _ _ prop5 l6 l7 l8 l9 l10 =
match Map.find (Inl l6) g5 with
| Some d ->
(match d with
| Inl p0 ->
(match p0 with
| FitchPI.Coq_prop_or (prop6, prop7) ->
(match Map.find (Inr (l7, l8)) g5 with
| Some d0 ->
(match d0 with
| Inl _ -> false
| Inr p1 ->
let (prop8, prop9) = p1 in
if prop_eq_dec a_eq_dec prop6 prop8
then if prop_eq_dec a_eq_dec prop5 prop9
then (match Map.find (Inr (l9, l10)) g5 with
| Some d1 ->
(match d1 with
| Inl _ -> false
| Inr p2 ->
let (prop10, prop11) = p2 in
if prop_eq_dec a_eq_dec prop7 prop10
then prop_eq_dec a_eq_dec prop5 prop11
else false)
| None -> false)
else false
else false)
| None -> false)
| _ -> false)
| Inr _ -> false)
| None -> false
(** val valid_derivation_deriv_pbc_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.l -> FitchPI.l -> bool **)
let valid_derivation_deriv_pbc_dec a_eq_dec g5 _ _ prop5 l6 l7 =
match Map.find (Inr (l6, l7)) g5 with
| Some d ->
(match d with
| Inl _ -> false
| Inr p0 ->
let (p1, p2) = p0 in
(match p1 with
| FitchPI.Coq_prop_neg prop6 ->
(match p2 with
| FitchPI.Coq_prop_cont -> prop_eq_dec a_eq_dec prop5 prop6
| _ -> false)
| _ -> false))
| None -> false
(** val valid_derivation_deriv_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
FitchPI.l -> 'a1 FitchPI.prop -> FitchPI.reason -> bool **)
let valid_derivation_deriv_dec a_eq_dec g5 proplist5 l5 prop5 = function
| FitchPI.Coq_reason_assumption -> false
| FitchPI.Coq_reason_justification justification5 ->
(match justification5 with
| FitchPI.Coq_justification_premise ->
valid_derivation_deriv_premise_dec a_eq_dec g5 proplist5 l5 prop5
| FitchPI.Coq_justification_lem ->
valid_derivation_deriv_lem_dec a_eq_dec g5 proplist5 l5 prop5
| FitchPI.Coq_justification_copy l6 ->
valid_derivation_deriv_copy_dec a_eq_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_andi (l6, l7) ->
valid_derivation_deriv_andi_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7
| FitchPI.Coq_justification_ande1 l6 ->
valid_derivation_deriv_ande1_dec a_eq_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_ande2 l6 ->
valid_derivation_deriv_ande2_dec a_eq_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_ori1 l6 ->
valid_derivation_deriv_ori1_dec a_eq_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_ori2 l6 ->
valid_derivation_deriv_ori2_dec a_eq_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_impe (l6, l7) ->
valid_derivation_deriv_impe_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7
| FitchPI.Coq_justification_nege (l6, l7) ->
valid_derivation_deriv_nege_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7
| FitchPI.Coq_justification_conte l6 ->
valid_derivation_deriv_conte_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_negnegi l6 ->
valid_derivation_deriv_negnegi_dec a_eq_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_negnege l6 ->
valid_derivation_deriv_negnege_dec a_eq_dec g5 proplist5 l5 prop5 l6
| FitchPI.Coq_justification_mt (l6, l7) ->
valid_derivation_deriv_mt_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7
| FitchPI.Coq_justification_impi (l6, l7) ->
valid_derivation_deriv_impi_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7
| FitchPI.Coq_justification_negi (l6, l7) ->
valid_derivation_deriv_negi_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7
| FitchPI.Coq_justification_ore (l6, l7, l8, l9, l10) ->
valid_derivation_deriv_ore_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7 l8
l9 l10
| FitchPI.Coq_justification_pbc (l6, l7) ->
valid_derivation_deriv_pbc_dec a_eq_dec g5 proplist5 l5 prop5 l6 l7)
(** val valid_proof_entry_list_ :
('a1 FitchPI.coq_G -> 'a1 FitchPI.proplist -> 'a1 FitchPI.entry ->
bool) -> 'a1 FitchPI.entry list -> 'a1 FitchPI.coq_G -> 'a1
FitchPI.proplist -> bool **)
let rec valid_proof_entry_list_ valid_entry_dec0 ls g5 proplist5 =
match ls with
| [] -> true
| e :: ls' ->
(match e with
| FitchPI.Coq_entry_derivation derivation5 ->
let FitchPI.Coq_derivation_deriv (l5, prop5, reason5) = derivation5
in
(match reason5 with
| FitchPI.Coq_reason_assumption -> false
| FitchPI.Coq_reason_justification _ ->
if valid_entry_dec0 g5 proplist5 e
then valid_proof_entry_list_ valid_entry_dec0 ls'
(Map.add (Inl l5) (Inl prop5) g5) proplist5
else false)
| FitchPI.Coq_entry_box proof5 ->
(match proof5 with
| [] -> false
| e' :: _ ->
(match e' with
| FitchPI.Coq_entry_derivation derivation5 ->
let FitchPI.Coq_derivation_deriv (l5, prop5, reason5) =
derivation5
in
(match reason5 with
| FitchPI.Coq_reason_assumption ->
(match last proof5 FitchPI.Coq_entry_invalid with
| FitchPI.Coq_entry_derivation derivation6 ->
let FitchPI.Coq_derivation_deriv (l6, prop6, _) =
derivation6
in
if valid_entry_dec0 g5 proplist5 e
then valid_proof_entry_list_ valid_entry_dec0 ls'
(Map.add (Inr (l5, l6)) (Inr (prop5, prop6)) g5)
proplist5
else false
| _ -> false)
| FitchPI.Coq_reason_justification _ -> false)
| _ -> false))
| FitchPI.Coq_entry_invalid -> false)
(** val valid_entry_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
'a1 FitchPI.entry -> bool **)
let rec valid_entry_dec a_eq_dec g5 proplist5 = function
| FitchPI.Coq_entry_derivation derivation5 ->
let FitchPI.Coq_derivation_deriv (l5, prop5, reason5) = derivation5 in
(match reason5 with
| FitchPI.Coq_reason_assumption -> false
| FitchPI.Coq_reason_justification justification5 ->
valid_derivation_deriv_dec a_eq_dec g5 proplist5 l5 prop5
(FitchPI.Coq_reason_justification justification5))
| FitchPI.Coq_entry_box proof5 ->
(match proof5 with
| [] -> false
| e0 :: ls' ->
(match e0 with
| FitchPI.Coq_entry_derivation derivation5 ->
let FitchPI.Coq_derivation_deriv (l5, prop5, reason5) = derivation5
in
(match reason5 with
| FitchPI.Coq_reason_assumption ->
valid_proof_entry_list_ (valid_entry_dec a_eq_dec) ls'
(Map.add (Inl l5) (Inl prop5) g5) proplist5
| FitchPI.Coq_reason_justification _ -> false)
| _ -> false))
| FitchPI.Coq_entry_invalid -> false
(** val valid_proof_entry_list :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.entry list -> 'a1 FitchPI.coq_G ->
'a1 FitchPI.proplist -> bool **)
let valid_proof_entry_list a_eq_dec =
valid_proof_entry_list_ (valid_entry_dec a_eq_dec)
(** val valid_proof_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.coq_G -> 'a1 FitchPI.proplist ->
'a1 FitchPI.proof -> bool **)
let valid_proof_dec a_eq_dec g5 proplist5 proof5 =
valid_proof_entry_list a_eq_dec proof5 g5 proplist5
(** val valid_claim_dec :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.claim -> bool **)
let valid_claim_dec a_eq_dec = function
| FitchPI.Coq_claim_judgment_proof (judgment5, proof5) ->
(match last proof5 FitchPI.Coq_entry_invalid with
| FitchPI.Coq_entry_derivation derivation5 ->
let FitchPI.Coq_derivation_deriv (_, prop5, reason5) = derivation5 in
(match reason5 with
| FitchPI.Coq_reason_assumption -> false
| FitchPI.Coq_reason_justification _ ->
let FitchPI.Coq_judgment_follows (proplist5, prop') = judgment5 in
if prop_eq_dec a_eq_dec prop5 prop'
then valid_proof_dec a_eq_dec Map.empty proplist5 proof5
else false)
| _ -> false)
(** val validate_claim :
('a1 -> 'a1 -> bool) -> 'a1 FitchPI.claim -> bool **)
let validate_claim a_eq_dec c =
if valid_claim_dec a_eq_dec c then true else false
end
module Nat_as_DUOT = DyadicLexLtUsualOrderedType(Nat_as_OT)
module Map = Make(Nat_as_DUOT)
module FitchProgramMap = FitchProgram(Nat_as_OT)(Nat_as_DUOT)(Map)
(** val valid_claim_dec0 : char list FitchProgramMap.FitchPI.claim -> bool **)
let valid_claim_dec0 =
FitchProgramMap.valid_claim_dec string_dec
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment