(match dec_name with
None -> "_"
| Some n -> n)) ;
- Box.b_text [] ":" ;
+ Box.b_space; Box.b_text [] ":"; Box.b_space;
term2pres ty] in
aux (r::accum) tl
| (Some (`Definition d))::tl ->
[ Box.b_object (p_mi []
(match def_name with
None -> "_"
- | Some n -> n)) ;
- Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
- term2pres bo] in
+ | Some n -> n)) ; Box.b_space ;
+ Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
+ Box.b_space; term2pres bo] in
aux (r::accum) tl
| _::_ -> assert false in
aux [] context in
+++ /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/fwd".
-
-include "Lift/defs.ma".
-
-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 H5
- | destruct H5
- ].
-qed.
-
-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 H1
- | destruct H2. clear H2. subst. auto
- | destruct H3. clear H3. subst. auto depth = 5
- | destruct H5
- | destruct H5
- ].
-qed.
-
-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 H1
- | destruct H2
- | destruct H3
- | destruct H5. clear H5 H1 H3. subst. auto depth = 5
- | destruct H5
- ].
-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.
--- /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/inv".
+
+include "Lift/defs.ma".
+
+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 H5
+ | destruct H5
+ ].
+qed.
+
+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 H1
+ | destruct H2. clear H2. subst. auto
+ | destruct H3. clear H3. subst. auto depth = 5
+ | destruct H5
+ | destruct H5
+ ].
+qed.
+
+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 H1
+ | destruct H2
+ | destruct H3
+ | destruct H5. clear H5 H1 H3. subst. auto depth = 5
+ | destruct H5
+ ].
+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.
set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
-include "Lift/fwd.ma".
+include "Lift/inv.ma".
theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
\forall y. Lift l i t y \to
].
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 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).
+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;
[ lapply lift_conf to H1, H2. clear H2. subst.
lapply linear lift_inv_sort_1 to H1.
| 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.
+ [ lapply linear nle_nplus to H5 as H0. clear l2. (**)
+ lapply linear nle_trans to H1, H0.
auto
- | lapply pippo to H3, H5; [ auto | apply nle_refl | auto ]. (**)
+ | lapply nle_nplus_comp_lt_2 to H3, H5; auto.
+ ]
+ | 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.
+ ]
]
- |
\ No newline at end of file
+ |
\ No newline at end of file
*)
include "logic/equality.ma".
-include "../../RELATIONAL/NPlus/defs.ma".
-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".
+include "../../RELATIONAL/datatypes/Bool.ma".
+include "../../RELATIONAL/NPlus/props.ma".
+include "../../RELATIONAL/NLE/props.ma".
+include "../../RELATIONAL/NLE/nplus.ma".
axiom f_equal_3: \forall (A,B,C,D:Set).
\forall (f:A \to B \to C \to D).
set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs".
-include "datatypes/defs.ma".
+include "datatypes/Nat.ma".
inductive NPlus (p:Nat): Nat \to Nat \to Prop \def
| nplus_zero_2: NPlus p zero p
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 new timeout=100.
+ 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 2. elim q; clear q;
- [ lapply linear nplus_gen_zero_2 to H as H0.
- subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose.
- subst
- ]; auto new timeout=100.
+ intros. elim H; clear H q r; auto.
qed.
-theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
- intros 2. elim q; clear q;
- [ lapply linear nplus_gen_zero_2 to H as H0.
- subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose.
- subst
- ]; auto new timeout=100.
+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.
decompose.
]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
qed.
+*)
-theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to
- \forall r2. (p + q == r2) \to r1 = 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.
- ]; 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/datatypes/Nat".
+
+include "preamble.ma".
+
+inductive Nat: Set \def
+ | zero: Nat
+ | succ: Nat \to Nat
+.
+++ /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/datatypes/Nat".
-
-include "preamble.ma".
-
-inductive Nat: Set \def
- | zero: Nat
- | succ: Nat \to Nat
-.
projects / helm.git / commitdiff