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 : (∀ (p : Prop) (p0 p1 : p), p0 = p1)
→ ∀ (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.

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
⇒ ∀ 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 : ∀ 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 : ∀ (t:Type) (r:relation t),
        (reflexive _ r)
        → (∀ x1 x2 y, r x1 x2 → r x1 y → r x2 y)
        → equivalence _ r.

Definition quotient_equivalence : ∀ 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

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)
) : ∀ n, ~succ_ord n O.

succ_ord is irreflexive

Definition succ_ord_irrefl := (fun n eq1
⇒ Coq.Init.Peano.n_Sn _ (sym_eq eq1)
) : ∀ 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.