--- /dev/null
+set "baseuri" "cic:/matita/LOGIC/CLE/defs".
+
+(* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS
+*)
+
+include "datatypes/Context.ma".
+
+inductive CLE: Nat \to Context \to Prop \def
+ | cle_zero: \forall Q. CLE zero Q
+ | cle_succ: \forall Q,R,i. CLE i Q \to CLE (succ i) (abst Q R)
+.
+
+interpretation "order relation between positions and contexts"
+ 'leq x y = (cic:/matita/LOGIC/CLE/defs/CLE.ind#xpointer(1/1) x y).
--- /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/LOGIC/Insert/defs".
+
+(* INSERT RELATION FOR CONTEXTS
+*)
+
+include "datatypes/Context.ma".
+
+inductive Insert (S:Sequent): Nat \to Context \to Context \to Prop \def
+ | insert_zero: \forall P. Insert S zero P (abst P S)
+ | insert_succ: \forall P,Q,R,i.
+ Insert S i P Q \to Insert S (succ i) (abst P R) (abst Q R)
+.
--- /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/LOGIC/Insert/fun".
+
+include "CLE/defs.ma".
+include "Insert/inv.ma".
+
+(* Functional properties ****************************************************)
+
+theorem insert_total: \forall S,i,P. i <= P \to \exists Q. Insert S i P Q.
+ intros 4; elim H; clear H i P;
+ decompose; autobatch.
+qed.
+
+theorem insert_inj: \forall S1,i,P, Q. Insert S1 i P Q \to
+ \forall S2. Insert S2 i P Q \to S1 = S2.
+ intros 5; elim H; clear H i P Q;
+ [ lapply linear insert_inv_zero to H1; subst; autobatch
+ | lapply linear insert_inv_succ to H3; decompose; subst; autobatch
+ ].
+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/LOGIC/Insert/inv".
+
+(*
+*)
+
+include "Insert/defs.ma".
+
+theorem insert_inv_zero: \forall S,P,Q. Insert S zero P Q \to Q = abst P S.
+ intros; inversion H; clear H; intros; subst; autobatch.
+qed.
+
+theorem insert_inv_succ: \forall S,Q1,Q2,i. Insert S (succ i) Q1 Q2 \to
+ \exists P1,P2,R. Insert S i P1 P2 \land
+ Q1 = abst P1 R \land Q2 = abst P2 R.
+ intros; inversion H; clear H; intros; subst; autobatch depth = 6 size = 8.
+qed.
+
+theorem insert_inv_leaf_1: \forall Q,S,i. Insert S i leaf Q \to
+ i = zero \land Q = S.
+ intros. inversion H; clear H; intros; subst. autobatch.
+qed.
+
+theorem insert_inv_abst_1: \forall P,Q,R,S,i. Insert S i (abst P R) Q \to
+ (i = zero \land Q = (abst (abst P R) S)) \lor
+ \exists n, c1.
+ i = succ n \land Q = abst c1 R \land
+ Insert S n P c1.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 6 size = 8.
+qed.
+
+theorem insert_inv_leaf_2: \forall P,S,i. Insert S i P leaf \to False.
+ intros. inversion H; clear H; intros; subst.
+qed.
+
+theorem insert_inv_abst_2: \forall P,i. \forall R,S:Sequent.
+ Insert S i P R \to
+ i = zero \land P = leaf \land R = S.
+ intros. inversion H; clear H; intros; subst;
+ [ autobatch
+ | clear H1. lapply linear insert_inv_leaf_2 to H. decompose
+ ].
+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/LOGIC/Insert/props".
+
+(*
+*)
+
+include "Insert/fun.ma".
+
+theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to
+ \forall Q2,S2,i2. Insert S2 i2 P Q2 \to
+ \exists Q,j1,j2.
+ Insert S2 j2 Q1 Q \land Insert S1 j1 Q2 Q.
+ intros 5. elim H; clear H i1 P Q1;
+ [ elim H1; clear H1 i2 c Q2; decompose; autobatch depth = 7 size = 8
+ | lapply linear insert_inv_abst_1 to H3. decompose; subst;
+ [ autobatch depth = 7 size = 8
+ | lapply linear H2 to H4. decompose. subst. autobatch depth = 6 size = 8
+ ]
+ ].
+qed.
+
+theorem insert_trans: \forall P1,Q1,S1,i1. Insert S1 i1 P1 Q1 \to
+ \forall Q2,S2,i2. Insert S2 i2 Q1 Q2 \to
+ \exists P2,j1,j2.
+ Insert S2 j2 P1 P2 \land Insert S1 j1 P2 Q2.
+ intros 5. elim H; clear H i1 P1 Q1;
+ [ lapply linear insert_inv_abst_1 to H1. decompose; subst; autobatch depth = 6 size = 7
+ | lapply linear insert_inv_abst_1 to H3. decompose; subst;
+ [ clear H2. autobatch depth = 7 size = 8
+ | lapply linear H2 to H4. decompose. subst. autobatch depth = 6 size = 8
+ ]
+ ].
+qed.
+
+theorem insert_conf_rev: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to
+ \forall P2,S2,i2. Insert S2 i2 P2 Q \to
+ (i1 = i2 \land P1 = P2) \lor
+ \exists Q1,Q2,j1,j2.
+ Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2.
+ intros 5; elim H; clear H i1 P1 Q;
+ [ inversion H1; clear H1; intros; subst; autobatch depth = 7 size = 8
+ | inversion H3; clear H3; intros; subst;
+ [ autobatch depth = 7 size = 8
+ | clear H3; lapply linear H2 to H; decompose; subst;
+ autobatch depth = 8 size = 10
+ ]
+ ].
+qed.
+
+theorem insert_conf_rev_full: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to
+ \forall P2,S2,i2. Insert S2 i2 P2 Q \to
+ (S1 = S2 \land i1 = i2 \land P1 = P2) \lor
+ \exists Q1,Q2,j1,j2.
+ Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2.
+ intros; lapply insert_conf_rev to H, H1; decompose; subst;
+ [ lapply linear insert_inj to H, H1; subst; autobatch depth = 4
+ | autobatch depth = 7 size = 8
+ ].
+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/LOGIC/Track/defs".
+
+(* PROOF TREE TRACKS
+*)
+
+include "datatypes/Proof.ma".
+include "Insert/defs.ma".
+
+inductive Track: Context \to Proof \to Sequent \to Prop \def
+ | track_proj: \forall P,Q,S,i. Insert S i P Q \to Track Q (lref i) S
+ | track_posr: \forall P,h.
+ Track P (parx h) (pair (posr h) (posr h))
+ | track_impw: \forall P,r,D,a,b. Track P r (pair lleaf D) \to
+ Track P (impw r) (pair (impl a b) D)
+ | track_impi: \forall P,r. \forall a,b:Formula.
+ Track P r (pair a b) \to
+ Track P (impi r) (pair lleaf (impl a b))
+ | track_impe: \forall P,Q,r,D,i. \forall a,b:Formula.
+ Track Q r (pair lleaf D) \to
+ Insert (pair a b) i P Q \to
+ Track P (impe r) (pair (impl a b) D)
+(*
+ | track_impe: \forall P,p,q,r,A,B,D,a,b.
+ Track P p (pair A (rinj a)) \to
+ Track P q (pair (linj b) B) \to
+ Track (abst P (pair A B)) r (pair lleaf D) \to
+ Track P (impe p q r) (pair (linj (impl a b)) D)
+*)
+.
--- /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/LOGIC/Track/inv".
+
+include "Track/defs.ma".
+
+theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to
+ \exists P. Insert S i P Q.
+ intros. inversion H; clear H; intros; subst. autobatch.
+qed.
+
+theorem track_inv_parx: \forall P,S,h. Track P (parx h) S \to
+ S = pair (posr h) (posr h).
+ intros. inversion H; clear H; intros; subst. autobatch.
+qed.
+
+theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
+ \exists B,a,b.
+ S = pair (impl a b) B \land
+ Track P p (pair lleaf B).
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
+qed.
+
+theorem track_inv_impi: \forall P,p,S. Track P (impi p) S \to
+ \exists a,b:Formula.
+ S = pair lleaf (impl a b) \land
+ Track P p (pair a b).
+ intros. inversion H; clear H; intros; subst. autobatch depth = 4.
+qed.
+
+theorem track_inv_impe: \forall P,r,S. Track P (impe r) S \to
+ \exists Q,D,i. \exists a,b:Formula.
+ S = pair (impl a b) D \land
+ Track Q r (pair lleaf D) \land
+ Insert (pair a b) i P Q.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 8 size = 10.
+qed.
+
+theorem track_inv_lleaf_impl:
+ \forall Q,p,a,b. Track Q p (pair lleaf (impl a b)) \to
+ (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor
+ (\exists r. p = impi r \land Track Q r (pair a b)).
+ intros. inversion H; clear H; intros; subst;
+ [ autobatch depth = 5
+ | subst. autobatch depth = 4
+ ].
+qed.
+(*
+theorem track_inv_impe: \forall P,p,q,r,S. Track P (impe p q r) S \to
+ \exists A,B,D. \exists a,b:Formula.
+ S = pair (impl a b) D \land
+ Track P p (pair A a) \land
+ Track P q (pair b B) \land
+ Track (abst P (pair A B)) r (pair lleaf D).
+ intros. inversion H; clear H; intros; subst;
+ [ destruct H2
+ | destruct H1
+ | destruct H3
+ | destruct H3
+ | destruct H7. clear H7. subst. autobatch depth = 9
+ ].
+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/LOGIC/Track/order".
+
+include "Track/props.ma".
+
+(* Order properties *********************************************************)
+
+theorem track_refl: \forall P. \forall c:Formula. \exists r.
+ Track P r (pair c c).
+ intros. elim c; clear c;
+ [ autobatch
+ | lapply (insert_total (pair f f1) zero P); [2:autobatch];
+ decompose. autobatch depth = 5
+ ].
+qed.
+
+theorem track_trans: \forall p,q,A,B. \forall c:Formula.
+ Track leaf p (pair A c) \to Track leaf q (pair c B) \to
+ \exists r. Track leaf r (pair A B).
+ intros 1; elim p names 0; clear p;
+ [ intros. clear H1.
+ lapply linear track_inv_lref to H. decompose.
+ lapply insert_inv_leaf_2 to H. decompose
+ | intros.
+ lapply linear track_inv_parx to H. subst. autobatch.
+ | intros.
+ lapply linear track_inv_impw to H1.
+ decompose. subst.
+ lapply linear H to H4, H2. decompose. autobatch
+ | intros 3. elim q; clear q;
+ [ clear H H1.
+ lapply linear track_inv_lref to H2. decompose.
+ lapply insert_inv_leaf_2 to H. decompose
+ | lapply linear track_inv_parx to H2. subst. autobatch
+ | clear H H1.
+ lapply linear track_inv_impi to H2.
+ lapply linear track_inv_impw to H3.
+ decompose. subst. autobatch
+ | clear H H1 H2.
+ lapply linear track_inv_impi to H3.
+ decompose. subst
+ | clear H H1.
+ lapply linear track_inv_impi to H2.
+ lapply linear track_inv_impe to H3.
+ decompose. subst. autobatch
+ ]
+ | intros 3. elim q; clear q;
+ [ clear H H1.
+ lapply linear track_inv_lref to H2. decompose.
+ lapply insert_inv_leaf_2 to H. decompose
+ | clear H.
+ lapply linear track_inv_parx to H2.
+ subst. autobatch
+ | clear H H1.
+ lapply linear track_inv_impe to H2.
+ lapply linear track_inv_impw to H3.
+ decompose. subst. autobatch
+ | clear H H1 H2.
+ lapply linear track_inv_impi to H3. decompose. subst
+ | clear H H1.
+ lapply linear track_inv_impe to H2.
+ lapply linear track_inv_impe to H3.
+ decompose. subst.
+ lapply linear track_inv_lleaf_impl to H5. decompose; subst;
+ [ clear H4 H6.
+ lapply linear insert_inv_leaf_1 to H3. decompose. subst.
+ lapply linear insert_inv_abst_2 to H2. decompose. subst
+ | lapply insert_conf to H3, H4. clear H4. decompose.
+ lapply linear track_weak to H6, H4. decompose.
+ lapply linear track_comp to H2, H, H1. decompose. autobatch
+ ]
+ ]
+ ].
+qed.
+(*
+ | lapply linear track_inv_impi to H4.
+ lapply linear track_inv_impe to H5.
+ decompose. subst.
+ destruct H4. destruct H5. clear H4 H5. subst.
+ unfold linj in Hcut. unfold rinj in Hcut3. destruct Hcut. destruct Hcut3. clear Hcut Hcut3. subst.
+ destruct Hcut2. clear Hcut2. subst.
+*)
--- /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/LOGIC/Track/props".
+
+include "Insert/props.ma".
+include "Track/inv.ma".
+
+theorem track_weak: \forall R,p,P,Q,S,i.
+ Track P p S \to Insert R i P Q \to
+ \exists q. Track Q q S.
+ intros 2. elim p; clear p;
+ [ lapply linear track_inv_lref to H as H0; decompose;
+ lapply linear insert_trans to H, H1; decompose; autobatch
+ | lapply linear track_inv_parx to H. subst. autobatch
+ | lapply linear track_inv_impw to H1. decompose. subst.
+ lapply linear H to H4, H2. decompose. autobatch
+ | lapply linear track_inv_impi to H1. decompose. subst.
+ lapply linear H to H4, H2. decompose. autobatch
+ | lapply linear track_inv_impe to H1. decompose. subst.
+ lapply linear insert_conf to H2, H4. decompose.
+ lapply linear H to H5, H3. decompose. autobatch
+ ]
+qed.
+
+theorem track_comp: \forall R,q,p,P,Q,S,i.
+ Track P p R \to Track Q q S \to Insert R i P Q \to
+ \exists r. Track P r S.
+ intros 2. elim q; clear q;
+ [ lapply linear track_inv_lref to H1 as H0; decompose;
+ lapply linear insert_conf_rev_full to H1,H2; decompose; subst; autobatch
+ | lapply linear track_inv_parx to H1. subst. autobatch
+ | lapply linear track_inv_impw to H2. decompose. subst.
+ lapply linear H to H1, H5, H3. decompose. autobatch
+ | lapply linear track_inv_impi to H2. decompose. subst.
+ lapply linear H to H1, H5, H3. decompose. autobatch
+ | lapply linear track_inv_impe to H2. decompose. subst.
+ lapply linear insert_trans to H3, H5. decompose.
+ lapply track_weak to H1, H3. clear H1. decompose.
+ lapply linear H to H1, H6, H4. decompose. autobatch
+ ].
+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/LOGIC/datatypes/Context".
+
+(* FLAT CONTEXTS
+ - Naming policy:
+ - contexts: P Q
+*)
+
+include "datatypes/Sequent.ma".
+
+inductive Context: Type \def
+ | leaf: Context
+ | abst: Context \to Sequent \to Context
+.
+
+definition inj: Sequent \to Context \def abst leaf.
+
+coercion cic:/matita/LOGIC/datatypes/Context/inj.con.
--- /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/LOGIC/datatypes/Formula".
+
+(* FORMULAE
+ - Naming policy:
+ - formulae: a b c d
+*)
+
+include "preamble.ma".
+
+inductive Formula: Type \def
+ | posr: Nat \to Formula
+ | impl: Formula \to Formula \to Formula
+.
--- /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/LOGIC/datatypes/Proof".
+
+(* PROOFS
+ - Naming policy:
+ - proofs: p q r s
+*)
+
+include "preamble.ma".
+
+inductive Proof: Type \def
+ | lref: Nat \to Proof
+ | parx: Nat \to Proof
+ | impw: Proof \to Proof
+ | impi: Proof \to Proof
+ | impe: Proof \to Proof
+(*
+ | impe: Proof \to Proof \to Proof \to Proof
+*)
+.
--- /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/LOGIC/datatypes/Sequent".
+
+(* SEQUENTS
+ - Naming policy:
+ - left hand sides (lhs): A C
+ - right hand sides (rhs): B D
+ - sequents : R S
+*)
+
+include "datatypes/Formula.ma".
+
+inductive LHS: Type \def
+ | lleaf: LHS
+ | labst: LHS \to Formula \to LHS
+.
+
+inductive RHS: Type \def
+ | rleaf: RHS
+ | rabst: Formula \to RHS \to RHS
+.
+
+inductive Sequent: Type \def
+ | pair: LHS \to RHS \to Sequent
+.
+
+definition linj: Formula \to LHS \def labst lleaf.
+
+definition rinj: Formula \to RHS \def \lambda b. rabst b rleaf.
+
+coercion cic:/matita/LOGIC/datatypes/Sequent/linj.con.
+
+coercion cic:/matita/LOGIC/datatypes/Sequent/rinj.con.
--- /dev/null
+H=@
+
+RT_BASEDIR=../../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS)
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS)
+
+devel:=$(shell basename `pwd`)
+
+ifneq "$(SRC)" ""
+ XXX="SRC=$(SRC)"
+endif
+
+all: preall
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall.opt
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall.opt
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall.opt
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall.opt
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
+
+preall:
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
+preall.opt:
+ $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* Project started Sat Apr 7, 2007 ****************************************)
+
+set "baseuri" "cic:/matita/LOGIC/preamble".
+
+(* PREAMBLE
+*)
+
+include "../LAMBDA-TYPES/Unified-Sub/preamble.ma".
GOALS = all opt clean clean.opt
-DEVELS = ../library ../legacy RELATIONAL LAMBDA-TYPES
+DEVELS = ../library ../legacy RELATIONAL LOGIC LAMBDA-TYPES
$(GOALS):
@$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;)
software/matita/dama
software/matita/contribs/PREDICATIVE-TOPOLOGY
software/matita/contribs/RELATIONAL
+software/matita/contribs/LOGIC
software/matita/contribs/LAMBDA-TYPES/Unified-Sub
software/matita/contribs/LAMBDA-TYPES/Base-1
software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1
set "baseuri" "cic:/matita/test/prova".
+include "../legacy/coq.ma".
+
+theorem pippo: \forall (A,B:Prop). A \land B \to A.
+ intros; decompose; assumption.
+qed.
+
+inline procedural "cic:/matita/test/prova/pippo.con".
+
+alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+theorem plus_comm: \forall n:nat.\forall m:nat.eq nat (plus n m) (plus m n).
+ intros; alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
+apply plus_comm.
+qed.
+(*
include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
|apply H(* assumption *)
].
qed.
+*)
+(*
+include "nat/orders.ma".
+theorem le_inv:
+ \forall P:nat \to Prop
+ .\forall p2
+ .\forall p1
+ .p2 <= p1 \to
+ (p1 = p2 \to P p2) \to
+ (\forall n1
+ .p2 <= n1 \to
+ (p1 = n1 \to P n1) \to
+ p1 = S n1 \to P (S n1)) \to
+ P p1.
+ intros 4; elim H names 0; clear H p1; intros;
+ [ apply H; reflexivity
+ | apply H3; clear H3; intros;
+ [ apply H | apply H1; clear H1; intros; subst;
+ [ apply H2; apply H3 | ]
+ | reflexivity
+ ]
+*)
projects / helm.git / commitdiff