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.

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.

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.