proposition: Lemma un_op_wd_unfolded : forall (op : CSetoid_un_op) (x y : S), x [=] y -> op x [=] op y.
proof: Proof. Proof csf_wd S S. Lemma un_op_strext_unfolded : forall (op : CSetoid_un_op) (x y : S), op x [#] op y -> x [#] y. Proof cs_un_op_strext. Lemma bin_op_wd_unfolded : forall (op : CSetoid_bin_op) (x1 x2 y1 y2 : S), x1 [=] x2 -> y1 [=] y2 -> op x1 y1 [=] op x2 y2. Proof cs_bin_op_wd. Lemma bin_op_strext_unfolded : forall (op : CSetoid_bin_op) (x1 x2 y1 y2 : S), op x1 y1 [#] op x2 y2 -> x1 [#] x2 or y1 [#] y2. Proof cs_bin_op_strext. End csetoid_inner_ops. Arguments commutes [S]. Arguments associative [S]. #[global] Hint Resolve ap_wdr_unfolded ap_wdl_unfolded bin_op_wd_unfolded un_op_wd_unfolded : algebra_c. Section csetoid_outer_ops. Variables S1 S2 : CSetoid. Definition outer_op_well_def := bin_fun_wd S1 S2 S2. Definition outer_op_strext := bin_fun_strext S1 S2 S2. Definition CSetoid_outer_op : Type := CSetoid_bin_fun S1 S2 S2. Definition Build_CSetoid_outer_op := Build_CSetoid_bin_fun S1 S2 S2. Definition csoo_wd := csbf_wd S1 S2 S2. Definition csoo_strext := csbf_strext S1 S2 S2. Lemma csoo_wd_unfolded : forall (op : CSetoid_outer_op) x1 x2 y1 y2, x1 [=] x2 -> y1 [=] y2 -> op x1 y1 [=] op x2 y2. Proof csoo_wd. Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun. End csetoid_outer_ops. #[global] Hint Resolve csoo_wd_unfolded: algebra_c. Section SubCSetoids. Variable S : CSetoid. Variable P : S -> CProp. Record subcsetoid_crr : Type := {scs_elem :> S; scs_prf : P scs_elem}. Definition restrict_relation (R : Relation S) : Relation subcsetoid_crr := fun a b : subcsetoid_crr => match a, b with | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y end. 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 : Relation subcsetoid_crr := restrict_relation (cs_eq (r:=S)). Definition subcsetoid_ap : Crelation subcsetoid_crr := Crestrict_relation (cs_ap (c:=S)). Remark subcsetoid_equiv : Tequiv _ subcsetoid_eq. Proof. split. intros a; case a. intros x s. apply (eq_reflexive S). split. intros a b c; case a. intros x s; case b. intros y t; case c. intros z u. apply eq_transitive. intros a b; case a. intros x s; case b. intros y t. apply eq_symmetric. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid