Changeset 3517
 Timestamp:
 Nov 18, 2014, 12:02:04 PM (7 years ago)
 Location:
 Papers/jarassembler2014
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Papers/jarassembler2014/boenderjar2014.tex
r3516 r3517 16 16 \usepackage[ttdefault=true]{AnonymousPro} 17 17 18 \newcommand{\All}[1]{\forall{#1}.\;} 18 19 \newcommand{\deffont}[1]{\textbf{#1}} 20 \newcommand{\lam}[1]{\lambda{#1}.\;} 21 \newcommand{\todo}[1]{\ensuremath{\texttt{[#1]}}} 19 22 20 23 \bibliographystyle{alpha} … … 57 60 58 61 Matita is a theorem prover based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. 59 The system features a full spectrum of dependent types and (co)inductive families, as well as a sophisticated system of coercions, all of which we exploit in the formalisation described in this paper.60 61 Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml .62 The system features a full spectrum of dependent types and (co)inductive families, as well as a sophisticated system of coercions, all of which we exploit in the formalisation described herein. 63 64 Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML, and the type theory that Matita implements is very similar to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}. 62 65 Nevertheless, we provide a brief explanation of the main syntactic and typetheoretic features of Matita that will be needed to follow the body of the paper: 63 66 \begin{itemize} 64 67 \item 65 Nonrecursive functions and definitions are introduced via the \texttt{definition} keyword ,whilst recursive functions are introduced with \texttt{let rec}.68 Nonrecursive functions and definitions are introduced via the \texttt{definition} keyword whilst recursive functions are introduced with \texttt{let rec}. 66 69 Mutually recursive functions are separated via the \texttt{and} keyword. 70 Matita checks that all recursive functions are terminating before being admitted. 67 71 \item 68 72 Matita has an infinite hierarchy of type universes. 69 A single impredicativeuniverse of types, \texttt{Prop}, exists at the base of this hierarchy.70 An infinite series of predicativeuniverses, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.71 Matita, unlike Coq ~\cite{coq:2004} or Agda~\cite{bove:brief:2009}, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.73 A single \emph{impredicative} universe of types, \texttt{Prop}, exists at the base of this hierarchy. 74 An infinite series of \emph{predicative} universes, \texttt{Type[0]} : \texttt{Type[1]} : \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}. 75 Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead. 72 76 \item 73 77 Matita's type theory plays host to a rich and expressive higherorder logic. 74 Constant \texttt{True} and \texttt{False} represent truth and (constructive)falsity in \texttt{Prop} respectively.75 Inductive families in \texttt{Prop} encode conjunction and disjunction$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectivelyalso.78 Constant \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively. 79 Two inductive families in \texttt{Prop} encode conjunction and disjunction$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively. 76 80 As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$type). 77 \item 78 Inductive families are introduced via the \texttt{inductive} keyword with named constructor declarations separated with a bar. 81 We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual. 82 \item 83 Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated with a bar. 79 84 Mutually inductive data family declarations are separated via \texttt{with}. 85 In the following declaration 86 \begin{lstlisting} 87 inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$ 88 \end{lstlisting} 89 we call $P_i$ for $0 \leq i \leq n$ the \deffont{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \deffont{indices} of \texttt{I}. 90 Matita checks that constructors have strictlypositive types before admitting an inductive family. 80 91 \item 81 92 Records are introduced with the \texttt{record} keyword. … … 89 100  mk_R : nat > R. 90 101 \end{lstlisting} 91 In particular,declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect.92 \deffont{Projections}, one for each of the record's fields, are also registered in the global context .93 In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection.102 The declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect. 103 \deffont{Projections}, one for each of the record's fields, are also registered in the global context, and in the example record above \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection. 104 A record field's type may depend on fields declared earlier in the record. 94 105 95 106 Record fields may be marked as coercions. … … 97 108 \begin{lstlisting} 98 109 record S : Type[1] := 99 { 100 Carrier :> Type[0]; 101 op : Carrier > Carrier > Carrier 102 } 103 \end{lstlisting} 104 the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}', and the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita's typechecker, thus facilitating the common mathematical practice of confusing a mathematical structure with its underlying carrier set. 105 \item 106 There is provision for customising syntax (through Unicode). 107 Matita has a typedirected system of overloading and resolution so that definitions and proofs look `natural'. 110 { 111 Carrier :> Type[0]; 112 op : Carrier > Carrier > Carrier 113 } 114 \end{lstlisting} 115 the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}' with the effect that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita. 116 Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set. 117 \item 118 Terms may be freely omitted, allowing the user to write down partial types and terms. 119 A question mark, \texttt{?}, denotes a single term that has been omitted by the user. 120 Some omitted terms can be deduced by Matita's refinement system. 121 Other, more complex goals arising from omitted terms may require user input to solve, in which case a proof obligation is opened for each term that cannot be deduced automatically. 122 Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted. 123 \item 124 Pattern matching is carried out with a \texttt{match} expression. 125 We may sometimes fully annotate a \texttt{match} expression with its return type. 126 This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions. 127 In the following 128 \begin{lstlisting} 129 match t return $\lam{x}x = 0 \rightarrow bool$ with 130 [ 0 $\Rightarrow$ $\lam{prf_1}P_1$ 131  S m $\Rightarrow$ $\lam{prf_2}P_2$ 132 ] (refl $\ldots$ t) 133 \end{lstlisting} 134 the \texttt{0} branch of the \texttt{match} expression returns a function from $0 = 0$ to \texttt{bool}, whereas the \texttt{S m} branch of the \texttt{match} expression returns a function from \texttt{S m = 0} to \texttt{bool}. 135 In both cases the annotated return type $\lam{x}x = 0 \rightarrow bool$ has been specialised given new information about \texttt{t} revealed by the act of pattern matching. 136 The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}. 137 \item 138 Matita features a liberal system of uniform coercions (distinct from the previously mentioned record field coercions). 139 \todo{dpm: more about coercions} 108 140 \end{itemize} 141 Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code. 142 We will always ensure that these omissions do not mislead the reader. 109 143 110 144 %%%%%%%%%%%%%%%%%%%%%% 
Papers/jarassembler2014/lstgrafite.tex
r3470 r3517 9 9 morekeywords={[2]include}, 10 10 %emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit}, 11 literate=12 {>}{{$\to$}}313 {:>}{{$\mathrm{:>}$}}114 {>>}{{$\mapsto$}}215 {<=}{{$\leq$}}216 {>=}{{$\geq$}}217 {<>}{{$\neq$}}118 {\\/}{{$\vee$}}119 {<>}{{$\leftrightarrow$}}220 {FORALL\ }{{$\forall\,$}}121 {EXISTS\ }{{$\exists\,$}}122 {ALPHA}{{$\alpha$}}123 {LAMBDA}{{$\lambda\,$}}124 {\\lambda}{{$\lambda\,$}}125 {LANGLE}{{$\langle$}}126 {RANGLE}{{$\rangle$}}127 {EQUIV}{{$\equiv$}}128 {SIGMA}{{$\Sigma$}}129 {PSI}{{$\Psi$}}130 {DOTS}{{$\ldots$}}131 {NOT}{{$\neg$}}132 {\\in}{{$\in$}}133 {𝟙}{{$\mathbf{1}$}}134 {𝟘}{{$\mathbf{0}$}}135 {/\\}{$\land$}136 {×}{{$\times\,$}}237 {\\x}{{$\times\,$}}238 {≝}{{:=}}139 {δ}{{$\delta$}}140 {λ}{{$\lambda\,$}}141 {≰}{{$\nleq\,$}}142 {∨}{{$\lor\,$}}143 {⋁}{{$\bigvee$}}144 {≈}{{$\approx\,$}}145 {∀}{{$\forall\,$}}146 {∃}{{$\exists\,$}}147 {⇝}{{$\leadsto\,$}}148 {→}{{$\rightarrow\,$}}149 {↔}{{$\leftrightarrow$}}150 {∧}{{$\land\,$}}151 {⋀}{{$\bigwedge$}}152 {≤}{{$\leq\,$}}153 {¬}{{$\lnot\,$}}154 {≪}{{$\ll\,$}}155 {≫}{{$\gg\,$}}156 {⇒}{{$\,\Rightarrow\,\,$}}257 {=>}{{$\,\Rightarrow\,\,$}}258 {⇒_0}{{$\,\Rightarrow_0\,\,$}}259 {=>_0}{{$\,\Rightarrow_0\,\,$}}260 {⇒_1}{{$\,\Rightarrow_1\,$}}161 {⇒_1.}{{$\,\Rightarrow_1\,$}}162 {⇒_\\r1}{{$\,\Rightarrow_1^{r}\,$}}163 {⇒_\\r2}{{$\,\Rightarrow_2^{r}\,$}}164 {=>_1}{{$\,\Rightarrow_1\,$}}165 {⇒_2}{{$\,\Rightarrow_2\,$}}166 {⇒_\\o2}{{$\,\Rightarrow_2^o\,$}}167 {⇒_\\c2}{{$\,\Rightarrow_2^c\,$}}168 {⇒_\\c3}{{$\,\Rightarrow_3^c\,$}}169 {⇒_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}170 {⇒_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}171 {⇒_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}172 {⇒_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}173 {⇒_2.}{{$\,\Rightarrow_2\,$}}174 {=>_2}{{$\,\Rightarrow_2\,$}}175 {=_1}{{$=$}}176 {=_2}{{$=$}}177 {⊢}{{$\vdash$}}178 {⊩}{{$\Vdash\,$}}279 {≬}{{$\between$}}280 {><}{{$>\!\!\!\!\!<\,$}}281 {⎻}{{$^$}}182 {⎻*}{{$^{*}$}}183 {\\sup\ ⎻}{{$\!^\,$}}184 {\\sup\ ⎻*}{{$\!^{*}\,$}}185 {\\sup\ *}{{$\!^{*}\,$}}186 {^*}{{$\!^{*}\,$}}187 {F*}{{F$^*$}}188 {G*}{{G$^*$}}189 {∘}{{$\circ\;$}}290 {Ω}{{$\Omega$}}191 {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}192 {Ω^A}{{$\Omega^A$}}193 {Ω^C}{{$\Omega^C$}}194 {Ω^U}{{$\Omega^U$}}195 {Ω^V}{{$\Omega^V$}}196 {Ω^X}{{$\Omega^X$}}197 {Ω^s}{{$\Omega^s$}}198 {‡}{{$\ddagger$}}199 {†}{{$\dagger$}}1100 {⊆}{{$\subseteq\,$}}2101 {♮}{{$\natural$}}1102 {∩}{{$\cap$}}2103 {∪}{{$\cup$}}2104 {⋂}{{$\bigcap$}}2105 {⋃}{{$\bigcup$}}2106 {∈}{{$\in\,$}}2107 {⎽o}{{$_o$}}1108 {⎽f}{{$_f$}}1109 {'\ \\sub\\c}{{'$\!_c$}}1110 {\ \\sub\\c}{{$_c$}}1111 {'\\sub\\c}{{'$\!_c$}}1112 {\\sub\\c}{{$_c$}}1113 {'\ \\sub\\f}{{'$\!_f$}}1114 {\ \\sub\\f}{{$_f$}}1115 {'\\sub\\f}{{'$\!_f$}}1116 {\\sub\\f}{{$_f$}}1117 {\\sup\ (form\ o)}{{$^{o_f}$}}1118 {\\sup\ (concr\ o)}{{$^{o_c}$}}1119 {(form\ o)}{{o$_f~$}}2120 {(concr\ o)}{{o$_c~$}}2121 {form\ o}{{o$_f~$}}2122 {concr\ o}{{o$_c~$}}2123 {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2124 {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2125 {◊⎽t}{{$\Diamond_t$}}1126 {□⎽t}{{$\boxempty_t$}}1127 {⎽⇒}{{$_\Rightarrow$}}1128 {o_operator_of_operator}{{o\_op\_of\_op}}2129 {o_saturation_expansive}{{o\_sat\_expa}}2130 {o_saturation_monotone}{{o\_sat\_monot}}2131 {o_saturation_idempotent}{{o\_sat\_idemp}}2132 {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2133 {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2134 {basic_topology_of_basic_pair}{{btop\_of\_bp}}2135 {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2136 {^1}{{$^{1}$}}1137 {^\ 1}{{$^{1}$}}1138 {\ \\sup\ 1}{{$^{1}$}}1139 {\\sup\ 1}{{$^{1}$}}1140 {\ \\sup1}{{$^{1}$}}1141 {\\sup1}{{$^{1}$}}1142 {...}{{$\ldots$}}111 % literate= 12 % {>}{{$\to$}}3 13 % {:>}{{$\mathrm{:>}$}}1 14 % {>>}{{$\mapsto$}}2 15 % {<=}{{$\leq$}}2 16 % {>=}{{$\geq$}}2 17 % {<>}{{$\neq$}}1 18 % {\\/}{{$\vee$}}1 19 % {<>}{{$\leftrightarrow$}}2 20 % {FORALL\ }{{$\forall\,$}}1 21 % {EXISTS\ }{{$\exists\,$}}1 22 % {ALPHA}{{$\alpha$}}1 23 % {LAMBDA}{{$\lambda\,$}}1 24 % {\\lambda}{{$\lambda\,$}}1 25 % {LANGLE}{{$\langle$}}1 26 % {RANGLE}{{$\rangle$}}1 27 % {EQUIV}{{$\equiv$}}1 28 % {SIGMA}{{$\Sigma$}}1 29 % {PSI}{{$\Psi$}}1 30 % {DOTS}{{$\ldots$}}1 31 % {NOT}{{$\neg$}}1 32 % {\\in}{{$\in$}}1 33 % {𝟙}{{$\mathbf{1}$}}1 34 % {𝟘}{{$\mathbf{0}$}}1 35 % {/\\}{$\land$}1 36 % {×}{{$\times\,$}}2 37 % {\\x}{{$\times\,$}}2 38 % {≝}{{:=}}1 39 % {δ}{{$\delta$}}1 40 % {λ}{{$\lambda\,$}}1 41 % {≰}{{$\nleq\,$}}1 42 % {∨}{{$\lor\,$}}1 43 % {⋁}{{$\bigvee$}}1 44 % {≈}{{$\approx\,$}}1 45 % {∀}{{$\forall\,$}}1 46 % {∃}{{$\exists\,$}}1 47 % {⇝}{{$\leadsto\,$}}1 48 % {→}{{$\rightarrow\,$}}1 49 % {↔}{{$\leftrightarrow$}}1 50 % {∧}{{$\land\,$}}1 51 % {⋀}{{$\bigwedge$}}1 52 % {≤}{{$\leq\,$}}1 53 % {¬}{{$\lnot\,$}}1 54 % {≪}{{$\ll\,$}}1 55 % {≫}{{$\gg\,$}}1 56 % {⇒}{{$\,\Rightarrow\,\,$}}2 57 % {=>}{{$\,\Rightarrow\,\,$}}2 58 % {⇒_0}{{$\,\Rightarrow_0\,\,$}}2 59 % {=>_0}{{$\,\Rightarrow_0\,\,$}}2 60 % {⇒_1}{{$\,\Rightarrow_1\,$}}1 61 % {⇒_1.}{{$\,\Rightarrow_1\,$}}1 62 % {⇒_\\r1}{{$\,\Rightarrow_1^{r}\,$}}1 63 % {⇒_\\r2}{{$\,\Rightarrow_2^{r}\,$}}1 64 % {=>_1}{{$\,\Rightarrow_1\,$}}1 65 % {⇒_2}{{$\,\Rightarrow_2\,$}}1 66 % {⇒_\\o2}{{$\,\Rightarrow_2^o\,$}}1 67 % {⇒_\\c2}{{$\,\Rightarrow_2^c\,$}}1 68 % {⇒_\\c3}{{$\,\Rightarrow_3^c\,$}}1 69 % {⇒_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}1 70 % {⇒_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}1 71 % {⇒_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}1 72 % {⇒_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}1 73 % {⇒_2.}{{$\,\Rightarrow_2\,$}}1 74 % {=>_2}{{$\,\Rightarrow_2\,$}}1 75 % {=_1}{{$=$}}1 76 % {=_2}{{$=$}}1 77 % {⊢}{{$\vdash$}}1 78 % {⊩}{{$\Vdash\,$}}2 79 % {≬}{{$\between$}}2 80 % {><}{{$>\!\!\!\!\!<\,$}}2 81 % {⎻}{{$^$}}1 82 % {⎻*}{{$^{*}$}}1 83 % {\\sup\ ⎻}{{$\!^\,$}}1 84 % {\\sup\ ⎻*}{{$\!^{*}\,$}}1 85 % {\\sup\ *}{{$\!^{*}\,$}}1 86 % {^*}{{$\!^{*}\,$}}1 87 % {F*}{{F$^*$}}1 88 % {G*}{{G$^*$}}1 89 % {∘}{{$\circ\;$}}2 90 % {Ω}{{$\Omega$}}1 91 % {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}1 92 % {Ω^A}{{$\Omega^A$}}1 93 % {Ω^C}{{$\Omega^C$}}1 94 % {Ω^U}{{$\Omega^U$}}1 95 % {Ω^V}{{$\Omega^V$}}1 96 % {Ω^X}{{$\Omega^X$}}1 97 % {Ω^s}{{$\Omega^s$}}1 98 % {‡}{{$\ddagger$}}1 99 % {†}{{$\dagger$}}1 100 % {⊆}{{$\subseteq\,$}}2 101 % {♮}{{$\natural$}}1 102 % {∩}{{$\cap$}}2 103 % {∪}{{$\cup$}}2 104 % {⋂}{{$\bigcap$}}2 105 % {⋃}{{$\bigcup$}}2 106 % {∈}{{$\in\,$}}2 107 % {⎽o}{{$_o$}}1 108 % {⎽f}{{$_f$}}1 109 % {'\ \\sub\\c}{{'$\!_c$}}1 110 % {\ \\sub\\c}{{$_c$}}1 111 % {'\\sub\\c}{{'$\!_c$}}1 112 % {\\sub\\c}{{$_c$}}1 113 % {'\ \\sub\\f}{{'$\!_f$}}1 114 % {\ \\sub\\f}{{$_f$}}1 115 % {'\\sub\\f}{{'$\!_f$}}1 116 % {\\sub\\f}{{$_f$}}1 117 % {\\sup\ (form\ o)}{{$^{o_f}$}}1 118 % {\\sup\ (concr\ o)}{{$^{o_c}$}}1 119 % {(form\ o)}{{o$_f~$}}2 120 % {(concr\ o)}{{o$_c~$}}2 121 % {form\ o}{{o$_f~$}}2 122 % {concr\ o}{{o$_c~$}}2 123 % {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2 124 % {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2 125 % {◊⎽t}{{$\Diamond_t$}}1 126 % {□⎽t}{{$\boxempty_t$}}1 127 % {⎽⇒}{{$_\Rightarrow$}}1 128 % {o_operator_of_operator}{{o\_op\_of\_op}}2 129 % {o_saturation_expansive}{{o\_sat\_expa}}2 130 % {o_saturation_monotone}{{o\_sat\_monot}}2 131 % {o_saturation_idempotent}{{o\_sat\_idemp}}2 132 % {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2 133 % {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2 134 % {basic_topology_of_basic_pair}{{btop\_of\_bp}}2 135 % {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2 136 % {^1}{{$^{1}$}}1 137 % {^\ 1}{{$^{1}$}}1 138 % {\ \\sup\ 1}{{$^{1}$}}1 139 % {\\sup\ 1}{{$^{1}$}}1 140 % {\ \\sup1}{{$^{1}$}}1 141 % {\\sup1}{{$^{1}$}}1 142 % {...}{{$\ldots$}}1 143 143 , 144 144 tabsize=1,
Note: See TracChangeset
for help on using the changeset viewer.