From e9de87c29c446a4e0169f55131a678535630ff18 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 11 Jan 2021 19:11:52 +0000
Subject: Add proof of empty items

Proof that correct items are returned from an empty forest.
---
 src/hls/Scheduleoracle.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src')

diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v
index 2c60e96..1625238 100644
--- a/src/hls/Scheduleoracle.v
+++ b/src/hls/Scheduleoracle.v
@@ -362,6 +362,16 @@ Proof.
    congruence.
 Qed.
 
+Definition empty : forest := Rtree.empty _.
+
+Lemma get_empty:
+  forall r, empty#r = Ebase r.
+Proof.
+  intros r. unfold get_forest.
+  destruct (Rtree.get r empty) eqn:Heq; auto.
+  rewrite Rtree.gempty in Heq. discriminate.
+Qed.
+
 (*|
 We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling
 transformation.
-- 
cgit