forked from cmu-phil/Spectral
-
Notifications
You must be signed in to change notification settings - Fork 0
/
logic.hlean
57 lines (37 loc) · 1.26 KB
/
logic.hlean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
/-
Copyright (c) 2017 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad
-/
import types.trunc
open funext eq trunc is_trunc prod sum
--reserve prefix `¬`:40
--reserve prefix `~`:40
--reserve infixr ` ∧ `:35
--reserve infixr ` /\ `:35
--reserve infixr ` \/ `:30
--reserve infixr ` ∨ `:30
--reserve infix ` <-> `:20
--reserve infix ` ↔ `:20
namespace logic
section
open trunc_index
definition propext {p q : Prop} (h : p ↔ q) : p = q :=
tua (equiv_of_iff_of_is_prop h)
end
definition false : Prop := trunctype.mk empty _
definition false.elim {A : Type} (h : false) : A := empty.elim h
definition true : Prop := trunctype.mk unit _
definition true.intro : true := unit.star
definition trivial : true := unit.star
definition and (p q : Prop) : Prop := tprod p q
infixr ` ∧ ` := and
infixr ` /\ ` := and
definition and.intro {p q : Prop} (h₁ : p) (h₂ : q) : and p q := prod.mk h₁ h₂
definition and.left {p q : Prop} (h : p ∧ q) : p := prod.pr1 h
definition and.right {p q : Prop} (h : p ∧ q) : q := prod.pr2 h
definition not (p : Prop) : Prop := trunctype.mk (p → empty) _
prefix `~` := not
definition or.inl := @or.intro_left
definition or.inr := @or.intro_right
end logic