Profile

Statistics
| Branch: | Revision:

 1 ```Add LoadPath "~/Schreibtisch/svnba/Elgot/Coq/". ``` ```Require Import biCCC. ``` ```Require Import Lemmas_biCCC. ``` ```Require Import ElgotMonad. ``` ```Require Import Coq_Steroids. ``` ```Open Scope c_scope. ``` ```Section Lemmas. ``` ```Context `(ElgotMonad). ``` ```(* Lemmas proven in the following: ``` ```map_id: ``` ``` map id (a:=x) = id ``` ```map_comp: ``` ``` map f ∘ map g = map (f ∘ g) ``` ```lifting_map: ``` ``` f * ∘ map g = (f ∘ g) * ``` ```map_unit: ``` ``` map f ∘ η = η ∘ f ``` ```map_lifting: ``` ``` map f ∘ g * = (map f ∘ g)* ``` ```mapinl_f_iter: ``` ``` (map inl ∘ f) † = f ``` ```map_naturality: ``` ``` map f ∘ u † = (map (f ⊕⊕ id) ∘ u) † ``` ```str_map : ``` ``` map (id ×× f) ∘ τ = τ ∘ (id (a:=z) ×× map f) ``` ```*) ``` ```Lemma map_id : forall ``` ```(x : Obj), ``` ``` map id (a:=x) = id. ``` ```Proof. ``` ```intros. ``` ```unfold map. ``` ```rewrite -> id_l, -> kl1. ``` ```trivial. ``` ```Qed. ``` ```Lemma map_comp : forall ``` ```(x y z : Obj) ``` ```(f: y ~> z) ``` ```(g: x ~> y), ``` ``` map f ∘ map g = map (f ∘ g). ``` ```Proof. ``` ```intros. ``` ```unfold map. ``` ```rewrite <- kl3. ``` ```rewrite -> comp_assoc, -> kl2, -> comp_assoc. ``` ```trivial. ``` ```Qed. ``` ```Lemma lifting_map : forall ``` ```(x y z : Obj) ``` ```(f: y ~> T z) ``` ```(g: x ~> y), ``` ``` f * ∘ map g = (f ∘ g) *. ``` ```Proof. ``` ```intros. ``` ```unfold map. ``` ```rewrite <- kl3. ``` ```rewrite -> comp_assoc, -> kl2. ``` ```trivial. ``` ```Qed. ``` ```Lemma map_unit : forall ``` ```(x y : Obj) ``` ```(f: x ~> y), ``` ``` map f ∘ η = η ∘ f. ``` ```Proof. ``` ```intros. ``` ```unfold map. ``` ```rewrite -> kl2. ``` ```trivial. ``` ```Qed. ``` ```Lemma map_lifting : forall ``` ```(x y z : Obj) ``` ```(f: y ~> z) ``` ```(g: x ~> T y), ``` ``` map f ∘ g * = (map f ∘ g)*. ``` ```Proof. ``` ```intros. ``` ```unfold map. ``` ```rewrite <- kl3. ``` ```trivial. ``` ```Qed. ``` ```Lemma mapinl_f_iter : forall ``` ```(x y : Obj) ``` ```(f: x ~> T y), ``` ``` (map inl ∘ f) † = f. ``` ```Proof. ``` ```intros. ``` ```rewrite <- unfolding. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> kl1, -> id_r. ``` ```trivial. ``` ```Qed. ``` ```Lemma map_naturality : forall ``` ```(x y z : Obj) ``` ```(f: y ~> z) ``` ```(u : x ~> T (y ⊕ x)), ``` ``` map f ∘ u † = (map (f ⊕⊕ id) ∘ u) †. ``` ```Proof. ``` ```intros. ``` ```unfold map. ``` ```rewrite -> naturality. ``` ```rewrite -> comp_assoc, -> map_unit. ``` ```unfold coprodhom. ``` ```rewrite -> f_cpr, -> id_l, -> comp_assoc. ``` ```trivial. ``` ```Qed. ``` ```Lemma str_map : forall ``` ```(x y z : Obj) ``` ```(f: x ~> y), ``` ``` map (id ×× f) ∘ τ = τ ∘ (id (a:=z) ×× map f). ``` ```Proof. ``` ```intros. ``` ```unfold map. ``` ```rewrite <- str4. ``` ```rewrite <- id_l with (f':=id), <- prodhom_comp, -> id_l. ``` ```rewrite -> comp_assoc, -> str3. ``` ```trivial. ``` ```Qed. ``` `End Lemmas.`