From f9ef8e5bc536042ad4a3ece108337c98231d4173 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 19 Jan 2007 14:30:00 +0000 Subject: [PATCH] some updates --- matita/contribs/RELATIONAL/BEq/defs.ma | 16 ++--- .../RELATIONAL/{BNot => List}/defs.ma | 28 +++++---- matita/contribs/RELATIONAL/NPlus/defs.ma | 3 +- matita/contribs/RELATIONAL/NPlusList/defs.ma | 38 ++++++++++++ matita/contribs/RELATIONAL/NPlusList/props.ma | 34 +++++++++++ matita/contribs/RELATIONAL/Zah/defs.ma | 32 ++++++++++ matita/contribs/RELATIONAL/Zah/setoid.ma | 60 +++++++++++++++++++ 7 files changed, 189 insertions(+), 22 deletions(-) rename matita/contribs/RELATIONAL/{BNot => List}/defs.ma (67%) create mode 100644 matita/contribs/RELATIONAL/NPlusList/defs.ma create mode 100644 matita/contribs/RELATIONAL/NPlusList/props.ma create mode 100644 matita/contribs/RELATIONAL/Zah/defs.ma create mode 100644 matita/contribs/RELATIONAL/Zah/setoid.ma diff --git a/matita/contribs/RELATIONAL/BEq/defs.ma b/matita/contribs/RELATIONAL/BEq/defs.ma index d851a6b9f..3ab3b002e 100644 --- a/matita/contribs/RELATIONAL/BEq/defs.ma +++ b/matita/contribs/RELATIONAL/BEq/defs.ma @@ -16,17 +16,17 @@ set "baseuri" "cic:/matita/RELATIONAL/BEq/defs". 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}. diff --git a/matita/contribs/RELATIONAL/BNot/defs.ma b/matita/contribs/RELATIONAL/List/defs.ma similarity index 67% rename from matita/contribs/RELATIONAL/BNot/defs.ma rename to matita/contribs/RELATIONAL/List/defs.ma index 401e599a7..435d72365 100644 --- a/matita/contribs/RELATIONAL/BNot/defs.ma +++ b/matita/contribs/RELATIONAL/List/defs.ma @@ -12,22 +12,26 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/BNot/defs". +set "baseuri" "cic:/matita/RELATIONAL/List/defs". -include "logic/equality.ma". +inductive List (A:Set): Set \def + | nil: List A + | cons: List A \to A \to List A +. -include "Bool/defs.ma". +(*CSC: the URI must disappear: there is a bug now *) +interpretation "nil" 'nil = + (cic:/matita/RELATIONAL/List/defs/List.ind#xpointer(1/1) _). -inductive BNot: Bool \to Bool \to Prop \def - | bnot_false: BNot false true - | bnot_true : BNot true false -. +notation "hvbox([])" + non associative with precedence 95 +for @{ 'nil }. (*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). +interpretation "right cons" 'rcons x y = + (cic:/matita/RELATIONAL/List/defs/List.ind#xpointer(1/2) _ x y). -(* FG: we can not use - here for some reason *) -notation "hvbox(~ a break == b)" +notation "hvbox([a break @ b])" non associative with precedence 95 -for @{ 'rel_not $a $b}. +for @{ 'rcons $a $b}. + diff --git a/matita/contribs/RELATIONAL/NPlus/defs.ma b/matita/contribs/RELATIONAL/NPlus/defs.ma index 289093403..a335b26ed 100644 --- a/matita/contribs/RELATIONAL/NPlus/defs.ma +++ b/matita/contribs/RELATIONAL/NPlus/defs.ma @@ -15,7 +15,6 @@ 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 @@ -26,6 +25,6 @@ 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}. diff --git a/matita/contribs/RELATIONAL/NPlusList/defs.ma b/matita/contribs/RELATIONAL/NPlusList/defs.ma new file mode 100644 index 000000000..a07889405 --- /dev/null +++ b/matita/contribs/RELATIONAL/NPlusList/defs.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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}. +*) diff --git a/matita/contribs/RELATIONAL/NPlusList/props.ma b/matita/contribs/RELATIONAL/NPlusList/props.ma new file mode 100644 index 000000000..3f53d92cf --- /dev/null +++ b/matita/contribs/RELATIONAL/NPlusList/props.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/matita/contribs/RELATIONAL/Zah/defs.ma b/matita/contribs/RELATIONAL/Zah/defs.ma new file mode 100644 index 000000000..2f9e42d4d --- /dev/null +++ b/matita/contribs/RELATIONAL/Zah/defs.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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 }. diff --git a/matita/contribs/RELATIONAL/Zah/setoid.ma b/matita/contribs/RELATIONAL/Zah/setoid.ma new file mode 100644 index 000000000..8815ee5bb --- /dev/null +++ b/matita/contribs/RELATIONAL/Zah/setoid.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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 -- 2.39.2