- formal_topology: compilation of categories.ma continues ...
- grafiteEngine.ml: coercions to sorts can now be defined with the short
syntax
let ty = NCicTypeChecker.typeof status [] [] [] t in
let source, target =
let clean = function
- | NCic.Appl (NCic.Const _ as r :: l) ->
- NotationPt.Appl (NotationPt.NCic r ::
- List.map (fun _ -> NotationPt.Implicit `JustOne)l)
- | NCic.Const _ as r -> NotationPt.NCic r
- | _ -> assert false in
+ | NCic.Appl (NCic.Const _ as r :: l) ->
+ NotationPt.Appl (NotationPt.NCic r ::
+ List.map (fun _ -> NotationPt.Implicit `JustOne)l)
+ | NCic.Const _ as r -> NotationPt.NCic r
+ | NCic.Sort _ as r -> NotationPt.NCic r (* FG: missing case *)
+ | _ -> assert false
+ in
let rec aux = function
- | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
- | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
- | _ -> assert false in aux ty in
- status, o_t, NotationPt.NCic ty, source, target in
+ | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
+ | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
+ | _ -> assert false
+ in
+ aux ty
+ in
+ status, o_t, NotationPt.NCic ty, source, target
+ in
let status, composites =
NCicCoercDeclaration.eval_ncoercion status name compose t ty source
- target in
+ target
+ in
let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
eval_alias status (mode,aliases)
pr3/fwd pr3_gen_abst
pr3/fwd pr3_gen_lref
pr3/fwd pr3_gen_void
-pr3/fwd pr3_gen_abbr
pr3/fwd pr3_gen_appl
pr3/fwd pr3_gen_bind
pr3/iso pr3_iso_appls_abbr
pr3/props pr3_head_21
pr3/props pr3_head_12
pr3/props pr3_flat
-pr3/props pr3_pr3_pr3_t
pr3/props pr3_eta
pr3/subst1 pr3_subst1
pr3/subst1 pr3_gen_cabbr
-pr3/wcpr0 pr3_wcpr0_t
sn3/props sn3_cpr3_trans
sn3/props sn3_shift
@(cprs_trans … IHV1) -IHV1 /2 width=1/
qed.
-(* Basic_1: was only: pr3_pr2_pr3_t *)
+(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
--- /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 "Basic_2/computation/cprs_cprs.ma".
+include "Basic_2/computation/lcprs_lcprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties exploiting context-senstive computation on local environments *)
+
+(* Basic_1: was just: pr3_pr3_pr3_t *)
+lemma lcprs_cprs_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was pr3_gen_abbr *)
+lemma cprs_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡* U2 →
+ (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
+ U2 = ⓓV2. T2
+ ) ∨
+ ∃∃U. ⇧[0, 1] U2 ≡ U & L. ⓓV1 ⊢ T1 ➡* U.
+#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpr_inv_abbr1 … HU02) -HU02 *
+ [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct
+ lapply (cpr_intro … HV0 … HV2) -HV2 #HV02
+ lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02
+ lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/
+ | -V0 #T2 #HT20 #HTU2
+ elim (lift_total U2 0 1) #U0 #HU20
+ lapply (cpr_lift (L.ⓓV1) … HT20 … HU20 HTU2) -T2 /2 width=1/ /4 width=5/
+ ]
+| #U1 #HU01 #HTU1
+ elim (lift_total U2 0 1) #U #HU2
+ lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=5/
+]
+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 "Basic_2/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
+
+definition lcprs: relation lenv ≝ TC … lcpr.
+
+interpretation
+ "context-sensitive parallel computation (environment)"
+ 'CPRedStar L1 L2 = (lcprs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lcprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → R L → R L2) →
+ ∀L2. L1 ⊢ ➡* L2 → R L2.
+#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lcprs_refl: ∀L. L ⊢ ➡* L.
+/2 width=1/ qed.
+
+lemma lcprs_strap1: ∀L1,L,L2.
+ L1 ⊢ ➡* L → L ⊢ ➡ L2 → L1 ⊢ ➡* L2.
+/2 width=3/ qed.
+
+lemma lcprs_strap2: ∀L1,L,L2.
+ L1 ⊢ ➡ L → L ⊢ ➡* L2 → L1 ⊢ ➡* L2.
+/2 width=3/ 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 "Basic_2/reducibility/lcpr_cpr.ma".
+include "Basic_2/computation/cprs.ma".
+include "Basic_2/computation/lcprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
+
+(* Advanced properties ******************************************************)
+
+lemma lcprs_pair_dx: ∀I,L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
+ L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2.
+#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2
+/3 width=1/ /3 width=5/
+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 "Basic_2/computation/lcprs_cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
+
+(* Main properties **********************************************************)
+
+theorem lcprs_trans: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ➡* L2.
+/2 width=3/ qed.
+
+lemma lcprs_pair: ∀L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
+ ∀I. L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2.
+#L1 #L2 #H @(lcprs_ind … H) -L2 /2 width=1/
+#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I
+@(lcprs_trans … (L.ⓑ{I}V1)) /2 width=1/
+qed.
| Flat2: flat2 → item2 (* non-binding item *)
.
-coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind2 on _I:bind2 to item2.
+coercion Bind2.
-coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat2 on _I:flat2 to item2.
+coercion Flat2.
(* Basic properties *********************************************************)
non associative with precedence 45
for @{ 'PConv $L $T1 $T2 }.
-(* Congruence ***************************************************************)
+(* Equivalence **************************************************************)
notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )"
non associative with precedence 45
etc/ld_%_sum.tbl: MAS = $(shell find $* -name "*.ma")
+%.tbl: V1 = $(shell ls $(MAS) | wc -l)
%.tbl: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l)
%.tbl: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l)
%.tbl: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l)
@printf ' class "grey" [ "category"\n' >> $@
@printf ' [ "objects" * ]\n' >> $@
@printf ' ]\n' >> $@
+ @printf ' class "cyan" [ "volume"\n' >> $@
+ @printf ' [ "files" "$(V1)" * ]\n' >> $@
+ @printf ' [ 4 ]\n' >> $@
+ @printf ' ]\n' >> $@
@printf ' class "green" [ "propositions"\n' >> $@
@printf ' [ "theorems" "$(P1)" * ]\n' >> $@
@printf ' [ "lemmas" "$(P2)" * ]\n' >> $@
notation > "B ⇒_2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
notation > "B ⇒_2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
-notation "A × term 74 B ⇒ term 19 C" non associative with precedence 72 for @{'binary_morphism0 $A $B $C}.
notation "A × term 74 B ⇒\sub 1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
[ @CProp[0]
| @mk_equivalence_relation1
[ @Iff
- | #H1 @mk_Iff #H3 #H5 assumption
- | #H7 #H8 #i cases i #H14 #H15 @mk_Iff assumption
- | #H17 #H18 #H19 #i1 #i cases i cases i1 #f #f1 #f2 #f3 @mk_Iff
- [ #x1 @(f2 (f x1)) | #z1 @(f1 (f3 z1))]]]
+ | #x @mk_Iff #x1 assumption
+ | #x #y #i cases i #f #f1 @mk_Iff assumption
+ | #x #y #z #i1 #i cases i cases i1 #f #f1 #f2 #f3 @mk_Iff #x1
+ [ @(f2 (f x1)) | @(f1 (f3 x1))]]]
qed.
definition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
alias symbol "eq" = "setoid1 eq".
definition fi': ∀A,B:CPROP. A = B → B → A.
- intros; @(fi ?? e); assumption.
+ #A #B #e #b @(fi ?? e) assumption.
qed.
notation ". r" with precedence 50 for @{'fi $r}.
interpretation "fi" 'fi r = (fi' ?? r).
definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
- constructor 1;
+ @mk_binary_morphism1
[ @And
- | intros; split; intro; cases a1; split;
+ | #a #a' #b #b' #e #e1 @mk_Iff #a1 cases a1 #a2 #b1 @Conj
[ @(if ?? e a2)
| @(if ?? e1 b1)
| @(fi ?? e a2)
interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).
definition or_morphism: binary_morphism1 CPROP CPROP CPROP.
- constructor 1;
+ @mk_binary_morphism1
[ @Or
- | intros; split; intro; cases o; [1,3:left |2,4: right]
+ | #a #a' #b #b' #e #e1 @mk_Iff #o cases o #a1 [1,3: @Left |2,4: @Right]
[ @(if ?? e a1)
| @(fi ?? e a1)
- | @(if ?? e1 b1)
- | @(fi ?? e1 b1)]]
+ | @(if ?? e1 a1)
+ | @(fi ?? e1 a1)]]
qed.
interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).
definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
- constructor 1;
+ @mk_binary_morphism1
[ @(λA,B. A → B)
- | intros; split; intros;
- [ @(if ?? e1); @f; @(fi ?? e); assumption
- | @(fi ?? e1); @f; @(if ?? e); assumption]]
+ | #a #a' #b #b' #e #e1 @mk_Iff #f #a1
+ [ @(if ?? e1) @f @(fi ?? e) assumption
+ | @(fi ?? e1) @f @(if ?? e) assumption]]
qed.
-
+(*
notation > "hvbox(a break ∘ b)" left associative with precedence 55 for @{ comp ??? $a $b }.
+*)
record category : Type[1] ≝ {
objs:> Type[0];
arrows: objs → objs → setoid;
id: ∀o:objs. arrows o o;
comp: ∀o1,o2,o3. (arrows o1 o2) × (arrows o2 o3) ⇒ (arrows o1 o3);
comp_assoc: ∀o1,o2,o3,o4.∀a12:arrows o1 ?.∀a23:arrows o2 ?.∀a34:arrows o3 o4.
- (a12 ∘ a23) ∘ a34 =_0 a12 ∘ (a23 ∘ a34);
- id_neutral_left : ∀o1,o2. ∀a: arrows o1 o2. (id o1) ∘ a =_0 a;
- id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. a ∘ (id o2) =_0 a
+ comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 =_0 comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
+ id_neutral_left : ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a =_0 a;
+ id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) =_0 a
}.
+(*
notation "hvbox(a break ∘ b)" left associative with precedence 55 for @{ 'compose $a $b }.
-
+*)
record category1 : Type[2] ≝
{ objs1:> Type[1];
arrows1: objs1 → objs1 → setoid1;
interpretation "category assoc" 'assoc = (comp_assoc ????????).
definition category2_of_category1: category1 → category2.
- intro;
- constructor 1;
- [ @(objs1 c);
- | intros; @(setoid2_of_setoid1 (arrows1 c o o1));
- | @(id1 c);
- | intros;
- constructor 1;
- [ intros; @(comp1 c o1 o2 o3 c1 c2);
- | intros; unfold setoid2_of_setoid1 in e e1 a a' b b'; simplify in e e1 a a' b b';
- change with ((b∘a) =_1 (b'∘a')); @(e‡e1); ]
- | intros; simplify; whd in a12 a23 a34; whd; @rule (ASSOC);
- | intros; simplify; whd in a; whd; @id_neutral_right1;
- | intros; simplify; whd in a; whd; @id_neutral_left1; ]
+ #c
+ @mk_category2
+ [ @(objs1 c)
+ | #o #o1 @(setoid2_of_setoid1 (arrows1 c o o1))
+ | @(id1 c)
+ | #o1 #o2 #o3
+ @mk_binary_morphism2
+ [ #c1 #c2 @(comp1 c o1 o2 o3 c1 c2)
+ | #a #a' #b #b' #e #e1 @(e‡e1) ]
+ | #o1 #o2 #o3 #o4 #a12 #a23 #a34 @comp_assoc1
+ | #o1 #o2 #a @id_neutral_right1
+ | #o1 #o2 #a @id_neutral_left1 ]
qed.
(*coercion category2_of_category1.*)
interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
definition functor2_setoid: category2 → category2 → setoid3.
- intros (C1 C2);
- constructor 1;
- [ @(functor2 C1 C2);
- | constructor 1;
- [ intros (f g);
+ #C1 #C2
+ @mk_setoid3
+ [ @(functor2 C1 C2)
+ | @mk_equivalence_relation3
+ [ #f #g
@(∀c:C1. cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? (f c) (g c));
| simplify; intros; @cic:/matita/logic/equality/eq.ind#xpointer(1/1/1);
| simplify; intros; @cic:/matita/logic/equality/sym_eq.con; @H;
projects / helm.git / commitdiff