From: Claudio Sacerdoti Coen Date: Mon, 10 Mar 2008 13:37:23 +0000 (+0000) Subject: Scripts fixed because of: X-Git-Tag: make_still_working~5542 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b37f3d17c490c83c69997c5e08057df2d36ce0a7;p=helm.git Scripts fixed because of: a) reduce got rid of b) different behaviour of reduction w.r.t. zeta-reduction --- diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma index 30c8c8bd5..ddbb807a8 100644 --- a/helm/software/matita/library/algebra/CoRN/Setoids.ma +++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma @@ -1115,7 +1115,7 @@ intros. unfold.unfold.intros 2.elim x 2.elim y 2. simplify. intro. -reduce in H2. +normalize in H2. apply (un_op_wd_unfolded ? f ? ? H2). qed. @@ -1123,7 +1123,7 @@ lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f. un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr). intros.unfold.unfold. intros 2.elim y 2. elim x 2. -intros.reduce in H2. +intros.normalize in H2. apply (cs_un_op_strext ? f ? ? H2). qed. @@ -1182,8 +1182,8 @@ intros. unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2. simplify. intros. -reduce in H4. -reduce in H5. +normalize in H4. +normalize in H5. apply (cs_bin_op_wd ? f ? ? ? ? H4 H5). qed. @@ -1192,7 +1192,7 @@ lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop. bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr). intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2. simplify.intros. -reduce in H4. +normalize in H4. apply (cs_bin_op_strext ? f ? ? ? ? H4). qed. diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma index 9223400e7..6bfa6969f 100644 --- a/helm/software/matita/library/decidable_kit/fintype.ma +++ b/helm/software/matita/library/decidable_kit/fintype.ma @@ -106,8 +106,8 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O)); fold simplify (sort nat_eqType); (* CANONICAL?! *) cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w); simplify; [2: reflexivity] - generalize in match H1; clear H1; cases s; clear s; intros (H1); - unfold segment; simplify; simplify in H1; rewrite > H1; + generalize in match H1; clear H1; cases s (r Pr); clear s; intros (H1); + unfold fsort; unfold segment; simplify; simplify in H1; rewrite > H1; rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?)); unfold Not; intros (Enw); rewrite > Enw in Hw; rewrite > ltb_refl in Hw; destruct Hw] diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma index 5f15bddc9..4796ec10b 100644 --- a/helm/software/matita/library/nat/generic_iter_p.ma +++ b/helm/software/matita/library/nat/generic_iter_p.ma @@ -1571,7 +1571,10 @@ apply (trans_eq ? ? [ assumption | assumption ] - | rewrite > H14. + | unfold ha. + unfold ha12. + unfold ha22. + rewrite > H14. rewrite > H13. apply sym_eq. apply div_mod. @@ -1618,18 +1621,23 @@ apply (trans_eq ? ? rewrite > Hcut. assumption ] - | rewrite > Hcut1. + | unfold ha. + unfold ha12. + rewrite > Hcut1. rewrite > Hcut. assumption ] - | rewrite > Hcut1. + | unfold ha. + unfold ha22. + rewrite > Hcut1. rewrite > Hcut. assumption ] | cut(O \lt m1) [ cut(O \lt n1) [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) ) - [ apply (lt_plus_r). + [ unfold ha. + apply (lt_plus_r). assumption | rewrite > sym_plus. rewrite > (sym_times (h11 i j) m1). @@ -1755,7 +1763,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y |assumption ] ] -qed. - - - +qed. \ No newline at end of file diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma index d9fd301fc..f9c5e878b 100644 --- a/helm/software/matita/library/technicalities/setoids.ma +++ b/helm/software/matita/library/technicalities/setoids.ma @@ -150,8 +150,8 @@ definition morphism_theory_of_function : Morphism_Theory In' Out'. intros; apply (mk_Morphism_Theory ? ? f); - unfold In' in f; clear In'; - unfold Out' in f; clear Out'; + unfold In' in f ⊢ %; clear In'; + unfold Out' in f ⊢ %; clear Out'; generalize in match f; clear f; elim In; [ unfold make_compatibility_goal; @@ -203,7 +203,7 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation: apply mk_Morphism_Theory; [ exact Aeq | unfold make_compatibility_goal; - simplify; + simplify; unfold ASetoidClass; simplify; intros; split; unfold transitive in H; @@ -236,7 +236,7 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation: (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class). intros; apply mk_Morphism_Theory; - reduce; + normalize; [ exact Aeq | intros; split; @@ -275,7 +275,7 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation: apply mk_Morphism_Theory; [ simplify; apply Aeq - | simplify; + | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify; intros; whd; intros; @@ -298,7 +298,7 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation: apply mk_Morphism_Theory; [ simplify; apply Aeq - | simplify; + | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify; intros; whd; intro; @@ -332,7 +332,7 @@ definition morphism_theory_of_predicate : | generalize in match f; clear f; unfold In'; clear In'; elim In; - [ reduce; + [ normalize; intro; apply iff_refl | simplify;