deactivated the library/formal_topology directory since it is completely broken and outdated
right associative with precedence 20
for @{ \Pi $_:$a.$b }.
-notation "hvbox(a break = b)"
+notation > "hvbox(a break = b)"
non associative with precedence 45
-for @{ 'eq $a $b }.
+for @{ 'eq ? $a $b }.
+notation < "hvbox(a break maction (=) (=\sub t) b)"
+ non associative with precedence 45
+for @{ 'eq $t $a $b }.
notation "hvbox(a break \leq b)"
non associative with precedence 45
non associative with precedence 45
for @{ 'gt $a $b }.
-notation "hvbox(a break \neq b)"
+notation > "hvbox(a break \neq b)"
+ non associative with precedence 45
+for @{ 'neq ? $a $b }.
+
+notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
non associative with precedence 45
-for @{ 'neq $a $b }.
+for @{ 'neq $t $a $b }.
notation "hvbox(a break \nleq b)"
non associative with precedence 45
notation > "⊩ " with precedence 60 for @{'Vdash ?}.
notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+notation < "maction (mstyle color #ff0000 (…)) (t)"
+non associative with precedence 90 for @{'hide $t}.
+
λG.λC,C':left_coset G.
∀x.((element ? C)·x \sub (subgrp ? C)) ∈ C'.
-interpretation "Left cosets equality" 'eq C C' =
- (cic:/matita/algebra/groups/left_coset_eq.con _ C C').
+interpretation "Left cosets equality" 'eq t C C' =
+ (cic:/matita/algebra/groups/left_coset_eq.con t C C').
definition left_coset_disjoint ≝
λG.λC,C':left_coset G.
rewrite > (?:x = O);
[2: cases Hx; lapply (os_le_to_nat_le ?? H1);
apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
- |1: intros; unfold Type_of_ordered_set in sg;
+ |1: intros; unfold Type_OF_ordered_set in sg a; whd in a:(? %);
lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
qed.
lemma hint_mah1:
- ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
+ ∀C. Type_OF_ordered_uniform_space__1 C → hos_carr (os_r C).
intros; assumption; qed.
coercion hint_mah1 nocomposites.
interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
+ Type_OF_ordered_set nat_ordered_set →
hos_carr (os_l (nat_ordered_set)).
intros; assumption;
qed.
coercion Leibniz.
*)
-interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
-interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y).
+interpretation "setoid1 eq" 'eq t x y = (eq_rel1 _ (eq1 t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel _ (eq t) x y).
interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r).
interpretation "setoid symmetry" 'invert r = (sym ____ r).
notation ".= r" with precedence 50 for @{'trans $r}.
assumption.
qed.
+(*
+
definition powerset_setoid: setoid → setoid1.
intros (T);
constructor 1;
qed.
interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a).
+
+*)
\ No newline at end of file
-formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma
demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma
dama/sandwich.ma dama/ordered_uniform.ma
Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
nat/div_and_mod_diseq.ma nat/lt_arith.ma
logic/cprop_connectives.ma logic/connectives.ma
algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
-formal_topology/saturations_reductions.ma datatypes/subsets.ma formal_topology/relations.ma
nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
didactic/exercises/substitution.ma nat/minus.ma
didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma
nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma
-formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma
dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma
logic/connectives.ma
Q/nat_fact/times.ma nat/factorization.ma
didactic/support/natural_deduction.ma
nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma
nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
-formal_topology/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma
Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.ma
didactic/exercises/shannon.ma nat/minus.ma
Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma
-formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma
nat/minus.ma nat/compare.ma nat/le_arith.ma
Q/ratio/ratio.ma Q/fraction/fraction.ma
nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
algebra/semigroups.ma higher_order_defs/functions.ma
dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma
dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma
-formal_topology/relations.ma datatypes/subsets.ma
higher_order_defs/relations.ma logic/connectives.ma
nat/factorization.ma nat/ord.ma
nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "formal_topology/relations.ma".
-include "datatypes/categories.ma".
-
-record basic_pair: Type ≝
- { concr: REL;
- form: REL;
- rel: arrows1 ? concr form
- }.
-
-notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
-notation "⊩" with precedence 60 for @{'Vdash}.
-
-interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y).
-interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
-
-record relation_pair (BP1,BP2: basic_pair): Type ≝
- { concr_rel: arrows1 ? (concr BP1) (concr BP2);
- form_rel: arrows1 ? (form BP1) (form BP2);
- commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
- }.
-
-notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
-notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
-
-interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
-interpretation "formal relation" 'form_rel r = (form_rel __ r).
-
-definition relation_pair_equality:
- ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
- intros;
- constructor 1;
- [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
- | simplify;
- intros;
- apply refl1;
- | simplify;
- intros 2;
- apply sym1;
- | simplify;
- intros 3;
- apply trans1;
- ]
-qed.
-
-definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
- intros;
- constructor 1;
- [ apply (relation_pair b b1)
- | apply relation_pair_equality
- ]
-qed.
-
-lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
- intros 7 (o1 o2 r r' H c1 f2);
- split; intro H1;
- [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
- lapply (if ?? (H c1 f2) H2) as H3;
- apply (if ?? (commute ?? r' c1 f2) H3);
- | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2;
- lapply (fi ?? (H c1 f2) H2) as H3;
- apply (if ?? (commute ?? r c1 f2) H3);
- ]
-qed.
-
-definition id_relation_pair: ∀o:basic_pair. relation_pair o o.
- intro;
- constructor 1;
- [1,2: apply id1;
- | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H;
- lapply (id_neutral_left1 ?? (form o) (⊩)) as H1;
- apply (.= H);
- apply (H1 \sup -1);]
-qed.
-
-definition relation_pair_composition:
- ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
- intros;
- constructor 1;
- [ intros (r r1);
- constructor 1;
- [ apply (r1 \sub\c ∘ r \sub\c)
- | apply (r1 \sub\f ∘ r \sub\f)
- | lapply (commute ?? r) as H;
- lapply (commute ?? r1) as H1;
- apply (.= ASSOC1);
- apply (.= #‡H1);
- apply (.= ASSOC1\sup -1);
- apply (.= H‡#);
- apply ASSOC1]
- | intros;
- change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));
- change in H with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
- change in H1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
- apply (.= ASSOC1);
- apply (.= #‡H1);
- apply (.= #‡(commute ?? b'));
- apply (.= ASSOC1 \sup -1);
- apply (.= H‡#);
- apply (.= ASSOC1);
- apply (.= #‡(commute ?? b')\sup -1);
- apply (ASSOC1 \sup -1)]
-qed.
-
-definition BP: category1.
- constructor 1;
- [ apply basic_pair
- | apply relation_pair_setoid
- | apply id_relation_pair
- | apply relation_pair_composition
- | intros;
- change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
- ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
- apply (ASSOC1‡#);
- | intros;
- change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
- apply ((id_neutral_right1 ????)‡#);
- | intros;
- change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
- apply ((id_neutral_left1 ????)‡#);]
-qed.
-
-definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
- intros; constructor 1;
- [ apply (ext ? ? (rel o));
- | intros;
- apply (.= #‡H);
- apply refl1]
-qed.
-
-definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
- λo.extS ?? (rel o).
-
-definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
- intros (o); constructor 1;
- [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
- intros; simplify; apply (.= (†H)‡#); apply refl1
- | intros; split; simplify; intros;
- [ apply (. #‡((†H)‡(†H1))); assumption
- | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
-qed.
-
-interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
-
-definition fintersectsS:
- ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
- intros (o); constructor 1;
- [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
- intros; simplify; apply (.= (†H)‡#); apply refl1
- | intros; split; simplify; intros;
- [ apply (. #‡((†H)‡(†H1))); assumption
- | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
-qed.
-
-interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
-
-definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
- intros (o); constructor 1;
- [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
- | intros; split; intros; cases H2; exists [1,3: apply w]
- [ apply (. (#‡H1)‡(H‡#)); assumption
- | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
-qed.
-
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "formal_topology/relations.ma".
+include "datatypes/categories.ma".
+
+record basic_pair: Type ≝
+ { concr: REL;
+ form: REL;
+ rel: arrows1 ? concr form
+ }.
+
+notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
+notation "⊩" with precedence 60 for @{'Vdash}.
+
+interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y).
+interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
+
+record relation_pair (BP1,BP2: basic_pair): Type ≝
+ { concr_rel: arrows1 ? (concr BP1) (concr BP2);
+ form_rel: arrows1 ? (form BP1) (form BP2);
+ commute: ⊩ ∘ concr_rel = form_rel ∘ ⊩
+ }.
+
+notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
+notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
+
+interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
+interpretation "formal relation" 'form_rel r = (form_rel __ r).
+
+definition relation_pair_equality:
+ ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
+ intros;
+ constructor 1;
+ [ apply (λr,r'. ⊩ ∘ r \sub\c = ⊩ ∘ r' \sub\c);
+ | simplify;
+ intros;
+ apply refl1;
+ | simplify;
+ intros 2;
+ apply sym1;
+ | simplify;
+ intros 3;
+ apply trans1;
+ ]
+qed.
+
+definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
+ intros;
+ constructor 1;
+ [ apply (relation_pair b b1)
+ | apply relation_pair_equality
+ ]
+qed.
+
+lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+ intros 7 (o1 o2 r r' H c1 f2);
+ split; intro H1;
+ [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
+ lapply (if ?? (H c1 f2) H2) as H3;
+ apply (if ?? (commute ?? r' c1 f2) H3);
+ | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2;
+ lapply (fi ?? (H c1 f2) H2) as H3;
+ apply (if ?? (commute ?? r c1 f2) H3);
+ ]
+qed.
+
+definition id_relation_pair: ∀o:basic_pair. relation_pair o o.
+ intro;
+ constructor 1;
+ [1,2: apply id1;
+ | lapply (id_neutral_right1 ? (concr o) ? (⊩)) as H;
+ lapply (id_neutral_left1 ?? (form o) (⊩)) as H1;
+ apply (.= H);
+ apply (H1 \sup -1);]
+qed.
+
+definition relation_pair_composition:
+ ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+ intros;
+ constructor 1;
+ [ intros (r r1);
+ constructor 1;
+ [ apply (r1 \sub\c ∘ r \sub\c)
+ | apply (r1 \sub\f ∘ r \sub\f)
+ | lapply (commute ?? r) as H;
+ lapply (commute ?? r1) as H1;
+ apply (.= ASSOC1);
+ apply (.= #‡H1);
+ apply (.= ASSOC1\sup -1);
+ apply (.= H‡#);
+ apply ASSOC1]
+ | intros;
+ change with (⊩ ∘ (b\sub\c ∘ a\sub\c) = ⊩ ∘ (b'\sub\c ∘ a'\sub\c));
+ change in H with (⊩ ∘ a \sub\c = ⊩ ∘ a' \sub\c);
+ change in H1 with (⊩ ∘ b \sub\c = ⊩ ∘ b' \sub\c);
+ apply (.= ASSOC1);
+ apply (.= #‡H1);
+ apply (.= #‡(commute ?? b'));
+ apply (.= ASSOC1 \sup -1);
+ apply (.= H‡#);
+ apply (.= ASSOC1);
+ apply (.= #‡(commute ?? b')\sup -1);
+ apply (ASSOC1 \sup -1)]
+qed.
+
+definition BP: category1.
+ constructor 1;
+ [ apply basic_pair
+ | apply relation_pair_setoid
+ | apply id_relation_pair
+ | apply relation_pair_composition
+ | intros;
+ change with (⊩ ∘ (a34\sub\c ∘ (a23\sub\c ∘ a12\sub\c)) =
+ ⊩ ∘ ((a34\sub\c ∘ a23\sub\c) ∘ a12\sub\c));
+ apply (ASSOC1‡#);
+ | intros;
+ change with (⊩ ∘ (a\sub\c ∘ (id_relation_pair o1)\sub\c) = ⊩ ∘ a\sub\c);
+ apply ((id_neutral_right1 ????)‡#);
+ | intros;
+ change with (⊩ ∘ ((id_relation_pair o2)\sub\c ∘ a\sub\c) = ⊩ ∘ a\sub\c);
+ apply ((id_neutral_left1 ????)‡#);]
+qed.
+
+definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
+ intros; constructor 1;
+ [ apply (ext ? ? (rel o));
+ | intros;
+ apply (.= #‡H);
+ apply refl1]
+qed.
+
+definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o) ≝
+ λo.extS ?? (rel o).
+
+definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
+ intros (o); constructor 1;
+ [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
+ intros; simplify; apply (.= (†H)‡#); apply refl1
+ | intros; split; simplify; intros;
+ [ apply (. #‡((†H)‡(†H1))); assumption
+ | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersects" 'fintersects U V = (fun1 ___ (fintersects _) U V).
+
+definition fintersectsS:
+ ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
+ intros (o); constructor 1;
+ [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
+ intros; simplify; apply (.= (†H)‡#); apply refl1
+ | intros; split; simplify; intros;
+ [ apply (. #‡((†H)‡(†H1))); assumption
+ | apply (. #‡((†H\sup -1)‡(†H1\sup -1))); assumption]]
+qed.
+
+interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V).
+
+definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
+ intros (o); constructor 1;
+ [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
+ | intros; split; intros; cases H2; exists [1,3: apply w]
+ [ apply (. (#‡H1)‡(H‡#)); assumption
+ | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]]
+qed.
+
+interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 (concr _) __ (relS _) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "formal_topology/relations.ma".
-include "datatypes/categories.ma".
-include "formal_topology/saturations_reductions.ma".
-
-record basic_topology: Type ≝
- { carrbt:> REL;
- A: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
- J: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
- A_is_saturation: is_saturation ? A;
- J_is_reduction: is_reduction ? J;
- compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
- }.
-
-record continuous_relation (S,T: basic_topology) : Type ≝
- { cont_rel:> arrows1 ? S T;
- reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
- saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)
- }.
-
-definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
- intros (S T); constructor 1;
- [ apply (continuous_relation S T)
- | constructor 1;
- [ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b));
- | simplify; intros; apply refl1;
- | simplify; intros; apply sym1; apply H
- | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
-qed.
-
-definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
-
-coercion cont_rel'.
-
-definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel.
-
-coercion cont_rel''.
-
-theorem continuous_relation_eq':
- ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
- a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).
- intros; split; intro; unfold minus_star_image; simplify; intros;
- [ cut (ext ?? a a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
- lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
- cut (A ? (ext ?? a' a1) ⊆ A ? X); [2: apply (. (H ?)‡#); assumption]
- lapply (fi ?? (A_is_saturation ???) Hcut);
- apply (Hletin1 x); change with (x ∈ ext ?? a' a1); split; simplify;
- [ apply I | assumption ]
- | cut (ext ?? a' a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
- lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
- cut (A ? (ext ?? a a1) ⊆ A ? X); [2: apply (. (H ?)\sup -1‡#); assumption]
- lapply (fi ?? (A_is_saturation ???) Hcut);
- apply (Hletin1 x); change with (x ∈ ext ?? a a1); split; simplify;
- [ apply I | assumption ]]
-qed.
-
-theorem continuous_relation_eq_inv':
- ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
- (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → a=a'.
- intros 6;
- cut (∀a,a': continuous_relation_setoid o1 o2.
- (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) →
- ∀V:o2. A ? (ext ?? a' V) ⊆ A ? (ext ?? a V));
- [2: clear b H a' a; intros;
- lapply depth=0 (λV.saturation_expansive ??? (extS ?? a V)); [2: apply A_is_saturation;|skip]
- (* fundamental adjunction here! to be taken out *)
- cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a (A ? (extS ?? a V)));
- [2: intro; intros 2; unfold minus_star_image; simplify; intros;
- apply (Hletin V1 x); whd; split; [ exact I | exists; [apply a1] split; assumption]]
- clear Hletin;
- cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a' (A ? (extS ?? a V)));
- [2: intro; apply (. #‡(H ?)); apply Hcut] clear H Hcut;
- (* second half of the fundamental adjunction here! to be taken out too *)
- intro; lapply (Hcut1 (singleton ? V)); clear Hcut1;
- unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin;
- whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin;
- apply (if ?? (A_is_saturation ???));
- intros 2 (x H); lapply (Hletin V ? x ?);
- [ apply refl | cases H; assumption; ]
- change with (x ∈ A ? (ext ?? a V));
- apply (. #‡(†(extS_singleton ????)));
- assumption;]
- split; apply Hcut; [2: assumption | intro; apply sym1; apply H]
-qed.
-
-definition continuous_relation_comp:
- ∀o1,o2,o3.
- continuous_relation_setoid o1 o2 →
- continuous_relation_setoid o2 o3 →
- continuous_relation_setoid o1 o3.
- intros (o1 o2 o3 r s); constructor 1;
- [ apply (s ∘ r)
- | intros;
- apply sym1;
- apply (.= †(image_comp ??????));
- apply (.= (reduced ?????)\sup -1);
- [ apply (.= (reduced ?????)); [ assumption | apply refl1 ]
- | apply (.= (image_comp ??????)\sup -1);
- apply refl1]
- | intros;
- apply sym1;
- apply (.= †(minus_star_image_comp ??????));
- apply (.= (saturated ?????)\sup -1);
- [ apply (.= (saturated ?????)); [ assumption | apply refl1 ]
- | apply (.= (minus_star_image_comp ??????)\sup -1);
- apply refl1]]
-qed.
-
-definition BTop: category1.
- constructor 1;
- [ apply basic_topology
- | apply continuous_relation_setoid
- | intro; constructor 1;
- [ apply id1
- | intros;
- apply (.= (image_id ??));
- apply sym1;
- apply (.= †(image_id ??));
- apply sym1;
- assumption
- | intros;
- apply (.= (minus_star_image_id ??));
- apply sym1;
- apply (.= †(minus_star_image_id ??));
- apply sym1;
- assumption]
- | intros; constructor 1;
- [ apply continuous_relation_comp;
- | intros; simplify; intro x; simplify;
- lapply depth=0 (continuous_relation_eq' ???? H) as H';
- lapply depth=0 (continuous_relation_eq' ???? H1) as H1';
- letin K ≝ (λX.H1' (minus_star_image ?? a (A ? X))); clearbody K;
- cut (∀X:Ω \sup o1.
- minus_star_image o2 o3 b (A o2 (minus_star_image o1 o2 a (A o1 X)))
- = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X))));
- [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);]
- clear K H' H1';
- cut (∀X:Ω \sup o1.
- minus_star_image o1 o3 (b ∘ a) (A o1 X) = minus_star_image o1 o3 (b'∘a') (A o1 X));
- [2: intro;
- apply (.= (minus_star_image_comp ??????));
- apply (.= #‡(saturated ?????));
- [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
- apply sym1;
- apply (.= (minus_star_image_comp ??????));
- apply (.= #‡(saturated ?????));
- [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
- apply ((Hcut X) \sup -1)]
- clear Hcut; generalize in match x; clear x;
- apply (continuous_relation_eq_inv');
- apply Hcut1;]
- | intros; simplify; intro; do 2 (unfold continuous_relation_comp); simplify;
- apply (.= †(ASSOC1‡#));
- apply refl1
- | intros; simplify; intro; unfold continuous_relation_comp; simplify;
- apply (.= †((id_neutral_right1 ????)‡#));
- apply refl1
- | intros; simplify; intro; simplify;
- apply (.= †((id_neutral_left1 ????)‡#));
- apply refl1]
-qed.
-
-(*CSC: unused! *)
-(* this proof is more logic-oriented than set/lattice oriented *)
-theorem continuous_relation_eqS:
- ∀o1,o2:basic_topology.∀a,a': continuous_relation_setoid o1 o2.
- a = a' → ∀X. A ? (extS ?? a X) = A ? (extS ?? a' X).
- intros;
- cut (∀a: arrows1 ? o1 ?.∀x. x ∈ extS ?? a X → ∃y:o2.y ∈ X ∧ x ∈ ext ?? a y);
- [2: intros; cases f; clear f; cases H1; exists [apply w] cases x1; split;
- try assumption; split; assumption]
- cut (∀a,a':continuous_relation_setoid o1 o2.eq1 ? a a' → ∀x. x ∈ extS ?? a X → ∃y:o2. y ∈ X ∧ x ∈ A ? (ext ?? a' y));
- [2: intros; cases (Hcut ?? f); exists; [apply w] cases x1; split; try assumption;
- apply (. #‡(H1 ?));
- apply (saturation_expansive ?? (A_is_saturation o1) (ext ?? a1 w) x);
- assumption;] clear Hcut;
- split; apply (if ?? (A_is_saturation ???)); intros 2;
- [lapply (Hcut1 a a' H a1 f) | lapply (Hcut1 a' a (H \sup -1) a1 f)]
- cases Hletin; clear Hletin; cases x; clear x;
- cut (∀a: arrows1 ? o1 ?. ext ?? a w ⊆ extS ?? a X);
- [2,4: intros 3; cases f3; clear f3; simplify in f5; split; try assumption;
- exists [1,3: apply w] split; assumption;]
- cut (∀a. A ? (ext o1 o2 a w) ⊆ A ? (extS o1 o2 a X));
- [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;]
- apply Hcut2; assumption.
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "formal_topology/relations.ma".
+include "datatypes/categories.ma".
+include "formal_topology/saturations_reductions.ma".
+
+record basic_topology: Type ≝
+ { carrbt:> REL;
+ A: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
+ J: unary_morphism (Ω \sup carrbt) (Ω \sup carrbt);
+ A_is_saturation: is_saturation ? A;
+ J_is_reduction: is_reduction ? J;
+ compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
+ }.
+
+record continuous_relation (S,T: basic_topology) : Type ≝
+ { cont_rel:> arrows1 ? S T;
+ reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
+ saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)
+ }.
+
+definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
+ intros (S T); constructor 1;
+ [ apply (continuous_relation S T)
+ | constructor 1;
+ [ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b));
+ | simplify; intros; apply refl1;
+ | simplify; intros; apply sym1; apply H
+ | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
+qed.
+
+definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
+
+coercion cont_rel'.
+
+definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel.
+
+coercion cont_rel''.
+
+theorem continuous_relation_eq':
+ ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
+ a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).
+ intros; split; intro; unfold minus_star_image; simplify; intros;
+ [ cut (ext ?? a a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
+ lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
+ cut (A ? (ext ?? a' a1) ⊆ A ? X); [2: apply (. (H ?)‡#); assumption]
+ lapply (fi ?? (A_is_saturation ???) Hcut);
+ apply (Hletin1 x); change with (x ∈ ext ?? a' a1); split; simplify;
+ [ apply I | assumption ]
+ | cut (ext ?? a' a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
+ lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
+ cut (A ? (ext ?? a a1) ⊆ A ? X); [2: apply (. (H ?)\sup -1‡#); assumption]
+ lapply (fi ?? (A_is_saturation ???) Hcut);
+ apply (Hletin1 x); change with (x ∈ ext ?? a a1); split; simplify;
+ [ apply I | assumption ]]
+qed.
+
+theorem continuous_relation_eq_inv':
+ ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
+ (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → a=a'.
+ intros 6;
+ cut (∀a,a': continuous_relation_setoid o1 o2.
+ (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) →
+ ∀V:o2. A ? (ext ?? a' V) ⊆ A ? (ext ?? a V));
+ [2: clear b H a' a; intros;
+ lapply depth=0 (λV.saturation_expansive ??? (extS ?? a V)); [2: apply A_is_saturation;|skip]
+ (* fundamental adjunction here! to be taken out *)
+ cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a (A ? (extS ?? a V)));
+ [2: intro; intros 2; unfold minus_star_image; simplify; intros;
+ apply (Hletin V1 x); whd; split; [ exact I | exists; [apply a1] split; assumption]]
+ clear Hletin;
+ cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a' (A ? (extS ?? a V)));
+ [2: intro; apply (. #‡(H ?)); apply Hcut] clear H Hcut;
+ (* second half of the fundamental adjunction here! to be taken out too *)
+ intro; lapply (Hcut1 (singleton ? V)); clear Hcut1;
+ unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin;
+ whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin;
+ apply (if ?? (A_is_saturation ???));
+ intros 2 (x H); lapply (Hletin V ? x ?);
+ [ apply refl | cases H; assumption; ]
+ change with (x ∈ A ? (ext ?? a V));
+ apply (. #‡(†(extS_singleton ????)));
+ assumption;]
+ split; apply Hcut; [2: assumption | intro; apply sym1; apply H]
+qed.
+
+definition continuous_relation_comp:
+ ∀o1,o2,o3.
+ continuous_relation_setoid o1 o2 →
+ continuous_relation_setoid o2 o3 →
+ continuous_relation_setoid o1 o3.
+ intros (o1 o2 o3 r s); constructor 1;
+ [ apply (s ∘ r)
+ | intros;
+ apply sym1;
+ apply (.= †(image_comp ??????));
+ apply (.= (reduced ?????)\sup -1);
+ [ apply (.= (reduced ?????)); [ assumption | apply refl1 ]
+ | apply (.= (image_comp ??????)\sup -1);
+ apply refl1]
+ | intros;
+ apply sym1;
+ apply (.= †(minus_star_image_comp ??????));
+ apply (.= (saturated ?????)\sup -1);
+ [ apply (.= (saturated ?????)); [ assumption | apply refl1 ]
+ | apply (.= (minus_star_image_comp ??????)\sup -1);
+ apply refl1]]
+qed.
+
+definition BTop: category1.
+ constructor 1;
+ [ apply basic_topology
+ | apply continuous_relation_setoid
+ | intro; constructor 1;
+ [ apply id1
+ | intros;
+ apply (.= (image_id ??));
+ apply sym1;
+ apply (.= †(image_id ??));
+ apply sym1;
+ assumption
+ | intros;
+ apply (.= (minus_star_image_id ??));
+ apply sym1;
+ apply (.= †(minus_star_image_id ??));
+ apply sym1;
+ assumption]
+ | intros; constructor 1;
+ [ apply continuous_relation_comp;
+ | intros; simplify; intro x; simplify;
+ lapply depth=0 (continuous_relation_eq' ???? H) as H';
+ lapply depth=0 (continuous_relation_eq' ???? H1) as H1';
+ letin K ≝ (λX.H1' (minus_star_image ?? a (A ? X))); clearbody K;
+ cut (∀X:Ω \sup o1.
+ minus_star_image o2 o3 b (A o2 (minus_star_image o1 o2 a (A o1 X)))
+ = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X))));
+ [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);]
+ clear K H' H1';
+ cut (∀X:Ω \sup o1.
+ minus_star_image o1 o3 (b ∘ a) (A o1 X) = minus_star_image o1 o3 (b'∘a') (A o1 X));
+ [2: intro;
+ apply (.= (minus_star_image_comp ??????));
+ apply (.= #‡(saturated ?????));
+ [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
+ apply sym1;
+ apply (.= (minus_star_image_comp ??????));
+ apply (.= #‡(saturated ?????));
+ [ apply ((saturation_idempotent ????) \sup -1); apply A_is_saturation ]
+ apply ((Hcut X) \sup -1)]
+ clear Hcut; generalize in match x; clear x;
+ apply (continuous_relation_eq_inv');
+ apply Hcut1;]
+ | intros; simplify; intro; do 2 (unfold continuous_relation_comp); simplify;
+ apply (.= †(ASSOC1‡#));
+ apply refl1
+ | intros; simplify; intro; unfold continuous_relation_comp; simplify;
+ apply (.= †((id_neutral_right1 ????)‡#));
+ apply refl1
+ | intros; simplify; intro; simplify;
+ apply (.= †((id_neutral_left1 ????)‡#));
+ apply refl1]
+qed.
+
+(*CSC: unused! *)
+(* this proof is more logic-oriented than set/lattice oriented *)
+theorem continuous_relation_eqS:
+ ∀o1,o2:basic_topology.∀a,a': continuous_relation_setoid o1 o2.
+ a = a' → ∀X. A ? (extS ?? a X) = A ? (extS ?? a' X).
+ intros;
+ cut (∀a: arrows1 ? o1 ?.∀x. x ∈ extS ?? a X → ∃y:o2.y ∈ X ∧ x ∈ ext ?? a y);
+ [2: intros; cases f; clear f; cases H1; exists [apply w] cases x1; split;
+ try assumption; split; assumption]
+ cut (∀a,a':continuous_relation_setoid o1 o2.eq1 ? a a' → ∀x. x ∈ extS ?? a X → ∃y:o2. y ∈ X ∧ x ∈ A ? (ext ?? a' y));
+ [2: intros; cases (Hcut ?? f); exists; [apply w] cases x1; split; try assumption;
+ apply (. #‡(H1 ?));
+ apply (saturation_expansive ?? (A_is_saturation o1) (ext ?? a1 w) x);
+ assumption;] clear Hcut;
+ split; apply (if ?? (A_is_saturation ???)); intros 2;
+ [lapply (Hcut1 a a' H a1 f) | lapply (Hcut1 a' a (H \sup -1) a1 f)]
+ cases Hletin; clear Hletin; cases x; clear x;
+ cut (∀a: arrows1 ? o1 ?. ext ?? a w ⊆ extS ?? a X);
+ [2,4: intros 3; cases f3; clear f3; simplify in f5; split; try assumption;
+ exists [1,3: apply w] split; assumption;]
+ cut (∀a. A ? (ext o1 o2 a w) ⊆ A ? (extS o1 o2 a X));
+ [2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;]
+ apply Hcut2; assumption.
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "formal_topology/basic_pairs.ma".
-
-record concrete_space : Type ≝
- { bp:> BP;
- converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
- all_covered: ∀x: concr bp. x ⊩ form bp
- }.
-
-definition bp': concrete_space → basic_pair ≝ λc.bp c.
-
-coercion bp'.
-
-record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
- { rp:> arrows1 ? CS1 CS2;
- respects_converges:
- ∀b,c.
- extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
- BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
- respects_all_covered:
- extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
- }.
-
-definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
- λCS1,CS2,c. rp CS1 CS2 c.
-
-coercion rp'.
-
-definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
- intros;
- constructor 1;
- [ apply (convergent_relation_pair c c1)
- | constructor 1;
- [ intros;
- apply (relation_pair_equality c c1 c2 c3);
- | intros 1; apply refl1;
- | intros 2; apply sym1;
- | intros 3; apply trans1]]
-qed.
-
-definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
- λCS1,CS2,c.rp ?? c.
-
-coercion rp''.
-
-definition convergent_relation_space_composition:
- ∀o1,o2,o3: concrete_space.
- binary_morphism1
- (convergent_relation_space_setoid o1 o2)
- (convergent_relation_space_setoid o2 o3)
- (convergent_relation_space_setoid o1 o3).
- intros; constructor 1;
- [ intros; whd in c c1 ⊢ %;
- constructor 1;
- [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
- | intros;
- change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
- change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
- with (c1 \sub \f ∘ c \sub \f);
- change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
- with (c1 \sub \f ∘ c \sub \f);
- apply (.= (extS_com ??????));
- apply (.= (†(respects_converges ?????)));
- apply (.= (respects_converges ?????));
- apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
- apply refl1;
- | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
- apply (.= (extS_com ??????));
- apply (.= (†(respects_all_covered ???)));
- apply (.= respects_all_covered ???);
- apply refl1]
- | intros;
- change with (b ∘ a = b' ∘ a');
- change in H with (rp'' ?? a = rp'' ?? a');
- change in H1 with (rp'' ?? b = rp ?? b');
- apply (.= (H‡H1));
- apply refl1]
-qed.
-
-definition CSPA: category1.
- constructor 1;
- [ apply concrete_space
- | apply convergent_relation_space_setoid
- | intro; constructor 1;
- [ apply id1
- | intros;
- unfold id; simplify;
- apply (.= (equalset_extS_id_X_X ??));
- apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
- (equalset_extS_id_X_X ??)\sup -1)));
- apply refl1;
- | apply (.= (equalset_extS_id_X_X ??));
- apply refl1]
- | apply convergent_relation_space_composition
- | intros; simplify;
- change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
- apply (.= ASSOC1);
- apply refl1
- | intros; simplify;
- change with (a ∘ id1 ? o1 = a);
- apply (.= id_neutral_right1 ????);
- apply refl1
- | intros; simplify;
- change with (id1 ? o2 ∘ a = a);
- apply (.= id_neutral_left1 ????);
- apply refl1]
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "formal_topology/basic_pairs.ma".
+
+record concrete_space : Type ≝
+ { bp:> BP;
+ converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+ all_covered: ∀x: concr bp. x ⊩ form bp
+ }.
+
+definition bp': concrete_space → basic_pair ≝ λc.bp c.
+
+coercion bp'.
+
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
+ { rp:> arrows1 ? CS1 CS2;
+ respects_converges:
+ ∀b,c.
+ extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
+ BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
+ respects_all_covered:
+ extS ?? rp\sub\c (BPextS CS2 (form CS2)) = BPextS CS1 (form CS1)
+ }.
+
+definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
+ λCS1,CS2,c. rp CS1 CS2 c.
+
+coercion rp'.
+
+definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
+ intros;
+ constructor 1;
+ [ apply (convergent_relation_pair c c1)
+ | constructor 1;
+ [ intros;
+ apply (relation_pair_equality c c1 c2 c3);
+ | intros 1; apply refl1;
+ | intros 2; apply sym1;
+ | intros 3; apply trans1]]
+qed.
+
+definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
+ λCS1,CS2,c.rp ?? c.
+
+coercion rp''.
+
+definition convergent_relation_space_composition:
+ ∀o1,o2,o3: concrete_space.
+ binary_morphism1
+ (convergent_relation_space_setoid o1 o2)
+ (convergent_relation_space_setoid o2 o3)
+ (convergent_relation_space_setoid o1 o3).
+ intros; constructor 1;
+ [ intros; whd in c c1 ⊢ %;
+ constructor 1;
+ [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+ | intros;
+ change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+ change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
+ with (c1 \sub \f ∘ c \sub \f);
+ change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
+ with (c1 \sub \f ∘ c \sub \f);
+ apply (.= (extS_com ??????));
+ apply (.= (†(respects_converges ?????)));
+ apply (.= (respects_converges ?????));
+ apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
+ apply refl1;
+ | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
+ apply (.= (extS_com ??????));
+ apply (.= (†(respects_all_covered ???)));
+ apply (.= respects_all_covered ???);
+ apply refl1]
+ | intros;
+ change with (b ∘ a = b' ∘ a');
+ change in H with (rp'' ?? a = rp'' ?? a');
+ change in H1 with (rp'' ?? b = rp ?? b');
+ apply (.= (H‡H1));
+ apply refl1]
+qed.
+
+definition CSPA: category1.
+ constructor 1;
+ [ apply concrete_space
+ | apply convergent_relation_space_setoid
+ | intro; constructor 1;
+ [ apply id1
+ | intros;
+ unfold id; simplify;
+ apply (.= (equalset_extS_id_X_X ??));
+ apply (.= (†((equalset_extS_id_X_X ??)\sup -1‡
+ (equalset_extS_id_X_X ??)\sup -1)));
+ apply refl1;
+ | apply (.= (equalset_extS_id_X_X ??));
+ apply refl1]
+ | apply convergent_relation_space_composition
+ | intros; simplify;
+ change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
+ apply (.= ASSOC1);
+ apply refl1
+ | intros; simplify;
+ change with (a ∘ id1 ? o1 = a);
+ apply (.= id_neutral_right1 ????);
+ apply refl1
+ | intros; simplify;
+ change with (id1 ? o2 ∘ a = a);
+ apply (.= id_neutral_left1 ????);
+ apply refl1]
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "formal_topology/basic_topologies.ma".
-
-definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
-
-coercion btop_carr.
-
-definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
-
-coercion btop_carr'.
-
-definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
- intros; constructor 1;
- [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
- intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
- split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
- | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
- try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
-qed.
-
-interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
-
-definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
- intros; constructor 1;
- [ apply (λU,V. ↓U ∩ ↓V);
- | intros; apply (.= (†H)‡(†H1)); apply refl1]
-qed.
-
-interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
-
-record formal_topology: Type ≝
- { bt:> BTop;
- converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
- }.
-
-definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
-
-coercion bt'.
-
-definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
- intros; constructor 1;
- [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
- | intros; apply (.= (†H)‡(†H1)); apply refl1]
-qed.
-
-interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
-
-record formal_map (S,T: formal_topology) : Type ≝
- { cr:> continuous_relation_setoid S T;
- C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
- C2: extS ?? cr T = S
- }.
-
-definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
- λFT1,FT2,c. cr FT1 FT2 c.
-
-coercion cr'.
-
-definition formal_map_setoid: formal_topology → formal_topology → setoid1.
- intros (S T); constructor 1;
- [ apply (formal_map S T);
- | constructor 1;
- [ apply (λf,f1: formal_map S T.f=f1);
- | simplify; intros 1; apply refl1
- | simplify; intros 2; apply sym1
- | simplify; intros 3; apply trans1]]
-qed.
-
-definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
- λFT1,FT2,c.cr ?? c.
-
-coercion cr''.
-
-definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
- λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
-
-coercion cr'''.
-
-axiom C1':
- ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
- extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
-
-definition formal_map_composition:
- ∀o1,o2,o3: formal_topology.
- binary_morphism1
- (formal_map_setoid o1 o2)
- (formal_map_setoid o2 o3)
- (formal_map_setoid o1 o3).
- intros; constructor 1;
- [ intros; whd in c c1; constructor 1;
- [ apply (comp1 BTop ??? c c1);
- | intros;
- apply (.= (extS_com ??? c c1 ?));
- apply (.= †(C1 ?????));
- apply (.= (C1' ?????));
- apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
- apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
- apply (.= (extS_singleton ????)‡(extS_singleton ????));
- apply refl1;
- | apply (.= (extS_com ??? c c1 ?));
- apply (.= (†(C2 ???)));
- apply (.= (C2 ???));
- apply refl1;]
- | intros; simplify;
- change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
- apply prop1; assumption]
-qed.
-
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "formal_topology/basic_topologies.ma".
+
+definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
+
+coercion btop_carr.
+
+definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
+
+coercion btop_carr'.
+
+definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
+ intros; constructor 1;
+ [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
+ intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
+ split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
+ | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
+ try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
+qed.
+
+interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).
+
+definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
+ intros; constructor 1;
+ [ apply (λU,V. ↓U ∩ ↓V);
+ | intros; apply (.= (†H)‡(†H1)); apply refl1]
+qed.
+
+interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+
+record formal_topology: Type ≝
+ { bt:> BTop;
+ converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
+ }.
+
+definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
+
+coercion bt'.
+
+definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
+ intros; constructor 1;
+ [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
+ | intros; apply (.= (†H)‡(†H1)); apply refl1]
+qed.
+
+interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
+
+record formal_map (S,T: formal_topology) : Type ≝
+ { cr:> continuous_relation_setoid S T;
+ C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
+ C2: extS ?? cr T = S
+ }.
+
+definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
+ λFT1,FT2,c. cr FT1 FT2 c.
+
+coercion cr'.
+
+definition formal_map_setoid: formal_topology → formal_topology → setoid1.
+ intros (S T); constructor 1;
+ [ apply (formal_map S T);
+ | constructor 1;
+ [ apply (λf,f1: formal_map S T.f=f1);
+ | simplify; intros 1; apply refl1
+ | simplify; intros 2; apply sym1
+ | simplify; intros 3; apply trans1]]
+qed.
+
+definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
+ λFT1,FT2,c.cr ?? c.
+
+coercion cr''.
+
+definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
+ λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
+
+coercion cr'''.
+
+axiom C1':
+ ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
+ extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
+
+definition formal_map_composition:
+ ∀o1,o2,o3: formal_topology.
+ binary_morphism1
+ (formal_map_setoid o1 o2)
+ (formal_map_setoid o2 o3)
+ (formal_map_setoid o1 o3).
+ intros; constructor 1;
+ [ intros; whd in c c1; constructor 1;
+ [ apply (comp1 BTop ??? c c1);
+ | intros;
+ apply (.= (extS_com ??? c c1 ?));
+ apply (.= †(C1 ?????));
+ apply (.= (C1' ?????));
+ apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
+ apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
+ apply (.= (extS_singleton ????)‡(extS_singleton ????));
+ apply refl1;
+ | apply (.= (extS_com ??? c c1 ?));
+ apply (.= (†(C2 ???)));
+ apply (.= (C2 ???));
+ apply refl1;]
+ | intros; simplify;
+ change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
+ apply prop1; assumption]
+qed.
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "datatypes/subsets.ma".
-
-record binary_relation (A,B: setoid) : Type ≝
- { satisfy:> binary_morphism1 A B CPROP }.
-
-notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}.
-notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}.
-interpretation "relation applied" 'satisfy r x y = (fun1 ___ (satisfy __ r) x y).
-
-definition binary_relation_setoid: setoid → setoid → setoid1.
- intros (A B);
- constructor 1;
- [ apply (binary_relation A B)
- | constructor 1;
- [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y)
- | simplify; intros 3; split; intro; assumption
- | simplify; intros 5; split; intro;
- [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption
- | simplify; intros 7; split; intro;
- [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
- [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
- assumption]]
-qed.
-
-definition composition:
- ∀A,B,C.
- binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
- intros;
- constructor 1;
- [ intros (R12 R23);
- constructor 1;
- constructor 1;
- [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
- | intros;
- split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ]
- [ apply (. (H‡#)‡(#‡H1)); assumption
- | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]]
- | intros 8; split; intro H2; simplify in H2 ⊢ %;
- cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3;
- [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
- [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
- exists; try assumption;
- split; assumption]
-qed.
-
-definition REL: category1.
- constructor 1;
- [ apply setoid
- | intros (T T1); apply (binary_relation_setoid T T1)
- | intros; constructor 1;
- constructor 1; unfold setoid1_of_setoid; simplify;
- [ intros; apply (c = c1)
- | intros; split; intro;
- [ apply (trans ????? (H \sup -1));
- apply (trans ????? H2);
- apply H1
- | apply (trans ????? H);
- apply (trans ????? H2);
- apply (H1 \sup -1)]]
- | apply composition
- | intros 9;
- split; intro;
- cases f (w H); clear f; cases H; clear H;
- [cases f (w1 H); clear f | cases f1 (w1 H); clear f1]
- cases H; clear H;
- exists; try assumption;
- split; try assumption;
- exists; try assumption;
- split; assumption
- |6,7: intros 5; unfold composition; simplify; split; intro;
- unfold setoid1_of_setoid in x y; simplify in x y;
- [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
- [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption
- | apply (. #‡(H : eq1 ? w y)); assumption]
- |2,4: exists; try assumption; split; first [apply refl | assumption]]]
-qed.
-
-definition full_subset: ∀s:REL. Ω \sup s.
- apply (λs.{x | True});
- intros; simplify; split; intro; assumption.
-qed.
-
-coercion full_subset.
-
-definition setoid1_of_REL: REL → setoid ≝ λS. S.
-
-coercion setoid1_of_REL.
-
-definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
- intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
-qed.
-
-interpretation "subset comprehension" 'comprehension s p =
- (comprehension s (mk_unary_morphism __ p _)).
-
-definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
- apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
- [ intros; simplify; apply (.= (H‡#)); apply refl1
- | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
- [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
- | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
-qed.
-
-definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
- (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
- intros (X S r); constructor 1;
- [ intro F; constructor 1; constructor 1;
- [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
- | intros; split; intro; cases f (H1 H2); clear f; split;
- [ apply (. (H‡#)); assumption
- |3: apply (. (H\sup -1‡#)); assumption
- |2,4: cases H2 (w H3); exists; [1,3: apply w]
- [ apply (. (#‡(H‡#))); assumption
- | apply (. (#‡(H \sup -1‡#))); assumption]]]
- | intros; split; simplify; intros; cases f; cases H1; split;
- [1,3: assumption
- |2,4: exists; [1,3: apply w]
- [ apply (. (#‡H)‡#); assumption
- | apply (. (#‡H\sup -1)‡#); assumption]]]
-qed.
-
-lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
- intros;
- unfold extS; simplify;
- split; simplify;
- [ intros 2; change with (a ∈ X);
- cases f; clear f;
- cases H; clear H;
- cases x; clear x;
- change in f2 with (eq1 ? a w);
- apply (. (f2\sup -1‡#));
- assumption
- | intros 2; change in f with (a ∈ X);
- split;
- [ whd; exact I
- | exists; [ apply a ]
- split;
- [ assumption
- | change with (a = a); apply refl]]]
-qed.
-
-lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (extS o2 o3 c2 S).
- intros; unfold extS; simplify; split; intros; simplify; intros;
- [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
- cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
- exists; [apply w1] split [2: assumption] constructor 1; [assumption]
- exists; [apply w] split; assumption
- | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
- cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
- cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
- assumption]
-qed.
-
-(* the same as ⋄ for a basic pair *)
-definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
- intros; constructor 1;
- [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
- intros; simplify; split; intro; cases H1; exists [1,3: apply w]
- [ apply (. (#‡H)‡#); assumption
- | apply (. (#‡H \sup -1)‡#); assumption]
- | intros; split; simplify; intros; cases H2; exists [1,3: apply w]
- [ apply (. #‡(#‡H1)); cases x; split; try assumption;
- apply (if ?? (H ??)); assumption
- | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption;
- apply (if ?? (H \sup -1 ??)); assumption]]
-qed.
-
-(* the same as □ for a basic pair *)
-definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
- intros; constructor 1;
- [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
- intros; simplify; split; intros; apply H1;
- [ apply (. #‡H \sup -1); assumption
- | apply (. #‡H); assumption]
- | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)]
- apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption]
-qed.
-
-(* minus_image is the same as ext *)
-
-theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
- intros; unfold image; simplify; split; simplify; intros;
- [ change with (a ∈ U);
- cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption
- | change in f with (a ∈ U);
- exists; [apply a] split; [ change with (a = a); apply refl | assumption]]
-qed.
-
-theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U.
- intros; unfold minus_star_image; simplify; split; simplify; intros;
- [ change with (a ∈ U); apply H; change with (a=a); apply refl
- | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f]
-qed.
-
-theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X).
- intros; unfold image; simplify; split; simplify; intros; cases H; clear H; cases x;
- clear x; [ cases f; clear f; | cases f1; clear f1 ]
- exists; try assumption; cases x; clear x; split; try assumption;
- exists; try assumption; split; assumption.
-qed.
-
-theorem minus_star_image_comp:
- ∀A,B,C,r,s,X.
- minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X).
- intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros;
- [ apply H; exists; try assumption; split; assumption
- | change with (x ∈ X); cases f; cases x1; apply H; assumption]
-qed.
-
-(*CSC: unused! *)
-theorem ext_comp:
- ∀o1,o2,o3: REL.
- ∀a: arrows1 ? o1 o2.
- ∀b: arrows1 ? o2 o3.
- ∀x. ext ?? (b∘a) x = extS ?? a (ext ?? b x).
- intros;
- unfold ext; unfold extS; simplify; split; intro; simplify; intros;
- cases f; clear f; split; try assumption;
- [ cases f2; clear f2; cases x1; clear x1; exists; [apply w] split;
- [1: split] assumption;
- | cases H; clear H; cases x1; clear x1; exists [apply w]; split;
- [2: cases f] assumption]
-qed.
-
-theorem extS_singleton:
- ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x.
- intros; unfold extS; unfold ext; unfold singleton; simplify;
- split; intros 2; simplify; cases f; split; try assumption;
- [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1);
- assumption
- | exists; try assumption; split; try assumption; change with (x = x); apply refl]
-qed.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "datatypes/subsets.ma".
+
+record binary_relation (A,B: setoid) : Type ≝
+ { satisfy:> binary_morphism1 A B CPROP }.
+
+notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}.
+notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}.
+interpretation "relation applied" 'satisfy r x y = (fun1 ___ (satisfy __ r) x y).
+
+definition binary_relation_setoid: setoid → setoid → setoid1.
+ intros (A B);
+ constructor 1;
+ [ apply (binary_relation A B)
+ | constructor 1;
+ [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y)
+ | simplify; intros 3; split; intro; assumption
+ | simplify; intros 5; split; intro;
+ [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption
+ | simplify; intros 7; split; intro;
+ [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
+ [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
+ assumption]]
+qed.
+
+definition composition:
+ ∀A,B,C.
+ binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
+ intros;
+ constructor 1;
+ [ intros (R12 R23);
+ constructor 1;
+ constructor 1;
+ [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
+ | intros;
+ split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ]
+ [ apply (. (H‡#)‡(#‡H1)); assumption
+ | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]]
+ | intros 8; split; intro H2; simplify in H2 ⊢ %;
+ cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); clear H3;
+ [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
+ [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
+ exists; try assumption;
+ split; assumption]
+qed.
+
+definition REL: category1.
+ constructor 1;
+ [ apply setoid
+ | intros (T T1); apply (binary_relation_setoid T T1)
+ | intros; constructor 1;
+ constructor 1; unfold setoid1_of_setoid; simplify;
+ [ intros; apply (c = c1)
+ | intros; split; intro;
+ [ apply (trans ????? (H \sup -1));
+ apply (trans ????? H2);
+ apply H1
+ | apply (trans ????? H);
+ apply (trans ????? H2);
+ apply (H1 \sup -1)]]
+ | apply composition
+ | intros 9;
+ split; intro;
+ cases f (w H); clear f; cases H; clear H;
+ [cases f (w1 H); clear f | cases f1 (w1 H); clear f1]
+ cases H; clear H;
+ exists; try assumption;
+ split; try assumption;
+ exists; try assumption;
+ split; assumption
+ |6,7: intros 5; unfold composition; simplify; split; intro;
+ unfold setoid1_of_setoid in x y; simplify in x y;
+ [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
+ [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption
+ | apply (. #‡(H : eq1 ? w y)); assumption]
+ |2,4: exists; try assumption; split; first [apply refl | assumption]]]
+qed.
+
+definition full_subset: ∀s:REL. Ω \sup s.
+ apply (λs.{x | True});
+ intros; simplify; split; intro; assumption.
+qed.
+
+coercion full_subset.
+
+definition setoid1_of_REL: REL → setoid ≝ λS. S.
+
+coercion setoid1_of_REL.
+
+definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
+ apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
+ intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
+qed.
+
+interpretation "subset comprehension" 'comprehension s p =
+ (comprehension s (mk_unary_morphism __ p _)).
+
+definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
+ apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 ? X S.λf:S.{x ∈ X | x ♮r f}) ?);
+ [ intros; simplify; apply (.= (H‡#)); apply refl1
+ | intros; simplify; split; intros; simplify; intros; cases f; split; try assumption;
+ [ apply (. (#‡H1)); whd in H; apply (if ?? (H ??)); assumption
+ | apply (. (#‡H1\sup -1)); whd in H; apply (fi ?? (H ??));assumption]]
+qed.
+
+definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
+ (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
+ intros (X S r); constructor 1;
+ [ intro F; constructor 1; constructor 1;
+ [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
+ | intros; split; intro; cases f (H1 H2); clear f; split;
+ [ apply (. (H‡#)); assumption
+ |3: apply (. (H\sup -1‡#)); assumption
+ |2,4: cases H2 (w H3); exists; [1,3: apply w]
+ [ apply (. (#‡(H‡#))); assumption
+ | apply (. (#‡(H \sup -1‡#))); assumption]]]
+ | intros; split; simplify; intros; cases f; cases H1; split;
+ [1,3: assumption
+ |2,4: exists; [1,3: apply w]
+ [ apply (. (#‡H)‡#); assumption
+ | apply (. (#‡H\sup -1)‡#); assumption]]]
+qed.
+
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
+ intros;
+ unfold extS; simplify;
+ split; simplify;
+ [ intros 2; change with (a ∈ X);
+ cases f; clear f;
+ cases H; clear H;
+ cases x; clear x;
+ change in f2 with (eq1 ? a w);
+ apply (. (f2\sup -1‡#));
+ assumption
+ | intros 2; change in f with (a ∈ X);
+ split;
+ [ whd; exact I
+ | exists; [ apply a ]
+ split;
+ [ assumption
+ | change with (a = a); apply refl]]]
+qed.
+
+lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c2 ∘ c1) S = extS o1 o2 c1 (extS o2 o3 c2 S).
+ intros; unfold extS; simplify; split; intros; simplify; intros;
+ [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+ cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
+ exists; [apply w1] split [2: assumption] constructor 1; [assumption]
+ exists; [apply w] split; assumption
+ | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+ cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
+ cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
+ assumption]
+qed.
+
+(* the same as ⋄ for a basic pair *)
+definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
+ intros; constructor 1;
+ [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
+ intros; simplify; split; intro; cases H1; exists [1,3: apply w]
+ [ apply (. (#‡H)‡#); assumption
+ | apply (. (#‡H \sup -1)‡#); assumption]
+ | intros; split; simplify; intros; cases H2; exists [1,3: apply w]
+ [ apply (. #‡(#‡H1)); cases x; split; try assumption;
+ apply (if ?? (H ??)); assumption
+ | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption;
+ apply (if ?? (H \sup -1 ??)); assumption]]
+qed.
+
+(* the same as □ for a basic pair *)
+definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
+ intros; constructor 1;
+ [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
+ intros; simplify; split; intros; apply H1;
+ [ apply (. #‡H \sup -1); assumption
+ | apply (. #‡H); assumption]
+ | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)]
+ apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption]
+qed.
+
+(* minus_image is the same as ext *)
+
+theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
+ intros; unfold image; simplify; split; simplify; intros;
+ [ change with (a ∈ U);
+ cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption
+ | change in f with (a ∈ U);
+ exists; [apply a] split; [ change with (a = a); apply refl | assumption]]
+qed.
+
+theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U.
+ intros; unfold minus_star_image; simplify; split; simplify; intros;
+ [ change with (a ∈ U); apply H; change with (a=a); apply refl
+ | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f]
+qed.
+
+theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X).
+ intros; unfold image; simplify; split; simplify; intros; cases H; clear H; cases x;
+ clear x; [ cases f; clear f; | cases f1; clear f1 ]
+ exists; try assumption; cases x; clear x; split; try assumption;
+ exists; try assumption; split; assumption.
+qed.
+
+theorem minus_star_image_comp:
+ ∀A,B,C,r,s,X.
+ minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X).
+ intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros;
+ [ apply H; exists; try assumption; split; assumption
+ | change with (x ∈ X); cases f; cases x1; apply H; assumption]
+qed.
+
+(*CSC: unused! *)
+theorem ext_comp:
+ ∀o1,o2,o3: REL.
+ ∀a: arrows1 ? o1 o2.
+ ∀b: arrows1 ? o2 o3.
+ ∀x. ext ?? (b∘a) x = extS ?? a (ext ?? b x).
+ intros;
+ unfold ext; unfold extS; simplify; split; intro; simplify; intros;
+ cases f; clear f; split; try assumption;
+ [ cases f2; clear f2; cases x1; clear x1; exists; [apply w] split;
+ [1: split] assumption;
+ | cases H; clear H; cases x1; clear x1; exists [apply w]; split;
+ [2: cases f] assumption]
+qed.
+
+theorem extS_singleton:
+ ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x.
+ intros; unfold extS; unfold ext; unfold singleton; simplify;
+ split; intros 2; simplify; cases f; split; try assumption;
+ [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1);
+ assumption
+ | exists; try assumption; split; try assumption; change with (x = x); apply refl]
+qed.
\ No newline at end of file
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "datatypes/subsets.ma".
-include "formal_topology/relations.ma".
-
-definition is_saturation ≝
- λC:REL.λA:unary_morphism (Ω \sup C) (Ω \sup C).
- ∀U,V. (U ⊆ A V) = (A U ⊆ A V).
-
-definition is_reduction ≝
- λC:REL.λJ:unary_morphism (Ω \sup C) (Ω \sup C).
- ∀U,V. (J U ⊆ V) = (J U ⊆ J V).
-
-theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U.
- intros; apply (fi ?? (H ??)); apply subseteq_refl.
-qed.
-
-theorem saturation_monotone:
- ∀C,A. is_saturation C A →
- ∀U,V. U ⊆ V → A U ⊆ A V.
- intros; apply (if ?? (H ??)); apply subseteq_trans; [apply V|3: apply saturation_expansive ]
- assumption.
-qed.
-
-theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. A (A U) = A U.
- intros; split;
- [ apply (if ?? (H ??)); apply subseteq_refl
- | apply saturation_expansive; assumption]
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "datatypes/subsets.ma".
+include "formal_topology/relations.ma".
+
+definition is_saturation ≝
+ λC:REL.λA:unary_morphism (Ω \sup C) (Ω \sup C).
+ ∀U,V. (U ⊆ A V) = (A U ⊆ A V).
+
+definition is_reduction ≝
+ λC:REL.λJ:unary_morphism (Ω \sup C) (Ω \sup C).
+ ∀U,V. (J U ⊆ V) = (J U ⊆ J V).
+
+theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U.
+ intros; apply (fi ?? (H ??)); apply subseteq_refl.
+qed.
+
+theorem saturation_monotone:
+ ∀C,A. is_saturation C A →
+ ∀U,V. U ⊆ V → A U ⊆ A V.
+ intros; apply (if ?? (H ??)); apply subseteq_trans; [apply V|3: apply saturation_expansive ]
+ assumption.
+qed.
+
+theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. A (A U) = A U.
+ intros; split;
+ [ apply (if ?? (H ??)); apply subseteq_refl
+ | apply saturation_expansive; assumption]
+qed.
(*CSC: the URI must disappear: there is a bug now *)
interpretation "leibnitz's equality"
- 'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
+ 'eq t x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "leibnitz's non-equality"
- 'neq x y = (cic:/matita/logic/connectives/Not.con
- (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)).
+ 'neq t x y = (cic:/matita/logic/connectives/Not.con
+ (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y)).
theorem eq_rect':
\forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type.
let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
(distance < 4.)
+let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML"
let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
let href_ds = Gdome.domString "href"
+let maction_ds = Gdome.domString "maction"
let xref_ds = Gdome.domString "xref"
let domImpl = Gdome.domImplementation ()
else
None
+let rec has_maction (elt :Gdome.element) =
+ (* fix this comparison *)
+ if elt#get_tagName#to_string = "m:maction" then
+ true
+ else
+ match elt#get_parentNode with
+ | Some node when node#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE ->
+ has_maction (new Gdome.element_of_node node)
+ | _ -> false
+;;
+
class clickableMathView obj =
let text_width = 80 in
object (self)
method private cic_info = _cic_info
val normal_cursor = Gdk.Cursor.create `LEFT_PTR
- val href_cursor = Gdk.Cursor.create `HAND1
+ val href_cursor = Gdk.Cursor.create `HAND2
+ val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW
initializer
self#set_font_size !current_font_size;
button_press_y <- GdkEvent.Button.y gdk_button;
selection_changed <- false
end else if button = right_button then
- self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
+ self#popup_contextual_menu
+ (self#get_element_at
+ (int_of_float (GdkEvent.Button.x gdk_button))
+ (int_of_float (GdkEvent.Button.y gdk_button)))
+ (GdkEvent.Button.time gdk_button);
false
method private element_over_cb (elt_opt, _, _, _) =
in
match elt_opt with
| Some elt ->
+ if has_maction elt then
+ Gdk.Window.set_cursor (win ()) maction_cursor
+ else
(match hrefs_of_elt elt with
| Some ((_ :: _) as hrefs) ->
Gdk.Window.set_cursor (win ()) href_cursor;
| [] -> assert false (* this method is invoked only if there's a sel. *)
| node :: _ -> self#tactic_text_pattern_of_node node
- method private popup_contextual_menu time =
+ method private popup_contextual_menu element time =
let menu = GMenu.menu () in
let add_menu_item ?(menu = menu) ?stock ?label () =
GMenu.image_menu_item ?stock ?label ~packing:menu#append () in
let check = add_menu_item ~label:"Check" () in
let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in
let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in
+ let hyperlinks_menu_item = GMenu.menu_item ~label:"Hyperlinks" () in
menu#append reductions_menu_item;
menu#append tactics_menu_item;
+ menu#append hyperlinks_menu_item;
let reductions = GMenu.menu () in
let tactics = GMenu.menu () in
+ let hyperlinks = GMenu.menu () in
reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
+ hyperlinks_menu_item#set_submenu hyperlinks;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
+ (match element with
+ | None -> hyperlinks_menu_item#misc#set_sensitive false
+ | Some elt ->
+ match hrefs_of_elt elt, href_callback with
+ | Some l, Some f ->
+ List.iter
+ (fun h ->
+ let item = add_menu_item ~menu:hyperlinks ~label:h () in
+ connect_menu_item item (fun () -> f h)) l
+ | _ -> hyperlinks_menu_item#misc#set_sensitive false);
menu#append (GMenu.separator_item ());
let copy = add_menu_item ~stock:`COPY () in
let gui = get_gui () in
(match self#get_element_at x y with
| None -> ()
| Some elt ->
+ if has_maction elt then ignore(self#action_toggle elt) else
(match hrefs_of_elt elt with
| Some hrefs -> self#invoke_href_callback hrefs gdk_button
- | None -> ignore (self#action_toggle elt)))
+ | None -> ()))
end;
false
projects / helm.git / commitdiff