Mercurial > hg > Papers > 2019 > ryokka-sigss

changeset 6:dbff3c44dc88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix some, but utf8 char invisible...
author ryokka
date Tue, 18 Dec 2018 01:45:09 +0900
parents 493983f2c9db
children b5f17725a347
files Paper/tecrep.pdf Paper/tecrep.tex
diffstat 2 files changed, 90 insertions(+), 69 deletions(-) [+]
line wrap: on
line diff
Binary file Paper/tecrep.pdf has changed
--- a/Paper/tecrep.tex	Tue Dec 18 00:12:40 2018 +0900
+++ b/Paper/tecrep.tex	Tue Dec 18 01:45:09 2018 +0900
@@ -4,7 +4,6 @@
 
 \usepackage[dvipdfmx]{graphicx}
 \usepackage{graphicx}
-\usepackage[T1]{fontenc}
 \usepackage{lmodern}
 \usepackage{textcomp}
 \usepackage{latexsym}
@@ -12,7 +11,11 @@
 %\usepackage{amssymb}
 \usepackage{url}
 \usepackage{cite}
+\usepackage[portuguese]{babel}
+\usepackage[utf8]{inputenc}
+\usepackage{listingsutf8}
 \usepackage{listings}
+\usepackage{inconsolata}
 \lstset{
   frame=single,
   keepspaces=true,
@@ -20,7 +23,7 @@
   commentstyle={\ttfamily},
   identifierstyle={\ttfamily},
   keywordstyle={\ttfamily},
-  basicstyle=\small,
+%  basicstyle=\footnotesize,
   breaklines=true,
   xleftmargin=0zw,
   xrightmargin=0zw,
@@ -33,9 +36,15 @@
   language={},
   tabsize=4,
   lineskip=-0.5zw,
-    inputencoding=utf8,
-    extendedchars=true,
-    escapechar={@}
+  inputencoding=utf8,
+  extendedchars=true,
+  escapechar={@},
+  escapeinside={\%*}{*},
+  literate=
+  {⟨}{{\langle}}1
+  {⟩}{{\rangle}}1
+  {ℕ}{{$\mathbb{N}$}}1
+  {^^e2^^84^^95}{{$\mathbb{N}$}}1
 }
 
 % basicstyle={\ttfamily},
@@ -143,20 +152,22 @@
  Code \ref{agda-record} はレコード型の例であり、Env では varn と vari の二つの field を持ち、
 それぞれの型が Agda 上で自然数を表す Nat になっている。
 
-\begin{lstlisting}[caption=record の例,label=agda-record]
-record Env : Set where
-  field
-    varn : ℕ
-    vari : ℕ
-\end{lstlisting}
+\lstinputlisting[caption=record の例,label=agda-record]{src/data.agda.replaced}
+%% \begin{lstlisting}[caption=record の例,label=agda-record]
+%% record Env : Set where
+%%   field
+%%     varn : ℕ
+%%     vari : ℕ
+%% \end{lstlisting}
 
 関数の定義は、関数名と型を記述した後に関数の本体を = の後に記述する。関数の型には → 、または-> を用いる。
 例えば引数が型 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
@@ -171,7 +182,7 @@
 $y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$
 を用いて証明している。
 \begin{lstlisting}[caption=等式変形の例,label=proof]
-+zero : { y : ℕ } → y + zero  ≡ y
++zero : { y :ℕ } → y + zero  ≡ y
 +zero {zero} = refl
 +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
 \end{lstlisting}
@@ -183,10 +194,10 @@
 $--$ は Agda 上ではコメントである。
 
 \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre]
-stmt2Cond : {c10 : ℕ} → Cond
+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\
+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
@@ -210,14 +221,14 @@
 ∧true {x} | false = refl
 ∧true {x} | true = refl
 
-stmt1Cond : {c10 : ℕ} → Cond
+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\
+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
@@ -272,7 +283,7 @@
  Code \ref{agda-gc}は Agda で書いた CodeGear の型の例である。
 
 \begin{lstlisting}[caption= whileTest の型,label=agda-cg]
-whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t
+whileTest : {l : Level} {t : Set l} -> (c10 :ℕ) → (Code : Env -> t) -> t
 whileTest c10 next = next (record {varn = c10 ; vari = 0} )
 \end{lstlisting}
 
@@ -363,8 +374,8 @@
 \begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare]
 record Env : Set where
   field
-    varn : ℕ
-    vari : ℕ
+    varn :ℕ
+    vari :ℕ
 open Env
 
 PrimComm : Set
@@ -495,41 +506,23 @@
 
 Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram を証明する。
 
- 
-\begin{lstlisting}[caption=whileProgram Condition, label=while-cond]
-initCond : Cond
-initCond env = true
-
-stmt1Cond : {c10 : ℕ} → Cond
-stmt1Cond {c10} env = Equal (varn env) c10
-
-init-case : {c10 :  ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari \
-= vari env }) ) ≡ true
-init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
-
-init-type : {c10 :  ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Co\
-nd {c10})
-init-type {c10} env = init-case env
-
-stmt2Cond : {c10 : ℕ} → Cond
-stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
-
-whileInv : {c10 : ℕ} → Cond
-whileInv {c10} env = Equal ((varn env) + (vari env)) c10
-
-whileInv' : {c10 : ℕ} → Cond
-whileInv' {c10}  env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
-
-termCond : {c10 : ℕ} → Cond
-termCond {c10} env = Equal (vari env) c10
-\end{lstlisting}
-
-証明は  Code \ref{agda-hoare-while}の proof1 の様になる。
+全体の証明は  Code \ref{agda-hoare-while}の proof1 の様になる。
 proof1 では型で initCond、  Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、
 initCond から program を実行し termCond に行き着く HoareLogic の証明になっている。
 
-lemma1 から lemma5 は Code \ref{agda-hoare-while-lemma} の通りで、
-lemma1 が
+それぞれの Condition は Rule の後に記述されている {} に囲まれた部分で、
+initCondのみ無条件で true を返す Condition になっている。
+
+それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。
+lemma1 から lemma5 の証明は長く、
+論文のページ上限を超えてしまうため 当研究室レポジトリ \cite{cr-ryukyu} のプログラムを参照していただきたい。
+
+これらの lemma は HTProof の Rule に沿って必要なものを記述されており、
+lemma1 では PreCondition と PostCondition が存在するときの代入の保証、
+lemma2 では While Loop に入る前の Condition からループ不変条件への変換の証明、
+lemma3 では While Loop 内での PComm の代入の証明、
+lemma4 では While Loop を抜けたときの Condition の整合性、
+lemma5 では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。
 
 \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]  
 proof1 : HTProof initCond program termCond
@@ -542,8 +535,36 @@
                      $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
 \end{lstlisting}
 
+%% \begin{lstlisting}[caption=whileProgram Condition, label=while-cond]
+%% initCond : Cond
+%% initCond env = true
+
+%% stmt1Cond : {c10 :ℕ} → Cond
+%% stmt1Cond {c10} env = Equal (varn env) c10
+
+%% init-case : {c10 : ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari \
+%% = vari env }) ) ≡ true
+%% init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
+
+%% init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Co\
+%% nd {c10})
+%% init-type {c10} env = init-case env
+
+%% stmt2Cond : {c10 :ℕ} → Cond
+%% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
+
+%% whileInv : {c10 :ℕ} → Cond
+%% whileInv {c10} env = Equal ((varn env) + (vari env)) c10
+
+%% whileInv' : {c10 :ℕ} → Cond
+%% whileInv' {c10}  env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
+
+%% 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
@@ -554,11 +575,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
@@ -571,7 +592,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
@@ -614,24 +635,24 @@
 %%           ≡⟨ ∧-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
-%%           ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-predℕ=n c2) )  ⟩
-%%             Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
+%%           ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-pred*ℕ*=n c2) )  ⟩
+%%             Equal ((suc (pred*ℕ* {varn env} c2 ) - 1) + vari env) c10
 %%           ≡⟨⟩
-%%             Equal ((predℕ {varn env} c2 ) + vari env) c10
+%%             Equal ((pred*ℕ* {varn env} c2 ) + vari env) c10
 %%           ≡⟨  Equal+1 ⟩
-%%             Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
-%%           ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-predℕ=n c2 )  ⟩
+%%             Equal ((suc (pred*ℕ* {varn env} c2 )) + vari env) (suc c10)
+%%           ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-pred*ℕ*=n c2 )  ⟩
 %%             Equal (varn env + vari env) (suc c10)
 %%           ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
 %%             Equal (suc c10) (suc c10)
 %%           ≡⟨ ≡→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 })
@@ -648,7 +669,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
@@ -677,7 +698,7 @@
 Code \ref{Gears-hoare-while} は、 CodeGear、 DataGear を用いた Agda 上での while Program の記述であり、証明でもある。
 
 \begin{lstlisting}[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while]
-proofGears : {c10 :  ℕ } → Set
+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 を見ていく
@@ -694,7 +715,7 @@
 そして、ループを抜けた後の termCondition は $i == 10$ となる。
 
 \begin{lstlisting}[caption=Gears whileProgram, label=gears-while]
-whileTest : {l : Level} {t : Set l}  -> {c10 :  ℕ } → (Code : (env : Env)  ->
+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
@@ -703,7 +724,7 @@
     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\
+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
@@ -721,7 +742,7 @@
           ∎
 
 {-# TERMINATING #-}
-whileLoop : {l : Level} {t : Set l} -> (env : Env) -> {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) -> (Co\
+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