+++ /dev/null
-include ../Makefile.defs
-
-DIR=$(shell basename $$PWD)
-
-$(DIR) all:
- $(BIN)matitac
-$(DIR).opt opt all.opt:
- $(BIN)matitac.opt
-clean:
- $(BIN)matitaclean
-clean.opt:
- $(BIN)matitaclean.opt
-depend:
- $(BIN)matitadep
-depend.opt:
- $(BIN)matitadep.opt
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/defs.ma".
-
-inductive NLE: Nat \to Nat \to Prop \def
- | nle_zero_1: \forall q. NLE zero q
- | nle_succ_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q)
-.
-
-(*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/datatypes/Nat/Nat.ind#xpointer(1/1/2) x) y).
-
-(*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.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.ind#xpointer(1/1)
- (cic:/matita/RELATIONAL/datatypes/Nat/Nat.ind#xpointer(1/1/2) 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/defs.ma".
-
-theorem nle_inv_succ_1: ∀x,y. x < y →
- ∃z. y = succ z ∧ x ≤ z.
- intros; inversion H; clear H; intros; destruct. autobatch.
-qed.
-
-theorem nle_inv_succ_succ: ∀x,y. x < succ y → x ≤ y.
- intros; inversion H; clear H; intros; destruct. autobatch.
-qed.
-
-theorem nle_inv_succ_zero: ∀x. x < zero → False.
- intros. inversion H; clear H; intros; destruct.
-qed.
-
-theorem nle_inv_zero_2: ∀x. x ≤ zero → x = zero.
- intros; inversion H; clear H; intros; destruct. autobatch.
-qed.
-
-theorem nle_inv_succ_2: ∀y,x. x ≤ succ y →
- x = zero ∨ ∃z. x = succ z ∧ z ≤ y.
- intros; inversion H; clear H; intros; destruct;
- autobatch 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/defs.ma".
-
-theorem nle_nplus: ∀p, q, r. p ⊕ q ≍ r → q ≤ r.
- intros; elim H; clear H q r; autobatch.
-qed.
-
-axiom nle_nplus_comp: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 →
- x1 ≤ y1 → x2 ≤ y2 → x3 ≤ y3.
-
-axiom nle_nplus_comp_lt_2: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 →
- x1 ≤ y1 → x2 < y2 → x3 < y3.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/inv.ma".
-
-theorem nle_refl: ∀x. x ≤ x.
- intros; elim x; clear x; autobatch.
-qed.
-
-theorem nle_trans: ∀x,y. x ≤ y → ∀z. y ≤ z → x ≤ z.
- intros 3; elim H; clear H x y;
- [ autobatch
- | lapply linear nle_inv_succ_1 to H3. decompose. destruct.
- autobatch
- ].
-qed.
-
-theorem nle_false: ∀x,y. x ≤ y → y < x → False.
- intros 3; elim H; clear H x y; autobatch.
-qed.
-
-theorem nle_irrefl: ∀x. x < x → False.
- intros. autobatch.
-qed.
-
-theorem nle_irrefl_ei: ∀x, z. z ≤ x → z = succ x → False.
- intros 3; elim H; clear H x z; destruct; autobatch.
-qed.
-
-theorem nle_irrefl_smart: ∀x. x < x → False.
- intros 1. elim x; clear x; autobatch.
-qed.
-
-theorem nle_lt_or_eq: ∀y, x. x ≤ y → x < y ∨ x = y.
- intros; elim H; clear H x y;
- [ elim n; clear n
- | 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/order.ma".
-
-theorem nle_trans_succ: ∀x,y. x ≤ y → x ≤ succ y.
- intros; elim H; clear H x y; autobatch.
-qed.
-
-theorem nle_gt_or_le: ∀x, y. y > x ∨ y ≤ x.
- intros 2; elim y; clear y;
- [ autobatch
- | decompose;
- [ lapply linear nle_inv_succ_1 to H1
- | lapply linear nle_lt_or_eq to H1
- ]; decompose; destruct; autobatch 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/Nat.ma".
-
-inductive NPlus (p:Nat): Nat → Nat → Prop ≝
- | nplus_zero_2: NPlus p zero p
- | nplus_succ_2: ∀q, r. NPlus p q r → NPlus p (succ q) (succ r).
-
-interpretation "natural plus predicate" 'rel_plus x y z = (NPlus x y z).
-
-notation "hvbox(a break ⊕ b break ≍ c)"
- non associative with precedence 45
-for @{'rel_plus $a $b $c}.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/inv.ma".
-
-(* Functional properties ****************************************************)
-
-theorem nplus_total: ∀p,q. ∃r. p ⊕ q ≍ r.
- intros; elim q; clear q;
- [ autobatch | decompose; autobatch ].
-qed.
-
-theorem nplus_mono: ∀p,q,r1. p ⊕ q ≍ r1 →
- ∀r2. p ⊕ q ≍ r2 → r1 = r2.
- intros 4; elim H; clear H q r1;
- [ lapply linear nplus_inv_zero_2 to H1
- | lapply linear nplus_inv_succ_2 to H3. decompose
- ]; destruct; autobatch.
-qed.
-
-theorem nplus_inj_1: ∀p1, q, r. p1 ⊕ q ≍ r →
- ∀p2. p2 ⊕ q ≍ r → p2 = p1.
- intros 4; elim H; clear H q r;
- [ lapply linear nplus_inv_zero_2 to H1
- | lapply linear nplus_inv_succ_2_3 to H3
- ]; 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/defs.ma".
-
-(* Inversion lemmas *********************************************************)
-
-theorem nplus_inv_zero_1: ∀q,r. zero ⊕ q ≍ r → q = r.
- intros. elim H; clear H q r; autobatch.
-qed.
-
-theorem nplus_inv_succ_1: ∀p,q,r. succ p ⊕ q ≍ r →
- ∃s. r = succ s ∧ p ⊕ q ≍ s.
- intros. elim H; clear H q r; intros;
- [ autobatch depth = 3
- | clear H1; decompose; destruct; autobatch depth = 4
- ]
-qed.
-
-theorem nplus_inv_zero_2: ∀p,r. p ⊕ zero ≍ r → p = r.
- intros; inversion H; clear H; intros; destruct; autobatch.
-qed.
-
-theorem nplus_inv_succ_2: ∀p,q,r. p ⊕ succ q ≍ r →
- ∃s. r = succ s ∧ p ⊕ q ≍ s.
- intros; inversion H; clear H; intros; destruct.
- autobatch depth = 3.
-qed.
-
-theorem nplus_inv_zero_3: ∀p,q. p ⊕ q ≍ zero →
- p = zero ∧ q = zero.
- intros; inversion H; clear H; intros; destruct; autobatch.
-qed.
-
-theorem nplus_inv_succ_3: ∀p,q,r. p ⊕ q ≍ succ r →
- ∃s. p = succ s ∧ s ⊕ q ≍ r ∨
- q = succ s ∧ p ⊕ s ≍ r.
- intros; inversion H; clear H; intros; destruct;
- autobatch depth = 4.
-qed.
-
-(* Corollaries to inversion lemmas ******************************************)
-
-theorem nplus_inv_succ_2_3: ∀p,q,r.
- p ⊕ succ q ≍ succ r → p ⊕ q ≍ r.
- intros;
- lapply linear nplus_inv_succ_2 to H; decompose; destruct; autobatch.
-qed.
-
-theorem nplus_inv_succ_1_3: ∀p,q,r.
- succ p ⊕ q ≍ succ r → p ⊕ q ≍ r.
- intros;
- lapply linear nplus_inv_succ_1 to H; decompose; destruct; autobatch.
-qed.
-
-theorem nplus_inv_eq_2_3: ∀p,q. p ⊕ q ≍ q → p = zero.
- intros 2; elim q; clear q;
- [ lapply linear nplus_inv_zero_2 to H
- | lapply linear nplus_inv_succ_2_3 to H1
- ]; autobatch.
-qed.
-
-theorem nplus_inv_eq_1_3: ∀p,q. p ⊕ q ≍ p → q = zero.
- intros 1; elim p; clear p;
- [ lapply linear nplus_inv_zero_1 to H
- | lapply linear nplus_inv_succ_1_3 to H1
- ]; 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/fun.ma".
-
-(* Monoidal properties ******************************************************)
-
-theorem nplus_zero_1: ∀q. zero ⊕ q ≍ q.
- intros; elim q; clear q; autobatch.
-qed.
-
-theorem nplus_succ_1: ∀p,q,r. p ⊕ q ≍ r → succ p ⊕ q ≍ succ r.
- intros; elim H; clear H q r; autobatch.
-qed.
-
-theorem nplus_comm: ∀p, q, x. p ⊕ q ≍ x → ∀y. q ⊕ p ≍ y → x = y.
- intros 4; elim H; clear H q x;
- [ lapply linear nplus_inv_zero_1 to H1
- | lapply linear nplus_inv_succ_1 to H3. decompose
- ]; destruct; autobatch.
-qed.
-
-theorem nplus_comm_rew: ∀p,q,r. p ⊕ q ≍ r → q ⊕ p ≍ r.
- intros; elim H; clear H q r; autobatch.
-qed.
-
-theorem nplus_ass: ∀p1, p2, r1. p1 ⊕ p2 ≍ r1 → ∀p3, s1. r1 ⊕ p3 ≍ s1 →
- ∀r3. p2 ⊕ p3 ≍ r3 → ∀s3. p1 ⊕ r3 ≍ s3 → s1 = s3.
- intros 4; elim H; clear H p2 r1;
- [ lapply linear nplus_inv_zero_1 to H2. destruct.
- lapply nplus_mono to H1, H3. destruct. autobatch
- | lapply linear nplus_inv_succ_1 to H3. decompose. destruct.
- lapply linear nplus_inv_succ_1 to H4. decompose. destruct.
- lapply linear nplus_inv_succ_2 to H5. decompose. destruct. autobatch
- ].
-qed.
-
-(* Corollaries of functional properties **************************************)
-
-theorem nplus_inj_2: ∀p, q1, r. p ⊕ q1 ≍ r → ∀q2. p ⊕ q2 ≍ r → q1 = q2.
- intros. autobatch.
-qed.
-
-(* Corollaries of nonoidal properties ***************************************)
-
-theorem nplus_comm_1: ∀p1, q, r1. p1 ⊕ q ≍ r1 → ∀p2, r2. p2 ⊕ q ≍ r2 →
- ∀x. p2 ⊕ r1 ≍ x → ∀y. p1 ⊕ r2 ≍ y → x = y.
- intros 4; elim H; clear H q r1;
- [ lapply linear nplus_inv_zero_2 to H1
- | lapply linear nplus_inv_succ_2 to H3.
- lapply linear nplus_inv_succ_2 to H4. decompose. destruct.
- lapply linear nplus_inv_succ_2 to H5. decompose
- ]; destruct; autobatch.
-qed.
-
-theorem nplus_comm_1_rew: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ q ≍ r2 →
- ∀s. p1 ⊕ r2 ≍ s → p2 ⊕ r1 ≍ s.
- intros 4; elim H; clear H q r1;
- [ lapply linear nplus_inv_zero_2 to H1. destruct
- | lapply linear nplus_inv_succ_2 to H3. decompose. destruct.
- lapply linear nplus_inv_succ_2 to H4. decompose. destruct
- ]; autobatch.
-qed.
-
-(*
-theorem nplus_shift_succ_sx: \forall p,q,r.
- (p \oplus (succ q) \asymp r) \to (succ p) \oplus q \asymp r.
- intros.
- lapply linear nplus_inv_succ_2 to H as H0.
- decompose. destruct. auto new timeout=100.
-qed.
-
-theorem nplus_shift_succ_dx: \forall p,q,r.
- ((succ p) \oplus q \asymp r) \to p \oplus (succ q) \asymp r.
- intros.
- lapply linear nplus_inv_succ_1 to H as H0.
- decompose. destruct. auto new timeout=100.
-qed.
-
-theorem nplus_trans_1: \forall p,q1,r1. (p \oplus q1 \asymp r1) \to
- \forall q2,r2. (r1 \oplus q2 \asymp r2) \to
- \exists q. (q1 \oplus q2 \asymp q) \land p \oplus q \asymp r2.
- intros 2; elim q1; clear q1; intros;
- [ lapply linear nplus_inv_zero_2 to H as H0.
- destruct.
- | lapply linear nplus_inv_succ_2 to H1 as H0.
- decompose. destruct.
- lapply linear nplus_inv_succ_1 to H2 as H0.
- decompose. destruct.
- 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: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ r1 ≍ r2 →
- ∃p. p1 ⊕ p2 ≍ p ∧ p ⊕ q ≍ r2.
- intros 2; elim q; clear q; intros;
- [ lapply linear nplus_inv_zero_2 to H as H0.
- destruct
- | lapply linear nplus_inv_succ_2 to H1 as H0.
- decompose. destruct.
- lapply linear nplus_inv_succ_2 to H2 as H0.
- decompose. destruct.
- lapply linear H to H4, H3 as H0.
- decompose.
- ]; autobatch. 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/List.ma".
-include "NPlus/defs.ma".
-
-
-inductive NPlusList: (List Nat) \to Nat \to Prop \def
- | nplus_nil: NPlusList (nil ?) zero
- | nplus_cons: \forall l,p,q,r.
- NPlusList l p \to NPlus p q r \to NPlusList (cons ? l q) r
-.
-
-definition NPlusListEq: (List Nat) \to (List Nat) \to Prop \def
- \lambda ns1,ns2. \exists n. NPlusList ns1 n \land NPlusList ns2 n.
-
-(*
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "ternary natural plus predicate" 'rel_plus3 x y z =
- (cic:/matita/RELATIONAL/NPlus/defs/NPlus3.con w x y z).
-
-notation "hvbox(a break + b break + c == d)"
- non associative with precedence 95
-for @{ 'rel_plus3 $a $b $c $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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlusList/defs.ma".
-(*
-axiom npluslist_gen_cons: \forall l,q,r.
- NPlusList (cons ? l q) r \to
- \exists p. NPlusList l p \land NPlus p q r.
-(*
- intros. inversion H; clear H; intros;
- [ id
- | destruct.
-*)
-
-theorem npluslist_inj_2: \forall ns1,ns2,n.
- NPlusListEq (cons ? ns1 n) (cons ? ns2 n) \to
- NPlusListEq ns1 ns2.
- unfold NPlusListEq. intros. decompose.
- lapply linear npluslist_gen_cons to H. decompose.
- lapply linear npluslist_gen_cons to H2. decompose.
-*)
\ No newline at end of file
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/Zah.ma".
-include "NPlus/defs.ma".
-
-inductive ZEq: Zah → Zah → Prop :=
- | zeq: ∀m1,m2,m3,m4,n. m1 ⊕ m4 ≍ n → m3 ⊕ m2 ≍ n →
- ZEq 〈m1,m2〉 〈m3, m4〉
-.
-
-interpretation "integer equality" 'napart x y = (ZEq 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/fun.ma".
-include "ZEq/defs.ma".
-
-theorem zeq_refl: ∀z. z ≈ z.
- intros; elim z. clear z.
- lapply (nplus_total a b); decompose;
- autobatch.
-qed.
-
-theorem zeq_sym: ∀z1,z2. z1 ≈ z2 → z2 ≈ z1.
- intros; elim H; clear H z1 z2; autobatch.
-qed.
-(*
-theorem zeq_trans: \forall z1,z2. z1 = z2 \to
- \forall z3. z2 = z3 \to z1 = z3.
- intros 3. elim H. clear H z1 z2.
- inversion H3. clear H3. intros. destruct.
- lapply (nplus_total n5 n6). decompose.
- lapply (nplus_total n4 n9). decompose.
- apply zeq.
-*)
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "preamble.ma".
-
-inductive Bool: Type \def
- | false: Bool
- | true : Bool
-.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "preamble.ma".
-
-inductive List (A: Type): Type \def
- | nil: List A
- | cons: List A \to A \to List A
-.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "nil" 'nil =
- (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/1) ?).
-
-notation "hvbox([])"
- non associative with precedence 95
-for @{ 'nil }.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "right cons" 'rcons x y =
- (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/2) ? x y).
-
-notation "hvbox([a break @ b])"
- non associative with precedence 95
-for @{ 'rcons $a $b}.
-
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "preamble.ma".
-
-inductive Nat: Type \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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/Nat.ma".
-
-definition Zah \def Nat \times Nat.
+++ /dev/null
-preamble.ma datatypes/constructors.ma logic/connectives.ma logic/equality.ma
-datatypes/Nat.ma preamble.ma
-datatypes/Zah.ma datatypes/Nat.ma
-datatypes/List.ma preamble.ma
-datatypes/Bool.ma preamble.ma
-ZEq/setoid.ma NPlus/fun.ma ZEq/defs.ma
-ZEq/defs.ma NPlus/defs.ma datatypes/Zah.ma
-NLE/nplus.ma NLE/defs.ma
-NLE/props.ma NLE/order.ma
-NLE/inv.ma NLE/defs.ma
-NLE/defs.ma NPlus/defs.ma datatypes/Nat.ma
-NLE/order.ma NLE/inv.ma
-NPlusList/props.ma NPlusList/defs.ma
-NPlusList/defs.ma NPlus/defs.ma datatypes/List.ma
-NPlus/inv.ma NPlus/defs.ma
-NPlus/monoid.ma NPlus/fun.ma
-NPlus/defs.ma datatypes/Nat.ma
-NPlus/fun.ma NPlus/inv.ma
-datatypes/constructors.ma
-logic/connectives.ma
-logic/equality.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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "logic/equality.ma".
-include "logic/connectives.ma".
-include "datatypes/constructors.ma".
+++ /dev/null
-baseuri=cic:/matita/RELATIONAL
software/matita/tests
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
-software/matita/contribs/LAMBDA-TYPES/Base-2
software/matita/tests
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
-software/matita/contribs/LAMBDA-TYPES/Base-2
+software/matita/contribs/lambdadelta
+++ /dev/null
-include ../Makefile.defs
-
-DIR=$(shell basename $$PWD)
-
-$(DIR) all:
- $(BIN)matitac
-$(DIR).opt opt all.opt:
- $(BIN)matitac.opt
-clean:
- $(BIN)matitaclean
-clean.opt:
- $(BIN)matitaclean.opt
-depend:
- $(BIN)matitadep
-depend.opt:
- $(BIN)matitadep.opt
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/defs.ma".
-
-inductive NLE: Nat \to Nat \to Prop \def
- | nle_zero_1: \forall q. NLE zero q
- | nle_succ_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q)
-.
-
-(*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/datatypes/Nat/Nat.ind#xpointer(1/1/2) x) y).
-
-(*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.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.ind#xpointer(1/1)
- (cic:/matita/RELATIONAL/datatypes/Nat/Nat.ind#xpointer(1/1/2) 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/defs.ma".
-
-theorem nle_inv_succ_1: ∀x,y. x < y →
- ∃z. y = succ z ∧ x ≤ z.
- intros; inversion H; clear H; intros; destruct. autobatch.
-qed.
-
-theorem nle_inv_succ_succ: ∀x,y. x < succ y → x ≤ y.
- intros; inversion H; clear H; intros; destruct. autobatch.
-qed.
-
-theorem nle_inv_succ_zero: ∀x. x < zero → False.
- intros. inversion H; clear H; intros; destruct.
-qed.
-
-theorem nle_inv_zero_2: ∀x. x ≤ zero → x = zero.
- intros; inversion H; clear H; intros; destruct. autobatch.
-qed.
-
-theorem nle_inv_succ_2: ∀y,x. x ≤ succ y →
- x = zero ∨ ∃z. x = succ z ∧ z ≤ y.
- intros; inversion H; clear H; intros; destruct;
- autobatch 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/defs.ma".
-
-theorem nle_nplus: ∀p, q, r. p ⊕ q ≍ r → q ≤ r.
- intros; elim H; clear H q r; autobatch.
-qed.
-
-axiom nle_nplus_comp: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 →
- x1 ≤ y1 → x2 ≤ y2 → x3 ≤ y3.
-
-axiom nle_nplus_comp_lt_2: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 →
- x1 ≤ y1 → x2 < y2 → x3 < y3.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/inv.ma".
-
-theorem nle_refl: ∀x. x ≤ x.
- intros; elim x; clear x; autobatch.
-qed.
-
-theorem nle_trans: ∀x,y. x ≤ y → ∀z. y ≤ z → x ≤ z.
- intros 3; elim H; clear H x y;
- [ autobatch
- | lapply linear nle_inv_succ_1 to H3. decompose. destruct.
- autobatch
- ].
-qed.
-
-theorem nle_false: ∀x,y. x ≤ y → y < x → False.
- intros 3; elim H; clear H x y; autobatch.
-qed.
-
-theorem nle_irrefl: ∀x. x < x → False.
- intros. autobatch.
-qed.
-
-theorem nle_irrefl_ei: ∀x, z. z ≤ x → z = succ x → False.
- intros 3; elim H; clear H x z; destruct; autobatch.
-qed.
-
-theorem nle_irrefl_smart: ∀x. x < x → False.
- intros 1. elim x; clear x; autobatch.
-qed.
-
-theorem nle_lt_or_eq: ∀y, x. x ≤ y → x < y ∨ x = y.
- intros; elim H; clear H x y;
- [ elim n; clear n
- | 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NLE/order.ma".
-
-theorem nle_trans_succ: ∀x,y. x ≤ y → x ≤ succ y.
- intros; elim H; clear H x y; autobatch.
-qed.
-
-theorem nle_gt_or_le: ∀x, y. y > x ∨ y ≤ x.
- intros 2; elim y; clear y;
- [ autobatch
- | decompose;
- [ lapply linear nle_inv_succ_1 to H1
- | lapply linear nle_lt_or_eq to H1
- ]; decompose; destruct; autobatch 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/Nat.ma".
-
-inductive NPlus (p:Nat): Nat → Nat → Prop ≝
- | nplus_zero_2: NPlus p zero p
- | nplus_succ_2: ∀q, r. NPlus p q r → NPlus p (succ q) (succ r).
-
-interpretation "natural plus predicate" 'rel_plus x y z = (NPlus x y z).
-
-notation "hvbox(a break ⊕ b break ≍ c)"
- non associative with precedence 45
-for @{'rel_plus $a $b $c}.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/inv.ma".
-
-(* Functional properties ****************************************************)
-
-theorem nplus_total: ∀p,q. ∃r. p ⊕ q ≍ r.
- intros; elim q; clear q;
- [ autobatch | decompose; autobatch ].
-qed.
-
-theorem nplus_mono: ∀p,q,r1. p ⊕ q ≍ r1 →
- ∀r2. p ⊕ q ≍ r2 → r1 = r2.
- intros 4; elim H; clear H q r1;
- [ lapply linear nplus_inv_zero_2 to H1
- | lapply linear nplus_inv_succ_2 to H3. decompose
- ]; destruct; autobatch.
-qed.
-
-theorem nplus_inj_1: ∀p1, q, r. p1 ⊕ q ≍ r →
- ∀p2. p2 ⊕ q ≍ r → p2 = p1.
- intros 4; elim H; clear H q r;
- [ lapply linear nplus_inv_zero_2 to H1
- | lapply linear nplus_inv_succ_2_3 to H3
- ]; 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/defs.ma".
-
-(* Inversion lemmas *********************************************************)
-
-theorem nplus_inv_zero_1: ∀q,r. zero ⊕ q ≍ r → q = r.
- intros. elim H; clear H q r; autobatch.
-qed.
-
-theorem nplus_inv_succ_1: ∀p,q,r. succ p ⊕ q ≍ r →
- ∃s. r = succ s ∧ p ⊕ q ≍ s.
- intros. elim H; clear H q r; intros;
- [ autobatch depth = 3
- | clear H1; decompose; destruct; autobatch depth = 4
- ]
-qed.
-
-theorem nplus_inv_zero_2: ∀p,r. p ⊕ zero ≍ r → p = r.
- intros; inversion H; clear H; intros; destruct; autobatch.
-qed.
-
-theorem nplus_inv_succ_2: ∀p,q,r. p ⊕ succ q ≍ r →
- ∃s. r = succ s ∧ p ⊕ q ≍ s.
- intros; inversion H; clear H; intros; destruct.
- autobatch depth = 3.
-qed.
-
-theorem nplus_inv_zero_3: ∀p,q. p ⊕ q ≍ zero →
- p = zero ∧ q = zero.
- intros; inversion H; clear H; intros; destruct; autobatch.
-qed.
-
-theorem nplus_inv_succ_3: ∀p,q,r. p ⊕ q ≍ succ r →
- ∃s. p = succ s ∧ s ⊕ q ≍ r ∨
- q = succ s ∧ p ⊕ s ≍ r.
- intros; inversion H; clear H; intros; destruct;
- autobatch depth = 4.
-qed.
-
-(* Corollaries to inversion lemmas ******************************************)
-
-theorem nplus_inv_succ_2_3: ∀p,q,r.
- p ⊕ succ q ≍ succ r → p ⊕ q ≍ r.
- intros;
- lapply linear nplus_inv_succ_2 to H; decompose; destruct; autobatch.
-qed.
-
-theorem nplus_inv_succ_1_3: ∀p,q,r.
- succ p ⊕ q ≍ succ r → p ⊕ q ≍ r.
- intros;
- lapply linear nplus_inv_succ_1 to H; decompose; destruct; autobatch.
-qed.
-
-theorem nplus_inv_eq_2_3: ∀p,q. p ⊕ q ≍ q → p = zero.
- intros 2; elim q; clear q;
- [ lapply linear nplus_inv_zero_2 to H
- | lapply linear nplus_inv_succ_2_3 to H1
- ]; autobatch.
-qed.
-
-theorem nplus_inv_eq_1_3: ∀p,q. p ⊕ q ≍ p → q = zero.
- intros 1; elim p; clear p;
- [ lapply linear nplus_inv_zero_1 to H
- | lapply linear nplus_inv_succ_1_3 to H1
- ]; 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/fun.ma".
-
-(* Monoidal properties ******************************************************)
-
-theorem nplus_zero_1: ∀q. zero ⊕ q ≍ q.
- intros; elim q; clear q; autobatch.
-qed.
-
-theorem nplus_succ_1: ∀p,q,r. p ⊕ q ≍ r → succ p ⊕ q ≍ succ r.
- intros; elim H; clear H q r; autobatch.
-qed.
-
-theorem nplus_comm: ∀p, q, x. p ⊕ q ≍ x → ∀y. q ⊕ p ≍ y → x = y.
- intros 4; elim H; clear H q x;
- [ lapply linear nplus_inv_zero_1 to H1
- | lapply linear nplus_inv_succ_1 to H3. decompose
- ]; destruct; autobatch.
-qed.
-
-theorem nplus_comm_rew: ∀p,q,r. p ⊕ q ≍ r → q ⊕ p ≍ r.
- intros; elim H; clear H q r; autobatch.
-qed.
-
-theorem nplus_ass: ∀p1, p2, r1. p1 ⊕ p2 ≍ r1 → ∀p3, s1. r1 ⊕ p3 ≍ s1 →
- ∀r3. p2 ⊕ p3 ≍ r3 → ∀s3. p1 ⊕ r3 ≍ s3 → s1 = s3.
- intros 4; elim H; clear H p2 r1;
- [ lapply linear nplus_inv_zero_1 to H2. destruct.
- lapply nplus_mono to H1, H3. destruct. autobatch
- | lapply linear nplus_inv_succ_1 to H3. decompose. destruct.
- lapply linear nplus_inv_succ_1 to H4. decompose. destruct.
- lapply linear nplus_inv_succ_2 to H5. decompose. destruct. autobatch
- ].
-qed.
-
-(* Corollaries of functional properties **************************************)
-
-theorem nplus_inj_2: ∀p, q1, r. p ⊕ q1 ≍ r → ∀q2. p ⊕ q2 ≍ r → q1 = q2.
- intros. autobatch.
-qed.
-
-(* Corollaries of nonoidal properties ***************************************)
-
-theorem nplus_comm_1: ∀p1, q, r1. p1 ⊕ q ≍ r1 → ∀p2, r2. p2 ⊕ q ≍ r2 →
- ∀x. p2 ⊕ r1 ≍ x → ∀y. p1 ⊕ r2 ≍ y → x = y.
- intros 4; elim H; clear H q r1;
- [ lapply linear nplus_inv_zero_2 to H1
- | lapply linear nplus_inv_succ_2 to H3.
- lapply linear nplus_inv_succ_2 to H4. decompose. destruct.
- lapply linear nplus_inv_succ_2 to H5. decompose
- ]; destruct; autobatch.
-qed.
-
-theorem nplus_comm_1_rew: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ q ≍ r2 →
- ∀s. p1 ⊕ r2 ≍ s → p2 ⊕ r1 ≍ s.
- intros 4; elim H; clear H q r1;
- [ lapply linear nplus_inv_zero_2 to H1. destruct
- | lapply linear nplus_inv_succ_2 to H3. decompose. destruct.
- lapply linear nplus_inv_succ_2 to H4. decompose. destruct
- ]; autobatch.
-qed.
-
-(*
-theorem nplus_shift_succ_sx: \forall p,q,r.
- (p \oplus (succ q) \asymp r) \to (succ p) \oplus q \asymp r.
- intros.
- lapply linear nplus_inv_succ_2 to H as H0.
- decompose. destruct. auto new timeout=100.
-qed.
-
-theorem nplus_shift_succ_dx: \forall p,q,r.
- ((succ p) \oplus q \asymp r) \to p \oplus (succ q) \asymp r.
- intros.
- lapply linear nplus_inv_succ_1 to H as H0.
- decompose. destruct. auto new timeout=100.
-qed.
-
-theorem nplus_trans_1: \forall p,q1,r1. (p \oplus q1 \asymp r1) \to
- \forall q2,r2. (r1 \oplus q2 \asymp r2) \to
- \exists q. (q1 \oplus q2 \asymp q) \land p \oplus q \asymp r2.
- intros 2; elim q1; clear q1; intros;
- [ lapply linear nplus_inv_zero_2 to H as H0.
- destruct.
- | lapply linear nplus_inv_succ_2 to H1 as H0.
- decompose. destruct.
- lapply linear nplus_inv_succ_1 to H2 as H0.
- decompose. destruct.
- 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: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ r1 ≍ r2 →
- ∃p. p1 ⊕ p2 ≍ p ∧ p ⊕ q ≍ r2.
- intros 2; elim q; clear q; intros;
- [ lapply linear nplus_inv_zero_2 to H as H0.
- destruct
- | lapply linear nplus_inv_succ_2 to H1 as H0.
- decompose. destruct.
- lapply linear nplus_inv_succ_2 to H2 as H0.
- decompose. destruct.
- lapply linear H to H4, H3 as H0.
- decompose.
- ]; autobatch. 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/List.ma".
-include "NPlus/defs.ma".
-
-
-inductive NPlusList: (List Nat) \to Nat \to Prop \def
- | nplus_nil: NPlusList (nil ?) zero
- | nplus_cons: \forall l,p,q,r.
- NPlusList l p \to NPlus p q r \to NPlusList (cons ? l q) r
-.
-
-definition NPlusListEq: (List Nat) \to (List Nat) \to Prop \def
- \lambda ns1,ns2. \exists n. NPlusList ns1 n \land NPlusList ns2 n.
-
-(*
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "ternary natural plus predicate" 'rel_plus3 x y z =
- (cic:/matita/RELATIONAL/NPlus/defs/NPlus3.con w x y z).
-
-notation "hvbox(a break + b break + c == d)"
- non associative with precedence 95
-for @{ 'rel_plus3 $a $b $c $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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlusList/defs.ma".
-(*
-axiom npluslist_gen_cons: \forall l,q,r.
- NPlusList (cons ? l q) r \to
- \exists p. NPlusList l p \land NPlus p q r.
-(*
- intros. inversion H; clear H; intros;
- [ id
- | destruct.
-*)
-
-theorem npluslist_inj_2: \forall ns1,ns2,n.
- NPlusListEq (cons ? ns1 n) (cons ? ns2 n) \to
- NPlusListEq ns1 ns2.
- unfold NPlusListEq. intros. decompose.
- lapply linear npluslist_gen_cons to H. decompose.
- lapply linear npluslist_gen_cons to H2. decompose.
-*)
\ No newline at end of file
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/Zah.ma".
-include "NPlus/defs.ma".
-
-inductive ZEq: Zah → Zah → Prop :=
- | zeq: ∀m1,m2,m3,m4,n. m1 ⊕ m4 ≍ n → m3 ⊕ m2 ≍ n →
- ZEq 〈m1,m2〉 〈m3, m4〉
-.
-
-interpretation "integer equality" 'napart x y = (ZEq 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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "NPlus/fun.ma".
-include "ZEq/defs.ma".
-
-theorem zeq_refl: ∀z. z ≈ z.
- intros; elim z. clear z.
- lapply (nplus_total a b); decompose;
- autobatch.
-qed.
-
-theorem zeq_sym: ∀z1,z2. z1 ≈ z2 → z2 ≈ z1.
- intros; elim H; clear H z1 z2; autobatch.
-qed.
-(*
-theorem zeq_trans: \forall z1,z2. z1 = z2 \to
- \forall z3. z2 = z3 \to z1 = z3.
- intros 3. elim H. clear H z1 z2.
- inversion H3. clear H3. intros. destruct.
- lapply (nplus_total n5 n6). decompose.
- lapply (nplus_total n4 n9). decompose.
- apply zeq.
-*)
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "preamble.ma".
-
-inductive Bool: Type \def
- | false: Bool
- | true : Bool
-.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "preamble.ma".
-
-inductive List (A: Type): Type \def
- | nil: List A
- | cons: List A \to A \to List A
-.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "nil" 'nil =
- (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/1) ?).
-
-notation "hvbox([])"
- non associative with precedence 95
-for @{ 'nil }.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "right cons" 'rcons x y =
- (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/2) ? x y).
-
-notation "hvbox([a break @ b])"
- non associative with precedence 95
-for @{ 'rcons $a $b}.
-
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "preamble.ma".
-
-inductive Nat: Type \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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "datatypes/Nat.ma".
-
-definition Zah \def Nat \times Nat.
+++ /dev/null
-preamble.ma datatypes/constructors.ma logic/connectives.ma logic/equality.ma
-datatypes/Nat.ma preamble.ma
-datatypes/Zah.ma datatypes/Nat.ma
-datatypes/List.ma preamble.ma
-datatypes/Bool.ma preamble.ma
-ZEq/setoid.ma NPlus/fun.ma ZEq/defs.ma
-ZEq/defs.ma NPlus/defs.ma datatypes/Zah.ma
-NLE/nplus.ma NLE/defs.ma
-NLE/props.ma NLE/order.ma
-NLE/inv.ma NLE/defs.ma
-NLE/defs.ma NPlus/defs.ma datatypes/Nat.ma
-NLE/order.ma NLE/inv.ma
-NPlusList/props.ma NPlusList/defs.ma
-NPlusList/defs.ma NPlus/defs.ma datatypes/List.ma
-NPlus/inv.ma NPlus/defs.ma
-NPlus/monoid.ma NPlus/fun.ma
-NPlus/defs.ma datatypes/Nat.ma
-NPlus/fun.ma NPlus/inv.ma
-datatypes/constructors.ma
-logic/connectives.ma
-logic/equality.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 *)
-(* *)
-(**************************************************************************)
-
-
-
-include "logic/equality.ma".
-include "logic/connectives.ma".
-include "datatypes/constructors.ma".
+++ /dev/null
-baseuri=cic:/matita/RELATIONAL
software/matita/tests
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
-software/matita/contribs/LAMBDA-TYPES/Base-2
projects / helm.git / commitdiff