From 085e4f45ebf81b7734efa70f018928ac49703f47 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 13 Mar 2020 11:12:00 +0100
Subject: inductive

---
 backend/CSE3proof.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index bdf5ecd7..f63636ce 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -142,6 +142,19 @@ Proof.
   exists x.
   assumption.
 Qed.
+Lemma transf_function_invariants_inductive:
+  forall f tf tenv, transf_function f = OK tf ->
+    type_function f = OK tenv ->
+    check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f))))
+                        f tenv (fst (preanalysis tenv f)) = true.
+Proof.
+  unfold transf_function; destruct f; simpl; intros.
+  monadInv H.
+  replace x with tenv in * by congruence.
+  clear x.
+  destruct preanalysis as [invariants hints].
+  destruct check_inductiveness; trivial; discriminate.
+Qed.
 
 Lemma find_function_translated:
   forall ros rs fd,
-- 
cgit