# HG changeset patch # User soto # Date 1636093148 -32400 # Node ID 9176dff8f38a1712a94a0f7aa65d8576751b3031 # Parent 3910f4639344c9be8ca525bd89278c88e272589d ADD while loop description diff -r 3910f4639344 -r 9176dff8f38a Paper/.DS_Store Binary file Paper/.DS_Store has changed diff -r 3910f4639344 -r 9176dff8f38a Paper/escape_agda.rb --- a/Paper/escape_agda.rb Tue Nov 02 06:58:39 2021 +0900 +++ b/Paper/escape_agda.rb Fri Nov 05 15:19:08 2021 +0900 @@ -28,7 +28,8 @@ '⊥' => 'bot', '∀' => 'forall', '#' => '\#', - '⊤' => '\top' + '⊤' => '\top', + '\'' => '\prime' } code = File.read(FileName) diff -r 3910f4639344 -r 9176dff8f38a Paper/soto.pdf Binary file Paper/soto.pdf has changed diff -r 3910f4639344 -r 9176dff8f38a Paper/soto.tex --- a/Paper/soto.tex Tue Nov 02 06:58:39 2021 +0900 +++ b/Paper/soto.tex Fri Nov 05 15:19:08 2021 +0900 @@ -74,21 +74,20 @@ \end{abstract} \begin{jkeyword} -プログラミング言語, Perl6, サーバー, Raku +プログラミング言語, CbC, Gears OS, Agda, 検証 \end{jkeyword} \maketitle % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \input{tex/intro.tex} % はじめに -\input{tex/cbc.tex} % cbcの説明 -\input{tex/agda.tex} % agdaの説明 -\input{tex/cbc_agda.tex}% cbcとagda(gearsagda) -\input{tex/hoare.tex} % hoare logicの説明 -% while loopの実装(簡単に) -% while loopの検証 -% red black treeの実装(こいつも簡単に) -% red black treeの検証 +\input{tex/cbc.tex} % cbc の説明 +\input{tex/agda.tex} % agda の説明 +\input{tex/cbc_agda.tex}% cbc と agda(gearsagda) +\input{tex/hoare.tex} % hoare logic の説明 +\input{tex/while_loop.tex} % while loop の実装と検証(簡単に) +% red black tree の実装(こいつも簡単に) +% red black tree の検証 % まとめ \nocite{*} diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/And.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/And.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,4 @@ +record _@$\wedge$@_ (A B : Set) : Set where + field + p1 : A + p2 : B diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/Nat.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/Nat.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,3 @@ +data @$\mathbb{N}$@ : Set where + zero : @$\mathbb{N}$@ + suc : (n : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/_Fresh.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/_Fresh.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,211 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in +-- "A Formalised Proof of the Soundness and Completeness of a Simply Typed +-- Lambda-Calculus with Explicit Substitutions" +------------------------------------------------------------------------ + +-- See README.Data.List.Fresh and README.Data.Trie.NonDependent for +-- examples of how to use fresh lists. + +{-@$\#$@ OPTIONS --without-K --safe @$\#$@-} + +module Data.List.Fresh where + +open import Level using (Level; _@$\sqcup$@_) +open import Data.Bool.Base using (true; false) +open import Data.Unit.Polymorphic.Base using (@$\top$@) +open import Data.Product using (∃; _@$\times$@_; _,_; -,_; proj@$\_{1}$@; proj@$\_{2}$@) +open import Data.List.Relation.Unary.All using (All; []; _@$\text{::}$@_) +open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _@$\text{::}$@_) +open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) +open import Data.Nat.Base using (@$\mathbb{N}$@; zero; suc) +open import Function using (_∘′_; flip; id; _on_) +open import Relation.Nullary using (does) +open import Relation.Unary as U using (Pred) +open import Relation.Binary as B using (Rel) +open import Relation.Nary + +private + variable + a b p r s : Level + A : Set a + B : Set b + +------------------------------------------------------------------------ +-- Basic type + +-- If we pick an R such that (R a b) means that a is different from b +-- then we have a list of distinct values. + +module _ {a} (A : Set a) (R : Rel A r) where + + data List@$\#$@ : Set (a @$\sqcup$@ r) + fresh : (a : A) (as : List@$\#$@) @$\rightarrow$@ Set r + + data List@$\#$@ where + [] : List@$\#$@ + cons : (a : A) (as : List@$\#$@) @$\rightarrow$@ fresh a as @$\rightarrow$@ List@$\#$@ + + -- Whenever R can be reconstructed by η-expansion (e.g. because it is + -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we + -- do not care about the proof, it is convenient to get back list syntax. + + -- We use a different symbol to avoid conflict when importing both Data.List + -- and Data.List.Fresh. + infixr 5 _@$\text{::}$@@$\#$@_ + pattern _@$\text{::}$@@$\#$@_ x xs = cons x xs _ + + fresh a [] = @$\top$@ + fresh a (x @$\text{::}$@@$\#$@ xs) = R a x @$\times$@ fresh a xs + +-- Convenient notation for freshness making A and R implicit parameters +infix 5 _@$\#$@_ +_@$\#$@_ : {R : Rel A r} (a : A) (as : List@$\#$@ A R) @$\rightarrow$@ Set r +_@$\#$@_ = fresh _ _ + +------------------------------------------------------------------------ +-- Operations for modifying fresh lists + +module _ {R : Rel A r} {S : Rel B s} (f : A @$\rightarrow$@ B) (R@$\Rightarrow$@S : @$\forall$@[ R @$\Rightarrow$@ (S on f) ]) where + + map : List@$\#$@ A R @$\rightarrow$@ List@$\#$@ B S + map-@$\#$@ : @$\forall$@ {a} as @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ f a @$\#$@ map as + + map [] = [] + map (cons a as ps) = cons (f a) (map as) (map-@$\#$@ as ps) + + map-@$\#$@ [] _ = _ + map-@$\#$@ (a @$\text{::}$@@$\#$@ as) (p , ps) = R@$\Rightarrow$@S p , map-@$\#$@ as ps + +module _ {R : Rel B r} (f : A @$\rightarrow$@ B) where + + map@$\_{1}$@ : List@$\#$@ A (R on f) @$\rightarrow$@ List@$\#$@ B R + map@$\_{1}$@ = map f id + +module _ {R : Rel A r} {S : Rel A s} (R@$\Rightarrow$@S : @$\forall$@[ R @$\Rightarrow$@ S ]) where + + map@$\_{2}$@ : List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A S + map@$\_{2}$@ = map id R@$\Rightarrow$@S + +------------------------------------------------------------------------ +-- Views + +data Empty {A : Set a} {R : Rel A r} : List@$\#$@ A R @$\rightarrow$@ Set (a @$\sqcup$@ r) where + [] : Empty [] + +data NonEmpty {A : Set a} {R : Rel A r} : List@$\#$@ A R @$\rightarrow$@ Set (a @$\sqcup$@ r) where + cons : @$\forall$@ x xs pr @$\rightarrow$@ NonEmpty (cons x xs pr) + +------------------------------------------------------------------------ +-- Operations for reducing fresh lists + +length : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ @$\mathbb{N}$@ +length [] = 0 +length (_ @$\text{::}$@@$\#$@ xs) = suc (length xs) + +------------------------------------------------------------------------ +-- Operations for constructing fresh lists + +pattern [_] a = a @$\text{::}$@@$\#$@ [] + +fromMaybe : {R : Rel A r} @$\rightarrow$@ Maybe A @$\rightarrow$@ List@$\#$@ A R +fromMaybe nothing = [] +fromMaybe (just a) = [ a ] + +module _ {R : Rel A r} (R-refl : B.Reflexive R) where + + replicate : @$\mathbb{N}$@ @$\rightarrow$@ A @$\rightarrow$@ List@$\#$@ A R + replicate-@$\#$@ : (n : @$\mathbb{N}$@) (a : A) @$\rightarrow$@ a @$\#$@ replicate n a + + replicate zero a = [] + replicate (suc n) a = cons a (replicate n a) (replicate-@$\#$@ n a) + + replicate-@$\#$@ zero a = _ + replicate-@$\#$@ (suc n) a = R-refl , replicate-@$\#$@ n a + +------------------------------------------------------------------------ +-- Operations for deconstructing fresh lists + +uncons : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe (A @$\times$@ List@$\#$@ A R) +uncons [] = nothing +uncons (a @$\text{::}$@@$\#$@ as) = just (a , as) + +head : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe A +head = Maybe.map proj@$\_{1}$@ ∘′ uncons + +tail : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ Maybe (List@$\#$@ A R) +tail = Maybe.map proj@$\_{2}$@ ∘′ uncons + +take : {R : Rel A r} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R +take-@$\#$@ : {R : Rel A r} @$\rightarrow$@ @$\forall$@ n a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ take n as + +take zero xs = [] +take (suc n) [] = [] +take (suc n) (cons a as ps) = cons a (take n as) (take-@$\#$@ n a as ps) + +take-@$\#$@ zero a xs _ = _ +take-@$\#$@ (suc n) a [] ps = _ +take-@$\#$@ (suc n) a (x @$\text{::}$@@$\#$@ xs) (p , ps) = p , take-@$\#$@ n a xs ps + +drop : {R : Rel A r} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R +drop zero as = as +drop (suc n) [] = [] +drop (suc n) (a @$\text{::}$@@$\#$@ as) = drop n as + +module _ {P : Pred A p} (P? : U.Decidable P) where + + takeWhile : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R + takeWhile-@$\#$@ : @$\forall$@ {R : Rel A r} a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ takeWhile as + + takeWhile [] = [] + takeWhile (cons a as ps) with does (P? a) + ... | true = cons a (takeWhile as) (takeWhile-@$\#$@ a as ps) + ... | false = [] + + takeWhile-@$\#$@ a [] _ = _ + takeWhile-@$\#$@ a (x @$\text{::}$@@$\#$@ xs) (p , ps) with does (P? x) + ... | true = p , takeWhile-@$\#$@ a xs ps + ... | false = _ + + dropWhile : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R + dropWhile [] = [] + dropWhile aas@(a @$\text{::}$@@$\#$@ as) with does (P? a) + ... | true = dropWhile as + ... | false = aas + + filter : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ List@$\#$@ A R + filter-@$\#$@ : @$\forall$@ {R : Rel A r} a (as : List@$\#$@ A R) @$\rightarrow$@ a @$\#$@ as @$\rightarrow$@ a @$\#$@ filter as + + filter [] = [] + filter (cons a as ps) with does (P? a) + ... | true = cons a (filter as) (filter-@$\#$@ a as ps) + ... | false = filter as + + filter-@$\#$@ a [] _ = _ + filter-@$\#$@ a (x @$\text{::}$@@$\#$@ xs) (p , ps) with does (P? x) + ... | true = p , filter-@$\#$@ a xs ps + ... | false = filter-@$\#$@ a xs ps + +------------------------------------------------------------------------ +-- Relationship to List and AllPairs + +toList : {R : Rel A r} @$\rightarrow$@ List@$\#$@ A R @$\rightarrow$@ ∃ (AllPairs R) +toAll : @$\forall$@ {R : Rel A r} {a} as @$\rightarrow$@ fresh A R a as @$\rightarrow$@ All (R a) (proj@$\_{1}$@ (toList as)) + +toList [] = -, [] +toList (cons x xs ps) = -, toAll xs ps @$\text{::}$@ proj@$\_{2}$@ (toList xs) + +toAll [] ps = [] +toAll (a @$\text{::}$@@$\#$@ as) (p , ps) = p @$\text{::}$@ toAll as ps + +fromList : @$\forall$@ {R : Rel A r} {xs} @$\rightarrow$@ AllPairs R xs @$\rightarrow$@ List@$\#$@ A R +fromList-@$\#$@ : @$\forall$@ {R : Rel A r} {x xs} (ps : AllPairs R xs) @$\rightarrow$@ + All (R x) xs @$\rightarrow$@ x @$\#$@ fromList ps + +fromList [] = [] +fromList (r @$\text{::}$@ rs) = cons _ (fromList rs) (fromList-@$\#$@ rs r) + +fromList-@$\#$@ [] _ = _ +fromList-@$\#$@ (p @$\text{::}$@ ps) (r @$\text{::}$@ rs) = r , fromList-@$\#$@ ps rs diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/abridgement.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/abridgement.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,22 @@ +module abridgement where + +open import Data.Nat + +record env : Set where + field + a : @$\mathbb{N}$@ + b : @$\mathbb{N}$@ + c : @$\mathbb{N}$@ +open env + +patternmatch-default : env @$\rightarrow$@ @$\mathbb{N}$@ +patternmatch-default record { a = a ; b = b ; c = c } = c + +patternmatch-extraction : env @$\rightarrow$@ @$\mathbb{N}$@ +patternmatch-extraction env with c env +patternmatch-extraction env | c = c + +patternmatch-extraction' : env @$\rightarrow$@ @$\mathbb{N}$@ +patternmatch-extraction' env with c env +... | c = c + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/cbc-agda.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/cbc-agda.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,22 @@ +module cbc-agda where + +open import Data.Nat +open import Level renaming ( suc to succ ; zero to Zero ) + +record Env : Set where + field + varx : @$\mathbb{N}$@ + vary : @$\mathbb{N}$@ +open Env + +plus-com : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-com env next exit with vary env +... | zero = exit (record { varx = varx env ; vary = vary env }) +... | suc y = next (record { varx = suc (varx env) ; vary = y }) + +{-@$\#$@ TERMINATING @$\#$@-} +plus-p : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-p env exit = plus-com env ( @$\lambda$@ env @$\rightarrow$@ plus-p env exit ) exit + +plus : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Env +plus x y = plus-p (record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env) diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/cmp.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/cmp.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,15 @@ +module cmp where + +open import Data.Nat +open import Data.Nat.Properties as NatProp -- <-cmp +open import Relation.Binary + +compare_test : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ +compare_test x y with <-cmp x y +... | tri< a @$\neg$@b @$\neg$@c = y +... | tri≈ @$\neg$@a b @$\neg$@c = x +... | tri> @$\neg$@a @$\neg$@b c = x + +-- test = compare_test 7 2 +-- 7 + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/fresh_test.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/fresh_test.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,14 @@ +module fresh_test where + +open import Data.Nat +open import Data.List.Base +open import Data.List.Fresh +open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) +open import Data.Product +open import Relation.Nary using (⌊_⌋; fromWitness) + +ISortedList : Set +ISortedList = List@$\#$@ @$\mathbb{N}$@ ⌊ _>?_ ⌋ + +ins : ISortedList +ins = 8 @$\text{::}$@@$\#$@ 4 @$\text{::}$@@$\#$@ 2 @$\text{::}$@@$\#$@ 0 @$\text{::}$@@$\#$@ [] diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/hoare-test.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/hoare-test.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,103 @@ +module hoare-test where + +open import Data.Nat hiding (_@$\sqcup$@_) +open import Level renaming ( suc to succ ; zero to Zero ) + +open import Relation.Binary +open import Relation.Binary.PropositionalEquality + +open import Relation.Nullary hiding (proof) + +open import Data.Nat.Properties as NatProp -- <-cmp + +record Env : Set where + field + var-init-x : @$\mathbb{N}$@ + var-init-y : @$\mathbb{N}$@ + var-x : @$\mathbb{N}$@ + var-y : @$\mathbb{N}$@ +open Env + +plus-com : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-com env next exit with var-y env +... | zero = exit record env{var-x = var-x env ; var-y = zero} +... | suc y = next record env{var-x = suc (var-x env) ; var-y = y} + +plus-init : {l : Level} {t : Set l} @$\rightarrow$@ ( x y : @$\mathbb{N}$@ ) @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-init x y next = next (record { var-init-x = x ; var-init-y = y ; var-x = x ; var-y = y }) + +{-@$\#$@ TERMINATING @$\#$@-} +plus-p : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-p env exit = plus-com env ( @$\lambda$@ env @$\rightarrow$@ plus-p env exit ) exit + +plus : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Env +plus x y = plus-init x y (@$\lambda$@ env @$\rightarrow$@ plus-p env (@$\lambda$@ env @$\rightarrow$@ env)) +--(record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env) + +-- ここまでplusの定義 + +-- mdg (meta code gear) +data mdg-state : Set where + s-init : mdg-state + s-doing : mdg-state + s-fin : mdg-state + +record _@$\wedge$@_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where + field + proj1 : A + proj2 : B + +-- mcg (meta code gear) +plus-mdg : mdg-state @$\rightarrow$@ Env @$\rightarrow$@ Set +plus-mdg s-init env = (var-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-y env @$\equiv$@ var-init-y env) +plus-mdg s-doing env = (var-init-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-init-y env @$\equiv$@ var-init-y env) -- よくないmdg +plus-mdg s-fin env = (var-init-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-init-y env @$\equiv$@ var-init-y env) -- よくないmdg + +-- 実行のwrapperを作って、そこでmcgが適切に選ばれて接続をしたい。多分できる気がする。 +plus-init-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (x y : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Env ) @$\rightarrow$@ plus-mdg s-init env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-init-mcg x y next = next ( plus-init x y ( @$\lambda$@ env @$\rightarrow$@ env ) ) record { proj1 = refl ; proj2 = refl } where + +plus-com-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env ) @$\rightarrow$@ (next : (env : Env ) @$\rightarrow$@ plus-mdg s-doing env @$\rightarrow$@ t) @$\rightarrow$@ (exit : (env : Env ) @$\rightarrow$@ plus-mdg s-fin env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-com-mcg env-in next exit with (var-y env-in) +... | suc y = next ( plus-com env-in ( @$\lambda$@ env @$\rightarrow$@ env ) ( @$\lambda$@ env @$\rightarrow$@ env ) ) (record { proj1 = refl ; proj2 = refl }) where +... | zero = exit env-in (record { proj1 = refl ; proj2 = refl }) + +--plus-com-mcg +{-@$\#$@ TERMINATING @$\#$@-} +plus-p-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : (env : Env ) @$\rightarrow$@ plus-mdg s-fin env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-p-mcg env exit = plus-com-mcg env (@$\lambda$@ env s @$\rightarrow$@ plus-p-mcg env exit ) exit + +plus-mcg : (x y : @$\mathbb{N}$@) @$\rightarrow$@ Env +plus-mcg x y = plus-init-mcg x y (@$\lambda$@ env s @$\rightarrow$@ plus-p-mcg env (@$\lambda$@ env s @$\rightarrow$@ env)) + +test1 = plus-mcg 3 4 + +{- +next env ? where + env : Env + env = plus-com env-in {!!} {!!} +-} +--plus-mdg s-init (plus-p record env{var-x = var-init-x env ; var-y = var-init-y env} (@$\lambda$@ env @$\rightarrow$@ env)) + + + +{- +whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t +whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where + env : Envc + env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env ) +-} + +data hoare-cond : Set where + p : hoare-cond + q : hoare-cond + + +{- +continuation-hoare-triple : {l : Level} {t : Set l} @$\rightarrow$@ hoare-cond @$\rightarrow$@ (next : Env @$\rightarrow$@ t) Set +continuation-hoare-triple p next = continuation-hoare-triple q +continuation-hoare-triple q next = continuation-hoare-triple p +-} + + + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/hoare-while.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/hoare-while.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,98 @@ +module hoare-while where + +open import Data.Nat +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat.Properties as NatProp -- <-cmp +open import Relation.Binary + +record Envc : Set (succ Zero) where + field + c10 : @$\mathbb{N}$@ + varn : @$\mathbb{N}$@ + vari : @$\mathbb{N}$@ +open Envc + +whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } ) + +whileLoopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopP env next exit with (varn env) +... | zero = exit env +... | suc n = exit (record env { varn = n ; vari = (suc n) }) + + +{-@$\#$@ TERMINATING @$\#$@-} +loopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +loopP env exit = whileLoopP env (@$\lambda$@ env @$\rightarrow$@ loopP env exit ) exit + +whileTestPCall : (c10 : @$\mathbb{N}$@ ) @$\rightarrow$@ Envc +whileTestPCall c10 = whileTestP {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP env (@$\lambda$@ env @$\rightarrow$@ env)) + +--- +open import Data.Empty +--open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) + +--open import Agda.Builtin.Unit +open import utilities + +open import Relation.Binary.PropositionalEquality + +open _@$\wedge$@_ + +data whileTestState : Set where + s1 : whileTestState + s2 : whileTestState + sf : whileTestState + +whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set +whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) +whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) +whileTestStateP sf env = (vari env @$\equiv$@ c10 env) + +whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t +whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where + env : Envc + env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env ) + +whileLoopPwP : {l : Level} {t : Set l} @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env + @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPwP env s next exit with <-cmp 0 (varn env) +whileLoopPwP env s next exit | tri≈ @$\neg$@a b @$\neg$@c = exit env (lem (sym b) s) + where + lem : (varn env @$\equiv$@ 0) @$\rightarrow$@ (varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ vari env @$\equiv$@ c10 env + lem refl refl = refl +whileLoopPwP env s next exit | tri< a @$\neg$@b @$\neg$@c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a) + where + 1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@ + 1<0 () + proof5 : (suc zero @$\leq$@ (varn env)) @$\rightarrow$@ ((varn env ) - 1) + (vari env + 1) @$\equiv$@ c10 env + proof5 (s@$\leq$@s lt) with varn env + proof5 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 a) + proof5 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in + begin + n' + (vari env + 1) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ 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 @$\rightarrow$@ z + vari env ) +1@$\equiv$@suc @$\rangle$@ + (suc n' ) + vari env + @$\equiv$@@$\langle$@@$\rangle$@ + varn env + vari env + @$\equiv$@@$\langle$@ s @$\rangle$@ + c10 env + @$\blacksquare$@ + + +whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env + @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPwP' zero env refl refl next exit = exit env refl +whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) + + + +whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ @$\top$@ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c)) +whileTestPSemSound c output refl = whileTestPSem c + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/hoare-while1.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/hoare-while1.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,41 @@ +module hoare-while1 where + +open import Level renaming (suc to Suc ; zero to Zero ) +module WhileTest where + +open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Core +open import Data.Nat hiding (compare) +open import Data.Maybe +open import Data.List +open import Function +open import logic + +record Env : Set (Suc Zero) where + field + varn : @$\mathbb{N}$@ + vari : @$\mathbb{N}$@ +open Env + +record WhileTest {m : Level } {t : Set m } : Set (Suc m) where + field + env : Env + whileInit : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Env @$\rightarrow$@ t) @$\rightarrow$@ t + whileInit c10 next = next (record {varn = c10 ; vari = 0 } ) + whileLoop : Env @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t + whileLoop env next = whileLoop1 (varn env) env where + whileLoop1 : @$\mathbb{N}$@ @$\rightarrow$@ Env @$\rightarrow$@ t + whileLoop1 zero env = next env + whileLoop1 (suc t ) env = + whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) + whileTest : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Env @$\rightarrow$@ t) @$\rightarrow$@ t + whileTest c10 next = whileInit c10 $ @$\lambda$@ env @$\rightarrow$@ whileLoop env next + +open WhileTest + +createWhileTest : {m : Level} {t : Set m } @$\rightarrow$@ WhileTest {m} {t} +createWhileTest = record { env = record { varn = 0; vari = 0 } } + +test2 : @$\mathbb{N}$@ +test2 = whileTest createWhileTest 10 $ @$\lambda$@ e @$\rightarrow$@ vari e + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/lambda.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/lambda.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,28 @@ +module lambda where + +open import Data.Nat + +ll+_ : (x y : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ +ll+ zero = @$\lambda$@ y @$\rightarrow$@ y +ll+ suc x = @$\lambda$@ y @$\rightarrow$@ (ll+ x) (suc y) + +test = (ll+ 5) 7 + +-- +1をしたのち、もう一度+1をする関数を定義する場合 + ++1 : (x : @$\mathbb{N}$@ )@$\rightarrow$@ @$\mathbb{N}$@ ++1 x = suc x + ++n : (a : @$\mathbb{N}$@) @$\rightarrow$@ (x : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ ++n a x = x a + +test*2 : (a : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ +test*2 a = +n a (@$\lambda$@ z @$\rightarrow$@ z + 2) + +test*2' : (a : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ +test*2' a = +n a (@$\lambda$@ z @$\rightarrow$@ +n z (@$\lambda$@ z @$\rightarrow$@ z)) + + +@$\lambda$@'+2 : (x : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ +@$\lambda$@'+2 d = {!!} -- (@$\lambda$@ x @$\rightarrow$@ x +1) + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/list-any.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/list-any.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,73 @@ +module list-any where + +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_@$\equiv$@_; refl; sym; trans; cong) +open Eq.@$\equiv$@-Reasoning +open import Data.Bool using (Bool; true; false; T; _@$\wedge$@_; _∨_; not) +open import Data.Nat using (@$\mathbb{N}$@; zero; suc; _+_; _*_; _∸_; _@$\leq$@_; s@$\leq$@s; z@$\leq$@n) +open import Data.Nat.Properties using + (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ) +open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) +open import Data.Product using (_@$\times$@_; ∃; ∃-syntax) renaming (_,_ to @$\langle$@_,_@$\rangle$@) +open import Function using (_∘_) +open import Level using (Level) +--open import plfa.part1.Isomorphism using (_≃_; _⇔_) + +open import Data.List +open import Data.Nat.Properties as NatProp -- <-cmp +open import Relation.Binary + +open import rbt_t + +-- infix 4 _∈_ _∉_ + +test-l : List @$\mathbb{N}$@ +test-l = 1 @$\text{::}$@ 2 @$\text{::}$@ [] + +data Any-test {A : Set} (P : A @$\rightarrow$@ Set) : List A @$\rightarrow$@ Set where + here : @$\forall$@ {x : A} {xs : List A} @$\rightarrow$@ P x @$\rightarrow$@ Any-test P (x @$\text{::}$@ xs) + there : @$\forall$@ {x : A} {xs : List A} @$\rightarrow$@ Any-test P xs @$\rightarrow$@ Any-test P (x @$\text{::}$@ xs) + +{- +_∈_ : @$\forall$@ {A : Set} (x : A) (xs : List A) @$\rightarrow$@ Set +x ∈ xs = Any (x @$\equiv$@_) xs +-} + +_∈1_ : @$\forall$@ (n : @$\mathbb{N}$@) (xs : List @$\mathbb{N}$@) @$\rightarrow$@ Set +n ∈1 [] = Any-test (n @$\equiv$@_) [] +n ∈1 l@(x @$\text{::}$@ xs) with <-cmp n x +... | tri< a @$\neg$@b @$\neg$@c = Any-test (n @$\equiv$@_) xs +... | tri≈ @$\neg$@a b @$\neg$@c = Any-test (n @$\equiv$@_) l +... | tri> @$\neg$@a @$\neg$@b c = Any-test (n @$\equiv$@_) xs + +test : 1 ∈1 test-l +test = here refl + +data Any (P : @$\mathbb{N}$@ @$\rightarrow$@ Set) : rbt @$\rightarrow$@ Set where + here : @$\forall$@ {x : @$\mathbb{N}$@} {xs : rbt} @$\rightarrow$@ P x @$\rightarrow$@ Any P xs + there : @$\forall$@ {x : @$\mathbb{N}$@} {xs : rbt} @$\rightarrow$@ Any P (get-rbt xs) @$\rightarrow$@ Any P xs + +_∈_ : @$\forall$@ (n : @$\mathbb{N}$@) (xs : rbt) @$\rightarrow$@ Bool +n ∈ bt-empty = false +n ∈ bt-node node with <-cmp n (node.number (tree.key node)) +... | tri< a @$\neg$@b @$\neg$@c = n ∈ (tree.ltree node) +... | tri≈ @$\neg$@a b @$\neg$@c = true +... | tri> @$\neg$@a @$\neg$@b c = n ∈ (tree.rtree node) + + + +testany1 : rbt @$\rightarrow$@ Set +testany1 bt-empty = {!!} +testany1 (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) = {!!} + +testrbt1 = whileTestPCall' bt-empty 0 +testrbt2 = whileTestPCall' (Env.vart testrbt1) 1 +testrbt3 = whileTestPCall' (Env.vart testrbt2) 2 +testrbt4 = whileTestPCall' (Env.vart testrbt3) 3 +testrbt5 = whileTestPCall' (Env.vart testrbt4) 4 +testrbt6 = whileTestPCall' (Env.vart testrbt5) 5 +testrbt7 = whileTestPCall' (Env.vart testrbt6) 6 + + +test1kk = 100 ∈ (Env.vart testrbt6) + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/logic.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/logic.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,152 @@ +module logic where + +open import Level +open import Relation.Nullary +open import Relation.Binary hiding(_⇔_) +open import Data.Empty + + +data Bool : Set where + true : Bool + false : Bool + +record _@$\wedge$@_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where + field + proj1 : A + proj2 : B + +data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where + case1 : A @$\rightarrow$@ A ∨ B + case2 : B @$\rightarrow$@ A ∨ B + +_⇔_ : {n m : Level } @$\rightarrow$@ ( A : Set n ) ( B : Set m ) @$\rightarrow$@ Set (n @$\sqcup$@ m) +_⇔_ A B = ( A @$\rightarrow$@ B ) @$\wedge$@ ( B @$\rightarrow$@ A ) + +contra-position : {n m : Level } {A : Set n} {B : Set m} @$\rightarrow$@ (A @$\rightarrow$@ B) @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ @$\neg$@ A +contra-position {n} {m} {A} {B} f @$\neg$@b a = @$\neg$@b ( f a ) + +double-neg : {n : Level } {A : Set n} @$\rightarrow$@ A @$\rightarrow$@ @$\neg$@ @$\neg$@ A +double-neg A notnot = notnot A + +double-neg2 : {n : Level } {A : Set n} @$\rightarrow$@ @$\neg$@ @$\neg$@ @$\neg$@ A @$\rightarrow$@ @$\neg$@ A +double-neg2 notnot A = notnot ( double-neg A ) + +de-morgan : {n : Level } {A B : Set n} @$\rightarrow$@ A @$\wedge$@ B @$\rightarrow$@ @$\neg$@ ( (@$\neg$@ A ) ∨ (@$\neg$@ B ) ) +de-morgan {n} {A} {B} and (case1 @$\neg$@A) = @$\bot$@-elim ( @$\neg$@A ( _@$\wedge$@_.proj1 and )) +de-morgan {n} {A} {B} and (case2 @$\neg$@B) = @$\bot$@-elim ( @$\neg$@B ( _@$\wedge$@_.proj2 and )) + +dont-or :　{n m : Level} {A : Set n} { B : Set m } @$\rightarrow$@ A ∨ B @$\rightarrow$@ @$\neg$@ A @$\rightarrow$@ B +dont-or {A} {B} (case1 a) @$\neg$@A = @$\bot$@-elim ( @$\neg$@A a ) +dont-or {A} {B} (case2 b) @$\neg$@A = b + +dont-orb :　{n m : Level} {A : Set n} { B : Set m } @$\rightarrow$@ A ∨ B @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ A +dont-orb {A} {B} (case2 b) @$\neg$@B = @$\bot$@-elim ( @$\neg$@B b ) +dont-orb {A} {B} (case1 a) @$\neg$@B = a + + + +infixr 130 _@$\wedge$@_ +infixr 140 _∨_ +infixr 150 _⇔_ + +_@$\wedge$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool +true @$\wedge$@ true = true +_ @$\wedge$@ _ = false + +_\/_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool +false \/ false = false +_ \/ _ = true + +not_ : Bool @$\rightarrow$@ Bool +not true = false +not false = true + +_<=>_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool +true <=> true = true +false <=> false = true +_ <=> _ = false + +infixr 130 _\/_ +infixr 140 _@$\wedge$@_ + +open import Relation.Binary.PropositionalEquality + + +@$\equiv$@-Bool-func : {A B : Bool } @$\rightarrow$@ ( A @$\equiv$@ true @$\rightarrow$@ B @$\equiv$@ true ) @$\rightarrow$@ ( B @$\equiv$@ true @$\rightarrow$@ A @$\equiv$@ true ) @$\rightarrow$@ A @$\equiv$@ B +@$\equiv$@-Bool-func {true} {true} a@$\rightarrow$@b b@$\rightarrow$@a = refl +@$\equiv$@-Bool-func {false} {true} a@$\rightarrow$@b b@$\rightarrow$@a with b@$\rightarrow$@a refl +... | () +@$\equiv$@-Bool-func {true} {false} a@$\rightarrow$@b b@$\rightarrow$@a with a@$\rightarrow$@b refl +... | () +@$\equiv$@-Bool-func {false} {false} a@$\rightarrow$@b b@$\rightarrow$@a = refl + +bool-@$\equiv$@-? : (a b : Bool) @$\rightarrow$@ Dec ( a @$\equiv$@ b ) +bool-@$\equiv$@-? true true = yes refl +bool-@$\equiv$@-? true false = no (@$\lambda$@ ()) +bool-@$\equiv$@-? false true = no (@$\lambda$@ ()) +bool-@$\equiv$@-? false false = yes refl + +@$\neg$@-bool-t : {a : Bool} @$\rightarrow$@ @$\neg$@ ( a @$\equiv$@ true ) @$\rightarrow$@ a @$\equiv$@ false +@$\neg$@-bool-t {true} ne = @$\bot$@-elim ( ne refl ) +@$\neg$@-bool-t {false} ne = refl + +@$\neg$@-bool-f : {a : Bool} @$\rightarrow$@ @$\neg$@ ( a @$\equiv$@ false ) @$\rightarrow$@ a @$\equiv$@ true +@$\neg$@-bool-f {true} ne = refl +@$\neg$@-bool-f {false} ne = @$\bot$@-elim ( ne refl ) + +@$\neg$@-bool : {a : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ @$\bot$@ +@$\neg$@-bool refl () + +lemma-@$\wedge$@-0 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ @$\bot$@ +lemma-@$\wedge$@-0 {true} {true} refl () +lemma-@$\wedge$@-0 {true} {false} () +lemma-@$\wedge$@-0 {false} {true} () +lemma-@$\wedge$@-0 {false} {false} () + +lemma-@$\wedge$@-1 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ @$\bot$@ +lemma-@$\wedge$@-1 {true} {true} refl () +lemma-@$\wedge$@-1 {true} {false} () +lemma-@$\wedge$@-1 {false} {true} () +lemma-@$\wedge$@-1 {false} {false} () + +bool-and-tt : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true +bool-and-tt refl refl = refl + +bool-@$\wedge$@@$\rightarrow$@tt-0 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ true +bool-@$\wedge$@@$\rightarrow$@tt-0 {true} {true} refl = refl +bool-@$\wedge$@@$\rightarrow$@tt-0 {false} {_} () + +bool-@$\wedge$@@$\rightarrow$@tt-1 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true +bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {true} refl = refl +bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {false} () +bool-@$\wedge$@@$\rightarrow$@tt-1 {false} {false} () + +bool-or-1 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ ( a \/ b ) @$\equiv$@ b +bool-or-1 {false} {true} refl = refl +bool-or-1 {false} {false} refl = refl +bool-or-2 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ (a \/ b ) @$\equiv$@ a +bool-or-2 {true} {false} refl = refl +bool-or-2 {false} {false} refl = refl + +bool-or-3 : {a : Bool} @$\rightarrow$@ ( a \/ true ) @$\equiv$@ true +bool-or-3 {true} = refl +bool-or-3 {false} = refl + +bool-or-31 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ true @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true +bool-or-31 {true} {true} refl = refl +bool-or-31 {false} {true} refl = refl + +bool-or-4 : {a : Bool} @$\rightarrow$@ ( true \/ a ) @$\equiv$@ true +bool-or-4 {true} = refl +bool-or-4 {false} = refl + +bool-or-41 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true +bool-or-41 {true} {b} refl = refl + +bool-and-1 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false +bool-and-1 {false} {b} refl = refl +bool-and-2 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false +bool-and-2 {true} {false} refl = refl +bool-and-2 {false} {false} refl = refl + + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/plus.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/plus.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,6 @@ +plus : (x y : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ +plus x zero = x +plus x (suc y) = plus (suc x) y + +-- plus 10 20 +-- 30 diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/plus2.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/plus2.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,10 @@ +module plus2 where + +open import Data.Nat hiding (_+_) + +_+_ : (x y : @$\mathbb{N}$@) @$\rightarrow$@ @$\mathbb{N}$@ +x + zero = x +x + suc y = (suc x) + y + +-- 10 + 20 +-- 30 diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/rbt_imple.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/rbt_imple.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,140 @@ +module rbt_imple where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Binary +open import Data.Nat hiding (_@$\leq$@_ ; _@$\leq$@?_) +open import Data.List hiding ([_]) +open import Data.Product +open import Data.Nat.Properties as NP + +open import rbt_t + +--このmutalの部分は別場所に書いてimportしたい。その方が綺麗に検証できそう +mutual + data right-List : Set where + [] : right-List + [_] : @$\mathbb{N}$@ @$\rightarrow$@ right-List + _@$\text{::}$@>_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : right-List ) @$\rightarrow$@ (p : x Data.Nat.> top-r xs) @$\rightarrow$@ right-List + + top-r : right-List @$\rightarrow$@ @$\mathbb{N}$@ + top-r [] = {!!} + top-r [ x ] = x + top-r (x @$\text{::}$@> l Cond x@$\_{1}$@) = x + + insert-r : @$\mathbb{N}$@ @$\rightarrow$@ right-List @$\rightarrow$@ right-List + insert-r x l with l + ... | [] = {!!} + ... | [ y ] = ? + ... | y @$\text{::}$@> ys Cond p with <-cmp x y + ... | tri< a @$\neg$@b @$\neg$@c = l + ... | tri≈ @$\neg$@a b @$\neg$@c = l + ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@> l Cond c + + data left-List : Set where + [] : left-List + [_] : @$\mathbb{N}$@ @$\rightarrow$@ left-List + _<@$\text{::}$@_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : left-List ) @$\rightarrow$@ (p : x Data.Nat.< top-l xs) @$\rightarrow$@ left-List + + top-l : left-List @$\rightarrow$@ @$\mathbb{N}$@ + top-l [] = {!!} + top-l [ x ] = x + top-l (x <@$\text{::}$@ l Cond x@$\_{1}$@) = x + + insert-l : @$\mathbb{N}$@ @$\rightarrow$@ left-List @$\rightarrow$@ left-List + insert-l x [] = [ x ] + insert-l x l@([ y ]) with <-cmp x y + ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a + ... | tri≈ @$\neg$@a b @$\neg$@c = l + ... | tri> @$\neg$@a @$\neg$@b c = l + insert-l x l@(y <@$\text{::}$@ ys Cond p) with <-cmp x y + ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a + ... | tri≈ @$\neg$@a b @$\neg$@c = l + ... | tri> @$\neg$@a @$\neg$@b c = l + + +record meta : Set where + field + deeps : @$\mathbb{N}$@ + black-nodes : @$\mathbb{N}$@ + l-list : left-List + r-list : right-List +open meta + +record tree-meta (A B C D : Set) : Set where + field + key : A + meta-data : B + ltree : C + rtree : D +open tree + +{- + +data rbt-meta : Set where + bt-empty : rbt-meta + bt-node : (node : tree-meta (node col @$\mathbb{N}$@ ) meta rbt-meta rbt-meta ) @$\rightarrow$@ rbt-meta + +test'1 = whileTestPCall' bt-empty 0 +test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1 +test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2 +test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3 +test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4 +test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5 +test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6 +test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7 +test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8 +test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9 +test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10 +test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11 +test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12 +test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13 +test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14 + +testdata = rbt_t.Env.vart test'7 + +-- ここからmetaの作成 + +makemeta-comm : rbt_t.rbt @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ meta @$\rightarrow$@ rbt-meta + +--make meta black nodes +makemeta-black-nodes : rbt_t.rbt @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ meta @$\rightarrow$@ rbt-meta +makemeta-black-nodes = {!!} + +-- make meta deeps +set-black-nodes : rbt_t.rbt @$\rightarrow$@ meta @$\rightarrow$@ @$\mathbb{N}$@ +set-black-nodes rbt fls with rbt +... | bt-empty = (suc (black-nodes fls) ) +... | bt-node node with (node.coler (key node)) +... | black = (suc (black-nodes fls) ) +... | red = (black-nodes fls) + +--make meta list +makemeta-comm rbt num fls with rbt +... | bt-empty = bt-empty +... | bt-node node = bt-node ( record { key = key node + ; meta-data = ( record {deeps = (deeps fls) + ; black-nodes = set-black-nodes rbt fls + ; l-list = insert-l (node.number (key node)) (l-list fls) + ; r-list = insert-r (node.number (key node)) (r-list fls) } ) + ; ltree = makemeta-comm (ltree node) (node.number (key node)) ( record { deeps = (suc (deeps fls)) + ; black-nodes = set-black-nodes rbt fls + ; l-list = insert-l (node.number (key node)) (l-list fls) + ; r-list = (r-list fls) } ) + ; rtree = makemeta-comm (rtree node) (node.number (key node)) ( record { deeps = (suc (deeps fls)) + ; black-nodes = set-black-nodes rbt fls + ; l-list = (l-list fls) + ; r-list = insert-r (node.number (key node)) (r-list fls) } ) }) + +-- init +makemeta : rbt @$\rightarrow$@ rbt-meta +makemeta rbt with rbt +... | bt-empty = bt-empty +... | bt-node node = bt-node ( record { key = key node + ; meta-data = ( record { deeps = 0 ; black-nodes = 1; l-list = [] ; r-list = [] } ) + ; ltree = makemeta-comm (ltree node) (node.number (key node)) + ( record { deeps = 1 ; black-nodes = 1 ; l-list = insert-l (node.number (key node)) [] ; r-list = [] } ) + ; rtree = makemeta-comm (rtree node) (node.number (key node)) + ( record { deeps = 1 ; black-nodes = 1 ; l-list = [] ; r-list = insert-r (node.number (key node)) [] } ) }) + +---test11 = makemeta (rbt_t.Env.vart test'11) +-} diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/rbt_t.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/rbt_t.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,283 @@ +module rbt_t where + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp -- <-cmp +open import Relation.Binary +open import Data.List + +-- @$\rightarrow$@ t を適用するために必要だった +open import Level renaming ( suc to succ ; zero to Zero ) +open import Level + + +data col : Set where + black : col + red : col + +record node (A B : Set) : Set where + field + coler : A + number : B +open node + +record tree (A B C : Set) : Set where + field + key : A + ltree : B + rtree : C +open tree + +data rbt : Set where + bt-empty : rbt + bt-node : (node : tree (node col @$\mathbb{N}$@) rbt rbt ) @$\rightarrow$@ rbt + +record Env : Set (succ Zero) where + field + vart : rbt + varn : @$\mathbb{N}$@ + varl : List rbt +open Env + + +whileTest-next : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (list : List rbt) @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} ) + +merge-tree : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t + +-- 全てmerge-treeへ +split : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node +split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node@$\_{1}$@) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node +split record { vart = (bt-node record { key = record { coler = coler@$\_{1}$@ ; number = number@$\_{1}$@ } + ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr }) + ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) }) + ; varn = varn ; varl = varl } next exit + = next record { vart = (bt-node record { key = record { coler = red ; number = number@$\_{1}$@ } + ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr }) + ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) }) + ; varn = varn ; varl = varl } + + +-- 右回転 +-- 実行時splitへ、それ以外はmerge-treeへ +merge-rotate-right : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-right record { vart = bt-node record { key = record { coler = y ; number = x } + ; ltree = (bt-node record { key = record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr }) + ; rtree = r } + ; varn = varn ; varl = varl } next exit + = next record { vart = bt-node record { key = record { coler = y ; number = lx } + ; ltree = ll + ; rtree = (bt-node record { key = record { coler = red ; number = x } ; ltree = lr; rtree = r }) } + ; varn = varn ; varl = varl } + + +-- split +split-branch : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +split-branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node@$\_{1}$@) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@ ; ltree = (bt-node record { key = record { coler = red ; number = number@$\_{1}$@ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree@$\_{1}$@ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node +split-branch node@record{ vart = bt-node record { key = key@$\_{1}$@ + ; ltree = (bt-node record { key = record { coler = red ; number = number@$\_{1}$@ } + ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree@$\_{1}$@ }) + ; rtree = lr }) + ; rtree = rtree } + ; varn = varn ; varl = varl } next exit + = next node + + +-- 左回転、exitはsplit_branchへ　nextもsplit_branchへ +merge-rotate-left : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node +merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit + = next record { vart = bt-node record { key = record { coler = y ; number = rx } + 　　; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl }) + 　　; rtree = rr} + 　　; varn = varn ; varl = varl } + + +-- skew exitがsplitへ　nextが左回転 +skew-bt : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node +skew-bt node@record { vart = (bt-node record { key = key@$\_{1}$@ + ; ltree = ltree@$\_{1}$@ + ; rtree = (bt-node record { key = record { coler = black ; number = number } + ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit + = exit node +skew-bt node@record { vart = (bt-node record { key = key@$\_{1}$@ + ; ltree = ltree@$\_{1}$@ + ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) }) + ; varn = varn ; varl = varl } next exit + = next node + + +set-node-coler : Env @$\rightarrow$@ Env +set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node +set-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } + = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } + +init-node-coler : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node +init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit + = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } + +--修正前 +merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node +merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty @$\text{::}$@ varl@$\_{1}$@) } next exit = exit node + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit with <-cmp varn number + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit | tri≈ @$\neg$@a b @$\neg$@c + = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl@$\_{1}$@ } + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit | tri> @$\neg$@a @$\neg$@b c + = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = vart }) ; varn = number ; varl = varl@$\_{1}$@ } + +merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } @$\text{::}$@ varl@$\_{1}$@) } next exit | tri< a @$\neg$@b @$\neg$@c + = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl@$\_{1}$@ } + +-- do marge-tree +-- next merge-tree-c +-- exit fin +merge-tree-c : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +merge-tree-c env next exit with varl env +... | [] = exit env +... | bt-empty @$\text{::}$@ nl = exit env +... | bt-node xtree @$\text{::}$@ varl with <-cmp (varn env) (number ( key xtree )) +... | tri≈ @$\neg$@a b @$\neg$@c = next (record env { vart = bt-node xtree ; varn = number (key xtree) ; varl = varl }) +... | tri> @$\neg$@a @$\neg$@b c = next (record env { vart = (bt-node record xtree{rtree = Env.vart env}) ; varn = number (key xtree) ; varl = varl }) +... | tri< a @$\neg$@b @$\neg$@c = next (record env { vart = (bt-node record xtree{ltree = Env.vart env}) ; varn = number (key xtree) ; varl = varl }) + +-- do brandh +-- next insert-c +-- exit merge-tree +insert-c : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +insert-c env next exit with Env.vart env +... | bt-empty = exit record env{vart = (bt-node (record { key = record { coler = red ; number = Env.varn env }; ltree = bt-empty; rtree = bt-empty }))} +... | bt-node node with <-cmp (Env.varn env) (node.number (tree.key node)) +... | tri≈ @$\neg$@a b @$\neg$@c = exit env +... | tri> @$\neg$@a @$\neg$@b c = next record env{vart = (tree.ltree node) ; varl = (bt-node record node{ltree = bt-empty}) @$\text{::}$@ (Env.varl env) } +... | tri< a @$\neg$@b @$\neg$@c = next record env{vart = (tree.rtree node) ; varl = (bt-node record node{rtree = bt-empty}) @$\text{::}$@ (Env.varl env) } + +-- insert +bt-insert : {le : Level} {t : Set le} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +-- mergeへ遷移する +bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit + = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl }) + +-- 場合分けを行う +bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n +bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ @$\neg$@a b @$\neg$@c + = exit node + +bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> @$\neg$@a @$\neg$@b c + = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) @$\text{::}$@ varl }) + +bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a @$\neg$@b @$\neg$@c + = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) @$\text{::}$@ varl }) + +-- normal loop without termination +{-@$\#$@ TERMINATING @$\#$@-} +insert : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +insert env exit = bt-insert env (@$\lambda$@ env @$\rightarrow$@ insert env exit ) exit + +init-col : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +init-col env exit = init-node-coler env exit exit + +{- +{-@$\#$@ TERMINATING @$\#$@-} +merge : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t + +{-@$\#$@ TERMINATING @$\#$@-} +split-p : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +split-p env exit = split env (@$\lambda$@ env @$\rightarrow$@ merge env (@$\lambda$@ env @$\rightarrow$@ merge env exit ) ) exit + +{-@$\#$@ TERMINATING @$\#$@-} +rotate_right : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +rotate_right env exit = merge-rotate-right env (@$\lambda$@ env @$\rightarrow$@ split-p env (@$\lambda$@ env @$\rightarrow$@ merge env exit ) ) exit + +{-@$\#$@ TERMINATING @$\#$@-} +split-b : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +split-b env exit = split-branch env (@$\lambda$@ env @$\rightarrow$@ rotate_right env exit ) @$\lambda$@ env @$\rightarrow$@ merge env exit + +{-@$\#$@ TERMINATING @$\#$@-} +rotate_left : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +rotate_left env exit = merge-rotate-left env (@$\lambda$@ env @$\rightarrow$@ split-b env exit ) exit + +{-@$\#$@ TERMINATING @$\#$@-} +skew : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +skew env exit = skew-bt env (@$\lambda$@ env @$\rightarrow$@ rotate_left env (@$\lambda$@ env @$\rightarrow$@ split-b env exit ) ) exit + +merge env exit = merge-tree env (@$\lambda$@ env @$\rightarrow$@ skew env exit ) exit +-} +-- skewはnextがrotate-right。exitはsplitとなる +-- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する +-- それはskewのexitと等しいので同時に記述してやる。 +skew' : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +skew' env exit = skew-bt env (@$\lambda$@ env @$\rightarrow$@ merge-rotate-left env exit exit ) exit + +split' : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +split' env exit = split-branch env (@$\lambda$@ env @$\rightarrow$@ merge-rotate-right env (@$\lambda$@ env @$\rightarrow$@ split env exit exit ) (@$\lambda$@ env @$\rightarrow$@ split env exit exit ) ) exit + + +{- +merge' : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node +merge' node@record { vart = vart ; varn = varn ; varl = (x @$\text{::}$@ varl@$\_{1}$@) } exit = merge' (merge-tree node (@$\lambda$@ env @$\rightarrow$@ skew' env (@$\lambda$@ env @$\rightarrow$@ split' env (@$\lambda$@ env @$\rightarrow$@ env) ) ) (@$\lambda$@ env @$\rightarrow$@ env) ) exit +-} + +whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (tree : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } ) + + + +{-@$\#$@ TERMINATING @$\#$@-} +mergeP : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +mergeP env exit = merge-tree env (@$\lambda$@ env @$\rightarrow$@ skew' env (@$\lambda$@ env @$\rightarrow$@ split' env (@$\lambda$@ env @$\rightarrow$@ mergeP env exit)) ) exit + +{- +mergeP1 : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +mergeP1 record { vart = vart ; varn = varn ; varl = [] } exit = {!!} +mergeP1 record { vart = vart ; varn = varn ; varl = (x @$\text{::}$@ varl@$\_{1}$@) } exit = {!!} +-} + +{- +merge-tree env + (@$\lambda$@ env @$\rightarrow$@ skew-bt env + (@$\lambda$@ env @$\rightarrow$@ merge-rotate-left env + (@$\lambda$@ env @$\rightarrow$@ split-branch env + (@$\lambda$@ env @$\rightarrow$@ merge-rotate-right env + (@$\lambda$@ env @$\rightarrow$@ split env (@$\lambda$@ env @$\rightarrow$@ mergeP env exit ) (@$\lambda$@ env @$\rightarrow$@ mergeP env exit ) ) exit) + (@$\lambda$@ env @$\rightarrow$@ mergeP env exit ) ) + exit ) + exit ) exit +-} + +--whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (c11 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +--whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } ) + +--whileTestPCall : (tree : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ Env +--whileTestPCall tree n = whileTestP {_} {_} tree n (@$\lambda$@ env @$\rightarrow$@ insert env (@$\lambda$@ env @$\rightarrow$@ merge env (@$\lambda$@ env @$\rightarrow$@ init-col env (@$\lambda$@ env @$\rightarrow$@ env ) ) ) ) + +whileTestPCall' : (tree : rbt) @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ Env +whileTestPCall' tree n = whileTestP {_} {_} tree n (@$\lambda$@ env @$\rightarrow$@ insert env (@$\lambda$@ env @$\rightarrow$@ mergeP env (@$\lambda$@ env @$\rightarrow$@ init-col env (@$\lambda$@ env @$\rightarrow$@ env ) ) ) ) + +-- 以下test部分 +test1 = whileTestPCall' bt-empty 8 +test2 = whileTestPCall' (vart test1) 10 +test3 = whileTestPCall' (vart test2) 24 +test4 = whileTestPCall' (vart test3) 31 +test5 = whileTestPCall' (vart test4) 41 +test6 = whileTestPCall' (vart test5) 45 +test7 = whileTestPCall' (vart test6) 50 +test8 = whileTestPCall' (vart test7) 59 +test9 = whileTestPCall' (vart test8) 73 +test10 = whileTestPCall' (vart test9) 74 +test11 = whileTestPCall' (vart test10) 79 + diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/rbt_varif.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/rbt_varif.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,54 @@ +module rbt_varif where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Binary +open import Data.Nat hiding (_@$\leq$@_ ; _@$\leq$@?_) +open import Data.List hiding ([_]) +open import Data.Product +open import Data.Nat.Properties as NP + + + +mutual + data right-List : Set where + [] : right-List + [_] : @$\mathbb{N}$@ @$\rightarrow$@ right-List + _@$\text{::}$@>_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : right-List ) @$\rightarrow$@ (p : x Data.Nat.> top-r xs) @$\rightarrow$@ right-List + + top-r : right-List @$\rightarrow$@ @$\mathbb{N}$@ + top-r [] = {!!} + top-r [ x ] = x + top-r (x @$\text{::}$@> l Cond x@$\_{1}$@) = x + + insert-r : @$\mathbb{N}$@ @$\rightarrow$@ right-List @$\rightarrow$@ right-List + insert-r x [] = {!!} + insert-r x [ y ] with <-cmp x y + ... | tri< a @$\neg$@b @$\neg$@c = [ y ] + ... | tri≈ @$\neg$@a b @$\neg$@c = [ y ] + ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@> [ y ] Cond c + insert-r x (y @$\text{::}$@> ys Cond p) with <-cmp x y + ... | tri< a @$\neg$@b @$\neg$@c = (y @$\text{::}$@> ys Cond p) + ... | tri≈ @$\neg$@a b @$\neg$@c = (y @$\text{::}$@> ys Cond p) + ... | tri> @$\neg$@a @$\neg$@b c = x @$\text{::}$@> (y @$\text{::}$@> ys Cond p) Cond c + + data left-List : Set where + [] : left-List + [_] : @$\mathbb{N}$@ @$\rightarrow$@ left-List + _<@$\text{::}$@_Cond_ : (x : @$\mathbb{N}$@) @$\rightarrow$@ (xs : left-List ) @$\rightarrow$@ (p : x Data.Nat.< top-l xs) @$\rightarrow$@ left-List + + top-l : left-List @$\rightarrow$@ @$\mathbb{N}$@ + top-l [] = {!!} + top-l [ x ] = x + top-l (x <@$\text{::}$@ l Cond x@$\_{1}$@) = x + + insert-l : @$\mathbb{N}$@ @$\rightarrow$@ left-List @$\rightarrow$@ left-List + insert-l x [] = [ x ] + insert-l x l@([ y ]) with <-cmp x y + ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a + ... | tri≈ @$\neg$@a b @$\neg$@c = l + ... | tri> @$\neg$@a @$\neg$@b c = l + insert-l x l@(y <@$\text{::}$@ ys Cond p) with <-cmp x y + ... | tri< a @$\neg$@b @$\neg$@c = x <@$\text{::}$@ l Cond a + ... | tri≈ @$\neg$@a b @$\neg$@c = l + + ... | tri> @$\neg$@a @$\neg$@b c = l diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/syllogism.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/syllogism.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,2 @@ +syllogism : {A B C : Set} @$\rightarrow$@ ((A @$\rightarrow$@ B) @$\wedge$@ (B @$\rightarrow$@ C)) @$\rightarrow$@ (A @$\rightarrow$@ C) +syllogism x a = _@$\wedge$@_.p2 x (_@$\wedge$@_.p1 x a) diff -r 3910f4639344 -r 9176dff8f38a Paper/src/agda/utilities.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/agda/utilities.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,171 @@ +{-@$\#$@ OPTIONS --allow-unsolved-metas @$\#$@-} +module utilities where + +open import Function +open import Data.Nat +open import Data.Product +open import Data.Bool hiding ( _≟_ ; _@$\leq$@?_) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +Pred : Set @$\rightarrow$@ Set@$\_{1}$@ +Pred X = X @$\rightarrow$@ Set + +Imply : Set @$\rightarrow$@ Set @$\rightarrow$@ Set +Imply X Y = X @$\rightarrow$@ Y + +Iff : Set @$\rightarrow$@ Set @$\rightarrow$@ Set +Iff X Y = Imply X Y @$\times$@ Imply Y X + +record _@$\wedge$@_ {n : Level } (a : Set n) (b : Set n): Set n where + field + pi1 : a + pi2 : b + +open _@$\wedge$@_ + +_-_ : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ +x - zero = x +zero - _ = zero +(suc x) - (suc y) = x - y + ++zero : { y : @$\mathbb{N}$@ } @$\rightarrow$@ y + zero @$\equiv$@ y ++zero {zero} = refl ++zero {suc y} = cong ( @$\lambda$@ x @$\rightarrow$@ suc x ) ( +zero {y} ) + + ++-sym : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ x + y @$\equiv$@ y + x ++-sym {zero} {zero} = refl ++-sym {zero} {suc y} = let open @$\equiv$@-Reasoning in + begin + zero + suc y + @$\equiv$@@$\langle$@@$\rangle$@ + suc y + @$\equiv$@@$\langle$@ sym +zero @$\rangle$@ + suc y + zero + @$\blacksquare$@ ++-sym {suc x} {zero} = let open @$\equiv$@-Reasoning in + begin + suc x + zero + @$\equiv$@@$\langle$@ +zero @$\rangle$@ + suc x + @$\equiv$@@$\langle$@@$\rangle$@ + zero + suc x + @$\blacksquare$@ ++-sym {suc x} {suc y} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) ( let open @$\equiv$@-Reasoning in + begin + x + suc y + @$\equiv$@@$\langle$@ +-sym {x} {suc y} @$\rangle$@ + suc (y + x) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) (+-sym {y} {x}) @$\rangle$@ + suc (x + y) + @$\equiv$@@$\langle$@ sym ( +-sym {y} {suc x}) @$\rangle$@ + y + suc x + @$\blacksquare$@ ) + + +minus-plus : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ (suc x - 1) + (y + 1) @$\equiv$@ suc x + y +minus-plus {zero} {y} = +-sym {y} {1} +minus-plus {suc x} {y} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) (minus-plus {x} {y}) + ++1@$\equiv$@suc : { x : @$\mathbb{N}$@ } @$\rightarrow$@ x + 1 @$\equiv$@ suc x ++1@$\equiv$@suc {zero} = refl ++1@$\equiv$@suc {suc x} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) ( +1@$\equiv$@suc {x} ) + +lt : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool +lt x y with (suc x ) @$\leq$@? y +lt x y | yes p = true +lt x y | no @$\neg$@p = false + +pred@$\mathbb{N}$@ : {n : @$\mathbb{N}$@ } @$\rightarrow$@ lt 0 n @$\equiv$@ true @$\rightarrow$@ @$\mathbb{N}$@ +pred@$\mathbb{N}$@ {zero} () +pred@$\mathbb{N}$@ {suc n} refl = n + +pred@$\mathbb{N}$@+1=n : {n : @$\mathbb{N}$@ } @$\rightarrow$@ (less : lt 0 n @$\equiv$@ true ) @$\rightarrow$@ (pred@$\mathbb{N}$@ less) + 1 @$\equiv$@ n +pred@$\mathbb{N}$@+1=n {zero} () +pred@$\mathbb{N}$@+1=n {suc n} refl = +1@$\equiv$@suc + +suc-pred@$\mathbb{N}$@=n : {n : @$\mathbb{N}$@ } @$\rightarrow$@ (less : lt 0 n @$\equiv$@ true ) @$\rightarrow$@ suc (pred@$\mathbb{N}$@ less) @$\equiv$@ n +suc-pred@$\mathbb{N}$@=n {zero} () +suc-pred@$\mathbb{N}$@=n {suc n} refl = refl + +Equal : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool +Equal x y with x ≟ y +Equal x y | yes p = true +Equal x y | no @$\neg$@p = false + +_@$\Rightarrow$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool +false @$\Rightarrow$@ _ = true +true @$\Rightarrow$@ true = true +true @$\Rightarrow$@ false = false + +@$\Rightarrow$@t : {x : Bool} @$\rightarrow$@ x @$\Rightarrow$@ true @$\equiv$@ true +@$\Rightarrow$@t {x} with x +@$\Rightarrow$@t {x} | false = refl +@$\Rightarrow$@t {x} | true = refl + +f@$\Rightarrow$@ : {x : Bool} @$\rightarrow$@ false @$\Rightarrow$@ x @$\equiv$@ true +f@$\Rightarrow$@ {x} with x +f@$\Rightarrow$@ {x} | false = refl +f@$\Rightarrow$@ {x} | true = refl + +@$\wedge$@-pi1 : { x y : Bool } @$\rightarrow$@ x @$\wedge$@ y @$\equiv$@ true @$\rightarrow$@ x @$\equiv$@ true +@$\wedge$@-pi1 {x} {y} eq with x | y | eq +@$\wedge$@-pi1 {x} {y} eq | false | b | () +@$\wedge$@-pi1 {x} {y} eq | true | false | () +@$\wedge$@-pi1 {x} {y} eq | true | true | refl = refl + +@$\wedge$@-pi2 : { x y : Bool } @$\rightarrow$@ x @$\wedge$@ y @$\equiv$@ true @$\rightarrow$@ y @$\equiv$@ true +@$\wedge$@-pi2 {x} {y} eq with x | y | eq +@$\wedge$@-pi2 {x} {y} eq | false | b | () +@$\wedge$@-pi2 {x} {y} eq | true | false | () +@$\wedge$@-pi2 {x} {y} eq | true | true | refl = refl + +@$\wedge$@true : { x : Bool } @$\rightarrow$@ x @$\wedge$@ true @$\equiv$@ x +@$\wedge$@true {x} with x +@$\wedge$@true {x} | false = refl +@$\wedge$@true {x} | true = refl + +true@$\wedge$@ : { x : Bool } @$\rightarrow$@ true @$\wedge$@ x @$\equiv$@ x +true@$\wedge$@ {x} with x +true@$\wedge$@ {x} | false = refl +true@$\wedge$@ {x} | true = refl +bool-case : ( x : Bool ) { p : Set } @$\rightarrow$@ ( x @$\equiv$@ true @$\rightarrow$@ p ) @$\rightarrow$@ ( x @$\equiv$@ false @$\rightarrow$@ p ) @$\rightarrow$@ p +bool-case x T F with x +bool-case x T F | false = F refl +bool-case x T F | true = T refl + +impl@$\Rightarrow$@ : {x y : Bool} @$\rightarrow$@ (x @$\equiv$@ true @$\rightarrow$@ y @$\equiv$@ true ) @$\rightarrow$@ x @$\Rightarrow$@ y @$\equiv$@ true +impl@$\Rightarrow$@ {x} {y} p = bool-case x (@$\lambda$@ x=t @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + x @$\Rightarrow$@ y + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ x @$\Rightarrow$@ z ) (p x=t ) @$\rangle$@ + x @$\Rightarrow$@ true + @$\equiv$@@$\langle$@ @$\Rightarrow$@t @$\rangle$@ + true + @$\blacksquare$@ + ) ( @$\lambda$@ x=f @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + x @$\Rightarrow$@ y + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z @$\Rightarrow$@ y ) x=f @$\rangle$@ + true + @$\blacksquare$@ + ) + +Equal@$\rightarrow$@@$\equiv$@ : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ Equal x y @$\equiv$@ true @$\rightarrow$@ x @$\equiv$@ y +Equal@$\rightarrow$@@$\equiv$@ {x} {y} eq with x ≟ y +Equal@$\rightarrow$@@$\equiv$@ {x} {y} refl | yes refl = refl +Equal@$\rightarrow$@@$\equiv$@ {x} {y} () | no @$\neg$@p + +Equal+1 : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ Equal x y @$\equiv$@ Equal (suc x) (suc y) +Equal+1 {x} {y} with x ≟ y +Equal+1 {x} {.x} | yes refl = {!!} +Equal+1 {x} {y} | no @$\neg$@p = {!!} + +open import Data.Empty + +@$\equiv$@@$\rightarrow$@Equal : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ x @$\equiv$@ y @$\rightarrow$@ Equal x y @$\equiv$@ true +@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl with x ≟ x +@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl | yes refl = refl +@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl | no @$\neg$@p = @$\bot$@-elim ( @$\neg$@p refl ) diff -r 3910f4639344 -r 9176dff8f38a Paper/src/cbc-agda.agda.replaced --- a/Paper/src/cbc-agda.agda.replaced Tue Nov 02 06:58:39 2021 +0900 +++ b/Paper/src/cbc-agda.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -1,3 +1,22 @@ -plus : {l : Level} {t : Set l} @$\rightarrow$@ (x y : @$\mathbb{N}$@) @$\rightarrow$@ (next : @$\mathbb{N}$@ @$\rightarrow$@ t) @$\rightarrow$@ t -plus x zero next = next x -plus x (suc y) next = plus (suc x) y next +module cbc-agda where + +open import Data.Nat +open import Level renaming ( suc to succ ; zero to Zero ) + +record Env : Set where + field + varx : @$\mathbb{N}$@ + vary : @$\mathbb{N}$@ +open Env + +plus-com : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-com env next exit with vary env +... | zero = exit (record { varx = varx env ; vary = vary env }) +... | suc y = next (record { varx = suc (varx env) ; vary = y }) + +{-@$\#$@ TERMINATING @$\#$@-} +plus-p : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t +plus-p env exit = plus-com env ( @$\lambda$@ env @$\rightarrow$@ plus-p env exit ) exit + +plus : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Env +plus x y = plus-p (record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env) diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/init_cg.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/init_cg.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,2 @@ +whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/init_cg.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/init_cg.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,2 @@ +whileTest : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/while_loop.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/while_loop.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,5 @@ +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/while_loop.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/while_loop.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,5 @@ +{-@$\#$@ TERMINATING @$\#$@-} +whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/while_loop_c.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/while_loop_c.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,2 @@ +whileLoopC : ℕ → Env +whileLoopC n = whileTest n (λ env → whileLoop env (λ env1 → env1 )) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/while_loop_c.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/while_loop_c.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,2 @@ +whileLoopC : @$\mathbb{N}$@ @$\rightarrow$@ Env +whileLoopC n = whileTest n (@$\lambda$@ env @$\rightarrow$@ whileLoop env (@$\lambda$@ env1 @$\rightarrow$@ env1 )) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/while_loop_dg.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/while_loop_dg.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,5 @@ +record Env : Set where + field + varn : ℕ + vari : ℕ +open Env \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_impl/while_loop_dg.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_impl/while_loop_dg.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,5 @@ +record Env : Set where + field + varn : @$\mathbb{N}$@ + vari : @$\mathbb{N}$@ +open Env \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/conversion.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/conversion.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,10 @@ +conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (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 + ∎ \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/conversion.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/conversion.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,10 @@ +conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((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 @$\rightarrow$@ n + vari env ) (pi2 p1 ) @$\rangle$@ + c10 + vari env @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ c10 + n ) (pi1 p1 ) @$\rangle$@ + c10 + 0 @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ + c10 + @$\blacksquare$@ \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/init_cg.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/init_cg.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,7 @@ +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) -- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl} diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/init_cg.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/init_cg.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,7 @@ +whileTest@$\prime$@ : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env) @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t +whileTest@$\prime$@ {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) -- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl} diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/verif.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/verif.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,4 @@ +proofGearsTermS : {c10 : ℕ } → ⊤ +proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 → + TerminatingLoopS Env (λ env → varn env) + (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/verif.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/verif.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,4 @@ +proofGearsTermS : {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ @$\top$@ +proofGearsTermS {c10} = whileTest@$\prime$@ {_} {_} {c10} (@$\lambda$@ n p @$\rightarrow$@ conversion1 n p (@$\lambda$@ n1 p1 @$\rightarrow$@ + TerminatingLoopS Env (@$\lambda$@ env @$\rightarrow$@ varn env) + (@$\lambda$@ n2 p2 loop @$\rightarrow$@ whileLoopSeg {_} {_} {c10} n2 p2 loop (@$\lambda$@ ne pe @$\rightarrow$@ whileTestSpec1 c10 ne pe)) n1 p1 )) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/verif_loop.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/verif_loop.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,12 @@ +TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) + → (r : Index) → (p : Invraiant r) → t +TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/verif_loop.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/verif_loop.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,12 @@ +TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) @$\rightarrow$@ {Invraiant : Index @$\rightarrow$@ Set } @$\rightarrow$@ ( reduce : Index @$\rightarrow$@ @$\mathbb{N}$@) + @$\rightarrow$@ (loop : (r : Index) @$\rightarrow$@ Invraiant r @$\rightarrow$@ (next : (r1 : Index) @$\rightarrow$@ Invraiant r1 @$\rightarrow$@ reduce r1 < reduce r @$\rightarrow$@ t ) @$\rightarrow$@ t) + @$\rightarrow$@ (r : Index) @$\rightarrow$@ (p : Invraiant r) @$\rightarrow$@ t +TerminatingLoopS {_} {t} Index {Invraiant} reduce loop r p with <-cmp 0 (reduce r) +... | tri≈ @$\neg$@a b @$\neg$@c = loop r p (@$\lambda$@ r1 p1 lt @$\rightarrow$@ @$\bot$@-elim (lemma3 b lt) ) +... | tri< a @$\neg$@b @$\neg$@c = loop r p (@$\lambda$@ r1 p1 lt1 @$\rightarrow$@ TerminatingLoop1 (reduce r) r r1 (@$\leq$@-step lt1) p1 lt1 ) where + TerminatingLoop1 : (j : @$\mathbb{N}$@) @$\rightarrow$@ (r r1 : Index) @$\rightarrow$@ reduce r1 < suc j @$\rightarrow$@ Invraiant r1 @$\rightarrow$@ reduce r1 < reduce r @$\rightarrow$@ t + TerminatingLoop1 zero r r1 n@$\leq$@j p1 lt = loop r1 p1 (@$\lambda$@ r2 p1 lt1 @$\rightarrow$@ @$\bot$@-elim (lemma5 n@$\leq$@j lt1)) + TerminatingLoop1 (suc j) r r1 n@$\leq$@j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a @$\neg$@b @$\neg$@c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ @$\neg$@a b @$\neg$@c = loop r1 p1 (@$\lambda$@ r2 p2 lt1 @$\rightarrow$@ TerminatingLoop1 j r1 r2 (subst (@$\lambda$@ k @$\rightarrow$@ reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> @$\neg$@a @$\neg$@b c = @$\bot$@-elim ( nat-@$\leq$@> c n@$\leq$@j ) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/verif_term.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/verif_term.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,5 @@ +whileTestSpec1 : (c10 : ℕ) → (e1 : Env ) → vari e1 ≡ c10 → ⊤ +whileTestSpec1 _ _ x = tt + +proofGears : {c10 : ℕ } → ⊤ +proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/verif_term.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/verif_term.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,5 @@ +whileTestSpec1 : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (e1 : Env ) @$\rightarrow$@ vari e1 @$\equiv$@ c10 @$\rightarrow$@ @$\top$@ +whileTestSpec1 _ _ x = tt + +proofGears : {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ @$\top$@ +proofGears {c10} = whileTest@$\prime$@ {_} {_} {c10} (@$\lambda$@ n p1 @$\rightarrow$@ conversion1 n p1 (@$\lambda$@ n1 p2 @$\rightarrow$@ whileLoop@$\prime$@ n1 p2 (@$\lambda$@ n2 p3 @$\rightarrow$@ whileTestSpec1 c10 n2 p3 ))) \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/while_loop.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/while_loop.agda Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,24 @@ +{-# TERMINATING #-} +whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) + → (Code : (e1 : Env )→ vari e1 ≡ c10 → t) → t +whileLoop' env proof next with ( suc zero ≤? (varn env) ) +whileLoop' env {c10} proof next | no p = next env ( begin + vari env ≡⟨ refl ⟩ + 0 + vari env ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩ + varn env + vari env ≡⟨ proof ⟩ + c10 ∎ ) where open ≡-Reasoning +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 + ∎ \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/src/while_loop_verif/while_loop.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/while_loop_verif/while_loop.agda.replaced Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,24 @@ +{-@$\#$@ TERMINATING @$\#$@-} +whileLoop@$\prime$@ : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((varn env) + (vari env) @$\equiv$@ c10) + @$\rightarrow$@ (Code : (e1 : Env )@$\rightarrow$@ vari e1 @$\equiv$@ c10 @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoop@$\prime$@ env proof next with ( suc zero @$\leq$@? (varn env) ) +whileLoop@$\prime$@ env {c10} proof next | no p = next env ( begin + vari env @$\equiv$@@$\langle$@ refl @$\rangle$@ + 0 + vari env @$\equiv$@@$\langle$@ cong (@$\lambda$@ k @$\rightarrow$@ k + vari env) (sym (lemma1 p )) @$\rangle$@ + varn env + vari env @$\equiv$@@$\langle$@ proof @$\rangle$@ + c10 @$\blacksquare$@ ) where open @$\equiv$@-Reasoning +whileLoop@$\prime$@ env {c10} proof next | yes p = whileLoop@$\prime$@ env1 (proof3 p ) next where + env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} + 1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@ + 1<0 () + proof3 : (suc zero @$\leq$@ (varn env)) @$\rightarrow$@ 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@$\prime$@}) ) | suc n = let open @$\equiv$@-Reasoning in begin + n@$\prime$@ + (vari env + 1) @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n@$\prime$@ + z ) ( +-sym {vari env} {1} ) @$\rangle$@ + n@$\prime$@ + (1 + vari env ) @$\equiv$@@$\langle$@ sym ( +-assoc (n@$\prime$@) 1 (vari env) ) @$\rangle$@ + (n@$\prime$@ + 1) + vari env @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env ) +1@$\equiv$@suc @$\rangle$@ + (suc n@$\prime$@ ) + vari env @$\equiv$@@$\langle$@@$\rangle$@ + varn env + vari env @$\equiv$@@$\langle$@ proof @$\rangle$@ + c10 + @$\blacksquare$@ \ No newline at end of file diff -r 3910f4639344 -r 9176dff8f38a Paper/tex/hoare.tex --- a/Paper/tex/hoare.tex Tue Nov 02 06:58:39 2021 +0900 +++ b/Paper/tex/hoare.tex Fri Nov 05 15:19:08 2021 +0900 @@ -16,7 +16,7 @@ これらを満たし、 事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。 -\section{Hoare Logic による Code Gear の検証手法 } +\subsection{Hoare Logic による Code Gear の検証手法 } \figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。 input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、 diff -r 3910f4639344 -r 9176dff8f38a Paper/tex/while_loop.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/tex/while_loop.tex Fri Nov 05 15:19:08 2021 +0900 @@ -0,0 +1,86 @@ +\section{Gears Agda にて Hoare Logic を用いた検証の例} +ここでは Gears Agda にて Hoare Logic を用いた検証の例として、 + While Loop プログラムを実装・検証する。 + +\subsection{While Loop の実装} +まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する。 +実装はまず、 Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う。 +\lstinputlisting[label=while-loop-dg, caption=Data Gearの定義] {src/while_loop_impl/while_loop_dg.agda.replaced} + +そのため最初の Code Gear は引数を受け取り、Envを作成する Code Gear となる Code \ref{while_init_cg}。 + +\lstinputlisting[label=while_init_cg, caption=Data Gear の定義を行う Code Gear] {src/while_loop_impl/init_cg.agda.replaced} + +次に、目的である While Loop の実装を行う。ソースコードは Code \ref{while-loop} のようになる。 + +\lstinputlisting[label=while-loop, caption=Loop の部分を担う Code Gears] {src/while_loop_impl/while_loop.agda.replaced} + +また Agda では停止性の検出機能が存在し、 +プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る。 +その場合は関数定義の直前に +\{-$\#$ TERMINATING $\#$-\} のタグを付けると +停止しないプログラムをコンパイルすることができる + +これまでの Code Gear を繋げることで、 While Loop　を行う Code を実装することができる。 + +\lstinputlisting[label=while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced} + +\subsection{While Loop の検証} + +Gears Agda にて行なった While Loop の実装コードを元に、 +5章にて述べた Pre / Post Condition を記述していくことで +Hoare Logic を用いた検証を行う。 + +検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear の定義から行う。Code \ref{while_verif_init_cg} がそれに当たる。 + +\lstinputlisting[label=while_verif_init_cg, caption=While Loop を行う Code Gear] {src/while_loop_verif/init_cg.agda.replaced} + +今回は検証を行いたいため 5.1 で述べたように、実装に加えて Pre / Post Condition を持つ必要がある。 +init時の Pre Condition のみ特殊で　Agda での関数定義の際に記述し、 +「Data Gear に正しく初期値が設定される」という条件を使用する。これが +((vari env) $\equiv$ 0) $\wedge$ ((varn env) $\equiv$ c10) +に当たる。 +そしてinit時以外の、Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する。 +今回は While Loop の不変条件として、 +$今回loopさせたい回数(c10) = 残りのloopする回数(vern) + 今回loopした回数(vari)$ +を設定した。これがinit時の Post Condition となる。 + +また、init時の Pre Condition と同じ値で +Post Condition を設定しなければならない。 +init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する。 + +\lstinputlisting[label=conversion, caption=init時の Pre Condition を Post Condition に変換する Code Gear] {src/while_loop_verif/conversion.agda.replaced} + +ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため、 +この後の Pre / Post Condition は停止するまでこれを用いる。 + +以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが、 Wile Loop の Loop 部分の検証を行う Code Gear となる。 + +\lstinputlisting[label=loop_verif_cg, caption=停止性以外の Loop の検証も行う Code Gear] {src/while_loop_verif/while_loop.agda.replaced} + +Loop が停止することを示していないため、関数定義の直前に \{-\# TERMINATING \#-\} が記述されている。 +こちらも Loop の実装以外に、Pre / Post Condition を満たしているか検証を行い、次の Code Gear に渡している。 + +ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで、 +停止性以外の While Loop の検証を行う Code Gear を実装できる。 + +\lstinputlisting[label=loop_verif_cg, caption=停止性以外の While Loop の検証を行う Code Gear] {src/while_loop_verif/verif_term.agda.replaced} + +停止性の検証も行う While Loop の検証を行う Code Gear を実装する + +\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の Code Gear] {src/while_loop_verif/verif_loop.agda.replaced} + +停止することを Agda が理解できるように記述すると良い。 +そのため引数に減少していく変数 reduce を追加し、 +loop するとデクリメントするように実装する。 + +loop には先ほど実装した loop の部分を担う Code Gear が次の関数遷移先を引数に受け取れるようにした +whileLoopSeg を使用する。 + +そしてこれらを繋げて While Loop の検証を行うことができる Code ref を実装できた。 + +\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced} + + + +