From f8d88d4cf2439f4920fa948b054c4f0b2899e368 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 12 Dec 2018 18:23:00 +0000
Subject: Move much of recursive function termination to a rewrite It now
 includes updating the effects so that morally pure recursive functions can be
 turned into this impure termination-by-assertion form.

---
 lib/coq/Sail2_prompt.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 8c0ca33c..85ca95f6 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -77,13 +77,14 @@ match b with
   | BU => undefined_bool tt
 end.
 
-(* For termination of recursive functions. *)
-Lemma _limit_is_limit {_limit : Z} : _limit >? 0 = true -> Zwf 0 (_limit - 1) _limit.
-intros.
-prepare_for_solver.
+(* For termination of recursive functions.  We don't name assertions, so use
+   the type class mechanism to find it. *)
+Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >= 0)} : Acc (Zwf 0) (_limit - 1).
+refine (Acc_inv _acc _).
+destruct H.
 red.
 omega.
-Qed.
+Defined.
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-- 
cgit v1.2.3