source: Deliverables/D4.1/Matita/Connectives.ma @ 268

Last change on this file since 268 was 268, checked in by sacerdot, 9 years ago
  • notation moved to proper places
  • new function split on Vectors
File size: 2.5 KB
Line 
1(**************************************************************************)
2(*       ___                                                                *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU Lesser General Public License Version 2.1         *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "Plogic/equality.ma".
16
17ninductive True: Prop ≝ 
18I : True.
19
20default "true" cic:/matita/basics/connectives/True.ind.
21
22ninductive False: Prop ≝ .
23
24default "false" cic:/matita/basics/connectives/False.ind.
25
26(*
27ndefinition Not: Prop → Prop ≝
28λA. A → False. *)
29
30ninductive Not (A:Prop): Prop ≝
31nmk: (A → False) → Not A.
32
33notation "⊥" with precedence 90
34  for @{ match ? in False with [ ] }.
35
36interpretation "logical not" 'not x = (Not x).
37
38ntheorem absurd : ∀ A:Prop. A → ¬A → False.
39#A; #H; #Hn; nelim Hn;/2/; nqed.
40
41(*
42ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
43#A; #C; #H; #Hn; nelim (Hn H).
44nqed. *)
45
46ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
47/4/; nqed.
48
49ninductive And (A,B:Prop) : Prop ≝
50    conj : A → B → And A B.
51
52interpretation "logical and" 'and x y = (And x y).
53
54ntheorem proj1: ∀A,B:Prop. A ∧ B → A.
55#A; #B; #AB; nelim AB; //.
56nqed.
57
58ntheorem proj2: ∀ A,B:Prop. A ∧ B → B.
59#A; #B; #AB; nelim AB; //.
60nqed.
61
62ninductive Or (A,B:Prop) : Prop ≝
63     or_introl : A → (Or A B)
64   | or_intror : B → (Or A B).
65
66interpretation "logical or" 'or x y = (Or x y).
67
68ndefinition decidable : Prop → Prop ≝
69λ A:Prop. A ∨ ¬ A.
70
71ninductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
72    ex_intro: ∀ x:A. P x →  ex A P.
73   
74interpretation "exists" 'exists x = (ex ? x).
75
76ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝
77    ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
78
79ndefinition iff :=
80 λ A,B. (A → B) ∧ (B → A).
81
82interpretation "iff" 'iff a b = (iff a b). 
Note: See TracBrowser for help on using the repository browser.