# HG changeset patch # User ryokka # Date 1545073708 -32400 # Node ID 83d000399c9dbba99d5b0d4475e0b60692c44692 # Parent b5f17725a347d1a20310dbb70b4ba5741fd44e66 fix invisible char diff -r b5f17725a347 -r 83d000399c9d Paper/Makefile --- a/Paper/Makefile Tue Dec 18 02:32:47 2018 +0900 +++ b/Paper/Makefile Tue Dec 18 04:08:28 2018 +0900 @@ -1,36 +1,44 @@ -# Created by Daichi Toma on Nov 16, 2011 - +# Settings TARGET=tecrep +BIBTEX=pbibtex +BB=extractbb -LATEX=platex -BIBTEX=pbibtex -DVIPDF=dvipdfmx -p a4 -#You need setting "-l" option if You think You get a landscape PDF -#DVIPDF_OPT=-l +vpath pdf fig +FIGURES=$(wildcard pic/*.pdf) +FIGURES_FOR_TEX=$(subst .pdf,.xbb,$(FIGURES)) + +vpath agda src +SOURCES=$(wildcard src/*agda) +SOURCES_FOR_TEX=$(subst .agda,.agda.replaced,$(SOURCES)) -#Embed fonts -#DVIPDF_OPT=-x 1in -y 1in -o - -.SUFFIXES: .tex .dvi .pdf +# dependencies +$(TARGET).pdf : $(TARGET).dvi + dvipdfmx $< -.tex.dvi: - $(LATEX) $< +$(TARGET).dvi : $(wildcard *.tex) $(FIGURES_FOR_TEX) $(SOURCES_FOR_TEX) + platex $(TARGET).tex $(BIBTEX) $(TARGET) - $(LATEX) $< - $(LATEX) $< + platex $(TARGET).tex + platex $(TARGET).tex -.dvi.pdf: - $(DVIPDF) $(DVIPDF_OPT) $(TARGET).dvi +%.xbb: %.pdf + $(BB) $< + +%.agda.replaced: %.agda + ruby escape_agda.rb $< +# commands +.PHONY : clean all open remake + +clean: + rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*.replaced + all: $(TARGET).pdf + +open: $(TARGET).pdf open $(TARGET).pdf -dvi: $(TARGET).dvi - -pdf: $(TARGET).pdf - - -clean: - rm -f *.dvi *.aux *.log *.ps *.gz *.bbl *.blg *.toc *~ *.core - +remake: + make clean + make all diff -r b5f17725a347 -r 83d000399c9d Paper/escape_agda.rb --- a/Paper/escape_agda.rb Tue Dec 18 02:32:47 2018 +0900 +++ b/Paper/escape_agda.rb Tue Dec 18 04:08:28 2018 +0900 @@ -16,7 +16,12 @@ '₁' => 'text{1}', 'ℕ' => 'mathbb{N}', '∎' => 'blacksquare', - 'λ' => 'lambda' + 'λ' => 'lambda', + '∧' => 'wedge', + '⇒' => 'Rightarrow', + '¬' => 'neg', + '≤' => 'leq', + '⊥' => 'bot', } code = File.read(FileName) diff -r b5f17725a347 -r 83d000399c9d Paper/src/function.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/function.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,4 @@ +_-_ :@$\mathbb{N}$@ →@$\mathbb{N}$@ →@$\mathbb{N}$@ +x - zero = x +zero - _ = zero +(suc x) - (suc y) = x - y diff -r b5f17725a347 -r 83d000399c9d Paper/src/gears-while.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/gears-while.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,51 @@ +whileTest : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } → (Code : (env : Env) @$\rightarrow$@ + ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t +whileTest {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) + proof2 = record {pi1 = refl ; pi2 = refl} + +conversion1 : {l : Level} {t : Set l } → (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } → ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) + @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t +conversion1 env {c10} p1 next = next env proof4 + where + proof4 : varn env + vari env @$\equiv$@ c10 + proof4 = let open @$\equiv$@-Reasoning in + begin + varn env + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n → n + vari env ) (pi2 p1 ) @$\rangle$@ + c10 + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n → c10 + n ) (pi1 p1 ) @$\rangle$@ + c10 + 0 + @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ + c10 + @$\blacksquare$@ + +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } → ((varn env) + (vari env) @$\equiv$@ c10) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoop env proof next with ( suc zero @$\leq$@? (varn env) ) +whileLoop env proof next | no p = next env +whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next + where + env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} + 1<0 : 1 @$\leq$@ zero → @$\bot$@ + 1<0 () + proof3 : (suc zero @$\leq$@ (varn env)) → varn env1 + vari env1 @$\equiv$@ c10 + proof3 (s@$\leq$@s lt) with varn env + proof3 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 p) + proof3 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in + begin + n' + (vari env + 1) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z → n' + z ) ( +-sym {vari env} {1} ) @$\rangle$@ + n' + (1 + vari env ) + @$\equiv$@@$\langle$@ sym ( +-assoc (n') 1 (vari env) ) @$\rangle$@ + (n' + 1) + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z → z + vari env ) +1@$\equiv$@suc @$\rangle$@ + (suc n' ) + vari env + @$\equiv$@@$\langle$@@$\rangle$@ + varn env + vari env + @$\equiv$@@$\langle$@ proof @$\rangle$@ + c10 + @$\blacksquare$@ diff -r b5f17725a347 -r 83d000399c9d Paper/src/gears.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/gears.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,2 @@ +proofGears : {c10 : @$\mathbb{N}$@ } → Set +proofGears {c10} = whileTest {_} {_} {c10} (@$\lambda$@ n p1 → conversion1 n p1 (@$\lambda$@ n1 p2 → whileLoop' n1 p2 (@$\lambda$@ n2 → ( vari n2 @$\equiv$@ c10 )))) diff -r b5f17725a347 -r 83d000399c9d Paper/src/record.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/record.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,4 @@ +record Env : Set where + field + varn : @$\mathbb{N}$@ + vari : @$\mathbb{N}$@ diff -r b5f17725a347 -r 83d000399c9d Paper/src/term1.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/term1.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,15 @@ +stmt2Cond : {c10 :@$\mathbb{N}$@} → Cond +stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0) + +lemma1 : {c10 :@$\mathbb{N}$@} → Axiom (stmt1Cond {c10}) (@$\lambda$@ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +10}) +lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond → let open @$\equiv$@-Reasoning in +begin +? -- ?0 +@$\equiv$@@$\langle$@ ? @$\rangle$@ -- ?1 +? -- ?2 +@$\blacksquare$@ ) + +-- ?0 : Bool +-- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) @$\equiv$@ true +-- ?2 : Bool diff -r b5f17725a347 -r 83d000399c9d Paper/src/term2.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/term2.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,7 @@ +@$\wedge$@true : { x : Bool } → x @$\wedge$@ true @$\equiv$@ x +@$\wedge$@true {x} with x +@$\wedge$@true {x} | false = refl +@$\wedge$@true {x} | true = refl + +stmt1Cond : {c10 :@$\mathbb{N}$@} → Cond +stmt1Cond {c10} env = Equal (varn env) c10 diff -r b5f17725a347 -r 83d000399c9d Paper/src/term3.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/term3.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,10 @@ +lemma1 : {c10 :@$\mathbb{N}$@} → Axiom (stmt1Cond {c10}) (@$\lambda$@ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +10}) +lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond → let open @$\equiv$@-Reasoning in +begin +(Equal (varn env) c10 ) @$\wedge$@ true +@$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@ +Equal (varn env) c10 +@$\equiv$@@$\langle$@ cond @$\rangle$@ +true +@$\blacksquare$@ ) diff -r b5f17725a347 -r 83d000399c9d Paper/src/while-test.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while-test.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,2 @@ +whileTest : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) → (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) diff -r b5f17725a347 -r 83d000399c9d Paper/src/zero.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/zero.agda.replaced Tue Dec 18 04:08:28 2018 +0900 @@ -0,0 +1,3 @@ ++zero : { y : @$\mathbb{N}$@ } → y + zero @$\equiv$@ y ++zero {zero} = refl ++zero {suc y} = cong ( @$\lambda$@ x → suc x ) ( +zero {y} ) diff -r b5f17725a347 -r 83d000399c9d Paper/tecrep.bib --- a/Paper/tecrep.bib Tue Dec 18 02:32:47 2018 +0900 +++ b/Paper/tecrep.bib Tue Dec 18 04:08:28 2018 +0900 @@ -73,7 +73,7 @@ } -@misc{agda-alfa, +@misc{agda-alpa, title = {Example - Hoare Logic}, howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}}, note = {Accessed: 2018/12/17(Mon)} diff -r b5f17725a347 -r 83d000399c9d Paper/tecrep.pdf Binary file Paper/tecrep.pdf has changed diff -r b5f17725a347 -r 83d000399c9d Paper/tecrep.tex --- a/Paper/tecrep.tex Tue Dec 18 02:32:47 2018 +0900 +++ b/Paper/tecrep.tex Tue Dec 18 04:08:28 2018 +0900 @@ -7,14 +7,17 @@ \usepackage{lmodern} \usepackage{textcomp} \usepackage{latexsym} -%\usepackage[fleqn]{amsmath} -%\usepackage{amssymb} +\usepackage{ascmac} +\usepackage[fleqn]{amsmath} +\usepackage{amssymb} +\usepackage[deluxe, multi]{otf} \usepackage{url} \usepackage{cite} \usepackage[portuguese]{babel} \usepackage[utf8]{inputenc} \usepackage{listingsutf8} \usepackage{listings} +\usepackage{colonequals} \usepackage{inconsolata} \lstset{ frame=single, @@ -38,15 +41,17 @@ lineskip=-0.5zw, inputencoding=utf8, extendedchars=true, + stringstyle={\ttfamily}, escapechar={@}, - escapeinside={\%*}{*}, - literate= - {⟨}{{\langle}}1 - {⟩}{{\rangle}}1 - {ℕ}{{$\mathbb{N}$}}1 - {^^e2^^84^^95}{{$\mathbb{N}$}}1 + %% mathescape=true, } + %% literate= + %% {⟨}{{\langle}}1 + %% {⟩}{{\rangle}}1 + %% {ℕ}{{$\mathbb{N}$}}1 + %% {^^e2^^84^^95}{{$\mathbb{N}$}}1 + % basicstyle={\ttfamily}, \renewcommand{\lstlistingname}{Code} \usepackage{caption} @@ -152,7 +157,7 @@ Code \ref{agda-record} はレコード型の例であり、Env では varn と vari の二つの field を持ち、 それぞれの型が Agda 上で自然数を表す Nat になっている。 -\lstinputlisting[caption=record の例,label=agda-record]{src/data.agda.replaced} +\lstinputlisting[caption=record の例,label=agda-record]{src/record.agda.replaced} %% \begin{lstlisting}[caption=record の例,label=agda-record] %% record Env : Set where %% field @@ -160,18 +165,18 @@ %% vari : ℕ %% \end{lstlisting} -関数の定義は、関数名と型を記述した後に関数の本体を = の後に記述する。関数の型には → 、または-> を用いる。 -例えば引数が型 A で返り値が型 B の関数は A -> B のように書ける。また、複数の引数を取る関数の型は A -> A -> B のように書ける。この時の型は A -> (A -> B) のように考えられる。 +関数の定義は、関数名と型を記述した後に関数の本体を = の後に記述する。関数の型には → 、または$->$ を用いる。 +例えば引数が型 A で返り値が型 B の関数は A $->$ B のように書ける。また、複数の引数を取る関数の型は A $->$ A $->$ B のように書ける。この時の型は A $->$ (A $->$ B) のように考えられる。 ここでは Code \ref{agda-function}を例にとる。これは引き算の演算子で、Agda の Nat を二つ引数に受けて Nat を返す 関数である。　 -\lstinputlisting{src/data.agda.replaced} -\begin{lstlisting}[caption=関数の例,label=agda-function] -_-_ :ℕ →ℕ →ℕ -x - zero = x -zero - _ = zero -(suc x) - (suc y) = x - y -\end{lstlisting} +\lstinputlisting[caption=関数の例,label=agda-function]{src/function.agda.replaced} +%% \begin{lstlisting}[caption=関数の例,label=agda-function] +%% _-_ : ℕ →ℕ →ℕ +%% x - zero = x +%% zero - _ = zero +%% (suc x) - (suc y) = x - y +%% \end{lstlisting} Agda での証明では型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明が完成する。 証明の例として Code \ref{proof} を見る。 @@ -181,11 +186,12 @@ $y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。 $y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$ を用いて証明している。 -\begin{lstlisting}[caption=等式変形の例,label=proof] -+zero : { y :ℕ } → y + zero ≡ y -+zero {zero} = refl -+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) -\end{lstlisting} +\lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例,label=proof] +%% +zero : { y : ℕ } → y + zero ≡ y +%% +zero {zero} = refl +%% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) +%% \end{lstlisting} また、他にも $\lambda$ 項部分で等式を変形する構文が存在している。 Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。 @@ -193,52 +199,54 @@ Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。 $--$ は Agda 上ではコメントである。 -\begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre] -stmt2Cond : {c10 :ℕ} → Cond -stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) +\lstinputlisting[caption=等式変形の例1/2,label=agda-term-pre]{src/term1.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre] +%% stmt2Cond : {c10 : ℕ} → Cond +%% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) -lemma1 : {c10 :ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ -10}) -lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in - begin - ? -- ?0 - ≡⟨ ? ⟩ -- ?1 - ? -- ?2 - ∎ ) +%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +%% 10}) +%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% ? -- ?0 +%% ≡⟨ ? ⟩ -- ?1 +%% ? -- ?2 +%% ∎ ) --- ?0 : Bool --- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true --- ?2 : Bool -\end{lstlisting} +%% -- ?0 : Bool +%% -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true +%% -- ?2 : Bool +%% \end{lstlisting} この状態で Compile すると ? 部分に入る型を Agda が示してくれるため、始めに変形する等式を ?0 に 記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。 ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。 -\begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid] -∧true : { x : Bool } → x ∧ true ≡ x -∧true {x} with x -∧true {x} | false = refl -∧true {x} | true = refl +\lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid] +%% ∧true : { x : Bool } → x ∧ true ≡ x +%% ∧true {x} with x +%% ∧true {x} | false = refl +%% ∧true {x} | true = refl -stmt1Cond : {c10 :ℕ} → Cond -stmt1Cond {c10} env = Equal (varn env) c10 -\end{lstlisting} +%% stmt1Cond : {c10 : ℕ} → Cond +%% stmt1Cond {c10} env = Equal (varn env) c10 +%% \end{lstlisting} 最終的な証明は\ref{agda-term-post} のようになる。 - -\begin{lstlisting}[caption=等式変形の例3/3,label=agda-term-post] -lemma1 : {c10 :ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ -10}) -lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in - begin - (Equal (varn env) c10 ) ∧ true - ≡⟨ ∧true ⟩ - Equal (varn env) c10 - ≡⟨ cond ⟩ - true - ∎ ) -\end{lstlisting} +\lstinputlisting[caption=等式変形の例2/2,label=agda-term-post]{src/term3.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post] +%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +%% 10}) +%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% (Equal (varn env) c10 ) ∧ true +%% ≡⟨ ∧true ⟩ +%% Equal (varn env) c10 +%% ≡⟨ cond ⟩ +%% true +%% ∎ ) +%% \end{lstlisting} \section{GearsOS} @@ -263,7 +271,7 @@ \begin{figure}[htpb] \begin{center} - \scalebox{0.25}{\includegraphics{pic/meta_cg_dg.pdf}} + \scalebox{0.425}{\includegraphics{pic/meta_cg_dg.pdf}} \end{center} \caption{CodeGear と DataGear の関係} \label{fig:cgdg} @@ -280,12 +288,13 @@ CodeGear は Agda では継続渡しで書かれた関数と等価である。 継続は不定の型 (\verb+t+) を返す関数で表される。 CodeGear 自体も同じ型 \verb+t+ を返す関数となる。 - Code \ref{agda-gc}は Agda で書いた CodeGear の型の例である。 + Code \ref{agda-cg}は Agda で書いた CodeGear の型の例である。 -\begin{lstlisting}[caption= whileTest の型,label=agda-cg] -whileTest : {l : Level} {t : Set l} -> (c10 :ℕ) → (Code : Env -> t) -> t -whileTest c10 next = next (record {varn = c10 ; vari = 0} ) -\end{lstlisting} +\lstinputlisting[caption= whileTest の型,label=agda-cg]{src/while-test.agda.replaced} +%% \begin{lstlisting}[caption= whileTest の型,label=agda-cg] +%% whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t +%% whileTest c10 next = next (record {varn = c10 ; vari = 0} ) +%% \end{lstlisting} GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と @@ -330,7 +339,7 @@ 今回は、 Code \ref{agda-while} のような while Loop に対しての検証を行う。 -\begin{lstlisting}[caption=while Loop,label=agda-while] +\begin{lstlisting}[caption=while Loop Program,label=agda-while] n = 10; i = 0; @@ -372,12 +381,6 @@ While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。 \begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare] -record Env : Set where - field - varn :ℕ - vari :ℕ -open Env - PrimComm : Set PrimComm = Env → Env @@ -400,7 +403,7 @@ Code \ref{agda-hoare-prog}は Code \ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。 ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 -\begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog] +\begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog,mathescape=false] program : Comm program = Seq ( PComm (λ env → record env {varn = 10})) @@ -539,7 +542,7 @@ %% initCond : Cond %% initCond env = true -%% stmt1Cond : {c10 :ℕ} → Cond +%% stmt1Cond : {c10 : ℕ} → Cond %% stmt1Cond {c10} env = Equal (varn env) c10 %% init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari \ @@ -550,21 +553,21 @@ %% nd {c10}) %% init-type {c10} env = init-case env -%% stmt2Cond : {c10 :ℕ} → Cond +%% stmt2Cond : {c10 : ℕ} → Cond %% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) -%% whileInv : {c10 :ℕ} → Cond +%% whileInv : {c10 : ℕ} → Cond %% whileInv {c10} env = Equal ((varn env) + (vari env)) c10 -%% whileInv' : {c10 :ℕ} → Cond +%% whileInv' : {c10 : ℕ} → Cond %% whileInv' {c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env) -%% termCond : {c10 :ℕ} → Cond +%% termCond : {c10 : ℕ} → Cond %% termCond {c10} env = Equal (vari env) c10 %% \end{lstlisting} %% \begin{lstlisting}[caption=proof1 の lemma ,label=agda-hoare-while-lemma] -%% lemma1 : {c10 :ℕ} → Axiom (stmt1Cond {c10}) +%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) %% (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) %% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in %% begin @@ -575,11 +578,11 @@ %% true %% ∎ ) -%% lemma21 : {env : Env } → {c10 :ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 +%% lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 %% lemma21 eq = Equal→≡ (∧-pi1 eq) -%% lemma22 : {env : Env } → {c10 :ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 +%% lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 %% lemma22 eq = Equal→≡ (∧-pi2 eq) -%% lemma23 : {env : Env } → {c10 :ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 +%% lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 %% lemma23 {env} {c10} eq = let open ≡-Reasoning in %% begin %% varn env + vari env @@ -592,7 +595,7 @@ %% ≡⟨⟩ %% c10 %% ∎ -%% lemma2 : {c10 :ℕ} → Tautology stmt2Cond whileInv +%% lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv %% lemma2 {c10} env = bool-case (stmt2Cond env) ( %% λ eq → let open ≡-Reasoning in %% begin @@ -635,7 +638,7 @@ %% ≡⟨ ∧-pi1 cond ⟩ %% true %% ∎ ) -%% lemma41 : (env : Env ) → {c10 :ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true +%% lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true %% lemma41 env {c10} c1 c2 = let open ≡-Reasoning in %% begin %% Equal ((varn env - 1) + vari env) c10 @@ -652,7 +655,7 @@ %% ≡⟨ ≡→Equal refl ⟩ %% true %% ∎ -%% lemma4 : {c10 :ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv +%% lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv %% lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in %% begin %% whileInv (record { varn = varn env - 1 ; vari = vari env }) @@ -669,7 +672,7 @@ %% lemma51 z refl | _ | no ¬p with varn z %% lemma51 z refl | _ | no ¬p | zero = refl %% lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) ) -%% lemma5 : {c10 :ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond +%% lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond %% lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in %% begin %% termCond env @@ -684,7 +687,7 @@ %% ∎ %% ) %% \end{lstlisting} -proof1 は Code \ref{Agda-hoare-prog}の program と似た形をとっている。 +proof1 は Code \ref{agda-hoare-prog}の program と似た形をとっている。 HoareLogic では Comannd に対応する証明規則があるため、証明はプログラムに対応する形になる。 \section{Gears ベースの HoareLogic の証明} @@ -697,10 +700,11 @@ こちらも通常の HoareLogic と同様に \ref{agda-while} のwhileプログラムと同様のものを記述する Code \ref{Gears-hoare-while} は、 CodeGear、 DataGear を用いた Agda 上での while Program の記述であり、証明でもある。 -\begin{lstlisting}[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while] -proofGears : {c10 : ℕ } → Set -proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) -\end{lstlisting} +\lstinputlisting[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while]{src/gears.agda.replaced} +%% \begin{lstlisting}[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while] +%% proofGears : {c10 : ℕ } → Set +%% proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +%% \end{lstlisting} Code \ref{Gears-hoare-while} で使われている CodeGear を見ていく 始めに Code \ref{gears-while} の whileTest では変数 i、n にそれぞれ 0 と 10 を代入している。 @@ -714,61 +718,62 @@ を行う。 そして、ループを抜けた後の termCondition は $i == 10$ となる。 -\begin{lstlisting}[caption=Gears whileProgram, label=gears-while] -whileTest : {l : Level} {t : Set l} -> {c10 : ℕ } → (Code : (env : Env) -> - ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t -whileTest {_} {_} {c10} next = next env proof2 - where - env : Env - env = record {vari = 0 ; varn = c10} - proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) - proof2 = record {pi1 = refl ; pi2 = refl} +\lstinputlisting[caption=Gears whileProgram, label=gears-while]{src/gears-while.agda.replaced} +%% \begin{lstlisting}[caption=Gears whileProgram, label=gears-while] +%% whileTest : {l : Level} {t : Set l} -> {c10 : ℕ } → (Code : (env : Env) -> +%% ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t +%% whileTest {_} {_} {c10} next = next env proof2 +%% where +%% env : Env +%% env = record {vari = 0 ; varn = c10} +%% proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) +%% proof2 = record {pi1 = refl ; pi2 = refl} -conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c\ -10) - -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ c10) -> t) -> t -conversion1 env {c10} p1 next = next env proof4 - where - proof4 : varn env + vari env ≡ c10 - proof4 = let open ≡-Reasoning in - begin - varn env + vari env - ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ - c10 + vari env - ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ - c10 + 0 - ≡⟨ +-sym {c10} {0} ⟩ - c10 - ∎ +%% conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c\ +%% 10) +%% -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ c10) -> t) -> t +%% conversion1 env {c10} p1 next = next env proof4 +%% where +%% proof4 : varn env + vari env ≡ c10 +%% proof4 = let open ≡-Reasoning in +%% begin +%% varn env + vari env +%% ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ +%% c10 + vari env +%% ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ +%% c10 + 0 +%% ≡⟨ +-sym {c10} {0} ⟩ +%% c10 +%% ∎ -{-# TERMINATING #-} -whileLoop : {l : Level} {t : Set l} -> (env : Env) -> {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) -> (Co\ -de : Env -> t) -> t -whileLoop env proof next with ( suc zero ≤? (varn env) ) -whileLoop env proof next | no p = next env -whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next - where - env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} - 1<0 : 1 ≤ zero → ⊥ - 1<0 () - proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10 - proof3 (s≤s lt) with varn env - proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) - proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in - begin - n' + (vari env + 1) - ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ - n' + (1 + vari env ) - ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ - (n' + 1) + vari env - ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ - (suc n' ) + vari env - ≡⟨⟩ - varn env + vari env - ≡⟨ proof ⟩ - c10 - ∎ -\end{lstlisting} +%% {-# TERMINATING #-} +%% whileLoop : {l : Level} {t : Set l} -> (env : Env) -> {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) -> (Co\ +%% de : Env -> t) -> t +%% whileLoop env proof next with ( suc zero ≤? (varn env) ) +%% whileLoop env proof next | no p = next env +%% whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next +%% where +%% env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} +%% 1<0 : 1 ≤ zero → ⊥ +%% 1<0 () +%% proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10 +%% proof3 (s≤s lt) with varn env +%% proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) +%% proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in +%% begin +%% n' + (vari env + 1) +%% ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ +%% n' + (1 + vari env ) +%% ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ +%% (n' + 1) + vari env +%% ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ +%% (suc n' ) + vari env +%% ≡⟨⟩ +%% varn env + vari env +%% ≡⟨ proof ⟩ +%% c10 +%% ∎ +%% \end{lstlisting} \section{まとめと今後の課題}