inductive Context: Set \def
| leaf: Context
- | head: Context \to Bind \to Term \to Context
+ | intb: Context \to IntB \to Term \to Context
.
include "Term/defs.ma".
-inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
- | lift_sort : \forall l,q,i,h.
- Lift q l i (leaf (sort h)) (leaf (sort h))
- | lift_lref : \forall l,i,j.
- Lift false l i (leaf (lref j)) (leaf (lref j))
- | lift_lref_lt: \forall l,i,j. j < i \to
- Lift true l i (leaf (lref j)) (leaf (lref j))
- | lift_lref_ge: \forall l,i,j1. i <= j1 \to
- \forall j2. (j1 + l == j2) \to
- Lift true l i (leaf (lref j1)) (leaf (lref j2))
- | lift_bind : \forall l,i,u1,u2. Lift true l i u1 u2 \to
- \forall q,t1,t2. Lift q l (succ i) t1 t2 \to
- \forall r.
- Lift q l i (head q (bind r) u1 t1) (head q (bind r) u2 t2)
- | lift_flat : \forall l,i,u1,u2. Lift true l i u1 u2 \to
- \forall q,t1,t2. Lift q l i t1 t2 \to
- \forall r.
- Lift q l i (head q (flat r) u1 t1) (head q (flat r) u2 t2)
- | lift_head : \forall l,q,p. (p = q \to False) \to
- \forall i,u1,u2. Lift false l i u1 u2 \to
- \forall t1,t2. Lift q l i t1 t2 \to
- \forall z.
- Lift q l i (head p z u1 t1) (head p z u2 t2)
+inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
+ | lift_sort : \forall i,h.
+ Lift l i (leaf (sort h)) (leaf (sort h))
+ | lift_lref_gt: \forall i,j. i > j \to
+ Lift l i (leaf (lref j)) (leaf (lref j))
+ | lift_lref_le: \forall i,j1. i <= j1 \to
+ \forall j2. (l + j1 == j2) \to
+ Lift l i (leaf (lref j1)) (leaf (lref j2))
+ | lift_bind : \forall i,u1,u2. Lift l i u1 u2 \to
+ \forall t1,t2. Lift l (succ i) t1 t2 \to
+ \forall r. Lift l i (intb r u1 t1) (intb r u2 t2)
+ | lift_flat : \forall i,u1,u2. Lift l i u1 u2 \to
+ \forall t1,t2. Lift l i t1 t2 \to
+ \forall r. Lift l i (intf r u1 t1) (intf r u2 t2)
.
include "Lift/defs.ma".
-theorem lift_sort_1: \forall q, h, d, k, x.
- Lift q h d (leaf (sort k)) x \to
- x = leaf (sort k).
+theorem lift_inv_sort_1: \forall l, i, h, x.
+ Lift l i (leaf (sort h)) x \to
+ x = leaf (sort h).
intros. inversion H; clear H; intros;
[ auto
+ | destruct H2
| destruct H3
- | destruct H4
| destruct H5
- | destruct H7
- | destruct H7
- | destruct H8
+ | destruct H5
].
qed.
-theorem lift_lref_1: \forall q, h, d, k, x.
- Lift q h d (leaf (lref k)) x \to
- (q = false \land x = leaf (lref k)) \lor
- (q = true \land k < d \land x = leaf (lref k)) \lor
- (q = true \land d <= k \land
- \exists e. (k + h == e) \land x = leaf (lref e)
- ).
+theorem lift_inv_lref_1: \forall l, i, j1, x.
+ Lift l i (leaf (lref j1)) x \to
+ (i > j1 \land x = leaf (lref j1)) \lor
+ (i <= j1 \land
+ \exists j2. (l + j1 == j2) \land x = leaf (lref j2)
+ ).
intros. inversion H; clear H; intros;
- [ destruct H3
- | destruct H3. clear H3. subst. auto depth = 4
- | destruct H4. clear H4. subst. auto depth = 5
- | destruct H5. clear H5. subst. auto depth = 5
- | destruct H7
- | destruct H7
- | destruct H8
+ [ destruct H1
+ | destruct H2. clear H2. subst. auto
+ | destruct H3. clear H3. subst. auto depth = 5
+ | destruct H5
+ | destruct H5
].
qed.
-theorem lift_head_1: \forall q, l, i, p, z, u1, t1, x.
- Lift q l i (head p z u1 t1) x \to
- (p = q \land
- \exists r, u2, t2.
- z = bind r \land
- Lift true l i u1 u2 \land Lift q l (succ i) t1 t2 \land
- x = head p z u2 t2
- ) \lor
- (p = q \land
- \exists r,u2,t2.
- z = flat r \land
- Lift true l i u1 u2 \land Lift q l i t1 t2 \land
- x = head p z u2 t2
- ) \lor
- ((p = q \to False) \land
- \exists u2,t2.
- Lift true l i u1 u2 \land Lift q l i t1 t2 \land
- x = head p z u2 t2
- ).
+theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
+ Lift l i (intb r u1 t1) x \to
+ \exists u2, t2.
+ Lift l i u1 u2 \land
+ Lift l (succ i) t1 t2 \land
+ x = intb r u2 t2.
intros. inversion H; clear H; intros;
- [ destruct H3
+ [ destruct H1
+ | destruct H2
| destruct H3
- | destruct H4
+ | destruct H5. clear H5 H1 H3. subst. auto depth = 5
| destruct H5
- | destruct H7. clear H7 H1 H3. subst. auto depth = 10
- | destruct H7. clear H7 H1 H3. subst. auto depth = 10
- | destruct H8. clear H8 H2 H4. subst. auto depth = 7
].
-qed.
\ No newline at end of file
+qed.
+
+theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
+ Lift l i (intf r u1 t1) x \to
+ \exists u2, t2.
+ Lift l i u1 u2 \land
+ Lift l i t1 t2 \land
+ x = intf r u2 t2.
+ intros. inversion H; clear H; intros;
+ [ destruct H1
+ | destruct H2
+ | destruct H3
+ | destruct H5
+ | destruct H5. clear H5 H1 H3. subst. auto depth = 5
+ ].
+qed.
include "Lift/fwd.ma".
-alias id "nplus_conf" = "cic:/matita/RELATIONAL/NPlus/props/nplus_conf.con".
-
-axiom pippo: \forall x,y. x < y \to y <= x \to False.
-
-theorem lift_conf: \forall q,h,d,t,x. Lift q h d t x \to
- \forall y. Lift q h d t y \to
+theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
+ \forall y. Lift l i t y \to
x = y.
- intros 6. elim H; clear H q h d t x;
- [ lapply linear lift_sort_fwd to H1.
+ intros 5. elim H; clear H i t x;
+ [ lapply linear lift_inv_sort_1 to H1.
subst. auto
- | lapply linear lift_lref_fwd to H1.
- decompose; subst;
- [ auto | destruct H1 | destruct H ]
- | lapply linear lift_lref_fwd to H2.
+ | lapply linear lift_inv_lref_1 to H2.
decompose; subst;
- [ destruct H | auto | lapply pippo to H1, H4. decompose ]
- | lapply linear lift_lref_fwd to H3.
+ [ auto | lapply nle_false to H2, H1. decompose ]
+ | lapply linear lift_inv_lref_1 to H3.
decompose; subst;
- [ destruct H
- | lapply linear pippo to H5, H1. decompose
- | lapply linear nplus_conf to H2, H4. subst. auto
+ [ lapply linear nle_false to H1, H3. decompose
+ | lapply linear nplus_conf to H2, H4. subst. auto
]
+ | lapply linear lift_inv_bind_1 to H5.
+ decompose. subst. auto.
+ | lapply linear lift_inv_flat_1 to H5.
+ decompose. subst. auto.
+ ].
+qed.
+
+alias id "nle_trans" = "cic:/matita/RELATIONAL/NLE/props/nle_trans.con".
+alias id "pippo" = "cic:/matita/RELATIONAL/NLE/nplus/pippo.con".
+alias id "nle_refl" = "cic:/matita/RELATIONAL/NLE/props/nle_refl.con".
-(*
-theorem lift_ct_le: \forall q,h,d,t,y. (Lift q h d t y) \to
- \forall k,e,x. (Lift q k e t x) \to
- \forall z. (Lift q k e y z) \to
- e <= d \to \forall d'. (k + d == d') \to
- (Lift q h d' x z).
- intros 6. elim H; clear H q h d t y;
- [ lapply linear lift_sort_fwd to H1.
- lapply linear lift_sort_fwd to H2.
+theorem lift_ct_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
+ \forall l2,i2,x. (Lift l2 i2 t x) \to
+ \forall z. (Lift l2 i2 y z) \to
+ i2 <= i1 \to \forall i. (l2 + i1 == i) \to
+ (Lift l1 i x z).
+ intros 5. elim H; clear H i1 t y;
+ [ lapply lift_conf to H1, H2. clear H2. subst.
+ lapply linear lift_inv_sort_1 to H1.
subst. auto
- | lapply linear lift_lref_fwd to H1.
- lapply linear lift_lref_fwd to H2.
- decompose; subst;
- [ auto
- | auto
- |
- *)
\ No newline at end of file
+ | lapply lift_conf to H2, H3. clear H3. subst.
+ lapply linear lift_inv_lref_1 to H2.
+ decompose; subst; clear H2 H4 i2;
+ [ lapply linear nle_nplus to H5 as H. clear l2. (**)
+ lapply linear nle_trans to H1, H.
+ auto
+ | lapply pippo to H3, H5; [ auto | apply nle_refl | auto ]. (**)
+ ]
+ |
\ No newline at end of file
| cast: Flat
.
-inductive Head: Set \def
- | bind: Bind \to Head
- | flat: Flat \to Head
+inductive IntB: Set \def
+ | bind: Bool \to Bind \to IntB
+.
+
+inductive IntF: Set \def
+ | flat: Bool \to Flat \to IntF
.
inductive Term: Set \def
| leaf: Leaf \to Term
- | head: Bool \to Head \to Term \to Term \to Term
+ | intb: IntB \to Term \to Term \to Term
+ | intf: IntF \to Term \to Term \to Term
.
include "../../RELATIONAL/NLE/defs.ma".
include "../../RELATIONAL/Nat/defs.ma".
include "../../RELATIONAL/Bool/defs.ma".
+
+alias id "nplus_conf" = "cic:/matita/RELATIONAL/NPlus/props/nplus_conf.con".
+alias id "nle_false" = "cic:/matita/RELATIONAL/NLE/props/nle_false.con".
+
+axiom f_equal_3: \forall (A,B,C,D:Set).
+ \forall (f:A \to B \to C \to D).
+ \forall (x1,x2:A).
+ \forall (y1,y2:B).
+ \forall (z1,z2:C).
+ x1 = x2 \to y1 = y2 \to z1 = z2 \to
+ f x1 y1 z1 = f x2 y2 z2.
theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
intros 2; elim y; clear y;
- [ auto new timeout=100
+ [ auto
| decompose;
- [ lapply linear nle_gen_succ_1 to H1. decompose.
- subst. auto new timeout=100 depth=4
+ [ lapply linear nle_inv_succ_1 to H1. decompose.
+ subst. auto depth=4
| lapply linear nle_lt_or_eq to H1; decompose;
- subst; auto new timeout=100
+ subst; auto
]
].
qed.
include "NPlus/defs.ma".
-definition NLE: Nat \to Nat \to Prop \def
- \lambda q,r. \exists p. (p + q == r).
+inductive NLE (q:Nat) (r:Nat): Prop \def
+ | nle_nplus: \forall p. (p + q == r) \to NLE q r.
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'less or equal to'" 'leq x y =
- (cic:/matita/RELATIONAL/NLE/defs/NLE.con x y).
+ (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'less than'" 'lt x y =
- (cic:/matita/RELATIONAL/NLE/defs/NLE.con
+ (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1)
+ (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y).
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'greater or equal to'" 'geq y x=
+ (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y).
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'greater than'" 'gt y x =
+ (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1)
(cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y).
include "logic/connectives.ma".
-include "NPlus/fwd.ma".
+include "NPlus/fwd.ma".
include "NLE/defs.ma".
-theorem nle_gen_succ_1: \forall x,y. x < y \to
- \exists z. y = succ z \land x <= z.
- unfold NLE.
- intros. decompose.
- lapply linear nplus_gen_succ_2 to H1 as H.
- decompose. subst.
- apply ex_intro;[| auto] (**)
+theorem nle_inv_succ_1: \forall x,y. x < y \to
+ \exists z. y = succ z \land x <= z.
+ intros. elim H.
+ lapply linear nplus_gen_succ_2 to H1.
+ decompose. subst. auto depth = 4.
qed.
-
-theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y.
+theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y.
intros.
- lapply linear nle_gen_succ_1 to H as H0. decompose H0.
- lapply linear eq_gen_succ_succ to H1 as H. subst.
+ lapply linear nle_inv_succ_1 to H. decompose.
+ lapply linear eq_gen_succ_succ to H1. subst.
auto.
qed.
-theorem nle_gen_succ_zero: \forall x. x < zero \to False.
+theorem nle_inv_succ_zero: \forall x. x < zero \to False.
intros.
- lapply linear nle_gen_succ_1 to H. decompose.
+ lapply linear nle_inv_succ_1 to H. decompose.
lapply linear eq_gen_zero_succ to H1. decompose.
qed.
-theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero.
+theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero.
intros 1. elim x; clear x; intros;
- [ auto new timeout=30
- | lapply linear nle_gen_succ_zero to H1. decompose.
+ [ auto
+ | lapply linear nle_inv_succ_zero to H1. decompose.
].
qed.
-theorem nle_gen_succ_2: \forall y,x. x <= succ y \to
+theorem nle_inv_succ_2: \forall y,x. x <= succ y \to
x = zero \lor \exists z. x = succ z \land z <= y.
intros 2; elim x; clear x; intros;
- [ auto new timeout=30
- | lapply linear nle_gen_succ_succ to H1.
- right. apply ex_intro; [|auto new timeout=30] (**)
+ [ auto
+ | lapply linear nle_inv_succ_succ to H1.
+ auto depth = 4.
].
qed.
--- /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/RELATIONAL/NLE/nplus".
+
+include "NLE/defs.ma".
+
+axiom pippo: \forall x1, x2, x3. (x1 + x2 == x3) \to
+ \forall y1, y2, y3. (y1 + y2 == y3) \to
+ x1 <= y1 \to x2 < y2 \to x3 < y3.
include "NLE/fwd.ma".
-theorem nle_zero: \forall q. zero <= q.
- unfold NLE.
- intros. apply ex_intro; auto. (**)
+theorem nle_zero_1: \forall q. zero <= q.
+ intros. auto.
qed.
-theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q.
- unfold NLE.
- intros. decompose.
- apply ex_intro; [|auto] (**)
+theorem nle_succ_succ: \forall p,q. p <= q \to succ p <= succ q.
+ intros. elim H. clear H. auto.
+qed.
+
+theorem nle_ind: \forall P:(Nat \to Nat \to Prop).
+ (\forall n:Nat.P zero n) \to
+ (\forall n,n1:Nat.
+ n <= n1 \to P n n1 \to P (succ n) (succ n1)
+ ) \to
+ \forall n,n1:Nat. n <= n1 \to P n n1.
+ intros 4. elim n; clear n;
+ [ auto
+ | lapply linear nle_inv_succ_1 to H3. decompose; subst.
+ auto
+ ].
qed.
theorem nle_refl: \forall x. x <= x.
- intros 1; elim x; clear x; intros; auto new timeout=100.
+ intros 1; elim x; clear x; intros; auto.
qed.
theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros 1. elim x; clear x; intros;
- [ auto new timeout=100.
- | lapply linear nle_gen_succ_1 to H1 as H0. decompose H0. subst.
- auto new timeout=100.
+ intros. elim H using nle_ind; clear H x y; auto.
+qed.
+
+theorem nle_false: \forall x,y. x <= y \to y < x \to False.
+ intros 3; elim H using nle_ind; clear H x y; auto.
+qed.
+
+theorem nle_trans: \forall x,y. x <= y \to
+ \forall z. y <= z \to x <= z.
+ intros 3. elim H using nle_ind; clear H x y;
+ [ auto
+ | lapply linear nle_inv_succ_1 to H3. decompose. subst.
+ auto
].
qed.
theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
- intros 1. elim y; clear y; intros;
- [ lapply linear nle_gen_zero_2 to H. auto new timeout=100
- | lapply linear nle_gen_succ_2 to H1. decompose;
- [ subst. auto new timeout=100
- | lapply linear H to H3 as H0. decompose;
- subst; auto new timeout=100
- ]
+ intros. elim H using nle_ind; clear H x y;
+ [ elim n; clear n; auto
+ | decompose; subst; auto
].
qed.
projects / helm.git / commitdiff