(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/generic_iter_p".
-
+include "nat/div_and_mod_diseq.ma".
include "nat/primes.ma".
include "nat/ord.ma".
reflexivity.
qed.
-
-
theorem false_to_iter_p_gen_Sn:
\forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
\forall baseA:A. \forall plusA: A \to A \to A.
reflexivity.
qed.
-
theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
\forall g1,g2: nat \to A. \forall baseA: A.
\forall plusA: A \to A \to A. \forall n:nat.
intros.
elim k
-[ rewrite < (plus_n_O n).
- simplify.
+[ simplify.
rewrite > H in \vdash (? ? ? %).
rewrite > (H1 ?).
reflexivity
]
qed.
+(* a therem slightly more general than the previous one *)
+theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
+\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
+(\forall a. plusA baseA a = a) \to
+n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
+\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
+intros 9.
+elim H1
+[reflexivity
+|apply (bool_elim ? (p n1));intro
+ [elim (H4 n1)
+ [apply False_ind.
+ apply not_eq_true_false.
+ rewrite < H5.
+ rewrite < H6.
+ reflexivity
+ |rewrite > true_to_iter_p_gen_Sn
+ [rewrite > H6.
+ rewrite > H.
+ apply H3.intros.
+ apply H4
+ [assumption
+ |apply le_S.assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ |apply le_n
+ ]
+ |rewrite > false_to_iter_p_gen_Sn
+ [apply H3.intros.
+ apply H4
+ [assumption
+ |apply le_S.assumption
+ ]
+ |assumption
+ ]
+ ]
+]
+qed.
+
theorem iter_p_gen2 :
\forall n,m:nat.
\forall p1,p2:nat \to bool.
rewrite > sym_plus.
rewrite > (div_plus_times ? ? ? H5).
rewrite > (mod_plus_times ? ? ? H5).
- rewrite > H4.
- simplify.reflexivity.
+ reflexivity.
]
| reflexivity
]
rewrite > sym_plus.
rewrite > (div_plus_times ? ? ? H5).
rewrite > (mod_plus_times ? ? ? H5).
- rewrite > H4.
- simplify.reflexivity.
+ reflexivity.
]
| reflexivity
]
]
qed.
-
-(* da spostare *)
-
+theorem eq_iter_p_gen_pred:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+\forall n,p,g.
+p O = true \to
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to
+iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA =
+plusA (iter_p_gen n p A g baseA plusA) (g O).
+intros.
+elim n
+ [rewrite > true_to_iter_p_gen_Sn
+ [simplify.apply H1
+ |assumption
+ ]
+ |apply (bool_elim ? (p n1));intro
+ [rewrite > true_to_iter_p_gen_Sn
+ [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
+ [rewrite > H2 in ⊢ (? ? ? %).
+ apply eq_f.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ |rewrite > false_to_iter_p_gen_Sn
+ [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
definition p_ord_times \def
\lambda p,m,x.
match p_ord x p with
]
qed.
-(* lemmino da postare *)
-theorem lt_times_to_lt_div: \forall i,n,m. i < n*m \to i/m < n.
-intros.
-cut (O < m)
- [apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? i)
- [rewrite > (div_mod i m) in \vdash (? ? %).
- apply le_plus_n_r.
- assumption
- |assumption
- ]
- ]
- |apply (lt_times_to_lt_O ? ? ? H)
- ]
-qed.
-
theorem iter_p_gen_knm:
\forall A:Type.
\forall baseA: A.
[ assumption
| assumption
]
- | rewrite > H14.
+ | unfold ha.
+ unfold ha12.
+ unfold ha22.
+ rewrite > H14.
rewrite > H13.
apply sym_eq.
apply div_mod.
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).
]
qed.
-
-
-
-
+theorem iter_p_gen_iter_p_gen:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to
+(associative A plusA) \to
+(\forall a:A.(plusA a baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall x,y. x < n \to y < m \to
+ (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
+iter_p_gen n p11 A
+ (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
+ baseA plusA =
+iter_p_gen m p21 A
+ (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA )
+ baseA plusA.
+intros.
+apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
+ n m m n p11 p21 p12 p22)
+ [intros.split
+ [split
+ [split
+ [split
+ [split
+ [apply (andb_true_true ? (p12 j i)).
+ rewrite > H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ |apply (andb_true_true_r (p11 j)).
+ rewrite > H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ ]
+ |reflexivity
+ ]
+ |reflexivity
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ |intros.split
+ [split
+ [split
+ [split
+ [split
+ [apply (andb_true_true ? (p22 j i)).
+ rewrite < H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ |apply (andb_true_true_r (p21 j)).
+ rewrite < H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ ]
+ |reflexivity
+ ]
+ |reflexivity
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+qed.
\ No newline at end of file
projects / helm.git / blobdiff