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