Require Export jset.
Require Export String.


(* $Id: jfunc.v,v 1.24 2009/07/20 06:33:18 grimm Exp $ *)


Set Implicit Arguments.
Unset Strict Implicit.

Module Function.

Definition is_graph r := forall y, inc y r -> is_pair y.
Definition domain f  := fun_image f P.
Definition range f := fun_image f Q.

Definition fgraph f :=
  is_graph f & (forall x y, inc x f -> inc y f -> P x = P y -> x = y).

Hint Rewrite fun_image_rw : aw. 


Lemma nonempty_domain: forall g,
  nonempty g -> nonempty (domain g).
Proof. ir. uf domain. nin H. exists (P y). app inc_fun_image.
Qed.

Lemma domain_pr: forall r x, 
  is_graph r ->
  inc x (domain r) = (exists y, inc (J x y) r).
Proof. ir. uf domain. aw. app iff_eq. ir. 
  induction H0. ee. assert (is_pair x0). app H.  exists (Q x0). wr H1.
  rw pair_recov. am. am. ir. nin H0. exists (J x x0). ee. am. aw.  
Qed.

Lemma range_pr: forall r y, 
  is_graph r -> inc y (range r) = (exists x, inc (J x y) r).
Proof. ir. uf range.  aw. app iff_eq. ir. 
  induction H0. ee. assert (is_pair x). app H.  exists (P x). wr H1.
  rw pair_recov. am. am. ir. nin H0. exists (J x y). ee. am. aw.
Qed.

Hint Rewrite range_pr domain_pr : aw.

Lemma inc_pr1_domain : forall f x, 
  fgraph f -> inc x f -> inc (P x) (domain f). 
Proof. ir. uf domain. app inc_fun_image. 
Qed. 

Lemma inc_pr2_range : forall f x, 
  fgraph f -> inc x f -> inc (Q x) (range f). 
Proof. ir. uf range. app inc_fun_image. 
Qed. 

Lemma fdefined_lem : forall f x, 
  fgraph f -> inc x (domain f) -> inc (J x (V x f)) f.
Proof.  ir. awi H0. pose (choose_pr H0). am. red in H; ee. am.
Qed. 

Lemma in_graph_V : forall f x, 
  fgraph f -> inc x f -> x = J (P x) (V (P x) f).
Proof. uf fgraph. ir. ee. set (z := P x). 
  assert (exists y, inc (J z y) f). exists (Q x). 
  uf z. rw pair_recov. am. app H. pose (choose_pr H2). 
  assert (inc (J z (V z f)) f). am. app H1. aw.
Qed.

Lemma frange_inc_rw : forall f y,
  fgraph f -> inc y (range f) = (exists x, inc x (domain f) & y = V x f).
Proof. ir. assert (is_graph f). red in H; ee; am. ap iff_eq; ir. 
  awi H1. nin H1. exists x. ee. aw. exists y. am. 
  cp (in_graph_V H H1).  awi H2. app (pr2_injective H2). am. 
  nin H1. ee. aw. cp (fdefined_lem H H1). exists x. rww H2. 
Qed.  

Lemma pr2_V : forall f x, 
  fgraph f -> inc x f -> Q x = V (P x) f.
Proof. ir. pose (in_graph_V H H0). set (a := pr1 x). rw e. aw.  
Qed.

Lemma inc_V_range:  forall f x,
  fgraph f -> inc x (domain f) -> inc (V x f) (range f).
Proof. ir. rw frange_inc_rw. exists x. ee. am. tv. am.
Qed.

(** Case of a subgraph *)

Lemma sub_axioms : forall f g, fgraph g -> sub f g -> fgraph f.
Proof. ir. red. split. red.  ir. red in H. ee. red in H. app H. app H0.
  ir. red in H. ee. app H4. app H0. app H0.
Qed.

Lemma sub_domain : forall f g, sub f g -> sub (domain f) (domain g).
Proof. ir. unfold domain. red. ir. awi H0. aw.
  nin H0. nin H0. exists x0. split. ap H. am. am.
Qed.

Lemma sub_range : forall f g, sub f g -> sub (range f) (range g).
Proof. ir. uf range. red. ir. awi H0. aw.
  nin H0. nin H0. exists x0. split. ap H. am. am.
Qed.

Lemma sub_ev: forall f g x,
  fgraph g -> sub f g -> inc x (domain f) -> V x f = V x g.
Proof. ir. cp (sub_axioms H H0).
  cp (sub_domain H0). assert (inc x (domain g)). app H3. 
  cp (fdefined_lem H2 H1). cp (H0 _ H5). cp (in_graph_V H H6).
  awi H7. app (pr2_injective H7). 
Qed.
  
Lemma function_sub : forall f g,
  fgraph f ->
  fgraph g ->
  sub  (domain f) (domain g) ->
  (forall x, inc x (domain f) -> V x f = V x g) -> sub f g.
Proof. ir. uf sub. ir. cp (in_graph_V H H3). 
  assert (inc (P x) (domain f)). aw. exists (Q x). 
  rw pair_recov. am. rw H4.  fprops. red in H; ee; am.
  cp (H2 _ H5). cp (H1 _ H5). awi H7. nin H7.
  cp (in_graph_V H0 H7). awi H8. rw H4. rw H6. wr H8. am. red in H0; ee; am.
Qed.

Lemma function_extensionality: forall f g,
  fgraph f -> fgraph g -> domain f = domain g ->
  (forall x, inc x (domain f) -> V x f = V x g) -> f = g.
Proof. ir. app extensionality. app function_sub. rw H1; fprops.
  app function_sub. rw H1; fprops. ir. sy. app H2. rww H1.
Qed.

Definition inverse_image (a f : Bset) :=
  Zo (domain f) (fun x  => inc (V x f) a). 

Lemma inverse_image_sub : 
  forall a f, sub (inverse_image a f) (domain f).
Proof. uf inverse_image. ir. apply Z_sub. 
Qed.

Lemma inverse_image_inc :   forall a f x,
    inc x (domain f) -> inc (V x f) a -> inc x (inverse_image a f). 
Proof. ir. uf inverse_image. Ztac. Qed. 

Lemma inverse_image_pr :
  forall a f x, inc x (inverse_image a f) -> inc (V x f) a.
Proof. ir. ufi inverse_image H. Ztac.  am.
Qed. 

Definition fcreate (x : Bset) (p : EE) :=
  fun_image x (fun y => pair y (p y)).

Lemma create_axioms : forall p x, fgraph (fcreate x p).
Proof. ir. uf fgraph. split; intros. red. ir. ufi fcreate H. awi H.
  nin H. nin H. wr H0. fprops.
  ufi fcreate H. awi H. ufi fcreate H0. awi H0.
  nin H. nin H0. ee. wri H3 H1; wri H2 H1.  awi H1. wr H2; wr H3; wrr H1.
Qed. 

Lemma create_domain : forall x p, domain (fcreate x p) = x.
Proof. ir. uf domain. set_extens. awi H. nin H; ee.
  ufi fcreate H; awi H; nin H; ee. wr H0; wr H1. aw.
  aw. exists (J x0 (p x0)). split. uf fcreate. aw. exists x0; split; auto. aw.
Qed.

Hint Rewrite create_domain : aw. 

Lemma create_V_apply :   forall x p y z,
    inc y x -> p y = z -> V y (fcreate x p) = z.
Proof. ir. set (S:=(fcreate x p)). 
  assert (inc (J y (V y S)) S). app V_inc. 
  exists (p y). uf S. uf fcreate. aw. exists y; split; auto. 
  assert (fgraph S). uf S. ap create_axioms. 
  ufi fgraph H2. ee. assert (J y (V y (fcreate x p)) = pair y z). fold S.
  assert (inc (J y (p y)) S). unfold S. uf fcreate. aw. exists y; split; auto.
  ap H3. app V_inc. exists (p y).  tv. wr H0. am. aw.
  uf S. transitivity (Q (J y z)). wr H4. sy. aw. aw. 
Qed.

Lemma create_V_rewrite : forall x p y, inc y x -> V y (fcreate x p) = p y. 
Proof. ir. app create_V_apply. Qed. 

Hint Rewrite create_V_rewrite : aw. 

Lemma create_range : forall p x, 
  range (fcreate x p) = fun_image x p.
Proof. ir. uf range. set_extens. awi H. nin H; ee. ufi fcreate H. 
  awi H; nin H; ee. aw. exists x2. split.  am. wr H0. wr H1. aw.
  awi H. nin H; ee. aw. exists (J x1 x0). split. uf fcreate. aw. 
  exists x1; split; auto. rww H0. aw. 
Qed.

Lemma create_recovers :   forall f, 
  fgraph f -> fcreate (domain f) (fun x => V x f) = f.
Proof. ir. app function_extensionality. ap create_axioms. 
  ir. aw. aw. ir. app create_V_apply. 
Qed. 

Lemma function_extensionality1 : forall  a b f g,
    a = b ->  (forall x, inc x a -> f x = g x) -> 
    fcreate a f = fcreate b g.
Proof. ir.
  assert (fgraph (fcreate a f)). apply create_axioms.
  assert (fgraph (fcreate b g)). apply create_axioms.
  app function_extensionality. aw. aw. ir. aw.  app H0. wrr H. 
Qed.

Lemma create_create : forall  a f,
  fcreate a (fun x => V x (fcreate a f)) = fcreate a f.
Proof. ir. app function_extensionality1. ir. aw. 
Qed.

Lemma inc_create_range: forall sf f a,
  inc a (range (fcreate sf f))  = exists b, inc b sf & f b = a.
Proof. ir. app iff_eq. ir. rwi create_range H. awi H. am.
  ir. rw create_range. aw. 
Qed.

Lemma inc_create_domain: forall sf f a,
  inc a (domain (fcreate sf f))  = inc a sf.
Proof. ir. aw. 
Qed.

Lemma create_V_out : forall x f y,
  ~inc y x -> V y (fcreate x f) = emptyset.
Proof. ir. set (V_or y (fcreate x f)). nin o.
  assert (fgraph (fcreate x f)). ap create_axioms. 
  cp (inc_pr1_domain H1 H0). awi H2. elim H. am. am. ee; am.
Qed. 

Definition fcomposable (f g : Bset) :=
  fgraph f & fgraph g & sub (range g) (domain f). 

Definition fcompose (f g : Bset) :=
  fcreate (inverse_image (domain f) g) (fun y => V (V y g) f).

Definition gcompose g f := fcreate(domain f)  (fun y => V (V y f) g).

Lemma fcompose_axioms : forall f g, fgraph (fcompose f g).
Proof. ir. uf fcompose. ap create_axioms. Qed. 

Lemma fcompose_domain :
  forall f g, domain (fcompose f g) = inverse_image (domain f) g.
Proof. ir. uf fcompose.  aw. Qed.

Lemma fcomposable_domain :
  forall f g, fcomposable f g -> domain (fcompose f g) = domain g. 
Proof. ir. uf fcompose. aw. ap extensionality. 
  ap inverse_image_sub. uf sub; ir. app inverse_image_inc. 
  red in H. ee. app H2. rw frange_inc_rw. exists x. split;auto. am.
Qed. 

Lemma fcompose_ev :  forall x f g,
  inc x (domain (fcompose f g)) -> V x (fcompose f g) = V (V x g) f.
Proof. uf fcompose. ir. rwi create_domain H. app create_V_apply.  
Qed. 

Lemma alternate_compose: forall g f,
  fcomposable g f -> gcompose g f = fcompose g f.
Proof. ir. uf gcompose. app function_extensionality. app create_axioms.
  app fcompose_axioms. aw. rw fcomposable_domain. tv. am. aw. ir.
  rw create_V_rewrite. sy. rw fcompose_ev. tv. rw fcomposable_domain. tv.  
  am. am.
Qed.

Definition identity (x : Bset) := fcreate x (fun y => y).

Lemma identity_axioms : forall x, fgraph (identity x). 
Proof. ir. uf identity. ap create_axioms. 
Qed. 

Lemma identity_domain : forall x, domain (identity x) = x.
Proof. ir. uf identity. aw.  
Qed. 

Lemma identity_ev : forall x a, inc x a -> V x (identity a) = x.
Proof. ir. uf identity. app create_V_apply. Qed.

Definition restr f x :=
  Zo f (fun y=> inc (P y) x).

Lemma restr_inc_rw : forall f x y,
  inc y (restr f x) = (inc y f & inc (P y) x).
Proof. ir. uf restr. ap iff_eq; ir. apply (Z_all H). ee. app Z_inc. Qed.

Lemma restr_sub : forall f x, sub (restr f x) f.
Proof.  ir. uf sub. ir. rwi restr_inc_rw H. intuition.  
Qed.

Lemma restr_axioms : forall f x,
  fgraph f -> fgraph (restr f x).
Proof. ir. cp (restr_sub (f:=f) (x:=x)). app (sub_axioms H H0).
Qed.

Lemma restr_domain : forall f x,
  fgraph f -> 
    domain (restr f x) = intersection2 (domain f) x.
Proof. ir. set_extens. ufi domain H0.  awi H0. nin H0; ee.
  ufi restr H0. Ztac. ap intersection2_inc. uf domain. aw.
  exists x1. intuition. wrr H1.  
  cp (intersection2_first H0). cp (intersection2_second H0). 
  uf domain. aw. ufi domain H1. awi H1. nin H1.  nin H1. exists x1. split.
  uf restr. Ztac. rww H3. am. 
Qed.

Lemma function_sub_eq : forall r s, 
  fgraph r -> fgraph s -> sub r s ->
    sub (domain s) (domain r) -> r = s.
Proof. ir. app extensionality. uf sub. ir.
  set (u:= in_graph_V H0 H3). assert ( x = J (P x) (V (P x) s)). am.
  clear u. set (u:= inc_pr1_domain H0 H3).
  assert (inc (P x) (domain s)). am. clear u.
  assert (inc (P x) (domain r)). app H2. 
  assert (inc (J (P x) (V (P x) r)) r). app fdefined_lem.  
  assert (inc (J (P x) (V (P x) r)) s). app H1.
  rewrite H4 in H3. red in H0. ee.
  assert (J (P x) (V (P x) r) = J (P x) (V (P x) s)).
  app H9. aw. rwi H10 H7; wri H4 H7. am.
Qed. 

Lemma restr_to_domain : forall f g, 
  fgraph f -> fgraph g -> sub f g ->
    restr g (domain f) = f.
Proof. ir. sy. app function_sub_eq. app restr_axioms. 
  unfold sub. ir. uf restr; app Z_inc. app H1. app inc_pr1_domain.
  rww restr_domain. uf sub;ir. pose (intersection2_second H2). am.
Qed. 

Lemma restr_ev : forall f u x,
  fgraph f -> sub u (domain f) -> inc x u ->
    V x (restr f u) = V x f.
Proof. ir. assert (inc (pair x (V x f)) f).  app fdefined_lem. app H0.  
  assert (inc (pair x (V x f)) (restr f u)). 
  uf restr; Ztac.  rw pr1_pair. am.
  assert (fgraph (restr f u)). app restr_axioms. cp (pr2_V H4 H3). 
  awi H5. sy. am.
Qed. 

Lemma function_glueing : forall z,
  (forall f, inc f z -> fgraph f) -> 
  (forall f g x, inc f z -> inc g z -> inc x (domain f) -> inc x (domain g)
    -> (V x f) = (V x g)) -> 
  fgraph (union z).
Proof. ir. red. split. red. ir. induction (union_exists H1). ee.
  cp (H _ H3). red in H4. ee. app H4.
  ir. induction (union_exists H1).  induction (union_exists H2). ee.
  pose (H8:=H _ H6). pose  (H9:=H _ H7).
  pose (in_graph_V H9 H4). pose (in_graph_V H8 H5). rw e; rw e0; rw H3. 
  assert (V (pr1 y) x0 = V (pr1 y) x1). app H0. 
  wr H3. red. app inc_pr1_domain.  red. app inc_pr1_domain. rww H10. 
Qed. 

Lemma function_sub_V : forall f g x,
  fgraph g -> inc x (domain f) -> sub f g ->  V x f = V x g.
Proof. ir. cp (sub_axioms H H1). red in H0.
  cp (fdefined_lem H2 H0). cp (H1 _ H3). set (in_graph_V H H4). 
  rewrite pr1_pair in e. app (pr2_injective e).
Qed. 

Definition is_restriction (f g :Bset) :=
  fgraph g &  exists x, f = restr g x.

Lemma is_restriction_pr: forall f g,
  is_restriction f g =
  (fgraph f & fgraph g & sub f g).
Proof. ir. app iff_eq. ir. 
  nin H. nin H0.  ee. rw H0. app restr_axioms. am. rw H0. red. ir.
  rwi restr_inc_rw H1. ee. am. 
  ir. ee. red. ee. am. exists (domain f).
  assert (fgraph (restr g (domain f))). app restr_axioms.
  cp (sub_domain H1).
  assert (domain (restr g (domain f)) = domain f). rw restr_domain.
  set_extens. app (intersection2_second H4). app intersection2_inc. app H3. am.
  app function_extensionality. ir. sy; am. 
  ir. rw restr_ev. app sub_ev. am. am. am.
Qed.

Lemma domain_union : forall z, domain (union z) =
  union (fun_image z domain).
Proof. ir. set_extens. ufi domain H. awi H. nin H. ee. 
  induction (union_exists H). ee. apply union_inc with (domain x1). 
  uf domain.  aw. exists x0; split; am. 
  aw. exists x1; split; auto.
  induction (union_exists H). induction H0.  awi H1. 
  induction H1; ee. uf domain. aw. ufi domain H2. 
  wri H2 H0. awi H0. induction H0. 
  exists x2.  ee.  apply union_inc with x1.  am.  am. am. 
Qed.  

Lemma domain_tack_on : forall f x y,
  domain (tack_on f (pair x y)) = tack_on (domain f) x.
Proof. ir. uf domain. set_extens. awi H. nin H; ee.
  rwi tack_on_inc H. rw tack_on_inc; aw. nin H. left. exists x1. split; am. 
  right. wr H0; rw H. aw.
  aw. rwi tack_on_inc H; nin H. awi H. nin H;ee.
  exists x1. split. rw tack_on_inc. left; am. am.
  exists (pair x y).  split. rw tack_on_inc; right; tv. aw. sy; am. 
Qed. 

Lemma range_union : forall z, range (union z) =
  union (fun_image z range).
Proof. ir.  set_extens.
  ufi range H. awi H. nin H. nin H. induction (union_exists H). nin H1.
  apply union_inc with (range x1). uf range. aw.
  exists x0; split; am. aw.  exists x1. split. am. tv.
  induction (union_exists H). ee. awi H1. nin H1. nin H1.
  wri H2 H0. ufi range H0. awi H0. nin H0. ee. uf range. aw. exists x2. split.
  apply union_inc with x1. am. am. am.
Qed.  

Lemma range_tack_on : forall f x y,
  range (tack_on f (pair x y)) = tack_on (range f) y.
Proof. uf range. ir. set_extens. awi H; nin H. ee.
  rw tack_on_inc. rwi tack_on_inc H; nin H.
  left; aw; exists x1; ee; am. right; wr H0; rw H;rw pr2_pair; tv. 
  rwi tack_on_inc H; nin H. awi H. nin H. nin H. 
  aw. exists x1. split. rw tack_on_inc. left; am. am.
  aw. exists (pair x y). rw tack_on_inc. split. right; trivial.
  rewrite pr2_pair. auto. 
Qed. 

Lemma function_tack_on_axioms : forall f x y,
  fgraph f -> ~inc x (domain f) ->
  fgraph (tack_on f (pair x y)).
Proof. ir. uf fgraph. assert (HH:=H). ufi fgraph H. ee.
  red. ir. rwi tack_on_inc H2. nin H2. app H. rw H2. app pair_is_pair.
  ir. rwi tack_on_inc H2; rwi tack_on_inc H3.
  nin H2. nin H3. app H1. 
  rwi H3 H4. rwi pr1_pair H4. assert (inc (P x0)  (domain f)).
  apply (inc_pr1_domain HH H2). rewrite H4 in H5. elim (H0 H5). 
  induction H3. assert (inc (P y0) (domain f)). apply (inc_pr1_domain HH H3).
  wri H4 H5. rwi H2 H5. rwi  pr1_pair H5. elim (H0 H5). rw H2 ; sy; am. 
Qed. 


(**** now we create a function given a set x and a map f : x->E ***)

Definition tcreate (x:Bset) (f:x->Bset) :=
  fcreate x (fun y => (Yy (fun (hyp : inc y x) => f (Bo hyp)) emptyset)).

Lemma tcreate_value_type : forall x (f:x->Bset) y,
  V (Ro y) (tcreate f) = f y.
Proof. ir. assert (inc (Ro y) x). app R_inc. uf tcreate. rw create_V_rewrite.  
  apply Yy_if with H. rewrite B_back. tv. am.
Qed.

Lemma tcreate_value_inc : forall x (f:x->Bset) y (hyp : inc y x),
  V y (tcreate f) = f (Bo hyp).
Proof. ir. assert (y = Ro (Bo hyp)). rw B_eq. tv.
  transitivity (V (Ro (Bo hyp)) (tcreate f)). wr H; tv. ap tcreate_value_type. 
Qed.

Lemma domain_tcreate : forall x (f:x->Bset), domain (tcreate f) = x.
Proof. ir. uf tcreate. rw create_domain. tv. 
Qed.

End Function.
Export Function.

Notation L := Function.fcreate.


Module Function_Set.

Definition in_function_set (a : Bset) (f : EE) (u : Bset) :=
  fgraph u
  & domain u = a
  & (forall y, inc y a -> inc (V y u) (f y)).

Lemma in_fs_sub_record : forall a f u,
 in_function_set a f u -> sub u (record a f).
Proof. uf in_function_set. ir. destruct H as [H1 [H2 H3]]. red. ir.
  pose (pr2_V H1 H). cp H1. red in H0. ee.
  assert (inc (P x) a). wr H2. app inc_pr1_domain. assert (J (P x) (Q x) =x).
  app pair_recov. app H0. wr H6. app record_pair_inc. rw e. app H3.
Qed.

Lemma in_fs_eq_L : forall a f u,
    in_function_set a f u -> u = fcreate a (fun y => V y u).
Proof. unfold in_function_set. intros. destruct H as [H1 [H2 H3]].
  symmetry. wr H2. app create_recovers. 
Qed.

Lemma in_fs_for_L : forall a f v,
 (forall y, inc y a -> inc (v y) (f y)) ->
 in_function_set a f (fcreate a v).
Proof.  ir. red. ee. apply create_axioms. apply create_domain. 
  ir. rww create_V_rewrite.  app H. 
Qed.

Lemma in_fs_bounded :  forall  a f, Bounded.axioms (in_function_set a f).
Proof. intros. apply Bounded.criterion.
  exists (powerset (record a f)). intros. 
  apply powerset_inc. apply in_fs_sub_record; auto.
Qed.

Definition function_set (a : Bset) (f : EE) :=
  Bounded.create (in_function_set a f).

Lemma function_set_iff :  forall  a f u,
 inc u (function_set a f) <-> in_function_set a f u.
Proof. ir. uf function_set. unfold iff;split;intros. 
  apply Bounded.lem1. apply in_fs_bounded. am.
  apply Bounded.lem2. apply in_fs_bounded. am.
Qed.

Lemma function_set_sub_powerset_record :  forall  a f,
  sub (function_set a f) (powerset (record a f)).
Proof. unfold sub;  intros. pose (function_set_iff a f x).
  unfold iff in (type of i). induction i. pose (H0 H).
  apply powerset_inc. apply in_fs_sub_record. assumption.
Qed.

Lemma function_set_pr :   forall a f u,
    inc u (function_set a f) ->
    (in_function_set a f u 
      & fgraph u
      & domain u = a
      & (forall y , inc y a -> inc (V y u) (f y))).
Proof. ir. assert (in_function_set a f u). 
  cp (function_set_iff a f u). unfold iff in H0. nin H0. app H0.
  ufi in_function_set H0; uf in_function_set. intuition.
Qed.

Lemma function_set_inc : forall a f u,
    fgraph u ->
    domain u = a ->
    (forall y, inc y a -> inc (V y u) (f y)) -> inc u (function_set a f).
Proof. intros. cp (function_set_iff a f u). unfold iff in H2. nin H2.
  apply H3. unfold in_function_set. intuition.
Qed.


Lemma in_function_set_inc : forall a f u,
 in_function_set a f u -> inc u (function_set a f).
Proof. intros. pose (function_set_iff a f u). unfold iff in (type of i).
  destruct i. apply (H1 H).
Qed.


End Function_Set.

Module Notation.
Import Function.

Definition is_notation f :=
  fgraph f & domain f = string.

Definition stop := L string (fun s => emptyset).

Lemma is_notation_stop : is_notation stop.
Proof. red. split. unfold stop. apply create_axioms. 
  unfold stop. aw.
Qed.

Lemma V_stop : forall x, V x stop = emptyset.
Proof. ir. uf stop. 
  apply by_cases with (inc x string); intros. aw.
  rewrite create_V_out; auto. 
Qed.

Definition denote str obj old :=
  L string (fun s => (Yo (s = str) obj (V s old))).

Lemma is_notation_denote : forall str obj old,
  is_notation old -> is_notation (denote str obj old).
Proof. ir. red. unfold denote. split. app create_axioms. aw.
Qed.

Lemma V_denote_new : forall str obj old x,
  x = str -> inc x string -> V x (denote str obj old) = obj.
Proof. ir. uf denote. aw. rww Y_if_rw.
Qed.

Lemma V_denote_old : forall str obj old x,
  ~x=str -> inc x string -> V x (denote str obj old) = V x old.
Proof. ir. uf denote.  aw. rww Y_if_not_rw.
Qed. 

Lemma R_string_inj : forall a b:string,
  ~a=b -> ~(Ro a = Ro b).
Proof. ir. red. ir. apply H. apply R_inj. assumption. 
Qed.


Ltac show_string :=
match goal with
| |- inc ?X1 string  => try assumption; unfold X1; apply R_inc
| _ => fail
end.
 
Ltac show_different :=
match goal with
| |- ~(?X1 = ?X2) => 
(try (unfold X1); try (unfold X2);
apply R_string_inj; discriminate)
| _ => fail
end. 

Ltac drw_solve := solve [trivial | show_different | assumption | show_string].

Ltac drw_new := 
rewrite V_denote_new; [idtac | drw_solve | drw_solve].

Ltac drw_old :=
rewrite V_denote_old; [idtac | drw_solve | drw_solve].

Ltac drw_stop := rewrite V_stop.

Ltac drw := first [
drw_new ; drw | drw_old; drw | drw_stop ; drw | 
trivial | assumption | idtac].

Open Local Scope string_scope. 

Definition Underlying := Ro "Underlying".  
Definition Source  := Ro "Source". 
Definition Target  := Ro "Target". 
Definition Graph  := Ro "Graph". 

Definition U x  := V Underlying x.
Definition sourceC x := V Source x.
Definition graphC x := V Graph x.
Definition targetC x := V Target x.

Definition unary (x:Bset) (f:EE) := L x f.

Lemma V_unary : forall x f a, inc a x -> 
  V a (unary x f) = f a.
Proof. ir. unfold unary.  aw.
Qed. 

Definition binary (x:Bset) (f:EEE) :=
  L x (fun a => (L x (fun b => f b a))).

Lemma V_V_binary : forall x f a b,
  inc a x -> inc b x -> V a (V b (binary x f)) = f a b.
Proof. ir. uf binary. aw.  
Qed. 
End Notation. 
Export Notation. 


Module Universe.
Export Function.
Export Notation.



Definition axioms u :=
(forall x y, inc x u -> inc y x -> inc y u) &
(forall x (f:x->Bset), inc x u -> (sub (IM f) u) ->
inc (IM f) u) &
(forall x, inc x u -> inc (union x) u) &
(forall x, inc x u -> inc (powerset x) u) &
inc nat u &
inc string u.

Lemma inc_trans_u : forall x u, axioms u -> 
(exists y, (inc x y & inc y u)) -> inc x u.
Proof. intros. destruct H as [H1 H2].
  induction H0. destruct H. apply (H1 x0 x H0 H).
Qed. 

Lemma inc_powerset_u : forall x u, axioms u ->  inc x u ->
inc (powerset x) u.
Proof. intros. destruct H as [H1 [H2 [H3 [H4 [H5 H6]]]]].
  apply (H4 _ H0).
Qed. 

Lemma inc_nat_u : forall u, axioms u -> inc nat u.
Proof.  intros. destruct H as [H1 [H2 [H3 [H4 [H5 H6]]]]]. assumption.
Qed.

Lemma inc_R_nat_u : forall (n:nat) u, axioms u -> inc (Ro n) u.
Proof. intros.  apply inc_trans_u.  assumption. 
  exists nat. split.  red. exists n.  trivial. apply (inc_nat_u  H). 
Qed. 

Lemma inc_prop_u : forall u, axioms u -> inc Prop u.
Proof. intros. rewrite <-  R_two_prop. apply inc_R_nat_u. assumption. 
Qed.

Lemma inc_R_a_prop_u : forall u (p:Prop), axioms u ->  inc (Ro p) u.
Proof. intros. apply inc_trans_u.  assumption. exists Prop. split. 
  red.  exists p; trivial.  apply inc_prop_u.  assumption.
Qed. 

Lemma inc_a_prop_u : forall u (p:Prop), axioms u -> inc p u.
Proof. intros. assert (Ro p = p). rewrite prop_realization.  trivial. 
  rewrite <-  H0. apply inc_R_a_prop_u.  assumption.
Qed.

Lemma inc_proof_u : forall u (p:Prop) (t:p), axioms u -> inc (Ro t) u. 
Proof. intros. apply inc_trans_u. assumption. exists p.  split.
  apply R_inc. apply inc_a_prop_u.  assumption.
Qed. 


Lemma inc_string_u : forall u, axioms u -> inc string u.
Proof. intros.  destruct H as [H1 [H2 [H3 [H4 [H5 H6]]]]]. assumption.
Qed. 

Lemma inc_subset_u : forall x u, axioms u ->
(exists y, (inc y u & sub x y)) -> inc x u.
Proof. intros. induction H0.  induction H0. apply inc_trans_u. assumption.
  exists (powerset x0).  split. apply powerset_inc. assumption. 
  apply inc_powerset_u.  assumption. assumption.
Qed. 

Lemma inc_emptyset_u : forall u, axioms u -> inc emptyset u.
Proof. intros. apply inc_subset_u.  assumption. exists nat. split.
  apply inc_nat_u. assumption.  red. intros. set (Bo H0). induction e. 
Qed. 

Lemma inc_IM_u : forall x (f:x->Bset) u,
  axioms u -> inc x u -> sub (IM f) u ->
  inc (IM f) u.
Proof. intros x f u Ha Hb. destruct Ha as [H1 [H2 [H3 [H4 [H5 H6]]]]].
  apply H2. assumption.
Qed. 


Definition doubleton_step :forall (x y:Bset) (n:nat), Bset.
intros. induction n. exact x. exact y. 
Defined.

Lemma IM_doubleton_step: forall x y,
  IM (doubleton_step x y) = (doubleton x y).
Proof. intros. apply extensionality; unfold sub; intros. 
  set (IM_exists H). induction e.  induction x1.
  assert (x = x0).  assumption. rewrite <- H1. 
  fprops. assert (y = x0).  assumption. rewrite <- H1. 
  fprops.  apply IM_inc.  
  pose (doubleton_or H). induction o. exists 0. symmetry; assumption. 
  exists 1. symmetry; assumption. 
Qed. 

Lemma inc_doubleton_u : forall x y u, 
  axioms u -> inc x u -> inc y u -> inc (doubleton x y) u.
Proof. intros.  rewrite <- IM_doubleton_step. 
  apply inc_IM_u. assumption. apply inc_nat_u.  assumption.
  rewrite IM_doubleton_step.  red. intros.
  set (doubleton_or H2). induction o. rewrite H3. assumption.
  rewrite H3. assumption.
Qed.

Lemma inc_singleton_u : forall x u,
axioms u -> inc x u -> inc (singleton x) u.
Proof. intros. rewrite <- doubleton_singleton. apply inc_doubleton_u. 
  assumption. assumption. assumption.
Qed. 

Lemma inc_pair_u : forall x y u, 
  axioms u -> inc x u -> inc y u -> inc (pair x y) u.
Proof. intros. unfold pair. uf pair_first. uf pair_second.
  apply inc_doubleton_u. assumption.  
  apply inc_singleton_u. assumption. assumption.
  apply inc_doubleton_u. assumption. apply inc_emptyset_u.  assumption.
  apply inc_singleton_u. assumption. assumption.
Qed.

Lemma sub_u : forall x u, axioms u -> inc x u -> sub x u.
Proof. intros. red.  intros. apply inc_trans_u. assumption. 
  exists x. intuition.
Qed. 

Lemma inc_function_create_u : forall x f u,
axioms u -> inc x u -> 
(forall y, inc y x -> inc (f y) u) ->
inc (L x f) u.
Proof. intros. unfold fcreate. uf fun_image.
  apply inc_IM_u. assumption. assumption.  red. intros.
  pose (IM_exists H2).  induction e.  rewrite <- H3.
  apply inc_pair_u. assumption. apply inc_trans_u. assumption.
  exists x. split. apply R_inc. assumption. apply H1. apply R_inc. 
Qed. 

Lemma inc_function_tcreate_u : forall x (f:x->Bset) u,
axioms u -> inc x u -> 
(forall y, inc (f y) u) ->
inc (tcreate f) u. 
Proof. intros. unfold tcreate.  apply inc_function_create_u. assumption. 
  assumption. intros.  
  assert ( (Yy (fun hyp : inc y x => f (Bo hyp)) emptyset) = f (Bo H2)). 
  apply (Yy_if H2). trivial.  rewrite H3. apply H1.
Qed. 

Lemma inc_pr1_of_pair_u : forall u x,
axioms u -> (exists y, inc (pair x y) u) -> inc x u.
Proof. intros.  induction H0. apply inc_trans_u. assumption.
  exists (singleton x). split.  apply singleton_inc. 
  apply inc_trans_u. assumption. exists (pair x x0). split. unfold pair.
  fprops. assumption. 
Qed.

Lemma inc_pr2_of_pair_u : forall u y,
axioms u -> (exists x, inc (pair x y) u) -> inc y u.
Proof.  intros.  induction H0. apply inc_trans_u. assumption.
  exists (singleton y). split.  apply singleton_inc. 
  apply inc_trans_u. assumption. exists (doubleton emptyset (singleton y)).
  split. fprops. apply inc_trans_u. assumption. 
  exists (pair x y). split.  unfold pair. fprops.  assumption. 
Qed. 

Lemma inc_V_u : forall f x u,
axioms u -> inc f u -> inc x u -> inc (V x f) u.
Proof. intros. pose (V_or x f). induction o.
  apply inc_pr2_of_pair_u.  assumption. exists x. 
  apply inc_trans_u. assumption. exists f. intuition.
  destruct H2. rewrite H3. apply inc_emptyset_u. assumption.
Qed. 

Lemma inc_denote_u : forall s x a u,
axioms u -> inc a u -> inc s string -> inc x u ->
inc (denote s x a) u.
Proof. intros. unfold denote. apply inc_function_create_u. assumption.
  apply inc_string_u.  assumption. intros.
  apply by_cases with (y=s). intros. rewrite Y_if_rw. assumption.
  assumption. intros. rewrite Y_if_not_rw.  apply inc_V_u. assumption.
  assumption. apply inc_trans_u. assumption. exists string.
  split. assumption. apply inc_string_u.  assumption. assumption.
Qed. 




Lemma inc_binary_u : forall x f u,
axioms u -> inc x u -> 
(forall y z, inc y x -> inc z x -> inc (f y z) u) ->
inc (binary x f) u.
Proof. intros. unfold binary. apply inc_function_create_u. assumption.
  assumption. intros. apply inc_function_create_u. assumption. 
  assumption.  intros. apply H1. assumption. assumption.
Qed. 

Lemma inc_stop_u : forall u,
axioms u -> inc stop u. 
Proof. intros. unfold stop.  apply inc_function_create_u. assumption.
  apply inc_string_u. assumption. intros.  apply inc_emptyset_u. 
  assumption.
Qed. 

Ltac incdu := 
first [
apply inc_denote_u; try drw_solve| apply inc_stop_u].


End Universe. 
(* EOF*)