6 (* eq ***********************************************************************)
8 Hint eq : ltlc := Constructors eq.
10 Hint f1N : ltlc := Resolve (f_equal nat).
12 Hint f2NN : ltlc := Resolve (f_equal2 nat nat).
14 Hints Resolve sym_equal : ltlc.
16 Hints Resolve plus_sym plus_n_Sm plus_assoc_r simpl_plus_l : ltlc.
18 Hints Resolve minus_n_O : ltlc.
20 (* le ***********************************************************************)
22 Hint le : ltlc := Constructors le.
24 Hints Resolve le_O_n le_n_S le_S_n le_trans : ltlc.
26 Hints Resolve lt_le_S : ltlc.
28 Hints Resolve le_plus_plus le_plus_trans le_plus_l le_plus_r : ltlc.
30 (* lt ***********************************************************************)
32 Hints Resolve lt_trans : ltlc.
34 Hints Resolve lt_le_trans le_lt_n_Sm : ltlc.
36 Hints Resolve lt_reg_r lt_le_plus_plus le_lt_plus_plus : ltlc.
38 (* not **********************************************************************)
40 Hints Resolve sym_not_equal : ltlc.
42 (* missing in the standard library ******************************************)
44 Theorem simpl_plus_r: (n,m,p:?) (plus m n) = (plus p n) -> m = p.
46 Apply (simpl_plus_l n).
51 Theorem minus_plus_r: (m,n:?) (minus (plus m n) n) = m.
57 Theorem plus_permute_2_in_3: (x,y,z:?) (plus (plus x y) z) = (plus (plus x z) y).
60 Rewrite (plus_sym y z).
61 Rewrite <- plus_assoc_r; XAuto.
64 Theorem plus_permute_2_in_3_assoc: (n,h,k:?) (plus (plus n h) k) = (plus n (plus k h)).
66 Rewrite plus_permute_2_in_3; Rewrite plus_assoc_l; XAuto.
69 Theorem plus_O: (x,y:?) (plus x y) = (0) -> x = (O) /\ y = (O).
70 XElim x; [ XAuto | Intros; Inversion H0 ].
73 Theorem minus_Sx_SO: (x:?) (minus (S x) (1)) = x.
74 Intros; Simpl; Rewrite <- minus_n_O; XAuto.
77 Theorem eq_nat_dec: (i,j:nat) ~i=j \/ i=j.
78 XElim i; XElim j; Intros; XAuto.
82 Theorem neq_eq_e: (i,j:nat; P:Prop) (~i=j -> P) -> (i=j -> P) -> P.
84 Pose (eq_nat_dec i j).
88 Theorem le_false: (m,n:?; P:Prop) (le m n) -> (le (S n) m) -> P.
94 (* case 2.1 : n = 0 *)
96 (* case 2.2 : n > 0 *)
101 Theorem le_plus_minus_sym: (n,m:?) (le n m) -> m = (plus (minus m n) n).
103 Rewrite plus_sym; Apply le_plus_minus; XAuto.
106 Theorem le_minus_minus: (x,y:?) (le x y) -> (z:?) (le y z) ->
107 (le (minus y x) (minus z x)).
109 EApply simpl_le_plus_l.
110 Rewrite le_plus_minus_r; [ Idtac | XAuto ].
111 Rewrite le_plus_minus_r; XEAuto.
114 Theorem le_minus_plus: (z,x:?) (le z x) -> (y:?)
115 (minus (plus x y) z) = (plus (minus x z) y).
118 Intros x H; Inversion H; XAuto.
120 Intros z; XElim x; Intros.
121 (* case 2.1 : x = 0 *)
123 (* case 2.2 : x > 0 *)
127 Theorem le_minus: (x,z,y:?) (le (plus x y) z) -> (le x (minus z y)).
129 Rewrite <- (minus_plus_r x y); XAuto.
130 Apply le_minus_minus; XAuto.
133 Theorem le_trans_plus_r: (x,y,z:?) (le (plus x y) z) -> (le y z).
135 EApply le_trans; [ EApply le_plus_r | Idtac ]; XEAuto.
138 Theorem le_gen_S: (m,x:?) (le (S m) x) ->
139 (EX n | x = (S n) & (le m n)).
140 Intros; Inversion H; XEAuto.
143 Theorem lt_x_plus_x_Sy: (x,y:?) (lt x (plus x (S y))).
144 Intros; Rewrite plus_sym; Simpl; XAuto.
147 Theorem simpl_lt_plus_r: (p,n,m:?) (lt (plus n p) (plus m p)) -> (lt n m).
149 EApply simpl_lt_plus_l.
150 Rewrite plus_sym in H; Rewrite (plus_sym m p) in H; Apply H.
153 Theorem minus_x_Sy: (x,y:?) (lt y x) ->
154 (minus x y) = (S (minus x (S y))).
159 XElim y; Intros; Simpl.
160 (* case 2.1 : y = 0 *)
161 Rewrite <- minus_n_O; XAuto.
162 (* case 2.2 : y > 0 *)
163 Cut (lt n0 n); XAuto.
166 Theorem lt_plus_minus: (x,y:?) (lt x y) ->
167 y = (S (plus x (minus y (S x)))).
169 Apply (le_plus_minus (S x) y); XAuto.
172 Theorem lt_plus_minus_r: (x,y:?) (lt x y) ->
173 y = (S (plus (minus y (S x)) x)).
175 Rewrite plus_sym; Apply lt_plus_minus; XAuto.
178 Theorem minus_x_SO: (x:?) (lt (0) x) -> x = (S (minus x (1))).
180 Rewrite <- minus_x_Sy; [ Rewrite <- minus_n_O; XEAuto | XEAuto ].
183 Theorem lt_le_minus: (x,y:?) (lt x y) -> (le x (minus y (1))).
184 Intros; Apply le_minus; Rewrite plus_sym; Simpl; XAuto.
187 Theorem lt_le_e: (n,d:?; P:Prop)
188 ((lt n d) -> P) -> ((le d n) -> P) -> P.
190 Cut (le d n) \/ (lt n d); [ Intros H1; XElim H1; XAuto | Apply le_or_lt ].
193 Theorem lt_eq_e: (x,y:?; P:Prop) ((lt x y) -> P) ->
194 (x = y -> P) -> (le x y) -> P.
196 LApply (le_lt_or_eq x y); [ Clear H1; Intros H1 | XAuto ].
200 Theorem lt_eq_gt_e: (x,y:?; P:Prop) ((lt x y) -> P) ->
201 (x = y -> P) -> ((lt y x) -> P) -> P.
203 Apply (lt_le_e x y); [ XAuto | Intros ].
204 Apply (lt_eq_e y x); XAuto.
207 Theorem lt_gen_S': (x,n:?) (lt x (S n)) ->
208 x = (0) \/ (EX m | x = (S m) & (lt m n)).
212 Hints Resolve le_lt_trans : ltlc.
214 Hints Resolve simpl_plus_r minus_plus_r minus_x_Sy
215 plus_permute_2_in_3 plus_permute_2_in_3_assoc : ltlc.
217 Hints Resolve le_minus_minus le_minus_plus le_minus le_trans_plus_r : ltlc.
219 Hints Resolve lt_x_plus_x_Sy simpl_lt_plus_r lt_le_minus lt_plus_minus
220 lt_plus_minus_r : ltlc.
222 Theorem lt_neq: (x,y:?) (lt x y) -> ~x=y.
223 Unfold not; Intros; Rewrite H0 in H; Clear H0 x.
224 LApply (lt_n_n y); XAuto.
227 Hints Resolve lt_neq : ltlc.
229 Theorem arith0: (h2,d2,n:?) (le (plus d2 h2) n) ->
230 (h1:?) (le (plus d2 h1) (minus (plus n h1) h2)).
232 Rewrite <- (minus_plus h2 (plus d2 h1)).
233 Apply le_minus_minus; [ XAuto | Idtac ].
234 Rewrite plus_assoc_l; Rewrite (plus_sym h2 d2); XAuto.
237 Hints Resolve arith0 : ltlc.
239 Tactic Definition EqFalse :=
241 [ H: ~?1=?1 |- ? ] ->
242 LApply H; [ Clear H; Intros H; Inversion H | XAuto ].
244 Tactic Definition PlusO :=
246 | [ H: (plus ?0 ?1) = (0) |- ? ] ->
247 LApply (plus_O ?0 ?1); [ Clear H; Intros H | XAuto ];
250 Tactic Definition SymEqual :=
252 | [ H: ?1 = ?2 |- ? ] ->
253 Cut ?2 = ?1; [ Clear H; Intros H | Apply sym_equal; XAuto ].
255 Tactic Definition LeLtGen :=
257 | [ H: (le (S ?1) ?2) |- ? ] ->
258 LApply (le_gen_S ?1 ?2); [ Clear H; Intros H | XAuto ];
260 | [ H: (lt ?1 (S ?2)) |- ? ] ->
261 LApply (lt_gen_S' ?1 ?2); [ Clear H; Intros H | XAuto ];
262 XElim H; [ Intros | Intros H; XElim H; Intros ].