From: Ferruccio Guidi Date: Tue, 15 May 2012 16:11:07 +0000 (+0000) Subject: we added the standard notation for True and False (logical constants) X-Git-Tag: make_still_working~1741 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc477154d15f6979c948f9af602199af547d193e;p=helm.git we added the standard notation for True and False (logical constants) --- diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 81d6c9310..76ccbd5cc 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 ⇒ False | (S p) ⇒ True ]. + λn: nat. match n with [ O ⇒ ⊥ | (S p) ⇒ ⊤ ]. (* order relations *) diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index 904adcd52..703e74823 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -316,3 +316,6 @@ 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 c89bb7856..4bda9ca70 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 ⇒ True | cons hd tl ⇒ False ]. + λA.λl.match l with [ nil ⇒ ⊤ | cons hd tl ⇒ ⊥ ]. 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 ⇒ False +[ nil ⇒ ⊥ | 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 70e743e99..b6a5d59b7 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -91,17 +91,21 @@ 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 → False. *) +λA. A → ⊥. *) inductive Not (A:Prop): Prop ≝ -nmk: (A → False) → Not A. +nmk: (A → ⊥) → Not A. interpretation "logical not" 'not x = (Not x). -theorem absurd : ∀A:Prop. A → ¬A → False. +theorem absurd : ∀A:Prop. A → ¬A → ⊥. #A #H #Hn (elim Hn); /2/; qed. (* diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma index cdc6ac9e8..43b22bff6 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.False. +definition empty_set ≝ λA:Type[0].λa:A.⊥. 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 b7a022ad2..35d5cd07b 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 ? → False. +lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → ⊥. (∀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 58b75fb68..0aeb58c73 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: False. +axiom daemon: ⊥. (*FG: alla faccia del costruttivismo *) 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 af183d0f6..7d24790ae 100644 --- a/matita/matita/lib/formal_topology/cprop_connectives.ma +++ b/matita/matita/lib/formal_topology/cprop_connectives.ma @@ -16,6 +16,13 @@ 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. @@ -131,7 +138,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 → False. +definition Not : CProp[0] → CProp[0] ≝ λx:CProp[0].x → ⊥. 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 496485975..c595bc029 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 ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]); +[ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ ⊤ | _ ⇒ ⊥] | false ⇒ match y with [ true ⇒ ⊥ | false ⇒ ⊤ ]]); | 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 2ad35655e..89273de05 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 | True}); + apply (λs.{x | ⊤}); intros; simplify; split; intro; assumption. qed. @@ -316,11 +316,9 @@ 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. \ No newline at end of file + | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed. 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 bc5153d5d..48ac80da0 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 | True}); + | apply ({x | ⊤}); simplify; intros; apply (refl1 ? (eq1 CPROP)); - | apply ({x | False}); + | apply ({x | ⊥}); 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 9f40045ae..7424522c7 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 ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. +match l with [ nil ⇒ ⊤ | 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 f4cd2e6c1..7a3553051 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 : ¬False. @; //; nqed. +nlemma notFalse : ¬⊥. @; //; 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 ∈ ∅ → False. +nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → ⊥. #S w abs; ninversion abs; #; ndestruct; nqed. -nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False. +nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → ⊥. #S w abs; ninversion abs; #; ndestruct; nqed. -nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False. +nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → ⊥. #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 (?:False); /2/ by XXz,XXze; + nnormalize; #; ndestruct; ncases (?:⊥); /2/ by XXz,XXze; ##|##2: *; ##[*; nnormalize; #; ndestruct] #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] - nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze; + nnormalize; #; ndestruct; ncases (?:⊥); /2/ by XXz,XXze; ##| #r; *; ##[ *; nnormalize; #; ndestruct] #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] ##[##2: nnormalize; #; ndestruct; @2; @2; //.##] - nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz; + nnormalize; #; ndestruct; ncases (?:⊥); /2/ by XXz; ##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##] #H; ninversion H; nnormalize; #; ndestruct; - ##[ncases (?:False); /2/ by XXz] /3/ by or_intror; + ##[ncases (?:⊥); /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 (?: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/] + [##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/] ##| #H1; ninversion H1 [ // - | #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/ ] + | #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/ ] ##| #H1; #H2; #H3; ninversion H3 - [ #_; #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/ ] + [ #_; #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/ ] ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;