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.
13 files changed:
λn. match n with [ O ⇒ O | S p ⇒ p].
definition not_zero: nat → Prop ≝
λ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 ].
notation < "maction (mstyle color #ff0000 (…)) (t)"
non associative with precedence 90 for @{'hide $t}.
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}.
interpretation "cons" 'cons hd tl = (cons ? hd tl).
definition is_nil: ∀A:Type[0].list A → Prop ≝
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 ≠ [].
theorem nil_cons:
∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
match l with
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
match l with
| cons h t ⇒ (P h) ∨ (Exists A P t)
].
| cons h t ⇒ (P h) ∨ (Exists A P t)
].
inductive True: Prop ≝
I : True.
inductive True: Prop ≝
I : True.
-interpretation "logical true" 'true = True.
-
inductive False: Prop ≝ .
inductive False: Prop ≝ .
-interpretation "logical false" 'false = False.
-
(* ndefinition Not: Prop → Prop ≝
(* ndefinition Not: Prop → Prop ≝
inductive Not (A:Prop): Prop ≝
inductive Not (A:Prop): Prop ≝
+nmk: (A → False) → Not A.
interpretation "logical not" 'not x = (Not x).
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.
(*
#A #H #Hn (elim Hn); /2/; qed.
(*
(**** a subset of A is just an object of type A→Prop ****)
(**** 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 ?).
notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
interpretation "empty set" 'empty_set = (empty_set ?).
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 ].
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 *
(∀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 *
[ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ]
qed.
[ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ]
qed.
-axiom daemon: ⊥. (*FG: alla faccia del costruttivismo *)
lemma o_continuous_relation_of_continuous_relation_morphism :
∀S,T:category2_of_category1 BTop.
lemma o_continuous_relation_of_continuous_relation_morphism :
∀S,T:category2_of_category1 BTop.
inductive False: CProp[0] ≝.
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.
inductive Or (A,B:CProp[0]) : CProp[0] ≝
| Left : A → Or A B
| Right : B → Or A B.
ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
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).
interpretation "constructive not" 'not x = (Not x).
lemma BOOL : objs1 SET.
constructor 1; [apply bool] constructor 1;
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;
| 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;
definition full_subset: ∀s:REL. Ω^s.
definition full_subset: ∀s:REL. Ω^s.
intros; simplify; split; intro; assumption.
qed.
intros; simplify; split; intro; assumption.
qed.
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;
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
| apply overlaps;
| apply big_intersects;
| apply big_union;
| apply overlaps;
| apply big_intersects;
| apply big_union;
simplify; intros; apply (refl1 ? (eq1 CPROP));
simplify; intros; apply (refl1 ? (eq1 CPROP));
simplify; intros; apply (refl1 ? (eq1 CPROP));
| intros; whd; intros; assumption
| intros; whd; split; assumption
simplify; intros; apply (refl1 ? (eq1 CPROP));
| intros; whd; intros; assumption
| intros; whd; split; assumption
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 ⇒ 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.
(* kleene's star *)
definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
| o e1 e2 ⇒ po ? (pre_of_re ? e1) (pre_of_re ? e2)
| k e1 ⇒ pk ? (pre_of_re ? e1)].
| 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: *]
nlemma dot0 : ∀S.∀A:word S → Prop. {} · A = {}.
#S A; nnormalize; napply extP; #w; @; ##[##2: *]
ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
interpretation "rmove" 'move x E = (rmove ? 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.
#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.
#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.
#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
nqed.
ncases e1 in H; ncases e2;
##[##1: *; ##[*; nnormalize; #; ndestruct]
#H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
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]
##|##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; //.##]
##| #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;
##| #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.
##| #r1 r2; *; ##[ *; #defw]
...
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
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
[ //
##| #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
##| #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;
##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;