Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Replace default equality on function types with ((=)==>(=)). Add Seto…

…id-specialized Functor type class. Add do-notation for monads. Add some theory for functors and monads.
  • Loading branch information...
commit 96e41f8ce5f4bb26bc7667b6b4761dad0fa2b059 1 parent 8b7460c
@Eelis Eelis authored
Showing with 325 additions and 123 deletions.
  1. +1 −1  src/categories/functor.v
  2. +1 −1  src/implementations/QType_rationals.v
  3. +1 −1  src/implementations/ZType_integers.v
  4. +2 −2 src/implementations/fast_rationals.v
  5. +2 −1  src/implementations/field_of_fractions.v
  6. +7 −4 src/implementations/natpair_integers.v
  7. +1 −1  src/implementations/peano_naturals.v
  8. +3 −2 src/implementations/positive_integers_naturals.v
  9. +3 −0  src/implementations/signed_binary_positive_integers.v
  10. +2 −2 src/implementations/stdlib_rationals.v
  11. +7 −2 src/interfaces/canonical_names.v
  12. +37 −1 src/interfaces/functors.v
  13. +4 −3 src/interfaces/integers.v
  14. +27 −17 src/interfaces/monads.v
  15. +5 −3 src/interfaces/naturals.v
  16. +8 −14 src/interfaces/sequences.v
  17. +3 −2 src/theory/adjunctions.v
  18. +3 −3 src/theory/categories.v
  19. +53 −0 src/theory/functors.v
  20. +1 −1  src/theory/hom_functor.v
  21. +9 −8 src/theory/integers.v
  22. +38 −23 src/theory/jections.v
  23. +50 −0 src/theory/monads.v
  24. +10 −8 src/theory/naturals.v
  25. +4 −4 src/theory/rationals.v
  26. +11 −7 src/theory/sequences.v
  27. +10 −5 src/theory/setoids.v
  28. +3 −0  src/theory/ua_congruence.v
  29. +4 −3 src/theory/ua_homomorphisms.v
  30. +12 −2 src/theory/ua_products.v
  31. +2 −2 src/theory/ua_term_monad.v
  32. +1 −0  tools/coq.mim
View
2  src/categories/functor.v
@@ -1,6 +1,6 @@
Require Import
Morphisms RelationClasses Equivalence Setoid
- abstract_algebra functors categories.
+ abstract_algebra interfaces.functors categories.
Section natural_transformations_id_comp.
View
2  src/implementations/QType_rationals.v
@@ -88,7 +88,7 @@ Qed.
Instance: Inverse to_Q := of_Q.
Instance: Surjective to_Q.
-Proof. constructor. exact spec_of_Q. apply _. Qed.
+Proof. constructor. intros x y E. rewrite <- E. apply spec_of_Q. apply _. Qed.
Instance: Injective to_Q.
Proof. constructor. auto. apply _. Qed.
View
2  src/implementations/ZType_integers.v
@@ -58,7 +58,7 @@ Qed.
Instance: Inverse to_Z := of_Z.
Instance: Surjective to_Z.
-Proof. constructor. exact spec_of_Z. apply _. Qed.
+Proof. constructor. intros x y E. rewrite <- E. apply spec_of_Z. apply _. Qed.
Instance: Injective to_Z.
Proof. constructor. intros. unfold equiv. unfold anyZ_eq. auto. apply _. Qed.
View
4 src/implementations/fast_rationals.v
@@ -42,8 +42,8 @@ Qed.
Instance: Surjective (λ p, fastZ_to_fastQ (fst p) * / fastZ_to_fastQ (snd p)).
Proof.
split.
-
- intros x. unfold id, compose, inverse, fastZ_to_fastQ.
+
+ intros x y E. rewrite <- E. clear E y. unfold id, compose, inverse, fastZ_to_fastQ.
destruct x as [x | x y]; simpl.
rewrite rings.preserves_1. field.
apply not_symmetry. apply zero_ne_one.
View
3  src/implementations/field_of_fractions.v
@@ -152,7 +152,8 @@ Global Instance: Inverse inject_frac := λ x, (num x, den x).
Global Instance: Surjective inject_frac.
Proof.
constructor.
- intros [n d P].
+ intros [n d P] y E.
+ rewrite <- E.
unfold Basics.compose, inject_frac, equiv, frac_equiv.
simpl.
ring_simplify.
View
11 src/implementations/natpair_integers.v
@@ -211,15 +211,18 @@ Section for_another_ring.
Instance: SemiRing_Morphism inject'_N.
Lemma agree_on_nat: inject'_N = n_to_sr.
- Proof. intro x. apply (naturals.to_semiring_unique inject'_N). Qed.
+ Proof.
+ intros x y E. rewrite E.
+ apply (naturals.to_semiring_unique inject'_N).
+ Qed.
Lemma same_morphism: integers_to_ring Z R = inject'.
- Proof.
- intros [pos0 neg0].
+ Proof with intuition.
+ intros [pos0 neg0] z' E. rewrite <- E. clear E z'.
rewrite split_into_nats.
preservation.
rewrite preserves_inv, abstract_algebra.preserves_inv.
- rewrite (agree_on_nat pos0), (agree_on_nat neg0).
+ rewrite (agree_on_nat pos0 pos0), (agree_on_nat neg0 neg0)...
unfold integers_to_ring, inject. simpl. rewrite theory.rings.preserves_0.
ring.
Qed.
View
2  src/implementations/peano_naturals.v
@@ -99,7 +99,7 @@ Proof. reflexivity. Qed.
Instance: Initial (semiring.object nat).
Proof.
intros. apply natural_initial. intros.
- intro x. induction x.
+ intros x y E. unfold equiv, nat_equiv in E. subst y. induction x.
replace 0%nat with (ring_zero:nat) by reflexivity.
do 2 rewrite preserves_0. reflexivity.
rewrite S_nat_1_plus.
View
5 src/implementations/positive_integers_naturals.v
@@ -126,8 +126,8 @@ Qed.
Instance: Surjective of_nat.
Proof.
split. 2: apply _.
- intros [x Ex].
- unfold to_nat, of_nat. unfold_equivs.
+ intros [x Ex] y E. rewrite <- E.
+ unfold to_nat, of_nat. unfold_equivs.
apply integers.abs_nonneg. assumption.
Qed.
@@ -162,6 +162,7 @@ Lemma ZPos_to_nat_int_abs x p : naturals_to_semiring ZPos nat (exist _ x p) = in
Proof.
replace (int_abs Z nat x) with (to_nat (exist _ x p)) by reflexivity.
apply naturals.to_semiring_unique'. apply _. apply ZPos_to_nat_sr_morphism.
+ reflexivity.
Qed.
Lemma ZPos_int_nat_precedes (x y : ZPos) : `x ≤ `y → x ≤ y.
View
3  src/implementations/signed_binary_positive_integers.v
@@ -153,8 +153,11 @@ Section for_another_ring.
Lemma same_morphism: integers_to_ring Z R = map_Z'.
Proof.
intros [].
+ intros y E. rewrite <- E.
apply agree_on_0.
+ intros p y E. rewrite <- E.
apply agree_on_positive.
+ intros p y E. rewrite <- E.
apply agree_on_negative.
Qed.
View
4 src/implementations/stdlib_rationals.v
@@ -80,7 +80,7 @@ Instance: Inverse inject := λ x, (Qnum x, Zpos (Qden x)).
Instance: Surjective (λ p, inject_Z (fst p) * / inject_Z (snd p)).
Proof.
constructor. 2: apply _.
- intros [num den]. unfold Basics.compose, id.
+ intros [num den] q E. rewrite <- E. unfold Basics.compose, id.
simpl. rewrite Qmake_Qdiv. reflexivity.
Qed.
@@ -94,4 +94,4 @@ Proof.
case (decide (q = 0)); intros E.
rewrite E. reflexivity.
reflexivity.
-Qed.
+Qed.
View
9 src/interfaces/canonical_names.v
@@ -22,8 +22,13 @@ Notation "x ≠ y":= (~ equiv x y): type_scope.
Infix "≡" := eq (at level 70, no associativity).
(* Hm, we could define a very low priority Equiv instance for Leibniz equality.. *)
-Instance ext_eq (A B: Type) `(Equiv B): Equiv (A → B)
- := λ f g: A → B, ∀ x, f x = g x.
+Instance ext_eq `{Equiv A} `{Equiv B}: Equiv (A → B)
+ := ((=) ==> (=))%signature.
+
+(** Interestingly, most of the development works fine if this is defined as
+ ∀ x, f x = g x.
+However, in the end that version was just not strong enough for comfortable rewriting
+in setoid-pervasive contexts. *)
(* Other canonically named relations/operations/constants: *)
Class Decision P := decide: sumbool P (~ P).
View
38 src/interfaces/functors.v
@@ -1,6 +1,6 @@
Global Set Automatic Introduction. (* todo: do this in a more sensible place *)
-Require Import abstract_algebra canonical_names Program.
+Require Import abstract_algebra canonical_names Program Morphisms.
Require setoids.
Section functor_class.
@@ -102,3 +102,39 @@ Section compose_functors.
Qed.
End compose_functors.
+
+(** The Functor class is nice and abstract and theory-friendly, but not as convenient
+ to use for regular programming as Haskell's Functor class. The reason for this is that
+ our Functor is parameterized on two Categories, which by necessity bundle setoid-
+ ness and setoid-morphism-ness into objects and arrows, respectively.
+ The Haskell Functor class, by contrast, is essentially specialized for endofunctors on
+ the category of Haskell types and functions between them. The latter corresponds to our
+ setoid.Object category.
+
+ To recover convenience, we introduce a second functor type class tailored specifically to
+ functors of this kind. The specialization allows us to forgo bundling, and lets us recover
+ the down-to-earth Type→Type type for the type constructor, and the (a→b)→(F a→F b)
+ type for the function map, with all setoid/morphism proofs hidden in the structure class
+ in Prop.
+
+ To justify this definition, in theory/functors we show that instances of this new functor
+ class do indeed give rise to instances of the original nice abstract Functor class. *)
+
+Section setoid_functor.
+
+ Context (map_obj: Type → Type) {map_eq: ∀ `{Equiv A}, Equiv (map_obj A)}.
+
+ Class SFmap: Type := sfmap: ∀ `(v → w), (map_obj v → map_obj w).
+
+ Class SFunctor `{SFmap}: Prop :=
+ { sfunctor_makes_setoids `{Setoid A}: Setoid (map_obj A)
+ ; sfunctor_makes_morphisms `{Equiv v} `{Equiv w} (f: v → w):>
+ Setoid_Morphism f → Setoid_Morphism (sfmap f)
+ ; sfunctor_morphism `{Setoid v} `{Setoid w}:>
+ Proper ((equiv ==> equiv) ==> (equiv ==> equiv)) (@sfmap _ v w)
+ ; sfunctor_id `{Setoid v}: sfmap id = id
+ ; sfunctor_comp `{Equiv a} `{Equiv b} `{Equiv c} (f: b → c) (g: a → b):
+ Setoid_Morphism f → Setoid_Morphism g →
+ sfmap (f ∘ g) = sfmap f ∘ sfmap g }.
+
+End setoid_functor.
View
7 src/interfaces/integers.v
@@ -25,10 +25,11 @@ Section initial_maps.
Lemma integer_initial (same_morphism : ∀ `{Ring B} {h : Int → B} `{!Ring_Morphism h}, integers_to_ring B = h) :
Initial (ring.object Int).
Proof.
- intros y [x h] []. simpl in *.
+ intros y [x h] [] ?. simpl in *.
apply same_morphism.
- apply ring.decode_variety_and_ops.
- apply (@ring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h).
+ apply ring.decode_variety_and_ops.
+ apply (@ring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h).
+ reflexivity.
Qed.
End initial_maps.
View
44 src/interfaces/monads.v
@@ -3,29 +3,39 @@ Require categories.setoid.
Require Import Setoid Morphisms.
Require Import abstract_algebra canonical_names theory.categories.
-Section contents.
+Section ops.
-Context (M: Type → Type).
+ Context (M: Type → Type).
-Class MonadReturn := ret: ∀ {A}, A → M A.
-Class MonadBind := bind: ∀ {A B}, M A → (A → M B) → M B.
+ Class MonadReturn := ret: ∀ {A}, A → M A.
+ Class MonadBind := bind: ∀ {A B}, M A → (A → M B) → M B.
+
+End ops.
+
+Implicit Arguments ret [[M] [MonadReturn] [A]].
+Implicit Arguments bind [[M] [MonadBind] [A] [B]].
Infix ">>=" := bind (at level 50, no associativity).
+Notation "x ← y ; z" := (y >>= (λ x : _, z)) (at level 30, right associativity).
+Notation "x >> y" := (_ ← x ; y) (at level 30, right associativity).
+
+Section structure.
+
+ Context (M: Type → Type).
-Class Monad {Me: ∀ A, Equiv A → Equiv (M A)} `{MonadReturn} `{MonadBind}: Prop :=
+ Class Monad {Me: ∀ A, Equiv A → Equiv (M A)} `{MonadReturn M} `{MonadBind M}: Prop :=
(* Propers: *)
- { ret_proper:> ∀ `{Equiv A}, Proper (equiv ==> equiv) (@ret _ A)
- ; bind_proper:> ∀ `{Equiv A} `{Equiv B},
- Proper (equiv ==> (equiv ==> equiv) ==> equiv) (@bind _ A B)
+ { ret_proper:> ∀ `{Equiv A}, Proper (equiv ==> equiv) (@ret _ _ A)
+ ; bind_proper:> ∀ `{Equiv A} `{Equiv B},
+ Proper (equiv ==> (equiv ==> equiv) ==> equiv) (@bind _ _ A B)
- ; equivalence: ∀ `{Setoid A}, Setoid (M A)
+ ; mon_setoid: ∀ `{Setoid A}, Setoid (M A)
- (* Laws: *)
- ; mon_lunit: ∀ `{Setoid A} `{Setoid B} (x: A) (f: A → M B), ret x >>= f = f x
- ; mon_runit: ∀ `{Setoid A} (m: M A), m >>= ret = m
- ; mon_assoc: ∀ `{Setoid A} `{Setoid B} `{Setoid C} (n: M A) (f: A → M B) (g: B → M C),
- (n >>= f) >>= g = n >>= (λ x, f x >>= g)
- (* todo: write using Setoid type class (rather than categories.setoid.Object) *)
- }.
+ (* Laws: *)
+ ; mon_lunit: ∀ `{Setoid A} `{Setoid B} (x: A) (f: A → M B), ret x >>= f = f x
+ ; mon_runit: ∀ `{Setoid A} (m: M A), m >>= ret = m
+ ; mon_assoc: ∀ `{Setoid A} `{Setoid B} `{Setoid C} (n: M A) (f: A → M B) (g: B → M C),
+ (n >>= f) >>= g = n >>= (λ x, f x >>= g)
+ }.
-End contents.
+End structure.
View
8 src/interfaces/naturals.v
@@ -34,11 +34,13 @@ Section initial_maps.
Lemma natural_initial (same_morphism : ∀ `{SemiRing B} {h : A → B} `{!SemiRing_Morphism h}, naturals_to_semiring B = h) :
Initial (semiring.object A).
Proof.
- intros y [x h] []. simpl in *.
+ intros y [x h] [] ?. simpl in *.
apply same_morphism.
- apply semiring.decode_variety_and_ops.
- apply (@semiring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h).
+ apply semiring.decode_variety_and_ops.
+ apply (@semiring.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h).
+ reflexivity.
Qed.
+
End initial_maps.
Instance: Params (@naturals_to_semiring) 7.
View
22 src/interfaces/sequences.v
@@ -3,26 +3,16 @@ Set Automatic Coercions Import.
Require Import
Morphisms List Program
- abstract_algebra theory.categories forget_algebra forget_variety theory.rings interfaces.functors.
+ abstract_algebra theory.categories forget_algebra forget_variety theory.rings interfaces.functors
+ canonical_names.
Require
categories.setoid categories.product varieties.monoid categories.algebra.
Require categories.cat theory.setoids.
Module ua := universal_algebra.
-Instance oh: ∀ {A} `{Equiv B} `{Equiv C} (f: B → C) `{!Setoid_Morphism f},
- Proper ((=) ==> (=)) (@compose A B C f).
-Proof. firstorder. Qed.
-
-Instance: ∀ {A} `{Equiv B} `{Equiv C}, Proper ((=) ==> eq ==> (=)) (@compose A B C).
-Proof. repeat intro. subst. firstorder. Qed.
-
-Lemma eta {A} `{Setoid B} (f: A → B): (λ x, f x) = f.
-Proof. intro. reflexivity. Qed.
-
Instance: Arrows Type := λ X Y, X → Y.
-
-(* todo: move last four elsewhere *)
+ (* todo: move elsewhere *)
(* First, the nice clean high level encapsulated version: *)
@@ -103,9 +93,11 @@ Section practical.
repeat intro.
simpl.
apply sequence_fmap_id.
+ reflexivity.
repeat intro.
simpl.
apply sequence_fmap_comp.
+ reflexivity.
Qed.
Program Definition posh_inject: id ⇛ monoid.forget ∘ posh_free := λ a, inject a.
@@ -135,6 +127,7 @@ Section practical.
rewrite E.
apply sequence_inject_natural.
apply _.
+ reflexivity.
Qed.
Goal @PoshSequence posh_free posh_fmap posh_inject posh_extend.
@@ -155,13 +148,14 @@ Section practical.
rewrite H4.
symmetry.
apply (@sequence_extend_commutes PS x _ _ _ _ _ _ H2 f fM).
+ reflexivity.
unfold compose.
intros [x0 h] H4 [] a.
unfold equiv, setoid.Equiv_instance_0 in H4.
simpl in *.
apply (@sequence_only_extend_commutes PS x _ _ _ _ _ _ H2 f _ (x0 tt)).
apply (@monoid.decode_morphism_and_ops _ _ _ _ _ _ _ _ _ h).
- intro. symmetry. apply H4. reflexivity.
+ intros. symmetry. apply H4. reflexivity.
unfold posh_extend.
intros [x ??] [y ?? yV].
constructor; try apply _.
View
5 src/theory/adjunctions.v
@@ -4,7 +4,7 @@ Set Automatic Introduction.
Require Import
Relation_Definitions Morphisms Setoid Program
- abstract_algebra setoids functors categories
+ abstract_algebra setoids interfaces.functors categories
workaround_tactics theory.jections.
Require dual.
@@ -151,7 +151,8 @@ Section for_ηAdjunction.
unfold φ.
repeat intro.
constructor.
- intro. symmetry.
+ intros x0 y E. symmetry.
+ rewrite <- E.
apply (η_adjunction_universal F G x).
constructor...
intros ?? E. rewrite E. reflexivity.
View
6 src/theory/categories.v
@@ -1,7 +1,7 @@
Set Automatic Introduction.
Require Import
- Relation_Definitions Morphisms Setoid Program abstract_algebra setoids functors theory.jections.
+ Relation_Definitions Morphisms Setoid Program abstract_algebra setoids interfaces.functors theory.jections.
Notation "x ⇛ y" := (∀ a, x a ⟶ y a) (at level 90, right associativity).
(* Transformations (polymorphic arrows). Couldn't find an "arrow with dot over it" unicode character. *)
@@ -60,8 +60,8 @@ Section adjunction.
; ηε_adjunction_right_functor: Functor G _
; ηε_adjunction_η_natural: NaturalTransformation η
; ηε_adjunction_ε_natural: NaturalTransformation ε
- ; ηε_adjunction_identity_at_G: a, fmap G (ε a) ◎ η (G a)) = id_nat_trans G
- ; ηε_adjunction_identity_at_F: a, ε (F a) ◎ fmap F (η a)) = id_nat_trans F }.
+ ; ηε_adjunction_identity_at_G: a, fmap G (ε a) ◎ η (G a) = id_nat_trans G a
+ ; ηε_adjunction_identity_at_F: a, ε (F a) ◎ fmap F (η a) = id_nat_trans F a }.
(* We currently don't define adjunctions as characterized in MacLane p81 Theorem 2 (ii) and (iv). *)
View
53 src/theory/functors.v
@@ -0,0 +1,53 @@
+
+Require Import
+ Program
+ canonical_names abstract_algebra
+ interfaces.functors.
+Require
+ categories.setoid.
+
+Section setoid_functor_as_posh_functor.
+
+ Context `{SFunctor F}.
+
+ Program Definition map_setoid: setoid.Object → setoid.Object :=
+ λ o, @setoid.object (F (setoid.T o)) (map_eq (setoid.T o) (setoid.e o)) _.
+
+ Next Obligation. Proof.
+ destruct o.
+ apply (@sfunctor_makes_setoids F _ _ _).
+ assumption.
+ Qed.
+
+ Program Instance: Fmap map_setoid := λ v w X, @sfmap F H _ _ (proj1_sig X).
+
+ Next Obligation. Proof.
+ destruct v, w, X. simpl in *.
+ apply sfunctor_makes_morphisms; apply _.
+ Qed.
+
+ Instance: Functor map_setoid _.
+ Proof with auto; intuition.
+ pose proof (@sfunctor_makes_setoids F _ _ _).
+ constructor; try apply _.
+ intros [???] [???].
+ constructor; try apply _.
+ intros [x ?] [y ?] U ?? E. simpl in *.
+ rewrite E.
+ cut (sfmap F x = sfmap F y)...
+ assert (x = y) as E'. intro...
+ rewrite E'...
+ apply (sfunctor_makes_morphisms F)...
+ intros [???] x ??. simpl in *.
+ rewrite (sfunctor_id F x x)...
+ intros [???] [???] [??] [???] [??] ?? E. simpl in *.
+ unfold compose at 2.
+ rewrite <- E.
+ apply (sfunctor_comp F)...
+ Qed.
+
+End setoid_functor_as_posh_functor.
+
+(** Note that we cannot prove the reverse (i.e. that an endo-Functor on
+ setoid.Object gives rise to an SFunctor, because an SFunctor requires a
+ Type→Type map, which we cannot get from a setoid.Object→setoid.Object map. *)
View
2  src/theory/hom_functor.v
@@ -2,7 +2,7 @@ Set Automatic Introduction.
Require Import
Relation_Definitions Morphisms Setoid Program
- abstract_algebra setoids functors categories.
+ abstract_algebra setoids interfaces.functors categories.
Require categories.setoid.
View
17 src/theory/integers.v
@@ -32,20 +32,21 @@ Qed.
Lemma to_ring_unique' `{Integers Int} `{Ring R} (f g: Int → R) `{!Ring_Morphism f} `{!Ring_Morphism g}:
f = g.
Proof.
- intro.
+ intros x y E.
rewrite (to_ring_unique f), (to_ring_unique g).
+ rewrite E.
reflexivity.
Qed.
(* A ring morphism from integers to another ring is injective if there's an injection in the other direction: *)
Lemma to_ring_injective `{Integers Int} `{Ring R} (f: R → Int) (g: Int → R) `{!Ring_Morphism f} `{!Ring_Morphism g}:
Injective g.
-Proof.
+Proof with intuition.
constructor. 2: constructor; apply _.
intros x y E.
- rewrite <- (to_ring_unique' (f ∘ g) id x).
- rewrite <- (to_ring_unique' (f ∘ g) id y).
- unfold compose. rewrite E. reflexivity.
+ rewrite <- (to_ring_unique' (f ∘ g) id x x)...
+ rewrite <- (to_ring_unique' (f ∘ g) id y y)...
+ unfold compose. rewrite E...
Qed.
Instance integers_to_integers_injective `{Integers Int} `{Integers Int2} (f: Int → Int2) `{!Ring_Morphism f}:
@@ -80,11 +81,11 @@ Section retract_is_int.
Lemma same_morphism: integers_to_ring Int R ∘ inverse f = h.
Proof with auto.
- intro x.
+ intros x y U.
pose proof (to_ring_unique (h ∘ f)) as E.
unfold compose in *.
- rewrite <-E. apply sm_proper.
- apply jections.surjective_applied.
+ rewrite <- E. apply sm_proper.
+ rewrite <- U. apply jections.surjective_applied.
Qed.
End for_another_ring.
View
61 src/theory/jections.v
@@ -18,14 +18,13 @@ Section compositions.
Proof. firstorder. Qed.
Global Instance: Surjective f → Surjective g → Surjective (f ∘ g).
- Proof with try apply _.
+ Proof with try apply _; intuition.
constructor...
- change (f ∘ (g ∘ gi ∘ fi) = id).
- intro. unfold compose.
pose proof (setoidmor_b f).
- posed_rewrite (surjective g (fi x)).
- posed_rewrite (surjective f x).
- reflexivity.
+ pose proof (setoidmor_a f).
+ intros x y E. unfold compose.
+ posed_rewrite (surjective g (fi x) (fi x))...
+ posed_rewrite (surjective f x x)...
Qed.
Global Instance: Bijective f → Bijective g → Bijective (f ∘ g).
@@ -33,7 +32,18 @@ Section compositions.
End compositions.
Lemma back `{Bijective A B f}: f ⁻¹ ∘ f = id. (* a.k.a. "split-mono" *)
-Proof. firstorder. Qed.
+Proof.
+ intros x y E.
+ unfold compose.
+ destruct H.
+ unfold id, inverse.
+ apply bijective_injective.
+ destruct (bijective_surjective).
+ apply surjective.
+ destruct surjective_mor.
+ apply sm_proper.
+ assumption.
+Qed.
(* recall that "f ∘ f ⁻¹ = id" is just surjective. *)
Lemma surjective_applied `{Surjective A B f} x : f (f⁻¹ x) = x.
@@ -50,20 +60,20 @@ Lemma alt_injective `{Equiv A} `{Equiv B} `{f: A → B} `{!Inverse f}:
Setoid_Morphism f →
Setoid_Morphism (f ⁻¹: B → A) →
f ⁻¹ ∘ f = id → Injective f.
-Proof with try tauto.
+Proof with try tauto; intuition.
intros ?? E.
pose proof (setoidmor_a f).
pose proof (setoidmor_b f).
- constructor...
- intros ?? E'.
- rewrite <- (E x), <- (E y).
- unfold compose.
- rewrite E'...
- intuition.
+ constructor.
+ intros ?? F.
+ rewrite <- (E x x), <- (E y y)...
+ unfold compose.
+ rewrite F...
+ tauto.
Qed.
Instance: ∀ `{Bijective A B f}, Setoid_Morphism (f⁻¹).
-Proof with try tauto.
+Proof with try tauto; intuition.
intros.
pose proof (setoidmor_a f).
pose proof (setoidmor_b f).
@@ -71,7 +81,8 @@ Proof with try tauto.
repeat intro.
apply (injective f).
change ((f ∘ f ⁻¹) x = (f ∘ f ⁻¹) y).
- do 2 rewrite (surjective f _)...
+ rewrite (surjective f x x)...
+ rewrite (surjective f y y)...
Qed.
Instance: ∀ `{Inverse A B f}, Inverse (f ⁻¹) := λ _ _ f _, f.
@@ -83,10 +94,11 @@ Proof with intuition.
pose proof (setoidmor_b f).
repeat (constructor; try apply _).
intros x y E.
- rewrite <- (surjective f x), <- (surjective f y).
+ rewrite <- (surjective f x x), <- (surjective f y y)...
unfold compose. (* f_equal ?*)
rewrite E...
- intro. apply (injective f), (surjective f).
+ intros x y E. rewrite <- E.
+ apply bijective_applied.
Qed.
Hint Extern 4 (Bijective (inverse _)) => apply flip_bijection_pseudoinstance: typeclass_instances.
@@ -104,8 +116,9 @@ Proof.
pose proof (setoidmor_a f).
pose proof (setoidmor_b f).
intros. apply (injective f).
- posed_rewrite (surjective f y).
+ posed_rewrite (surjective f y y).
assumption.
+ reflexivity.
Qed.
Lemma cancel_left' `{Bijective A B f} x y: f ⁻¹ x = y → x = f y.
@@ -123,15 +136,17 @@ Proof with intuition.
constructor.
intros x y ?.
apply (injective f).
- rewrite (P x), (P y)...
+ rewrite (P x x), (P y y)...
rewrite <-P...
Qed.
Instance Surjective_proper `{Equiv A} `{Equiv B} (f g: A → B) {finv: Inverse f}:
f = g → Surjective g (inv:=finv) → Surjective f.
-Proof with try apply _; try assumption.
+Proof with try apply _; intuition.
intros E [P [Q U Z]].
repeat constructor...
- intro. unfold compose. rewrite (E (inverse f x)). apply P.
- repeat intro. rewrite (E x), (E y). apply Z...
+ intros x y F. unfold compose.
+ rewrite <- F.
+ rewrite (E (inverse f x) (inverse f x))... apply P...
+ repeat intro. rewrite (E x x), (E y y)...
Qed.
View
50 src/theory/monads.v
@@ -0,0 +1,50 @@
+
+Require Import
+ Program Morphisms
+ canonical_names
+ abstract_algebra
+ interfaces.monads
+ interfaces.functors.
+
+Section contents.
+
+ Context `{Monad M}.
+
+ Instance liftM: SFmap M := λ {A B} (f: A → B) (ma: M A), ma >>= ret ∘ f.
+
+ Instance: SFunctor M.
+ Proof with intuition.
+ pose proof (@mon_setoid M _ _ _ _).
+ constructor; intros; try apply _; unfold sfmap, liftM.
+ pose proof (setoidmor_a f).
+ pose proof (setoidmor_b f).
+ constructor; try apply _.
+ intros ?? E. rewrite E...
+ intros ?? E. repeat intro.
+ apply (@bind_proper M _ _ _ _ v _ w _)...
+ intros c d. intros.
+ unfold compose.
+ rewrite (E c d)...
+ intros x y E.
+ unfold id at 2.
+ rewrite <- E.
+ rewrite compose_id_right.
+ apply mon_runit; apply _.
+ intros x y E.
+ unfold compose at 3.
+ pose proof (setoidmor_a g).
+ pose proof (setoidmor_b g).
+ pose proof (setoidmor_b f).
+ rewrite mon_assoc; try apply _.
+ apply (bind_proper M x y E).
+ intros v w U.
+ unfold compose.
+ rewrite mon_lunit; try apply _.
+ rewrite U.
+ reflexivity.
+ Qed.
+
+ Definition liftM2 {A B C} (f: A → B → C) (x: M A) (y: M B): M C :=
+ xv ← x; yv ← y; ret (f xv yv).
+
+End contents.
View
18 src/theory/naturals.v
@@ -29,9 +29,10 @@ Qed.
Lemma to_semiring_unique' `{Naturals N} `{SemiRing SR} (f g: N → SR) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} :
f = g.
Proof.
- intro.
+ intros x y E.
rewrite (to_semiring_unique f).
rewrite (to_semiring_unique g).
+ rewrite E.
reflexivity.
Qed.
@@ -60,11 +61,11 @@ Qed.
Lemma to_semiring_injective `{Naturals N} `{SemiRing A}
(f: A → N) (g: N → A) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g}: Injective g.
-Proof.
+Proof with intuition.
constructor. 2: constructor; apply _.
intros x y E.
- rewrite <- (to_semiring_unique' (f ∘ g) id x).
- rewrite <- (to_semiring_unique' (f ∘ g) id y).
+ rewrite <- (to_semiring_unique' (f ∘ g) id x x)...
+ rewrite <- (to_semiring_unique' (f ∘ g) id y y)...
unfold compose. rewrite E. reflexivity.
Qed.
@@ -90,10 +91,11 @@ Section retract_is_nat.
Lemma same_morphism: naturals_to_semiring N R ∘ inverse f = h.
Proof with auto.
- intro x.
+ intros x y F.
pose proof (to_semiring_unique (h ∘ f)) as E.
unfold compose in *.
- rewrite <-E. apply sm_proper.
+ rewrite <- E. apply sm_proper.
+ rewrite <- F.
apply jections.surjective_applied.
Qed.
End for_another_semiring.
@@ -260,8 +262,8 @@ Section contents.
rewrite A, E, F, B...
Qed.
- Lemma nat_distance_unique {a b: NatDistance N} x: a x = b x.
- Proof. intro. apply nat_distance_unique_respectful; reflexivity. Qed.
+(* Lemma nat_distance_unique {a b: NatDistance N} x: a x = b x.
+ Proof. intro. apply nat_distance_unique_respectful; reflexivity. Qed.*)
Global Instance nat_distance_proper `{!NatDistance N}: Proper ((=) ==> (=) ==> (=)) (λ x y: N, ` (nat_distance x y)).
(* Program *should* allow us to write plain nat_distance instead of the
View
8 src/theory/rationals.v
@@ -21,11 +21,11 @@ Section alt_Build_Rationals.
intro x.
unfold Basics.compose, id in *.
transitivity (inject (fst (inverse _ x)) * / inject (snd (inverse _ x))).
- 2: apply sur.
+ 2: apply sur...
pose proof (integers.to_ring_unique'
(integers_to_ring (Z nat) A ∘ integers_to_ring Int (Z nat)) inject) as B.
- pose proof (B (fst (inverse _ x))) as P1. simpl in P1. rewrite P1.
- pose proof (B (snd (inverse _ x))) as P2. simpl in P2. rewrite P2.
+ pose proof (B (fst (inverse _ x)) (fst (inverse _ x)) (reflexivity _)) as P1. simpl in P1. rewrite P1.
+ pose proof (B (snd (inverse _ x)) (snd (inverse _ x)) (reflexivity _)) as P2. simpl in P2. rewrite P2.
reflexivity.
constructor; try apply _.
intros x y E.
@@ -80,7 +80,7 @@ Section isomorphism_is_rationals.
Lemma isomorphism_is_rationals: Rationals F (inj_inv:=isomorphism_is_inj_inv).
Proof.
repeat (split; try apply _).
- intros x. unfold id, compose, inverse, isomorphism_is_inj_inv, compose.
+ intros x y U. rewrite <- U. unfold id, compose, inverse, isomorphism_is_inj_inv, compose.
apply (injective (inverse f)).
rewrite <-(@surjective_applied _ _ _ _ _ inj_inv rationals_frac (inverse f x)) at 3.
rewrite rings.preserves_mult, preserves_dec_mult_inv.
View
18 src/theory/sequences.v
@@ -3,7 +3,7 @@ Set Automatic Introduction.
Require Import
Program
theory.categories
- functors
+ interfaces.functors
abstract_algebra
interfaces.sequences
canonical_names.
@@ -22,7 +22,11 @@ Section contents.
pose proof (@setoidmor_a _ _ _ _ f _).
pose proof (@monmor_b _ _ _ _ _ _ _ _ g _).
pose proof (sequence_only_extend_commutes sq (f ∘ inject A) _) as E.
+ pose proof (_: Setoid_Morphism (f ∘ inject A)) as cm.
rewrite (E f), (E g)...
+ apply (sequence_extend_morphism sq)...
+ apply cm.
+ apply cm.
Qed.
Lemma extend_comp
@@ -40,17 +44,17 @@ Section contents.
apply (sequence_only_extend_commutes sq (f ∘ g))...
symmetry.
rewrite <- (sequence_extend_commutes sq g _) at 1.
- reflexivity.
+ apply sm_proper.
Qed.
- Lemma extend_inject A `{Setoid A}: extend (inject A) = id.
+ Lemma extend_inject `{Setoid A}: extend (inject A) = @id (sq A).
Proof with try apply _.
symmetry. apply (sequence_only_extend_commutes sq)...
- intro. reflexivity.
+ apply sm_proper.
Qed.
Lemma fmap_alt `{Equiv A} `{Equiv B} (f: A → B):
- Setoid_Morphism f → extend (inject B ∘ f) = fmap sq f.
+ Setoid_Morphism f → extend (inject B ∘ f) = (fmap sq f: sq A → sq B).
Proof with try apply _.
intros.
pose proof (@setoidmor_a _ _ _ _ f _).
@@ -76,7 +80,7 @@ Section contents.
change (f = fold sq ∘ inject B ∘ f).
rewrite fold_inject.
rewrite compose_id_left.
- reflexivity.
+ apply sm_proper.
Qed.
End contents.
@@ -98,7 +102,7 @@ Section semiring_folds.
rewrite <- extend_comp...
rewrite compose_id_right.
rewrite fold_map...
- reflexivity.
+ apply sm_proper.
Qed.
End semiring_folds.
View
15 src/theory/setoids.v
@@ -5,11 +5,15 @@ Set Automatic Introduction.
Require Import
Morphisms Setoid abstract_algebra Program.
+Instance ext_eq_trans `{Setoid A} `{Setoid B}: Transitive (equiv: relation (A → B)).
+Proof. intros ? y ???? w ?. transitivity (y w); firstorder. Qed.
+
+Instance ext_eq_sym `{Setoid A} `{Setoid B}: Symmetric (equiv: relation (A → B)).
+Proof. firstorder. Qed.
+
Instance: Equiv Prop := iff.
Instance: Setoid Prop.
-Instance: ∀ A `{Setoid B}, Setoid (A → B).
-
Instance sig_Setoid `{Setoid A} (P: A → Prop): Setoid (sig P).
Instance sigT_Setoid `{Setoid A} (P: A → Type): Setoid (sigT P).
@@ -39,7 +43,7 @@ Section product.
Let product: Type := ∀ i, c i.
- Global Instance: Equiv product := `(∀ i, x i = y i).
+ Instance product_eq: Equiv product := `(∀ i, x i = y i).
Global Instance: Setoid product.
Proof.
@@ -69,7 +73,8 @@ Proof.
constructor; try apply _.
repeat intro. apply (injective f).
pose proof (surjective f) as E.
- rewrite (E x), (E y). assumption.
+ unfold compose in E.
+ rewrite (E x x), (E y y); intuition.
Qed.
Instance morphism_proper `{ea: Equiv A} `{eb: Equiv B}: Proper ((=) ==> (=)) (@Setoid_Morphism A B _ _).
@@ -78,7 +83,7 @@ Proof.
firstorder.
intros x y E [AS BS P].
constructor; try apply _. intros v w E'.
- rewrite <- (E v), <- (E w), E'. reflexivity.
+ rewrite <- (E v), <- (E w), E'; reflexivity.
Qed.
Lemma projected_equivalence `{Setoid B} `{f: A → B}: Equivalence (λ x y, f x = f y).
View
3  src/theory/ua_congruence.v
@@ -19,6 +19,9 @@ Section contents.
(* Given an equivalence on the algebra's carrier that respects its setoid equality... *)
+ Let hint' (a: sorts σ): Equiv (ua_products.carrier σ bool (fun _: bool => v) a).
+ Proof. apply setoids.product_eq. intro. apply _. Defined.
+
Context (e: ∀ s, relation (v s)).
Section for_nice_e.
View
7 src/theory/ua_homomorphisms.v
@@ -155,15 +155,16 @@ Implicit Arguments inverse [[A] [B] [Inverse]].
induction (σ o); simpl.
intros.
apply (injective (f t)).
- pose proof (surjective (f t) o1).
+ pose proof (surjective (f t) o1 o1 (reflexivity o1)).
transitivity o1...
symmetry...
intros P Q R S T x.
apply IHo0.
specialize (R (inv t x)).
- pose proof (surjective (f t) x) as E.
+ pose proof (surjective (f t) x x) as E.
rewrite E in R.
- assumption.
+ assumption.
+ reflexivity.
apply S. reflexivity.
apply T. reflexivity.
Qed.
View
14 src/theory/ua_products.v
@@ -22,7 +22,13 @@ Section algebras.
| ne_list.cons _ g => λ X X0, rec_impl g (λ i, X i (X0 i))
end.
- Instance rec_impl_proper: ∀ o, Proper (equiv ==> equiv) (rec_impl o).
+ Let u (s: sorts sig): Equiv (forall i : I, carriers i s).
+ apply setoids.product_eq.
+ intro. apply _.
+ Defined.
+
+ Instance rec_impl_proper: ∀ o,
+ Proper (@setoids.product_eq I _ (fun _ => op_type_equiv _ _ _) ==> equiv) (rec_impl o).
Proof with auto.
induction o; simpl. repeat intro...
intros ? ? Y x0 y0 ?. apply IHo.
@@ -103,7 +109,11 @@ Section varieties.
(eval et vars term1 (eval et vars term2))).
apply sig_type_refl.
intro. apply _.
- apply _.
+ apply eval_proper; try apply _.
+ apply product_algebra.
+ intro. apply _.
+ reflexivity.
+ reflexivity.
apply (nqe_proper t (eval et vars term1 (eval et vars term2)) (eval et vars term1 (eval et vars term2)) H2 k p).
subst p k.
simpl.
View
4 src/theory/ua_term_monad.v
@@ -1,6 +1,6 @@
Require Import
Morphisms Setoid
- abstract_algebra universal_algebra monads canonical_names.
+ abstract_algebra universal_algebra interfaces.monads canonical_names.
Section contents.
@@ -100,7 +100,7 @@ Section contents.
Instance: MonadReturn M := λ _ x, Var sign _ x tt.
- Instance: ∀ `{Equiv A}, Proper (equiv ==> equiv) (ret M).
+ Instance: ∀ `{Equiv A}, Proper (equiv ==> equiv) (@ret M _ A).
Proof. repeat intro. assumption. Qed.
(* What remains are the laws: *)
View
1  tools/coq.mim
@@ -16,6 +16,7 @@
("\\/" ?∨)
("/\\" ?∧)
("->" "→")
+ ("<-" "←")
("<->" "↔")
;; Our notations:
Please sign in to comment.
Something went wrong with that request. Please try again.