From 0e50062a04d72b333403d633a77dd113b32d6784 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Jul 2008 14:16:17 +0000 Subject: [PATCH] better notation --- .../matita/library/demo/formal_topology.ma | 80 +++++++++++++------ 1 file changed, 54 insertions(+), 26 deletions(-) diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma index 6a3235445..a68378408 100644 --- a/helm/software/matita/library/demo/formal_topology.ma +++ b/helm/software/matita/library/demo/formal_topology.ma @@ -19,6 +19,12 @@ inductive And (A,B:CProp) : CProp ≝ interpretation "constructive and" 'and x y = (And x y). +inductive Or (A,B:CProp) : CProp ≝ + | or_intro_l: A → Or A B + | or_intro_r: B → Or A B. + +interpretation "constructive or" 'or x y = (Or x y). + inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝ ex_introT2: ∀w:A. P w → Q w → exT2 A P Q. @@ -29,6 +35,14 @@ for @{ 'powerset $A }. interpretation "powerset" 'powerset A = (powerset A). +notation < "hvbox({ ident i | term 19 p })" with precedence 90 +for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}. + +notation > "hvbox({ ident i | term 19 p })" with precedence 90 +for @{ 'subset (\lambda ${ident i}. $p)}. + +interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x). + definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x]. notation "hvbox(a break ∈ b)" non associative with precedence 45 @@ -36,11 +50,39 @@ for @{ 'mem $a $b }. interpretation "mem" 'mem a S = (mem _ S a). -record axiom_set : Type ≝ - { A:> Type; - i: A → Type; - C: ∀a:A. i a → 2 \sup A - }. +definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V). + +notation "hvbox(a break ≬ b)" non associative with precedence 45 +for @{ 'overlaps $a $b }. (* \between *) + +interpretation "overlaps" 'overlaps U V = (overlaps _ U V). + +definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V. + +notation "hvbox(a break ⊆ b)" non associative with precedence 45 +for @{ 'subseteq $a $b }. (* \subseteq *) + +interpretation "subseteq" 'subseteq U V = (subseteq _ U V). + +definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}. + +notation "hvbox(a break ∩ b)" non associative with precedence 55 +for @{ 'intersects $a $b }. (* \cap *) + +interpretation "intersects" 'intersects U V = (intersects _ U V). + +definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}. + +notation "hvbox(a break ∪ b)" non associative with precedence 55 +for @{ 'union $a $b }. (* \cup *) + +interpretation "union" 'union U V = (union _ U V). + +record axiom_set : Type ≝ { + A:> Type; + i: A → Type; + C: ∀a:A. i a → 2 \sup A +}. inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝ iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers. @@ -58,13 +100,13 @@ interpretation "covers" 'covers a U = (covers _ U a). definition covers_elim ≝ λA:axiom_set.λU: 2 \sup A.λP:2 \sup A. λH1:∀a:A. a ∈ U → a ∈ P. - λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ P. + λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → C ? a j ⊆ P → a ∈ P. let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝ match p return λaa.λ_:aa ◃ U.aa ∈ P with [ refl a q ⇒ H1 a q | infinity a j q ⇒ H2 a j q - match q return λ_:(C ? a j) ◃ U.∀b. b ∈ (C ? a j) → b ∈ P with + match q return λ_:(C ? a j) ◃ U. C ? a j ⊆ P with [ iter f ⇒ λb.λr. aux b (f b r) ]] in aux. @@ -83,7 +125,7 @@ interpretation "fish" 'fish a U = (fish _ U a). let corec fish_rec (A:axiom_set) (U: 2 \sup A) (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U) - (H2: ∀a:A. a ∈ P → ∀j: i ? a. exT2 ? (λy.y ∈ C ? a j) (λy.y ∈ P)) : + (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ λa,p. mk_fish A U a @@ -102,7 +144,7 @@ qed. theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V. intros; - apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); simplify; intros; + apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros; [ cases H1 in H2; apply H2; | apply infinity; [ assumption @@ -119,7 +161,7 @@ qed. theorem cotransitivity: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V. intros; - apply (fish_rec ?? (mk_powerset A (λa.a ⋉ U)) ??? H); simplify; intros; + apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros; [ apply H1; apply H2; | cases H2 in j; clear H2; intro i; cases (H4 i); clear H4; exists[apply a3] assumption] @@ -128,14 +170,14 @@ qed. theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V. intros; generalize in match H; clear H; - apply (covers_elim ?? (mk_powerset A (λa.a ⋉ V → U ⋉ V)) ??? H1); + apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1); clear H1; simplify; intros; [ exists [apply a1] assumption | cases H2 in j H H1; clear H2 a1; intros; cases (H1 i); clear H1; apply (H3 a1); assumption] qed. -definition singleton ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A.a=b). +definition singleton ≝ λA:axiom_set.λa:A.{b | a=b}. notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}. @@ -169,20 +211,6 @@ notation "↑a" with precedence 80 for @{ 'uparrow $a }. interpretation "uparrow" 'uparrow a = (uparrow _ a). -definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V). - -notation "hvbox(a break ≬ b)" non associative with precedence 45 -for @{ 'overlaps $a $b }. - -interpretation "overlaps" 'overlaps U V = (overlaps _ U V). - -definition intersects ≝ λA:Type.λU,V:2 \sup A.mk_powerset ? (λa:A. a ∈ U ∧ a ∈ V). - -notation "hvbox(a break ∩ b)" non associative with precedence 55 -for @{ 'intersects $a $b }. - -interpretation "intersects" 'intersects U V = (intersects _ U V). - definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U). notation "↓a" with precedence 80 for @{ 'downarrow $a }. -- 2.39.2