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.

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 76ccbd5cc48cc3c169fedd0f86ae6567bf68cf00..81d6c9310247dc42c5f2d0d76e66a986ae1d45fc 100644 (file)
--- 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 703e748237562332aa73aaff8f8f9ad218cf0f3f..904adcd52f2fff140dd65eadb6e0945a219c4237 100644 (file)
--- 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 4bda9ca704070b947147b393797251ffdafa90fe..c89bb78560b5ac1b1a9dbb061a372e85318afd9a 100644 (file)
--- 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 b6a5d59b7e09a575ab43c3361cc33a0ae28eafdf..70e743e993ac96c12cdbf7a4a56cdc23bc8280b6 100644 (file)
--- 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 43b22bff6900c1a329610a05596c4a37b41346a6..cdc6ac9e8e278e19c3d7957bf600f7150ae1d895 100644 (file)
--- 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 35d5cd07b10b37df64cf2c4989c4ed0ae6d699de..b7a022ad201056d7d5d1842ea9b3def64d0d862b 100644 (file)
--- 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 0aeb58c737a459c5b691a21561a37ba199cfa610..58b75fb680ececa60755fcb2e77b7105b9245254 100644 (file)
--- 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 7d24790ae6b79b5ff96e6cb17c844217400dfab7..af183d0f656bf7c32fc847b9b087e615213193ea 100644 (file)
--- 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 c595bc0295434fe369481dcb1c46ffbddf055727..496485975f0db459fc03f0e05dd225dd8fc7dd45 100644 (file)
--- 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 89273de051a3982f3825f27355f5d7ac0b52bc01..2ad35655e51756a1ceceda01182f1c126b0100f2 100644 (file)
--- 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 48ac80da02696d4f93a7377fbf768e3854054959..bc5153d5db66532004203625260f99767955eea9 100644 (file)
--- 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 7424522c7fcb00a784431ca666e85e8c8f44e2f0..9f40045aee9b6b923e0c911078066c5f8b6d0ef8 100644 (file)
--- 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 7a3553051069484b7c59849c20bfe5f6b1db9c29..f4cd2e6c163cb007334f0a3c061fa1673364e2ce 100644 (file)
--- 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;