+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
-(* ||A|| E.Tassi, S.Zacchiroli *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU Lesser General Public License Version 2.1 *)
-(* *)
-(**************************************************************************)
-
-(* $Id: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *)
-
-set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun".
-include "algebra/Setoids.ma".
-
-
-definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
-\lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
- \exists a:A. (csf_fun A B f) a \neq (csf_fun A B g) a.
-(* Definition ap_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
- {a : A | f a[#]g a}. *)
-
-definition eq_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
-\lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
- \forall a:A. (csf_fun A B f) a = (csf_fun A B g) a.
-(* Definition eq_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
- forall a : A, f a[=]g a. *)
-
-lemma irrefl_apfun : \forall A,B : CSetoid.
- irreflexive (CSetoid_fun A B) (ap_fun A B).
-intros.
-unfold irreflexive. intro f.
-unfold ap_fun.
-unfold.
-intro.
-elim H.
-cut (csf_fun A B f a = csf_fun A B f a)
-[ apply (eq_imp_not_ap A)
- [
- assumption|assumption|apply eq_reflexive_unfolded|
- apply (csf_strext_unfolded A B f).
- exact H1
- ]
-|apply eq_reflexive_unfolded
-]
-qed.
-
-(*
-Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
-intros A B.
-unfold irreflexive in |- *.
-intros f.
-unfold ap_fun in |- *.
-red in |- *.
-intro H.
-elim H.
-intros a H0.
-set (H1 := ap_irreflexive_unfolded B (f a)) in *.
-intuition.
-Qed.
-*)
-
-
-lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B).
-intros (A B).
-unfold.
-unfold ap_fun.
-intros (f g H h).
-elim H.
-lapply (ap_cotransitive ? ? ? H1 (csf_fun A B h a)).
-elim Hletin.
-left.
-apply (ex_intro ? ? a H2).
-right.
-apply (ex_intro ? ? a H2).
-qed.
-
-lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
-unfold tight_apart.
-intros (A B f g).
-unfold ap_fun.
-unfold eq_fun.
-split
-[ intros. apply not_ap_imp_eq.
-unfold.intro.apply H.
-apply (ex_intro ? ? a).assumption.
- | intros.unfold.intro.
- elim H1.
- apply (eq_imp_not_ap ? ? ? ? H2).
- apply H.
-]
-qed.
-
-lemma sym_apfun : \forall A, B : CSetoid. symmetric (ap_fun A B).
-intros.unfold.
-intros.
-unfold .unfold.
-elim H.
-apply (ex_intro ? ? a).
-apply ap_symmetric_unfolded.
-assumption.
-qed.
-
-definition FS_is_CSetoid : \forall A, B : CSetoid. ? \def
- \lambda A, B : CSetoid.
- mk_is_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
- (irrefl_apfun A B) (sym_apfun A B) (cotrans_apfun A B) (ta_apfun A B).
-
-definition FS_as_CSetoid : \forall A, B : CSetoid. ? \def
- \lambda A, B : CSetoid.
- mk_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
- (FS_is_CSetoid A B).
-
-(* Nullary and n-ary operations
-*)
-
-definition is_nullary_operation : \forall S:CSetoid. \forall s:S. Prop \def
-\lambda S:CSetoid. \lambda s:S. True.
-
-(*
-Definition is_nullary_operation (S:CSetoid) (s:S):Prop := True.
-*)
-
-let rec n_ary_operation (n:nat) (V:CSetoid) on n : CSetoid \def
-match n with
-[ O \Rightarrow V
-|(S m) \Rightarrow (FS_as_CSetoid V (n_ary_operation m V))].
-
-
-(* Section unary_function_composition. *)
-
-(* Composition of Setoid functions
-
-Let [S1], [S2] and [S3] be setoids, [f] a
-setoid function from [S1] to [S2], and [g] from [S2]
-to [S3] in the following definition of composition. *)
-
-(* Variables S1 S2 S3 : CSetoid.
-Variable f : CSetoid_fun S1 S2.
-Variable g : CSetoid_fun S2 S3. *)
-
-
-definition compose_CSetoid_fun : \forall S1,S2,S3 :CSetoid. \forall f: (CSetoid_fun S1 S2). \forall g: (CSetoid_fun S2 S3).
-CSetoid_fun S1 S3.
-intros (S1 S2 S3 f g).
-apply (mk_CSetoid_fun ? ? (\lambda x :cs_crr S1. csf_fun S2 S3 g (csf_fun S1 S2 f x))).
-(* str_ext *)
-unfold fun_strext.
-intros (x y H).
-apply (csf_strext ? ? f).
-apply (csf_strext ? ? g).
-assumption.
-qed.
-
-(* End unary_function_composition. *)
-
-(* Composition as operation *)
-definition comp : \forall A, B, C : CSetoid.
-FS_as_CSetoid A B \to FS_as_CSetoid B C \to FS_as_CSetoid A C.
-intros (A B C f g).
-letin H \def (compose_CSetoid_fun A B C f g).
-exact H.
-qed.
-
-definition comp_as_bin_op : \forall A:CSetoid. CSetoid_bin_op (FS_as_CSetoid A A).
-intro A.
-unfold CSetoid_bin_op.
-apply (mk_CSetoid_bin_fun ? ? ? (comp A A A)).
-unfold bin_fun_strext.
-unfold comp.
-intros 4 (f1 f2 g1 g2).
-simplify.
-unfold compose_CSetoid_fun.
-simplify.
-elim f1 0.
-unfold fun_strext.
-clear f1.
-intros 2 (f1 Hf1).
-elim f2 0.
-unfold fun_strext.
-clear f2.
-intros 2 (f2 Hf2).
-elim g1 0.
-unfold fun_strext.
-clear g1.
-intros 2 (g1 Hg1).
-elim g2 0.
-unfold fun_strext.
-clear g2.
-intros 2 (g2 Hg2).
-simplify.
-intro H.
-elim H 0.
-clear H.
-intros 2 (a H).
-letin H0 \def (ap_cotransitive A (g1 (f1 a)) (g2 (f2 a)) H (g2 (f1 a))).
-elim H0 0.
-clear H0.
-intro H0.
-right.
-exists.
-apply (f1 a).
-exact H0.
-
-clear H0.
-intro H0.
-left.
-exists.
-apply a.
-apply Hg2.
-exact H0.
-qed.
-
-
-(* Questa coercion composta non e' stata generata automaticamente *)
-lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S).
- intros;
- unfold in c;
- apply (c c1 c2).
-qed.
-coercion cic:/matita/algebra/CoRN/SetoidFun/mycor.con 2.
-
-(* Mettendola a mano con una beta-espansione funzionerebbe *)
-(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (\lambda e.mycor ? (comp_as_bin_op A) e)).*)
-(* Questo sarebbe anche meglio: senza beta-espansione *)
-(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))).*)
-(* QUESTO E' QUELLO ORIGINALE MA NON FUNZIONANTE *)
-(* lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)). *)
-lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)).
-unfold associative in |- *.
-unfold comp_as_bin_op in |- *.
-intros A f g h.
-simpl in |- *.
-unfold eq_fun in |- *.
-simpl in |- *.
-intuition.
-Qed.
-
-Lemma assoc_comp : forall A : CSetoid, associative (comp_as_bin_op A).
-unfold associative in |- *.
-unfold comp_as_bin_op in |- *.
-intros A f g h.
-simpl in |- *.
-unfold eq_fun in |- *.
-simpl in |- *.
-intuition.
-Qed.
-
-Section unary_and_binary_function_composition.
-
-Definition compose_CSetoid_bin_un_fun (A B C : CSetoid)
- (f : CSetoid_bin_fun B B C) (g : CSetoid_fun A B) : CSetoid_bin_fun A A C.
-intros A B C f g.
-apply (Build_CSetoid_bin_fun A A C (fun a0 a1 : A => f (g a0) (g a1))).
-intros x1 x2 y1 y2 H0.
-assert (H10:= csbf_strext B B C f).
-red in H10.
-assert (H40 := csf_strext A B g).
-red in H40.
-elim (H10 (g x1) (g x2) (g y1) (g y2) H0); [left | right]; auto.
-Defined.
-
-Definition compose_CSetoid_bin_fun A B C (f g : CSetoid_fun A B)
- (h : CSetoid_bin_fun B B C) : CSetoid_fun A C.
-intros A B C f g h.
-apply (Build_CSetoid_fun A C (fun a : A => h (f a) (g a))).
-intros x y H.
-elim (csbf_strext _ _ _ _ _ _ _ _ H); apply csf_strext.
-Defined.
-
-Definition compose_CSetoid_un_bin_fun A B C (f : CSetoid_bin_fun B B C)
- (g : CSetoid_fun C A) : CSetoid_bin_fun B B A.
-intros A0 B0 C f g.
-apply Build_CSetoid_bin_fun with (fun x y : B0 => g (f x y)).
-intros x1 x2 y1 y2.
-case f.
-simpl in |- *.
-unfold bin_fun_strext in |- *.
-case g.
-simpl in |- *.
-unfold fun_strext in |- *.
-intros gu gstrext fu fstrext H.
-apply fstrext.
-apply gstrext.
-exact H.
-Defined.
-
-End unary_and_binary_function_composition.
-
-(** ***Projections
-*)
-
-Section function_projection.
-
-Lemma proj_bin_fun : forall A B C (f : CSetoid_bin_fun A B C) a, fun_strext (f a).
-intros A B C f a.
-red in |- *.
-elim f.
-intro fo.
-simpl.
-intros csbf_strext0 x y H.
-elim (csbf_strext0 _ _ _ _ H); intro H0.
- elim (ap_irreflexive_unfolded _ _ H0).
-exact H0.
-Qed.
-
-Definition projected_bin_fun A B C (f : CSetoid_bin_fun A B C) (a : A) :=
- Build_CSetoid_fun B C (f a) (proj_bin_fun A B C f a).
-
-End function_projection.
-
-Section BinProj.
-
-Variable S : CSetoid.
-
-Definition binproj1 (x y:S) := x.
-
-Lemma binproj1_strext : bin_fun_strext _ _ _ binproj1.
-red in |- *; auto.
-Qed.
-
-Definition cs_binproj1 : CSetoid_bin_op S.
-red in |- *; apply Build_CSetoid_bin_op with binproj1.
-apply binproj1_strext.
-Defined.
-
-End BinProj.
-
-(** **Combining operations
-%\begin{convention}% Let [S1], [S2] and [S3] be setoids.
-%\end{convention}%
-*)
-
-Section CombiningOperations.
-Variables S1 S2 S3 : CSetoid.
-
-(**
-In the following definition, we assume [f] is a setoid function from
-[S1] to [S2], and [op] is an unary operation on [S2].
-Then [opOnFun] is the composition [op] after [f].
-*)
-Section CombiningUnaryOperations.
-Variable f : CSetoid_fun S1 S2.
-Variable op : CSetoid_un_op S2.
-
-Definition opOnFun : CSetoid_fun S1 S2.
-apply (Build_CSetoid_fun S1 S2 (fun x : S1 => op (f x))).
-(* str_ext *)
-unfold fun_strext in |- *; intros x y H.
-apply (csf_strext _ _ f x y).
-apply (csf_strext _ _ op _ _ H).
-Defined.
-
-End CombiningUnaryOperations.
-
-End CombiningOperations.
-
-Section p66E2b4.
-
-(** **The Free Setoid
-%\begin{convention}% Let [A:CSetoid].
-%\end{convention}%
-*)
-Variable A:CSetoid.
-
-Definition Astar := (list A).
-
-Definition empty_word := (nil A).
-
-Definition appA:= (app A).
-
-Fixpoint eq_fm (m:Astar)(k:Astar){struct m}:Prop:=
-match m with
-|nil => match k with
- |nil => True
- |cons a l => False
- end
-|cons b n => match k with
- |nil => False
- |cons a l => b[=]a /\ (eq_fm n l)
- end
-end.
-
-Fixpoint ap_fm (m:Astar)(k:Astar){struct m}: CProp :=
-match m with
-|nil => match k with
- |nil => CFalse
- |cons a l => CTrue
- end
-|cons b n => match k with
- |nil => CTrue
- |cons a l => b[#]a or (ap_fm n l)
- end
-end.
-
-Lemma ap_fm_irreflexive: (irreflexive ap_fm).
-unfold irreflexive.
-intro x.
-induction x.
-simpl.
-red.
-intuition.
-
-simpl.
-red.
-intro H.
-apply IHx.
-elim H.
-clear H.
-generalize (ap_irreflexive A a).
-unfold Not.
-intuition.
-
-intuition.
-Qed.
-
-
-Lemma ap_fm_symmetric: Csymmetric ap_fm.
-unfold Csymmetric.
-intros x.
-induction x.
-intro y.
-case y.
-simpl.
-intuition.
-
-simpl.
-intuition.
-simpl.
-intro y.
-case y.
-simpl.
-intuition.
-
-simpl.
-intros c l H0.
-elim H0.
-generalize (ap_symmetric A a c).
-intuition.
-clear H0.
-intro H0.
-right.
-apply IHx.
-exact H0.
-Qed.
-
-Lemma ap_fm_cotransitive : (cotransitive ap_fm).
-unfold cotransitive.
-intro x.
-induction x.
-simpl.
-intro y.
-case y.
-intuition.
-
-intros c l H z.
-case z.
-simpl.
-intuition.
-
-intuition.
-
-simpl.
-intro y.
-case y.
-intros H z.
-case z.
-intuition.
-
-simpl.
-intuition.
-
-intros c l H z.
-case z.
-intuition.
-
-simpl.
-intros c0 l0.
-elim H.
-clear H.
-intro H.
-generalize (ap_cotransitive A a c H c0).
-intuition.
-
-clear H.
-intro H.
-generalize (IHx l H l0).
-intuition.
-Qed.
-
-Lemma ap_fm_tight : (tight_apart eq_fm ap_fm).
-unfold tight_apart.
-intros x.
-induction x.
-simpl.
-intro y.
-case y.
-red.
-unfold Not.
-intuition.
-
-intuition.
-
-intro y.
-simpl.
-case y.
-intuition.
-
-intros c l.
-generalize (IHx l).
-red.
-intro H0.
-elim H0.
-intros H1 H2.
-split.
-intro H3.
-split.
-red in H3.
-generalize (ap_tight A a c).
-intuition.
-
-apply H1.
-intro H4.
-apply H3.
-right.
-exact H4.
-
-intro H3.
-elim H3.
-clear H3.
-intros H3 H4.
-intro H5.
-elim H5.
-generalize (ap_tight A a c).
-intuition.
-
-apply H2.
-exact H4.
-Qed.
-
-Definition free_csetoid_is_CSetoid:(is_CSetoid Astar eq_fm ap_fm):=
- (Build_is_CSetoid Astar eq_fm ap_fm ap_fm_irreflexive ap_fm_symmetric
- ap_fm_cotransitive ap_fm_tight).
-
-Definition free_csetoid_as_csetoid:CSetoid:=
-(Build_CSetoid Astar eq_fm ap_fm free_csetoid_is_CSetoid).
-
-Lemma app_strext:
- (bin_fun_strext free_csetoid_as_csetoid free_csetoid_as_csetoid
- free_csetoid_as_csetoid appA).
-unfold bin_fun_strext.
-intros x1.
-induction x1.
-simpl.
-intro x2.
-case x2.
-simpl.
-intuition.
-
-intuition.
-
-intros x2 y1 y2.
-simpl.
-case x2.
-case y2.
-simpl.
-intuition.
-
-simpl.
-intuition.
-
-case y2.
-simpl.
-simpl in IHx1.
-intros c l H.
-elim H.
-intuition.
-
-clear H.
-generalize (IHx1 l y1 (nil A)).
-intuition.
-
-simpl.
-intros c l c0 l0.
-intro H.
-elim H.
-intuition.
-
-generalize (IHx1 l0 y1 (cons c l)).
-intuition.
-Qed.
-
-Definition app_as_csb_fun:
-(CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
- free_csetoid_as_csetoid):=
- (Build_CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
- free_csetoid_as_csetoid appA app_strext).
-
-Lemma eq_fm_reflexive: forall (x:Astar), (eq_fm x x).
-intro x.
-induction x.
-simpl.
-intuition.
-
-simpl.
-intuition.
-Qed.
-
-End p66E2b4.
-
-(** **Partial Functions
-
-In this section we define a concept of partial function for an
-arbitrary setoid. Essentially, a partial function is what would be
-expected---a predicate on the setoid in question and a total function
-from the set of points satisfying that predicate to the setoid. There
-is one important limitations to this approach: first, the record we
-obtain has type [Type], meaning that we can't use, for instance,
-elimination of existential quantifiers.
-
-Furthermore, for reasons we will explain ahead, partial functions will
-not be defined via the [CSetoid_fun] record, but the whole structure
-will be incorporated in a new record.
-
-Finally, notice that to be completely general the domains of the
-functions have to be characterized by a [CProp]-valued predicate;
-otherwise, the use you can make of a function will be %\emph{%#<i>#a
-priori#</i>#%}% restricted at the moment it is defined.
-
-Before we state our definitions we need to do some work on domains.
-*)
-
-Section SubSets_of_G.
-
-(** ***Subsets of Setoids
-
-Subsets of a setoid will be identified with predicates from the
-carrier set of the setoid into [CProp]. At this stage, we do not make
-any assumptions about these predicates.
-
-We will begin by defining elementary operations on predicates, along
-with their basic properties. In particular, we will work with well
-defined predicates, so we will prove that these operations preserve
-welldefinedness.
-
-%\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
-%\end{convention}%
-*)
-
-Variable S : CSetoid.
-
-Section Conjunction.
-
-Variables P Q : S -> CProp.
-
-Definition conjP (x : S) : CProp := P x and Q x.
-
-Lemma prj1 : forall x : S, conjP x -> P x.
-intros x H; inversion_clear H; assumption.
-Qed.
-
-Lemma prj2 : forall x : S, conjP x -> Q x.
-intros x H; inversion_clear H; assumption.
-Qed.
-
-Lemma conj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ conjP.
-intros H H0.
-red in |- *; intros x y H1 H2.
-inversion_clear H1; split.
-
-apply H with x; assumption.
-
-apply H0 with x; assumption.
-Qed.
-
-End Conjunction.
-
-Section Disjunction.
-
-Variables P Q : S -> CProp.
-
-(**
-Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
-*)
-
-Definition disj (x : S) : CProp := P x or Q x.
-
-Lemma inj1 : forall x : S, P x -> disj x.
-intros; left; assumption.
-Qed.
-
-Lemma inj2 : forall x : S, Q x -> disj x.
-intros; right; assumption.
-Qed.
-
-Lemma disj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ disj.
-intros H H0.
-red in |- *; intros x y H1 H2.
-inversion_clear H1.
-
-left; apply H with x; assumption.
-
-right; apply H0 with x; assumption.
-Qed.
-
-End Disjunction.
-
-Section Extension.
-
-(**
-The next definition is a bit tricky, and is useful for choosing among the elements that satisfy a predicate [P] those that also satisfy [R] in the case where [R] is only defined for elements satisfying [P]---consider [R] to be a condition on the image of an object via a function with domain [P]. We chose to call this operation [extension].
-*)
-
-Variable P : S -> CProp.
-Variable R : forall x : S, P x -> CProp.
-
-Definition extend (x : S) : CProp := P x and (forall H : P x, R x H).
-
-Lemma ext1 : forall x : S, extend x -> P x.
-intros x H; inversion_clear H; assumption.
-Qed.
-
-Lemma ext2_a : forall x : S, extend x -> {H : P x | R x H}.
-intros x H; inversion_clear H.
-exists X; auto.
-Qed.
-
-Lemma ext2 : forall (x : S) (Hx : extend x), R x (ProjT1 (ext2_a x Hx)).
-intros; apply projT2.
-Qed.
-
-Lemma extension_wd : pred_wd _ P ->
- (forall (x y : S) Hx Hy, x [=] y -> R x Hx -> R y Hy) -> pred_wd _ extend.
-intros H H0.
-red in |- *; intros x y H1 H2.
-elim H1; intros H3 H4; split.
-
-apply H with x; assumption.
-
-intro H5; apply H0 with x H3; [ apply H2 | apply H4 ].
-Qed.
-
-End Extension.
-
-End SubSets_of_G.
-
-Notation Conj := (conjP _).
-Implicit Arguments disj [S].
-
-Implicit Arguments extend [S].
-Implicit Arguments ext1 [S P R x].
-Implicit Arguments ext2 [S P R x].
-
-(** ***Operations
-
-We are now ready to define the concept of partial function between arbitrary setoids.
-*)
-
-Record BinPartFunct (S1 S2 : CSetoid) : Type :=
- {bpfdom : S1 -> CProp;
- bdom_wd : pred_wd S1 bpfdom;
- bpfpfun :> forall x : S1, bpfdom x -> S2;
- bpfstrx : forall x y Hx Hy, bpfpfun x Hx [#] bpfpfun y Hy -> x [#] y}.
-
-
-Notation BDom := (bpfdom _ _).
-Implicit Arguments bpfpfun [S1 S2].
-
-(**
-The next lemma states that every partial function is well defined.
-*)
-
-Lemma bpfwdef : forall S1 S2 (F : BinPartFunct S1 S2) x y Hx Hy,
- x [=] y -> F x Hx [=] F y Hy.
-intros.
-apply not_ap_imp_eq; intro H0.
-generalize (bpfstrx _ _ _ _ _ _ _ H0).
-exact (eq_imp_not_ap _ _ _ H).
-Qed.
-
-(** Similar for automorphisms. *)
-
-Record PartFunct (S : CSetoid) : Type :=
- {pfdom : S -> CProp;
- dom_wd : pred_wd S pfdom;
- pfpfun :> forall x : S, pfdom x -> S;
- pfstrx : forall x y Hx Hy, pfpfun x Hx [#] pfpfun y Hy -> x [#] y}.
-
-Notation Dom := (pfdom _).
-Notation Part := (pfpfun _).
-Implicit Arguments pfpfun [S].
-
-(**
-The next lemma states that every partial function is well defined.
-*)
-
-Lemma pfwdef : forall S (F : PartFunct S) x y Hx Hy, x [=] y -> F x Hx [=] F y Hy.
-intros.
-apply not_ap_imp_eq; intro H0.
-generalize (pfstrx _ _ _ _ _ _ H0).
-exact (eq_imp_not_ap _ _ _ H).
-Qed.
-
-(**
-A few characteristics of this definition should be explained:
- - The domain of the partial function is characterized by a predicate
-that is required to be well defined but not strongly extensional. The
-motivation for this choice comes from two facts: first, one very
-important subset of real numbers is the compact interval
-[[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
-[<=] b], which is not strongly extensional; on the other hand, if we
-can apply a function to an element [s] of a setoid [S] it seems
-reasonable (and at some point we do have to do it) to apply that same
-function to any element [s'] which is equal to [s] from the point of
-view of the setoid equality.
- - The last two conditions state that [pfpfun] is really a subsetoid
-function. The reason why we do not write it that way is the
-following: when applying a partial function [f] to an element [s] of
-[S] we also need a proof object [H]; with this definition the object
-we get is [f(s,H)], where the proof is kept separate from the object.
-Using subsetoid notation, we would get $f(\langle
-s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two
-projections to get either the original object or the proof, and we
-need to apply an extra constructor to get $f(\langle
-s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts
-to spending more resources when actually working with these objects.
- - This record has type [Type], which is very unfortunate, because it
-means in particular that we cannot use the well behaved set
-existential quantification over partial functions; however, later on
-we will manage to avoid this problem in a way that also justifies that
-we don't really need to use that kind of quantification. Another
-approach to this definition that completely avoid this complication
-would be to make [PartFunct] a dependent type, receiving the predicate
-as an argument. This does work in that it allows us to give
-[PartFunct] type [Set] and do some useful stuff with it; however, we
-are not able to define something as simple as an operator that gets a
-function and returns its domain (because of the restrictions in the
-type elimination rules). This sounds very unnatural, and soon gets us
-into strange problems that yield very unlikely definitions, which is
-why we chose to altogether do away with this approach.
-
-%\begin{convention}% All partial functions will henceforth be denoted by capital letters.
-%\end{convention}%
-
-We now present some methods for defining partial functions.
-*)
-
-Hint Resolve CI: core.
-
-Section CSetoid_Ops.
-
-Variable S : CSetoid.
-
-(**
-To begin with, we want to be able to ``see'' each total function as a partial function.
-*)
-
-Definition total_eq_part : CSetoid_un_op S -> PartFunct S.
-intros f.
-apply
- Build_PartFunct with (fun x : S => CTrue) (fun (x : S) (H : CTrue) => f x).
-red in |- *; intros; auto.
-intros x y Hx Hy H.
-exact (csf_strext_unfolded _ _ f _ _ H).
-Defined.
-
-Section Part_Function_Const.
-
-(**
-In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
-
-%\begin{convention}% Let [c:S].
-%\end{convention}%
-*)
-
-Variable c : S.
-
-Definition Fconst := total_eq_part (Const_CSetoid_fun _ _ c).
-
-End Part_Function_Const.
-
-Section Part_Function_Id.
-
-Definition Fid := total_eq_part (id_un_op S).
-
-End Part_Function_Id.
-
-(**
-(These happen to be always total functions, but that is more or less obvious, as we have no information on the setoid; however, we will be able to define partial functions just applying other operators to these ones.)
-
-If we have two setoid functions [F] and [G] we can always compose them. The domain of our new function will be the set of points [s] in the domain of [F] for which [F(s)] is in the domain of [G]#. #%\footnote{%Notice that the use of extension here is essential.%}.% The inversion in the order of the variables is done to maintain uniformity with the usual mathematical notation.
-
-%\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
-%\end{convention}%
-*)
-
-Section Part_Function_Composition.
-
-Variables G F : PartFunct S.
-
-(* begin hide *)
-Let P := Dom F.
-Let Q := Dom G.
-(* end hide *)
-Let R x := {Hx : P x | Q (F x Hx)}.
-
-Lemma part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
- G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
-intros x y Hx Hy H.
-exact (pfstrx _ _ _ _ _ _ (pfstrx _ _ _ _ _ _ H)).
-Qed.
-
-Lemma part_function_comp_dom_wd : pred_wd S R.
-red in |- *; intros x y H H0.
-unfold R in |- *; inversion_clear H.
-exists (dom_wd _ F x y x0 H0).
-apply (dom_wd _ G) with (F x x0).
-assumption.
-apply pfwdef; assumption.
-Qed.
-
-Definition Fcomp := Build_PartFunct _ R part_function_comp_dom_wd
- (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
- part_function_comp_strext.
-
-End Part_Function_Composition.
-
-End CSetoid_Ops.
-
-(**
-%\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
-%\end{convention}%
-*)
-
-Section BinPart_Function_Composition.
-
-Variables S1 S2 S3 : CSetoid.
-
-Variable G : BinPartFunct S2 S3.
-Variable F : BinPartFunct S1 S2.
-
-(* begin hide *)
-Let P := BDom F.
-Let Q := BDom G.
-(* end hide *)
-Let R x := {Hx : P x | Q (F x Hx)}.
-
-Lemma bin_part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
- G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
-intros x y Hx Hy H.
-exact (bpfstrx _ _ _ _ _ _ _ (bpfstrx _ _ _ _ _ _ _ H)).
-Qed.
-
-Lemma bin_part_function_comp_dom_wd : pred_wd S1 R.
-red in |- *; intros x y H H0.
-unfold R in |- *; inversion_clear H.
-exists (bdom_wd _ _ F x y x0 H0).
-apply (bdom_wd _ _ G) with (F x x0).
-assumption.
-apply bpfwdef; assumption.
-Qed.
-
-Definition BinFcomp := Build_BinPartFunct _ _ R bin_part_function_comp_dom_wd
- (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
- bin_part_function_comp_strext.
-
-End BinPart_Function_Composition.
-
-(* Different tokens for compatibility with coqdoc *)
-
-Implicit Arguments Fconst [S].
-Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
-
-Notation FId := (Fid _).
-
-Implicit Arguments Fcomp [S].
-Infix "[o]" := Fcomp (at level 65, no associativity).
-
-Hint Resolve pfwdef bpfwdef: algebra.
-
-Section bijections.
-(** **Bijections *)
-
-Definition injective A B (f : CSetoid_fun A B) := (forall a0 a1 : A,
- a0 [#] a1 -> f a0 [#] f a1):CProp.
-
-Definition injective_weak A B (f : CSetoid_fun A B) := forall a0 a1 : A,
- f a0 [=] f a1 -> a0 [=] a1.
-
-Definition surjective A B (f : CSetoid_fun A B) := (forall b : B, {a : A | f a [=] b}):CProp.
-
-Implicit Arguments injective [A B].
-Implicit Arguments injective_weak [A B].
-Implicit Arguments surjective [A B].
-
-Lemma injective_imp_injective_weak : forall A B (f : CSetoid_fun A B),
- injective f -> injective_weak f.
-intros A B f.
-unfold injective in |- *.
-intro H.
-unfold injective_weak in |- *.
-intros a0 a1 H0.
-apply not_ap_imp_eq.
-red in |- *.
-intro H1.
-set (H2 := H a0 a1 H1) in *.
-set (H3 := ap_imp_neq B (f a0) (f a1) H2) in *.
-set (H4 := eq_imp_not_neq B (f a0) (f a1) H0) in *.
-apply H4.
-exact H3.
-Qed.
-
-Definition bijective A B (f:CSetoid_fun A B) := injective f and surjective f.
-
-Implicit Arguments bijective [A B].
-
-Lemma id_is_bij : forall A, bijective (id_un_op A).
-intro A.
-split.
- red; simpl; auto.
-intro b; exists b; apply eq_reflexive.
-Qed.
-
-Lemma comp_resp_bij : forall A B C f g, bijective f -> bijective g ->
- bijective (compose_CSetoid_fun A B C f g).
-intros A B C f g.
-intros H0 H1.
-elim H0; clear H0; intros H00 H01.
-elim H1; clear H1; intros H10 H11.
-split.
- intros a0 a1; simpl; intro.
- apply H10; apply H00; auto.
-intro c; simpl.
-elim (H11 c); intros b H20.
-elim (H01 b); intros a H30.
-exists a.
-Step_final (g b).
-Qed.
-
-Lemma inv : forall A B (f:CSetoid_fun A B),
- bijective f -> forall b : B, {a : A | f a [=] b}.
-unfold bijective in |- *.
-unfold surjective in |- *.
-intuition.
-Qed.
-
-Implicit Arguments inv [A B].
-
-Definition invfun A B (f : CSetoid_fun A B) (H : bijective f) : B -> A.
-intros A B f H H0.
-elim (inv f H H0); intros a H2.
-apply a.
-Defined.
-
-Implicit Arguments invfun [A B].
-
-Lemma inv1 : forall A B (f : CSetoid_fun A B) (H : bijective f) (b : B),
- f (invfun f H b) [=] b.
-intros A B f H b.
-unfold invfun in |- *; case inv.
-simpl; auto.
-Qed.
-
-Lemma inv2 : forall A B (f : CSetoid_fun A B) (H : bijective f) (a : A),
- invfun f H (f a) [=] a.
-intros.
-unfold invfun in |- *; case inv; simpl.
-elim H; clear H; intros H0 H1.
-intro x.
-apply injective_imp_injective_weak.
-auto.
-Qed.
-
-Lemma inv_strext : forall A B (f : CSetoid_fun A B) (H : bijective f),
- fun_strext (invfun f H).
-intros A B f H x y.
-intro H1.
-elim H; intros H00 H01.
-elim (H01 x); intros a0 H2.
-elim (H01 y); intros a1 H3.
-astepl (f a0).
-astepr (f a1).
-apply H00.
-astepl (invfun f H x).
-astepr (invfun f H y).
-exact H1.
-astepl (invfun f H (f a1)).
-apply inv2.
-apply injective_imp_injective_weak with (f := f); auto.
-astepl (f a1).
-astepl y.
-apply eq_symmetric.
-apply inv1.
-apply eq_symmetric.
-apply inv1.
-astepl (invfun f H (f a0)).
-apply inv2.
-
-apply injective_imp_injective_weak with (f := f); auto.
-astepl (f a0).
-astepl x.
-apply eq_symmetric; apply inv1.
-apply eq_symmetric; apply inv1.
-Qed.
-
-Definition Inv A B f (H : bijective f) :=
- Build_CSetoid_fun B A (invfun f H) (inv_strext A B f H).
-
-Implicit Arguments Inv [A B].
-
-Definition Inv_bij : forall A B (f : CSetoid_fun A B) (H : bijective f),
- bijective (Inv f H).
-intros A B f H.
-unfold bijective in |- *.
-split.
-unfold injective in |- *.
-unfold bijective in H.
-unfold surjective in H.
-elim H.
-intros H0 H1.
-intros b0 b1 H2.
-elim (H1 b0).
-intros a0 H3.
-elim (H1 b1).
-intros a1 H4.
-astepl (Inv f (CAnd_intro _ _ H0 H1) (f a0)).
-astepr (Inv f (CAnd_intro _ _ H0 H1) (f a1)).
-cut (fun_strext f).
-unfold fun_strext in |- *.
-intros H5.
-apply H5.
-astepl (f a0).
-astepr (f a1).
-astepl b0.
-astepr b1.
-exact H2.
-apply eq_symmetric.
-unfold Inv in |- *.
-simpl in |- *.
-apply inv1.
-apply eq_symmetric.
-unfold Inv in |- *.
-simpl in |- *.
-apply inv1.
-elim f.
-intuition.
-
-unfold surjective in |- *.
-intro a.
-exists (f a).
-unfold Inv in |- *.
-simpl in |- *.
-apply inv2.
-Qed.
-
-
-End bijections.
-Implicit Arguments bijective [A B].
-Implicit Arguments injective [A B].
-Implicit Arguments injective_weak [A B].
-Implicit Arguments surjective [A B].
-Implicit Arguments inv [A B].
-Implicit Arguments invfun [A B].
-Implicit Arguments Inv [A B].
-
-Implicit Arguments conj_wd [S P Q].
-
-Notation Prj1 := (prj1 _ _ _ _).
-Notation Prj2 := (prj2 _ _ _ _).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
-(* ||A|| E.Tassi, S.Zacchiroli *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU Lesser General Public License Version 2.1 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/algebra/CoRN/Setoid".
-
-
-include "higher_order_defs/relations.ma".
-include "Z/plus.ma".
-
-include "datatypes/constructors.ma".
-include "nat/nat.ma".
-include "logic/equality.ma".
-(*include "Z/Zminus.ma".*)
-
-(* Setoids
-Definition of a constructive setoid with apartness,
-i.e. a set with an equivalence relation and an apartness relation compatible with it.
-*)
-
-(* Definition of Setoid
-Apartness, being the main relation, needs to be [CProp]-valued. Equality,
-as it is characterized by a negative statement, lives in [Prop].
-
-N.B. for the moment we use Prop for both (Matita group)
-*)
-
-record is_CSetoid (A : Type) (eq : relation A) (ap : relation A) : Prop \def
- {ax_ap_irreflexive : irreflexive A ap;
- ax_ap_symmetric : symmetric A ap;
- ax_ap_cotransitive : cotransitive A ap;
- ax_ap_tight : tight_apart A eq ap}.
-
-record CSetoid : Type \def
- {cs_crr :> Type;
- cs_eq : relation cs_crr;
- cs_ap : relation cs_crr;
- cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
-
-interpretation "setoid equality"
- 'eq x y = (cic:/matita/algebra/CoRN/Setoid/cs_eq.con _ x y).
-
-interpretation "setoid apart"
- 'neq x y = (cic:/matita/algebra/CoRN/Setoid/cs_ap.con _ x y).
-
-(* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
-"cs_neq" e "ap" non sono la stessa cosa? *)
-definition cs_neq : \forall S : CSetoid. relation S \def
- \lambda S : CSetoid. \lambda x,y : S. \not x = y.
-
-lemma CSetoid_is_CSetoid :
- \forall S : CSetoid. is_CSetoid S (cs_eq S) (cs_ap S).
-intro. apply (cs_proof S).
-qed.
-
-lemma ap_irreflexive: \forall S : CSetoid. irreflexive S (cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-lemma ap_symmetric : \forall S : CSetoid. symmetric S(cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-lemma ap_cotransitive : \forall S : CSetoid. cotransitive S (cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-lemma ap_tight : \forall S : CSetoid. tight_apart S (cs_eq S) (cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-definition ex_unq : \forall S : CSetoid. (S \to Prop) \to Prop \def
- \lambda S : CSetoid. \lambda P : S \to Prop.
- ex2 S (\lambda x. \forall y : S. P y \to x = y) P.
-
-
-lemma eq_reflexive : \forall S : CSetoid. reflexive S (cs_eq S).
-intro. unfold. intro.
-generalize in match (ap_tight S x x).
-intro.
-generalize in match (ap_irreflexive S x);
-elim H. apply H1. assumption.
-qed.
-
-axiom eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
-(*
-lemma eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
-intro. unfold. intros.
-generalize in match (ap_tight S x y). intro.
-generalize in match (ap_tight S y x). intro.
-generalize in match (ap_symmetric S y x). intro.
-elim H1. clear H1.
-elim H2. clear H2.
-apply H1. unfold. intro. auto.
-qed.
-*)
-lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S).
-intro. unfold. intros (x y z H H0).
-generalize in match (ap_tight S x y). intro.
-generalize in match (ap_tight S y z). intro.
-generalize in match (ap_tight S x z). intro.
-elim H3.
-apply H4. unfold. intro.
-generalize in match (ap_cotransitive ? ? ? H6 y). intro H7.
-elim H1 (H1' H1''). clear H1.
-elim H2 (H2' H2''). clear H2.
-elim H3 (H3' H3''). clear H3.
-elim H7 (H1). clear H7.
-generalize in match H1. apply H1''. assumption. (*non ho capito il secondo passo*)
-generalize in match H1. apply H2''. assumption.
-qed.
-
-lemma eq_reflexive_unfolded : \forall S:CSetoid. \forall x:S. x = x.
-apply eq_reflexive.
-qed.
-
-lemma eq_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S. x = y \to y = x.
-apply eq_symmetric.
-qed.
-
-lemma eq_transitive_unfolded : \forall S:CSetoid. \forall x,y,z:S. x = y \to y = z \to x = z.
-apply eq_transitive.
-qed.
-
-
-lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
-intros.
-(* perche' auto non arriva in fondo ??? *)
-apply (eq_transitive_unfolded ? ? x).
-apply eq_symmetric_unfolded.
-exact H1.
-exact H.
-qed.
-
-
-lemma ap_irreflexive_unfolded : \forall S:CSetoid. \forall x:S. \not (x \neq x).
-apply ap_irreflexive.
-qed.
-
-lemma ap_cotransitive_unfolded : \forall S:CSetoid. \forall a,b:S. a \neq b \to
- \forall c:S. a \neq c \or c \neq b.
-apply ap_cotransitive.
-qed.
-
-lemma ap_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S.
- x \neq y \to y \neq x.
-apply ap_symmetric.
-qed.
-
-lemma eq_imp_not_ap : \forall S:CSetoid. \forall x,y:S.
- x = y \to \not (x \neq y).
-intros.
-elim (ap_tight S x y).
-apply H2. assumption.
-qed.
-
-lemma not_ap_imp_eq : \forall S:CSetoid. \forall x,y:S.
- \not (x \neq y) \to x = y.
-intros.
-elim (ap_tight S x y).
-apply H1. assumption.
-qed.
-
-lemma neq_imp_notnot_ap : \forall S:CSetoid. \forall x,y:S.
- (cs_neq S x y) \to \not \not (x \neq y).
-intros. unfold. intro.
-apply H.
-apply not_ap_imp_eq.
-assumption.
-qed.
-
-lemma notnot_ap_imp_neq: \forall S:CSetoid. \forall x,y:S.
- (\not \not (x \neq y)) \to (cs_neq S x y).
-intros. unfold. unfold. intro.
-apply H.
-apply eq_imp_not_ap.
-assumption.
-qed.
-
-lemma ap_imp_neq : \forall S:CSetoid. \forall x,y:S.
- x \neq y \to (cs_neq S x y).
-intros. unfold. unfold. intro.
-apply (eq_imp_not_ap S ? ? H1).
-assumption.
-qed.
-
-lemma not_neq_imp_eq : \forall S:CSetoid. \forall x,y:S.
- \not (cs_neq S x y) \to x = y.
-intros.
-apply not_ap_imp_eq.
-unfold. intro.
-apply H.
-apply ap_imp_neq.
-assumption.
-qed.
-
-lemma eq_imp_not_neq : \forall S:CSetoid. \forall x,y:S.
- x = y \to \not (cs_neq S x y).
-intros. unfold. intro.
-apply H1.
-assumption.
-qed.
-
-
-
-(* -----------------The product of setoids----------------------- *)
-
-definition prod_ap: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: ProdT A B.
- ((cs_ap A (fstT A B c) (fstT A B d)) \or
- (cs_ap B (sndT A B c) (sndT A B d))).
-
-definition prod_eq: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: ProdT A B.
- ((cs_eq A (fstT A B c) (fstT A B d)) \and
- (cs_eq B (sndT A B c) (sndT A B d))).
-
-
-lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
- is_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B).
-intros.
-apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
- [unfold.
- intros.
- elim x.
- unfold.
- unfold prod_ap. simplify.
- intros.
- elim H
- [apply (ap_irreflexive A t H1)
- |apply (ap_irreflexive B t1 H1)
- ]
- |unfold.
- intros 2.
- elim x 2.
- elim y 2.
- unfold prod_ap. simplify.
- intro.
- elim H
- [left. apply ap_symmetric. assumption.
- |right. apply ap_symmetric. assumption
- ]
- |unfold.
- intros 2.
- elim x 2.
- elim y 4.
- elim z.
- unfold prod_ap in H. simplify in H.
- unfold prod_ap. simplify.
- elim H
- [cut ((t \neq t4) \or (t4 \neq t2))
- [elim Hcut
- [left. left. assumption
- |right. left. assumption
- ]
- |apply (ap_cotransitive A). assumption
- ]
- |cut ((t1 \neq t5) \or (t5 \neq t3))
- [elim Hcut
- [left. right. assumption
- |right. right. assumption
- ]
- |apply (ap_cotransitive B). assumption.
- ]
- ]
-|unfold.
- intros 2.
- elim x 2.
- elim y 2.
- unfold prod_ap. simplify.
- split
- [intro.
- left
- [apply not_ap_imp_eq.
- unfold. intro. apply H.
- left. assumption
- |apply not_ap_imp_eq.
- unfold. intro. apply H.
- right. assumption
- ]
- |intro. unfold. intro.
- elim H.
- elim H1
- [apply (eq_imp_not_ap A t t2 H2). assumption
- |apply (eq_imp_not_ap B t1 t3 H3). assumption
- ]
- ]
-]
-qed.
-
-
-definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
- \lambda A,B: CSetoid.
- mk_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
-
-
-
-(* Relations and predicates
-Here we define the notions of well-definedness and strong extensionality
-on predicates and relations.
-*)
-
-
-
-(*-----------------------------------------------------------------------*)
-(*-------------------------- Predicates on Setoids ----------------------*)
-(*-----------------------------------------------------------------------*)
-
-(* throughout this section consider (S : CSetoid) and (P : S -> Prop) *)
-
-(* Definition pred_strong_ext : CProp := forall x y : S, P x -> P y or x [#] y. *)
-definition pred_strong_ext : \forall S: CSetoid. (S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y: S.
- P x \to (P y \or (x \neq y)).
-
-(* Definition pred_wd : CProp := forall x y : S, P x -> x [=] y -> P y. *)
-definition pred_wd : \forall S: CSetoid. (S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y : S.
- P x \to x = y \to P y.
-
-record wd_pred (S: CSetoid) : Type \def
- {wdp_pred :> S \to Prop;
- wdp_well_def : pred_wd S wdp_pred}.
-
-record CSetoid_predicate (S: CSetoid) : Type \def
- {csp_pred :> S \to Prop;
- csp_strext : pred_strong_ext S csp_pred}.
-
-lemma csp_wd : \forall S: CSetoid. \forall P: CSetoid_predicate S.
- pred_wd S (csp_pred S P).
-intros.
-elim P.
-simplify.unfold pred_wd.
-intros.
-elim (H x y H1)
- [assumption|apply False_ind.apply (eq_imp_not_ap S x y H2 H3)]
-qed.
-
-
-(* Same result with CProp instead of Prop: but we just work with Prop (Matita group) *)
-(*
-Definition pred_strong_ext' : CProp := forall x y : S, P x -> P y or x [#] y.
-Definition pred_wd' : Prop := forall x y : S, P x -> x [=] y -> P y.
-
-Record CSetoid_predicate' : Type :=
- {csp'_pred :> S -> Prop;
- csp'_strext : pred_strong_ext' csp'_pred}.
-
-Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
-intro P.
-intro x; intros y H H0.
-elim (csp'_strext P x y H).
-
-auto.
-
-intro H1.
-elimtype False.
-generalize H1.
-exact (eq_imp_not_ap _ _ _ H0).
-Qed.
-*)
-
-
-
-(*------------------------------------------------------------------------*)
-(* --------------------------- Relations on Setoids --------------------- *)
-(*------------------------------------------------------------------------*)
-(* throughout this section consider (S : CSetoid) and (R : S -> S -> Prop) *)
-
-
-(* Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z. *)
-(*
- primo tentativo ma R non e' ben tipato: si puo' fare il cast giusto (carrier di S)
- in modo da sfruttare "relation"?
- e' concettualmente sbagliato lavorare ad un livello piu' alto (Type) ? *)
-(*
-definition rel_wdr : \forall S: CSetoid. \forall x,y,z: S. \lambda R: relation S. Prop \def
- \lambda S: CSetoid. \lambda x,y,z: S. \lambda R: relation S.
- R S x y \to y = z \to R S x z.
-
-definition rel_wdr : \forall S: CSetoid. \forall x,y,z: (cs_crr S). \lambda R: relation (cs_crr S). Prop \def
- \lambda S: CSetoid. \lambda x,y,z: (cs_crr S). \lambda R: relation (cs_crr S).
- R (cs_crr S) x y \to y = z \to R (cs_crr S) x z.
-*)
-definition rel_wdr : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
- R x y \to y = z \to R x z.
-
-(*Definition rel_wdl : Prop := forall x y z : S, R x y -> x [=] z -> R z y.*)
-definition rel_wdl : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
- R x y \to x = z \to R z y.
-
-(* Definition rel_strext : CProp := forall x1 x2 y1 y2 : S, R x1 y1 -> (x1 [#] x2 or y1 [#] y2) or R x2 y2. *)
-definition rel_strext : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y1,y2: S.
- R x1 y1 \to (x1 \neq x2 \or y1 \neq y2) \or R x2 y2.
-
-
-(* Definition rel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> x1 [#] x2 or R x2 y. *)
-definition rel_strext_lft : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y: S.
- R x1 y \to (x1 \neq x2 \or R x2 y).
-
-(* Definition rel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> y1 [#] y2 or R x y2. *)
-definition rel_strext_rht : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y1,y2: S.
- R x y1 \to (y1 \neq y2 \or R x y2).
-
-
-lemma rel_strext_imp_lftarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
- rel_strext S R \to rel_strext_lft S R.
-unfold rel_strext.
-unfold rel_strext_lft.
-intros.
-elim (H x1 x2 y y H1)
-[elim H2
- [left. assumption
- |absurd (y \neq y) [assumption | apply (ap_irreflexive S y)]
- ]
-|right. assumption
-]
-qed.
-
-
-lemma rel_strext_imp_rhtarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
- rel_strext S R \to rel_strext_rht S R.
-unfold rel_strext.
-unfold rel_strext_rht.
-intros.
-elim (H x x y1 y2 H1)
-[elim H2
- [absurd (x \neq x) [assumption | apply (ap_irreflexive S x)]
- |left. assumption
- ]
-|right. assumption
-]
-qed.
-
-
-lemma rel_strextarg_imp_strext : \forall S: CSetoid. \forall R: S \to S \to Prop.
- (rel_strext_rht S R) \to (rel_strext_lft S R) \to (rel_strext S R).
-unfold rel_strext_rht.
-unfold rel_strext_lft.
-unfold rel_strext.
-intros.
-elim ((H x1 y1 y2) H2)
-[left. right. assumption
-|elim ((H1 x1 x2 y1) H2)
- [left. left. assumption
- |elim ((H x2 y1 y2) H4)
- [left. right. assumption
- |right. assumption.
- ]
- ]
-]
-qed.
-
-(* ---------- Definition of a setoid relation ----------------- *)
-(* The type of relations over a setoid. *)
-
-(* TODO
-record CSetoid_relation1 (S: CSetoid) : Type \def
- {csr_rel : S \to S \to Prop;
- csr_wdr : rel_wdr S csr_rel;
- csr_wdl : rel_wdl S csr_rel;
- csr_strext : rel_strext S csr_rel}.
-*)
-(* CORN
-Record CSetoid_relation : Type :=
- {csr_rel :> S -> S -> Prop;
- csr_wdr : rel_wdr csr_rel;
- csr_wdl : rel_wdl csr_rel;
- csr_strext : rel_strext csr_rel}.
-*)
-
-
-(* ---------- gli stessi risultati di prima ma in CProp ---------*)
-(*
-Variable R : S -> S -> CProp.
-Definition Crel_wdr : CProp := forall x y z : S, R x y -> y [=] z -> R x z.
-Definition Crel_wdl : CProp := forall x y z : S, R x y -> x [=] z -> R z y.
-Definition Crel_strext : CProp := forall x1 x2 y1 y2 : S,
- R x1 y1 -> R x2 y2 or x1 [#] x2 or y1 [#] y2.
-
-Definition Crel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> R x2 y or x1 [#] x2.
-Definition Crel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> R x y2 or y1 [#] y2.
-
-Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
-Proof.
-unfold Crel_strext, Crel_strext_lft in |- *; intros H x1 x2 y H0.
-generalize (H x1 x2 y y).
-intro H1.
-elim (H1 H0).
-
-auto.
-
-intro H3.
-elim H3; intro H4.
-
-auto.
-elim (ap_irreflexive _ _ H4).
-Qed.
-
-Lemma Crel_strext_imp_rhtarg : Crel_strext -> Crel_strext_rht.
-unfold Crel_strext, Crel_strext_rht in |- *; intros H x y1 y2 H0.
-generalize (H x x y1 y2 H0); intro H1.
-elim H1; intro H2.
-
-auto.
-
-elim H2; intro H3.
-
-elim (ap_irreflexive _ _ H3).
-
-auto.
-Qed.
-
-Lemma Crel_strextarg_imp_strext :
- Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
-unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
- intros H H0 x1 x2 y1 y2 H1.
-elim (H x1 y1 y2 H1); auto.
-intro H2.
-elim (H0 x1 x2 y2 H2); auto.
-Qed.
-*)
-
-
-
-
-(* ---- e questo ??????? -----*)
-
-(*Definition of a [CProp] setoid relation
-The type of relations over a setoid. *)
-(*
-Record CCSetoid_relation : Type :=
- {Ccsr_rel :> S -> S -> CProp;
- Ccsr_strext : Crel_strext Ccsr_rel}.
-
-Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
-intro R.
-red in |- *; intros x y z H H0.
-elim (Ccsr_strext R x x y z H).
-
-auto.
-
-intro H1; elimtype False.
-elim H1; intro H2.
-
-exact (ap_irreflexive_unfolded _ _ H2).
-
-generalize H2.
-exact (eq_imp_not_ap _ _ _ H0).
-Qed.
-
-Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.
-intro R.
-red in |- *; intros x y z H H0.
-elim (Ccsr_strext R x z y y H).
-
-auto.
-
-intro H1; elimtype False.
-elim H1; intro H2.
-
-generalize H2.
-exact (eq_imp_not_ap _ _ _ H0).
-
-exact (ap_irreflexive_unfolded _ _ H2).
-Qed.
-
-Lemma ap_wdr : Crel_wdr (cs_ap (c:=S)).
-red in |- *; intros x y z H H0.
-generalize (eq_imp_not_ap _ _ _ H0); intro H1.
-elim (ap_cotransitive_unfolded _ _ _ H z); intro H2.
-
-assumption.
-
-elim H1.
-apply ap_symmetric_unfolded.
-assumption.
-Qed.
-
-Lemma ap_wdl : Crel_wdl (cs_ap (c:=S)).
-red in |- *; intros x y z H H0.
-generalize (ap_wdr y x z); intro H1.
-apply ap_symmetric_unfolded.
-apply H1.
-
-apply ap_symmetric_unfolded.
-assumption.
-
-assumption.
-Qed.
-
-Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
-Proof ap_wdr.
-
-Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.
-Proof ap_wdl.
-
-Lemma ap_strext : Crel_strext (cs_ap (c:=S)).
-red in |- *; intros x1 x2 y1 y2 H.
-case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
-
-auto.
-
-case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
-
-auto.
-
-right; right.
-apply ap_symmetric_unfolded.
-assumption.
-Qed.
-
-Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
- P x -> x [=] y -> P y.
-
-End CSetoid_relations_and_predicates.
-
-Declare Left Step ap_wdl_unfolded.
-Declare Right Step ap_wdr_unfolded.
-*)
-
-
-
-
-
-
-
-
-
-(*------------------------------------------------------------------------*)
-(* ------------------------- Functions between setoids ------------------ *)
-(*------------------------------------------------------------------------*)
-
-(* Such functions must preserve the setoid equality
-and be strongly extensional w.r.t. the apartness, i.e.
-if f(x,y) # f(x1,y1), then x # x1 or y # y1.
-For every arity this has to be defined separately. *)
-
-(* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2) *)
-
-(* First we consider unary functions. *)
-
-(*
-In the following two definitions,
-f is a function from (the carrier of) S1 to (the carrier of) S2 *)
-
-(* Nota: senza le parentesi di (S1 \to S2) non funziona, perche'? *)
-definition fun_wd : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
- \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
- x = y \to f x = f y.
-
-definition fun_strext : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
- \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
- (f x \neq f y) \to (x \neq y).
-
-lemma fun_strext_imp_wd : \forall S1,S2 : CSetoid. \forall f : S1 \to S2.
- fun_strext S1 S2 f \to fun_wd S1 S2 f.
-unfold fun_strext.
-unfold fun_wd.
-intros.
-apply not_ap_imp_eq.
-unfold.intro.
-apply (eq_imp_not_ap ? ? ? H1).
-apply H.assumption.
-qed.
-
-(* funzioni tra setoidi *)
-record CSetoid_fun (S1,S2 : CSetoid) : Type \def
- {csf_fun : S1 \to S2;
- csf_strext : (fun_strext S1 S2 csf_fun)}.
-
-lemma csf_wd : \forall S1,S2 : CSetoid. \forall f : CSetoid_fun S1 S2. fun_wd S1 S2 (csf_fun S1 S2 f).
-intros.
-apply fun_strext_imp_wd.
-apply csf_strext.
-qed.
-
-definition Const_CSetoid_fun : \forall S1,S2: CSetoid. S2 \to CSetoid_fun S1 S2.
-intros. apply (mk_CSetoid_fun S1 S2 (\lambda x:S1.c)).
-unfold.intros.
-elim (ap_irreflexive ? ? H).
-qed.
-
-
-(* ---- Binary functions ------*)
-(* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2 \to S3) *)
-
-definition bin_fun_wd : \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
- \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
- x1 = x2 \to y1 = y2 \to f x1 y1 = f x2 y2.
-
-(*
-Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
- f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.
-*)
-
-definition bin_fun_strext: \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
- \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
- f x1 y1 \neq f x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
-
-lemma bin_fun_strext_imp_wd : \forall S1,S2,S3: CSetoid.\forall f:S1 \to S2 \to S3.
-bin_fun_strext ? ? ? f \to bin_fun_wd ? ? ? f.
-intros.unfold in H.
-unfold.intros.
-apply not_ap_imp_eq.unfold.intro.
-elim (H x1 x2 y1 y2 H3).
-apply (eq_imp_not_ap ? ? ? H1 H4).
-apply (eq_imp_not_ap ? ? ? H2 H4).
-qed.
-
-
-
-record CSetoid_bin_fun (S1,S2,S3: CSetoid) : Type \def
- {csbf_fun :2> S1 \to S2 \to S3;
- csbf_strext : (bin_fun_strext S1 S2 S3 csbf_fun)}.
-
-lemma csbf_wd : \forall S1,S2,S3: CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3.
- bin_fun_wd S1 S2 S3 (csbf_fun S1 S2 S3 f).
-intros.
-apply bin_fun_strext_imp_wd.
-apply csbf_strext.
-qed.
-
-lemma csf_wd_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,x' : S1.
- x = x' \to (csf_fun S1 S2 f) x = (csf_fun S1 S2 f) x'.
-intros.
-apply (csf_wd S1 S2 f x x').
-assumption.
-qed.
-
-lemma csf_strext_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,y : S1.
-(csf_fun S1 S2 f) x \neq (csf_fun S1 S2 f) y \to x \neq y.
-intros.
-apply (csf_strext S1 S2 f x y).
-assumption.
-qed.
-
-lemma csbf_wd_unfolded : \forall S1,S2,S3 : CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3. \forall x,x':S1.
-\forall y,y' : S2. x = x' \to y = y' \to (csbf_fun S1 S2 S3 f) x y = (csbf_fun S1 S2 S3 f) x' y'.
-intros.
-apply (csbf_wd S1 S2 S3 f x x' y y'); assumption.
-qed.
-
-(* Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.*)
-
-(* The unary and binary (inner) operations on a csetoid
-An operation is a function with domain(s) and co-domain equal. *)
-
-(* Properties of binary operations *)
-
-definition commutes : \forall S: CSetoid. (S \to S \to S) \to Prop \def
- \lambda S: CSetoid. \lambda f : S \to S \to S.
- \forall x,y : S. f x y = f y x.
-
-definition CSassociative : \forall S: CSetoid. \forall f: S \to S \to S. Prop \def
-\lambda S: CSetoid. \lambda f : S \to S \to S.
-\forall x,y,z : S.
- f x (f y z) = f (f x y) z.
-
-definition un_op_wd : \forall S:CSetoid. (S \to S) \to Prop \def
-\lambda S: CSetoid. \lambda f: (S \to S). fun_wd S S f.
-
-
-definition un_op_strext: \forall S:CSetoid. (S \to S) \to Prop \def
-\lambda S:CSetoid. \lambda f: (S \to S). fun_strext S S f.
-
-
-definition CSetoid_un_op : CSetoid \to Type \def
-\lambda S:CSetoid. CSetoid_fun S S.
-
-definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext S S f \to CSetoid_fun S S
- \def
-\lambda S:CSetoid. \lambda f: S \to S. mk_CSetoid_fun S S f.
-
-lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
-unfold un_op_strext.
-unfold fun_strext.
-intros.
-simplify in H.
-exact H.
-qed.
-
-lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x).
-unfold un_op_wd.
-unfold fun_wd.
-intros.
-simplify.
-exact H.
-qed.
-
-definition id_un_op : \forall S:CSetoid. CSetoid_un_op S
- \def \lambda S: CSetoid. mk_CSetoid_un_op S (\lambda x : cs_crr S.x) (id_strext S).
-
-definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
-\def \lambda S.\lambda f.f.
-
-coercion cic:/matita/algebra/CoRN/Setoid/un_op_fun.con.
-
-definition cs_un_op_strext : \forall S:CSetoid. \forall f: CSetoid_fun S S. fun_strext S S (csf_fun S S f) \def
-\lambda S:CSetoid. \lambda f : CSetoid_fun S S. csf_strext S S f.
-
-lemma un_op_wd_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
-\forall x, y : S.
-x = y \to (csf_fun S S op) x = (csf_fun S S op) y.
-intros.
-apply (csf_wd S S ?).assumption.
-qed.
-
-lemma un_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
-\forall x, y : S.
- (csf_fun S S op) x \neq (csf_fun S S op) y \to x \neq y.
-exact cs_un_op_strext.
-qed.
-
-
-(* Well-defined binary operations on a setoid. *)
-
-definition bin_op_wd : \forall S:CSetoid. (S \to S \to S) \to Prop \def
-\lambda S:CSetoid. bin_fun_wd S S S.
-
-definition bin_op_strext : \forall S:CSetoid. (S \to S \to S) \to Prop \def
-\lambda S:CSetoid. bin_fun_strext S S S.
-
-definition CSetoid_bin_op : CSetoid \to Type \def
-\lambda S:CSetoid. CSetoid_bin_fun S S S.
-
-
-definition mk_CSetoid_bin_op : \forall S:CSetoid. \forall f: S \to S \to S.
-bin_fun_strext S S S f \to CSetoid_bin_fun S S S \def
- \lambda S:CSetoid. \lambda f: S \to S \to S.
- mk_CSetoid_bin_fun S S S f.
-
-(* da controllare che sia ben tipata
-definition cs_bin_op_wd : \forall S:CSetoid. ? \def
-\lambda S:CSetoid. csbf_wd S S S.
-*)
-definition cs_bin_op_wd : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_wd S S S (csbf_fun S S S f) \def
-\lambda S:CSetoid. csbf_wd S S S.
-
-definition cs_bin_op_strext : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_strext S S S (csbf_fun S S S f) \def
-\lambda S:CSetoid. csbf_strext S S S.
-
-
-
-(* Identity Coercion bin_op_bin_fun : CSetoid_bin_op >-> CSetoid_bin_fun. *)
-
-definition bin_op_bin_fun: \forall S:CSetoid. CSetoid_bin_op S \to CSetoid_bin_fun S S S
-\def \lambda S.\lambda f.f.
-
-coercion cic:/matita/algebra/CoRN/Setoid/bin_op_bin_fun.con.
-
-
-
-
-lemma bin_op_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
- x1 = x2 \to y1 = y2 \to (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
-exact cs_bin_op_wd.
-qed.
-
-lemma bin_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
- (csbf_fun S S S op) x1 y1 \neq (csbf_fun S S S op) x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
-exact cs_bin_op_strext.
-qed.
-
-lemma bin_op_is_wd_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
-intros. unfold. unfold.
-intros. apply bin_op_wd_unfolded [ assumption | apply eq_reflexive_unfolded ]
-qed.
-
-lemma bin_op_is_wd_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
-intros. unfold. unfold.
-intros. apply bin_op_wd_unfolded [ apply eq_reflexive_unfolded | assumption ]
-qed.
-
-
-lemma bin_op_is_strext_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
-intros. unfold un_op_strext. unfold fun_strext.
-intros.
-cut (x \neq y \lor c \neq c)
-[ elim Hcut
- [ assumption
- | generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
- ]
-| apply (bin_op_strext_unfolded S op x y c c). assumption.
-]
-qed.
-
-lemma bin_op_is_strext_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
-intros. unfold un_op_strext. unfold fun_strext.
-intros.
-cut (c \neq c \lor x \neq y)
-[ elim Hcut
- [ generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
- | assumption
- ]
-| apply (bin_op_strext_unfolded S op c c x y). assumption.
-]
-qed.
-
-definition bin_op2un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
-\forall c : cs_crr S. CSetoid_un_op S \def
- \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
- mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) c x))
- (bin_op_is_strext_un_op_rht S op c).
-
-definition bin_op2un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
-\forall c : cs_crr S. CSetoid_un_op S \def
- \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
- mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) x c))
- (bin_op_is_strext_un_op_lft S op c).
-
-(*
-Definition bin_op2un_op_rht (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
- Build_CSetoid_un_op (fun x : S => op c x) (bin_op_is_strext_un_op_rht op c).
-
-
-Definition bin_op2un_op_lft (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
- Build_CSetoid_un_op (fun x : S => op x c) (bin_op_is_strext_un_op_lft op c).
-*)
-
-
-(*
-Implicit Arguments commutes [S].
-Implicit Arguments associative [S].
-Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
-*)
-
-(*The binary outer operations on a csetoid*)
-
-
-(*
-Well-defined outer operations on a setoid.
-*)
-definition outer_op_well_def : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
-\lambda S1,S2:CSetoid. bin_fun_wd S1 S2 S2.
-
-definition outer_op_strext : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
-\lambda S1,S2:CSetoid. bin_fun_strext S1 S2 S2.
-
-definition CSetoid_outer_op : \forall S1,S2:CSetoid.Type \def
-\lambda S1,S2:CSetoid.
- CSetoid_bin_fun S1 S2 S2.
-
-definition mk_CSetoid_outer_op : \forall S1,S2:CSetoid.
-\forall f : S1 \to S2 \to S2.
-bin_fun_strext S1 S2 S2 f \to CSetoid_bin_fun S1 S2 S2 \def
-\lambda S1,S2:CSetoid.
-mk_CSetoid_bin_fun S1 S2 S2.
-
-definition csoo_wd : \forall S1,S2:CSetoid. \forall f : CSetoid_bin_fun S1 S2 S2.
-bin_fun_wd S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
-\lambda S1,S2:CSetoid.
-csbf_wd S1 S2 S2.
-
-definition csoo_strext : \forall S1,S2:CSetoid.
-\forall f : CSetoid_bin_fun S1 S2 S2.
-bin_fun_strext S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
-\lambda S1,S2:CSetoid.
-csbf_strext S1 S2 S2.
-
-
-definition outer_op_bin_fun: \forall S:CSetoid.
-CSetoid_outer_op S S \to CSetoid_bin_fun S S S
-\def \lambda S.\lambda f.f.
-
-coercion cic:/matita/algebra/CoRN/Setoid/outer_op_bin_fun.con.
-(* begin hide
-Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
-end hide *)
-
-lemma csoo_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_outer_op S S.
-\forall x1, x2, y1, y2 : S.
- x1 = x2 -> y1 = y2 -> (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
-intros.
-apply csoo_wd[assumption|assumption]
-qed.
-
-(*
-Hint Resolve csoo_wd_unfolded: algebra_c.
-*)
-
-
-
-(*---------------------------------------------------------------*)
-(*--------------------------- Subsetoids ------------------------*)
-(*---------------------------------------------------------------*)
-
-(* Let S be a setoid, and P a predicate on the carrier of S *)
-(* Variable P : S -> CProp *)
-
-record subcsetoid_crr (S: CSetoid) (P: S \to Prop) : Type \def
- {scs_elem :> S;
- scs_prf : P scs_elem}.
-
-definition restrict_relation : \forall S:CSetoid. \forall R : S \to S \to Prop.
- \forall P: S \to Prop. relation (subcsetoid_crr S P) \def
- \lambda S:CSetoid. \lambda R : S \to S \to Prop.
- \lambda P: S \to Prop. \lambda a,b: subcsetoid_crr S P.
- match a with
- [ (mk_subcsetoid_crr x H) \Rightarrow
- match b with
- [ (mk_subcsetoid_crr y H) \Rightarrow R x y ]
- ].
-(* CPROP
-definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
- fun a b : subcsetoid_crr =>
- match a, b with
- | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
- end.
-*)
-
-definition subcsetoid_eq : \forall S:CSetoid. \forall P: S \to Prop.
- relation (subcsetoid_crr S P)\def
- \lambda S:CSetoid.
- restrict_relation S (cs_eq S).
-
-definition subcsetoid_ap : \forall S:CSetoid. \forall P: S \to Prop.
- relation (subcsetoid_crr S P)\def
- \lambda S:CSetoid.
- restrict_relation S (cs_ap S).
-
-(* N.B. da spostare in relations.ma... *)
-definition equiv : \forall A: Type. \forall R: relation A. Prop \def
- \lambda A: Type. \lambda R: relation A.
- (reflexive A R) \land (transitive A R) \land (symmetric A R).
-
-remark subcsetoid_equiv : \forall S:CSetoid. \forall P: S \to Prop.
-equiv ? (subcsetoid_eq S P).
-intros. unfold equiv. split
-[split
- [unfold. intro. elim x. simplify. apply (eq_reflexive S)
- |unfold. intros 3. elim y 2.
- elim x 2. elim z 2. simplify.
- exact (eq_transitive ? c1 c c2)
- ]
-| unfold. intros 2. elim x 2. elim y 2. simplify. exact (eq_symmetric ? c c1).
-]
-qed.
-
-(*
-axiom subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
-is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
-*)
-
-lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
-is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
-intros.
-apply (mk_is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P))
-[ unfold. intros.unfold. elim x. exact (ap_irreflexive_unfolded S ? ?)
- [ assumption | simplify in H1. exact H1 ]
- (* irreflexive *)
-|unfold. intros 2. elim x. generalize in match H1. elim y.simplify in H3. simplify.
-exact (ap_symmetric ? ? ? H3)
-(* cotransitive *)
-|unfold.intros 2. elim x.generalize in match H1. elim y. elim z.simplify. simplify in H3.
-apply (ap_cotransitive ? ? ? H3)
-(* tight *)
-|unfold.intros.elim x. elim y.simplify.
-apply (ap_tight S ? ?)]
-qed.
-
-
-definition mk_SubCSetoid : \forall S:CSetoid. \forall P: S \to Prop. CSetoid \def
-\lambda S:CSetoid. \lambda P:S \to Prop.
-mk_CSetoid (subcsetoid_crr S P) (subcsetoid_eq S P) (subcsetoid_ap S P) (subcsetoid_is_CSetoid S P).
-
-(* Subsetoid unary operations
-%\begin{convention}%
-Let [f] be a unary setoid operation on [S].
-%\end{convention}%
-*)
-
-(* Section SubCSetoid_unary_operations.
-Variable f : CSetoid_un_op S.
-*)
-
-definition un_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
- CSetoid_un_op S \to Prop \def
- \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
- \forall x : cs_crr S. P x \to P ((csf_fun S S f) x).
-
-definition restr_un_op : \forall S:CSetoid. \forall P: S \to Prop.
- \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
- subcsetoid_crr S P \to subcsetoid_crr S P \def
- \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
- \lambda pr : un_op_pres_pred S P f.\lambda a: subcsetoid_crr S P.
- match a with
- [ (mk_subcsetoid_crr x p) \Rightarrow
- (mk_subcsetoid_crr ? ? ((csf_fun S S f) x) (pr x p))].
-
-(* TODO *)
-lemma restr_un_op_wd : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
-un_op_wd (mk_SubCSetoid S P) (restr_un_op S P f pr).
-intros.
-unfold.unfold.intros 2.elim x 2.elim y 2.
-simplify.
-intro.
-reduce in H2.
-apply (un_op_wd_unfolded ? f ? ? H2).
-qed.
-
-lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
-un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
-intros.unfold.unfold. intros 2.elim y 2. elim x 2.
-intros.reduce in H2.
-apply (cs_un_op_strext ? f ? ? H2).
-qed.
-
-definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
- \forall pr:un_op_pres_pred S P f.
- CSetoid_un_op (mk_SubCSetoid S P) \def
- \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
- \lambda pr:un_op_pres_pred S P f.
- mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr).
-
-
-(* Subsetoid binary operations
-Let [f] be a binary setoid operation on [S].
-*)
-
-(* Section SubCSetoid_binary_operations.
-Variable f : CSetoid_bin_op S.
-*)
-
-definition bin_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
-(CSetoid_bin_op S) \to Prop \def
- \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_bin_op S.
- \forall x,y : S. P x \to P y \to P ( (csbf_fun S S S f) x y).
-
-(*
-Assume [bin_op_pres_pred].
-*)
-
-(* Variable pr : bin_op_pres_pred. *)
-
-definition restr_bin_op : \forall S:CSetoid. \forall P:S \to Prop.
- \forall f: CSetoid_bin_op S.\forall op : (bin_op_pres_pred S P f).
- \forall a, b : subcsetoid_crr S P. subcsetoid_crr S P \def
- \lambda S:CSetoid. \lambda P:S \to Prop.
- \lambda f: CSetoid_bin_op S. \lambda pr : (bin_op_pres_pred S P f).
- \lambda a, b : subcsetoid_crr S P.
- match a with
- [ (mk_subcsetoid_crr x p) \Rightarrow
- match b with
- [ (mk_subcsetoid_crr y q) \Rightarrow
- (mk_subcsetoid_crr ? ? ((csbf_fun S S S f) x y) (pr x y p q))]
- ].
-
-
-(* TODO *)
-lemma restr_bin_op_well_def : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
-bin_op_wd (mk_SubCSetoid S P) (restr_bin_op S P f pr).
-intros.
-unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
-simplify.
-intros.
-reduce in H4.
-reduce in H5.
-apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
-qed.
-
-lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
-bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
-intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
-simplify.intros.
-reduce in H4.
-apply (cs_bin_op_strext ? f ? ? ? ? H4).
-qed.
-
-definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
- \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
- CSetoid_bin_op (mk_SubCSetoid S P) \def
- \lambda S:CSetoid. \lambda P: S \to Prop.
- \lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
- mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).
-
-lemma restr_f_assoc : \forall S:CSetoid. \forall P: S \to Prop.
- \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
- CSassociative S (csbf_fun S S S f)
- \to CSassociative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)).
-intros 4.
-intro.
-unfold.
-intros 3.
-elim z 2.elim y 2. elim x 2.
-whd.
-apply H.
-qed.
-
-definition caseZ_diff: \forall A:Type.Z \to (nat \to nat \to A) \to A \def
-\lambda A:Type.\lambda z:Z.\lambda f:nat \to nat \to A.
- match z with
- [OZ \Rightarrow f O O
- |(pos n) \Rightarrow f (S n) O
- |(neg n) \Rightarrow f O (S n)].
-
-(* Zminus.ma *)
-theorem Zminus_S_S : \forall n,m:nat.
-Z_of_nat (S n) - S m = Z_of_nat n - m.
-intros.
-elim n.elim m.simplify. reflexivity.reflexivity.
-elim m.simplify.reflexivity.reflexivity.
-qed.
-
-
-
-lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
- (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
- \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
-intros.
-(* perche' apply nat_elim2 non funziona?? *)
-apply (nat_elim2 (\lambda m,n.caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = f m n)).
-intro.simplify.
-apply (nat_case n1).simplify.
-apply eq_reflexive.
-intro.simplify.apply eq_reflexive.
-intro.simplify.apply eq_reflexive.
-intros 2.
-rewrite > (Zminus_S_S n1 m1).
-intros.
-cut (f n1 m1 = f (S n1) (S m1)).
-apply eq_symmetric_unfolded.
-apply eq_transitive.
-apply f. apply n1. apply m1.
-apply eq_symmetric_unfolded.assumption.
-apply eq_symmetric_unfolded.assumption.
-apply H.
-auto new timeout=100.
-qed.
-
-(*
-Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
-*)
-
-
-definition nat_less_n_fun : \forall S:CSetoid. \forall n:nat. ? \def
- \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i:nat. i < n \to S.
- \forall i,j : nat. eq nat i j \to (\forall H : i < n.
- \forall H' : j < n . (f i H) = (f j H')).
-
-definition nat_less_n_fun' : \forall S:CSetoid. \forall n:nat. ? \def
- \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i: nat. i <= n \to S.
- \forall i,j : nat. eq nat i j \to \forall H : i <= n.
- \forall H' : j <= n. f i H = f j H'.
projects / helm.git / commitdiff