From 7efd47ee7d3ccd9435d7efa26f2b8658ca44579c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 30 Oct 2016 20:13:41 -0400 Subject: Add trueify to src/Util/PartiallyReifiedProp.v --- src/Util/PartiallyReifiedProp.v | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) (limited to 'src/Util/PartiallyReifiedProp.v') diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v index d85473271..c950b0971 100644 --- a/src/Util/PartiallyReifiedProp.v +++ b/src/Util/PartiallyReifiedProp.v @@ -7,7 +7,7 @@ Require Import Crypto.Util.Notations. Require Import Crypto.Util.Tactics. Delimit Scope reified_prop_scope with reified_prop. -Inductive reified_Prop := rTrue | rFalse | rAnd (x y : reified_Prop) | rOr (x y : reified_Prop) | rImpl (x y : reified_Prop) | rForall {T} (f : T -> reified_Prop) | rEq {T} (x y : T) | rEqRefl {T} (x : T) | inject (_ : Prop). +Inductive reified_Prop := rTrue | rFalse | rAnd (x y : reified_Prop) | rOr (x y : reified_Prop) | rImpl (x y : reified_Prop) | rForall {T} (f : T -> reified_Prop) | rEq {T} (x y : T) | inject (_ : Prop). Bind Scope reified_prop_scope with reified_Prop. Fixpoint to_prop (x : reified_Prop) : Prop @@ -19,7 +19,6 @@ Fixpoint to_prop (x : reified_Prop) : Prop | rImpl x y => to_prop x -> to_prop y | @rForall _ f => forall x, to_prop (f x) | @rEq _ x y => x = y - | @rEqRefl _ x => x = x | inject x => x end. @@ -82,10 +81,6 @@ Definition reified_Prop_eq (x y : reified_Prop) eq_rect _ (fun t => t) x0 _ pf = y0 /\ eq_rect _ (fun t => t) x1 _ pf = y1 | rEq _ _ _, _ => False - | @rEqRefl Tx x, @rEqRefl Ty y - => exists pf : Tx = Ty, - eq_rect _ (fun t => t) x _ pf = y - | rEqRefl _ _, _ => False | inject x, inject y => x = y | inject _, _ => False end. @@ -138,7 +133,6 @@ Ltac inversion_reified_Prop_step := | [ H : rImpl _ _ = _ |- _ ] => do_on H | [ H : rForall _ = _ |- _ ] => do_on H | [ H : rEq _ _ = _ |- _ ] => do_on H - | [ H : rEqRefl _ = _ |- _ ] => do_on H | [ H : inject _ = _ |- _ ] => do_on H end. Ltac inversion_reified_Prop := repeat inversion_reified_Prop_step. @@ -148,3 +142,21 @@ Proof. destruct x, y; simpl; try tauto. { split; intro H; inversion H; subst; repeat split. } Qed. + +(** Remove all possibly false terms in a reified prop *) +Fixpoint trueify (p : reified_Prop) : reified_Prop + := match p with + | rTrue => rTrue + | rFalse => rTrue + | rAnd x y => rAnd (trueify x) (trueify y) + | rOr x y => rOr (trueify x) (trueify y) + | rImpl x y => rImpl x (trueify y) + | rForall T f => rForall (fun x => trueify (f x)) + | rEq T x y => rEq x x + | inject x => inject True + end. + +Lemma trueify_true : forall p, to_prop (trueify p). +Proof. + induction p; simpl; auto. +Qed. -- cgit v1.2.3