From 4f20163965e7c336f28740628fa9d64528006861 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 11 Dec 2018 11:54:36 +0000
Subject: Initial attempt at using termination measures in Coq This only
 applies to recursive functions and uses the termination measure merely as a
 limit to the recursive call depth, rather than proving the measure correct.

---
 lib/coq/Sail2_prompt.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 1b12f360..8c0ca33c 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -1,7 +1,7 @@
 (*Require Import Sail_impl_base*)
 Require Import Sail2_values.
 Require Import Sail2_prompt_monad.
-
+Require Export ZArith.Zwf.
 Require Import List.
 Import ListNotations.
 (*
@@ -77,6 +77,13 @@ 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.
+red.
+omega.
+Qed.
 
 (*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