# Library Beroal.Init

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 before 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.

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.

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.

Definition rel_dec_bool_equiv a b : true = rel_dec_bool a b <-> rel a b.

Definition rel_dec_bool_refl a : true = rel_dec_bool a a.

Definition rel_dec_bool_sym a b : rel_dec_bool a b = rel_dec_bool b a.

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

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.

Definition half_odd (n : nat) : odd n -> n = S (half n + half n).

End half.

Definition half_le (n : nat) : half (S n) <= n.

Definition half_lt (n : nat) : IsSucc n -> half n < n.

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.

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

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.