match m with
[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
-
+
interpretation "natural minus" 'minus x y = (minus x y).
+theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
+intros;reflexivity.
+qed.
+
theorem minus_n_O: \forall n:nat.n=n-O.
intros.elim n.simplify.reflexivity.
simplify.reflexivity.
qed.
theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
-intros 2.
-elim m in n ⊢ %.
+intros 2 .elim m in n ⊢ %.
rewrite < minus_n_O.apply plus_n_O.
-elim n1.simplify.
-apply minus_n_n.
-rewrite < plus_n_Sm.
+elim n1.simplify. apply minus_n_n.
+autobatch by H.
+(* rewrite < plus_n_Sm.
change with (S n2 = (S n2 + n)-n).
-apply H.
+apply H. *)
qed.
theorem plus_minus_m_m: \forall n,m:nat.
intros.apply (le_n_O_elim n1 H).
reflexivity.
intros.simplify.rewrite < plus_n_O.reflexivity.
-intros.simplify.rewrite < sym_plus.simplify.
-apply eq_f.rewrite < sym_plus.apply H.
+intros.
+rewrite < sym_plus.simplify. apply eq_f.
+rewrite < sym_plus.apply H.
apply le_S_S_to_le.assumption.
qed.
+theorem le_plus_minus_m_m: \forall n,m:nat. n \le (n-m)+m.
+intro.elim n;
+ [apply le_O_n
+ |cases m; simplify[autobatch|autobatch by H, le_S_S]
+ ]
+qed.
+
theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
n = m+p.
intros.apply (trans_eq ? ? ((n-m)+m)).
theorem plus_to_minus :\forall n,m,p:nat.
n = m+p \to n-m = p.
intros.
-apply (inj_plus_r m).
+(* autobatch by transitive_eq, eq_f2, H. *)
+autobatch depth=4 by inj_plus_r, symmetric_eq, minus_to_plus, le_plus_n_r.
+(*
rewrite < H.
rewrite < sym_plus.
symmetry.
apply plus_minus_m_m.rewrite > H.
rewrite > sym_plus.
-apply le_plus_n.
-qed.
-
-theorem minus_S_S : \forall n,m:nat.
-eq nat (minus (S n) (S m)) (minus n m).
-intros.
-reflexivity.
+apply le_plus_n.*)
qed.
theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
qed.
theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
-intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
+intros.
+apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
intro.elim n1.simplify.apply le_n_Sn.
simplify.rewrite < minus_n_O.apply le_n.
intros.simplify.apply le_n_Sn.
qed.
theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
-intros 3.simplify.intro.
+intros 3.intro.
+(* autobatch *)
+(* end auto($Revision$) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
apply (trans_le (m-n) (S (m-(S n))) p).
apply minus_le_S_minus_S.
assumption.
(* galois *)
theorem monotonic_le_minus_r:
\forall p,q,n:nat. q \leq p \to n-p \le n-q.
-simplify.intros 2.apply (nat_elim2
-(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
-intros.apply (le_n_O_elim n H).apply le_n.
-intros.rewrite < minus_n_O.
-apply le_minus_m.
-intros.elim a.simplify.apply le_n.
-simplify.apply H.apply le_S_S_to_le.assumption.
+intros 2.apply (nat_elim2 ???? p q); intros;
+ [apply (le_n_O_elim n H).apply le_n.
+ |applyS le_minus_m.
+ |elim n1;intros;[apply le_n|simplify.apply H.apply le_S_S_to_le.assumption]
+ ]
+qed.
+
+theorem monotonic_le_minus_l:
+∀p,q,n:nat. q \leq p \to q-n \le p-n.
+intros 2.apply (nat_elim2 ???? p q); intros;
+ [apply (le_n_O_elim n H).apply le_n.
+ |apply le_O_n.
+ |cases n1;[apply H1|simplify. apply H.apply le_S_S_to_le.assumption]
+ ]
qed.
theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
-intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))).
-intros.apply le_O_n.
-simplify.intros.rewrite < plus_n_O.assumption.
intros.
-rewrite < plus_n_Sm.
-apply le_S_S.apply H.
-exact H1.
+(* autobatch by transitive_le, le_plus_minus_m_m, le_plus_l, H.*)
+apply transitive_le
+ [2:apply le_plus_minus_m_m.
+ |3:apply le_plus_l.apply H.
+ ]
+ skip.
qed.
theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
+intros.
+autobatch by (monotonic_le_minus_l (p+m) n m), H.
+(*
intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))).
intros.simplify.apply le_O_n.
intros 2.rewrite < plus_n_O.intro.simplify.assumption.
intros.simplify.apply H.
-apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
+apply le_S_S_to_le.rewrite > plus_n_Sm.assumption. *)
qed.
(* the converse of le_plus_to_minus does not hold *)
theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
-intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
+intros.
+autobatch by trans_le, le_plus_to_le, H, le_plus_minus_m_m.
+(*
+apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n.
apply sym_eq. apply le_n_O_to_eq.
apply le_plus_n.assumption.
intros.simplify.
apply H.apply le_S_S_to_le.
-rewrite > plus_n_Sm.assumption.
+rewrite > plus_n_Sm.assumption. *)
qed.
(* minus and lt - to be completed *)
l < m \to m \le n \to n - m < n - l.
apply nat_elim2
[intros.apply False_ind.apply (not_le_Sn_O ? H)
- |intros.rewrite < minus_n_O.
- change in H1 with (n<n1);
- apply lt_minus_m; autobatch depth=2;
+ |intros.autobatch.
+ (* rewrite < minus_n_O.
+ change in H1 with (n<n1);
+ apply lt_minus_m; autobatch depth=2; *)
|intros.
generalize in match H2.
apply (nat_case n1)
theorem lt_minus_r: \forall n,m,l:nat.
n \le l \to l < m \to l -n < m -n.
+ unfold lt.
intro.elim n
[applyS H1
- |rewrite > eq_minus_S_pred.
+ |(*
+ letin x ≝ (lt_pred (l-n1) (m-n1)).
+ clearbody x.
+ unfold lt in x.
+ autobatch depth=4 width=5 size=10 by
+ x, H, H1, H2, trans_le, le_n_Sn, le_n.
+ ]*)
+ rewrite > eq_minus_S_pred.
rewrite > eq_minus_S_pred.
apply lt_pred
[unfold lt.apply le_plus_to_minus_r.applyS H1
projects / helm.git / commitdiff