$(DEPEND_NAME): $(SRC)
$(H)$(MATITADEP) $(SRC) > $@ || rm -f $@
-include $(DEPEND_NAME)
+#include $(DEPEND_NAME)
+include .depend
(\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to
(\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to
\forall f,g:fraction. R f g.
-intros 7.elim f.apply H.
-elim g.apply H2.
-apply H4.apply H5.
-apply H3.
-apply H1.
+intros 7.elim f.
+ apply H.
+ apply H1.
+ elim g.
+ apply H2.
+ apply H3.
+ apply H4.apply H5.
qed.
(* boolean equality *)
decidable (f = g).
intros.simplify.
apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)).
-intros.elim g1.
-elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
-left.apply eq_f. assumption.
-right.intro.apply H.apply injective_pp.assumption.
-right.apply not_eq_pp_cons.
-right.apply not_eq_pp_nn.
-intros. elim g1.
-right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
-right.apply not_eq_nn_cons.
-elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
-left. apply eq_f. assumption.
-right.intro.apply H.apply injective_nn.assumption.
-intros.right.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq.assumption.
-intros.right.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq.assumption.
-intros.elim H.
-elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
-left.apply eq_f2.assumption. assumption.
-right.intro.apply H2.
-apply eq_cons_to_eq1 f1 g1.assumption.
-right.intro.apply H1.
-apply eq_cons_to_eq2 x y f1 g1.assumption.
+ intros.elim g1.
+ elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+ left.apply eq_f. assumption.
+ right.intro.apply H.apply injective_pp.assumption.
+ right.apply not_eq_pp_nn.
+ right.apply not_eq_pp_cons.
+ intros. elim g1.
+ right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
+ elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
+ left. apply eq_f. assumption.
+ right.intro.apply H.apply injective_nn.assumption.
+ right.apply not_eq_nn_cons.
+ intros.right.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq.assumption.
+ intros.right.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq.assumption.
+ intros.elim H.
+ elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
+ left.apply eq_f2.assumption.
+ assumption.
+ right.intro.apply H2.apply eq_cons_to_eq1 f1 g1.assumption.
+ right.intro.apply H1.apply eq_cons_to_eq2 x y f1 g1.assumption.
qed.
theorem eqfb_to_Prop: \forall f,g:fraction.
(\lambda f,g.match (eqfb f g) with
[true \Rightarrow f=g
|false \Rightarrow \lnot f=g]).
-intros.elim g1.
-simplify.
-apply eqb_elim.
-intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply injective_pp.assumption.
-simplify.apply not_eq_pp_cons.
-simplify.apply not_eq_pp_nn.
-intros.
-elim g1.simplify.
-intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
-simplify.apply not_eq_nn_cons.
-simplify.apply eqb_elim.
-intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply injective_nn.assumption.
-intros.
-simplify.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq. assumption.
-intros.simplify.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq. assumption.
-intros.
-change in match (eqfb (cons x f1) (cons y g1)) with
-(andb (eqZb x y) (eqfb f1 g1)).
-apply eqZb_elim.
-intro.generalize in match H.
-elim (eqfb f1 g1).
-simplify.apply eq_f2.assumption.apply H2.
-simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption.
-intro.simplify.
-intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption.
+ intros.elim g1.
+ simplify.apply eqb_elim.
+ intro.simplify.apply eq_f.assumption.
+ intro.simplify.intro.apply H.apply injective_pp.assumption.
+ simplify.apply not_eq_pp_nn.
+ simplify.apply not_eq_pp_cons.
+ intros.elim g1.
+ simplify.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
+ simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
+ intro.simplify.intro.apply H.apply injective_nn.assumption.
+ simplify.apply not_eq_nn_cons.
+ intros.simplify.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq. assumption.
+ intros.simplify.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq. assumption.
+ intros.
+ change in match (eqfb (cons x f1) (cons y g1))
+ with (andb (eqZb x y) (eqfb f1 g1)).
+ apply eqZb_elim.
+ intro.generalize in match H.elim (eqfb f1 g1).
+ simplify.apply eq_f2.assumption.
+ apply H2.
+ simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption.
+ intro.simplify.intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption.
qed.
let rec finv f \def
| (frac h) \Rightarrow frac (cons (Zplus x y) h)]]].
theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
-simplify. intros.
-apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
-intros.elim g.
-change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)).
-apply eq_f.apply sym_Zplus.
-change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
-rewrite < sym_Zplus.reflexivity.
-change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
-apply eq_f.apply sym_Zplus.
-intros.elim g.
-change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)).
-apply eq_f.apply sym_Zplus.
-change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f).
-rewrite < sym_Zplus.reflexivity.
-change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
-apply eq_f.apply sym_Zplus.
-intros.
-change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f).
-rewrite < sym_Zplus.reflexivity.
-intros.
-change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f).
-rewrite < sym_Zplus.reflexivity.
-intros.
-change with
- match ftimes f g with
- [ one \Rightarrow Z_to_ratio (Zplus x1 y1)
- | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] =
- match ftimes g f with
- [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
- | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
-rewrite < H.rewrite < sym_Zplus.
-reflexivity.
+simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
+ intros.elim g.
+ change with Z_to_ratio (Zplus (pos n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (pos n)).
+ apply eq_f.apply sym_Zplus.
+ change with Z_to_ratio (Zplus (pos n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (pos n)).
+ apply eq_f.apply sym_Zplus.
+ change with frac (cons (Zplus (pos n) z) f) = frac (cons (Zplus z (pos n)) f).
+ rewrite < sym_Zplus.reflexivity.
+ intros.elim g.
+ change with Z_to_ratio (Zplus (neg n) (pos n1)) = Z_to_ratio (Zplus (pos n1) (neg n)).
+ apply eq_f.apply sym_Zplus.
+ change with Z_to_ratio (Zplus (neg n) (neg n1)) = Z_to_ratio (Zplus (neg n1) (neg n)).
+ apply eq_f.apply sym_Zplus.
+ change with frac (cons (Zplus (neg n) z) f) = frac (cons (Zplus z (neg n)) f).
+ rewrite < sym_Zplus.reflexivity.
+ intros.change with frac (cons (Zplus x1 (pos m)) f) = frac (cons (Zplus (pos m) x1) f).
+ rewrite < sym_Zplus.reflexivity.
+ intros.change with frac (cons (Zplus x1 (neg m)) f) = frac (cons (Zplus (neg m) x1) f).
+ rewrite < sym_Zplus.reflexivity.
+ intros.
+ change with
+ match ftimes f g with
+ [ one \Rightarrow Z_to_ratio (Zplus x1 y1)
+ | (frac h) \Rightarrow frac (cons (Zplus x1 y1) h)] =
+ match ftimes g f with
+ [ one \Rightarrow Z_to_ratio (Zplus y1 x1)
+ | (frac h) \Rightarrow frac (cons (Zplus y1 x1) h)].
+ rewrite < H.rewrite < sym_Zplus.reflexivity.
qed.
theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
-intro.
-elim f.
-change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one.
-rewrite > Zplus_Zopp.reflexivity.
+intro.elim f.
+ change with Z_to_ratio (Zplus (pos n) (Zopp (pos n))) = one.
+ rewrite > Zplus_Zopp.reflexivity.
+ change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one.
+ rewrite > Zplus_Zopp.reflexivity.
(* again: we would need something to help finding the right change *)
-change with
-match ftimes f1 (finv f1) with
- [ one \Rightarrow Z_to_ratio (Zplus z (Zopp z))
- | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one.
-rewrite > H.
-rewrite > Zplus_Zopp.reflexivity.
-change with Z_to_ratio (Zplus (neg n) (Zopp (neg n))) = one.
-rewrite > Zplus_Zopp.reflexivity.
+ change with
+ match ftimes f1 (finv f1) with
+ [ one \Rightarrow Z_to_ratio (Zplus z (Zopp z))
+ | (frac h) \Rightarrow frac (cons (Zplus z (Zopp z)) h)] = one.
+ rewrite > H.rewrite > Zplus_Zopp.reflexivity.
qed.
definition rtimes : ratio \to ratio \to ratio \def
match eqZb x y with
[ true \Rightarrow x=y
| false \Rightarrow \lnot x=y].
-intros.elim x.
-elim y.
-simplify.reflexivity.
-simplify.apply not_eq_OZ_neg.
-simplify.apply not_eq_OZ_pos.
-elim y.
-simplify.intro.apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
-simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply inj_neg.assumption.
-simplify.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
-elim y.
-simplify.intro.apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
-simplify.apply not_eq_pos_neg.
-simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply inj_pos.assumption.
+intros.
+elim x.
+ elim y.
+ simplify.reflexivity.
+ simplify.apply not_eq_OZ_pos.
+ simplify.apply not_eq_OZ_neg.
+ elim y.
+ simplify.intro.apply not_eq_OZ_pos n.apply sym_eq.assumption.
+ simplify.apply eqb_elim.
+ intro.simplify.apply eq_f.assumption.
+ intro.simplify.intro.apply H.apply inj_pos.assumption.
+ simplify.apply not_eq_pos_neg.
+ elim y.
+ simplify.intro.apply not_eq_OZ_neg n.apply sym_eq.assumption.
+ simplify.intro.apply not_eq_pos_neg n1 n.apply sym_eq.assumption.
+ simplify.apply eqb_elim.
+ intro.simplify.apply eq_f.assumption.
+ intro.simplify.intro.apply H.apply inj_neg.assumption.
qed.
theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
| EQ \Rightarrow x=y
| GT \Rightarrow y < x].
intros.
-elim x. elim y.
-simplify.apply refl_eq.
-simplify.exact I.
-simplify.exact I.
-elim y. simplify.exact I.
-simplify.
-cut match (nat_compare n1 n) with
-[ LT \Rightarrow n1<n
-| EQ \Rightarrow n1=n
-| GT \Rightarrow n<n1] \to
-match (nat_compare n1 n) with
-[ LT \Rightarrow (S n1) \leq n
-| EQ \Rightarrow neg n = neg n1
-| GT \Rightarrow (S n) \leq n1].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n1 n).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.apply sym_eq.exact H.
-simplify.exact I.
-elim y.simplify.exact I.
-simplify.exact I.
-simplify.
-cut match (nat_compare n n1) with
-[ LT \Rightarrow n<n1
-| EQ \Rightarrow n=n1
-| GT \Rightarrow n1<n] \to
-match (nat_compare n n1) with
-[ LT \Rightarrow (S n) \leq n1
-| EQ \Rightarrow pos n = pos n1
-| GT \Rightarrow (S n1) \leq n].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n n1).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.exact H.
+elim x.
+ elim y.
+ simplify.apply refl_eq.
+ simplify.exact I.
+ simplify.exact I.
+ elim y.
+ simplify.exact I.
+ simplify.
+ cut match (nat_compare n n1) with
+ [ LT \Rightarrow n<n1
+ | EQ \Rightarrow n=n1
+ | GT \Rightarrow n1<n] \to
+ match (nat_compare n n1) with
+ [ LT \Rightarrow (S n) \leq n1
+ | EQ \Rightarrow pos n = pos n1
+ | GT \Rightarrow (S n1) \leq n].
+ apply Hcut.apply nat_compare_to_Prop.
+ elim (nat_compare n n1).
+ simplify.exact H.
+ simplify.apply eq_f.exact H.
+ simplify.exact H.
+ simplify.exact I.
+ elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.
+ cut match (nat_compare n1 n) with
+ [ LT \Rightarrow n1<n
+ | EQ \Rightarrow n1=n
+ | GT \Rightarrow n<n1] \to
+ match (nat_compare n1 n) with
+ [ LT \Rightarrow (S n1) \leq n
+ | EQ \Rightarrow neg n = neg n1
+ | GT \Rightarrow (S n) \leq n1].
+ apply Hcut. apply nat_compare_to_Prop.
+ elim (nat_compare n1 n).
+ simplify.exact H.
+ simplify.apply eq_f.apply sym_eq.exact H.
+ simplify.exact H.
qed.
qed.
theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
-intros 2.elim x.
-cut OZ < y \to Zsucc OZ \leq y.
-apply Hcut. assumption.simplify.elim y.
-simplify.exact H1.
-simplify.exact H1.
-simplify.apply le_O_n.
-cut neg n < y \to Zsucc (neg n) \leq y.
-apply Hcut. assumption.elim n.
-cut neg O < y \to Zsucc (neg O) \leq y.
-apply Hcut. assumption.simplify.elim y.
-simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
-simplify.exact I.
-cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
-apply Hcut. assumption.simplify.
-elim y.
-simplify.exact I.
-simplify.apply le_S_S_to_le n2 n1 H3.
-simplify.exact I.
-exact H.
+intros 2.
+elim x.
+(* goal: x=OZ *)
+ cut OZ < y \to Zsucc OZ \leq y.
+ apply Hcut. assumption.
+ simplify.elim y.
+ simplify.exact H1.
+ simplify.apply le_O_n.
+ simplify.exact H1.
+(* goal: x=pos *)
+ exact H.
+(* goal: x=neg *)
+ cut neg n < y \to Zsucc (neg n) \leq y.
+ apply Hcut. assumption.
+ elim n.
+ cut neg O < y \to Zsucc (neg O) \leq y.
+ apply Hcut. assumption.
+ simplify.elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.apply not_le_Sn_O n1 H2.
+ cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
+ apply Hcut. assumption.simplify.
+ elim y.
+ simplify.exact I.
+ simplify.exact I.
+ simplify.apply le_S_S_to_le n2 n1 H3.
qed.
theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
intros.elim z.
-simplify.reflexivity.
-simplify.reflexivity.
-elim n.simplify.reflexivity.
-simplify.reflexivity.
+ simplify.reflexivity.
+ elim n.
+ simplify.reflexivity.
+ simplify.reflexivity.
+ simplify.reflexivity.
qed.
theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
intros.elim z.
-simplify.reflexivity.
-elim n.simplify.reflexivity.
-simplify.reflexivity.
-simplify.reflexivity.
+ simplify.reflexivity.
+ simplify.reflexivity.
+ elim n.
+ simplify.reflexivity.
+ simplify.reflexivity.
qed.
theorem Zplus_pos_pos:
theorem Zplus_Zsucc_Zpred:
\forall x,y. x+y = (Zsucc x)+(Zpred y).
-intros.
-elim x. elim y.
-simplify.reflexivity.
-simplify.reflexivity.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zsucc_Zpred.reflexivity.
-elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
-rewrite < Zpred_Zplus_neg_O.
-rewrite > Zpred_Zsucc.
-simplify.reflexivity.
-rewrite < Zplus_neg_neg.reflexivity.
-apply Zplus_neg_pos.
-elim y.simplify.reflexivity.
-apply Zplus_pos_neg.
-apply Zplus_pos_pos.
+intros.elim x.
+ elim y.
+ simplify.reflexivity.
+ rewrite < Zsucc_Zplus_pos_O.rewrite > Zsucc_Zpred.reflexivity.
+ simplify.reflexivity.
+ elim y.
+ simplify.reflexivity.
+ apply Zplus_pos_pos.
+ apply Zplus_pos_neg.
+ elim y.
+ rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
+ rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity.
+ apply Zplus_neg_pos.
+ rewrite < Zplus_neg_neg.reflexivity.
qed.
theorem Zplus_Zsucc_pos_pos :
qed.
theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
-intros.elim x.elim y.
-simplify. reflexivity.
-rewrite < Zsucc_Zplus_pos_O.reflexivity.
-simplify.reflexivity.
-elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
-apply Zplus_Zsucc_neg_neg.
-apply Zplus_Zsucc_neg_pos.
-elim y.
-rewrite < sym_Zplus OZ.reflexivity.
-apply Zplus_Zsucc_pos_neg.
-apply Zplus_Zsucc_pos_pos.
+intros.elim x.
+ elim y.
+ simplify. reflexivity.
+ simplify.reflexivity.
+ rewrite < Zsucc_Zplus_pos_O.reflexivity.
+ elim y.
+ rewrite < sym_Zplus OZ.reflexivity.
+ apply Zplus_Zsucc_pos_pos.
+ apply Zplus_Zsucc_pos_neg.
+ elim y.
+ rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
+ apply Zplus_Zsucc_neg_pos.
+ apply Zplus_Zsucc_neg_neg.
qed.
theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
theorem associative_Zplus: associative Z Zplus.
change with \forall x,y,z:Z. (x + y) + z = x + (y + z).
(* simplify. *)
-intros.elim x.simplify.reflexivity.
-elim n.rewrite < (Zpred_Zplus_neg_O (y+z)).
-rewrite < (Zpred_Zplus_neg_O y).
-rewrite < Zplus_Zpred.
-reflexivity.
-rewrite > Zplus_Zpred (neg n1).
-rewrite > Zplus_Zpred (neg n1).
-rewrite > Zplus_Zpred ((neg n1)+y).
-apply eq_f.assumption.
-elim n.rewrite < Zsucc_Zplus_pos_O.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zplus_Zsucc.
-reflexivity.
-rewrite > Zplus_Zsucc (pos n1).
-rewrite > Zplus_Zsucc (pos n1).
-rewrite > Zplus_Zsucc ((pos n1)+y).
-apply eq_f.assumption.
+intros.elim x.
+ simplify.reflexivity.
+ elim n.
+ rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O.
+ rewrite > Zplus_Zsucc.reflexivity.
+ rewrite > Zplus_Zsucc (pos n1).rewrite > Zplus_Zsucc (pos n1).
+ rewrite > Zplus_Zsucc ((pos n1)+y).apply eq_f.assumption.
+ elim n.
+ rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y).
+ rewrite < Zplus_Zpred.reflexivity.
+ rewrite > Zplus_Zpred (neg n1).rewrite > Zplus_Zpred (neg n1).
+ rewrite > Zplus_Zpred ((neg n1)+y).apply eq_f.assumption.
qed.
variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z)
theorem associative_Ztimes: associative Z Ztimes.
change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
-intros.
-elim x.simplify.reflexivity.
-elim y.simplify.reflexivity.
-elim z.simplify.reflexivity.
-change with
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
-change with
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-elim z.simplify.reflexivity.
-change with
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-change with
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
-elim y.simplify.reflexivity.
-elim z.simplify.reflexivity.
-change with
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
-change with
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-elim z.simplify.reflexivity.
-change with
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.apply lt_O_times_S_S.
-change with
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
+intros.elim x.
+ simplify.reflexivity.
+ elim y.
+ simplify.reflexivity.
+ elim z.
+ simplify.reflexivity.
+ change with
+ eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ elim z.
+ simplify.reflexivity.
+ change with
+ eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ elim y.
+ simplify.reflexivity.
+ elim z.
+ simplify.reflexivity.
+ change with
+ eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ elim z.
+ simplify.reflexivity.
+ change with
+ eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
+ rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
qed.
variant assoc_Ztimes : \forall x,y,z:Z.
distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
change with \forall n,y,z.
eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
-intros.
-elim y.reflexivity.
-elim z.reflexivity.
-change with
-eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
+intros.elim y.
+ reflexivity.
+ elim z.
+ reflexivity.
+ change with
+ eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
+ (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
+ rewrite < distr_times_plus.reflexivity.
+ apply Ztimes_Zplus_pos_pos_neg.
+ elim z.
+ reflexivity.
+ apply Ztimes_Zplus_pos_neg_pos.
+ change with
+ eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
(neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus.reflexivity.
-apply Ztimes_Zplus_pos_neg_pos.
-elim z.reflexivity.
-apply Ztimes_Zplus_pos_pos_neg.
-change with
-eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
- (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus.
-reflexivity.
+ rewrite < distr_times_plus.reflexivity.
qed.
variant distr_Ztimes_Zplus_pos: \forall n,y,z.
intros.elim x.
(* case x = OZ *)
simplify.reflexivity.
-(* case x = neg n *)
-apply distr_Ztimes_Zplus_neg.
(* case x = pos n *)
apply distr_Ztimes_Zplus_pos.
+(* case x = neg n *)
+apply distr_Ztimes_Zplus_neg.
qed.
variant distr_Ztimes_Zplus: \forall x,y,z.
|false \Rightarrow \lnot (z=OZ)].
intros.elim z.
simplify.reflexivity.
-simplify.intros.
-cut match neg n with
-[ OZ \Rightarrow True
-| (pos n) \Rightarrow False
-| (neg n) \Rightarrow False].
-apply Hcut.rewrite > H.simplify.exact I.
-simplify.intros.
-cut match pos n with
-[ OZ \Rightarrow True
-| (pos n) \Rightarrow False
-| (neg n) \Rightarrow False].
-apply Hcut. rewrite > H.simplify.exact I.
+simplify.intros [H].
+discriminate H.
+simplify.intros [H].
+discriminate H.
qed.
(* discrimination *)
\def injective_neg.
theorem not_eq_OZ_pos: \forall n:nat. \lnot (OZ = (pos n)).
-simplify.intros.
-change with
- match pos n with
- [ OZ \Rightarrow True
- | (pos n) \Rightarrow False
- | (neg n) \Rightarrow False].
-rewrite < H.
-simplify.exact I.
+simplify.intros [n; H].
+discriminate H.
qed.
theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)).
-simplify.intros.
-change with
- match neg n with
- [ OZ \Rightarrow True
- | (pos n) \Rightarrow False
- | (neg n) \Rightarrow False].
-rewrite < H.
-simplify.exact I.
+simplify.intros [n; H].
+discriminate H.
qed.
theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)).
-simplify.intros.
-change with
- match neg m with
- [ OZ \Rightarrow False
- | (pos n) \Rightarrow True
- | (neg n) \Rightarrow False].
-rewrite < H.
-simplify.exact I.
+simplify.intros [n; m; H].
+discriminate H.
qed.
theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
intros.simplify.
-elim x.elim y.
-left.reflexivity.
-right.apply not_eq_OZ_neg.
-right.apply not_eq_OZ_pos.
-elim y.right.intro.
-apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
-elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
-left.apply eq_f.assumption.
-right.intro.apply H.apply injective_neg.assumption.
-right.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
-elim y.right.intro.
-apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
-right.apply not_eq_pos_neg.
-elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
-left.apply eq_f.assumption.
-right.intro.apply H.apply injective_pos.assumption.
+elim x.
+(* goal: x=OZ *)
+ elim y.
+ (* goal: x=OZ y=OZ *)
+ left.reflexivity.
+ (* goal: x=OZ 2=2 *)
+ right.apply not_eq_OZ_pos.
+ (* goal: x=OZ 2=3 *)
+ right.apply not_eq_OZ_neg.
+(* goal: x=pos *)
+ elim y.
+ (* goal: x=pos y=OZ *)
+ right.intro.
+ apply not_eq_OZ_pos n. symmetry. assumption.
+ (* goal: x=pos y=pos *)
+ elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
+ left.apply eq_f.assumption.
+ right.intros [H_inj].apply H. injection H_inj. assumption.
+ (* goal: x=pos y=neg *)
+ right.intro.apply not_eq_pos_neg n n1. assumption.
+(* goal: x=neg *)
+ elim y.
+ (* goal: x=neg y=OZ *)
+ right.intro.
+ apply not_eq_OZ_neg n. symmetry. assumption.
+ (* goal: x=neg y=pos *)
+ right. intro. apply not_eq_pos_neg n1 n. symmetry. assumption.
+ (* goal: x=neg y=neg *)
+ elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
+ left.apply eq_f.assumption.
+ right.intro.apply H.apply injective_neg.assumption.
qed.
(* end discrimination *)
| (neg n) \Rightarrow neg (S n)].
theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
-intros.elim z.reflexivity.
-elim n.reflexivity.
-reflexivity.
-reflexivity.
+intros.
+elim z.
+ reflexivity.
+ reflexivity.
+ elim n.
+ reflexivity.
+ reflexivity.
qed.
theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
-intros.elim z.reflexivity.
-reflexivity.
-elim n.reflexivity.
-reflexivity.
+intros.
+elim z.
+ reflexivity.
+ elim n.
+ reflexivity.
+ reflexivity.
+ reflexivity.
qed.
intro.simplify.apply le_S_S. apply le_O_n.
intros 2.simplify.elim (nat_compare n1 m1).
simplify. apply le_S_S.apply H.
-simplify. apply le_S_S.apply H.
simplify. apply eq_f. apply H.
+simplify. apply le_S_S.apply H.
qed.
theorem nat_compare_n_m_m_n: \forall n,m:nat.
apply Hcut.apply nat_compare_to_Prop.
elim (nat_compare n m).
apply (H H3).
-apply (H2 H3).
apply (H1 H3).
+apply (H2 H3).
qed.
theorem div_times: \forall n,m:nat. div ((S n)*m) (S n) = m.
intros.
apply div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O.
+goal 15. (* ?11 is closed with the following tactics *)
apply div_mod_spec_div_mod.
simplify.apply le_S_S.apply le_O_n.
apply div_mod_spec_times.
rewrite > H.
simplify.rewrite < assoc_times.
rewrite < Hcut.reflexivity.
-rewrite > sym_times.
-apply plog_aux_to_exp n1 n1.
-apply lt_O_nth_prime_n.assumption.
cut O < r \lor O = r.
elim Hcut1.assumption.absurd n1 = O.
rewrite > Hcut.rewrite < H4.reflexivity.
apply le_to_or_lt_eq r (S O).
apply not_lt_to_le.assumption.
apply decidable_lt (S O) r.
+rewrite > sym_times.
+apply plog_aux_to_exp n1 n1.
+apply lt_O_nth_prime_n.assumption.
qed.
theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
change with divides (nth_prime p) r \to False.
intro.
apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?.
-apply divides_to_mod_O.
-apply lt_O_nth_prime_n.
-assumption.
apply lt_SO_nth_prime_n.
-simplify.apply le_S_S.apply le_O_n.
-apply le_n.
-assumption.rewrite > times_n_SO in \vdash (? ? ? %).
+simplify.apply le_S_S.apply le_O_n.apply le_n.
+assumption.
+apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
+rewrite > times_n_SO in \vdash (? ? ? %).
rewrite < sym_times.
rewrite > exp_n_O (nth_prime p).
rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
assumption.
-apply le_to_or_lt_eq.apply le_O_n.
-(* O < r *)
-cut O < r \lor O = r.
-elim Hcut1.assumption.
-apply False_ind.
-apply not_eq_O_S (S m1).
-rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
-apply le_to_or_lt_eq.apply le_O_n.
-(* prova del cut *)
-apply plog_aux_to_exp (S(S m1)).
-apply lt_O_nth_prime_n.
-assumption.
-(* fine prova cut *)
-assumption.
-(* e adesso l'ultimo goal *)
+apply le_to_or_lt_eq.apply le_O_n.assumption.
+(* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
cut (S O) < r \lor \lnot (S O) < r.
elim Hcut2.
-right.
+right.
apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r.
simplify.apply le_S_S. apply le_O_n.
apply le_n.
apply le_to_or_lt_eq r (S O).
apply not_lt_to_le.assumption.
apply decidable_lt (S O) r.
+(* O < r *)
+cut O < r \lor O = r.
+elim Hcut1.assumption.
+apply False_ind.
+apply not_eq_O_S (S m1).
+rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
+apply le_to_or_lt_eq.apply le_O_n.
+(* prova del cut *)
+goal 20.
+apply plog_aux_to_exp (S(S m1)).
+apply lt_O_nth_prime_n.
+assumption.
+(* fine prova cut *)
qed.
let rec max_p f \def
apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
apply injective_nth_prime ? ? H4.
apply H i (S j) ?.
-assumption.apply trans_lt ? j.assumption.simplify.apply le_n.
+apply trans_lt ? j.assumption.simplify.apply le_n.
+assumption.
apply divides_times_to_divides.
apply prime_nth_prime.assumption.
qed.
rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
apply False_ind.
apply not_divides_defactorize_aux n1 i (S i) ?.
+simplify. apply le_n.
simplify in H5.
rewrite > plus_n_O (defactorize_aux n1 (S i)).
rewrite > H5.
rewrite > assoc_times.
apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))).
reflexivity.
-simplify. apply le_n.
intros.
apply False_ind.
apply not_divides_defactorize_aux n3 i (S i) ?.
+simplify. apply le_n.
simplify in H4.
rewrite > plus_n_O (defactorize_aux n3 (S i)).
rewrite < H4.
rewrite > assoc_times.
apply witness ? ? ((exp (nth_prime i) n4)*(defactorize_aux n1 (S i))).
reflexivity.
-simplify. apply le_n.
intros.
cut nf_cons n4 n1 = nf_cons m n3.
cut n4=m.
rewrite > sym_times.
apply eq_plus_to_le ? ? (mod m n).
reflexivity.
+assumption.
rewrite > sym_times.
-apply div_mod.assumption. assumption.
+apply div_mod.assumption.
qed.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
elim Hcut.rewrite > divides_to_divides_b_true.
simplify.
split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
+assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
(divides (gcd_aux n n1 (mod m n1)) m) \land
apply trans_le ? n1.
change with mod m n1 < n1.
apply lt_mod_m_m.assumption.assumption.
-apply decidable_divides n1 m.assumption.
-apply lt_to_le_to_lt ? n1.assumption.reflexivity.
-assumption.
assumption.assumption.
+apply decidable_divides n1 m.assumption.
qed.
theorem divides_gcd_nm: \forall n,m.
elim Hcut.
rewrite > divides_to_divides_b_true.
simplify.assumption.
+assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with divides d (gcd_aux n n1 (mod m n1)).
apply H.
apply lt_mod_m_m.assumption.assumption.
assumption.
apply divides_mod.assumption.assumption.assumption.
+assumption.assumption.
apply decidable_divides n1 m.assumption.
-apply lt_to_le_to_lt ? n1.assumption.reflexivity.
-assumption.assumption.assumption.
qed.
theorem divides_d_gcd: \forall m,n,d.
apply ex_intro ? ? O.
left.simplify.rewrite < plus_n_O.
apply sym_eq.apply minus_n_O.
+assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
ex nat (\lambda a. ex nat (\lambda b.
rewrite < sym_plus.
rewrite < plus_minus.
rewrite < minus_n_n.reflexivity.
+apply le_n.
+assumption.
(* second case *)
rewrite < H7.
apply ex_intro ? ? (a1+a*(div m n1)).
rewrite < sym_plus.
rewrite < plus_minus.
rewrite < minus_n_n.reflexivity.
-(* end second case *)
+apply le_n.
+assumption.
apply H n1 (mod m n1).
-(* a lot of trivialities left *)
cut O \lt mod m n1 \lor O = mod m n1.
-elim Hcut2.assumption.
+elim Hcut2.assumption.
absurd divides n1 m.apply mod_O_to_divides.
-assumption.apply sym_eq.assumption.assumption.
+assumption.
+symmetry.assumption.assumption.
apply le_to_or_lt_eq.apply le_O_n.
apply lt_to_le.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
apply trans_le ? n1.
change with mod m n1 < n1.
-apply lt_mod_m_m.assumption.assumption.
+apply lt_mod_m_m.
+assumption.assumption.assumption.assumption.
apply decidable_divides n1 m.assumption.
apply lt_to_le_to_lt ? n1.assumption.assumption.
-assumption.assumption.assumption.assumption.assumption.
-apply le_n.assumption.
-apply le_n.
qed.
theorem eq_minus_gcd: \forall m,n.
change with (S (S O)) \le gcd n m \to False.intro.
apply H1.rewrite < H3 (gcd n m).
apply divides_gcd_m.
+apply divides_gcd_n.assumption.
cut O < gcd n m \lor O = gcd n m.
elim Hcut.assumption.
apply False_ind.
elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
apply gcd_O_to_eq_O.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
-apply divides_gcd_n.assumption.
qed.
(* esempio di sfarfallalmento !!! *)
(* end second case *)
rewrite < prime_to_gcd_SO n p.
apply eq_minus_gcd.
+assumption.assumption.
apply decidable_divides n p.
apply trans_lt ? (S O).simplify.apply le_n.
simplify in H.elim H. assumption.
-assumption.assumption.
qed.
rewrite < H2.
rewrite > sym_times.
rewrite < div_mod.reflexivity.
-intros.simplify.apply plus_n_O.
assumption.assumption.
+intros.simplify.apply plus_n_O.
qed.
theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
cut div ((exp m (S n1))*n) m = (exp m n1)*n.
rewrite > Hcut1.
rewrite > H2 m1. simplify.reflexivity.
+apply le_S_S_to_le.assumption.
(* div_exp *)
change with div (m*(exp m n1)*n) m = (exp m n1)*n.
rewrite > assoc_times.
assumption.
simplify.rewrite > assoc_times.
apply witness ? ? ((exp m n1)*n).reflexivity.
-apply le_S_S_to_le.assumption.
qed.
theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
intros.
change with (\lnot (mod n1 m = O)).
rewrite > H4.
-(* META NOT FOUND !!!
+(* META NOT FOUND !!!
rewrite > sym_eq. *)
simplify.intro.
apply not_eq_O_S m1 ?.
(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow (S n1)
| false \Rightarrow (max n1 f)])) = true) ? ? ?.
-reflexivity.
simplify.intro.assumption.
simplify.intro.apply H.
elim H1.elim H3.generalize in match H5.
split.apply le_S_S_to_le.assumption.assumption.
intros.apply False_ind.apply not_eq_true_false ?.
rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
+reflexivity.
qed.
theorem lt_max_to_false : \forall f:nat \to bool.
(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow m-(S n)
| false \Rightarrow (min_aux n m f)])) = true) ? ? ?.
-reflexivity.
simplify.intro.assumption.
simplify.intro.apply H.
elim H1.elim H3.elim H4.
absurd f a = false.rewrite < H8.assumption.
rewrite > H5.
apply not_eq_true_false.
+reflexivity.
qed.
theorem lt_min_aux_to_false : \forall f:nat \to bool.
elim H3.
elim le_to_or_lt_eq (n -(S n1)) m.
apply H.apply lt_minus_S_n_to_le_minus_n.assumption.
-rewrite < H6.assumption.assumption.
+rewrite < H6.assumption.
rewrite < H7.assumption.
+assumption.
qed.
theorem le_min_aux : \forall f:nat \to bool.
theorem distributive_times_minus: distributive nat times minus.
simplify.
intros.
-apply (leb_elim z y).intro.
-cut x*(y-z)+x*z = (x*y-x*z)+x*z.
-apply inj_plus_l (x*z).
-assumption.
-apply trans_eq nat ? (x*y).
-rewrite < distr_times_plus.
-rewrite < plus_minus_m_m ? ? H.reflexivity.
-rewrite < plus_minus_m_m ? ? ?.reflexivity.
-apply le_times_r.
-assumption.
-intro.
-rewrite > eq_minus_n_m_O.
-rewrite > eq_minus_n_m_O (x*y).
-rewrite < sym_times.simplify.reflexivity.
-apply lt_to_le.
-apply not_le_to_lt.assumption.
-apply le_times_r.apply lt_to_le.
-apply not_le_to_lt.assumption.
+apply (leb_elim z y).
+ intro.cut x*(y-z)+x*z = (x*y-x*z)+x*z.
+ apply inj_plus_l (x*z).assumption.
+ apply trans_eq nat ? (x*y).
+ rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
+ rewrite < plus_minus_m_m ? ? ?.
+ reflexivity.
+ apply le_times_r.assumption.
+ intro.rewrite > eq_minus_n_m_O.
+ rewrite > eq_minus_n_m_O (x*y).
+ rewrite < sym_times.simplify.reflexivity.
+ apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
+ apply lt_to_le.apply not_le_to_lt.assumption.
qed.
theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
intros.
cut m+p \le n \or \not m+p \le n.
-elim Hcut.
-apply sym_eq.
-apply plus_to_minus.assumption.
-rewrite > assoc_plus.
-rewrite > sym_plus p.
-rewrite < plus_minus_m_m.
-rewrite > sym_plus.
-rewrite < plus_minus_m_m.reflexivity.
-rewrite > eq_minus_n_m_O n (m+p).
-rewrite > eq_minus_n_m_O (n-m) p.reflexivity.
-apply decidable_le (m+p) n.
-apply le_plus_to_minus_r.
-rewrite > sym_plus.assumption.
-apply trans_le ? (m+p).
-rewrite < sym_plus.
-apply le_plus_n.assumption.
-apply lt_to_le.apply not_le_to_lt.assumption.
-apply le_plus_to_minus.
-apply lt_to_le.apply not_le_to_lt.
-rewrite < sym_plus.assumption.
+ elim Hcut.
+ symmetry.apply plus_to_minus.assumption.
+ rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
+ rewrite > sym_plus.rewrite < plus_minus_m_m.
+ reflexivity.
+ apply trans_le ? (m+p).
+ rewrite < sym_plus.apply le_plus_n.
+ assumption.
+ apply le_plus_to_minus_r.rewrite > sym_plus.assumption.
+ rewrite > eq_minus_n_m_O n (m+p).
+ rewrite > eq_minus_n_m_O (n-m) p.
+ reflexivity.
+ apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
+ apply not_le_to_lt. assumption.
+ apply lt_to_le.apply not_le_to_lt.assumption.
+ apply decidable_le (m+p) n.
qed.
theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
apply not_le_to_lt.
change with smallest_factor (S (fact n)) \le n \to False.intro.
apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
-apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
apply lt_SO_smallest_factor.
simplify.apply le_S_S.apply le_SO_fact.
assumption.
+apply divides_smallest_factor_n.
+simplify.apply le_S_S.apply le_O_n.
qed.
(* mi sembra che il problem sia ex *)
simplify.rewrite < sym_plus.
apply le_plus_n.
elim le_to_or_lt_eq O n2.
-assumption.apply le_O_n.
+assumption.
absurd O<m.assumption.
rewrite > H2.rewrite < H3.rewrite < times_n_O.
apply not_le_Sn_n O.
+apply le_O_n.
qed.
theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n.
matitamake /x/y/z/foo/a.ma
- notazione -> Luca e Zack
- non chiudere transitivamente i moo ??
+ - matitaclean all (non troglie i moo?)
DEMONI E ALTRO
in
status_ref, tactic
+let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
+ let module PEH = ProofEngineHelpers in
+ (* phase one calculates:
+ * new_goals_from_refine: goals added by refine
+ * head_goal: the first goal opened by ythe tactic
+ * other_goals: other goals opened by the tactic
+ *)
+ let new_goals_from_refine = PEH.compare_metasenvs start refine in
+ let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in
+ let head_goal, other_goals, goals =
+ match goals with
+ | [] -> None,[],goals
+ | hd::tl ->
+ (* assert (List.mem hd new_goals_from_tactic);
+ * invalidato dalla goal_tac
+ * *)
+ Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>)
+ hd) goals
+ in
+ let produced_goals =
+ match head_goal with
+ | None -> new_goals_from_refine @ other_goals
+ | Some x -> x :: new_goals_from_refine @ other_goals
+ in
+ (* extract the metas generated by refine and tactic *)
+ let metas_for_tactic_head =
+ match head_goal with
+ | None -> []
+ | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in
+ let metas_for_tactic_goals =
+ List.map
+ (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic)
+ goals
+ in
+ let metas_for_refine_goals =
+ List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in
+ let produced_metas, goals =
+ let produced_metas =
+ if always_opens_a_goal then
+ metas_for_tactic_head @ metas_for_refine_goals @
+ metas_for_tactic_goals
+ else
+ metas_for_refine_goals @ metas_for_tactic_head @
+ metas_for_tactic_goals
+ in
+ let goals = List.map (fun (metano, _, _) -> metano) produced_metas in
+ produced_metas, goals
+ in
+ (* residual metas, preserving the original order *)
+ let before, after =
+ let rec split e =
+ function
+ | [] -> [],[]
+ | (metano, _, _) :: tl when metano = e ->
+ [], List.map (fun (x,_,_) -> x) tl
+ | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a
+ in
+ let find n metasenv =
+ try
+ Some (List.find (fun (metano, _, _) -> metano = n) metasenv)
+ with Not_found -> None
+ in
+ let extract l =
+ List.fold_right
+ (fun n acc ->
+ match find n tactic with
+ | Some x -> x::acc
+ | None -> acc
+ ) l [] in
+ let before_l, after_l = split current_goal start in
+ let before_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) before_l in
+ let after_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) after_l in
+ let before = extract before_l in
+ let after = extract after_l in
+ before, after
+ in
+ (* DEBUG CODE
+ let print_m name metasenv =
+ prerr_endline (">>>>> " ^ name);
+ prerr_endline (CicMetaSubst.ppmetasenv metasenv [])
+ in
+ print_m "BEGIN" start;
+ prerr_endline ("goal was: " ^ string_of_int current_goal);
+ prerr_endline ("and metas from refine are:");
+ List.iter
+ (fun t -> prerr_string (" " ^ string_of_int t))
+ new_goals_from_refine;
+ prerr_endline "";
+ print_m "before" before;
+ print_m "metas_for_tactic_head" metas_for_tactic_head;
+ print_m "metas_for_refine_goals" metas_for_refine_goals;
+ print_m "metas_for_tactic_goals" metas_for_tactic_goals;
+ print_m "after" after;
+ FINE DEBUG CODE *)
+ before @ produced_metas @ after, goals
+
+(* maybe we only need special cases for apply and goal *)
+let classify_tactic tactic =
+ match tactic with
+ (* tactics that can't close the goal (return a goal we want to "select") *)
+ | GrafiteAst.Rewrite _
+ | GrafiteAst.Split _
+ | GrafiteAst.Replace _
+ | GrafiteAst.Reduce _
+ | GrafiteAst.Injection _
+ | GrafiteAst.IdTac _
+ | GrafiteAst.Generalize _
+ | GrafiteAst.Elim _
+ | GrafiteAst.Decompose _ -> true, true
+ (* tactics we don't want to reorder goals. I think only Goal needs this. *)
+ | GrafiteAst.Goal _ -> false, true
+ (* tactics like apply *)
+ | _ -> true, false
+
let apply_tactic tactic status =
+ let starting_metasenv = MatitaMisc.get_proof_metasenv status in
let status_ref, tactic = disambiguate_tactic status tactic in
+ let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in
let proof_status = MatitaMisc.get_proof_status !status_ref in
+ let needs_reordering, always_opens_a_goal = classify_tactic tactic in
let tactic = tactic_of_ast tactic in
(* apply tactic will change the status pointed by status_ref ... *)
+ let current_goal = let _, g = proof_status in g in
let (proof, goals) = ProofEngineTypes.apply_tactic tactic proof_status in
+ let proof, goals =
+ if needs_reordering then
+ let uri, metasenv_after_tactic, t, ty = proof in
+ let reordered_metasenv, goals =
+ reorder_metasenv starting_metasenv metasenv_after_refinement
+ metasenv_after_tactic goals current_goal always_opens_a_goal in
+ (uri, reordered_metasenv, t, ty), goals
+ else
+ proof, goals
+ in
let dummy = -1 in
{ !status_ref with
proof_status = MatitaTypes.Incomplete_proof (proof,dummy) },
--- /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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/tests/metasenv_ordering".
+
+include "coq.ma".
+
+alias num (instance 0) = "natural number".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+
+(* REWRITE *)
+
+theorem th1 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 2 = 2.
+ intros. split. split.
+ goal 13.
+ rewrite > H; [reflexivity | exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+theorem th2 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 3 = 3.
+ intros. split. split.
+ goal 13.
+ rewrite > H ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+theorem th3 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 4 = 4.
+ intros. split. split.
+ goal 13.
+ rewrite > H ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+theorem th4 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 5 = 5.
+ intros. split. split.
+ goal 13.
+ rewrite > H ? ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+(* APPLY *)
+
+theorem th5 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 6 = 6.
+ intros. split. split.
+ goal 13.
+ apply H; [exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+theorem th6 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 7 = 7.
+ intros. split. split.
+ goal 13.
+ apply H ?; [exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+theorem th7 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 8 = 8.
+ intros. split. split.
+ goal 13.
+ apply H ? ?; [exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+theorem th8 :
+ \forall P:Prop.
+ \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
+ 1 = 1 \land 1 = 0 \land 9 = 9.
+ intros. split. split.
+ goal 13.
+ apply H ? ? ?; [exact nat | exact 0=0 | exact Type].
+ reflexivity.
+ reflexivity.
+qed.
+
+(* ELIM *)
+
+theorem th9:
+ \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
+ intros [P; Q; R; S; r; s; H].
+ elim H ? ?; [split; assumption | exact r | exact s].
+ qed.
+
+theorem th10:
+ \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
+ intros [P; Q; R; S; r; s; H].
+ elim H ?; [split; assumption | exact r | exact s].
+ qed.
+
+theorem th11:
+ \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
+ intros [P; Q; R; S; r; s; H].
+ elim H; [split; assumption | exact r | exact s].
+ qed.
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
projects / helm.git / commitdiff