+++ /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/LAMBDA-TYPES/Unified-Sub/Context/defs".
-
-(* FLAT CONTEXTS
- - Naming policy:
- - contexts: c d
-*)
-
-include "Term/defs.ma".
-
-inductive Context: Set \def
- | leaf: Context
- | intb: Context \to IntB \to Term \to Context
-.
- Usage: invoke with positive polarity
*)
-include "Term/defs.ma".
+include "datatypes/Term.ma".
inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
| lift_sort : \forall i,h.
--- /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/LAMBDA-TYPES/Unified-Sub/Lift/fun".
+
+include "Lift/inv.ma".
+
+(* Functional properties ****************************************************)
+(*
+theorem lift_total: \forall l, t, i. \exists u. Lift l i t u.
+ intros 2. elim t; clear t;
+ [
+*)
+theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
+ \forall t2. Lift l i t t2 \to
+ t1 = t2.
+ intros 5. elim H; clear H i t t1;
+ [ lapply linear lift_inv_sort_1 to H1
+ | lapply linear lift_inv_lref_1_gt to H2, H1
+ | lapply linear lift_inv_lref_1_le to H3, H1, H2
+ | lapply linear lift_inv_bind_1 to H5. decompose
+ | lapply linear lift_inv_flat_1 to H5. decompose
+ ]; subst; auto.
+qed.
+
+theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
+ \forall t2. Lift l i t2 t \to
+ t2 = t1.
+ intros 5. elim H; clear H i t1 t;
+ [ lapply linear lift_inv_sort_2 to H1
+ | lapply linear lift_inv_lref_2_gt to H2, H1
+ | lapply nle_nplus to H2 as H. (**)
+ lapply linear nle_trans to H1, H as H0.
+ lapply lift_inv_lref_2_le to H3, H0, H2
+ | lapply linear lift_inv_bind_2 to H5. decompose
+ | lapply linear lift_inv_flat_2 to H5. decompose
+ ]; subst; auto.
+qed.
include "Lift/defs.ma".
+(* Inversion properties *****************************************************)
+
theorem lift_inv_sort_1: \forall l, i, h, x.
Lift l i (leaf (sort h)) x \to
x = leaf (sort h).
| destruct H5. clear H5 H1 H3. subst. auto depth = 5
].
qed.
+
+theorem lift_inv_sort_2: \forall l, i, x, h.
+ Lift l i x (leaf (sort h)) \to
+ x = leaf (sort h).
+ intros. inversion H; clear H; intros;
+ [ auto
+ | destruct H3
+ | destruct H4
+ | destruct H6
+ | destruct H6
+ ].
+qed.
+
+theorem lift_inv_lref_2: \forall l, i, x, j2.
+ Lift l i x (leaf (lref j2)) \to
+ (i > j2 \land x = leaf (lref j2)) \lor
+ (i <= j2 \land
+ \exists j1. (l + j1 == j2) \land x = leaf (lref j1)
+ ).
+ intros. inversion H; clear H; intros;
+ [ destruct H2
+ | destruct H3. clear H3. subst. auto
+ | destruct H4. clear H4. subst. auto depth = 5
+ | destruct H6
+ | destruct H6
+ ].
+qed.
+
+theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
+ Lift l i x (intb r u2 t2) \to
+ \exists u1, t1.
+ Lift l i u1 u2 \land
+ Lift l (succ i) t1 t2 \land
+ x = intb r u1 t1.
+ intros. inversion H; clear H; intros;
+ [ destruct H2
+ | destruct H3
+ | destruct H4
+ | destruct H6. clear H5 H1 H3. subst. auto depth = 5
+ | destruct H6
+ ].
+qed.
+
+theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
+ Lift l i x (intf r u2 t2) \to
+ \exists u1, t1.
+ Lift l i u1 u2 \land
+ Lift l i t1 t2 \land
+ x = intf r u1 t1.
+ intros. inversion H; clear H; intros;
+ [ destruct H2
+ | destruct H3
+ | destruct H4
+ | destruct H6
+ | destruct H6. clear H6 H1 H3. subst. auto depth = 5
+ ].
+qed.
+
+(* Corollaries of inversion properties ***************************************)
+
+theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
+ Lift l i (leaf (lref j1)) x \to
+ i > j1 \to x = leaf (lref j1).
+ intros 5.
+ lapply linear lift_inv_lref_1 to H. decompose; subst;
+ [ auto
+ | lapply linear nle_false to H2, H1. decompose
+ ].
+ qed.
+
+theorem lift_inv_lref_1_le: \forall l, i, j1, x.
+ Lift l i (leaf (lref j1)) x \to
+ i <= j1 \to \forall j2. (l + j1 == j2) \to
+ x = leaf (lref j2).
+ intros 5.
+ lapply linear lift_inv_lref_1 to H. decompose; subst;
+ [ lapply linear nle_false to H1, H3. decompose
+ | lapply linear nplus_mono to H2, H4. subst. auto
+ ].
+qed.
+
+theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
+ Lift l i x (leaf (lref j2)) \to
+ i > j2 \to x = leaf (lref j2).
+ intros 5.
+ lapply linear lift_inv_lref_2 to H. decompose; subst;
+ [ auto
+ | lapply linear nle_false to H2, H1. decompose
+ ].
+ qed.
+
+theorem lift_inv_lref_2_le: \forall l, i, x, j2.
+ Lift l i x (leaf (lref j2)) \to
+ i <= j2 \to \forall j1. (l + j1 == j2) \to
+ x = leaf (lref j1).
+ intros 5.
+ lapply linear lift_inv_lref_2 to H. decompose; subst;
+ [ lapply linear nle_false to H1, H3. decompose
+ | lapply linear nplus_inj_2 to H2, H4. subst. auto
+ ].
+qed.
set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
-include "Lift/inv.ma".
+include "Lift/fun.ma".
-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 5. elim H; clear H i t x;
- [ lapply linear lift_inv_sort_1 to H1.
- subst. auto
- | lapply linear lift_inv_lref_1 to H2.
- decompose; subst;
- [ auto | lapply nle_false to H2, H1. decompose ]
- | lapply linear lift_inv_lref_1 to H3.
- decompose; subst;
- [ 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.
-
-theorem lift_comp_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;
+theorem lift_comp_ge_1: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
+ \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
+ \forall u2. Lift l2 i2 t2 u2 \to
+ i1 >= i2 \to \forall i. (l2 + i1 == i) \to
+ Lift l1 i u1 u2.
+ intros 5. elim H; clear H i1 t1 t2;
[ lapply lift_conf to H1, H2. clear H2. subst.
lapply linear lift_inv_sort_1 to H1.
subst. auto
lapply nle_nplus_comp to H6, H7; auto.
]
]
- |
\ No newline at end of file
+ | clear H1 H3.
+ lapply linear lift_inv_bind_1 to H5.
+ lapply linear lift_inv_bind_1 to H6.
+ decompose. subst. auto width = 4
+ | clear H1 H3.
+ lapply linear lift_inv_flat_1 to H5.
+ lapply linear lift_inv_flat_1 to H6.
+ decompose. subst. auto width = 4
+ ].
+qed.
+
+theorem lift_comp_ge_2: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
+ \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
+ \forall i,u2. Lift l2 i t2 u2 \to
+ i2 >= i1 \to (l1 + i2 == i) \to
+ Lift l1 i1 u1 u2.
+ intros 5. elim H; clear H i1 t1 t2;
+ [ lapply linear lift_inv_sort_1 to H1.
+ lapply linear lift_inv_sort_1 to H2.
+ subst. auto
+ | lapply linear lift_inv_lref_1 to H2.
+ lapply linear lift_inv_lref_1 to H3.
+ decompose; subst; (* clear H2 H4 i2; *)
+ [ clear H H3 H4 H5. auto
+ | clear H1 H4 H7.
+ lapply linear nle_nplus to H5 as H0. (**)
+ lapply linear nle_trans to H3, H0 as H2.
+ lapply nle_false to H, H2. decompose
+ | clear H H5 H6.
+ lapply linear nle_trans to H4, H3 as H.
+ lapply nle_false to H, H1. decompose
+ | clear H H2 H5 H7.
+ lapply linear nle_trans to H4, H3 as H.
+ lapply nle_false to H, H1. decompose
+ ]
+(*
+ | lapply linear lift_inv_lref_1 to H3.
+ decompose; subst;
+ [ clear H2 H4 H6 n3 l2.
+ lapply linear nle_trans to H3, H5 as H0.
+ lapply linear nle_false to H1, H0. decompose
+ | lapply linear lift_inv_lref_1 to H4.
+ decompose; subst;
+ [ clear H1 H5 H6 H7 n1.
+ lapply linear nle_nplus to H2 as H0. (**)
+ lapply linear nle_trans to H3, H0 as H2.
+ lapply linear nle_false to H2, H4. decompose
+ | clear H3 H4 H5.
+ lapply nle_nplus_comp to H6, H7; auto.
+ ]
+ ]
+ | clear H1 H3.
+ lapply linear lift_inv_bind_1 to H5.
+ lapply linear lift_inv_bind_1 to H6.
+ decompose. subst. auto width = 4
+ | clear H1 H3.
+ lapply linear lift_inv_flat_1 to H5.
+ lapply linear lift_inv_flat_1 to H6.
+ decompose. subst. auto width = 4
+ ].
+qed.
+
+
+(*
+theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
+ \forall l2,i2,z. Lift l2 i2 t2 t3 \to
+ i1 <= i2 \to
+ \forall i. \to i2 <= i \to (l1 + i1 == i) \to
+ \forall l. (l1 + l2 == l) \to Lift l i1 t1 t3.
+*)
+axiom lift_conf_back_ge: \forall l1,i1,u1,u2. Lift l1 i1 u1 u2 \to
+ \forall l2,i,t2. Lift l2 i t2 u2 \to
+ \forall i2. i2 >= i1 \to (l1 + i2 == i) \to
+ \exists t1. | Lift l2 i2 t1 u1 \land
+ Lift l1 i1 t1 t2.
+
+*)
+++ /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/LAMBDA-TYPES/Unified-Sub/Term/defs".
-
-(* POLARIZED TERMS
- - Naming policy:
- - natural numbers : sorts h k, local references i j, lengths l o
- - boolean values : p q
- - generic leaf items : m n
- - generic binding items: r s
- - generic flat items : r s
- - generic head items : m n
- - terms : t u
-*)
-
-include "preamble.ma".
-
-inductive Leaf: Set \def
- | sort: Nat \to Leaf
- | lref: Nat \to Leaf
-.
-
-inductive Bind: Set \def
- | abbr: Bind
- | abst: Bind
- | excl: Bind
-.
-
-inductive Flat: Set \def
- | appl: Flat
- | cast: Flat
-.
-
-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
- | intb: IntB \to Term \to Term \to Term
- | intf: IntF \to Term \to Term \to Term
-.
--- /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/LAMBDA-TYPES/Unified-Sub/datatypes/Context".
+
+(* FLAT CONTEXTS
+ - Naming policy:
+ - contexts: c d
+*)
+
+include "datatypes/Term.ma".
+
+inductive Context: Set \def
+ | leaf: Context
+ | intb: Context \to IntB \to Term \to Context
+.
--- /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/LAMBDA-TYPES/Unified-Sub/datatypes/Term".
+
+(* POLARIZED TERMS
+ - Naming policy:
+ - natural numbers : sorts h k, local references i j, lengths l o
+ - boolean values : p q
+ - generic leaf items : m n
+ - generic binding items: r s
+ - generic flat items : r s
+ - generic head items : m n
+ - terms : t u
+*)
+
+include "preamble.ma".
+
+inductive Leaf: Set \def
+ | sort: Nat \to Leaf
+ | lref: Nat \to Leaf
+.
+
+inductive Bind: Set \def
+ | abbr: Bind
+ | abst: Bind
+ | excl: Bind
+.
+
+inductive Flat: Set \def
+ | appl: Flat
+ | cast: Flat
+.
+
+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
+ | intb: IntB \to Term \to Term \to Term
+ | intf: IntF \to Term \to Term \to Term
+.
include "logic/equality.ma".
include "../../RELATIONAL/datatypes/Bool.ma".
-include "../../RELATIONAL/NPlus/props.ma".
+include "../../RELATIONAL/NPlus/monoid.ma".
include "../../RELATIONAL/NLE/props.ma".
include "../../RELATIONAL/NLE/nplus.ma".
--- /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/NPlus/fun".
+
+include "NPlus/inv.ma".
+
+(* Functional properties ****************************************************)
+
+theorem nplus_total: \forall p,q. \exists r. p + q == r.
+ intros 2. elim q; clear q;
+ [ auto | decompose. auto ].
+qed.
+
+theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to
+ \forall r2. (p + q == r2) \to r1 = r2.
+ intros 4. elim H; clear H q r1;
+ [ lapply linear nplus_gen_zero_2 to H1
+ | lapply linear nplus_gen_succ_2 to H3. decompose
+ ]; subst; auto.
+qed.
+
+theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to
+ \forall p2. (p2 + q == r) \to p2 = p1.
+ intros 4. elim H; clear H q r;
+ [ lapply linear nplus_gen_zero_2 to H1
+ | lapply linear nplus_gen_succ_2_3 to H3
+ ]; auto.
+qed.
subst
]; auto new timeout=30.
qed.
+
+theorem nplus_gen_succ_2_3: \forall p,q,r.
+ (p + (succ q) == (succ r)) \to p + q == r.
+ intros.
+ lapply linear nplus_gen_succ_2 to H. decompose. subst.
+ destruct H1. clear H1. subst. auto.
+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/NPlus/monoid".
+
+include "NPlus/fun.ma".
+
+(* Monoidal properties ******************************************************)
+
+theorem nplus_zero_1: \forall q. zero + q == q.
+ intros. elim q; clear q; auto.
+qed.
+
+theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to
+ (succ p) + q == (succ r).
+ intros. elim H; clear H q r; auto.
+qed.
+
+theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r.
+ intros. elim H; clear H q r; auto.
+qed.
+
+(* Corollaries of functional properties **************************************)
+
+theorem nplus_inj_2: \forall p, q1, r. (p + q1 == r) \to
+ \forall q2. (p + q2 == r) \to q1 = q2.
+ intros. auto.
+qed.
+
+(* Corollaries of nonoidal properties ***************************************)
+
+theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to
+ \forall p2,r2. (p2 + q == r2) \to
+ \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
+ intros 4. elim H; clear H q r1;
+ [ lapply linear nplus_gen_zero_2 to H1. subst
+ | lapply linear nplus_gen_succ_2 to H3. decompose. subst.
+ lapply linear nplus_gen_succ_2 to H4. decompose. subst
+ ]; auto.
+qed.
+
+(*
+theorem nplus_shift_succ_sx: \forall p,q,r.
+ (p + (succ q) == r) \to (succ p) + q == r.
+ intros.
+ lapply linear nplus_gen_succ_2 to H as H0.
+ decompose. subst. auto new timeout=100.
+qed.
+
+theorem nplus_shift_succ_dx: \forall p,q,r.
+ ((succ p) + q == r) \to p + (succ q) == r.
+ intros.
+ lapply linear nplus_gen_succ_1 to H as H0.
+ decompose. subst. auto new timeout=100.
+qed.
+
+theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
+ \forall q2,r2. (r1 + q2 == r2) \to
+ \exists q. (q1 + q2 == q) \land p + q == r2.
+ intros 2; elim q1; clear q1; intros;
+ [ lapply linear nplus_gen_zero_2 to H as H0.
+ subst.
+ | lapply linear nplus_gen_succ_2 to H1 as H0.
+ decompose. subst.
+ lapply linear nplus_gen_succ_1 to H2 as H0.
+ decompose. subst.
+ lapply linear H to H4, H3 as H0.
+ decompose.
+ ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
+qed.
+
+theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
+ \forall p2,r2. (p2 + r1 == r2) \to
+ \exists p. (p1 + p2 == p) \land p + q == r2.
+ intros 2; elim q; clear q; intros;
+ [ lapply linear nplus_gen_zero_2 to H as H0.
+ subst
+ | lapply linear nplus_gen_succ_2 to H1 as H0.
+ decompose. subst.
+ lapply linear nplus_gen_succ_2 to H2 as H0.
+ decompose. subst.
+ lapply linear H to H4, H3 as H0.
+ decompose.
+ ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
+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/NPlus/props".
-
-include "NPlus/inv.ma".
-
-(* Monoidal properties *)
-
-theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to
- \forall r2. (p + q == r2) \to r1 = r2.
- intros 4. elim H; clear H q r1;
- [ lapply linear nplus_gen_zero_2 to H1
- | lapply linear nplus_gen_succ_2 to H3. decompose
- ]; subst; auto.
-qed.
-
-theorem nplus_zero_1: \forall q. zero + q == q.
- intros. elim q; clear q; auto.
-qed.
-
-theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to
- (succ p) + q == (succ r).
- intros. elim H; clear H q r; auto.
-qed.
-
-theorem nplus_comm: \forall p,q,r. (p + q == r) \to q + p == r.
- intros. elim H; clear H q r; auto.
-qed.
-
-(* Corollaries *)
-
-theorem nplus_comm_1: \forall p1,q,r1. (p1 + q == r1) \to
- \forall p2,r2. (p2 + q == r2) \to
- \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
- intros 4. elim H; clear H q r1;
- [ lapply linear nplus_gen_zero_2 to H1. subst
- | lapply linear nplus_gen_succ_2 to H3. decompose. subst.
- lapply linear nplus_gen_succ_2 to H4. decompose. subst
- ]; auto.
-qed.
-
-(*
-theorem nplus_shift_succ_sx: \forall p,q,r.
- (p + (succ q) == r) \to (succ p) + q == r.
- intros.
- lapply linear nplus_gen_succ_2 to H as H0.
- decompose. subst. auto new timeout=100.
-qed.
-
-theorem nplus_shift_succ_dx: \forall p,q,r.
- ((succ p) + q == r) \to p + (succ q) == r.
- intros.
- lapply linear nplus_gen_succ_1 to H as H0.
- decompose. subst. auto new timeout=100.
-qed.
-
-theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
- \forall q2,r2. (r1 + q2 == r2) \to
- \exists q. (q1 + q2 == q) \land p + q == r2.
- intros 2; elim q1; clear q1; intros;
- [ lapply linear nplus_gen_zero_2 to H as H0.
- subst.
- | lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose. subst.
- lapply linear nplus_gen_succ_1 to H2 as H0.
- decompose. subst.
- lapply linear H to H4, H3 as H0.
- decompose.
- ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
-qed.
-
-theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
- \forall p2,r2. (p2 + r1 == r2) \to
- \exists p. (p1 + p2 == p) \land p + q == r2.
- intros 2; elim q; clear q; intros;
- [ lapply linear nplus_gen_zero_2 to H as H0.
- subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose. subst.
- lapply linear nplus_gen_succ_2 to H2 as H0.
- decompose. subst.
- lapply linear H to H4, H3 as H0.
- decompose.
- ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
-qed.
-*)
-
set "baseuri" "cic:/matita/RELATIONAL/Zah/setoid".
-include "NPlus/props.ma".
+include "NPlus/monoid.ma".
include "Zah/defs.ma".
theorem nplus_total: \forall p,q. \exists r. p + q == r.
-*)
\ No newline at end of file
+*)
projects / helm.git / commitdiff