From 42c44d828983e4ea2d115eba20a8020b62108384 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 23 Aug 2008 19:12:21 +0000 Subject: [PATCH] Some notation moved to core_notation. A few new things in datatypes/subsets and related stuff. --- helm/software/matita/core_notation.moo | 9 ++ .../matita/library/datatypes/subsets.ma | 95 +++++++++++++++++++ .../matita/library/logic/coimplication.ma | 11 +-- .../matita/library/logic/cprop_connectives.ma | 7 ++ 4 files changed, 112 insertions(+), 10 deletions(-) diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 1ea2f922b..9891129af 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -137,6 +137,15 @@ notation "hvbox(\lnot a)" non associative with precedence 40 for @{ 'not $a }. +notation > "hvbox(a break \liff b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +notation "hvbox(a break \leftrightarrow b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + + notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70 for @{ 'powerset $A }. diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma index f9fae64a0..96ec347c7 100644 --- a/helm/software/matita/library/datatypes/subsets.ma +++ b/helm/software/matita/library/datatypes/subsets.ma @@ -40,6 +40,101 @@ definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}. interpretation "union" 'union U V = (union _ U V). +record ssigma (A:Type) (S: powerset A) : Type ≝ + { witness:> A; + proof:> witness ∈ S + }. + +coercion ssigma. + +record binary_relation (A,B: Type) (U: Ω \sup A) (V: Ω \sup B) : Type ≝ + { satisfy:2> U → V → CProp }. + +(*notation < "hvbox (x (\circ term 19 r \frac \nbsp \circ) y)" with precedence 45 for @{'satisfy $r $x $y}.*) +notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}. +notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}. +interpretation "relation applied" 'satisfy r x y = (satisfy ____ r x y). + +definition composition: + ∀A,B,C.∀U1: Ω \sup A.∀U2: Ω \sup B.∀U3: Ω \sup C. + binary_relation ?? U1 U2 → binary_relation ?? U2 U3 → + binary_relation ?? U1 U3. + intros (A B C U1 U2 U3 R12 R23); + constructor 1; + intros (s1 s3); + apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3); +qed. + +interpretation "binary relation composition" 'compose x y = (composition ______ x y). + +definition equal_relations ≝ + λA,B,U,V.λr,r': binary_relation A B U V. + ∀x,y. r x y ↔ r' x y. + +interpretation "equal relation" 'eq x y = (equal_relations ____ x y). + +lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V). + intros 5; intros 2; split; intro; assumption. +qed. + +lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V). + intros 7; intros 2; split; intro; + [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption. +qed. + +lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V). + intros 9; intros 2; split; intro; + [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ] + [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ] + assumption. +qed. + +lemma equal_morphism: + ∀A,B,U,V.∀r1,r1',r2,r2':binary_relation A B U V. + r1' = r1 → r2 = r2' → r1 = r2 → r1' = r2'. + intros 13; + split; intro; + [ apply (if ?? (H1 ??)); + apply (if ?? (H2 ??)); + apply (if ?? (H ??)); + assumption + | apply (fi ?? (H ??)); + apply (fi ?? (H2 ??)); + apply (fi ?? (H1 ??)); + assumption + ] +qed. + +lemma associative_composition: + ∀A,B,C,D.∀U1,U2,U3,U4. + ∀r1:binary_relation A B U1 U2. + ∀r2:binary_relation B C U2 U3. + ∀r3:binary_relation C D U3 U4. + (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3). + intros 13; + split; intro; + cases H; clear H; cases H1; clear H1; + [cases H; clear H | cases H2; clear H2] + cases H1; clear H1; + exists; try assumption; + split; try assumption; + exists; try assumption; + split; assumption. +qed. + +lemma composition_morphism: + ∀A,B,C.∀U1,U2,U3. + ∀r1,r1':binary_relation A B U1 U2. + ∀r2,r2':binary_relation B C U2 U3. + r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'. + intros 14; split; intro; + cases H2; clear H2; cases H3; clear H3; + [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ] + [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ] + exists; try assumption; + split; assumption. +qed. + include "logic/equality.ma". definition singleton ≝ λA:Type.λa:A.{b | a=b}. diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma index a8fc4a232..67f04b903 100644 --- a/helm/software/matita/library/logic/coimplication.ma +++ b/helm/software/matita/library/logic/coimplication.ma @@ -17,16 +17,7 @@ include "logic/connectives.ma". definition Iff : Prop \to Prop \to Prop \def \lambda A,B. (A \to B) \land (B \to A). - (*CSC: the URI must disappear: there is a bug now *) -interpretation "logical iff" 'iff x y = (cic:/matita/logic/coimplication/Iff.con x y). - -notation > "hvbox(a break \liff b)" - left associative with precedence 25 -for @{ 'iff $a $b }. - -notation < "hvbox(a break \leftrightarrow b)" - left associative with precedence 25 -for @{ 'iff $a $b }. +interpretation "logical iff" 'iff x y = (Iff x y). theorem iff_intro: \forall A,B. (A \to B) \to (B \to A) \to (A \liff B). unfold Iff. intros. split; intros; autobatch. diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma index 3b43ef399..c0bbdda18 100644 --- a/helm/software/matita/library/logic/cprop_connectives.ma +++ b/helm/software/matita/library/logic/cprop_connectives.ma @@ -58,6 +58,13 @@ notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t). +record Iff (A,B:CProp) : CProp ≝ + { if: A → B; + fi: B → A + }. + +interpretation "logical iff" 'iff x y = (Iff x y). + inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. -- 2.39.2