Set Implicit Arguments.
Require Import Coq.Relations.Relation_Definitions.
Require Coq.Arith.Le.
Require Coq.Arith.Lt.
Require Coq.Arith.Plus.
Require Import Coq.Arith.Even.
Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List.

(** identity function *)
Definition id := fun t (a : t) => a.

(** Composition of functions. Respecting tradition [bc] goes #<strong>before</strong># [ab] *)
Definition cf := fun a b c (bc : b -> c) (ab : a -> b)
	=> fun x => bc (ab x).

(** two functions with reciprocal types *)
Definition iff_Type := fun a b : Type => ((a -> b) * (b -> a))%type.

Definition decidable_Prop := fun p : Prop => sumbool p (~ p).
Definition decidable_Type := fun p : Type => sum p (p -> False).

(** This is different from standard [ProofIrrelevanceTheory.subset_eq_compat]. The standard theorem narrows [t] to [Set], contrary to [sig] definition. *)
Definition sig_eq : (forall (p : Prop) (p0 p1 : p), p0 = p1)
	-> forall (t : Type) (p : t -> Prop) (a0 a1 : sig p),
	proj1_sig a0 = proj1_sig a1 -> a0 = a1.
Proof.
refine (fun pi t p a0 => _).
destruct a0 as [v0 p0].
refine (fun a1 => _).
destruct a1 as [v1 p1].
simpl.
refine (fun eq0 => _ p0 p1).
refine (eq_ind _
	(fun dep => forall (p00:_) (p10:p dep), _ = exist _ dep _)
	_ _ eq0).
refine (fun p00 p10 => f_equal _ (pi _ p00 p10)).
Qed.

(** [IsSucc] is equivalent to [0 <] *)
Definition lt_IsSucc := fun n:nat
	=> match n as n return O < n <-> IsSucc n
	with O => conj
		(fun lt1 => match Coq.Arith.Lt.lt_irrefl _ lt1 with end)
		(fun f:False => match f with end)
	| S pn => conj (fun _ => I)
		(fun _ => Coq.Arith.Lt.le_lt_n_Sm _ _
			(Coq.Arith.Le.le_O_n pn))
	end.

(** Haskell.base.Data.Maybe.maybe *)
Definition match_option a b : (a -> b) -> b -> option a -> b
	:= option_rect (fun _ => b).

(** return default value if [None] *)
Definition Some_or_default := fun t (o : option t) default
	=> match o with None => default | Some x => x end.



(** a type with decidable equality *)
Definition decidable_equality := fun e : Type
	=> forall x y : e, decidable_Prop (x = y).

Section decidable_relation.
Record type_rel_dec : Type :=
{ trd_type : Type
; trd_rel : relation trd_type
; trd_equiv : equivalence _ trd_rel
; trd_dec : forall x y : trd_type, decidable_Prop (trd_rel x y)
}.
Variable trd : type_rel_dec.
Let type := trd_type trd.
Let rel := trd_rel trd.
Let equiv := trd_equiv trd.
Let dec := trd_dec trd.

(** boolean equality *)
Definition rel_dec_bool a b := if dec a b then true else false.

(* ==> rel_dec_bool_prop *)
Definition rel_dec_bool_equiv a b : true = rel_dec_bool a b <-> rel a b.
Proof.
unfold rel_dec_bool.
refine (fun a b => _).
destruct (dec a b) as [p|p].
refine (conj (fun _ => p) (fun _ => refl_equal _)).
refine (conj (fun eq0 => match Coq.Bool.Bool.diff_true_false eq0 with end)
	(fun eq0 => match p eq0 with end)).
Qed.

Definition rel_dec_bool_refl a : true = rel_dec_bool a a.
Proof.
refine (fun a => proj2 (rel_dec_bool_equiv a a) (equiv_refl _ _ equiv _)).
Qed.

Definition rel_dec_bool_sym a b : rel_dec_bool a b = rel_dec_bool b a.
Proof.
refine (fun a b => _).
unfold rel_dec_bool.
destruct (dec a b) as [p0|p0].
destruct (dec b a) as [p1|p1].
refine (refl_equal _).
refine (match p1 (equiv_sym _ _ equiv _ _ p0) with end).
destruct (dec b a) as [p1|p1].
refine (match p0 (equiv_sym _ _ equiv _ _ p1) with end).
refine (refl_equal _).
Qed.

Definition rel_dec_bool_trans a b c
: true = negb (rel_dec_bool a b) || negb (rel_dec_bool b c) || (rel_dec_bool a c).
Proof.
refine (fun a b c => _).
unfold rel_dec_bool.
destruct (dec a b) as [p0|p0].
destruct (dec b c) as [p1|p1].
destruct (dec a c) as [p2|p2].
simpl.
refine (refl_equal _).
simpl.
refine (match p2 (equiv_trans _ _ equiv _ _ _ p0 p1) with end).
simpl.
refine (refl_equal _).
simpl.
refine (refl_equal _).
Qed.

End decidable_relation.



Section half.

Definition half := fix rec (n : nat) := match n with
	| O => 0
	| S pn => match pn with
		| O => 0
		| S ppn => S (rec ppn)
		end
	end.

Definition half_even (n : nat) : even n -> n = half n + half n.
Proof.
refine (fix rec n0 (p0 : even n0) {struct p0} := _).
destruct p0 as [|n1 p1].
refine (refl_equal _).
destruct p1 as [n2 p2].
simpl.
refine (f_equal S _).
refine (eq_ind _ (fun dep => _ = dep)
_ _ (Coq.Arith.Plus.plus_Snm_nSm _ _)).
refine (f_equal S (rec _ p2)).
Qed.

Definition half_odd (n : nat) : odd n -> n = S (half n + half n).
Proof.
refine (fix rec n0 (p0 : odd n0) {struct p0} := _).
destruct p0 as [n1 p1].
destruct p1 as [|n2 p2].
refine (refl_equal _).
simpl.
refine (f_equal S (f_equal S _)).
refine (eq_ind _ (fun dep => _ = dep)
_ _ (Coq.Arith.Plus.plus_Snm_nSm _ _)).
refine (rec _ p2).
Qed.

End half.

Definition half_le (n : nat) : half (S n) <= n.
Proof.
refine (fix rec (n0 : nat) := _).
destruct n0 as [|n1].
refine (le_n _).
destruct n1 as [|n2].
refine (le_n _).
change (S (half (S n2)) <= S (S n2)).
refine (Coq.Arith.Le.le_n_S _ _ (le_S _ _ (rec _))).
Qed.

Definition half_lt (n : nat) : IsSucc n -> half n < n.
Proof.
refine (fun n0 => _).
destruct n0 as [|n1].
refine (fun false_prop => match false_prop with end).
refine (fun _ => Coq.Arith.Le.le_n_S _ _ (half_le _)).
Qed.



(** Relations *)

Definition subst2equivalence : forall (t:Type) (r:relation t),
	(reflexive _ r)
	-> (forall x1 x2 y, r x1 x2 -> r x1 y -> r x2 y)
	-> equivalence _ r.
Proof.
refine (fun t r refl p => _).
refine (let sym := (fun x1 x2 r1 => p _ _ _ r1 (refl _)) : symmetric _ r in _).
refine (Build_equivalence _ _ refl _ _).
unfold transitive.
	refine (fun _ _ _ rx2x1 rx1y => p _ _ _ (sym _ _ rx2x1) rx1y).
refine (sym).
Defined.

Definition quotient_equivalence : forall a r (quotient_map : a -> r)
	(rel : relation r), equivalence r rel
	-> equivalence a (fun c d => rel (quotient_map c) (quotient_map d)).
Proof.
refine (fun a r f rel rel_equiv => _).
refine (Build_equivalence _ _ _ _ _).
unfold reflexive.
	refine (fun _ => equiv_refl _ _ rel_equiv _).
unfold transitive.
	refine (fun _ _ _ => equiv_trans _ _ rel_equiv _ _ _).
unfold symmetric.
	refine (fun _ _ => equiv_sym _ _ rel_equiv _ _).
Defined.

Definition implication_preorder := (Build_preorder
	Prop (fun x y : Prop => x -> y)
	(fun p (x:p) => x)
	(fun p1 p2 p3 imp12 imp23 => fun p11 => imp23 (imp12 p11))
	) : preorder Prop (fun x y : Prop => x -> y).

Definition iff_equivalence := (Build_equivalence Prop iff
	Coq.Init.Logic.iff_refl
	Coq.Init.Logic.iff_trans
	Coq.Init.Logic.iff_sym
	) : equivalence Prop iff.

Check fun t => @eq t : relation t.
Definition eq_equivalence := fun t => (Build_equivalence _ (@eq t)
	(@Coq.Init.Logic.refl_equal t)
	(@Coq.Init.Logic.trans_eq t)
	(@Coq.Init.Logic.sym_eq t)
	) : equivalence _ (@eq t).

Definition Acc_irrefl := fun (t : Type) (r : relation t)
	=> fix rec (x : t) (acc1 : Acc r x) (x_refl : r x x) : False
	:= match acc1 return False
	with Acc_intro all_pred => rec _ (all_pred x x_refl) x_refl end.



(** * Iterator; repeat function; [nat] to Church numeral. Also nat_rect. *)
Definition rep := fun (t:Type) (f:t->t) => fix rec (n:nat) {struct n}
	:= match n with O => fun x=>x | S pn => fun x => f (rec pn x) end.
	Implicit Arguments rep [t].

(** [rep f n] commutes with [f] *)
Definition rep_fun_comm_fun := fun (t:Type) (f:t->t) n x
	=> (fix rec (n:nat) : f (rep f n x)=rep f n (f x)
	:= match n as n return f (rep f n x)=rep f n (f x)
		with O => refl_equal _
		| S pn => f_equal _ (rec pn)
		end
	) n.

(** tail-recursive version of [rep] *)
Definition reptr
	:= fun (t : Type) (f : t -> t) => fix rec (n : nat) {struct n}
	:= match n
		with O => fun x=>x
		| S pn => fun x => rec pn (f x)
		end.
	Implicit Arguments reptr [t].

(** [reptr f n] commutes with [f] *)
Definition reptr_fun_comm_fun := fun (t : Type) (f : t -> t)
	=> (fix rec (n : nat) x : f (reptr f n x) = reptr f n (f x)
	:= match n as n return f (reptr f n x) = reptr f n (f x)
	with O => refl_equal _
	| S pn => rec pn (f x)
	end).

(** [rep] is pointwise equal to [reptr] *)
Definition rep_eq_reptr := fun (t : Type) (f : t -> t)
	=> (fix rec (n : nat) x : rep f n x = reptr f n x
	:= match n as n return rep f n x = reptr f n x
	with O => refl_equal _
	| S pn => match reptr_fun_comm_fun _ _ _ in _=dep
		return rep f (S pn) x = dep
		with refl_equal => f_equal f (rec pn x) end
	end).

(** composition of [rep], [reptr] is an action of [nat] on function composition *)

Definition rep_plus := fun (t:Type) (f:t->t) n m x
	=> (fix rec (n:nat) : rep f (n+m) x = rep f n (rep f m x)
	:= match n as n return rep f (n+m) x = rep f n (rep f m x)
		with O => refl_equal _
		| S pn => f_equal f (rec pn)
		end
	) n.

Definition reptr_plus := fun (t:Type) (f:t->t) n m
	=> (fix rec (n:nat) x : reptr f (n+m) x = reptr f m (reptr f n x)
	:= match n as n return reptr f (n+m) x = reptr f m (reptr f n x)
		with O => refl_equal _
		| S pn => rec pn (f x)
		end
	) n.



(** * Successor relation *)

(** m is a successor of n *)
Definition succ_ord n m := (S n) = m.
Check succ_ord : relation nat.

(** O is not a successor *)
Check (fun n eq1 => Coq.Init.Peano.O_S _ (sym_eq eq1)
	) : forall n, ~succ_ord n O.

(** succ_ord is irreflexive *)
Definition succ_ord_irrefl := (fun n eq1
	=> Coq.Init.Peano.n_Sn _ (sym_eq eq1)
	) : forall n, ~(succ_ord n n).

(** succ_ord is a well-founded relation *)
Definition succ_ord_wf := fix rec (n:nat)
	: Acc succ_ord n
	:= match n as n return Acc succ_ord n
	with O => Acc_intro O
		(fun _ spz => match Coq.Init.Peano.O_S _ (sym_eq spz) with end)
	| S pn => Acc_intro (R:=succ_ord) (S pn) (fun y spy
		=> match spy in _=dep
		return Acc succ_ord (pred dep) -> Acc succ_ord y
		with refl_equal => fun x=>x
		end (rec pn))
	end.