From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
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;