From 3fbd49b8905cf97e955a6aacdc59913f65c56c5e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 30 Oct 2016 17:24:22 -0400 Subject: Fix a loop in PartiallyReifiedProp --- src/Util/PartiallyReifiedProp.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'src/Util/PartiallyReifiedProp.v') diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v index 2ef332c5b..6733bbb98 100644 --- a/src/Util/PartiallyReifiedProp.v +++ b/src/Util/PartiallyReifiedProp.v @@ -25,14 +25,12 @@ Fixpoint to_prop (x : reified_Prop) : Prop Coercion reified_Prop_of_bool (x : bool) : reified_Prop := if x then rTrue else rFalse. -Fixpoint and_reified_Prop (x y : reified_Prop) : reified_Prop +Definition and_reified_Prop (x y : reified_Prop) : reified_Prop := match x, y with | rTrue, y => y | x, rTrue => x | rFalse, y => rFalse | x, rFalse => rFalse - | rForall T f, y => rForall (fun x => and_reified_Prop (f x) y) - | x, rForall T f => rForall (fun y => rAnd x (f y)) | rEq T a b, rEq T' a' b' => rEq (a, a') (b, b') | x', y' => rAnd x' y' end. @@ -121,12 +119,15 @@ Ltac inversion_reified_Prop_step := match goal with | [ H : False |- _ ] => solve [ destruct H ] | [ H : (_ = _ :> reified_Prop) /\ (_ = _ :> reified_Prop) |- _ ] => destruct H + | [ H : ?x = ?x :> reified_Prop |- _ ] => clear H | [ H : exists pf : _ = _ :> Type, forall x, _ = _ :> reified_Prop |- _ ] => destruct H as [? H]; subst; simpl @eq_rect in H | [ H : ?x = _ :> reified_Prop |- _ ] => is_var x; subst x | [ H : _ = ?y :> reified_Prop |- _ ] => is_var y; subst y - | [ H : rTrue = _ |- _ ] => do_on H - | [ H : rFalse = _ |- _ ] => do_on H + | [ H : rTrue = rFalse |- _ ] => solve [ inversion H ] + | [ H : rFalse = rTrue |- _ ] => solve [ inversion H ] + | [ H : rTrue = _ |- _ ] => do_on H; progress subst + | [ H : rFalse = _ |- _ ] => do_on H; progress subst | [ H : rAnd _ _ = _ |- _ ] => do_on H | [ H : rOr _ _ = _ |- _ ] => do_on H | [ H : rImpl _ _ = _ |- _ ] => do_on H -- cgit v1.2.3