From 564fb33a504d7611d73bbe5e20b23453e141ed3d Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sun, 2 May 2021 11:12:45 +0100 Subject: Simplify some HTLgenspec proofs --- src/common/Vericertlib.v | 5 +++++ src/hls/HTLgenspec.v | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index c537cef..722edef 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -57,6 +57,11 @@ Ltac learn_tac fact name := Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name. Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name. +Ltac auto_hyp H := + match goal with + | H' : _ |- _ => solve [ apply H in H'; auto | auto ] + end. + Ltac unfold_rec c := unfold c; fold c. Ltac solve_by_inverts n := diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 77e8c3d..f3c375c 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -222,7 +222,7 @@ Lemma map_externctrl_datapath_trans : map_externctrl om sig s = OK x s' i -> s.(st_datapath) = s'.(st_datapath). Proof. - intros. monadInv H. apply create_reg_datapath_trans in EQ. auto. + intros. monadInv H. auto_hyp create_reg_datapath_trans. Qed. Hint Resolve map_externctrl_datapath_trans : htlspec. @@ -231,7 +231,7 @@ Lemma map_externctrl_controllogic_trans : map_externctrl om sig s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic). Proof. - intros. monadInv H. apply create_reg_controllogic_trans in EQ. auto. + intros. monadInv H. auto_hyp create_reg_controllogic_trans. Qed. Hint Resolve map_externctrl_datapath_trans : htlspec. -- cgit