From c5afefdfb2c847288463ab85d8348a65aa747637 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 13 Oct 2021 08:58:22 +0100
Subject: [sched] Add more proof to sem_pred_det

---
 src/hls/Abstr.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/hls')

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 512235e..c7deab3 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -794,7 +794,12 @@ Section CORRECT.
                     sem_val_list ictx p v -> sem_val_list octx p v' -> v = v');
     try solve [inversion 1]; inv HSIM; simplify.
     - inv H0. inv H1. auto.
-    - inv H0. inv H1.
+    - inv H0. inv H1. simplify.
+      assert (lv = lv0). { apply IHe; auto. } subst.
+      crush.
+    - inv H0; inv H1; auto.
+    - inv H0; inv H1; f_equal.
+      eapply sem_value_det.
 
   Lemma check_correct_sem_value:
     forall x x' v v' n,
-- 
cgit