matita/library/algebra/CoRN/SetoidFun.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* $Id: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *)
  16
  17 set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun".
  18 include "algebra/CoRN/Setoids.ma".
  19
  20
  21 definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
  22 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
  23  \exists a:A. (csf_fun A B f) a \neq (csf_fun A B g) a.
  24 (* Definition ap_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
  25   {a : A | f a[#]g a}. *)
  26
  27 definition eq_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
  28 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
  29  \forall a:A. (csf_fun A B f) a = (csf_fun A B g) a.
  30 (* Definition eq_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
  31   forall a : A, f a[=]g a. *)
  32
  33 lemma irrefl_apfun : \forall A,B : CSetoid.
  34  irreflexive (CSetoid_fun A B) (ap_fun A B).
  35 intros.
  36 unfold irreflexive. intro f.
  37 unfold ap_fun.
  38 unfold.
  39 intro.
  40 elim H.
  41 cut (csf_fun A B f a = csf_fun A B f a)
  42 [
  43  apply eq_imp_not_ap.
  44  apply A.
  45  assumption.
  46  assumption.
  47  auto.
  48  auto
  49 |
  50  apply eq_reflexive_unfolded
  51 ]
  52 qed.
  53
  54 (*
  55 Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
  56 intros A B.
  57 unfold irreflexive in |- *.
  58 intros f.
  59 unfold ap_fun in |- *.
  60 red in |- *.
  61 intro H.
  62 elim H.
  63 intros a H0.
  64 set (H1 := ap_irreflexive_unfolded B (f a)) in *.
  65 intuition.
  66 Qed.
  67 *)
  68
  69
  70 (*
  71 lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B).
  72 intros (A B).
  73 unfold.
  74 unfold ap_fun.
  75 intros (f g H h).
  76 decompose.
  77 apply ap_cotransitive.
  78 apply (ap_imp_neq B (csf_fun A B x a) (csf_fun A B y a) H1).
  79 (* letin foo \def (\exist a:A.csf_fun A B x a\neq csf_fun A B z a). *)
  80
  81
  82 apply (ap_cotransitive B ? ? H1 ?).
  83
  84 split.
  85 left.
  86 elim H.
  87 clear H.
  88 intros a H.
  89 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
  90 elim H1.
  91 clear H1.
  92 intros H1.
  93 left.
  94 exists a.
  95 exact H1.
  96
  97 clear H1.
  98 intro H1.
  99 right.
 100 exists a.
 101 exact H1.
 102 Qed.
 103 *)
 104
 105 (*
 106 Lemma cotrans_apfun : forall A B : CSetoid, cotransitive (ap_fun A B).
 107 intros A B.
 108 unfold cotransitive in |- *.
 109 unfold ap_fun in |- *.
 110 intros f g H h.
 111 elim H.
 112 clear H.
 113 intros a H.
 114 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
 115 elim H1.
 116 clear H1.
 117 intros H1.
 118 left.
 119 exists a.
 120 exact H1.
 121
 122 clear H1.
 123 intro H1.
 124 right.
 125 exists a.
 126 exact H1.
 127 Qed.
 128 *)
 129
 130 lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
 131 unfold tight_apart.
 132 intros (A B f g).
 133 unfold ap_fun.
 134 unfold eq_fun.
 135 split
 136 [ intros.
 137   apply not_ap_imp_eq.unfold.intro.auto.
 138  |intros. unfold.intro.elim H1.
 139   apply (ap_imp_neq B ? ? H2). auto.
 140 ]
 141 qed.
 142