include "logic/equality.ma".
-include "BNot/defs.ma".
+include "Bool/defs.ma".
-inductive BEq (b1:Bool): Bool \to Bool \to Prop \def
- | beq_false: \forall b2. (~b1 == b2) \to BEq b1 false b2
- | beq_true : BEq b1 true b1
+inductive BEq (A:Type) (a1:A): A \to Bool \to Prop \def
+ | beq_true : BEq A a1 a1 true
+ | beq_false: \forall a2. (a1 = a2 -> False) \to BEq A a1 a2 false
.
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "boolean coimplication predicate" 'rel_coimp x y z =
- (cic:/matita/RELATIONAL/BEq/defs/BEq.ind#xpointer(1/1) x y z).
+interpretation "boolean equality" 'beq x y z =
+ (cic:/matita/RELATIONAL/BEq/defs/BEq.ind#xpointer(1/1) _ x y z).
-notation "hvbox(a break * b break == c)"
+notation "hvbox(a break -- b break == c)"
non associative with precedence 95
-for @{ 'rel_coimp $a $b $c}.
+for @{ 'beq $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 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/RELATIONAL/BNot/defs".
-
-include "logic/equality.ma".
-
-include "Bool/defs.ma".
-
-inductive BNot: Bool \to Bool \to Prop \def
- | bnot_false: BNot false true
- | bnot_true : BNot true false
-.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "boolean not predicate" 'rel_not x y =
- (cic:/matita/RELATIONAL/BNot/defs/BNot.ind#xpointer(1/1) x y).
-
-(* FG: we can not use - here for some reason *)
-notation "hvbox(~ a break == b)"
- non associative with precedence 95
-for @{ 'rel_not $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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/List/defs".
+
+inductive List (A:Set): Set \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/List/defs/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/List/defs/List.ind#xpointer(1/2) _ x y).
+
+notation "hvbox([a break @ b])"
+ non associative with precedence 95
+for @{ 'rcons $a $b}.
+
set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs".
include "logic/equality.ma".
-
include "Nat/defs.ma".
inductive NPlus (p:Nat): Nat \to Nat \to Prop \def
interpretation "natural plus predicate" 'rel_plus x y z =
(cic:/matita/RELATIONAL/NPlus/defs/NPlus.ind#xpointer(1/1) x y z).
-notation "hvbox(a break + b break == c)"
+notation "hvbox(a break + b break == c)"
non associative with precedence 95
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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/NPlusList/defs".
+
+include "List/defs.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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/NPlusList/props".
+
+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
+ | subst.
+*)
+
+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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/Zah/defs".
+
+include "datatypes/constructors.ma".
+include "logic/coimplication.ma".
+include "NPlusList/defs.ma".
+
+definition Zah \def Nat \times Nat.
+
+definition ZEq: Zah \to Zah -> Prop :=
+ \lambda z1,z2.
+ \forall n. ((\fst z1) + (\snd z2) == n) \liff (\fst z2) + (\snd z1) == n.
+
+interpretation "integer equality" 'zeq x y =
+ (cic:/matita/RELATIONAL/Zah/defs/ZEq.con x y).
+
+notation "hvbox(a break = b)"
+ non associative with precedence 45
+for @{ 'zeq $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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/Zah/setoid".
+
+include "NPlus/props.ma".
+include "Zah/defs.ma".
+
+theorem nplus_total: \forall p,q. \exists r. p + q == r.
+ intros 2. elim q; clear q;
+ decompose; auto.
+qed.
+
+theorem zeq_intro: \forall z1,z2.
+ (\forall n.((\fst z1) + (\snd z2) == n) \to ((\fst z2) + (\snd z1) == n)) \to
+ (\forall n.((\fst z2) + (\snd z1) == n) \to ((\fst z1) + (\snd z2) == n)) \to
+ z1 = z2.
+ unfold ZEq. intros. apply iff_intro; intros; auto.
+qed.
+
+theorem zeq_refl: \forall z. z = z.
+ unfold ZEq. intros. auto.
+qed.
+
+theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
+ unfold ZEq. intros. lapply linear (H n). auto.
+qed.
+(*
+theorem zeq_trans: \forall z1,z2. z1 = z2 \to
+ \forall z3. z2 = z3 \to z1 = z3.
+ unfold ZEq. intros.
+ lapply (nplus_total (\snd z2) (\fst z2)). decompose.
+
+
+
+ apply iff_intro; intros;
+ [ lapply (nplus_total (\fst z1) (\snd z3)). decompose
+ |
+
+
+
+
+ lapply (nplus_total (\snd z2) (\fst z2)). decompose.
+ lapply (nplus_total n a). decompose.
+ lapply linear (H a1). lapply linear (H1 a1). decompose.
+
+
+
+*)
\ No newline at end of file
projects / helm.git / commitdiff