From dcd2863252751b95b3859fd46cc81d4b29089cab Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 9 Jan 2016 12:52:28 +0100
Subject: [PATCH] optimize the step_by_value proof: Determine which case we are
in, and call the appropriate tactic
---
channel/heap_lang.v | 23 +++++++++++++++++------
1 file changed, 17 insertions(+), 6 deletions(-)
diff --git a/channel/heap_lang.v b/channel/heap_lang.v
index 0cb39a93f..4c02bbfb2 100644
--- a/channel/heap_lang.v
+++ b/channel/heap_lang.v
@@ -320,13 +320,24 @@ Proof.
exists K''; by eauto using f_equal, f_equal2, f_equal3, v2e_inj.
intros Hfill Hred Hnval.
- revert K' Hfill; induction K=>K' /= Hfill;
+ Time revert K' Hfill; induction K=>K' /= Hfill;
first (now eexists; reflexivity);
- destruct K'; simpl; try discriminate Hfill; try first [
- bad_red Hfill e' Hred
- | bad_fill Hfill
- | good Hfill IHK
- ].
+ (destruct K'; simpl;
+ (* The first case is: K' is EmpyCtx. *)
+ first (by bad_red Hfill e' Hred);
+ (* Many of the other cases result in contradicting equalities. *)
+ try discriminate Hfill;
+ (* The remaining cases are "compatible" contexts - that result in the same head symbol of the expression.
+ Test whether the context als has the same head, and use the appropriate tactic. *)
+ match goal with
+ | [ |- exists x, ?C _ = ?C _ ] => by good Hfill IHK
+ | [ |- exists x, ?C _ _ = ?C _ _ ] => by good Hfill IHK
+ | [ |- exists x, ?C _ _ _ = ?C _ _ _ ] => by good Hfill IHK
+ | [ |- exists x, ?C _ _ _ _ = ?C _ _ _ _ ] => by good Hfill IHK
+ | [ |- exists x, ?C _ _ _ _ _ = ?C _ _ _ _ _ ] => by good Hfill IHK
+ | [ |- exists x, ?C _ _ _ _ _ _ = ?C _ _ _ _ _ _ ] => by good Hfill IHK
+ | _ => by bad_fill Hfill
+ end).
Qed.
End step_by_value.
--
GitLab