Mercurial > hg > Members > ryokka > HoareLogic

changeset 91:bbbdc8ce8d04

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 31 Oct 2021 23:43:06 +0900
parents fb2e12dca19a
children 9c91d23c2836
files whileTestGears1.agda
diffstat 1 files changed, 23 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears1.agda	Sun Oct 31 22:31:19 2021 +0900
+++ b/whileTestGears1.agda	Sun Oct 31 23:43:06 2021 +0900
@@ -156,4 +156,27 @@
        lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 lt1 eq lt1 
     ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
+TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set ) → (ExitCond : Set) → ( reduce : Index → ℕ)
+   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → (exit : ExitCond → t) → t)
+   → (i : ℕ) → (r : Index) → reduce r ≡ i  → (p : Invraiant r)  → (exit : ExitCond → t)  → t 
+TerminatingLoopS {_} {t} Index Invraiant ExitCond reduce loop  i r refl p exit with <-cmp 0 i
+... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) exit 
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r1) r1  {!!} {!!} {!!} {!!} ) exit where 
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j {!!})) exit  
+    TerminatingLoop1 (suc j) r r1  n≤j p lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p lt 
+    ... | tri≈ ¬a b ¬c = loop {!!} {!!} {!!} {!!} where
+       lemma4 : (r1 : Index) → Invraiant r → reduce r1 < reduce r  → t
+       lemma4 r1 p1 lt1 = TerminatingLoop1 (reduce r1) r r1 {!!} p1 lt1 
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
+
+proofGearsTerm : {c10 :  ℕ } → ⊤
+proofGearsTerm {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → TerminatingLoop (varn n1) n1 refl p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
+
+
+
+
+
+