lambdapi-stdlib/Prop.lp at master · Deducteam/lambdapi-stdlib · GitHub

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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
// propositional logic

constant symbol Prop : TYPE;

builtin "Prop" ≔ Prop;

// interpretation of propositions in TYPE

injective symbol π : Prop → TYPE; // `p

builtin "Prf" ≔ π;

// true

constant symbol ⊤ : Prop; // \top

builtin "top" ≔ ⊤;

constant symbol ⊤ᵢ : π ⊤;

// false

constant symbol ⊥ : Prop; // \bot

builtin "bot" ≔ ⊥;

constant symbol ⊥ₑ [p] : π ⊥ → π p;

// implication

constant symbol ⇒ : Prop → Prop → Prop; // =>

notation ⇒ infix right 5;

builtin "imp" ≔ ⇒;

rule π ($p ⇒ $q) ↪ π $p → π $q;

symbol fold_⇒ [p q] : π (p ⇒ q) → π p → π q ≔
begin
  assume p q pq h; apply pq h;
end;

// negation

symbol ¬ p ≔ p ⇒ ⊥; // ~~ or \neg

notation ¬ prefix 35;

builtin "not" ≔ ¬;

// conjunction

constant symbol ∧ : Prop → Prop → Prop; // /\ or \wedge

notation ∧ infix right 7;

builtin "and" ≔ ∧;

constant symbol ∧ᵢ [p q] : π p → π q → π (p ∧ q);
symbol ∧ₑ₁ [p q] : π (p ∧ q) → π p;
symbol ∧ₑ₂ [p q] : π (p ∧ q) → π q;

// disjunction

constant symbol ∨ : Prop → Prop → Prop; // \/ or \vee

notation ∨ infix right 6;

builtin "or" ≔ ∨;

constant symbol ∨ᵢ₁ [p q] : π p → π (p ∨ q);
constant symbol ∨ᵢ₂ [p q] : π q → π (p ∨ q);
symbol ∨ₑ [p q r] : π (p ∨ q) → (π p → π r) → (π q → π r) → π r;

// equivalence

symbol ⇔ p q ≔ (p ⇒ q) ∧ (q ⇒ p); // \Leftrightarrow

notation ⇔ infix right 5;

builtin "eqv" ≔ ⇔;

opaque symbol ⇔_refl [p] : π (p ⇔ p) ≔
begin
  assume p; apply ∧ᵢ { assume h; apply h } { assume h; apply h }
end;

opaque symbol ⇔_sym [p q] : π (p ⇔ q) → π (q ⇔ p) ≔
begin
  assume p q h; apply ∧ᵢ { apply ∧ₑ₂ h } { apply ∧ₑ₁ h };
end;

opaque symbol ⇔_trans p q r : π (p ⇔ q) → π (q ⇔ r) → π (p ⇔ r) ≔
begin
  assume p q r epq eqr; apply ∧ᵢ
    { assume hp; apply ∧ₑ₁ eqr _; apply ∧ₑ₁ epq hp }
    { assume hr; apply ∧ₑ₂ epq _; apply ∧ₑ₂ eqr hr }
end;

// check that priorities are correctly set
assert x y z ⊢ x ∨ y ∧ z ≡ x ∨ (y ∧ z);
assert p q ⊢ ¬ p ∧ q ≡ (¬ p) ∧ q;
assert p q ⊢ ¬ p ∨ q ≡ (¬ p) ∨ q;
assert p q ⊢ ¬ p ⇒ q ≡ (¬ p) ⇒ q;
assert p q ⊢ ¬ p ⇔ q ≡ (¬ p) ⇔ q;
assert p q r ⊢ p ⇒ q ∧ r ≡ p ⇒ (q ∧ r);
assert p q r ⊢ p ⇒ q ∨ r ≡ p ⇒ (q ∨ r);