From d2b59bd89f761a16a2dbc663f446b4f95c767b83 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 15 May 2012 19:26:03 +0000 Subject: [PATCH] Patch by Ferruccio that enables \top/\bot for False/True undone. This needs some rediscussion. In particular: 1) \top/\bot are also used as the (only?) symbols for bottom/top in square lattices. Overloading is not a great idea in this case (type vs term). 2) \bot is also traditionally used as the undefined value. For instance, we use it in CerCo for (match ?:\bot in False with []) so that you can use/apply \bot just to say that that case is undefined. Interpretation can't be used for this because "match"es can't be used in interpretations. Thus we use a notation which cannot be overloaded and conflicts with Ferruccio's. Is there any other commonly used symbol for undefined terms? 3) True/False are rarely used in statements. Do they really deserve a symbol? (maybe they do) The patch can be re-enabled by re-applying the inverse svn diff of this commit. --- matita/matita/lib/arithmetics/nat.ma | 2 +- matita/matita/lib/basics/core_notation.ma | 3 - matita/matita/lib/basics/lists/list.ma | 4 +- matita/matita/lib/basics/logic.ma | 10 +--- matita/matita/lib/basics/sets.ma | 2 +- matita/matita/lib/basics/types.ma | 2 +- .../basic_topologies_to_o-basic_topologies.ma | 2 +- .../lib/formal_topology/cprop_connectives.ma | 9 +-- .../matita/lib/formal_topology/o-algebra.ma | 2 +- .../matita/lib/formal_topology/relations.ma | 6 +- .../formal_topology/relations_to_o-algebra.ma | 4 +- matita/matita/lib/re/lang.ma | 2 +- matita/matita/lib/re/reb.ma | 56 +++++++++---------- 13 files changed, 46 insertions(+), 58 deletions(-) diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 76ccbd5cc..81d6c9310 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -27,7 +27,7 @@ definition pred ≝ λn. match n with [ O ⇒ O | S p ⇒ p]. definition not_zero: nat → Prop ≝ - λn: nat. match n with [ O ⇒ ⊥ | (S p) ⇒ ⊤ ]. + λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ]. (* order relations *) diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 703e74823..904adcd52 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -316,6 +316,3 @@ notation "(⊩ \sub term 90 c) " with precedence 65 for @{'Vdash $c}. notation < "maction (mstyle color #ff0000 (­…­)) (t)" non associative with precedence 90 for @{'hide $t}. - -notation "⊤" non associative with precedence 90 for @{'true}. -notation "⊥" non associative with precedence 90 for @{'false}. diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index 4bda9ca70..c89bb7856 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -32,7 +32,7 @@ interpretation "nil" 'nil = (nil ?). interpretation "cons" 'cons hd tl = (cons ? hd tl). definition is_nil: ∀A:Type[0].list A → Prop ≝ - λA.λl.match l with [ nil ⇒ ⊤ | cons hd tl ⇒ ⊥ ]. + λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ]. theorem nil_cons: ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. @@ -232,7 +232,7 @@ lemma All_nth : ∀A,P,n,l. let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ match l with -[ nil ⇒ ⊥ +[ nil ⇒ False | cons h t ⇒ (P h) ∨ (Exists A P t) ]. diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index b6a5d59b7..70e743e99 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -91,21 +91,17 @@ unification hint 0 ≔ T,a,b; inductive True: Prop ≝ I : True. -interpretation "logical true" 'true = True. - inductive False: Prop ≝ . -interpretation "logical false" 'false = False. - (* ndefinition Not: Prop → Prop ≝ -λA. A → ⊥. *) +λA. A → False. *) inductive Not (A:Prop): Prop ≝ -nmk: (A → ⊥) → Not A. +nmk: (A → False) → Not A. interpretation "logical not" 'not x = (Not x). -theorem absurd : ∀A:Prop. A → ¬A → ⊥. +theorem absurd : ∀A:Prop. A → ¬A → False. #A #H #Hn (elim Hn); /2/; qed. (* diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma index 43b22bff6..cdc6ac9e8 100644 --- a/matita/matita/lib/basics/sets.ma +++ b/matita/matita/lib/basics/sets.ma @@ -13,7 +13,7 @@ include "basics/logic.ma". (**** a subset of A is just an object of type A→Prop ****) -definition empty_set ≝ λA:Type[0].λa:A.⊥. +definition empty_set ≝ λA:Type[0].λa:A.False. notation "\emptyv" non associative with precedence 90 for @{'empty_set}. interpretation "empty set" 'empty_set = (empty_set ?). diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma index 35d5cd07b..b7a022ad2 100644 --- a/matita/matita/lib/basics/types.ma +++ b/matita/matita/lib/basics/types.ma @@ -47,7 +47,7 @@ lemma option_map_some : ∀A,B,f,x,v. definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝ λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ]. -lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → ⊥. +lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False. (∀v. x = Some ? v → Q (P v)) → Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)). #A #B #P #Q * diff --git a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma index 0aeb58c73..58b75fb68 100644 --- a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma +++ b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma @@ -29,7 +29,7 @@ definition o_continuous_relation_of_continuous_relation: [ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ] qed. -axiom daemon: ⊥. (*FG: alla faccia del costruttivismo *) +axiom daemon: False. lemma o_continuous_relation_of_continuous_relation_morphism : ∀S,T:category2_of_category1 BTop. diff --git a/matita/matita/lib/formal_topology/cprop_connectives.ma b/matita/matita/lib/formal_topology/cprop_connectives.ma index 7d24790ae..af183d0f6 100644 --- a/matita/matita/lib/formal_topology/cprop_connectives.ma +++ b/matita/matita/lib/formal_topology/cprop_connectives.ma @@ -16,13 +16,6 @@ include "basics/pts.ma". inductive False: CProp[0] ≝. -interpretation "constructive logical false" 'false = False. - -inductive True: CProp[0] ≝ -I : True. - -interpretation "constructive logical true" 'true = True. - inductive Or (A,B:CProp[0]) : CProp[0] ≝ | Left : A → Or A B | Right : B → Or A B. @@ -138,7 +131,7 @@ inductive exT2 (A:Type[0]) (P,Q:A→CProp[0]) : CProp[0] ≝ ex_introT2: ∀w:A. P w → Q w → exT2 A P Q. -definition Not : CProp[0] → CProp[0] ≝ λx:CProp[0].x → ⊥. +definition Not : CProp[0] → CProp[0] ≝ λx:CProp[0].x → False. interpretation "constructive not" 'not x = (Not x). diff --git a/matita/matita/lib/formal_topology/o-algebra.ma b/matita/matita/lib/formal_topology/o-algebra.ma index c595bc029..496485975 100644 --- a/matita/matita/lib/formal_topology/o-algebra.ma +++ b/matita/matita/lib/formal_topology/o-algebra.ma @@ -18,7 +18,7 @@ inductive bool : Type[0] := true : bool | false : bool. lemma BOOL : objs1 SET. constructor 1; [apply bool] constructor 1; -[ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ ⊤ | _ ⇒ ⊥] | false ⇒ match y with [ true ⇒ ⊥ | false ⇒ ⊤ ]]); +[ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]); | whd; simplify; intros; cases x; apply I; | whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption; | whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros; diff --git a/matita/matita/lib/formal_topology/relations.ma b/matita/matita/lib/formal_topology/relations.ma index 89273de05..2ad35655e 100644 --- a/matita/matita/lib/formal_topology/relations.ma +++ b/matita/matita/lib/formal_topology/relations.ma @@ -115,7 +115,7 @@ interpretation "'arrows2_REL" 'arrows2_REL A B = (arrows2 (category2_of_category definition full_subset: ∀s:REL. Ω^s. - apply (λs.{x | ⊤}); + apply (λs.{x | True}); intros; simplify; split; intro; assumption. qed. @@ -316,9 +316,11 @@ theorem ext_comp: qed. *) +axiom daemon : False. + theorem extS_singleton: ∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x. intros; unfold extS; unfold ext; unfold singleton; simplify; split; intros 2; simplify; simplify in f; [ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption; - | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed. + | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed. \ No newline at end of file diff --git a/matita/matita/lib/formal_topology/relations_to_o-algebra.ma b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma index 48ac80da0..bc5153d5d 100644 --- a/matita/matita/lib/formal_topology/relations_to_o-algebra.ma +++ b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma @@ -22,9 +22,9 @@ definition POW': objs1 SET → OAlgebra. | apply overlaps; | apply big_intersects; | apply big_union; - | apply ({x | ⊤}); + | apply ({x | True}); simplify; intros; apply (refl1 ? (eq1 CPROP)); - | apply ({x | ⊥}); + | apply ({x | False}); simplify; intros; apply (refl1 ? (eq1 CPROP)); | intros; whd; intros; assumption | intros; whd; split; assumption diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma index 7424522c7..9f40045ae 100644 --- a/matita/matita/lib/re/lang.ma +++ b/matita/matita/lib/re/lang.ma @@ -34,7 +34,7 @@ let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝ -match l with [ nil ⇒ ⊤ | cons w tl ⇒ r w ∧ conjunct ? tl r ]. +match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. (* kleene's star *) definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. diff --git a/matita/matita/lib/re/reb.ma b/matita/matita/lib/re/reb.ma index 7a3553051..f4cd2e6c1 100644 --- a/matita/matita/lib/re/reb.ma +++ b/matita/matita/lib/re/reb.ma @@ -500,7 +500,7 @@ nlet rec pre_of_re (S : Alpha) (e : re S) on e : pitem S ≝ | o e1 e2 ⇒ po ? (pre_of_re ? e1) (pre_of_re ? e2) | k e1 ⇒ pk ? (pre_of_re ? e1)]. -nlemma notFalse : ¬⊥. @; //; nqed. +nlemma notFalse : ¬False. @; //; nqed. nlemma dot0 : ∀S.∀A:word S → Prop. {} · A = {}. #S A; nnormalize; napply extP; #w; @; ##[##2: *] @@ -562,16 +562,16 @@ interpretation "move" 'move x E = (move ? x E). ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e). interpretation "rmove" 'move x E = (rmove ? x E). -nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → ⊥. +nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → False. #S w abs; ninversion abs; #; ndestruct; nqed. -nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → ⊥. +nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False. #S w abs; ninversion abs; #; ndestruct; nqed. -nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → ⊥. +nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False. #S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe; nqed. @@ -583,17 +583,17 @@ naxiom in_move_cat: ncases e1 in H; ncases e2; ##[##1: *; ##[*; nnormalize; #; ndestruct] #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] - nnormalize; #; ndestruct; ncases (?:⊥); /2/ by XXz,XXze; + nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze; ##|##2: *; ##[*; nnormalize; #; ndestruct] #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] - nnormalize; #; ndestruct; ncases (?:⊥); /2/ by XXz,XXze; + nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze; ##| #r; *; ##[ *; nnormalize; #; ndestruct] #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] ##[##2: nnormalize; #; ndestruct; @2; @2; //.##] - nnormalize; #; ndestruct; ncases (?:⊥); /2/ by XXz; + nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz; ##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##] #H; ninversion H; nnormalize; #; ndestruct; - ##[ncases (?:⊥); /2/ by XXz] /3/ by or_intror; + ##[ncases (?:False); /2/ by XXz] /3/ by or_intror; ##| #r1 r2; *; ##[ *; #defw] ... nqed. @@ -751,28 +751,28 @@ nqed. *) ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e. #S; #a; #E; #E'; #w; #H; nelim H [##1,2: #H1; ninversion H1 - [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:⊥); (* perche' due goal?*) /2/ - |##2,9: #X; #Y; #K; ncases (?:⊥); /2/ - |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:⊥); /2/ - |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/ - |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/ - |##6,13: #x; #y; #K; ncases (?:⊥); /2/ - |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:⊥); /2/] + [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/ + |##2,9: #X; #Y; #K; ncases (?:False); /2/ + |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ + |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + |##6,13: #x; #y; #K; ncases (?:False); /2/ + |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/] ##| #H1; ninversion H1 [ // - | #X; #Y; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/ - | #x; #y; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:⊥); /2/ ] + | #X; #Y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] ##| #H1; #H2; #H3; ninversion H3 - [ #_; #K; ncases (?:⊥); /2/ - | #X; #Y; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:⊥); /2/ - | #x; #y; #K; ncases (?:⊥); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:⊥); /2/ ] + [ #_; #K; ncases (?:False); /2/ + | #X; #Y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ + | #x; #y; #K; ncases (?:False); /2/ + | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6; -- 2.39.2