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.
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
Composition of functions. Respecting tradition bc goes before ab
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).
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.
-> 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.
=> 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
return default value if None
Definition Some_or_default := fun t (o : option t) default
=> match o with None => default | Some x => x end.
=> 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.
=> 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.
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.
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].
:= 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.
=> (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].
:= 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).
=> (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).
=> (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.
m is a successor of n
O is not a successor
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).
=> 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.
: 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.