From 71590f4a0cb620a5e98fee3e8d65670271234532 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 25 Jul 2005 21:39:27 +0000 Subject: [PATCH] More notation (up to where the open bugs allow me to put it without adding too many aliases). --- helm/matita/library/Z/orders.ma | 39 +++++++++++++++--------- helm/matita/library/Z/z.ma | 5 ++- helm/matita/library/datatypes/bool.ma | 3 ++ helm/matita/library/logic/connectives.ma | 6 ++++ helm/matita/library/logic/equality.ma | 2 ++ helm/matita/library/nat/minus.ma | 1 + helm/matita/library/nat/orders.ma | 5 ++- helm/matita/library/nat/plus.ma | 2 +- helm/matita/library/nat/times.ma | 1 + 9 files changed, 46 insertions(+), 18 deletions(-) diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma index 1a2d65a4f..60c727ceb 100644 --- a/helm/matita/library/Z/orders.ma +++ b/helm/matita/library/Z/orders.ma @@ -35,6 +35,10 @@ definition Zle : Z \to Z \to Prop \def | (pos m) \Rightarrow True | (neg m) \Rightarrow (le m n) ]]. +(*CSC: the URI must disappear: there is a bug now *) +interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y). +(*CSC: this alias must disappear: there is a bug in the generation of the .moos *) +alias symbol "leq" (instance 0) = "integer 'less or equal to'". definition Zlt : Z \to Z \to Prop \def \lambda x,y:Z. @@ -55,12 +59,17 @@ definition Zlt : Z \to Z \to Prop \def | (pos m) \Rightarrow True | (neg m) \Rightarrow (lt m n) ]]. +(*CSC: the URI must disappear: there is a bug now *) +interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y). +(*CSC: this alias must disappear: there is a bug in the generation of the .moos *) +alias symbol "lt" (instance 0) = "integer 'less than'". + theorem irreflexive_Zlt: irreflexive Z Zlt. -change with \forall x:Z. Zlt x x \to False. +change with \forall x:Z. x < x \to False. intro.elim x.exact H. -cut (Zlt (neg n) (neg n)) \to False. +cut neg n < neg n \to False. apply Hcut.apply H.simplify.apply not_le_Sn_n. -cut (Zlt (pos n) (pos n)) \to False. +cut pos n < pos n \to False. apply Hcut.apply H.simplify.apply not_le_Sn_n. qed. @@ -87,30 +96,30 @@ definition Z_compare : Z \to Z \to compare \def | (neg m) \Rightarrow nat_compare m n ]]. theorem Zlt_neg_neg_to_lt: -\forall n,m:nat. Zlt (neg n) (neg m) \to lt m n. +\forall n,m:nat. neg n < neg m \to lt m n. intros.apply H. qed. -theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to Zlt (neg n) (neg m). +theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m. intros. simplify.apply H. qed. theorem Zlt_pos_pos_to_lt: -\forall n,m:nat. Zlt (pos n) (pos m) \to lt n m. +\forall n,m:nat. pos n < pos m \to lt n m. intros.apply H. qed. -theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to Zlt (pos n) (pos m). +theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m. intros. simplify.apply H. qed. theorem Z_compare_to_Prop : \forall x,y:Z. match (Z_compare x y) with -[ LT \Rightarrow (Zlt x y) -| EQ \Rightarrow (eq Z x y) -| GT \Rightarrow (Zlt y x)]. +[ LT \Rightarrow x < y +| EQ \Rightarrow x=y +| GT \Rightarrow y < x]. intros. elim x. elim y. simplify.apply refl_eq. @@ -150,20 +159,20 @@ simplify.exact H. simplify.apply eq_f.exact H. qed. -theorem Zlt_to_Zle: \forall x,y:Z. Zlt x y \to Zle (Zsucc x) y. +theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y. intros 2.elim x. -cut (Zlt OZ y) \to (Zle (Zsucc OZ) y). +cut OZ < y \to Zsucc OZ \leq y. apply Hcut. assumption.simplify.elim y. simplify.exact H1. simplify.exact H1. simplify.apply le_O_n. -cut (Zlt (neg n) y) \to (Zle (Zsucc (neg n)) y). +cut neg n < y \to Zsucc (neg n) \leq y. apply Hcut. assumption.elim n. -cut (Zlt (neg O) y) \to (Zle (Zsucc (neg O)) y). +cut neg O < y \to Zsucc (neg O) \leq y. apply Hcut. assumption.simplify.elim y. simplify.exact I.simplify.apply not_le_Sn_O n1 H2. simplify.exact I. -cut (Zlt (neg (S n1)) y) \to (Zle (Zsucc (neg (S n1))) y). +cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y. apply Hcut. assumption.simplify. elim y. simplify.exact I. diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index 9dffcee52..da249902b 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -123,8 +123,11 @@ definition Zplus :Z \to Z \to Z \def | EQ \Rightarrow OZ | GT \Rightarrow (neg (pred (minus m n)))] | (neg n) \Rightarrow (neg (S (plus m n)))]]. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y). -theorem Zplus_z_OZ: \forall z:Z. eq Z (Zplus z OZ) z. +theorem Zplus_z_OZ: \forall z:Z. Zplus z OZ = z. intro.elim z. simplify.reflexivity. simplify.reflexivity. diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma index 8267aa7f6..cac5ebbe9 100644 --- a/helm/matita/library/datatypes/bool.ma +++ b/helm/matita/library/datatypes/bool.ma @@ -24,6 +24,7 @@ definition notb : bool \to bool \def [ true \Rightarrow false | false \Rightarrow true ]. +(*CSC: the URI must disappear: there is a bug now *) interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x). definition andb : bool \to bool \to bool\def @@ -33,6 +34,7 @@ definition andb : bool \to bool \to bool\def match b2 with [true \Rightarrow true | false \Rightarrow false] | false \Rightarrow false ]. +(*CSC: the URI must disappear: there is a bug now *) interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y). definition orb : bool \to bool \to bool\def @@ -42,6 +44,7 @@ definition orb : bool \to bool \to bool\def match b2 with [true \Rightarrow true | false \Rightarrow false] | false \Rightarrow false ]. +(*CSC: the URI must disappear: there is a bug now *) interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y). definition if_then_else : bool \to Prop \to Prop \to Prop \def diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma index 5a1ad1fdd..dacf542af 100644 --- a/helm/matita/library/logic/connectives.ma +++ b/helm/matita/library/logic/connectives.ma @@ -26,7 +26,9 @@ default "false" cic:/matita/logic/connectives/False.ind. definition Not: Prop \to Prop \def \lambda A. (A \to False). +(*CSC: the URI must disappear: there is a bug now *) interpretation "logical not" 'not x = (cic:/matita/logic/connectives/Not.con x). +(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *) alias symbol "not" (instance 0) = "logical not". theorem absurd : \forall A,C:Prop. A \to \lnot A \to C. @@ -38,7 +40,9 @@ default "absurd" cic:/matita/logic/connectives/absurd.con. inductive And (A,B:Prop) : Prop \def conj : A \to B \to (And A B). +(*CSC: the URI must disappear: there is a bug now *) interpretation "logical and" 'and x y = (cic:/matita/logic/connectives/And.ind#xpointer(1/1) x y). +(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *) alias symbol "and" (instance 0) = "logical and". theorem proj1: \forall A,B:Prop. A \land B \to A. @@ -53,7 +57,9 @@ inductive Or (A,B:Prop) : Prop \def or_introl : A \to (Or A B) | or_intror : B \to (Or A B). +(*CSC: the URI must disappear: there is a bug now *) interpretation "logical or" 'or x y = (cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y). +(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *) alias symbol "or" (instance 0) = "logical or". definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A. diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma index 87fe22bac..77ef0eb82 100644 --- a/helm/matita/library/logic/equality.ma +++ b/helm/matita/library/logic/equality.ma @@ -19,8 +19,10 @@ include "higher_order_defs/relations.ma". inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x. +(*CSC: the URI must disappear: there is a bug now *) interpretation "leibnitz's equality" 'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y). +(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *) alias symbol "eq" (instance 0) = "leibnitz's equality". diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 7ba20e821..e725185e0 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -26,6 +26,7 @@ let rec minus n m \def [O \Rightarrow (S p) | (S q) \Rightarrow minus p q ]]. +(*CSC: the URI must disappear: there is a bug now *) interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y). theorem minus_n_O: \forall n:nat.n=n-O. diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index 5389418b5..d269e5fe1 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -22,22 +22,25 @@ inductive le (n:nat) : nat \to Prop \def | le_n : le n n | le_S : \forall m:nat. le n m \to le n (S m). +(*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y). -alias symbol "leq" (instance 0) = "natural 'less or equal to'". definition lt: nat \to nat \to Prop \def \lambda n,m:nat.(S n) \leq m. +(*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y). definition ge: nat \to nat \to Prop \def \lambda n,m:nat.m \leq n. +(*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y). definition gt: nat \to nat \to Prop \def \lambda n,m:nat.m