]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/logic.ma
All the equalityTactics have now been ported to use both the equality of
[helm.git] / helm / matita / library / logic.ma
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
15 set "baseuri" "cic:/matita/logic/".
16
17
18 inductive True: Prop \def
19 I : True.
20
21 inductive False: Prop \def .
22
23 definition Not: Prop \to Prop \def
24 \lambda A. (A \to False).
25
26 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
27 intros. elim (H1 H).
28 qed.
29
30 inductive And (A,B:Prop) : Prop \def
31     conj : A \to B \to (And A B).
32
33 theorem proj1: \forall A,B:Prop. (And A B) \to A.
34 intros. elim H. assumption.
35 qed.
36
37 theorem proj2: \forall A,B:Prop. (And A B) \to A.
38 intros. elim H. assumption.
39 qed.
40
41 inductive Or (A,B:Prop) : Prop \def
42      or_introl : A \to (Or A B)
43    | or_intror : B \to (Or A B).
44
45 inductive ex (A:Type) (P:A \to Prop) : Prop \def
46     ex_intro: \forall x:A. P x \to ex A P.
47
48 inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
49     ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.