From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 18:19:39 +0000 (+0000) Subject: Dummy dependent types are no longer cleaned in inductive type arities. X-Git-Tag: make_still_working~5165 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=76ccef4bc06a1cc4634c9261d65e2462a016ecde;p=helm.git Dummy dependent types are no longer cleaned in inductive type arities. --- diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma index b57d3b2fd..8613d83e2 100644 --- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma +++ b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma @@ -187,8 +187,8 @@ lemma part_function_plus_strext : \forall G:CSemiGroup. \forall F,F': PartFunct \to x \neq y. intros (G F F' x y Hx Hy H). elim (bin_op_strext_unfolded ? ? ? ? ? ? H)[ -apply pfstrx[apply F|elim Hx.apply t|elim Hy.apply t|exact H1]| -apply pfstrx[apply F'|elim Hx.apply t1|elim Hy.apply t1|exact H1]] +apply pfstrx[apply F|elim Hx.apply a|elim Hy.apply a|exact H1]| +apply pfstrx[apply F'|elim Hx.apply b|elim Hy.apply b|exact H1]] qed. definition Fplus : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma index 67f8ac1d6..9fb4073ba 100644 --- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma +++ b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma @@ -421,7 +421,7 @@ unfold Not. intro. unfold in H. apply False_ind. -apply H1.apply t. +apply H1.apply a. exact H2|exact H2] ] qed. @@ -677,7 +677,7 @@ lemma conj_wd : \forall S:CSetoid. \forall P,Q : S \to Type. unfold pred_wd. unfold conjP. intros.elim c. - split [ apply (f x ? t).assumption|apply (f1 x ? t1). assumption] + split [ apply (f x ? a).assumption|apply (f1 x ? b). assumption] qed. (* End Conjunction. *) @@ -754,7 +754,7 @@ lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop. intros. elim e. apply (existT).assumption. -apply (t1 t). +apply (b a). qed. (* @@ -827,7 +827,7 @@ intros (S P R H H0). unfold. intros (x y H1 H2). elim H1;split[apply (H x).assumption. exact H2| - intro H5.apply (H0 x ? t)[apply H2|apply t1] + intro H5.apply (H0 x ? a)[apply H2|apply b] ] qed. @@ -1272,8 +1272,8 @@ lemma Inv_bij : \forall A, B:CSetoid. bijective ? ? (inverse A B f). intros; elim f 2; - elim c2 0; - elim c3 0; + elim c 0; + elim c1 0; simplify; intros; split; diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index 4c51d3a44..35f3b0920 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -86,8 +86,8 @@ definition Arguments := nelistT Argument_Class. definition function_type_of_morphism_signature : Arguments → Relation_Class → Type. intros (In Out); elim In; - [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out) - | exact (carrier_of_relation_class ? t → T) + [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out) + | exact (carrier_of_relation_class ? a → T) ] qed. @@ -99,24 +99,24 @@ definition make_compatibility_goal_aux: generalize in match f; clear f; [ elim a; simplify in f f1; [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) - | cases t; + | cases x; [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2)) ] | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) - | cases t; + | cases x; [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2)) | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2)) ] | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x)) ] | change with - ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) → - (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) → + ((carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) → + (carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) → Prop). - elim t; simplify in f f1; + elim a; simplify in f f1; [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) - |2,4: cases t1; + |2,4: cases x; [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2)) |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2)) ] @@ -136,8 +136,8 @@ record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type := definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments. intro; elim n; - [ apply (singl ? (Leibniz ? t)) - | apply (cons ? (Leibniz ? t) a) + [ apply (singl ? (Leibniz ? a)) + | apply (cons ? (Leibniz ? a) a1) ] qed. @@ -367,9 +367,9 @@ definition variance_of_argument_class : Argument_Class → option variance. intros; elim a; [ apply None - | apply (Some ? t) + | apply (Some ? x) | apply None - | apply (Some ? t) + | apply (Some ? x) | apply None ] qed. @@ -569,8 +569,8 @@ in F0. definition product_of_arguments : Arguments → Type. intro; elim a; - [ apply (carrier_of_relation_class ? t) - | apply (Prod (carrier_of_relation_class ? t) T) + [ apply (carrier_of_relation_class ? a1) + | apply (Prod (carrier_of_relation_class ? a1) T) ] qed. @@ -611,15 +611,15 @@ definition relation_of_product_of_arguments: elim In 0; [ simplify; intro; - exact (directed_relation_of_argument_class (get_rewrite_direction r t) t) + exact (directed_relation_of_argument_class (get_rewrite_direction r a) a) | intros; - change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n)); - change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n)); + change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n)); + change in p1 with (Prod (carrier_of_relation_class variance a) (product_of_arguments n)); cases p (c p2); cases p1 (c1 p3); apply And; [ exact - (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1) + (directed_relation_of_argument_class (get_rewrite_direction r a) a c c1) | exact (R p2 p3) ] ] @@ -631,10 +631,10 @@ definition apply_morphism: intro; elim In; [ exact (f p) - | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n)); + | change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n)); elim p; - change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out); - exact (f ? (f1 t1) t2) + change in f1 with (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); + exact (f ? (f1 a1) b) ] qed. @@ -651,14 +651,14 @@ theorem apply_morphism_compatibility_Right2Left: [ simplify in m1 m2 args1 args2 ⊢ %; change in H1 with (directed_relation_of_argument_class - (get_rewrite_direction Right2Left t) t args1 args2); + (get_rewrite_direction Right2Left a) a args1 args2); generalize in match H1; clear H1; generalize in match H; clear H; generalize in match args2; clear args2; generalize in match args1; clear args1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; simplify; + elim a 0; simplify; [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1); apply H; exact H1 @@ -682,32 +682,32 @@ theorem apply_morphism_compatibility_Right2Left: exact H1 ] | change in m1 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in m2 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in args1 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); change in args2 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); generalize in match H2; clear H2; elim args2 0; clear args2; elim args1; clear args1; simplify in H2; change in H2:(? ? %) with - (relation_of_product_of_arguments Right2Left n t2 t4); + (relation_of_product_of_arguments Right2Left n b b1); elim H2; clear H2; change with - (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4) - (apply_morphism n Out (m2 t1) t2)); + (relation_of_relation_class unit Out (apply_morphism n Out (m1 a2) b1) + (apply_morphism n Out (m2 a1) b)); generalize in match H3; clear H3; - generalize in match t3; clear t3; - generalize in match t1; clear t1; + generalize in match a1; clear a1; + generalize in match a2; clear a2; generalize in match H1; clear H1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim a 0; [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3); simplify in H3; change in H1 with @@ -772,14 +772,14 @@ theorem apply_morphism_compatibility_Left2Right: elim In 0; simplify; intros; [ change in H1 with (directed_relation_of_argument_class - (get_rewrite_direction Left2Right t) t args1 args2); + (get_rewrite_direction Left2Right a) a args1 args2); generalize in match H1; clear H1; generalize in match H; clear H; generalize in match args2; clear args2; generalize in match args1; clear args1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; simplify; + elim a 0; simplify; [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1); apply H; exact H1 @@ -805,31 +805,31 @@ theorem apply_morphism_compatibility_Left2Right: exact H1 ] | change in m1 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in m2 with - (carrier_of_relation_class variance t → + (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out); change in args1 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); change in args2 with - ((carrier_of_relation_class ? t) × (product_of_arguments n)); + ((carrier_of_relation_class ? a) × (product_of_arguments n)); generalize in match H2; clear H2; elim args2 0; clear args2; elim args1; clear args1; simplify in H2; change in H2:(? ? %) with - (relation_of_product_of_arguments Left2Right n t2 t4); + (relation_of_product_of_arguments Left2Right n b b1); elim H2; clear H2; change with - (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2) - (apply_morphism n Out (m2 t3) t4)); + (relation_of_relation_class unit Out (apply_morphism n Out (m1 a1) b) + (apply_morphism n Out (m2 a2) b1)); generalize in match H3; clear H3; - generalize in match t3; clear t3; - generalize in match t1; clear t1; + generalize in match a2; clear a2; + generalize in match a1; clear a1; generalize in match H1; clear H1; generalize in match m2; clear m2; generalize in match m1; clear m1; - elim t 0; + elim a 0; [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3); change in H1 with (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));