-
Notifications
You must be signed in to change notification settings - Fork 0
/
Intro_to_Coq.tex
102 lines (97 loc) · 1.32 KB
/
Intro_to_Coq.tex
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
\documentclass{article}
\usepackage[utf8]{inputenc}
\title{Lambda Conf Notes}
\author{Krystal Maughan }
\date{May 26th 2017}
\begin{document}
\maketitle
\mathversion{bold}{$ LambdaConf Day 2 $}
\\
\\
\mathversion{normal}
\\
\section{Introduction to Coq}
Gabriel Claramunt
\\
\\
Programming Logic
\\
Type Theory
\\
Proof Assistants
\\
Implementation of the Calculus of Contructions
\\
Thierry Coquand
\\
based on Martin-Lof's Intuitionistic Type Theory
\\
\\
$\frac{hypothesis}{goal}$
\\
$\frac{\gamma}{\alpha}$
\\
\\
Assumption: Goal is in hypothesis
\\
Propositional Logic
\\
split $\rightarrow$ $\frac{\gamma}{\alpha \land \beta}$
\\
\\
Apply
\\
$\frac{H: \alpha \rightarrow \beta}{\beta}$
\\
\\
Cut $\beta$
\\
$\frac{\gamma}{\alpha}$
\\
\\
Unfold
\\
$\frac{\gamma}{\neg \alpha}$
\\
\\
Classical Logic
\\
Constructive tautologies (auto)
\\
\\
\section{Proofs}
A $\rightarrow$ A.
\\
intro Ha.
\\
assumption
\\
\\
$A \rightarrow B \rightarrow A$
\\
intro Ha.
\\
intro Hb.
\\
assumption.
\\
\\
$(A \rightarrow (B \rightarrow C)) \rightarrow (A \rightarrow B) \rightarrow (A \rightarrow C)$.
\\
intros will define three hypothesis values:
\\
A, B and C.
\\
\\
intros.
\\
apply H.
\\
assumption.
\\
apply H0.
\\
assumption.
\\
\\
\end{document}