]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma
- new tactic subst removes simple non recursive equalities from the context
[helm.git] / helm / software / matita / contribs / RELATIONAL / NLE / fwd.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/RELATIONAL/NLE/fwd".
16
17 include "logic/connectives.ma".
18
19 include "Nat/fwd.ma". 
20 include "NLE/defs.ma".
21
22 theorem nle_gen_succ_1: \forall x,y. x < y \to 
23                         \exists z. y = succ z \land x <= z.
24  intros. inversion H; clear H; intros;
25  [ apply (eq_gen_succ_zero ? ? H)
26  | lapply linear eq_gen_succ_succ to H2 as H0.
27    subst.
28    apply ex_intro; [|auto] (**)
29  ].
30 qed.
31
32 theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y.
33  intros; inversion H; clear H; intros;
34  [ apply (eq_gen_succ_zero ? ? H)
35  | lapply linear eq_gen_succ_succ to H2 as H0.
36    lapply linear eq_gen_succ_succ to H3 as H2.
37    subst. auto
38  ].
39 qed.
40
41 theorem nle_gen_succ_zero: \forall (P:Prop). \forall x. x < zero \to P.
42  intros.
43  lapply linear nle_gen_succ_1 to H. decompose.
44  apply (eq_gen_zero_succ ? ? H1).
45 qed.
46
47 theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero.
48  intros 1. elim x; clear x; intros;
49  [ auto
50  | apply (nle_gen_succ_zero ? ? H1)
51  ].
52 qed.
53
54 theorem nle_gen_succ_2: \forall y,x. x <= succ y \to
55                         x = zero \lor \exists z. x = succ z \land z <= y.
56  intros 2; elim x; clear x; intros;
57  [ auto
58  | lapply linear nle_gen_succ_succ to H1.
59    right. apply ex_intro; [|auto] (**)
60  ].
61 qed.